1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,586 @@
1.4 +(* use"ME/generate.sml";
1.5 + use"generate.sml";
1.6 + *)
1.7 +
1.8 +(*.initialize istate for Detail_Set.*)
1.9 +(*
1.10 +fun init_istate (Rewrite_Set rls) =
1.11 +(* val (Rewrite_Set rls) = (get_obj g_tac pt p);
1.12 + *)
1.13 + (case assoc_rls rls of
1.14 + Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))
1.15 +(* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
1.16 + *)
1.17 + | Rls {scr=EmptyScr,...} =>
1.18 + raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.19 + ^"use prep_rls for storing rule-sets !")
1.20 + | Rls {scr=Script s,...} =>
1.21 +(* val Rls {scr=Script s,...} = assoc_rls rls;
1.22 + *)
1.23 + (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
1.24 + | Seq {scr=EmptyScr,...} =>
1.25 + raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.26 + ^"use prep_rls for storing rule-sets !")
1.27 + | Seq {srls=srls,scr=Script s,...} =>
1.28 + (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
1.29 + | init_istate (Rewrite_Set_Inst (subs, rls)) =
1.30 +(* val (Rewrite_Set_Inst (subs, rls)) = (get_obj g_tac pt p);
1.31 + *)
1.32 + let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs
1.33 + in case assoc_rls rls of
1.34 + Rls {scr=EmptyScr,...} =>
1.35 + raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.36 + ^"use prep_rls for storing rule-sets !")
1.37 + | Rls {scr=Script s,...} =>
1.38 + let val (a1, a2) = two_scr_arg s
1.39 + in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end
1.40 + | Seq {scr=EmptyScr,...} =>
1.41 + raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.42 + ^"use prep_rls for storing rule-sets !")
1.43 +(* val Seq {scr=Script s,...} = assoc_rls rls;
1.44 + *)
1.45 + | Seq {scr=Script s,...} =>
1.46 + let val (a1, a2) = two_scr_arg s
1.47 + in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end
1.48 + end;
1.49 +*)
1.50 +(*~~~~~~~~~~~~~~~~~~~~~~copy for dev. until del.~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.51 +fun init_istate (Rewrite_Set rls) t =
1.52 +(* val (Rewrite_Set rls) = (get_obj g_tac pt p);
1.53 + *)
1.54 + (case assoc_rls rls of
1.55 + Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))
1.56 +(* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
1.57 + *)
1.58 + | Rls {scr=EmptyScr,...} =>
1.59 + raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.60 + ^"use prep_rls for storing rule-sets !")
1.61 + | Rls {scr=Script s,...} =>
1.62 +(* val Rls {scr=Script s,...} = assoc_rls rls;
1.63 + *)
1.64 + (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
1.65 + | Seq {scr=EmptyScr,...} =>
1.66 + raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.67 + ^"use prep_rls for storing rule-sets !")
1.68 + | Seq {srls=srls,scr=Script s,...} =>
1.69 + (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
1.70 +(* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t);
1.71 + *)
1.72 + | init_istate (Rewrite_Set_Inst (subs, rls)) t =
1.73 + let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs
1.74 + (*...we suppose the substitution of only _one_ bound variable*)
1.75 + in case assoc_rls rls of
1.76 + Rls {scr=EmptyScr,...} =>
1.77 + raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.78 + ^"use prep_rls for storing rule-sets !")
1.79 + | Rls {scr=Script s,...} =>
1.80 + let val (form, bdv) = two_scr_arg s
1.81 + in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
1.82 + end
1.83 + | Seq {scr=EmptyScr,...} =>
1.84 + raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.85 + ^"use prep_rls for storing rule-sets !")
1.86 +(* val Seq {scr=Script s,...} = assoc_rls rls;
1.87 + *)
1.88 + | Seq {scr=Script s,...} =>
1.89 + let val (form, bdv) = two_scr_arg s
1.90 + in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
1.91 + end
1.92 + end;
1.93 +
1.94 +
1.95 +(*.a taci holds alle information required to build a node in the calc-tree;
1.96 + a taci is assumed to be used efficiently such that the calc-tree
1.97 + resulting from applying a taci need not be stored separately;
1.98 + see "type calcstate".*)
1.99 +(*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
1.100 + TODO.WN0512 ? redesign this _list_:
1.101 + # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
1.102 + # the latter problem may be resolved automatically if "fun autocalc" is
1.103 + not any more used for the specify-phase and for changing the phases*)
1.104 +type taci =
1.105 + (tac * (*for comparison with input tac*)
1.106 + tac_ * (*for ptree generation*)
1.107 + (pos' * (*after applying tac_, for ptree generation*)
1.108 + istate)); (*after applying tac_, for ptree generation*)
1.109 +val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', e_istate)): taci;
1.110 +(* val (tac, tac_, (pos', istate))::_ = tacis';
1.111 + *)
1.112 +fun taci2str ((tac, tac_, (pos', istate)):taci) =
1.113 + "( "^tac2str tac^", "^tac_2str tac_^", ( "^pos'2str pos'
1.114 + ^", "^istate2str istate^" ))";
1.115 +fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis;
1.116 +
1.117 +datatype pblmet = (*%^%*)
1.118 + Upblmet (*undefined*)
1.119 + | Problem of pblID (*%^%*)
1.120 + | Method of metID; (*%^%*)
1.121 +fun pblmet2str (Problem pblID) = "Problem "^(strs2str pblID)(*%^%*)
1.122 + | pblmet2str (Method metID) = "Method "^(metID2str metID);(*%^%*)
1.123 + (*%^%*) (*26.6. moved to sequent.sml: fun ~~~~~~~~~; was here below*)
1.124 +
1.125 +
1.126 +(* copy from 03.60.usecases.sml 15.11.99 *)
1.127 +datatype user_cmd =
1.128 + Accept | NotAccept | Example
1.129 +| YourTurn | MyTurn (* internal use only 7.6.02 java-sml*)
1.130 +| Rules
1.131 +| DontKnow (*| HowComes | WhatFor 7.6.02 java-sml*)
1.132 +| Undo (*| Back | Forward 7.6.02 java-sml*)
1.133 +| EndProof | EndSession
1.134 +| ActivePlus | ActiveMinus | SpeedPlus | SpeedMinus
1.135 + (*Stepwidth...7.6.02 java-sml*)
1.136 +| Auto | NotAuto | Details;
1.137 +(* for test-print-outs *)
1.138 +fun user_cmd2str Accept ="Accept"
1.139 + | user_cmd2str NotAccept ="NotAccept"
1.140 + | user_cmd2str Example ="Example"
1.141 + | user_cmd2str MyTurn ="MyTurn"
1.142 + | user_cmd2str YourTurn ="YourTurn"
1.143 + | user_cmd2str Rules ="Rules"
1.144 +(*| user_cmd2str HowComes ="HowComes"*)
1.145 + | user_cmd2str DontKnow ="DontKnow"
1.146 +(*| user_cmd2str WhatFor ="WhatFor"
1.147 + | user_cmd2str Back ="Back"*)
1.148 + | user_cmd2str Undo ="Undo"
1.149 +(*| user_cmd2str Forward ="Forward"*)
1.150 + | user_cmd2str EndProof ="EndProof"
1.151 + | user_cmd2str EndSession ="EndSession"
1.152 + | user_cmd2str ActivePlus = "ActivePlus"
1.153 + | user_cmd2str ActiveMinus = "ActiveMinus"
1.154 + | user_cmd2str SpeedPlus = "SpeedPlus"
1.155 + | user_cmd2str SpeedMinus = "SpeedMinus"
1.156 + | user_cmd2str Auto = "Auto"
1.157 + | user_cmd2str NotAuto = "NotAuto"
1.158 + | user_cmd2str Details = "Details";
1.159 +
1.160 +
1.161 +
1.162 +(*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
1.163 +datatype foppFK = (* in DG cases div 2 *)
1.164 + EmptyFoppFK (*DG internal*)
1.165 +| FormFK of cterm'
1.166 +| PpcFK of cterm' ppc;
1.167 +fun foppFK2str (FormFK ct') ="FormFK "^ct'
1.168 + | foppFK2str (PpcFK ppc) ="PpcFK "^(ppc2str ppc)
1.169 + | foppFK2str EmptyFoppFK ="EmptyFoppFK";
1.170 +
1.171 +
1.172 +datatype nest = Open | Closed | Nundef;
1.173 +fun nest2str Open = "Open"
1.174 + | nest2str Closed = "Closed"
1.175 + | nest2str Nundef = "Nundef";
1.176 +
1.177 +type indent = int;
1.178 +datatype edit = EdUndef | Write | Protect;
1.179 + (* bridge --> kernel *)
1.180 + (* bridge <-> kernel *)
1.181 +(* needed in dialog.sml *) (* bridge <-- kernel *)
1.182 +fun edit2str EdUndef = "EdUndef"
1.183 + | edit2str Write = "Write"
1.184 + | edit2str Protect = "Protect";
1.185 +
1.186 +
1.187 +datatype inout =
1.188 + New_User | End_User (*<->*)
1.189 +| New_Proof | End_Proof (*<->*)
1.190 +| Command of user_cmd (*-->*)
1.191 +| Request of string | Message of string (*<--*)
1.192 +| Error_ of string | System of string (*<--*)
1.193 +| FoPpcFK of foppFK (*-->*)
1.194 +| FormKF of cellID * edit * indent * nest * cterm' (*<--*)
1.195 +| PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) (*<--*)
1.196 +| RuleFK of tac (*-->*)
1.197 +| RuleKF of edit * tac (*<--*)
1.198 +| RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*)
1.199 +| Select of tac list (*<--*)
1.200 +| RefineKF of match list (*<--*)
1.201 +| Speed of int (*<--*)
1.202 +| Active of int (*<--*)
1.203 +| Domain of domID; (*<--*)
1.204 +
1.205 +fun inout2str End_Proof = "End_Proof"
1.206 + | inout2str (Command user_cmd) = "Command "^(user_cmd2str user_cmd)
1.207 + | inout2str (Request s) = "Request "^s
1.208 + | inout2str (Message s) = "Message "^s
1.209 + | inout2str (Error_ s) = "Error_ "^s
1.210 + | inout2str (System s) = "System "^s
1.211 + | inout2str (FoPpcFK foppFK) = "FoPpcFK "^(foppFK2str foppFK)
1.212 + | inout2str (FormKF (cellID, edit, indent, nest, ct')) =
1.213 + "FormKF ("^(string_of_int cellID)^","
1.214 + ^(edit2str edit)^","^(string_of_int indent)^","
1.215 + ^(nest2str nest)^",("
1.216 + ^ct' ^")"
1.217 + | inout2str (PpcKF (cellID, edit, indent, nest, (pm,itemppc))) =
1.218 + "PpcKF ("^(string_of_int cellID)^","
1.219 + ^(edit2str edit)^","^(string_of_int indent)^","
1.220 + ^(nest2str nest)^",("
1.221 + ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))"
1.222 + | inout2str (RuleKF (edit,tac)) = "RuleKF "^
1.223 + pair2str(edit2str edit,tac2str tac)
1.224 + | inout2str (RuleFK tac) = "RuleFK "^(tac2str tac)
1.225 + | inout2str (Select tacs)=
1.226 + "Select "^((strs2str' o (map tac2str)) tacs)
1.227 + | inout2str (RefineKF ms) = "RefineKF "^(matchs2str ms)
1.228 + | inout2str (Speed i) = "Speed "^(string_of_int i)
1.229 + | inout2str (Active i) = "Active "^(string_of_int i)
1.230 + | inout2str (Domain dI) = "Domain "^dI;
1.231 +fun inouts2str ios = (strs2str' o (map inout2str)) ios;
1.232 +
1.233 +datatype mout =
1.234 + Form' of inout (* packing cterm' | cterm' ppc *)
1.235 +| Problems of inout (* passes specify (and solve) *)
1.236 +| Error' of inout
1.237 +| EmptyMout;
1.238 +
1.239 +fun mout2str (Form' inout) ="Form' "^(inout2str inout)
1.240 + | mout2str (Error' inout) ="Error' "^(inout2str inout)
1.241 + | mout2str (EmptyMout ) ="EmptyMout";
1.242 +
1.243 +(*fun Form'2str (Form' )*)
1.244 +
1.245 +
1.246 +
1.247 +
1.248 +
1.249 +(* init pbl with ...,dsc,empty | [] *)
1.250 +fun init_pbl pbt =
1.251 + let
1.252 + fun pbt2itm (f,(d,t)) =
1.253 + ((0,[],false,f,Inc((d,[]),(e_term,[]))):itm);
1.254 + in map pbt2itm pbt end;
1.255 +(*take formal parameters from pbt, for transfer from pbl/met-hierarchy*)
1.256 +fun init_pbl' pbt =
1.257 + let
1.258 + fun pbt2itm (f,(d,t)) =
1.259 + ((0,[],false,f,Inc((d,[t]),(e_term,[]))):itm);
1.260 + in map pbt2itm pbt end;
1.261 +
1.262 +
1.263 +(*generate 1 ppobj in ptree*)
1.264 +(*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
1.265 +fun generate1 thy (Add_Given' (_, itmlist)) Uistate (pos as (p,p_)) pt =
1.266 + (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,
1.267 + (Upblmet,itms2itemppc thy [][]))),
1.268 + case p_ of Pbl => update_pbl pt p itmlist
1.269 + | Met => update_met pt p itmlist)
1.270 + | generate1 thy (Add_Find' (_, itmlist)) Uistate (pos as (p,p_)) pt =
1.271 + (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.272 + case p_ of Pbl => update_pbl pt p itmlist
1.273 + | Met => update_met pt p itmlist)
1.274 + | generate1 thy (Add_Relation' (_, itmlist)) Uistate (pos as (p,p_)) pt =
1.275 + (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.276 + case p_ of Pbl => update_pbl pt p itmlist
1.277 + | Met => update_met pt p itmlist)
1.278 +
1.279 + | generate1 thy (Specify_Theory' domID) Uistate (pos as (p,_)) pt =
1.280 + (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.281 + update_domID pt p domID)
1.282 +
1.283 + | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate
1.284 + (pos as (p,_)) pt =
1.285 + let val pt = update_pbl pt p itms
1.286 + val pt = update_pblID pt p pI
1.287 + in ((p,Pbl),[],
1.288 + Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.289 + pt) end
1.290 +
1.291 + | generate1 thy (Specify_Method' (mID, oris, itms)) Uistate
1.292 + (pos as (p,_)) pt =
1.293 + let val pt = update_oris pt p oris
1.294 + val pt = update_met pt p itms
1.295 + val pt = update_metID pt p mID
1.296 + in ((p,Met),[],
1.297 + Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.298 + pt) end
1.299 +
1.300 + | generate1 thy (Model_Problem' (_, itms, met)) Uistate (pos as (p,_)) pt =
1.301 +(* val (itms,pos as (p,_)) = (pbl, pos);
1.302 + *)
1.303 + let val pt = update_pbl pt p itms
1.304 + val pt = update_met pt p met
1.305 + in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef,
1.306 + (Upblmet,itms2itemppc thy [][]))), pt) end
1.307 +
1.308 + | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl))
1.309 + Uistate (pos as (p,_)) pt =
1.310 + let val pt = update_pbl pt p pbl
1.311 + val pt = update_orispec pt p (domID,pIre,metID)
1.312 + in (pos,[],
1.313 + Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.314 + pt) end
1.315 +
1.316 + | generate1 thy (Refine_Problem' (pI,_)) Uistate (pos as (p,_)) pt =
1.317 + let val (dI,_,mI) = get_obj g_spec pt p
1.318 + val pt = update_spec pt p (dI, pI, mI)
1.319 + in (pos,[],
1.320 + Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),pt)
1.321 + end
1.322 +
1.323 + | generate1 thy (Apply_Method' (_,topt, is)) _ (pos as (p,p_)) pt =
1.324 + ((*writeln("###generate1 Apply_Method': pos = "^pos'2str (p,p_));
1.325 + writeln("###generate1 Apply_Method': topt= "^termopt2str topt);
1.326 + writeln("###generate1 Apply_Method': is = "^istate2str is);*)
1.327 + case topt of
1.328 + SOME t =>
1.329 + let val (pt,c) = cappend_form pt p is t
1.330 + (*val _= writeln("###generate1 Apply_Method: after cappend")*)
1.331 + in (pos,c, EmptyMout,pt)
1.332 + end
1.333 + | NONE =>
1.334 + (pos,[],EmptyMout,update_env pt p (SOME is)))
1.335 +(* val (thy, (Take' t), l, (p,p_), pt) =
1.336 + ((assoc_thy "Isac.thy"), tac_, is, pos, pt);
1.337 + *)
1.338 + | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *)
1.339 + let (*val _=writeln("### generate1: Take' pos="^pos'2str (p,p_));*)
1.340 + val p = let val (ps,p') = split_last p(*no connex to prev.ppobj*)
1.341 + in if p'=0 then ps@[1] else p end;
1.342 + val (pt,c) = cappend_form pt p l t;
1.343 + in ((p,Frm):pos', c,
1.344 + Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
1.345 +
1.346 +(* val (l, (p,p_)) = (RrlsState is, p);
1.347 +
1.348 + val (thy, Begin_Trans' t, l, (p,Frm), pt) =
1.349 + (assoc_thy "Isac.thy", tac_, is, p, pt);
1.350 + *)
1.351 + | generate1 thy (Begin_Trans' t) l (p,Frm) pt =
1.352 + let (* print_depth 99;
1.353 + map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
1.354 + *)
1.355 + val (pt,c) = cappend_form pt p l t
1.356 + (* print_depth 99;
1.357 + map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
1.358 + *)
1.359 + val pt = update_branch pt p TransitiveB (*040312*)
1.360 + (*replace the old PrfOjb ~~~~~*)
1.361 + val p = (lev_on o lev_dn(*starts with [...,0]*)) p;
1.362 + val (pt,c') = cappend_form pt p l t(*FIXME.0402 same istate ???*);
1.363 + in ((p,Frm), c @ c', Form' (FormKF (~1,EdUndef,(length p), Nundef,
1.364 + term2str t)), pt) end
1.365 +
1.366 + (* val (thy, Begin_Trans' t, l, (p,Res), pt) =
1.367 + (assoc_thy "Isac.thy", tac_, is, p, pt);
1.368 + *)
1.369 + | generate1 thy (Begin_Trans' t) l (p ,Res) pt =
1.370 + (*append after existing PrfObj _________*)
1.371 + generate1 thy (Begin_Trans' t) l (lev_on p,Frm) pt
1.372 +
1.373 + | generate1 thy (End_Trans' tasm) l (p,p_) pt =
1.374 + let val p' = lev_up p
1.375 + val (pt,c) = append_result pt p' l tasm Complete;
1.376 + in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)),
1.377 + pt) end
1.378 +
1.379 + | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) l (p,p_) pt =
1.380 + let (*val _= writeln("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));*)
1.381 + val (pt,c) = cappend_atomic pt p l f
1.382 + (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
1.383 + val pt = update_branch pt p TransitiveB (*040312*)
1.384 + (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
1.385 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.386 + pt) end
1.387 +
1.388 + | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) l (p,p_) pt =
1.389 + let (*val _= writeln("###generate1 Rewrite': pos= "^pos'2str (p,p_))*)
1.390 + val (pt,c) = cappend_atomic pt p l f (Rewrite thm') (f',asm) Complete
1.391 + val pt = update_branch pt p TransitiveB (*040312*)
1.392 + (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
1.393 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.394 + pt)end
1.395 +
1.396 + | generate1 thy (Rewrite_Asm' all) l p pt =
1.397 + generate1 thy (Rewrite' all) l p pt
1.398 +
1.399 + | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) l (p,p_) pt =
1.400 +(* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) =
1.401 + (assoc_thy "Isac.thy", tac_, is, pos, pt);
1.402 + *)
1.403 + let (*val _=writeln("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*)
1.404 + val (pt,c) = cappend_atomic pt p l f
1.405 + (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
1.406 + val pt = update_branch pt p TransitiveB (*040312*)
1.407 + (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
1.408 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.409 + pt) end
1.410 +
1.411 + | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) l (p,p_) pt =
1.412 + let val (pt,c) = cappend_form pt p l f
1.413 + val pt = update_branch pt p TransitiveB (*040312*)
1.414 +
1.415 + val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
1.416 + val tac_ = Apply_Method' (e_metID, SOME t, is)
1.417 + val pos' = ((lev_on o lev_dn) p, Frm)
1.418 + in (*implicit Take*) generate1 thy tac_ is pos' pt end
1.419 +
1.420 + | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =
1.421 + let (*val _= writeln("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
1.422 + val (pt,c) = cappend_atomic pt p l f
1.423 + (Rewrite_Set (id_rls rls')) (f',asm) Complete
1.424 + val pt = update_branch pt p TransitiveB (*040312*)
1.425 + (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
1.426 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.427 + pt) end
1.428 +
1.429 + | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) l (p,p_) pt =
1.430 + let val (pt,c) = cappend_form pt p l f
1.431 + val pt = update_branch pt p TransitiveB (*040312*)
1.432 +
1.433 + val is = init_istate (Rewrite_Set (id_rls rls)) f
1.434 + val tac_ = Apply_Method' (e_metID, SOME t, is)
1.435 + val pos' = ((lev_on o lev_dn) p, Frm)
1.436 + in (*implicit Take*) generate1 thy tac_ is pos' pt end
1.437 +
1.438 + | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
1.439 + let (*val _=writeln("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
1.440 + (*val (l',_) = get_obj g_loc pt p..don't overwrite with l from subpbl*)
1.441 + val (pt,c) = append_result pt p l (scval,map str2term asm) Complete
1.442 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p),
1.443 + Nundef, term2str scval)), pt) end
1.444 +
1.445 + | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt =
1.446 + let val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f',[]) Complete;
1.447 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.448 + pt) end
1.449 +
1.450 + | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt =
1.451 + let(*val _=writeln("###generate1 Check_elementwise': p= "^pos'2str(p,p_))*)
1.452 + val (pt,c) = cappend_atomic pt p l consts
1.453 + (Check_elementwise pred) (f',asm) Complete;
1.454 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.455 + pt) end
1.456 +
1.457 + | generate1 thy (Or_to_List' (ors,list)) l (p,p_) pt =
1.458 + let val (pt,c) = cappend_atomic pt p l ors
1.459 + Or_to_List (list,[]) Complete;
1.460 + in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)),
1.461 + pt) end
1.462 +
1.463 + | generate1 thy (Substitute' (subte, t, t')) l (p,p_) pt =
1.464 + let val (pt,c) = cappend_atomic pt p l t (Substitute (subte2sube subte))
1.465 + (t',[]) Complete;
1.466 + in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef,
1.467 + term2str t')), pt)
1.468 + end
1.469 +
1.470 + | generate1 thy (Tac_ (_,f,id,f')) l (p,p_) pt =
1.471 + let val (pt,c) = cappend_atomic pt p l (str2term f)
1.472 + (Tac id) (str2term f',[]) Complete;
1.473 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end
1.474 +
1.475 + | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, f))
1.476 + l (p,p_) pt =
1.477 + let (*val _=writeln("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
1.478 + val (pt,c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
1.479 + (oris, (domID, pblID, metID), hdl);
1.480 + (*val pbl = init_pbl ((#ppc o get_pbt) pblID);
1.481 + val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*)
1.482 + (*val _= writeln("### generate1: is([3],Frm)= "^
1.483 + (istate2str (get_istate pt ([3],Frm))));*)
1.484 + val f = Syntax.string_of_term (thy2ctxt thy) f;
1.485 + in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
1.486 +
1.487 + | generate1 thy m' _ _ _ =
1.488 + raise error ("generate1: not impl.for "^(tac_2str m'))
1.489 +;
1.490 +
1.491 +
1.492 +fun generate_hard thy m' (p,p_) pt =
1.493 + let
1.494 + val p = case p_ of Frm => p | Res => lev_on p
1.495 + | _ => raise error ("generate_hard: call by "^(pos'2str (p,p_)));
1.496 + in generate1 thy m' e_istate (p,p_) pt end;
1.497 +
1.498 +
1.499 +
1.500 +(*tacis are in reverse order from nxt_solve_/specify_: last = fst to insert*)
1.501 +(* val (tacis, (pt, _)) = (tacis, ptp);
1.502 +
1.503 + val (tacis, (pt, c, _)) = (rev tacis, (pt, [], (p, Res)));
1.504 + *)
1.505 +fun generate ([]: taci list) ptp = ptp
1.506 + | generate tacis (pt, c, _:pos'(*!dropped!WN0504redesign generate/tacis?*))=
1.507 + let val (tacis', (_, tac_, (p, is))) = split_last tacis
1.508 + (* for recursion ...
1.509 + (tacis', (_, tac_, (p, is))) = split_last tacis';
1.510 + *)
1.511 + val (p',c',_,pt') = generate1 (assoc_thy "Isac.thy") tac_ is p pt
1.512 + in generate tacis' (pt', c@c', p') end;
1.513 +
1.514 +
1.515 +
1.516 +(*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
1.517 + * of for connecting a user-input formula with the current calc-state. *
1.518 + *# It is somewhat incompatible with the rest of the math-engine: *
1.519 + * (1) it is not created by a script *
1.520 + * (2) thus there cannot be another user-input within a derivation *
1.521 + *# It suffers particularily from the not-well-foundedness of the math-engine*
1.522 + * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
1.523 + * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
1.524 + * (3) FIXME and eventually 'lev_back' *
1.525 + *# SOME improvements are evident FIXME.040215 '_deriv'ation: *
1.526 + * (1) FIXME nest Rls_ in 'make_deriv' *
1.527 + * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
1.528 + * user-input will become possible in this part of a derivation *
1.529 + * (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
1.530 + * while a non-derivable inform requires to step until End_Proof' *
1.531 + * (4) FIXME find criteria on when _not_ to step until End_Proof' *
1.532 + * (5) FIXME
1.533 +.*)
1.534 +(*.update pos in tacis for embedding by generate.*)
1.535 +(* val
1.536 + *)
1.537 +fun insert_pos _ [] = []
1.538 + | insert_pos (p:pos) (((tac,tac_,(_, ist))::tacis):taci list) =
1.539 + ((tac,tac_,((p, Res), ist)):taci)
1.540 + ::((insert_pos (lev_on p) tacis):taci list);
1.541 +
1.542 +fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm)
1.543 + | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm)
1.544 + | res_from_taci (_, tac_, _) =
1.545 + raise error ("res_from_taci: called with" ^ tac_2str tac_);
1.546 +
1.547 +(*.embed the tacis created by a '_deriv'ation; sys.form <> input.form
1.548 + tacis are in order, thus are reverted for generate.*)
1.549 +(* val (tacis, (pt, pos as (p, Frm))) = (tacis', ptp);
1.550 + *)
1.551 +fun embed_deriv (tacis:taci list) (pt, pos as (p, Frm):pos') =
1.552 + (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
1.553 + and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
1.554 + let val (res, asm) = (res_from_taci o last_elem) tacis
1.555 + val (SOME ist,_) = get_obj g_loc pt p
1.556 + val form = get_obj g_form pt p
1.557 + (*val p = lev_on p; ---------------only difference to (..,Res) below*)
1.558 + val tacis = (Begin_Trans, Begin_Trans' form, (pos, Uistate))
1.559 + ::(insert_pos ((lev_on o lev_dn) p) tacis)
1.560 + @ [(End_Trans, End_Trans' (res, asm),
1.561 + (pos_plus (length tacis) (lev_dn p, Res),
1.562 + new_val res ist))]
1.563 + val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.564 + val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
1.565 + val pt = update_tac pt p (Derive (id_rls nrls))
1.566 + (*FIXME.040216 struct.ctree*)
1.567 + val pt = update_branch pt p TransitiveB
1.568 + in (c, (pt, pos:pos')) end
1.569 +
1.570 +(* val (tacis, (pt, (p, Res))) = (tacis', ptp);
1.571 + *)
1.572 + | embed_deriv tacis (pt, (p, Res)) =
1.573 + (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
1.574 + and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
1.575 + let val (res, asm) = (res_from_taci o last_elem) tacis
1.576 + val (_, SOME ist) = get_obj g_loc pt p
1.577 + val (f,a) = get_obj g_result pt p
1.578 + val p = lev_on p(*---------------only difference to (..,Frm) above*);
1.579 + val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), Uistate))
1.580 + ::(insert_pos ((lev_on o lev_dn) p) tacis)
1.581 + @ [(End_Trans, End_Trans' (res, asm),
1.582 + (pos_plus (length tacis) (lev_dn p, Res),
1.583 + new_val res ist))];
1.584 + val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.585 + val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
1.586 + val pt = update_tac pt p (Derive (id_rls nrls))
1.587 + (*FIXME.040216 struct.ctree*)
1.588 + val pt = update_branch pt p TransitiveB
1.589 + in (c, (pt, pos)) end;