1.1 --- a/src/Tools/isac/MathEngBasic/method.sml	Sat Jun 12 18:33:15 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/method.sml	Tue Jun 15 22:24:20 2021 +0200
     1.3 @@ -17,6 +17,9 @@
     1.4    val prep_input : theory ->  Check_Unique.id -> string list -> id ->
     1.5       id * Problem.model_input * input * thm -> T * id
     1.6  
     1.7 +  val set_input: input -> theory -> theory
     1.8 +  val the_input: theory -> input
     1.9 +
    1.10    val from_store: id -> T
    1.11    val from_store': theory -> id -> T
    1.12  end
    1.13 @@ -41,7 +44,7 @@
    1.14    {calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
    1.15      prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T}
    1.16  
    1.17 -fun prep_input thy guh maa init
    1.18 +fun prep_input thy guh (mathauthors: string list) (init: References_Def.id)
    1.19  	    (metID, ppc,
    1.20          {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
    1.21            errpats = ep, nrls = nr}, scr) =
    1.22 @@ -88,12 +91,68 @@
    1.23  		  val sc = Program.prep_program scr
    1.24  		  val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
    1.25      in
    1.26 -       ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro,
    1.27 -         erls = rls, srls = srls, prls = prls, calc = calc,
    1.28 +       ({guh = guh, mathauthors = mathauthors, init = init, ppc = gi @ fi @ re, pre = wh,
    1.29 +         rew_ord' = ro, erls = rls, srls = srls, prls = prls, calc = calc,
    1.30           crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID)
    1.31      end;
    1.32  
    1.33  
    1.34 +(** Isar command **)
    1.35 +
    1.36 +structure Data = Theory_Data
    1.37 +(
    1.38 +  type T = input option;
    1.39 +  val empty = NONE;
    1.40 +  val extend = I;
    1.41 +  fun merge _ = NONE;
    1.42 +);
    1.43 +
    1.44 +val set_input = Data.put o SOME;
    1.45 +val the_input = the o Data.get;
    1.46 +
    1.47 +local
    1.48 +
    1.49 +fun parse_item keyword parse = (keyword -- Args.colon) |-- Parse.!!! parse;
    1.50 +
    1.51 +val parse_authors =
    1.52 +  Scan.optional (parse_item \<^keyword>\<open>Author\<close> (Scan.repeat1 Parse.name)) [];
    1.53 +
    1.54 +val parse_program =
    1.55 +  Scan.option (parse_item \<^keyword>\<open>Program\<close> (Parse.position Parse.name));
    1.56 +
    1.57 +fun parse_terms keyword (tag: string) =
    1.58 +  Scan.optional (parse_item keyword (Scan.repeat Parse.term) >> (fn ts => [(tag, ts)])) [];
    1.59 +
    1.60 +val parse_ppc =
    1.61 +  parse_terms \<^keyword>\<open>Given\<close> "#Given" @@@
    1.62 +  parse_terms \<^keyword>\<open>Where\<close> "#Where" @@@
    1.63 +  parse_terms \<^keyword>\<open>Find\<close> "#Find" @@@
    1.64 +  parse_terms \<^keyword>\<open>Relate\<close> "#Relate";
    1.65 +
    1.66 +val ml = ML_Lex.read;
    1.67 +
    1.68 +val _ =
    1.69 +  Outer_Syntax.command \<^command_keyword>\<open>method\<close>
    1.70 +    "prepare ISAC method and register it to Knowledge Store"
    1.71 +    (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --
    1.72 +      Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- parse_authors -- parse_program -- parse_ppc)) >>
    1.73 +      (fn (name, (id, (((source, mathauthors), simp), ppc))) => Toplevel.theory (fn thy =>
    1.74 +        let
    1.75 +          val metID = References_Def.explode_id id;
    1.76 +          val eval_input =
    1.77 +            ML_Context.expression (Input.pos_of source)
    1.78 +              (ml "Theory.setup (MethodC.set_input (" @ ML_Lex.read_source source @ ml "))")
    1.79 +            |> Context.theory_map;
    1.80 +          val input = the_input (eval_input thy);
    1.81 +          val thm =
    1.82 +            (case simp of
    1.83 +              NONE => @{thm refl}
    1.84 +            | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a));
    1.85 +          val arg = prep_input thy name mathauthors id_empty (metID, ppc, input, thm);
    1.86 +        in KEStore_Elems.add_mets [arg] thy end)))
    1.87 +
    1.88 +in end;
    1.89 +
    1.90  (** get MethodC from Store **)
    1.91  
    1.92  (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)