(* Title: Specify/p-model.sml

   Author: Walther Neuper 170207

   (c) due to copyright terms

This will be dropped at switch to Isabelle/PIDE.

*)

signature PRESENTATION_MODEL =

sig

  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 ppc     (*shall be dropped with PIDE*)

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

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  val to_list: 'a ppc -> 'a list

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

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

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

(*val mk_additem: string -> TermC.as_string -> Tactic.input*)

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

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

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

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

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

(**)

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

struct

(**)

(** types **)

type 'a ppc = 

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

type T = item ppc;

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

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

fun item_from_feedback (_: theory) (I_Model.Cor ((d, ts), _)) = Correct (UnparseC.term (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 _ (I_Model.Inc ((d, ts), _)) = Incompl (UnparseC.term (Input_Descript.join (d, ts)))

  | item_from_feedback _ (I_Model.Sup (d, ts)) = Superfl (UnparseC.term (Input_Descript.join (d, ts)))

  | item_from_feedback _ (I_Model.Mis (d, pid)) = Missing (UnparseC.term d ^ " " ^ UnparseC.term pid)

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

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

  | _  => 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 (true, term) = Correct (UnparseC.term term)

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

fun from thy itms pre =

  let

    fun coll ppc [] = ppc

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

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

    val gfr = coll empty itms;

  in add_where gfr (map boolterm2item pre) 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(**);