1.1 --- a/src/Tools/isac/ME/generate.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,586 +0,0 @@
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;