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

equal deleted inserted replaced

-:2d12beb7f983
+:722c19bfb6ba
 (*.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) [] =
-("'"^(string_of_cterm (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') <> []
 then if sel = sel'
 	     then ("",(id,vat,sel,d, ts inter(*!overlap!*) ts'):ori, ts')
-	   else ((string_of_cterm (comp_dts thy(d,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;
-(*FIXXXME.WN.11.03: + dont take first inter<>[] .. ev. variants are following:
-thus take largest intersection !!!
-if sel NOTok .. then the correct itm should NOT be overwritten by insert_ppc*)
-(*fun eq7 d (_,_,_,d',_) = d = d';
-fun inter_length ((_,_,_,_,ts), (_,_,_,_,ts')) = (length ts) < (length ts');
-fun seek_oridts _ sel (d,ts) [] =
-("'"^(string_of_cterm (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 _ sel (d,ts) oris =
-let val dscOK = filter (eq7 d) oris;
-in if dscOK = [] then ("'"^(string_of_cterm (comp_dts thy (d,ts)))^
-			   "' not found (typed)", (0,[],sel,d,ts):ori, [])
-else let val (id,vat,sel',d',ts') = gen_max inter_length dscOK;
-	    in if sel = sel' then ("",(id,vat,sel,d,ts inter ts'), [])
-	       else ("wrong field",(id,vat,sel,d,ts inter ts'), []) end
-end;
---------------------didnt work with Add_Given/_Find/_Relation 11.03*)
 (*.to an input (_,ts) find the according ori and insert the ts.*)
 fun seek_orits thy sel ts [] =
 ("'"^
-(strs2str (map (Sign.string_of_term (sign_of 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') <> []
 then if sel = sel'
 	   then ("",(id,vat,sel,d,ts inter(*!overlap!*) ts'):ori, ts')
-	   else (((strs2str' o map (Sign.string_of_term (sign_of thy))) 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')];
 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 '"^(Sign.string_of_term (sign_of thy) t')^
+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;
 	   SOME (_,_,_,_,itm_) =>
 	   let
 	       val ts' = (ts_in itm_) inter ts;
 	   in if ts subset ts'
 	      then (((strs2str' o
-		      map (Sign.string_of_term (sign_of 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*)
 	   end
 	 | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
 				 pid all (i,v,f,d,ts))                  (*1*)
 	   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 (Sign.string_of_term (sign_of thy))) ts')^
+		      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))
 			  | msg => (msg, e_ori_, []))
 		     | (msg,_,_) => (msg, e_ori_, []))
 	 else
 	     if d mem (map #4 ori)
 	     then seek_oridts thy sel (d,ts) ori
-	     else ((Sign.string_of_term (sign_of 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;
 (* test-printouts ---
 val _=writeln("### insert_ppc: (d,ts)="^(string_of_cterm(comp_dts thy(d,ts))));
 val _=writeln("### insert_ppc: pts= "^
-(strs2str' o map (Sign.string_of_term (sign_of 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;
 	    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)
-in let val chked = subtract op = gi wh
+val chked = subtract op = gi wh
-if chked <> [] then ("wh\\gi", chked)
+in if chked <> [] then ("wh\\gi", chked)
 else let val chked = subtract op = (union op = gi fi) re
-if chked  <> []
+in if chked  <> []
-	    then ("re\\(gi union fi)", chked)
+	     then ("re\\(gi union fi)", chked)
-	  else ("ok", []) end;
+	     else ("ok", [])
+end
+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)

branch	isac-update-Isa09-2
changeset 37932	722c19bfb6ba
parent 37931	2d12beb7f983
child 37934	56f10b13005e