1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Thu Apr 09 12:03:14 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Thu Apr 09 17:13:17 2020 +0200
1.3 @@ -21,7 +21,7 @@
1.4 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.5
1.6 | CAScmd' of term
1.7 - | Calculate' of ThyC.theory' * string * term * (term * Celem.thm')
1.8 + | Calculate' of ThyC.theory' * string * term * (term * ThmC.thm')
1.9 | Check_Postcond' of Celem.pblID * term
1.10 | Check_elementwise' of term * Rule.cterm' * Selem.result
1.11 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
1.12 @@ -40,8 +40,8 @@
1.13 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
1.14 | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.domID * Celem.metID * Model.itm list
1.15
1.16 - | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
1.17 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.18 + | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.thm'' * term * Selem.result
1.19 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Rule.subst * ThmC.thm'' * term * Selem.result
1.20 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.21 | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.22
1.23 @@ -91,8 +91,8 @@
1.24 | Refine_Problem of Celem.pblID
1.25 | Refine_Tacitly of Celem.pblID
1.26
1.27 - | Rewrite of Celem.thm''
1.28 - | Rewrite_Inst of Selem.subs * Celem.thm''
1.29 + | Rewrite of ThmC.thm''
1.30 + | Rewrite_Inst of Selem.subs * ThmC.thm''
1.31 | Rewrite_Set of Rule_Set.identifier
1.32 | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
1.33
1.34 @@ -183,8 +183,8 @@
1.35 because there all the thms are present with both (thmID, thm)
1.36 (where user-views can show both or only one of (thmID, thm)),
1.37 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
1.38 - | Rewrite of Celem.thm''
1.39 - | Rewrite_Inst of Selem.subs * Celem.thm''
1.40 + | Rewrite of ThmC.thm''
1.41 + | Rewrite_Inst of Selem.subs * ThmC.thm''
1.42 | Rewrite_Set of Rule_Set.identifier
1.43 | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
1.44
1.45 @@ -218,8 +218,8 @@
1.46 | Free_Solve => "Free_Solve"
1.47
1.48 | Rewrite_Inst (subs, (id, thm)) =>
1.49 - "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> Rule.term2str)))
1.50 - | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
1.51 + "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> UnparseC.term2str)))
1.52 + | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> UnparseC.term2str)
1.53 | Rewrite_Set_Inst (subs, rls) =>
1.54 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
1.55 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
1.56 @@ -351,7 +351,7 @@
1.57 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.58 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.59 | CAScmd' of term
1.60 - | Calculate' of ThyC.theory' * string * term * (term * Celem.thm')
1.61 + | Calculate' of ThyC.theory' * string * term * (term * ThmC.thm')
1.62 | Check_Postcond' of Celem.pblID *
1.63 term (* returnvalue of program in solve *)
1.64 | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
1.65 @@ -381,8 +381,8 @@
1.66 ThyC.domID * (* from new pbt?! filled in specify *)
1.67 Celem.metID * (* from new pbt?! filled in specify *)
1.68 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
1.69 - | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
1.70 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.71 + | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.thm'' * term * Selem.result
1.72 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Rule.subst * ThmC.thm'' * term * Selem.result
1.73 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.74 | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.75
1.76 @@ -429,7 +429,7 @@
1.77
1.78 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
1.79 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
1.80 - (spair2str (strs2str pblID, Rule.term2str scval))
1.81 + (spair2str (strs2str pblID, UnparseC.term2str scval))
1.82
1.83 | Free_Solve' => "Free_Solve'"
1.84
1.85 @@ -437,7 +437,7 @@
1.86 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
1.87 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
1.88 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
1.89 - "," ^ Rule_Set.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
1.90 + "," ^ Rule_Set.id_rls rls' ^ "," ^ UnparseC.term2str f ^ ",(" ^ UnparseC.term2str f' ^ "," ^ UnparseC.terms2str asm ^ "))"
1.91 | End_Detail' _ => "End_Detail' xxx"
1.92 | Detail_Set' _ => "Detail_Set' xxx"
1.93 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
1.94 @@ -480,7 +480,7 @@
1.95 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
1.96
1.97 | input_from_T (Or_to_List' _) = Or_to_List
1.98 - | input_from_T (Take' term) = Take (Rule.term2str term)
1.99 + | input_from_T (Take' term) = Take (UnparseC.term2str term)
1.100 | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Selem.subte2sube subte)
1.101 | input_from_T (Tac_ (_, _, id, _)) = Tac id
1.102