1.1 --- a/src/Tools/isac/Interpret/ctree.sml Sat May 21 09:54:39 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/ctree.sml Sat May 21 12:52:59 2011 +0200
1.3 @@ -523,97 +523,95 @@
1.4 (* tac_ is made from tac in applicable_in,
1.5 and carries all data necessary for generate *)
1.6 datatype tac_ =
1.7 - Init_Proof' of ((cterm' list) * spec)
1.8 -| Model_Problem' of pblID *
1.9 - itm list * (*the 'untouched' pbl*)
1.10 - itm list (*the casually completed met*)
1.11 -| Refine_Tacitly' of pblID * (*input*)
1.12 - pblID * (*the refined from applicable_in*)
1.13 - domID * (*from new pbt?! filled in specify*)
1.14 - metID * (*from new pbt?! filled in specify*)
1.15 - itm list (*drop ! 9.03: remains [] for
1.16 + Init_Proof' of ((cterm' list) * spec)
1.17 + | Model_Problem' of
1.18 + pblID *
1.19 + itm list * (*the 'untouched' pbl*)
1.20 + itm list (*the casually completed met*)
1.21 + | Refine_Tacitly' of
1.22 + pblID * (*input*)
1.23 + pblID * (*the refined from applicable_in*)
1.24 + domID * (*from new pbt?! filled in specify*)
1.25 + metID * (*from new pbt?! filled in specify*)
1.26 + itm list (*drop ! 9.03: remains [] for
1.27 Model_Problem recognizing its activation*)
1.28 -| Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
1.29 - (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)
1.30 -| Add_Given' of cterm' *
1.31 - itm list (*updated with input in fun specify_additem*)
1.32 -| Add_Find' of cterm' *
1.33 - itm list (*updated with input in fun specify_additem*)
1.34 -| Add_Relation' of cterm' *
1.35 - itm list (*updated with input in fun specify_additem*)
1.36 -| Del_Given' of cterm' | Del_Find' of cterm' | Del_Relation' of cterm'
1.37 - (*4.00.: all.. term: in applicable_in ..? Syn ?only for FormFK?*)
1.38 -
1.39 -| Specify_Theory' of domID
1.40 -| Specify_Problem' of (pblID * (* *)
1.41 - (bool * (* matches *)
1.42 - (itm list * (* ppc *)
1.43 - (bool * term) list))) (* preconditions *)
1.44 -| Specify_Method' of metID *
1.45 - ori list * (*repl. "#undef"*)
1.46 - itm list (*... updated from pbl to met*)
1.47 -| Apply_Method' of metID *
1.48 - (term option) * (*init_form*)
1.49 - istate * Proof.context
1.50 -| Check_Postcond' of
1.51 - pblID *
1.52 - (term * (*returnvalue of script in solve*)
1.53 - term list) (*collect by get_assumptions_ in applicable_in, except if
1.54 + | Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
1.55 + (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)
1.56 + | Add_Given' of
1.57 + cterm' *
1.58 + itm list (*updated with input in fun specify_additem*)
1.59 + | Add_Find' of cterm' * itm list (* see Add_Given' *)
1.60 + | Add_Relation' of cterm' * itm list (* see Add_Given' *)
1.61 + | Del_Given' of cterm' | Del_Find' of cterm' | Del_Relation' of cterm'
1.62 + (*4.00.: all.. term: in applicable_in ..? Syn ?only for FormFK?*)
1.63 + | Specify_Theory' of domID
1.64 + | Specify_Problem' of
1.65 + (pblID * (* *)
1.66 + (bool * (* matches *)
1.67 + (itm list * (* ppc *)
1.68 + (bool * term) list))) (* preconditions *)
1.69 + | Specify_Method' of
1.70 + metID *
1.71 + ori list * (*repl. "#undef"*)
1.72 + itm list (*... updated from pbl to met*)
1.73 + | Apply_Method' of
1.74 + metID *
1.75 + (term option) * (*init_form*)
1.76 + istate * Proof.context
1.77 + | Check_Postcond' of
1.78 + pblID *
1.79 + (term * (*returnvalue of script in solve*)
1.80 + term list) (*collect by get_assumptions_ in applicable_in, except if
1.81 butlast tac is Check_elementwise: take only these asms*)
1.82 -| Free_Solve'
1.83 -
1.84 -| Rewrite_Inst' of theory' * rew_ord' * rls
1.85 - * bool * subst * thm' * term * (term * term list)
1.86 -| Rewrite' of theory' * rew_ord' * rls * bool * thm' *
1.87 - term * (term * term list)
1.88 -| Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' *
1.89 - term * (term * term list)
1.90 -| Rewrite_Set_Inst' of theory' * bool * subst * rls *
1.91 - term * (term * term list)
1.92 -| Detail_Set_Inst' of theory' * bool * subst * rls *
1.93 - term * (term * term list)
1.94 -| Rewrite_Set' of theory' * bool * rls * term * (term * term list)
1.95 -| Detail_Set' of theory' * bool * rls * term * (term * term list)
1.96 -| End_Detail' of (term * (term list)) (*see End_Trans'*)
1.97 -| End_Ruleset' of term
1.98 -| Derive' of rls
1.99 -| Calculate' of theory' * string * term * (term * thm')
1.100 - (*WN.29.4.03 asm?: * term list??*)
1.101 -| Substitute' of subte (*the 'substitution': terms of type bool*)
1.102 - * term (*to be substituted in*)
1.103 - * term (*resulting from the substitution*)
1.104 -| Apply_Assumption' of term list * term
1.105 -
1.106 -| Take' of term | Take_Inst' of term
1.107 -| Group' of (con * int list * term)
1.108 -| Subproblem' of (spec *
1.109 - (ori list) * (* filled in assod Subproblem' *)
1.110 - term * (*-"-, headline of calc-head *)
1.111 - fmz_ *
1.112 - Proof.context *(* transported from assod to generate1 *)
1.113 - term) (* Subproblem(dom,pbl) OR cascmd*)
1.114 -| CAScmd' of term
1.115 -| End_Subproblem' of term (*???*)
1.116 -| Split_And' of term | Conclude_And' of term
1.117 -| Split_Or' of term | Conclude_Or' of term
1.118 -| Begin_Trans' of term | End_Trans' of (term * (term list))
1.119 -| Begin_Sequ' | End_Sequ'(* substitute root.env*)
1.120 -| Split_Intersect' of term | End_Intersect' of term
1.121 -| Check_elementwise' of (*special case:*)
1.122 - term * (*(1)the current formula: [x=1,x=...]*)
1.123 - string * (*(2)the pred from Check_elementwise *)
1.124 - (term * (*(3)composed from (1) and (2): {x. pred}*)
1.125 - term list) (*20.5.03 assumptions*)
1.126 -
1.127 -| Or_to_List' of term * term (* (a | b, [a,b]) *)
1.128 -| Collect_Trues' of term
1.129 -
1.130 -| Empty_Tac_ | Tac_ of (*for dummies*)
1.131 - theory *
1.132 - string * (*form*)
1.133 - string * (*in Tac*)
1.134 - string (*result of Tac".."*)
1.135 -| User' (*internal for ets*) | End_Proof'';(*End_Proof:inout*)
1.136 + | Free_Solve'
1.137 + | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm' * term * (term * term list)
1.138 + | Rewrite' of theory' * rew_ord' * rls * bool * thm' * term * (term * term list)
1.139 + | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' * term * (term * term list)
1.140 + | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
1.141 + | Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
1.142 + | Rewrite_Set' of theory' * bool * rls * term * (term * term list)
1.143 + | Detail_Set' of theory' * bool * rls * term * (term * term list)
1.144 + | End_Detail' of (term * (term list)) (*see End_Trans'*)
1.145 + | End_Ruleset' of term
1.146 + | Derive' of rls
1.147 + | Calculate' of theory' * string * term * (term * thm')
1.148 + | Substitute' of
1.149 + subte * (*the 'substitution': terms of type bool*)
1.150 + term * (*to be substituted in*)
1.151 + term (*resulting from the substitution*)
1.152 + | Apply_Assumption' of term list * term
1.153 + | Take' of term
1.154 + | Take_Inst' of term
1.155 + | Group' of (con * int list * term)
1.156 + | Subproblem' of
1.157 + (spec *
1.158 + (ori list) * (* filled in assod Subproblem' *)
1.159 + term * (*-"-, headline of calc-head *)
1.160 + fmz_ *
1.161 + Proof.context *(* transported from assod to generate1 *)
1.162 + term) (* Subproblem(dom,pbl) OR cascmd*)
1.163 + | CAScmd' of term
1.164 + | End_Subproblem' of term (*???*)
1.165 + | Split_And' of term | Conclude_And' of term
1.166 + | Split_Or' of term | Conclude_Or' of term
1.167 + | Begin_Trans' of term | End_Trans' of (term * (term list))
1.168 + | Begin_Sequ' | End_Sequ'(* substitute root.env*)
1.169 + | Split_Intersect' of term | End_Intersect' of term
1.170 + | Check_elementwise' of (*special case:*)
1.171 + term * (*(1)the current formula: [x=1,x=...]*)
1.172 + string * (*(2)the pred from Check_elementwise *)
1.173 + (term * (*(3)composed from (1) and (2): {x. pred}*)
1.174 + term list) (*20.5.03 assumptions*)
1.175 + | Or_to_List' of term * term (* (a | b, [a,b]) *)
1.176 + | Collect_Trues' of term
1.177 + | Empty_Tac_
1.178 + | Tac_ of (*for dummies*)
1.179 + theory *
1.180 + string * (*form*)
1.181 + string * (*in Tac*)
1.182 + string (*result of Tac".."*)
1.183 + | User' (*internal for ets FIXME.WN110521 delete this and check occurrences of others*)
1.184 + | End_Proof'';(*End_Proof:inout*)
1.185
1.186 fun tac_2str ma = case ma of
1.187 Init_Proof' (ppc, spec) =>