author  haftmann 
Tue, 20 Jun 2017 08:01:56 +0200  
changeset 66125  28e782dd0278 
parent 66024  77d9334830ec 
child 66126  60bf6934fabd 
permissions  rwrr 
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 
55722  23 
val assert_abs_eqn: theory > string option > thm > thm * 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*) 
31156  33 
val add_datatype: (string * typ) list > theory > theory 
34 
val add_datatype_cmd: string list > theory > theory 

35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

35 
val datatype_interpretation: 
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset

36 
(string * ((string * sort) list * (string * ((string * sort) list * typ list)) list) 
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

37 
> theory > theory) > theory > theory 
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset

38 
val add_abstype: thm > theory > theory 
59458  39 
val add_abstype_default: thm > theory > theory 
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

40 
val abstype_interpretation: 
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset

41 
(string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm))) 
31156  42 
> theory > theory) > theory > theory 
63239
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

43 
type kind 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

44 
val Equation: kind 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

45 
val Nbe: kind 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

46 
val Abstract: kind 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

47 
val add_eqn: kind * bool > thm > theory > theory 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

48 
val add_default_eqn_attribute: kind > attribute 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

49 
val add_default_eqn_attrib: kind > Token.src 
64430
1d85ac286c72
avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar
blanchet
parents:
63244
diff
changeset

50 
val del_eqn_silent: thm > theory > theory 
28368  51 
val del_eqn: thm > theory > theory 
52 
val del_eqns: string > theory > theory 

54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

53 
val del_exception: string > theory > theory 
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24837
diff
changeset

54 
val add_case: thm > theory > theory 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24837
diff
changeset

55 
val add_undefined: string > theory > theory 
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset

56 
val get_type: theory > string 
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset

57 
> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool 
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

58 
val get_type_of_constr_or_abstr: theory > string > (string * bool) option 
35226  59 
val is_constr: theory > string > bool 
60 
val is_abstr: theory > string > bool 

57429  61 
val get_cert: Proof.context > ((thm * bool) list > (thm * bool) list option) list 
62 
> string > cert 

47437
4625ee486ff6
generalise case certificates to allow ignored parameters
Andreas Lochbihler
parents:
46513
diff
changeset

63 
val get_case_scheme: theory > string > (int * (int * string option list)) option 
37438  64 
val get_case_cong: theory > string > thm option 
31890
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31642
diff
changeset

65 
val undefineds: theory > string list 
24219  66 
val print_codesetup: theory > unit 
67 
end; 

68 

69 
signature CODE_DATA_ARGS = 

70 
sig 

71 
type T 

72 
val empty: T 

73 
end; 

74 

75 
signature CODE_DATA = 

76 
sig 

77 
type T 

39397  78 
val change: theory option > (T > T) > T 
79 
val change_yield: theory option > (T > 'a * T) > 'a * T 

24219  80 
end; 
81 

82 
signature PRIVATE_CODE = 

83 
sig 

84 
include CODE 

51368
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
49971
diff
changeset

85 
val declare_data: Any.T > serial 
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
49971
diff
changeset

86 
val change_yield_data: serial * ('a > Any.T) * (Any.T > 'a) 
34251  87 
> theory > ('a > 'b * 'a) > 'b * 'a 
24219  88 
end; 
89 

90 
structure Code : PRIVATE_CODE = 

91 
struct 

92 

31962  93 
(** auxiliary **) 
94 

95 
(* printing *) 

31156  96 

39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39020
diff
changeset

97 
fun string_of_typ thy = 
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39020
diff
changeset

98 
Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy)); 
31962  99 

42359  100 
fun string_of_const thy c = 
42360  101 
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

102 
case Axclass.inst_of_param thy c of 
42359  103 
SOME (c, tyco) => 
42360  104 
Proof_Context.extern_const ctxt c ^ " " ^ enclose "[" "]" 
105 
(Proof_Context.extern_type ctxt tyco) 

106 
 NONE => Proof_Context.extern_const ctxt c 

42359  107 
end; 
31156  108 

31962  109 

110 
(* constants *) 

31156  111 

49534
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset

112 
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

113 

791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset

114 
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

115 

791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset

116 
fun devarify ty = 
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset

117 
let 
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset

118 
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

119 
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

120 
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

121 
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

122 

791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset

123 
fun typscheme thy (c, ty) = 
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset

124 
(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

125 

791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset

126 
fun typscheme_equiv (ty1, ty2) = 
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset

127 
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

128 

31962  129 
fun check_bare_const thy t = case try dest_Const t 
130 
of SOME c_ty => c_ty 

131 
 NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t); 

31156  132 

40362
82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset

133 
fun check_unoverload thy (c, ty) = 
82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset

134 
let 
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset

135 
val c' = Axclass.unoverload_const thy (c, ty); 
54604
1512fa5fe531
prefer sortstripping const_typ over Sign.the_const_type whenever appropriate
haftmann
parents:
54603
diff
changeset

136 
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

137 
in 
49534
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset

138 
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

139 
then c' 
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset

140 
else 
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset

141 
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

142 
"\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

143 
"\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

144 
string_of_typ thy ty_decl) 
40362
82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset

145 
end; 
82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset

146 

82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset

147 
fun check_const thy = check_unoverload thy o check_bare_const thy; 
31962  148 

149 
fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy; 

150 

40362
82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset

151 
fun read_const thy = check_unoverload thy o read_bare_const thy; 
31156  152 

32872
019201eb7e07
variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents:
32738
diff
changeset

153 

31962  154 
(** data store **) 
155 

35226  156 
(* datatypes *) 
157 

43634  158 
datatype typ_spec = Constructors of (string * ((string * sort) list * typ list)) list * 
159 
string list (*references to associated case constructors*) 

40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset

160 
 Abstractor of (string * ((string * sort) list * typ)) * (string * thm); 
31962  161 

43634  162 
fun constructors_of (Constructors (cos, _)) = (cos, false) 
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset

163 
 constructors_of (Abstractor ((co, (vs, ty)), _)) = ([(co, (vs, [ty]))], true); 
35226  164 

43638  165 
fun case_consts_of (Constructors (_, case_consts)) = case_consts 
166 
 case_consts_of (Abstractor _) = []; 

35226  167 

66125  168 

35226  169 
(* functions *) 
31962  170 

59458  171 
datatype fun_spec = Eqns_Default of (thm * bool) list * (thm * bool) list lazy 
43634  172 
(* (cache for default equations, lazy computation of default equations) 
173 
 helps to restore natural order of default equations *) 

35226  174 
 Eqns of (thm * bool) list 
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

175 
 None 
59458  176 
 Proj of (term * string) * bool 
177 
 Abstr of (thm * string) * bool; 

31962  178 

59458  179 
val initial_fun_spec = Eqns_Default ([], Lazy.value []); 
31962  180 

59458  181 
fun is_default (Eqns_Default _) = true 
182 
 is_default (Proj (_, default)) = default 

183 
 is_default (Abstr (_, default)) = default 

35226  184 
 is_default _ = false; 
185 

59458  186 
fun associated_abstype (Abstr ((_, tyco), _)) = SOME tyco 
35226  187 
 associated_abstype _ = NONE; 
31962  188 

189 

190 
(* executable code data *) 

191 

192 
datatype spec = Spec of { 

193 
history_concluded: bool, 

35226  194 
functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table 
31962  195 
(*with explicit history*), 
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

196 
types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table 
31962  197 
(*with explicit history*), 
66024  198 
cases: ((int * (int * string option list)) * thm) Symtab.table, 
199 
undefineds: unit Symtab.table 

31962  200 
}; 
201 

66024  202 
fun make_spec (history_concluded, (functions, (types, (cases, undefineds)))) = 
203 
Spec { history_concluded = history_concluded, functions = functions, types = types, 

204 
cases = cases, undefineds = undefineds }; 

45987  205 
fun map_spec f (Spec { history_concluded = history_concluded, 
66024  206 
functions = functions, types = types, cases = cases, undefineds = undefineds }) = 
207 
make_spec (f (history_concluded, (functions, (types, (cases, undefineds))))); 

