diff -r 106e7d8723ca -r 4616b145b1cd src/Tools/isac/BaseDefinitions/Know_Store.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 12:22:37 2020 +0200 @@ -0,0 +1,271 @@ +(* Title: src/Tools/isac/Know_Store.thy + Author: Mathias Lehnfeld + +The files (in "xxxxx-def.sml") contain definitions required for Know_Store; +they also include minimal code required for other "xxxxx-def.sml" files. +These files have companion files "xxxxx.sml" with all further code, +located at appropriate positions in the file structure. + +The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by +appropriate use of polymorphic high order functions. +*) + +theory Know_Store imports Complex_Main + +begin +ML_file libraryC.sml +ML_file theoryC.sml +ML_file unparseC.sml +ML_file "rule-def.sml" +ML_file "thmC-def.sml" +ML_file "exec-def.sml" (*rename identifiers by use of struct.id*) +ML_file "rewrite-order.sml" (*rename identifiers by use of struct.id*) +ML_file rule.sml +ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*) +ML_file "rule-set.sml" + +ML_file "celem-0.sml" (*survey Celem.*) +ML_file "celem-1.sml" (*datatype 'a ptyp*) +ML_file "celem-2.sml" (*guh*) +ML_file "celem-3.sml" (*spec*) +ML_file "celem-4.sml" (*pat*) +ML_file "celem-5.sml" (*ptyps*) +ML_file "celem-6.sml" (*mets*) +ML_file "celem-7.sml" (*cas_elem*) +ML_file "celem-8.sml" (*thydata*) +ML_file "celem-91.sml" (*check_guhs_unique*) +ML_file "celem-92.sml" (**) +ML_file "celem-93.sml" (**) + +ML_file calcelems.sml +ML_file tracing.sml +ML \ +\ ML \ +\ ML \ +\ +section \Knowledge elements for problems and methods\ +ML \ +(* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end. + In the front-end Knowledge comprises theories, problems and methods. + Elements of problems and methods are defined in theories alongside + the development of respective language elements. + However, the structure of methods and problems is independent from theories' + deductive structure. Thus respective structures are built in Build_Thydata.thy. + + Most elements of problems and methods are implemented in "Knowledge/", but some + of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this + location in the directory structure. + + get_* retrieves all * of the respective theory PLUS of all ancestor theories. +*) +signature KESTORE_ELEMS = +sig + val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list + val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory + val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list + val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory + val get_cas: theory -> Celem.cas_elem list + val add_cas: Celem.cas_elem list -> theory -> theory + val get_ptyps: theory -> Celem.ptyps + val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory + val get_mets: theory -> Celem.mets + val add_mets: (Celem.met * Celem.metID) list -> theory -> theory + val get_thes: theory -> (Celem.thydata Celem1.ptyp) list + val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *) + val insert_fillpats: (Celem.theID * Error_Fill_Def.fillpat list) list -> theory -> theory + val get_ref_thy: unit -> theory + val set_ref_thy: theory -> unit +end; + +structure KEStore_Elems: KESTORE_ELEMS = +struct + fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1; + + structure Data = Theory_Data ( + type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list; + val empty = []; + val extend = I; + val merge = Rule_Set.to_kestore; + ); + fun get_rlss thy = Data.get thy + fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss) + + structure Data = Theory_Data ( + type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list; + val empty = []; + val extend = I; + val merge = merge Exec_Def.calc_eq; + ); + fun get_calcs thy = Data.get thy + fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs) + + structure Data = Theory_Data ( + type T = (term * (Celem.spec * (term list -> (term * term list) list))) list; + val empty = []; + val extend = I; + val merge = merge Celem.cas_eq; + ); + fun get_cas thy = Data.get thy + fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas) + + structure Data = Theory_Data ( + type T = Celem.ptyps; + val empty = [Celem.e_Ptyp]; + val extend = I; + val merge = Celem.merge_ptyps; + ); + fun get_ptyps thy = Data.get thy; + fun add_pbts pbts thy = let + fun add_pbt (pbt as {guh,...}, pblID) = + (* the pblID has the leaf-element as first; better readability achieved *) + (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else (); + rev pblID |> Celem.insrt pblID pbt); + in Data.map (fold add_pbt pbts) thy end; + + structure Data = Theory_Data ( + type T = Celem.mets; + val empty = [Celem.e_Mets]; + val extend = I; + val merge = Celem.merge_ptyps; + ); + val get_mets = Data.get; + fun add_mets mets thy = let + fun add_met (met as {guh,...}, metID) = + (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else (); + Celem.insrt metID met metID); + in Data.map (fold add_met mets) thy end; + + structure Data = Theory_Data ( + type T = (Celem.thydata Celem1.ptyp) list; + val empty = []; + val extend = I; + val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *) + ); + fun get_thes thy = Data.get thy + fun add_thes thes thy = let + fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata + in Data.map (fold add_the thes) thy end; + fun insert_fillpats fis thy = + let + fun update_elem (theID, fillpats) = + let + val hthm = Celem.get_py (Data.get thy) theID theID + val hthm' = Celem.update_hthm hthm fillpats + handle ERROR _ => + error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem") + in Celem.update_ptyps theID theID hthm' end + in Data.map (fold update_elem fis) thy end + + val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory}; + fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *) + fun get_ref_thy () = Synchronized.value cur_thy; +end; +\ + +section \Re-use existing access functions for knowledge elements\ +text \ + The independence of problems' and methods' structure enforces the accesse + functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined. +\ +ML \ +val get_ref_thy = KEStore_Elems.get_ref_thy; + +fun assoc_rls (rls' : Rule_Set.id) = + case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of + SOME (_, rls) => rls + | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^ + "TODO exception hierarchy needs to be established.") + +fun assoc_rls' thy (rls' : Rule_Set.id) = + case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of + SOME (_, rls) => rls + | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^ + "TODO exception hierarchy needs to be established.") + +fun assoc_calc thy calID = let + fun ass ([], key) = + error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy)) + | ass ((calc, (keyi, _)) :: pairs, key) = + if key = keyi then calc else ass (pairs, key); + in ass (thy |> KEStore_Elems.get_calcs, calID) end; + +fun assoc_calc' thy key = let + fun ass ([], key') = + error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy)) + | ass ((all as (keyi, _)) :: pairs, key') = + if key' = keyi then all else ass (pairs, key'); + in ass (KEStore_Elems.get_calcs thy, key) end; + +fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key); + +fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps; +fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets; +fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes; +\ +setup \KEStore_Elems.add_rlss + [("empty", (Context.theory_name @{theory}, Rule_Set.empty)), + ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\ + +section \determine sequence of main parts in thehier\ +setup \ +KEStore_Elems.add_thes + [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "", + mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]), + (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "", + mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]), + (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "", + mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])] +\ + +section \Functions for checking KEStore_Elems\ +ML \ +fun short_string_of_rls Rule_Set.Empty = "Erls" + | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) = + "Rls {#calc = " ^ string_of_int (length calc) ^ + ", #rules = " ^ string_of_int (length rules) ^ ", ..." + | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) = + "Seq {#calc = " ^ string_of_int (length calc) ^ + ", #rules = " ^ string_of_int (length rules) ^ ", ..." + | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}"; +fun check_kestore_rls (rls', (thyID, rls)) = + "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))"; + +fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))"; + +(* we avoid term_to_string''' defined later *) +fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) = + "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false + (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")"; + +fun count_kestore_ptyps [] = 0 + | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') = + 1 + count_kestore_ptyps ps + count_kestore_ptyps ps'; +fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^ + (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed; +val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str; +fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2); +fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2); +fun sort_kestore_ptyp' _ [] = [] + | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') = + ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord)) + :: sort_kestore_ptyp' ordfun ps'); +val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord; + +fun metguh2str ({guh,...} : Celem.met) = guh : string; +fun check_kestore_met (mp: Celem.met Celem1.ptyp) = + check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp; +fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2); +val sort_kestore_met = sort_kestore_ptyp' met_ord; + +fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes +fun write_thes thydata_list = + thydata_list + |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the)) + |> map pair2str + |> map writeln +\ +ML \ +\ ML \ +\ ML \ +\ +end