# HG changeset patch # User Walther Neuper # Date 1298989439 -3600 # Node ID b772eb34c16c0999afcb1dfd7054a79acf2a4e66 # Parent 0a36a8722b80d17008edca73887abe73e78af71c intermed.update to Isabelle2011: test/../syntax added present problem: test/Tools/isac/ADDTESTS/filed-depend does not update diff -r 0a36a8722b80 -r b772eb34c16c src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Sat Feb 26 12:53:00 2011 +0100 +++ b/src/Tools/isac/Build_Isac.thy Tue Mar 01 15:23:59 2011 +0100 @@ -19,64 +19,61 @@ header {* Loading the isac mathengine *} -theory Build_Isac -imports - Complex_Main - "ProgLang/ListC" - "ProgLang/Tools" - "ProgLang/Script" -(*"ProgLang/Language" - "Knowledge/Isac"*) +theory Build_Isac imports Complex_Main +(* use "library.sml" + use "calcelems.sml" + + use "ProgLang/termC.sml" + use "ProgLang/calculate.sml" + use "ProgLang/rewrite.sml" + "use_thy ProgLang/ListC" + "use_thy ProgLang/Tools" + "use_thy ProgLang/Script" + use "ProgLang/scrtools.sml" +*) "ProgLang/Language" + +(* use "Interpret/mstools.sml" + use "Interpret/ctree.sml" + use "Interpret/ptyps.sml" + use "Interpret/generate.sml" + use "Interpret/calchead.sml" + use "Interpret/appl.sml" + use "Interpret/rewtools.sml" + use "Interpret/script.sml" + use "Interpret/solve.sml" + use "Interpret/inform.sml" + use "Interpret/mathengine.sml" +*) "Interpret/Interpret" + +(* use "xmlsrc/mathml.sml" + use "xmlsrc/datatypes.sml" + use "xmlsrc/pbl-met-hierarchy.sml" + use "xmlsrc/thy-hierarchy.sml" + use "xmlsrc/interface-xml.sml" +*) "xmlsrc/xmlsrc" + +(* use "Frontend/messages.sml" + use "Frontend/states.sml" + use "Frontend/interface.sml" + + use "print_exn_G.sml" +*) "Frontend/Frontend" begin - -ML {* -tracing "**** build the isac kernel = math-engine + Knowledge ***********"; -tracing "**** build the math-engine *************************************" *} - -ML {* Toplevel.debug := true; *} -use "library.sml" -use "calcelems.sml" -ML {* check_guhs_unique := true *} - -use "ProgLang/termC.sml" -use "ProgLang/calculate.sml" -use "ProgLang/rewrite.sml" - -use_thy "ProgLang/ListC" -use_thy"ProgLang/Tools" -use_thy"ProgLang/Script" (*ListC, Tools, Script*) -use "ProgLang/scrtools.sml" -use_thy"ProgLang/Language" (*just for integrating scrtools.sml*) - -use "Interpret/mstools.sml" -use "Interpret/ctree.sml" -use "Interpret/ptyps.sml" -use "Interpret/generate.sml" -use "Interpret/calchead.sml" -use "Interpret/appl.sml" -use "Interpret/rewtools.sml" -use "Interpret/script.sml" -use "Interpret/solve.sml" -use "Interpret/inform.sml" -use "Interpret/mathengine.sml" - -use "xmlsrc/mathml.sml" -use "xmlsrc/datatypes.sml" -use "xmlsrc/pbl-met-hierarchy.sml" -use "xmlsrc/thy-hierarchy.sml" -use "xmlsrc/interface-xml.sml" - -use "Frontend/messages.sml" -use "Frontend/states.sml" -use "Frontend/interface.sml" - -use "print_exn_G.sml" -ML {* tracing "**** build math-engine complete **************************" *} +ML {* is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *} +ML {* me; (*from "Interpret/mathengine.sml"*) *} +ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *} +ML {* print_exn_unit *} +ML {*1*} ML {* tracing "**** build the Knowledge *********************************" *} -(*use_thy "Knowledge/Delete" +(**) +use_thy "Knowledge/Delete" use_thy "Knowledge/Descript" use_thy "Knowledge/Atools" +ML {* list_rls (*from Atools.thy*) *} +ML {* eval_occurs_in (*from Atools.thy*) *} +ML {* @{thm last_thmI} (*from Atools.thy*) *} + use_thy "Knowledge/Simplify" use_thy "Knowledge/Poly" use_thy "Knowledge/Rational" @@ -99,7 +96,11 @@ use_thy "Knowledge/EqSystem" use_thy "Knowledge/Biegelinie" use_thy "Knowledge/AlgEin" -*) + +ML {* +@{thm Querkraft_Belastung} +*} + use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*) use_thy "Knowledge/Isac" diff -r 0a36a8722b80 -r b772eb34c16c src/Tools/isac/Frontend/Frontend.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Frontend/Frontend.thy Tue Mar 01 15:23:59 2011 +0100 @@ -0,0 +1,17 @@ +(* Title: collect all defitions for the Frontend + Author: Walther Neuper 110226 + (c) due to copyright terms + *) + +theory Frontend imports xmlsrc + uses ("messages.sml") ("states.sml") ("interface.sml") + ("../print_exn_G.sml") +begin + + use "messages.sml" + use "states.sml" + use "interface.sml" + + use "../print_exn_G.sml" + +end \ No newline at end of file diff -r 0a36a8722b80 -r b772eb34c16c src/Tools/isac/Interpret/Interpret.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Interpret/Interpret.thy Tue Mar 01 15:23:59 2011 +0100 @@ -0,0 +1,24 @@ +(* Title: collect all defitions for the Lucas-Interpreter + Author: Walther Neuper 110226 + (c) due to copyright terms + *) + +theory Interpret imports Language + uses ("mstools.sml") ("ctree.sml") ("ptyps.sml") ("generate.sml") + ("calchead.sml") ("appl.sml") ("rewtools.sml") ("script.sml") + ("solve.sml") ("inform.sml") ("mathengine.sml") +begin + + use "mstools.sml" + use "ctree.sml" + use "ptyps.sml" + use "generate.sml" + use "calchead.sml" + use "appl.sml" + use "rewtools.sml" + use "script.sml" + use "solve.sml" + use "inform.sml" + use "mathengine.sml" + +end \ No newline at end of file diff -r 0a36a8722b80 -r b772eb34c16c src/Tools/isac/Interpret/calchead.sml --- a/src/Tools/isac/Interpret/calchead.sml Sat Feb 26 12:53:00 2011 +0100 +++ b/src/Tools/isac/Interpret/calchead.sml Tue Mar 01 15:23:59 2011 +0100 @@ -711,7 +711,7 @@ fun test_types thy (d,ts) = let - val s = !show_types; val _ = show_types:= true; + (*val s = !show_types; val _ = show_types:= true;*) val opt = (try (comp_dts thy)) (d,ts); val msg = case opt of SOME _ => "" @@ -720,7 +720,7 @@ ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)))) ts) ^ " is illtyped"); - val _ = show_types:= s + (*val _ = show_types:= s*) in msg end; @@ -887,7 +887,9 @@ ^"*** typeconstructor in script: "^(term_detail2str ty) ^"*** checked by theory: "^(theory2str thy)^"\n" ^"*** " ^ dots 66); - OldGoals.print_exn e; (*raises exn again*) + (*OldGoals.print_exn e; raises exn again*) + writeln (PolyML.makestring e); + reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*) NONE); @@ -961,8 +963,8 @@ (*.report part of the error-msg which is not available in match_args.*) fun match_ags_msg pI stac ags = - let val s = !show_types - val _ = show_types:= true + let (*val s = !show_types + val _ = show_types:= true*) val pats = (#ppc o get_pbt) pI val msg = (dots 70^"\n" ^"*** problem "^strs2str pI^" has the ...\n" @@ -971,7 +973,7 @@ ^"*** arg-list "^terms2str ags^"\n" ^dashs 70) (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*) - val _ = show_types:= s + (*val _ = show_types:= s*) in tracing msg end; diff -r 0a36a8722b80 -r b772eb34c16c src/Tools/isac/Interpret/mstools.sml --- a/src/Tools/isac/Interpret/mstools.sml Sat Feb 26 12:53:00 2011 +0100 +++ b/src/Tools/isac/Interpret/mstools.sml Tue Mar 01 15:23:59 2011 +0100 @@ -570,10 +570,10 @@ "("^(string_of_int i)^", "^((strs2str o (map string_of_int)) vs)^", "^fi^","^ (term2str t)^", "^((strs2str o (map term2str)) ts)^")"; val oris2str = - let val s = !show_types - val _ = show_types:= true + let (*val s = !show_types + val _ = show_types:= true*) val str = (strs2str' o (map (linefeed o ori2str))) - val _ = show_types:= s + (*val _ = show_types:= s*) in str end; (*.an or without leading integer.*) diff -r 0a36a8722b80 -r b772eb34c16c src/Tools/isac/Knowledge/Atools.thy --- a/src/Tools/isac/Knowledge/Atools.thy Sat Feb 26 12:53:00 2011 +0100 +++ b/src/Tools/isac/Knowledge/Atools.thy Tue Mar 01 15:23:59 2011 +0100 @@ -6,40 +6,45 @@ 10 20 30 40 50 60 70 80 *) -theory Atools imports Descript -uses ("Interpret/mstools.sml")("Interpret/ctree.sml")("Interpret/ptyps.sml") -("Interpret/generate.sml")("Interpret/calchead.sml")("Interpret/appl.sml") -("Interpret/rewtools.sml")("Interpret/script.sml")("Interpret/solve.sml") -("Interpret/inform.sml")("Interpret/mathengine.sml") -("xmlsrc/mathml.sml")("xmlsrc/datatypes.sml")("xmlsrc/pbl-met-hierarchy.sml") -("xmlsrc/thy-hierarchy.sml")("xmlsrc/interface-xml.sml") -("Frontend/messages.sml")("Frontend/states.sml")("Frontend/interface.sml") -("print_exn_G.sml") +theory Atools imports Descript "../Interpret/Interpret" +(* +uses ("../Interpret/mstools.sml")("../Interpret/ctree.sml") +("../Interpret/ptyps.sml")("../Interpret/generate.sml") +("../Interpret/calchead.sml")("../Interpret/appl.sml") +("../Interpret/rewtools.sml")("../Interpret/script.sml") +("../Interpret/solve.sml")("../Interpret/inform.sml") +("../Interpret/mathengine.sml")("../xmlsrc/mathml.sml") +("../xmlsrc/datatypes.sml")("../xmlsrc/pbl-met-hierarchy.sml") +("../xmlsrc/thy-hierarchy.sml")("../xmlsrc/interface-xml.sml") +("../Frontend/messages.sml")("../Frontend/states.sml") +("../Frontend/interface.sml")("../print_exn_G.sml") +*) begin -use "Interpret/mstools.sml" -use "Interpret/ctree.sml" -use "Interpret/ptyps.sml" (*^^^ need files for: fun prep_pbt, fun store_pbt*) -use "Interpret/generate.sml" -use "Interpret/calchead.sml" -use "Interpret/appl.sml" -use "Interpret/rewtools.sml" -use "Interpret/script.sml" -use "Interpret/solve.sml" -use "Interpret/inform.sml" (*^^^ need files for: fun castab*) -use "Interpret/mathengine.sml" +(* +use "../Interpret/mstools.sml" +use "../Interpret/ctree.sml" +use "../Interpret/ptyps.sml" (*^^^ need for: fun prep_pbt, fun store_pbt*) +use "../Interpret/generate.sml" +use "../Interpret/calchead.sml" +use "../Interpret/appl.sml" +use "../Interpret/rewtools.sml" +use "../Interpret/script.sml" +use "../Interpret/solve.sml" +use "../Interpret/inform.sml" (*^^^ need files for: fun castab*) +use "../Interpret/mathengine.sml" -use "xmlsrc/mathml.sml" -use "xmlsrc/datatypes.sml" -use "xmlsrc/pbl-met-hierarchy.sml" -use "xmlsrc/thy-hierarchy.sml" (*^^^ need files for: fun store_isa*) -use "xmlsrc/interface-xml.sml" +use "../xmlsrc/mathml.sml" +use "../xmlsrc/datatypes.sml" +use "../xmlsrc/pbl-met-hierarchy.sml" +use "../xmlsrc/thy-hierarchy.sml" (*^^^ need files for: fun store_isa*) +use "../xmlsrc/interface-xml.sml" -use "Frontend/messages.sml" -use "Frontend/states.sml" (*^^^ need files for: val states in Test_Isac.thy*) -use "Frontend/interface.sml" +use "../Frontend/messages.sml" +use "../Frontend/states.sml" (*^^^ need for: val states in Test_Isac.thy*) +use "../Frontend/interface.sml" -use "print_exn_G.sml" - +use "../print_exn_G.sml" +*) consts Arbfix :: "real" diff -r 0a36a8722b80 -r b772eb34c16c src/Tools/isac/Knowledge/DiffApp.thy --- a/src/Tools/isac/Knowledge/DiffApp.thy Sat Feb 26 12:53:00 2011 +0100 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Tue Mar 01 15:23:59 2011 +0100 @@ -31,7 +31,7 @@ (*primrec*)axioms filterVar_Nil: "filterVar v [] = []" filterVar_Const: "filterVar v (x#xs) = - (if (v mem (Vars x)) then x#(filterVar v xs) + (if (v : set (Vars x)) then x#(filterVar v xs) else filterVar v xs) " text {*WN.6.5.03: old decisions in this file partially are being changed in a quick-and-dirty way to make scripts run: Maximum_value, diff -r 0a36a8722b80 -r b772eb34c16c src/Tools/isac/ProgLang/Language.thy --- a/src/Tools/isac/ProgLang/Language.thy Sat Feb 26 12:53:00 2011 +0100 +++ b/src/Tools/isac/ProgLang/Language.thy Tue Mar 01 15:23:59 2011 +0100 @@ -4,7 +4,7 @@ *) theory Language imports Script -uses ("../ProgLang/scrtools.sml") + uses ("../ProgLang/scrtools.sml") begin use "../ProgLang/scrtools.sml" diff -r 0a36a8722b80 -r b772eb34c16c src/Tools/isac/ProgLang/ListC.thy --- a/src/Tools/isac/ProgLang/ListC.thy Sat Feb 26 12:53:00 2011 +0100 +++ b/src/Tools/isac/ProgLang/ListC.thy Tue Mar 01 15:23:59 2011 +0100 @@ -197,6 +197,4 @@ [("list_rls",list_rls) ]); *} -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) end diff -r 0a36a8722b80 -r b772eb34c16c src/Tools/isac/calcelems.sml --- a/src/Tools/isac/calcelems.sml Sat Feb 26 12:53:00 2011 +0100 +++ b/src/Tools/isac/calcelems.sml Tue Mar 01 15:23:59 2011 +0100 @@ -665,7 +665,7 @@ (*.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; +val check_guhs_unique = Unsynchronized.ref true; datatype lrd = (*elements of a path (=loc_) into an Isabelle term*) @@ -681,1086 +681,3 @@ (* 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*) -*) diff -r 0a36a8722b80 -r b772eb34c16c src/Tools/isac/xmlsrc/xmlsrc.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/xmlsrc/xmlsrc.thy Tue Mar 01 15:23:59 2011 +0100 @@ -0,0 +1,17 @@ +(* Title: collect all defitions for xml generation + Author: Walther Neuper 110226 + (c) due to copyright terms +*) + +theory xmlsrc imports Interpret + uses ("mathml.sml") ("datatypes.sml") ("pbl-met-hierarchy.sml") + ("thy-hierarchy.sml") ("interface-xml.sml") +begin + + use "mathml.sml" + use "datatypes.sml" + use "pbl-met-hierarchy.sml" + use "thy-hierarchy.sml" + use "interface-xml.sml" + +end \ No newline at end of file diff -r 0a36a8722b80 -r b772eb34c16c test/Pure/Syntax/syntax.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Pure/Syntax/syntax.thy Tue Mar 01 15:23:59 2011 +0100 @@ -0,0 +1,34 @@ +theory syntaxe imports Main begin + +section {* Old parsing *} +text {* Old parsing in ISAC used theories *} +ML {* +val thy = @{theory}; +fun parse thy str = Syntax.read_term_global thy str; +val env = + [(parse thy "equ::bool", parse thy "x + (1::int) = 2"), + (parse thy "var::int", parse thy "x::int"), + (parse thy "sol::bool", parse thy "(x::int) = 1") + ]; +val precond = parse thy "(0::int) < x" +*} +text {* However, user input could not be parsed ...*} +ML {* parse thy "x = 2 - 1" *} +text {* ... because the type 'int' is lost (we have type 'a now). + The learner would need to input x::int all the time. *} + +section {* Contexts *} +ML {* +val ctxt = ProofContext.init_global thy; + +(*... prepare ctxt ...*) + +fun parseNEW ctxt str = Syntax.read_term ctxt str; +*} + +section {* New parsing *} +text {* New parsing in ISAC uses contexts, which are rigorously updated + by the Lucas-Interpreter. Then ...*} +ML {* parse thy "x = 2 - 1" *} +text {* ... x gets type 'int' from the context. *} +end diff -r 0a36a8722b80 -r b772eb34c16c test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML --- a/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML Sat Feb 26 12:53:00 2011 +0100 +++ b/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML Tue Mar 01 15:23:59 2011 +0100 @@ -3,7 +3,9 @@ fun foointerpret ((Const ("Foo_Language.fooprog", _)) $ (_ $ _ $ res)) = res; (* Foo_Language's definitions are recognized: *) -val trm = Syntax.read_term_global @{theory Foo_Language} "fooprog (a = b)"; +(*val trm = Syntax.read_term_global @{theory Foo_Language} "fooprog (a = b)"; *) +val trm = Syntax.read_term_global @{theory "../1language/Foo_Language"} + "fooprog (a = b)"; (*val trm = Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $ (Const ("op =", "'a => 'a => bool") $ Free ("a", "'a") $ diff -r 0a36a8722b80 -r b772eb34c16c test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy --- a/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy Sat Feb 26 12:53:00 2011 +0100 +++ b/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy Tue Mar 01 15:23:59 2011 +0100 @@ -1,25 +1,36 @@ -(* +(* Title: test/Tools/isac/ADDTESTS/file-depend + Author: Walther Neuper +*) + +header {* Test file dependencies analogous to ISAC + $ cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/file-depend $ /usr/local/Isabelle/bin/isabelle emacs Build_Test.thy & - -*) - +*} +(*---------------------------------------------------------------------------- theory Build_Test imports Complex_Main "1language/Foo_Language" "3knowledge/Foo_KnowALL" begin +----------------------------------------------------------------------------*) -use "0foolibrary.ML" -use_thy "1language/Foo_Language" -use "2interpreter/2foointerpreter.ML" +theory Build_Test +imports + Complex_Main +begin + use "0foolibrary.ML" ML {* foolibrhs *} + use_thy "1language/Foo_Language" (*ML {* @{const fooprog} *}*) + use "2interpreter/2foointerpreter.ML" ML {* foointerpret *} -(*vvvvvvv can be bypassed with Foo_KnowALL -use_thy "3knowledge/Foo_Know111" -use_thy "3knowledge/Foo_Know222" - ^^^^^^^ can be bypassed with Foo_KnowALL*) -use_thy "3knowledge/Foo_KnowALL" +text {* The top 'theory ... begin' can be outcommended and done stepwise: + + use "2interpreter/2foointerpreter.ML" + use_thy "3knowledge/Foo_Know111" + use_thy "3knowledge/Foo_Know222" + use_thy "3knowledge/Foo_KnowALL" +*} text {* the different theories of knowledge are recognized, Const bar*: *} ML {* @@ -48,4 +59,18 @@ (Const ("op =", "'a => 'a => bool") $ Free ("foo111", "'a") $ Free ("bar111", "'a")) : term*) +*} + +text {* dir structure reflects ISAC, see Build_Isac.thy: +/file-depend/0foolibrary.ML +/file-depend/Build_Test.thy +/file-depend/README + +/file-depend/1language/Foo_Language.thy + +/file-depend/2interpreter/2foointerpreter.ML + +/file-depend/3knowledge/Foo_Know111.thy +/file-depend/3knowledge/Foo_Know222.thy +/file-depend/3knowledge/Foo_KnowALL.thy *} \ No newline at end of file