45987  208 
fun merge_spec (Spec { history_concluded = _, functions = functions1, 
66024  209 
types = types1, cases = cases1, undefineds = undefineds1 }, 
45987  210 
Spec { history_concluded = _, functions = functions2, 
66024  211 
types = types2, cases = cases2, undefineds = undefineds2 }) = 
31156  212 
let 
42707
42d607a9ae65
improving merge of code specifications by removing code equations of constructors after merging two theories
bulwahn
parents:
42375
diff
changeset

213 
val types = Symtab.join (K (AList.merge (op =) (K true))) (types1, types2); 
43639
9cba66fb109a
correction: do not assume that case const index covered all cases
haftmann
parents:
43638
diff
changeset

214 
val case_consts_of' = (maps case_consts_of o map (snd o snd o hd o snd) o Symtab.dest); 
35226  215 
fun merge_functions ((_, history1), (_, history2)) = 
31962  216 
let 
217 
val raw_history = AList.merge (op = : serial * serial > bool) 

35226  218 
(K true) (history1, history2); 
219 
val filtered_history = filter_out (is_default o snd) raw_history; 

31962  220 
val history = if null filtered_history 
221 
then raw_history else filtered_history; 

222 
in ((false, (snd o hd) history), history) end; 

43638  223 
val all_datatype_specs = map (snd o snd o hd o snd) (Symtab.dest types); 
224 
val all_constructors = maps (map fst o fst o constructors_of) all_datatype_specs; 

43639
9cba66fb109a
correction: do not assume that case const index covered all cases
haftmann
parents:
43638
diff
changeset

225 
val invalidated_case_consts = union (op =) (case_consts_of' types1) (case_consts_of' types2) 
9cba66fb109a
correction: do not assume that case const index covered all cases
haftmann
parents:
43638
diff
changeset

226 
> subtract (op =) (maps case_consts_of all_datatype_specs) 
42707
42d607a9ae65
improving merge of code specifications by removing code equations of constructors after merging two theories
bulwahn
parents:
42375
diff
changeset

227 
val functions = Symtab.join (K merge_functions) (functions1, functions2) 
54887  228 
> fold (fn c => Symtab.map_entry c (apfst (K (true, initial_fun_spec)))) all_constructors; 
66024  229 
val cases = Symtab.merge (K true) (cases1, cases2) 
230 
> fold Symtab.delete invalidated_case_consts; 

231 
val undefineds = Symtab.merge (K true) (undefineds1, undefineds2); 

232 
in make_spec (false, (functions, (types, (cases, undefineds)))) end; 

31962  233 

234 
fun history_concluded (Spec { history_concluded, ... }) = history_concluded; 

35226  235 
fun the_functions (Spec { functions, ... }) = functions; 
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

236 
fun the_types (Spec { types, ... }) = types; 
31962  237 
fun the_cases (Spec { cases, ... }) = cases; 
66024  238 
fun the_undefineds (Spec { undefineds, ... }) = undefineds; 
32544  239 
val map_history_concluded = map_spec o apfst; 
45987  240 
val map_functions = map_spec o apsnd o apfst; 
35226  241 
val map_typs = map_spec o apsnd o apsnd o apfst; 
66024  242 
val map_cases = map_spec o apsnd o apsnd o apsnd o apfst; 
243 
val map_undefineds = map_spec o apsnd o apsnd o apsnd o apsnd; 

31962  244 

245 

246 
(* data slots dependent on executable code *) 

247 

248 
(*private copy avoids potential conflict of table exceptions*) 

31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31962
diff
changeset

249 
structure Datatab = Table(type key = int val ord = int_ord); 
31962  250 

251 
local 

252 

51368
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
49971
diff
changeset

253 
type kind = { empty: Any.T }; 
31962  254 

43684  255 
val kinds = Synchronized.var "Code_Data" (Datatab.empty: kind Datatab.table); 
31962  256 

43684  257 
fun invoke f k = 
258 
(case Datatab.lookup (Synchronized.value kinds) k of 

259 
SOME kind => f kind 

260 
 NONE => raise Fail "Invalid code data identifier"); 

31962  261 

262 
in 

263 

34173
458ced35abb8
reduced code generator cache to the baremost minimum
haftmann
parents:
33977
diff
changeset

264 
fun declare_data empty = 
31962  265 
let 
266 
val k = serial (); 

34173
458ced35abb8
reduced code generator cache to the baremost minimum
haftmann
parents:
33977
diff
changeset

267 
val kind = { empty = empty }; 
43684  268 
val _ = Synchronized.change kinds (Datatab.update (k, kind)); 
31962  269 
in k end; 
270 

271 
fun invoke_init k = invoke (fn kind => #empty kind) k; 

272 

273 
end; (*local*) 

274 

275 

276 
(* theory store *) 

277 

278 
local 

279 

51368
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
49971
diff
changeset

280 
type data = Any.T Datatab.table; 
52788  281 
fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory) option); 
31962  282 

