equal
deleted
inserted
replaced
581 gtfx |
581 gtfx |
582 end |
582 end |
583 |
583 |
584 fun input_types thyname (Elem("tylist",[("i",i)],xtys)) = |
584 fun input_types thyname (Elem("tylist",[("i",i)],xtys)) = |
585 let |
585 let |
586 val types = Array.array(valOf (Int.fromString i),XMLty (Elem("",[],[]))) |
586 val types = Array.array(the (Int.fromString i),XMLty (Elem("",[],[]))) |
587 fun IT _ [] = () |
587 fun IT _ [] = () |
588 | IT n (xty::xtys) = |
588 | IT n (xty::xtys) = |
589 (Array.update(types,n,XMLty xty); |
589 (Array.update(types,n,XMLty xty); |
590 IT (n+1) xtys) |
590 IT (n+1) xtys) |
591 val _ = IT 0 xtys |
591 val _ = IT 0 xtys |
648 gtfx |
648 gtfx |
649 end |
649 end |
650 |
650 |
651 fun input_terms thyname types (Elem("tmlist",[("i",i)],xtms)) = |
651 fun input_terms thyname types (Elem("tmlist",[("i",i)],xtms)) = |
652 let |
652 let |
653 val terms = Array.array(valOf(Int.fromString i),XMLtm (Elem("",[],[]))) |
653 val terms = Array.array(the (Int.fromString i), XMLtm (Elem("",[],[]))) |
654 |
654 |
655 fun IT _ [] = () |
655 fun IT _ [] = () |
656 | IT n (xtm::xtms) = |
656 | IT n (xtm::xtms) = |
657 (Array.update(terms,n,XMLtm xtm); |
657 (Array.update(terms,n,XMLtm xtm); |
658 IT (n+1) xtms) |
658 IT (n+1) xtms) |
1237 val sub = Substring.full str |
1237 val sub = Substring.full str |
1238 val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub) |
1238 val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub) |
1239 val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f) |
1239 val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f) |
1240 in |
1240 in |
1241 if not (idx = "") andalso u = "_" |
1241 if not (idx = "") andalso u = "_" |
1242 then SOME (newstr,valOf(Int.fromString idx)) |
1242 then SOME (newstr, the (Int.fromString idx)) |
1243 else NONE |
1243 else NONE |
1244 end |
1244 end |
1245 handle _ => NONE (* FIXME avoid handle _ *) |
1245 handle _ => NONE (* FIXME avoid handle _ *) |
1246 |
1246 |
1247 fun rewrite_hol4_term t thy = |
1247 fun rewrite_hol4_term t thy = |
1912 val spaces = space_implode " " |
1912 val spaces = space_implode " " |
1913 |
1913 |
1914 fun new_definition thyname constname rhs thy = |
1914 fun new_definition thyname constname rhs thy = |
1915 let |
1915 let |
1916 val constname = rename_const thyname thy constname |
1916 val constname = rename_const thyname thy constname |
1917 val redeclared = isSome (Sign.const_type thy (Sign.intern_const thy constname)); |
1917 val redeclared = is_some (Sign.const_type thy (Sign.intern_const thy constname)); |
1918 val _ = warning ("Introducing constant " ^ constname) |
1918 val _ = warning ("Introducing constant " ^ constname) |
1919 val (thmname,thy) = get_defname thyname constname thy |
1919 val (thmname,thy) = get_defname thyname constname thy |
1920 val (info,rhs') = disamb_term rhs |
1920 val (info,rhs') = disamb_term rhs |
1921 val ctype = type_of rhs' |
1921 val ctype = type_of rhs' |
1922 val csyn = mk_syn thy constname |
1922 val csyn = mk_syn thy constname |