1.1 --- a/src/Tools/isac/ME/mstools.sml Tue Aug 17 09:05:51 2010 +0200
1.2 +++ b/src/Tools/isac/ME/mstools.sml Wed Aug 18 13:40:09 2010 +0200
1.3 @@ -7,6 +7,8 @@
1.4
1.5 use"ME/mstools.sml" (*re-evaluate sml/ from scratch!*);
1.6 use"mstools.sml";
1.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.8 + 10 20 30 40 50 60 70 80
1.9 *)
1.10
1.11 signature SPECIFY_TOOLS =
1.12 @@ -23,19 +25,19 @@
1.13 | TypeE of string
1.14 val item2str : item -> string
1.15 type itm
1.16 - val itm2str : Theory.theory -> itm -> string
1.17 + val itm2str_ : Proof.context -> itm -> string
1.18 datatype
1.19 itm_ =
1.20 - Cor of (Term.term * Term.term list) * (Term.term * Term.term list)
1.21 - | Inc of (Term.term * Term.term list) * (Term.term * Term.term list)
1.22 - | Mis of Term.term * Term.term
1.23 + Cor of (term * term list) * (term * term list)
1.24 + | Inc of (term * term list) * (term * term list)
1.25 + | Mis of term * term
1.26 | Par of cterm'
1.27 - | Sup of Term.term * Term.term list
1.28 + | Sup of term * term list
1.29 | Syn of cterm'
1.30 | Typ of cterm'
1.31 val itm_2str : itm_ -> string
1.32 - val itm__2str : Theory.theory -> itm_ -> string
1.33 - val itms2str : Theory.theory -> itm list -> string
1.34 + val itm_2str_ : Proof.context -> itm_ -> string
1.35 + val itms2str_ : Proof.context -> itm list -> string
1.36 type 'a ppc
1.37 val ppc2str :
1.38 {Find: string list, With: string list, Given: string list,
1.39 @@ -47,7 +49,7 @@
1.40 val match2str : match -> string
1.41 datatype
1.42 match_ =
1.43 - Match_ of pblID * (itm list * (bool * Term.term) list)
1.44 + Match_ of pblID * (itm list * (bool * term) list)
1.45 | NoMatch_
1.46 val matchs2str : match list -> string
1.47 type ori
1.48 @@ -57,108 +59,107 @@
1.49 val preori2str : preori -> string
1.50 val preoris2str : preori list -> string
1.51 type penv
1.52 - (* val penv2str : Theory.theory -> penv -> string *)
1.53 + (* val penv2str_ : Proof.context -> penv -> string *)
1.54 type vats
1.55 (*----------------------------------------------------------------------*)
1.56 - val all_ts_in : itm_ list -> Term.term list
1.57 + val all_ts_in : itm_ list -> term list
1.58 val check_preconds :
1.59 'a ->
1.60 rls ->
1.61 - Term.term list -> itm list -> (bool * Term.term) list
1.62 + term list -> itm list -> (bool * term) list
1.63 val check_preconds' :
1.64 rls ->
1.65 - Term.term list ->
1.66 - itm list -> 'a -> (bool * Term.term) list
1.67 - (* val chkpre2item : rls -> Term.term -> bool * item *)
1.68 - val pres2str : (bool * Term.term) list -> string
1.69 - (* val evalprecond : rls -> Term.term -> bool * Term.term *)
1.70 + term list ->
1.71 + itm list -> 'a -> (bool * term) list
1.72 + (* val chkpre2item : rls -> term -> bool * item *)
1.73 + val pres2str : (bool * term) list -> string
1.74 + (* val evalprecond : rls -> term -> bool * term *)
1.75 (* val cnt : itm list -> int -> int * int *)
1.76 - val comp_dts : Theory.theory -> Term.term * Term.term list -> Thm.cterm
1.77 - val comp_dts' : Term.term * Term.term list -> Term.term
1.78 - val comp_dts'' : Term.term * Term.term list -> string
1.79 - val comp_ts : Term.term * Term.term list -> Term.term
1.80 - val d_in : itm_ -> Term.term
1.81 + val comp_dts : theory -> term * term list -> term
1.82 + val comp_dts' : term * term list -> term
1.83 + val comp_dts'' : term * term list -> string
1.84 + val comp_ts : term * term list -> term
1.85 + val d_in : itm_ -> term
1.86 val de_item : item -> cterm'
1.87 - val dest_list : Term.term * Term.term list -> Term.term list (* for testing *)
1.88 - val dest_list' : Term.term -> Term.term list
1.89 - val dts2str : Term.term * Term.term list -> string
1.90 + val dest_list : term * term list -> term list (* for testing *)
1.91 + val dest_list' : term -> term list
1.92 + val dts2str : term * term list -> string
1.93 val e_itm : itm
1.94 - (* val e_listBool : Term.term *)
1.95 - (* val e_listReal : Term.term *)
1.96 + (* val e_listBool : term *)
1.97 + (* val e_listReal : term *)
1.98 val e_ori : ori
1.99 val e_ori_ : ori
1.100 val empty_ppc : item ppc
1.101 (* val empty_ppc_ct' : cterm' ppc *)
1.102 - (* val getval : Term.term * Term.term list -> Term.term * Term.term *)
1.103 + (* val getval : term * term list -> term * term *)
1.104 (*val head_precond :
1.105 domID * pblID * 'a ->
1.106 - Term.term Library.option ->
1.107 + term option ->
1.108 rls ->
1.109 - Term.term list ->
1.110 - itm list -> 'b -> Term.term * (bool * Term.term) list*)
1.111 + term list ->
1.112 + itm list -> 'b -> term * (bool * term) list*)
1.113 (* val init_item : string -> item *)
1.114 (* val is_matches : match -> bool *)
1.115 (* val is_matches_ : match_ -> bool *)
1.116 - val is_var : Term.term -> bool
1.117 + val is_var : term -> bool
1.118 (* val item_ppc :
1.119 string ppc -> item ppc *)
1.120 val itemppc2str : item ppc -> string
1.121 - val linefeed : string -> string
1.122 (* val matches_pblID : match -> pblID *)
1.123 val max2 : ('a * int) list -> 'a * int
1.124 val max_vt : itm list -> int
1.125 - val mk_e : itm_ -> (Term.term * Term.term) list
1.126 - val mk_en : int -> itm -> (Term.term * Term.term) list
1.127 - val mk_env : itm list -> (Term.term * Term.term) list
1.128 - val mkval : 'a -> Term.term list -> Term.term
1.129 - val mkval' : Term.term list -> Term.term
1.130 + val mk_e : itm_ -> (term * term) list
1.131 + val mk_en : int -> itm -> (term * term) list
1.132 + val mk_env : itm list -> (term * term) list
1.133 + val mkval : 'a -> term list -> term
1.134 + val mkval' : term list -> term
1.135 (* val pblID_of_match : match -> pblID *)
1.136 - val pbl_ids : Theory.theory -> Term.term -> Term.term -> Term.term list
1.137 - val pbl_ids' : 'a -> Term.term -> Term.term list -> Term.term list
1.138 - (* val pen2str : Theory.theory -> Term.term * Term.term list -> string *)
1.139 - val penvval_in : itm_ -> Term.term list
1.140 + val pbl_ids : Proof.context -> term -> term -> term list
1.141 + val pbl_ids' : 'a -> term -> term list -> term list
1.142 + (* val pen2str : theory -> term * term list -> string *)
1.143 + val penvval_in : itm_ -> term list
1.144 val refined : match list -> pblID
1.145 val refined_ :
1.146 - match_ list -> match_ Library.option
1.147 + match_ list -> match_ option
1.148 (* val refined_IDitms :
1.149 - match list -> match Library.option *)
1.150 - val split_dts : 'a -> Term.term -> Term.term * Term.term list
1.151 - val split_dts' : Term.term * Term.term -> Term.term list
1.152 - (* val take_apart : Term.term -> Term.term list *)
1.153 - (* val take_apart_inv : Term.term list -> Term.term *)
1.154 - val ts_in : itm_ -> Term.term list
1.155 - (* val unique : Term.term *)
1.156 + match list -> match option *)
1.157 + val split_dts : 'a -> term -> term * term list
1.158 + val split_dts' : term * term -> term list
1.159 + (* val take_apart : term -> term list *)
1.160 + (* val take_apart_inv : term list -> term *)
1.161 + val ts_in : itm_ -> term list
1.162 + (* val unique : term *)
1.163 val untouched : itm list -> bool
1.164 val upd :
1.165 - Theory.theory ->
1.166 - (''a * (''b * Term.term list) list) list ->
1.167 - Term.term ->
1.168 - ''b * Term.term -> ''a -> ''a * (''b * Term.term list) list
1.169 + Proof.context ->
1.170 + (''a * (''b * term list) list) list ->
1.171 + term ->
1.172 + ''b * term -> ''a -> ''a * (''b * term list) list
1.173 val upd_envv :
1.174 - Theory.theory ->
1.175 + Proof.context ->
1.176 envv ->
1.177 vats ->
1.178 - Term.term -> Term.term -> Term.term -> envv
1.179 + term -> term -> term -> envv
1.180 val upd_penv :
1.181 - Theory.theory ->
1.182 - (''a * Term.term list) list ->
1.183 - Term.term -> ''a * Term.term -> (''a * Term.term list) list
1.184 + Proof.context ->
1.185 + (''a * term list) list ->
1.186 + term -> ''a * term -> (''a * term list) list
1.187 (* val upds_envv :
1.188 - Theory.theory ->
1.189 + Proof.context ->
1.190 envv ->
1.191 - (vats * Term.term * Term.term * Term.term) list ->
1.192 + (vats * term * term * term) list ->
1.193 envv *)
1.194 val vts_cnt : int list -> itm list -> (int * int) list
1.195 val vts_in : itm list -> int list
1.196 - (* val w_itms2str : Theory.theory -> itm list -> unit *)
1.197 + (* val w_itms2str_ : Proof.context -> itm list -> unit *)
1.198 end
1.199
1.200 (*----------------------------------------------------------*)
1.201 structure SpecifyTools : SPECIFY_TOOLS =
1.202 struct
1.203 (*----------------------------------------------------------*)
1.204 -val e_listReal = (term_of o the o (parse Script.thy)) "[]::(real list)";
1.205 -val e_listBool = (term_of o the o (parse Script.thy)) "[]::(bool list)";
1.206 +val e_listReal = (term_of o the o (parse (theory "Script"))) "[]::(real list)";
1.207 +val e_listBool = (term_of o the o (parse (theory "Script"))) "[]::(bool list)";
1.208
1.209 (*.take list-term apart w.r.t. handling elementwise input.*)
1.210 fun take_apart t =
1.211 @@ -197,18 +198,28 @@
1.212 WN050903 we do NOT know which is from subtheory, description or term;
1.213 typecheck thus may lead to TYPE-error 'unknown constant';
1.214 solution: typecheck with Isac.thy; i.e. arg 'thy' superfluous*)
1.215 -fun comp_dts thy (d,[]) =
1.216 - cterm_of ((sign_of o assoc_thy) "Isac.thy")
1.217 +(*fun comp_dts thy (d,[]) =
1.218 + cterm_of (*(sign_of o assoc_thy) "Isac.thy"*)
1.219 + (theory "Isac")
1.220 (*comp_dts:FIXXME stay with term for efficiency !!!*)
1.221 (if is_reall_dsc d then (d $ e_listReal)
1.222 else if is_booll_dsc d then (d $ e_listBool)
1.223 else d)
1.224 | comp_dts thy (d,ts) =
1.225 - (cterm_of ((sign_of o assoc_thy) "Isac.thy")
1.226 + (cterm_of (*(sign_of o assoc_thy) "Isac.thy"*)
1.227 + (theory "Isac")
1.228 (*comp_dts:FIXXME stay with term for efficiency !!*)
1.229 (d $ (comp_ts (d, ts)))
1.230 handle _ => raise error ("comp_dts: "^(term2str d)^
1.231 - " $ "^(term2str (hd ts))));
1.232 + " $ "^(term2str (hd ts))));*)
1.233 +fun comp_dts thy (d,[]) =
1.234 + (if is_reall_dsc d then (d $ e_listReal)
1.235 + else if is_booll_dsc d then (d $ e_listBool)
1.236 + else d)
1.237 + | comp_dts thy (d,ts) =
1.238 + (d $ (comp_ts (d, ts)))
1.239 + handle _ => raise error ("comp_dts: "^(term2str d)^
1.240 + " $ "^(term2str (hd ts)));
1.241 (*25.8.03*)
1.242 fun comp_dts' (d,[]) =
1.243 if is_reall_dsc d then (d $ e_listReal)
1.244 @@ -365,10 +376,10 @@
1.245 type penv = (term (*err_*)
1.246 * (term list) (*[#0, epsilon] 9.5.03 outcommented*)
1.247 ) list;
1.248 -fun pen2str thy (t, ts) =
1.249 - pair2str(Syntax.string_of_term GOON (sign_of thy) t,
1.250 - (strs2str' o map (Sign.string_of_term (sign_of thy))) ts);
1.251 -fun penv2str thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv;
1.252 +fun pen2str ctxt (t, ts) =
1.253 + pair2str(Syntax.string_of_term ctxt t,
1.254 + (strs2str' o map (Syntax.string_of_term ctxt)) ts);
1.255 +fun penv2str_ thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv;
1.256
1.257 (*
1.258 9.5.03: still unused, but left for eventual future development*)
1.259 @@ -388,7 +399,7 @@
1.260 fun getval (id, values) =
1.261 case values of
1.262 [] => raise error ("penv_value: no values in '"^
1.263 - (Sign.string_of_term (sign_of Tools.thy) id))
1.264 + (Syntax.string_of_term (thy2ctxt "Tools") id))
1.265 | [v] => (id, v)
1.266 | (v1::v2::_) => (case v1 of
1.267 Const ("Script.Arbfix",_) => (id, v2)
1.268 @@ -535,7 +546,7 @@
1.269 | mk_e (Sup _) = []
1.270 | mk_e (Mis _) = [];
1.271 fun mk_en vt ((i,vts,b,f,itm_):itm) =
1.272 - if vt mem vts then mk_e itm_ else [];
1.273 + if member op = vts vt then mk_e itm_ else [];
1.274 (*. extract the environment from an item list;
1.275 takes the variant with most items .*)
1.276 fun mk_env itms =
1.277 @@ -580,25 +591,24 @@
1.278 (*. given the input value (from split_dts)
1.279 make the value in a problem-env according to description-type .*)
1.280 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)
1.281 -(*9.5.03 penv-concept postponed *)
1.282 -fun pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v =
1.283 +fun pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v =
1.284 if is_list v
1.285 then [v] (*eg. [r=Arbfix]*)
1.286 else (case v of (*eg. eps=#0*)
1.287 (Const ("op =",_) $ l $ r) => [r,l]
1.288 | _ => raise error ("pbl_ids Tools.nam: no equality "
1.289 - ^(Sign.string_of_term (sign_of thy) v)))
1.290 - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v]
1.291 - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v]
1.292 - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v]
1.293 - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v]
1.294 - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v]
1.295 - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v]
1.296 - | pbl_ids thy _ v = raise error ("pbl_ids: not implemented for "
1.297 - ^(Sign.string_of_term (sign_of thy) v));
1.298 + ^(Syntax.string_of_term ctxt v)))
1.299 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v]
1.300 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v]
1.301 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v]
1.302 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v]
1.303 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v]
1.304 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v]
1.305 + | pbl_ids ctxt _ v = raise error ("pbl_ids: not implemented for "
1.306 + ^(Syntax.string_of_term ctxt v));
1.307 (*
1.308 val t as t1 $ t2 = str2term "antiDerivativeName M_b";
1.309 -pbl_ids thy t1 t2;
1.310 +pbl_ids ctxt t1 t2;
1.311
1.312 val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
1.313 val (d,argl) = strip_comb t;
1.314 @@ -606,7 +616,7 @@
1.315 dest_list (d,argl);
1.316 val (_ $ v) = t;
1.317 is_list v;
1.318 - pbl_ids thy d v;
1.319 + pbl_ids ctxt d v;
1.320 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
1.321 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
1.322
1.323 @@ -615,13 +625,13 @@
1.324 val vl = Free ("x","RealDef.real") : term
1.325
1.326 val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
1.327 - pbl_ids thy dsc vl;
1.328 + pbl_ids ctxt dsc vl;
1.329 val it = [Free ("x","RealDef.real")] : term list
1.330
1.331 val (dsc,vl) = (split_dts o term_of o the o(parse thy))
1.332 "errorBound (eps=#0)";
1.333 val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_";
1.334 - pbl_ids thy dsc vl;
1.335 + pbl_ids ctxt dsc vl;
1.336 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *)
1.337
1.338 (*. given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))
1.339 @@ -633,7 +643,7 @@
1.340 | [t] => (case t of (*eg. eps=#0*)
1.341 (Const ("op =",_) $ l $ r) => [r,l]
1.342 | _ => raise error ("pbl_ids' Tools.nam: no equality "
1.343 - ^(Sign.string_of_term (sign_of thy) t)))
1.344 + ^(Syntax.string_of_term (ctxt_Isac"")t)))
1.345 | vs' => vs (*14.9.01: ???TODO *))
1.346 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs
1.347 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs
1.348 @@ -650,11 +660,11 @@
1.349
1.350 (*14.9.01: not used after putting values for penv into itm_
1.351 WN.5.5.03: used in upd .. upd_envv*)
1.352 -fun upd_penv thy penv dsc (id, vl) =
1.353 +fun upd_penv ctxt penv dsc (id, vl) =
1.354 (writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
1.355 writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
1.356 writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
1.357 - overwrite (penv, (id, pbl_ids thy dsc vl))
1.358 + overwrite (penv, (id, pbl_ids ctxt dsc vl))
1.359 );
1.360 (*
1.361 val penv = [];
1.362 @@ -678,8 +688,8 @@
1.363 (*WN.9.5.03: not reconsidered; looks strange !!!*)
1.364 fun upd thy envv dsc (id, vl) i =
1.365 let val penv = case assoc (envv, i) of
1.366 - Some e => e
1.367 - | None => [];
1.368 + SOME e => e
1.369 + | NONE => [];
1.370 val penv' = upd_penv thy penv dsc (id, vl);
1.371 in (i, penv') end;
1.372 (*
1.373 @@ -699,7 +709,7 @@
1.374 if length envv = 0 then [1]
1.375 else (intsto o length) envv
1.376 else vats
1.377 - fun isin vats (i,_) = i mem vats;
1.378 + fun isin vats (i,_) = member op = vats i;
1.379 val envs_notin_vat = filter_out (isin vats) envv;
1.380 in ((map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat):envv end;
1.381 (*
1.382 @@ -777,32 +787,34 @@
1.383 | Incompl of cterm' (**)
1.384 | Superfl of string (**)
1.385 | Missing of cterm';
1.386 -fun item2str (Correct s) ="Correct "^s
1.387 - | item2str (SyntaxE s) ="SyntaxE "^s
1.388 - | item2str (TypeE s) ="TypeE "^s
1.389 - | item2str (False s) ="False "^s
1.390 - | item2str (Incompl s) ="Incompl "^s
1.391 - | item2str (Superfl s) ="Superfl "^s
1.392 - | item2str (Missing s) ="Missing "^s;
1.393 +fun item2str (Correct s) ="Correct " ^ s
1.394 + | item2str (SyntaxE s) ="SyntaxE " ^ s
1.395 + | item2str (TypeE s) ="TypeE " ^ s
1.396 + | item2str (False s) ="False " ^ s
1.397 + | item2str (Incompl s) ="Incompl " ^ s
1.398 + | item2str (Superfl s) ="Superfl " ^ s
1.399 + | item2str (Missing s) ="Missing " ^ s;
1.400 (*make string for error-msgs*)
1.401 -fun itm__2str thy (Cor ((d,ts), penv)) =
1.402 - "Cor " ^ string_of_cterm (comp_dts thy(d,ts)) ^" ,"^ pen2str thy penv
1.403 - | itm__2str thy (Syn c) = "Syn "^c
1.404 - | itm__2str thy (Typ c) = "Typ "^c
1.405 - | itm__2str thy (Inc ((d,ts), penv)) =
1.406 - "Inc " ^ string_of_cterm (comp_dts thy(d,ts)) ^" ,"^ pen2str thy penv
1.407 - | itm__2str thy (Sup (d,ts)) = "Sup "^(string_of_cterm (comp_dts thy(d,ts)))
1.408 - | itm__2str thy (Mis (d,pid))=
1.409 - "Mis "^ Sign.string_of_term (sign_of thy) d ^
1.410 - " "^ Sign.string_of_term (sign_of thy) pid
1.411 - | itm__2str thy (Par s) = "Trm "^s;
1.412 -fun itm_2str t = itm__2str (assoc_thy "Isac.thy") t;
1.413 -fun itm2str thy ((i,is,b,s,itm_):itm) =
1.414 +fun itm_2str_ ctxt (Cor ((d,ts), penv)) =
1.415 + "Cor " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) ^ " ,"
1.416 + ^ pen2str ctxt penv
1.417 + | itm_2str_ ctxt (Syn c) = "Syn " ^ c
1.418 + | itm_2str_ ctxt (Typ c) = "Typ " ^ c
1.419 + | itm_2str_ ctxt (Inc ((d,ts), penv)) =
1.420 + "Inc " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) ^ " ,"
1.421 + ^ pen2str ctxt penv
1.422 + | itm_2str_ ctxt (Sup (d,ts)) =
1.423 + "Sup " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts))
1.424 + | itm_2str_ ctxt (Mis (d,pid))=
1.425 + "Mis "^ Syntax.string_of_term ctxt d ^
1.426 + " "^ Syntax.string_of_term ctxt pid
1.427 + | itm_2str_ ctxt (Par s) = "Trm "^s;
1.428 +fun itm_2str t = itm_2str_ (thy2ctxt "Isac") t;
1.429 +fun itm2str_ ctxt ((i,is,b,s,itm_):itm) =
1.430 "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^
1.431 - s^" ,"^(itm__2str thy itm_)^")";
1.432 -val linefeed = (curry op^) "\n";
1.433 -fun itms2str thy itms = strs2str' (map (linefeed o (itm2str thy)) itms);
1.434 -fun w_itms2str thy itms = writeln (itms2str thy itms);
1.435 + s^" ,"^(itm_2str_ ctxt itm_)^")";
1.436 +fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
1.437 +fun w_itms2str_ ctxt itms = writeln (itms2str_ ctxt itms);
1.438
1.439 fun init_item str = SyntaxE str;
1.440
1.441 @@ -896,7 +908,7 @@
1.442 | ts_in (Mis _) = [];
1.443 (*WN050629 unused*)
1.444 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
1.445 -val unique = (term_of o the o (parse Real.thy)) "UnIqE_tErM";
1.446 +val unique = (term_of o the o (parse (theory "Real"))) "UnIqE_tErM";
1.447 fun d_in (Cor ((d,_),_)) = d
1.448 | d_in (Syn (c)) = (writeln("*** d_in: Syn ("^c^")"); unique)
1.449 | d_in (Typ (c)) = (writeln("*** d_in: Typ ("^c^")"); unique)
1.450 @@ -918,10 +930,10 @@
1.451 rls -> (*for eval_true*)
1.452 bool * (*have _all_ variables(Free) from the model-pattern
1.453 been substituted by a value from the pattern's environment ?*)
1.454 -Term.term (*the precondition*)
1.455 +term (*the precondition*)
1.456 ->
1.457 bool * (*has the precondition evaluated to true*)
1.458 -Term.term (*the precondition (for map)*)
1.459 +term (*the precondition (for map)*)
1.460 .*)
1.461 fun evalprecond prls (false, pre) =
1.462 (*NOT ALL Free's have been substituted, eg. because of incomplete model*)
1.463 @@ -969,9 +981,9 @@
1.464 fun cpy its [] (f, (d, id)) =
1.465 if length its = 0 (*no dsc found in pbl*)
1.466 then case find_first (vt_and_dsc d) oris
1.467 - of Some (i,v,_,_,ts) =>
1.468 + of SOME (i,v,_,_,ts) =>
1.469 [(i,v,true,f, Cor ((d,ts), (id,pbl_ids' thy d ts)))]
1.470 - | None => [(0,[],false,f,Mis (d, id))]
1.471 + | NONE => [(0,[],false,f,Mis (d, id))]
1.472 else its
1.473 | cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =
1.474 if d = d_in itm_ andalso i<>0 (*already touched by user*)
1.475 @@ -1018,7 +1030,7 @@
1.476 fun copy_pbl (pbl:itm list) met oris =
1.477 let fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;
1.478 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
1.479 - Some _ => false | None => true;
1.480 + SOME _ => false | NONE => true;
1.481 (*1*)val mis = ((map (cons2 (fst, fst o snd))) o (filter (notmem pbl))) met;
1.482
1.483 fun eqdsc_ori d ((_,_,_,d',_):ori) = d = d';