# HG changeset patch # User Walther Neuper # Date 1298313636 -3600 # Node ID 69364e021751b1d3f7df71a1b697901f3eff1d71 # Parent 7f4cfec6b91094762c0be01caa04c2c4a5a05b71 part.update Isabelle2011 works neither on 2009-2 nor on 2011 diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Frontend/interface.sml --- a/src/Tools/isac/Frontend/interface.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Frontend/interface.sml Mon Feb 21 19:40:36 2011 +0100 @@ -69,7 +69,7 @@ let fun enc [] = [] | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs) | enc (c :: cs) = c :: (enc cs) - in (implode o enc o explode) str:cterm' end; + in (implode o enc o Symbol.explode) str:cterm' end; fun encode_imodel (imodel:imodel) = let fun enc (Given ifos) = Given (map encode ifos) | enc (Find ifos) = Find (map encode ifos) @@ -402,7 +402,7 @@ (*.set the context determined on a knowledgebrowser to the current calc.*) fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) = - (case (implode o (take_fromto 1 4) o explode) guh of + (case (implode o (take_fromto 1 4) o Symbol.explode) guh of "thy_" => (* val (cI, ip as (_,p_), guh) = (1, p, "thy_isac_Test-rls-Test_simplify"); *) @@ -775,7 +775,7 @@ (1, ([1], Res), "thy_isac_Test-rls-Test_simplify"); *) fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) = - (case (implode o (take_fromto 1 4) o explode) guh of + (case (implode o (take_fromto 1 4) o Symbol.explode) guh of "thy_" => if member op = [Pbl,Met] p_ then message2xml cI "thy-context not to calchead" diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Interpret/appl.sml --- a/src/Tools/isac/Interpret/appl.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Interpret/appl.sml Mon Feb 21 19:40:36 2011 +0100 @@ -207,7 +207,7 @@ let fun scan s' [] = (implode s', "") | scan s' (s::ss) = if s=" " then (implode s', implode ss) else scan (s'@[s]) ss; -in ((scan []) o explode) str end; +in ((scan []) o Symbol.explode) str end; (* split_dummy "subproblem_equation_dummy (x=-#5//#12)"; val it = ("subproblem_equation_dummy","(x=-#5//#12)") : string * string > split_dummy "x=-#5//#12"; diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Interpret/calchead.sml --- a/src/Tools/isac/Interpret/calchead.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Feb 21 19:40:36 2011 +0100 @@ -850,17 +850,17 @@ (*.can this formal argument (of a model-pattern) be omitted in the arg-list of a SubProblem ? see ME/ptyps.sml 'type met '.*) fun is_copy_named_idstr str = - case (rev o explode) str of - "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o explode)) + case (rev o Symbol.explode) str of + "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " T"); true) - | _ => (tracing ((strs2str o (rev o explode)) + | _ => (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " F"); false); fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t; (*.should this formal argument (of a model-pattern) create a new identifier?.*) fun is_copy_named_generating_idstr str = if is_copy_named_idstr str - then case (rev o explode) str of + then case (rev o Symbol.explode) str of "'"::"'"::"'"::_ => false | _ => true else false; @@ -934,8 +934,8 @@ (if is_copy_named_generating p then (*WN051014 kept strange old code ...*) let fun sel (_,_,d,ts) = comp_ts (d, ts) - val cy' = (implode o (drop_last_n 3) o explode o free2str) t - val ext = (last_elem o drop_last o explode o free2str) t + val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t + val ext = (last_elem o drop_last o Symbol.explode o free2str) t val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*) val vals = map sel oris val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext @@ -1334,7 +1334,7 @@ (*TODO.WN03 pass error-msgs to the frontend.. FIXME ..and dont abuse a tactic for that purpose*) ([(Tac msg, - Tac_ (theory "Pure", msg,msg,msg), + Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg), (e_pos', e_istate))], [], ptp) end diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Interpret/inform.sml --- a/src/Tools/isac/Interpret/inform.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Interpret/inform.sml Mon Feb 21 19:40:36 2011 +0100 @@ -219,7 +219,7 @@ in SOME (pt, (true, Met, hdt, mits, pre, spec):ocalhd) end end; -(*lazy evaluation for (theory "Isac")*) +(*lazy evaluation for (Thy_Info.get_theory "Isac")*) fun Isac _ = assoc_thy "Isac"; (*re-parse itms with a new thy and prepare for checking with ori list*) diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Interpret/mstools.sml --- a/src/Tools/isac/Interpret/mstools.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Interpret/mstools.sml Mon Feb 21 19:40:36 2011 +0100 @@ -158,8 +158,8 @@ structure SpecifyTools : SPECIFY_TOOLS = struct (*----------------------------------------------------------*) -val e_listReal = (term_of o the o (parse (theory "Script"))) "[]::(real list)"; -val e_listBool = (term_of o the o (parse (theory "Script"))) "[]::(bool list)"; +val e_listReal = (term_of o the o (parse (Thy_Info.get_theory "Script"))) "[]::(real list)"; +val e_listBool = (term_of o the o (parse (Thy_Info.get_theory "Script"))) "[]::(bool list)"; (*.take list-term apart w.r.t. handling elementwise input.*) fun take_apart t = @@ -197,17 +197,17 @@ (*.revert split_. WN050903 we do NOT know which is from subtheory, description or term; typecheck thus may lead to TYPE-error 'unknown constant'; - solution: typecheck with (theory "Isac"); i.e. arg 'thy' superfluous*) + solution: typecheck with (Thy_Info.get_theory "Isac"); i.e. arg 'thy' superfluous*) (*fun comp_dts thy (d,[]) = cterm_of (*(sign_of o assoc_thy) "Isac"*) - (theory "Isac") + (Thy_Info.get_theory "Isac") (*comp_dts:FIXXME stay with term for efficiency !!!*) (if is_reall_dsc d then (d $ e_listReal) else if is_booll_dsc d then (d $ e_listBool) else d) | comp_dts thy (d,ts) = (cterm_of (*(sign_of o assoc_thy) "Isac"*) - (theory "Isac") + (Thy_Info.get_theory "Isac") (*comp_dts:FIXXME stay with term for efficiency !!*) (d $ (comp_ts (d, ts))) handle _ => error ("comp_dts: "^(term2str d)^ @@ -301,7 +301,7 @@ fun dest_list' t = if is_list t then isalist2list t else [t]; (*fun is_metavar (Free (str, _)) = - if (last_elem o explode) str = "_" then true else false + if (last_elem o Symbol.explode) str = "_" then true else false | is_metavar _ = false;*) fun is_var (Free _) = true | is_var _ = false; @@ -909,7 +909,7 @@ | ts_in (Mis _) = []; (*WN050629 unused*) fun all_ts_in itm_s = (flat o (map ts_in)) itm_s; -val unique = (term_of o the o (parse (theory "Real"))) "UnIqE_tErM"; +val unique = (term_of o the o (parse (Thy_Info.get_theory "Real"))) "UnIqE_tErM"; fun d_in (Cor ((d,_),_)) = d | d_in (Syn (c)) = (tracing("*** d_in: Syn ("^c^")"); unique) | d_in (Typ (c)) = (tracing("*** d_in: Typ ("^c^")"); unique) diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Interpret/ptyps.sml --- a/src/Tools/isac/Interpret/ptyps.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Interpret/ptyps.sml Mon Feb 21 19:40:36 2011 +0100 @@ -388,7 +388,7 @@ it contains "#Given","#Where","#Find","#Relate"-patterns for constraints on identifiers see "fun cpy_nam"*) met : metID list}; (* methods solving the pbt*) -val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=theory "Pure", +val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=Thy_Info.get_theory "Pure", cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt; fun pbt2 (str, (t1, t2)) = pair2str (str, pair2str (term2str t1, term2str t2)); @@ -437,15 +437,15 @@ (*TODO: search generalized for subthy*) fun get_pbt (pblID:pblID) = let val pblRD = rev pblID; - in get_py (theory "Pure") pblID pblRD (!ptyps) end; + in get_py (Thy_Info.get_theory "Pure") pblID pblRD (!ptyps) end; (* get_pbt thy ["1"]; get_pbt thy ["21","2"]; *) (*TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument !!!!!*) -fun get_met (metID:metID) = get_py (theory "Pure") metID metID (!mets); -fun get_the (theID:theID) = get_py (theory "Pure") theID theID (! thehier); +fun get_met (metID:metID) = get_py (Thy_Info.get_theory "Pure") metID metID (!mets); +fun get_the (theID:theID) = get_py (Thy_Info.get_theory "Pure") theID theID (! thehier); @@ -491,7 +491,7 @@ (*.lookup a guh in hierarchy or methods depending on fst chars in guh.*) fun guh2kestoreID (guh:guh) = - case (implode o (take_fromto 1 4) o explode) guh of + case (implode o (take_fromto 1 4) o Symbol.explode) guh of "pbl_" => let fun node ids gu (Ptyp (id,[n as {guh,...} : pbt], ns)) = if gu = guh diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Interpret/rewtools.sml --- a/src/Tools/isac/Interpret/rewtools.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Interpret/rewtools.sml Mon Feb 21 19:40:36 2011 +0100 @@ -195,7 +195,7 @@ (*.toggles the marker for 'fun sym_thm'.*) fun sym_thmID (thmID : thmID) = - case explode thmID of + case Symbol.explode thmID of "s"::"y"::"m"::"_"::id => implode id : thmID | id => "sym_"^thmID; (* @@ -206,11 +206,11 @@ > sym_thmID thmID; val it = "sym_real_num_collect" : string*) fun sym_drop (thmID : thmID) = - case explode thmID of + case Symbol.explode thmID of "s"::"y"::"m"::"_"::id => implode id : thmID | id => thmID; fun is_sym (thmID : thmID) = - case explode thmID of + case Symbol.explode thmID of "s"::"y"::"m"::"_"::id => true | id => false; @@ -763,7 +763,7 @@ fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename; fun guh2theID (guh:guh) = - let val guh' = explode guh + let val guh' = Symbol.explode guh val part = implode (take_fromto 1 4 guh') val isa = implode (take_fromto 5 9 guh') in if not (member op = ["exp_", "thy_", "pbl_", "met_"] part) diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Interpret/script.sml --- a/src/Tools/isac/Interpret/script.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Interpret/script.sml Mon Feb 21 19:40:36 2011 +0100 @@ -97,7 +97,7 @@ let fun scan [] = [] | scan (s::ss) = if s = "'" then (scan ss) else (s::(scan ss)) - in (implode o scan o explode) str end; + in (implode o scan o Symbol.explode) str end; (* > val str = "Rewrite_Set_Inst"; > val esc = esc_underscore str; @@ -159,7 +159,7 @@ fun test_negotiable t = member op = (!negotiable) - ((strip_thy o (term_str (theory "Script")) o head_of) t); + ((strip_thy o (term_str (Thy_Info.get_theory "Script")) o head_of) t); (*.get argument of first stactic in a script for init_form.*) fun get_stac thy (h $ body) = @@ -381,7 +381,7 @@ stac2tac_ pt thy mm; assoc_thm' (assoc_thy "Isac") (tid,""); - assoc_thm' (theory "Isac") (tid,""); + assoc_thm' (Thy_Info.get_theory "Isac") (tid,""); *) | stac2tac_ pt thy (Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thmID,_) $ _ $ f) = @@ -443,7 +443,7 @@ Free (dI',_) $ (Const ("Pair",_) $ pI' $ mI')) $ ags') = (*compare "| assod _ (Subproblem'"*) - let val dI = ((implode o drop_last(*.."'"*) o explode) dI')(*^""*); + let val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*); val thy = maxthy (assoc_thy dI) (rootthy pt); val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI'; val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI'; @@ -654,7 +654,7 @@ Free (dI',_) $ (Const ("Pair",_) $ pI' $ mI')) $ ags') = (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*) - let val dI = ((implode o drop_last(*.."'"*) o explode) dI')(*^""*); + let val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*); val thy = maxthy (assoc_thy dI) (rootthy pt); val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI'; val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI'; @@ -1074,7 +1074,7 @@ assy ya ((E,(l@[R]),a,v,S,b),ss) e2 | ay => (ay)) (* val ((m,_,pt,(p,p_),c)::ss) = [(m,EmptyMout,pt,p,[])]; - val t = (term_of o the o (parse (theory "Isac"))) "Rewrite rmult_1 False"; + val t = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "Rewrite rmult_1 False"; val (ap,(p,p_),c,ss) = (Aundef,p,[],[]); assy (((thy',srls),d),ap) ((E,l,a,v,S,b), (m,EmptyMout,pt,(p,p_),c)::ss) t; @@ -1928,8 +1928,8 @@ (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) end; (* > val Script sc = (#scr o get_met) ("SqRoot","sqrt-equ-test"); -> val env = [((term_of o the o (parse (theory "Isac"))) "bdv", - (term_of o the o (parse (theory "Isac"))) "x")]; +> val env = [((term_of o the o (parse (Thy_Info.get_theory "Isac"))) "bdv", + (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "x")]; > map ((stac2tac pt thy) o #2 o(subst_stacexpr env NONE e_term)) (stacpbls sc); *) diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Knowledge/EqSystem.thy --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Feb 21 19:40:36 2011 +0100 @@ -112,7 +112,7 @@ fun dest_hd' (Const (a, T)) = (((a, 0), T), 0) | dest_hd' (Free (ccc, T)) = - (case explode ccc of + (case Symbol.explode ccc of "c"::[] => ((("|||||||||||||||||||||", 0), T), 1)(*greatest string WN*) | "c"::"_"::_ => ((("|||||||||||||||||||||", 0), T), 1) | _ => (((ccc, 0), T), 1)) @@ -121,7 +121,7 @@ | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4); fun size_of_term' (Free (ccc, _)) = - (case explode ccc of (*WN0510 hack for the bound variables*) + (case Symbol.explode ccc of (*WN0510 hack for the bound variables*) "c"::[] => 1000 | "c"::"_"::is => 1000 * ((str2int o implode) is) | _ => 1) @@ -190,7 +190,7 @@ val order_add_mult_System = Rls{id = "order_add_mult_System", preconds = [], rew_ord = ("ord_simplify_System", - ord_simplify_System false (theory "Integrate")), + ord_simplify_System false (Thy_Info.get_theory "Integrate")), erls = e_rls,srls = Erls, calc = [], rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}), (* z * w = w * z *) diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Knowledge/InsSort.thy --- a/src/Tools/isac/Knowledge/InsSort.thy Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Knowledge/InsSort.thy Mon Feb 21 19:40:36 2011 +0100 @@ -62,7 +62,7 @@ (** problem type **) store_pbt - (prep_pbt (theory "InsSort") + (prep_pbt (Thy_Info.get_theory "InsSort") (["functional"]:pblID, [("#Given" ,["unsorted u_"]), ("#Find" ,["sorted s_"]) @@ -70,7 +70,7 @@ [])); store_pbt - (prep_pbt (theory "InsSort") + (prep_pbt (Thy_Info.get_theory "InsSort") (["inssort","functional"]:pblID, [("#Given" ,["unsorted u_"]), ("#Find" ,["sorted s_"]) @@ -81,14 +81,14 @@ todo: implementation needs extra object-level lists **) store_met - (prep_met (theory "Diff") + (prep_met (Thy_Info.get_theory "Diff") (["InsSort"], [], {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, crls = Atools_rls, nrls=norm_Rational (*, asm_rls=[],asm_thm=[]*)}, "empty_script")); store_met - (prep_met (theory "InsSort") (*test-version for [#1,#3,#2] only: see *.sml*) + (prep_met (Thy_Info.get_theory "InsSort") (*test-version for [#1,#3,#2] only: see *.sml*) (["InsSort""sort"]:metID, [("#Given" ,["unsorted u_"]), ("#Find" ,["sorted s_"]) diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Knowledge/Integrate.thy --- a/src/Tools/isac/Knowledge/Integrate.thy Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Feb 21 19:40:36 2011 +0100 @@ -56,13 +56,13 @@ from a variable, but the value '(new_c es__)' itself.*) fun new_c term = let fun selc var = - case (explode o id_of) var of + case (Symbol.explode o id_of) var of "c"::[] => true | "c"::"_"::is => (case (int_of_str o implode) is of SOME _ => true | NONE => false) | _ => false; - fun get_coeff c = case (explode o id_of) c of + fun get_coeff c = case (Symbol.explode o id_of) c of "c"::"_"::is => (the o int_of_str o implode) is | _ => 0; val cs = filter selc (vars term); diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Knowledge/PolyEq.thy --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Feb 21 19:40:36 2011 +0100 @@ -1,7 +1,7 @@ (* theory collecting all knowledge (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in') for PolynomialEquations. - alternative dependencies see (theory "Isac") + alternative dependencies see (Thy_Info.get_theory "Isac") created by: rlang date: 02.07 changed by: rlang @@ -1384,7 +1384,7 @@ val order_add_mult_in = prep_rls( Rls{id = "order_add_mult_in", preconds = [], rew_ord = ("ord_make_polynomial_in", - ord_make_polynomial_in false (theory "Poly")), + ord_make_polynomial_in false (Thy_Info.get_theory "Poly")), erls = e_rls,srls = Erls, calc = [], (*asm_thm = [],*) diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Knowledge/PolyMinus.thy --- a/src/Tools/isac/Knowledge/PolyMinus.thy Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Mon Feb 21 19:40:36 2011 +0100 @@ -113,7 +113,7 @@ (*. get the identifier from specific monomials; see fun ist_monom .*) (*HACK.WN080107*) fun increase str = - let val s::ss = explode str + let val s::ss = Symbol.explode str in implode ((chr (ord s + 1))::ss) end; fun identifier (Free (id,_)) = id (* 2, a *) | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) = diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Knowledge/Root.thy --- a/src/Tools/isac/Knowledge/Root.thy Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Knowledge/Root.thy Mon Feb 21 19:40:36 2011 +0100 @@ -159,7 +159,7 @@ rew_ord' := overwritel (!rew_ord', [("termlessI", termlessI), - ("sqrt_right", sqrt_right false (theory "Pure")) + ("sqrt_right", sqrt_right false (Thy_Info.get_theory "Pure")) ]); (*-------------------------rulse-------------------------*) diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Knowledge/RootRatEq.thy --- a/src/Tools/isac/Knowledge/RootRatEq.thy Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Mon Feb 21 19:40:36 2011 +0100 @@ -152,7 +152,7 @@ ML {* (*-------------------------Methode-----------------------*) store_met - (prep_met (theory "LinEq") "met_rootrateq" [] e_metID + (prep_met (Thy_Info.get_theory "LinEq") "met_rootrateq" [] e_metID (["RootRatEq"], [], {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Knowledge/Simplify.thy --- a/src/Tools/isac/Knowledge/Simplify.thy Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Knowledge/Simplify.thy Mon Feb 21 19:40:36 2011 +0100 @@ -70,7 +70,7 @@ (*.function for handling the cas-input "Simplify (2*a + 3*a)": make a model which is already in ptree-internal format.*) (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)"); - val (h,argl) = strip_comb ((term_of o the o (parse (theory "Simplify"))) + val (h,argl) = strip_comb ((term_of o the o (parse (Thy_Info.get_theory "Simplify"))) "Simplify (2*a + 3*a)"); *) fun argl2dtss t = diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Knowledge/Test.thy --- a/src/Tools/isac/Knowledge/Test.thy Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Feb 21 19:40:36 2011 +0100 @@ -244,7 +244,7 @@ (*FIXXXXXXME 10.8.02: handle like _simplify*) val tval_rls = Rls{id = "tval_rls", preconds = [], - rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")), + rew_ord = ("sqrt_right",sqrt_right false (Thy_Info.get_theory "Pure")), erls=testerls,srls = e_rls, calc=[], rules = [Thm ("refl",num_str @{thm refl}), @@ -383,7 +383,7 @@ (* expects * distributed over + *) val Test_simplify = Rls{id = "Test_simplify", preconds = [], - rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")), + rew_ord = ("sqrt_right",sqrt_right false (Thy_Info.get_theory "Pure")), erls = tval_rls, srls = e_rls, calc=[(*since 040209 filled by prep_rls*)], (*asm_thm = [],*) @@ -566,7 +566,7 @@ [])); -val ttt = (term_of o the o (parse (theory "Isac"))) "(matches ( v_v = 0) e_e)"; +val ttt = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "(matches ( v_v = 0) e_e)"; ------ 25.8.01*) @@ -574,7 +574,7 @@ ML {* (** methods **) store_met - (prep_met (theory "Diff") "met_test" [] e_metID + (prep_met (Thy_Info.get_theory "Diff") "met_test" [] e_metID (["Test"], [], {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, @@ -582,7 +582,7 @@ asm_rls=[],asm_thm=[]*)}, "empty_script")); (* store_met - (prep_met (theory "Script") + (prep_met (Thy_Info.get_theory "Script") (e_metID,(*empty method*) [], {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], @@ -1290,7 +1290,7 @@ val make_polytest = Rls{id = "make_polytest", preconds = []:term list, - rew_ord = ("ord_make_polytest", ord_make_polytest false (theory "Poly")), + rew_ord = ("ord_make_polytest", ord_make_polytest false (Thy_Info.get_theory "Poly")), erls = testerls, srls = Erls, calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/ProgLang/ListC.thy --- a/src/Tools/isac/ProgLang/ListC.thy Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/ProgLang/ListC.thy Mon Feb 21 19:40:36 2011 +0100 @@ -4,15 +4,15 @@ *) theory ListC imports Complex_Main -uses ("library.sml")("calcelems.sml") -("ProgLang/termC.sml")("ProgLang/calculate.sml") -("ProgLang/rewrite.sml") +uses ("../library.sml")("../calcelems.sml") +("termC.sml")("calculate.sml") +("rewrite.sml") begin -use "library.sml" (*indent,...*) -use "calcelems.sml" (*str_of_type, Thm,...*) -use "ProgLang/termC.sml" (*num_str,...*) -use "ProgLang/calculate.sml" (*???*) -use "ProgLang/rewrite.sml" (*?*** At command "end" (line 205../ListC.thy*) +use "../library.sml" (*indent,...*) +use "../calcelems.sml" (*str_of_type, Thm,...*) +use "termC.sml" (*num_str,...*) +use "calculate.sml" (*???*) +use "rewrite.sml" (*?*** At command "end" (line 205../ListC.thy*) text {* 'nat' in List.thy replaced by 'real' *} diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/ProgLang/calculate.sml --- a/src/Tools/isac/ProgLang/calculate.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/ProgLang/calculate.sml Mon Feb 21 19:40:36 2011 +0100 @@ -215,7 +215,7 @@ *) (* val ((op_, eval_fn),ct)=(cc,pre); - (get_calculation_ (theory "Isac") (op_, eval_fn) ct) handle e => print_exn e; + (get_calculation_ (Thy_Info.get_theory "Isac") (op_, eval_fn) ct) handle e => print_exn e; parse thy "" *) (*.get a thm from an op_ somewhere in the term; @@ -240,7 +240,7 @@ val it = SOME ("sqrt_9_","sqrt 9 = 3 [sqrt 9 = 3]") : (string * thm) option > val ct = (the o (parse thy)) "#4<#4"; -> get_calculation_ thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o explode) str = "#"; +> get_calculation_ thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o Symbol.explode) str = "#"; val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]") diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/ProgLang/rewrite.sml --- a/src/Tools/isac/ProgLang/rewrite.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Feb 21 19:40:36 2011 +0100 @@ -395,7 +395,7 @@ identifiers starting with "#" come from Calc and get a hand-made theorem (containing numerals only).*) fun assoc_thm' (thy:theory) ((thmid, ct'):thm') = - (case explode thmid of + (case Symbol.explode thmid of "s"::"y"::"m"::"_"::id => if hd id = "#" then mk_thm thy ct' @@ -407,13 +407,13 @@ ) handle _ => error ("assoc_thm': '"^thmid^"' not in '"^ (theory2domID thy)^"' (and parents)"); -(*> assoc_thm' (theory "Isac") ("sym_#mult_2_3","6 = 2 * 3"); +(*> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_#mult_2_3","6 = 2 * 3"); val it = "6 = 2 * 3" : thm -> assoc_thm' (theory "Isac") ("add_0_left",""); +> assoc_thm' (Thy_Info.get_theory "Isac") ("add_0_left",""); val it = "0 + ?z = ?z" : thm -> assoc_thm' (theory "Isac") ("sym_real_add_zero_left",""); +> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_real_add_zero_left",""); val it = "?t = 0 + ?t" [.] : thm > assoc_thm' HOL.thy ("sym_real_add_zero_left",""); @@ -514,7 +514,7 @@ end; (* fun instantiate'' thy' subs ((thmid,ct'):thm') = - let val thmid_ = implode ("#"::(explode thmid)) (*see type thm'*) + let val thmid_ = implode ("#"::(Symbol.explode thmid)) (*see type thm'*) in (thmid_, (string_of_thmI o (read_instantiate subs)) ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end; @@ -539,7 +539,7 @@ (* instantiate'' fun instantiate'' thy' subs ((thmid,ct'):thm') = let - val thmid_ = implode ("#"::(explode thmid)); (*see type thm'*) + val thmid_ = implode ("#"::(Symbol.explode thmid)); (*see type thm'*) val thy = assoc_thy thy'; val typs = map (#T o rep_cterm o the o (parse thy)) ((snd o split_list) subs); @@ -642,7 +642,7 @@ - rewrite_set_ (theory "Isac") eval_rls false test_rls + rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false test_rls ((the o (parse thy)) "matches (?a = ?b) (x = #0)"); val xxx = (term_of o the o (parse thy)) "matches (?a = ?b) (x = #0)"; @@ -652,7 +652,7 @@ - rewrite_set_ (theory "Isac") eval_rls false eval_rls + rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false eval_rls ((the o (parse thy)) "contains_root (sqrt #0)"); val it = SOME ("True",[]) : (cterm * cterm list) option diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/ProgLang/termC.sml --- a/src/Tools/isac/ProgLang/termC.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/ProgLang/termC.sml Mon Feb 21 19:40:36 2011 +0100 @@ -130,14 +130,14 @@ *) (*fun int_of_str str = - let val ss = explode str + let val ss = Symbol.explode str val str' = case ss of "("::s => drop_last s | _ => ss in case BasisLibrary.Int.fromString (implode str') of SOME i => SOME i | NONE => NONE end;*) fun int_of_str str = - let val ss = explode str + let val ss = Symbol.explode str val str' = case ss of "("::s => drop_last s | _ => ss in (SOME (Thy_Output.integer (implode str'))) handle _ => NONE end; @@ -221,7 +221,7 @@ | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2) in (distinct o (scan [])) t end; fun is_bdv str = - case explode str of + case Symbol.explode str of "b"::"d"::"v"::_ => true | _ => false; fun is_bdv_ (Free (s,_)) = is_bdv s @@ -295,8 +295,8 @@ fun mk_prop t = Trueprop $ t; val true_as_term = Const("True",bool); val false_as_term = Const("False",bool); -val true_as_cterm = cterm_of (theory "HOL") true_as_term; -val false_as_cterm = cterm_of (theory "HOL") false_as_term; +val true_as_cterm = cterm_of (Thy_Info.get_theory "HOL") true_as_term; +val false_as_cterm = cterm_of (Thy_Info.get_theory "HOL") false_as_term; infixr 5 -->; (*2002 /Pure/term.ML *) infixr --->; (*2002 /Pure/term.ML *) @@ -1073,9 +1073,9 @@ (*version for testing local to theories*) fun str2term_ thy str = (term_of o the o (parse thy)) str; -fun str2term str = (term_of o the o (parse (theory "Isac"))) str; +fun str2term str = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) str; fun strs2terms ss = map str2term ss; -fun str2termN str = (term_of o the o (parseN (theory "Isac"))) str; +fun str2termN str = (term_of o the o (parseN (Thy_Info.get_theory "Isac"))) str; (*+ makes a substitution from the output of Pattern.match +*) (*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*) @@ -1089,7 +1089,7 @@ fun inst_bdv [] t = t : term | inst_bdv (instl: (term*term) list) t = let fun subst (v as Var((s,_),T)) = - (case explode s of + (case Symbol.explode s of "b"::"d"::"v"::_ => if_none (assoc(instl,Free(s,T))) (Free(s,T)) | _ => v) diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Test_Isac.thy --- a/src/Tools/isac/Test_Isac.thy Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Test_Isac.thy Mon Feb 21 19:40:36 2011 +0100 @@ -125,7 +125,7 @@ use"algein.sml"; *) ML {* -theory "Isac" +Thy_Info.get_theory "Isac" *} use "../../../test/Tools/isac/Knowledge/isac.sml"; (**) @@ -139,7 +139,7 @@ use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test" : *** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library" -*** Theory loader: the error(s) above occurred while examining theory "Foo_Language" +*** Theory loader: the error(s) above occurred while examining Thy_Info.get_theory "Foo_Language" use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test" *) diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/Test_Some.thy --- a/src/Tools/isac/Test_Some.thy Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/Test_Some.thy Mon Feb 21 19:40:36 2011 +0100 @@ -13,7 +13,7 @@ ML {* fun term2st t = Print_Mode.setmp [] (Syntax.string_of_term -(ProofContext.init_global (Thy_Info.get_theory "Rational"))) t; +(ProofContext.init_global (Thy_Info.get_Thy_Info.get_theory "Rational"))) t; (*..............................................########......................*) *} diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/calcelems.sml --- a/src/Tools/isac/calcelems.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/calcelems.sml Mon Feb 21 19:40:36 2011 +0100 @@ -20,15 +20,15 @@ type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*) type thm'' = thmID * term; type rls' = string; -(*.a 'guh'='globally unique handle' is a string unique for each element +(*.a 'guh'='globally unique handle' is a string unique for each element of isac's KEStore and persistent over time (in particular under shifts within the respective hierarchy); - specialty for thys: + specialty for thys: # guh NOT resistant agains shifts from one thy to another (which is the price for Isabelle's design: thy's overwrite ids of subthy's) # requirement for matchTheory: induce guh from tac + current thy (see 'fun thy_containing_thm', 'fun thy_containing_rls' etc.) - TODO: introduce to pbl, met.*) + TODO: introduce to pbl, met.*) type guh = string; val e_guh = "e_guh":guh; @@ -59,20 +59,20 @@ val e_rew_ordX = (e_rew_ord', e_rew_ord_) : rew_ord; -datatype rule = +datatype rule = Erule (*.the empty rule .*) -| Thm of (string * thm)(*.a theorem, ie (identifier, Thm.thm).*) +| Thm of (string * Basic_Thm.thm)(*.a theorem, ie (identifier, Thm.thm).*) | Calc of string * (*.sml-code manipulating a (sub)term .*) (string -> term -> theory -> (string * term) option) | Cal1 of string * (*.sml-code applied only to whole term or left/right-hand-side of eqality .*) (string -> term -> theory -> (string * term) option) | Rls_ of rls (*.ie. rule sets may be nested.*) -and scr = - EmptyScr +and scr = + EmptyScr | Script of term (*for met*) - | Rfuns of {init_state : term -> - (term * (*the current formula: + | Rfuns of {init_state : term -> + (term * (*the current formula: goes locate_gen -> next_tac via istate*) term * (*the final formula*) rule list (*of reverse rewrite set (#1#)*) @@ -81,18 +81,19 @@ (term * (*... rewrite with ...*) term list)) (*... assumptions*) list), (*derivation from given term to normalform - in reverse order with sym_thm; + in reverse order with sym_thm; (#1#) could be extracted from here #1*) normal_form: term -> (term * term list) option, - locate_rule: rule list list -> term -> rule + locate_rule: rule list list -> term -> rule -> (rule * (term * term list)) list, next_rule : rule list list -> term -> rule option, - attach_form: rule list list -> term -> term + attach_form: rule list list -> term -> term -> (rule * (term * term list)) list} + and rls = Erls (*for init e_rls*) - + | Rls of (*a confluent and terminating ruleset, in general *) {id : string, (*for trace_rewrite:=true *) preconds : term list, (*unused WN020820 *) @@ -112,16 +113,16 @@ rew_ord : rew_ord, (*for rules *) erls : rls, (*for the conditions in rules *) srls : rls, (*for evaluation of list_fns in script *) - calc : calc list, (*for Calculate in scr, set by prep_rls *) + calc : calc list, (*for Calculate in scr, set by prep_rls *) rules : rule list, scr : scr} (*Script term (how to restrict type ???)*) (*Rrls call SML-code and simulate an rls difference: there is always _ONE_ redex rewritten in 1 call, thus wrap Rrls by: Rls (Rls_ ...)*) - + | Rrls of (* for 'reverse rewriting' by SML-functions instead Script *) {id : string, (* for trace_rewrite := true *) - prepat : (term list *(* preconds, eval with subst from pattern; + prepat : (term list *(* preconds, eval with subst from pattern; if [HOLogic.true_const], match decides alone *) term ) (* pattern matched with current (sub)term *) list, (* meta-conjunction is or *) @@ -132,18 +133,17 @@ (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently from rls, and then contain both Script _AND_ Rfuns !!!*) -fun thy2ctxt' thy' = ProofContext.init_global (theory thy');(*FIXXXME thy-ctxt*) +fun thy2ctxt' thy' = ProofContext.init_global (Thy_Info.get_theory thy');(*FIXXXME thy-ctxt*) fun thy2ctxt thy = ProofContext.init_global thy;(*FIXXXME thy-ctxt*) (*ctxt for retrieval of all thms in HOL; FIXME make this local?*) -(*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*) +(*val ctxt_HOL = ProofContext.init_global (Thy_Info.get_theory "Complex_Main");*) (*val ctxt_HOL = thy2ctxt' "Complex_Main";*) (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*) (*fun ctxt_Isac _ = thy2ctxt' "Isac";*) fun Isac _ = ProofContext.theory_of (thy2ctxt' "Isac"); -val e_rule = - Thm ("refl", ProofContext.get_thm (thy2ctxt' "Complex_Main") "refl" ); +val e_rule = Thm ("refl", @{thm refl}); fun id_of_thm (Thm (id, _)) = id | id_of_thm _ = error "id_of_thm"; fun thm_of_thm (Thm (_, thm)) = thm @@ -164,8 +164,8 @@ (*check for [.] as caused by "fun assoc_thm'"*) fun string_of_thmI thm = let val ct' = (de_quote o string_of_thm) thm - val (a, b) = split_nlast (5, explode ct') - in case b of + val (a, b) = split_nlast (5, Symbol.explode ct') + in case b of [" ", " ","[", ".", "]"] => implode a | _ => ct' end; @@ -204,7 +204,7 @@ type rrlsstate = (*state for reverse rewriting*) - (term * (*the current formula: + (term * (*the current formula: goes locate_gen -> next_tac via istate*) term * (*the final formula*) rule list (*of reverse rewrite set (#1#)*) @@ -213,7 +213,7 @@ (term * (*... rewrite with ...*) term list)) (*... assumptions*) list); (*derivation from given term to normalform - in reverse order with sym_thm; + in reverse order with sym_thm; (#1#) could be extracted from here #1*) val e_type = Type("empty",[]); val a_type = TFree("'a",[]); @@ -246,14 +246,14 @@ val theory2thyID = (get_thy o string_of_thy) : theory -> thyID; val theory2theory' = string_of_thy; val theory2str = string_of_thy; (*WN050903 ..most consistent naming*) -val theory2str' = implode o (drop_last_n 4) o explode o string_of_thy; -(*> theory2str' (theory "Isac"); +val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy; +(*> theory2str' (Thy_Info.get_theory "Isac"); al it = "Isac" : string *) fun thyID2theory' (thyID:thyID) = thyID; (* - let val ss = explode thyID + let val ss = Symbol.explode thyID val ext = implode (takelast (4, ss)) in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*) else thyID ^ ".thy" @@ -267,7 +267,7 @@ fun theory'2thyID (theory':theory') = theory'; (* - let val ss = explode theory' + let val ss = Symbol.explode theory' val ext = implode (takelast (4, ss)) in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID else theory' (*disarm abuse of theory'*) @@ -287,25 +287,25 @@ eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..' which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script - because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b + because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard (see match_ags). Preliminary solution: # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically, # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl - # however, a thy specified by the user in the rootpbl may lead to - errors in far-off subpbls (which are not yet reported properly !!!) + # however, a thy specified by the user in the rootpbl may lead to + errors in far-off subpbls (which are not yet reported properly !!!) and interactively specifiying thys in subpbl is not very relevant. Other solutions possible: - # always parse and type-check with theory "Isac" + # always parse and type-check with Thy_Info.get_theory "Isac" (rejected tue to the vague idea eg. to re-use equations for R in C etc.) # regard the subthy-relation in specifying thys of subpbls # specifically handle 'SubProblem (undefined, pbl, arglist)' # ??? .*) -(*WN0509 TODO "ProtoPure" ... would be more consistent +(*WN0509 TODO "ProtoPure" ... would be more consistent with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*) val e_domID = "e_domID":domID; @@ -336,18 +336,18 @@ (*for distinction of contexts*) datatype ketype = Exp_ | Thy_ | Pbl_ | Met_; fun ketype2str Exp_ = "Exp_" - | ketype2str Thy_ = "Thy_" - | ketype2str Pbl_ = "Pbl_" + | ketype2str Thy_ = "Thy_" + | ketype2str Pbl_ = "Pbl_" | ketype2str Met_ = "Met_"; fun ketype2str' Exp_ = "Example" - | ketype2str' Thy_ = "Theory" - | ketype2str' Pbl_ = "Problem" + | ketype2str' Thy_ = "Theory" + | ketype2str' Pbl_ = "Problem" | ketype2str' Met_ = "Method"; (*see 'How to manage theorys in subproblems' at 'type thyID'*) val theory' = Unsynchronized.ref ([]:(theory' * theory) list); -(*.all theories defined for Scripts, recorded in Scripts/Script.ML; +(*.all theories defined for Scripts, recorded in Scripts/Script.ML; in order to distinguish them from general IsacKnowledge defined later on.*) val script_thys = Unsynchronized.ref ([] : (theory' * theory) list); @@ -379,7 +379,7 @@ (*.'a is for pbt | met.*) (*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*) -datatype 'a ptyp = +datatype 'a ptyp = Ptyp of string * (*element within pblID*) 'a list * (*several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69) @@ -416,7 +416,7 @@ type thehier = (thydata ptyp) list; val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*) -(* an association list, gets the value once in Isac.ML. +(* an association list, gets the value once in Isac.ML. stores Isabelle's thms as terms for compatibility with Theory.axioms_of. WN1-1-28 make this data arguments and del ref ?*) val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list); @@ -437,9 +437,9 @@ next_rule=ne,attach_form=fo}; end; -val e_rls = +val e_rls = Rls{id = "e_rls", - preconds = [], + preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,srls = Erls, calc = [], @@ -464,20 +464,20 @@ | rep_rls Erls = rep_rls e_rls | rep_rls (Rrls {id,...}) = rep_rls e_rls (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*); -(*| rep_rls (Seq {id,...}) = +(*| rep_rls (Seq {id,...}) = error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id); --1.7.03*) -fun rep_rrls - (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord, +fun rep_rrls + (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord, scr=Rfuns {attach_form,init_state,locate_rule, next_rule,normal_form}}) = - {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat, - rew_ord=rew_ord, attach_form=attach_form, init_state=init_state, + {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat, + rew_ord=rew_ord, attach_form=attach_form, init_state=init_state, locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form} - | rep_rrls (Rls {id,...}) = + | rep_rrls (Rls {id,...}) = error ("rep_rrls doesn't take apart (normal) rule-sets: "^id) - | rep_rrls (Seq {id,...}) = + | rep_rrls (Seq {id,...}) = error ("rep_rrls doesn't take apart (normal) rule-sets: "^id); fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, @@ -488,7 +488,7 @@ rules =rs,scr=sc}) r = (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, rules = rs @ r,scr=sc}:rls) - | append_rls id (Rrls _) _ = + | append_rls id (Rrls _) _ = error ("append_rls: not for reverse-rewrite-rule-set "^id); (*. are _atomic_ rules equal ?.*) @@ -503,12 +503,12 @@ | merge_rls _ rls Erls = rls | merge_rls id (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1, - (*asm_thm=at1,*)rules =rs1,scr=sc1}) + (*asm_thm=at1,*)rules =rs1,scr=sc1}) (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2, (*asm_thm=at2,*)rules =rs2,scr=sc2}) = (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2), rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*), - srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 ((#srls o rep_rls) r2), calc=ca1 @ ((#calc o rep_rls) r2), (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*) @@ -516,18 +516,18 @@ scr=sc1}:rls) | merge_rls id (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1, - (*asm_thm=at1,*)rules =rs1,scr=sc1}) + (*asm_thm=at1,*)rules =rs1,scr=sc1}) (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2, (*asm_thm=at2,*)rules =rs2,scr=sc2}) = (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2), rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*), - srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 ((#srls o rep_rls) r2), calc=ca1 @ ((#calc o rep_rls) r2), (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*) rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2), scr=sc1}:rls) - | merge_rls _ _ _ = + | merge_rls _ _ _ = error "merge_rls: not for reverse-rewrite-rule-sets\ \and not for mixed Rls -- Seq"; fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, @@ -540,21 +540,21 @@ (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r), scr=sc}:rls) - | remove_rls id (Rrls _) _ = error + | remove_rls id (Rrls _) _ = error ("remove_rls: not for reverse-rewrite-rule-set "^id); (*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]); val it = [1, 2] : int list*) (*elder version: migrated 3 calls in smtest to memrls -fun mem_rls id rls = +fun mem_rls id rls = case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of SOME _ => true | NONE => false;*) fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules) | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules) | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r)); fun rls_get_thm rls (id: xstring) = - case find_first (curry eq_rule e_rule) + case find_first (curry eq_rule e_rule) ((#rules o rep_rls) rls) of SOME thm => SOME thm | NONE => NONE; @@ -565,10 +565,10 @@ (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy)) handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*) fun assoc_thy (thy:theory') = - if thy = "e_domID" then (theory "Script") (*lower bound of Knowledge*) - else (theory thy) + if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*) + else (Thy_Info.get_theory thy) handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system"); - + (*.associate an rls-identifier with an rls; related to 'fun assoc_rls'; these are NOT compatible to "fun assoc_thm'" in that they do NOT handle overlays by re-using an identifier in different thys.*) @@ -581,7 +581,7 @@ in order to create the thy_hierarchy; overwrites existing rls' even if they are defined in a different thy; this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*) -(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that +(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that they do NOT handle overlays by re-using an identifier in different thys; "thyID.rlsID" would be a good solution, if the "." would be possible in scripts... @@ -598,13 +598,13 @@ | assoc_calc ((calc, (keyi, xi)) :: pairs, key) = if key = keyi then calc else assoc_calc (pairs, key); (*only used for !calclist'...*) -fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key +fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key ^"' not found") | assoc1 ((all as (keyi, _)) :: pairs, key) = if key = keyi then all else assoc1 (pairs, key); (*TODO.WN080102 clarify usage of type cal and type calc..*) -fun calID2calcID (calID : calID) = +fun calID2calcID (calID : calID) = let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'") | ass ((calci, (cali, eval_fn))::ids) = if calID = cali then calci @@ -624,19 +624,19 @@ fun termopt2str (SOME t) = "SOME " ^ term2str t | termopt2str NONE = "NONE"; -fun type2str typ = +fun type2str typ = Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ; val string_of_typ = type2str; -fun subst2str (s:subst) = - (strs2str o +fun subst2str (s:subst) = + (strs2str o (map (linefeed o pair2str o - (apsnd term2str) o + (apsnd term2str) o (apfst term2str)))) s; -fun subst2str' (s:subst) = - (strs2str' o +fun subst2str' (s:subst) = + (strs2str' o (map (pair2str o - (apsnd term2str) o + (apsnd term2str) o (apfst term2str)))) s; (*> subst2str' [(str2term "bdv", str2term "x"), (str2term "bdv_2", str2term "y")]; @@ -669,7 +669,7 @@ datatype lrd = (*elements of a path (=loc_) into an Isabelle term*) - L (*go left at $*) + L (*go left at $*) | R (*go right at $*) | D; (*go down at Abs*) type loc_ = lrd list; @@ -681,3 +681,1089 @@ (* end (*struct*) *) + + + +val e_rule = + Thm ("refl", @{thm refl}); +fun id_of_thm (Thm (id, _)) = id + | id_of_thm _ = error "id_of_thm"; +fun thm_of_thm (Thm (_, thm)) = thm + | thm_of_thm _ = error "thm_of_thm"; +fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); + +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); +fun thyID_of_derivation_name dn = hd (space_explode "." dn); + +fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) = + (strip_thy thmid1) = (strip_thy thmid2); +(*version typed weaker WN100910*) +fun eq_thmI' ((thmid1, _), (thmid2, _)) = + (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2); + + +val string_of_thm = Thm.get_name_hint; (*FIXME.2009*) +(*check for [.] as caused by "fun assoc_thm'"*) +fun string_of_thmI thm = + let val ct' = (de_quote o string_of_thm) thm + val (a, b) = split_nlast (5, Symbol.explode ct') + in case b of + [" ", " ","[", ".", "]"] => implode a + | _ => ct' + end; + +(*.id requested for all, Rls,Seq,Rrls.*) +fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*) + | id_rls (Rls {id,...}) = id + | id_rls (Seq {id,...}) = id + | id_rls (Rrls {id,...}) = id; +val rls2str = id_rls; +fun id_rule (Thm (id, _)) = id + | id_rule (Calc (id, _)) = id + | id_rule (Rls_ rls) = id_rls rls; + +fun get_rules (Rls {rules,...}) = rules + | get_rules (Seq {rules,...}) = rules + | get_rules (Rrls _) = []; + +fun rule2str Erule = "Erule" + | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")" + | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)" + | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)" + | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")"; +fun rule2str' Erule = "Erule" + | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")" + | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)" + | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)" + | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")"; + +(*WN080102 compare eq_rule ?!?*) +fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2 + | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2 + | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2 + | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*) + | eqrule _ = false; + + +type rrlsstate = (*state for reverse rewriting*) + (term * (*the current formula: + goes locate_gen -> next_tac via istate*) + term * (*the final formula*) + rule list (*of reverse rewrite set (#1#)*) + list * (*may be serveral, eg. in norm_rational*) + (rule * (*Thm (+ Thm generated from Calc) resulting in ...*) + (term * (*... rewrite with ...*) + term list)) (*... assumptions*) + list); (*derivation from given term to normalform + in reverse order with sym_thm; + (#1#) could be extracted from here #1*) +val e_type = Type("empty",[]); +val a_type = TFree("'a",[]); +val e_term = Const("empty",e_type); +val a_term = Free("empty",a_type); +val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate; + + + + +(*22.2.02: ging auf Linux nicht (Stefan) +val e_scr = Script ((term_of o the o (parse thy)) "e_script");*) +val e_term = Const("empty", Type("'a", [])); +val e_scr = Script e_term; + + +(*ad thm': + there are two kinds of theorems ... + (1) known by isabelle + (2) not known, eg. calc_thm, instantiated rls + the latter have a thmid "#..." + and thus outside isa we ALWAYS transport both (thmid,string_of_thmI) + and have a special assoc_thm / assoc_rls in this interface *) +type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*) +type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*) +type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*) + +fun string_of_thy thy = Context.theory_name thy: theory'; +val theory2domID = string_of_thy; +val theory2thyID = (get_thy o string_of_thy) : theory -> thyID; +val theory2theory' = string_of_thy; +val theory2str = string_of_thy; (*WN050903 ..most consistent naming*) +val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy; +(*> theory2str' (Thy_Info.get_theory "Isac"); +al it = "Isac" : string +*) + +fun thyID2theory' (thyID:thyID) = thyID; +(* + let val ss = Symbol.explode thyID + val ext = implode (takelast (4, ss)) + in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*) + else thyID ^ ".thy" + end; +*) +(* thyID2theory' "Isac" (*ok*); +val it = "Isac" : theory' + > thyID2theory' "Isac" (*abuse, goes ok...*); +val it = "Isac" : theory' +*) + +fun theory'2thyID (theory':theory') = theory'; +(* + let val ss = Symbol.explode theory' + val ext = implode (takelast (4, ss)) + in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID + else theory' (*disarm abuse of theory'*) + end; +*) +(* theory'2thyID "Isac"; +val it = "Isac" : thyID +> theory'2thyID "Isac"; +val it = "Isac" : thyID*) + + +(*. WN0509 discussion: +############################################################################# +# How to manage theorys in subproblems wrt. the requirement, # +# that scripts should be re-usable ? # +############################################################################# + + eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..' + which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script + because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b + is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard + (see match_ags). + + Preliminary solution: + # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically, + # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl + # however, a thy specified by the user in the rootpbl may lead to + errors in far-off subpbls (which are not yet reported properly !!!) + and interactively specifiying thys in subpbl is not very relevant. + + Other solutions possible: + # always parse and type-check with Thy_Info.get_theory "Isac" + (rejected tue to the vague idea eg. to re-use equations for R in C etc.) + # regard the subthy-relation in specifying thys of subpbls + # specifically handle 'SubProblem (undefined, pbl, arglist)' + # ??? +.*) +(*WN0509 TODO "ProtoPure" ... would be more consistent + with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*) +val e_domID = "e_domID":domID; + +(*the key into the hierarchy ob theory elements*) +type theID = string list; +val e_theID = ["e_theID"]; +val theID2str = strs2str; +(*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*) +fun theID2thyID (theID:theID) = + if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID + else error ("theID2thyID called with "^ theID2str theID); + +(*the key into the hierarchy ob problems*) +type pblID = string list; (* domID::...*) +val e_pblID = ["e_pblID"]:pblID; +val pblID2str = strs2str; + +(*the key into the hierarchy ob methods*) +type metID = string list; +val e_metID = ["e_metID"]:metID; +val metID2str = strs2str; + +(*either theID or pblID or metID*) +type kestoreID = string list; +val e_kestoreID = ["e_kestoreID"]; +val kestoreID2str = strs2str; + +(*for distinction of contexts*) +datatype ketype = Exp_ | Thy_ | Pbl_ | Met_; +fun ketype2str Exp_ = "Exp_" + | ketype2str Thy_ = "Thy_" + | ketype2str Pbl_ = "Pbl_" + | ketype2str Met_ = "Met_"; +fun ketype2str' Exp_ = "Example" + | ketype2str' Thy_ = "Theory" + | ketype2str' Pbl_ = "Problem" + | ketype2str' Met_ = "Method"; + +(*see 'How to manage theorys in subproblems' at 'type thyID'*) +val theory' = Unsynchronized.ref ([]:(theory' * theory) list); + +(*.all theories defined for Scripts, recorded in Scripts/Script.ML; + in order to distinguish them from general IsacKnowledge defined later on.*) +val script_thys = Unsynchronized.ref ([] : (theory' * theory) list); + + +(*rewrite orders, also stored in 'type met' and type 'and rls' + The association list is required for 'rewrite.."rew_ord"..' + WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*) +val rew_ord' = + Unsynchronized.ref + ([]:(rew_ord' * (*the key for the association list *) + (subst (*the bound variables - they get high order*) + -> (term * term) (*(t1, t2) to be compared *) + -> bool)) (*if t1 <= t2 then true else false *) + list); (*association list *) + +rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord), + ("dummy_ord", dummy_ord)]); + + +(*WN060120 a hack to get alltogether run again with minimal effort: + theory' is inserted for creating thy_hierarchy; calls for assoc_rls + need not be called*) +val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list); + +(*FIXME.040207 calclist': used by prep_rls, NOT in met*) +val calclist'= Unsynchronized.ref ([]: calc list); + +(*.the hierarchy of thydata.*) + +(*.'a is for pbt | met.*) +(*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*) +datatype 'a ptyp = + Ptyp of string * (*element within pblID*) + 'a list * (*several pbts with different domIDs/thy + TODO: select by subthy (isaref.p.69) + presently only _ONE_ elem*) + ('a ptyp) list; (*the children nodes*) + +(*.datatype for collecting thydata for hierarchy.*) +(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*) +(*WN0606 Htxt contains html which does not belong to the sml-kernel*) +datatype thydata = Html of {guh: guh, + coursedesign: authors, + mathauthors: authors, + html: string} (*html; for demos before database*) + | Hthm of {guh: guh, + coursedesign: authors, + mathauthors: authors, + thm: term} + | Hrls of {guh: guh, + coursedesign: authors, + mathauthors: authors, + (*like vvvvvvvvvvvvv val ruleset' + WN060711 redesign together !*) + thy_rls: (thyID * rls)} + | Hcal of {guh: guh, + coursedesign: authors, + mathauthors: authors, + calc: calc} + | Hord of {guh: guh, + coursedesign: authors, + mathauthors: authors, + ord: (subst -> (term * term) -> bool)}; +val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""}; + +type thehier = (thydata ptyp) list; +val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*) + +(* an association list, gets the value once in Isac.ML. + stores Isabelle's thms as terms for compatibility with Theory.axioms_of. + WN1-1-28 make this data arguments and del ref ?*) +val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list); + + +type path = string; +type filename = string; + +(*val xxx = fn: a b => (a,b); ??? fun-definition ???*) +local + fun ii (_:term) = e_rrlsstate; + fun no (_:term) = SOME (e_term,[e_term]); + fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))]; + fun ne (_:rule list list) (_:term) = SOME e_rule; + fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))]; +in +val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo, + next_rule=ne,attach_form=fo}; +end; + +val e_rls = + Rls{id = "e_rls", + preconds = [], + rew_ord = ("dummy_ord", dummy_ord), + erls = Erls,srls = Erls, + calc = [], + rules = [], scr = EmptyScr}:rls; +val e_rrls = Rrls {id = "e_rrls", + prepat = [], + rew_ord = ("dummy_ord", dummy_ord), + erls = Erls, + calc = [], + (*asm_thm=[],*) + scr=e_rfuns}:rls; +ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)), + ("e_rrls",("Tools",e_rrls)) + ]); + +fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) = + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc, + (*asm_thm=asm_thm,*)rules=rules,scr=scr} + | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) = + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc, + (*asm_thm=asm_thm,*)rules=rules,scr=scr} + | rep_rls Erls = rep_rls e_rls + | rep_rls (Rrls {id,...}) = rep_rls e_rls + (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*); +(*| rep_rls (Seq {id,...}) = + error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id); +--1.7.03*) +fun rep_rrls + (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord, + scr=Rfuns + {attach_form,init_state,locate_rule, + next_rule,normal_form}}) = + {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat, + rew_ord=rew_ord, attach_form=attach_form, init_state=init_state, + locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form} + | rep_rrls (Rls {id,...}) = + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id) + | rep_rrls (Seq {id,...}) = + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id); + +fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + rules =rs,scr=sc}) r = + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + rules = rs @ r,scr=sc}:rls) + | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + rules =rs,scr=sc}) r = + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + rules = rs @ r,scr=sc}:rls) + | append_rls id (Rrls _) _ = + error ("append_rls: not for reverse-rewrite-rule-set "^id); + +(*. are _atomic_ rules equal ?.*) +(*WN080102 compare eqrule ?!?*) +fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2 + | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2 + | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2 + (*id_rls checks for Rls, Seq, Rrls*) + | eq_rule _ = false; + +fun merge_rls _ Erls rls = rls + | merge_rls _ rls Erls = rls + | merge_rls id + (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1, + (*asm_thm=at1,*)rules =rs1,scr=sc1}) + (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2, + (*asm_thm=at2,*)rules =rs2,scr=sc2}) = + (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2), + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*), + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 + ((#srls o rep_rls) r2), + calc=ca1 @ ((#calc o rep_rls) r2), + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*) + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2), + scr=sc1}:rls) + | merge_rls id + (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1, + (*asm_thm=at1,*)rules =rs1,scr=sc1}) + (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2, + (*asm_thm=at2,*)rules =rs2,scr=sc2}) = + (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2), + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*), + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 + ((#srls o rep_rls) r2), + calc=ca1 @ ((#calc o rep_rls) r2), + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*) + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2), + scr=sc1}:rls) + | merge_rls _ _ _ = + error "merge_rls: not for reverse-rewrite-rule-sets\ + \and not for mixed Rls -- Seq"; +fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + (*asm_thm=at,*)rules =rs,scr=sc}) r = + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r), + scr=sc}:rls) + | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + (*asm_thm=at,*)rules =rs,scr=sc}) r = + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r), + scr=sc}:rls) + | remove_rls id (Rrls _) _ = error + ("remove_rls: not for reverse-rewrite-rule-set "^id); + +(*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]); +val it = [1, 2] : int list*) + +(*elder version: migrated 3 calls in smtest to memrls +fun mem_rls id rls = + case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of + SOME _ => true | NONE => false;*) +fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules) + | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules) + | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r)); +fun rls_get_thm rls (id: xstring) = + case find_first (curry eq_rule e_rule) + ((#rules o rep_rls) rls) of + SOME thm => SOME thm | NONE => NONE; + +fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known") + | assoc' ((keyi, xi) :: pairs, key) = + if key = keyi then SOME xi else assoc' (pairs, key); + +(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy)) + handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*) +fun assoc_thy (thy:theory') = + if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*) + else (Thy_Info.get_theory thy) + handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system"); + +(*.associate an rls-identifier with an rls; related to 'fun assoc_rls'; + these are NOT compatible to "fun assoc_thm'" in that they do NOT handle + overlays by re-using an identifier in different thys.*) +fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls)) + handle _ => error ("ME_Isa: '"^rls^"' not in system"); +(*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls)) + handle _ => error ("ME_Isa: '"^rls^"' not in system");*) + +(*.overwrite an element in an association list and pair it with a thyID + in order to create the thy_hierarchy; + overwrites existing rls' even if they are defined in a different thy; + this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*) +(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that + they do NOT handle overlays by re-using an identifier in different thys; + "thyID.rlsID" would be a good solution, if the "." would be possible + in scripts... + actually a hack to get alltogether run again with minimal effort*) +fun insthy thy' (rls', rls) = (rls', (thy', rls)); +fun overwritelthy thy (al, bl:(rls' * rls) list) = + let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl + in overwritel (al, bl') end; + +fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro)) + handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system"); +(*get the string for stac from rule*) +fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found") + | assoc_calc ((calc, (keyi, xi)) :: pairs, key) = + if key = keyi then calc else assoc_calc (pairs, key); +(*only used for !calclist'...*) +fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key + ^"' not found") + | assoc1 ((all as (keyi, _)) :: pairs, key) = + if key = keyi then all else assoc1 (pairs, key); + +(*TODO.WN080102 clarify usage of type cal and type calc..*) +fun calID2calcID (calID : calID) = + let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'") + | ass ((calci, (cali, eval_fn))::ids) = + if calID = cali then calci + else ass ids + in ass (!calclist') : calcID end; + +fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term +(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t; + +fun terms2str ts = (strs2str o (map term2str )) ts; +(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*) +fun terms2str' ts = (strs2str' o (map term2str )) ts; +(*terms2str' [t1,t2] = "[1 + 2,abc]";*) +fun terms2strs ts = (map term2str) ts; +(*terms2strs [t1,t2] = ["1 + 2", "abc"];*) + +fun termopt2str (SOME t) = "SOME " ^ term2str t + | termopt2str NONE = "NONE"; + +fun type2str typ = + Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ; +val string_of_typ = type2str; + +fun subst2str (s:subst) = + (strs2str o + (map (linefeed o pair2str o + (apsnd term2str) o + (apfst term2str)))) s; +fun subst2str' (s:subst) = + (strs2str' o + (map (pair2str o + (apsnd term2str) o + (apfst term2str)))) s; +(*> subst2str' [(str2term "bdv", str2term "x"), + (str2term "bdv_2", str2term "y")]; +val it = "[(bdv, x)]" : string +*) +val env2str = subst2str; + + +(*recursive defs:*) +fun scr2str (Script s) = "Script "^(term2str s) + | scr2str (Rfuns _) = "Rfuns"; + + +fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1; + + +(*.trace internal steps of isac's rewriter*) +val trace_rewrite = Unsynchronized.ref false; +(*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*) +val depth = Unsynchronized.ref 99999; +(*.no of rewrites exceeding this int -> NO rewrite.*) +(*WN060829 still unused...*) +val lim_rewrite = Unsynchronized.ref 99999; +(*.no of derivation-elements exceeding this int -> SOME derivation-elements.*) +val lim_deriv = Unsynchronized.ref 100; +(*.switch for checking guhs unique before storing a pbl or met; + set true at startup (done at begin of ROOT.ML) + set false for editing IsacKnowledge (done at end of ROOT.ML).*) +val check_guhs_unique = Unsynchronized.ref false; + + +datatype lrd = (*elements of a path (=loc_) into an Isabelle term*) + L (*go left at $*) + | R (*go right at $*) + | D; (*go down at Abs*) +type loc_ = lrd list; +fun ldr2str L = "L" + | ldr2str R = "R" + | ldr2str D = "D"; +fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k; + +(* +end (*struct*) +*) + + +val e_rule = + Thm ("refl", @{thm refl}); +fun id_of_thm (Thm (id, _)) = id + | id_of_thm _ = error "id_of_thm"; +fun thm_of_thm (Thm (_, thm)) = thm + | thm_of_thm _ = error "thm_of_thm"; +fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); + +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); +fun thyID_of_derivation_name dn = hd (space_explode "." dn); + +fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) = + (strip_thy thmid1) = (strip_thy thmid2); +(*version typed weaker WN100910*) +fun eq_thmI' ((thmid1, _), (thmid2, _)) = + (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2); + + +val string_of_thm = Thm.get_name_hint; (*FIXME.2009*) +(*check for [.] as caused by "fun assoc_thm'"*) +fun string_of_thmI thm = + let val ct' = (de_quote o string_of_thm) thm + val (a, b) = split_nlast (5, Symbol.explode ct') + in case b of + [" ", " ","[", ".", "]"] => implode a + | _ => ct' + end; + +(*.id requested for all, Rls,Seq,Rrls.*) +fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*) + | id_rls (Rls {id,...}) = id + | id_rls (Seq {id,...}) = id + | id_rls (Rrls {id,...}) = id; +val rls2str = id_rls; +fun id_rule (Thm (id, _)) = id + | id_rule (Calc (id, _)) = id + | id_rule (Rls_ rls) = id_rls rls; + +fun get_rules (Rls {rules,...}) = rules + | get_rules (Seq {rules,...}) = rules + | get_rules (Rrls _) = []; + +fun rule2str Erule = "Erule" + | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")" + | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)" + | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)" + | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")"; +fun rule2str' Erule = "Erule" + | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")" + | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)" + | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)" + | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")"; + +(*WN080102 compare eq_rule ?!?*) +fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2 + | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2 + | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2 + | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*) + | eqrule _ = false; + + +type rrlsstate = (*state for reverse rewriting*) + (term * (*the current formula: + goes locate_gen -> next_tac via istate*) + term * (*the final formula*) + rule list (*of reverse rewrite set (#1#)*) + list * (*may be serveral, eg. in norm_rational*) + (rule * (*Thm (+ Thm generated from Calc) resulting in ...*) + (term * (*... rewrite with ...*) + term list)) (*... assumptions*) + list); (*derivation from given term to normalform + in reverse order with sym_thm; + (#1#) could be extracted from here #1*) +val e_type = Type("empty",[]); +val a_type = TFree("'a",[]); +val e_term = Const("empty",e_type); +val a_term = Free("empty",a_type); +val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate; + + + + +(*22.2.02: ging auf Linux nicht (Stefan) +val e_scr = Script ((term_of o the o (parse thy)) "e_script");*) +val e_term = Const("empty", Type("'a", [])); +val e_scr = Script e_term; + + +(*ad thm': + there are two kinds of theorems ... + (1) known by isabelle + (2) not known, eg. calc_thm, instantiated rls + the latter have a thmid "#..." + and thus outside isa we ALWAYS transport both (thmid,string_of_thmI) + and have a special assoc_thm / assoc_rls in this interface *) +type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*) +type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*) +type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*) + +fun string_of_thy thy = Context.theory_name thy: theory'; +val theory2domID = string_of_thy; +val theory2thyID = (get_thy o string_of_thy) : theory -> thyID; +val theory2theory' = string_of_thy; +val theory2str = string_of_thy; (*WN050903 ..most consistent naming*) +val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy; +(*> theory2str' (Thy_Info.get_theory "Isac"); +al it = "Isac" : string +*) + +fun thyID2theory' (thyID:thyID) = thyID; +(* + let val ss = Symbol.explode thyID + val ext = implode (takelast (4, ss)) + in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*) + else thyID ^ ".thy" + end; +*) +(* thyID2theory' "Isac" (*ok*); +val it = "Isac" : theory' + > thyID2theory' "Isac" (*abuse, goes ok...*); +val it = "Isac" : theory' +*) + +fun theory'2thyID (theory':theory') = theory'; +(* + let val ss = Symbol.explode theory' + val ext = implode (takelast (4, ss)) + in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID + else theory' (*disarm abuse of theory'*) + end; +*) +(* theory'2thyID "Isac"; +val it = "Isac" : thyID +> theory'2thyID "Isac"; +val it = "Isac" : thyID*) + + +(*. WN0509 discussion: +############################################################################# +# How to manage theorys in subproblems wrt. the requirement, # +# that scripts should be re-usable ? # +############################################################################# + + eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..' + which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script + because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b + is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard + (see match_ags). + + Preliminary solution: + # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically, + # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl + # however, a thy specified by the user in the rootpbl may lead to + errors in far-off subpbls (which are not yet reported properly !!!) + and interactively specifiying thys in subpbl is not very relevant. + + Other solutions possible: + # always parse and type-check with Thy_Info.get_theory "Isac" + (rejected tue to the vague idea eg. to re-use equations for R in C etc.) + # regard the subthy-relation in specifying thys of subpbls + # specifically handle 'SubProblem (undefined, pbl, arglist)' + # ??? +.*) +(*WN0509 TODO "ProtoPure" ... would be more consistent + with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*) +val e_domID = "e_domID":domID; + +(*the key into the hierarchy ob theory elements*) +type theID = string list; +val e_theID = ["e_theID"]; +val theID2str = strs2str; +(*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*) +fun theID2thyID (theID:theID) = + if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID + else error ("theID2thyID called with "^ theID2str theID); + +(*the key into the hierarchy ob problems*) +type pblID = string list; (* domID::...*) +val e_pblID = ["e_pblID"]:pblID; +val pblID2str = strs2str; + +(*the key into the hierarchy ob methods*) +type metID = string list; +val e_metID = ["e_metID"]:metID; +val metID2str = strs2str; + +(*either theID or pblID or metID*) +type kestoreID = string list; +val e_kestoreID = ["e_kestoreID"]; +val kestoreID2str = strs2str; + +(*for distinction of contexts*) +datatype ketype = Exp_ | Thy_ | Pbl_ | Met_; +fun ketype2str Exp_ = "Exp_" + | ketype2str Thy_ = "Thy_" + | ketype2str Pbl_ = "Pbl_" + | ketype2str Met_ = "Met_"; +fun ketype2str' Exp_ = "Example" + | ketype2str' Thy_ = "Theory" + | ketype2str' Pbl_ = "Problem" + | ketype2str' Met_ = "Method"; + +(*see 'How to manage theorys in subproblems' at 'type thyID'*) +val theory' = Unsynchronized.ref ([]:(theory' * theory) list); + +(*.all theories defined for Scripts, recorded in Scripts/Script.ML; + in order to distinguish them from general IsacKnowledge defined later on.*) +val script_thys = Unsynchronized.ref ([] : (theory' * theory) list); + + +(*rewrite orders, also stored in 'type met' and type 'and rls' + The association list is required for 'rewrite.."rew_ord"..' + WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*) +val rew_ord' = + Unsynchronized.ref + ([]:(rew_ord' * (*the key for the association list *) + (subst (*the bound variables - they get high order*) + -> (term * term) (*(t1, t2) to be compared *) + -> bool)) (*if t1 <= t2 then true else false *) + list); (*association list *) + +rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord), + ("dummy_ord", dummy_ord)]); + + +(*WN060120 a hack to get alltogether run again with minimal effort: + theory' is inserted for creating thy_hierarchy; calls for assoc_rls + need not be called*) +val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list); + +(*FIXME.040207 calclist': used by prep_rls, NOT in met*) +val calclist'= Unsynchronized.ref ([]: calc list); + +(*.the hierarchy of thydata.*) + +(*.'a is for pbt | met.*) +(*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*) +datatype 'a ptyp = + Ptyp of string * (*element within pblID*) + 'a list * (*several pbts with different domIDs/thy + TODO: select by subthy (isaref.p.69) + presently only _ONE_ elem*) + ('a ptyp) list; (*the children nodes*) + +(*.datatype for collecting thydata for hierarchy.*) +(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*) +(*WN0606 Htxt contains html which does not belong to the sml-kernel*) +datatype thydata = Html of {guh: guh, + coursedesign: authors, + mathauthors: authors, + html: string} (*html; for demos before database*) + | Hthm of {guh: guh, + coursedesign: authors, + mathauthors: authors, + thm: term} + | Hrls of {guh: guh, + coursedesign: authors, + mathauthors: authors, + (*like vvvvvvvvvvvvv val ruleset' + WN060711 redesign together !*) + thy_rls: (thyID * rls)} + | Hcal of {guh: guh, + coursedesign: authors, + mathauthors: authors, + calc: calc} + | Hord of {guh: guh, + coursedesign: authors, + mathauthors: authors, + ord: (subst -> (term * term) -> bool)}; +val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""}; + +type thehier = (thydata ptyp) list; +val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*) + +(* an association list, gets the value once in Isac.ML. + stores Isabelle's thms as terms for compatibility with Theory.axioms_of. + WN1-1-28 make this data arguments and del ref ?*) +val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list); + + +type path = string; +type filename = string; + +(*val xxx = fn: a b => (a,b); ??? fun-definition ???*) +local + fun ii (_:term) = e_rrlsstate; + fun no (_:term) = SOME (e_term,[e_term]); + fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))]; + fun ne (_:rule list list) (_:term) = SOME e_rule; + fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))]; +in +val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo, + next_rule=ne,attach_form=fo}; +end; + +val e_rls = + Rls{id = "e_rls", + preconds = [], + rew_ord = ("dummy_ord", dummy_ord), + erls = Erls,srls = Erls, + calc = [], + rules = [], scr = EmptyScr}:rls; +val e_rrls = Rrls {id = "e_rrls", + prepat = [], + rew_ord = ("dummy_ord", dummy_ord), + erls = Erls, + calc = [], + (*asm_thm=[],*) + scr=e_rfuns}:rls; +ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)), + ("e_rrls",("Tools",e_rrls)) + ]); + +fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) = + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc, + (*asm_thm=asm_thm,*)rules=rules,scr=scr} + | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) = + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc, + (*asm_thm=asm_thm,*)rules=rules,scr=scr} + | rep_rls Erls = rep_rls e_rls + | rep_rls (Rrls {id,...}) = rep_rls e_rls + (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*); +(*| rep_rls (Seq {id,...}) = + error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id); +--1.7.03*) +fun rep_rrls + (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord, + scr=Rfuns + {attach_form,init_state,locate_rule, + next_rule,normal_form}}) = + {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat, + rew_ord=rew_ord, attach_form=attach_form, init_state=init_state, + locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form} + | rep_rrls (Rls {id,...}) = + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id) + | rep_rrls (Seq {id,...}) = + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id); + +fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + rules =rs,scr=sc}) r = + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + rules = rs @ r,scr=sc}:rls) + | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + rules =rs,scr=sc}) r = + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + rules = rs @ r,scr=sc}:rls) + | append_rls id (Rrls _) _ = + error ("append_rls: not for reverse-rewrite-rule-set "^id); + +(*. are _atomic_ rules equal ?.*) +(*WN080102 compare eqrule ?!?*) +fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2 + | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2 + | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2 + (*id_rls checks for Rls, Seq, Rrls*) + | eq_rule _ = false; + +fun merge_rls _ Erls rls = rls + | merge_rls _ rls Erls = rls + | merge_rls id + (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1, + (*asm_thm=at1,*)rules =rs1,scr=sc1}) + (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2, + (*asm_thm=at2,*)rules =rs2,scr=sc2}) = + (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2), + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*), + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 + ((#srls o rep_rls) r2), + calc=ca1 @ ((#calc o rep_rls) r2), + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*) + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2), + scr=sc1}:rls) + | merge_rls id + (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1, + (*asm_thm=at1,*)rules =rs1,scr=sc1}) + (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2, + (*asm_thm=at2,*)rules =rs2,scr=sc2}) = + (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2), + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*), + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 + ((#srls o rep_rls) r2), + calc=ca1 @ ((#calc o rep_rls) r2), + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*) + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2), + scr=sc1}:rls) + | merge_rls _ _ _ = + error "merge_rls: not for reverse-rewrite-rule-sets\ + \and not for mixed Rls -- Seq"; +fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + (*asm_thm=at,*)rules =rs,scr=sc}) r = + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r), + scr=sc}:rls) + | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + (*asm_thm=at,*)rules =rs,scr=sc}) r = + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r), + scr=sc}:rls) + | remove_rls id (Rrls _) _ = error + ("remove_rls: not for reverse-rewrite-rule-set "^id); + +(*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]); +val it = [1, 2] : int list*) + +(*elder version: migrated 3 calls in smtest to memrls +fun mem_rls id rls = + case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of + SOME _ => true | NONE => false;*) +fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules) + | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules) + | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r)); +fun rls_get_thm rls (id: xstring) = + case find_first (curry eq_rule e_rule) + ((#rules o rep_rls) rls) of + SOME thm => SOME thm | NONE => NONE; + +fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known") + | assoc' ((keyi, xi) :: pairs, key) = + if key = keyi then SOME xi else assoc' (pairs, key); + +(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy)) + handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*) +fun assoc_thy (thy:theory') = + if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*) + else (Thy_Info.get_theory thy) + handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system"); + +(*.associate an rls-identifier with an rls; related to 'fun assoc_rls'; + these are NOT compatible to "fun assoc_thm'" in that they do NOT handle + overlays by re-using an identifier in different thys.*) +fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls)) + handle _ => error ("ME_Isa: '"^rls^"' not in system"); +(*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls)) + handle _ => error ("ME_Isa: '"^rls^"' not in system");*) + +(*.overwrite an element in an association list and pair it with a thyID + in order to create the thy_hierarchy; + overwrites existing rls' even if they are defined in a different thy; + this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*) +(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that + they do NOT handle overlays by re-using an identifier in different thys; + "thyID.rlsID" would be a good solution, if the "." would be possible + in scripts... + actually a hack to get alltogether run again with minimal effort*) +fun insthy thy' (rls', rls) = (rls', (thy', rls)); +fun overwritelthy thy (al, bl:(rls' * rls) list) = + let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl + in overwritel (al, bl') end; + +fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro)) + handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system"); +(*get the string for stac from rule*) +fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found") + | assoc_calc ((calc, (keyi, xi)) :: pairs, key) = + if key = keyi then calc else assoc_calc (pairs, key); +(*only used for !calclist'...*) +fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key + ^"' not found") + | assoc1 ((all as (keyi, _)) :: pairs, key) = + if key = keyi then all else assoc1 (pairs, key); + +(*TODO.WN080102 clarify usage of type cal and type calc..*) +fun calID2calcID (calID : calID) = + let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'") + | ass ((calci, (cali, eval_fn))::ids) = + if calID = cali then calci + else ass ids + in ass (!calclist') : calcID end; + +fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term +(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t; + +fun terms2str ts = (strs2str o (map term2str )) ts; +(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*) +fun terms2str' ts = (strs2str' o (map term2str )) ts; +(*terms2str' [t1,t2] = "[1 + 2,abc]";*) +fun terms2strs ts = (map term2str) ts; +(*terms2strs [t1,t2] = ["1 + 2", "abc"];*) + +fun termopt2str (SOME t) = "SOME " ^ term2str t + | termopt2str NONE = "NONE"; + +fun type2str typ = + Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ; +val string_of_typ = type2str; + +fun subst2str (s:subst) = + (strs2str o + (map (linefeed o pair2str o + (apsnd term2str) o + (apfst term2str)))) s; +fun subst2str' (s:subst) = + (strs2str' o + (map (pair2str o + (apsnd term2str) o + (apfst term2str)))) s; +(*> subst2str' [(str2term "bdv", str2term "x"), + (str2term "bdv_2", str2term "y")]; +val it = "[(bdv, x)]" : string +*) +val env2str = subst2str; + + +(*recursive defs:*) +fun scr2str (Script s) = "Script "^(term2str s) + | scr2str (Rfuns _) = "Rfuns"; + + +fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1; + + +(*.trace internal steps of isac's rewriter*) +val trace_rewrite = Unsynchronized.ref false; +(*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*) +val depth = Unsynchronized.ref 99999; +(*.no of rewrites exceeding this int -> NO rewrite.*) +(*WN060829 still unused...*) +val lim_rewrite = Unsynchronized.ref 99999; +(*.no of derivation-elements exceeding this int -> SOME derivation-elements.*) +val lim_deriv = Unsynchronized.ref 100; +(*.switch for checking guhs unique before storing a pbl or met; + set true at startup (done at begin of ROOT.ML) + set false for editing IsacKnowledge (done at end of ROOT.ML).*) +val check_guhs_unique = Unsynchronized.ref false; + + +datatype lrd = (*elements of a path (=loc_) into an Isabelle term*) + L (*go left at $*) + | R (*go right at $*) + | D; (*go down at Abs*) +type loc_ = lrd list; +fun ldr2str L = "L" + | ldr2str R = "R" + | ldr2str D = "D"; +fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k; + +(* +end (*struct*) +*) + +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/library.sml --- a/src/Tools/isac/library.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/library.sml Mon Feb 21 19:40:36 2011 +0100 @@ -174,7 +174,7 @@ let fun scan ss' [] = ss' | scan ss' ("\""::ss) = scan ss' ss | scan ss' (s::ss) = scan (ss' @ [s]) ss; - in (implode o (scan []) o explode) str end; + in (implode o (scan []) o Symbol.explode) str end; (*> de_quote "\"d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v\""; val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : string*) @@ -224,13 +224,13 @@ let fun get strl [] = strl | get strl ("."::ss) = strl | get strl ( s ::ss) = get (strl @ [s]) ss - in implode( get [] (explode str)) end; + in implode( get [] (Symbol.explode str)) end; fun strip_thy str = let fun strip bdVar [] = implode (rev bdVar) | strip bdVar ("."::_ ) = implode (rev bdVar) | strip bdVar (c ::cs) = strip (bdVar @[c]) cs - in strip [] (rev(explode str)) end; + in strip [] (rev(Symbol.explode str)) end; fun id_of (Var ((id,ix),_)) = if ix=0 then id else id^(string_of_int ix) | id_of (Free (id ,_)) = id @@ -326,14 +326,14 @@ | if_none (SOME x) _ = x; (* redirect tracing, following The Isabelle Cookbook *) -(* TODO: how redirect tracing to emacs buffer again ? *) +(* TODO: how redirect tracing to emacs buffer again ? val strip_specials = let fun strip ("\^A" :: _ :: cs) = strip cs | strip (c :: cs) = c :: strip cs | strip [] = []; in - implode o strip o explode + implode o strip o Symbol.explode end fun redir stream = Output.tracing_fn := (fn s => @@ -341,9 +341,10 @@ TextIO.output (stream, "\n"); TextIO.flushOut stream)); fun redirect_tracing path = redir (TextIO.openOut path); +WN110221-----*) fun compare_strs str1 str2 = let fun comp_char (c1, c2) = tracing ("comp_strs: " ^ c1 ^ " = " ^ c2 ^ " ..." ^ bool2str (c1 = c2)) - in map comp_char ((explode str1) ~~ (explode str2)) end; + in map comp_char ((Symbol.explode str1) ~~ (Symbol.explode str2)) end; diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/xmlsrc/datatypes.sml --- a/src/Tools/isac/xmlsrc/datatypes.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Mon Feb 21 19:40:36 2011 +0100 @@ -628,7 +628,7 @@ fun posformheads2xml j [] = ("":xml) | posformheads2xml j (r::rs) = posformhead2xml j r ^ posformheads2xml j rs; -val e_pblterm = (term_of o the o (parse (theory "Script"))) +val e_pblterm = (term_of o the o (parse (Thy_Info.get_theory "Script"))) ("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")"); (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*) @@ -666,7 +666,7 @@ *) fun theref2xml j (thyID:thyID) typ (xstring:xstring) = let val guh = theID2guh ["IsacKnowledge", thyID, typ, xstring] - val typ' = (implode o (drop_last_n 1) o explode) typ + val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ in indt j ^ "\n" ^ indt (j+i) ^ " " ^ typ' ^ " \n" ^ indt (j+i) ^ " " ^ xstring ^ " \n" ^ diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/xmlsrc/mathml.sml --- a/src/Tools/isac/xmlsrc/mathml.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/xmlsrc/mathml.sml Mon Feb 21 19:40:36 2011 +0100 @@ -24,7 +24,7 @@ | dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs) | dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs) | dec (c::cs) = c::(dec cs) - in (implode o dec o explode) str:cterm' end; + in (implode o dec o Symbol.explode) str:cterm' end; fun strs2xml strs = foldl (op ^) ("", strs); diff -r 7f4cfec6b910 -r 69364e021751 src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Tue Jan 11 15:28:03 2011 +0100 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Mon Feb 21 19:40:36 2011 +0100 @@ -108,7 +108,7 @@ str2term ("Problem (" ^ (get_thy o theory2domID) thy ^ "_, " ^ (strs2str' o rev) pblRD ^ ")"); -(* term2str (pbl2term (theory "Isac") ["equations","univariate","normalize"]); +(* term2str (pbl2term (Thy_Info.get_theory "Isac") ["equations","univariate","normalize"]); val it = "Problem (Isac, [normalize, univariate, equations])" : string *)