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

    Author:     Mathias Lehnfeld

Store of Theory_Data of all knowledge required by the Lucas-Interpreter.

Types of elements are defined in "xxxxx-def.sml". 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.)

Notable are Problem.T and MethodC.T; these are trees with a structure different from

Isabelle's theories dependencies.

*)

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"

ML_file "rewrite-order.sml"

ML_file rule.sml

ML_file "references-def.sml"

ML_file "cas-def.sml"

ML_file "model-pattern.sml"

ML_file "error-pattern-def.sml"

ML_file "rule-set.sml"

ML_file "store.sml"

ML_file "check-unique.sml"

ML_file "problem-def.sml"

ML_file "method-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>

text \<open>

  \<open>ML_structure Problem\<close>, \<open>ML_structure MethodC\<close> and \<open>Example\<close>s are held by "Know_Store".

  The structure of \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> is independent from 

  theories' dependency graph. Thus the respective elements are stored as \<open>TermC.as_string\<close>

  and parsed on the fly within the current @{ML_structure Context},

  while being loaded into \<open>ML_structure Calc\<close>.

  Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)

  are adapted for "adapt_to_type on the fly" until further clarification.

  Why \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> are not parsed on the fly

  within the current \<open>ML_structure Context\<close> see \<open>ML_structure Refine\<close>

\<open>\<close>

  Most elements of \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> are implemented in 

  \<open>directory Knowledge/\<close> but some of them are implemented in \<open>directory ProgLang/\<close>already; 

  thus \<open>theory Know_Store\<close> got this location in the directory structure.

  \<open>term Know_Store.get_*\<close> retrieves all * of the respective theory PLUS of all ancestor theories.

\<close> ML \<open>

signature KNOW_STORE =

