src/Tools/isac/BaseDefinitions/Know_Store.thy
author wneuper <Walther.Neuper@jku.at>
Sat, 04 Feb 2023 16:20:45 +0100
changeset 60673 ef24b1eed505
parent 60671 8998cb4818dd
child 60676 8c37f1009457
permissions -rw-r--r--
eliminate use of Thy_Info 21: replace Unparse.term, TermC.unparse_ERROR for far off ctxt
     1 (*  Title:      src/Tools/isac/Know_Store.thy
     2     Author:     Mathias Lehnfeld
     3 
     4 Store of Theory_Data of all knowledge required by the Lucas-Interpreter.
     5 
     6 Types of elements are defined in "xxxxx-def.sml". These files have companion files "xxxxx.sml" 
     7 with all further code, located at appropriate positions in the file structure.
     8 (The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by
     9 appropriate use of polymorphic high order functions.)
    10 
    11 Notable are Problem.T and MethodC.T; these are trees with a structure different from
    12 Isabelle's theories dependencies.
    13 *)
    14 
    15 theory Know_Store
    16   imports Complex_Main
    17   keywords "rule_set_knowledge" "calculation" :: thy_decl
    18 begin
    19 
    20 setup \<open>
    21   ML_Antiquotation.conditional \<^binding>\<open>isac_test\<close>
    22     (fn _ => Options.default_bool \<^system_option>\<open>isac_test\<close>)
    23 \<close>
    24 
    25 ML_file libraryC.sml
    26 ML_file theoryC.sml
    27 ML_file parseC.sml
    28 ML_file unparseC.sml
    29 ML_file "rule-def.sml"
    30 ML_file "thmC-def.sml"
    31 ML_file "eval-def.sml"
    32 ML_file "rewrite-order.sml"
    33 ML_file rule.sml
    34 ML_file "references-def.sml"
    35 ML_file "cas-def.sml"
    36 ML_file "model-pattern.sml"
    37 ML_file "error-pattern-def.sml"
    38 ML_file "rule-set.sml"
    39 
    40 ML_file "store.sml"
    41 ML_file "check-unique.sml"
    42 ML_file "problem-def.sml"
    43 ML_file "method-def.sml"
    44 ML_file "formalise.sml"
    45 ML_file "example.sml"
    46 
    47 ML \<open>
    48 \<close> ML \<open>
    49 \<close> ML \<open>
    50 \<close>
    51 section \<open>Knowledge elements for problems and methods\<close>
    52 text \<open>
    53   \<open>ML_structure Problem\<close>, \<open>ML_structure MethodC\<close> and \<open>Example\<close>s are held by "Know_Store".
    54 
    55   The structure of \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> is independent from 
    56   theories' dependency graph. Thus the respective elements are stored as \<open>TermC.as_string\<close>
    57   and parsed on the fly within the current @{ML_structure Context},
    58   while being loaded into \<open>ML_structure Calc\<close>.
    59 
    60   Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)
    61   are adapted for "adapt_to_type on the fly" until further clarification.
    62   Why \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> are not parsed on the fly
    63   within the current \<open>ML_structure Context\<close> see \<open>ML_structure Refine\<close>
    64 \<open>\<close>
    65   Most elements of \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> are implemented in 
    66   \<open>directory Knowledge/\<close> but some of them are implemented in \<open>directory ProgLang/\<close>already; 
    67   thus \<open>theory Know_Store\<close> got this location in the directory structure.
    68 
    69   \<open>term Know_Store.get_*\<close> retrieves all * of the respective theory PLUS of all ancestor theories.
    70 \<close> ML \<open>
    71 signature KNOW_STORE =
    72 sig
    73   val get_rew_ords: theory -> Rewrite_Ord.T list
    74   val add_rew_ords: Rewrite_Ord.T list -> theory -> theory
    75   val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
    76   val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
    77   val get_calcs: theory -> (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list
    78   val add_calcs: (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list -> theory -> theory
    79   val get_cass: theory -> CAS_Def.T list
    80   val add_cass: CAS_Def.T list -> theory -> theory
    81   val get_pbls: theory -> Probl_Def.store
    82   val add_pbls: Proof.context -> (Probl_Def.T * References_Def.id) list -> theory -> theory
    83   val get_mets: theory -> Meth_Def.store
    84   val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory
    85   val get_expls: theory -> Example.store
    86   val add_expls: (Example.T * Store.key) list -> theory -> theory
    87   val get_ref_last_thy: unit -> theory
    88   val set_ref_last_thy: theory -> unit
    89   val get_via_last_thy: ThyC.id -> theory (*only used for * (Sub-)problem retrieving respective thy
    90                                                           * problem refinement                    
    91                                                           * in fun UnparseC.term_ERROR           *)
    92 end;
    93 
    94 structure Know_Store(**): KNOW_STORE(**) =
    95 struct
    96   structure Data = Theory_Data (
    97     type T = Rewrite_Ord.T list;
    98     val empty = [];
    99     val merge = merge Rewrite_Ord.equal;
   100     );  
   101   fun get_rew_ords thy = Data.get thy
   102   fun add_rew_ords rlss = Data.map (curry (Library.merge Rewrite_Ord.equal) rlss)
   103 
   104   structure Data = Theory_Data (
   105     type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
   106                             (* ^^^^^ would allow same Rls_Set.id for different thys, NOT impl. *)
   107     val empty = [];
   108     val merge = Rule_Set.to_kestore;
   109     );  
   110   fun get_rlss thy = Data.get thy
   111   fun add_rlss rlss = Data.map (curry (Library.merge Rule_Set.equal) rlss)
   112 
   113   structure Data = Theory_Data (
   114     type T = (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list;
   115     val empty = [];
   116     val merge = merge Eval_Def.equal;
   117     );                                                              
   118   fun get_calcs thy = Data.get thy
   119   fun add_calcs calcs = Data.map (curry (Library.merge Eval_Def.equal) calcs)
   120 
   121   structure Data = Theory_Data (
   122     type T = (term * (References_Def.T * CAS_Def.generate_fn)) list;
   123     val empty = [];
   124     val merge = merge CAS_Def.equal;
   125     );                                                              
   126   fun get_cass thy = Data.get thy
   127   fun add_cass cas = Data.map (curry (Library.merge CAS_Def.equal) cas)
   128 
   129   structure Data = Theory_Data (
   130     type T = Probl_Def.store;
   131     val empty = [Probl_Def.empty_store];
   132     val merge = Store.merge;
   133     );
   134   fun get_pbls thy = Data.get thy;
   135   fun add_pbls ctxt pbts thy =
   136     let
   137       fun add_pbt (pbt as {guh,...}, pblID) =
   138         (* the pblID has the leaf-element as first; better readability achieved *)
   139         (if (Config.get ctxt check_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
   140           rev pblID |> Store.insert pblID pbt);
   141     in Data.map (fold add_pbt pbts) thy end;
   142 
   143   structure Data = Theory_Data (
   144     type T = Meth_Def.store;
   145     val empty = [Meth_Def.empty_store];
   146     val merge = Store.merge;
   147     );
   148   val get_mets = Data.get;
   149   fun add_mets ctxt mets thy =
   150     let
   151       fun add_met (met as {guh,...}, metID) =
   152         (if (Config.get ctxt check_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
   153           Store.insert metID met metID);
   154     in Data.map (fold add_met mets) thy end;
   155 
   156   structure Data = Theory_Data (
   157     type T = Example.store;
   158     val empty = [Example.empty_store];
   159     val merge = Store.merge;
   160     );
   161   val get_expls = Data.get;
   162   fun add_expls expls thy =
   163     let
   164       fun add_expl (expl, expl_id) = Store.insert expl_id expl expl_id;
   165     in Data.map (fold add_expl expls) thy end;
   166 
   167 
   168   val last_thy = Synchronized.var "finally_knowledge_complete" @{theory};
   169   fun set_ref_last_thy thy = Synchronized.change last_thy (fn _ => thy); (* never RE-set ! *)
   170   fun get_ref_last_thy () = Synchronized.value last_thy;
   171 
   172 fun get_via_last_thy thy_id =
   173   let
   174     val last_thy = get_ref_last_thy ()
   175     val known_thys = Theory.nodes_of last_thy
   176   in 
   177     (find_first (fn thy => Context.theory_name thy = thy_id) known_thys
   178       |> the)
   179     handle Option.Option => raise ERROR ("get_via_last_thy fails with " ^ quote thy_id)
   180   end
   181 
   182 (**)end(*struct*);
   183 \<close>
   184 
   185 
   186 subsection \<open>Isar command syntax\<close>
   187 
   188 ML \<open>
   189 local
   190 
   191 val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);
   192 
   193 val ml = ML_Lex.read;
   194 
   195 fun ml_rule thy (name, source) =
   196   ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @
   197   ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @
   198   ML_Lex.read_source source @ ml "))";
   199 
   200 fun ml_rules thy args =
   201   ml "Theory.setup (Know_Store.add_rlss [" @
   202     flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
   203 
   204 val _ =
   205   Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"
   206     (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
   207       thy |> Context.theory_map
   208         (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
   209 
   210 val calc_name =
   211   Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||
   212   Scan.ahead Parse.name -- Parse.const;
   213 
   214 val _ =
   215   Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>
   216     "prepare ISAC calculation and register it to Knowledge Store"
   217     (calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>
   218       Toplevel.theory (fn thy =>
   219         let
   220           val ctxt = Proof_Context.init_global thy;
   221           val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
   222           val set_data =
   223             ML_Context.expression (Input.pos_of source)
   224               (ml "Theory.setup (Eval_Def.ml_fun_to_store (" @ ML_Lex.read_source source @ ml "))")
   225             |> Context.theory_map;
   226           val eval = Eval_Def.ml_fun_from_store (set_data thy);
   227         in Know_Store.add_calcs [(calcID, (c, eval))] thy end)))
   228 
   229 in end;
   230 \<close>
   231 
   232 
   233 section \<open>Re-use existing access functions for knowledge elements\<close>
   234 text \<open>
   235   The independence of problems' and methods' structure from theory dependency structure
   236   enforces the access functions to use "Isac_Knowledge",
   237   the final theory which comprises all knowledge defined.
   238 \<close>
   239 ML \<open>
   240 val get_ref_last_thy = Know_Store.get_ref_last_thy;
   241 
   242 (*val get_rew_ord: Proof.context -> string -> Rewrite_Ord.function*)
   243 fun get_rew_ord ctxt (id: Rewrite_Ord.id) = 
   244   case AList.lookup (op =) (Know_Store.get_rew_ords (Proof_Context.theory_of ctxt)) id of
   245     SOME function => function: Rewrite_Ord.function
   246   | NONE => raise ERROR ("rewrite-order \"" ^ id ^ "\" missing in theory \"" ^ 
   247     (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
   248     "\nTODO exception hierarchy needs to be established.")
   249 
   250 (*val get_rls: Proof.context -> Rule_Set.id -> Rule_Def.rule_set*)
   251 fun get_rls ctxt (id : Rule_Set.id) =
   252   case AList.lookup (op =) (Know_Store.get_rlss (Proof_Context.theory_of ctxt)) id of
   253     SOME (_, rls) => rls
   254   | NONE => raise ERROR ("rls \"" ^ id ^ "\" missing in theory \"" ^ 
   255     (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
   256     "\nTODO exception hierarchy needs to be established.")
   257 
   258 (*val get_calc: Proof.context -> Eval_Def.prog_id -> 
   259   Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)*)
   260 fun get_calc ctxt (id: Eval_Def.prog_id) = 
   261   case AList.lookup (op =) (Know_Store.get_calcs (Proof_Context.theory_of ctxt)) id of
   262     SOME const_id__ml_fun => (id, const_id__ml_fun)
   263   | NONE => raise ERROR ("ml-calculation \"" ^ id ^ "\" missing in theory \"" ^ 
   264     (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
   265     "\nTODO exception hierarchy needs to be established.")
   266 
   267 (*val get_calc_prog_id: Proof.context -> Eval_Def.const_id -> Eval_Def.prog_id*)
   268 fun get_calc_prog_id ctxt (const_id: Eval_Def.const_id) =
   269   let
   270     fun assoc ([], prog_id) =
   271         raise ERROR ("ml-calculation \"" ^ prog_id ^ "\" missing in theory \"" ^ 
   272           (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)." ^
   273           "\nThus " ^ quote const_id  ^ " cannot be retrieved." ^
   274           "\nTODO exception hierarchy needs to be established.")
   275       | assoc ((prog_id, (const_id, _)) :: pairs, key) =
   276           if key = const_id then prog_id else assoc (pairs, key);
   277   in assoc (ctxt |> Proof_Context.theory_of |> Know_Store.get_calcs, const_id) end;
   278 
   279 (*val get_cas: Proof.context -> term -> References_Def.T * CAS_Def.generate_fn*)
   280 fun get_cas ctxt tm = 
   281   case AList.lookup (op =) (Know_Store.get_cass (Proof_Context.theory_of ctxt)) tm of
   282     SOME refs__gen_fun => refs__gen_fun: References_Def.T * CAS_Def.generate_fn
   283   | NONE => raise ERROR ("CAS_Cmd \"" ^ 
   284     UnparseC.term_in_thy (get_ref_last_thy ()) tm ^ "\" missing in theory \"" ^ 
   285     (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
   286     "\nTODO exception hierarchy needs to be established.")
   287 
   288 (*for starting an Exmaple by CAS_Cmd*)
   289 (*val get_cas_global: term -> References_Def.T * CAS_Def.generate_fn*)
   290 fun get_cas_global tm =
   291   let
   292     val thy = get_ref_last_thy ()
   293   in
   294     case AList.lookup (op =) (Know_Store.get_cass thy) tm of
   295       NONE => (writeln ("CAS_Cmd \"" ^ 
   296           UnparseC.term_in_thy thy tm ^ "\" missing in theory \"" ^ 
   297           (thy |> Context.theory_name) ^ "\" (and ancestors).");
   298         NONE)
   299     | SOME refs__gen_fun => SOME refs__gen_fun
   300   end
   301 
   302 
   303 fun get_pbls () = get_ref_last_thy () |> Know_Store.get_pbls;
   304 fun get_mets () = get_ref_last_thy () |> Know_Store.get_mets;
   305 fun get_expls () = get_ref_last_thy () |> Know_Store.get_expls;
   306 \<close>
   307 
   308 rule_set_knowledge
   309   empty = \<open>Rule_Set.empty\<close> and
   310   e_rrls = \<open>Rule_Set.e_rrls\<close>
   311 
   312 section \<open>Functions for checking Know_Store\<close>
   313 ML \<open>
   314 fun short_string_of_rls Rule_Set.Empty = "Erls"
   315   | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
   316     "Rls {#calc = " ^ string_of_int (length calc) ^
   317     ", #rules = " ^ string_of_int (length rules) ^ ", ..."
   318   | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
   319     "Seq {#calc = " ^ string_of_int (length calc) ^
   320     ", #rules = " ^ string_of_int (length rules) ^ ", ..."
   321   | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
   322 fun check_kestore_rls (rls', (thyID, rls)) =
   323   "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
   324 
   325 fun check_kestore_calc ((id, (c, _)) : Rule_Def.eval_ml_from_prog)  = "(" ^ id ^ ", (" ^ c ^ ", fn))";
   326 
   327 (* we avoid term_to_string''' defined later *)
   328 fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
   329   "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
   330   (Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.to_string s ^ ")";
   331 
   332 fun count_kestore_ptyps [] = 0
   333   | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
   334       1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';
   335 fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
   336       (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
   337 fun check_kestore_ptyp ctxt ptyp = check_kestore_ptyp' (Probl_Def.s_to_string ctxt) ptyp;
   338 fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
   339 fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
   340 fun sort_kestore_ptyp' _ [] = []
   341   | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
   342      ((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
   343        :: sort_kestore_ptyp' ordfun ps');
   344 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
   345 
   346 fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
   347 fun check_kestore_met (mp: Meth_Def.T Store.node) =
   348       check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
   349 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
   350 val sort_kestore_met = sort_kestore_ptyp' met_ord;
   351 \<close>
   352 
   353 ML \<open>
   354 \<close> ML \<open>
   355 \<close> ML \<open>
   356 \<close>
   357 end