(* Title:  Specify/input-calchead.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 filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list

   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_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*)

   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 parsitm: theory -> I_Model.single -> I_Model.single

   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)

 (* re-parse itms with a new thy and prepare for checking with ori list *)

 fun parsitm thy (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =

     (case \<^try>\<open>

         let val t = Input_Descript.join (d, ts)

           val _ = (UnparseC.term_in_thy thy t)

           (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)

         in itm end\<close> of

       SOME x => x

     | NONE =>

       (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))

   | parsitm _ (i, v, b, f, I_Model.Syn str) =

     (case \<^try>\<open>

         let val _ = Syntax.read_term\<^context> str

         in (i, v, b ,f, I_Model.Par str) end\<close> of

       SOME x => x

     | NONE => (i, v, b, f, I_Model.Syn str))

   | parsitm _ (i, v, b, f, I_Model.Typ str) =

     (case \<^try>\<open>

         let val _ = Syntax.read_term\<^context> str

          in (i, v, b, f, I_Model.Par str) end\<close> of

       SOME x => x

     | NONE => (i, v, b, f, I_Model.Syn str))

   | parsitm thy (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =

     (case \<^try>\<open>

         let val t = Input_Descript.join (d,ts);

 	        val _ = UnparseC.term_in_thy thy t;

         (*this    ^ should raise the exn on unability of re-parsing dts*)

         in itm end\<close> of

       SOME x => x

     | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))

   | parsitm thy (itm as (i, v, _, f, I_Model.Sup (d, ts))) =

     (case \<^try>\<open>

         let val t = Input_Descript.join (d,ts);

 	        val _ = UnparseC.term_in_thy thy t;

         (*this    ^ should raise the exn on unability of re-parsing dts*)

         in itm end\<close> of

       SOME x => x

     | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))

   | parsitm thy (itm as (i, v, _, f, I_Model.Mis (d, t'))) =

     (case \<^try>\<open>

         let val t = d $ t';

 	        val _ = UnparseC.term_in_thy thy t;

         (*this    ^ should raise the exn on unability of re-parsing dts*)

         in itm end\<close> of

       SOME x => x

     | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))

   | parsitm thy (itm as (_, _, _, _, I_Model.Par _)) = 

     raise ERROR ("parsitm (" ^ I_Model.single_to_string (Proof_Context.init_global thy) itm ^

       "): Par should be internal");

 (*separate a list to a pair of elements that do NOT satisfy the predicate,

  and of elements that satisfy the predicate, i.e. (false, true)*)

 fun filter_sep pred xs =

   let

     fun filt ab [] = ab

       | filt (a, b) (x :: xs) =

         if pred x 

 			  then filt (a, b @ [x]) xs 

 			  else filt (a @ [x], b) xs

   in filt ([], []) xs end;

 fun is_Par (_, _, _, _, I_Model.Par _) = true

   | is_Par _ = false;

 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 = ThyC.get_theory 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

 (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation

    appl_add': generate 1 item 

    appl_add' . contains: parse, get data from oris (vats, all (elems if list)..)

    appl_add' . is_notyet_input: compare with items in model already input

    insert_ppc': insert this 1 item*)

 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 (I_Model.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 (ThyC.id_to_ctxt "Isac_Knowledge") 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 ("parsitm (" ^ 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, ctxt, ...}

         => (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 val its = map (parsitm (ThyC.get_theory dI)) 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 met = (#model o MethodC.from_store ctxt) mI

 		                     val mits = I_Model.complete oris probl meth met

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

 		                      then (Pos.Pbl, probl, mits) else (Pos.Met, probl, 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_,...} = Problem.from_store ctxt

 	                (#2 (References.select_input ospec spec))

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

 	            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_,...} = MethodC.from_store ctxt 

 	                (#3 (References.select_input ospec spec))

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

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