(* Title:  Specify/p-spec.sml

   Author: Walther Neuper

   (c) due to copyright terms

This will be dropped at switch to Isabelle/PIDE .

*)

signature PRESENTATION_SPECIFICATION =

sig

  type record

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

  datatype iitem =

      Find of TermC.as_string list

    | Given of TermC.as_string list

    | Relate of TermC.as_string list

  type imodel = iitem list

  type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T

  val empty: icalhd

  val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * SpecificationC.T

\<^isac_test>\<open>

  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 ->

    (string * TermC.as_string) list -> I_Model.T

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

  val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->

    int list * bool * ''a * I_Model.feedback (*I_Model.single'*)

  val imodel2fstr: iitem 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 -> (''a * (term * term)) list -> (*Model_Pattern.T*)

    (''a * string) list ->

      (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T*)

\<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 iitem = 

  Given of TermC.as_string list

(*Where is still not input*) 

| Find  of TermC.as_string list

| Relate  of TermC.as_string list

type imodel = iitem list

type icalhd =

  Pos.pos' *         (* the position in Ctree              *) 

  TermC.as_string *  (* the headline shown on Calc.T       *)

  imodel *           (* the model                          *)

  Pos.pos_ *         (* model belongs to Problem or MethodC *)

  References.T;      (* into Know_Store                    *)

val empty = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)

fun is_e_ts [] = true

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

  | is_e_ts _ = false;

(* WN.9.11.03 copied from fun appl_add *)

fun appl_add' dI oris model 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)

	  | 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 ("appl_add': " ^ msg))

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

        if is_e_ts ts

        then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, [])))

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

   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)

    | 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))

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

	    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 (*([1],true,"#Given",Cor (...))*)

    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_)

(* handles superfluous items carelessly *)

fun add itm itms = 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 _ [] = model

  | appl_adds dI oris model 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.Par 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.Typ 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))

  | itms2fstr ctxt (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term ctxt (d $ t))

  | itms2fstr ctxt (itm as (_, _, _, _, I_Model.Par _)) = 

    raise ERROR ("itms2fstr (" ^ I_Model.single_to_string ctxt itm ^ "): Par should be internal");

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;

(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)

fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =

    let

		  val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of

		    Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), 

		      spec = sspec as (sdI, spI, smI), probl, meth, ...}

        => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)

      | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"

      val thy = Know_Store.get_via_last_thy dI

      val ctxt = Proof_Context.init_global thy

    in if CAS_Cmd.is_from hdf fmz

       then the (CAS_Cmd.input (ParseC.term_opt ctxt hdf |> the)) 

       else

         let val (pos_, pits, mits) = 

	         if dI <> sdI

	         then let (* eliminated for PIDE turn 11: take Position into I_Model

                  val its = map (parsitm thy) probl;

			            val (its, trms) = filter_sep is_Par its;*)

			            val pbt = (#model o Problem.from_store ctxt)

			              (#2 (References.select_input ospec sspec))

		            in (Pos.Pbl, appl_adds dI oris [](*its*) pbt  (map par2fstr [](*trms*)), meth) end 

           else

             if pI <> spI 

	           then if pI = snd3 ospec then (Pos.Pbl, probl, meth) 

                  else let

                      val pbt = (#model o Problem.from_store ctxt) pI

			                val dI' = #1 (References.select_input ospec spec)

			                val oris =

			                  if pI = #2 ospec then oris 

				                else O_Model.init thy fmz_ pbt |> #1;

		                in (Pos.Pbl, appl_adds dI' oris probl pbt 

				              (map (itms2fstr ctxt) probl), meth) end 

             else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)

	                then let

		                  val (_, mits) = I_Model.s_make_complete ctxt oris

		                    (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (pI, mI)

		                in if foldl and_ (true, map #3 mits)

		                   then (Pos.Pbl, probl, I_Model.TEST_to_OLD mits)

		                   else (Pos.Met, probl, I_Model.TEST_to_OLD mits)

		                end 

                  else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]

			                  ((#model o Problem.from_store ctxt)

			                    (#2 (References.select_input ospec spec)))

			                      (imodel2fstr imodel), meth)

	         val pt = Ctree.update_spec pt p spec;

         in if pos_ = Pos.Pbl

	          then 

	            let 

	              val {where_rls, where_, model, ...} = Problem.from_store ctxt

	                (#2 (References.select_input ospec spec))

		            val (_, where_) = Pre_Conds.check ctxt where_rls where_

		              (model, I_Model.OLD_to_TEST pits)

	            in (Ctree.update_pbl pt p pits,

		                 (SpecificationC.is_complete' pits where_ spec, Pos.Pbl, hdf', pits, where_, spec)) 

              end

	          else 

	            let 

	              val {where_rls,where_, model, ...} = MethodC.from_store ctxt 

	                (#3 (References.select_input ospec spec))

		            val (_, where_) = Pre_Conds.check ctxt where_rls where_

		              (model, I_Model.OLD_to_TEST mits)

	            in (Ctree.update_met pt p mits,

		                  (SpecificationC.is_complete' mits where_ spec, Pos.Met, hdf', mits, where_, spec))

              end

         end 

    end

  | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl."

(**)end (**)