1.1 --- a/src/Tools/isac/Isac_Mathengine.thy Wed Aug 18 13:40:09 2010 +0200
1.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Wed Aug 18 13:53:15 2010 +0200
1.3 @@ -33,18 +33,17 @@
1.4 use_thy"Scripts/Script"
1.5 use "Scripts/scrtools.sml"
1.6
1.7 +use "ME/mstools.sml"
1.8 +use "ME/ctree.sml"
1.9 +
1.10 +
1.11 ML {*
1.12 member;
1.13 @{term 111};
1.14 *}
1.15
1.16 -use "ME/mstools.sml"
1.17 -
1.18 -
1.19 -
1.20
1.21 (*
1.22 -use "ME/ctree.sml"
1.23 use "ME/ptyps.sml"
1.24 use "ME/generate.sml"
1.25 use "ME/calchead.sml"
1.26 @@ -77,7 +76,7 @@
1.27 *}
1.28 *)
1.29
1.30 -
1.31 +(*--------------------------shift to some isac-10 -------------------
1.32 (*cleaner output from...*)
1.33 ML_command {*
1.34 "----- ";
1.35 @@ -179,6 +178,7 @@
1.36 ML{* Name.invents context "foo" 10 *}
1.37 (*ML{* Name variants ... *}*)
1.38 *)
1.39 +--------------------------shift to some isac-10 -------------------*)
1.40
1.41 end
1.42
2.1 --- a/src/Tools/isac/ME/ctree.sml Wed Aug 18 13:40:09 2010 +0200
2.2 +++ b/src/Tools/isac/ME/ctree.sml Wed Aug 18 13:53:15 2010 +0200
2.3 @@ -233,10 +233,10 @@
2.4 (apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o
2.5 (apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;*)
2.6 fun subst2subs s = map (pair2str o
2.7 - (apfst (Sign.string_of_term (sign_of thy))) o
2.8 - (apsnd (Sign.string_of_term (sign_of thy)))) s;
2.9 -fun subst2subs' s = map ((apfst (Sign.string_of_term (sign_of thy))) o
2.10 - (apsnd (Sign.string_of_term (sign_of thy)))) s;
2.11 + (apfst (Syntax.string_of_term (ctxt_Isac""))) o
2.12 + (apsnd (Syntax.string_of_term (ctxt_Isac"")))) s;
2.13 +fun subst2subs' s = map ((apfst (Syntax.string_of_term (ctxt_Isac""))) o
2.14 + (apsnd (Syntax.string_of_term (ctxt_Isac"")))) s;
2.15 fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;
2.16 (*> subs2subst thy ["(bdv,x)","(err,#0)"];
2.17 val it =
2.18 @@ -264,7 +264,7 @@
2.19 * safe (*estimation of how result will be obtained*)
2.20 * bool; (*true = strongly .., false = weakly associated:
2.21 only used during ass_dn/up*)
2.22 -val e_scrstate = ([],[],None,e_term,Sundef,false):scrstate;
2.23 +val e_scrstate = ([],[],NONE,e_term,Sundef,false):scrstate;
2.24
2.25
2.26 (*21.8.02 ---> definitions.sml for datatype scr
2.27 @@ -283,7 +283,7 @@
2.28 Uistate (*undefined in modspec, in '_deriv'ation*)
2.29 | ScrState of scrstate (*for script interpreter*)
2.30 | RrlsState of rrlsstate; (*for reverse rewriting*)
2.31 -val e_istate = (ScrState ([],[],None,e_term,Sundef,false)):istate;
2.32 +val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false)):istate;
2.33
2.34 type iist = istate option * istate option;
2.35 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
2.36 @@ -300,10 +300,10 @@
2.37 "RrlsState ("^(term2str t)^", "^(term2str t1)^", "^
2.38 ((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^
2.39 ((strs2str o (map rta2str)) rtas)^")";
2.40 -fun istates2str (None, None) = "(#None, #None)"
2.41 - | istates2str (None, Some ist) = "(#None,\n#Some "^istate2str ist^")"
2.42 - | istates2str (Some ist, None) = "(#Some "^istate2str ist^",\n #None)"
2.43 - | istates2str (Some i1, Some i2) = "(#Some "^istate2str i1^",\n #Some "^
2.44 +fun istates2str (NONE, NONE) = "(#NONE, #NONE)"
2.45 + | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME "^istate2str ist^")"
2.46 + | istates2str (SOME ist, NONE) = "(#SOME "^istate2str ist^",\n #NONE)"
2.47 + | istates2str (SOME i1, SOME i2) = "(#SOME "^istate2str i1^",\n #SOME "^
2.48 istate2str i2^")";
2.49
2.50 fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =
2.51 @@ -351,7 +351,7 @@
2.52 | Apply_Method of metID
2.53 (*.creates an 'istate' in PblObj.env; in case of 'init_form'
2.54 creates a formula at ((lev_on o lev_dn) p, Frm) and in this ppobj.'loc'
2.55 - 'Some istate' (at fst of 'loc').
2.56 + 'SOME istate' (at fst of 'loc').
2.57 As each step (in the solve-phase) has a resulting formula (at the front-end)
2.58 Apply_Method also does the 1st step in the script (an 'initac') if there
2.59 is no 'init_form' .*)
2.60 @@ -508,16 +508,16 @@
2.61 | rls_of tac = raise error ("rls_of: called with tac '"^tac2IDstr tac^"'");
2.62
2.63 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) =
2.64 - (thmID, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst))
2.65 - | thm_of_rew (Rewrite (thmID,_)) = (thmID, None)
2.66 - | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, None);
2.67 + (thmID, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst))
2.68 + | thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE)
2.69 + | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE);
2.70
2.71 fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) =
2.72 - (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst))
2.73 - | rls_of_rewset (Rewrite_Set rls) = (rls, None)
2.74 - | rls_of_rewset (Detail_Set rls) = (rls, None)
2.75 + (rls, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst))
2.76 + | rls_of_rewset (Rewrite_Set rls) = (rls, NONE)
2.77 + | rls_of_rewset (Detail_Set rls) = (rls, NONE)
2.78 | rls_of_rewset (Detail_Set_Inst (subs, rls)) =
2.79 - (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst));
2.80 + (rls, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst));
2.81
2.82 fun rule2tac _ (Calc (opID, thm)) = Calculate (calID2calcID opID)
2.83 | rule2tac [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm)
2.84 @@ -679,8 +679,8 @@
2.85 "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
2.86 | Rewrite_Set'(thy',pasm,rls',f,(f',asm))
2.87 => "Rewrite_Set' ("^thy'^","^(bool2str pasm)^","^(id_rls rls')^","
2.88 - ^(Sign.string_of_term (sign_of thy) f)^",("^(Sign.string_of_term (sign_of thy) f')
2.89 - ^","^((strs2str o (map (Sign.string_of_term (sign_of thy)))) asm)^"))"
2.90 + ^(Syntax.string_of_term (ctxt_Isac"") f)^",("^(Syntax.string_of_term (ctxt_Isac"") f')
2.91 + ^","^((strs2str o (map (Syntax.string_of_term (ctxt_Isac"")))) asm)^"))"
2.92
2.93 | End_Detail' _ => "End_Detail' xxx"
2.94 | Detail_Set' _ => "Detail_Set' xxx"
2.95 @@ -724,8 +724,8 @@
2.96 "\n("^(loc_2str l)^",("^(tac_2str m)^
2.97 ",\n ens= "^(subst2str eno)^
2.98 ",\n env= "^(subst2str env)^
2.99 - ",\n iar= "^(Sign.string_of_term (sign_of thy) iar)^
2.100 - ",\n res= "^(Sign.string_of_term (sign_of thy) res)^
2.101 + ",\n iar= "^(Syntax.string_of_term (ctxt_Isac"") iar)^
2.102 + ",\n res= "^(Syntax.string_of_term (ctxt_Isac"") res)^
2.103 ",\n "^(safe2str s)^"))";
2.104 fun ets2str (ets:ets) = (strs2str o (map ets2s)) ets;
2.105
2.106 @@ -743,7 +743,7 @@
2.107 form : term,
2.108 tac : tac, (* also in istate*)
2.109 loc : istate option * istate option, (*for form, result
2.110 -13.8.02: (None,None) <==> e_istate ! see update_loc, get_loc*)
2.111 +13.8.02: (NONE,NONE) <==> e_istate ! see update_loc, get_loc*)
2.112 branch: branch,
2.113 result: term * term list,
2.114 ostate: ostate} (*Complete <=> result is OK*)
2.115 @@ -852,16 +852,16 @@
2.116 (* show hd origin or form only *)
2.117 fun pr_short (p:pos) (PblObj {origin = (ori,_,_),...}) =
2.118 ((pr_pos p) ^ " ----- pblobj -----\n")
2.119 -(* ((((Sign.string_of_term (sign_of thy)) o #4 o hd) ori)^" "^
2.120 - (((Sign.string_of_term (sign_of thy)) o hd(*!?!*) o #5 o hd) ori))^
2.121 +(* ((((Syntax.string_of_term (ctxt_Isac"")) o #4 o hd) ori)^" "^
2.122 + (((Syntax.string_of_term (ctxt_Isac"")) o hd(*!?!*) o #5 o hd) ori))^
2.123 "\n") *)
2.124 | pr_short p (PrfObj {form = form,...}) =
2.125 ((pr_pos p) ^ (term2str form) ^ "\n");
2.126 (*
2.127 fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) =
2.128 ((ints2str c) ^" "^
2.129 - ((((Sign.string_of_term (sign_of thy)) o #4 o hd) ori)^" "^
2.130 - (((Sign.string_of_term (sign_of thy)) o hd(*!?!*) o #5 o hd) ori))^
2.131 + ((((Syntax.string_of_term (ctxt_Isac"")) o #4 o hd) ori)^" "^
2.132 + (((Syntax.string_of_term (ctxt_Isac"")) o hd(*!?!*) o #5 o hd) ori))^
2.133 "\n")
2.134 | pr_cell p (PrfObj {cell = c, form = form,...}) =
2.135 ((ints2str c) ^" "^ (term2str form) ^ "\n");
2.136 @@ -938,7 +938,7 @@
2.137
2.138
2.139 (* for use by get_obj *)
2.140 -fun g_cell (PblObj {cell = c,...}) = None
2.141 +fun g_cell (PblObj {cell = c,...}) = NONE
2.142 | g_cell (PrfObj {cell = c,...}) = c;(*WN0607 hack for quick introduction of lrd + rewrite-at (thms, calcs)*)
2.143 fun g_form (PrfObj {form = f,...}) = f
2.144 | g_form (PblObj {origin=(_,_,f),...}) = f;
2.145 @@ -978,7 +978,7 @@
2.146 fun g_ostate' (Nd (PblObj {ostate = r,...}, _)) = r
2.147 | g_ostate' (Nd (PrfObj {ostate = r,...}, _)) = r;
2.148
2.149 -fun gpt_cell (Nd (PblObj {cell = c,...},_)) = None
2.150 +fun gpt_cell (Nd (PblObj {cell = c,...},_)) = NONE
2.151 | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;
2.152
2.153 (*in CalcTree/Subproblem an 'just_created_' model is created;
2.154 @@ -1271,17 +1271,17 @@
2.155
2.156
2.157 fun delete_result pt (p:pos) =
2.158 - (appl_obj (repl_result (fst (get_obj g_loc pt p), None)
2.159 + (appl_obj (repl_result (fst (get_obj g_loc pt p), NONE)
2.160 (e_term,[]) Incomplete) pt p);
2.161
2.162 fun del_res (PblObj {cell, fmz, origin, spec, probl, meth,
2.163 env, loc=(l1,_), branch, result, ostate}) =
2.164 PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth,
2.165 - env=env, loc=(l1,None), branch=branch, result=(e_term,[]),
2.166 + env=env, loc=(l1,NONE), branch=branch, result=(e_term,[]),
2.167 ostate=Incomplete}
2.168
2.169 | del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) =
2.170 - PrfObj {cell=cell,form=form,tac=tac, loc=(l1,None), branch=branch,
2.171 + PrfObj {cell=cell,form=form,tac=tac, loc=(l1,NONE), branch=branch,
2.172 result=(e_term,[]), ostate=Incomplete};
2.173
2.174
2.175 @@ -1318,22 +1318,22 @@
2.176 fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
2.177
2.178 (*done by append_* !! 3.5.02; ununsed WN050305 thus outcommented
2.179 -fun update_loc pt (p,_) (ScrState ([],[],None,
2.180 +fun update_loc pt (p,_) (ScrState ([],[],NONE,
2.181 Const ("empty",_),Sundef,false)) =
2.182 - appl_obj (repl_loc (None,None)) pt p
2.183 + appl_obj (repl_loc (NONE,NONE)) pt p
2.184 | update_loc pt (p,Res) x =
2.185 let val (lform,_) = get_obj g_loc pt p
2.186 - in appl_obj (repl_loc (lform,Some x)) pt p end
2.187 + in appl_obj (repl_loc (lform,SOME x)) pt p end
2.188
2.189 | update_loc pt (p,_) x =
2.190 let val (_,lres) = get_obj g_loc pt p
2.191 - in appl_obj (repl_loc (Some x,lres)) pt p end;-------------*)
2.192 + in appl_obj (repl_loc (SOME x,lres)) pt p end;-------------*)
2.193
2.194 (*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*)
2.195 fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p;
2.196
2.197 (*13.8.02---------------------------
2.198 -fun get_loc EmptyPtree _ = None
2.199 +fun get_loc EmptyPtree _ = NONE
2.200 | get_loc pt (p,Res) =
2.201 let val (lfrm,lres) = get_obj g_loc pt p
2.202 in if lres = e_istate then lfrm else lres end
2.203 @@ -1344,14 +1344,14 @@
2.204 fun get_loc EmptyPtree _ = e_istate
2.205 | get_loc pt (p,Res) =
2.206 (case get_obj g_loc pt p of
2.207 - (Some i, None) => i
2.208 - | (None , None) => e_istate
2.209 - | (_ , Some i) => i)
2.210 + (SOME i, NONE) => i
2.211 + | (NONE , NONE) => e_istate
2.212 + | (_ , SOME i) => i)
2.213 | get_loc pt (p,_) =
2.214 (case get_obj g_loc pt p of
2.215 - (None , Some i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
2.216 - | (None , None) => e_istate
2.217 - | (Some i, _) => i);
2.218 + (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
2.219 + | (NONE , NONE) => e_istate
2.220 + | (SOME i, _) => i);
2.221 val get_istate = get_loc; (*3.5.02*)
2.222
2.223 (*.collect the assumptions within a problem up to a certain position.*)
2.224 @@ -1510,7 +1510,7 @@
2.225 (apfst bool2str)))) bts;
2.226 fun ocalhd2str ((b, p, hdf, itms, prec, spec):ocalhd) =
2.227 "("^bool2str b^", "^pos_2str p^", "^term2str hdf^
2.228 - ", "^itms2str_ (assoc_thy "Isac.thy") itms^
2.229 + ", "^itms2str_ (thy2ctxt "Isac") itms^
2.230 ", "^preconds2str prec^", \n"^spec2str spec^" )";
2.231
2.232
2.233 @@ -2015,10 +2015,10 @@
2.234 let (**val _= writeln("#@append_atomic: pos ="^pos2str p)**)
2.235 val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
2.236 then (*after Take*)
2.237 - ((fst (get_obj g_loc pt p), Some l),
2.238 + ((fst (get_obj g_loc pt p), SOME l),
2.239 get_obj g_form pt p)
2.240 - else ((None, Some l), f)
2.241 - in insert (PrfObj {cell = None,
2.242 + else ((NONE, SOME l), f)
2.243 + in insert (PrfObj {cell = NONE,
2.244 form = f,
2.245 tac = r,
2.246 loc = iss,
2.247 @@ -2048,7 +2048,7 @@
2.248 get_obj g_form pt p)
2.249 val (pt, cs) = cut_tree pt (p,Frm)
2.250 val pt = append_atomic p e_istate f r f' s pt
2.251 - val pt = update_loc' pt p (Some ist_form, Some ist_res)
2.252 + val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
2.253 in (pt, cs) end
2.254 else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
2.255
2.256 @@ -2056,13 +2056,13 @@
2.257 (* called by Take *)
2.258 fun append_form p l f pt =
2.259 ((*writeln("##@append_form: pos ="^pos2str p);*)
2.260 - insert (PrfObj {cell = None,
2.261 + insert (PrfObj {cell = NONE,
2.262 form = (*if existpt p pt
2.263 andalso get_obj g_tac pt p = Empty_Tac
2.264 (*distinction from 'old' (+complete!) pobjs*)
2.265 then get_obj g_form pt p else*) f,
2.266 tac = Empty_Tac,
2.267 - loc = (Some l, None),
2.268 + loc = (SOME l, NONE),
2.269 branch= NoBranch,
2.270 result= (e_term,[]),
2.271 ostate= Incomplete}) pt p
2.272 @@ -2088,7 +2088,7 @@
2.273 fun append_result pt p l f s =
2.274 ((*writeln("##@append_result: pos ="^pos2str p);*)
2.275 (appl_obj (repl_result (fst (get_obj g_loc pt p),
2.276 - Some l) f s) pt p, [])
2.277 + SOME l) f s) pt p, [])
2.278 );
2.279
2.280
2.281 @@ -2096,11 +2096,11 @@
2.282 fun append_parent p l f r b pt =
2.283 let (*val _= writeln("###append_parent: pos ="^pos2str p);*)
2.284 val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
2.285 - then ((fst (get_obj g_loc pt p), Some l),
2.286 + then ((fst (get_obj g_loc pt p), SOME l),
2.287 get_obj g_form pt p)
2.288 - else ((Some l, None), f)
2.289 + else ((SOME l, NONE), f)
2.290 in insert (PrfObj
2.291 - {cell = None,
2.292 + {cell = NONE,
2.293 form = f,
2.294 tac = r,
2.295 loc = ll,
2.296 @@ -2116,14 +2116,14 @@
2.297 fun append_problem [] l fmz (strs,spec,hdf) _ =
2.298 ((*writeln("###append_problem: pos = []");*)
2.299 (Nd (PblObj
2.300 - {cell = None,
2.301 + {cell = NONE,
2.302 origin= (strs,spec,hdf),
2.303 fmz = fmz,
2.304 spec = empty_spec,
2.305 probl = []:itm list,
2.306 meth = []:itm list,
2.307 - env = None,
2.308 - loc = (Some l, None),
2.309 + env = NONE,
2.310 + loc = (SOME l, NONE),
2.311 branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)
2.312 result= (e_term,[]),
2.313 ostate= Incomplete},[]))
2.314 @@ -2131,14 +2131,14 @@
2.315 | append_problem p l fmz (strs,spec,hdf) pt =
2.316 ((*writeln("###append_problem: pos ="^pos2str p);*)
2.317 insert (PblObj
2.318 - {cell = None,
2.319 + {cell = NONE,
2.320 origin= (strs,spec,hdf),
2.321 fmz = fmz,
2.322 spec = empty_spec,
2.323 probl = []:itm list,
2.324 meth = []:itm list,
2.325 - env = None,
2.326 - loc = (Some l, None),
2.327 + env = NONE,
2.328 + loc = (SOME l, NONE),
2.329 branch= TransitiveB,
2.330 result= (e_term,[]),
2.331 ostate= Incomplete}) pt p