wneuper/isa: comparison src/Tools/isac/ME/calchead.sml

equal deleted inserted replaced

-:b65c6037eb6d
+:56f10b13005e
 991122
 (c) due to copyright terms
 use"ME/calchead.sml";
 use"calchead.sml";
+12345678901234567890123456789012345678901234567890123456789012345678901234567890
+10        20        30        40        50        60        70        80
 *)
 (* TODO interne Funktionen aus sig entfernen *)
 signature CALC_HEAD =
 sig
 SpecifyTools.ori list ->
 SpecifyTools.itm list ->
 (string * (Term.term * Term.term)) list -> cterm' -> additm
 type calcstate
 type calcstate'
-val chk_vars : Thm.cterm SpecifyTools.ppc -> string * Term.term list
+val chk_vars : term ppc -> string * Term.term list
 val chktyp :
-theory -> int * Thm.cterm list * Thm.cterm list -> Thm.cterm
+theory -> int * term list * term list -> term
 val chktyps :
-theory -> Thm.cterm list * Thm.cterm list -> Thm.cterm list
+theory -> term list * term list -> term list
 val complete_metitms :
 SpecifyTools.ori list ->
 SpecifyTools.itm list ->
 SpecifyTools.itm list -> pat list -> SpecifyTools.itm list
 val complete_mod_ : ori list * pat list * pat list * itm list ->
 cterm' * 'a ->
 int list * pos_ ->
 'b ->
 ptree ->
 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
-val tag_form : theory -> Thm.cterm * Thm.cterm -> Thm.cterm
+val tag_form : theory -> term * term -> term
 val test_types : theory -> Term.term * Term.term list -> string
 val typeless : Term.term -> Term.term
-val unbound_ppc : Thm.cterm SpecifyTools.ppc -> Term.term list
+val unbound_ppc : term SpecifyTools.ppc -> Term.term list
 val vals_of_oris : SpecifyTools.ori list -> Term.term list
 val variants_in : Term.term list -> int
 val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
 val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list
 end
 (*.to an input (d,ts) find the according ori and insert the ts.*)
 (*WN.11.03: + dont take first inter<>[]*)
 fun seek_oridts thy sel (d,ts) [] =
