(* Title:  Specify/p-spec.sml

    Author: Walther Neuper

    (c) due to copyright terms

 Major parts will be dropped at switch to Isabelle/PIDE.

 Thus the switch to I_Model.T is prepared quick and dirty.

 *)

 signature PRESENTATION_SPECIFICATION =

 sig

   type record

 (*/------- rename -------\*)

   datatype p_model =

       Find of TermC.as_string list

     | Given of TermC.as_string list

     | Relate of TermC.as_string list

   val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->

     string * TermC.as_string -> I_Model.single

   val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->

     (Model_Def.m_field * TermC.as_string) list -> I_Model.T

   val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool

   val fstr2itm_: theory -> Model_Pattern.T -> Model_Def.m_field * string ->

     int list * bool * Model_Def.m_field * (I_Model.feedback * Position.T)

   val imodel2fstr: p_model list -> (string * TermC.as_string) list

   val is_e_ts: term list -> bool

   val itms2fstr: Proof.context -> I_Model.single -> string * string

   val par2fstr: I_Model.single -> string * TermC.as_string

   val unknown_expl: ThyC.id -> Model_Pattern.T -> (Model_Def.m_field * string) list -> I_Model.T

 (*\----- from isac_test for Minisubpbl*)

 \<^isac_test>\<open>

 (**)

 \<close>

 (*\------- rename -------/*)

 end

 (**)

 structure P_Spec(**): PRESENTATION_SPECIFICATION(**) =

 struct

 (**)

   type record = {thy_id: ThyC.id, pbl_id: Problem.id,           (* headline of Problem *)

     givens: TermC.as_string list, wheres: TermC.as_string list, (* Model.T             *)

       find: TermC.as_string, relates: TermC.as_string list,

     rthy_id: ThyC.id, rpbl_id: Problem.id, rmet_id: MethodC.id}  (* References.T        *)

 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)

 (** handle an input P_Specific'action **)

 datatype p_model = 

   Given of TermC.as_string list

 (*Where is still not input*) 

 | Find  of TermC.as_string list

 | Relate  of TermC.as_string list

 fun is_e_ts [] = true

   | is_e_ts [Const (\<^const_name>\<open>Nil\<close>, _)] = true

   | is_e_ts _ = false;

 fun appl_add' dI oris (model: I_Model.T) pbt (sel, ct) = 

   let 

      val ctxt = Know_Store.get_via_last_thy dI |> Proof_Context.init_global;

   in

     (*/------------ replace by ParseC.term_position ------------------\*)

     case ParseC.term_opt ctxt ct of

     (*\------------ replace by ParseC.term_position ------------------/*)

 	    NONE => (0, [], false, sel, (I_Model.Syn ct, Position.none))

 	  | SOME t =>

 	    (case O_Model.contains ctxt sel oris t of

         ("", ori', all) =>

           (case I_Model.is_notyet_input ctxt model all ori' pbt of

             ("", itm)  => itm

           | (msg,_) => raise ERROR ("P_Spec.appl_add': " ^ msg))

       | (_, (i, v, _, d, ts), _) =>

         if is_e_ts ts

         then (i, v, false, sel, (I_Model.Inc (d, ts), Position.none))

         else (i, v, false, sel, (I_Model.Sup (d, ts), Position.none)))

    end

 (* generate preliminary itm_ from a string (with field "#Given" etc.) *)

 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';

 fun fstr2itm_ thy pbt (f, str) =

   let

     (*/------------ replace by ParseC.term_position ? ------------\*)

     val topt = ParseC.term_opt (Proof_Context.init_global thy) str

     (*\------------ replace by ParseC.term_position ? ------------/*)

   in

     case topt of

       NONE => ([], false, f, (I_Model.Syn str, Position.none))

     | SOME ct => 

 	    let

 	      val (d, ts) = Input_Descript.split ct

 	      val popt = find_first (eq7 (f, d)) pbt

 	    in

 	      case popt of

 	        NONE => ([1](*??*), true(*??*), f, (I_Model.Sup (d, ts), Position.none))

 	      | SOME (f, (d, id)) => ([1], true, f, (I_Model.Cor (d, ts), Position.none))

 	    end

   end

 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)

 fun unknown_expl dI pbt selcts =

   let

     val thy = Know_Store.get_via_last_thy dI

     val its_ = map (fstr2itm_ thy pbt) selcts

     val its = O_Model.add_enumerate its_ 

   in map flattup2 its end

 fun eq_dsc ((_, _, _, _, (itm_, _)), (_, _, _, _, (iitm_, _))) =

   (I_Model.descriptor itm_ = I_Model.descriptor iitm_)

 fun add itm (itms: I_Model.T) = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)

 fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts

     (*already present itms in model are being overwritten*)

   | appl_adds _ _ (model: I_Model.T) _ [] = model

   | appl_adds dI oris (model: I_Model.T) pbt (selct :: ss) =

     let val itm = appl_add' dI oris model pbt selct;

     in appl_adds dI oris (add itm model) pbt ss end

 fun par2fstr (_, _, _, f, (I_Model.Syn s, _)) = (f, s)

   | par2fstr itm = raise ERROR ("par2fstr: called with " ^

     I_Model.single_to_string (ContextC.for_ERROR ()) itm)

 fun itms2fstr _ (_, _, _, f, (I_Model.Cor (d, ts), _)) = (f, Input_Descript.join''' (d, ts))

   | itms2fstr _ (_, _, _, f, (I_Model.Syn str, _)) = (f, str)

   | itms2fstr _ (_, _, _, f, (I_Model.Inc (d, ts), _)) = (f, Input_Descript.join''' (d,ts))

   | itms2fstr _ (_, _, _, f, (I_Model.Sup (d, ts), _)) = (f, Input_Descript.join''' (d, ts))

 fun imodel2fstr iitems = 

   let 

     fun xxx is [] = is

 	    | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis

 	    | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis

 	    | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis

   in xxx [] iitems end;

 (**)end (**)