author | wenzelm |
Fri, 28 Oct 2011 23:41:16 +0200 | |
changeset 45294 | 3c5d3d286055 |
parent 45290 | f599ac41e7f5 |
child 46042 | ab32a87ba01a |
permissions | -rw-r--r-- |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
1 |
(* Title: HOL/Tools/Function/function_common.ML |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
3 |
|
41114 | 4 |
Common definitions and other infrastructure for the function package. |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
5 |
*) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
6 |
|
34230 | 7 |
signature FUNCTION_DATA = |
8 |
sig |
|
9 |
||
10 |
type info = |
|
11 |
{is_partial : bool, |
|
12 |
defname : string, |
|
13 |
(* contains no logical entities: invariant under morphisms: *) |
|
14 |
add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
|
15 |
Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
|
16 |
case_names : string list, |
|
17 |
fs : term list, |
|
18 |
R : term, |
|
19 |
psimps: thm list, |
|
20 |
pinducts: thm list, |
|
34231 | 21 |
simps : thm list option, |
22 |
inducts : thm list option, |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
23 |
termination: thm} |
34230 | 24 |
|
25 |
end |
|
26 |
||
27 |
structure Function_Data : FUNCTION_DATA = |
|
28 |
struct |
|
29 |
||
30 |
type info = |
|
31 |
{is_partial : bool, |
|
32 |
defname : string, |
|
33 |
(* contains no logical entities: invariant under morphisms: *) |
|
34 |
add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
|
35 |
Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
|
36 |
case_names : string list, |
|
37 |
fs : term list, |
|
38 |
R : term, |
|
39 |
psimps: thm list, |
|
40 |
pinducts: thm list, |
|
34231 | 41 |
simps : thm list option, |
42 |
inducts : thm list option, |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
43 |
termination: thm} |
34230 | 44 |
|
45 |
end |
|
46 |
||
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
47 |
structure Function_Common = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
48 |
struct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
49 |
|
34230 | 50 |
open Function_Data |
51 |
||
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
52 |
local open Function_Lib in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
53 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
54 |
(* Profiling *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
55 |
val profile = Unsynchronized.ref false; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
56 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
57 |
fun PROFILE msg = if !profile then timeap_msg msg else I |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
58 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
59 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
60 |
val acc_const_name = @{const_name accp} |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
61 |
fun mk_acc domT R = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
62 |
Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
63 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
64 |
val function_name = suffix "C" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
65 |
val graph_name = suffix "_graph" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
66 |
val rel_name = suffix "_rel" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
67 |
val dom_name = suffix "_dom" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
68 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
69 |
(* Termination rules *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
70 |
|
33519 | 71 |
structure TerminationRule = Generic_Data |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
72 |
( |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
73 |
type T = thm list |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
74 |
val empty = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
75 |
val extend = I |
33519 | 76 |
val merge = Thm.merge_thms |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
77 |
); |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
78 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
79 |
val get_termination_rules = TerminationRule.get |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
80 |
val store_termination_rule = TerminationRule.map o cons |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
81 |
val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
82 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
83 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
84 |
(* Function definition result data *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
85 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
86 |
datatype function_result = FunctionResult of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
87 |
{fs: term list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
88 |
G: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
89 |
R: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
90 |
psimps : thm list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
91 |
simple_pinducts : thm list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
92 |
cases : thm, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
93 |
termination : thm, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
94 |
domintros : thm list option} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
95 |
|
45290 | 96 |
fun transform_function_data ({add_simps, case_names, fs, R, psimps, pinducts, |
34231 | 97 |
simps, inducts, termination, defname, is_partial} : info) phi = |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
98 |
let |
45290 | 99 |
val term = Morphism.term phi |
100 |
val thm = Morphism.thm phi |
|
101 |
val fact = Morphism.fact phi |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
102 |
val name = Binding.name_of o Morphism.binding phi o Binding.name |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
103 |
in |
34230 | 104 |
{ add_simps = add_simps, case_names = case_names, |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
105 |
fs = map term fs, R = term R, psimps = fact psimps, |
34231 | 106 |
pinducts = fact pinducts, simps = Option.map fact simps, |
107 |
inducts = Option.map fact inducts, termination = thm termination, |
|
34230 | 108 |
defname = name defname, is_partial=is_partial } |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
109 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
110 |
|
33519 | 111 |
structure FunctionData = Generic_Data |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
112 |
( |
34230 | 113 |
type T = (term * info) Item_Net.T; |
33373 | 114 |
val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
115 |
val extend = I; |
33519 | 116 |
fun merge tabs : T = Item_Net.merge tabs; |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
117 |
) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
118 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
119 |
val get_function = FunctionData.get o Context.Proof; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
120 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
121 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
122 |
fun lift_morphism thy f = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
123 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
124 |
val term = Drule.term_rule thy f |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
125 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
126 |
Morphism.thm_morphism f $> Morphism.term_morphism term |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
127 |
$> Morphism.typ_morphism (Logic.type_map term) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
128 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
129 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
130 |
fun import_function_data t ctxt = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
131 |
let |
42361 | 132 |
val thy = Proof_Context.theory_of ctxt |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
133 |
val ct = cterm_of thy t |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
134 |
val inst_morph = lift_morphism thy o Thm.instantiate |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
135 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
136 |
fun match (trm, data) = |
45290 | 137 |
SOME (transform_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
138 |
handle Pattern.MATCH => NONE |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
139 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
140 |
get_first match (Item_Net.retrieve (get_function ctxt) t) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
141 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
142 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
143 |
fun import_last_function ctxt = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
144 |
case Item_Net.content (get_function ctxt) of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
145 |
[] => NONE |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
146 |
| (t, data) :: _ => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
147 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
148 |
val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
149 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
150 |
import_function_data t' ctxt' |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
151 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
152 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
153 |
val all_function_data = Item_Net.content o get_function |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
154 |
|
34230 | 155 |
fun add_function_data (data : info as {fs, termination, ...}) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
156 |
FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
157 |
#> store_termination_rule termination |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
158 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
159 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
160 |
(* Simp rules for termination proofs *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
161 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
162 |
structure Termination_Simps = Named_Thms |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
163 |
( |
45294 | 164 |
val name = @{binding termination_simp} |
38764
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38761
diff
changeset
|
165 |
val description = "simplification rules for termination proofs" |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
166 |
) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
167 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
168 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
169 |
(* Default Termination Prover *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
170 |
|
33519 | 171 |
structure TerminationProver = Generic_Data |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
172 |
( |
36521 | 173 |
type T = Proof.context -> tactic |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
174 |
val empty = (fn _ => error "Termination prover not configured") |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
175 |
val extend = I |
38761 | 176 |
fun merge (a, _) = a |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
177 |
) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
178 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
179 |
val set_termination_prover = TerminationProver.put |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
180 |
val get_termination_prover = TerminationProver.get o Context.Proof |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
181 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
182 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
183 |
(* Configuration management *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
184 |
datatype function_opt |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
185 |
= Sequential |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
186 |
| Default of string |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
187 |
| DomIntros |
33101 | 188 |
| No_Partials |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
189 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
190 |
datatype function_config = FunctionConfig of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
191 |
{sequential: bool, |
41417 | 192 |
default: string option, |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
193 |
domintros: bool, |
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
194 |
partials: bool} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
195 |
|
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
196 |
fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials}) = |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
197 |
FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials} |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
198 |
| apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials}) = |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
199 |
FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials} |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
200 |
| apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials}) = |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
201 |
FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials} |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
202 |
| apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials}) = |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
203 |
FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
204 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
205 |
val default_config = |
41417 | 206 |
FunctionConfig { sequential=false, default=NONE, |
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
207 |
domintros=false, partials=true} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
208 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
209 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
210 |
(* Analyzing function equations *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
211 |
|
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
212 |
fun split_def ctxt check_head geq = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
213 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
214 |
fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
215 |
val qs = Term.strip_qnt_vars "all" geq |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
216 |
val imp = Term.strip_qnt_body "all" geq |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
217 |
val (gs, eq) = Logic.strip_horn imp |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
218 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
219 |
val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
220 |
handle TERM _ => error (input_error "Not an equation") |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
221 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
222 |
val (head, args) = strip_comb f_args |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
223 |
|
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
224 |
val fname = fst (dest_Free head) handle TERM _ => "" |
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
225 |
val _ = check_head fname |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
226 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
227 |
(fname, qs, gs, args, rhs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
228 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
229 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
230 |
(* Check for all sorts of errors in the input *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
231 |
fun check_defs ctxt fixes eqs = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
232 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
233 |
val fnames = map (fst o fst) fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
234 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
235 |
fun check geq = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
236 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
237 |
fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
238 |
|
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
239 |
fun check_head fname = |
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
240 |
member (op =) fnames fname orelse |
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
241 |
input_error ("Illegal equation head. Expected " ^ commas_quote fnames) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
242 |
|
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
243 |
val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
244 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
245 |
val _ = length args > 0 orelse input_error "Function has no arguments:" |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
246 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
247 |
fun add_bvs t is = add_loose_bnos (t, 0, is) |
42081 | 248 |
val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs [])) |
249 |
|> map (fst o nth (rev qs)) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
250 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
251 |
val _ = null rvs orelse input_error |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
252 |
("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
253 |
" occur" ^ plural "s" "" rvs ^ " on right hand side only:") |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
254 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
255 |
val _ = forall (not o Term.exists_subterm |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36521
diff
changeset
|
256 |
(fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
257 |
orelse input_error "Defined function may not occur in premises or arguments" |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
258 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
259 |
val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
260 |
val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
261 |
val _ = null funvars orelse (warning (cat_lines |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
262 |
["Bound variable" ^ plural " " "s " funvars ^ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
263 |
commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
264 |
" in function position.", "Misspelled constructor???"]); true) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
265 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
266 |
(fname, length args) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
267 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
268 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
269 |
val grouped_args = AList.group (op =) (map check eqs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
270 |
val _ = grouped_args |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
271 |
|> map (fn (fname, ars) => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
272 |
length (distinct (op =) ars) = 1 |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
273 |
orelse error ("Function " ^ quote fname ^ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
274 |
" has different numbers of arguments in different equations")) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
275 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
276 |
val not_defined = subtract (op =) (map fst grouped_args) fnames |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
277 |
val _ = null not_defined |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
278 |
orelse error ("No defining equations for function" ^ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
279 |
plural " " "s " not_defined ^ commas_quote not_defined) |
33751
7ead0ccf6cbd
check if equations are present for all functions to avoid low-level exception later
krauss
parents:
33519
diff
changeset
|
280 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
281 |
fun check_sorts ((fname, fT), _) = |
42361 | 282 |
Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
283 |
orelse error (cat_lines |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
284 |
["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", |
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
38764
diff
changeset
|
285 |
Syntax.string_of_typ (Config.put show_sorts true ctxt) fT]) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
286 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
287 |
val _ = map check_sorts fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
288 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
289 |
() |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
290 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
291 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
292 |
(* Preprocessors *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
293 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
294 |
type fixes = ((string * typ) * mixfix) list |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
295 |
type 'a spec = (Attrib.binding * 'a list) list |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
296 |
type preproc = function_config -> Proof.context -> fixes -> term spec -> |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
297 |
(term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
298 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
299 |
val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
300 |
HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
301 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
302 |
fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
303 |
| mk_case_names _ n 0 = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
304 |
| mk_case_names _ n 1 = [n] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
305 |
| mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
306 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
307 |
fun empty_preproc check _ ctxt fixes spec = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
308 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
309 |
val (bnds, tss) = split_list spec |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
310 |
val ts = flat tss |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
311 |
val _ = check ctxt fixes ts |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
312 |
val fnames = map (fst o fst) fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
313 |
val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
314 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
315 |
fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
316 |
(indices ~~ xs) |> map (map snd) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
317 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
318 |
(* using theorem names for case name currently disabled *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
319 |
val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
320 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
321 |
(ts, curry op ~~ bnds o Library.unflat tss, sort, cnames) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
322 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
323 |
|
33519 | 324 |
structure Preprocessor = Generic_Data |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
325 |
( |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
326 |
type T = preproc |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
327 |
val empty : T = empty_preproc check_defs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
328 |
val extend = I |
33519 | 329 |
fun merge (a, _) = a |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
330 |
) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
331 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
332 |
val get_preproc = Preprocessor.get o Context.Proof |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
333 |
val set_preproc = Preprocessor.map o K |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
334 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
335 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
336 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
337 |
local |
44357 | 338 |
val option_parser = Parse.group (fn () => "option") |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
339 |
((Parse.reserved "sequential" >> K Sequential) |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
340 |
|| ((Parse.reserved "default" |-- Parse.term) >> Default) |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
341 |
|| (Parse.reserved "domintros" >> K DomIntros) |
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
342 |
|| (Parse.reserved "no_partials" >> K No_Partials)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
343 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
344 |
fun config_parser default = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
345 |
(Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") []) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
346 |
>> (fn opts => fold apply_opt opts default) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
347 |
in |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
348 |
fun function_parser default_cfg = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
349 |
config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
350 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
351 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
352 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
353 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
354 |
end |