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

  datatype item

  = 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

  val empty_ppc : item ppc

  val ppc2str : {Find: string list, Given: string list, Relate: string list, Where: string list,

    With: string list} -> string

  val itemppc2str : item ppc -> string

  val mkval' : term list -> term

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

  (* NONE *)

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

  (* NONE *)

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

end

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

struct

fun mkval _(*dsc*) [] = error "mkval called with []"

  | mkval _ [t] = t

  | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;

fun mkval' x = mkval TermC.empty x;

(* for _output_ of the items of a Model *)

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;

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;

type 'a ppc = 

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

fun ppc2str {Given = Given, Where = Where, Find = Find, With = With, Relate = Relate}=

  "{Given =" ^ strs2str Given ^ ",Where=" ^ strs2str Where ^ ",Find  =" ^ strs2str Find ^

  ",With =" ^ strs2str With ^ ",Relate=" ^ strs2str Relate ^ "}";

fun itemppc2str ({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_ppc = {Given = [], Where= [], Find  = [], With = [], Relate= []};

(**)end(**);