# HG changeset patch # User Walther Neuper # Date 1282224962 -7200 # Node ID 722c19bfb6bab554de88fb4bcc7003897c4e9ad3 # Parent 2d12beb7f983eff1fe32711ddadde4ad24352e23 cleanup diff -r 2d12beb7f983 -r 722c19bfb6ba src/Tools/isac/Isac_Mathengine.thy --- a/src/Tools/isac/Isac_Mathengine.thy Thu Aug 19 15:20:53 2010 +0200 +++ b/src/Tools/isac/Isac_Mathengine.thy Thu Aug 19 15:36:02 2010 +0200 @@ -37,12 +37,13 @@ use "ME/ptyps.sml" use "ME/generate.sml" +use "ME/calchead.sml" + ML {* SOME 111; *} (* -use "ME/calchead.sml" use "ME/appl.sml" use "ME/rewtools.sml" use "ME/script.sml" diff -r 2d12beb7f983 -r 722c19bfb6ba src/Tools/isac/ME/calchead.sml --- a/src/Tools/isac/ME/calchead.sml Thu Aug 19 15:20:53 2010 +0200 +++ b/src/Tools/isac/ME/calchead.sml Thu Aug 19 15:36:02 2010 +0200 @@ -279,7 +279,7 @@ (*.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; @@ -289,42 +289,20 @@ 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 @@ -430,7 +408,7 @@ (*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; @@ -799,7 +777,7 @@ 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 @@ -821,7 +799,7 @@ 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 @@ -888,7 +866,7 @@ 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; @@ -1210,7 +1188,7 @@ (* 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; @@ -1867,12 +1845,14 @@ 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 - if chked <> [] then ("wh\\gi", chked) + val chked = subtract op = gi wh + in if chked <> [] then ("wh\\gi", chked) else let val chked = subtract op = (union op = gi fi) re - if chked <> [] - then ("re\\(gi union fi)", chked) - else ("ok", []) end; + in if chked <> [] + then ("re\\(gi union fi)", chked) + else ("ok", []) + end + end; (* check a new pbltype: variables (Free) unbound by given, find*) fun unbound_ppc ctppc =