(* Title:  Interpret/lucas-interpreter.sml

    Author: Walther Neuper 2019

    (c) due to copyright terms

 \<open>ML_structure MethodC\<close> holds the essential information required for automated doing

 \<open>ML_structure Specification\<close> and \<open>ML_structure Solution\<close>.

 Why \<open>ML_structure MethodC\<close> is parsed with general types within the current \<open>ML_structure Context\<close>

 and refined with appropriate types from the ctxt of an Example.

 *)

 signature METHOD =

 sig

   type T = Meth_Def.T

   val empty: T

   type id = Meth_Def.id

   val id_empty: id

   val id_to_string: id -> string

   type ml_input

   val prep_store: theory -> Check_Unique.id -> string list -> References_Def.id ->

     id * (Model_Pattern.m_field * (Model_Def.descriptor * term)) list * term list * ml_input * thm ->

       T * id

   val set_data: ml_input -> theory -> theory

   val the_data: theory -> ml_input

   val from_store': theory -> id -> T

   val from_store: Proof.context -> id -> T

 end

 (**)

 structure MethodC(**): METHOD(**) =

 struct

 (**)

 type T = Meth_Def.T;

 val empty = Meth_Def.empty;

 type id = Meth_Def.id;

 val id_empty = Meth_Def.id_empty;

 val id_to_string = Meth_Def.id_to_string;

 (** prepare MethodC for Store **)

 (* a subset of MethodC.T record's fields occuring in \<open>method\<close> *)

 type ml_input = 

   {calc: Rule_Def.eval_ml_from_prog list, errpats: Error_Pattern_Def.T list, rew_rls: Rule_Set.T,

     where_rls: Rule_Set.T, rew_ord: Rewrite_Ord.id, rls': Rule_Set.T, prog_rls: Rule_Set.T}

 fun prep_store thy guh mathauthors start_refine (met_id, model, where_,

     {rew_ord = ro, rls' = rls, prog_rls = prog_rls, where_rls = where_rls, calc = _(*scr_isa_fns*),

       errpats = ep, rew_rls = nr}, prog) =

   let

 	  val sc = Program.prep_program prog

 	  val calc = if Thm.eq_thm (prog, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc

   in

      ({guh = guh, mathauthors = mathauthors, start_refine = start_refine, model = model(*'*),

       where_ = where_, rew_ord = ro, asm_rls = rls, prog_rls = prog_rls, where_rls = where_rls,

       calc = calc, errpats = ep, rew_rls = nr, program = Rule.Prog sc}: T, met_id)

   end;

 (** Isar command **)

 structure Data = Theory_Data

 (

   type T = ml_input option;

   val empty = NONE;

   fun merge _ = NONE;

 );

 val set_data = Data.put o SOME;

 val the_data = the o Data.get;

 local

 val drop_pos_model = (fn (a, b, _) => (a, b))

 val drop_pos_where_ = (fn (b, _) => b)

 val parse_program =

   Scan.option (Problem.parse_item \<^keyword>\<open>Program\<close> (Parse.position Parse.name));

 val ml = ML_Lex.read;

 val _ =

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

     "prepare ISAC method and register it to Knowledge Store"

     (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --

       Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Problem.parse_authors --

         parse_program -- (** )Problem.parse_model_input( **)Problem.parse_pos_model_input(**) )) >>

       (fn (name, (id, (((source, maa), program), model_input))) => Toplevel.theory (fn thy =>

         let

           val ctxt = Proof_Context.init_global thy

           val met_id = References_Def.explode_id id;

           val (model, where_) = Model_Pattern.parse_pos ctxt model_input

           val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)

           val set_data =

             ML_Context.expression (Input.pos_of source)

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

             |> Context.theory_map;

           val ml_input = the_data (set_data thy);

           val thm =

             (case program of

               NONE => @{thm refl}

             | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a));

           val arg = prep_store thy name maa id_empty (met_id, model', where_', ml_input, thm);

         in Know_Store.add_mets ctxt [arg] thy end)))      

 in end;

 (** get MethodC from Store **)

 fun adapt_to_type ctxt {guh, mathauthors, start_refine, rew_ord, asm_rls, prog_rls, (*crls,*) rew_rls, errpats, calc, 

     program, where_rls, model, where_} =

   let

     val where_ = map (ParseC.adapt_term_to_type ctxt) where_

     val model = map (Model_Pattern.adapt_to_type ctxt) model

     val errpats = map (Error_Pattern_Def.adapt_to_type ctxt) errpats

   in

     {guh = guh, mathauthors = mathauthors, start_refine = start_refine, rew_ord = rew_ord, asm_rls = asm_rls, 

     prog_rls = prog_rls, (*crls = crls,*) rew_rls = rew_rls, errpats = errpats, calc = calc, program = program, where_rls = where_rls, 

     model = model, where_ = where_}

     end

 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)

 fun from_store' thy id =

   (Store.get (Know_Store.get_mets thy) id id)

     handle ERROR _ =>

       raise error ("*** ERROR MethodC.from_store' thy " ^ strs2str id ^ " not found");

 fun from_store ctxt id =

   let

     val pbl = Store.get (get_mets ()) id id

   in adapt_to_type ctxt pbl end

     handle ERROR _ =>

       raise error ("*** ERROR MethodC.from_store ctxt " ^ strs2str id ^ " not found");

 (**)end(**)