-("'"^(Syntax.string_of_term (thy2ctxt' thy) (comp_dts thy (d,ts)))^
+("'"^(Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))^
-(*"' not found (typed)", e_ori_:ori, [])          ///11.11.03*)
 "' not found (typed)", (0,[],sel,d,ts):ori, [])
 (* val (id,vat,sel',d',ts')::oris = ori;
 val (id,vat,sel',d',ts') = ori;
 *)
 | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
-if sel = sel' andalso d=d' andalso (ts inter ts') <> []
+if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
 then if sel = sel'
-	     then ("",(id,vat,sel,d, ts inter(*!overlap!*) ts'):ori, ts')
+	 then ("",
-	   else ((Syntax.string_of_term (thy2ctxt' thy) (comp_dts thy(d,ts)))^
+(id,vat,sel,d, inter op = ts ts'):ori,
-		 " not for "^sel, e_ori_, [])
+ts')
+	 else ((Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))
+^ " not for " ^ sel,
+e_ori_,
+[])
 else seek_oridts thy sel (d,ts) oris;
 (*.to an input (_,ts) find the according ori and insert the ts.*)
 fun seek_orits thy sel ts [] =
 ("'"^
-(strs2str (map (Syntax.string_of_term (thy2ctxt' thy)) ts))^
+(strs2str (map (Syntax.string_of_term (thy2ctxt thy)) ts))^
 "' not found (typed)", e_ori_, [])
 | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
-if sel = sel' andalso (ts inter ts') <> []
+if sel = sel' andalso (inter op = ts ts') <> []
 then if sel = sel'
-	   then ("",(id,vat,sel,d,ts inter(*!overlap!*) ts'):ori, ts')
+	   then ("",
-	   else (((strs2str' o map (Syntax.string_of_term (thy2ctxt' thy))) ts)^
+(id,vat,sel,d, inter op = ts ts'):ori,
-		 " not for "^sel, e_ori_, [])
+ts')
+	   else (((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
+^ " not for "^sel,
+e_ori_,
+[])
 else seek_orits thy sel ts oris;
 (* false
 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
 > seek_orits thy sel ts [(id,vat,sel',d,ts')];
 uncaught exception TYPE
 			     else ([n], x::xs);
 fun coll eq  xs [] = xs
 | coll eq  xs (y::ys) =
 let val (n,ys') = cnt eq (y::ys) y 0;
 in if ys' = [] then xs @ n else coll eq  (xs @ n) ys' end;
-val vts = (distinct (coll eq [] ts))\\[1];
+val vts = subtract op = [1] (distinct (coll eq [] ts));
 in case vts of [] => 1 | [n] => n
 | _ => error "different variants in formalization" end;
 (*
 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
 val it = ([3],[4,5,5,5,5,5]) : int list * int list
 val it = true : bool
 > val (SOME ct) = parse thy "[lll::real]";
 > has_list_type (term_of ct);
 val it = false : bool *)
-(*fdcrs = descriptions in formalization
-unused 22.11.00
-fun is_already_input thy fdcrs ts t =
-let
-val tss = flat (map isalist2list ts);
-(*28.1.     val (dcr,t') = split_dsc_t fdcrs t; *)
-val (dcr,[t']) = split_dts t;
-in if (typeless t') mem (map typeless tss)
-then ("term '"^(Syntax.string_of_term (thy2ctxt' thy) t')^
-		  "' already input")
-	  else "" end;
-> val pts = appc (map (term_of o the o (parse thy))) pbl;
-> val ts = #Relate pts;
-> val t = (term_of o the o (parse thy))"(A=#2*a*b - a^^^#2)";
-> is_already_input thy ts t;
-val it = "term 'A = #2 * a * b - a ^^^ #2' already input" : string
-> val t = (term_of o the o (parse thy))"a=#2*R*sin alpha";
-> is_already_input thy ts t;
-val it = "term 'a = #2 * R * sin alpha' already input" : string
-> val t = (term_of o the o (parse thy))"a=R*sin alpha";
-> is_already_input thy ts t;
-val it = "" : string
-*)
 fun is_parsed (Syn _) = false
 | is_parsed _ = true;
 fun parse_ok its = foldl and_ (true, map is_parsed its);
 fun all_dsc_in itm_s =
 (*.get the first term in ts from ori.*)
 (* val (_,_,fd,d,ts) = hd miss;
 *)
 fun getr_ct thy ((_,_,fd,d,ts):ori) =
-(fd, (string_of_cterm o (comp_dts thy)) (d,[hd ts]):cterm');
+(fd, ((Syntax.string_of_term (thy2ctxt thy)) o
+(comp_dts thy)) (d,[hd ts]):cterm');
 (* val t = comp_dts thy (d,[hd ts]);
 *)
 (* get a term from ori, notyet input in itm *)
 fun geti_ct thy ((_,_,_,d,ts):ori) ((_,_,_,fd,itm_):itm) =
-(fd, (string_of_cterm o (comp_dts thy)) (d,ts \\ (ts_in itm_)):cterm');
+(fd, ((Syntax.string_of_term (thy2ctxt thy)) o (comp_dts thy))
+(d, subtract op = (ts_in itm_) ts):cterm');
 (* test-maximum.sml fmy <> [], Init_Proof ...
 val (_,_,_,d,ts) = ori; val (_,_,_,fd,itm_) = hd icl;
 val d' $ ts' = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
 atomty d;
 atomty d';
 atomty (hd ts);
 atomty ts';
-cterm_of (sign_of thy) (d $ (hd ts));
+Thm.cterm_of thy (d $ (hd ts));
-cterm_of (sign_of thy) (d' $ ts');
+Thm.cterm_of thy (d' $ ts');
 comp_dts thy (d,ts);
 *)
 | is_untouched _ = false;
 (* select an item in oris, notyet input in itms
 (precondition: in itms are only Cor, Sup, Inc) *)
+local
+infix mem;
+fun x mem [] = false
+| x mem (y :: ys) = x = y orelse x mem ys;
+in
 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
 let
 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
 fun is_elem itms (f,(d,t)) =
 case find_first (test_d d) itms of
 	SOME _ => true | NONE => false;
 in case filter_out (is_elem itms) pbt of
 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
 *)
 (f,(d,_))::itms =>
-SOME (f:string, (string_of_cterm o comp_dts thy) (d,[]):cterm')
+SOME (f:string, ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts thy) (d,[]):cterm')
 | _ => NONE end
 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
 *)
 | nxt_add thy oris pbt itms =
 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
 (* val itm = hd icl; val (_,_,_,d,ts) = v6;
 *)
 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
-	(d_in (#5 itm)) = d andalso (ts_in (#5 itm)) subset ts;
+	(d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
 | false_and_not_Sup (i,v,false,f, _) = true
 | false_and_not_Sup  _ = false;
 val v = if itms = [] then 1 else max_vt itms;
 	 case find_first (test_subset (hd icl)) vors of
 	     (* val SOME ori = find_first (test_subset (hd icl)) vors;
 	      *)
 	     NONE => raise error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
 	   | SOME ori => SOME (geti_ct thy ori (hd icl))
-end;
+end
+end;
 fun mk_delete thy "#Given"  itm_ = Del_Given   (itm_out thy itm_)
 | mk_delete thy "#Find"   itm_ = Del_Find    (itm_out thy itm_)
 (*3.3.--
 fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) =
 (id,vt,cl,sl,Cor (d,ts)):itm
 | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) =
-raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^
+raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
 	       " not not for Syn (s:cterm')")
 | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) =
-raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^
+raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
 	       " not not for Typ (s:cterm')")
 | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) =
 (id,vt,cl,sl,Fal (d,ts))
 | update_itm (cl,d,ts) (id,vt,_,sl,Inc (_,_)) =
 (id,vt,cl,sl,Inc (d,ts))
 fun is_field_correct sel d dscpbt =
 case assoc (dscpbt, sel) of
 NONE => false
-| SOME ds => d mem ds;
+| SOME ds => member op = ds d;
 (*. update the itm_ already input, all..from ori .*)
 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
 *)
 fun ori_2itm thy itm_ pid all ((id,vt,fd,d,ts):ori) =
 let
 val ts' = union op = (ts_in itm_) ts;
 val pval = pbl_ids' thy d ts'
 	(*WN.9.5.03: FIXXXME [#0, epsilon]
 	  here would upd_penv be called for [#0, epsilon] etc. *)
-val complete = if eq_set (ts', all) then true else false;
+val complete = if eq_set op = (ts', all) then true else false;
 in case itm_ of
 (Cor _) =>
 	(if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
 	 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
 | (Syn c)     => raise error ("ori_2itm wants to overwrite "^c)
 val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
 			   *)
 (case find_first (eq3 f d) itms of
 	   SOME (_,_,_,_,itm_) =>
 	   let
-	       val ts' = (ts_in itm_) inter ts;
+	       val ts' = inter op = (ts_in itm_) ts;
-	   in if ts subset ts'
+	   in if subset op = (ts, ts')
 	      then (((strs2str' o
-		      map (Syntax.string_of_term (thy2ctxt' thy))) ts')^
+		      map (Syntax.string_of_term (thy2ctxt thy))) ts')^
 		    " already input", e_itm)                            (*2*)
-	      else ("", ori_2itm thy itm_ pid all (i,v,f,d,ts\\ts'))    (*3,4*)
+	      else ("",
+ori_2itm thy itm_ pid all (i,v,f,d,
+subtract op = ts' ts))   (*3,4*)
 	   end
 	 | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
 				 pid all (i,v,f,d,ts))                  (*1*)
 	)
 | NONE => ("", ori_2itm thy (Sup (d,ts))
 			      e_term all (i,v,f,d,ts));
-(*------------------------------------------------
-fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
-fun is_notyet_input thy itms pval all ((id,vt,fd,d,ts):ori) pbt =
-case find_first (eq1 d) pbt of
-SOME (_,(_,pid)) => (* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
-*)
-(case seek_ppc id itms of
-	   SOME (id',_,_,_,itm_) =>
-	   let
-	       val ts' = (ts_in itm_) inter ts;
-	   in if ts'= [] then ("", ori_2itm itm_ (pid, pval) all
-					    (id,vt,fd,d,(ts_in itm_)@ts))
-	      else (((strs2str' o
-		      map (Syntax.string_of_term (thy2ctxt' thy))) ts')^
-		    " already input", e_itm) end
-	 | NONE =>
-	   if all = ts
-	   then ("", ori_2itm (Cor ((e_term,[]),(pid,[])))
-			      (pid, pval) all (id,vt,fd,d,ts))
-	   else ("", ori_2itm (Inc ((e_term,[]),(e_term,[])))
-			      (pid, pval) all (id,vt,fd,d,ts))
-	)
-| NONE => ("", ori_2itm (Sup (e_term,[]))
-			      (e_term, []) all (id,vt,fd,d,ts));----*)
 fun test_types thy (d,ts) =
 let
 val s = !show_types; val _ = show_types:= true;
 val opt = (try (comp_dts thy)) (d,ts);
 val msg = case opt of
 SOME _ => ""
-| NONE => ((Sign.string_of_term  (sign_of thy) d)^" "^
+| NONE => ((Syntax.string_of_term (thy2ctxt thy) d)^" "^
-	     ((strs2str' o map (Sign.string_of_term(sign_of thy)))ts)
+	     ((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
-	     ^" is illtyped");
+	     ^ " is illtyped");
 val _ = show_types:= s
 in msg end;
 val oids = ((map (fst o dest_Free)) o distinct o
 		flat o (map vars)) ots;
 val (d,ts(*,pval*)) = split_dts thy t;
 val ids = map (fst o dest_Free)
 ((distinct o (flat o (map vars))) ts);
-in if (ids \\ oids) <> []
+in if (subtract op = oids ids) <> []
-then (("identifiers "^(strs2str' (ids \\ oids))^
+then (("identifiers "^(strs2str' (subtract op = oids ids))^
 	    " not in example"), e_ori_, [])
 else
 	 if d = e_term
 	 then
-	     if not ((map typeless ts) subset (map typeless ots))
+	     if not (subset op = (map typeless ts, map typeless ots))
 	     then (("terms '"^
-		    ((strs2str' o (map (Sign.string_of_term
+		    ((strs2str' o (map (Syntax.string_of_term
-					    (sign_of thy)))) ts)^
+					    (thy2ctxt thy)))) ts)^
 		    "' not in example (typeless)"), e_ori_, [])
 	     else (case seek_orits thy sel ts ori of
 		       ("", ori_ as (_,_,_,d,ts), all) =>
 		       (case test_types thy (d,ts) of
 			    "" => ("", ori_, all)
 			  | msg => (msg, e_ori_, []))
 		     | (msg,_,_) => (msg, e_ori_, []))
 	 else
-	     if d mem (map #4 ori)
+	     if member op = (map #4 ori) d
 	     then seek_oridts thy sel (d,ts) ori
-	     else ((Syntax.string_of_term (thy2ctxt' thy) d)^
+	     else ((Syntax.string_of_term (thy2ctxt thy) d)^
 		   (*" not in example", e_ori_, []) ///11.11.03*)
 		   " not in example", (0,[],sel,d,ts), [])
 end;
 (*.split type-wrapper from scr-arg and build part of an ori;
 an type-error is reported immediately, raises an exn,
 subsequent handling of exn provides 2nd part of error message.*)
-fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
+(*fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =   WN100820 made cterm to term
 (* val (thy, (str, (dsc, _)), (ty $ var)) =
 	   (thy,  p,               a);
 *)
-(cterm_of (sign_of thy) (dsc $ var);(*type check*)
+(Thm.cterm_of thy (dsc $ var);(*type check*)
 SOME ((([1], str, dsc, (*[var]*)
 	    split_dts' (dsc, var))): preori)(*:ori without leading #*))
 handle e  as TYPE _ =>
 	   (writeln (dashs 70^"\n"
 		      ^"*** ERROR while creating the items for the model of the ->problem\n"
 		      ^"*** value: "^(term_detail2str var)
 		      ^"*** typeconstructor in script: "^(term_detail2str ty)
 		      ^"*** checked by theory: "^(theory2str thy)^"\n"
 		      ^"*** "^dots 66);
 	     print_exn e; (*raises exn again*)
+	    NONE);*)
+fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
+(* val (thy, (str, (dsc, _)), (ty $ var)) =
+	   (thy,  p,               a);
+*)
+(Thm.cterm_of thy (dsc $ var);(*type check*)
+SOME ((([1], str, dsc, (*[var]*)
+	    split_dts' (dsc, var))): preori)(*:ori without leading #*))
+handle e  as TYPE _ =>
+	   (writeln (dashs 70^"\n"
+		      ^"*** ERROR while creating the items for the model of the ->problem\n"
+		      ^"*** from the ->stac with ->typeconstructor in arglist:\n"
+		      ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
+		      ^"*** description: "^(term_detail2str dsc)
+		      ^"*** value: "^(term_detail2str var)
+		      ^"*** typeconstructor in script: "^(term_detail2str ty)
+		      ^"*** checked by theory: "^(theory2str thy)^"\n"
+		      ^"*** "^dots 66);
+	    (*WN100820 postponed: print_exn e; raises exn again*)
 	    NONE);
 (*> val pbt = (#ppc o get_pbt) ["univariate","equation"];
 > val Const ("Script.SubProblem",_) $
 	  (Const ("Pair",_) $ Free (thy', _) $
 		 (Const ("Pair",_) $ pblID' $ metID')) $ ags =
 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
 fun overwrite_ppc thy itm ppc =
 let
 fun repl ppc' (_,_,_,_,itm_) [] =
-raise error ("overwrite_ppc: "^(itm__2str thy itm_)^" not found")
+raise error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
+" not found")
 | repl ppc' itm (p::ppc) =
 	if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
 	else repl (ppc' @ [p]) itm ppc
 in repl [] itm ppc end;
 	     | pos => raise error ("header called with "^ pos_2str pos);
 (* test-printouts ---
-val _=writeln("### insert_ppc: (d,ts)="^(string_of_cterm(comp_dts thy(d,ts))));
+val _=writeln("### insert_ppc: (d,ts)="^((Syntax.string_of_term (thy2ctxt thy))(comp_dts thy(d,ts))));
 val _=writeln("### insert_ppc: pts= "^
-(strs2str' o map (Syntax.string_of_term (thy2ctxt' thy))) pts);
+(strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) pts);
 val sel = "#Given"; val Add_Given' ct = m;
 val sel = "#Find"; val Add_Find' (ct,_) = m;
 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
 let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
 		   meth=met, ...}) = get_obj I pt p;
 (*val pt = update_pbl pt p itms;
 val pt = update_pblID pt p pI;*)
+val thy = assoc_thy dI
 val ((p,Pbl),_,_,pt)=
 	generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
 val mI'' = if mI=e_metID then mI' else mI;
 (*val _=writeln("@@@ specify (Specify_Problem) before nxt_spec")*)
 	 | Err msg =>
 	   (*TODO.WN03 pass error-msgs to the frontend..
 FIXME ..and dont abuse a tactic for that purpose*)
 	   ([(Tac msg,
-	      Tac_ (ProtoPure.thy, msg,msg,msg),
+	      Tac_ (theory "Pure", msg,msg,msg),
 	      (e_pos', e_istate))], [], ptp)
 end
 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
 val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
 | filter_outs oris (i::itms) =
 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
 			      (#4:ori -> term)) oris;
 in filter_outs ors itms end;
-fun memI a b = b mem a;
+fun memI a b = member op = a b;
 (*filter oris which are in pbt, too*)
 fun filter_pbt oris pbt =
 let val dscs = map (fst o snd) pbt
 in filter ((memI dscs) o (#4: ori -> term)) oris end;
 (*.combine itms from pbl + met and complete them wrt. pbt.*)
 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
+local
+infix mem;
+fun x mem [] = false
+| x mem (y :: ys) = x = y orelse x mem ys;
+in
 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
 *)
 let val vat = max_vt pits;
 val itms = pits @
 		   (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
 	val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
 val os = filter_outs ors itms;
 (*WN.12.03?: does _NOT_ add itms from met ?!*)
-in itms @ (map (ori2Coritm met) os) end;
+in itms @ (map (ori2Coritm met) os) end
+end;
 (*.complete model and guard of a calc-head .*)
+local
+infix mem;
+fun x mem [] = false
+| x mem (y :: ys) = x = y orelse x mem ys;
+in
 fun complete_mod_ (oris, mpc, ppc, probl) =
 let	val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
 	val vat = if probl = [] then 1 else max_vt probl
 	val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
 	val pors = filter_outs pors pits (*which are in pbl already*)
 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
 	val pits = pits @ (map (ori2Coritm ppc) pors)
 	val mits = complete_metitms oris pits [] mpc
-in (pits, mits) end;
+in (pits, mits) end
+end;
 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
 (if dI = e_domID then odI else dI,
 if pI = e_pblID then opI else pI,
 if mI = e_metID then omI else mI):spec;
 (*WN.24.10.03        fun nxt_solv   = ...................................??*)
 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
 let
 val (PblObj{origin=(oris,ospec,_),probl,spec,...}) = get_obj I pt p
 val (dI,pI,mI) = some_spec ospec spec
+val thy = assoc_thy dI
 val mpc = (#ppc o get_met) mI (*just for reuse complete_mod_*)
 val {cas,ppc,...} = get_pbt pI
 val pbl = init_pbl ppc (*fill in descriptions*)
 (*--------------if you think, this should be done by the Dialog
 in the java front-end, search there for WN060225-modelProblem----*)
 	   SOME pI' =>
 	   let val {met,ppc,...} = get_pbt pI'
 	       val pbl = init_pbl ppc
 	       (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
 	       val mI = if length met = 0 then e_metID else hd met
+val thy = assoc_thy dI
 	       val (pos,c,_,pt) =
 		   generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
 			     Uistate pos pt
 	   in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
 		 (pos, Uistate))], c, (pt,pos)) end
 | nxt_specif m' _ =
 raise error ("nxt_specif: not impl. for "^tac2str m');
 (*.get the values from oris; handle the term list w.r.t. penv.*)
+local
+infix mem;
+fun x mem [] = false
+| x mem (y :: ys) = x = y orelse x mem ys;
+in
 fun vals_of_oris oris =
 ((map (mkval' o (#5:ori -> term list))) o
-(filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris;
+(filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
+end;
 (*.create a calc-tree with oris via an cas.refined pbl.*)
 fun nxt_specify_init_calc (([],(dI,pI,mI)): fmz) =
 | Appl =>
 *)    let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
 in f end;
+(*fun tag_form thy (formal, given) = Thm.cterm_of thy
+	      (((head_of o term_of) given) $ (term_of formal)); WN100819*)
+fun tag_form thy (formal, given) =
+(let val gf = (head_of given) $ formal;
-(* --------------------- ME --------------------- *)
+val _ = Thm.cterm_of thy gf
-fun tag_form thy (formal, given) = cterm_of (sign_of thy)
+in gf end)
-	      (((head_of o term_of) given) $ (term_of formal));
+handle _ => raise error ("calchead.tag_form: " ^
+Syntax.string_of_term (thy2ctxt thy) given ^
+" .. " ^
+Syntax.string_of_term (thy2ctxt thy) formal ^
+" ..types do not match");
 (* val formal = (the o (parse thy)) "[R::real]";
 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
 > tag_form thy (formal, given);
 val it = "fixed_values [R]" : cterm
 *)
 fun chktyp thy (n, fs, gs) =
-((writeln o string_of_cterm o (nth n)) fs;
+((writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) fs;
-(writeln o string_of_cterm o (nth n)) gs;
+(writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) gs;
 tag_form thy (nth n fs, nth n gs));
 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
 (* #####################################################
 else if (re\\(gi union fi)) <> []
 	    then ("re\\(gi union fi)",re\\(gi union fi))
 	  else ("ok",[]) end;*)
 fun chk_vars ctppc =
 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
-appc flat (mappc (vars o term_of) ctppc)
+appc flat (mappc vars ctppc)
 val chked = subtract op = gi wh
 in if chked <> [] then ("wh\\gi", chked)
 else let val chked = subtract op = (union op = gi fi) re
 in if chked  <> []
 	     then ("re\\(gi union fi)", chked)
 end;
 (* check a new pbltype: variables (Free) unbound by given, find*)
 fun unbound_ppc ctppc =
 let val {Given=gi,Find=fi,Relate=re,...} =
-appc flat (mappc (vars o term_of) ctppc)
+appc flat (mappc vars ctppc)
 in distinct (*re\\(gi union fi)*)
 (subtract op = (union op = gi fi) re) end;
 (*
 > val org = {Given=["[R=(R::real)]"],Where=[],
 	   Find=["[A::real]"],With=[],
 | fld f (x::x'::[]) = f (x',x)
 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
 in ((fld f) o rev) xs end;
 (*
 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
-> val ces = map (cterm_of (sign_of thy)) (isalist2list (term_of ct));
+> val ces = map (Thm.cterm_of thy) (isalist2list (term_of ct));
 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
-> cterm_of (sign_of thy) conj;
+> Thm.cterm_of thy conj;
 val it = "(a = b & c = d) & e = f" : cterm
 *)
 (* f, a binary operator, is nested leftassociative *)
 fun foldl1 f (x::[]) = x
 | foldl1 f (x::x'::[]) = f (x,x')
 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
 (*
 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
-> val ces = map (cterm_of (sign_of thy)) (isalist2list (term_of ct));
+> val ces = map (Thm.cterm_of thy) (isalist2list (term_of ct));
 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
-> cterm_of (sign_of thy) conj;
+> Thm.cterm_of thy conj;
 val it = "a = b & c = d & e = f & g = h" : cterm
 *)
 (* called only once, if a Subproblem has been located in the script*)
 > nxt_model_pbl mst;
 val it = Refine_Tacitly ["univariate","equation"] : tac
 *)
 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
-fun eq4 v (_,vts,_,_,_) = v mem vts;
+fun eq4 v (_,vts,_,_,_) = member op = vts v;
-(*((curry (op mem)) (vat:int)) o (#2:ori -> int list);*)
 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
 (*

branch	isac-update-Isa09-2
changeset 37934	56f10b13005e
parent 37932	722c19bfb6ba
child 37936	8de0b6207074