34244  283 
structure Code_Data = Theory_Data 
31962  284 
( 
52788  285 
type T = spec * (data * theory) option Synchronized.var; 
45987  286 
val empty = (make_spec (false, (Symtab.empty, 
34244  287 
(Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ()); 
49556  288 
val extend : T > T = apsnd (K (empty_dataref ())); 
34244  289 
fun merge ((spec1, _), (spec2, _)) = 
290 
(merge_spec (spec1, spec2), empty_dataref ()); 

31962  291 
); 
292 

293 
in 

294 

35226  295 

31962  296 
(* access to executable code *) 
297 

49535  298 
val the_exec : theory > spec = fst o Code_Data.get; 
31962  299 

34244  300 
fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ())); 
31962  301 

54886
3774542df61b
uniform bookkeeping also in the case of deletion
haftmann
parents:
54884
diff
changeset

302 
fun change_fun_spec c f = (map_exec_purge o map_functions 
54887  303 
o (Symtab.map_default (c, ((false, initial_fun_spec), []))) 
35226  304 
o apfst) (fn (_, spec) => (true, f spec)); 
31962  305 

306 

307 
(* tackling equation history *) 

308 

309 
fun continue_history thy = if (history_concluded o the_exec) thy 

310 
then thy 

311 
> (Code_Data.map o apfst o map_history_concluded) (K false) 

312 
> SOME 

313 
else NONE; 

314 

315 
fun conclude_history thy = if (history_concluded o the_exec) thy 

316 
then NONE 

317 
else thy 

318 
> (Code_Data.map o apfst) 

39020  319 
((map_functions o Symtab.map) (fn _ => fn ((changed, current), history) => 
31962  320 
((false, current), 
321 
if changed then (serial (), current) :: history else history)) 

322 
#> map_history_concluded (K true)) 

323 
> SOME; 

324 

53171  325 
val _ = Theory.setup 
326 
(Theory.at_begin continue_history #> Theory.at_end conclude_history); 

31962  327 

328 

329 
(* access to data dependent on abstract executable code *) 

330 

34244  331 
fun change_yield_data (kind, mk, dest) theory f = 
31962  332 
let 
34244  333 
val dataref = (snd o Code_Data.get) theory; 
52788  334 
val (datatab, thy) = case Synchronized.value dataref 
335 
of SOME (datatab, thy) => 

60948  336 
if Context.eq_thy (theory, thy) 
52788  337 
then (datatab, thy) 
338 
else (Datatab.empty, theory) 

339 
 NONE => (Datatab.empty, theory) 

34244  340 
val data = case Datatab.lookup datatab kind 
341 
of SOME data => data 

342 
 NONE => invoke_init kind; 

40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset

343 
val result as (_, data') = f (dest data); 
34244  344 
val _ = Synchronized.change dataref 
52788  345 
((K o SOME) (Datatab.update (kind, mk data') datatab, thy)); 
34244  346 
in result end; 
31962  347 

348 
end; (*local*) 

349 

350 

351 
(** foundation **) 

352 

353 
(* datatypes *) 

31156  354 

35226  355 
fun no_constr thy s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c 
356 
^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s); 

357 

45987  358 
fun analyze_constructor thy (c, ty) = 
31156  359 
let 
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59458
diff
changeset

360 
val _ = Thm.global_cterm_of thy (Const (c, ty)); 
54603
89d5b69e5a08
prefer namenormalizing devarify over unvarifyT whenever appropriate
haftmann
parents:
53171
diff
changeset

361 
val ty_decl = devarify (const_typ thy c); 
31156  362 
fun last_typ c_ty ty = 
363 
let 

33531  364 
val tfrees = Term.add_tfreesT ty []; 
40844  365 
val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type ty)) 
35226  366 
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

367 
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

368 
val _ = 
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset

369 
if has_duplicates (eq_fst (op =)) vs 
35226  370 
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

371 
val _ = 
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45211
diff
changeset

372 
if length tfrees <> length vs 
35226  373 
then no_constr thy "type variables missing in datatype" c_ty else (); 
31156  374 
in (tyco, vs) end; 
35226  375 
val (tyco, _) = last_typ (c, ty) ty_decl; 
376 
val (_, vs) = last_typ (c, ty) ty; 

377 
in ((tyco, map snd vs), (c, (map fst vs, ty))) end; 

378 

49904
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset

379 
fun constrset_of_consts thy consts = 
35226  380 
let 
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset

381 
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

382 
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

383 
val raw_constructors = map (analyze_constructor thy) consts; 
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset

384 
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

385 
of [tyco] => tyco 
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset

386 
 [] => error "Empty constructor set" 
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset

387 
 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

388 
val vs = Name.invent Name.context Name.aT (Sign.arity_number thy tyco); 
31156  389 
fun inst vs' (c, (vs, ty)) = 
390 
let 

391 
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

392 
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

393 
val (vs'', ty'') = typscheme thy (c, ty'); 
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset

394 
in (c, (vs'', binder_types ty'')) end; 
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset

395 
val constructors = map (inst vs o snd) raw_constructors; 
2df2786ac7b7
no sort constraints on datatype constructors in internal bookkeeping
haftmann
parents:
49760
diff
changeset

396 
in (tyco, (map (rpair []) vs, constructors)) end; 
31156  397 

35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

398 
fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco) 
35226  399 
of (_, entry) :: _ => SOME entry 
400 
 _ => NONE; 

31962  401 

40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset

402 
fun get_type thy tyco = case get_type_entry thy tyco 
35226  403 
of SOME (vs, spec) => apfst (pair vs) (constructors_of spec) 
45987  404 
 NONE => Sign.arity_number thy tyco 
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset

405 
> Name.invent Name.context Name.aT 
35226  406 
> map (rpair []) 
407 
> rpair [] 

408 
> rpair false; 

409 

35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

410 
fun get_abstype_spec thy tyco = case get_type_entry thy tyco 
35226  411 
of SOME (vs, Abstractor spec) => (vs, spec) 
36122  412 
 _ => error ("Not an abstract type: " ^ tyco); 
35226  413 

35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

414 
fun get_type_of_constr_or_abstr thy c = 
40844  415 
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

416 
of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco 
35226  417 
in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end 
31962  418 
 _ => NONE; 
419 

35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

420 
fun is_constr thy c = case get_type_of_constr_or_abstr thy c 
35226  421 
of SOME (_, false) => true 
422 
 _ => false; 

423 

35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

424 
fun is_abstr thy c = case get_type_of_constr_or_abstr thy c 
35226  425 
of SOME (_, true) => true 
426 
 _ => false; 

31962  427 

31156  428 

34874  429 
(* bare code equations *) 
31156  430 

35226  431 
(* convention for variables: 
432 
?x ?'a for freefloating theorems (e.g. in the data store) 

433 
?x 'a for certificates 

434 
x 'a for final representation of equations 

435 
*) 

436 

31156  437 
exception BAD_THM of string; 
63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

438 

31156  439 
fun bad_thm msg = raise BAD_THM msg; 
63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

440 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

441 
datatype strictness = Silent  Liberal  Strict 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

442 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

443 
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

444 
handle BAD_THM msg => case strictness of 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

445 
Silent => NONE 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

446 
 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

447 
 Strict => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy (thm_of x)); 
31156  448 

449 
fun is_linear thm = 

63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

450 
let 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

451 
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

452 
in 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

453 
not (has_duplicates (op =) ((fold o fold_aterms) 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

454 
(fn Var (v, _) => cons v  _ => I) args [])) 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

455 
end; 
31156  456 

36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset

457 
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

458 
let 
54604
1512fa5fe531
prefer sortstripping const_typ over Sign.the_const_type whenever appropriate
haftmann
parents:
54603
diff
changeset

459 
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

460 
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

461 
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

462 
^ "\nof constant " ^ quote c 
40362
82a066bff182
Code.check_const etc.: reject too specific types
haftmann
parents:
40316
diff
changeset

463 
^ "\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

464 
^ string_of_typ thy ty_decl) 
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset

465 
end; 
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset

466 

35226  467 
fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) = 
31156  468 
let 
469 
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

470 
 Free _ => bad_thm "Illegal free variable" 
31156  471 
 _ => I) t []; 
472 
fun tvars_of t = fold_term_types (fn _ => 

473 
fold_atyps (fn TVar (v, _) => insert (op =) v 

49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

474 
 TFree _ => bad_thm "Illegal free type variable")) t []; 
31156  475 
val lhs_vs = vars_of lhs; 
476 
val rhs_vs = vars_of rhs; 

477 
val lhs_tvs = tvars_of lhs; 

478 
val rhs_tvs = tvars_of rhs; 

479 
val _ = if null (subtract (op =) lhs_vs rhs_vs) 

480 
then () 

49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

481 
else bad_thm "Free variables on right hand side of equation"; 
31156  482 
val _ = if null (subtract (op =) lhs_tvs rhs_tvs) 
483 
then () 

49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

484 
else bad_thm "Free type variables on right hand side of equation"; 
34894  485 
val (head, args) = strip_comb lhs; 
31156  486 
val (c, ty) = case head 
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset

487 
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

488 
 _ => bad_thm "Equation not headed by constant"; 
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

489 
fun check _ (Abs _) = bad_thm "Abstraction on left hand side of equation" 
31156  490 
 check 0 (Var _) = () 
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

491 
 check _ (Var _) = bad_thm "Variable with application on left hand side of equation" 
31156  492 
 check n (t1 $ t2) = (check (n+1) t1; check 0 t2) 
34894  493 
 check n (Const (c_ty as (c, ty))) = 
35226  494 
if allow_pats then let 
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset

495 
val c' = Axclass.unoverload_const thy c_ty 
45987  496 
in if n = (length o binder_types) ty 
35226  497 
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

498 
then () 
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

499 
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

500 
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

501 
end else bad_thm ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side of equation") 
31156  502 
val _ = map (check 0) args; 
35226  503 
val _ = if allow_nonlinear orelse is_linear thm then () 
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

504 
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

505 
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

506 
else bad_thm "Overloaded constant as head in equation"; 
34894  507 
val _ = if not (is_constr thy c) then () 
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

508 
else bad_thm "Constructor as head in equation"; 
35226  509 
val _ = if not (is_abstr thy c) then () 
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

510 
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

511 
val _ = check_decl_ty thy (c, ty); 
52475
445ae7a4e4e1
sort out code equations headed by a projection of a abstract datatype
haftmann
parents:
51717
diff
changeset

512 
val _ = case strip_type ty 
445ae7a4e4e1
sort out code equations headed by a projection of a abstract datatype
haftmann
parents:
51717
diff
changeset

513 
of (Type (tyco, _) :: _, _) => (case get_type_entry thy tyco 
445ae7a4e4e1
sort out code equations headed by a projection of a abstract datatype
haftmann
parents:
51717
diff
changeset

514 
of SOME (_, Abstractor (_, (proj, _))) => if c = proj 
445ae7a4e4e1
sort out code equations headed by a projection of a abstract datatype
haftmann
parents:
51717
diff
changeset

515 
then bad_thm "Projection as head in equation" 
445ae7a4e4e1
sort out code equations headed by a projection of a abstract datatype
haftmann
parents:
51717
diff
changeset

516 
else () 
445ae7a4e4e1
sort out code equations headed by a projection of a abstract datatype
haftmann
parents:
51717
diff
changeset

517 
 _ => ()) 
445ae7a4e4e1
sort out code equations headed by a projection of a abstract datatype
haftmann
parents:
51717
diff
changeset

518 
 _ => (); 
35226  519 
in () end; 
520 

63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

521 
local 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

522 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

