1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Wed Mar 07 13:04:44 2018 +0100
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Wed Mar 07 13:15:21 2018 +0100
1.3 @@ -333,7 +333,7 @@
1.4 | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
1.5 handle _ => error ("prep_pbt: syntax error in '#Where' of " ^ strs2str metID))
1.6 | _ => error ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
1.7 - val sc = (((TermC.inst_abs thy) o Thm.term_of o the o (TermC.parse thy)) scr)
1.8 + val sc = ((TermC.inst_abs o Thm.term_of o the o (TermC.parse thy)) scr)
1.9 val calc = if scr = "empty_script" then [] else LTool.get_calcs thy sc
1.10 in
1.11 ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro,
2.1 --- a/src/Tools/isac/ProgLang/ListC.thy Wed Mar 07 13:04:44 2018 +0100
2.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Wed Mar 07 13:15:21 2018 +0100
2.3 @@ -12,12 +12,6 @@
2.4 ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
2.5 ML {*
2.6 *} ML {*
2.7 -HOLogic.realT;
2.8 -HOLogic.boolT;
2.9 -*} ML {*
2.10 -*} ML {*
2.11 -*} ML {*
2.12 -*} ML {*
2.13 *}
2.14
2.15 subsection {* Notes on Isac's programming language *}
3.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Wed Mar 07 13:04:44 2018 +0100
3.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Wed Mar 07 13:15:21 2018 +0100
3.3 @@ -211,7 +211,7 @@
3.4 (** build up a program from rules **)
3.5
3.6 (* transform type rule to a term *)
3.7 -val ScrStep $ _ $ _ = ((TermC.inst_abs @{theory}) o Thm.term_of o the o (TermC.parse @{theory}))
3.8 +val ScrStep $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory}))
3.9 (*'z not affected by parse: 'a --> real*)
3.10 "Script Stepwise (t_t::'z) =\
3.11 \(Repeat\
3.12 @@ -220,7 +220,7 @@
3.13 \ (Try (Repeat (Rewrite mult_commute False)))) \
3.14 \ t_t)";
3.15 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body are inconsistent !!!*)
3.16 -val ScrStep_inst $ Term $ Bdv $ _= ((TermC.inst_abs @{theory}) o Thm.term_of o the o (TermC.parse @{theory}))
3.17 +val ScrStep_inst $ Term $ Bdv $ _= (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory}))
3.18 (*'z not affected by parse: 'a --> real*)
3.19 "Script Stepwise_inst (t_t::'z) (v::real) =\
3.20 \(Repeat\
3.21 @@ -228,23 +228,23 @@
3.22 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] add_commute False))) @@\
3.23 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] mult_commute False)))) \
3.24 \ t_t)";
3.25 -val Repeat $ _ = ((TermC.inst_abs @{theory}) o Thm.term_of o the o (TermC.parseN @{theory}))
3.26 +val Repeat $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
3.27 "Repeat (Rewrite real_diff_minus False t)";
3.28 -val Try $ _ = ((TermC.inst_abs @{theory}) o Thm.term_of o the o (TermC.parseN @{theory}))
3.29 +val Try $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
3.30 "Try (Rewrite real_diff_minus False t)";
3.31 -val Cal $ _ = ((TermC.inst_abs @{theory}) o Thm.term_of o the o (TermC.parseN @{theory}))
3.32 +val Cal $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
3.33 "Calculate PLUS";
3.34 -val Ca1 $ _ = ((TermC.inst_abs @{theory}) o Thm.term_of o the o (TermC.parseN @{theory}))
3.35 +val Ca1 $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
3.36 "Calculate1 PLUS";
3.37 -val Rew $ (Free (_, IDtype)) $ _ $ _ = ((TermC.inst_abs @{theory}) o Thm.term_of o the o (TermC.parseN @{theory}))
3.38 +val Rew $ (Free (_, IDtype)) $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
3.39 "Rewrite real_diff_minus False t";
3.40 -val Rew_Inst $ Subs $ _ $ _ = ((TermC.inst_abs @{theory}) o Thm.term_of o the o (TermC.parseN @{theory}))
3.41 +val Rew_Inst $ Subs $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
3.42 "Rewrite_Inst [(bdv,v)] real_diff_minus False";
3.43 -val Rew_Set $ _ $ _ = ((TermC.inst_abs @{theory}) o Thm.term_of o the o (TermC.parseN @{theory}))
3.44 +val Rew_Set $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
3.45 "Rewrite_Set real_diff_minus False";
3.46 -val Rew_Set_Inst $ _ $ _ $ _ = ((TermC.inst_abs @{theory}) o Thm.term_of o the o (TermC.parseN @{theory}))
3.47 +val Rew_Set_Inst $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
3.48 "Rewrite_Set_Inst [(bdv,v)] real_diff_minus False";
3.49 -val SEq $ _ $ _ $ _ = ((TermC.inst_abs @{theory}) o Thm.term_of o the o (TermC.parseN @{theory}))
3.50 +val SEq $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
3.51 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
3.52 \ (Try (Repeat (Rewrite add_commute False))) @@ \
3.53 \ (Try (Repeat (Rewrite mult_commute False)))) t";
4.1 --- a/src/Tools/isac/ProgLang/termC.sml Wed Mar 07 13:04:44 2018 +0100
4.2 +++ b/src/Tools/isac/ProgLang/termC.sml Wed Mar 07 13:15:21 2018 +0100
4.3 @@ -13,7 +13,7 @@
4.4 val free2str: term -> string
4.5 val ids2str: term -> string list
4.6 val ins_concl: term -> term -> term
4.7 - val inst_abs: 'a -> term -> term
4.8 + val inst_abs: term -> term
4.9 val inst_bdv: (term * term) list -> term -> term
4.10
4.11 val term_of_num: typ -> int -> term
4.12 @@ -512,16 +512,16 @@
4.13 in subst (t, 0) end;
4.14
4.15 (* instantiate let; necessary for ass_up *)
4.16 -fun inst_abs thy (Const sT) = Const sT (*TODO.WN100907 drop thy*)
4.17 - | inst_abs thy (Free sT) = Free sT
4.18 - | inst_abs thy (Bound n) = Bound n
4.19 - | inst_abs thy (Var iT) = Var iT
4.20 - | inst_abs thy (Const ("HOL.Let",T1) $ e $ (Abs (v, T2, b))) =
4.21 +fun inst_abs (Const sT) = Const sT (*TODO.WN100907 drop thy*)
4.22 + | inst_abs (Free sT) = Free sT
4.23 + | inst_abs (Bound n) = Bound n
4.24 + | inst_abs (Var iT) = Var iT
4.25 + | inst_abs (Const ("HOL.Let",T1) $ e $ (Abs (v, T2, b))) =
4.26 let val b' = subst_bound (Free (v, T2), b);
4.27 (*fun variant_abs: term.ML*)
4.28 - in Const ("HOL.Let", T1) $ inst_abs thy e $ (Abs (v, T2, inst_abs thy b')) end
4.29 - | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
4.30 - | inst_abs thy t = t;
4.31 + in Const ("HOL.Let", T1) $ inst_abs e $ (Abs (v, T2, inst_abs b')) end
4.32 + | inst_abs (t1 $ t2) = inst_abs t1 $ inst_abs t2
4.33 + | inst_abs t = t;
4.34 (*val scr =
4.35 "Script Make_fun_by_explicit (f_::real) (v_::real) (eqs_::bool list) = \
4.36 \ (let h_ = (hd o (filterVar f_)) eqs_; \
5.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Wed Mar 07 13:04:44 2018 +0100
5.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Wed Mar 07 13:15:21 2018 +0100
5.3 @@ -197,7 +197,7 @@
5.4 if term = e_term
5.5 then indt j ^"<SCRIPT> </SCRIPT>\n"
5.6 else indt j ^"<SCRIPT>\n"^
5.7 - term2xml j (TermC.inst_abs (assoc_thy "Isac") term) ^ "\n" ^
5.8 + term2xml j (TermC.inst_abs term) ^ "\n" ^
5.9 indt j ^"</SCRIPT>\n"
5.10 | scr2xml j (Rfuns _) =
5.11 indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
5.12 @@ -513,7 +513,7 @@
5.13 | xml_of_src (Prog term) =
5.14 XML.Elem (("CODE", []), [
5.15 if term = e_term then xml_of_src EmptyScr
5.16 - else xml_of_term (TermC.inst_abs (assoc_thy "Isac") term)])
5.17 + else xml_of_term (TermC.inst_abs term)])
5.18 | xml_of_src (Rfuns _) =
5.19 XML.Elem (("NOCODE", []), [XML.Text "reverse rewrite functions"])
5.20