walther@59938
|
1 |
(* Title: Specify/o-model.sml
|
walther@59938
|
2 |
Author: Walther Neuper 110226
|
walther@59938
|
3 |
(c) due to copyright terms
|
walther@59953
|
4 |
|
walther@59953
|
5 |
Original model created initially from Formale.T and Model_Pattern.T;
|
walther@59953
|
6 |
This model makes student's editing via I_Model.T more efficient.
|
walther@59953
|
7 |
TODO: revise with an example with more than 1 variant.
|
walther@59953
|
8 |
*)
|
walther@59938
|
9 |
|
walther@59938
|
10 |
signature ORIGINAL_MODEL =
|
walther@59938
|
11 |
sig
|
walther@59961
|
12 |
type T
|
walther@59961
|
13 |
type single
|
walther@59961
|
14 |
type variants
|
walther@59961
|
15 |
type m_field
|
walther@59961
|
16 |
type descriptor
|
walther@59940
|
17 |
val to_string: T -> string
|
walther@59957
|
18 |
val single_to_string: single -> string
|
walther@59940
|
19 |
val single_empty: single
|
walther@59939
|
20 |
|
walther@59952
|
21 |
val init: Formalise.model -> theory -> Model_Pattern.T -> T
|
walther@59960
|
22 |
val add : theory -> Model_Pattern.T -> T -> T
|
walther@59969
|
23 |
val values : T -> term list
|
walther@59969
|
24 |
|
walther@59969
|
25 |
(*put add_id into a new auxiliary fun..*)
|
walther@59961
|
26 |
val add_id: 'a list -> (int * 'a) list
|
walther@59961
|
27 |
type preori
|
walther@59961
|
28 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59961
|
29 |
val preoris2str : preori list -> string
|
walther@59961
|
30 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59952
|
31 |
val add_field: theory -> Model_Pattern.T -> term * 'b -> m_field * descriptor * 'b
|
walther@59952
|
32 |
val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
|
walther@59952
|
33 |
val max: variants -> int
|
walther@59947
|
34 |
val coll_variants: ('a * ''b) list -> ('a list * ''b) list
|
walther@59947
|
35 |
val replace_0: int -> int list -> int list
|
walther@59947
|
36 |
val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
|
walther@59938
|
37 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59938
|
38 |
end
|
walther@59938
|
39 |
|
walther@59938
|
40 |
structure O_Model(**) : ORIGINAL_MODEL(**) =
|
walther@59938
|
41 |
struct
|
walther@59938
|
42 |
|
walther@59960
|
43 |
(** types **)
|
walther@59960
|
44 |
|
walther@59940
|
45 |
type variants = Model_Def.variants;
|
walther@59952
|
46 |
type m_field = Model_Def.m_field;
|
walther@59952
|
47 |
type descriptor = Model_Def.descriptor;
|
walther@59938
|
48 |
|
walther@59940
|
49 |
type T = Model_Def.o_model;
|
walther@59940
|
50 |
type single = Model_Def.o_model_single
|
walther@59940
|
51 |
val single_empty = Model_Def.o_model_empty;
|
walther@59957
|
52 |
val single_to_string = Model_Def.o_model_single_to_string;
|
walther@59940
|
53 |
val to_string = Model_Def.o_model_to_string;
|
walther@59940
|
54 |
|
walther@59952
|
55 |
(* O_Model.single without leading integer *)
|
walther@59952
|
56 |
type preori = (variants * m_field * term * term list);
|
walther@59942
|
57 |
fun preori2str (vs, fi, t, ts) =
|
walther@59942
|
58 |
"(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
|
walther@59942
|
59 |
UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
|
walther@59942
|
60 |
val preoris2str = (strs2str' o (map (linefeed o preori2str)));
|
walther@59942
|
61 |
|
walther@59960
|
62 |
|
walther@59960
|
63 |
(** initialise O_Model **)
|
walther@59960
|
64 |
|
walther@59947
|
65 |
(* compare d and dsc in pbt and transfer field to pre-ori *)
|
walther@59947
|
66 |
fun add_field (_: theory) pbt (d,ts) =
|
walther@59947
|
67 |
let fun eq d pt = (d = (fst o snd) pt);
|
walther@59947
|
68 |
in case filter (eq d) pbt of
|
walther@59947
|
69 |
[(fi, (_, _))] => (fi, d, ts)
|
walther@59947
|
70 |
| [] => ("#undef", d, ts) (*may come with met.ppc*)
|
walther@59952
|
71 |
| _ => raise ERROR ("add_field: " ^ UnparseC.term d ^ " more than once in pbt")
|
walther@59947
|
72 |
end;
|
walther@59947
|
73 |
|
walther@59952
|
74 |
(*
|
walther@59952
|
75 |
mark an element with the position within a plateau;
|
walther@59952
|
76 |
a plateau with length 1 is marked with 0
|
walther@59952
|
77 |
*)
|
walther@59952
|
78 |
fun mark _ [] = raise ERROR "mark []"
|
walther@59952
|
79 |
| mark eq xs =
|
walther@59952
|
80 |
let
|
walther@59952
|
81 |
fun mar xx _ [x] n = xx @ [(if n = 1 then 0 else n, x)]
|
walther@59952
|
82 |
| mar _ _ [] _ = raise ERROR "mark []"
|
walther@59952
|
83 |
| mar xx eq (x:: x' :: xs) n =
|
walther@59952
|
84 |
if eq(x, x') then mar (xx @ [(n, x)]) eq (x' :: xs) (n + 1)
|
walther@59952
|
85 |
else mar (xx @ [(if n = 1 then 0 else n, x)]) eq (x' :: xs) 1;
|
walther@59952
|
86 |
in mar [] eq xs 1 end;
|
walther@59952
|
87 |
|
walther@59952
|
88 |
(*
|
walther@59952
|
89 |
assumes equal descriptions to be in adjacent 'plateaus',
|
walther@59952
|
90 |
items at a certain position within the plateaus form a variant;
|
walther@59952
|
91 |
length = 1 ... marked with 0: covers all variants
|
walther@59952
|
92 |
*)
|
walther@59947
|
93 |
fun add_variants fdts =
|
walther@59947
|
94 |
let
|
walther@59947
|
95 |
fun eq (a, b) = curry op= (snd3 a) (snd3 b);
|
walther@59947
|
96 |
in mark eq fdts end;
|
walther@59947
|
97 |
|
walther@59952
|
98 |
fun max [] = raise ERROR "max of []"
|
walther@59947
|
99 |
| max (y :: ys) =
|
walther@59947
|
100 |
let fun mx x [] = x
|
walther@59947
|
101 |
| mx x (y :: ys) = if x < y then mx y ys else mx x ys;
|
walther@59947
|
102 |
in mx y ys end;
|
walther@59947
|
103 |
|
walther@59947
|
104 |
fun coll_variants (((v,x) :: vxs)) =
|
walther@59947
|
105 |
let
|
walther@59947
|
106 |
fun col xs (vs, x) [] = xs @ [(vs, x)]
|
walther@59947
|
107 |
| col xs (vs, x) ((v', x') :: vxs') =
|
walther@59947
|
108 |
if x = x' then col xs (vs @ [v'], x') vxs'
|
walther@59947
|
109 |
else col (xs @ [(vs, x)]) ([v'], x') vxs';
|
walther@59947
|
110 |
in col [] ([v], x) vxs end
|
walther@59952
|
111 |
| coll_variants _ = raise ERROR "coll_variants: called with []";
|
walther@59947
|
112 |
|
walther@59947
|
113 |
fun replace_0 vm [0] = intsto vm
|
walther@59947
|
114 |
| replace_0 _ vs = vs;
|
walther@59947
|
115 |
|
walther@59961
|
116 |
fun add_id [] = raise ERROR "O_Model.add_id []"
|
walther@59947
|
117 |
| add_id xs =
|
walther@59947
|
118 |
let
|
walther@59947
|
119 |
fun add _ [] = []
|
walther@59947
|
120 |
| add n (x :: xs) = (n, x) :: add (n + 1) xs;
|
walther@59947
|
121 |
in add 1 xs end;
|
walther@59947
|
122 |
|
walther@59947
|
123 |
fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);
|
walther@59947
|
124 |
|
walther@59952
|
125 |
fun init [] _ _ = []
|
walther@59952
|
126 |
| init fmz thy pbt =
|
walther@59947
|
127 |
let
|
walther@59952
|
128 |
val model = (map (fn str => str
|
walther@59952
|
129 |
|> TermC.parseNEW'' thy
|
walther@59953
|
130 |
|> Input_Descript.split
|
walther@59952
|
131 |
|> add_field thy pbt) fmz)
|
walther@59952
|
132 |
|> add_variants;
|
walther@59952
|
133 |
val maxv = model |> map fst |> max;
|
walther@59947
|
134 |
val maxv = if maxv = 0 then 1 else maxv;
|
walther@59952
|
135 |
val model' = model
|
walther@59952
|
136 |
|> coll_variants
|
walther@59947
|
137 |
|> map (replace_0 maxv |> apfst)
|
walther@59947
|
138 |
|> add_id
|
walther@59947
|
139 |
|> map flattup;
|
walther@59952
|
140 |
in model' end;
|
walther@59938
|
141 |
|
walther@59960
|
142 |
|
walther@59960
|
143 |
(** add new m_field's from method **)
|
walther@59960
|
144 |
|
walther@59960
|
145 |
fun add _ mpc ori =
|
walther@59960
|
146 |
let
|
walther@59960
|
147 |
fun eq d pt = (d = (fst o snd) pt);
|
walther@59960
|
148 |
fun repl mpc (i, v, _, d, ts) =
|
walther@59960
|
149 |
case filter (eq d) mpc of
|
walther@59960
|
150 |
[(fi, (_, _))] => [(i, v, fi, d, ts)]
|
walther@59960
|
151 |
| [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
|
walther@59962
|
152 |
| _ => raise ERROR ("O_Model.add: " ^ UnparseC.term d ^ " more than once in met");
|
walther@59960
|
153 |
in flat ((map (repl mpc)) ori) end;
|
walther@59960
|
154 |
|
walther@59969
|
155 |
|
walther@59969
|
156 |
(** get the values **)
|
walther@59969
|
157 |
|
walther@59969
|
158 |
fun mkval _(*dsc*) [] = raise ERROR "mkval called with []"
|
walther@59969
|
159 |
| mkval _ [t] = t
|
walther@59969
|
160 |
| mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
|
walther@59969
|
161 |
fun mkval' x = mkval TermC.empty x;
|
walther@59969
|
162 |
fun values oris =
|
walther@59969
|
163 |
((map (mkval' o (#5))) o (filter ((member_swap op= 1) o (#2)))) oris
|
walther@59969
|
164 |
|
walther@59938
|
165 |
(**)end(**); |