1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 08 13:21:19 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 08 14:24:38 2020 +0200
1.3 @@ -21,14 +21,14 @@
1.4 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.5
1.6 | CAScmd' of term
1.7 - | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
1.8 + | Calculate' of ThyC.theory' * string * term * (term * Celem.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
1.13 | Derive' of Rule_Set.T
1.14 - | Detail_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
1.15 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.16 + | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.17 + | Detail_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.18 | End_Detail' of Selem.result
1.19
1.20 | Empty_Tac_
1.21 @@ -38,16 +38,16 @@
1.22 | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
1.23 | Or_to_List' of term * term
1.24 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
1.25 - | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
1.26 + | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.domID * Celem.metID * Model.itm list
1.27
1.28 - | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
1.29 - | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.30 - | Rewrite_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
1.31 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.32 + | Rewrite' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
1.33 + | Rewrite_Inst' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.34 + | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.35 + | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.36
1.37 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
1.38 | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
1.39 - | Specify_Theory' of Rule.domID
1.40 + | Specify_Theory' of ThyC.domID
1.41 | Subproblem' of
1.42 Celem.spec * Model.ori list *
1.43 term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
1.44 @@ -98,8 +98,8 @@
1.45
1.46 | Specify_Method of Celem.metID
1.47 | Specify_Problem of Celem.pblID
1.48 - | Specify_Theory of Rule.domID
1.49 - | Subproblem of Rule.domID * Celem.pblID
1.50 + | Specify_Theory of ThyC.domID
1.51 + | Subproblem of ThyC.domID * Celem.pblID
1.52
1.53 | Substitute of Selem.sube
1.54 | Tac of string
1.55 @@ -190,8 +190,8 @@
1.56
1.57 | Specify_Method of Celem.metID
1.58 | Specify_Problem of Celem.pblID
1.59 - | Specify_Theory of Rule.domID
1.60 - | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *)
1.61 + | Specify_Theory of ThyC.domID
1.62 + | Subproblem of ThyC.domID * Celem.pblID (* WN0509 drop *)
1.63
1.64 | Substitute of Selem.sube
1.65 | Tac of string (* WN0509 drop *)
1.66 @@ -351,7 +351,7 @@
1.67 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.68 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.69 | CAScmd' of term
1.70 - | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
1.71 + | Calculate' of ThyC.theory' * string * term * (term * Celem.thm')
1.72 | Check_Postcond' of Celem.pblID *
1.73 term (* returnvalue of program in solve *)
1.74 | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
1.75 @@ -361,8 +361,8 @@
1.76 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
1.77
1.78 | Derive' of Rule_Set.T
1.79 - | Detail_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
1.80 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.81 + | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.82 + | Detail_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.83 | End_Detail' of Selem.result
1.84
1.85 | Empty_Tac_
1.86 @@ -378,20 +378,20 @@
1.87 | Refine_Tacitly' of
1.88 Celem.pblID * (* input *)
1.89 Celem.pblID * (* the refined from applicable_in *)
1.90 - Rule.domID * (* from new pbt?! filled in specify *)
1.91 + ThyC.domID * (* from new pbt?! filled in specify *)
1.92 Celem.metID * (* from new pbt?! filled in specify *)
1.93 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
1.94 - | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
1.95 - | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.96 - | Rewrite_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
1.97 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.98 + | Rewrite' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
1.99 + | Rewrite_Inst' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.100 + | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.101 + | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.102
1.103 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
1.104 | Specify_Problem' of Celem.pblID *
1.105 (bool * (* matches *)
1.106 (Model.itm list * (* ppc *)
1.107 (bool * term) list)) (* preconditions marked true/false *)
1.108 - | Specify_Theory' of Rule.domID
1.109 + | Specify_Theory' of ThyC.domID
1.110 | Subproblem' of
1.111 Celem.spec *
1.112 (Model.ori list) * (* filled in associate Subproblem' *)