(* Title:  MathEngBasic/problem.sml

    Author: Walther Neuper 2019

    (c) due to copyright terms

 *)

 signature PROBLEM =

 sig

   type T = Probl_Def.T

   val empty: 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

   val split_did_PIDE: term -> term * term

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

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

   val prep_input_PIDE : 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 parse_cas: Token.T list -> string option * Token.T list

   val parse_methods: string list parser

   val ml: string -> ML_Lex.token Antiquote.antiquote list

   val from_store: id -> T

 end

 (**)

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

 struct

 (**)

 type T = Probl_Def.T;

 val empty = Probl_Def.empty

 (*

   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

 fun split_did_PIDE t =

   let

     val (hd, arg) = case strip_comb t of

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

     | _ => raise ERROR ("split_did_PIDE: doesn't match (hd,[arg]) for t = xxxxx" (*^ 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;

 fun prep_input_PIDE thy guh maa init (pblID, dsc_dats, ev, ca, metIDs) =

     let

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

 val _ = writeln "#prep_input_PIDE 1";

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

 val _ = writeln "#prep_input_PIDE 1a";

       val gi = (case gi of

 		    [] => []

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

         (*(case \<^try>\<open> *)map (split_did_PIDE o (Syntax.read_term_global thy)) gi'(*\<close> of

           SOME x => x

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

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

 val _ = writeln "#prep_input_PIDE 1b";

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

 val _ = writeln "#prep_input_PIDE 2";

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

 		  val fi = (case fi of

 		    [] => []

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

         (*(case \<^try>\<open> *)map (split_did_PIDE o (Syntax.read_term_global thy)) fi'(*\<close> of

           SOME x => x

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

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

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

 val _ = writeln "#prep_input_PIDE 3";

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

 		  val re = (case re of

 		    [] => []

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

         (*(case \<^try>\<open> *)map (split_did_PIDE o (Syntax.read_term_global thy)) re'(*\<close> of

           SOME x => x

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

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

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

 val _ = writeln "#prep_input_PIDE 4";

 		  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_PIDE: syntax raise ERROR in '#Where' of " ^ strs2str pblID))*)

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

     in

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

         cas = Option.map (Syntax.read_term_global 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_Set.T 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>;

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

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

 val ml = ML_Lex.read;

 (* command definition *)

 local

 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

 (*Ouptut from Biegelinie.problem pbl_bieg : "Biegelinien":*)

             val pblID = References_Def.explode_id id;

             val metIDs = map References_Def.explode_id mets;

 (*val _ = writeln ("#problem source: " ^ @{make_string} source)*)

             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 _ = writeln ("#problem set_data: " ^ @{make_string} set_data)*)

             (* Context.theory_map HAS STORED THE ml-source IN Theory_Data ALREADY,

                BUT prep_input_PIDE REQUIRES ml-source AGAIN ... *)

             val input = the_data (set_data thy);

 (*val _ = writeln ("#problem input: " ^ @{make_string} input)*)

 (*

 val _ = writeln ("#problem model_input: " ^ @{make_string} model_input)

 val (m1, m2) = case model_input of

   ("#Given", [m1, m2]) :: _ => (m1, m2) (*=("<markup>", "<markup>")*)

 | _ => ("different case model_input", "different case model_input")

 val _ = writeln ("#problem m1: " ^ m1)  (*= Traegerlaenge l_l*)

 val _ = writeln ("#problem m2: " ^ m2)  (*= Streckenlast q_q *)

             ( * TODO: 

              * parse_model_input should preserve Position.T, Position.range, etc

              * ? preserve Position.T etc within ML_Lex.token Antiquote.antiquote list ?.. 

                ..in analogy to set_data ?!?

              * by Context.theory_map notify Isabelle/PIDE of errors from model_input at Position.T

              * in case there are no errors, do prep_input_PIDE (to be simplified)

              *)

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

           in KEStore_Elems.add_pbls @{context} [arg] thy end)))

 in end;

 (** get Problem from Store **)

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

 (**)end(**)