1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 09:15:39 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 10:57:04 2020 +0200
1.3 @@ -39,15 +39,9 @@
1.4 | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
1.5 (*RM*)| Tac_ of theory * string * string * string
1.6 | Take' of term
1.7 -(*RM* )| Take_Inst of TermC.as_string( *RM*)
1.8 -(*RM*)| Begin_Sequ' | Begin_Trans' of term
1.9 -(*RM*)| Split_And' of term | Split_Or' of term | Split_Intersect' of term
1.10 -(*RM*)| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
1.11 -(*RM*)| End_Sequ' | End_Trans' of Selem.result
1.12 -(*RM*)| End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.13 -(*RM*)| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.14 -(*RM*)| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
1.15 -(*RM*)| End_Detail' of Selem.result;
1.16 + | End_Detail' of Selem.result
1.17 + | Begin_Trans' of term | End_Trans' of Selem.result
1.18 + | End_Proof''
1.19
1.20 val string_of: T -> string
1.21
1.22 @@ -81,15 +75,8 @@
1.23 | Substitute of Subst.input
1.24 (*RM*)| Tac of string
1.25 | Take of TermC.as_string
1.26 -(*RM*)| Take_Inst of TermC.as_string
1.27 -(*RM*)| Begin_Sequ | Begin_Trans
1.28 -(*RM*)| Split_And | Split_Or | Split_Intersect
1.29 -(*RM*)| Conclude_And | Conclude_Or | Collect_Trues
1.30 -(*RM*)| End_Sequ | End_Trans
1.31 -(*RM*)| End_Ruleset | End_Subproblem | End_Intersect
1.32 -(*RM*)| Detail_Set of Rule_Set.id
1.33 -(*RM*)| Detail_Set_Inst of Subst.input * Rule_Set.id
1.34 -(*RM*)| End_Detail
1.35 + | End_Detail
1.36 + | Begin_Trans | End_Trans
1.37 | End_Proof';
1.38
1.39 val input_to_string : input -> string
1.40 @@ -156,15 +143,8 @@
1.41 | Substitute of Subst.input
1.42 (*RM*)| Tac of string
1.43 | Take of TermC.as_string
1.44 -(*RM*)| Take_Inst of TermC.as_string
1.45 -(*RM*)| Begin_Sequ | Begin_Trans
1.46 -(*RM*)| Split_And | Split_Or | Split_Intersect
1.47 -(*RM*)| Conclude_And | Conclude_Or | Collect_Trues
1.48 -(*RM*)| End_Sequ | End_Trans
1.49 -(*RM*)| End_Ruleset | End_Subproblem | End_Intersect
1.50 -(*RM*)| Detail_Set of Rule_Set.id
1.51 -(*RM*)| Detail_Set_Inst of Subst.input * Rule_Set.id
1.52 -(*RM*)| End_Detail
1.53 + | End_Detail
1.54 + | Begin_Trans | End_Trans
1.55 | End_Proof';
1.56
1.57 fun input_to_string ma = case ma of
1.58 @@ -193,8 +173,6 @@
1.59 | Rewrite_Set_Inst (subs, rls) =>
1.60 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
1.61 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
1.62 - | Detail_Set rls => "Detail_Set " ^ quote rls
1.63 - | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
1.64 | End_Detail => "End_Detail"
1.65 | Derive rls' => "Derive " ^ rls'
1.66 | Calculate op_ => "Calculate " ^ op_
1.67 @@ -202,7 +180,6 @@
1.68 | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
1.69
1.70 | Take cterm' => "Take " ^ quote cterm'
1.71 - | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
1.72 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
1.73 | End_Subproblem => "End_Subproblem"
1.74 | CAScmd cterm' => "CAScmd " ^ quote cterm'
1.75 @@ -238,15 +215,12 @@
1.76 | Rewrite _ => "Rewrite"
1.77 | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
1.78 | Rewrite_Set _ => "Rewrite_Set"
1.79 - | Detail_Set _ => "Detail_Set"
1.80 - | Detail_Set_Inst _ => "Detail_Set_Inst"
1.81 | Derive _ => "Derive "
1.82 | Calculate _ => "Calculate "
1.83 | Substitute _ => "Substitute"
1.84 | Apply_Assumption _ => "Apply_Assumption"
1.85
1.86 | Take _ => "Take"
1.87 - | Take_Inst _ => "Take_Inst"
1.88 | Subproblem _ => "Subproblem"
1.89 | End_Subproblem => "End_Subproblem"
1.90 | CAScmd _ => "CAScmd"
1.91 @@ -377,7 +351,6 @@
1.92 (*RM*)| Derive' of Rule_Set.T
1.93 | Empty_Tac_
1.94 | Free_Solve'
1.95 -(*RM* )| Apply_Assumption of TermC.as_string list( *RM*)
1.96 | Or_to_List' of term * term
1.97 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
1.98 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
1.99 @@ -398,14 +371,9 @@
1.100 term (* resulting from the substitution *)
1.101 (*RM*)| Tac_ of theory * string * string * string
1.102 | Take' of term
1.103 -(*RM*)| Begin_Sequ' | Begin_Trans' of term
1.104 -(*RM*)| Split_And' of term | Split_Or' of term | Split_Intersect' of term
1.105 -(*RM*)| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
1.106 -(*RM*)| End_Sequ' | End_Trans' of Selem.result
1.107 -(*RM*)| End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.108 -(*RM*)| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.109 -(*RM*)| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
1.110 -(*RM*)| End_Detail' of Selem.result;
1.111 + | End_Detail' of Selem.result
1.112 + | Begin_Trans' of term | End_Trans' of Selem.result
1.113 + | End_Proof''
1.114
1.115 fun string_of ma = case ma of
1.116 Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.to_string spec)
1.117 @@ -438,8 +406,6 @@
1.118 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
1.119 "," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ "," ^ UnparseC.terms asm ^ "))"
1.120 | End_Detail' _ => "End_Detail' xxx"
1.121 - | Detail_Set' _ => "Detail_Set' xxx"
1.122 - | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
1.123
1.124 | Derive' rls => "Derive' " ^ Rule_Set.id rls
1.125 | Calculate' _ => "Calculate' "
1.126 @@ -452,6 +418,10 @@
1.127
1.128 | Empty_Tac_ => "Empty_Tac_"
1.129 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
1.130 +
1.131 + | Begin_Trans' _ => "Begin_Trans' xxx"
1.132 + | End_Trans' _ => "End_Trans' xxx"
1.133 + | End_Proof'' => "End_Trans' xxx"
1.134 | _ => "string_of not impl. for arg";
1.135
1.136 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
1.137 @@ -468,12 +438,8 @@
1.138 | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Subst.T_to_input sub, thm)
1.139
1.140 | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)
1.141 - | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id rls)
1.142 -
1.143 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
1.144 Rewrite_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
1.145 - | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
1.146 - Detail_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
1.147
1.148 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
1.149 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred