prefer symbolic directories $ISABELLE_ISAC and $ISABELLE_ISAC_TEST, instead of re-using ~~ for $ISABELLE_HOME;
1 (* Title: collect all defitions for the Lucas-Interpreter
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
5 Descriptors for input into an I_Model.
6 Since PblObj.ctxt records explicit type constraints in Formalise.model,
7 the types of the descriptors below can be more relaxed.
10 theory Input_Descript imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
13 subsection \<open>typedecl for descriptors of input in specify-phase\<close>
15 The typedecl below MUST ALL be registered in "Input_Descript.is_a"
17 typedecl nam (* named variables *)
18 typedecl una (* unnamed variables *)
19 typedecl unl (* unnamed variables of type list, elementwise input prohibited*)
20 typedecl str (* structured variables *)
21 typedecl toreal (* var with undef real value: forces typing *)
22 typedecl toreall (* var with undef real list value: forces typing *)
23 typedecl tobooll (* var with undef bool list value: forces typing *)
24 typedecl unknow (* input without dsc in fmz=[] *)
25 typedecl cpy (* copy-named variables identified by .._0, .._i .._' in pbt *)
27 subsection \<open>consts for general descriptors of input in the specify-phase\<close>
30 (*TODO.180331: review for localisation of model-patterns and of method's guards*)
31 someList :: "'a list => unl" (*not for elementwise input, eg. inssort*)
33 additionalRels :: "bool list => una"
34 boundVariable :: "real => una"
35 derivative :: "real => una"
36 equalities :: "bool list => tobooll" (*WN071228 see fixedValues*)
37 equality :: "bool => una"
38 errorBound :: "bool => nam"
40 fixedValues :: "bool list => nam"
41 functionEq :: "bool => una" (*6.5.03: functionTerm -> functionEq*)
42 antiDerivative :: "bool => una"
43 functionOf :: "real => una"
44 (*functionTerm :: 'a => toreal 28.11.00*)
45 functionTerm :: "real => una" (*6.5.03: functionTerm -> functionEq*)
46 functionName :: "real => una"
47 interval :: "real set => una"
48 maxArgument :: "bool => toreal"
49 maximum :: "real => toreal"
51 relations :: "bool list => una"
52 solutions :: "bool list => toreall"
53 (*solution :: bool => toreal WN0509 bool list=> toreall --->EqSystem*)
54 solveFor :: "real => una"
55 differentiateFor:: "real => una"
56 unknown :: "'a => unknow"
57 valuesFor :: "real list => toreall"
59 intTestGiven :: "int => una"
60 realTestGiven :: "real => una"
61 realTestFind :: "real => una"
62 boolTestGiven :: "bool => una"
63 boolTestFind :: "bool => una"
65 subsection \<open>Functions decking for descriptions of input in specify-phase\<close>
68 signature INPUT_DESCRIPT =
70 (*type T ..TODO rename*)
71 type descriptor = Model_Pattern.descriptor
73 val for_list: term -> bool
75 val split: term -> descriptor * term list
76 val split': term * term -> term list
77 val join: descriptor * term list -> term
78 val join': descriptor * term list -> term
79 val join''': descriptor * term list -> string
80 val join'''': descriptor * term list -> term
82 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
83 val for_real_list: term -> bool
84 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
85 val is_a: term -> bool
86 val for_bool_list: term -> bool
87 val for_fun: term -> bool
88 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
94 structure Input_Descript(**): INPUT_DESCRIPT =(**)
98 type descriptor = Model_Pattern.descriptor;
100 (* distinguish input to Model (deep embedding of terms as Isac's object language) *)
101 fun for_real_list (Const (_, Type("fun", [Type ("List.list", [Type ("Real.real", [])]), _]))) = true
102 | for_real_list (Const (_, Type("fun", [Type ("List.list", [Type ("Real.real", [])]),_])) $ _) = true
103 | for_real_list _ = false;
104 fun for_bool_list (Const (_, Type("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _]))) = true
105 | for_bool_list (Const (_, Type("fun", [Type ("List.list", [Type ("HOL.bool", [])]),_])) $ _) = true
106 | for_bool_list _ = false;
107 fun for_list (Const (_, Type("fun", [Type("List.list", _), _]))) = true
108 | for_list (Const (_, Type("fun", [Type("List.list", _), _])) $ _) = true
109 (*WN:8.5.03: ??? TODO test/../scrtools.sml ~~~~ ???*)
110 | for_list _ = false;
111 fun for_fun (Const (_, Type("fun", [_, Type("Input_Descript.unl", _)]))) = true
113 fun is_a (Const(_, Type("fun", [_, Type ("Input_Descript.nam",_)]))) = true
114 | is_a (Const(_, Type("fun", [_, Type ("Input_Descript.una",_)]))) = true
115 | is_a (Const(_, Type("fun", [_, Type ("Input_Descript.unl",_)]))) = true
116 | is_a (Const(_, Type("fun", [_, Type ("Input_Descript.str",_)]))) = true
117 | is_a (Const(_, Type("fun", [_, Type ("Input_Descript.toreal",_)]))) = true
118 | is_a (Const(_, Type("fun", [_, Type ("Input_Descript.toreall",_)])))= true
119 | is_a (Const(_, Type("fun", [_, Type ("Input_Descript.tobooll",_)])))= true
120 | is_a (Const(_, Type("fun", [_, Type ("Input_Descript.unknow",_)])))= true
121 | is_a (Const(_, Type("fun", [_, Type ("Input_Descript.cpy",_)])))= true
124 (* special handling for lists. ?WN:14.5.03 ??!? *)
125 fun dest_list (d, ts) =
127 if for_list d andalso not (for_fun d) andalso not (is_Free t) (*..for pbt*)
128 then TermC.isalist2list t
130 in (flat o (map dest)) ts end;
132 (* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]", "[b]"] *)
134 let val elems = TermC.isalist2list t
135 in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
137 (* decompose an input into description, terms (ev. elems of lists),
138 and the value for the problem-environment; inv to join *)
139 fun split (t as d $ arg) =
141 then if for_list d andalso TermC.is_list arg andalso for_fun d |> not
142 then (d, take_apart arg)
144 else (TermC.empty, TermC.dest_list' t)
146 let val t' as (h, _) = strip_comb t;
149 then (h, dest_list t')
150 else (TermC.empty, TermC.dest_list' t)
153 (* version returning ts only *)
154 fun split' (d, arg) =
157 then if TermC.is_list arg
159 then ([arg]) (* e.g. someList [1,3,2] *)
160 else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
161 else ([arg]) (* a variable or metavariable for a list *)
163 else (TermC.dest_list' arg)
165 (* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]", "[b]"] *)
166 fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
167 let val elems = (flat o (map TermC.isalist2list)) ts;
168 in TermC.list2isalist (type_of (hd elems)) elems end;
170 val script_parse = the o (@{theory BaseDefinitions} |> ThyC.to_ctxt |> TermC.parseNEW);
171 val e_listReal = script_parse "[]::(real list)";
172 val e_listBool = script_parse "[]::(bool list)";
174 (* revert split only for ts; jcompare join *)
175 fun join'''' (d, ts) =
177 then if TermC.is_list (hd ts)
179 then (hd ts) (* e.g. someList [1,3,2] *)
180 else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *)
181 else (hd ts) (* a variable or metavariable for a list *)
185 then (d $ e_listReal)
186 else if for_bool_list d then (d $ e_listBool) else d
187 | join (d, ts) = (d $ (join'''' (d, ts)))
188 handle _ => raise ERROR ("join: " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
191 then (d $ e_listReal)
192 else if for_bool_list d then (d $ e_listBool) else d
193 | join' (d, ts) = (d $ (join'''' (d, ts)))
194 handle _ => raise ERROR ("join': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
195 fun join''' (d, []) =
197 then UnparseC.term (d $ e_listReal)
198 else if for_bool_list d
199 then UnparseC.term (d $ e_listBool)
201 | join''' (d, ts) = UnparseC.term (d $ (join'''' (d, ts)))
202 handle _ => raise ERROR ("join''': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));