(* Title: Specify/p-model.sml

    Author: Walther Neuper 170207

    (c) due to copyright terms

 This will mostly be dropped at switch to Isabelle/PIDE .

 *)

 signature PRESENTATION_MODEL =

 sig

   (* for the OLD P_Model.T *)

   type T

   val empty: T

   val to_string: T -> string

   datatype item = (*shall be dropped with PIDE*)

     Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string

   | Missing of TermC.as_string | Superfl of string | SyntaxE of string | TypeE of string

   type 'a model     (*shall be dropped with PIDE*)

   val from : theory -> I_Model.T -> Pre_Conds.T -> T

   val to_list: 'a model -> 'a list

   val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input

   val mk_additem: string -> TermC.as_string -> Tactic.input

   val item_from_feedback: theory -> I_Model.feedback -> item

 (*from isac_test for Minisubpbl*)

   val add_sel_ppc: theory -> string -> {Find: 'a list, Given: 'a list, Relate: 'a list, Where: 'a list, With: 'b} -> 'a -> {Find: 'a list, Given: 'a list, Relate: 'a list, Where: 'a list, With: 'b}

 (**)

 \<^isac_test>\<open>

 (**)

 \<close>

 end

 (**)

 structure P_Model(**) : PRESENTATION_MODEL(**) =

 struct

 (**)

 datatype switch_pbl_met = For_Problem | For_Method

 (** types for OLD presentation**)

 type 'a model = 

   {Given : 'a list, Where: 'a list, Find  : 'a list, With : 'a list, Relate: 'a list};

 datatype item = 

     Correct of TermC.as_string (* labels a correct formula (type cterm') *)

   | SyntaxE of string (**)

   | TypeE   of string (**)

   | False   of TermC.as_string (* WN050618 notexistent in itm_: only used in Where *)

   | Incompl of TermC.as_string (**)

   | Superfl of string (**)

   | Missing of TermC.as_string; (*REVIEW: a "missing" item is not shown, thus cannot be marked*)

 type T = item model;

 fun item2str (Correct  s) = "Correct " ^ s

   | item2str (SyntaxE  s) = "SyntaxE " ^ s

   | item2str (TypeE    s) = "TypeE " ^ s

   | item2str (False    s) = "False " ^ s

   | item2str (Incompl  s) = "Incompl " ^ s

   | item2str (Superfl  s) = "Superfl " ^ s

   | item2str (Missing  s) = "Missing " ^ s;

 fun to_string ({Given=Given,Where=Where,

 		 Find=Find,With=With,Relate=Relate}:item model)=

     ("{Given =" ^ ((strs2str' o (map item2str))	 Given ) ^

      ",Where=" ^ ((strs2str' o (map item2str))	 Where) ^

      ",Find  =" ^ ((strs2str' o (map item2str))	 Find  ) ^

      ",With =" ^ ((strs2str' o (map item2str))	 With ) ^

      ",Relate=" ^ ((strs2str' o (map item2str))	 Relate) ^ "}");

 val empty = {Given = [], Where= [], Find  = [], With = [], Relate= []};

 (** build T **)

 (*T_POSold*)

 fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))

   | item_from_feedback _ (I_Model.Syn c) = SyntaxE c

   | item_from_feedback _ (I_Model.Typ c) = TypeE c

   | item_from_feedback thy (I_Model.Inc ((d, ts), _)) = Incompl (UnparseC.term_in_thy thy  (Input_Descript.join (d, ts)))

   | item_from_feedback thy (I_Model.Sup (d, ts)) = Superfl (UnparseC.term_in_thy thy  (Input_Descript.join (d, ts)))

   | item_from_feedback thy (I_Model.Mis (d, pid)) = Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy  pid)

   | item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"

 (*T_POS* )

 fun item_from_feedback_POS thy (I_Model.Cor_POS ((d, ts), _)) = Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))

   | item_from_feedback_POS _ (I_Model.Syn_POS c) = SyntaxE c

   | item_from_feedback_POS thy (I_Model.Inc_POS ((d, ts), _)) = Incompl (UnparseC.term_in_thy thy  (Input_Descript.join (d, ts)))

   | item_from_feedback_POS thy (I_Model.Sup_POS (d, ts)) = Superfl (UnparseC.term_in_thy thy  (Input_Descript.join (d, ts)))

 ( *T_POSnew*)

 fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =

   case sel of

     "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re}

   | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}

   | "#Find"  => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}

   | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}

   | "#undef" =>         {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)

   | "i_model_empty" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)

   | _  => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")

 fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =

   {Given = gi, Where = wh, Find= fi , With = wi, Relate = re}

 fun boolterm2item ctxt (true, term) = Correct (UnparseC.term ctxt term)

   | boolterm2item ctxt(false, term) = False (UnparseC.term ctxt term);

 fun from thy itms where_ =

   let                                                                                     

     fun coll model [] = model

       | coll model ((_, _, _, field, itm_) :: itms) =

         coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;

     val gfr = coll empty itms;

   in add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_) end;

 fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (I_Model.to_p_model thy itm_)

   | mk_delete thy "#Find" itm_ = Tactic.Del_Find (I_Model.to_p_model thy itm_)

   | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (I_Model.to_p_model thy itm_)

   | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"")

 fun mk_additem "#Given" ct = Tactic.Add_Given ct

   | mk_additem "#Find" ct = Tactic.Add_Find ct    

   | mk_additem "#Relate"ct = Tactic.Add_Relation ct

   | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"")

 fun to_list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =

   gis @ whs @ fis @ wis @ res

 (**)end(*struct*);