1.1 --- a/src/Tools/isac/Interpret/generate.sml Tue Mar 13 15:04:27 2018 +0100
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Thu Mar 15 10:17:44 2018 +0100
1.3 @@ -9,13 +9,13 @@
1.4 (* for calchead.sml --------------------------------------------------------------- vvv *)
1.5 type taci
1.6 val e_taci : taci
1.7 - datatype pblmet = Method of metID | Problem of pblID | Upblmet
1.8 + datatype pblmet = Method of Celem.metID | Problem of Celem.pblID | Upblmet
1.9 datatype mout =
1.10 EmptyMout
1.11 | Error' of string
1.12 - | FormKF of cterm'
1.13 + | FormKF of Celem.cterm'
1.14 | PpcKF of pblmet * Model.item Model.ppc
1.15 - | RefinedKF of pblID * (Model.itm list * (bool * term) list)
1.16 + | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
1.17 val generate1 : theory -> Tac.tac_ -> Selem.istate * Proof.context ->
1.18 Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree (* for calchead.sml------------- ^^^ *)
1.19 val init_istate : Tac.tac -> term -> Selem.istate (* for solve.sml *)
1.20 @@ -26,7 +26,7 @@
1.21 theory -> Tac.tac_ -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree
1.22 val generate : (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list ->
1.23 Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
1.24 - val generate_inconsistent_rew : Selem.subs option * thm'' -> term -> Selem.istate * Proof.context ->
1.25 + val generate_inconsistent_rew : Selem.subs option * Celem.thm'' -> term -> Selem.istate * Proof.context ->
1.26 Ctree.pos' -> Ctree.ctree -> Ctree.state (* for interface.sml *)
1.27 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.28 val tacis2str : taci list -> string
1.29 @@ -45,36 +45,36 @@
1.30 (* initialize istate for Detail_Set *)
1.31 fun init_istate (Tac.Rewrite_Set rls) t =
1.32 (case assoc_rls rls of
1.33 - Rrls {scr = Rfuns {init_state = ii, ...}, ...} => Selem.RrlsState (ii t)
1.34 - | Rls {scr = EmptyScr, ...} =>
1.35 + Celem.Rrls {scr = Celem.Rfuns {init_state = ii, ...}, ...} => Selem.RrlsState (ii t)
1.36 + | Celem.Rls {scr = EmptyScr, ...} =>
1.37 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
1.38 "use prep_rls' for storing rule-sets !")
1.39 - | Rls {scr = Prog s, ...} => (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, e_term, Selem.Sundef, true))
1.40 - | Seq {scr=EmptyScr,...} =>
1.41 + | Celem.Rls {scr = Celem.Prog s, ...} => (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Celem.e_term, Selem.Sundef, true))
1.42 + | Celem.Seq {scr=EmptyScr,...} =>
1.43 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
1.44 "use prep_rls' for storing rule-sets !")
1.45 - | Seq {scr = Prog s,...} => (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, e_term, Selem.Sundef, true))
1.46 + | Celem.Seq {scr = Celem.Prog s,...} => (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Celem.e_term, Selem.Sundef, true))
1.47 | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
1.48 | init_istate (Tac.Rewrite_Set_Inst (subs, rls)) t =
1.49 let
1.50 - val v = case Selem.subs2subst (assoc_thy "Isac") subs of
1.51 + val v = case Selem.subs2subst (Celem.assoc_thy "Isac") subs of
1.52 (_, v) :: _ => v
1.53 | _ => error "init_istate: uncovered case "
1.54 (*...we suppose the substitution of only _one_ bound variable*)
1.55 in case assoc_rls rls of
1.56 - Rls {scr = EmptyScr, ...} =>
1.57 + Celem.Rls {scr = EmptyScr, ...} =>
1.58 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
1.59 "use prep_rls' for storing rule-sets !")
1.60 - | Rls {scr = Prog s, ...} =>
1.61 + | Celem.Rls {scr = Celem.Prog s, ...} =>
1.62 let val (form, bdv) = LTool.two_scr_arg s
1.63 - in (Selem.ScrState ([(form, t), (bdv, v)], [], NONE, e_term, Selem.Sundef,true))
1.64 + in (Selem.ScrState ([(form, t), (bdv, v)], [], NONE, Celem.e_term, Selem.Sundef,true))
1.65 end
1.66 - | Seq {scr = EmptyScr, ...} =>
1.67 + | Celem.Seq {scr = EmptyScr, ...} =>
1.68 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
1.69 "use prep_rls' for storing rule-sets !")
1.70 - | Seq {scr = Prog s,...} =>
1.71 + | Celem.Seq {scr = Celem.Prog s,...} =>
1.72 let val (form, bdv) = LTool.two_scr_arg s
1.73 - in (Selem.ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Selem.Sundef,true))
1.74 + in (Selem.ScrState ([(form, t), (bdv, v)],[], NONE, Celem.e_term, Selem.Sundef,true))
1.75 end
1.76 | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls"
1.77 end
1.78 @@ -98,21 +98,21 @@
1.79 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
1.80 "( " ^ Tac.tac2str tac ^ ", " ^ Tac.tac_2str tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
1.81 Selem.istate2str istate ^ " ))"
1.82 -fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis
1.83 +fun tacis2str tacis = (strs2str o (map (Celem.linefeed o taci2str))) tacis
1.84
1.85 -datatype pblmet = (*%^%*)
1.86 - Upblmet (*undefined*)
1.87 -| Problem of pblID (*%^%*)
1.88 -| Method of metID; (*%^%*)
1.89 +datatype pblmet = (*%^%*)
1.90 + Upblmet (*undefined*)
1.91 +| Problem of Celem.pblID (*%^%*)
1.92 +| Method of Celem.metID; (*%^%*)
1.93 fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)
1.94 - | pblmet2str (Method metID) = "Method " ^ metID2str metID (*%^%*)
1.95 + | pblmet2str (Method metID) = "Method " ^ Celem.metID2str metID (*%^%*)
1.96 | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x)
1.97
1.98 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
1.99 datatype foppFK = (* in DG cases div 2 *)
1.100 EmptyFoppFK (*DG internal*)
1.101 -| FormFK of cterm'
1.102 -| PpcFK of cterm' Model.ppc
1.103 +| FormFK of Celem.cterm'
1.104 +| PpcFK of Celem.cterm' Model.ppc
1.105 fun foppFK2str (FormFK ct') ="FormFK " ^ ct'
1.106 | foppFK2str (PpcFK ppc) ="PpcFK " ^ Model.ppc2str ppc
1.107 | foppFK2str EmptyFoppFK ="EmptyFoppFK"
1.108 @@ -132,19 +132,19 @@
1.109 | edit2str Protect = "Protect";
1.110
1.111 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
1.112 - Error_ of string (*<--*)
1.113 -| FormKF of cellID * edit * indent * nest * cterm' (*<--*)
1.114 + Error_ of string (*<--*)
1.115 +| FormKF of cellID * edit * indent * nest * Celem.cterm' (*<--*)
1.116 | PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*)
1.117 -| RefineKF of Stool.match list (*<--*)
1.118 -| RefinedKF of (pblID * ((Model.itm list) * ((bool * term) list))) (*<--*)
1.119 +| RefineKF of Stool.match list (*<--*)
1.120 +| RefinedKF of (Celem.pblID * ((Model.itm list) * ((bool * term) list))) (*<--*)
1.121
1.122 (*
1.123 datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
1.124 *)
1.125 datatype mout =
1.126 - FormKF of cterm'
1.127 + FormKF of Celem.cterm'
1.128 | PpcKF of (pblmet * Model.item Model.ppc)
1.129 -| RefinedKF of pblID * (Model.itm list * (bool * term) list)
1.130 +| RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
1.131 | Error' of string
1.132 | EmptyMout
1.133
1.134 @@ -157,13 +157,13 @@
1.135 (* init pbl with ...,dsc,empty | [] *)
1.136 fun init_pbl pbt =
1.137 let
1.138 - fun pbt2itm (f, (d, _)) = (0, [], false, f, Model.Inc ((d, []), (e_term, [])))
1.139 + fun pbt2itm (f, (d, _)) = (0, [], false, f, Model.Inc ((d, []), (Celem.e_term, [])))
1.140 in map pbt2itm pbt end
1.141
1.142 (* take formal parameters from pbt, for transfer from pbl/met-hierarchy *)
1.143 fun init_pbl' pbt =
1.144 let
1.145 - fun pbt2itm (f, (d, t)) = (0, [], false, f, Model.Inc((d, [t]), (e_term, [])))
1.146 + fun pbt2itm (f, (d, t)) = (0, [], false, f, Model.Inc((d, [t]), (Celem.e_term, [])))
1.147 in map pbt2itm pbt end
1.148
1.149 (*generate 1 ppobj in ctree*)
1.150 @@ -241,7 +241,7 @@
1.151 in if p' = 0 then ps @ [1] else p end
1.152 val (pt, c) = cappend_form pt p l t
1.153 in
1.154 - ((p, Frm): pos', c, FormKF (term2str t), pt)
1.155 + ((p, Frm): pos', c, FormKF (Celem.term2str t), pt)
1.156 end
1.157 | generate1 _ (Tac.Begin_Trans' t) l (p, Frm) pt =
1.158 let
1.159 @@ -251,7 +251,7 @@
1.160 val p = (lev_on o lev_dn (* starts with [...,0] *)) p
1.161 val (pt, c') = cappend_form pt p l t (*FIXME.0402 same istate ???*)
1.162 in
1.163 - ((p, Frm), c @ c', FormKF (term2str t), pt)
1.164 + ((p, Frm), c @ c', FormKF (Celem.term2str t), pt)
1.165 end
1.166 | generate1 thy (Tac.Begin_Trans' t) l (p, Res) pt =
1.167 (*append after existing PrfObj vvvvvvvvvvvvv*)
1.168 @@ -269,7 +269,7 @@
1.169 (Tac.Rewrite_Inst (Selem.subst2subs subs', thm')) (f',asm) Complete;
1.170 val pt = update_branch pt p TransitiveB
1.171 in
1.172 - ((p, Res), c, FormKF (term2str f'), pt)
1.173 + ((p, Res), c, FormKF (Celem.term2str f'), pt)
1.174 end
1.175 | generate1 _ (Tac.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt =
1.176 let
1.177 @@ -277,24 +277,24 @@
1.178 (Tac.Rewrite thm') (f', asm) Complete
1.179 val pt = update_branch pt p TransitiveB
1.180 in
1.181 - ((p, Res), c, FormKF (term2str f'), pt)
1.182 + ((p, Res), c, FormKF (Celem.term2str f'), pt)
1.183 end
1.184 | generate1 thy (Tac.Rewrite_Asm' all) l p pt = generate1 thy (Tac.Rewrite' all) l p pt
1.185 | generate1 _ (Tac.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (p, _) pt =
1.186 let
1.187 val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f
1.188 - (Tac.Rewrite_Set_Inst (Selem.subst2subs subs', id_rls rls')) (f', asm) Complete
1.189 + (Tac.Rewrite_Set_Inst (Selem.subst2subs subs', Celem.id_rls rls')) (f', asm) Complete
1.190 val pt = update_branch pt p TransitiveB
1.191 in
1.192 - ((p, Res), c, FormKF (term2str f'), pt)
1.193 + ((p, Res), c, FormKF (Celem.term2str f'), pt)
1.194 end
1.195 | generate1 thy (Tac.Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
1.196 let
1.197 val ctxt' = Stool.insert_assumptions asm ctxt
1.198 val (pt, _) = cappend_form pt p (is, ctxt') f
1.199 val pt = update_branch pt p TransitiveB
1.200 - val is = init_istate (Tac.Rewrite_Set_Inst (Selem.subst2subs subs, id_rls rls)) f
1.201 - val tac_ = Tac.Apply_Method' (e_metID, SOME e_term (*t ..has not been declared*), is, ctxt')
1.202 + val is = init_istate (Tac.Rewrite_Set_Inst (Selem.subst2subs subs, Celem.id_rls rls)) f
1.203 + val tac_ = Tac.Apply_Method' (Celem.e_metID, SOME Celem.e_term (*t ..has not been declared*), is, ctxt')
1.204 val pos' = ((lev_on o lev_dn) p, Frm)
1.205 in
1.206 generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*)
1.207 @@ -302,18 +302,18 @@
1.208 | generate1 _ (Tac.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (p, _) pt =
1.209 let
1.210 val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f
1.211 - (Tac.Rewrite_Set (id_rls rls')) (f',asm) Complete
1.212 + (Tac.Rewrite_Set (Celem.id_rls rls')) (f',asm) Complete
1.213 val pt = update_branch pt p TransitiveB
1.214 in
1.215 - ((p, Res), c, FormKF (term2str f'), pt)
1.216 + ((p, Res), c, FormKF (Celem.term2str f'), pt)
1.217 end
1.218 | generate1 thy (Tac.Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
1.219 let
1.220 val ctxt' = Stool.insert_assumptions asm ctxt
1.221 val (pt, _) = cappend_form pt p (is, ctxt') f
1.222 val pt = update_branch pt p TransitiveB
1.223 - val is = init_istate (Tac.Rewrite_Set (id_rls rls)) f
1.224 - val tac_ = Tac.Apply_Method' (e_metID, SOME e_term (*t ..has not been declared*), is, ctxt')
1.225 + val is = init_istate (Tac.Rewrite_Set (Celem.id_rls rls)) f
1.226 + val tac_ = Tac.Apply_Method' (Celem.e_metID, SOME Celem.e_term (*t ..has not been declared*), is, ctxt')
1.227 val pos' = ((lev_on o lev_dn) p, Frm)
1.228 in
1.229 generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*)
1.230 @@ -322,31 +322,31 @@
1.231 let
1.232 val (pt, c) = append_result pt p l (scval, asm) Complete
1.233 in
1.234 - ((p, Res), c, FormKF (term2str scval), pt)
1.235 + ((p, Res), c, FormKF (Celem.term2str scval), pt)
1.236 end
1.237 | generate1 _ (Tac.Calculate' (_, op_, f, (f', _))) l (p, _) pt =
1.238 let
1.239 val (pt,c) = cappend_atomic pt p l f (Tac.Calculate op_) (f', []) Complete
1.240 in
1.241 - ((p, Res), c, FormKF (term2str f'), pt)
1.242 + ((p, Res), c, FormKF (Celem.term2str f'), pt)
1.243 end
1.244 | generate1 _ (Tac.Check_elementwise' (consts, pred, (f', asm))) l (p, _) pt =
1.245 let
1.246 val (pt,c) = cappend_atomic pt p l consts (Tac.Check_elementwise pred) (f', asm) Complete
1.247 in
1.248 - ((p, Res), c, FormKF (term2str f'), pt)
1.249 + ((p, Res), c, FormKF (Celem.term2str f'), pt)
1.250 end
1.251 | generate1 _ (Tac.Or_to_List' (ors, list)) l (p, _) pt =
1.252 let
1.253 val (pt,c) = cappend_atomic pt p l ors Tac.Or_to_List (list, []) Complete
1.254 in
1.255 - ((p, Res), c, FormKF (term2str list), pt)
1.256 + ((p, Res), c, FormKF (Celem.term2str list), pt)
1.257 end
1.258 | generate1 _ (Tac.Substitute' (_, _, subte, t, t')) l (p, _) pt =
1.259 let
1.260 val (pt,c) =
1.261 cappend_atomic pt p l t (Tac.Substitute (Selem.subte2sube subte)) (t',[]) Complete
1.262 - in ((p, Res), c, FormKF (term2str t'), pt)
1.263 + in ((p, Res), c, FormKF (Celem.term2str t'), pt)
1.264 end
1.265 | generate1 _ (Tac.Tac_ (_, f, id, f')) l (p, _) pt =
1.266 let
1.267 @@ -358,7 +358,7 @@
1.268 let
1.269 val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl)
1.270 val pt = update_ctxt pt p ctxt
1.271 - val f = Syntax.string_of_term (thy2ctxt thy) f
1.272 + val f = Syntax.string_of_term (Celem.thy2ctxt thy) f
1.273 in
1.274 ((p, Pbl), c, FormKF f, pt)
1.275 end
1.276 @@ -388,7 +388,7 @@
1.277 | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*))=
1.278 let
1.279 val (tacis', (_, tac_, (p, is))) = split_last tacis
1.280 - val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
1.281 + val (p',c',_,pt') = generate1 (Celem.assoc_thy "Isac") tac_ is p pt
1.282 in
1.283 generate tacis' (pt', c@c', p')
1.284 end
1.285 @@ -419,7 +419,7 @@
1.286 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]
1.287 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
1.288 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
1.289 - val pt = update_tac pt p (Tac.Derive (id_rls nrls))
1.290 + val pt = update_tac pt p (Tac.Derive (Celem.id_rls nrls))
1.291 val pt = update_branch pt p TransitiveB
1.292 in (c, (pt, pos: pos')) end
1.293 | embed_deriv tacis (pt, (p, Res)) =
1.294 @@ -436,7 +436,7 @@
1.295 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];
1.296 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
1.297 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
1.298 - val pt = update_tac pt p (Tac.Derive (id_rls nrls))
1.299 + val pt = update_tac pt p (Tac.Derive (Celem.id_rls nrls))
1.300 val pt = update_branch pt p TransitiveB
1.301 in (c, (pt, pos)) end
1.302 | embed_deriv _ _ = error "embed_deriv: uncovered definition"