1.1 --- a/src/Tools/isac/Build_Isac.thy Sat Feb 26 12:53:00 2011 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Mar 01 15:23:59 2011 +0100
1.3 @@ -19,64 +19,61 @@
1.4
1.5 header {* Loading the isac mathengine *}
1.6
1.7 -theory Build_Isac
1.8 -imports
1.9 - Complex_Main
1.10 - "ProgLang/ListC"
1.11 - "ProgLang/Tools"
1.12 - "ProgLang/Script"
1.13 -(*"ProgLang/Language"
1.14 - "Knowledge/Isac"*)
1.15 +theory Build_Isac imports Complex_Main
1.16 +(* use "library.sml"
1.17 + use "calcelems.sml"
1.18 +
1.19 + use "ProgLang/termC.sml"
1.20 + use "ProgLang/calculate.sml"
1.21 + use "ProgLang/rewrite.sml"
1.22 + "use_thy ProgLang/ListC"
1.23 + "use_thy ProgLang/Tools"
1.24 + "use_thy ProgLang/Script"
1.25 + use "ProgLang/scrtools.sml"
1.26 +*) "ProgLang/Language"
1.27 +
1.28 +(* use "Interpret/mstools.sml"
1.29 + use "Interpret/ctree.sml"
1.30 + use "Interpret/ptyps.sml"
1.31 + use "Interpret/generate.sml"
1.32 + use "Interpret/calchead.sml"
1.33 + use "Interpret/appl.sml"
1.34 + use "Interpret/rewtools.sml"
1.35 + use "Interpret/script.sml"
1.36 + use "Interpret/solve.sml"
1.37 + use "Interpret/inform.sml"
1.38 + use "Interpret/mathengine.sml"
1.39 +*) "Interpret/Interpret"
1.40 +
1.41 +(* use "xmlsrc/mathml.sml"
1.42 + use "xmlsrc/datatypes.sml"
1.43 + use "xmlsrc/pbl-met-hierarchy.sml"
1.44 + use "xmlsrc/thy-hierarchy.sml"
1.45 + use "xmlsrc/interface-xml.sml"
1.46 +*) "xmlsrc/xmlsrc"
1.47 +
1.48 +(* use "Frontend/messages.sml"
1.49 + use "Frontend/states.sml"
1.50 + use "Frontend/interface.sml"
1.51 +
1.52 + use "print_exn_G.sml"
1.53 +*) "Frontend/Frontend"
1.54 begin
1.55 -
1.56 -ML {*
1.57 -tracing "**** build the isac kernel = math-engine + Knowledge ***********";
1.58 -tracing "**** build the math-engine *************************************" *}
1.59 -
1.60 -ML {* Toplevel.debug := true; *}
1.61 -use "library.sml"
1.62 -use "calcelems.sml"
1.63 -ML {* check_guhs_unique := true *}
1.64 -
1.65 -use "ProgLang/termC.sml"
1.66 -use "ProgLang/calculate.sml"
1.67 -use "ProgLang/rewrite.sml"
1.68 -
1.69 -use_thy "ProgLang/ListC"
1.70 -use_thy"ProgLang/Tools"
1.71 -use_thy"ProgLang/Script" (*ListC, Tools, Script*)
1.72 -use "ProgLang/scrtools.sml"
1.73 -use_thy"ProgLang/Language" (*just for integrating scrtools.sml*)
1.74 -
1.75 -use "Interpret/mstools.sml"
1.76 -use "Interpret/ctree.sml"
1.77 -use "Interpret/ptyps.sml"
1.78 -use "Interpret/generate.sml"
1.79 -use "Interpret/calchead.sml"
1.80 -use "Interpret/appl.sml"
1.81 -use "Interpret/rewtools.sml"
1.82 -use "Interpret/script.sml"
1.83 -use "Interpret/solve.sml"
1.84 -use "Interpret/inform.sml"
1.85 -use "Interpret/mathengine.sml"
1.86 -
1.87 -use "xmlsrc/mathml.sml"
1.88 -use "xmlsrc/datatypes.sml"
1.89 -use "xmlsrc/pbl-met-hierarchy.sml"
1.90 -use "xmlsrc/thy-hierarchy.sml"
1.91 -use "xmlsrc/interface-xml.sml"
1.92 -
1.93 -use "Frontend/messages.sml"
1.94 -use "Frontend/states.sml"
1.95 -use "Frontend/interface.sml"
1.96 -
1.97 -use "print_exn_G.sml"
1.98 -ML {* tracing "**** build math-engine complete **************************" *}
1.99 +ML {* is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
1.100 +ML {* me; (*from "Interpret/mathengine.sml"*) *}
1.101 +ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *}
1.102 +ML {* print_exn_unit *}
1.103 +ML {*1*}
1.104
1.105 ML {* tracing "**** build the Knowledge *********************************" *}
1.106 -(*use_thy "Knowledge/Delete"
1.107 +(**)
1.108 +use_thy "Knowledge/Delete"
1.109 use_thy "Knowledge/Descript"
1.110 use_thy "Knowledge/Atools"
1.111 +ML {* list_rls (*from Atools.thy*) *}
1.112 +ML {* eval_occurs_in (*from Atools.thy*) *}
1.113 +ML {* @{thm last_thmI} (*from Atools.thy*) *}
1.114 +
1.115 use_thy "Knowledge/Simplify"
1.116 use_thy "Knowledge/Poly"
1.117 use_thy "Knowledge/Rational"
1.118 @@ -99,7 +96,11 @@
1.119 use_thy "Knowledge/EqSystem"
1.120 use_thy "Knowledge/Biegelinie"
1.121 use_thy "Knowledge/AlgEin"
1.122 -*)
1.123 +
1.124 +ML {*
1.125 +@{thm Querkraft_Belastung}
1.126 +*}
1.127 +
1.128 use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*)
1.129 use_thy "Knowledge/Isac"
1.130
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Tools/isac/Frontend/Frontend.thy Tue Mar 01 15:23:59 2011 +0100
2.3 @@ -0,0 +1,17 @@
2.4 +(* Title: collect all defitions for the Frontend
2.5 + Author: Walther Neuper 110226
2.6 + (c) due to copyright terms
2.7 + *)
2.8 +
2.9 +theory Frontend imports xmlsrc
2.10 + uses ("messages.sml") ("states.sml") ("interface.sml")
2.11 + ("../print_exn_G.sml")
2.12 +begin
2.13 +
2.14 + use "messages.sml"
2.15 + use "states.sml"
2.16 + use "interface.sml"
2.17 +
2.18 + use "../print_exn_G.sml"
2.19 +
2.20 +end
2.21 \ No newline at end of file
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Tue Mar 01 15:23:59 2011 +0100
3.3 @@ -0,0 +1,24 @@
3.4 +(* Title: collect all defitions for the Lucas-Interpreter
3.5 + Author: Walther Neuper 110226
3.6 + (c) due to copyright terms
3.7 + *)
3.8 +
3.9 +theory Interpret imports Language
3.10 + uses ("mstools.sml") ("ctree.sml") ("ptyps.sml") ("generate.sml")
3.11 + ("calchead.sml") ("appl.sml") ("rewtools.sml") ("script.sml")
3.12 + ("solve.sml") ("inform.sml") ("mathengine.sml")
3.13 +begin
3.14 +
3.15 + use "mstools.sml"
3.16 + use "ctree.sml"
3.17 + use "ptyps.sml"
3.18 + use "generate.sml"
3.19 + use "calchead.sml"
3.20 + use "appl.sml"
3.21 + use "rewtools.sml"
3.22 + use "script.sml"
3.23 + use "solve.sml"
3.24 + use "inform.sml"
3.25 + use "mathengine.sml"
3.26 +
3.27 +end
3.28 \ No newline at end of file
4.1 --- a/src/Tools/isac/Interpret/calchead.sml Sat Feb 26 12:53:00 2011 +0100
4.2 +++ b/src/Tools/isac/Interpret/calchead.sml Tue Mar 01 15:23:59 2011 +0100
4.3 @@ -711,7 +711,7 @@
4.4
4.5 fun test_types thy (d,ts) =
4.6 let
4.7 - val s = !show_types; val _ = show_types:= true;
4.8 + (*val s = !show_types; val _ = show_types:= true;*)
4.9 val opt = (try (comp_dts thy)) (d,ts);
4.10 val msg = case opt of
4.11 SOME _ => ""
4.12 @@ -720,7 +720,7 @@
4.13 ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
4.14 (thy2ctxt thy)))) ts)
4.15 ^ " is illtyped");
4.16 - val _ = show_types:= s
4.17 + (*val _ = show_types:= s*)
4.18 in msg end;
4.19
4.20
4.21 @@ -887,7 +887,9 @@
4.22 ^"*** typeconstructor in script: "^(term_detail2str ty)
4.23 ^"*** checked by theory: "^(theory2str thy)^"\n"
4.24 ^"*** " ^ dots 66);
4.25 - OldGoals.print_exn e; (*raises exn again*)
4.26 + (*OldGoals.print_exn e; raises exn again*)
4.27 + writeln (PolyML.makestring e);
4.28 + reraise e;
4.29 (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
4.30 NONE);
4.31
4.32 @@ -961,8 +963,8 @@
4.33
4.34 (*.report part of the error-msg which is not available in match_args.*)
4.35 fun match_ags_msg pI stac ags =
4.36 - let val s = !show_types
4.37 - val _ = show_types:= true
4.38 + let (*val s = !show_types
4.39 + val _ = show_types:= true*)
4.40 val pats = (#ppc o get_pbt) pI
4.41 val msg = (dots 70^"\n"
4.42 ^"*** problem "^strs2str pI^" has the ...\n"
4.43 @@ -971,7 +973,7 @@
4.44 ^"*** arg-list "^terms2str ags^"\n"
4.45 ^dashs 70)
4.46 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
4.47 - val _ = show_types:= s
4.48 + (*val _ = show_types:= s*)
4.49 in tracing msg end;
4.50
4.51
5.1 --- a/src/Tools/isac/Interpret/mstools.sml Sat Feb 26 12:53:00 2011 +0100
5.2 +++ b/src/Tools/isac/Interpret/mstools.sml Tue Mar 01 15:23:59 2011 +0100
5.3 @@ -570,10 +570,10 @@
5.4 "("^(string_of_int i)^", "^((strs2str o (map string_of_int)) vs)^", "^fi^","^
5.5 (term2str t)^", "^((strs2str o (map term2str)) ts)^")";
5.6 val oris2str =
5.7 - let val s = !show_types
5.8 - val _ = show_types:= true
5.9 + let (*val s = !show_types
5.10 + val _ = show_types:= true*)
5.11 val str = (strs2str' o (map (linefeed o ori2str)))
5.12 - val _ = show_types:= s
5.13 + (*val _ = show_types:= s*)
5.14 in str end;
5.15
5.16 (*.an or without leading integer.*)
6.1 --- a/src/Tools/isac/Knowledge/Atools.thy Sat Feb 26 12:53:00 2011 +0100
6.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Tue Mar 01 15:23:59 2011 +0100
6.3 @@ -6,40 +6,45 @@
6.4 10 20 30 40 50 60 70 80
6.5 *)
6.6
6.7 -theory Atools imports Descript
6.8 -uses ("Interpret/mstools.sml")("Interpret/ctree.sml")("Interpret/ptyps.sml")
6.9 -("Interpret/generate.sml")("Interpret/calchead.sml")("Interpret/appl.sml")
6.10 -("Interpret/rewtools.sml")("Interpret/script.sml")("Interpret/solve.sml")
6.11 -("Interpret/inform.sml")("Interpret/mathengine.sml")
6.12 -("xmlsrc/mathml.sml")("xmlsrc/datatypes.sml")("xmlsrc/pbl-met-hierarchy.sml")
6.13 -("xmlsrc/thy-hierarchy.sml")("xmlsrc/interface-xml.sml")
6.14 -("Frontend/messages.sml")("Frontend/states.sml")("Frontend/interface.sml")
6.15 -("print_exn_G.sml")
6.16 +theory Atools imports Descript "../Interpret/Interpret"
6.17 +(*
6.18 +uses ("../Interpret/mstools.sml")("../Interpret/ctree.sml")
6.19 +("../Interpret/ptyps.sml")("../Interpret/generate.sml")
6.20 +("../Interpret/calchead.sml")("../Interpret/appl.sml")
6.21 +("../Interpret/rewtools.sml")("../Interpret/script.sml")
6.22 +("../Interpret/solve.sml")("../Interpret/inform.sml")
6.23 +("../Interpret/mathengine.sml")("../xmlsrc/mathml.sml")
6.24 +("../xmlsrc/datatypes.sml")("../xmlsrc/pbl-met-hierarchy.sml")
6.25 +("../xmlsrc/thy-hierarchy.sml")("../xmlsrc/interface-xml.sml")
6.26 +("../Frontend/messages.sml")("../Frontend/states.sml")
6.27 +("../Frontend/interface.sml")("../print_exn_G.sml")
6.28 +*)
6.29 begin
6.30 -use "Interpret/mstools.sml"
6.31 -use "Interpret/ctree.sml"
6.32 -use "Interpret/ptyps.sml" (*^^^ need files for: fun prep_pbt, fun store_pbt*)
6.33 -use "Interpret/generate.sml"
6.34 -use "Interpret/calchead.sml"
6.35 -use "Interpret/appl.sml"
6.36 -use "Interpret/rewtools.sml"
6.37 -use "Interpret/script.sml"
6.38 -use "Interpret/solve.sml"
6.39 -use "Interpret/inform.sml" (*^^^ need files for: fun castab*)
6.40 -use "Interpret/mathengine.sml"
6.41 +(*
6.42 +use "../Interpret/mstools.sml"
6.43 +use "../Interpret/ctree.sml"
6.44 +use "../Interpret/ptyps.sml" (*^^^ need for: fun prep_pbt, fun store_pbt*)
6.45 +use "../Interpret/generate.sml"
6.46 +use "../Interpret/calchead.sml"
6.47 +use "../Interpret/appl.sml"
6.48 +use "../Interpret/rewtools.sml"
6.49 +use "../Interpret/script.sml"
6.50 +use "../Interpret/solve.sml"
6.51 +use "../Interpret/inform.sml" (*^^^ need files for: fun castab*)
6.52 +use "../Interpret/mathengine.sml"
6.53
6.54 -use "xmlsrc/mathml.sml"
6.55 -use "xmlsrc/datatypes.sml"
6.56 -use "xmlsrc/pbl-met-hierarchy.sml"
6.57 -use "xmlsrc/thy-hierarchy.sml" (*^^^ need files for: fun store_isa*)
6.58 -use "xmlsrc/interface-xml.sml"
6.59 +use "../xmlsrc/mathml.sml"
6.60 +use "../xmlsrc/datatypes.sml"
6.61 +use "../xmlsrc/pbl-met-hierarchy.sml"
6.62 +use "../xmlsrc/thy-hierarchy.sml" (*^^^ need files for: fun store_isa*)
6.63 +use "../xmlsrc/interface-xml.sml"
6.64
6.65 -use "Frontend/messages.sml"
6.66 -use "Frontend/states.sml" (*^^^ need files for: val states in Test_Isac.thy*)
6.67 -use "Frontend/interface.sml"
6.68 +use "../Frontend/messages.sml"
6.69 +use "../Frontend/states.sml" (*^^^ need for: val states in Test_Isac.thy*)
6.70 +use "../Frontend/interface.sml"
6.71
6.72 -use "print_exn_G.sml"
6.73 -
6.74 +use "../print_exn_G.sml"
6.75 +*)
6.76 consts
6.77
6.78 Arbfix :: "real"
7.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Sat Feb 26 12:53:00 2011 +0100
7.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Tue Mar 01 15:23:59 2011 +0100
7.3 @@ -31,7 +31,7 @@
7.4 (*primrec*)axioms
7.5 filterVar_Nil: "filterVar v [] = []"
7.6 filterVar_Const: "filterVar v (x#xs) =
7.7 - (if (v mem (Vars x)) then x#(filterVar v xs)
7.8 + (if (v : set (Vars x)) then x#(filterVar v xs)
7.9 else filterVar v xs) "
7.10 text {*WN.6.5.03: old decisions in this file partially are being changed
7.11 in a quick-and-dirty way to make scripts run: Maximum_value,
8.1 --- a/src/Tools/isac/ProgLang/Language.thy Sat Feb 26 12:53:00 2011 +0100
8.2 +++ b/src/Tools/isac/ProgLang/Language.thy Tue Mar 01 15:23:59 2011 +0100
8.3 @@ -4,7 +4,7 @@
8.4 *)
8.5
8.6 theory Language imports Script
8.7 -uses ("../ProgLang/scrtools.sml")
8.8 + uses ("../ProgLang/scrtools.sml")
8.9 begin
8.10
8.11 use "../ProgLang/scrtools.sml"
9.1 --- a/src/Tools/isac/ProgLang/ListC.thy Sat Feb 26 12:53:00 2011 +0100
9.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Tue Mar 01 15:23:59 2011 +0100
9.3 @@ -197,6 +197,4 @@
9.4 [("list_rls",list_rls)
9.5 ]);
9.6 *}
9.7 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
9.8 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
9.9 end
10.1 --- a/src/Tools/isac/calcelems.sml Sat Feb 26 12:53:00 2011 +0100
10.2 +++ b/src/Tools/isac/calcelems.sml Tue Mar 01 15:23:59 2011 +0100
10.3 @@ -665,7 +665,7 @@
10.4 (*.switch for checking guhs unique before storing a pbl or met;
10.5 set true at startup (done at begin of ROOT.ML)
10.6 set false for editing IsacKnowledge (done at end of ROOT.ML).*)
10.7 -val check_guhs_unique = Unsynchronized.ref false;
10.8 +val check_guhs_unique = Unsynchronized.ref true;
10.9
10.10
10.11 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
10.12 @@ -681,1086 +681,3 @@
10.13 (*
10.14 end (*struct*)
10.15 *)
10.16 -
10.17 -
10.18 -
10.19 -val e_rule =
10.20 - Thm ("refl", @{thm refl});
10.21 -fun id_of_thm (Thm (id, _)) = id
10.22 - | id_of_thm _ = error "id_of_thm";
10.23 -fun thm_of_thm (Thm (_, thm)) = thm
10.24 - | thm_of_thm _ = error "thm_of_thm";
10.25 -fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
10.26 -
10.27 -fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
10.28 -fun thyID_of_derivation_name dn = hd (space_explode "." dn);
10.29 -
10.30 -fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
10.31 - (strip_thy thmid1) = (strip_thy thmid2);
10.32 -(*version typed weaker WN100910*)
10.33 -fun eq_thmI' ((thmid1, _), (thmid2, _)) =
10.34 - (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
10.35 -
10.36 -
10.37 -val string_of_thm = Thm.get_name_hint; (*FIXME.2009*)
10.38 -(*check for [.] as caused by "fun assoc_thm'"*)
10.39 -fun string_of_thmI thm =
10.40 - let val ct' = (de_quote o string_of_thm) thm
10.41 - val (a, b) = split_nlast (5, Symbol.explode ct')
10.42 - in case b of
10.43 - [" ", " ","[", ".", "]"] => implode a
10.44 - | _ => ct'
10.45 - end;
10.46 -
10.47 -(*.id requested for all, Rls,Seq,Rrls.*)
10.48 -fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
10.49 - | id_rls (Rls {id,...}) = id
10.50 - | id_rls (Seq {id,...}) = id
10.51 - | id_rls (Rrls {id,...}) = id;
10.52 -val rls2str = id_rls;
10.53 -fun id_rule (Thm (id, _)) = id
10.54 - | id_rule (Calc (id, _)) = id
10.55 - | id_rule (Rls_ rls) = id_rls rls;
10.56 -
10.57 -fun get_rules (Rls {rules,...}) = rules
10.58 - | get_rules (Seq {rules,...}) = rules
10.59 - | get_rules (Rrls _) = [];
10.60 -
10.61 -fun rule2str Erule = "Erule"
10.62 - | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
10.63 - | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
10.64 - | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
10.65 - | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
10.66 -fun rule2str' Erule = "Erule"
10.67 - | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"
10.68 - | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
10.69 - | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
10.70 - | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
10.71 -
10.72 -(*WN080102 compare eq_rule ?!?*)
10.73 -fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
10.74 - | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
10.75 - | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2
10.76 - | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
10.77 - | eqrule _ = false;
10.78 -
10.79 -
10.80 -type rrlsstate = (*state for reverse rewriting*)
10.81 - (term * (*the current formula:
10.82 - goes locate_gen -> next_tac via istate*)
10.83 - term * (*the final formula*)
10.84 - rule list (*of reverse rewrite set (#1#)*)
10.85 - list * (*may be serveral, eg. in norm_rational*)
10.86 - (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
10.87 - (term * (*... rewrite with ...*)
10.88 - term list)) (*... assumptions*)
10.89 - list); (*derivation from given term to normalform
10.90 - in reverse order with sym_thm;
10.91 - (#1#) could be extracted from here #1*)
10.92 -val e_type = Type("empty",[]);
10.93 -val a_type = TFree("'a",[]);
10.94 -val e_term = Const("empty",e_type);
10.95 -val a_term = Free("empty",a_type);
10.96 -val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;
10.97 -
10.98 -
10.99 -
10.100 -
10.101 -(*22.2.02: ging auf Linux nicht (Stefan)
10.102 -val e_scr = Script ((term_of o the o (parse thy)) "e_script");*)
10.103 -val e_term = Const("empty", Type("'a", []));
10.104 -val e_scr = Script e_term;
10.105 -
10.106 -
10.107 -(*ad thm':
10.108 - there are two kinds of theorems ...
10.109 - (1) known by isabelle
10.110 - (2) not known, eg. calc_thm, instantiated rls
10.111 - the latter have a thmid "#..."
10.112 - and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
10.113 - and have a special assoc_thm / assoc_rls in this interface *)
10.114 -type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
10.115 -type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
10.116 -type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
10.117 -
10.118 -fun string_of_thy thy = Context.theory_name thy: theory';
10.119 -val theory2domID = string_of_thy;
10.120 -val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
10.121 -val theory2theory' = string_of_thy;
10.122 -val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
10.123 -val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy;
10.124 -(*> theory2str' (Thy_Info.get_theory "Isac");
10.125 -al it = "Isac" : string
10.126 -*)
10.127 -
10.128 -fun thyID2theory' (thyID:thyID) = thyID;
10.129 -(*
10.130 - let val ss = Symbol.explode thyID
10.131 - val ext = implode (takelast (4, ss))
10.132 - in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
10.133 - else thyID ^ ".thy"
10.134 - end;
10.135 -*)
10.136 -(* thyID2theory' "Isac" (*ok*);
10.137 -val it = "Isac" : theory'
10.138 - > thyID2theory' "Isac" (*abuse, goes ok...*);
10.139 -val it = "Isac" : theory'
10.140 -*)
10.141 -
10.142 -fun theory'2thyID (theory':theory') = theory';
10.143 -(*
10.144 - let val ss = Symbol.explode theory'
10.145 - val ext = implode (takelast (4, ss))
10.146 - in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
10.147 - else theory' (*disarm abuse of theory'*)
10.148 - end;
10.149 -*)
10.150 -(* theory'2thyID "Isac";
10.151 -val it = "Isac" : thyID
10.152 -> theory'2thyID "Isac";
10.153 -val it = "Isac" : thyID*)
10.154 -
10.155 -
10.156 -(*. WN0509 discussion:
10.157 -#############################################################################
10.158 -# How to manage theorys in subproblems wrt. the requirement, #
10.159 -# that scripts should be re-usable ? #
10.160 -#############################################################################
10.161 -
10.162 - eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'
10.163 - which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
10.164 - because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
10.165 - is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
10.166 - (see match_ags).
10.167 -
10.168 - Preliminary solution:
10.169 - # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
10.170 - # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
10.171 - # however, a thy specified by the user in the rootpbl may lead to
10.172 - errors in far-off subpbls (which are not yet reported properly !!!)
10.173 - and interactively specifiying thys in subpbl is not very relevant.
10.174 -
10.175 - Other solutions possible:
10.176 - # always parse and type-check with Thy_Info.get_theory "Isac"
10.177 - (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
10.178 - # regard the subthy-relation in specifying thys of subpbls
10.179 - # specifically handle 'SubProblem (undefined, pbl, arglist)'
10.180 - # ???
10.181 -.*)
10.182 -(*WN0509 TODO "ProtoPure" ... would be more consistent
10.183 - with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)
10.184 -val e_domID = "e_domID":domID;
10.185 -
10.186 -(*the key into the hierarchy ob theory elements*)
10.187 -type theID = string list;
10.188 -val e_theID = ["e_theID"];
10.189 -val theID2str = strs2str;
10.190 -(*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
10.191 -fun theID2thyID (theID:theID) =
10.192 - if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID
10.193 - else error ("theID2thyID called with "^ theID2str theID);
10.194 -
10.195 -(*the key into the hierarchy ob problems*)
10.196 -type pblID = string list; (* domID::...*)
10.197 -val e_pblID = ["e_pblID"]:pblID;
10.198 -val pblID2str = strs2str;
10.199 -
10.200 -(*the key into the hierarchy ob methods*)
10.201 -type metID = string list;
10.202 -val e_metID = ["e_metID"]:metID;
10.203 -val metID2str = strs2str;
10.204 -
10.205 -(*either theID or pblID or metID*)
10.206 -type kestoreID = string list;
10.207 -val e_kestoreID = ["e_kestoreID"];
10.208 -val kestoreID2str = strs2str;
10.209 -
10.210 -(*for distinction of contexts*)
10.211 -datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
10.212 -fun ketype2str Exp_ = "Exp_"
10.213 - | ketype2str Thy_ = "Thy_"
10.214 - | ketype2str Pbl_ = "Pbl_"
10.215 - | ketype2str Met_ = "Met_";
10.216 -fun ketype2str' Exp_ = "Example"
10.217 - | ketype2str' Thy_ = "Theory"
10.218 - | ketype2str' Pbl_ = "Problem"
10.219 - | ketype2str' Met_ = "Method";
10.220 -
10.221 -(*see 'How to manage theorys in subproblems' at 'type thyID'*)
10.222 -val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
10.223 -
10.224 -(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
10.225 - in order to distinguish them from general IsacKnowledge defined later on.*)
10.226 -val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
10.227 -
10.228 -
10.229 -(*rewrite orders, also stored in 'type met' and type 'and rls'
10.230 - The association list is required for 'rewrite.."rew_ord"..'
10.231 - WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
10.232 -val rew_ord' =
10.233 - Unsynchronized.ref
10.234 - ([]:(rew_ord' * (*the key for the association list *)
10.235 - (subst (*the bound variables - they get high order*)
10.236 - -> (term * term) (*(t1, t2) to be compared *)
10.237 - -> bool)) (*if t1 <= t2 then true else false *)
10.238 - list); (*association list *)
10.239 -
10.240 -rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
10.241 - ("dummy_ord", dummy_ord)]);
10.242 -
10.243 -
10.244 -(*WN060120 a hack to get alltogether run again with minimal effort:
10.245 - theory' is inserted for creating thy_hierarchy; calls for assoc_rls
10.246 - need not be called*)
10.247 -val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list);
10.248 -
10.249 -(*FIXME.040207 calclist': used by prep_rls, NOT in met*)
10.250 -val calclist'= Unsynchronized.ref ([]: calc list);
10.251 -
10.252 -(*.the hierarchy of thydata.*)
10.253 -
10.254 -(*.'a is for pbt | met.*)
10.255 -(*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*)
10.256 -datatype 'a ptyp =
10.257 - Ptyp of string * (*element within pblID*)
10.258 - 'a list * (*several pbts with different domIDs/thy
10.259 - TODO: select by subthy (isaref.p.69)
10.260 - presently only _ONE_ elem*)
10.261 - ('a ptyp) list; (*the children nodes*)
10.262 -
10.263 -(*.datatype for collecting thydata for hierarchy.*)
10.264 -(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
10.265 -(*WN0606 Htxt contains html which does not belong to the sml-kernel*)
10.266 -datatype thydata = Html of {guh: guh,
10.267 - coursedesign: authors,
10.268 - mathauthors: authors,
10.269 - html: string} (*html; for demos before database*)
10.270 - | Hthm of {guh: guh,
10.271 - coursedesign: authors,
10.272 - mathauthors: authors,
10.273 - thm: term}
10.274 - | Hrls of {guh: guh,
10.275 - coursedesign: authors,
10.276 - mathauthors: authors,
10.277 - (*like vvvvvvvvvvvvv val ruleset'
10.278 - WN060711 redesign together !*)
10.279 - thy_rls: (thyID * rls)}
10.280 - | Hcal of {guh: guh,
10.281 - coursedesign: authors,
10.282 - mathauthors: authors,
10.283 - calc: calc}
10.284 - | Hord of {guh: guh,
10.285 - coursedesign: authors,
10.286 - mathauthors: authors,
10.287 - ord: (subst -> (term * term) -> bool)};
10.288 -val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
10.289 -
10.290 -type thehier = (thydata ptyp) list;
10.291 -val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
10.292 -
10.293 -(* an association list, gets the value once in Isac.ML.
10.294 - stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
10.295 - WN1-1-28 make this data arguments and del ref ?*)
10.296 -val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
10.297 -
10.298 -
10.299 -type path = string;
10.300 -type filename = string;
10.301 -
10.302 -(*val xxx = fn: a b => (a,b); ??? fun-definition ???*)
10.303 -local
10.304 - fun ii (_:term) = e_rrlsstate;
10.305 - fun no (_:term) = SOME (e_term,[e_term]);
10.306 - fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];
10.307 - fun ne (_:rule list list) (_:term) = SOME e_rule;
10.308 - fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];
10.309 -in
10.310 -val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,
10.311 - next_rule=ne,attach_form=fo};
10.312 -end;
10.313 -
10.314 -val e_rls =
10.315 - Rls{id = "e_rls",
10.316 - preconds = [],
10.317 - rew_ord = ("dummy_ord", dummy_ord),
10.318 - erls = Erls,srls = Erls,
10.319 - calc = [],
10.320 - rules = [], scr = EmptyScr}:rls;
10.321 -val e_rrls = Rrls {id = "e_rrls",
10.322 - prepat = [],
10.323 - rew_ord = ("dummy_ord", dummy_ord),
10.324 - erls = Erls,
10.325 - calc = [],
10.326 - (*asm_thm=[],*)
10.327 - scr=e_rfuns}:rls;
10.328 -ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)),
10.329 - ("e_rrls",("Tools",e_rrls))
10.330 - ]);
10.331 -
10.332 -fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
10.333 - {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
10.334 - (*asm_thm=asm_thm,*)rules=rules,scr=scr}
10.335 - | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
10.336 - {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
10.337 - (*asm_thm=asm_thm,*)rules=rules,scr=scr}
10.338 - | rep_rls Erls = rep_rls e_rls
10.339 - | rep_rls (Rrls {id,...}) = rep_rls e_rls
10.340 - (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
10.341 -(*| rep_rls (Seq {id,...}) =
10.342 - error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
10.343 ---1.7.03*)
10.344 -fun rep_rrls
10.345 - (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
10.346 - scr=Rfuns
10.347 - {attach_form,init_state,locate_rule,
10.348 - next_rule,normal_form}}) =
10.349 - {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
10.350 - rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
10.351 - locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
10.352 - | rep_rrls (Rls {id,...}) =
10.353 - error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
10.354 - | rep_rrls (Seq {id,...}) =
10.355 - error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
10.356 -
10.357 -fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.358 - rules =rs,scr=sc}) r =
10.359 - (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.360 - rules = rs @ r,scr=sc}:rls)
10.361 - | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.362 - rules =rs,scr=sc}) r =
10.363 - (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.364 - rules = rs @ r,scr=sc}:rls)
10.365 - | append_rls id (Rrls _) _ =
10.366 - error ("append_rls: not for reverse-rewrite-rule-set "^id);
10.367 -
10.368 -(*. are _atomic_ rules equal ?.*)
10.369 -(*WN080102 compare eqrule ?!?*)
10.370 -fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
10.371 - | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
10.372 - | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
10.373 - (*id_rls checks for Rls, Seq, Rrls*)
10.374 - | eq_rule _ = false;
10.375 -
10.376 -fun merge_rls _ Erls rls = rls
10.377 - | merge_rls _ rls Erls = rls
10.378 - | merge_rls id
10.379 - (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
10.380 - (*asm_thm=at1,*)rules =rs1,scr=sc1})
10.381 - (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
10.382 - (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
10.383 - (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
10.384 - rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
10.385 - srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
10.386 - ((#srls o rep_rls) r2),
10.387 - calc=ca1 @ ((#calc o rep_rls) r2),
10.388 - (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
10.389 - rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
10.390 - scr=sc1}:rls)
10.391 - | merge_rls id
10.392 - (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
10.393 - (*asm_thm=at1,*)rules =rs1,scr=sc1})
10.394 - (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
10.395 - (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
10.396 - (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
10.397 - rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
10.398 - srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
10.399 - ((#srls o rep_rls) r2),
10.400 - calc=ca1 @ ((#calc o rep_rls) r2),
10.401 - (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
10.402 - rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
10.403 - scr=sc1}:rls)
10.404 - | merge_rls _ _ _ =
10.405 - error "merge_rls: not for reverse-rewrite-rule-sets\
10.406 - \and not for mixed Rls -- Seq";
10.407 -fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.408 - (*asm_thm=at,*)rules =rs,scr=sc}) r =
10.409 - (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.410 - (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
10.411 - scr=sc}:rls)
10.412 - | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.413 - (*asm_thm=at,*)rules =rs,scr=sc}) r =
10.414 - (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.415 - (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
10.416 - scr=sc}:rls)
10.417 - | remove_rls id (Rrls _) _ = error
10.418 - ("remove_rls: not for reverse-rewrite-rule-set "^id);
10.419 -
10.420 -(*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
10.421 -val it = [1, 2] : int list*)
10.422 -
10.423 -(*elder version: migrated 3 calls in smtest to memrls
10.424 -fun mem_rls id rls =
10.425 - case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of
10.426 - SOME _ => true | NONE => false;*)
10.427 -fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
10.428 - | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
10.429 - | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
10.430 -fun rls_get_thm rls (id: xstring) =
10.431 - case find_first (curry eq_rule e_rule)
10.432 - ((#rules o rep_rls) rls) of
10.433 - SOME thm => SOME thm | NONE => NONE;
10.434 -
10.435 -fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known")
10.436 - | assoc' ((keyi, xi) :: pairs, key) =
10.437 - if key = keyi then SOME xi else assoc' (pairs, key);
10.438 -
10.439 -(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
10.440 - handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
10.441 -fun assoc_thy (thy:theory') =
10.442 - if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*)
10.443 - else (Thy_Info.get_theory thy)
10.444 - handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
10.445 -
10.446 -(*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
10.447 - these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
10.448 - overlays by re-using an identifier in different thys.*)
10.449 -fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls))
10.450 - handle _ => error ("ME_Isa: '"^rls^"' not in system");
10.451 -(*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))
10.452 - handle _ => error ("ME_Isa: '"^rls^"' not in system");*)
10.453 -
10.454 -(*.overwrite an element in an association list and pair it with a thyID
10.455 - in order to create the thy_hierarchy;
10.456 - overwrites existing rls' even if they are defined in a different thy;
10.457 - this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
10.458 -(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
10.459 - they do NOT handle overlays by re-using an identifier in different thys;
10.460 - "thyID.rlsID" would be a good solution, if the "." would be possible
10.461 - in scripts...
10.462 - actually a hack to get alltogether run again with minimal effort*)
10.463 -fun insthy thy' (rls', rls) = (rls', (thy', rls));
10.464 -fun overwritelthy thy (al, bl:(rls' * rls) list) =
10.465 - let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl
10.466 - in overwritel (al, bl') end;
10.467 -
10.468 -fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
10.469 - handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
10.470 -(*get the string for stac from rule*)
10.471 -fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found")
10.472 - | assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
10.473 - if key = keyi then calc else assoc_calc (pairs, key);
10.474 -(*only used for !calclist'...*)
10.475 -fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
10.476 - ^"' not found")
10.477 - | assoc1 ((all as (keyi, _)) :: pairs, key) =
10.478 - if key = keyi then all else assoc1 (pairs, key);
10.479 -
10.480 -(*TODO.WN080102 clarify usage of type cal and type calc..*)
10.481 -fun calID2calcID (calID : calID) =
10.482 - let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'")
10.483 - | ass ((calci, (cali, eval_fn))::ids) =
10.484 - if calID = cali then calci
10.485 - else ass ids
10.486 - in ass (!calclist') : calcID end;
10.487 -
10.488 -fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
10.489 -(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
10.490 -
10.491 -fun terms2str ts = (strs2str o (map term2str )) ts;
10.492 -(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
10.493 -fun terms2str' ts = (strs2str' o (map term2str )) ts;
10.494 -(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
10.495 -fun terms2strs ts = (map term2str) ts;
10.496 -(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
10.497 -
10.498 -fun termopt2str (SOME t) = "SOME " ^ term2str t
10.499 - | termopt2str NONE = "NONE";
10.500 -
10.501 -fun type2str typ =
10.502 - Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ;
10.503 -val string_of_typ = type2str;
10.504 -
10.505 -fun subst2str (s:subst) =
10.506 - (strs2str o
10.507 - (map (linefeed o pair2str o
10.508 - (apsnd term2str) o
10.509 - (apfst term2str)))) s;
10.510 -fun subst2str' (s:subst) =
10.511 - (strs2str' o
10.512 - (map (pair2str o
10.513 - (apsnd term2str) o
10.514 - (apfst term2str)))) s;
10.515 -(*> subst2str' [(str2term "bdv", str2term "x"),
10.516 - (str2term "bdv_2", str2term "y")];
10.517 -val it = "[(bdv, x)]" : string
10.518 -*)
10.519 -val env2str = subst2str;
10.520 -
10.521 -
10.522 -(*recursive defs:*)
10.523 -fun scr2str (Script s) = "Script "^(term2str s)
10.524 - | scr2str (Rfuns _) = "Rfuns";
10.525 -
10.526 -
10.527 -fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1;
10.528 -
10.529 -
10.530 -(*.trace internal steps of isac's rewriter*)
10.531 -val trace_rewrite = Unsynchronized.ref false;
10.532 -(*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
10.533 -val depth = Unsynchronized.ref 99999;
10.534 -(*.no of rewrites exceeding this int -> NO rewrite.*)
10.535 -(*WN060829 still unused...*)
10.536 -val lim_rewrite = Unsynchronized.ref 99999;
10.537 -(*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
10.538 -val lim_deriv = Unsynchronized.ref 100;
10.539 -(*.switch for checking guhs unique before storing a pbl or met;
10.540 - set true at startup (done at begin of ROOT.ML)
10.541 - set false for editing IsacKnowledge (done at end of ROOT.ML).*)
10.542 -val check_guhs_unique = Unsynchronized.ref false;
10.543 -
10.544 -
10.545 -datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
10.546 - L (*go left at $*)
10.547 - | R (*go right at $*)
10.548 - | D; (*go down at Abs*)
10.549 -type loc_ = lrd list;
10.550 -fun ldr2str L = "L"
10.551 - | ldr2str R = "R"
10.552 - | ldr2str D = "D";
10.553 -fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
10.554 -
10.555 -(*
10.556 -end (*struct*)
10.557 -*)
10.558 -
10.559 -
10.560 -val e_rule =
10.561 - Thm ("refl", @{thm refl});
10.562 -fun id_of_thm (Thm (id, _)) = id
10.563 - | id_of_thm _ = error "id_of_thm";
10.564 -fun thm_of_thm (Thm (_, thm)) = thm
10.565 - | thm_of_thm _ = error "thm_of_thm";
10.566 -fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
10.567 -
10.568 -fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
10.569 -fun thyID_of_derivation_name dn = hd (space_explode "." dn);
10.570 -
10.571 -fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
10.572 - (strip_thy thmid1) = (strip_thy thmid2);
10.573 -(*version typed weaker WN100910*)
10.574 -fun eq_thmI' ((thmid1, _), (thmid2, _)) =
10.575 - (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
10.576 -
10.577 -
10.578 -val string_of_thm = Thm.get_name_hint; (*FIXME.2009*)
10.579 -(*check for [.] as caused by "fun assoc_thm'"*)
10.580 -fun string_of_thmI thm =
10.581 - let val ct' = (de_quote o string_of_thm) thm
10.582 - val (a, b) = split_nlast (5, Symbol.explode ct')
10.583 - in case b of
10.584 - [" ", " ","[", ".", "]"] => implode a
10.585 - | _ => ct'
10.586 - end;
10.587 -
10.588 -(*.id requested for all, Rls,Seq,Rrls.*)
10.589 -fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
10.590 - | id_rls (Rls {id,...}) = id
10.591 - | id_rls (Seq {id,...}) = id
10.592 - | id_rls (Rrls {id,...}) = id;
10.593 -val rls2str = id_rls;
10.594 -fun id_rule (Thm (id, _)) = id
10.595 - | id_rule (Calc (id, _)) = id
10.596 - | id_rule (Rls_ rls) = id_rls rls;
10.597 -
10.598 -fun get_rules (Rls {rules,...}) = rules
10.599 - | get_rules (Seq {rules,...}) = rules
10.600 - | get_rules (Rrls _) = [];
10.601 -
10.602 -fun rule2str Erule = "Erule"
10.603 - | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
10.604 - | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
10.605 - | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
10.606 - | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
10.607 -fun rule2str' Erule = "Erule"
10.608 - | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"
10.609 - | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
10.610 - | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
10.611 - | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
10.612 -
10.613 -(*WN080102 compare eq_rule ?!?*)
10.614 -fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
10.615 - | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
10.616 - | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2
10.617 - | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
10.618 - | eqrule _ = false;
10.619 -
10.620 -
10.621 -type rrlsstate = (*state for reverse rewriting*)
10.622 - (term * (*the current formula:
10.623 - goes locate_gen -> next_tac via istate*)
10.624 - term * (*the final formula*)
10.625 - rule list (*of reverse rewrite set (#1#)*)
10.626 - list * (*may be serveral, eg. in norm_rational*)
10.627 - (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
10.628 - (term * (*... rewrite with ...*)
10.629 - term list)) (*... assumptions*)
10.630 - list); (*derivation from given term to normalform
10.631 - in reverse order with sym_thm;
10.632 - (#1#) could be extracted from here #1*)
10.633 -val e_type = Type("empty",[]);
10.634 -val a_type = TFree("'a",[]);
10.635 -val e_term = Const("empty",e_type);
10.636 -val a_term = Free("empty",a_type);
10.637 -val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;
10.638 -
10.639 -
10.640 -
10.641 -
10.642 -(*22.2.02: ging auf Linux nicht (Stefan)
10.643 -val e_scr = Script ((term_of o the o (parse thy)) "e_script");*)
10.644 -val e_term = Const("empty", Type("'a", []));
10.645 -val e_scr = Script e_term;
10.646 -
10.647 -
10.648 -(*ad thm':
10.649 - there are two kinds of theorems ...
10.650 - (1) known by isabelle
10.651 - (2) not known, eg. calc_thm, instantiated rls
10.652 - the latter have a thmid "#..."
10.653 - and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
10.654 - and have a special assoc_thm / assoc_rls in this interface *)
10.655 -type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
10.656 -type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
10.657 -type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
10.658 -
10.659 -fun string_of_thy thy = Context.theory_name thy: theory';
10.660 -val theory2domID = string_of_thy;
10.661 -val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
10.662 -val theory2theory' = string_of_thy;
10.663 -val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
10.664 -val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy;
10.665 -(*> theory2str' (Thy_Info.get_theory "Isac");
10.666 -al it = "Isac" : string
10.667 -*)
10.668 -
10.669 -fun thyID2theory' (thyID:thyID) = thyID;
10.670 -(*
10.671 - let val ss = Symbol.explode thyID
10.672 - val ext = implode (takelast (4, ss))
10.673 - in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
10.674 - else thyID ^ ".thy"
10.675 - end;
10.676 -*)
10.677 -(* thyID2theory' "Isac" (*ok*);
10.678 -val it = "Isac" : theory'
10.679 - > thyID2theory' "Isac" (*abuse, goes ok...*);
10.680 -val it = "Isac" : theory'
10.681 -*)
10.682 -
10.683 -fun theory'2thyID (theory':theory') = theory';
10.684 -(*
10.685 - let val ss = Symbol.explode theory'
10.686 - val ext = implode (takelast (4, ss))
10.687 - in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
10.688 - else theory' (*disarm abuse of theory'*)
10.689 - end;
10.690 -*)
10.691 -(* theory'2thyID "Isac";
10.692 -val it = "Isac" : thyID
10.693 -> theory'2thyID "Isac";
10.694 -val it = "Isac" : thyID*)
10.695 -
10.696 -
10.697 -(*. WN0509 discussion:
10.698 -#############################################################################
10.699 -# How to manage theorys in subproblems wrt. the requirement, #
10.700 -# that scripts should be re-usable ? #
10.701 -#############################################################################
10.702 -
10.703 - eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'
10.704 - which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
10.705 - because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
10.706 - is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
10.707 - (see match_ags).
10.708 -
10.709 - Preliminary solution:
10.710 - # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
10.711 - # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
10.712 - # however, a thy specified by the user in the rootpbl may lead to
10.713 - errors in far-off subpbls (which are not yet reported properly !!!)
10.714 - and interactively specifiying thys in subpbl is not very relevant.
10.715 -
10.716 - Other solutions possible:
10.717 - # always parse and type-check with Thy_Info.get_theory "Isac"
10.718 - (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
10.719 - # regard the subthy-relation in specifying thys of subpbls
10.720 - # specifically handle 'SubProblem (undefined, pbl, arglist)'
10.721 - # ???
10.722 -.*)
10.723 -(*WN0509 TODO "ProtoPure" ... would be more consistent
10.724 - with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)
10.725 -val e_domID = "e_domID":domID;
10.726 -
10.727 -(*the key into the hierarchy ob theory elements*)
10.728 -type theID = string list;
10.729 -val e_theID = ["e_theID"];
10.730 -val theID2str = strs2str;
10.731 -(*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
10.732 -fun theID2thyID (theID:theID) =
10.733 - if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID
10.734 - else error ("theID2thyID called with "^ theID2str theID);
10.735 -
10.736 -(*the key into the hierarchy ob problems*)
10.737 -type pblID = string list; (* domID::...*)
10.738 -val e_pblID = ["e_pblID"]:pblID;
10.739 -val pblID2str = strs2str;
10.740 -
10.741 -(*the key into the hierarchy ob methods*)
10.742 -type metID = string list;
10.743 -val e_metID = ["e_metID"]:metID;
10.744 -val metID2str = strs2str;
10.745 -
10.746 -(*either theID or pblID or metID*)
10.747 -type kestoreID = string list;
10.748 -val e_kestoreID = ["e_kestoreID"];
10.749 -val kestoreID2str = strs2str;
10.750 -
10.751 -(*for distinction of contexts*)
10.752 -datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
10.753 -fun ketype2str Exp_ = "Exp_"
10.754 - | ketype2str Thy_ = "Thy_"
10.755 - | ketype2str Pbl_ = "Pbl_"
10.756 - | ketype2str Met_ = "Met_";
10.757 -fun ketype2str' Exp_ = "Example"
10.758 - | ketype2str' Thy_ = "Theory"
10.759 - | ketype2str' Pbl_ = "Problem"
10.760 - | ketype2str' Met_ = "Method";
10.761 -
10.762 -(*see 'How to manage theorys in subproblems' at 'type thyID'*)
10.763 -val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
10.764 -
10.765 -(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
10.766 - in order to distinguish them from general IsacKnowledge defined later on.*)
10.767 -val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
10.768 -
10.769 -
10.770 -(*rewrite orders, also stored in 'type met' and type 'and rls'
10.771 - The association list is required for 'rewrite.."rew_ord"..'
10.772 - WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
10.773 -val rew_ord' =
10.774 - Unsynchronized.ref
10.775 - ([]:(rew_ord' * (*the key for the association list *)
10.776 - (subst (*the bound variables - they get high order*)
10.777 - -> (term * term) (*(t1, t2) to be compared *)
10.778 - -> bool)) (*if t1 <= t2 then true else false *)
10.779 - list); (*association list *)
10.780 -
10.781 -rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
10.782 - ("dummy_ord", dummy_ord)]);
10.783 -
10.784 -
10.785 -(*WN060120 a hack to get alltogether run again with minimal effort:
10.786 - theory' is inserted for creating thy_hierarchy; calls for assoc_rls
10.787 - need not be called*)
10.788 -val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list);
10.789 -
10.790 -(*FIXME.040207 calclist': used by prep_rls, NOT in met*)
10.791 -val calclist'= Unsynchronized.ref ([]: calc list);
10.792 -
10.793 -(*.the hierarchy of thydata.*)
10.794 -
10.795 -(*.'a is for pbt | met.*)
10.796 -(*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*)
10.797 -datatype 'a ptyp =
10.798 - Ptyp of string * (*element within pblID*)
10.799 - 'a list * (*several pbts with different domIDs/thy
10.800 - TODO: select by subthy (isaref.p.69)
10.801 - presently only _ONE_ elem*)
10.802 - ('a ptyp) list; (*the children nodes*)
10.803 -
10.804 -(*.datatype for collecting thydata for hierarchy.*)
10.805 -(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
10.806 -(*WN0606 Htxt contains html which does not belong to the sml-kernel*)
10.807 -datatype thydata = Html of {guh: guh,
10.808 - coursedesign: authors,
10.809 - mathauthors: authors,
10.810 - html: string} (*html; for demos before database*)
10.811 - | Hthm of {guh: guh,
10.812 - coursedesign: authors,
10.813 - mathauthors: authors,
10.814 - thm: term}
10.815 - | Hrls of {guh: guh,
10.816 - coursedesign: authors,
10.817 - mathauthors: authors,
10.818 - (*like vvvvvvvvvvvvv val ruleset'
10.819 - WN060711 redesign together !*)
10.820 - thy_rls: (thyID * rls)}
10.821 - | Hcal of {guh: guh,
10.822 - coursedesign: authors,
10.823 - mathauthors: authors,
10.824 - calc: calc}
10.825 - | Hord of {guh: guh,
10.826 - coursedesign: authors,
10.827 - mathauthors: authors,
10.828 - ord: (subst -> (term * term) -> bool)};
10.829 -val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
10.830 -
10.831 -type thehier = (thydata ptyp) list;
10.832 -val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
10.833 -
10.834 -(* an association list, gets the value once in Isac.ML.
10.835 - stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
10.836 - WN1-1-28 make this data arguments and del ref ?*)
10.837 -val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
10.838 -
10.839 -
10.840 -type path = string;
10.841 -type filename = string;
10.842 -
10.843 -(*val xxx = fn: a b => (a,b); ??? fun-definition ???*)
10.844 -local
10.845 - fun ii (_:term) = e_rrlsstate;
10.846 - fun no (_:term) = SOME (e_term,[e_term]);
10.847 - fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];
10.848 - fun ne (_:rule list list) (_:term) = SOME e_rule;
10.849 - fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];
10.850 -in
10.851 -val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,
10.852 - next_rule=ne,attach_form=fo};
10.853 -end;
10.854 -
10.855 -val e_rls =
10.856 - Rls{id = "e_rls",
10.857 - preconds = [],
10.858 - rew_ord = ("dummy_ord", dummy_ord),
10.859 - erls = Erls,srls = Erls,
10.860 - calc = [],
10.861 - rules = [], scr = EmptyScr}:rls;
10.862 -val e_rrls = Rrls {id = "e_rrls",
10.863 - prepat = [],
10.864 - rew_ord = ("dummy_ord", dummy_ord),
10.865 - erls = Erls,
10.866 - calc = [],
10.867 - (*asm_thm=[],*)
10.868 - scr=e_rfuns}:rls;
10.869 -ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)),
10.870 - ("e_rrls",("Tools",e_rrls))
10.871 - ]);
10.872 -
10.873 -fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
10.874 - {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
10.875 - (*asm_thm=asm_thm,*)rules=rules,scr=scr}
10.876 - | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
10.877 - {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
10.878 - (*asm_thm=asm_thm,*)rules=rules,scr=scr}
10.879 - | rep_rls Erls = rep_rls e_rls
10.880 - | rep_rls (Rrls {id,...}) = rep_rls e_rls
10.881 - (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
10.882 -(*| rep_rls (Seq {id,...}) =
10.883 - error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
10.884 ---1.7.03*)
10.885 -fun rep_rrls
10.886 - (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
10.887 - scr=Rfuns
10.888 - {attach_form,init_state,locate_rule,
10.889 - next_rule,normal_form}}) =
10.890 - {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
10.891 - rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
10.892 - locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
10.893 - | rep_rrls (Rls {id,...}) =
10.894 - error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
10.895 - | rep_rrls (Seq {id,...}) =
10.896 - error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
10.897 -
10.898 -fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.899 - rules =rs,scr=sc}) r =
10.900 - (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.901 - rules = rs @ r,scr=sc}:rls)
10.902 - | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.903 - rules =rs,scr=sc}) r =
10.904 - (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.905 - rules = rs @ r,scr=sc}:rls)
10.906 - | append_rls id (Rrls _) _ =
10.907 - error ("append_rls: not for reverse-rewrite-rule-set "^id);
10.908 -
10.909 -(*. are _atomic_ rules equal ?.*)
10.910 -(*WN080102 compare eqrule ?!?*)
10.911 -fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
10.912 - | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
10.913 - | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
10.914 - (*id_rls checks for Rls, Seq, Rrls*)
10.915 - | eq_rule _ = false;
10.916 -
10.917 -fun merge_rls _ Erls rls = rls
10.918 - | merge_rls _ rls Erls = rls
10.919 - | merge_rls id
10.920 - (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
10.921 - (*asm_thm=at1,*)rules =rs1,scr=sc1})
10.922 - (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
10.923 - (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
10.924 - (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
10.925 - rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
10.926 - srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
10.927 - ((#srls o rep_rls) r2),
10.928 - calc=ca1 @ ((#calc o rep_rls) r2),
10.929 - (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
10.930 - rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
10.931 - scr=sc1}:rls)
10.932 - | merge_rls id
10.933 - (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
10.934 - (*asm_thm=at1,*)rules =rs1,scr=sc1})
10.935 - (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
10.936 - (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
10.937 - (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
10.938 - rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
10.939 - srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
10.940 - ((#srls o rep_rls) r2),
10.941 - calc=ca1 @ ((#calc o rep_rls) r2),
10.942 - (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
10.943 - rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
10.944 - scr=sc1}:rls)
10.945 - | merge_rls _ _ _ =
10.946 - error "merge_rls: not for reverse-rewrite-rule-sets\
10.947 - \and not for mixed Rls -- Seq";
10.948 -fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.949 - (*asm_thm=at,*)rules =rs,scr=sc}) r =
10.950 - (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.951 - (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
10.952 - scr=sc}:rls)
10.953 - | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.954 - (*asm_thm=at,*)rules =rs,scr=sc}) r =
10.955 - (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
10.956 - (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
10.957 - scr=sc}:rls)
10.958 - | remove_rls id (Rrls _) _ = error
10.959 - ("remove_rls: not for reverse-rewrite-rule-set "^id);
10.960 -
10.961 -(*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
10.962 -val it = [1, 2] : int list*)
10.963 -
10.964 -(*elder version: migrated 3 calls in smtest to memrls
10.965 -fun mem_rls id rls =
10.966 - case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of
10.967 - SOME _ => true | NONE => false;*)
10.968 -fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
10.969 - | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
10.970 - | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
10.971 -fun rls_get_thm rls (id: xstring) =
10.972 - case find_first (curry eq_rule e_rule)
10.973 - ((#rules o rep_rls) rls) of
10.974 - SOME thm => SOME thm | NONE => NONE;
10.975 -
10.976 -fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known")
10.977 - | assoc' ((keyi, xi) :: pairs, key) =
10.978 - if key = keyi then SOME xi else assoc' (pairs, key);
10.979 -
10.980 -(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
10.981 - handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
10.982 -fun assoc_thy (thy:theory') =
10.983 - if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*)
10.984 - else (Thy_Info.get_theory thy)
10.985 - handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
10.986 -
10.987 -(*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
10.988 - these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
10.989 - overlays by re-using an identifier in different thys.*)
10.990 -fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls))
10.991 - handle _ => error ("ME_Isa: '"^rls^"' not in system");
10.992 -(*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))
10.993 - handle _ => error ("ME_Isa: '"^rls^"' not in system");*)
10.994 -
10.995 -(*.overwrite an element in an association list and pair it with a thyID
10.996 - in order to create the thy_hierarchy;
10.997 - overwrites existing rls' even if they are defined in a different thy;
10.998 - this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
10.999 -(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
10.1000 - they do NOT handle overlays by re-using an identifier in different thys;
10.1001 - "thyID.rlsID" would be a good solution, if the "." would be possible
10.1002 - in scripts...
10.1003 - actually a hack to get alltogether run again with minimal effort*)
10.1004 -fun insthy thy' (rls', rls) = (rls', (thy', rls));
10.1005 -fun overwritelthy thy (al, bl:(rls' * rls) list) =
10.1006 - let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl
10.1007 - in overwritel (al, bl') end;
10.1008 -
10.1009 -fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
10.1010 - handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
10.1011 -(*get the string for stac from rule*)
10.1012 -fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found")
10.1013 - | assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
10.1014 - if key = keyi then calc else assoc_calc (pairs, key);
10.1015 -(*only used for !calclist'...*)
10.1016 -fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
10.1017 - ^"' not found")
10.1018 - | assoc1 ((all as (keyi, _)) :: pairs, key) =
10.1019 - if key = keyi then all else assoc1 (pairs, key);
10.1020 -
10.1021 -(*TODO.WN080102 clarify usage of type cal and type calc..*)
10.1022 -fun calID2calcID (calID : calID) =
10.1023 - let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'")
10.1024 - | ass ((calci, (cali, eval_fn))::ids) =
10.1025 - if calID = cali then calci
10.1026 - else ass ids
10.1027 - in ass (!calclist') : calcID end;
10.1028 -
10.1029 -fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
10.1030 -(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
10.1031 -
10.1032 -fun terms2str ts = (strs2str o (map term2str )) ts;
10.1033 -(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
10.1034 -fun terms2str' ts = (strs2str' o (map term2str )) ts;
10.1035 -(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
10.1036 -fun terms2strs ts = (map term2str) ts;
10.1037 -(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
10.1038 -
10.1039 -fun termopt2str (SOME t) = "SOME " ^ term2str t
10.1040 - | termopt2str NONE = "NONE";
10.1041 -
10.1042 -fun type2str typ =
10.1043 - Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ;
10.1044 -val string_of_typ = type2str;
10.1045 -
10.1046 -fun subst2str (s:subst) =
10.1047 - (strs2str o
10.1048 - (map (linefeed o pair2str o
10.1049 - (apsnd term2str) o
10.1050 - (apfst term2str)))) s;
10.1051 -fun subst2str' (s:subst) =
10.1052 - (strs2str' o
10.1053 - (map (pair2str o
10.1054 - (apsnd term2str) o
10.1055 - (apfst term2str)))) s;
10.1056 -(*> subst2str' [(str2term "bdv", str2term "x"),
10.1057 - (str2term "bdv_2", str2term "y")];
10.1058 -val it = "[(bdv, x)]" : string
10.1059 -*)
10.1060 -val env2str = subst2str;
10.1061 -
10.1062 -
10.1063 -(*recursive defs:*)
10.1064 -fun scr2str (Script s) = "Script "^(term2str s)
10.1065 - | scr2str (Rfuns _) = "Rfuns";
10.1066 -
10.1067 -
10.1068 -fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1;
10.1069 -
10.1070 -
10.1071 -(*.trace internal steps of isac's rewriter*)
10.1072 -val trace_rewrite = Unsynchronized.ref false;
10.1073 -(*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
10.1074 -val depth = Unsynchronized.ref 99999;
10.1075 -(*.no of rewrites exceeding this int -> NO rewrite.*)
10.1076 -(*WN060829 still unused...*)
10.1077 -val lim_rewrite = Unsynchronized.ref 99999;
10.1078 -(*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
10.1079 -val lim_deriv = Unsynchronized.ref 100;
10.1080 -(*.switch for checking guhs unique before storing a pbl or met;
10.1081 - set true at startup (done at begin of ROOT.ML)
10.1082 - set false for editing IsacKnowledge (done at end of ROOT.ML).*)
10.1083 -val check_guhs_unique = Unsynchronized.ref false;
10.1084 -
10.1085 -
10.1086 -datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
10.1087 - L (*go left at $*)
10.1088 - | R (*go right at $*)
10.1089 - | D; (*go down at Abs*)
10.1090 -type loc_ = lrd list;
10.1091 -fun ldr2str L = "L"
10.1092 - | ldr2str R = "R"
10.1093 - | ldr2str D = "D";
10.1094 -fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
10.1095 -
10.1096 -(*
10.1097 -end (*struct*)
10.1098 -*)
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/Tools/isac/xmlsrc/xmlsrc.thy Tue Mar 01 15:23:59 2011 +0100
11.3 @@ -0,0 +1,17 @@
11.4 +(* Title: collect all defitions for xml generation
11.5 + Author: Walther Neuper 110226
11.6 + (c) due to copyright terms
11.7 +*)
11.8 +
11.9 +theory xmlsrc imports Interpret
11.10 + uses ("mathml.sml") ("datatypes.sml") ("pbl-met-hierarchy.sml")
11.11 + ("thy-hierarchy.sml") ("interface-xml.sml")
11.12 +begin
11.13 +
11.14 + use "mathml.sml"
11.15 + use "datatypes.sml"
11.16 + use "pbl-met-hierarchy.sml"
11.17 + use "thy-hierarchy.sml"
11.18 + use "interface-xml.sml"
11.19 +
11.20 +end
11.21 \ No newline at end of file
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/test/Pure/Syntax/syntax.thy Tue Mar 01 15:23:59 2011 +0100
12.3 @@ -0,0 +1,34 @@
12.4 +theory syntaxe imports Main begin
12.5 +
12.6 +section {* Old parsing *}
12.7 +text {* Old parsing in ISAC used theories *}
12.8 +ML {*
12.9 +val thy = @{theory};
12.10 +fun parse thy str = Syntax.read_term_global thy str;
12.11 +val env =
12.12 + [(parse thy "equ::bool", parse thy "x + (1::int) = 2"),
12.13 + (parse thy "var::int", parse thy "x::int"),
12.14 + (parse thy "sol::bool", parse thy "(x::int) = 1")
12.15 + ];
12.16 +val precond = parse thy "(0::int) < x"
12.17 +*}
12.18 +text {* However, user input could not be parsed ...*}
12.19 +ML {* parse thy "x = 2 - 1" *}
12.20 +text {* ... because the type 'int' is lost (we have type 'a now).
12.21 + The learner would need to input x::int all the time. *}
12.22 +
12.23 +section {* Contexts *}
12.24 +ML {*
12.25 +val ctxt = ProofContext.init_global thy;
12.26 +
12.27 +(*... prepare ctxt ...*)
12.28 +
12.29 +fun parseNEW ctxt str = Syntax.read_term ctxt str;
12.30 +*}
12.31 +
12.32 +section {* New parsing *}
12.33 +text {* New parsing in ISAC uses contexts, which are rigorously updated
12.34 + by the Lucas-Interpreter. Then ...*}
12.35 +ML {* parse thy "x = 2 - 1" *}
12.36 +text {* ... x gets type 'int' from the context. *}
12.37 +end
13.1 --- a/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML Sat Feb 26 12:53:00 2011 +0100
13.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML Tue Mar 01 15:23:59 2011 +0100
13.3 @@ -3,7 +3,9 @@
13.4 fun foointerpret ((Const ("Foo_Language.fooprog", _)) $ (_ $ _ $ res)) = res;
13.5
13.6 (* Foo_Language's definitions are recognized: *)
13.7 -val trm = Syntax.read_term_global @{theory Foo_Language} "fooprog (a = b)";
13.8 +(*val trm = Syntax.read_term_global @{theory Foo_Language} "fooprog (a = b)"; *)
13.9 +val trm = Syntax.read_term_global @{theory "../1language/Foo_Language"}
13.10 + "fooprog (a = b)";
13.11 (*val trm =
13.12 Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $
13.13 (Const ("op =", "'a => 'a => bool") $ Free ("a", "'a") $
14.1 --- a/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy Sat Feb 26 12:53:00 2011 +0100
14.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy Tue Mar 01 15:23:59 2011 +0100
14.3 @@ -1,25 +1,36 @@
14.4 -(*
14.5 +(* Title: test/Tools/isac/ADDTESTS/file-depend
14.6 + Author: Walther Neuper
14.7 +*)
14.8 +
14.9 +header {* Test file dependencies analogous to ISAC
14.10 +
14.11 $ cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/file-depend
14.12 $ /usr/local/Isabelle/bin/isabelle emacs Build_Test.thy &
14.13 -
14.14 -*)
14.15 -
14.16 +*}
14.17 +(*----------------------------------------------------------------------------
14.18 theory Build_Test
14.19 imports
14.20 Complex_Main
14.21 "1language/Foo_Language"
14.22 "3knowledge/Foo_KnowALL"
14.23 begin
14.24 +----------------------------------------------------------------------------*)
14.25
14.26 -use "0foolibrary.ML"
14.27 -use_thy "1language/Foo_Language"
14.28 -use "2interpreter/2foointerpreter.ML"
14.29 +theory Build_Test
14.30 +imports
14.31 + Complex_Main
14.32 +begin
14.33 + use "0foolibrary.ML" ML {* foolibrhs *}
14.34 + use_thy "1language/Foo_Language" (*ML {* @{const fooprog} *}*)
14.35 + use "2interpreter/2foointerpreter.ML" ML {* foointerpret *}
14.36
14.37 -(*vvvvvvv can be bypassed with Foo_KnowALL
14.38 -use_thy "3knowledge/Foo_Know111"
14.39 -use_thy "3knowledge/Foo_Know222"
14.40 - ^^^^^^^ can be bypassed with Foo_KnowALL*)
14.41 -use_thy "3knowledge/Foo_KnowALL"
14.42 +text {* The top 'theory ... begin' can be outcommended and done stepwise:
14.43 +
14.44 + use "2interpreter/2foointerpreter.ML"
14.45 + use_thy "3knowledge/Foo_Know111"
14.46 + use_thy "3knowledge/Foo_Know222"
14.47 + use_thy "3knowledge/Foo_KnowALL"
14.48 +*}
14.49
14.50 text {* the different theories of knowledge are recognized, Const bar*: *}
14.51 ML {*
14.52 @@ -48,4 +59,18 @@
14.53 (Const ("op =", "'a => 'a => bool") $ Free ("foo111", "'a") $
14.54 Free ("bar111", "'a"))
14.55 : term*)
14.56 +*}
14.57 +
14.58 +text {* dir structure reflects ISAC, see Build_Isac.thy:
14.59 +/file-depend/0foolibrary.ML
14.60 +/file-depend/Build_Test.thy
14.61 +/file-depend/README
14.62 +
14.63 +/file-depend/1language/Foo_Language.thy
14.64 +
14.65 +/file-depend/2interpreter/2foointerpreter.ML
14.66 +
14.67 +/file-depend/3knowledge/Foo_Know111.thy
14.68 +/file-depend/3knowledge/Foo_Know222.thy
14.69 +/file-depend/3knowledge/Foo_KnowALL.thy
14.70 *}
14.71 \ No newline at end of file