walther@59894: (* Title:  Interpret/lucas-interpreter.sml
walther@59894:    Author: Walther Neuper 2019
walther@59894:    (c) due to copyright terms
walther@59894: *)
walther@59894: 
walther@59894: signature METHOD =
walther@59894: sig
walther@59895:   type T = Meth_Def.T
walther@59903:   val empty: T
walther@59903: 
walther@59903:   type id = Meth_Def.id
walther@59903:   val id_empty: id
walther@59903:   val id_to_string: id -> string
walther@59970: 
walther@59973:   type input
walther@59973:   (* TODO: ------------- remove always empty --- vvvvvvvvvvv -- vvv*)
walther@59973:   val prep_input : theory ->  Check_Unique.id -> string list -> id ->
walther@59973:      id * Problem.model_input * input * thm -> T * id
walther@59973: 
wenzelm@60307:   val set_data: input -> theory -> theory
wenzelm@60307:   val the_data: theory -> input
wenzelm@60303: 
walther@59970:   val from_store: id -> T
walther@59970:   val from_store': theory -> id -> T
walther@59894: end
walther@59894: 
walther@59894: (**)
walther@60154: structure MethodC(**): METHOD(**) =
walther@59894: struct
walther@59894: (**)
walther@59894: 
walther@59895: type T = Meth_Def.T;
walther@59903: val empty = Meth_Def.empty;
walther@59903: 
walther@59903: type id = Meth_Def.id;
walther@59903: val id_empty = Meth_Def.id_empty;
walther@59903: val id_to_string = Meth_Def.id_to_string;
walther@59894: 
walther@59973: 
walther@60154: (** prepare MethodC for Store **)
walther@59973: 
walther@60154: (* a subset of MethodC.T record's fields *)
walther@59973: type input = 
walther@59973:   {calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
walther@59973:     prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T}
walther@59973: 
wenzelm@60303: fun prep_input thy guh (mathauthors: string list) (init: References_Def.id)
walther@59973: 	    (metID, ppc,
walther@59973:         {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
walther@59973:           errpats = ep, nrls = nr}, scr) =
walther@59973:     let
walther@59973:       fun eq f (f', _) = f = f';
walther@59973:       val gi = filter (eq "#Given") ppc;
walther@59973:       val gi = (case gi of
walther@59973: 		    [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])
walther@60265: 		  | ((_, gi') :: []) => 
walther@60417:         (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) gi'\<close> of
walther@60265:           SOME x => x
walther@60265:         | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))
walther@59973: 		  | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
walther@59973: 		  val gi = map (pair "#Given") gi;
walther@59973: 
walther@59973: 		  val fi = filter (eq "#Find") ppc;
walther@59973: 		  val fi = (case fi of
walther@59973: 		    [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])
walther@60265: 		  | ((_, fi') :: []) => 
walther@60417:         (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) fi'\<close> of
walther@60265:           SOME x => x
walther@60265:         | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))
walther@59973: 		  | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
walther@59973: 		  val fi = map (pair "#Find") fi;
walther@59973: 
walther@59973: 		  val re = filter (eq "#Relate") ppc;
walther@59973: 		  val re = (case re of
walther@59973: 		    [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])
walther@60265: 		  | ((_,re') :: []) =>
walther@60417:         (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) re'\<close> of
walther@60265:           SOME x => x
walther@60265:         | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))
walther@59973: 		  | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
walther@59973: 		  val re = map (pair "#Relate") re;
walther@59973: 
walther@59973: 		  val wh = filter (eq "#Where") ppc;
walther@59973: 		  val wh = (case wh of
walther@59973: 		    [] => (writeln ("prep_input: in " ^ guh ^ " #Where is empty ?!?"); [])
walther@60265: 		  | ((_, wh') :: []) => 
walther@60265:         (case \<^try>\<open> map (TermC.parse_patt thy) wh'\<close> of
walther@60265:           SOME x => x
walther@60265:         | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))
walther@59973: 		  | _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
walther@59973: 		  val sc = Program.prep_program scr
walther@59973: 		  val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
walther@59973:     in
wenzelm@60303:        ({guh = guh, mathauthors = mathauthors, init = init, ppc = gi @ fi @ re, pre = wh,
wenzelm@60303:          rew_ord' = ro, erls = rls, srls = srls, prls = prls, calc = calc,
walther@59973:          crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID)
walther@59973:     end;
walther@59973: 
walther@59973: 
wenzelm@60303: (** Isar command **)
wenzelm@60303: 
wenzelm@60303: structure Data = Theory_Data
wenzelm@60303: (
wenzelm@60303:   type T = input option;
wenzelm@60303:   val empty = NONE;
wenzelm@60303:   val extend = I;
wenzelm@60303:   fun merge _ = NONE;
wenzelm@60303: );
wenzelm@60303: 
wenzelm@60307: val set_data = Data.put o SOME;
wenzelm@60307: val the_data = the o Data.get;
wenzelm@60303: 
wenzelm@60303: local
wenzelm@60303: 
wenzelm@60303: val parse_program =
wenzelm@60307:   Scan.option (Problem.parse_item \<^keyword>\<open>Program\<close> (Parse.position Parse.name));
wenzelm@60303: 
wenzelm@60303: val ml = ML_Lex.read;
wenzelm@60303: 
wenzelm@60303: val _ =
wenzelm@60303:   Outer_Syntax.command \<^command_keyword>\<open>method\<close>
wenzelm@60303:     "prepare ISAC method and register it to Knowledge Store"
wenzelm@60303:     (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --
wenzelm@60307:       Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Problem.parse_authors --
wenzelm@60307:         parse_program -- Problem.parse_model_input)) >>
wenzelm@60307:       (fn (name, (id, (((source, maa), program), model_input))) => Toplevel.theory (fn thy =>
wenzelm@60303:         let
wenzelm@60303:           val metID = References_Def.explode_id id;
wenzelm@60314:           val set_data =
wenzelm@60303:             ML_Context.expression (Input.pos_of source)
wenzelm@60307:               (ml "Theory.setup (MethodC.set_data (" @ ML_Lex.read_source source @ ml "))")
wenzelm@60303:             |> Context.theory_map;
wenzelm@60314:           val input = the_data (set_data thy);
wenzelm@60303:           val thm =
wenzelm@60307:             (case program of
wenzelm@60303:               NONE => @{thm refl}
wenzelm@60303:             | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a));
wenzelm@60307:           val arg = prep_input thy name maa id_empty (metID, model_input, input, thm);
wenzelm@60303:         in KEStore_Elems.add_mets [arg] thy end)))
wenzelm@60303: 
wenzelm@60303: in end;
wenzelm@60303: 
walther@60154: (** get MethodC from Store **)
walther@59973: 
walther@59970: (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
walther@59970: fun from_store metID = Store.get (get_mets ()) metID metID;
walther@59970: fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID;
walther@59970: 
walther@59894: (**)end(**)