1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Sun Feb 25 16:31:17 2018 +0100
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Fri Mar 02 14:19:59 2018 +0100
1.3 @@ -67,7 +67,7 @@
1.4 open Model
1.5
1.6 type field = string * (term * term)
1.7 -val dsc_unknown = (Thm.term_of o the o (parseold @{theory Script})) "unknown::'a => unknow";
1.8 +val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory Script})) "unknown::'a => unknow";
1.9
1.10 fun itm_2item (_: theory) (Model.Cor ((d, ts), _)) = Model.Correct (term2str (Model.comp_dts (d, ts)))
1.11 | itm_2item _ (Model.Syn c) = Model.SyntaxE c
1.12 @@ -192,7 +192,7 @@
1.13 | prep_ori fmz thy pbt =
1.14 let
1.15 val ctxt = Proof_Context.init_global thy |> fold Stool.declare_constraints fmz;
1.16 - val ori = map (add_field thy pbt o Model.split_dts o the o parseNEW ctxt) fmz |> add_variants;
1.17 + val ori = map (add_field thy pbt o Model.split_dts o the o TermC.parseNEW ctxt) fmz |> add_variants;
1.18 val maxv = map fst ori |> max;
1.19 val maxv = if maxv = 0 then 1 else maxv;
1.20 val oris = coll_variants ori
1.21 @@ -201,8 +201,8 @@
1.22 |> map flattup;
1.23 in (oris, ctxt) end;
1.24
1.25 -val e_errpat = ("e_errpatID", [parse_patt @{theory} "?a = ?b"], [@{thm refl}]): errpat
1.26 -val e_fillpat = ("e_fillpatID", parse_patt @{theory} "?a = _", "e_errpatID")
1.27 +val e_errpat = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}]): errpat
1.28 +val e_fillpat = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")
1.29
1.30 (** breadth-first search on hierarchy of problem-types **)
1.31
1.32 @@ -261,7 +261,7 @@
1.33 val gi = filter (eq "#Given") dsc_dats;
1.34 val gi = (case gi of
1.35 [] => []
1.36 - | ((_, gi') :: []) => (map (split_did o Thm.term_of o the o (parse thy)) gi'
1.37 + | ((_, gi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) gi'
1.38 handle _ => error ("prep_pbt: syntax error in '#Given' of " ^ strs2str pblID))
1.39 | _ => error ("prep_pbt: more than one '#Given' in " ^ strs2str pblID));
1.40 val gi = map (pair "#Given") gi;
1.41 @@ -269,7 +269,7 @@
1.42 val fi = filter (eq "#Find") dsc_dats;
1.43 val fi = (case fi of
1.44 [] => []
1.45 - | ((_, fi') :: []) => (map (split_did o Thm.term_of o the o (parse thy)) fi'
1.46 + | ((_, fi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) fi'
1.47 handle _ => error ("prep_pbt: syntax error in '#Find' of " ^ strs2str pblID))
1.48 | _ => error ("prep_pbt: more than one '#Find' in " ^ strs2str pblID));
1.49 val fi = map (pair "#Find") fi;
1.50 @@ -277,7 +277,7 @@
1.51 val re = filter (eq "#Relate") dsc_dats;
1.52 val re = (case re of
1.53 [] => []
1.54 - | ((_, re') :: []) => (map (split_did o Thm.term_of o the o (parse thy)) re'
1.55 + | ((_, re') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) re'
1.56 handle _ => error ("prep_pbt: syntax error in '#Relate' of " ^ strs2str pblID))
1.57 | _ => error ("prep_pbt: more than one '#Relate' in " ^ strs2str pblID));
1.58 val re = map (pair "#Relate") re;
1.59 @@ -285,14 +285,14 @@
1.60 val wh = filter (eq "#Where") dsc_dats;
1.61 val wh = (case wh of
1.62 [] => []
1.63 - | ((_, wh') :: []) => (map (parse_patt thy) wh'
1.64 + | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
1.65 handle _ => error ("prep_pbt: syntax error in '#Where' of " ^ strs2str pblID))
1.66 | _ => error ("prep_pbt: more than one '#Where' in " ^ strs2str pblID));
1.67 in
1.68 ({guh = guh, mathauthors = maa, init = init, thy = thy,
1.69 cas= case ca of
1.70 NONE => NONE
1.71 - | SOME s => SOME ((Thm.term_of o the o (parse thy)) s),
1.72 + | SOME s => SOME ((Thm.term_of o the o (TermC.parse thy)) s),
1.73 prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID): pbt * pblID
1.74 end;
1.75
1.76 @@ -306,7 +306,7 @@
1.77 val gi = filter (eq "#Given") ppc;
1.78 val gi = (case gi of
1.79 [] => (writeln ("prep_met: in " ^ guh ^ " #Given is empty ?!?"); [])
1.80 - | ((_, gi') :: []) => (map (split_did o Thm.term_of o the o (parse thy)) gi'
1.81 + | ((_, gi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) gi'
1.82 handle _ => error ("prep_pbt: syntax error in '#Given' of " ^ strs2str metID))
1.83 | _ => error ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
1.84 val gi = map (pair "#Given") gi;
1.85 @@ -314,7 +314,7 @@
1.86 val fi = filter (eq "#Find") ppc;
1.87 val fi = (case fi of
1.88 [] => (writeln ("prep_met: in " ^ guh ^ " #Find is empty ?!?"); [])
1.89 - | ((_, fi') :: []) => (map (split_did o Thm.term_of o the o (parse thy)) fi'
1.90 + | ((_, fi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) fi'
1.91 handle _ => error ("prep_pbt: syntax error in '#Find' of " ^ strs2str metID))
1.92 | _ => error ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
1.93 val fi = map (pair "#Find") fi;
1.94 @@ -322,7 +322,7 @@
1.95 val re = filter (eq "#Relate") ppc;
1.96 val re = (case re of
1.97 [] => (writeln ("prep_met: in " ^ guh ^ " #Relate is empty ?!?"); [])
1.98 - | ((_,re') :: []) => (map (split_did o Thm.term_of o the o (parse thy)) re'
1.99 + | ((_,re') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) re'
1.100 handle _ => error ("prep_pbt: syntax error in '#Relate' of " ^ strs2str metID))
1.101 | _ => error ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
1.102 val re = map (pair "#Relate") re;
1.103 @@ -330,10 +330,10 @@
1.104 val wh = filter (eq "#Where") ppc;
1.105 val wh = (case wh of
1.106 [] => (writeln ("prep_met: in " ^ guh ^ " #Where is empty ?!?"); [])
1.107 - | ((_, wh') :: []) => (map (parse_patt thy) wh'
1.108 + | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
1.109 handle _ => error ("prep_pbt: syntax error in '#Where' of " ^ strs2str metID))
1.110 | _ => error ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
1.111 - val sc = (((inst_abs thy) o Thm.term_of o the o (parse thy)) scr)
1.112 + val sc = (((TermC.inst_abs thy) o Thm.term_of o the o (TermC.parse thy)) scr)
1.113 val calc = if scr = "empty_script" then [] else LTool.get_calcs thy sc
1.114 in
1.115 ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro,