author | haftmann |
Thu, 03 Aug 2017 12:50:00 +0200 | |
changeset 66328 | cf9ce8016da1 |
parent 66324 | 859b66d75dff |
child 66329 | a0369be63948 |
permissions | -rw-r--r-- |
24219 | 1 |
(* Title: Pure/Isar/code.ML |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
||
34173
458ced35abb8
reduced code generator cache to the baremost minimum
haftmann
parents:
33977
diff
changeset
|
4 |
Abstract executable ingredients of theory. Management of data |
458ced35abb8
reduced code generator cache to the baremost minimum
haftmann
parents:
33977
diff
changeset
|
5 |
dependent on executable ingredients as synchronized cache; purged |
458ced35abb8
reduced code generator cache to the baremost minimum
haftmann
parents:
33977
diff
changeset
|
6 |
on any change of underlying executable ingredients. |
24219 | 7 |
*) |
8 |
||
9 |
signature CODE = |
|
10 |
sig |
|
31957 | 11 |
(*constants*) |
12 |
val check_const: theory -> term -> string |
|
13 |
val read_const: theory -> string -> string |
|
31962 | 14 |
val string_of_const: theory -> string -> string |
15 |
val args_number: theory -> string -> int |
|
31957 | 16 |
|
31156 | 17 |
(*constructor sets*) |
18 |
val constrset_of_consts: theory -> (string * typ) list |
|
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset
|
19 |
-> string * ((string * sort) list * (string * ((string * sort) list * typ list)) list) |
31156 | 20 |
|
34874 | 21 |
(*code equations and certificates*) |
31156 | 22 |
val assert_eqn: theory -> thm * bool -> thm * bool |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
23 |
val assert_abs_eqn: theory -> string option -> thm -> thm * (string * string) |
34895 | 24 |
type cert |
34874 | 25 |
val constrain_cert: theory -> sort list -> cert -> cert |
49971
8b50286c36d3
close code theorems explicitly after preprocessing
haftmann
parents:
49904
diff
changeset
|
26 |
val conclude_cert: cert -> cert |
35226 | 27 |
val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list |
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
28 |
val equations_of_cert: theory -> cert -> ((string * sort) list * typ) |
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
29 |
* (((term * string option) list * (term * string option)) * (thm option * bool)) list option |
34895 | 30 |
val pretty_cert: theory -> cert -> Pretty.T list |
31156 | 31 |
|
31962 | 32 |
(*executable code*) |
66328 | 33 |
type constructors |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
34 |
val declare_datatype_global: (string * typ) list -> theory -> theory |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
35 |
val declare_datatype_cmd: string list -> theory -> theory |
66328 | 36 |
val datatype_interpretation: (string * constructors -> theory -> theory) -> theory -> theory |
37 |
type abs_type |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
38 |
val declare_abstype: thm -> local_theory -> local_theory |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
39 |
val declare_abstype_global: thm -> theory -> theory |
66328 | 40 |
val abstype_interpretation: (string * abs_type -> theory -> theory) -> theory -> theory |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
41 |
val declare_default_eqns: (thm * bool) list -> local_theory -> local_theory |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
42 |
val declare_default_eqns_global: (thm * bool) list -> theory -> theory |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
43 |
val declare_eqns: (thm * bool) list -> local_theory -> local_theory |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
44 |
val declare_eqns_global: (thm * bool) list -> theory -> theory |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
45 |
val add_eqn_global: thm * bool -> theory -> theory |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
46 |
val del_eqn_global: thm -> theory -> theory |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
47 |
val declare_abstract_eqn: thm -> local_theory -> local_theory |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
48 |
val declare_abstract_eqn_global: thm -> theory -> theory |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
49 |
val declare_aborting_global: string -> theory -> theory |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
50 |
val declare_unimplemented_global: string -> theory -> theory |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
51 |
val declare_case_global: thm -> theory -> theory |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
52 |
val declare_undefined_global: string -> theory -> theory |
66328 | 53 |
val get_type: theory -> string -> constructors * bool |
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset
|
54 |
val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option |
35226 | 55 |
val is_constr: theory -> string -> bool |
56 |
val is_abstr: theory -> string -> bool |
|
57429 | 57 |
val get_cert: Proof.context -> ((thm * bool) list -> (thm * bool) list option) list |
58 |
-> string -> cert |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
59 |
type case_schema |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
60 |
val get_case_schema: theory -> string -> case_schema option |
37438 | 61 |
val get_case_cong: theory -> string -> thm option |
66189
23917e861eaa
treat "undefined" constants internally as special form of case combinators
haftmann
parents:
66167
diff
changeset
|
62 |
val is_undefined: theory -> string -> bool |
24219 | 63 |
val print_codesetup: theory -> unit |
64 |
end; |
|
65 |
||
66 |
signature CODE_DATA_ARGS = |
|
67 |
sig |
|
68 |
type T |
|
69 |
val empty: T |
|
70 |
end; |
|
71 |
||
72 |
signature CODE_DATA = |
|
73 |
sig |
|
74 |
type T |
|
39397 | 75 |
val change: theory option -> (T -> T) -> T |
76 |
val change_yield: theory option -> (T -> 'a * T) -> 'a * T |
|
24219 | 77 |
end; |
78 |
||
79 |
signature PRIVATE_CODE = |
|
80 |
sig |
|
81 |
include CODE |
|
51368
2ea5c7c2d825
tuned signature -- prefer terminology of Scala and Axiom;
wenzelm
parents:
49971
diff
changeset
|
82 |
val declare_data: Any.T -> serial |
2ea5c7c2d825
tuned signature -- prefer terminology of Scala and Axiom;
wenzelm
parents:
49971
diff
changeset
|
83 |
val change_yield_data: serial * ('a -> Any.T) * (Any.T -> 'a) |
34251 | 84 |
-> theory -> ('a -> 'b * 'a) -> 'b * 'a |
24219 | 85 |
end; |
86 |
||
87 |
structure Code : PRIVATE_CODE = |
|
88 |
struct |
|
89 |
||
31962 | 90 |
(** auxiliary **) |
91 |
||
92 |
(* printing *) |
|
31156 | 93 |
|
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39020
diff
changeset
|
94 |
fun string_of_typ thy = |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39020
diff
changeset
|
95 |
Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy)); |
31962 | 96 |
|
42359 | 97 |
fun string_of_const thy c = |
42360 | 98 |
let val ctxt = Proof_Context.init_global thy in |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset
|
99 |
case Axclass.inst_of_param thy c of |
42359 | 100 |
SOME (c, tyco) => |
42360 | 101 |
Proof_Context.extern_const ctxt c ^ " " ^ enclose "[" "]" |
102 |
(Proof_Context.extern_type ctxt tyco) |
|
103 |
| NONE => Proof_Context.extern_const ctxt c |
|
42359 | 104 |
end; |
31156 | 105 |
|
31962 | 106 |
|
107 |
(* constants *) |
|
31156 | 108 |
|
49534
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
109 |
fun const_typ thy = Type.strip_sorts o Sign.the_const_type thy; |
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
110 |
|
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
111 |
fun args_number thy = length o binder_types o const_typ thy; |
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
112 |
|
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
113 |
fun devarify ty = |
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
114 |
let |
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
115 |
val tys = fold_atyps (fn TVar vi_sort => AList.update (op =) vi_sort) ty []; |
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
116 |
val vs = Name.invent Name.context Name.aT (length tys); |
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
117 |
val mapping = map2 (fn v => fn (vi, sort) => (vi, TFree (v, sort))) vs tys; |
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
118 |
in Term.typ_subst_TVars mapping ty end; |
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
119 |
|
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
120 |
fun typscheme thy (c, ty) = |
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
121 |
(map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty); |
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
122 |
|
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
123 |
fun typscheme_equiv (ty1, ty2) = |
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
124 |
Type.raw_instance (devarify ty1, ty2) andalso Type.raw_instance (devarify ty2, ty1); |
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
125 |
|
31962 | 126 |
fun check_bare_const thy t = case try dest_Const t |
127 |
of SOME c_ty => c_ty |
|
128 |
| NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t); |
|
31156 | 129 |
|
40362
82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset
|
130 |
fun check_unoverload thy (c, ty) = |
82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset
|
131 |
let |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset
|
132 |
val c' = Axclass.unoverload_const thy (c, ty); |
54604
1512fa5fe531
prefer sort-stripping const_typ over Sign.the_const_type whenever appropriate
haftmann
parents:
54603
diff
changeset
|
133 |
val ty_decl = const_typ thy c'; |
45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
134 |
in |
49534
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
135 |
if typscheme_equiv (ty_decl, Logic.varifyT_global ty) |
45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
136 |
then c' |
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
137 |
else |
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
138 |
error ("Type\n" ^ string_of_typ thy ty ^ |
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
139 |
"\nof constant " ^ quote c ^ |
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
140 |
"\nis too specific compared to declared type\n" ^ |
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
141 |
string_of_typ thy ty_decl) |
66167 | 142 |
end; |
40362
82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset
|
143 |
|
82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset
|
144 |
fun check_const thy = check_unoverload thy o check_bare_const thy; |
31962 | 145 |
|
146 |
fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy; |
|
147 |
||
40362
82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset
|
148 |
fun read_const thy = check_unoverload thy o read_bare_const thy; |
31156 | 149 |
|
32872
019201eb7e07
variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents:
32738
diff
changeset
|
150 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
151 |
(** executable specifications **) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
152 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
153 |
(* types *) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
154 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
155 |
datatype type_spec = Constructors of { |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
156 |
constructors: (string * ((string * sort) list * typ list)) list, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
157 |
case_combinators: string list} |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
158 |
| Abstractor of { |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
159 |
abs_rep: thm, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
160 |
abstractor: string * ((string * sort) list * typ), |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
161 |
projection: string, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
162 |
more_abstract_functions: string list}; |
31962 | 163 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
164 |
fun concrete_constructors_of (Constructors {constructors, ...}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
165 |
constructors |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
166 |
| concrete_constructors_of _ = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
167 |
[]; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
168 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
169 |
fun constructors_of (Constructors {constructors, ...}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
170 |
(constructors, false) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
171 |
| constructors_of (Abstractor {abstractor = (co, (vs, ty)), ...}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
172 |
([(co, (vs, [ty]))], true); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
173 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
174 |
fun case_combinators_of (Constructors {case_combinators, ...}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
175 |
case_combinators |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
176 |
| case_combinators_of (Abstractor _) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
177 |
[]; |
35226 | 178 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
179 |
fun add_case_combinator c (vs, Constructors {constructors, case_combinators}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
180 |
(vs, Constructors {constructors = constructors, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
181 |
case_combinators = insert (op =) c case_combinators}); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
182 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
183 |
fun projection_of (Constructors _) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
184 |
NONE |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
185 |
| projection_of (Abstractor {projection, ...}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
186 |
SOME projection; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
187 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
188 |
fun abstract_functions_of (Constructors _) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
189 |
[] |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
190 |
| abstract_functions_of (Abstractor {more_abstract_functions, projection, ...}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
191 |
projection :: more_abstract_functions; |
31962 | 192 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
193 |
fun add_abstract_function c (vs, Abstractor {abs_rep, abstractor, projection, more_abstract_functions}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
194 |
(vs, Abstractor {abs_rep = abs_rep, abstractor = abstractor, projection = projection, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
195 |
more_abstract_functions = insert (op =) c more_abstract_functions}); |
35226 | 196 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
197 |
fun join_same_types' (Constructors {constructors, case_combinators = case_combinators1}, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
198 |
Constructors {case_combinators = case_combinators2, ...}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
199 |
Constructors {constructors = constructors, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
200 |
case_combinators = merge (op =) (case_combinators1, case_combinators2)} |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
201 |
| join_same_types' (Abstractor {abs_rep, abstractor, projection, more_abstract_functions = more_abstract_functions1}, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
202 |
Abstractor {more_abstract_functions = more_abstract_functions2, ...}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
203 |
Abstractor {abs_rep = abs_rep, abstractor = abstractor, projection = projection, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
204 |
more_abstract_functions = merge (op =) (more_abstract_functions1, more_abstract_functions2)}; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
205 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
206 |
fun join_same_types ((vs, spec1), (_, spec2)) = (vs, join_same_types' (spec1, spec2)); |
35226 | 207 |
|
66125 | 208 |
|
35226 | 209 |
(* functions *) |
31962 | 210 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
211 |
datatype fun_spec = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
212 |
Eqns of bool * (thm * bool) list |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
213 |
| Proj of term * (string * string) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
214 |
| Abstr of thm * (string * string); |
31962 | 215 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
216 |
val unimplemented = Eqns (true, []); |
31962 | 217 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
218 |
fun is_unimplemented (Eqns (true, [])) = true |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
219 |
| is_unimplemented _ = false; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
220 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
221 |
fun is_default (Eqns (true, _)) = true |
35226 | 222 |
| is_default _ = false; |
223 |
||
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
224 |
val aborting = Eqns (false, []); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
225 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
226 |
fun associated_abstype (Proj (_, tyco_abs)) = SOME tyco_abs |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
227 |
| associated_abstype (Abstr (_, tyco_abs)) = SOME tyco_abs |
35226 | 228 |
| associated_abstype _ = NONE; |
31962 | 229 |
|
230 |
||
66189
23917e861eaa
treat "undefined" constants internally as special form of case combinators
haftmann
parents:
66167
diff
changeset
|
231 |
(* cases *) |
23917e861eaa
treat "undefined" constants internally as special form of case combinators
haftmann
parents:
66167
diff
changeset
|
232 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
233 |
type case_schema = int * (int * string option list); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
234 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
235 |
datatype case_spec = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
236 |
No_Case |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
237 |
| Case of {schema: case_schema, tycos: string list, cong: thm} |
66189
23917e861eaa
treat "undefined" constants internally as special form of case combinators
haftmann
parents:
66167
diff
changeset
|
238 |
| Undefined; |
23917e861eaa
treat "undefined" constants internally as special form of case combinators
haftmann
parents:
66167
diff
changeset
|
239 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
240 |
fun associated_datatypes (Case {tycos, schema = (_, (_, raw_cos)), ...}) = (tycos, map_filter I raw_cos) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
241 |
| associated_datatypes _ = ([], []); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
242 |
|
66189
23917e861eaa
treat "undefined" constants internally as special form of case combinators
haftmann
parents:
66167
diff
changeset
|
243 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
244 |
(** background theory data store **) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
245 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
246 |
(* historized declaration data *) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
247 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
248 |
structure History = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
249 |
struct |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
250 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
251 |
type 'a T = { |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
252 |
entry: 'a, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
253 |
suppressed: bool, (*incompatible entries are merely suppressed after theory merge but sustain*) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
254 |
history: serial list (*explicit trace of declaration history supports non-monotonic declarations*) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
255 |
} Symtab.table; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
256 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
257 |
fun some_entry (SOME {suppressed = false, entry, ...}) = SOME entry |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
258 |
| some_entry _ = NONE; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
259 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
260 |
fun lookup table = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
261 |
Symtab.lookup table #> some_entry; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
262 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
263 |
fun register key entry table = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
264 |
if is_some (Symtab.lookup table key) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
265 |
then Symtab.map_entry key |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
266 |
(fn {history, ...} => {entry = entry, suppressed = false, history = serial () :: history}) table |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
267 |
else Symtab.update (key, {entry = entry, suppressed = false, history = [serial ()]}) table; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
268 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
269 |
fun modify_entry key f = Symtab.map_entry key |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
270 |
(fn {entry, suppressed, history} => {entry = f entry, suppressed = suppressed, history = history}); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
271 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
272 |
fun all table = Symtab.dest table |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
273 |
|> map_filter (fn (key, {entry, suppressed = false, ...}) => SOME (key, entry) | _ => NONE); |
31962 | 274 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
275 |
local |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
276 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
277 |
fun merge_history join_same |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
278 |
({entry = entry1, history = history1, ...}, {entry = entry2, history = history2, ...}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
279 |
let |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
280 |
val history = merge (op =) (history1, history2); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
281 |
val entry = if hd history1 = hd history2 then join_same (entry1, entry2) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
282 |
else if hd history = hd history1 then entry1 else entry2; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
283 |
in {entry = entry, suppressed = false, history = history} end; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
284 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
285 |
in |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
286 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
287 |
fun join join_same tables = Symtab.join (K (merge_history join_same)) tables; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
288 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
289 |
fun suppress key = Symtab.map_entry key |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
290 |
(fn {entry, history, ...} => {entry = entry, suppressed = true, history = history}); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
291 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
292 |
fun suppress_except f = Symtab.map (fn key => fn {entry, suppressed, history} => |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
293 |
{entry = entry, suppressed = suppressed orelse (not o f) (key, entry), history = history}); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
294 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
295 |
end; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
296 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
297 |
end; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
298 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
299 |
datatype specs = Specs of { |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
300 |
types: ((string * sort) list * type_spec) History.T, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
301 |
pending_eqns: (thm * bool) list Symtab.table, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
302 |
functions: fun_spec History.T, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
303 |
cases: case_spec History.T |
31962 | 304 |
}; |
305 |
||
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
306 |
fun types_of (Specs {types, ...}) = types; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
307 |
fun pending_eqns_of (Specs {pending_eqns, ...}) = pending_eqns; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
308 |
fun functions_of (Specs {functions, ...}) = functions; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
309 |
fun cases_of (Specs {cases, ...}) = cases; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
310 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
311 |
fun make_specs (types, ((pending_eqns, functions), cases)) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
312 |
Specs {types = types, pending_eqns = pending_eqns, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
313 |
functions = functions, cases = cases}; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
314 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
315 |
val empty_specs = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
316 |
make_specs (Symtab.empty, ((Symtab.empty, Symtab.empty), Symtab.empty)); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
317 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
318 |
fun map_specs f (Specs {types = types, pending_eqns = pending_eqns, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
319 |
functions = functions, cases = cases}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
320 |
make_specs (f (types, ((pending_eqns, functions), cases))); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
321 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
322 |
fun merge_specs (Specs {types = types1, pending_eqns = _, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
323 |
functions = functions1, cases = cases1}, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
324 |
Specs {types = types2, pending_eqns = _, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
325 |
functions = functions2, cases = cases2}) = |
31156 | 326 |
let |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
327 |
val types = History.join join_same_types (types1, types2); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
328 |
val all_types = map (snd o snd) (History.all types); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
329 |
fun check_abstype (c, fun_spec) = case associated_abstype fun_spec of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
330 |
NONE => true |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
331 |
| SOME (tyco, abs) => (case History.lookup types tyco of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
332 |
NONE => false |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
333 |
| SOME (_, Abstractor {abstractor = (abs', _), projection, more_abstract_functions, ...}) => |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
334 |
abs = abs' andalso (c = projection orelse member (op =) more_abstract_functions c)); |
66324 | 335 |
fun check_datatypes (_, case_spec) = |
31962 | 336 |
let |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
337 |
val (tycos, required_constructors) = associated_datatypes case_spec; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
338 |
val allowed_constructors = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
339 |
tycos |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
340 |
|> maps (these o Option.map (concrete_constructors_of o snd) o History.lookup types) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
341 |
|> map fst; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
342 |
in subset (op =) (required_constructors, allowed_constructors) end; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
343 |
val all_constructors = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
344 |
maps (fst o constructors_of) all_types; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
345 |
val functions = History.join fst (functions1, functions2) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
346 |
|> fold (History.suppress o fst) all_constructors |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
347 |
|> History.suppress_except check_abstype; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
348 |
val cases = History.join fst (cases1, cases2) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
349 |
|> History.suppress_except check_datatypes; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
350 |
in make_specs (types, ((Symtab.empty, functions), cases)) end; |
31962 | 351 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
352 |
val map_types = map_specs o apfst; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
353 |
val map_pending_eqns = map_specs o apsnd o apfst o apfst; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
354 |
val map_functions = map_specs o apsnd o apfst o apsnd; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
355 |
val map_cases = map_specs o apsnd o apsnd; |
31962 | 356 |
|
357 |
||
358 |
(* data slots dependent on executable code *) |
|
359 |
||
360 |
(*private copy avoids potential conflict of table exceptions*) |
|
31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31962
diff
changeset
|
361 |
structure Datatab = Table(type key = int val ord = int_ord); |
31962 | 362 |
|
363 |
local |
|
364 |
||
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
365 |
type kind = {empty: Any.T}; |
31962 | 366 |
|
43684 | 367 |
val kinds = Synchronized.var "Code_Data" (Datatab.empty: kind Datatab.table); |
31962 | 368 |
|
43684 | 369 |
fun invoke f k = |
370 |
(case Datatab.lookup (Synchronized.value kinds) k of |
|
371 |
SOME kind => f kind |
|
372 |
| NONE => raise Fail "Invalid code data identifier"); |
|
31962 | 373 |
|
374 |
in |
|
375 |
||
34173
458ced35abb8
reduced code generator cache to the baremost minimum
haftmann
parents:
33977
diff
changeset
|
376 |
fun declare_data empty = |
31962 | 377 |
let |
378 |
val k = serial (); |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
379 |
val kind = {empty = empty}; |
43684 | 380 |
val _ = Synchronized.change kinds (Datatab.update (k, kind)); |
31962 | 381 |
in k end; |
382 |
||
383 |
fun invoke_init k = invoke (fn kind => #empty kind) k; |
|
384 |
||
385 |
end; (*local*) |
|
386 |
||
387 |
||
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
388 |
(* global theory store *) |
31962 | 389 |
|
390 |
local |
|
391 |
||
51368
2ea5c7c2d825
tuned signature -- prefer terminology of Scala and Axiom;
wenzelm
parents:
49971
diff
changeset
|
392 |
type data = Any.T Datatab.table; |
52788 | 393 |
fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory) option); |
31962 | 394 |
|
34244 | 395 |
structure Code_Data = Theory_Data |
31962 | 396 |
( |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
397 |
type T = specs * (data * theory) option Synchronized.var; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
398 |
val empty = (empty_specs, empty_dataref ()); |
49556 | 399 |
val extend : T -> T = apsnd (K (empty_dataref ())); |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
400 |
fun merge ((specs1, _), (specs2, _)) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
401 |
(merge_specs (specs1, specs2), empty_dataref ()); |
31962 | 402 |
); |
403 |
||
404 |
in |
|
405 |
||
35226 | 406 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
407 |
(* access to executable specifications *) |
31962 | 408 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
409 |
val specs_of : theory -> specs = fst o Code_Data.get; |
31962 | 410 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
411 |
fun modify_specs f = Code_Data.map (fn (specs, _) => (f specs, empty_dataref ())); |
31962 | 412 |
|
413 |
||
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
414 |
(* access to data dependent on executable specifications *) |
31962 | 415 |
|
34244 | 416 |
fun change_yield_data (kind, mk, dest) theory f = |
31962 | 417 |
let |
34244 | 418 |
val dataref = (snd o Code_Data.get) theory; |
52788 | 419 |
val (datatab, thy) = case Synchronized.value dataref |
420 |
of SOME (datatab, thy) => |
|
60948 | 421 |
if Context.eq_thy (theory, thy) |
52788 | 422 |
then (datatab, thy) |
423 |
else (Datatab.empty, theory) |
|
424 |
| NONE => (Datatab.empty, theory) |
|
34244 | 425 |
val data = case Datatab.lookup datatab kind |
426 |
of SOME data => data |
|
427 |
| NONE => invoke_init kind; |
|
40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset
|
428 |
val result as (_, data') = f (dest data); |
34244 | 429 |
val _ = Synchronized.change dataref |
52788 | 430 |
((K o SOME) (Datatab.update (kind, mk data') datatab, thy)); |
34244 | 431 |
in result end; |
31962 | 432 |
|
433 |
end; (*local*) |
|
434 |
||
435 |
||
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
436 |
(* pending function equations *) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
437 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
438 |
(* Ideally, *all* equations implementing a functions would be treated as |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
439 |
*one* atomic declaration; unfortunately, we cannot implement this: |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
440 |
the too-well-established declaration interface are Isar attributes |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
441 |
which operate on *one* single theorem. Hence we treat such Isar |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
442 |
declarations as "pending" and historize them as proper declarations |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
443 |
at the end of each theory. *) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
444 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
445 |
fun modify_pending_eqns c f specs = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
446 |
let |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
447 |
val existing_eqns = case History.lookup (functions_of specs) c of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
448 |
SOME (Eqns (false, eqns)) => eqns |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
449 |
| _ => []; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
450 |
in |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
451 |
specs |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
452 |
|> map_pending_eqns (Symtab.map_default (c, existing_eqns) f) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
453 |
end; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
454 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
455 |
fun register_fun_spec c spec = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
456 |
map_pending_eqns (Symtab.delete_safe c) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
457 |
#> map_functions (History.register c spec); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
458 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
459 |
fun lookup_fun_spec specs c = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
460 |
case Symtab.lookup (pending_eqns_of specs) c of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
461 |
SOME eqns => Eqns (false, eqns) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
462 |
| NONE => (case History.lookup (functions_of specs) c of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
463 |
SOME spec => spec |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
464 |
| NONE => unimplemented); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
465 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
466 |
fun lookup_proper_fun_spec specs c = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
467 |
let |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
468 |
val spec = lookup_fun_spec specs c |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
469 |
in |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
470 |
if is_unimplemented spec then NONE else SOME spec |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
471 |
end; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
472 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
473 |
fun all_fun_specs specs = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
474 |
map_filter (fn c => Option.map (pair c) (lookup_proper_fun_spec specs c)) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
475 |
(union (op =) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
476 |
((Symtab.keys o pending_eqns_of) specs) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
477 |
((Symtab.keys o functions_of) specs)); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
478 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
479 |
fun historize_pending_fun_specs thy = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
480 |
let |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
481 |
val pending_eqns = (pending_eqns_of o specs_of) thy; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
482 |
in if Symtab.is_empty pending_eqns |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
483 |
then |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
484 |
NONE |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
485 |
else |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
486 |
thy |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
487 |
|> modify_specs (map_functions |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
488 |
(Symtab.fold (fn (c, eqs) => History.register c (Eqns (false, eqs))) pending_eqns) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
489 |
#> map_pending_eqns (K Symtab.empty)) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
490 |
|> SOME |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
491 |
end; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
492 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
493 |
val _ = Theory.setup (Theory.at_end historize_pending_fun_specs); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
494 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
495 |
|
31962 | 496 |
(** foundation **) |
497 |
||
66128 | 498 |
(* types *) |
31156 | 499 |
|
35226 | 500 |
fun no_constr thy s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c |
501 |
^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s); |
|
502 |
||
45987 | 503 |
fun analyze_constructor thy (c, ty) = |
31156 | 504 |
let |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59458
diff
changeset
|
505 |
val _ = Thm.global_cterm_of thy (Const (c, ty)); |
54603
89d5b69e5a08
prefer name-normalizing devarify over unvarifyT whenever appropriate
haftmann
parents:
53171
diff
changeset
|
506 |
val ty_decl = devarify (const_typ thy c); |
31156 | 507 |
fun last_typ c_ty ty = |
508 |
let |
|
33531 | 509 |
val tfrees = Term.add_tfreesT ty []; |
40844 | 510 |
val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type ty)) |
35226 | 511 |
handle TYPE _ => no_constr thy "bad type" c_ty |
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset
|
512 |
val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else (); |
45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
513 |
val _ = |
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
514 |
if has_duplicates (eq_fst (op =)) vs |
35226 | 515 |
then no_constr thy "duplicate type variables in datatype" c_ty else (); |
45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
516 |
val _ = |
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
517 |
if length tfrees <> length vs |
35226 | 518 |
then no_constr thy "type variables missing in datatype" c_ty else (); |
31156 | 519 |
in (tyco, vs) end; |
35226 | 520 |
val (tyco, _) = last_typ (c, ty) ty_decl; |
521 |
val (_, vs) = last_typ (c, ty) ty; |
|
522 |
in ((tyco, map snd vs), (c, (map fst vs, ty))) end; |
|
523 |
||
49904
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
524 |
fun constrset_of_consts thy consts = |
35226 | 525 |
let |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset
|
526 |
val _ = map (fn (c, _) => if (is_some o Axclass.class_of_param thy) c |
49904
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
527 |
then error ("Is a class parameter: " ^ string_of_const thy c) else ()) consts; |
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
528 |
val raw_constructors = map (analyze_constructor thy) consts; |
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
529 |
val tyco = case distinct (op =) (map (fst o fst) raw_constructors) |
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
530 |
of [tyco] => tyco |
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
531 |
| [] => error "Empty constructor set" |
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
532 |
| tycos => error ("Different type constructors in constructor set: " ^ commas_quote tycos) |
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
533 |
val vs = Name.invent Name.context Name.aT (Sign.arity_number thy tyco); |
31156 | 534 |
fun inst vs' (c, (vs, ty)) = |
535 |
let |
|
536 |
val the_v = the o AList.lookup (op =) (vs ~~ vs'); |
|
49904
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
537 |
val ty' = map_type_tfree (fn (v, _) => TFree (the_v v, [])) ty; |
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
538 |
val (vs'', ty'') = typscheme thy (c, ty'); |
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
539 |
in (c, (vs'', binder_types ty'')) end; |
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
540 |
val constructors = map (inst vs o snd) raw_constructors; |
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset
|
541 |
in (tyco, (map (rpair []) vs, constructors)) end; |
31156 | 542 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
543 |
fun lookup_vs_type_spec thy = History.lookup ((types_of o specs_of) thy); |
31962 | 544 |
|
66328 | 545 |
type constructors = |
546 |
(string * sort) list * (string * ((string * sort) list * typ list)) list; |
|
547 |
||
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
548 |
fun get_type thy tyco = case lookup_vs_type_spec thy tyco |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
549 |
of SOME (vs, type_spec) => apfst (pair vs) (constructors_of type_spec) |
45987 | 550 |
| NONE => Sign.arity_number thy tyco |
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
551 |
|> Name.invent Name.context Name.aT |
35226 | 552 |
|> map (rpair []) |
553 |
|> rpair [] |
|
554 |
|> rpair false; |
|
555 |
||
66328 | 556 |
type abs_type = |
557 |
(string * sort) list * {abs_rep: thm, abstractor: string * ((string * sort) list * typ), projection: string}; |
|
558 |
||
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
559 |
fun get_abstype_spec thy tyco = case lookup_vs_type_spec thy tyco of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
560 |
SOME (vs, Abstractor {abs_rep, abstractor, projection, ...}) => |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
561 |
(vs, {abs_rep = abs_rep, abstractor = abstractor, projection = projection}) |
36122 | 562 |
| _ => error ("Not an abstract type: " ^ tyco); |
66167 | 563 |
|
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset
|
564 |
fun get_type_of_constr_or_abstr thy c = |
40844 | 565 |
case (body_type o const_typ thy) c |
40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset
|
566 |
of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco |
35226 | 567 |
in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end |
31962 | 568 |
| _ => NONE; |
569 |
||
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset
|
570 |
fun is_constr thy c = case get_type_of_constr_or_abstr thy c |
35226 | 571 |
of SOME (_, false) => true |
572 |
| _ => false; |
|
573 |
||
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset
|
574 |
fun is_abstr thy c = case get_type_of_constr_or_abstr thy c |
35226 | 575 |
of SOME (_, true) => true |
576 |
| _ => false; |
|
31962 | 577 |
|
31156 | 578 |
|
34874 | 579 |
(* bare code equations *) |
31156 | 580 |
|
35226 | 581 |
(* convention for variables: |
582 |
?x ?'a for free-floating theorems (e.g. in the data store) |
|
583 |
?x 'a for certificates |
|
584 |
x 'a for final representation of equations |
|
585 |
*) |
|
586 |
||
31156 | 587 |
exception BAD_THM of string; |
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
588 |
|
31156 | 589 |
fun bad_thm msg = raise BAD_THM msg; |
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
590 |
|
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
591 |
datatype strictness = Silent | Liberal | Strict |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
592 |
|
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
593 |
fun handle_strictness thm_of f strictness thy x = SOME (f x) |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
594 |
handle BAD_THM msg => case strictness of |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
595 |
Silent => NONE |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
596 |
| Liberal => (warning (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy (thm_of x)); NONE) |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
597 |
| Strict => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy (thm_of x)); |
31156 | 598 |
|
599 |
fun is_linear thm = |
|
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
600 |
let |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
601 |
val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
602 |
in |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
603 |
not (has_duplicates (op =) ((fold o fold_aterms) |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
604 |
(fn Var (v, _) => cons v | _ => I) args [])) |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
605 |
end; |
31156 | 606 |
|
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
607 |
fun check_decl_ty thy (c, ty) = |
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
608 |
let |
54604
1512fa5fe531
prefer sort-stripping const_typ over Sign.the_const_type whenever appropriate
haftmann
parents:
54603
diff
changeset
|
609 |
val ty_decl = const_typ thy c; |
49534
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
610 |
in if typscheme_equiv (ty_decl, ty) then () |
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
611 |
else bad_thm ("Type\n" ^ string_of_typ thy ty |
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
612 |
^ "\nof constant " ^ quote c |
40362
82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset
|
613 |
^ "\nis too specific compared to declared type\n" |
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
614 |
^ string_of_typ thy ty_decl) |
66167 | 615 |
end; |
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
616 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
617 |
fun check_eqn thy {allow_nonlinear, allow_consts, allow_pats} thm (lhs, rhs) = |
31156 | 618 |
let |
619 |
fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v |
|
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
620 |
| Free _ => bad_thm "Illegal free variable" |
31156 | 621 |
| _ => I) t []; |
622 |
fun tvars_of t = fold_term_types (fn _ => |
|
623 |
fold_atyps (fn TVar (v, _) => insert (op =) v |
|
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
624 |
| TFree _ => bad_thm "Illegal free type variable")) t []; |
31156 | 625 |
val lhs_vs = vars_of lhs; |
626 |
val rhs_vs = vars_of rhs; |
|
627 |
val lhs_tvs = tvars_of lhs; |
|
628 |
val rhs_tvs = tvars_of rhs; |
|
629 |
val _ = if null (subtract (op =) lhs_vs rhs_vs) |
|
630 |
then () |
|
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
631 |
else bad_thm "Free variables on right hand side of equation"; |
31156 | 632 |
val _ = if null (subtract (op =) lhs_tvs rhs_tvs) |
633 |
then () |
|
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
634 |
else bad_thm "Free type variables on right hand side of equation"; |
34894 | 635 |
val (head, args) = strip_comb lhs; |
31156 | 636 |
val (c, ty) = case head |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset
|
637 |
of Const (c_ty as (_, ty)) => (Axclass.unoverload_const thy c_ty, ty) |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
638 |
| _ => bad_thm "Equation not headed by constant"; |
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
639 |
fun check _ (Abs _) = bad_thm "Abstraction on left hand side of equation" |
31156 | 640 |
| check 0 (Var _) = () |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
641 |
| check _ (Var _) = bad_thm "Variable with application on left hand side of equation" |
31156 | 642 |
| check n (t1 $ t2) = (check (n+1) t1; check 0 t2) |
34894 | 643 |
| check n (Const (c_ty as (c, ty))) = |
35226 | 644 |
if allow_pats then let |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset
|
645 |
val c' = Axclass.unoverload_const thy c_ty |
45987 | 646 |
in if n = (length o binder_types) ty |
35226 | 647 |
then if allow_consts orelse is_constr thy c' |
33940
317933ce3712
crude support for type aliasses and corresponding constant signatures
haftmann
parents:
33756
diff
changeset
|
648 |
then () |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
649 |
else bad_thm (quote c ^ " is not a constructor, on left hand side of equation") |
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
650 |
else bad_thm ("Partially applied constant " ^ quote c ^ " on left hand side of equation") |
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
651 |
end else bad_thm ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side of equation") |
31156 | 652 |
val _ = map (check 0) args; |
35226 | 653 |
val _ = if allow_nonlinear orelse is_linear thm then () |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
654 |
else bad_thm "Duplicate variables on left hand side of equation"; |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset
|
655 |
val _ = if (is_none o Axclass.class_of_param thy) c then () |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
656 |
else bad_thm "Overloaded constant as head in equation"; |
34894 | 657 |
val _ = if not (is_constr thy c) then () |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
658 |
else bad_thm "Constructor as head in equation"; |
35226 | 659 |
val _ = if not (is_abstr thy c) then () |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
660 |
else bad_thm "Abstractor as head in equation"; |
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
661 |
val _ = check_decl_ty thy (c, ty); |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
662 |
val _ = case strip_type ty of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
663 |
(Type (tyco, _) :: _, _) => (case lookup_vs_type_spec thy tyco of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
664 |
SOME (_, type_spec) => (case projection_of type_spec of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
665 |
SOME proj => |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
666 |
if c = proj |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
667 |
then bad_thm "Projection as head in equation" |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
668 |
else () |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
669 |
| _ => ()) |
52475
445ae7a4e4e1
sort out code equations headed by a projection of a abstract datatype
haftmann
parents:
51717
diff
changeset
|
670 |
| _ => ()) |
445ae7a4e4e1
sort out code equations headed by a projection of a abstract datatype
haftmann
parents:
51717
diff
changeset
|
671 |
| _ => (); |
35226 | 672 |
in () end; |
673 |
||
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
674 |
local |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
675 |
|
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
676 |
fun raw_assert_eqn thy check_patterns (thm, proper) = |
35226 | 677 |
let |
678 |
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm |
|
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
679 |
handle TERM _ => bad_thm "Not an equation" |
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
680 |
| THM _ => bad_thm "Not a proper equation"; |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
681 |
val _ = check_eqn thy {allow_nonlinear = not proper, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
682 |
allow_consts = not (proper andalso check_patterns), allow_pats = true} thm (lhs, rhs); |
31156 | 683 |
in (thm, proper) end; |
684 |
||
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
685 |
fun raw_assert_abs_eqn thy some_tyco thm = |
35226 | 686 |
let |
687 |
val (full_lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm |
|
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
688 |
handle TERM _ => bad_thm "Not an equation" |
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
689 |
| THM _ => bad_thm "Not a proper equation"; |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
690 |
val (proj_t, lhs) = dest_comb full_lhs |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
691 |
handle TERM _ => bad_thm "Not an abstract equation"; |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
692 |
val (proj, ty) = dest_Const proj_t |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
693 |
handle TERM _ => bad_thm "Not an abstract equation"; |
40187
9b6e918682d5
more general treatment of type argument in code certificates for operations on abstract types
haftmann
parents:
39811
diff
changeset
|
694 |
val (tyco, Ts) = (dest_Type o domain_type) ty |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
695 |
handle TERM _ => bad_thm "Not an abstract equation" |
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
696 |
| TYPE _ => bad_thm "Not an abstract equation"; |
35226 | 697 |
val _ = case some_tyco of SOME tyco' => if tyco = tyco' then () |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
698 |
else bad_thm ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco') |
35226 | 699 |
| NONE => (); |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
700 |
val (vs, proj', (abs', _)) = case lookup_vs_type_spec thy tyco |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
701 |
of SOME (vs, Abstractor spec) => (vs, #projection spec, #abstractor spec) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
702 |
| _ => bad_thm ("Not an abstract type: " ^ tyco); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
703 |
val _ = if proj = proj' then () |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
704 |
else bad_thm ("Projection mismatch: " ^ quote proj ^ " vs. " ^ quote proj'); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
705 |
val _ = check_eqn thy {allow_nonlinear = false, |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
706 |
allow_consts = false, allow_pats = false} thm (lhs, rhs); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
707 |
val _ = if ListPair.all (fn (T, (_, sort)) => Sign.of_sort thy (T, sort)) (Ts, vs) then () |
40187
9b6e918682d5
more general treatment of type argument in code certificates for operations on abstract types
haftmann
parents:
39811
diff
changeset
|
708 |
else error ("Type arguments do not satisfy sort constraints of abstype certificate."); |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
709 |
in (thm, (tyco, abs')) end; |
35226 | 710 |
|
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
711 |
in |
31156 | 712 |
|
66260 | 713 |
fun generic_assert_eqn strictness thy check_patterns eqn = |
714 |
handle_strictness fst (raw_assert_eqn thy check_patterns) strictness thy eqn; |
|
31156 | 715 |
|
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
716 |
fun generic_assert_abs_eqn strictness thy check_patterns thm = |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
717 |
handle_strictness I (raw_assert_abs_eqn thy check_patterns) strictness thy thm; |
52637
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset
|
718 |
|
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
719 |
end; |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
720 |
|
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
721 |
fun assert_eqn thy = the o generic_assert_eqn Strict thy true; |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
722 |
|
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
723 |
fun assert_abs_eqn thy some_tyco = the o generic_assert_abs_eqn Strict thy some_tyco; |
35226 | 724 |
|
33940
317933ce3712
crude support for type aliasses and corresponding constant signatures
haftmann
parents:
33756
diff
changeset
|
725 |
val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; |
31156 | 726 |
|
31957 | 727 |
fun const_typ_eqn thy thm = |
31156 | 728 |
let |
32640
ba6531df2c64
corrected order of type variables in code equations; more precise certificate for cases
haftmann
parents:
32544
diff
changeset
|
729 |
val (c, ty) = head_eqn thm; |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset
|
730 |
val c' = Axclass.unoverload_const thy (c, ty); |
33940
317933ce3712
crude support for type aliasses and corresponding constant signatures
haftmann
parents:
33756
diff
changeset
|
731 |
(*permissive wrt. to overloaded constants!*) |
31156 | 732 |
in (c', ty) end; |
33940
317933ce3712
crude support for type aliasses and corresponding constant signatures
haftmann
parents:
33756
diff
changeset
|
733 |
|
31957 | 734 |
fun const_eqn thy = fst o const_typ_eqn thy; |
31156 | 735 |
|
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset
|
736 |
fun const_abs_eqn thy = Axclass.unoverload_const thy o dest_Const o fst o strip_comb o snd |
35226 | 737 |
o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of; |
738 |
||
739 |
fun mk_proj tyco vs ty abs rep = |
|
740 |
let |
|
741 |
val ty_abs = Type (tyco, map TFree vs); |
|
742 |
val xarg = Var (("x", 0), ty); |
|
743 |
in Logic.mk_equals (Const (rep, ty_abs --> ty) $ (Const (abs, ty --> ty_abs) $ xarg), xarg) end; |
|
744 |
||
34895 | 745 |
|
746 |
(* technical transformations of code equations *) |
|
747 |
||
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
748 |
fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy); |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
749 |
|
34895 | 750 |
fun expand_eta thy k thm = |
751 |
let |
|
752 |
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm; |
|
753 |
val (_, args) = strip_comb lhs; |
|
754 |
val l = if k = ~1 |
|
755 |
then (length o fst o strip_abs) rhs |
|
756 |
else Int.max (0, k - length args); |
|
757 |
val (raw_vars, _) = Term.strip_abs_eta l rhs; |
|
758 |
val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs []))) |
|
759 |
raw_vars; |
|
760 |
fun expand (v, ty) thm = Drule.fun_cong_rule thm |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59458
diff
changeset
|
761 |
(Thm.global_cterm_of thy (Var ((v, 0), ty))); |
34895 | 762 |
in |
763 |
thm |
|
764 |
|> fold expand vars |
|
765 |
|> Conv.fconv_rule Drule.beta_eta_conversion |
|
766 |
end; |
|
767 |
||
768 |
fun same_arity thy thms = |
|
31962 | 769 |
let |
34895 | 770 |
val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; |
771 |
val k = fold (Integer.max o num_args_of o Thm.prop_of) thms 0; |
|
772 |
in map (expand_eta thy k) thms end; |
|
773 |
||
774 |
fun mk_desymbolization pre post mk vs = |
|
775 |
let |
|
776 |
val names = map (pre o fst o fst) vs |
|
56811 | 777 |
|> map (Name.desymbolize (SOME false)) |
34895 | 778 |
|> Name.variant_list [] |
779 |
|> map post; |
|
780 |
in map_filter (fn (((v, i), x), v') => |
|
781 |
if v = v' andalso i = 0 then NONE |
|
782 |
else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names) |
|
783 |
end; |
|
784 |
||
60367 | 785 |
fun desymbolize_tvars thy thms = |
34895 | 786 |
let |
787 |
val tvs = fold (Term.add_tvars o Thm.prop_of) thms []; |
|
60805 | 788 |
val instT = |
789 |
mk_desymbolization (unprefix "'") (prefix "'") (Thm.global_ctyp_of thy o TVar) tvs; |
|
790 |
in map (Thm.instantiate (instT, [])) thms end; |
|
34895 | 791 |
|
60367 | 792 |
fun desymbolize_vars thy thm = |
34895 | 793 |
let |
794 |
val vs = Term.add_vars (Thm.prop_of thm) []; |
|
60805 | 795 |
val inst = mk_desymbolization I I (Thm.global_cterm_of thy o Var) vs; |
796 |
in Thm.instantiate ([], inst) thm end; |
|
34895 | 797 |
|
60367 | 798 |
fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy); |
31156 | 799 |
|
34874 | 800 |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
801 |
(* preparation and classification of code equations *) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
802 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
803 |
fun prep_eqn strictness thy = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
804 |
apfst (meta_rewrite thy) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
805 |
#> generic_assert_eqn strictness thy false |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
806 |
#> Option.map (fn eqn => (const_eqn thy (fst eqn), eqn)); |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
807 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
808 |
fun prep_eqns strictness thy = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
809 |
map_filter (prep_eqn strictness thy) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
810 |
#> AList.group (op =); |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
811 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
812 |
fun prep_abs_eqn strictness thy = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
813 |
meta_rewrite thy |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
814 |
#> generic_assert_abs_eqn strictness thy NONE |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
815 |
#> Option.map (fn abs_eqn => (const_abs_eqn thy (fst abs_eqn), abs_eqn)); |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
816 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
817 |
fun prep_maybe_abs_eqn thy raw_thm = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
818 |
let |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
819 |
val thm = meta_rewrite thy raw_thm; |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
820 |
val some_abs_thm = generic_assert_abs_eqn Silent thy NONE thm; |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
821 |
in case some_abs_thm of |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
822 |
SOME (thm, tyco) => SOME (const_abs_eqn thy thm, ((thm, true), SOME tyco)) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
823 |
| NONE => generic_assert_eqn Liberal thy false (thm, false) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
824 |
|> Option.map (fn (thm, _) => (const_eqn thy thm, ((thm, is_linear thm), NONE))) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
825 |
end; |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
826 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
827 |
|
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset
|
828 |
(* abstype certificates *) |
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset
|
829 |
|
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
830 |
local |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
831 |
|
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
832 |
fun raw_abstype_cert thy proto_thm = |
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset
|
833 |
let |
63073
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset
|
834 |
val thm = (Axclass.unoverload (Proof_Context.init_global thy) o meta_rewrite thy) proto_thm; |
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset
|
835 |
val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm) |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
836 |
handle TERM _ => bad_thm "Not an equation" |
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
837 |
| THM _ => bad_thm "Not a proper equation"; |
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
838 |
val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb) |
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset
|
839 |
o apfst dest_Const o dest_comb) lhs |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
840 |
handle TERM _ => bad_thm "Not an abstype certificate"; |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58666
diff
changeset
|
841 |
val _ = apply2 (fn c => if (is_some o Axclass.class_of_param thy) c |
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
842 |
then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep); |
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
843 |
val _ = check_decl_ty thy (abs, raw_ty); |
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
844 |
val _ = check_decl_ty thy (rep, rep_ty); |
48068
04aeda922be2
explicit check for correct number of arguments for abstract constructor
haftmann
parents:
47555
diff
changeset
|
845 |
val _ = if length (binder_types raw_ty) = 1 |
04aeda922be2
explicit check for correct number of arguments for abstract constructor
haftmann
parents:
47555
diff
changeset
|
846 |
then () |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
847 |
else bad_thm "Bad type for abstract constructor"; |
40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset
|
848 |
val _ = (fst o dest_Var) param |
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
849 |
handle TERM _ => bad_thm "Not an abstype certificate"; |
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset
|
850 |
val _ = if param = rhs then () else bad_thm "Not an abstype certificate"; |
45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
851 |
val ((tyco, sorts), (abs, (vs, ty'))) = |
54603
89d5b69e5a08
prefer name-normalizing devarify over unvarifyT whenever appropriate
haftmann
parents:
53171
diff
changeset
|
852 |
analyze_constructor thy (abs, devarify raw_ty); |
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset
|
853 |
val ty = domain_type ty'; |
49534
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
854 |
val (vs', _) = typscheme thy (abs, ty'); |
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset
|
855 |
in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end; |
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset
|
856 |
|
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
857 |
in |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
858 |
|
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
859 |
fun check_abstype_cert strictness thy proto_thm = |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
860 |
handle_strictness I (raw_abstype_cert thy) strictness thy proto_thm; |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
861 |
|
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
862 |
end; |
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
863 |
|
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset
|
864 |
|
34874 | 865 |
(* code equation certificates *) |
866 |
||
34895 | 867 |
fun build_head thy (c, ty) = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59458
diff
changeset
|
868 |
Thm.global_cterm_of thy (Logic.mk_equals (Free ("HEAD", ty), Const (c, ty))); |
34874 | 869 |
|
34895 | 870 |
fun get_head thy cert_thm = |
871 |
let |
|
60949 | 872 |
val [head] = Thm.chyps_of cert_thm; |
34895 | 873 |
val (_, Const (c, ty)) = (Logic.dest_equals o Thm.term_of) head; |
874 |
in (typscheme thy (c, ty), head) end; |
|
875 |
||
35226 | 876 |
fun typscheme_projection thy = |
877 |
typscheme thy o dest_Const o fst o dest_comb o fst o Logic.dest_equals; |
|
878 |
||
879 |
fun typscheme_abs thy = |
|
880 |
typscheme thy o dest_Const o fst o strip_comb o snd o dest_comb o fst o Logic.dest_equals o Thm.prop_of; |
|
881 |
||
882 |
fun constrain_thm thy vs sorts thm = |
|
883 |
let |
|
884 |
val mapping = map2 (fn (v, sort) => fn sort' => |
|
885 |
(v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts; |
|
886 |
val inst = map2 (fn (v, sort) => fn (_, sort') => |
|
60805 | 887 |
(((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping; |
66130 | 888 |
val subst = (Term.map_types o map_type_tfree) |
40803 | 889 |
(fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v))); |
35226 | 890 |
in |
891 |
thm |
|
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35624
diff
changeset
|
892 |
|> Thm.varifyT_global |
60805 | 893 |
|> Thm.instantiate (inst, []) |
35226 | 894 |
|> pair subst |
895 |
end; |
|
896 |
||
897 |
fun concretify_abs thy tyco abs_thm = |
|
898 |
let |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
899 |
val (_, {abstractor = (c_abs, _), abs_rep, ...}) = get_abstype_spec thy tyco; |
35226 | 900 |
val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm |
901 |
val ty = fastype_of lhs; |
|
902 |
val ty_abs = (fastype_of o snd o dest_comb) lhs; |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
903 |
val abs = Thm.global_cterm_of thy (Const (c_abs, ty --> ty_abs)); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
904 |
val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric abs_rep, Thm.combination (Thm.reflexive abs) abs_thm]; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
905 |
in (c_abs, (Thm.varifyT_global o zero_var_indexes) raw_concrete_thm) end; |
35226 | 906 |
|
907 |
fun add_rhss_of_eqn thy t = |
|
908 |
let |
|
45987 | 909 |
val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals) t; |
35226 | 910 |
fun add_const (Const (c, ty)) = insert (op =) (c, Sign.const_typargs thy (c, ty)) |
911 |
| add_const _ = I |
|
39568
839a0446630b
corrected long-overlooked slip: the Pure equality of a code equation is no part of the code equation itself
haftmann
parents:
39552
diff
changeset
|
912 |
val add_consts = fold_aterms add_const |
839a0446630b
corrected long-overlooked slip: the Pure equality of a code equation is no part of the code equation itself
haftmann
parents:
39552
diff
changeset
|
913 |
in add_consts rhs o fold add_consts args end; |
35226 | 914 |
|
46513
2659ee0128c2
more explicit error on malformed abstract equation; dropped dead code; tuned signature
haftmann
parents:
45987
diff
changeset
|
915 |
val dest_eqn = apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify_global; |
35226 | 916 |
|
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
917 |
abstype cert = Nothing of thm |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
918 |
| Equations of thm * bool list |
35226 | 919 |
| Projection of term * string |
920 |
| Abstract of thm * string |
|
921 |
with |
|
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset
|
922 |
|
55364 | 923 |
fun dummy_thm ctxt c = |
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset
|
924 |
let |
55364 | 925 |
val thy = Proof_Context.theory_of ctxt; |
54603
89d5b69e5a08
prefer name-normalizing devarify over unvarifyT whenever appropriate
haftmann
parents:
53171
diff
changeset
|
926 |
val raw_ty = devarify (const_typ thy c); |
49534
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset
|
927 |
val (vs, _) = typscheme thy (c, raw_ty); |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset
|
928 |
val sortargs = case Axclass.class_of_param thy c |
40761
1ef64dcb24b7
corrected: use canonical variables of type scheme uniformly
haftmann
parents:
40758
diff
changeset
|
929 |
of SOME class => [[class]] |
1ef64dcb24b7
corrected: use canonical variables of type scheme uniformly
haftmann
parents:
40758
diff
changeset
|
930 |
| NONE => (case get_type_of_constr_or_abstr thy c |
1ef64dcb24b7
corrected: use canonical variables of type scheme uniformly
haftmann
parents:
40758
diff
changeset
|
931 |
of SOME (tyco, _) => (map snd o fst o the) |
1ef64dcb24b7
corrected: use canonical variables of type scheme uniformly
haftmann
parents:
40758
diff
changeset
|
932 |
(AList.lookup (op =) ((snd o fst o get_type thy) tyco) c) |
1ef64dcb24b7
corrected: use canonical variables of type scheme uniformly
haftmann
parents:
40758
diff
changeset
|
933 |
| NONE => replicate (length vs) []); |
1ef64dcb24b7
corrected: use canonical variables of type scheme uniformly
haftmann
parents:
40758
diff
changeset
|
934 |
val the_sort = the o AList.lookup (op =) (map fst vs ~~ sortargs); |
1ef64dcb24b7
corrected: use canonical variables of type scheme uniformly
haftmann
parents:
40758
diff
changeset
|
935 |
val ty = map_type_tfree (fn (v, _) => TFree (v, the_sort v)) raw_ty |
34895 | 936 |
val chead = build_head thy (c, ty); |
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
937 |
in Thm.weaken chead Drule.dummy_thm end; |
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset
|
938 |
|
55364 | 939 |
fun nothing_cert ctxt c = Nothing (dummy_thm ctxt c); |
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
940 |
|
55364 | 941 |
fun cert_of_eqns ctxt c [] = Equations (dummy_thm ctxt c, []) |
66167 | 942 |
| cert_of_eqns ctxt c raw_eqns = |
34874 | 943 |
let |
55364 | 944 |
val thy = Proof_Context.theory_of ctxt; |
34895 | 945 |
val eqns = burrow_fst (canonize_thms thy) raw_eqns; |
63240 | 946 |
val _ = map (assert_eqn thy) eqns; |
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset
|
947 |
val (thms, propers) = split_list eqns; |
34895 | 948 |
val _ = map (fn thm => if c = const_eqn thy thm then () |
949 |
else error ("Wrong head of code equation,\nexpected constant " |
|
61268 | 950 |
^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy thm)) thms; |
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset
|
951 |
fun tvars_of T = rev (Term.add_tvarsT T []); |
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset
|
952 |
val vss = map (tvars_of o snd o head_eqn) thms; |
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset
|
953 |
fun inter_sorts vs = |
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset
|
954 |
fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs []; |
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset
|
955 |
val sorts = map_transpose inter_sorts vss; |
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
956 |
val vts = Name.invent_names Name.context Name.aT sorts; |
40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset
|
957 |
val thms' = |
60805 | 958 |
map2 (fn vs => Thm.instantiate (vs ~~ map (Thm.ctyp_of ctxt o TFree) vts, [])) vss thms; |
40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset
|
959 |
val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms')))); |
34874 | 960 |
fun head_conv ct = if can Thm.dest_comb ct |
961 |
then Conv.fun_conv head_conv ct |
|
962 |
else Conv.rewr_conv head_thm ct; |
|
963 |
val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv); |
|
40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset
|
964 |
val cert_thm = Conjunction.intr_balanced (map rewrite_head thms'); |
35226 | 965 |
in Equations (cert_thm, propers) end; |
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset
|
966 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
967 |
fun cert_of_proj ctxt proj tyco = |
35226 | 968 |
let |
66127 | 969 |
val thy = Proof_Context.theory_of ctxt |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
970 |
val (vs, {abstractor = (abs, (_, ty)), projection = proj', ...}) = get_abstype_spec thy tyco; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
971 |
val _ = if proj = proj' then () else |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
972 |
error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy proj); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
973 |
in Projection (mk_proj tyco vs ty abs proj, tyco) end; |
35226 | 974 |
|
66127 | 975 |
fun cert_of_abs ctxt tyco c raw_abs_thm = |
34874 | 976 |
let |
66127 | 977 |
val thy = Proof_Context.theory_of ctxt; |
35226 | 978 |
val abs_thm = singleton (canonize_thms thy) raw_abs_thm; |
979 |
val _ = assert_abs_eqn thy (SOME tyco) abs_thm; |
|
980 |
val _ = if c = const_abs_eqn thy abs_thm then () |
|
981 |
else error ("Wrong head of abstract code equation,\nexpected constant " |
|
61268 | 982 |
^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy abs_thm); |
36615
88756a5a92fc
renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
wenzelm
parents:
36610
diff
changeset
|
983 |
in Abstract (Thm.legacy_freezeT abs_thm, tyco) end; |
34874 | 984 |
|
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
985 |
fun constrain_cert_thm thy sorts cert_thm = |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
986 |
let |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
987 |
val ((vs, _), head) = get_head thy cert_thm; |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
988 |
val (subst, cert_thm') = cert_thm |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
989 |
|> Thm.implies_intr head |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
990 |
|> constrain_thm thy vs sorts; |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
991 |
val head' = Thm.term_of head |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
992 |
|> subst |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59458
diff
changeset
|
993 |
|> Thm.global_cterm_of thy; |
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
994 |
val cert_thm'' = cert_thm' |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
995 |
|> Thm.elim_implies (Thm.assume head'); |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
996 |
in cert_thm'' end; |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
997 |
|
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
998 |
fun constrain_cert thy sorts (Nothing cert_thm) = |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
999 |
Nothing (constrain_cert_thm thy sorts cert_thm) |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1000 |
| constrain_cert thy sorts (Equations (cert_thm, propers)) = |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1001 |
Equations (constrain_cert_thm thy sorts cert_thm, propers) |
66324 | 1002 |
| constrain_cert _ _ (cert as Projection _) = |
35226 | 1003 |
cert |
1004 |
| constrain_cert thy sorts (Abstract (abs_thm, tyco)) = |
|
1005 |
Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco); |
|
1006 |
||
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1007 |
fun conclude_cert (Nothing cert_thm) = |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1008 |
Nothing (Thm.close_derivation cert_thm) |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1009 |
| conclude_cert (Equations (cert_thm, propers)) = |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1010 |
Equations (Thm.close_derivation cert_thm, propers) |
49971
8b50286c36d3
close code theorems explicitly after preprocessing
haftmann
parents:
49904
diff
changeset
|
1011 |
| conclude_cert (cert as Projection _) = |
8b50286c36d3
close code theorems explicitly after preprocessing
haftmann
parents:
49904
diff
changeset
|
1012 |
cert |
8b50286c36d3
close code theorems explicitly after preprocessing
haftmann
parents:
49904
diff
changeset
|
1013 |
| conclude_cert (Abstract (abs_thm, tyco)) = |
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1014 |
Abstract (Thm.close_derivation abs_thm, tyco); |
49971
8b50286c36d3
close code theorems explicitly after preprocessing
haftmann
parents:
49904
diff
changeset
|
1015 |
|
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1016 |
fun typscheme_of_cert thy (Nothing cert_thm) = |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1017 |
fst (get_head thy cert_thm) |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1018 |
| typscheme_of_cert thy (Equations (cert_thm, _)) = |
35226 | 1019 |
fst (get_head thy cert_thm) |
1020 |
| typscheme_of_cert thy (Projection (proj, _)) = |
|
1021 |
typscheme_projection thy proj |
|
1022 |
| typscheme_of_cert thy (Abstract (abs_thm, _)) = |
|
1023 |
typscheme_abs thy abs_thm; |
|
34874 | 1024 |
|
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1025 |
fun typargs_deps_of_cert thy (Nothing cert_thm) = |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1026 |
let |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1027 |
val vs = (fst o fst) (get_head thy cert_thm); |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1028 |
in (vs, []) end |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1029 |
| typargs_deps_of_cert thy (Equations (cert_thm, propers)) = |
35226 | 1030 |
let |
1031 |
val vs = (fst o fst) (get_head thy cert_thm); |
|
1032 |
val equations = if null propers then [] else |
|
1033 |
Thm.prop_of cert_thm |
|
1034 |
|> Logic.dest_conjunction_balanced (length propers); |
|
1035 |
in (vs, fold (add_rhss_of_eqn thy) equations []) end |
|
40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset
|
1036 |
| typargs_deps_of_cert thy (Projection (t, _)) = |
35226 | 1037 |
(fst (typscheme_projection thy t), add_rhss_of_eqn thy t []) |
1038 |
| typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) = |
|
1039 |
let |
|
1040 |
val vs = fst (typscheme_abs thy abs_thm); |
|
1041 |
val (_, concrete_thm) = concretify_abs thy tyco abs_thm; |
|
45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
1042 |
in (vs, add_rhss_of_eqn thy (Logic.unvarify_types_global (Thm.prop_of concrete_thm)) []) end; |
34895 | 1043 |
|
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1044 |
fun equations_of_cert thy (cert as Nothing _) = |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1045 |
(typscheme_of_cert thy cert, NONE) |
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1046 |
| equations_of_cert thy (cert as Equations (cert_thm, propers)) = |
35226 | 1047 |
let |
1048 |
val tyscm = typscheme_of_cert thy cert; |
|
1049 |
val thms = if null propers then [] else |
|
1050 |
cert_thm |
|
35624 | 1051 |
|> Local_Defs.expand [snd (get_head thy cert_thm)] |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35624
diff
changeset
|
1052 |
|> Thm.varifyT_global |
35226 | 1053 |
|> Conjunction.elim_balanced (length propers); |
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
1054 |
fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, NONE)); |
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1055 |
in (tyscm, SOME (map (abstractions o dest_eqn o Thm.prop_of) thms ~~ (map SOME thms ~~ propers))) end |
35226 | 1056 |
| equations_of_cert thy (Projection (t, tyco)) = |
1057 |
let |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1058 |
val (_, {abstractor = (abs, _), ...}) = get_abstype_spec thy tyco; |
35226 | 1059 |
val tyscm = typscheme_projection thy t; |
45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
1060 |
val t' = Logic.varify_types_global t; |
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
1061 |
fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE)); |
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1062 |
in (tyscm, SOME [((abstractions o dest_eqn) t', (NONE, true))]) end |
35226 | 1063 |
| equations_of_cert thy (Abstract (abs_thm, tyco)) = |
1064 |
let |
|
1065 |
val tyscm = typscheme_abs thy abs_thm; |
|
1066 |
val (abs, concrete_thm) = concretify_abs thy tyco abs_thm; |
|
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
1067 |
fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, (SOME abs))); |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35624
diff
changeset
|
1068 |
in |
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1069 |
(tyscm, SOME [((abstractions o dest_eqn o Thm.prop_of) concrete_thm, |
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
|
1070 |
(SOME (Thm.varifyT_global abs_thm), true))]) |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35624
diff
changeset
|
1071 |
end; |
34895 | 1072 |
|
66324 | 1073 |
fun pretty_cert _ (Nothing _) = |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1074 |
[Pretty.str "(unimplemented)"] |
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1075 |
| pretty_cert thy (cert as Equations _) = |
63073
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset
|
1076 |
(map_filter |
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset
|
1077 |
(Option.map (Thm.pretty_thm_global thy o |
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset
|
1078 |
Axclass.overload (Proof_Context.init_global thy)) o fst o snd) |
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1079 |
o these o snd o equations_of_cert thy) cert |
35226 | 1080 |
| pretty_cert thy (Projection (t, _)) = |
45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset
|
1081 |
[Syntax.pretty_term_global thy (Logic.varify_types_global t)] |
40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset
|
1082 |
| pretty_cert thy (Abstract (abs_thm, _)) = |
63073
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset
|
1083 |
[(Thm.pretty_thm_global thy o |
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset
|
1084 |
Axclass.overload (Proof_Context.init_global thy) o Thm.varifyT_global) abs_thm]; |
35226 | 1085 |
|
34895 | 1086 |
end; |
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset
|
1087 |
|
34874 | 1088 |
|
57430
020cea57eaa4
tracing facilities for the code generator preprocessor
haftmann
parents:
57429
diff
changeset
|
1089 |
(* code certificate access with preprocessing *) |
35226 | 1090 |
|
48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset
|
1091 |
fun eqn_conv conv ct = |
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset
|
1092 |
let |
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset
|
1093 |
fun lhs_conv ct = if can Thm.dest_comb ct |
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset
|
1094 |
then Conv.combination_conv lhs_conv conv ct |
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset
|
1095 |
else Conv.all_conv ct; |
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset
|
1096 |
in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end; |
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset
|
1097 |
|
55364 | 1098 |
fun rewrite_eqn conv ctxt = |
1099 |
singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt) |
|
48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset
|
1100 |
|
55364 | 1101 |
fun preprocess conv ctxt = |
63073
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset
|
1102 |
Thm.transfer (Proof_Context.theory_of ctxt) |
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset
|
1103 |
#> rewrite_eqn conv ctxt |
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset
|
1104 |
#> Axclass.unoverload ctxt; |
55363 | 1105 |
|
55364 | 1106 |
fun cert_of_eqns_preprocess ctxt functrans c = |
58559
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset
|
1107 |
let |
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset
|
1108 |
fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks) |
61268 | 1109 |
(Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns); |
58559
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset
|
1110 |
val tracing = if Config.get ctxt simp_trace then trace_eqns else (K o K) (); |
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset
|
1111 |
in |
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset
|
1112 |
tap (tracing "before function transformation") |
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset
|
1113 |
#> (perhaps o perhaps_loop o perhaps_apply) functrans |
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset
|
1114 |
#> tap (tracing "after function transformation") |
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset
|
1115 |
#> (map o apfst) (preprocess eqn_conv ctxt) |
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset
|
1116 |
#> cert_of_eqns ctxt c |
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset
|
1117 |
end; |
48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset
|
1118 |
|
57429 | 1119 |
fun get_cert ctxt functrans c = |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1120 |
case lookup_proper_fun_spec (specs_of (Proof_Context.theory_of ctxt)) c of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1121 |
NONE => nothing_cert ctxt c |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1122 |
| SOME (Eqns (_, eqns)) => eqns |
66127 | 1123 |
|> cert_of_eqns_preprocess ctxt functrans c |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1124 |
| SOME (Proj (_, (tyco, _))) => cert_of_proj ctxt c tyco |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1125 |
| SOME (Abstr (abs_thm, (tyco, _))) => abs_thm |
66127 | 1126 |
|> preprocess Conv.arg_conv ctxt |
1127 |
|> cert_of_abs ctxt tyco c; |
|
31962 | 1128 |
|
1129 |
||
66128 | 1130 |
(* case certificates *) |
31156 | 1131 |
|
66128 | 1132 |
local |
1133 |
||
1134 |
fun raw_case_cert thm = |
|
31156 | 1135 |
let |
1136 |
val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals |
|
32640
ba6531df2c64
corrected order of type variables in code equations; more precise certificate for cases
haftmann
parents:
32544
diff
changeset
|
1137 |
o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm; |
66132 | 1138 |
val _ = case head of Free _ => () |
1139 |
| Var _ => () |
|
31156 | 1140 |
| _ => raise TERM ("case_cert", []); |
1141 |
val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr; |
|
1142 |
val (Const (case_const, _), raw_params) = strip_comb case_expr; |
|
1143 |
val n = find_index (fn Free (v, _) => v = case_var | _ => false) raw_params; |
|
1144 |
val _ = if n = ~1 then raise TERM ("case_cert", []) else (); |
|
1145 |
val params = map (fst o dest_Var) (nth_drop n raw_params); |
|
1146 |
fun dest_case t = |
|
1147 |
let |
|
1148 |
val (head' $ t_co, rhs) = Logic.dest_equals t; |
|
1149 |
val _ = if head' = head then () else raise TERM ("case_cert", []); |
|
1150 |
val (Const (co, _), args) = strip_comb t_co; |
|
1151 |
val (Var (param, _), args') = strip_comb rhs; |
|
1152 |
val _ = if args' = args then () else raise TERM ("case_cert", []); |
|
1153 |
in (param, co) end; |
|
1154 |
fun analyze_cases cases = |
|
1155 |
let |
|
1156 |
val co_list = fold (AList.update (op =) o dest_case) cases []; |
|
47437
4625ee486ff6
generalise case certificates to allow ignored parameters
Andreas Lochbihler
parents:
46513
diff
changeset
|
1157 |
in map (AList.lookup (op =) co_list) params end; |
31156 | 1158 |
fun analyze_let t = |
1159 |
let |
|
1160 |
val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t; |
|
1161 |
val _ = if head' = head then () else raise TERM ("case_cert", []); |
|
1162 |
val _ = if arg' = arg then () else raise TERM ("case_cert", []); |
|
1163 |
val _ = if [param'] = params then () else raise TERM ("case_cert", []); |
|
1164 |
in [] end; |
|
1165 |
fun analyze (cases as [let_case]) = |
|
1166 |
(analyze_cases cases handle Bind => analyze_let let_case) |
|
1167 |
| analyze cases = analyze_cases cases; |
|
1168 |
in (case_const, (n, analyze cases)) end; |
|
1169 |
||
66128 | 1170 |
in |
1171 |
||
1172 |
fun case_cert thm = raw_case_cert thm |
|
31156 | 1173 |
handle Bind => error "bad case certificate" |
1174 |
| TERM _ => error "bad case certificate"; |
|
1175 |
||
66128 | 1176 |
end; |
1177 |
||
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1178 |
fun lookup_case_spec thy = History.lookup ((cases_of o specs_of) thy); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1179 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1180 |
fun get_case_schema thy c = case lookup_case_spec thy c of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1181 |
SOME (Case {schema, ...}) => SOME schema |
66189
23917e861eaa
treat "undefined" constants internally as special form of case combinators
haftmann
parents:
66167
diff
changeset
|
1182 |
| _ => NONE; |
24219 | 1183 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1184 |
fun get_case_cong thy c = case lookup_case_spec thy c of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1185 |
SOME (Case {cong, ...}) => SOME cong |
66189
23917e861eaa
treat "undefined" constants internally as special form of case combinators
haftmann
parents:
66167
diff
changeset
|
1186 |
| _ => NONE; |
23917e861eaa
treat "undefined" constants internally as special form of case combinators
haftmann
parents:
66167
diff
changeset
|
1187 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1188 |
fun is_undefined thy c = case lookup_case_spec thy c of |
66189
23917e861eaa
treat "undefined" constants internally as special form of case combinators
haftmann
parents:
66167
diff
changeset
|
1189 |
SOME Undefined => true |
23917e861eaa
treat "undefined" constants internally as special form of case combinators
haftmann
parents:
66167
diff
changeset
|
1190 |
| _ => false; |
24219 | 1191 |
|
1192 |
||
31962 | 1193 |
(* diagnostic *) |
24219 | 1194 |
|
1195 |
fun print_codesetup thy = |
|
1196 |
let |
|
42360 | 1197 |
val ctxt = Proof_Context.init_global thy; |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1198 |
val specs = specs_of thy; |
35226 | 1199 |
fun pretty_equations const thms = |
51584 | 1200 |
(Pretty.block o Pretty.fbreaks) |
61268 | 1201 |
(Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms); |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1202 |
fun pretty_function (const, Eqns (_, eqns)) = |
66131 | 1203 |
pretty_equations const (map fst eqns) |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1204 |
| pretty_function (const, Proj (proj, _)) = Pretty.block |
35226 | 1205 |
[Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj] |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1206 |
| pretty_function (const, Abstr (thm, _)) = pretty_equations const [thm]; |
35226 | 1207 |
fun pretty_typ (tyco, vs) = Pretty.str |
1208 |
(string_of_typ thy (Type (tyco, map TFree vs))); |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1209 |
fun pretty_type_spec (typ, (cos, abstract)) = if null cos |
35226 | 1210 |
then pretty_typ typ |
1211 |
else (Pretty.block o Pretty.breaks) ( |
|
1212 |
pretty_typ typ |
|
1213 |
:: Pretty.str "=" |
|
1214 |
:: (if abstract then [Pretty.str "(abstract)"] else []) |
|
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset
|
1215 |
@ separate (Pretty.str "|") (map (fn (c, (_, [])) => Pretty.str (string_of_const thy c) |
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset
|
1216 |
| (c, (_, tys)) => |
35226 | 1217 |
(Pretty.block o Pretty.breaks) |
1218 |
(Pretty.str (string_of_const thy c) |
|
1219 |
:: Pretty.str "of" |
|
1220 |
:: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos) |
|
1221 |
); |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1222 |
fun pretty_case_param NONE = "<ignored>" |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1223 |
| pretty_case_param (SOME c) = string_of_const thy c |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1224 |
fun pretty_case (const, Case {schema = (_, (_, [])), ...}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1225 |
Pretty.str (string_of_const thy const) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1226 |
| pretty_case (const, Case {schema = (_, (_, cos)), ...}) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1227 |
(Pretty.block o Pretty.breaks) [ |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1228 |
Pretty.str (string_of_const thy const), Pretty.str "with", |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1229 |
(Pretty.block o Pretty.commas o map (Pretty.str o pretty_case_param)) cos] |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1230 |
| pretty_case (const, Undefined) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1231 |
(Pretty.block o Pretty.breaks) [ |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1232 |
Pretty.str (string_of_const thy const), Pretty.str "<undefined>"]; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1233 |
val functions = all_fun_specs specs |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58666
diff
changeset
|
1234 |
|> sort (string_ord o apply2 fst); |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1235 |
val types = History.all (types_of specs) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1236 |
|> map (fn (tyco, (vs, spec)) => |
35226 | 1237 |
((tyco, vs), constructors_of spec)) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58666
diff
changeset
|
1238 |
|> sort (string_ord o apply2 (fst o fst)); |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1239 |
val cases = History.all (cases_of specs) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1240 |
|> filter (fn (_, No_Case) => false | _ => true) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1241 |
|> sort (string_ord o apply2 fst); |
24219 | 1242 |
in |
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56204
diff
changeset
|
1243 |
Pretty.writeln_chunks [ |
24219 | 1244 |
Pretty.block ( |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1245 |
Pretty.str "types:" :: Pretty.fbrk |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1246 |
:: (Pretty.fbreaks o map pretty_type_spec) types |
24219 | 1247 |
), |
25968 | 1248 |
Pretty.block ( |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1249 |
Pretty.str "functions:" :: Pretty.fbrk |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1250 |
:: (Pretty.fbreaks o map pretty_function) functions |
34901 | 1251 |
), |
1252 |
Pretty.block ( |
|
1253 |
Pretty.str "cases:" :: Pretty.fbrk |
|
1254 |
:: (Pretty.fbreaks o map pretty_case) cases |
|
24219 | 1255 |
) |
1256 |
] |
|
1257 |
end; |
|
1258 |
||
1259 |
||
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1260 |
(** declaration of executable ingredients **) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1261 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1262 |
(* abstract code declarations *) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1263 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1264 |
local |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1265 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1266 |
fun generic_code_declaration strictness lift_phi f x = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1267 |
Local_Theory.declaration |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1268 |
{syntax = false, pervasive = false} |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1269 |
(fn phi => Context.mapping (f strictness (lift_phi phi x)) I); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1270 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1271 |
in |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1272 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1273 |
fun silent_code_declaration lift_phi = generic_code_declaration Silent lift_phi; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1274 |
fun code_declaration lift_phi = generic_code_declaration Liberal lift_phi; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1275 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1276 |
end; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1277 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1278 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1279 |
(* types *) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1280 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1281 |
fun invalidate_constructors_of (_, type_spec) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1282 |
fold (fn (c, _) => History.register c unimplemented) (fst (constructors_of type_spec)); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1283 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1284 |
fun invalidate_abstract_functions_of (_, type_spec) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1285 |
fold (fn c => History.register c unimplemented) (abstract_functions_of type_spec); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1286 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1287 |
fun invalidate_case_combinators_of (_, type_spec) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1288 |
fold (fn c => History.register c No_Case) (case_combinators_of type_spec); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1289 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1290 |
fun register_type (tyco, vs_typ_spec) specs = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1291 |
let |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1292 |
val olds = the_list (History.lookup (types_of specs) tyco); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1293 |
in |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1294 |
specs |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1295 |
|> map_functions (fold invalidate_abstract_functions_of olds |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1296 |
#> invalidate_constructors_of vs_typ_spec) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1297 |
|> map_cases (fold invalidate_case_combinators_of olds) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1298 |
|> map_types (History.register tyco vs_typ_spec) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1299 |
end; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1300 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1301 |
structure Datatype_Plugin = Plugin(type T = string); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1302 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1303 |
val datatype_plugin = Plugin_Name.declare_setup @{binding datatype_code}; |
31962 | 1304 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1305 |
fun datatype_interpretation f = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1306 |
Datatype_Plugin.interpretation datatype_plugin |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1307 |
(fn tyco => Local_Theory.background_theory (fn thy => |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1308 |
thy |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1309 |
|> Sign.root_path |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1310 |
|> Sign.add_path (Long_Name.qualifier tyco) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1311 |
|> f (tyco, fst (get_type thy tyco)) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1312 |
|> Sign.restore_naming thy)); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1313 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1314 |
fun declare_datatype_global proto_constrs thy = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1315 |
let |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1316 |
fun unoverload_const_typ (c, ty) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1317 |
(Axclass.unoverload_const thy (c, ty), ty); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1318 |
val constrs = map unoverload_const_typ proto_constrs; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1319 |
val (tyco, (vs, cos)) = constrset_of_consts thy constrs; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1320 |
in |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1321 |
thy |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1322 |
|> modify_specs (register_type |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1323 |
(tyco, (vs, Constructors {constructors = cos, case_combinators = []}))) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1324 |
|> Named_Target.theory_map (Datatype_Plugin.data_default tyco) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1325 |
end; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1326 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1327 |
fun declare_datatype_cmd raw_constrs thy = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1328 |
declare_datatype_global (map (read_bare_const thy) raw_constrs) thy; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1329 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1330 |
structure Abstype_Plugin = Plugin(type T = string); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1331 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1332 |
val abstype_plugin = Plugin_Name.declare_setup @{binding abstype_code}; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1333 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1334 |
fun abstype_interpretation f = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1335 |
Abstype_Plugin.interpretation abstype_plugin |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1336 |
(fn tyco => |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1337 |
Local_Theory.background_theory (fn thy => f (tyco, get_abstype_spec thy tyco) thy)); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1338 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1339 |
fun generic_declare_abstype strictness proto_thm thy = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1340 |
case check_abstype_cert strictness thy proto_thm of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1341 |
SOME (tyco, (vs, (abstractor as (abs, (_, ty)), (proj, abs_rep)))) => |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1342 |
thy |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1343 |
|> modify_specs (register_type |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1344 |
(tyco, (vs, Abstractor {abstractor = abstractor, projection = proj, abs_rep = abs_rep, more_abstract_functions = []})) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1345 |
#> register_fun_spec proj |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1346 |
(Proj (Logic.varify_types_global (mk_proj tyco vs ty abs proj), (tyco, abs)))) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1347 |
|> Named_Target.theory_map (Abstype_Plugin.data_default tyco) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1348 |
| NONE => thy; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1349 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1350 |
val declare_abstype_global = generic_declare_abstype Strict; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1351 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1352 |
val declare_abstype = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1353 |
code_declaration Morphism.thm generic_declare_abstype; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1354 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1355 |
|
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1356 |
(* functions *) |
31962 | 1357 |
|
63239
d562c9948dee
explicit tagging of code equations de-baroquifies interface
haftmann
parents:
63238
diff
changeset
|
1358 |
(* |
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
1359 |
strictness wrt. shape of theorem propositions: |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1360 |
* default equations: silent |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1361 |
* using declarations and attributes: warnings (after morphism application!) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1362 |
* using global declarations (... -> thy -> thy): strict |
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
1363 |
* internal processing after storage: strict |
63239
d562c9948dee
explicit tagging of code equations de-baroquifies interface
haftmann
parents:
63238
diff
changeset
|
1364 |
*) |
d562c9948dee
explicit tagging of code equations de-baroquifies interface
haftmann
parents:
63238
diff
changeset
|
1365 |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1366 |
local |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1367 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1368 |
fun subsumptive_add thy verbose (thm, proper) eqns = |
52637
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset
|
1369 |
let |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1370 |
val args_of = snd o take_prefix is_Var o rev o snd o strip_comb |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1371 |
o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of; |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1372 |
val args = args_of thm; |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1373 |
val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1); |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1374 |
fun matches_args args' = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1375 |
let |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1376 |
val k = length args' - length args |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1377 |
in if k >= 0 |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1378 |
then Pattern.matchess thy (args, (map incr_idx o drop k) args') |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1379 |
else false |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1380 |
end; |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1381 |
fun drop (thm', proper') = if (proper orelse not proper') |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1382 |
andalso matches_args (args_of thm') then |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1383 |
(if verbose then warning ("Code generator: dropping subsumed code equation\n" ^ |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1384 |
Thm.string_of_thm_global thy thm') else (); true) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1385 |
else false; |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1386 |
in (thm, proper) :: filter_out drop eqns end; |
31962 | 1387 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1388 |
fun add_eqn_for (c, eqn) thy = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1389 |
thy |> modify_specs (modify_pending_eqns c |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1390 |
(subsumptive_add thy true (apfst Thm.close_derivation eqn))); |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1391 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1392 |
fun add_eqns_for default (c, proto_eqns) thy = |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1393 |
thy |> modify_specs (fn specs => |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1394 |
if is_default (lookup_fun_spec specs c) orelse not default |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1395 |
then |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1396 |
let |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1397 |
val eqns = [] |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1398 |
|> fold_rev (subsumptive_add thy (not default)) proto_eqns |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1399 |
|> (map o apfst) Thm.close_derivation; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1400 |
in specs |> register_fun_spec c (Eqns (default, eqns)) end |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1401 |
else specs); |
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
1402 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1403 |
fun add_abstract_for (c, (thm, tyco_abs as (tyco, _))) = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1404 |
modify_specs (register_fun_spec c (Abstr (Thm.close_derivation thm, tyco_abs)) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1405 |
#> map_types (History.modify_entry tyco (add_abstract_function c))) |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1406 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1407 |
in |
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
1408 |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1409 |
fun generic_declare_eqns default strictness raw_eqns thy = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1410 |
fold (add_eqns_for default) (prep_eqns strictness thy raw_eqns) thy; |
37425 | 1411 |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1412 |
fun generic_add_eqn strictness raw_eqn thy = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1413 |
fold add_eqn_for (the_list (prep_eqn strictness thy raw_eqn)) thy; |
52637
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset
|
1414 |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1415 |
fun generic_declare_abstract_eqn strictness raw_abs_eqn thy = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1416 |
fold add_abstract_for (the_list (prep_abs_eqn strictness thy raw_abs_eqn)) thy; |
55720 | 1417 |
|
63242
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset
|
1418 |
fun add_maybe_abs_eqn_liberal thm thy = |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1419 |
case prep_maybe_abs_eqn thy thm |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1420 |
of SOME (c, (eqn, NONE)) => add_eqn_for (c, eqn) thy |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1421 |
| SOME (c, ((thm, _), SOME tyco)) => add_abstract_for (c, (thm, tyco)) thy |
52637
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset
|
1422 |
| NONE => thy; |
35226 | 1423 |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1424 |
end; |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1425 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1426 |
val declare_default_eqns_global = generic_declare_eqns true Silent; |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1427 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1428 |
val declare_default_eqns = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1429 |
silent_code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns true); |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1430 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1431 |
val declare_eqns_global = generic_declare_eqns false Strict; |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1432 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1433 |
val declare_eqns = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1434 |
code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns false); |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1435 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1436 |
val add_eqn_global = generic_add_eqn Strict; |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1437 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1438 |
fun del_eqn_global thm thy = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1439 |
case prep_eqn Liberal thy (thm, false) of |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1440 |
SOME (c, (thm, _)) => |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1441 |
modify_specs (modify_pending_eqns c (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')))) thy |
31962 | 1442 |
| NONE => thy; |
1443 |
||
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1444 |
val declare_abstract_eqn_global = generic_declare_abstract_eqn Strict; |
64430
1d85ac286c72
avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar
blanchet
parents:
63242
diff
changeset
|
1445 |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1446 |
val declare_abstract_eqn = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1447 |
code_declaration Morphism.thm generic_declare_abstract_eqn; |
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset
|
1448 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1449 |
fun declare_aborting_global c = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1450 |
modify_specs (register_fun_spec c aborting); |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1451 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1452 |
fun declare_unimplemented_global c = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1453 |
modify_specs (register_fun_spec c unimplemented); |
34244 | 1454 |
|
1455 |
||
1456 |
(* cases *) |
|
1457 |
||
40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset
|
1458 |
fun case_cong thy case_const (num_args, (pos, _)) = |
37438 | 1459 |
let |
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
42707
diff
changeset
|
1460 |
val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context; |
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
42707
diff
changeset
|
1461 |
val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt; |
37438 | 1462 |
val (ws, vs) = chop pos zs; |
54604
1512fa5fe531
prefer sort-stripping const_typ over Sign.the_const_type whenever appropriate
haftmann
parents:
54603
diff
changeset
|
1463 |
val T = devarify (const_typ thy case_const); |
40844 | 1464 |
val Ts = binder_types T; |
37438 | 1465 |
val T_cong = nth Ts pos; |
1466 |
fun mk_prem z = Free (z, T_cong); |
|
1467 |
fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts); |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58666
diff
changeset
|
1468 |
val (prem, concl) = apply2 Logic.mk_equals (apply2 mk_prem (x, y), apply2 mk_concl (x, y)); |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54604
diff
changeset
|
1469 |
in |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54604
diff
changeset
|
1470 |
Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54604
diff
changeset
|
1471 |
(fn {context = ctxt', prems} => |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54604
diff
changeset
|
1472 |
Simplifier.rewrite_goals_tac ctxt' prems |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54604
diff
changeset
|
1473 |
THEN ALLGOALS (Proof_Context.fact_tac ctxt' [Drule.reflexive_thm])) |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54604
diff
changeset
|
1474 |
end; |
37438 | 1475 |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1476 |
fun declare_case_global thm thy = |
34244 | 1477 |
let |
43634 | 1478 |
val (case_const, (k, cos)) = case_cert thm; |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1479 |
fun get_type_of_constr c = case get_type_of_constr_or_abstr thy c of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1480 |
SOME (c, false) => SOME c |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1481 |
| _ => NONE; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1482 |
val cos_with_tycos = |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1483 |
(map_filter o Option.map) (fn c => (c, get_type_of_constr c)) cos; |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1484 |
val _ = case map_filter (fn (c, NONE) => SOME c | _ => NONE) cos_with_tycos of |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1485 |
[] => () |
45430 | 1486 |
| cs => error ("Non-constructor(s) in case certificate: " ^ commas_quote cs); |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1487 |
val tycos = distinct (op =) (map_filter snd cos_with_tycos); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1488 |
val schema = (1 + Int.max (1, length cos), (k, cos)); |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1489 |
val cong = case_cong thy case_const schema; |
37438 | 1490 |
in |
1491 |
thy |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1492 |
|> modify_specs (map_cases (History.register case_const |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1493 |
(Case {schema = schema, tycos = tycos, cong = cong})) |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1494 |
#> map_types (fold (fn tyco => History.modify_entry tyco |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1495 |
(add_case_combinator case_const)) tycos)) |
37438 | 1496 |
end; |
34244 | 1497 |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1498 |
fun declare_undefined_global c = |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1499 |
(modify_specs o map_cases) (History.register c Undefined); |
34244 | 1500 |
|
1501 |
||
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1502 |
(* attributes *) |
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31971
diff
changeset
|
1503 |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1504 |
fun code_attribute f = Thm.declaration_attribute |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1505 |
(fn thm => Context.mapping (f thm) I); |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1506 |
|
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1507 |
fun code_const_attribute f cs = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1508 |
code_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs)); |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1509 |
|
53171 | 1510 |
val _ = Theory.setup |
31962 | 1511 |
(let |
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31971
diff
changeset
|
1512 |
val code_attribute_parser = |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1513 |
Args.$$$ "equation" |-- Scan.succeed (code_attribute |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1514 |
(fn thm => generic_add_eqn Liberal (thm, true))) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1515 |
|| Args.$$$ "nbe" |-- Scan.succeed (code_attribute |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1516 |
(fn thm => generic_add_eqn Liberal (thm, false))) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1517 |
|| Args.$$$ "abstract" |-- Scan.succeed (code_attribute |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1518 |
(generic_declare_abstract_eqn Liberal)) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1519 |
|| Args.$$$ "abstype" |-- Scan.succeed (code_attribute |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1520 |
(generic_declare_abstype Liberal)) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1521 |
|| Args.del |-- Scan.succeed (code_attribute del_eqn_global) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1522 |
|| Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term |
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66260
diff
changeset
|
1523 |
>> code_const_attribute declare_aborting_global) |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1524 |
|| Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1525 |
>> code_const_attribute declare_unimplemented_global) |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1526 |
|| Scan.succeed (code_attribute |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66189
diff
changeset
|
1527 |
add_maybe_abs_eqn_liberal); |
31962 | 1528 |
in |
58663 | 1529 |
Attrib.setup @{binding code} (Scan.lift code_attribute_parser) |
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31971
diff
changeset
|
1530 |
"declare theorems for code generation" |
53171 | 1531 |
end); |
31962 | 1532 |
|
24219 | 1533 |
end; (*struct*) |
1534 |
||
1535 |
||
35226 | 1536 |
(* type-safe interfaces for data dependent on executable code *) |
24219 | 1537 |
|
34173
458ced35abb8
reduced code generator cache to the baremost minimum
haftmann
parents:
33977
diff
changeset
|
1538 |
functor Code_Data(Data: CODE_DATA_ARGS): CODE_DATA = |
24219 | 1539 |
struct |
1540 |
||
1541 |
type T = Data.T; |
|
1542 |
exception Data of T; |
|
1543 |
fun dest (Data x) = x |
|
1544 |
||
34173
458ced35abb8
reduced code generator cache to the baremost minimum
haftmann
parents:
33977
diff
changeset
|
1545 |
val kind = Code.declare_data (Data Data.empty); |
24219 | 1546 |
|
1547 |
val data_op = (kind, Data, dest); |
|
1548 |
||
39397 | 1549 |
fun change_yield (SOME thy) f = Code.change_yield_data data_op thy f |
1550 |
| change_yield NONE f = f Data.empty |
|
1551 |
||
1552 |
fun change some_thy f = snd (change_yield some_thy (pair () o f)); |
|
24219 | 1553 |
|
1554 |
end; |
|
1555 |
||
28143 | 1556 |
structure Code : CODE = struct open Code; end; |