1 (* Title: Model for (sub-)calculations.
2 Various representations: item and ppc for frontend, itm_ and itm for internal functions.
3 The former are related to structure Specify, the latter to structure Chead --
4 -- apt to re-arrangement of structures
5 Author: Walther Neuper 170207
6 (c) due to copyright terms
12 = Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string | Missing of TermC.as_string | Superfl of string
13 | SyntaxE of string | TypeE of string
16 val empty_ppc : item ppc
17 val ppc2str : {Find: string list, Given: string list, Relate: string list, Where: string list,
18 With: string list} -> string
19 val itemppc2str : item ppc -> string
21 val mkval' : term list -> term
23 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
25 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
27 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
30 structure Model(**) : MODEL(**) =
32 (*==========================================================================
33 23.3.02 TODO: ideas on redesign of type I_Model.feedback,type item,type ori,type item ppc
35 (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)
36 =(presently) Mis (? should be Inc initially, and Mis after match_itms?)
37 (1.2) Syn,Typ,Sup: not related to oris
38 Syn, Typ (presently) should be accepted in I_Model.check_single (instead Error')
39 Sup (presently) should be accepted in I_Model.check_single (instead Error')
40 _could_ be w.r.t current vat (and then _is_ related to vat
41 Mis should _not_ be made Inc ((presently, by I_Model.check_single & match_itms)
42 - dsc in I_Model.feedback is timeconsuming -- keep id for respective queries ?
43 - order of items in ppc should be stable w.r.t order of itms
45 - stepwise input of itms --- match_itms (in one go) ..not coordinated
47 - match_itms / match_itms_oris ..2 versions ?!
48 (fast, for refine / slow, for modeling)
50 - clarify: efficiency <--> simplicity !!!
51 ?: shift dsc I_Model.feedback -> itm | discard int in ori,itm | take int instead dsc
52 | take int for perserving order of item ppc in itms
53 | make all(!?) handling of itms stable against reordering(?)
54 | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)
55 -"- "#undef" ?= not touched ?= (id,..)
56 -----------------------------------------------------------------
58 def: type pbt = (field, (dsc, pid)) *** design considerations ***
61 (2) input + oris -> itm
62 (3) match_itms : schnell(?) f"ur refine
63 match_itms_oris : r"uckmeldung f"ur item ppc
65 (1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)
66 ---------- ^^^^^ --- dh. pbt meist als argument zu viel !!!
68 (3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht;
69 wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:
70 (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid) dh.vt neu ????
72 ==========================================================================*)
74 fun mkval _(*dsc*) [] = error "mkval called with []"
76 | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
77 fun mkval' x = mkval TermC.empty x;
79 (* for _output_ of the items of a Model *)
81 Correct of TermC.as_string (* labels a correct formula (type cterm') *)
82 | SyntaxE of string (**)
83 | TypeE of string (**)
84 | False of TermC.as_string (* WN050618 notexistent in itm_: only used in Where *)
85 | Incompl of TermC.as_string (**)
86 | Superfl of string (**)
87 | Missing of TermC.as_string;
88 fun item2str (Correct s) = "Correct " ^ s
89 | item2str (SyntaxE s) = "SyntaxE " ^ s
90 | item2str (TypeE s) = "TypeE " ^ s
91 | item2str (False s) = "False " ^ s
92 | item2str (Incompl s) = "Incompl " ^ s
93 | item2str (Superfl s) = "Superfl " ^ s
94 | item2str (Missing s) = "Missing " ^ s;
97 {Given : 'a list, Where: 'a list, Find : 'a list, With : 'a list, Relate: 'a list};
98 fun ppc2str {Given = Given, Where = Where, Find = Find, With = With, Relate = Relate}=
99 "{Given =" ^ strs2str Given ^ ",Where=" ^ strs2str Where ^ ",Find =" ^ strs2str Find ^
100 ",With =" ^ strs2str With ^ ",Relate=" ^ strs2str Relate ^ "}";
102 fun itemppc2str ({Given=Given,Where=Where,
103 Find=Find,With=With,Relate=Relate}:item ppc)=
104 ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
105 ",Where=" ^ ((strs2str' o (map item2str)) Where) ^
106 ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^
107 ",With =" ^ ((strs2str' o (map item2str)) With ) ^
108 ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}");
110 val empty_ppc = {Given = [], Where= [], Find = [], With = [], Relate= []};