walther@59938
|
1 |
(* Title: Specify/i-model.sml
|
walther@59938
|
2 |
Author: Walther Neuper 110226
|
walther@59938
|
3 |
(c) due to copyright terms
|
walther@59998
|
4 |
|
walther@60004
|
5 |
\<open>I_Model\<close> serves students' interactive modelling and gives feedback in the specify-phase.
|
walther@59998
|
6 |
*)
|
walther@59938
|
7 |
|
Walther@60694
|
8 |
signature INTERACTION_MODEL =
|
walther@59938
|
9 |
sig
|
walther@59969
|
10 |
|
walther@59961
|
11 |
type T
|
Walther@60695
|
12 |
type T_TEST
|
Walther@60708
|
13 |
val OLD_to_TEST: T -> T_TEST
|
Walther@60714
|
14 |
val TEST_to_OLD: T_TEST -> T
|
Walther@60467
|
15 |
val empty: T
|
Walther@60704
|
16 |
val empty_TEST: T_TEST
|
walther@59961
|
17 |
type single
|
Walther@60694
|
18 |
type single_TEST
|
Walther@60467
|
19 |
val empty_single: single
|
walther@60018
|
20 |
type variant
|
walther@59960
|
21 |
type variants
|
walther@59961
|
22 |
type m_field
|
walther@59961
|
23 |
type descriptor
|
walther@59948
|
24 |
datatype feedback = datatype Model_Def.i_model_feedback
|
Walther@60694
|
25 |
datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST
|
Walther@60705
|
26 |
type env
|
walther@59998
|
27 |
type message
|
walther@59938
|
28 |
|
walther@59942
|
29 |
val feedback_to_string': feedback -> string
|
walther@59942
|
30 |
val feedback_to_string: Proof.context -> feedback -> string
|
Walther@60705
|
31 |
(*eliminate ..*)
|
Walther@60694
|
32 |
val feedback_to_string'_TEST: Proof.context -> feedback_TEST -> string
|
Walther@60705
|
33 |
val feedback_TEST_to_string: feedback_TEST -> string
|
walther@59942
|
34 |
val single_to_string: Proof.context -> single -> string
|
Walther@60694
|
35 |
val single_to_string_TEST: Proof.context -> single_TEST -> string
|
walther@59942
|
36 |
val to_string: Proof.context -> T -> string
|
Walther@60694
|
37 |
val to_string_TEST: Proof.context -> T_TEST -> string
|
Walther@60708
|
38 |
val feedback_OLD_to_TEST: feedback -> feedback_TEST
|
walther@59942
|
39 |
|
Walther@60477
|
40 |
datatype add_single = Add of single | Err of string
|
walther@59958
|
41 |
val init: Model_Pattern.T -> T
|
Walther@60703
|
42 |
val init_TEST: O_Model.T -> Model_Pattern.T -> T_TEST
|
walther@59998
|
43 |
val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
|
Walther@60477
|
44 |
TermC.as_string -> add_single
|
walther@59958
|
45 |
val add_single: theory -> single -> T -> T
|
walther@59956
|
46 |
|
Walther@60477
|
47 |
val make_tactic: m_field -> TermC.as_string * T -> Tactic.T
|
Walther@60477
|
48 |
val descriptor: feedback -> descriptor
|
Walther@60705
|
49 |
val descriptor_TEST: feedback_TEST -> descriptor
|
Walther@60710
|
50 |
val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_TEST) list -> string
|
Walther@60477
|
51 |
val o_model_values: feedback -> O_Model.values
|
Walther@60477
|
52 |
val variables: T -> term list
|
walther@59998
|
53 |
val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
|
walther@59998
|
54 |
-> message * single
|
Walther@60477
|
55 |
val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
|
walther@59956
|
56 |
|
Walther@60477
|
57 |
val penvval_in: feedback -> term list
|
Walther@60477
|
58 |
|
Walther@60477
|
59 |
val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T
|
walther@59988
|
60 |
val add: single -> T -> T
|
walther@59988
|
61 |
val complete_method: O_Model.T * Model_Pattern.T * Model_Pattern.T * T -> T * T
|
walther@59988
|
62 |
val is_error: feedback -> bool
|
walther@59988
|
63 |
val complete': Model_Pattern.T -> O_Model.single -> single
|
walther@59956
|
64 |
|
walther@59988
|
65 |
val is_complete: T -> bool
|
walther@59988
|
66 |
val to_p_model: theory -> feedback -> string
|
walther@59956
|
67 |
val eq1: ''a -> 'b * (''a * 'c) -> bool
|
Walther@60705
|
68 |
|
Walther@60705
|
69 |
val is_complete_OLD: Proof.context -> Model_Pattern.T -> Rule_Def.rule_set ->
|
Walther@60705
|
70 |
Pre_Conds.unchecked -> T_TEST -> variants option
|
Walther@60706
|
71 |
val is_complete_variant: int -> T_TEST-> bool
|
Walther@60710
|
72 |
|
Walther@60710
|
73 |
val of_max_variant: Model_Pattern.T -> T_TEST -> T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval
|
Walther@60715
|
74 |
(*
|
Walther@60715
|
75 |
val of_max_variant: Model_Pattern.T -> T_TEST -> T_TEST * Env.T
|
Walther@60715
|
76 |
*)
|
Walther@60694
|
77 |
(*from isac_test for Minisubpbl*)
|
Walther@60710
|
78 |
val penv_to_string: Proof.context -> T -> string
|
Walther@60705
|
79 |
|
Walther@60694
|
80 |
\<^isac_test>\<open>
|
Walther@60694
|
81 |
(**)
|
Walther@60694
|
82 |
\<close>
|
Walther@60694
|
83 |
|
walther@59938
|
84 |
end
|
walther@59938
|
85 |
|
walther@59942
|
86 |
(**)
|
Walther@60694
|
87 |
structure I_Model(**) : INTERACTION_MODEL(**) =
|
walther@59938
|
88 |
struct
|
walther@59942
|
89 |
(**)
|
walther@59955
|
90 |
|
walther@59958
|
91 |
(** data types **)
|
walther@59958
|
92 |
|
walther@60018
|
93 |
type variant = Model_Def.variant;
|
walther@59940
|
94 |
type variants = Model_Def.variants;
|
walther@59952
|
95 |
type m_field = Model_Def.m_field;
|
walther@59952
|
96 |
type descriptor = Model_Def.descriptor;
|
walther@59938
|
97 |
|
walther@59940
|
98 |
type T = Model_Def.i_model_single list;
|
Walther@60702
|
99 |
(* for developing input from PIDE, we use T_TEST with these ideas:
|
Walther@60702
|
100 |
(1) the new structure is as close to old T, because we want to preserve the old tests
|
Walther@60702
|
101 |
(2) after development (with *_TEST) of essential parts of the Specification's semantics,
|
Walther@60702
|
102 |
we adapt the old tests to the new T_TEST
|
Walther@60702
|
103 |
(3) together with adaption of the tests we remove the *_TEST
|
Walther@60702
|
104 |
*)
|
Walther@60694
|
105 |
type T_TEST = Model_Def.i_model_single_TEST list;
|
walther@59940
|
106 |
datatype feedback = datatype Model_Def.i_model_feedback;
|
Walther@60694
|
107 |
datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST;
|
walther@59940
|
108 |
type single = Model_Def.i_model_single;
|
Walther@60694
|
109 |
type single_TEST = Model_Def.i_model_single_TEST;
|
Walther@60467
|
110 |
val empty_single = Model_Def.i_model_empty;
|
Walther@60467
|
111 |
val empty = []: T;
|
Walther@60704
|
112 |
val empty_TEST = []: T_TEST;
|
Walther@60706
|
113 |
fun feedback_OLD_to_TEST (Cor ((d, ts), penv)) = (Model_Def.Cor_TEST ((d, ts), penv))
|
Walther@60706
|
114 |
| feedback_OLD_to_TEST (Syn c) = (Model_Def.Syn_TEST c)
|
Walther@60706
|
115 |
| feedback_OLD_to_TEST (Typ c) = (Model_Def.Syn_TEST c)
|
Walther@60706
|
116 |
| feedback_OLD_to_TEST (Inc ((d, ts), penv)) = (Model_Def.Inc_TEST ((d, ts), penv))
|
Walther@60706
|
117 |
| feedback_OLD_to_TEST (Sup (d, ts)) = (Model_Def.Sup_TEST (d, ts))
|
Walther@60706
|
118 |
| feedback_OLD_to_TEST (Mis (d, pid)) = Model_Def.Syn_TEST ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
|
Walther@60706
|
119 |
(UnparseC.term (ContextC.for_ERROR ()) pid))
|
Walther@60706
|
120 |
| feedback_OLD_to_TEST (Par s) = (Model_Def.Syn_TEST s)
|
Walther@60706
|
121 |
fun OLD_to_TEST i_old =
|
Walther@60706
|
122 |
map (fn (a, b, c, d, e) => (a, b, c, d, (feedback_OLD_to_TEST e, Position.none))) i_old
|
Walther@60705
|
123 |
|
Walther@60714
|
124 |
fun feedback_TEST_to_OLD (Model_Def.Cor_TEST ((d, ts), penv)) = (Cor ((d, ts), penv))
|
Walther@60714
|
125 |
| feedback_TEST_to_OLD (Model_Def.Syn_TEST c) = (Syn c)
|
Walther@60714
|
126 |
| feedback_TEST_to_OLD (Model_Def.Inc_TEST ((d, ts), penv)) = (Inc ((d, ts), penv))
|
Walther@60714
|
127 |
| feedback_TEST_to_OLD (Model_Def.Sup_TEST (d, ts)) = (Sup (d, ts))
|
Walther@60714
|
128 |
fun TEST_to_OLD i_model =
|
Walther@60714
|
129 |
map (fn (a, b, c, d, (e, _)) => (a, b, c, d, feedback_TEST_to_OLD e)) i_model
|
Walther@60714
|
130 |
|
Walther@60705
|
131 |
type env = Env.T
|
walther@59998
|
132 |
type message = string;
|
walther@59938
|
133 |
|
walther@59942
|
134 |
fun pen2str ctxt (t, ts) =
|
Walther@60675
|
135 |
pair2str (UnparseC.term ctxt t, (strs2str' o map (UnparseC.term ctxt)) ts);
|
walther@59948
|
136 |
|
walther@59942
|
137 |
fun feedback_to_string ctxt (Cor ((d, ts), penv)) =
|
Walther@60675
|
138 |
"Cor " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
|
walther@59942
|
139 |
| feedback_to_string _ (Syn c) = "Syn " ^ c
|
walther@59942
|
140 |
| feedback_to_string _ (Typ c) = "Typ " ^ c
|
walther@59942
|
141 |
| feedback_to_string ctxt (Inc ((d, ts), penv)) =
|
Walther@60675
|
142 |
"Inc " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
|
walther@59942
|
143 |
| feedback_to_string ctxt (Sup (d, ts)) =
|
Walther@60675
|
144 |
"Sup " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
|
walther@59942
|
145 |
| feedback_to_string ctxt (Mis (d, pid)) =
|
Walther@60698
|
146 |
"Mis " ^ UnparseC.term ctxt d ^ " " ^ UnparseC.term ctxt pid
|
walther@59942
|
147 |
| feedback_to_string _ (Par s) = "Trm "^s;
|
Walther@60698
|
148 |
|
Walther@60694
|
149 |
fun feedback_to_string_TEST ctxt (Cor_TEST ((d, ts), penv)) =
|
Walther@60694
|
150 |
"Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
|
Walther@60694
|
151 |
| feedback_to_string_TEST _ (Syn_TEST c) =
|
Walther@60694
|
152 |
"Syn_TEST " ^ c
|
Walther@60714
|
153 |
| feedback_to_string_TEST ctxt (Inc_TEST ((d, []), penv)) =
|
Walther@60717
|
154 |
"Inc_TEST " ^ UnparseC.term ctxt d ^ " " ^ Model_Pattern.empty_for d
|
Walther@60694
|
155 |
| feedback_to_string_TEST ctxt (Inc_TEST ((d, ts), penv)) =
|
Walther@60694
|
156 |
"Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
|
Walther@60694
|
157 |
| feedback_to_string_TEST ctxt (Sup_TEST (d, ts)) =
|
Walther@60694
|
158 |
"Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
|
Walther@60694
|
159 |
|
Walther@60676
|
160 |
fun feedback_to_string' t = feedback_to_string (ContextC.for_ERROR ()) t;
|
Walther@60694
|
161 |
fun feedback_to_string'_TEST _ t = feedback_to_string_TEST (ContextC.for_ERROR ()) t;
|
Walther@60705
|
162 |
fun feedback_TEST_to_string t = feedback_to_string_TEST (ContextC.for_ERROR ()) t;
|
walther@59942
|
163 |
|
walther@59942
|
164 |
fun single_to_string ctxt (i, is, b, s, itm_) =
|
walther@59942
|
165 |
"(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
|
walther@59942
|
166 |
s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
|
Walther@60702
|
167 |
fun single_to_string_TEST ctxt (i, is, b, s, (itm_, _(*Position.T*))) =
|
Walther@60694
|
168 |
"(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
|
Walther@60702
|
169 |
s ^ ", (" ^ feedback_to_string'_TEST ctxt itm_ ^ ", Position.T))";
|
Walther@60694
|
170 |
|
walther@59942
|
171 |
fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
|
Walther@60694
|
172 |
fun to_string_TEST ctxt itms = strs2str' (map (linefeed o (single_to_string_TEST ctxt)) itms);
|
walther@59942
|
173 |
|
walther@59958
|
174 |
|
Walther@60694
|
175 |
(** make a Tactic.T **)
|
Walther@60694
|
176 |
|
Walther@60477
|
177 |
fun make_tactic m_field (term_as_string, i_model) =
|
walther@59992
|
178 |
case m_field of
|
walther@59992
|
179 |
"#Given" => Tactic.Add_Given' (term_as_string, i_model)
|
walther@59992
|
180 |
| "#Find" => Tactic.Add_Find' (term_as_string, i_model)
|
walther@59992
|
181 |
| "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
|
walther@59992
|
182 |
| str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
|
walther@59992
|
183 |
|
walther@59992
|
184 |
|
walther@59958
|
185 |
(** initialise a model **)
|
walther@59958
|
186 |
|
walther@59958
|
187 |
fun init pbt =
|
walther@59958
|
188 |
let
|
walther@59958
|
189 |
fun pbt2itm (f, (d, _)) = (0, [], false, f, Inc ((d, []), (TermC.empty, [])))
|
walther@59958
|
190 |
in map pbt2itm pbt end
|
Walther@60556
|
191 |
|
Walther@60702
|
192 |
(*
|
Walther@60702
|
193 |
Design decision:
|
Walther@60705
|
194 |
* Now the Model in Specification is intialised such that the placement of items can be
|
Walther@60702
|
195 |
maximally stable during interactive input to the Specification.
|
Walther@60702
|
196 |
* Template.show provides the initial output to the user and thus determines what will be parsed
|
Walther@60702
|
197 |
by Outer_Syntax later during interaction.
|
Walther@60705
|
198 |
* The relation between O_Model.T and I_Model.T becomes much simpler.
|
Walther@60702
|
199 |
*)
|
Walther@60702
|
200 |
(**)
|
Walther@60702
|
201 |
fun pat_to_item o_model (_, (descriptor, _)) =
|
Walther@60702
|
202 |
case find_first (fn (_, _, _, desc, _) => desc = descriptor) o_model of
|
Walther@60702
|
203 |
NONE => raise ERROR "I_Model.pat_to_item_TEST with NONE"
|
Walther@60702
|
204 |
| SOME (_, variants, m_field, descr, _) => (variants, false, m_field,
|
Walther@60714
|
205 |
(Inc_TEST ((descr, []), (descr, [])), Position.none))
|
Walther@60702
|
206 |
fun init_TEST o_model model_patt =
|
Walther@60690
|
207 |
let
|
Walther@60702
|
208 |
val pre_items = map (pat_to_item o_model) model_patt
|
Walther@60702
|
209 |
in
|
Walther@60702
|
210 |
O_Model.add_enumerate pre_items |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e))
|
Walther@60702
|
211 |
end
|
Walther@60702
|
212 |
(**)
|
Walther@60691
|
213 |
(*########################* )
|
Walther@60692
|
214 |
val init = init_TEST see Test_Theory.thy
|
Walther@60691
|
215 |
( *########################*)
|
walther@59958
|
216 |
|
walther@59958
|
217 |
(** check input on a model **)
|
walther@59942
|
218 |
|
Walther@60705
|
219 |
(*/---------------- old code before I_Model.T_TEST -------------------------------------------\* )
|
Walther@60705
|
220 |
WENT TO Pre_Conds
|
Walther@60705
|
221 |
( *\---------------- old code before I_Model.T_TEST -------------------------------------------/*)
|
walther@59943
|
222 |
|
Walther@60705
|
223 |
(*/---------------- new code with I_Model.T_TEST ---------------------------------------------\*)
|
Walther@60705
|
224 |
(*\---------------- new code with I_Model.T_TEST ---------------------------------------------/*)
|
walther@59943
|
225 |
|
Walther@60705
|
226 |
(*/---------------- old code -----------------------------------------------------------------\*)
|
Walther@60477
|
227 |
fun o_model_values (Cor ((_, ts), _)) = ts
|
Walther@60477
|
228 |
| o_model_values (Syn _) = []
|
Walther@60477
|
229 |
| o_model_values (Typ _) = []
|
Walther@60477
|
230 |
| o_model_values (Inc ((_, ts), _)) = ts
|
Walther@60477
|
231 |
| o_model_values (Sup (_, ts)) = ts
|
Walther@60477
|
232 |
| o_model_values (Mis _) = []
|
Walther@60477
|
233 |
| o_model_values _ = raise ERROR "o_model_values: uncovered case in fun.def.";
|
walther@59943
|
234 |
|
Walther@60664
|
235 |
val unique = Syntax.read_term\<^context> "UnIqE_tErM";
|
Walther@60477
|
236 |
fun descriptor (Cor ((d ,_), _)) = d
|
Walther@60477
|
237 |
| descriptor (Syn _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
|
Walther@60477
|
238 |
| descriptor (Typ _) = ((*tracing ("*** descriptor: Typ ("^c^")");*) unique)
|
Walther@60477
|
239 |
| descriptor (Inc ((d, _), _)) = d
|
Walther@60477
|
240 |
| descriptor (Sup (d, _)) = d
|
Walther@60477
|
241 |
| descriptor (Mis (d, _)) = d
|
Walther@60477
|
242 |
| descriptor _ = raise ERROR "descriptor: uncovered case in fun.def.";
|
Walther@60705
|
243 |
fun descriptor_TEST (Cor_TEST ((d ,_), _)) = d
|
Walther@60705
|
244 |
| descriptor_TEST (Syn_TEST _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
|
Walther@60705
|
245 |
| descriptor_TEST (Inc_TEST ((d, _), _)) = d
|
Walther@60705
|
246 |
| descriptor_TEST (Sup_TEST (d, _)) = d
|
Walther@60705
|
247 |
| descriptor_TEST _ = raise ERROR "descriptor_TEST: uncovered case in fun.def.";
|
walther@59943
|
248 |
|
Walther@60710
|
249 |
fun descr_pairs_to_string ctxt equal_descr_pairs =
|
Walther@60710
|
250 |
(map (fn (a, b) => pair (Model_Pattern.pat2str ctxt a) (single_to_string_TEST ctxt b)
|
Walther@60710
|
251 |
|> pair2str) equal_descr_pairs)
|
Walther@60710
|
252 |
|> strs2str'
|
Walther@60710
|
253 |
|
Walther@60668
|
254 |
(*val string_of_descr_values: term * (term list) -> string
|
Walther@60678
|
255 |
fun string_of_descr_values (d, ts) = pair2str (UnparseC.term (ContextC.for_ERROR ()) d, UnparseC.terms ts);*)
|
Walther@60710
|
256 |
fun penvval_in (Cor ((d, _), (_, ts))) = (**)[Input_Descript.join'''' (d, ts)](** )------(**)[]( **)
|
walther@59956
|
257 |
| penvval_in (Syn (_)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
|
walther@59956
|
258 |
| penvval_in (Typ (_)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
|
Walther@60710
|
259 |
| penvval_in (Inc (_, (_, ts))) = (**)ts(** )------------------------------------------(**)[]( **)
|
Walther@60477
|
260 |
| penvval_in (Sup _) = ((*tracing ("*** penvval_in: Sup " ^ string_of_descr_values dts);*) [])
|
walther@59956
|
261 |
| penvval_in (Mis (_, _)) = ((*tracing ("*** penvval_in: Mis " ^
|
Walther@60678
|
262 |
pair2str(UnparseC.term (ContextC.for_ERROR ()) d, UnparseC.term (ContextC.for_ERROR ()) t));*) [])
|
walther@59962
|
263 |
| penvval_in _ = raise ERROR "penvval_in: uncovered case in fun.def.";
|
walther@59943
|
264 |
|
Walther@60705
|
265 |
fun variables itms = itms |> Pre_Conds.environment |> map snd
|
walther@59943
|
266 |
|
Walther@60664
|
267 |
val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";
|
walther@59956
|
268 |
|
Walther@60670
|
269 |
(* get a term from O_Model, notyet input in I_Model.
|
Walther@60670
|
270 |
the term from O_Model is thrown back to a string in order to reuse
|
walther@59992
|
271 |
machinery for immediate input by the user. *)
|
Walther@60477
|
272 |
fun get_field_term thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
|
Walther@60477
|
273 |
(fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (o_model_values itm_) ts))
|
walther@59992
|
274 |
|
walther@59956
|
275 |
(* update the itm_ already input, all..from ori *)
|
walther@59956
|
276 |
fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
|
walther@59956
|
277 |
let
|
Walther@60477
|
278 |
val ts' = union op = (o_model_values itm_) ts;
|
Walther@60478
|
279 |
val pval = [Input_Descript.join'''' (d, ts')]
|
walther@59956
|
280 |
(* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
|
walther@59956
|
281 |
val complete = if eq_set op = (ts', all) then true else false
|
walther@59956
|
282 |
in
|
walther@59956
|
283 |
case itm_ of
|
walther@59956
|
284 |
(Cor _) =>
|
walther@59956
|
285 |
(if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
|
walther@59956
|
286 |
else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval))))
|
walther@59962
|
287 |
| (Syn c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
|
walther@59962
|
288 |
| (Typ c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
|
walther@59956
|
289 |
| (Inc _) =>
|
walther@59956
|
290 |
if complete
|
walther@59956
|
291 |
then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
|
walther@59956
|
292 |
else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
|
walther@59956
|
293 |
| (Sup (d,ts')) => (*4.9.01 lost env*)
|
walther@59956
|
294 |
(*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
|
walther@59956
|
295 |
(*else (id,vt,complete,fd,Cor((d,ts'),e))*)
|
walther@59956
|
296 |
(* 28.1.00: not completely clear ---^^^ etc.*)
|
walther@59956
|
297 |
| (Mis _) => (* 4.9.01: Mis just copied *)
|
walther@59956
|
298 |
if complete
|
walther@59956
|
299 |
then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
|
walther@59956
|
300 |
else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
|
walther@59998
|
301 |
| i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_to_string' i)
|
walther@59956
|
302 |
end
|
walther@59956
|
303 |
|
walther@59956
|
304 |
fun eq1 d (_, (d', _)) = (d = d')
|
Walther@60477
|
305 |
fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (descriptor itm_)
|
walther@59956
|
306 |
|
walther@59956
|
307 |
fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
|
walther@59956
|
308 |
case find_first (eq1 d) pbt of
|
walther@59956
|
309 |
SOME (_, (_, pid)) =>
|
walther@59956
|
310 |
(case find_first (eq3 f d) itms of
|
walther@59998
|
311 |
SOME (_, _, _, _, itm_) =>
|
Walther@60477
|
312 |
let val ts' = inter op = (o_model_values itm_) ts
|
walther@59956
|
313 |
in
|
walther@59956
|
314 |
if subset op = (ts, ts')
|
Walther@60675
|
315 |
then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single)
|
walther@59998
|
316 |
else ("", ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts))
|
walther@59956
|
317 |
end
|
walther@59998
|
318 |
| NONE => ("", ori_2itm (Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts)))
|
walther@59956
|
319 |
| NONE => ("", ori_2itm (Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
|
walther@59956
|
320 |
|
Walther@60477
|
321 |
datatype add_single =
|
walther@59958
|
322 |
Add of single (* return-value of check_single *)
|
walther@59998
|
323 |
| Err of string (* error-message *)
|
walther@59956
|
324 |
|
walther@59956
|
325 |
(*
|
walther@59956
|
326 |
Create feedback for input of TermC.as_string to m_field;
|
walther@59956
|
327 |
check w.r.t. O_Model.T and Model_Pattern.T.
|
walther@59998
|
328 |
In case of O_Model.T = [] (i.e. no data for user-guidance in Formalise.T)
|
walther@59958
|
329 |
check_single is extremely permissive.
|
walther@59956
|
330 |
*)
|
Walther@60658
|
331 |
(*will come directly from PIDE -----------------vvvvvvvvvvv
|
Walther@60658
|
332 |
in case t comes from Step.specify_do_next -----------vvv = Position.none*)
|
Walther@60658
|
333 |
fun check_single ctxt m_field [] i_model m_patt (ct(*, pos*)) =
|
Walther@60658
|
334 |
let
|
Walther@60658
|
335 |
val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
|
Walther@60661
|
336 |
(*/------------ replace by ParseC.term_position -----------\*)
|
Walther@60661
|
337 |
val t = Syntax.read_term ctxt ct
|
Walther@60658
|
338 |
handle ERROR msg => error (msg (*^ Position.here pos*))
|
Walther@60661
|
339 |
(*\------------ replace by ParseC.term_position -----------/*)
|
Walther@60658
|
340 |
(*NONE => Add (i, [], false, m_field, Syn ct)*)
|
Walther@60658
|
341 |
val (d, ts) = Input_Descript.split t
|
Walther@60658
|
342 |
in
|
Walther@60658
|
343 |
if d = TermC.empty then
|
Walther@60658
|
344 |
Add (i, [], false, m_field, Mis (unknown_descriptor, hd ts))
|
Walther@60658
|
345 |
else
|
Walther@60658
|
346 |
(case find_first (eq1 d) m_patt of
|
Walther@60658
|
347 |
NONE => Add (i, [], true, m_field, Sup (d,ts))
|
Walther@60658
|
348 |
| SOME (f, (_, id)) =>
|
Walther@60658
|
349 |
let
|
Walther@60658
|
350 |
fun eq2 d (i, _, _, _, itm_) = d = (descriptor itm_) andalso i <> 0
|
Walther@60658
|
351 |
in
|
Walther@60658
|
352 |
case find_first (eq2 d) i_model of
|
Walther@60658
|
353 |
NONE => Add (i, [], true, f,Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
|
Walther@60658
|
354 |
| SOME (i', _, _, _, itm_) =>
|
Walther@60658
|
355 |
if Input_Descript.for_list d then
|
Walther@60658
|
356 |
let
|
Walther@60658
|
357 |
val in_itm = o_model_values itm_
|
Walther@60658
|
358 |
val ts' = union op = ts in_itm
|
Walther@60658
|
359 |
val i'' = if in_itm = [] then i else i'
|
Walther@60658
|
360 |
in Add (i'', [], true, f, Cor ((d, ts'), (id, [Input_Descript.join'''' (d, ts')])))end
|
Walther@60658
|
361 |
else Add (i', [], true, f, Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
|
Walther@60658
|
362 |
end)
|
Walther@60658
|
363 |
end
|
Walther@60658
|
364 |
(* for MethodC: #undef completed vvvvv vvvvvv term_as_string *)
|
Walther@60658
|
365 |
(*will come directly from PIDE ----------------------vvvvvvvvvvv*)
|
Walther@60658
|
366 |
| check_single ctxt m_field o_model i_model m_patt (str(*, pos*)) =
|
Walther@60658
|
367 |
let
|
Walther@60659
|
368 |
val (t as (descriptor $ _)) = Syntax.read_term ctxt str
|
Walther@60658
|
369 |
handle ERROR msg => error (msg (*^ Position.here pp*))
|
Walther@60659
|
370 |
(*old code: NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")*)
|
Walther@60658
|
371 |
in
|
Walther@60658
|
372 |
case Model_Pattern.get_field descriptor m_patt of
|
Walther@60658
|
373 |
NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^
|
Walther@60675
|
374 |
UnparseC.term ctxt descriptor ^ "\"")
|
Walther@60658
|
375 |
| SOME m_field' =>
|
Walther@60658
|
376 |
if m_field <> m_field' then
|
Walther@60675
|
377 |
Err ("ERROR I_Model.check_single: \"" ^ UnparseC.term ctxt t ^ "\"" ^
|
Walther@60658
|
378 |
"\" not for field \"" ^ m_field ^ "\"")
|
Walther@60658
|
379 |
else
|
Walther@60658
|
380 |
case O_Model.contains ctxt m_field o_model t of
|
Walther@60658
|
381 |
("", ori', all) =>
|
Walther@60658
|
382 |
(case is_notyet_input ctxt i_model all ori' m_patt of
|
Walther@60658
|
383 |
("", itm) => Add itm
|
Walther@60658
|
384 |
| (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
|
Walther@60658
|
385 |
| (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg)
|
Walther@60658
|
386 |
end
|
Walther@60658
|
387 |
|
walther@59958
|
388 |
|
walther@59958
|
389 |
(** add input **)
|
walther@59958
|
390 |
|
Walther@60586
|
391 |
fun overwrite_ppc thy itm model =
|
walther@59958
|
392 |
let
|
walther@59958
|
393 |
fun repl _ (_, _, _, _, itm_) [] =
|
walther@60360
|
394 |
raise ERROR ("overwrite_ppc: " ^ feedback_to_string (Proof_Context.init_global thy) itm_
|
walther@60360
|
395 |
^ " not found")
|
Walther@60586
|
396 |
| repl model' itm (p :: model) =
|
walther@59958
|
397 |
if (#1 itm) = (#1 p)
|
Walther@60586
|
398 |
then model' @ [itm] @ model
|
Walther@60586
|
399 |
else repl (model' @ [p]) itm model
|
Walther@60586
|
400 |
in repl [] itm model end
|
walther@59958
|
401 |
|
walther@59958
|
402 |
(* find_first item with #1 equal to id *)
|
walther@59958
|
403 |
fun seek_ppc _ [] = NONE
|
Walther@60586
|
404 |
| seek_ppc id (p :: model) = if id = #1 (p: single) then SOME p else seek_ppc id model
|
walther@59958
|
405 |
|
walther@59958
|
406 |
(* 10.3.00: insert the already compiled itm into model;
|
walther@59958
|
407 |
ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
|
Walther@60586
|
408 |
fun add_single thy itm model =
|
walther@59958
|
409 |
let
|
Walther@60477
|
410 |
fun eq_untouched d (0, _, _, _, itm_) = (d = descriptor itm_)
|
walther@59958
|
411 |
| eq_untouched _ _ = false
|
Walther@60586
|
412 |
val model' = case seek_ppc (#1 itm) model of
|
Walther@60586
|
413 |
SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
|
Walther@60586
|
414 |
| NONE => (model @ [itm])
|
Walther@60586
|
415 |
in filter_out (eq_untouched ((descriptor o #5) itm)) model' end
|
walther@59956
|
416 |
|
walther@59988
|
417 |
fun complete' pbt (i, v, f, d, ts) =
|
Walther@60654
|
418 |
case \<^try>\<open> (i, v, true, f, Cor ((d, ts),
|
Walther@60654
|
419 |
((find_first ((fn descriptor => (fn (_, (d, _)) => descriptor = d)) d)) pbt |> the |> snd |> snd, ts)
|
Walther@60654
|
420 |
))\<close> of
|
walther@60265
|
421 |
SOME x => x
|
walther@60265
|
422 |
| NONE => (i, v, true, f, Cor ((d, ts), (d, ts)))
|
walther@59988
|
423 |
|
walther@59988
|
424 |
(* filter out oris which have same description in itms *)
|
walther@59988
|
425 |
fun filter_outs oris [] = oris
|
walther@59988
|
426 |
| filter_outs oris (i::itms) =
|
walther@59988
|
427 |
let
|
Walther@60477
|
428 |
val ors = filter_out ((curry op = ((descriptor o #5) i)) o (#4)) oris
|
walther@59988
|
429 |
in
|
walther@59988
|
430 |
filter_outs ors itms
|
walther@59988
|
431 |
end
|
walther@59988
|
432 |
|
walther@59988
|
433 |
(* filter oris which are in pbt, too *)
|
walther@59988
|
434 |
fun filter_pbt oris pbt =
|
walther@59988
|
435 |
let
|
walther@59988
|
436 |
val dscs = map (fst o snd) pbt
|
walther@59988
|
437 |
in
|
walther@59988
|
438 |
filter ((member op= dscs) o (#4)) oris
|
walther@59988
|
439 |
end
|
walther@59988
|
440 |
|
walther@59988
|
441 |
fun is_error (Cor _) = false
|
walther@59988
|
442 |
| is_error (Sup _) = false
|
walther@59988
|
443 |
| is_error (Inc _) = false
|
walther@59988
|
444 |
| is_error (Mis _) = false
|
walther@59988
|
445 |
| is_error _ = true
|
walther@59988
|
446 |
|
walther@59988
|
447 |
(*create output-string for itm_*)
|
Walther@60674
|
448 |
fun to_p_model thy (Cor ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
|
walther@59988
|
449 |
| to_p_model _ (Syn c) = c
|
walther@59988
|
450 |
| to_p_model _ (Typ c) = c
|
Walther@60673
|
451 |
| to_p_model thy (Inc ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
|
Walther@60673
|
452 |
| to_p_model thy (Sup (d, ts)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
|
Walther@60674
|
453 |
| to_p_model thy (Mis (d, pid)) = UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid
|
walther@59988
|
454 |
| to_p_model _ _ = raise ERROR "to_p_model: uncovered definition"
|
walther@59988
|
455 |
|
Walther@60477
|
456 |
fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (descriptor itm_ = descriptor iitm_)
|
walther@59988
|
457 |
|
walther@59988
|
458 |
(* insert_ppc = add for appl_add', input_icalhd 11.03,
|
walther@59988
|
459 |
handles superfluous items carelessly *)
|
walther@59988
|
460 |
fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
|
walther@59988
|
461 |
|
walther@59988
|
462 |
(* combine itms from pbl + met and complete them wrt. pbt *)
|
walther@59988
|
463 |
(* FIXXXME.WN031205 complete doesnt handle incorrect itms !*)
|
walther@59988
|
464 |
fun complete oris pits mits met =
|
walther@59988
|
465 |
let
|
Walther@60705
|
466 |
val vat = Pre_Conds.max_variant pits;
|
walther@59988
|
467 |
val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
|
walther@59988
|
468 |
val ors = filter ((member_swap op= vat) o (#2)) oris
|
walther@59988
|
469 |
val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
|
walther@59988
|
470 |
in
|
walther@59988
|
471 |
itms @ (map (complete' met) os)
|
walther@59988
|
472 |
end
|
Walther@60704
|
473 |
val complete_Test = complete
|
walther@59988
|
474 |
|
walther@59988
|
475 |
(* complete model and guard of a calc-head *)
|
Walther@60586
|
476 |
fun complete_method (oris, mpc, model, probl) =
|
walther@59988
|
477 |
let
|
walther@59988
|
478 |
val pits = filter_out ((curry op= false) o (#3)) probl
|
Walther@60705
|
479 |
val vat = if probl = [] then 1 else Pre_Conds.max_variant probl
|
walther@59988
|
480 |
val pors = filter ((member_swap op = vat) o (#2)) oris
|
walther@59988
|
481 |
val pors = filter_outs pors pits (*which are in pbl already*)
|
Walther@60586
|
482 |
val pors = (filter_pbt pors model) (*which are in pbt, too*)
|
Walther@60586
|
483 |
val pits = pits @ (map (complete' model) pors)
|
walther@59988
|
484 |
val mits = complete oris pits [] mpc
|
walther@59988
|
485 |
in (pits, mits) end
|
walther@59988
|
486 |
|
Walther@60480
|
487 |
(* TODO: also check if all elements are I_Model.Cor *)
|
walther@59998
|
488 |
fun is_complete ([]: T) = false
|
walther@59988
|
489 |
| is_complete itms = foldl and_ (true, (map #3 itms))
|
walther@59986
|
490 |
|
Walther@60705
|
491 |
|
Walther@60705
|
492 |
(** is_complete_OLD for PIDE **)
|
Walther@60705
|
493 |
|
Walther@60705
|
494 |
(*
|
Walther@60705
|
495 |
"OLD" means: this code will adapted to maintain the old texts.
|
Walther@60705
|
496 |
Parts of the code will be required for Template.show etc.
|
Walther@60705
|
497 |
*)
|
Walther@60705
|
498 |
|
Walther@60705
|
499 |
fun is_complete_variant no_model_items i_model =
|
Walther@60705
|
500 |
no_model_items = length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model)
|
Walther@60705
|
501 |
|
Walther@60705
|
502 |
fun is_complete_OLD ctxt model_patt where_rls pres i_model =
|
Walther@60705
|
503 |
let
|
Walther@60705
|
504 |
val no_model_items = length model_patt
|
Walther@60706
|
505 |
val variants_envs = Pre_Conds.sep_variants_envs model_patt i_model;
|
Walther@60705
|
506 |
val result_all_variants = map
|
Walther@60705
|
507 |
(fn ((i_model, env_subst, env_eval), variant) =>
|
Walther@60705
|
508 |
if fst (Pre_Conds.check_variant_envs ctxt where_rls pres env_subst env_eval)
|
Walther@60705
|
509 |
andalso is_complete_variant no_model_items i_model
|
Walther@60705
|
510 |
then SOME [variant] else NONE) variants_envs
|
Walther@60705
|
511 |
in
|
Walther@60705
|
512 |
if forall is_none result_all_variants
|
Walther@60705
|
513 |
then NONE
|
Walther@60705
|
514 |
else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
|
Walther@60705
|
515 |
end
|
Walther@60705
|
516 |
|
Walther@60710
|
517 |
val of_max_variant = Pre_Conds.of_max_variant
|
Walther@60710
|
518 |
|
Walther@60710
|
519 |
(*get_penv: single -> (term * term list) list*)
|
Walther@60710
|
520 |
fun get_penv (_, _, _, _, Cor (_, elem)) = [elem]
|
Walther@60710
|
521 |
| get_penv (_, _, _, _, Inc (_, elem)) = [elem]
|
Walther@60710
|
522 |
| get_penv _ = []
|
Walther@60710
|
523 |
fun penv_to_string ctxt i_model = map get_penv i_model
|
Walther@60710
|
524 |
|> flat
|
Walther@60710
|
525 |
|> map (fn (t, ts) => pair2str (UnparseC.term ctxt t, UnparseC.terms ctxt ts))
|
Walther@60710
|
526 |
|> strs2str'
|
Walther@60710
|
527 |
|
walther@60126
|
528 |
(**)end(**);
|