523 
fun raw_assert_eqn thy check_patterns (thm, proper) = 
35226  524 
let 
525 
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

526 
handle TERM _ => bad_thm "Not an equation" 
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

527 
 THM _ => bad_thm "Not a proper equation"; 
35226  528 
val _ = check_eqn thy { allow_nonlinear = not proper, 
529 
allow_consts = not (proper andalso check_patterns), allow_pats = true } thm (lhs, rhs); 

31156  530 
in (thm, proper) end; 
531 

63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

532 
fun raw_assert_abs_eqn thy some_tyco thm = 
35226  533 
let 
534 
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

535 
handle TERM _ => bad_thm "Not an equation" 
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

536 
 THM _ => bad_thm "Not a proper equation"; 
35226  537 
val (rep, lhs) = dest_comb full_lhs 
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

538 
handle TERM _ => bad_thm "Not an abstract equation"; 
46513
2659ee0128c2
more explicit error on malformed abstract equation; dropped dead code; tuned signature
haftmann
parents:
45987
diff
changeset

539 
val (rep_const, ty) = dest_Const rep 
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

540 
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

541 
val (tyco, Ts) = (dest_Type o domain_type) ty 
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

542 
handle TERM _ => bad_thm "Not an abstract equation" 
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

543 
 TYPE _ => bad_thm "Not an abstract equation"; 
35226  544 
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

545 
else bad_thm ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco') 
35226  546 
 NONE => (); 
52637
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset

547 
val (vs', (_, (rep', _))) = case try (get_abstype_spec thy) tyco 
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset

548 
of SOME data => data 
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset

549 
 NONE => bad_thm ("Not an abstract type: " ^ tyco); 
35226  550 
val _ = if rep_const = rep' then () 
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

551 
else bad_thm ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep'); 
35226  552 
val _ = check_eqn thy { allow_nonlinear = false, 
553 
allow_consts = false, allow_pats = false } thm (lhs, rhs); 

58635  554 
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

555 
else error ("Type arguments do not satisfy sort constraints of abstype certificate."); 
35226  556 
in (thm, tyco) end; 
557 

63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

558 
in 
31156  559 

63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

560 
fun generic_assert_eqn strictness thy check_patterns thm_proper = 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

561 
handle_strictness fst (raw_assert_eqn thy check_patterns) strictness thy thm_proper; 
31156  562 

63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

563 
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

564 
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

565 

63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

566 
end; 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

567 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

568 
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

569 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

570 
fun assert_abs_eqn thy some_tyco = the o generic_assert_abs_eqn Strict thy some_tyco; 
35226  571 

33940
317933ce3712
crude support for type aliasses and corresponding constant signatures
haftmann
parents:
33756
diff
changeset

572 
val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; 
31156  573 

31957  574 
fun const_typ_eqn thy thm = 
31156  575 
let 
32640
ba6531df2c64
corrected order of type variables in code equations; more precise certificate for cases
haftmann
parents:
32544
diff
changeset

576 
val (c, ty) = head_eqn thm; 
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset

577 
val c' = Axclass.unoverload_const thy (c, ty); 
33940
317933ce3712
crude support for type aliasses and corresponding constant signatures
haftmann
parents:
33756
diff
changeset

578 
(*permissive wrt. to overloaded constants!*) 
31156  579 
in (c', ty) end; 
33940
317933ce3712
crude support for type aliasses and corresponding constant signatures
haftmann
parents:
33756
diff
changeset

580 

31957  581 
fun const_eqn thy = fst o const_typ_eqn thy; 
31156  582 

51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset

583 
fun const_abs_eqn thy = Axclass.unoverload_const thy o dest_Const o fst o strip_comb o snd 
35226  584 
o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of; 
585 

586 
fun mk_proj tyco vs ty abs rep = 

587 
let 

588 
val ty_abs = Type (tyco, map TFree vs); 

589 
val xarg = Var (("x", 0), ty); 

590 
in Logic.mk_equals (Const (rep, ty_abs > ty) $ (Const (abs, ty > ty_abs) $ xarg), xarg) end; 

591 

34895  592 

593 
(* technical transformations of code equations *) 

594 

63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

595 
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

596 

34895  597 
fun expand_eta thy k thm = 
598 
let 

599 
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm; 

600 
val (_, args) = strip_comb lhs; 

601 
val l = if k = ~1 

602 
then (length o fst o strip_abs) rhs 

603 
else Int.max (0, k  length args); 

604 
val (raw_vars, _) = Term.strip_abs_eta l rhs; 

605 
val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs []))) 

606 
raw_vars; 

607 
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

608 
(Thm.global_cterm_of thy (Var ((v, 0), ty))); 
34895  609 
in 
610 
thm 

611 
> fold expand vars 

612 
> Conv.fconv_rule Drule.beta_eta_conversion 

613 
end; 

614 

615 
fun same_arity thy thms = 

31962  616 
let 
34895  617 
val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; 
618 
val k = fold (Integer.max o num_args_of o Thm.prop_of) thms 0; 

619 
in map (expand_eta thy k) thms end; 

620 

621 
fun mk_desymbolization pre post mk vs = 

622 
let 

623 
val names = map (pre o fst o fst) vs 

56811  624 
> map (Name.desymbolize (SOME false)) 
34895  625 
> Name.variant_list [] 
626 
> map post; 

627 
in map_filter (fn (((v, i), x), v') => 

628 
if v = v' andalso i = 0 then NONE 

629 
else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names) 

630 
end; 

631 

60367  632 
fun desymbolize_tvars thy thms = 
34895  633 
let 
634 
val tvs = fold (Term.add_tvars o Thm.prop_of) thms []; 

60805  635 
val instT = 
636 
mk_desymbolization (unprefix "'") (prefix "'") (Thm.global_ctyp_of thy o TVar) tvs; 

637 
in map (Thm.instantiate (instT, [])) thms end; 

34895  638 

60367  639 
fun desymbolize_vars thy thm = 
34895  640 
let 
641 
val vs = Term.add_vars (Thm.prop_of thm) []; 

60805  642 
val inst = mk_desymbolization I I (Thm.global_cterm_of thy o Var) vs; 
643 
in Thm.instantiate ([], inst) thm end; 

34895  644 

60367  645 
fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy); 
31156  646 

34874  647 

36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset

648 
(* abstype certificates *) 
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset

649 

63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

650 
local 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

651 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

652 
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

653 
let 
63073
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset

654 
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

655 
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

656 
handle TERM _ => bad_thm "Not an equation" 
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

657 
 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

658 
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

659 
o apfst dest_Const o dest_comb) lhs 
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

660 
handle TERM _ => bad_thm "Not an abstype certificate"; 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58666
diff
changeset

661 
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

662 
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

663 
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

664 
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

665 
val _ = if length (binder_types raw_ty) = 1 
04aeda922be2
explicit check for correct number of arguments for abstract constructor
haftmann
parents:
47555
diff
changeset

666 
then () 
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

667 
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

668 
val _ = (fst o dest_Var) param 
49760
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

669 
handle TERM _ => bad_thm "Not an abstype certificate"; 
0721b1311327
more consistent error messages on malformed code equations
haftmann
parents:
49556
diff
changeset

670 
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

