1.1 --- a/src/Tools/isac/Frontend/interface.sml Mon Dec 12 18:08:13 2016 +0100
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Wed Dec 14 09:37:01 2016 +0100
1.3 @@ -343,7 +343,7 @@
1.4 let
1.5 val ctxt = get_ctxt pt pold
1.6 val (p, c, _, pt) =
1.7 - generate1 (assoc_thy "Isac") m (Uistate, ctxt) ip pt
1.8 + Ctree.generate1 (assoc_thy "Isac") m (Uistate, ctxt) ip pt
1.9 in upd_calc cI ((pt, p), []);
1.10 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p
1.11 end)
1.12 @@ -672,7 +672,7 @@
1.13 (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
1.14 (_, fillform, thm, sube_opt) :: _ =>
1.15 let
1.16 - val (pt, pos') = generate_inconsistent_rew (sube_opt, thm''_of_thm thm)
1.17 + val (pt, pos') = Ctree.generate_inconsistent_rew (sube_opt, thm''_of_thm thm)
1.18 fillform (get_loc pt pos) pos pt
1.19 in
1.20 (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
2.1 --- a/src/Tools/isac/Interpret/appl.sml Mon Dec 12 18:08:13 2016 +0100
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Wed Dec 14 09:37:01 2016 +0100
2.3 @@ -225,7 +225,7 @@
2.4 let
2.5 val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
2.6 val {ppc,...} = get_pbt pI'
2.7 - val pbl = init_pbl ppc
2.8 + val pbl = Ctree.init_pbl ppc
2.9 in Chead.Appl (Model_Problem' (pI', pbl, [])) end
2.10
2.11 | applicable_in (p,p_) pt (Refine_Tacitly pI) =
2.12 @@ -318,7 +318,7 @@
2.13 val thy = assoc_thy (if dI' = e_domID then dI else dI');
2.14 val {ppc,where_,prls,...} = get_pbt pID;
2.15 val pbl = if pI'=e_pblID andalso pI=e_pblID
2.16 - then (false, (init_pbl ppc, []))
2.17 + then (false, (Ctree.init_pbl ppc, []))
2.18 else match_itms_oris thy itms (ppc,where_,prls) oris;
2.19 in Chead.Appl (Specify_Problem' (pID, pbl)) end
2.20 (* val Specify_Method mID = nxt; val (p,p_) = p;
3.1 --- a/src/Tools/isac/Interpret/calchead.sml Mon Dec 12 18:08:13 2016 +0100
3.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed Dec 14 09:37:01 2016 +0100
3.3 @@ -10,7 +10,7 @@
3.4 datatype appl = Appl of tac_ | Notappl of string
3.5 val nxt_specify_init_calc : fmz -> calcstate
3.6 val specify : tac_ -> pos' -> cid -> ptree ->
3.7 - (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac * safe * ptree
3.8 + (posel list * pos_) * ((posel list * pos_) * istate) * Ctree.mout * tac * safe * ptree
3.9 val nxt_specif : tac -> ptree * (pos * pos_) -> calcstate'
3.10 val nxt_spec : pos_ -> bool -> ori list -> spec -> itm list * itm list ->
3.11 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> pos_ * tac
3.12 @@ -69,9 +69,9 @@
3.13 *)
3.14 type calcstate =
3.15 (ptree * pos') * (* the calc-state to which the tacis could be applied *)
3.16 - (taci list) (* ev. several (hidden) steps;
3.17 + (Ctree.taci list) (* ev. several (hidden) steps;
3.18 in REVERSE order: first tac_ to apply is last_elem *)
3.19 -val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]) : calcstate;
3.20 +val e_calcstate = ((EmptyPtree, e_pos'), [Ctree.e_taci]) : calcstate;
3.21
3.22 (*the state used during one calculation within the mathengine; it contains
3.23 a list of [tac,istate](="tacis") which generated the the calc-state;
3.24 @@ -83,14 +83,14 @@
3.25 because the tacis hold enought information for efficiently rebuilding
3.26 this state just by "fun generate ".*)
3.27 type calcstate' =
3.28 - taci list * (* cas. several (hidden) steps;
3.29 - in REVERSE order: first tac_ to apply is last_elem*)
3.30 - pos' list * (* a "continuous" sequence of pos', deleted by application of taci list*)
3.31 - (ptree * pos') (* the calc-state resulting from the application of tacis*)
3.32 -val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
3.33 + Ctree.taci list * (* cas. several (hidden) steps;
3.34 + in REVERSE order: first tac_ to apply is last_elem *)
3.35 + pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
3.36 + (ptree * pos') (* the calc-state resulting from the application of tacis *)
3.37 +val e_calcstate' = ([Ctree.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
3.38
3.39 (* FIXXXME.WN020430 intermediate hack for fun ass_up *)
3.40 -fun f_mout thy (Form' (FormKF (_, _, _, _, f))) = (Thm.term_of o the o (parse thy)) f
3.41 +fun f_mout thy (Ctree.Form' (Ctree.FormKF (_, _, _, _, f))) = (Thm.term_of o the o (parse thy)) f
3.42 | f_mout _ _ = error "f_mout: not called with formula";
3.43
3.44 (* is the calchead complete ? *)
3.45 @@ -606,8 +606,8 @@
3.46
3.47 (* output the headline to a ppc *)
3.48 fun header p_ pI mI =
3.49 - case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
3.50 - | Met => Method mI
3.51 + case p_ of Pbl => Ctree.Problem (if pI = e_pblID then [] else pI)
3.52 + | Met => Ctree.Method mI
3.53 | pos => error ("header called with "^ pos_2str pos)
3.54
3.55 fun specify_additem sel (ct, _) (p, Met) _ pt =
3.56 @@ -630,7 +630,7 @@
3.57 | "#Find" => Add_Find' (ct, met')
3.58 | "#Relate"=> Add_Relation'(ct, met')
3.59 | str => error ("specify_additem: uncovered case with " ^ str)
3.60 - val (p, Met, pt') = case generate1 thy arg (Uistate, ctxt) (p, Met) pt of
3.61 + val (p, Met, pt') = case Ctree.generate1 thy arg (Uistate, ctxt) (p, Met) pt of
3.62 ((p, Met), _, _, pt') => (p, Met, pt')
3.63 | _ => error "specify_additem: uncovered case of generate1 (WARNING WHY ?)"
3.64 val pre' = check_preconds thy prls pre met'
3.65 @@ -639,8 +639,8 @@
3.66 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
3.67 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
3.68 in ((p, p_), ((p, p_), Uistate),
3.69 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
3.70 - (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
3.71 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef,
3.72 + (Ctree.Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
3.73 end
3.74 | Err msg =>
3.75 let
3.76 @@ -649,7 +649,7 @@
3.77 val (p_, nxt) =
3.78 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
3.79 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
3.80 - in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
3.81 + in ((p,p_), ((p,p_),Uistate), Ctree.Error' (Ctree.Error_ msg), nxt, Safe,pt) end
3.82 end
3.83 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
3.84 let
3.85 @@ -671,7 +671,7 @@
3.86 | "#Find" => Add_Find' (ct, pbl')
3.87 | "#Relate"=> Add_Relation'(ct, pbl')
3.88 | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
3.89 - val ((p, Pbl), _, _, pt') = generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
3.90 + val ((p, Pbl), _, _, pt') = Ctree.generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
3.91 val pre = check_preconds thy prls where_ pbl'
3.92 val pb = foldl and_ (true, map fst pre)
3.93 val (p_, nxt) =
3.94 @@ -679,7 +679,7 @@
3.95 val ppc = if p_= Pbl then pbl' else met
3.96 in
3.97 ((p, p_), ((p, p_), Uistate),
3.98 - Form' (PpcKF (0, EdUndef, (length p), Nundef,
3.99 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef,
3.100 (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt, Safe, pt')
3.101 end
3.102 | Err msg =>
3.103 @@ -689,7 +689,7 @@
3.104 val (p_, nxt) =
3.105 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
3.106 (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
3.107 - in ((p, p_), ((p, p_), Uistate), Error' (Error_ msg), nxt, Safe,pt) end
3.108 + in ((p, p_), ((p, p_), Uistate), Ctree.Error' (Ctree.Error_ msg), nxt, Safe,pt) end
3.109 end
3.110
3.111 fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
3.112 @@ -707,11 +707,11 @@
3.113 case mI' of
3.114 ["no_met"] =>
3.115 (([], Pbl), (([], Pbl), Uistate),
3.116 - Form' (PpcKF (0, EdUndef, (length []), Nundef, (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
3.117 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length [], Ctree.Nundef, (Ctree.Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
3.118 Refine_Tacitly pI', Safe, pt)
3.119 | _ =>
3.120 (([], Pbl), (([], Pbl), Uistate),
3.121 - Form' (PpcKF (0, EdUndef, (length []), Nundef, (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
3.122 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length [], Ctree.Nundef, (Ctree.Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
3.123 Model_Problem, Safe, pt)
3.124 end
3.125 (* ONLY for STARTING modeling phase *)
3.126 @@ -727,12 +727,12 @@
3.127 val pre = check_preconds thy prls where_ pbl
3.128 val pb = foldl and_ (true, map fst pre)
3.129 val ((p, _), _, _, pt) =
3.130 - generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
3.131 + Ctree.generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
3.132 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
3.133 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
3.134 in
3.135 ((p, Pbl), ((p, p_), Uistate),
3.136 - Form' (PpcKF (0, EdUndef, length p, Nundef, (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
3.137 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
3.138 nxt, Safe, pt)
3.139 end
3.140 (* called only if no_met is specified *)
3.141 @@ -744,19 +744,19 @@
3.142 val {met, thy,...} = get_pbt pIre
3.143 val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)
3.144 val ((p,_), _, _, pt) =
3.145 - generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
3.146 + Ctree.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
3.147 val (pbl, pre, _) = ([], [], false)
3.148 in ((p, Pbl), (pos, Uistate),
3.149 - Form' (PpcKF (0, EdUndef, length p, Nundef, (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
3.150 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
3.151 Model_Problem, Safe, pt)
3.152 end
3.153 | specify (Refine_Problem' rfd) pos _ pt =
3.154 let
3.155 val ctxt = get_ctxt pt pos
3.156 val (pos, _, _, pt) =
3.157 - generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
3.158 + Ctree.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
3.159 in
3.160 - (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Problems (RefinedKF rfd), Model_Problem, Safe, pt)
3.161 + (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Ctree.Problems (Ctree.RefinedKF rfd), Model_Problem, Safe, pt)
3.162 end
3.163 (*WN110515 initialise ctxt again from itms and add preconds*)
3.164 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
3.165 @@ -767,7 +767,7 @@
3.166 | _ => error "specify (Specify_Problem': uncovered case get_obj"
3.167 val thy = assoc_thy dI
3.168 val (p, Pbl, pt) =
3.169 - case generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
3.170 + case Ctree.generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
3.171 ((p, Pbl), _, _, pt) => (p, Pbl, pt)
3.172 | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
3.173 val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
3.174 @@ -776,7 +776,7 @@
3.175 (#ppc o get_met) mI'') (dI, pI, mI);
3.176 in
3.177 ((p,Pbl), (pos,Uistate),
3.178 - Form' (PpcKF (0,EdUndef,(length p),Nundef, (Problem pI, itms2itemppc dI'' itms pre))),
3.179 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Problem pI, itms2itemppc dI'' itms pre))),
3.180 nxt, Safe, pt)
3.181 end
3.182 (*WN110515 initialise ctxt again from itms and add preconds*)
3.183 @@ -794,12 +794,12 @@
3.184 val met = if met = [] then pbl else met
3.185 val (_, (itms, pre')) = match_itms_oris thy met (ppc, pre, prls ) oris
3.186 val (pos, _, _, pt) =
3.187 - generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
3.188 + Ctree.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
3.189 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
3.190 ((#ppc o get_pbt) pI'', ppc) (dI'', pI'', mID)
3.191 in
3.192 (pos, (pos,Uistate),
3.193 - Form' (PpcKF (0, EdUndef, length p, Nundef, (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
3.194 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
3.195 nxt, Safe, pt)
3.196 end
3.197 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
3.198 @@ -828,16 +828,16 @@
3.199 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
3.200 in
3.201 ((p, p_), (pos, Uistate),
3.202 - Form'(PpcKF (0, EdUndef, length p, Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
3.203 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
3.204 nxt, Safe, pt)
3.205 end
3.206 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
3.207 let
3.208 - val ((p, p_), _, _, pt) = generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
3.209 + val ((p, p_), _, _, pt) = Ctree.generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
3.210 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
3.211 in
3.212 ((p,p_), (pos,Uistate),
3.213 - Form' (PpcKF (0, EdUndef, length p, Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
3.214 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
3.215 nxt, Safe, pt)
3.216 end
3.217 end
3.218 @@ -863,7 +863,7 @@
3.219 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
3.220 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
3.221 | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
3.222 - val (p, Pbl, c, pt') = case generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
3.223 + val (p, Pbl, c, pt') = case Ctree.generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
3.224 ((p, Pbl), c, _, pt') => (p, Pbl, c, pt')
3.225 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
3.226 in
3.227 @@ -892,7 +892,7 @@
3.228 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
3.229 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
3.230 | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
3.231 - val (p, Met, c, pt') = case generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
3.232 + val (p, Met, c, pt') = case Ctree.generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
3.233 ((p, Met), c, _, pt') => (p, Met, c, pt')
3.234 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
3.235 in
3.236 @@ -967,7 +967,7 @@
3.237 val thy = assoc_thy dI
3.238 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
3.239 val {cas, ppc, ...} = get_pbt pI
3.240 - val pbl = init_pbl ppc (* fill in descriptions *)
3.241 + val pbl = Ctree.init_pbl ppc (* fill in descriptions *)
3.242 (*----------------if you think, this should be done by the Dialog
3.243 in the java front-end, search there for WN060225-modelProblem----*)
3.244 val (pbl, met) = case cas of
3.245 @@ -975,7 +975,7 @@
3.246 | _ => complete_mod_ (oris, mpc, ppc, probl)
3.247 (*----------------------------------------------------------------*)
3.248 val tac_ = Model_Problem' (pI, pbl, met)
3.249 - val (pos,c,_,pt) = generate1 thy tac_ (Uistate, ctxt) pos pt
3.250 + val (pos,c,_,pt) = Ctree.generate1 thy tac_ (Uistate, ctxt) pos pt
3.251 in ([(tac, tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end
3.252 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
3.253 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
3.254 @@ -996,7 +996,7 @@
3.255 val mI = if length met = 0 then e_metID else hd met
3.256 val thy = assoc_thy dI
3.257 val (pos, c, _, pt) =
3.258 - generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
3.259 + Ctree.generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
3.260 in
3.261 ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
3.262 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
3.263 @@ -1015,7 +1015,7 @@
3.264 NONE => ([], [], ptp)
3.265 | SOME rfd =>
3.266 let
3.267 - val (pos,c,_,pt) = generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
3.268 + val (pos,c,_,pt) = Ctree.generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
3.269 in
3.270 ([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Uistate, e_ctxt)))], c, (pt,pos))
3.271 end
3.272 @@ -1030,10 +1030,10 @@
3.273 val {ppc,where_,prls,...} = get_pbt pI
3.274 val pbl =
3.275 if pI' = e_pblID andalso pI = e_pblID
3.276 - then (false, (init_pbl ppc, []))
3.277 + then (false, (Ctree.init_pbl ppc, []))
3.278 else match_itms_oris thy probl (ppc,where_,prls) oris
3.279 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
3.280 - val (c, pt) = case generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
3.281 + val (c, pt) = case Ctree.generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
3.282 ((_, Pbl), c, _, pt) => (c, pt)
3.283 | _ => error ""
3.284 in
3.285 @@ -1053,7 +1053,7 @@
3.286 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
3.287 val (_, (itms, _)) = match_itms_oris thy met (ppc,pre,prls ) oris
3.288 val (pos, c, _, pt) =
3.289 - generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
3.290 + Ctree.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
3.291 in
3.292 ([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Uistate, e_ctxt)))], c, (pt, pos))
3.293 end
3.294 @@ -1061,7 +1061,7 @@
3.295 let
3.296 val ctxt = get_ctxt pt pos
3.297 val (pos, c, _, pt) =
3.298 - generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
3.299 + Ctree.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
3.300 in (*FIXXXME: check if pbl can still be parsed*)
3.301 ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c,
3.302 (pt, pos))
3.303 @@ -1069,7 +1069,7 @@
3.304 | nxt_specif (Specify_Theory dI) (pt, pos as (_, Met)) =
3.305 let
3.306 val ctxt = get_ctxt pt pos
3.307 - val (pos, c, _, pt) = generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
3.308 + val (pos, c, _, pt) = Ctree.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
3.309 in (*FIXXXME: check if met can still be parsed*)
3.310 ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, (pt, pos))
3.311 end
3.312 @@ -1092,7 +1092,7 @@
3.313 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI))
3.314 ([], (dI,pI,mI), hdl)
3.315 val pt = update_spec pt [] (dI, pI, mI)
3.316 - val pits = init_pbl' ppc
3.317 + val pits = Ctree.init_pbl' ppc
3.318 val pt = update_pbl pt [] pits
3.319 in ((pt, ([] , Pbl)), []) : calcstate end
3.320 else
3.321 @@ -1104,7 +1104,7 @@
3.322 val (pt, _) =
3.323 cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
3.324 val pt = update_spec pt [] (dI, pI, mI)
3.325 - val mits = init_pbl' ppc
3.326 + val mits = Ctree.init_pbl' ppc
3.327 val pt = update_met pt [] mits
3.328 in ((pt, ([], Met)), []) end
3.329 else (* new example, pepare for interactive modeling *)
4.1 --- a/src/Tools/isac/Interpret/generate.sml Mon Dec 12 18:08:13 2016 +0100
4.2 +++ b/src/Tools/isac/Interpret/generate.sml Wed Dec 14 09:37:01 2016 +0100
4.3 @@ -1,129 +1,125 @@
4.4 (* use"ME/generate.sml";
4.5 use"generate.sml";
4.6 *)
4.7 +signature CALC_TREE =
4.8 +sig (*vvv request into signature is incremental *)
4.9 + (* for calchead.sml *)
4.10 + type taci
4.11 + val e_taci : taci
4.12 + datatype edit = EdUndef | Protect | Write
4.13 + eqtype indent
4.14 + datatype nest = Closed | Nundef | Open
4.15 + datatype pblmet = Method of metID | Problem of pblID | Upblmet
4.16 + datatype inout
4.17 + = Error_ of string | FormKF of cellID * edit * indent * nest * cterm'
4.18 + | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) | RefineKF of match list
4.19 + | RefinedKF of pblID * (itm list * (bool * term) list)
4.20 + datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
4.21 + val generate1 : theory -> tac_ -> istate * Proof.context ->
4.22 + posel list * pos_ -> ptree -> pos' * pos' list * mout * ptree
4.23 + val init_pbl : (string * (term * 'a)) list -> itm list
4.24 + val init_pbl' : (string * (term * term)) list -> itm list
4.25 + (* for appl.sml *)
4.26 + (* for script.sml *)
4.27 + (* for solve.sml *)
4.28 + val generate_hard : theory -> tac_ -> pos * pos_ -> ptree -> pos' * pos' list * mout * ptree
4.29 + val init_istate : tac -> term -> istate
4.30 + (* for inform.sml *)
4.31 + val embed_deriv : taci list -> ptree * pos' -> pos' list * (ptree * pos')
4.32 + (* for mathengine.sml *)
4.33 + val generate : (tac * tac_ * ((posel list * pos_) * (istate * Proof.context))) list ->
4.34 + ptree * pos' list * pos' -> ptree * pos' list * pos'
4.35 + (* for interface.sml *)
4.36 + val generate_inconsistent_rew :
4.37 + subs option * thm'' ->
4.38 + term -> istate * Proof.context -> pos * pos_ -> ptree -> ptree * (posel list * pos_)
4.39 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.40 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.41 +end
4.42
4.43 -(*.initialize istate for Detail_Set.*)
4.44 +(**)
4.45 +structure Ctree(**): CALC_TREE(**) =
4.46 +(**)
4.47 +struct
4.48 +(* initialize istate for Detail_Set *)
4.49 fun init_istate (Rewrite_Set rls) t =
4.50 -(* val (Rewrite_Set rls) = (get_obj g_tac pt p);
4.51 - *)
4.52 (case assoc_rls rls of
4.53 - Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))
4.54 -(* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
4.55 - *)
4.56 - | Rls {scr=EmptyScr,...} =>
4.57 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
4.58 - ^"use prep_rls' for storing rule-sets !")
4.59 - | Rls {scr = Prog s,...} =>
4.60 - (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
4.61 - | Seq {scr=EmptyScr,...} =>
4.62 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
4.63 - ^"use prep_rls' for storing rule-sets !")
4.64 - | Seq {srls=srls,scr = Prog s,...} =>
4.65 - (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
4.66 -(* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t);
4.67 - *)
4.68 + Rrls {scr = Rfuns {init_state = ii, ...}, ...} => RrlsState (ii t)
4.69 + | Rls {scr = EmptyScr, ...} =>
4.70 + error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
4.71 + "use prep_rls' for storing rule-sets !")
4.72 + | Rls {scr = Prog s, ...} => (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
4.73 + | Seq {scr=EmptyScr,...} =>
4.74 + error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
4.75 + "use prep_rls' for storing rule-sets !")
4.76 + | Seq {scr = Prog s,...} => (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
4.77 + | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
4.78 | init_istate (Rewrite_Set_Inst (subs, rls)) t =
4.79 - let val (_, v)::_ = subs2subst (assoc_thy "Isac") subs
4.80 + let
4.81 + val v = case subs2subst (assoc_thy "Isac") subs of
4.82 + (_, v) :: _ => v
4.83 + | _ => error "init_istate: uncovered case "
4.84 (*...we suppose the substitution of only _one_ bound variable*)
4.85 in case assoc_rls rls of
4.86 - Rls {scr=EmptyScr,...} =>
4.87 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
4.88 - ^"use prep_rls' for storing rule-sets !")
4.89 - | Rls {scr = Prog s,...} =>
4.90 - let val (form, bdv) = two_scr_arg s
4.91 - in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
4.92 - end
4.93 - | Seq {scr=EmptyScr,...} =>
4.94 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
4.95 - ^"use prep_rls' for storing rule-sets !")
4.96 - | Seq {scr = Prog s,...} =>
4.97 - let val (form, bdv) = two_scr_arg s
4.98 - in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
4.99 - end
4.100 - end;
4.101 + Rls {scr = EmptyScr, ...} =>
4.102 + error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
4.103 + "use prep_rls' for storing rule-sets !")
4.104 + | Rls {scr = Prog s, ...} =>
4.105 + let val (form, bdv) = two_scr_arg s
4.106 + in (ScrState ([(form, t), (bdv, v)], [], NONE, e_term, Sundef,true))
4.107 + end
4.108 + | Seq {scr = EmptyScr, ...} =>
4.109 + error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
4.110 + "use prep_rls' for storing rule-sets !")
4.111 + | Seq {scr = Prog s,...} =>
4.112 + let val (form, bdv) = two_scr_arg s
4.113 + in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
4.114 + end
4.115 + | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls"
4.116 + end
4.117 + | init_istate tac _ = error ("init_istate: uncovered definition for " ^ tac2str tac)
4.118
4.119 -
4.120 -(*.a taci holds alle information required to build a node in the calc-tree;
4.121 +(* a taci holds alle information required to build a node in the calc-tree;
4.122 a taci is assumed to be used efficiently such that the calc-tree
4.123 resulting from applying a taci need not be stored separately;
4.124 - see "type calcstate".*)
4.125 + see "type calcstate" *)
4.126 (*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
4.127 TODO.WN0512 ? redesign this _list_:
4.128 # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
4.129 # the latter problem may be resolved automatically if "fun autocalc" is
4.130 not any more used for the specify-phase and for changing the phases*)
4.131 type taci =
4.132 - (tac * (*for comparison with input tac*)
4.133 - tac_ * (*for ptree generation*)
4.134 - (pos' * (*after applying tac_, for ptree generation*)
4.135 - (istate * Proof.context))); (*after applying tac_, for ptree generation*)
4.136 -val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci;
4.137 -(* val (tac, tac_, (pos', istate))::_ = tacis';
4.138 - *)
4.139 + (tac * (* for comparison with input tac *)
4.140 + tac_ * (* for ptree generation *)
4.141 + (pos' * (* after applying tac_, for ptree generation *)
4.142 + (istate * Proof.context))) (* after applying tac_, for ptree generation *)
4.143 +val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci
4.144 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
4.145 - "( "^tac2str tac^", "^tac_2str tac_^", ( "^pos'2str pos'
4.146 - ^", "^istate2str istate^" ))";
4.147 -fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis;
4.148 + "( " ^ tac2str tac ^ ", " ^ tac_2str tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
4.149 + istate2str istate ^ " ))"
4.150 +fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis
4.151
4.152 -datatype pblmet = (*%^%*)
4.153 - Upblmet (*undefined*)
4.154 - | Problem of pblID (*%^%*)
4.155 - | Method of metID; (*%^%*)
4.156 -fun pblmet2str (Problem pblID) = "Problem "^(strs2str pblID)(*%^%*)
4.157 - | pblmet2str (Method metID) = "Method "^(metID2str metID);(*%^%*)
4.158 - (*%^%*) (*26.6. moved to sequent.sml: fun ~~~~~~~~~; was here below*)
4.159 -
4.160 -
4.161 -(* copy from 03.60.usecases.sml 15.11.99 *)
4.162 -datatype user_cmd =
4.163 - Accept | NotAccept | Example
4.164 -| YourTurn | MyTurn (* internal use only 7.6.02 java-sml*)
4.165 -| Rules
4.166 -| DontKnow (*| HowComes | WhatFor 7.6.02 java-sml*)
4.167 -| Undo (*| Back | Forward 7.6.02 java-sml*)
4.168 -| EndProof | EndSession
4.169 -| ActivePlus | ActiveMinus | SpeedPlus | SpeedMinus
4.170 - (*Stepwidth...7.6.02 java-sml*)
4.171 -| Auto | NotAuto | Details;
4.172 -(* for test-print-outs *)
4.173 -fun user_cmd2str Accept ="Accept"
4.174 - | user_cmd2str NotAccept ="NotAccept"
4.175 - | user_cmd2str Example ="Example"
4.176 - | user_cmd2str MyTurn ="MyTurn"
4.177 - | user_cmd2str YourTurn ="YourTurn"
4.178 - | user_cmd2str Rules ="Rules"
4.179 -(*| user_cmd2str HowComes ="HowComes"*)
4.180 - | user_cmd2str DontKnow ="DontKnow"
4.181 -(*| user_cmd2str WhatFor ="WhatFor"
4.182 - | user_cmd2str Back ="Back"*)
4.183 - | user_cmd2str Undo ="Undo"
4.184 -(*| user_cmd2str Forward ="Forward"*)
4.185 - | user_cmd2str EndProof ="EndProof"
4.186 - | user_cmd2str EndSession ="EndSession"
4.187 - | user_cmd2str ActivePlus = "ActivePlus"
4.188 - | user_cmd2str ActiveMinus = "ActiveMinus"
4.189 - | user_cmd2str SpeedPlus = "SpeedPlus"
4.190 - | user_cmd2str SpeedMinus = "SpeedMinus"
4.191 - | user_cmd2str Auto = "Auto"
4.192 - | user_cmd2str NotAuto = "NotAuto"
4.193 - | user_cmd2str Details = "Details";
4.194 -
4.195 -
4.196 +datatype pblmet = (*%^%*)
4.197 + Upblmet (*undefined*)
4.198 +| Problem of pblID (*%^%*)
4.199 +| Method of metID; (*%^%*)
4.200 +fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)
4.201 + | pblmet2str (Method metID) = "Method " ^ metID2str metID (*%^%*)
4.202 + | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x)
4.203
4.204 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
4.205 datatype foppFK = (* in DG cases div 2 *)
4.206 EmptyFoppFK (*DG internal*)
4.207 | FormFK of cterm'
4.208 -| PpcFK of cterm' ppc;
4.209 -fun foppFK2str (FormFK ct') ="FormFK "^ct'
4.210 - | foppFK2str (PpcFK ppc) ="PpcFK "^(ppc2str ppc)
4.211 - | foppFK2str EmptyFoppFK ="EmptyFoppFK";
4.212 -
4.213 +| PpcFK of cterm' ppc
4.214 +fun foppFK2str (FormFK ct') ="FormFK " ^ ct'
4.215 + | foppFK2str (PpcFK ppc) ="PpcFK " ^ ppc2str ppc
4.216 + | foppFK2str EmptyFoppFK ="EmptyFoppFK"
4.217
4.218 datatype nest = Open | Closed | Nundef;
4.219 fun nest2str Open = "Open"
4.220 | nest2str Closed = "Closed"
4.221 - | nest2str Nundef = "Nundef";
4.222 + | nest2str Nundef = "Nundef"
4.223
4.224 type indent = int;
4.225 datatype edit = EdUndef | Write | Protect;
4.226 @@ -134,32 +130,15 @@
4.227 | edit2str Write = "Write"
4.228 | edit2str Protect = "Protect";
4.229
4.230 -
4.231 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
4.232 - New_User | End_User (*<->*)
4.233 -| New_Proof | End_Proof (*<->*)
4.234 -| Command of user_cmd (*-->*)
4.235 -| Request of string | Message of string (*<--*)
4.236 -| Error_ of string | System of string (*<--*)
4.237 -| FoPpcFK of foppFK (*-->*)
4.238 + Error_ of string (*<--*)
4.239 | FormKF of cellID * edit * indent * nest * cterm' (*<--*)
4.240 | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) (*<--*)
4.241 -| RuleFK of tac (*-->*)
4.242 -| RuleKF of edit * tac (*<--*)
4.243 -| RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*)
4.244 -| Select of tac list (*<--*)
4.245 | RefineKF of match list (*<--*)
4.246 -| Speed of int (*<--*)
4.247 -| Active of int (*<--*)
4.248 -| Domain of domID; (*<--*)
4.249 +| RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*)
4.250
4.251 fun inout2str End_Proof = "End_Proof"
4.252 - | inout2str (Command user_cmd) = "Command "^(user_cmd2str user_cmd)
4.253 - | inout2str (Request s) = "Request "^s
4.254 - | inout2str (Message s) = "Message "^s
4.255 | inout2str (Error_ s) = "Error_ "^s
4.256 - | inout2str (System s) = "System "^s
4.257 - | inout2str (FoPpcFK foppFK) = "FoPpcFK "^(foppFK2str foppFK)
4.258 | inout2str (FormKF (cellID, edit, indent, nest, ct')) =
4.259 "FormKF ("^(string_of_int cellID)^","
4.260 ^(edit2str edit)^","^(string_of_int indent)^","
4.261 @@ -170,16 +149,9 @@
4.262 ^(edit2str edit)^","^(string_of_int indent)^","
4.263 ^(nest2str nest)^",("
4.264 ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))"
4.265 - | inout2str (RuleKF (edit,tac)) = "RuleKF "^
4.266 - pair2str(edit2str edit,tac2str tac)
4.267 - | inout2str (RuleFK tac) = "RuleFK "^(tac2str tac)
4.268 - | inout2str (Select tacs)=
4.269 - "Select "^((strs2str' o (map tac2str)) tacs)
4.270 | inout2str (RefineKF ms) = "RefineKF "^(matchs2str ms)
4.271 - | inout2str (Speed i) = "Speed "^(string_of_int i)
4.272 - | inout2str (Active i) = "Active "^(string_of_int i)
4.273 - | inout2str (Domain dI) = "Domain "^dI;
4.274 -fun inouts2str ios = (strs2str' o (map inout2str)) ios;
4.275 + | inout2str _ = error "inout2str: uncovered definition"
4.276 +fun inouts2str ios = (strs2str' o (map inout2str)) ios
4.277
4.278 datatype mout =
4.279 Form' of inout (* packing cterm' | cterm' ppc *)
4.280 @@ -189,341 +161,291 @@
4.281
4.282 fun mout2str (Form' inout) ="Form' "^(inout2str inout)
4.283 | mout2str (Error' inout) ="Error' "^(inout2str inout)
4.284 - | mout2str (EmptyMout ) ="EmptyMout";
4.285 -
4.286 -(*fun Form'2str (Form' )*)
4.287 -
4.288 -
4.289 -
4.290 -
4.291 + | mout2str (EmptyMout ) ="EmptyMout"
4.292 + | mout2str _ = error "mout2str: uncovered definition"
4.293
4.294 (* init pbl with ...,dsc,empty | [] *)
4.295 fun init_pbl pbt =
4.296 - let
4.297 - fun pbt2itm (f, (d, t)) =
4.298 - ((0, [], false, f, Inc ((d, []), (e_term, []))) : itm);
4.299 - in map pbt2itm pbt end;
4.300 -(*take formal parameters from pbt, for transfer from pbl/met-hierarchy*)
4.301 + let
4.302 + fun pbt2itm (f, (d, _)) = ((0, [], false, f, Inc ((d, []), (e_term, []))) : itm)
4.303 + in map pbt2itm pbt end
4.304 +
4.305 +(* take formal parameters from pbt, for transfer from pbl/met-hierarchy *)
4.306 fun init_pbl' pbt =
4.307 let
4.308 - fun pbt2itm (f,(d,t)) =
4.309 - ((0,[],false,f,Inc((d,[t]),(e_term,[]))):itm);
4.310 - in map pbt2itm pbt end;
4.311 -
4.312 + fun pbt2itm (f, (d, t)) = ((0, [], false, f, Inc((d, [t]), (e_term, []))) : itm)
4.313 + in map pbt2itm pbt end
4.314
4.315 (*generate 1 ppobj in ptree*)
4.316 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
4.317 -fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p,p_)) pt =
4.318 - (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet, itms2itemppc thy [][]))),
4.319 - case p_ of
4.320 - Pbl => update_pbl pt p itmlist
4.321 - | Met => update_met pt p itmlist)
4.322 - (*WN110515 probably declare_constraints with input item (without dsc) --
4.323 - -- important when specifying without formalisation*)
4.324 - | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p,p_)) pt =
4.325 - (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
4.326 - case p_ of
4.327 - Pbl => update_pbl pt p itmlist
4.328 - | Met => update_met pt p itmlist)
4.329 +fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt =
4.330 + (pos:pos',[],Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [][]))),
4.331 + case p_ of
4.332 + Pbl => update_pbl pt p itmlist
4.333 + | Met => update_met pt p itmlist
4.334 + | _ => error ("uncovered case " ^ pos_2str p_))
4.335 + (* WN110515 probably declare_constraints with input item (without dsc) --
4.336 + -- important when specifying without formalisation *)
4.337 + | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p, p_)) pt =
4.338 + (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
4.339 + case p_ of
4.340 + Pbl => update_pbl pt p itmlist
4.341 + | Met => update_met pt p itmlist
4.342 + | _ => error ("uncovered case " ^ pos_2str p_))
4.343 (*WN110515 probably declare_constraints with input item (without dsc)*)
4.344 - | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p,p_)) pt =
4.345 - (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
4.346 - case p_ of
4.347 - Pbl => update_pbl pt p itmlist
4.348 - | Met => update_met pt p itmlist)
4.349 -
4.350 + | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p, p_)) pt =
4.351 + (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
4.352 + case p_ of
4.353 + Pbl => update_pbl pt p itmlist
4.354 + | Met => update_met pt p itmlist
4.355 + | _ => error ("uncovered case " ^ pos_2str p_))
4.356 | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt =
4.357 - (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
4.358 - update_domID pt p domID)
4.359 -
4.360 - | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) _
4.361 - (pos as (p,_)) pt =
4.362 - let val pt = update_pbl pt p itms
4.363 - val pt = update_pblID pt p pI
4.364 - in ((p,Pbl),[],
4.365 - Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
4.366 - pt) end
4.367 -
4.368 - | generate1 thy (Specify_Method' (mID, oris, itms)) _
4.369 - (pos as (p,_)) pt =
4.370 - let val pt = update_oris pt p oris
4.371 - val pt = update_met pt p itms
4.372 - val pt = update_metID pt p mID
4.373 - in ((p,Met),[],
4.374 - Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
4.375 - pt) end
4.376 -
4.377 + (pos, [] ,Form' (PpcKF (0 ,EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
4.378 + update_domID pt p domID)
4.379 + | generate1 thy (Specify_Problem' (pI, (_, (itms, _)))) _ (p, _) pt =
4.380 + let
4.381 + val pt = update_pbl pt p itms
4.382 + val pt = update_pblID pt p pI
4.383 + in
4.384 + ((p, Pbl), [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
4.385 + end
4.386 + | generate1 thy (Specify_Method' (mID, oris, itms)) _ (p, _) pt =
4.387 + let
4.388 + val pt = update_oris pt p oris
4.389 + val pt = update_met pt p itms
4.390 + val pt = update_metID pt p mID
4.391 + in
4.392 + ((p, Met), [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
4.393 + end
4.394 | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
4.395 - let
4.396 - val pt = update_pbl pt p itms
4.397 - val pt = update_met pt p met
4.398 - in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
4.399 - end
4.400 -
4.401 - | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl))
4.402 - _ (pos as (p,_)) pt =
4.403 - let val pt = update_pbl pt p pbl
4.404 - val pt = update_orispec pt p (domID,pIre,metID)
4.405 - in (pos,[],
4.406 - Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
4.407 - pt) end
4.408 -
4.409 - | generate1 thy (Refine_Problem' (pI,_)) _ (pos as (p,_)) pt =
4.410 - let val (dI,_,mI) = get_obj g_spec pt p
4.411 - val pt = update_spec pt p (dI, pI, mI)
4.412 - in (pos,[],
4.413 - Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),pt)
4.414 + let
4.415 + val pt = update_pbl pt p itms
4.416 + val pt = update_met pt p met
4.417 + in
4.418 + (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
4.419 end
4.420 -
4.421 - | generate1 thy (Apply_Method' (_,topt, is, ctxt)) _ (pos as (p,p_)) pt =
4.422 - ((*tracing("###generate1 Apply_Method': pos = "^pos'2str (p,p_));
4.423 - tracing("###generate1 Apply_Method': topt= "^termopt2str topt);
4.424 - tracing("###generate1 Apply_Method': is = "^istate2str is);*)
4.425 - case topt of
4.426 - SOME t =>
4.427 - let val (pt,c) = cappend_form pt p (is, ctxt) t
4.428 - (*val _= tracing("###generate1 Apply_Method: after cappend")*)
4.429 - in (pos,c, EmptyMout,pt)
4.430 - end
4.431 - | NONE =>
4.432 - (pos,[],EmptyMout,update_env pt p (SOME (is, ctxt))))
4.433 -(* val (thy, (Take' t), l, (p,p_), pt) =
4.434 - ((assoc_thy "Isac"), tac_, is, pos, pt);
4.435 - *)
4.436 - | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *)
4.437 - let (*val _=tracing("### generate1: Take' pos="^pos'2str (p,p_));*)
4.438 - val p = let val (ps,p') = split_last p(*no connex to prev.ppobj*)
4.439 - in if p'=0 then ps@[1] else p end;
4.440 - val (pt,c) = cappend_form pt p l t;
4.441 - in ((p,Frm):pos', c,
4.442 - Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
4.443 -
4.444 -(* val (l, (p,p_)) = (RrlsState is, p);
4.445 -
4.446 - val (thy, Begin_Trans' t, l, (p,Frm), pt) =
4.447 - (assoc_thy "Isac", tac_, is, p, pt);
4.448 - *)
4.449 - | generate1 thy (Begin_Trans' t) l (p,Frm) pt =
4.450 - let (* print_depth 99;
4.451 - map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
4.452 - *)
4.453 - val (pt,c) = cappend_form pt p l t
4.454 - (* print_depth 99;
4.455 - map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
4.456 - *)
4.457 + | generate1 thy (Refine_Tacitly' (_, pIre, domID, metID, pbl)) _ (pos as (p, _)) pt =
4.458 + let
4.459 + val pt = update_pbl pt p pbl
4.460 + val pt = update_orispec pt p (domID, pIre, metID)
4.461 + in
4.462 + (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
4.463 + end
4.464 + | generate1 thy (Refine_Problem' (pI, _)) _ (pos as (p, _)) pt =
4.465 + let
4.466 + val (dI, _, mI) = get_obj g_spec pt p
4.467 + val pt = update_spec pt p (dI, pI, mI)
4.468 + in
4.469 + (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
4.470 + end
4.471 + | generate1 _ (Apply_Method' (_, topt, is, ctxt)) _ (pos as (p, _)) pt =
4.472 + (case topt of
4.473 + SOME t =>
4.474 + let val (pt, c) = cappend_form pt p (is, ctxt) t
4.475 + in (pos, c, EmptyMout, pt) end
4.476 + | NONE => (pos, [], EmptyMout, update_env pt p (SOME (is, ctxt))))
4.477 + | generate1 _ (Take' t) l (p, _) pt = (* val (Take' t) = m; *)
4.478 + let
4.479 + val p =
4.480 + let val (ps, p') = split_last p (* no connex to prev.ppobj *)
4.481 + in if p' = 0 then ps @ [1] else p end
4.482 + val (pt, c) = cappend_form pt p l t
4.483 + in
4.484 + ((p, Frm): pos', c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
4.485 + end
4.486 + | generate1 _ (Begin_Trans' t) l (p, Frm) pt =
4.487 + let
4.488 + val (pt, c) = cappend_form pt p l t
4.489 val pt = update_branch pt p TransitiveB (*040312*)
4.490 - (*replace the old PrfOjb ~~~~~*)
4.491 - val p = (lev_on o lev_dn(*starts with [...,0]*)) p;
4.492 - val (pt,c') = cappend_form pt p l t(*FIXME.0402 same istate ???*);
4.493 - in ((p,Frm), c @ c', Form' (FormKF (~1,EdUndef,(length p), Nundef,
4.494 - term2str t)), pt) end
4.495 -
4.496 - (* val (thy, Begin_Trans' t, l, (p,Res), pt) =
4.497 - (assoc_thy "Isac", tac_, is, p, pt);
4.498 - *)
4.499 - | generate1 thy (Begin_Trans' t) l (p ,Res) pt =
4.500 - (*append after existing PrfObj _________*)
4.501 - generate1 thy (Begin_Trans' t) l (lev_on p,Frm) pt
4.502 -
4.503 - | generate1 thy (End_Trans' tasm) l (p,p_) pt =
4.504 + (* replace the old PrfOjb ~~~~~ *)
4.505 + val p = (lev_on o lev_dn (* starts with [...,0] *)) p
4.506 + val (pt, c') = cappend_form pt p l t (*FIXME.0402 same istate ???*)
4.507 + in
4.508 + ((p, Frm), c @ c', Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
4.509 + end
4.510 + | generate1 thy (Begin_Trans' t) l (p, Res) pt =
4.511 + (*append after existing PrfObj vvvvvvvvvvvvv*)
4.512 + generate1 thy (Begin_Trans' t) l (lev_on p, Frm) pt
4.513 + | generate1 _ (End_Trans' tasm) l (p, _) pt =
4.514 + let
4.515 + val p' = lev_up p
4.516 + val (pt, c) = append_result pt p' l tasm Complete
4.517 + in
4.518 + ((p', Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
4.519 + end
4.520 + | generate1 _ (Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (p, _) pt =
4.521 + let
4.522 + val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
4.523 + (Rewrite_Inst (subst2subs subs', thm')) (f',asm) Complete;
4.524 + val pt = update_branch pt p TransitiveB
4.525 + in ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt) end
4.526 + | generate1 _ (Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt =
4.527 + let
4.528 + val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
4.529 + (Rewrite thm') (f', asm) Complete
4.530 + val pt = update_branch pt p TransitiveB
4.531 + in
4.532 + ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
4.533 + end
4.534 + | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt
4.535 + | generate1 _ (Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (p, _) pt =
4.536 + let
4.537 + val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
4.538 + (Rewrite_Set_Inst (subst2subs subs', id_rls rls')) (f', asm) Complete
4.539 + val pt = update_branch pt p TransitiveB
4.540 + in
4.541 + ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
4.542 + end
4.543 + | generate1 thy (Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
4.544 + let
4.545 + val ctxt' = insert_assumptions asm ctxt
4.546 + val (pt, _) = cappend_form pt p (is, ctxt') f
4.547 + val pt = update_branch pt p TransitiveB
4.548 + val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
4.549 + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
4.550 + val pos' = ((lev_on o lev_dn) p, Frm)
4.551 + in
4.552 + generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*)
4.553 + end
4.554 + | generate1 _ (Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (p, _) pt =
4.555 + let
4.556 + val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
4.557 + (Rewrite_Set (id_rls rls')) (f',asm) Complete
4.558 + val pt = update_branch pt p TransitiveB
4.559 + in
4.560 + ((p, Res), c, Form' (FormKF (~1 ,EdUndef, length p, Nundef, term2str f')), pt)
4.561 + end
4.562 + | generate1 thy (Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
4.563 + let
4.564 + val ctxt' = insert_assumptions asm ctxt
4.565 + val (pt, _) = cappend_form pt p (is, ctxt') f
4.566 + val pt = update_branch pt p TransitiveB
4.567 + val is = init_istate (Rewrite_Set (id_rls rls)) f
4.568 + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
4.569 + val pos' = ((lev_on o lev_dn) p, Frm)
4.570 + in
4.571 + generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*)
4.572 + end
4.573 + | generate1 _ (Check_Postcond' (_, (scval, asm))) l (p, _) pt =
4.574 let
4.575 - val p' = lev_up p
4.576 - val (pt,c) = append_result pt p' l tasm Complete;
4.577 - in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
4.578 -
4.579 - | generate1 thy (Rewrite_Inst' (_,_,_,_,subs', thm', f, (f', asm))) (is, ctxt) (p,p_) pt =
4.580 + val (pt, c) = append_result pt p l (scval, asm) Complete
4.581 + in
4.582 + ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str scval)), pt)
4.583 + end
4.584 + | generate1 _ (Calculate' (_, op_, f, (f', _))) l (p, _) pt =
4.585 let
4.586 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
4.587 - (Rewrite_Inst (subst2subs subs', thm')) (f',asm) Complete;
4.588 - val pt = update_branch pt p TransitiveB
4.589 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
4.590 -
4.591 - | generate1 thy (Rewrite' (thy', ord', rls', pa, thm', f, (f', asm))) (is, ctxt) (p, p_) pt =
4.592 + val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f', []) Complete
4.593 + in
4.594 + ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
4.595 + end
4.596 + | generate1 _ (Check_elementwise' (consts, pred, (f', asm))) l (p, _) pt =
4.597 let
4.598 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
4.599 - (Rewrite thm') (f',asm) Complete
4.600 - val pt = update_branch pt p TransitiveB
4.601 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
4.602 -
4.603 - | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt
4.604 -
4.605 - | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) (is, ctxt) (p,p_) pt =
4.606 + val (pt,c) = cappend_atomic pt p l consts (Check_elementwise pred) (f',asm) Complete
4.607 + in
4.608 + ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
4.609 + end
4.610 + | generate1 _ (Or_to_List' (ors, list)) l (p, _) pt =
4.611 let
4.612 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
4.613 - (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
4.614 - val pt = update_branch pt p TransitiveB
4.615 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
4.616 -
4.617 - | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =
4.618 - let
4.619 - val ctxt' = insert_assumptions asm ctxt
4.620 - val (pt,c) = cappend_form pt p (is, ctxt') f
4.621 - val pt = update_branch pt p TransitiveB
4.622 -
4.623 - val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
4.624 - val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
4.625 - val pos' = ((lev_on o lev_dn) p, Frm)
4.626 - in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
4.627 -
4.628 - | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) (is, ctxt) (p,p_) pt =
4.629 - let
4.630 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
4.631 - (Rewrite_Set (id_rls rls')) (f',asm) Complete
4.632 - val pt = update_branch pt p TransitiveB
4.633 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
4.634 -
4.635 - | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =
4.636 - let
4.637 - val ctxt' = insert_assumptions asm ctxt
4.638 - val (pt,c) = cappend_form pt p (is, ctxt') f
4.639 - val pt = update_branch pt p TransitiveB
4.640 -
4.641 - val is = init_istate (Rewrite_Set (id_rls rls)) f
4.642 - val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
4.643 - val pos' = ((lev_on o lev_dn) p, Frm)
4.644 - in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
4.645 -
4.646 - | generate1 thy (Check_Postcond' (pI, (scval, asm))) l (p,p_) pt =
4.647 - let val (pt,c) = append_result pt p l (scval, asm) Complete
4.648 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str scval)), pt) end
4.649 -
4.650 - | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt =
4.651 - let val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f',[]) Complete;
4.652 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
4.653 -
4.654 - | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt =
4.655 - let
4.656 - val (pt,c) = cappend_atomic pt p l consts (Check_elementwise pred) (f',asm) Complete;
4.657 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
4.658 -
4.659 - | generate1 thy (Or_to_List' (ors,list)) l (p,p_) pt =
4.660 - let val (pt,c) = cappend_atomic pt p l ors Or_to_List (list,[]) Complete;
4.661 - in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)), pt) end
4.662 -
4.663 - | generate1 thy (Substitute' (_, _, subte, t, t')) l (p,p_) pt =
4.664 - let
4.665 - val (pt,c) =
4.666 - cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete;
4.667 - in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str t')), pt)
4.668 - end
4.669 -
4.670 - | generate1 thy (Tac_ (_,f,id,f')) l (p,p_) pt =
4.671 + val (pt,c) = cappend_atomic pt p l ors Or_to_List (list, []) Complete
4.672 + in
4.673 + ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str list)), pt)
4.674 + end
4.675 + | generate1 _ (Substitute' (_, _, subte, t, t')) l (p, _) pt =
4.676 let
4.677 val (pt,c) =
4.678 - cappend_atomic pt p l (str2term f) (Tac id) (str2term f',[]) Complete;
4.679 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end
4.680 -
4.681 - | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p,p_) pt =
4.682 + cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete
4.683 + in ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t')), pt)
4.684 + end
4.685 + | generate1 _ (Tac_ (_, f, id, f')) l (p, _) pt =
4.686 let
4.687 - val (pt,c) =
4.688 - cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);
4.689 - val pt = update_ctxt pt p ctxt
4.690 - val f = Syntax.string_of_term (thy2ctxt thy) f;
4.691 - in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
4.692 -
4.693 - | generate1 thy m' _ _ _ =
4.694 - error ("generate1: not impl.for "^(tac_2str m'));
4.695 + val (pt, c) = cappend_atomic pt p l (str2term f) (Tac id) (str2term f', []) Complete
4.696 + in
4.697 + ((p,Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, f')), pt)
4.698 + end
4.699 + | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p, _) pt =
4.700 + let
4.701 + val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl)
4.702 + val pt = update_ctxt pt p ctxt
4.703 + val f = Syntax.string_of_term (thy2ctxt thy) f
4.704 + in
4.705 + ((p, Pbl), c, Form' (FormKF (~1, EdUndef, length p, Nundef, f)), pt)
4.706 + end
4.707 + | generate1 _ m' _ _ _ = error ("generate1: not impl.for " ^ tac_2str m')
4.708
4.709 fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
4.710 let
4.711 - val f = get_curr_formula (pt, pos);
4.712 - val pos' as (p', _) = (lev_on p, Res);
4.713 - val (pt,c) =
4.714 - case subs_opt of
4.715 - NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
4.716 - (Rewrite thm') (f', []) Inconsistent
4.717 - | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
4.718 - (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
4.719 - val pt = update_branch pt p' TransitiveB;
4.720 + val f = get_curr_formula (pt, pos)
4.721 + val pos' as (p', _) = (lev_on p, Res)
4.722 + val (pt, _) = case subs_opt of
4.723 + NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
4.724 + (Rewrite thm') (f', []) Inconsistent
4.725 + | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
4.726 + (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
4.727 + val pt = update_branch pt p' TransitiveB
4.728 in (pt, pos') end
4.729
4.730 fun generate_hard thy m' (p,p_) pt =
4.731 let
4.732 - val p =
4.733 - case p_ of
4.734 - Frm => p | Res => lev_on p
4.735 - | _ => error ("generate_hard: call by " ^ pos'2str (p,p_));
4.736 - in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end;
4.737 + val p = case p_ of
4.738 + Frm => p | Res => lev_on p
4.739 + | _ => error ("generate_hard: call by " ^ pos'2str (p,p_))
4.740 + in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end
4.741
4.742 -(*tacis are in reverse order from nxt_solve_/specify_: last = fst to insert*)
4.743 +(* tacis are in reverse order from nxt_solve_/specify_: last = fst to insert *)
4.744 fun generate ([]: taci list) ptp = ptp
4.745 - | generate tacis (pt, c, _:pos'(*!dropped!WN0504redesign generate/tacis?*))=
4.746 - let
4.747 - val (tacis', (_, tac_, (p, is))) = split_last tacis
4.748 - val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
4.749 - in generate tacis' (pt', c@c', p') end;
4.750 + | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*))=
4.751 + let
4.752 + val (tacis', (_, tac_, (p, is))) = split_last tacis
4.753 + val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
4.754 + in
4.755 + generate tacis' (pt', c@c', p')
4.756 + end
4.757
4.758 -(*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
4.759 - * of for connecting a user-input formula with the current calc-state. *
4.760 - *# It is somewhat incompatible with the rest of the math-engine: *
4.761 - * (1) it is not created by a script *
4.762 - * (2) thus there cannot be another user-input within a derivation *
4.763 - *# It suffers particularily from the not-well-foundedness of the math-engine*
4.764 - * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
4.765 - * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
4.766 - * (3) FIXME and eventually 'lev_back' *
4.767 - *# SOME improvements are evident FIXME.040215 '_deriv'ation: *
4.768 - * (1) FIXME nest Rls_ in 'make_deriv' *
4.769 - * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
4.770 - * user-input will become possible in this part of a derivation *
4.771 - * (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
4.772 - * while a non-derivable inform requires to step until End_Proof' *
4.773 - * (4) FIXME find criteria on when _not_ to step until End_Proof' *
4.774 - * (5) FIXME
4.775 -.*)
4.776 -(*.update pos in tacis for embedding by generate.*)
4.777 -(* val
4.778 - *)
4.779 -fun insert_pos _ [] = []
4.780 - | insert_pos (p:pos) (((tac,tac_,(_, ist))::tacis):taci list) =
4.781 - ((tac,tac_,((p, Res), ist)):taci)
4.782 - ::((insert_pos (lev_on p) tacis):taci list);
4.783 +(* update pos in tacis for embedding by generate *)
4.784 +fun insert_pos (_: pos) [] = []
4.785 + | insert_pos (p: pos) (((tac, tac_, (_, ist)): taci) :: tacis) =
4.786 + ((tac, tac_, ((p, Res), ist)): taci) :: (insert_pos (lev_on p) tacis)
4.787
4.788 -fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm)
4.789 - | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm)
4.790 - | res_from_taci (_, tac_, _) =
4.791 - error ("res_from_taci: called with" ^ tac_2str tac_);
4.792 +fun res_from_taci (_, Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
4.793 + | res_from_taci (_, Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
4.794 + | res_from_taci (_, tac_, _) = error ("res_from_taci: called with" ^ tac_2str tac_)
4.795
4.796 -(*.embed the tacis created by a '_deriv'ation; sys.form <> input.form
4.797 - tacis are in order, thus are reverted for generate.*)
4.798 -(* val (tacis, (pt, pos as (p, Frm))) = (tacis', ptp);
4.799 - *)
4.800 -fun embed_deriv (tacis:taci list) (pt, pos as (p, Frm):pos') =
4.801 +(* embed the tacis created by a '_deriv'ation; sys.form <> input.form
4.802 + tacis are in order, thus are reverted for generate *)
4.803 +fun embed_deriv (tacis: taci list) (pt, pos as (p, Frm): pos') =
4.804 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
4.805 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
4.806 + let
4.807 + val (res, asm) = (res_from_taci o last_elem) tacis
4.808 + val (ist, ctxt) = case get_obj g_loc pt p of
4.809 + (SOME (ist, ctxt), _) => (ist, ctxt)
4.810 + | (NONE, _) => error "embed_deriv Frm: uncovered case get_obj"
4.811 + val form = get_obj g_form pt p
4.812 + (*val p = lev_on p; ---------------only difference to (..,Res) below*)
4.813 + val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt))) ::
4.814 + (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm),
4.815 + (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]
4.816 + val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
4.817 + val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
4.818 + val pt = update_tac pt p (Derive (id_rls nrls))
4.819 + val pt = update_branch pt p TransitiveB
4.820 + in (c, (pt, pos: pos')) end
4.821 + | embed_deriv tacis (pt, (p, Res)) =
4.822 + (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
4.823 + and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
4.824 let val (res, asm) = (res_from_taci o last_elem) tacis
4.825 - val (SOME (ist, ctxt),_) = get_obj g_loc pt p
4.826 - val form = get_obj g_form pt p
4.827 - (*val p = lev_on p; ---------------only difference to (..,Res) below*)
4.828 - val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt)))
4.829 - ::(insert_pos ((lev_on o lev_dn) p) tacis)
4.830 - @ [(End_Trans, End_Trans' (res, asm),
4.831 - (pos_plus (length tacis) (lev_dn p, Res),
4.832 - (new_val res ist, ctxt)))]
4.833 - val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
4.834 - val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
4.835 - val pt = update_tac pt p (Derive (id_rls nrls))
4.836 - (*FIXME.040216 struct.ctree*)
4.837 - val pt = update_branch pt p TransitiveB
4.838 - in (c, (pt, pos:pos')) end
4.839 -
4.840 -(* val (tacis, (pt, (p, Res))) = (tacis', ptp);
4.841 - *)
4.842 - | embed_deriv tacis (pt, (p, Res)) =
4.843 - (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
4.844 - and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
4.845 - let val (res, asm) = (res_from_taci o last_elem) tacis
4.846 - val (_, SOME (ist, ctxt)) = get_obj g_loc pt p
4.847 - val (f,a) = get_obj g_result pt p
4.848 - val p = lev_on p(*---------------only difference to (..,Frm) above*);
4.849 - val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt)))
4.850 - ::(insert_pos ((lev_on o lev_dn) p) tacis)
4.851 - @ [(End_Trans, End_Trans' (res, asm),
4.852 - (pos_plus (length tacis) (lev_dn p, Res),
4.853 - (new_val res ist, ctxt)))];
4.854 - val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
4.855 - val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
4.856 - val pt = update_tac pt p (Derive (id_rls nrls))
4.857 - (*FIXME.040216 struct.ctree*)
4.858 - val pt = update_branch pt p TransitiveB
4.859 - in (c, (pt, pos)) end;
4.860 + val (ist, ctxt) = case get_obj g_loc pt p of
4.861 + (_, SOME (ist, ctxt)) => (ist, ctxt)
4.862 + | (_, NONE) => error "embed_deriv Frm: uncovered case get_obj"
4.863 + val (f, _) = get_obj g_result pt p
4.864 + val p = lev_on p(*---------------only difference to (..,Frm) above*);
4.865 + val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt))) ::
4.866 + (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm),
4.867 + (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];
4.868 + val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
4.869 + val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
4.870 + val pt = update_tac pt p (Derive (id_rls nrls))
4.871 + val pt = update_branch pt p TransitiveB
4.872 + in (c, (pt, pos)) end
4.873 + | embed_deriv _ _ = error "embed_deriv: uncovered definition"
4.874 +end
4.875 \ No newline at end of file
5.1 --- a/src/Tools/isac/Interpret/inform.sml Mon Dec 12 18:08:13 2016 +0100
5.2 +++ b/src/Tools/isac/Interpret/inform.sml Wed Dec 14 09:37:01 2016 +0100
5.3 @@ -19,7 +19,7 @@
5.4 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
5.5 val cas_input : term -> (ptree * ocalhd) option
5.6 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
5.7 - val compare_step : taci list * pos' list * (ptree * pos') -> term -> string * Chead.calcstate'
5.8 + val compare_step : Ctree.taci list * pos' list * (ptree * pos') -> term -> string * Chead.calcstate'
5.9 val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
5.10 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
5.11 rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
5.12 @@ -389,7 +389,7 @@
5.13 then
5.14 let
5.15 val tacis' = map (mk_tacis rew_ord erls) der;
5.16 - val (c', ptp) = embed_deriv tacis' ptp;
5.17 + val (c', ptp) = Ctree.embed_deriv tacis' ptp;
5.18 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
5.19 else
5.20 if pos = ([], Res) (*TODO: we should stop earlier with trying subproblems *)
6.1 --- a/src/Tools/isac/Interpret/mathengine.sml Mon Dec 12 18:08:13 2016 +0100
6.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed Dec 14 09:37:01 2016 +0100
6.3 @@ -9,11 +9,11 @@
6.4 signature MATH_ENGINE =
6.5 sig
6.6 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
6.7 - val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * mout * tac'_ * safe * ptree
6.8 + val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Ctree.mout * tac'_ * safe * ptree
6.9 val autocalc :
6.10 - pos' list -> pos' -> (ptree * pos') * taci list -> auto -> string * pos' list * (ptree * pos')
6.11 + pos' list -> pos' -> (ptree * pos') * Ctree.taci list -> auto -> string * pos' list * (ptree * pos')
6.12 val locatetac :
6.13 - tac -> ptree * (posel list * pos_) -> string * (taci list * pos' list * (ptree * pos'))
6.14 + tac -> ptree * (posel list * pos_) -> string * (Ctree.taci list * pos' list * (ptree * pos'))
6.15 val step : pos' -> Chead.calcstate -> string * Chead.calcstate'
6.16 val detailstep :
6.17 ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option
6.18 @@ -30,8 +30,8 @@
6.19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.20 type nxt_
6.21 type lOc_
6.22 - val CalcTreeTEST : fmz list -> pos' * NEW * mout * (string * tac) * safe * ptree
6.23 - val f2str : mout -> cterm'
6.24 + val CalcTreeTEST : fmz list -> pos' * NEW * Ctree.mout * (string * tac) * safe * ptree
6.25 + val f2str : Ctree.mout -> cterm'
6.26 val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_
6.27 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.28 end
6.29 @@ -62,7 +62,7 @@
6.30 let
6.31 val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
6.32 in
6.33 - case f of (Error' (Error_ e)) => ERror e | _ => Updated ([], [], (pt,p))
6.34 + case f of (Ctree.Error' (Ctree.Error_ e)) => ERror e | _ => Updated ([], [], (pt,p))
6.35 end
6.36
6.37 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
6.38 @@ -195,7 +195,7 @@
6.39 (_::_) =>
6.40 if ip = p (*the request is done where ptp waits for*)
6.41 then
6.42 - let val (pt',c',p') = generate tacis (pt,[],p)
6.43 + let val (pt',c',p') = Ctree.generate tacis (pt,[],p)
6.44 in ("ok", (tacis, c', (pt', p'))) end
6.45 else (case (if member op = [Pbl, Met] p_
6.46 then nxt_specify_ (pt, ip) else nxt_solve_ (pt, ip))
6.47 @@ -368,10 +368,10 @@
6.48 val (form, _, _) = Chead.pt_extract ptp
6.49 in
6.50 case form of
6.51 - Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
6.52 + Form t => Ctree.Form' (Ctree.FormKF (~1,Ctree.EdUndef,0,Ctree.Nundef,term2str t))
6.53 | ModSpec (_,p_, _, gfr, pre, _) =>
6.54 - Form' (PpcKF (0, EdUndef, 0, Nundef,
6.55 - (case p_ of Pbl => Problem [] | Met => Method [] | _ => error "TESTg_form: uncovered case",
6.56 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, 0, Ctree.Nundef,
6.57 + (case p_ of Pbl => Ctree.Problem [] | Met => Ctree.Method [] | _ => error "TESTg_form: uncovered case",
6.58 itms2itemppc (assoc_thy"Isac") gfr pre)))
6.59 end;
6.60
6.61 @@ -421,6 +421,6 @@
6.62 end
6.63
6.64 (* for quick test-print-out, until 'type inout' is removed *)
6.65 -fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';
6.66 +fun f2str (Ctree.Form' (Ctree.FormKF (_, _, _, _, cterm'))) = cterm';
6.67
6.68 end
7.1 --- a/src/Tools/isac/Interpret/rewtools.sml Mon Dec 12 18:08:13 2016 +0100
7.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Dec 14 09:37:01 2016 +0100
7.3 @@ -54,7 +54,24 @@
7.4 struct
7.5 (**)
7.6 (*** reverse rewriting ***)
7.7 -
7.8 +(*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
7.9 + * of for connecting a user-input formula with the current calc-state. *
7.10 + *# It is somewhat incompatible with the rest of the math-engine: *
7.11 + * (1) it is not created by a script *
7.12 + * (2) thus there cannot be another user-input within a derivation *
7.13 + *# It suffers particularily from the not-well-foundedness of the math-engine*
7.14 + * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
7.15 + * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
7.16 + * (3) FIXME and eventually 'lev_back' *
7.17 + *# SOME improvements are evident FIXME.040215 '_deriv'ation: *
7.18 + * (1) FIXME nest Rls_ in 'make_deriv' *
7.19 + * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
7.20 + * user-input will become possible in this part of a derivation *
7.21 + * (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
7.22 + * while a non-derivable inform requires to step until End_Proof' *
7.23 + * (4) FIXME find criteria on when _not_ to step until End_Proof' *
7.24 + * (5) FIXME
7.25 +.*)
7.26 type deriv = (* derivation for insertin one level of nodes into the calctree *)
7.27 ( term * (* where the rule is applied to *)
7.28 rule * (* rule to be applied *)
8.1 --- a/src/Tools/isac/Interpret/script.sml Mon Dec 12 18:08:13 2016 +0100
8.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Dec 14 09:37:01 2016 +0100
8.3 @@ -8,7 +8,7 @@
8.4 signature LUCAS_INTERPRETER =
8.5 sig
8.6
8.7 - type step = tac_ * mout * ptree * pos' * pos' list
8.8 + type step = tac_ * Ctree.mout * ptree * pos' * pos' list
8.9 datatype locate = NotLocatable | Steps of istate * step list
8.10
8.11 val next_tac : (*diss: next-tactic-function*)
8.12 @@ -61,7 +61,7 @@
8.13 Assoc (scrstate, steps) => ... ass* scrstate steps *)
8.14 type step =
8.15 tac_ (*transformed from associated tac *)
8.16 - * mout (*result with indentation etc. *)
8.17 + * Ctree.mout (*result with indentation etc. *)
8.18 * ptree (*containing node created by tac_ + resp. scrstate *)
8.19 * pos' (*position in ptree; ptree * pos' is the proofstate *)
8.20 * pos' list; (*of ptree-nodes probably cut (by fst tac_) *)
8.21 @@ -80,7 +80,7 @@
8.22 val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
8.23 val is = RrlsState (f', f'', rss, rts)
8.24 val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
8.25 - val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
8.26 + val (p', cid, mout, pt') = Ctree.generate1 thy m (is, ctxt) p pt
8.27 in (is, (m, mout, pt', p', cid) :: steps) end
8.28 | rts2steps steps ((pt, p) ,(f, f'', rss, rts), (thy', ro, er, pa)) ((r, (f', am)) :: rts') =
8.29 let
8.30 @@ -89,7 +89,7 @@
8.31 val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
8.32 val is = RrlsState (f', f'', rss, rts)
8.33 val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
8.34 - val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
8.35 + val (p', cid, mout, pt') = Ctree.generate1 thy m (is, ctxt) p pt
8.36 in rts2steps ((m, mout, pt', p', cid)::steps)
8.37 ((pt', p'), (f', f'', rss, rts), (thy', ro, er, pa)) rts'
8.38 end
8.39 @@ -665,11 +665,11 @@
8.40 case assod pt d m stac of
8.41 Ass (m,v') =>
8.42 let val (p'',c',f',pt') =
8.43 - generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
8.44 + Ctree.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
8.45 in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
8.46 | AssWeak (m,v') =>
8.47 let val (p'',c',f',pt') =
8.48 - generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
8.49 + Ctree.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
8.50 in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
8.51 | NotAss =>
8.52 (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
8.53 @@ -680,7 +680,7 @@
8.54 let
8.55 val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
8.56 val (p'',c',f',pt') =
8.57 - generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p',p_) pt;
8.58 + Ctree.generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p', p_) pt;
8.59 in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
8.60 | Chead.Notappl _ => (NasNap (v, E))
8.61 )
8.62 @@ -822,8 +822,8 @@
8.63 let val thy = assoc_thy thy';
8.64 in case if l = [] orelse (
8.65 (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res)
8.66 - then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
8.67 - else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of
8.68 + then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,Ctree.EmptyMout,pt,p,[])]) body)
8.69 + else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,Ctree.EmptyMout,pt,p,[])]) ) of
8.70 Assoc ((is as (_,_,_,_,_,strong_ass), ss as (_ :: _))) =>
8.71 (if strong_ass
8.72 then (Steps (ScrState is, ss))
8.73 @@ -833,7 +833,7 @@
8.74 let
8.75 val (po,p_) = p
8.76 val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_gen " ^ pos_2str p_)
8.77 - val (p'',c'',f'',pt'') = generate1 thy m (ScrState is, ctxt) (po',p_) pt
8.78 + val (p'',c'',f'',pt'') = Ctree.generate1 thy m (ScrState is, ctxt) (po',p_) pt
8.79 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
8.80 else Steps (ScrState is, ss))
8.81
9.1 --- a/src/Tools/isac/Interpret/solve.sml Mon Dec 12 18:08:13 2016 +0100
9.2 +++ b/src/Tools/isac/Interpret/solve.sml Wed Dec 14 09:37:01 2016 +0100
9.3 @@ -135,7 +135,7 @@
9.4
9.5
9.6 fun step2taci ((tac_, _, pt, p, _) : Lucin.step) = (*FIXXME.040312: redesign step*)
9.7 - (Lucin.tac_2tac tac_, tac_, (p, get_loc pt p)):taci;
9.8 + (Lucin.tac_2tac tac_, tac_, (p, get_loc pt p)): Ctree.taci;
9.9
9.10
9.11 (*FIXME.WN050821 compare solve ... nxt_solv*)
9.12 @@ -154,7 +154,7 @@
9.13 case ini of
9.14 SOME t =>
9.15 let val (pos,c,_,pt) =
9.16 - generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
9.17 + Ctree.generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
9.18 (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
9.19 in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
9.20 ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos)) : Chead.calcstate')
9.21 @@ -168,7 +168,7 @@
9.22 Lucin.Steps (is'', ss as (m'',f',pt',p',c')::_) =>
9.23 ("ok", (map step2taci ss, c', (pt',p')))
9.24 | NotLocatable =>
9.25 - let val (p,ps,f,pt) = generate_hard (assoc_thy "Isac") m (p,Frm) pt;
9.26 + let val (p,ps,f,pt) = Ctree.generate_hard (assoc_thy "Isac") m (p,Frm) pt;
9.27 in
9.28 ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p)))
9.29 end
9.30 @@ -203,7 +203,7 @@
9.31 let
9.32 val is = ScrState (E,l,a,scval,scsaf,b)
9.33 val tac_ = Check_Postcond' (pI, (scval, asm))
9.34 - val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt;
9.35 + val (pos,ps,f,pt) = Ctree.generate1 thy tac_ (is, ctxt) (pp,Res) pt;
9.36 in ("ok", ([(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
9.37 else
9.38 let (*resume script of parpbl, transfer value of subpbl-script*)
9.39 @@ -215,7 +215,7 @@
9.40 val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm);
9.41 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
9.42 val ((p,p_),ps,f,pt) =
9.43 - generate1 thy (Check_Postcond' (pI, (scval, asm)))
9.44 + Ctree.generate1 thy (Check_Postcond' (pI, (scval, asm)))
9.45 (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
9.46 in ("ok", ([(Check_Postcond pI, Check_Postcond'(pI,(scval, asm)),
9.47 ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_))))
9.48 @@ -246,7 +246,7 @@
9.49 let
9.50 val ctxt = get_ctxt pt po
9.51 val ((p,p_),ps,f,pt) =
9.52 - generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
9.53 + Ctree.generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
9.54 m (e_istate, ctxt) (p,p_) pt;
9.55 in ("no-method-specified", (*Free_Solve*)
9.56 ([(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, ctxt)))], ps, (pt,(p,p_))))
9.57 @@ -264,7 +264,7 @@
9.58 in ("ok", (map step2taci ss, c', (pt',p'))) end
9.59 | NotLocatable =>
9.60 let val (p,ps,f,pt) =
9.61 - generate_hard (assoc_thy "Isac") m (p,p_) pt;
9.62 + Ctree.generate_hard (assoc_thy "Isac") m (p,p_) pt;
9.63 in ("not-found-in-script",
9.64 ([(Lucin.tac_2tac m, m, (po,is))], ps, (pt,p)))
9.65 end
9.66 @@ -288,7 +288,7 @@
9.67 val pos = ((lev_on o lev_dn) p, Frm)
9.68 val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
9.69 val (pos,c,_,pt) = (*implicit Take*)
9.70 - generate1 thy tac_ (is, ctxt) pos pt
9.71 + Ctree.generate1 thy tac_ (is, ctxt) pos pt
9.72 in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)) : Chead.calcstate' end
9.73 | NONE =>
9.74 let
9.75 @@ -323,7 +323,7 @@
9.76 val is = ScrState (E,l,a,scval,scsaf,b)
9.77 val tac_ = Check_Postcond'(pI,(scval, asm))
9.78 val ((p,p_),ps,f,pt) =
9.79 - generate1 thy tac_ (is, ctxt) (pp,Res) pt;
9.80 + Ctree.generate1 thy tac_ (is, ctxt) (pp,Res) pt;
9.81 in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
9.82 else
9.83 let (*resume script of parpbl, transfer value of subpbl-script*)
9.84 @@ -336,7 +336,7 @@
9.85 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
9.86 val tac_ = Check_Postcond' (pI, (scval, asm))
9.87 val is = ScrState (E,l,a,scval,scsaf,b)
9.88 - val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
9.89 + val ((p,p_),ps,f,pt) = Ctree.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
9.90 in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end
9.91 end
9.92
9.93 @@ -349,7 +349,7 @@
9.94 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
9.95 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
9.96 | _ => pos
9.97 - val (pos',c,_,pt) = generate1 (assoc_thy "Isac") tac_ is pos pt;
9.98 + val (pos',c,_,pt) = Ctree.generate1 (assoc_thy "Isac") tac_ is pos pt;
9.99 in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
9.100
9.101 (* find the next tac from the script, nxt_solv will update the ptree *)
9.102 @@ -448,13 +448,13 @@
9.103 in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
9.104 | _ =>
9.105 let
9.106 - val is = init_istate tac t
9.107 + val is = Ctree.init_istate tac t
9.108 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
9.109 is wrong for simpl, but working ?!? *)
9.110 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
9.111 val pos' = ((lev_on o lev_dn) p, Frm)
9.112 val thy = assoc_thy "Isac"
9.113 - val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, ctxt) pos' pt
9.114 + val (_,_,_,pt') = (*implicit Take*)Ctree.generate1 thy tac_ (is, ctxt) pos' pt
9.115 val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
9.116 val newnds = children (get_nd pt'' p)
9.117 val pt''' = ins_chn newnds pt p
9.118 @@ -469,7 +469,7 @@
9.119 *)
9.120 fun get_form ((mI,m):tac'_) ((p,p_):pos') pt =
9.121 case applicable_in (p,p_) pt m of
9.122 - Chead.Notappl e => Error' (Error_ e)
9.123 + Chead.Notappl e => Ctree.Error' (Ctree.Error_ e)
9.124 | Chead.Appl m =>
9.125 (* val Appl m=applicable_in (p,p_) pt m;
9.126 *)
9.127 @@ -477,5 +477,5 @@
9.128 then let val (_,_,f,_,_,_) = Chead.specify m (p,p_) [] pt
9.129 in f end
9.130 else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))
9.131 - in (*f*) EmptyMout end;
9.132 + in (*f*) Ctree.EmptyMout end;
9.133
10.1 --- a/test/Tools/isac/Test_Isac.thy Mon Dec 12 18:08:13 2016 +0100
10.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Dec 14 09:37:01 2016 +0100
10.3 @@ -75,6 +75,7 @@
10.4 open Inform; cas_input;
10.5 open Rtools; trtas2str;
10.6 open Chead; pt_extract;
10.7 + open Ctree; (*//*)
10.8 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.9 *}
10.10 ML {*