(* Title:  Interpret/lucas-interpreter.sml

    Author: Walther Neuper 2019

    (c) due to copyright terms

 *)

 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 input

   (* TODO: ------------- remove always empty --- vvvvvvvvvvv -- vvv*)

   val prep_input : theory ->  Check_Unique.id -> string list -> id ->

      id * Problem.model_input * input * thm -> T * id

   val from_store: id -> T

   val from_store': theory -> 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 *)

 type input = 

   {calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,

     prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T}

 fun prep_input thy guh maa init

 	    (metID, ppc,

         {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,

           errpats = ep, nrls = nr}, scr) =

     let

       fun eq f (f', _) = f = f';

       val gi = filter (eq "#Given") ppc;

       val gi = (case gi of

 		    [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])

 		  | ((_, gi') :: []) => 

         (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) gi'\<close> of

           SOME x => x

         | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))

 		  | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));

 		  val gi = map (pair "#Given") gi;

 		  val fi = filter (eq "#Find") ppc;

 		  val fi = (case fi of

 		    [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])

 		  | ((_, fi') :: []) => 

         (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) fi'\<close> of

           SOME x => x

         | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))

 		  | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));

 		  val fi = map (pair "#Find") fi;

 		  val re = filter (eq "#Relate") ppc;

 		  val re = (case re of

 		    [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])

 		  | ((_,re') :: []) =>

         (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) re'\<close> of

           SOME x => x

         | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))

 		  | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));

 		  val re = map (pair "#Relate") re;

 		  val wh = filter (eq "#Where") ppc;

 		  val wh = (case wh of

 		    [] => (writeln ("prep_input: in " ^ guh ^ " #Where is empty ?!?"); [])

 		  | ((_, wh') :: []) => 

         (case \<^try>\<open> map (TermC.parse_patt thy) wh'\<close> of

           SOME x => x

         | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))

 		  | _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str metID));

 		  val sc = Program.prep_program scr

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

     in

        ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro,

          erls = rls, srls = srls, prls = prls, calc = calc,

          crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID)

     end;

 (** get MethodC from Store **)

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

 fun from_store metID = Store.get (get_mets ()) metID metID;

 fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID;

 (**)end(**)