wneuper@59595
|
1 |
(* Title: collect all defitions for the Lucas-Interpreter
|
wneuper@59595
|
2 |
Author: Walther Neuper 110226
|
wneuper@59595
|
3 |
(c) due to copyright terms
|
walther@59950
|
4 |
|
Walther@60556
|
5 |
Descriptors for interactive input into a Specification of an Example.
|
Walther@60556
|
6 |
|
walther@59950
|
7 |
Since PblObj.ctxt records explicit type constraints in Formalise.model,
|
Walther@60556
|
8 |
and since we have Model_Pattern.adapt_to_type,
|
walther@59950
|
9 |
the types of the descriptors below can be more relaxed.
|
walther@59950
|
10 |
*)
|
wneuper@59595
|
11 |
|
wenzelm@60192
|
12 |
theory Input_Descript imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
|
wneuper@59595
|
13 |
begin
|
wneuper@59595
|
14 |
|
walther@59951
|
15 |
subsection \<open>typedecl for descriptors of input in specify-phase\<close>
|
wneuper@59595
|
16 |
text \<open>
|
walther@59953
|
17 |
The typedecl below MUST ALL be registered in "Input_Descript.is_a"
|
wneuper@59595
|
18 |
\<close>
|
wneuper@59595
|
19 |
typedecl nam (* named variables *)
|
wneuper@59595
|
20 |
typedecl una (* unnamed variables *)
|
wneuper@59595
|
21 |
typedecl unl (* unnamed variables of type list, elementwise input prohibited*)
|
wneuper@59595
|
22 |
typedecl str (* structured variables *)
|
wneuper@59595
|
23 |
typedecl toreal (* var with undef real value: forces typing *)
|
wneuper@59595
|
24 |
typedecl toreall (* var with undef real list value: forces typing *)
|
wneuper@59595
|
25 |
typedecl tobooll (* var with undef bool list value: forces typing *)
|
wneuper@59595
|
26 |
typedecl unknow (* input without dsc in fmz=[] *)
|
wneuper@59595
|
27 |
typedecl cpy (* copy-named variables identified by .._0, .._i .._' in pbt *)
|
wneuper@59595
|
28 |
|
walther@59951
|
29 |
subsection \<open>consts for general descriptors of input in the specify-phase\<close>
|
wneuper@59595
|
30 |
|
wneuper@59595
|
31 |
consts
|
wneuper@59595
|
32 |
(*TODO.180331: review for localisation of model-patterns and of method's guards*)
|
wneuper@59595
|
33 |
someList :: "'a list => unl" (*not for elementwise input, eg. inssort*)
|
wneuper@59595
|
34 |
|
wneuper@59595
|
35 |
additionalRels :: "bool list => una"
|
Walther@60460
|
36 |
boundVariable :: "real => una"
|
Walther@60460
|
37 |
FunctionVariable :: "real => una"
|
wneuper@59595
|
38 |
derivative :: "real => una"
|
wneuper@59595
|
39 |
equalities :: "bool list => tobooll" (*WN071228 see fixedValues*)
|
wneuper@59595
|
40 |
equality :: "bool => una"
|
wneuper@59595
|
41 |
errorBound :: "bool => nam"
|
Walther@60460
|
42 |
ErrorBound :: "bool => nam"
|
wneuper@59595
|
43 |
|
wneuper@59595
|
44 |
fixedValues :: "bool list => nam"
|
Walther@60460
|
45 |
Constants :: "bool list => nam"
|
wneuper@59595
|
46 |
functionEq :: "bool => una" (*6.5.03: functionTerm -> functionEq*)
|
wneuper@59595
|
47 |
antiDerivative :: "bool => una"
|
wneuper@59595
|
48 |
functionOf :: "real => una"
|
wneuper@59595
|
49 |
(*functionTerm :: 'a => toreal 28.11.00*)
|
wneuper@59595
|
50 |
functionTerm :: "real => una" (*6.5.03: functionTerm -> functionEq*)
|
wneuper@59595
|
51 |
functionName :: "real => una"
|
wneuper@59595
|
52 |
interval :: "real set => una"
|
Walther@60460
|
53 |
Domain :: "real set => una"
|
wneuper@59595
|
54 |
maxArgument :: "bool => toreal"
|
wneuper@59595
|
55 |
maximum :: "real => toreal"
|
Walther@60460
|
56 |
Maximum :: "real => toreal"
|
Walther@60460
|
57 |
Extremum :: "bool => toreal"
|
wneuper@59595
|
58 |
|
wneuper@59595
|
59 |
relations :: "bool list => una"
|
Walther@60460
|
60 |
SideConditions :: "bool list => una"
|
wneuper@59595
|
61 |
solutions :: "bool list => toreall"
|
wneuper@59595
|
62 |
solveFor :: "real => una"
|
wneuper@59595
|
63 |
differentiateFor:: "real => una"
|
wneuper@59595
|
64 |
unknown :: "'a => unknow"
|
Walther@60460
|
65 |
valuesFor :: "real list => toreall"
|
Walther@60460
|
66 |
AdditionalValues :: "real list => toreall"
|
wneuper@59595
|
67 |
|
wneuper@59595
|
68 |
intTestGiven :: "int => una"
|
wneuper@59595
|
69 |
realTestGiven :: "real => una"
|
wneuper@59595
|
70 |
realTestFind :: "real => una"
|
wneuper@59595
|
71 |
boolTestGiven :: "bool => una"
|
wneuper@59595
|
72 |
boolTestFind :: "bool => una"
|
wneuper@59595
|
73 |
|
wneuper@59595
|
74 |
subsection \<open>Functions decking for descriptions of input in specify-phase\<close>
|
wneuper@59595
|
75 |
ML \<open>
|
wneuper@59595
|
76 |
\<close> ML \<open>
|
wneuper@59595
|
77 |
signature INPUT_DESCRIPT =
|
wneuper@59595
|
78 |
sig
|
walther@60125
|
79 |
(*type T ..TODO rename*)
|
Walther@60766
|
80 |
type descriptor
|
walther@59953
|
81 |
|
wenzelm@60223
|
82 |
val for_real_list: term -> bool
|
walther@59953
|
83 |
val for_list: term -> bool
|
wenzelm@60223
|
84 |
\<^isac_test>\<open>
|
wenzelm@60223
|
85 |
val for_bool_list: term -> bool
|
wenzelm@60223
|
86 |
val for_fun: term -> bool
|
wenzelm@60223
|
87 |
val is_a: term -> bool
|
wenzelm@60223
|
88 |
\<close>
|
walther@59953
|
89 |
val split: term -> descriptor * term list
|
walther@59953
|
90 |
val split': term * term -> term list
|
walther@59953
|
91 |
val join: descriptor * term list -> term
|
walther@59953
|
92 |
val join': descriptor * term list -> term
|
walther@59953
|
93 |
val join''': descriptor * term list -> string
|
walther@59953
|
94 |
val join'''': descriptor * term list -> term
|
wneuper@59595
|
95 |
end
|
wneuper@59595
|
96 |
\<close> ML \<open>
|
walther@59954
|
97 |
|
walther@59954
|
98 |
|
wneuper@59595
|
99 |
(**)
|
wneuper@59595
|
100 |
structure Input_Descript(**): INPUT_DESCRIPT =(**)
|
wneuper@59595
|
101 |
struct
|
wneuper@59595
|
102 |
(**)
|
walther@59953
|
103 |
|
Walther@60766
|
104 |
type descriptor = term; (*see Model_Def.descriptor*)
|
walther@59953
|
105 |
|
wneuper@59595
|
106 |
(* distinguish input to Model (deep embedding of terms as Isac's object language) *)
|
walther@60373
|
107 |
fun for_real_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>real\<close>, [])]), _]))) = true
|
walther@60373
|
108 |
| for_real_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>real\<close>, [])]),_])) $ _) = true
|
walther@59953
|
109 |
| for_real_list _ = false;
|
walther@60373
|
110 |
fun for_bool_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>, [])]), _]))) = true
|
walther@60373
|
111 |
| for_bool_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>, [])]),_])) $ _) = true
|
walther@59953
|
112 |
| for_bool_list _ = false;
|
wenzelm@60309
|
113 |
fun for_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, _), _]))) = true
|
wenzelm@60309
|
114 |
| for_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, _), _])) $ _) = true
|
wneuper@59595
|
115 |
(*WN:8.5.03: ??? TODO test/../scrtools.sml ~~~~ ???*)
|
walther@59953
|
116 |
| for_list _ = false;
|
walther@60373
|
117 |
fun for_fun (Const (_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>unl\<close>, _)]))) = true
|
walther@59953
|
118 |
| for_fun _ = false;
|
walther@60373
|
119 |
fun is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>nam\<close>, _)]))) = true
|
walther@60373
|
120 |
| is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>una\<close>, _)]))) = true
|
walther@60373
|
121 |
| is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>unl\<close>, _)]))) = true
|
walther@60373
|
122 |
| is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>str\<close>, _)]))) = true
|
walther@60373
|
123 |
| is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>toreal\<close>, _)]))) = true
|
walther@60373
|
124 |
| is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>toreall\<close>, _)])))= true
|
walther@60373
|
125 |
| is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>tobooll\<close>, _)])))= true
|
walther@60373
|
126 |
| is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>unknow\<close>, _)])))= true
|
walther@60373
|
127 |
| is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>cpy\<close>, _)])))= true
|
walther@59953
|
128 |
| is_a _ = false;
|
wneuper@59595
|
129 |
|
walther@59953
|
130 |
(* special handling for lists. ?WN:14.5.03 ??!? *)
|
walther@59953
|
131 |
fun dest_list (d, ts) =
|
walther@59953
|
132 |
let fun dest t =
|
walther@59953
|
133 |
if for_list d andalso not (for_fun d) andalso not (is_Free t) (*..for pbt*)
|
walther@59953
|
134 |
then TermC.isalist2list t
|
walther@59953
|
135 |
else [t]
|
walther@59953
|
136 |
in (flat o (map dest)) ts end;
|
wneuper@59599
|
137 |
|
walther@59997
|
138 |
(* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]", "[b]"] *)
|
walther@59953
|
139 |
fun take_apart t =
|
walther@59953
|
140 |
let val elems = TermC.isalist2list t
|
walther@59953
|
141 |
in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
|
walther@59953
|
142 |
|
walther@59953
|
143 |
(* decompose an input into description, terms (ev. elems of lists),
|
walther@59953
|
144 |
and the value for the problem-environment; inv to join *)
|
walther@59953
|
145 |
fun split (t as d $ arg) =
|
walther@59953
|
146 |
if is_a d
|
walther@59953
|
147 |
then if for_list d andalso TermC.is_list arg andalso for_fun d |> not
|
walther@59953
|
148 |
then (d, take_apart arg)
|
walther@59953
|
149 |
else (d, [arg])
|
walther@59953
|
150 |
else (TermC.empty, TermC.dest_list' t)
|
walther@59953
|
151 |
| split t =
|
walther@59953
|
152 |
let val t' as (h, _) = strip_comb t;
|
walther@59953
|
153 |
in
|
walther@59953
|
154 |
if is_a h
|
walther@59953
|
155 |
then (h, dest_list t')
|
walther@59953
|
156 |
else (TermC.empty, TermC.dest_list' t)
|
walther@59953
|
157 |
end;
|
walther@59953
|
158 |
|
walther@59953
|
159 |
(* version returning ts only *)
|
walther@59953
|
160 |
fun split' (d, arg) =
|
walther@59953
|
161 |
if is_a d
|
walther@59953
|
162 |
then if for_list d
|
walther@59953
|
163 |
then if TermC.is_list arg
|
walther@59953
|
164 |
then if for_fun d
|
walther@59953
|
165 |
then ([arg]) (* e.g. someList [1,3,2] *)
|
walther@59953
|
166 |
else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
|
walther@59953
|
167 |
else ([arg]) (* a variable or metavariable for a list *)
|
walther@59953
|
168 |
else ([arg])
|
walther@59953
|
169 |
else (TermC.dest_list' arg)
|
walther@59953
|
170 |
|
Walther@60710
|
171 |
(*
|
Walther@60710
|
172 |
take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]", "[b]"]
|
Walther@60710
|
173 |
take_apart_inv: term list -> term
|
Walther@60710
|
174 |
*)
|
walther@59953
|
175 |
fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
|
walther@59953
|
176 |
let val elems = (flat o (map TermC.isalist2list)) ts;
|
walther@59953
|
177 |
in TermC.list2isalist (type_of (hd elems)) elems end;
|
walther@59953
|
178 |
|
Walther@60661
|
179 |
fun script_parse str =
|
Walther@60661
|
180 |
let
|
Walther@60661
|
181 |
val ctxt = @{theory BaseDefinitions} |> Proof_Context.init_global
|
Walther@60661
|
182 |
in
|
Walther@60661
|
183 |
ParseC.term_opt ctxt str |> the
|
Walther@60661
|
184 |
end;
|
walther@59953
|
185 |
val e_listReal = script_parse "[]::(real list)";
|
walther@59953
|
186 |
val e_listBool = script_parse "[]::(bool list)";
|
walther@59953
|
187 |
|
Walther@60478
|
188 |
(* revert split only for ts *)
|
walther@59953
|
189 |
fun join'''' (d, ts) =
|
walther@59953
|
190 |
if for_list d
|
walther@59953
|
191 |
then if TermC.is_list (hd ts)
|
walther@59953
|
192 |
then if for_fun d
|
walther@59953
|
193 |
then (hd ts) (* e.g. someList [1,3,2] *)
|
Walther@60766
|
194 |
else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b], see "type values"*)
|
walther@59953
|
195 |
else (hd ts) (* a variable or metavariable for a list *)
|
walther@59953
|
196 |
else (hd ts);
|
walther@59953
|
197 |
fun join (d, []) =
|
walther@59953
|
198 |
if for_real_list d
|
walther@59953
|
199 |
then (d $ e_listReal)
|
walther@59953
|
200 |
else if for_bool_list d then (d $ e_listBool) else d
|
walther@60265
|
201 |
| join (d, ts) =
|
walther@60265
|
202 |
case \<^try>\<open> d $ (join'''' (d, ts))\<close> of
|
walther@60265
|
203 |
SOME x => x
|
Walther@60678
|
204 |
| NONE => raise ERROR ("join: " ^ UnparseC.term (ContextC.for_ERROR ()) d ^ " $ " ^ UnparseC.term (ContextC.for_ERROR ()) (hd ts));
|
walther@59953
|
205 |
fun join' (d, []) =
|
walther@59953
|
206 |
if for_real_list d
|
walther@59953
|
207 |
then (d $ e_listReal)
|
walther@59953
|
208 |
else if for_bool_list d then (d $ e_listBool) else d
|
walther@60265
|
209 |
| join' (d, ts) =
|
walther@60265
|
210 |
case \<^try>\<open> d $ (join'''' (d, ts))\<close> of
|
walther@60265
|
211 |
SOME x => x
|
Walther@60678
|
212 |
| NONE => raise ERROR ("join': " ^ UnparseC.term (ContextC.for_ERROR ()) d ^ " $ " ^ UnparseC.term (ContextC.for_ERROR ()) (hd ts));
|
walther@59953
|
213 |
fun join''' (d, []) =
|
walther@59953
|
214 |
if for_real_list d
|
Walther@60678
|
215 |
then UnparseC.term (ContextC.for_ERROR ()) (d $ e_listReal)
|
walther@59953
|
216 |
else if for_bool_list d
|
Walther@60678
|
217 |
then UnparseC.term (ContextC.for_ERROR ()) (d $ e_listBool)
|
Walther@60678
|
218 |
else UnparseC.term (ContextC.for_ERROR ()) d
|
walther@60265
|
219 |
| join''' (d, ts) =
|
Walther@60678
|
220 |
case \<^try>\<open> UnparseC.term (ContextC.for_ERROR ()) (d $ (join'''' (d, ts)))\<close> of
|
walther@60265
|
221 |
SOME x => x
|
Walther@60678
|
222 |
| NONE => raise ERROR ("join''': " ^ UnparseC.term (ContextC.for_ERROR ()) d ^ " $ " ^ UnparseC.term (ContextC.for_ERROR ()) (hd ts));
|
wneuper@59599
|
223 |
|
wneuper@59595
|
224 |
(**)end(**)
|
wneuper@59595
|
225 |
\<close> ML \<open>
|
wneuper@59595
|
226 |
\<close> ML \<open>
|
wneuper@59595
|
227 |
\<close>
|
wneuper@59595
|
228 |
|
wneuper@59599
|
229 |
end
|