1 (* Title: collect all defitions for the Lucas-Interpreter
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
5 Descriptors for interactive input into a Specification of an Example.
7 Since PblObj.ctxt records explicit type constraints in Formalise.model,
8 and since we have Model_Pattern.adapt_to_type,
9 the types of the descriptors below can be more relaxed.
12 theory Input_Descript imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
15 subsection \<open>typedecl for descriptors of input in specify-phase\<close>
17 The typedecl below MUST ALL be registered in "Input_Descript.is_a"
19 typedecl nam (* named variables *)
20 typedecl una (* unnamed variables *)
21 typedecl unl (* unnamed variables of type list, elementwise input prohibited*)
22 typedecl str (* structured variables *)
23 typedecl toreal (* var with undef real value: forces typing *)
24 typedecl toreall (* var with undef real list value: forces typing *)
25 typedecl tobooll (* var with undef bool list value: forces typing *)
26 typedecl unknow (* input without dsc in fmz=[] *)
27 typedecl cpy (* copy-named variables identified by .._0, .._i .._' in pbt *)
29 subsection \<open>consts for general descriptors of input in the specify-phase\<close>
32 (*TODO.180331: review for localisation of model-patterns and of method's guards*)
33 someList :: "'a list => unl" (*not for elementwise input, eg. inssort*)
35 additionalRels :: "bool list => una"
36 boundVariable :: "real => una"
37 FunctionVariable :: "real => una"
38 derivative :: "real => una"
39 equalities :: "bool list => tobooll" (*WN071228 see fixedValues*)
40 equality :: "bool => una"
41 errorBound :: "bool => nam"
42 ErrorBound :: "bool => nam"
44 fixedValues :: "bool list => nam"
45 Constants :: "bool list => nam"
46 functionEq :: "bool => una" (*6.5.03: functionTerm -> functionEq*)
47 antiDerivative :: "bool => una"
48 functionOf :: "real => una"
49 (*functionTerm :: 'a => toreal 28.11.00*)
50 functionTerm :: "real => una" (*6.5.03: functionTerm -> functionEq*)
51 functionName :: "real => una"
52 interval :: "real set => una"
53 Domain :: "real set => una"
54 maxArgument :: "bool => toreal"
55 maximum :: "real => toreal"
56 Maximum :: "real => toreal"
57 Extremum :: "bool => toreal"
59 relations :: "bool list => una"
60 SideConditions :: "bool list => una"
61 solutions :: "bool list => toreall"
62 solveFor :: "real => una"
63 differentiateFor:: "real => una"
64 unknown :: "'a => unknow"
65 valuesFor :: "real list => toreall"
66 AdditionalValues :: "real list => toreall"
68 intTestGiven :: "int => una"
69 realTestGiven :: "real => una"
70 realTestFind :: "real => una"
71 boolTestGiven :: "bool => una"
72 boolTestFind :: "bool => una"
74 subsection \<open>Functions decking for descriptions of input in specify-phase\<close>
77 signature INPUT_DESCRIPT =
79 (*type T ..TODO rename*)
82 val for_real_list: term -> bool
83 val for_list: term -> bool
85 val for_bool_list: term -> bool
86 val for_fun: term -> bool
87 val is_a: term -> bool
89 val split: term -> descriptor * term list
90 val split': term * term -> term list
91 val join: descriptor * term list -> term
92 val join': descriptor * term list -> term
93 val join''': descriptor * term list -> string
94 val join'''': descriptor * term list -> term
100 structure Input_Descript(**): INPUT_DESCRIPT =(**)
104 type descriptor = term; (*see Model_Def.descriptor*)
106 (* distinguish input to Model (deep embedding of terms as Isac's object language) *)
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
108 | for_real_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>real\<close>, [])]),_])) $ _) = true
109 | for_real_list _ = false;
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
111 | for_bool_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>, [])]),_])) $ _) = true
112 | for_bool_list _ = false;
113 fun for_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, _), _]))) = true
114 | for_list (Const (_, Type(\<^type_name>\<open>fun\<close>, [Type(\<^type_name>\<open>list\<close>, _), _])) $ _) = true
115 (*WN:8.5.03: ??? TODO test/../scrtools.sml ~~~~ ???*)
116 | for_list _ = false;
117 fun for_fun (Const (_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>unl\<close>, _)]))) = true
119 fun is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>nam\<close>, _)]))) = true
120 | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>una\<close>, _)]))) = true
121 | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>unl\<close>, _)]))) = true
122 | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>str\<close>, _)]))) = true
123 | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>toreal\<close>, _)]))) = true
124 | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>toreall\<close>, _)])))= true
125 | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>tobooll\<close>, _)])))= true
126 | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>unknow\<close>, _)])))= true
127 | is_a (Const(_, Type(\<^type_name>\<open>fun\<close>, [_, Type(\<^type_name>\<open>cpy\<close>, _)])))= true
130 (* special handling for lists. ?WN:14.5.03 ??!? *)
131 fun dest_list (d, ts) =
133 if for_list d andalso not (for_fun d) andalso not (is_Free t) (*..for pbt*)
134 then TermC.isalist2list t
136 in (flat o (map dest)) ts end;
138 (* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]", "[b]"] *)
140 let val elems = TermC.isalist2list t
141 in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
143 (* decompose an input into description, terms (ev. elems of lists),
144 and the value for the problem-environment; inv to join *)
145 fun split (t as d $ arg) =
147 then if for_list d andalso TermC.is_list arg andalso for_fun d |> not
148 then (d, take_apart arg)
150 else (TermC.empty, TermC.dest_list' t)
152 let val t' as (h, _) = strip_comb t;
155 then (h, dest_list t')
156 else (TermC.empty, TermC.dest_list' t)
159 (* version returning ts only *)
160 fun split' (d, arg) =
163 then if TermC.is_list arg
165 then ([arg]) (* e.g. someList [1,3,2] *)
166 else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
167 else ([arg]) (* a variable or metavariable for a list *)
169 else (TermC.dest_list' arg)
172 take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]", "[b]"]
173 take_apart_inv: term list -> term
175 fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
176 let val elems = (flat o (map TermC.isalist2list)) ts;
177 in TermC.list2isalist (type_of (hd elems)) elems end;
179 fun script_parse str =
181 val ctxt = @{theory BaseDefinitions} |> Proof_Context.init_global
183 ParseC.term_opt ctxt str |> the
185 val e_listReal = script_parse "[]::(real list)";
186 val e_listBool = script_parse "[]::(bool list)";
188 (* revert split only for ts *)
189 fun join'''' (d, ts) =
191 then if TermC.is_list (hd ts)
193 then (hd ts) (* e.g. someList [1,3,2] *)
194 else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b], see "type values"*)
195 else (hd ts) (* a variable or metavariable for a list *)
199 then (d $ e_listReal)
200 else if for_bool_list d then (d $ e_listBool) else d
202 case \<^try>\<open> d $ (join'''' (d, ts))\<close> of
204 | NONE => raise ERROR ("join: " ^ UnparseC.term (ContextC.for_ERROR ()) d ^ " $ " ^ UnparseC.term (ContextC.for_ERROR ()) (hd ts));
207 then (d $ e_listReal)
208 else if for_bool_list d then (d $ e_listBool) else d
210 case \<^try>\<open> d $ (join'''' (d, ts))\<close> of
212 | NONE => raise ERROR ("join': " ^ UnparseC.term (ContextC.for_ERROR ()) d ^ " $ " ^ UnparseC.term (ContextC.for_ERROR ()) (hd ts));
213 fun join''' (d, []) =
215 then UnparseC.term (ContextC.for_ERROR ()) (d $ e_listReal)
216 else if for_bool_list d
217 then UnparseC.term (ContextC.for_ERROR ()) (d $ e_listBool)
218 else UnparseC.term (ContextC.for_ERROR ()) d
220 case \<^try>\<open> UnparseC.term (ContextC.for_ERROR ()) (d $ (join'''' (d, ts)))\<close> of
222 | NONE => raise ERROR ("join''': " ^ UnparseC.term (ContextC.for_ERROR ()) d ^ " $ " ^ UnparseC.term (ContextC.for_ERROR ()) (hd ts));