1.1 --- a/src/Tools/isac/Interpret/script.sml Wed May 11 14:58:07 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Wed May 11 16:51:30 2011 +0200
1.3 @@ -437,38 +437,39 @@
1.4 \ REAL_LIST [c, c_2]]";
1.5 *)
1.6 | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $
1.7 - (Const ("Product_Type.Pair",_) $
1.8 - Free (dI',_) $
1.9 - (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
1.10 -(*compare "| assod _ (Subproblem'"*)
1.11 - let val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
1.12 + (Const ("Product_Type.Pair",_) $Free (dI',_) $
1.13 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
1.14 + (*compare "| assod _ (Subproblem'"*)
1.15 + let
1.16 + val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
1.17 val thy = maxthy (assoc_thy dI) (rootthy pt);
1.18 - val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
1.19 - val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
1.20 - val ags = isalist2list ags';
1.21 - val (pI, pors, mI) =
1.22 - if mI = ["no_met"]
1.23 - then let val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
1.24 - handle ERROR "actual args do not match formal args"
1.25 - => (match_ags_msg pI stac ags(*raise exn*);[])
1.26 - val pI' = refine_ori' pors pI;
1.27 - in (pI', pors (*refinement over models with diff.prec only*),
1.28 - (hd o #met o get_pbt) pI') end
1.29 - else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
1.30 - handle ERROR "actual args do not match formal args"
1.31 - => (match_ags_msg pI stac ags(*raise exn*); []),
1.32 - mI);
1.33 + val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
1.34 + val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
1.35 + val ags = isalist2list ags';
1.36 + val (pI, pors, mI) =
1.37 + if mI = ["no_met"]
1.38 + then
1.39 + let
1.40 + val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
1.41 + handle ERROR "actual args do not match formal args"
1.42 + => (match_ags_msg pI stac ags(*raise exn*); [])
1.43 + val pI' = refine_ori' pors pI;
1.44 + in (pI', pors (*refinement over models with diff.prec only*),
1.45 + (hd o #met o get_pbt) pI') end
1.46 + else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
1.47 + handle ERROR "actual args do not match formal args"
1.48 + => (match_ags_msg pI stac ags(*raise exn*); []), mI);
1.49 val (fmz_, vals) = oris2fmz_vals pors;
1.50 - val {cas,ppc,thy,...} = get_pbt pI
1.51 - val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
1.52 - val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
1.53 - val hdl = case cas of
1.54 - NONE => pblterm dI pI
1.55 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
1.56 + val {cas,ppc,thy,...} = get_pbt pI
1.57 + val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
1.58 + val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
1.59 + val hdl =
1.60 + case cas of
1.61 + NONE => pblterm dI pI
1.62 + | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
1.63 val f = subpbl (strip_thy dI) pI
1.64 - in (Subproblem (dI, pI),
1.65 - Subproblem' ((dI, pI, mI), pors, hdl, fmz_, f))
1.66 - end
1.67 + in (Subproblem (dI, pI), Subproblem' ((dI, pI, mI), pors, hdl, fmz_, (*FIXME.WN110511*)e_ctxt, f))
1.68 + end
1.69
1.70 | stac2tac_ pt thy t = error
1.71 ("stac2tac_ TODO: no match for " ^
1.72 @@ -490,11 +491,13 @@
1.73
1.74
1.75 datatype ass =
1.76 - Ass of tac_ * (*SubProblem gets args instantiated in assod*)
1.77 - term (*for itr_arg,result in ets*)
1.78 -| AssWeak of tac_ *
1.79 - term (*for itr_arg,result in ets*)
1.80 -| NotAss;
1.81 + Ass of
1.82 + tac_ * (* SubProblem gets args instantiated in assod *)
1.83 + term (* for itr_arg, result in ets *)
1.84 + | AssWeak of
1.85 + tac_ *
1.86 + term (*for itr_arg,result in ets*)
1.87 + | NotAss;
1.88
1.89 (*.assod: tac_ associated with stac w.r.t. d
1.90 args
1.91 @@ -508,174 +511,159 @@
1.92 tac_ SubProblem with args completed from script
1.93 .*)
1.94 fun assod pt d (m as Rewrite_Inst' (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) stac =
1.95 - (case stac of
1.96 - (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_)=>
1.97 - if thmID = thmID_ then
1.98 - if f = f_ then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
1.99 - else ((*tracing"3### assod ..AssWeak";*)AssWeak(m, f'))
1.100 - else ((*tracing"3### assod ..NotAss";*)NotAss)
1.101 - | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $_$f_)=>
1.102 - if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_) then
1.103 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.104 - else NotAss
1.105 + (case stac of
1.106 + (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_) =>
1.107 + if thmID = thmID_
1.108 + then
1.109 + if f = f_
1.110 + then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
1.111 + else ((*tracing"3### assod ..AssWeak";*)AssWeak(m, f'))
1.112 + else ((*tracing"3### assod ..NotAss";*)NotAss)
1.113 + | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $_$f_) =>
1.114 + if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_)
1.115 + then
1.116 + if f = f_ then Ass (m,f') else AssWeak (m,f')
1.117 + else NotAss
1.118 | _ => NotAss)
1.119
1.120 | assod pt d (m as Rewrite' (thy,rod,rls,put,(thmID,thm),f,(f',asm))) stac =
1.121 - (case stac of
1.122 - (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
1.123 - ((*tracing ("3### assod: stac = " ^ ter2str t);
1.124 - tracing ("3### assod: f(m)= " ^ term2str f);*)
1.125 - if thmID = thmID_ then
1.126 - if f = f_ then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
1.127 - else ((*tracing"### assod ..AssWeak";
1.128 - tracing("### assod: f(m) = " ^ term2str f);
1.129 - tracing("### assod: f(stac)= " ^ term2str f_)*)
1.130 - AssWeak (m,f'))
1.131 - else ((*tracing"3### assod ..NotAss";*)NotAss))
1.132 + (case stac of
1.133 + (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
1.134 + ((*tracing ("3### assod: stac = " ^ ter2str t);
1.135 + tracing ("3### assod: f(m)= " ^ term2str f);*)
1.136 + if thmID = thmID_
1.137 + then
1.138 + if f = f_
1.139 + then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
1.140 + else
1.141 + ((*tracing"### assod ..AssWeak";
1.142 + tracing("### assod: f(m) = " ^ term2str f);
1.143 + tracing("### assod: f(stac)= " ^ term2str f_)*)
1.144 + AssWeak (m,f'))
1.145 + else ((*tracing"3### assod ..NotAss";*)NotAss))
1.146 | (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =>
1.147 - if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_) then
1.148 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.149 - else NotAss
1.150 + if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_)
1.151 + then
1.152 + if f = f_ then Ass (m,f') else AssWeak (m,f')
1.153 + else NotAss
1.154 | _ => NotAss)
1.155
1.156 -(*val f = (term_of o the o (parse thy))"#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0";
1.157 -> val f'= (term_of o the o (parse thy))"#0+(sqrt(sqrt a))^^^#2=#0";
1.158 -> val m = Rewrite'("Script","tless_true","eval_rls",false,
1.159 - ("rroot_square_inv",""),f,(f',[]));
1.160 -> val stac = (term_of o the o (parse thy))
1.161 - "Rewrite rroot_square_inv False (#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0)";
1.162 -> assod e_rls m stac;
1.163 -val it =
1.164 - (SOME (Rewrite' (#,#,#,#,#,#,#)),Const ("empty","RealDef.real"),
1.165 - Const ("empty","RealDef.real")) : tac_ option * term * term*)
1.166 -
1.167 | assod pt d (m as Rewrite_Set_Inst' (thy',put,sub,rls,f,(f',asm)))
1.168 - (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_)=
1.169 - if id_rls rls = rls_ then
1.170 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.171 - else NotAss
1.172 + (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) =
1.173 + if id_rls rls = rls_
1.174 + then
1.175 + if f = f_ then Ass (m,f') else AssWeak (m,f')
1.176 + else NotAss
1.177
1.178 | assod pt d (m as Detail_Set_Inst' (thy',put,sub,rls,f,(f',asm)))
1.179 - (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_)=
1.180 - if id_rls rls = rls_ then
1.181 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.182 - else NotAss
1.183 + (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) =
1.184 + if id_rls rls = rls_
1.185 + then
1.186 + if f = f_ then Ass (m,f') else AssWeak (m,f')
1.187 + else NotAss
1.188
1.189 | assod pt d (m as Rewrite_Set' (thy,put,rls,f,(f',asm)))
1.190 - (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
1.191 - if id_rls rls = rls_ then
1.192 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.193 - else NotAss
1.194 + (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
1.195 + if id_rls rls = rls_
1.196 + then
1.197 + if f = f_ then Ass (m,f') else AssWeak (m,f')
1.198 + else NotAss
1.199
1.200 | assod pt d (m as Detail_Set' (thy,put,rls,f,(f',asm)))
1.201 - (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
1.202 - if id_rls rls = rls_ then
1.203 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.204 - else NotAss
1.205 + (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
1.206 + if id_rls rls = rls_
1.207 + then
1.208 + if f = f_ then Ass (m,f') else AssWeak (m,f')
1.209 + else NotAss
1.210
1.211 | assod pt d (m as Calculate' (thy',op_,f,(f',thm'))) stac =
1.212 - (case stac of
1.213 - (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) =>
1.214 - if op_ = op__ then
1.215 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.216 - else NotAss
1.217 - | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_)=>
1.218 - if contains_rule (Calc (snd (assoc1 (!calclist', op_))))
1.219 - (assoc_rls rls_) then
1.220 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.221 - else NotAss
1.222 + (case stac of
1.223 + (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) =>
1.224 + if op_ = op__
1.225 + then
1.226 + if f = f_ then Ass (m,f') else AssWeak (m,f')
1.227 + else NotAss
1.228 + | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_) =>
1.229 + if contains_rule (Calc (snd (assoc1 (!calclist', op_)))) (assoc_rls rls_)
1.230 + then
1.231 + if f = f_ then Ass (m,f') else AssWeak (m,f')
1.232 + else NotAss
1.233 | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) =>
1.234 - if contains_rule (Calc (snd (assoc1 (!calclist', op_))))
1.235 - (assoc_rls rls_) then
1.236 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.237 - else NotAss
1.238 + if contains_rule (Calc (snd (assoc1 (!calclist', op_)))) (assoc_rls rls_)
1.239 + then
1.240 + if f = f_ then Ass (m,f') else AssWeak (m,f')
1.241 + else NotAss
1.242 | _ => NotAss)
1.243
1.244 | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
1.245 (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
1.246 - ((*tracing("### assod Check'_elementwise: consts= "^(term2str consts)^
1.247 + ((*tracing("### assod Check'_elementwise: consts= "^(term2str consts)^
1.248 ", consts'= "^(term2str consts'));
1.249 - atomty consts; atomty consts';*)
1.250 - if consts = consts' then ((*tracing"### assod Check'_elementwise: Ass";*)
1.251 - Ass (m, consts_chkd))
1.252 - else ((*tracing"### assod Check'_elementwise: NotAss";*) NotAss))
1.253 + atomty consts; atomty consts';*)
1.254 + if consts = consts'
1.255 + then ((*tracing"### assod Check'_elementwise: Ass";*) Ass (m, consts_chkd))
1.256 + else ((*tracing"### assod Check'_elementwise: NotAss";*) NotAss))
1.257
1.258 - | assod pt _ (m as Or_to_List' (ors, list))
1.259 - (Const ("Script.Or'_to'_List",_) $ _) =
1.260 - Ass (m, list)
1.261 + | assod pt _ (m as Or_to_List' (ors, list)) (Const ("Script.Or'_to'_List",_) $ _) =
1.262 + Ass (m, list)
1.263
1.264 - | assod pt _ (m as Take' term)
1.265 - (Const ("Script.Take",_) $ _) =
1.266 - Ass (m, term)
1.267 + | assod pt _ (m as Take' term) (Const ("Script.Take",_) $ _) =
1.268 + Ass (m, term)
1.269
1.270 - | assod pt _ (m as Substitute' (_, _, res))
1.271 - (Const ("Script.Substitute",_) $ _ $ _) =
1.272 - Ass (m, res)
1.273 -(* val t = str2term "Substitute [(x, 3)] (x^^^2 + x + 1)";
1.274 - val (Const ("Script.Substitute",_) $ _ $ _) = t;
1.275 - *)
1.276 + | assod pt _ (m as Substitute' (_, _, res)) (Const ("Script.Substitute",_) $ _ $ _) =
1.277 + Ass (m, res)
1.278
1.279 - | assod pt _ (m as Tac_ (thy,f,id,f'))
1.280 - (Const ("Script.Tac",_) $ Free (id',_)) =
1.281 - if id = id' then Ass (m, ((term_of o the o (parse thy)) f'))
1.282 - else NotAss
1.283 + | assod pt _ (m as Tac_ (thy,f,id,f')) (Const ("Script.Tac",_) $ Free (id',_)) =
1.284 + if id = id'
1.285 + then Ass (m, ((term_of o the o (parse thy)) f'))
1.286 + else NotAss
1.287
1.288 -
1.289 -(* val t = str2term
1.290 - "SubProblem (DiffApp_,[make,function],[no_met]) \
1.291 - \[REAL m_, REAL v_, BOOL_LIST rs_]";
1.292 -
1.293 - val (Subproblem' ((domID,pblID,metID),_,_,_,f)) = m;
1.294 - val (Const ("Script.SubProblem",_) $
1.295 - (Const ("Product_Type.Pair",_) $
1.296 - Free (dI',_) $
1.297 - (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') = stac;
1.298 - *)
1.299 - | assod pt _ (Subproblem' ((domID,pblID,metID),_,_,_,f))
1.300 - (stac as Const ("Script.SubProblem",_) $
1.301 - (Const ("Product_Type.Pair",_) $
1.302 - Free (dI',_) $
1.303 - (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
1.304 -(*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
1.305 - let val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
1.306 + | assod pt _ (Subproblem' ((domID,pblID,metID),_,_,_,_,f))
1.307 + (stac as Const ("Script.SubProblem",_) $ (Const ("Product_Type.Pair",_) $
1.308 + Free (dI',_) $ (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
1.309 + (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
1.310 + let
1.311 + val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
1.312 val thy = maxthy (assoc_thy dI) (rootthy pt);
1.313 - val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
1.314 - val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
1.315 - val ags = isalist2list ags';
1.316 - val (pI, pors, mI) =
1.317 - if mI = ["no_met"]
1.318 - then let val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
1.319 - handle ERROR "actual args do not match formal args"
1.320 - => (match_ags_msg pI stac ags(*raise exn*);[]);
1.321 - val pI' = refine_ori' pors pI;
1.322 - in (pI', pors (*refinement over models with diff.prec only*),
1.323 - (hd o #met o get_pbt) pI') end
1.324 - else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
1.325 - handle ERROR "actual args do not match formal args"
1.326 - => (match_ags_msg pI stac ags(*raise exn*);[]),
1.327 - mI);
1.328 + val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
1.329 + val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
1.330 + val ags = isalist2list ags';
1.331 + val (pI, pors, mI) =
1.332 + if mI = ["no_met"]
1.333 + then
1.334 + let
1.335 + val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
1.336 + handle ERROR "actual args do not match formal args"
1.337 + => (match_ags_msg pI stac ags(*raise exn*);[]);
1.338 + val pI' = refine_ori' pors pI;
1.339 + in (pI', pors (*refinement over models with diff.prec only*),
1.340 + (hd o #met o get_pbt) pI')
1.341 + end
1.342 + else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
1.343 + handle ERROR "actual args do not match formal args"
1.344 + => (match_ags_msg pI stac ags(*raise exn*);[]), mI);
1.345 val (fmz_, vals) = oris2fmz_vals pors;
1.346 - val {cas, ppc,...} = get_pbt pI
1.347 - val {cas, ppc, thy,...} = get_pbt pI
1.348 - val dI = theory2theory' thy (*take dI from _refined_ pbl*)
1.349 - val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
1.350 - val hdl = case cas of
1.351 - NONE => pblterm dI pI
1.352 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
1.353 + val {cas, ppc,...} = get_pbt pI
1.354 + val {cas, ppc, thy,...} = get_pbt pI
1.355 + val dI = theory2theory' thy (*take dI from _refined_ pbl*)
1.356 + val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
1.357 + val hdl =
1.358 + case cas of
1.359 + NONE => pblterm dI pI
1.360 + | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
1.361 val f = subpbl (strip_thy dI) pI
1.362 - in if domID = dI andalso pblID = pI
1.363 - then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, f), f)
1.364 - else NotAss
1.365 - end
1.366 + in
1.367 + if domID = dI andalso pblID = pI
1.368 + then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, (*FIXME.WN110511*)e_ctxt, f), f)
1.369 + else NotAss
1.370 + end
1.371
1.372 | assod pt d m t =
1.373 - (if (!trace_script)
1.374 - then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"^
1.375 - "@@@ tac_ = "^(tac_2str m))
1.376 - else ();
1.377 - NotAss);
1.378 -
1.379 -
1.380 + (if (!trace_script)
1.381 + then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"^
1.382 + "@@@ tac_ = "^(tac_2str m))
1.383 + else ();
1.384 + NotAss);
1.385
1.386 fun tac_2tac (Refine_Tacitly' (pI,_,_,_,_)) = Refine_Tacitly pI
1.387 | tac_2tac (Model_Problem' (pI,_,_)) = Model_Problem
1.388 @@ -716,7 +704,7 @@
1.389
1.390 | tac_2tac (Tac_ (_,f,id,f')) = Tac id
1.391
1.392 - | tac_2tac (Subproblem' ((domID, pblID, _), _, _,_,_)) =
1.393 + | tac_2tac (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) =
1.394 Subproblem (domID, pblID)
1.395 | tac_2tac (Check_Postcond' (pblID, _)) =
1.396 Check_Postcond pblID
1.397 @@ -878,7 +866,7 @@
1.398 > lhs'=lhs;
1.399 val it = true : bool*)
1.400 | rep_tac_ (Check_elementwise' (t,str,(t',asm))) = (Erule, (e_term, t'))
1.401 - | rep_tac_ (Subproblem' (_,_,_,_,t')) = (Erule, (e_term, t'))
1.402 + | rep_tac_ (Subproblem' (_, _, _, _, _, t')) = (Erule, (e_term, t'))
1.403 | rep_tac_ (Take' (t')) = (Erule, (e_term, t'))
1.404 | rep_tac_ (Substitute' (subst,t,t')) = (Erule, (t, t'))
1.405 | rep_tac_ (Or_to_List' (t, t')) = (Erule, (t, t'))