(*  Title:      src/Tools/isac/Know_Store.thy

     Author:     Mathias Lehnfeld

 Calc work on Problem employing MethodC; both are collected in a respective Store;

 The collections' structure is independent from the dependency graph of Isabelle's theories

 in Knowledge.

 Store is also used by Thy_Write, required for Isac's Java front end, irrelevant for PIDE.

 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

   keywords "rule_set_knowledge" "calculation" :: thy_decl

 begin

 setup \<open>

   ML_Antiquotation.conditional \<^binding>\<open>isac_test\<close>

     (fn _ => Options.default_bool \<^system_option>\<open>isac_test\<close>)

 \<close>

 ML_file libraryC.sml

 ML_file theoryC.sml

 ML_file unparseC.sml

 ML_file "rule-def.sml"

 ML_file "thmC-def.sml"

 ML_file "eval-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-pattern-def.sml"

 ML_file "rule-set.sml"

 ML_file "store.sml"

 ML_file "check-unique.sml"

 ML_file "references-def.sml"

 ML_file "model-pattern.sml"

 ML_file "problem-def.sml"

 ML_file "method-def.sml"

 ML_file "cas-def.sml"

 ML_file "formalise.sml"

 ML_file "example.sml"

 ML_file "thy-write.sml"

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 section \<open>Knowledge elements for problems and methods\<close>

 ML \<open>

 (* 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_rew_ord: theory -> Rewrite_Ord.T list

   val add_rew_ord: Rewrite_Ord.T list -> theory -> theory

   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 -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list

   val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory

   val get_cas: theory -> CAS_Def.T list

   val add_cas: CAS_Def.T list -> theory -> theory

   val get_pbls: theory -> Probl_Def.store

   val add_pbls: Proof.context -> (Probl_Def.T * References_Def.id) list -> theory -> theory

   val get_mets: theory -> Meth_Def.store

   val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory

   val get_expls: theory -> Example.store

   val add_expls: (Example.T * Store.key) list -> theory -> theory

   val get_thes: theory -> (Thy_Write.thydata Store.node) list

   val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)

   val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in 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 = (string * (LibraryC.subst -> term * term -> bool)) list;

     val empty = [];

     val extend = I;

     val merge = merge Rewrite_Ord.equal;

     );  

   fun get_rew_ord thy = Data.get thy

   fun add_rew_ord rlss = Data.map (union_overwrite Rewrite_Ord.equal rlss)

   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 = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;

     val empty = [];

     val extend = I;

     val merge = merge Eval_Def.calc_eq;

     );                                                              

   fun get_calcs thy = Data.get thy

   fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)

   structure Data = Theory_Data (

     type T = (term * (References_Def.T * (term list -> (term * term list) list))) list;

     val empty = [];

     val extend = I;

     val merge = merge CAS_Def.equal;

     );                                                              

   fun get_cas thy = Data.get thy

   fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)

   structure Data = Theory_Data (

     type T = Probl_Def.store;

     val empty = [Probl_Def.empty_store];

     val extend = I;

     val merge = Store.merge;

     );

   fun get_pbls thy = Data.get thy;

   fun add_pbls ctxt pbts thy =

     let

       fun add_pbt (pbt as {guh,...}, pblID) =

         (* the pblID has the leaf-element as first; better readability achieved *)

         (if (Config.get ctxt check_unique) then Probl_Def.check_unique guh (Data.get thy) else ();

           rev pblID |> Store.insert pblID pbt);

     in Data.map (fold add_pbt pbts) thy end;

   structure Data = Theory_Data (

     type T = Meth_Def.store;

     val empty = [Meth_Def.empty_store];

     val extend = I;

     val merge = Store.merge;

     );

   val get_mets = Data.get;

   fun add_mets ctxt mets thy =

     let

       fun add_met (met as {guh,...}, metID) =

         (if (Config.get ctxt check_unique) then Meth_Def.check_unique guh (Data.get thy) else ();

           Store.insert metID met metID);

     in Data.map (fold add_met mets) thy end;

   structure Data = Theory_Data (

     type T = Example.store;

     val empty = [Example.empty_store];

     val extend = I;

     val merge = Store.merge;

     );

   val get_expls = Data.get;

   fun add_expls expls thy =

     let

       fun add_expl (expl, expl_id) = Store.insert expl_id expl expl_id;

     in Data.map (fold add_expl expls) thy end;

   structure Data = Theory_Data (

     type T = (Thy_Write.thydata Store.node) list;

     val empty = [];

     val extend = I;

     val merge = Store.merge; (* relevant for store_thm, store_rls *)

     );                                                              

   fun get_thes thy = Data.get thy

   fun add_thes thes thy = let

     fun add_the (thydata, theID) = Thy_Write.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 = Store.get (Data.get thy) theID theID

           val hthm' = Thy_Write.update_hthm hthm fillpats

             handle ERROR _ =>

               raise ERROR ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")

         in Store.update 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(**);

 \<close>

 subsection \<open>Isar command syntax\<close>

 ML \<open>

 local

 val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);

 val ml = ML_Lex.read;

 fun ml_rule thy (name, source) =

   ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @

   ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @

   ML_Lex.read_source source @ ml "))";

 fun ml_rules thy args =

   ml "Theory.setup (KEStore_Elems.add_rlss [" @

     flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";

 val _ =

   Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"

     (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>

       thy |> Context.theory_map

         (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));

 val calc_name =

   Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||

   Scan.ahead Parse.name -- Parse.const;

 val _ =

   Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>

     "prepare ISAC calculation and register it to Knowledge Store"

     (calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>

       Toplevel.theory (fn thy =>

         let

           val ctxt = Proof_Context.init_global thy;

           val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;

           val set_data =

             ML_Context.expression (Input.pos_of source)

               (ml "Theory.setup (Eval_Def.set_data (" @ ML_Lex.read_source source @ ml "))")

             |> Context.theory_map;

           val eval = Eval_Def.the_data (set_data thy);

         in KEStore_Elems.add_calcs [(calcID, (c, eval))] thy end)))

 in end;

 \<close>

 section \<open>Re-use existing access functions for knowledge elements\<close>

 text \<open>

   The independence of problems' and methods' structure from theory dependency structure

   enforces the access functions to use "Isac_Knowledge",

   the final theory which comprises all knowledge defined.

 \<close>

 ML \<open>

 val get_ref_thy = KEStore_Elems.get_ref_thy;

 fun assoc' ([], key) = raise ERROR ("ME_Isa: rew_ord \"" ^ key ^ "\" not in system 2")

   | assoc' ((keyi, xi) :: pairs, key) =

     if key = keyi then SOME xi else assoc' (pairs, key);

 fun assoc_rew_ord thy ro = ((the o assoc') (KEStore_Elems.get_rew_ord thy, ro))

   handle ERROR _ => raise ERROR ("ME_Isa: rew_ord \"" ^ ro ^ "\" not in system 1");

 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) =

           raise 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') =

           raise 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_pbls () = get_ref_thy () |> KEStore_Elems.get_pbls;

 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;

 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;

 fun get_expls () = get_ref_thy () |> KEStore_Elems.get_expls;

 \<close>

 rule_set_knowledge

   empty = \<open>Rule_Set.empty\<close> and

   e_rrls = \<open>Rule_Set.e_rrls\<close>

 section \<open>determine sequence of main parts in thehier\<close>

 setup \<open>

 KEStore_Elems.add_thes

   [(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",

     mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),

   (Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",

     mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),

   (Thy_Write.Html {guh = Thy_Write.part2guh ["IsacScripts"], html = "",

     mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]

 \<close>

 section \<open>Functions for checking KEStore_Elems\<close>

 ML \<open>

 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, _)) : CAS_Def.T) =

   "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false

   (Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.to_string s ^ ")";

 fun count_kestore_ptyps [] = 0

   | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =

       1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';

 fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^

       (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;

 val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;

 fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);

 fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);

 fun sort_kestore_ptyp' _ [] = []

   | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =

      ((Store.Node (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,...} : Meth_Def.T) = guh : string;

 fun check_kestore_met (mp: Meth_Def.T Store.node) =

       check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;

 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = 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' Thy_Write.thes2str))) thes

 fun write_thes thydata_list =

   thydata_list 

     |> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.the2str the))

     |> map pair2str

     |> map writeln

 \<close>

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end