671 
val ((tyco, sorts), (abs, (vs, ty'))) = 
54603
89d5b69e5a08
prefer namenormalizing devarify over unvarifyT whenever appropriate
haftmann
parents:
53171
diff
changeset

672 
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

673 
val ty = domain_type ty'; 
49534
791e6fc53f73
more strict typscheme_equiv check: must fix variables of more specific type;
haftmann
parents:
49533
diff
changeset

674 
val (vs', _) = typscheme thy (abs, ty'); 
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset

675 
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

676 

63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

677 
in 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

678 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

679 
fun check_abstype_cert strictness thy proto_thm = 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

680 
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

681 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

682 
end; 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

683 

36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35845
diff
changeset

684 

34874  685 
(* code equation certificates *) 
686 

34895  687 
fun build_head thy (c, ty) = 
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59458
diff
changeset

688 
Thm.global_cterm_of thy (Logic.mk_equals (Free ("HEAD", ty), Const (c, ty))); 
34874  689 

34895  690 
fun get_head thy cert_thm = 
691 
let 

60949  692 
val [head] = Thm.chyps_of cert_thm; 
34895  693 
val (_, Const (c, ty)) = (Logic.dest_equals o Thm.term_of) head; 
694 
in (typscheme thy (c, ty), head) end; 

695 

35226  696 
fun typscheme_projection thy = 
697 
typscheme thy o dest_Const o fst o dest_comb o fst o Logic.dest_equals; 

698 

699 
fun typscheme_abs thy = 

700 
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; 

701 

702 
fun constrain_thm thy vs sorts thm = 

703 
let 

704 
val mapping = map2 (fn (v, sort) => fn sort' => 

705 
(v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts; 

706 
val inst = map2 (fn (v, sort) => fn (_, sort') => 

60805  707 
(((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping; 
40803  708 
val subst = (map_types o map_type_tfree) 
709 
(fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v))); 

35226  710 
in 
711 
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

712 
> Thm.varifyT_global 
60805  713 
> Thm.instantiate (inst, []) 
35226  714 
> pair subst 
715 
end; 

716 

717 
fun concretify_abs thy tyco abs_thm = 

718 
let 

40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset

719 
val (_, ((c, _), (_, cert))) = get_abstype_spec thy tyco; 
35226  720 
val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm 
721 
val ty = fastype_of lhs; 

722 
val ty_abs = (fastype_of o snd o dest_comb) lhs; 

59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59458
diff
changeset

723 
val abs = Thm.global_cterm_of thy (Const (c, ty > ty_abs)); 
35226  724 
val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric cert, Thm.combination (Thm.reflexive abs) abs_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

725 
in (c, (Thm.varifyT_global o zero_var_indexes) raw_concrete_thm) end; 
35226  726 

727 
fun add_rhss_of_eqn thy t = 

728 
let 

45987  729 
val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals) t; 
35226  730 
fun add_const (Const (c, ty)) = insert (op =) (c, Sign.const_typargs thy (c, ty)) 
731 
 add_const _ = I 

39568
839a0446630b
corrected longoverlooked slip: the Pure equality of a code equation is no part of the code equation itself
haftmann
parents:
39552
diff
changeset

732 
val add_consts = fold_aterms add_const 
839a0446630b
corrected longoverlooked slip: the Pure equality of a code equation is no part of the code equation itself
haftmann
parents:
39552
diff
changeset

733 
in add_consts rhs o fold add_consts args end; 
35226  734 

46513
2659ee0128c2
more explicit error on malformed abstract equation; dropped dead code; tuned signature
haftmann
parents:
45987
diff
changeset

735 
val dest_eqn = apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify_global; 
35226  736 

54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

737 
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

738 
 Equations of thm * bool list 
35226  739 
 Projection of term * string 
740 
 Abstract of thm * string 

741 
with 

34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset

742 

55364  743 
fun dummy_thm ctxt c = 
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset

744 
let 
55364  745 
val thy = Proof_Context.theory_of ctxt; 
54603
89d5b69e5a08
prefer namenormalizing devarify over unvarifyT whenever appropriate
haftmann
parents:
53171
diff
changeset

746 
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

747 
val (vs, _) = typscheme thy (c, raw_ty); 
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51584
diff
changeset

748 
val sortargs = case Axclass.class_of_param thy c 
40761
1ef64dcb24b7
corrected: use canonical variables of type scheme uniformly
haftmann
parents:
40758
diff
changeset

749 
of SOME class => [[class]] 
1ef64dcb24b7
corrected: use canonical variables of type scheme uniformly
haftmann
parents:
40758
diff
changeset

750 
 NONE => (case get_type_of_constr_or_abstr thy c 
1ef64dcb24b7
corrected: use canonical variables of type scheme uniformly
haftmann
parents:
40758
diff
changeset

751 
of SOME (tyco, _) => (map snd o fst o the) 
1ef64dcb24b7
corrected: use canonical variables of type scheme uniformly
haftmann
parents:
40758
diff
changeset

752 
(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

753 
 NONE => replicate (length vs) []); 
1ef64dcb24b7
corrected: use canonical variables of type scheme uniformly
haftmann
parents:
40758
diff
changeset

754 
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

755 
val ty = map_type_tfree (fn (v, _) => TFree (v, the_sort v)) raw_ty 
34895  756 
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

757 
in Thm.weaken chead Drule.dummy_thm end; 
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset

758 

55364  759 
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

760 

55364  761 
fun cert_of_eqns ctxt c [] = Equations (dummy_thm ctxt c, []) 
762 
 cert_of_eqns ctxt c raw_eqns = 

34874  763 
let 
55364  764 
val thy = Proof_Context.theory_of ctxt; 
34895  765 
val eqns = burrow_fst (canonize_thms thy) raw_eqns; 
63240  766 
val _ = map (assert_eqn thy) eqns; 
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset

767 
val (thms, propers) = split_list eqns; 
34895  768 
val _ = map (fn thm => if c = const_eqn thy thm then () 
769 
else error ("Wrong head of code equation,\nexpected constant " 

61268  770 
^ 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

771 
fun tvars_of T = rev (Term.add_tvarsT T []); 
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset

772 
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

773 
fun inter_sorts vs = 
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset

774 
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

775 
val sorts = map_transpose inter_sorts vss; 
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset

776 
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

777 
val thms' = 
60805  778 
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

779 
val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms')))); 
34874  780 
fun head_conv ct = if can Thm.dest_comb ct 
781 
then Conv.fun_conv head_conv ct 

782 
else Conv.rewr_conv head_thm ct; 

783 
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

784 
val cert_thm = Conjunction.intr_balanced (map rewrite_head thms'); 
35226  785 
in Equations (cert_thm, propers) end; 
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset

786 

35226  787 
fun cert_of_proj thy c tyco = 
788 
let 

40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset

789 
val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco; 
35226  790 
val _ = if c = rep then () else 
791 
error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep); 

792 
in Projection (mk_proj tyco vs ty abs rep, tyco) end; 

793 

794 
fun cert_of_abs thy tyco c raw_abs_thm = 

34874  795 
let 
35226  796 
val abs_thm = singleton (canonize_thms thy) raw_abs_thm; 
797 
val _ = assert_abs_eqn thy (SOME tyco) abs_thm; 

798 
val _ = if c = const_abs_eqn thy abs_thm then () 

799 
else error ("Wrong head of abstract code equation,\nexpected constant " 

61268  800 
^ 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

801 
in Abstract (Thm.legacy_freezeT abs_thm, tyco) end; 
34874  802 

54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

803 
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

804 
let 
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

805 
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

806 
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

807 
> Thm.implies_intr head 
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

808 
> 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

809 
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

810 
> subst 
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59458
diff
changeset

811 
> 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

812 
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

813 
> 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

814 
in cert_thm'' end; 
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

815 

4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

816 
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

817 
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

818 
 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

819 
Equations (constrain_cert_thm thy sorts cert_thm, propers) 
35226  820 
 constrain_cert thy _ (cert as Projection _) = 
821 
cert 

822 
 constrain_cert thy sorts (Abstract (abs_thm, tyco)) = 

823 
Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco); 

824 

54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

825 
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

826 
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

827 
 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

828 
Equations (Thm.close_derivation cert_thm, propers) 
49971
8b50286c36d3
close code theorems explicitly after preprocessing
haftmann
parents:
49904
diff
changeset

829 
 conclude_cert (cert as Projection _) = 
8b50286c36d3
close code theorems explicitly after preprocessing
haftmann
parents:
49904
diff
changeset

830 
cert 
8b50286c36d3
close code theorems explicitly after preprocessing
haftmann
parents:
49904
diff
changeset

831 
 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

832 
Abstract (Thm.close_derivation abs_thm, tyco); 
49971
8b50286c36d3
close code theorems explicitly after preprocessing
haftmann
parents:
49904
diff
changeset

833 

54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

834 
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

835 
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

836 
 typscheme_of_cert thy (Equations (cert_thm, _)) = 
35226  837 
fst (get_head thy cert_thm) 
838 
 typscheme_of_cert thy (Projection (proj, _)) = 

839 
typscheme_projection thy proj 

840 
 typscheme_of_cert thy (Abstract (abs_thm, _)) = 

841 
typscheme_abs thy abs_thm; 

34874  842 

54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

843 
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

844 
let 
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

845 
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

846 
in (vs, []) end 
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

847 
 typargs_deps_of_cert thy (Equations (cert_thm, propers)) = 
35226  848 
let 
849 
val vs = (fst o fst) (get_head thy cert_thm); 

850 
val equations = if null propers then [] else 

851 
Thm.prop_of cert_thm 

852 
> Logic.dest_conjunction_balanced (length propers); 

853 
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

854 
 typargs_deps_of_cert thy (Projection (t, _)) = 
35226  855 
(fst (typscheme_projection thy t), add_rhss_of_eqn thy t []) 
856 
 typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) = 

857 
let 

858 
val vs = fst (typscheme_abs thy abs_thm); 

859 
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

860 
in (vs, add_rhss_of_eqn thy (Logic.unvarify_types_global (Thm.prop_of concrete_thm)) []) end; 
34895  861 

54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

862 
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

863 
(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

864 
 equations_of_cert thy (cert as Equations (cert_thm, propers)) = 
35226  865 
let 
866 
val tyscm = typscheme_of_cert thy cert; 

867 
val thms = if null propers then [] else 

868 
cert_thm 

35624  869 
> 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

870 
> Thm.varifyT_global 
35226  871 
> 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

872 
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

873 
in (tyscm, SOME (map (abstractions o dest_eqn o Thm.prop_of) thms ~~ (map SOME thms ~~ propers))) end 
35226  874 
 equations_of_cert thy (Projection (t, tyco)) = 
875 
let 

876 
val (_, ((abs, _), _)) = get_abstype_spec thy tyco; 

877 
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

878 
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

879 
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

880 
in (tyscm, SOME [((abstractions o dest_eqn) t', (NONE, true))]) end 
35226  881 
 equations_of_cert thy (Abstract (abs_thm, tyco)) = 
882 
let 

883 
val tyscm = typscheme_abs thy abs_thm; 

884 
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

885 
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

886 
in 
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

887 
(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

888 
(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

889 
end; 
34895  890 

54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

891 
fun pretty_cert thy (cert as Nothing _) = 
66022  892 
[Pretty.str "(no equations)"] 
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

893 
 pretty_cert thy (cert as Equations _) = 
63073
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset

894 
(map_filter 
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset

895 
(Option.map (Thm.pretty_thm_global thy o 
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset

896 
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

897 
o these o snd o equations_of_cert thy) cert 
35226  898 
 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

899 
[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

900 
 pretty_cert thy (Abstract (abs_thm, _)) = 
63073
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset

901 
[(Thm.pretty_thm_global thy o 
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset

902 
Axclass.overload (Proof_Context.init_global thy) o Thm.varifyT_global) abs_thm]; 
35226  903 

34895  904 
end; 
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34874
diff
changeset

905 

34874  906 

57430
020cea57eaa4
tracing facilities for the code generator preprocessor
haftmann
parents:
57429
diff
changeset

907 
(* code certificate access with preprocessing *) 
35226  908 

909 
fun retrieve_raw thy c = 

910 
Symtab.lookup ((the_functions o the_exec) thy) c 

911 
> Option.map (snd o fst) 

54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

912 
> the_default None 
34874  913 

48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset

914 
fun eqn_conv conv ct = 
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset

915 
let 
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset

916 
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

917 
then Conv.combination_conv lhs_conv conv ct 
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset

918 
else Conv.all_conv ct; 
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset

919 
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

920 

55364  921 
fun rewrite_eqn conv ctxt = 
922 
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

923 

55364  924 
fun preprocess conv ctxt = 
63073
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset

925 
Thm.transfer (Proof_Context.theory_of ctxt) 
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset

926 
#> rewrite_eqn conv ctxt 
413184c7a2a2
clarified context, notably for internal use of Simplifier;
wenzelm
parents:
61268
diff
changeset

927 
#> Axclass.unoverload ctxt; 
55363  928 

55364  929 
fun cert_of_eqns_preprocess ctxt functrans c = 
58559
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset

930 
let 
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset

931 
fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks) 
61268  932 
(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

933 
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

934 
in 
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset

935 
tap (tracing "before function transformation") 
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset

936 
#> (perhaps o perhaps_loop o perhaps_apply) functrans 
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset

937 
#> tap (tracing "after function transformation") 
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset

938 
#> (map o apfst) (preprocess eqn_conv ctxt) 
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset

939 
#> cert_of_eqns ctxt c 
d230e7075bcf
code preprocessor tracing also for function transformers
haftmann
parents:
58011
diff
changeset

940 
end; 
48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset

941 

57429  942 
fun get_cert ctxt functrans c = 
55364  943 
let 
57429  944 
val thy = Proof_Context.theory_of ctxt; 
55364  945 
in 
946 
case retrieve_raw thy c of 

59458  947 
Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy 
55364  948 
> cert_of_eqns_preprocess ctxt functrans c 
48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48068
diff
changeset

949 
 Eqns eqns => eqns 
55364  950 
> cert_of_eqns_preprocess ctxt functrans c 
951 
 None => nothing_cert ctxt c 

59458  952 
 Proj ((_, tyco), _) => cert_of_proj thy c tyco 
953 
 Abstr ((abs_thm, tyco), _) => abs_thm 

55364  954 
> preprocess Conv.arg_conv ctxt 
955 
> cert_of_abs thy tyco c 

956 
end; 

31962  957 

958 

959 
(* cases *) 

31156  960 

961 
fun case_certificate thm = 

962 
let 

963 
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

964 
o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm; 
31156  965 
val _ = case head of Free _ => true 
966 
 Var _ => true 

967 
 _ => raise TERM ("case_cert", []); 

968 
val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr; 

969 
val (Const (case_const, _), raw_params) = strip_comb case_expr; 

970 
val n = find_index (fn Free (v, _) => v = case_var  _ => false) raw_params; 

971 
val _ = if n = ~1 then raise TERM ("case_cert", []) else (); 

972 
val params = map (fst o dest_Var) (nth_drop n raw_params); 

973 
fun dest_case t = 

974 
let 

975 
val (head' $ t_co, rhs) = Logic.dest_equals t; 

976 
val _ = if head' = head then () else raise TERM ("case_cert", []); 

977 
val (Const (co, _), args) = strip_comb t_co; 

978 
val (Var (param, _), args') = strip_comb rhs; 

979 
val _ = if args' = args then () else raise TERM ("case_cert", []); 

980 
in (param, co) end; 

981 
fun analyze_cases cases = 

982 
let 

983 
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

984 
in map (AList.lookup (op =) co_list) params end; 
31156  985 
fun analyze_let t = 
986 
let 

987 
val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t; 

988 
val _ = if head' = head then () else raise TERM ("case_cert", []); 

989 
val _ = if arg' = arg then () else raise TERM ("case_cert", []); 

990 
val _ = if [param'] = params then () else raise TERM ("case_cert", []); 

991 
in [] end; 

992 
fun analyze (cases as [let_case]) = 

993 
(analyze_cases cases handle Bind => analyze_let let_case) 

994 
 analyze cases = analyze_cases cases; 

995 
in (case_const, (n, analyze cases)) end; 

996 

997 
fun case_cert thm = case_certificate thm 

998 
handle Bind => error "bad case certificate" 

999 
 TERM _ => error "bad case certificate"; 

1000 

66024  1001 
fun get_case_scheme thy = 
1002 
Option.map fst o (Symtab.lookup o the_cases o the_exec) thy; 

1003 
fun get_case_cong thy = 

1004 
Option.map snd o (Symtab.lookup o the_cases o the_exec) thy; 

24219  1005 

66024  1006 
val undefineds = Symtab.keys o the_undefineds o the_exec; 
24219  1007 

1008 

31962  1009 
(* diagnostic *) 
24219  1010 

1011 
fun print_codesetup thy = 

1012 
let 

42360  1013 
val ctxt = Proof_Context.init_global thy; 
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24837
diff
changeset

1014 
val exec = the_exec thy; 
35226  1015 
fun pretty_equations const thms = 
51584  1016 
(Pretty.block o Pretty.fbreaks) 
61268  1017 
(Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms); 
59458  1018 
fun pretty_function (const, Eqns_Default (_, eqns_lazy)) = 
51580
64ef8260dc60
Pretty.item markup for improved readability of lists of items;
wenzelm
parents:
51551
diff
changeset

1019 
pretty_equations const (map fst (Lazy.force eqns_lazy)) 
35226  1020 
 pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns) 
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

1021 
 pretty_function (const, None) = pretty_equations const [] 
59458  1022 
 pretty_function (const, Proj ((proj, _), _)) = Pretty.block 
35226  1023 
[Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj] 
59458  1024 
 pretty_function (const, Abstr ((thm, _), _)) = pretty_equations const [thm]; 
35226  1025 
fun pretty_typ (tyco, vs) = Pretty.str 
1026 
(string_of_typ thy (Type (tyco, map TFree vs))); 

1027 
fun pretty_typspec (typ, (cos, abstract)) = if null cos 

1028 
then pretty_typ typ 

1029 
else (Pretty.block o Pretty.breaks) ( 

1030 
pretty_typ typ 

1031 
:: Pretty.str "=" 

1032 
:: (if abstract then [Pretty.str "(abstract)"] else []) 

40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40564
diff
changeset

1033 
@ 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

1034 
 (c, (_, tys)) => 
35226  1035 
(Pretty.block o Pretty.breaks) 
1036 
(Pretty.str (string_of_const thy c) 

1037 
:: Pretty.str "of" 

1038 
:: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos) 

1039 
); 

47555  1040 
fun pretty_caseparam NONE = "<ignored>" 
1041 
 pretty_caseparam (SOME c) = string_of_const thy c 

37438  1042 
fun pretty_case (const, ((_, (_, [])), _)) = Pretty.str (string_of_const thy const) 
1043 
 pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [ 

34901  1044 
Pretty.str (string_of_const thy const), Pretty.str "with", 
47555  1045 
(Pretty.block o Pretty.commas o map (Pretty.str o pretty_caseparam)) cos]; 
35226  1046 
val functions = the_functions exec 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24283
diff
changeset

1047 
> Symtab.dest 
28695  1048 
> (map o apsnd) (snd o fst) 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58666
diff
changeset

1049 
> sort (string_ord o apply2 fst); 
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

1050 
val datatypes = the_types exec 
24219  1051 
> Symtab.dest 
35226  1052 
> map (fn (tyco, (_, (vs, spec)) :: _) => 
1053 
((tyco, vs), constructors_of spec)) 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58666
diff
changeset

1054 
> sort (string_ord o apply2 (fst o fst)); 
66024  1055 
val cases = Symtab.dest ((the_cases o the_exec) thy); 
1056 
val undefineds = Symtab.keys ((the_undefineds o the_exec) thy); 

24219  1057 
in 
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56204
diff
changeset

1058 
Pretty.writeln_chunks [ 
24219  1059 
Pretty.block ( 
34901  1060 
Pretty.str "code equations:" :: Pretty.fbrk 
35226  1061 
:: (Pretty.fbreaks o map pretty_function) functions 
24219  1062 
), 
25968  1063 
Pretty.block ( 
34901  1064 
Pretty.str "datatypes:" :: Pretty.fbrk 
35226  1065 
:: (Pretty.fbreaks o map pretty_typspec) datatypes 
34901  1066 
), 
1067 
Pretty.block ( 

1068 
Pretty.str "cases:" :: Pretty.fbrk 

1069 
:: (Pretty.fbreaks o map pretty_case) cases 

1070 
), 

1071 
Pretty.block ( 

1072 
Pretty.str "undefined:" :: Pretty.fbrk 

1073 
:: (Pretty.commas o map (Pretty.str o string_of_const thy)) undefineds 

24219  1074 
) 
1075 
] 

1076 
end; 

1077 

1078 

31962  1079 
(** declaring executable ingredients **) 
1080 

1081 
(* code equations *) 

1082 

63239
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1083 
(* 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1084 
external distinction: 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1085 
kind * default 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1086 
processual distinction: 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1087 
thm * proper for concrete equations 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1088 
thm for abstract equations 
63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1089 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1090 
strictness wrt. shape of theorem propositions: 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1091 
* default attributes: silent 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1092 
* user attributes: warnings (after morphism application!) 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1093 
* Isabelle/ML functions: strict 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1094 
* internal processing after storage: strict 
63239
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1095 
*) 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1096 

35226  1097 
fun gen_add_eqn default (raw_thm, proper) thy = 
33075  1098 
let 
35226  1099 
val thm = Thm.close_derivation raw_thm; 
1100 
val c = const_eqn thy thm; 

52788  1101 
fun update_subsume verbose (thm, proper) eqns = 
37460
910b2422571d
drop subsumed default equations (requires a little bit unfortunate laziness)
haftmann
parents:
37448
diff
changeset

1102 
let 
48902
44a6967240b7
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
wenzelm
parents:
48075
diff
changeset

1103 
val args_of = snd o take_prefix is_Var o rev o snd o strip_comb 
39791
a91430778479
redundancy check: drop trailing Var arguments (avoids eta problems with equations)
haftmann
parents:
39568
diff
changeset

1104 
o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of; 
37460
910b2422571d
drop subsumed default equations (requires a little bit unfortunate laziness)
haftmann
parents:
37448
diff
changeset

1105 
val args = args_of thm; 
59787  1106 
val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1); 
39794
51451d73c3d4
corrected subsumption check: arguments have been reversed; addition of default equations to nondefault equations is identity
haftmann
parents:
39791
diff
changeset

1107 
fun matches_args args' = 
51451d73c3d4
corrected subsumption check: arguments have been reversed; addition of default equations to nondefault equations is identity
haftmann
parents:
39791
diff
changeset

1108 
let 
51451d73c3d4
corrected subsumption check: arguments have been reversed; addition of default equations to nondefault equations is identity
haftmann
parents:
39791
diff
changeset

1109 
val k = length args'  length args 
51451d73c3d4
corrected subsumption check: arguments have been reversed; addition of default equations to nondefault equations is identity
haftmann
parents:
39791
diff
changeset

1110 
in if k >= 0 
51451d73c3d4
corrected subsumption check: arguments have been reversed; addition of default equations to nondefault equations is identity
haftmann
parents:
39791
diff
changeset

1111 
then Pattern.matchess thy (args, (map incr_idx o drop k) args') 
51451d73c3d4
corrected subsumption check: arguments have been reversed; addition of default equations to nondefault equations is identity
haftmann
parents:
39791
diff
changeset

1112 
else false 
51451d73c3d4
corrected subsumption check: arguments have been reversed; addition of default equations to nondefault equations is identity
haftmann
parents:
39791
diff
changeset

1113 
end; 
37460
910b2422571d
drop subsumed default equations (requires a little bit unfortunate laziness)
haftmann
parents:
37448
diff
changeset

1114 
fun drop (thm', proper') = if (proper orelse not proper') 
910b2422571d
drop subsumed default equations (requires a little bit unfortunate laziness)
haftmann
parents:
37448
diff
changeset

1115 
andalso matches_args (args_of thm') then 
52781
e78c3023162b
silenced subsumption warnings for default code equations entirely
haftmann
parents:
52637
diff
changeset

1116 
(if verbose then warning ("Code generator: dropping subsumed code equation\n" ^ 
61268  1117 
Thm.string_of_thm_global thy thm') else (); true) 
37460
910b2422571d
drop subsumed default equations (requires a little bit unfortunate laziness)
haftmann
parents:
37448
diff
changeset

1118 
else false; 
910b2422571d
drop subsumed default equations (requires a little bit unfortunate laziness)
haftmann
parents:
37448
diff
changeset

1119 
in (thm, proper) :: filter_out drop eqns end; 
52788  1120 
fun natural_order eqns = 
1121 
(eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns [])) 

59458  1122 
fun add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns)) 
37460
910b2422571d
drop subsumed default equations (requires a little bit unfortunate laziness)
haftmann
parents:
37448
diff
changeset

1123 
(*this restores the natural order and drops syntactic redundancies*) 
59458  1124 
 add_eqn' true None = Eqns_Default (natural_order [(thm, proper)]) 
39794
51451d73c3d4
corrected subsumption check: arguments have been reversed; addition of default equations to nondefault equations is identity
haftmann
parents:
39791
diff
changeset

1125 
 add_eqn' true fun_spec = fun_spec 
52788  1126 
 add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns) 
35226  1127 
 add_eqn' false _ = Eqns [(thm, proper)]; 
54886
3774542df61b
uniform bookkeeping also in the case of deletion
haftmann
parents:
54884
diff
changeset

1128 
in change_fun_spec c (add_eqn' default) thy end; 
31962  1129 

59458  1130 
fun gen_add_abs_eqn default raw_thm thy = 
52637
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset

1131 
let 
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset

1132 
val (abs_thm, tyco) = apfst Thm.close_derivation raw_thm; 
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset

1133 
val c = const_abs_eqn thy abs_thm; 
59458  1134 
in change_fun_spec c (K (Abstr ((abs_thm, tyco), default))) thy end; 
52637
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset

1135 

63239
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1136 
datatype kind = Equation  Nbe  Abstract; 
31962  1137 

63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1138 
fun mk_eqn strictness thy = generic_assert_eqn strictness thy false o 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1139 
apfst (meta_rewrite thy); 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1140 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1141 
fun mk_abs_eqn strictness thy = generic_assert_abs_eqn strictness thy NONE o 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1142 
meta_rewrite thy; 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1143 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1144 
fun mk_maybe_abs_eqn thy raw_thm = 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1145 
let 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1146 
val thm = meta_rewrite thy raw_thm; 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1147 
val some_abs_thm = generic_assert_abs_eqn Silent thy NONE thm; 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1148 
in case some_abs_thm 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1149 
of SOME (thm, tyco) => SOME ((thm, true), SOME tyco) 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1150 
 NONE => Option.map (fn (thm, _) => ((thm, is_linear thm), NONE)) 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1151 
(generic_assert_eqn Liberal thy false (thm, false)) 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1152 
end; 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1153 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1154 
fun generic_add_eqn strictness (kind, default) thm thy = 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1155 
case kind of 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1156 
Equation => fold (gen_add_eqn default) 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1157 
(the_list (mk_eqn strictness thy (thm, true))) thy 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1158 
 Nbe => fold (gen_add_eqn default) 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1159 
(the_list (mk_eqn strictness thy (thm, false))) thy 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1160 
 Abstract => fold (gen_add_abs_eqn default) 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1161 
(the_list (mk_abs_eqn strictness thy thm)) thy; 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1162 

9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1163 
val add_eqn = generic_add_eqn Strict; 
37425  1164 

63239
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1165 
fun lift_attribute f = Thm.declaration_attribute 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1166 
(fn thm => Context.mapping (f thm) I); 
37425  1167 

63239
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1168 
fun add_default_eqn_attribute kind = 
63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1169 
lift_attribute (generic_add_eqn Silent (kind, true)); 
52637
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset

1170 

63239
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1171 
fun add_default_eqn_attrib kind = 
d562c9948dee
explicit tagging of code equations debaroquifies interface
haftmann
parents:
63238
diff
changeset

1172 
Attrib.internal (K (add_default_eqn_attribute kind)); 
55720  1173 

63244
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1174 
fun add_maybe_abs_eqn_liberal thm thy = 
9986559617ee
clear distinction between different situations concerning strictness of code equations
haftmann
parents:
63241
diff
changeset

1175 
case mk_maybe_abs_eqn thy thm 
52637
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset

1176 
of SOME (eqn, NONE) => gen_add_eqn false eqn thy 
59458  1177 
 SOME ((thm, _), SOME tyco) => gen_add_abs_eqn false (thm, tyco) thy 
52637
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52475
diff
changeset

1178 
 NONE => thy; 
35226  1179 

64430
1d85ac286c72
avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar
blanchet
parents:
63244
diff
changeset

1180 
fun generic_del_eqn strictness thm thy = case mk_eqn strictness thy (thm, true) 
54888  1181 
of SOME (thm, _) => 
1182 
let 

59458  1183 
fun del_eqn' (Eqns_Default _) = initial_fun_spec 
35226  1184 
 del_eqn' (Eqns eqns) = 
54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

1185 
let 
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

1186 
val eqns' = filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns 
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

1187 
in if null eqns' then None else Eqns eqns' end 
35226  1188 
 del_eqn' spec = spec 
54886
3774542df61b
uniform bookkeeping also in the case of deletion
haftmann
parents:
54884
diff
changeset

1189 
in change_fun_spec (const_eqn thy thm) del_eqn' thy end 
31962  1190 
 NONE => thy; 
1191 

64430
1d85ac286c72
avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar
blanchet
parents:
63244
diff
changeset

1192 
val del_eqn_silent = generic_del_eqn Silent; 
1d85ac286c72
avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar
blanchet
parents:
63244
diff
changeset

1193 
val del_eqn = generic_del_eqn Liberal; 
1d85ac286c72
avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar
blanchet
parents:
63244
diff
changeset

1194 

54889
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

1195 
fun del_eqns c = change_fun_spec c (K None); 
4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

1196 

4121d64fde90
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents:
54888
diff
changeset

1197 
fun del_exception c = change_fun_spec c (K (Eqns [])); 
34244  1198 

1199 

1200 
(* cases *) 

1201 

40758
4f2c3e842ef8
consider sort constraints for datatype constructors when constructing the empty equation certificate;
haftmann
parents:
40726
diff
changeset

1202 
fun case_cong thy case_const (num_args, (pos, _)) = 
37438  1203 
let 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42707
diff
changeset

1204 
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

1205 
val (zs, _) = fold_map Name.variant (replicate (num_args  1) "") ctxt; 
37438  1206 
val (ws, vs) = chop pos zs; 
54604
1512fa5fe531
prefer sortstripping const_typ over Sign.the_const_type whenever appropriate
haftmann
parents:
54603
diff
changeset

1207 
val T = devarify (const_typ thy case_const); 
40844  1208 
val Ts = binder_types T; 
37438  1209 
val T_cong = nth Ts pos; 
1210 
fun mk_prem z = Free (z, T_cong); 

1211 
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

1212 
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

1213 
in 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54604
diff
changeset

1214 
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

1215 
(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

1216 
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

1217 
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

1218 
end; 
37438  1219 

34244  1220 
fun add_case thm thy = 
1221 
let 

43634  1222 
val (case_const, (k, cos)) = case_cert thm; 
47555  1223 
val _ = case (filter_out (is_constr thy) o map_filter I) cos 
34244  1224 
of [] => () 
45430  1225 
 cs => error ("Nonconstructor(s) in case certificate: " ^ commas_quote cs); 
43634  1226 
val entry = (1 + Int.max (1, length cos), (k, cos)); 
66024  1227 
fun register_case cong = map_cases 
43634  1228 
(Symtab.update (case_const, (entry, cong))); 
1229 
fun register_for_constructors (Constructors (cos', cases)) = 

1230 
Constructors (cos', 

47437
4625ee486ff6
generalise case certificates to allow ignored parameters
Andreas Lochbihler
parents:
46513
diff
changeset

1231 
if exists (fn (co, _) => member (op =) cos (SOME co)) cos' 
43634  1232 
then insert (op =) case_const cases 
1233 
else cases) 

1234 
 register_for_constructors (x as Abstractor _) = x; 

1235 
val register_type = (map_typs o Symtab.map) 

1236 
(K ((map o apsnd o apsnd) register_for_constructors)); 

37438  1237 
in 
1238 
thy 

1239 
> `(fn thy => case_cong thy case_const entry) 

43634  1240 
> (fn cong => map_exec_purge (register_case cong #> register_type)) 
37438  1241 
end; 
34244  1242 

1243 
fun add_undefined c thy = 

66024  1244 
(map_exec_purge o map_undefineds) (Symtab.update (c, ())) thy; 
34244  1245 

1246 

35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

1247 
(* types *) 
34244  1248 

35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

1249 
fun register_type (tyco, vs_spec) thy = 
34244  1250 
let 
35226  1251 
val (old_constrs, some_old_proj) = 
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset

1252 
case these (Symtab.lookup ((the_types o the_exec) thy) tyco) 
43634  1253 
of (_, (_, Constructors (cos, _))) :: _ => (map fst cos, NONE) 
36209
566be5d48090
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
haftmann
parents:
36202
diff
changeset
