(* Title: Model for (sub-)calculations.

          Various representations: item and ppc for frontend, itm_ and itm for internal functions.

          The former are related to structure Specify, the latter to structure Chead --

          -- apt to re-arrangement of structures

   Author: Walther Neuper 170207

   (c) due to copyright terms

*)

signature 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 Model(**) : MODEL(**) =

struct

(*==========================================================================

23.3.02 TODO: ideas on redesign of type I_Model.feedback,type item,type ori,type item ppc

(1) kinds of itms:

  (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)

        =(presently) Mis (? should be Inc initially, and Mis after match_itms?)

  (1.2)  Syn,Typ,Sup: not related to oris

    Syn, Typ (presently) should be accepted in I_Model.add_single (instead Error')

    Sup      (presently) should be accepted in I_Model.add_single (instead Error')

         _could_ be w.r.t current vat (and then _is_ related to vat

    Mis should _not_ be  made Inc ((presently, by I_Model.add_single & match_itms)

- dsc in I_Model.feedback is timeconsuming -- keep id for respective queries ?

- order of items in ppc should be stable w.r.t order of itms

- stepwise input of itms --- match_itms (in one go) ..not coordinated

  - unify code

  - match_itms / match_itms_oris ..2 versions ?!

    (fast, for refine / slow, for modeling)

- clarify: efficiency <--> simplicity !!!

  ?: shift dsc I_Model.feedback -> itm | discard int in ori,itm | take int instead dsc 

    | take int for perserving order of item ppc in itms 

    | make all(!?) handling of itms stable against reordering(?)

    | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)

      -"- "#undef" ?= not touched ?= (id,..)

-----------------------------------------------------------------

27.3.02:

def: type pbt = (field, (dsc, pid)) *** design considerations ***

(1) fmz + pbt -> oris

(2) input + oris -> itm

(3) match_itms      : schnell(?) f"ur refine

    match_itms_oris : r"uckmeldung f"ur item ppc

(1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)

---------- ^^^^^ --- dh. pbt meist als argument zu viel !!!

(3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht;

      wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:

      (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid)  dh.vt neu  ????

      (b) 

==========================================================================*)

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