(* Title:  MathEngBasic/problem.sml

   Author: Walther Neuper 2019

   (c) due to copyright terms

*)

signature PROBLEM =

sig

  type T = Probl_Def.T

  type id = Probl_Def.id

  type id_reverse

  val id_empty: id

  val id_to_string: id -> string

  type input

  type model_input

  val split_did: term -> term * term

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

  val prep_input : theory -> Check_Unique.id -> string list -> id -> input -> T * id                       

  val set_data: Rule_Def.rule_set -> theory -> theory

  val the_data: theory -> Rule_Def.rule_set

  val parse_item: string parser -> 'a parser -> 'a parser

  val parse_item_name: string parser -> string -> string parser

  val parse_item_names: string parser -> string list parser

  val parse_model_input: model_input parser

  val parse_authors: string list parser

  val from_store: id -> T

end

(**)

structure Problem(**): PROBLEM(**) =

struct

(**)

type T = Probl_Def.T;

(*

  elements if the id are in reverse order as compared to MethodC:

  e.g. ["linear", "univariate", "equation"] has "equation" as parent node --

  -- this makes the id readable.

*)

type id = Probl_Def.id;

(* same order as for MethodC (used in Store )*)

type id_reverse = Probl_Def.id;

val id_empty = Probl_Def.id_empty;

val id_to_string = Probl_Def.id_to_string;

(** prepare Problem for Store **)

type model_input =

  (Model_Pattern.m_field *     (* "#Given", "#Find", "#Where", "#Relate" *)

    TermC.as_string list)      (* list of items belonging to m_field     *)

  list;                        (* list of "#Given" .. "#Relate"          *)

type input =

  id *                         (* the key into the problem hierarchy     *)

  model_input *                (* e.g. ("#Given", ["unsorted u_u"]) list *)

  Rule_Set.T *                 (* for evaluating "#Where"                *)

  TermC.as_string option *     (* CAS_Cmd                                *)

  Meth_Def.id list;            (* methods that can solve the problem     *)

(* split a term into description and (id | structured variable) for pbt, met.ppc *)

fun split_did t =

  let

    val (hd, arg) = case strip_comb t of

      (hd, [arg]) => (hd, arg)

    | _ => raise ERROR ("split_did: doesn't match (hd,[arg]) for t = " ^ UnparseC.term t)

  in (hd, arg) end

(* prepare problem-types before storing in pbltypes; 

   dont forget to "check_guh_unique" before ins   *)

fun prep_input thy guh maa init ((pblID, dsc_dats, ev, ca, metIDs): input) : T * id =

    let

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

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

      val gi = (case gi of

		    [] => []

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

        (case \<^try>\<open> map (split_did o (TermC.parseNEW'' thy)) gi'\<close> of

          SOME x => x

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

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

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

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

		  val fi = (case fi of

		    [] => []

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

        (case \<^try>\<open> map (split_did o (TermC.parseNEW'' thy)) fi'\<close> of

          SOME x => x

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

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

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

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

		  val re = (case re of

		    [] => []

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

        (case \<^try>\<open> map (split_did o (TermC.parseNEW'' thy)) re'\<close> of

          SOME x => x

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

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

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

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

		  val wh = (case wh of

		    [] => []

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

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

          SOME x => x

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

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

    in

      ({guh = guh, mathauthors = maa, init = init, thy = thy,

        cas = Option.map (TermC.parseNEW'' thy) ca,

			  prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)

    end;

(** Isar command **)

(* theory data *)

structure Data = Theory_Data

(

  type T = Rule_Def.rule_set option;

  val empty = NONE;

  val extend = I;

  fun merge _ = NONE;

);

val set_data = Data.put o SOME;

val the_data = the o Data.get;

(* auxiliary parsers *)

fun parse_item (keyword: string parser) (parse: 'a parser) =

  (keyword -- Args.colon) |-- Parse.!!! parse;

fun parse_item_name keyword =

  Scan.optional (parse_item keyword Parse.name);

fun parse_item_names (keyword: string parser) =

  Scan.optional (parse_item keyword (Scan.repeat1 Parse.name)) [];

fun parse_tagged_terms keyword (tag: string) =

  Scan.optional (parse_item keyword (Scan.repeat Parse.term) >> (fn ts => [(tag, ts)])) [];

val parse_model_input : model_input parser =

  parse_tagged_terms \<^keyword>\<open>Given\<close> "#Given" @@@

  parse_tagged_terms \<^keyword>\<open>Where\<close> "#Where" @@@

  parse_tagged_terms \<^keyword>\<open>Find\<close> "#Find" @@@

  parse_tagged_terms \<^keyword>\<open>Relate\<close> "#Relate";

val parse_authors = parse_item_names \<^keyword>\<open>Author\<close>;

(* command definition *)

local

val parse_methods = parse_item_names \<^keyword>\<open>Method\<close>;

val parse_cas = Scan.option (parse_item \<^keyword>\<open>CAS\<close> Parse.term);

val ml = ML_Lex.read;

val _ =

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

    "prepare ISAC problem type and register it to Knowledge Store"

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

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

        parse_methods -- parse_cas -- parse_model_input)) >>

      (fn (name, (id, ((((source, maa), mets), cas), model_input))) =>

        Toplevel.theory (fn thy =>

          let

            val pblID = References_Def.explode_id id;

            val metIDs = map References_Def.explode_id mets;

            val set_data =

              ML_Context.expression (Input.pos_of source)

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

              |> Context.theory_map;

            val input = the_data (set_data thy);

            val arg = prep_input thy name maa id_empty (pblID, model_input, input, cas, metIDs);

          in KEStore_Elems.add_pbts [arg] thy end)))

in end;

(** get MethodC from Store **)

fun from_store id = Store.get (get_ptyps ()) id (rev id);

(**)end(**)