1.1 --- a/src/Tools/isac/Interpret/script.sml Mon Dec 12 18:08:13 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Dec 14 09:37:01 2016 +0100
1.3 @@ -8,7 +8,7 @@
1.4 signature LUCAS_INTERPRETER =
1.5 sig
1.6
1.7 - type step = tac_ * mout * ptree * pos' * pos' list
1.8 + type step = tac_ * Ctree.mout * ptree * pos' * pos' list
1.9 datatype locate = NotLocatable | Steps of istate * step list
1.10
1.11 val next_tac : (*diss: next-tactic-function*)
1.12 @@ -61,7 +61,7 @@
1.13 Assoc (scrstate, steps) => ... ass* scrstate steps *)
1.14 type step =
1.15 tac_ (*transformed from associated tac *)
1.16 - * mout (*result with indentation etc. *)
1.17 + * Ctree.mout (*result with indentation etc. *)
1.18 * ptree (*containing node created by tac_ + resp. scrstate *)
1.19 * pos' (*position in ptree; ptree * pos' is the proofstate *)
1.20 * pos' list; (*of ptree-nodes probably cut (by fst tac_) *)
1.21 @@ -80,7 +80,7 @@
1.22 val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
1.23 val is = RrlsState (f', f'', rss, rts)
1.24 val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
1.25 - val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
1.26 + val (p', cid, mout, pt') = Ctree.generate1 thy m (is, ctxt) p pt
1.27 in (is, (m, mout, pt', p', cid) :: steps) end
1.28 | rts2steps steps ((pt, p) ,(f, f'', rss, rts), (thy', ro, er, pa)) ((r, (f', am)) :: rts') =
1.29 let
1.30 @@ -89,7 +89,7 @@
1.31 val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
1.32 val is = RrlsState (f', f'', rss, rts)
1.33 val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
1.34 - val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
1.35 + val (p', cid, mout, pt') = Ctree.generate1 thy m (is, ctxt) p pt
1.36 in rts2steps ((m, mout, pt', p', cid)::steps)
1.37 ((pt', p'), (f', f'', rss, rts), (thy', ro, er, pa)) rts'
1.38 end
1.39 @@ -665,11 +665,11 @@
1.40 case assod pt d m stac of
1.41 Ass (m,v') =>
1.42 let val (p'',c',f',pt') =
1.43 - generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
1.44 + Ctree.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
1.45 in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
1.46 | AssWeak (m,v') =>
1.47 let val (p'',c',f',pt') =
1.48 - generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
1.49 + Ctree.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
1.50 in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
1.51 | NotAss =>
1.52 (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
1.53 @@ -680,7 +680,7 @@
1.54 let
1.55 val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
1.56 val (p'',c',f',pt') =
1.57 - generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p',p_) pt;
1.58 + Ctree.generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p', p_) pt;
1.59 in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
1.60 | Chead.Notappl _ => (NasNap (v, E))
1.61 )
1.62 @@ -822,8 +822,8 @@
1.63 let val thy = assoc_thy thy';
1.64 in case if l = [] orelse (
1.65 (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res)
1.66 - then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
1.67 - else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of
1.68 + then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,Ctree.EmptyMout,pt,p,[])]) body)
1.69 + else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,Ctree.EmptyMout,pt,p,[])]) ) of
1.70 Assoc ((is as (_,_,_,_,_,strong_ass), ss as (_ :: _))) =>
1.71 (if strong_ass
1.72 then (Steps (ScrState is, ss))
1.73 @@ -833,7 +833,7 @@
1.74 let
1.75 val (po,p_) = p
1.76 val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_gen " ^ pos_2str p_)
1.77 - val (p'',c'',f'',pt'') = generate1 thy m (ScrState is, ctxt) (po',p_) pt
1.78 + val (p'',c'',f'',pt'') = Ctree.generate1 thy m (ScrState is, ctxt) (po',p_) pt
1.79 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
1.80 else Steps (ScrState is, ss))
1.81