1.1 --- a/src/Tools/isac/Interpret/generate.sml Mon Dec 12 18:08:13 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Wed Dec 14 09:37:01 2016 +0100
1.3 @@ -1,129 +1,125 @@
1.4 (* use"ME/generate.sml";
1.5 use"generate.sml";
1.6 *)
1.7 +signature CALC_TREE =
1.8 +sig (*vvv request into signature is incremental *)
1.9 + (* for calchead.sml *)
1.10 + type taci
1.11 + val e_taci : taci
1.12 + datatype edit = EdUndef | Protect | Write
1.13 + eqtype indent
1.14 + datatype nest = Closed | Nundef | Open
1.15 + datatype pblmet = Method of metID | Problem of pblID | Upblmet
1.16 + datatype inout
1.17 + = Error_ of string | FormKF of cellID * edit * indent * nest * cterm'
1.18 + | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) | RefineKF of match list
1.19 + | RefinedKF of pblID * (itm list * (bool * term) list)
1.20 + datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
1.21 + val generate1 : theory -> tac_ -> istate * Proof.context ->
1.22 + posel list * pos_ -> ptree -> pos' * pos' list * mout * ptree
1.23 + val init_pbl : (string * (term * 'a)) list -> itm list
1.24 + val init_pbl' : (string * (term * term)) list -> itm list
1.25 + (* for appl.sml *)
1.26 + (* for script.sml *)
1.27 + (* for solve.sml *)
1.28 + val generate_hard : theory -> tac_ -> pos * pos_ -> ptree -> pos' * pos' list * mout * ptree
1.29 + val init_istate : tac -> term -> istate
1.30 + (* for inform.sml *)
1.31 + val embed_deriv : taci list -> ptree * pos' -> pos' list * (ptree * pos')
1.32 + (* for mathengine.sml *)
1.33 + val generate : (tac * tac_ * ((posel list * pos_) * (istate * Proof.context))) list ->
1.34 + ptree * pos' list * pos' -> ptree * pos' list * pos'
1.35 + (* for interface.sml *)
1.36 + val generate_inconsistent_rew :
1.37 + subs option * thm'' ->
1.38 + term -> istate * Proof.context -> pos * pos_ -> ptree -> ptree * (posel list * pos_)
1.39 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.40 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.41 +end
1.42
1.43 -(*.initialize istate for Detail_Set.*)
1.44 +(**)
1.45 +structure Ctree(**): CALC_TREE(**) =
1.46 +(**)
1.47 +struct
1.48 +(* initialize istate for Detail_Set *)
1.49 fun init_istate (Rewrite_Set rls) t =
1.50 -(* val (Rewrite_Set rls) = (get_obj g_tac pt p);
1.51 - *)
1.52 (case assoc_rls rls of
1.53 - Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))
1.54 -(* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
1.55 - *)
1.56 - | Rls {scr=EmptyScr,...} =>
1.57 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.58 - ^"use prep_rls' for storing rule-sets !")
1.59 - | Rls {scr = Prog s,...} =>
1.60 - (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
1.61 - | Seq {scr=EmptyScr,...} =>
1.62 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.63 - ^"use prep_rls' for storing rule-sets !")
1.64 - | Seq {srls=srls,scr = Prog s,...} =>
1.65 - (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
1.66 -(* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t);
1.67 - *)
1.68 + Rrls {scr = Rfuns {init_state = ii, ...}, ...} => RrlsState (ii t)
1.69 + | Rls {scr = EmptyScr, ...} =>
1.70 + error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
1.71 + "use prep_rls' for storing rule-sets !")
1.72 + | Rls {scr = Prog s, ...} => (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
1.73 + | Seq {scr=EmptyScr,...} =>
1.74 + error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
1.75 + "use prep_rls' for storing rule-sets !")
1.76 + | Seq {scr = Prog s,...} => (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
1.77 + | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
1.78 | init_istate (Rewrite_Set_Inst (subs, rls)) t =
1.79 - let val (_, v)::_ = subs2subst (assoc_thy "Isac") subs
1.80 + let
1.81 + val v = case subs2subst (assoc_thy "Isac") subs of
1.82 + (_, v) :: _ => v
1.83 + | _ => error "init_istate: uncovered case "
1.84 (*...we suppose the substitution of only _one_ bound variable*)
1.85 in case assoc_rls rls of
1.86 - Rls {scr=EmptyScr,...} =>
1.87 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.88 - ^"use prep_rls' for storing rule-sets !")
1.89 - | Rls {scr = Prog s,...} =>
1.90 - let val (form, bdv) = two_scr_arg s
1.91 - in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
1.92 - end
1.93 - | Seq {scr=EmptyScr,...} =>
1.94 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.95 - ^"use prep_rls' for storing rule-sets !")
1.96 - | Seq {scr = Prog s,...} =>
1.97 - let val (form, bdv) = two_scr_arg s
1.98 - in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
1.99 - end
1.100 - end;
1.101 + Rls {scr = EmptyScr, ...} =>
1.102 + error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
1.103 + "use prep_rls' for storing rule-sets !")
1.104 + | Rls {scr = Prog s, ...} =>
1.105 + let val (form, bdv) = two_scr_arg s
1.106 + in (ScrState ([(form, t), (bdv, v)], [], NONE, e_term, Sundef,true))
1.107 + end
1.108 + | Seq {scr = EmptyScr, ...} =>
1.109 + error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
1.110 + "use prep_rls' for storing rule-sets !")
1.111 + | Seq {scr = Prog s,...} =>
1.112 + let val (form, bdv) = two_scr_arg s
1.113 + in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
1.114 + end
1.115 + | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls"
1.116 + end
1.117 + | init_istate tac _ = error ("init_istate: uncovered definition for " ^ tac2str tac)
1.118
1.119 -
1.120 -(*.a taci holds alle information required to build a node in the calc-tree;
1.121 +(* a taci holds alle information required to build a node in the calc-tree;
1.122 a taci is assumed to be used efficiently such that the calc-tree
1.123 resulting from applying a taci need not be stored separately;
1.124 - see "type calcstate".*)
1.125 + see "type calcstate" *)
1.126 (*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
1.127 TODO.WN0512 ? redesign this _list_:
1.128 # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
1.129 # the latter problem may be resolved automatically if "fun autocalc" is
1.130 not any more used for the specify-phase and for changing the phases*)
1.131 type taci =
1.132 - (tac * (*for comparison with input tac*)
1.133 - tac_ * (*for ptree generation*)
1.134 - (pos' * (*after applying tac_, for ptree generation*)
1.135 - (istate * Proof.context))); (*after applying tac_, for ptree generation*)
1.136 -val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci;
1.137 -(* val (tac, tac_, (pos', istate))::_ = tacis';
1.138 - *)
1.139 + (tac * (* for comparison with input tac *)
1.140 + tac_ * (* for ptree generation *)
1.141 + (pos' * (* after applying tac_, for ptree generation *)
1.142 + (istate * Proof.context))) (* after applying tac_, for ptree generation *)
1.143 +val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci
1.144 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
1.145 - "( "^tac2str tac^", "^tac_2str tac_^", ( "^pos'2str pos'
1.146 - ^", "^istate2str istate^" ))";
1.147 -fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis;
1.148 + "( " ^ tac2str tac ^ ", " ^ tac_2str tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
1.149 + istate2str istate ^ " ))"
1.150 +fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis
1.151
1.152 -datatype pblmet = (*%^%*)
1.153 - Upblmet (*undefined*)
1.154 - | Problem of pblID (*%^%*)
1.155 - | Method of metID; (*%^%*)
1.156 -fun pblmet2str (Problem pblID) = "Problem "^(strs2str pblID)(*%^%*)
1.157 - | pblmet2str (Method metID) = "Method "^(metID2str metID);(*%^%*)
1.158 - (*%^%*) (*26.6. moved to sequent.sml: fun ~~~~~~~~~; was here below*)
1.159 -
1.160 -
1.161 -(* copy from 03.60.usecases.sml 15.11.99 *)
1.162 -datatype user_cmd =
1.163 - Accept | NotAccept | Example
1.164 -| YourTurn | MyTurn (* internal use only 7.6.02 java-sml*)
1.165 -| Rules
1.166 -| DontKnow (*| HowComes | WhatFor 7.6.02 java-sml*)
1.167 -| Undo (*| Back | Forward 7.6.02 java-sml*)
1.168 -| EndProof | EndSession
1.169 -| ActivePlus | ActiveMinus | SpeedPlus | SpeedMinus
1.170 - (*Stepwidth...7.6.02 java-sml*)
1.171 -| Auto | NotAuto | Details;
1.172 -(* for test-print-outs *)
1.173 -fun user_cmd2str Accept ="Accept"
1.174 - | user_cmd2str NotAccept ="NotAccept"
1.175 - | user_cmd2str Example ="Example"
1.176 - | user_cmd2str MyTurn ="MyTurn"
1.177 - | user_cmd2str YourTurn ="YourTurn"
1.178 - | user_cmd2str Rules ="Rules"
1.179 -(*| user_cmd2str HowComes ="HowComes"*)
1.180 - | user_cmd2str DontKnow ="DontKnow"
1.181 -(*| user_cmd2str WhatFor ="WhatFor"
1.182 - | user_cmd2str Back ="Back"*)
1.183 - | user_cmd2str Undo ="Undo"
1.184 -(*| user_cmd2str Forward ="Forward"*)
1.185 - | user_cmd2str EndProof ="EndProof"
1.186 - | user_cmd2str EndSession ="EndSession"
1.187 - | user_cmd2str ActivePlus = "ActivePlus"
1.188 - | user_cmd2str ActiveMinus = "ActiveMinus"
1.189 - | user_cmd2str SpeedPlus = "SpeedPlus"
1.190 - | user_cmd2str SpeedMinus = "SpeedMinus"
1.191 - | user_cmd2str Auto = "Auto"
1.192 - | user_cmd2str NotAuto = "NotAuto"
1.193 - | user_cmd2str Details = "Details";
1.194 -
1.195 -
1.196 +datatype pblmet = (*%^%*)
1.197 + Upblmet (*undefined*)
1.198 +| Problem of pblID (*%^%*)
1.199 +| Method of metID; (*%^%*)
1.200 +fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)
1.201 + | pblmet2str (Method metID) = "Method " ^ metID2str metID (*%^%*)
1.202 + | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x)
1.203
1.204 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
1.205 datatype foppFK = (* in DG cases div 2 *)
1.206 EmptyFoppFK (*DG internal*)
1.207 | FormFK of cterm'
1.208 -| PpcFK of cterm' ppc;
1.209 -fun foppFK2str (FormFK ct') ="FormFK "^ct'
1.210 - | foppFK2str (PpcFK ppc) ="PpcFK "^(ppc2str ppc)
1.211 - | foppFK2str EmptyFoppFK ="EmptyFoppFK";
1.212 -
1.213 +| PpcFK of cterm' ppc
1.214 +fun foppFK2str (FormFK ct') ="FormFK " ^ ct'
1.215 + | foppFK2str (PpcFK ppc) ="PpcFK " ^ ppc2str ppc
1.216 + | foppFK2str EmptyFoppFK ="EmptyFoppFK"
1.217
1.218 datatype nest = Open | Closed | Nundef;
1.219 fun nest2str Open = "Open"
1.220 | nest2str Closed = "Closed"
1.221 - | nest2str Nundef = "Nundef";
1.222 + | nest2str Nundef = "Nundef"
1.223
1.224 type indent = int;
1.225 datatype edit = EdUndef | Write | Protect;
1.226 @@ -134,32 +130,15 @@
1.227 | edit2str Write = "Write"
1.228 | edit2str Protect = "Protect";
1.229
1.230 -
1.231 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
1.232 - New_User | End_User (*<->*)
1.233 -| New_Proof | End_Proof (*<->*)
1.234 -| Command of user_cmd (*-->*)
1.235 -| Request of string | Message of string (*<--*)
1.236 -| Error_ of string | System of string (*<--*)
1.237 -| FoPpcFK of foppFK (*-->*)
1.238 + Error_ of string (*<--*)
1.239 | FormKF of cellID * edit * indent * nest * cterm' (*<--*)
1.240 | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) (*<--*)
1.241 -| RuleFK of tac (*-->*)
1.242 -| RuleKF of edit * tac (*<--*)
1.243 -| RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*)
1.244 -| Select of tac list (*<--*)
1.245 | RefineKF of match list (*<--*)
1.246 -| Speed of int (*<--*)
1.247 -| Active of int (*<--*)
1.248 -| Domain of domID; (*<--*)
1.249 +| RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*)
1.250
1.251 fun inout2str End_Proof = "End_Proof"
1.252 - | inout2str (Command user_cmd) = "Command "^(user_cmd2str user_cmd)
1.253 - | inout2str (Request s) = "Request "^s
1.254 - | inout2str (Message s) = "Message "^s
1.255 | inout2str (Error_ s) = "Error_ "^s
1.256 - | inout2str (System s) = "System "^s
1.257 - | inout2str (FoPpcFK foppFK) = "FoPpcFK "^(foppFK2str foppFK)
1.258 | inout2str (FormKF (cellID, edit, indent, nest, ct')) =
1.259 "FormKF ("^(string_of_int cellID)^","
1.260 ^(edit2str edit)^","^(string_of_int indent)^","
1.261 @@ -170,16 +149,9 @@
1.262 ^(edit2str edit)^","^(string_of_int indent)^","
1.263 ^(nest2str nest)^",("
1.264 ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))"
1.265 - | inout2str (RuleKF (edit,tac)) = "RuleKF "^
1.266 - pair2str(edit2str edit,tac2str tac)
1.267 - | inout2str (RuleFK tac) = "RuleFK "^(tac2str tac)
1.268 - | inout2str (Select tacs)=
1.269 - "Select "^((strs2str' o (map tac2str)) tacs)
1.270 | inout2str (RefineKF ms) = "RefineKF "^(matchs2str ms)
1.271 - | inout2str (Speed i) = "Speed "^(string_of_int i)
1.272 - | inout2str (Active i) = "Active "^(string_of_int i)
1.273 - | inout2str (Domain dI) = "Domain "^dI;
1.274 -fun inouts2str ios = (strs2str' o (map inout2str)) ios;
1.275 + | inout2str _ = error "inout2str: uncovered definition"
1.276 +fun inouts2str ios = (strs2str' o (map inout2str)) ios
1.277
1.278 datatype mout =
1.279 Form' of inout (* packing cterm' | cterm' ppc *)
1.280 @@ -189,341 +161,291 @@
1.281
1.282 fun mout2str (Form' inout) ="Form' "^(inout2str inout)
1.283 | mout2str (Error' inout) ="Error' "^(inout2str inout)
1.284 - | mout2str (EmptyMout ) ="EmptyMout";
1.285 -
1.286 -(*fun Form'2str (Form' )*)
1.287 -
1.288 -
1.289 -
1.290 -
1.291 + | mout2str (EmptyMout ) ="EmptyMout"
1.292 + | mout2str _ = error "mout2str: uncovered definition"
1.293
1.294 (* init pbl with ...,dsc,empty | [] *)
1.295 fun init_pbl pbt =
1.296 - let
1.297 - fun pbt2itm (f, (d, t)) =
1.298 - ((0, [], false, f, Inc ((d, []), (e_term, []))) : itm);
1.299 - in map pbt2itm pbt end;
1.300 -(*take formal parameters from pbt, for transfer from pbl/met-hierarchy*)
1.301 + let
1.302 + fun pbt2itm (f, (d, _)) = ((0, [], false, f, Inc ((d, []), (e_term, []))) : itm)
1.303 + in map pbt2itm pbt end
1.304 +
1.305 +(* take formal parameters from pbt, for transfer from pbl/met-hierarchy *)
1.306 fun init_pbl' pbt =
1.307 let
1.308 - fun pbt2itm (f,(d,t)) =
1.309 - ((0,[],false,f,Inc((d,[t]),(e_term,[]))):itm);
1.310 - in map pbt2itm pbt end;
1.311 -
1.312 + fun pbt2itm (f, (d, t)) = ((0, [], false, f, Inc((d, [t]), (e_term, []))) : itm)
1.313 + in map pbt2itm pbt end
1.314
1.315 (*generate 1 ppobj in ptree*)
1.316 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
1.317 -fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p,p_)) pt =
1.318 - (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet, itms2itemppc thy [][]))),
1.319 - case p_ of
1.320 - Pbl => update_pbl pt p itmlist
1.321 - | Met => update_met pt p itmlist)
1.322 - (*WN110515 probably declare_constraints with input item (without dsc) --
1.323 - -- important when specifying without formalisation*)
1.324 - | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p,p_)) pt =
1.325 - (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.326 - case p_ of
1.327 - Pbl => update_pbl pt p itmlist
1.328 - | Met => update_met pt p itmlist)
1.329 +fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt =
1.330 + (pos:pos',[],Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [][]))),
1.331 + case p_ of
1.332 + Pbl => update_pbl pt p itmlist
1.333 + | Met => update_met pt p itmlist
1.334 + | _ => error ("uncovered case " ^ pos_2str p_))
1.335 + (* WN110515 probably declare_constraints with input item (without dsc) --
1.336 + -- important when specifying without formalisation *)
1.337 + | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p, p_)) pt =
1.338 + (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
1.339 + case p_ of
1.340 + Pbl => update_pbl pt p itmlist
1.341 + | Met => update_met pt p itmlist
1.342 + | _ => error ("uncovered case " ^ pos_2str p_))
1.343 (*WN110515 probably declare_constraints with input item (without dsc)*)
1.344 - | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p,p_)) pt =
1.345 - (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.346 - case p_ of
1.347 - Pbl => update_pbl pt p itmlist
1.348 - | Met => update_met pt p itmlist)
1.349 -
1.350 + | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p, p_)) pt =
1.351 + (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
1.352 + case p_ of
1.353 + Pbl => update_pbl pt p itmlist
1.354 + | Met => update_met pt p itmlist
1.355 + | _ => error ("uncovered case " ^ pos_2str p_))
1.356 | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt =
1.357 - (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.358 - update_domID pt p domID)
1.359 -
1.360 - | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) _
1.361 - (pos as (p,_)) pt =
1.362 - let val pt = update_pbl pt p itms
1.363 - val pt = update_pblID pt p pI
1.364 - in ((p,Pbl),[],
1.365 - Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.366 - pt) end
1.367 -
1.368 - | generate1 thy (Specify_Method' (mID, oris, itms)) _
1.369 - (pos as (p,_)) pt =
1.370 - let val pt = update_oris pt p oris
1.371 - val pt = update_met pt p itms
1.372 - val pt = update_metID pt p mID
1.373 - in ((p,Met),[],
1.374 - Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.375 - pt) end
1.376 -
1.377 + (pos, [] ,Form' (PpcKF (0 ,EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
1.378 + update_domID pt p domID)
1.379 + | generate1 thy (Specify_Problem' (pI, (_, (itms, _)))) _ (p, _) pt =
1.380 + let
1.381 + val pt = update_pbl pt p itms
1.382 + val pt = update_pblID pt p pI
1.383 + in
1.384 + ((p, Pbl), [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
1.385 + end
1.386 + | generate1 thy (Specify_Method' (mID, oris, itms)) _ (p, _) pt =
1.387 + let
1.388 + val pt = update_oris pt p oris
1.389 + val pt = update_met pt p itms
1.390 + val pt = update_metID pt p mID
1.391 + in
1.392 + ((p, Met), [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
1.393 + end
1.394 | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
1.395 - let
1.396 - val pt = update_pbl pt p itms
1.397 - val pt = update_met pt p met
1.398 - in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
1.399 - end
1.400 -
1.401 - | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl))
1.402 - _ (pos as (p,_)) pt =
1.403 - let val pt = update_pbl pt p pbl
1.404 - val pt = update_orispec pt p (domID,pIre,metID)
1.405 - in (pos,[],
1.406 - Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.407 - pt) end
1.408 -
1.409 - | generate1 thy (Refine_Problem' (pI,_)) _ (pos as (p,_)) pt =
1.410 - let val (dI,_,mI) = get_obj g_spec pt p
1.411 - val pt = update_spec pt p (dI, pI, mI)
1.412 - in (pos,[],
1.413 - Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),pt)
1.414 + let
1.415 + val pt = update_pbl pt p itms
1.416 + val pt = update_met pt p met
1.417 + in
1.418 + (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
1.419 end
1.420 -
1.421 - | generate1 thy (Apply_Method' (_,topt, is, ctxt)) _ (pos as (p,p_)) pt =
1.422 - ((*tracing("###generate1 Apply_Method': pos = "^pos'2str (p,p_));
1.423 - tracing("###generate1 Apply_Method': topt= "^termopt2str topt);
1.424 - tracing("###generate1 Apply_Method': is = "^istate2str is);*)
1.425 - case topt of
1.426 - SOME t =>
1.427 - let val (pt,c) = cappend_form pt p (is, ctxt) t
1.428 - (*val _= tracing("###generate1 Apply_Method: after cappend")*)
1.429 - in (pos,c, EmptyMout,pt)
1.430 - end
1.431 - | NONE =>
1.432 - (pos,[],EmptyMout,update_env pt p (SOME (is, ctxt))))
1.433 -(* val (thy, (Take' t), l, (p,p_), pt) =
1.434 - ((assoc_thy "Isac"), tac_, is, pos, pt);
1.435 - *)
1.436 - | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *)
1.437 - let (*val _=tracing("### generate1: Take' pos="^pos'2str (p,p_));*)
1.438 - val p = let val (ps,p') = split_last p(*no connex to prev.ppobj*)
1.439 - in if p'=0 then ps@[1] else p end;
1.440 - val (pt,c) = cappend_form pt p l t;
1.441 - in ((p,Frm):pos', c,
1.442 - Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
1.443 -
1.444 -(* val (l, (p,p_)) = (RrlsState is, p);
1.445 -
1.446 - val (thy, Begin_Trans' t, l, (p,Frm), pt) =
1.447 - (assoc_thy "Isac", tac_, is, p, pt);
1.448 - *)
1.449 - | generate1 thy (Begin_Trans' t) l (p,Frm) pt =
1.450 - let (* print_depth 99;
1.451 - map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
1.452 - *)
1.453 - val (pt,c) = cappend_form pt p l t
1.454 - (* print_depth 99;
1.455 - map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
1.456 - *)
1.457 + | generate1 thy (Refine_Tacitly' (_, pIre, domID, metID, pbl)) _ (pos as (p, _)) pt =
1.458 + let
1.459 + val pt = update_pbl pt p pbl
1.460 + val pt = update_orispec pt p (domID, pIre, metID)
1.461 + in
1.462 + (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
1.463 + end
1.464 + | generate1 thy (Refine_Problem' (pI, _)) _ (pos as (p, _)) pt =
1.465 + let
1.466 + val (dI, _, mI) = get_obj g_spec pt p
1.467 + val pt = update_spec pt p (dI, pI, mI)
1.468 + in
1.469 + (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
1.470 + end
1.471 + | generate1 _ (Apply_Method' (_, topt, is, ctxt)) _ (pos as (p, _)) pt =
1.472 + (case topt of
1.473 + SOME t =>
1.474 + let val (pt, c) = cappend_form pt p (is, ctxt) t
1.475 + in (pos, c, EmptyMout, pt) end
1.476 + | NONE => (pos, [], EmptyMout, update_env pt p (SOME (is, ctxt))))
1.477 + | generate1 _ (Take' t) l (p, _) pt = (* val (Take' t) = m; *)
1.478 + let
1.479 + val p =
1.480 + let val (ps, p') = split_last p (* no connex to prev.ppobj *)
1.481 + in if p' = 0 then ps @ [1] else p end
1.482 + val (pt, c) = cappend_form pt p l t
1.483 + in
1.484 + ((p, Frm): pos', c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
1.485 + end
1.486 + | generate1 _ (Begin_Trans' t) l (p, Frm) pt =
1.487 + let
1.488 + val (pt, c) = cappend_form pt p l t
1.489 val pt = update_branch pt p TransitiveB (*040312*)
1.490 - (*replace the old PrfOjb ~~~~~*)
1.491 - val p = (lev_on o lev_dn(*starts with [...,0]*)) p;
1.492 - val (pt,c') = cappend_form pt p l t(*FIXME.0402 same istate ???*);
1.493 - in ((p,Frm), c @ c', Form' (FormKF (~1,EdUndef,(length p), Nundef,
1.494 - term2str t)), pt) end
1.495 -
1.496 - (* val (thy, Begin_Trans' t, l, (p,Res), pt) =
1.497 - (assoc_thy "Isac", tac_, is, p, pt);
1.498 - *)
1.499 - | generate1 thy (Begin_Trans' t) l (p ,Res) pt =
1.500 - (*append after existing PrfObj _________*)
1.501 - generate1 thy (Begin_Trans' t) l (lev_on p,Frm) pt
1.502 -
1.503 - | generate1 thy (End_Trans' tasm) l (p,p_) pt =
1.504 + (* replace the old PrfOjb ~~~~~ *)
1.505 + val p = (lev_on o lev_dn (* starts with [...,0] *)) p
1.506 + val (pt, c') = cappend_form pt p l t (*FIXME.0402 same istate ???*)
1.507 + in
1.508 + ((p, Frm), c @ c', Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
1.509 + end
1.510 + | generate1 thy (Begin_Trans' t) l (p, Res) pt =
1.511 + (*append after existing PrfObj vvvvvvvvvvvvv*)
1.512 + generate1 thy (Begin_Trans' t) l (lev_on p, Frm) pt
1.513 + | generate1 _ (End_Trans' tasm) l (p, _) pt =
1.514 + let
1.515 + val p' = lev_up p
1.516 + val (pt, c) = append_result pt p' l tasm Complete
1.517 + in
1.518 + ((p', Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
1.519 + end
1.520 + | generate1 _ (Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (p, _) pt =
1.521 + let
1.522 + val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.523 + (Rewrite_Inst (subst2subs subs', thm')) (f',asm) Complete;
1.524 + val pt = update_branch pt p TransitiveB
1.525 + in ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt) end
1.526 + | generate1 _ (Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt =
1.527 + let
1.528 + val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.529 + (Rewrite thm') (f', asm) Complete
1.530 + val pt = update_branch pt p TransitiveB
1.531 + in
1.532 + ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
1.533 + end
1.534 + | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt
1.535 + | generate1 _ (Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (p, _) pt =
1.536 + let
1.537 + val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.538 + (Rewrite_Set_Inst (subst2subs subs', id_rls rls')) (f', asm) Complete
1.539 + val pt = update_branch pt p TransitiveB
1.540 + in
1.541 + ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
1.542 + end
1.543 + | generate1 thy (Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
1.544 + let
1.545 + val ctxt' = insert_assumptions asm ctxt
1.546 + val (pt, _) = cappend_form pt p (is, ctxt') f
1.547 + val pt = update_branch pt p TransitiveB
1.548 + val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
1.549 + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
1.550 + val pos' = ((lev_on o lev_dn) p, Frm)
1.551 + in
1.552 + generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*)
1.553 + end
1.554 + | generate1 _ (Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (p, _) pt =
1.555 + let
1.556 + val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.557 + (Rewrite_Set (id_rls rls')) (f',asm) Complete
1.558 + val pt = update_branch pt p TransitiveB
1.559 + in
1.560 + ((p, Res), c, Form' (FormKF (~1 ,EdUndef, length p, Nundef, term2str f')), pt)
1.561 + end
1.562 + | generate1 thy (Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
1.563 + let
1.564 + val ctxt' = insert_assumptions asm ctxt
1.565 + val (pt, _) = cappend_form pt p (is, ctxt') f
1.566 + val pt = update_branch pt p TransitiveB
1.567 + val is = init_istate (Rewrite_Set (id_rls rls)) f
1.568 + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
1.569 + val pos' = ((lev_on o lev_dn) p, Frm)
1.570 + in
1.571 + generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*)
1.572 + end
1.573 + | generate1 _ (Check_Postcond' (_, (scval, asm))) l (p, _) pt =
1.574 let
1.575 - val p' = lev_up p
1.576 - val (pt,c) = append_result pt p' l tasm Complete;
1.577 - in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
1.578 -
1.579 - | generate1 thy (Rewrite_Inst' (_,_,_,_,subs', thm', f, (f', asm))) (is, ctxt) (p,p_) pt =
1.580 + val (pt, c) = append_result pt p l (scval, asm) Complete
1.581 + in
1.582 + ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str scval)), pt)
1.583 + end
1.584 + | generate1 _ (Calculate' (_, op_, f, (f', _))) l (p, _) pt =
1.585 let
1.586 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.587 - (Rewrite_Inst (subst2subs subs', thm')) (f',asm) Complete;
1.588 - val pt = update_branch pt p TransitiveB
1.589 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.590 -
1.591 - | generate1 thy (Rewrite' (thy', ord', rls', pa, thm', f, (f', asm))) (is, ctxt) (p, p_) pt =
1.592 + val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f', []) Complete
1.593 + in
1.594 + ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
1.595 + end
1.596 + | generate1 _ (Check_elementwise' (consts, pred, (f', asm))) l (p, _) pt =
1.597 let
1.598 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.599 - (Rewrite thm') (f',asm) Complete
1.600 - val pt = update_branch pt p TransitiveB
1.601 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.602 -
1.603 - | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt
1.604 -
1.605 - | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) (is, ctxt) (p,p_) pt =
1.606 + val (pt,c) = cappend_atomic pt p l consts (Check_elementwise pred) (f',asm) Complete
1.607 + in
1.608 + ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
1.609 + end
1.610 + | generate1 _ (Or_to_List' (ors, list)) l (p, _) pt =
1.611 let
1.612 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.613 - (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
1.614 - val pt = update_branch pt p TransitiveB
1.615 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.616 -
1.617 - | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =
1.618 - let
1.619 - val ctxt' = insert_assumptions asm ctxt
1.620 - val (pt,c) = cappend_form pt p (is, ctxt') f
1.621 - val pt = update_branch pt p TransitiveB
1.622 -
1.623 - val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
1.624 - val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
1.625 - val pos' = ((lev_on o lev_dn) p, Frm)
1.626 - in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
1.627 -
1.628 - | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) (is, ctxt) (p,p_) pt =
1.629 - let
1.630 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.631 - (Rewrite_Set (id_rls rls')) (f',asm) Complete
1.632 - val pt = update_branch pt p TransitiveB
1.633 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.634 -
1.635 - | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =
1.636 - let
1.637 - val ctxt' = insert_assumptions asm ctxt
1.638 - val (pt,c) = cappend_form pt p (is, ctxt') f
1.639 - val pt = update_branch pt p TransitiveB
1.640 -
1.641 - val is = init_istate (Rewrite_Set (id_rls rls)) f
1.642 - val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
1.643 - val pos' = ((lev_on o lev_dn) p, Frm)
1.644 - in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
1.645 -
1.646 - | generate1 thy (Check_Postcond' (pI, (scval, asm))) l (p,p_) pt =
1.647 - let val (pt,c) = append_result pt p l (scval, asm) Complete
1.648 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str scval)), pt) end
1.649 -
1.650 - | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt =
1.651 - let val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f',[]) Complete;
1.652 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.653 -
1.654 - | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt =
1.655 - let
1.656 - val (pt,c) = cappend_atomic pt p l consts (Check_elementwise pred) (f',asm) Complete;
1.657 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.658 -
1.659 - | generate1 thy (Or_to_List' (ors,list)) l (p,p_) pt =
1.660 - let val (pt,c) = cappend_atomic pt p l ors Or_to_List (list,[]) Complete;
1.661 - in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)), pt) end
1.662 -
1.663 - | generate1 thy (Substitute' (_, _, subte, t, t')) l (p,p_) pt =
1.664 - let
1.665 - val (pt,c) =
1.666 - cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete;
1.667 - in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str t')), pt)
1.668 - end
1.669 -
1.670 - | generate1 thy (Tac_ (_,f,id,f')) l (p,p_) pt =
1.671 + val (pt,c) = cappend_atomic pt p l ors Or_to_List (list, []) Complete
1.672 + in
1.673 + ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str list)), pt)
1.674 + end
1.675 + | generate1 _ (Substitute' (_, _, subte, t, t')) l (p, _) pt =
1.676 let
1.677 val (pt,c) =
1.678 - cappend_atomic pt p l (str2term f) (Tac id) (str2term f',[]) Complete;
1.679 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end
1.680 -
1.681 - | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p,p_) pt =
1.682 + cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete
1.683 + in ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t')), pt)
1.684 + end
1.685 + | generate1 _ (Tac_ (_, f, id, f')) l (p, _) pt =
1.686 let
1.687 - val (pt,c) =
1.688 - cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);
1.689 - val pt = update_ctxt pt p ctxt
1.690 - val f = Syntax.string_of_term (thy2ctxt thy) f;
1.691 - in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
1.692 -
1.693 - | generate1 thy m' _ _ _ =
1.694 - error ("generate1: not impl.for "^(tac_2str m'));
1.695 + val (pt, c) = cappend_atomic pt p l (str2term f) (Tac id) (str2term f', []) Complete
1.696 + in
1.697 + ((p,Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, f')), pt)
1.698 + end
1.699 + | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p, _) pt =
1.700 + let
1.701 + val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl)
1.702 + val pt = update_ctxt pt p ctxt
1.703 + val f = Syntax.string_of_term (thy2ctxt thy) f
1.704 + in
1.705 + ((p, Pbl), c, Form' (FormKF (~1, EdUndef, length p, Nundef, f)), pt)
1.706 + end
1.707 + | generate1 _ m' _ _ _ = error ("generate1: not impl.for " ^ tac_2str m')
1.708
1.709 fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
1.710 let
1.711 - val f = get_curr_formula (pt, pos);
1.712 - val pos' as (p', _) = (lev_on p, Res);
1.713 - val (pt,c) =
1.714 - case subs_opt of
1.715 - NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
1.716 - (Rewrite thm') (f', []) Inconsistent
1.717 - | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
1.718 - (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
1.719 - val pt = update_branch pt p' TransitiveB;
1.720 + val f = get_curr_formula (pt, pos)
1.721 + val pos' as (p', _) = (lev_on p, Res)
1.722 + val (pt, _) = case subs_opt of
1.723 + NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
1.724 + (Rewrite thm') (f', []) Inconsistent
1.725 + | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
1.726 + (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
1.727 + val pt = update_branch pt p' TransitiveB
1.728 in (pt, pos') end
1.729
1.730 fun generate_hard thy m' (p,p_) pt =
1.731 let
1.732 - val p =
1.733 - case p_ of
1.734 - Frm => p | Res => lev_on p
1.735 - | _ => error ("generate_hard: call by " ^ pos'2str (p,p_));
1.736 - in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end;
1.737 + val p = case p_ of
1.738 + Frm => p | Res => lev_on p
1.739 + | _ => error ("generate_hard: call by " ^ pos'2str (p,p_))
1.740 + in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end
1.741
1.742 -(*tacis are in reverse order from nxt_solve_/specify_: last = fst to insert*)
1.743 +(* tacis are in reverse order from nxt_solve_/specify_: last = fst to insert *)
1.744 fun generate ([]: taci list) ptp = ptp
1.745 - | generate tacis (pt, c, _:pos'(*!dropped!WN0504redesign generate/tacis?*))=
1.746 - let
1.747 - val (tacis', (_, tac_, (p, is))) = split_last tacis
1.748 - val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
1.749 - in generate tacis' (pt', c@c', p') end;
1.750 + | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*))=
1.751 + let
1.752 + val (tacis', (_, tac_, (p, is))) = split_last tacis
1.753 + val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
1.754 + in
1.755 + generate tacis' (pt', c@c', p')
1.756 + end
1.757
1.758 -(*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
1.759 - * of for connecting a user-input formula with the current calc-state. *
1.760 - *# It is somewhat incompatible with the rest of the math-engine: *
1.761 - * (1) it is not created by a script *
1.762 - * (2) thus there cannot be another user-input within a derivation *
1.763 - *# It suffers particularily from the not-well-foundedness of the math-engine*
1.764 - * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
1.765 - * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
1.766 - * (3) FIXME and eventually 'lev_back' *
1.767 - *# SOME improvements are evident FIXME.040215 '_deriv'ation: *
1.768 - * (1) FIXME nest Rls_ in 'make_deriv' *
1.769 - * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
1.770 - * user-input will become possible in this part of a derivation *
1.771 - * (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
1.772 - * while a non-derivable inform requires to step until End_Proof' *
1.773 - * (4) FIXME find criteria on when _not_ to step until End_Proof' *
1.774 - * (5) FIXME
1.775 -.*)
1.776 -(*.update pos in tacis for embedding by generate.*)
1.777 -(* val
1.778 - *)
1.779 -fun insert_pos _ [] = []
1.780 - | insert_pos (p:pos) (((tac,tac_,(_, ist))::tacis):taci list) =
1.781 - ((tac,tac_,((p, Res), ist)):taci)
1.782 - ::((insert_pos (lev_on p) tacis):taci list);
1.783 +(* update pos in tacis for embedding by generate *)
1.784 +fun insert_pos (_: pos) [] = []
1.785 + | insert_pos (p: pos) (((tac, tac_, (_, ist)): taci) :: tacis) =
1.786 + ((tac, tac_, ((p, Res), ist)): taci) :: (insert_pos (lev_on p) tacis)
1.787
1.788 -fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm)
1.789 - | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm)
1.790 - | res_from_taci (_, tac_, _) =
1.791 - error ("res_from_taci: called with" ^ tac_2str tac_);
1.792 +fun res_from_taci (_, Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
1.793 + | res_from_taci (_, Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
1.794 + | res_from_taci (_, tac_, _) = error ("res_from_taci: called with" ^ tac_2str tac_)
1.795
1.796 -(*.embed the tacis created by a '_deriv'ation; sys.form <> input.form
1.797 - tacis are in order, thus are reverted for generate.*)
1.798 -(* val (tacis, (pt, pos as (p, Frm))) = (tacis', ptp);
1.799 - *)
1.800 -fun embed_deriv (tacis:taci list) (pt, pos as (p, Frm):pos') =
1.801 +(* embed the tacis created by a '_deriv'ation; sys.form <> input.form
1.802 + tacis are in order, thus are reverted for generate *)
1.803 +fun embed_deriv (tacis: taci list) (pt, pos as (p, Frm): pos') =
1.804 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
1.805 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
1.806 + let
1.807 + val (res, asm) = (res_from_taci o last_elem) tacis
1.808 + val (ist, ctxt) = case get_obj g_loc pt p of
1.809 + (SOME (ist, ctxt), _) => (ist, ctxt)
1.810 + | (NONE, _) => error "embed_deriv Frm: uncovered case get_obj"
1.811 + val form = get_obj g_form pt p
1.812 + (*val p = lev_on p; ---------------only difference to (..,Res) below*)
1.813 + val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt))) ::
1.814 + (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm),
1.815 + (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]
1.816 + val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.817 + val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
1.818 + val pt = update_tac pt p (Derive (id_rls nrls))
1.819 + val pt = update_branch pt p TransitiveB
1.820 + in (c, (pt, pos: pos')) end
1.821 + | embed_deriv tacis (pt, (p, Res)) =
1.822 + (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
1.823 + and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
1.824 let val (res, asm) = (res_from_taci o last_elem) tacis
1.825 - val (SOME (ist, ctxt),_) = get_obj g_loc pt p
1.826 - val form = get_obj g_form pt p
1.827 - (*val p = lev_on p; ---------------only difference to (..,Res) below*)
1.828 - val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt)))
1.829 - ::(insert_pos ((lev_on o lev_dn) p) tacis)
1.830 - @ [(End_Trans, End_Trans' (res, asm),
1.831 - (pos_plus (length tacis) (lev_dn p, Res),
1.832 - (new_val res ist, ctxt)))]
1.833 - val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.834 - val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
1.835 - val pt = update_tac pt p (Derive (id_rls nrls))
1.836 - (*FIXME.040216 struct.ctree*)
1.837 - val pt = update_branch pt p TransitiveB
1.838 - in (c, (pt, pos:pos')) end
1.839 -
1.840 -(* val (tacis, (pt, (p, Res))) = (tacis', ptp);
1.841 - *)
1.842 - | embed_deriv tacis (pt, (p, Res)) =
1.843 - (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
1.844 - and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
1.845 - let val (res, asm) = (res_from_taci o last_elem) tacis
1.846 - val (_, SOME (ist, ctxt)) = get_obj g_loc pt p
1.847 - val (f,a) = get_obj g_result pt p
1.848 - val p = lev_on p(*---------------only difference to (..,Frm) above*);
1.849 - val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt)))
1.850 - ::(insert_pos ((lev_on o lev_dn) p) tacis)
1.851 - @ [(End_Trans, End_Trans' (res, asm),
1.852 - (pos_plus (length tacis) (lev_dn p, Res),
1.853 - (new_val res ist, ctxt)))];
1.854 - val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.855 - val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
1.856 - val pt = update_tac pt p (Derive (id_rls nrls))
1.857 - (*FIXME.040216 struct.ctree*)
1.858 - val pt = update_branch pt p TransitiveB
1.859 - in (c, (pt, pos)) end;
1.860 + val (ist, ctxt) = case get_obj g_loc pt p of
1.861 + (_, SOME (ist, ctxt)) => (ist, ctxt)
1.862 + | (_, NONE) => error "embed_deriv Frm: uncovered case get_obj"
1.863 + val (f, _) = get_obj g_result pt p
1.864 + val p = lev_on p(*---------------only difference to (..,Frm) above*);
1.865 + val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt))) ::
1.866 + (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm),
1.867 + (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];
1.868 + val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.869 + val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
1.870 + val pt = update_tac pt p (Derive (id_rls nrls))
1.871 + val pt = update_branch pt p TransitiveB
1.872 + in (c, (pt, pos)) end
1.873 + | embed_deriv _ _ = error "embed_deriv: uncovered definition"
1.874 +end
1.875 \ No newline at end of file