sig

  val get_rew_ords: theory -> Rewrite_Ord.T list

  val add_rew_ords: 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_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list

  val add_calcs: (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list -> theory -> theory

  val get_cass: theory -> CAS_Def.T list

  val add_cass: 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

  val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory 

  val get_ref_last_thy: unit -> theory

  val set_ref_last_thy: theory -> unit

  val get_via_last_thy: ThyC.id -> theory (* only used for Subproblem retrieving respective thy *)

end;

structure Know_Store(**): KNOW_STORE(**) =

struct

  structure Data = Theory_Data (

    type T = Rewrite_Ord.T list;

    val empty = [];

    val merge = merge Rewrite_Ord.equal;

    );  

  fun get_rew_ords thy = Data.get thy

  fun add_rew_ords rlss = Data.map (curry (Library.merge Rewrite_Ord.equal) rlss)

  structure Data = Theory_Data (

    type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;

                            (* ^^^^^ would allow same Rls_Set.id for different thys, NOT impl. *)

    val empty = [];

    val merge = Rule_Set.to_kestore;

    );  

  fun get_rlss thy = Data.get thy

  fun add_rlss rlss = Data.map (curry (Library.merge Rule_Set.equal) rlss)

  structure Data = Theory_Data (

    type T = (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list;

    val empty = [];

    val merge = merge Eval_Def.equal;

    );                                                              

  fun get_calcs thy = Data.get thy

  fun add_calcs calcs = Data.map (curry (Library.merge Eval_Def.equal) calcs)

  structure Data = Theory_Data (

    type T = (term * (References_Def.T * CAS_Def.generate_fn)) list;

    val empty = [];

    val merge = merge CAS_Def.equal;

    );                                                              

  fun get_cass thy = Data.get thy

  fun add_cass cas = Data.map (curry (Library.merge CAS_Def.equal) cas)

  structure Data = Theory_Data (

    type T = Probl_Def.store;

    val empty = [Probl_Def.empty_store];

    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 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 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 merge = Store.merge;

    );                                                              

  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 last_thy = Synchronized.var "finally_knowledge_complete" @{theory};

  fun set_ref_last_thy thy = Synchronized.change last_thy (fn _ => thy); (* never RE-set ! *)

  fun get_ref_last_thy () = Synchronized.value last_thy;

fun get_via_last_thy thy_id =

  let

    val last_thy = get_ref_last_thy ()

    val known_thys = Theory.nodes_of last_thy

  in 

    (find_first (fn thy => Context.theory_name thy = thy_id) known_thys

      |> the)

    handle Option.Option => raise ERROR ("get_via_last_thy fails with " ^ quote thy_id)

  end

(**)end(*struct*);

\<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 (Know_Store.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.ml_fun_to_store (" @ ML_Lex.read_source source @ ml "))")

            |> Context.theory_map;

          val eval = Eval_Def.ml_fun_from_store (set_data thy);

        in Know_Store.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_last_thy = Know_Store.get_ref_last_thy;

(*val get_rew_ord: Proof.context -> string -> Rewrite_Ord.function*)

fun get_rew_ord ctxt (id: Rewrite_Ord.id) = 

  case AList.lookup (op =) (Know_Store.get_rew_ords (Proof_Context.theory_of ctxt)) id of

    SOME function => function: Rewrite_Ord.function

  | NONE => raise ERROR ("rewrite-order \"" ^ id ^ "\" missing in theory \"" ^ 

    (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^

    "\nTODO exception hierarchy needs to be established.")

(*val get_rls: Proof.context -> Rule_Set.id -> Rule_Def.rule_set*)

fun get_rls ctxt (id : Rule_Set.id) =

  case AList.lookup (op =) (Know_Store.get_rlss (Proof_Context.theory_of ctxt)) id of

    SOME (_, rls) => rls

  | NONE => raise ERROR ("rls \"" ^ id ^ "\" missing in theory \"" ^ 

    (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^

    "\nTODO exception hierarchy needs to be established.")

(*val get_calc: Proof.context -> Eval_Def.prog_id -> 

  Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)*)

fun get_calc ctxt (id: Eval_Def.prog_id) = 

  case AList.lookup (op =) (Know_Store.get_calcs (Proof_Context.theory_of ctxt)) id of

    SOME const_id__ml_fun => (id, const_id__ml_fun)

  | NONE => raise ERROR ("ml-calculation \"" ^ id ^ "\" missing in theory \"" ^ 

    (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^

    "\nTODO exception hierarchy needs to be established.")

(*val get_calc_prog_id: Proof.context -> Eval_Def.const_id -> Eval_Def.prog_id*)

fun get_calc_prog_id ctxt (const_id: Eval_Def.const_id) =

  let

    fun assoc ([], prog_id) =

        raise ERROR ("ml-calculation \"" ^ prog_id ^ "\" missing in theory \"" ^ 

          (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)." ^

          "\nThus " ^ quote const_id  ^ " cannot be retrieved." ^

          "\nTODO exception hierarchy needs to be established.")

      | assoc ((prog_id, (const_id, _)) :: pairs, key) =

          if key = const_id then prog_id else assoc (pairs, key);

  in assoc (ctxt |> Proof_Context.theory_of |> Know_Store.get_calcs, const_id) end;

(*val get_cas: Proof.context -> term -> References_Def.T * CAS_Def.generate_fn*)

fun get_cas ctxt tm = 

  case AList.lookup (op =) (Know_Store.get_cass (Proof_Context.theory_of ctxt)) tm of

    SOME refs__gen_fun => refs__gen_fun: References_Def.T * CAS_Def.generate_fn

  | NONE => raise ERROR ("CAS_Cmd \"" ^ 

    UnparseC.term_in_thy (get_ref_last_thy ()) tm ^ "\" missing in theory \"" ^ 

    (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^

    "\nTODO exception hierarchy needs to be established.")

(*for starting an Exmaple by CAS_Cmd*)

(*val get_cas_global: term -> References_Def.T * CAS_Def.generate_fn*)

fun get_cas_global tm =

  let

    val thy = get_ref_last_thy ()

  in

    case AList.lookup (op =) (Know_Store.get_cass thy) tm of

      NONE => (writeln ("CAS_Cmd \"" ^ 

          UnparseC.term_in_thy thy tm ^ "\" missing in theory \"" ^ 

          (thy |> Context.theory_name) ^ "\" (and ancestors).");

        NONE)

    | SOME refs__gen_fun => SOME refs__gen_fun

  end

fun get_pbls () = get_ref_last_thy () |> Know_Store.get_pbls;

fun get_mets () = get_ref_last_thy () |> Know_Store.get_mets;

fun get_thes () = get_ref_last_thy () |> Know_Store.get_thes;

fun get_expls () = get_ref_last_thy () |> Know_Store.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>

Know_Store.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 Know_Store\<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.eval_ml_from_prog)  = "(" ^ 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