author | wenzelm |
Sun, 08 Nov 2009 16:30:41 +0100 | |
changeset 33519 | e31a85f92ce9 |
parent 33395 | 62571cb54811 |
child 33751 | 7ead0ccf6cbd |
permissions | -rw-r--r-- |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Function/fundef_common.ML |
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 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
4 |
A package for general recursive function definitions. |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
5 |
Common definitions and other infrastructure. |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
6 |
*) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
7 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
8 |
structure Function_Common = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
9 |
struct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
10 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
11 |
local open Function_Lib in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
12 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
13 |
(* Profiling *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
14 |
val profile = Unsynchronized.ref false; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
15 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
16 |
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
|
17 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
18 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
19 |
val acc_const_name = @{const_name accp} |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
20 |
fun mk_acc domT R = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
21 |
Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
22 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
23 |
val function_name = suffix "C" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
24 |
val graph_name = suffix "_graph" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
25 |
val rel_name = suffix "_rel" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
26 |
val dom_name = suffix "_dom" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
27 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
28 |
(* Termination rules *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
29 |
|
33519 | 30 |
structure TerminationRule = Generic_Data |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
31 |
( |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
32 |
type T = thm list |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
33 |
val empty = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
34 |
val extend = I |
33519 | 35 |
val merge = Thm.merge_thms |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
36 |
); |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
37 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
38 |
val get_termination_rules = TerminationRule.get |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
39 |
val store_termination_rule = TerminationRule.map o cons |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
40 |
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
|
41 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
42 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
43 |
(* Function definition result data *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
44 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
45 |
datatype function_result = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
46 |
FunctionResult of |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
47 |
{ |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
48 |
fs: term list, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
49 |
G: term, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
50 |
R: term, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
51 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
52 |
psimps : thm list, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
53 |
trsimps : thm list option, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
54 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
55 |
simple_pinducts : thm list, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
56 |
cases : thm, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
57 |
termination : thm, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
58 |
domintros : thm list option |
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 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
61 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
62 |
datatype function_context_data = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
63 |
FunctionCtxData of |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
64 |
{ |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
65 |
defname : string, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
66 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
67 |
(* contains no logical entities: invariant under morphisms *) |
33395
62571cb54811
conceal partial rules depending on config flag (i.e. when called via "fun")
krauss
parents:
33373
diff
changeset
|
68 |
add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
62571cb54811
conceal partial rules depending on config flag (i.e. when called via "fun")
krauss
parents:
33373
diff
changeset
|
69 |
Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
62571cb54811
conceal partial rules depending on config flag (i.e. when called via "fun")
krauss
parents:
33373
diff
changeset
|
70 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
71 |
case_names : string list, |
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 |
fs : term list, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
74 |
R : term, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
75 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
76 |
psimps: thm list, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
77 |
pinducts: thm list, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
78 |
termination: thm |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
79 |
} |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
80 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
81 |
fun morph_function_data (FunctionCtxData {add_simps, case_names, fs, R, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
82 |
psimps, pinducts, termination, defname}) phi = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
83 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
84 |
val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
85 |
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
|
86 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
87 |
FunctionCtxData { add_simps = add_simps, case_names = case_names, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
88 |
fs = map term fs, R = term R, psimps = fact psimps, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
89 |
pinducts = fact pinducts, termination = thm termination, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
90 |
defname = name defname } |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
91 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
92 |
|
33519 | 93 |
structure FunctionData = Generic_Data |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
94 |
( |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
95 |
type T = (term * function_context_data) Item_Net.T; |
33373 | 96 |
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
|
97 |
val extend = I; |
33519 | 98 |
fun merge tabs : T = Item_Net.merge tabs; |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
99 |
); |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
100 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
101 |
val get_function = FunctionData.get o Context.Proof; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
102 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
103 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
104 |
(* Generally useful?? *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
105 |
fun lift_morphism thy f = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
106 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
107 |
val term = Drule.term_rule thy f |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
108 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
109 |
Morphism.thm_morphism f $> Morphism.term_morphism term |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
110 |
$> Morphism.typ_morphism (Logic.type_map term) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
111 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
112 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
113 |
fun import_function_data t ctxt = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
114 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
115 |
val thy = ProofContext.theory_of ctxt |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
116 |
val ct = cterm_of thy t |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
117 |
val inst_morph = lift_morphism thy o Thm.instantiate |
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 |
fun match (trm, data) = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
120 |
SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
121 |
handle Pattern.MATCH => NONE |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
122 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
123 |
get_first match (Item_Net.retrieve (get_function ctxt) t) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
124 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
125 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
126 |
fun import_last_function ctxt = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
127 |
case Item_Net.content (get_function ctxt) of |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
128 |
[] => NONE |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
129 |
| (t, data) :: _ => |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
130 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
131 |
val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
132 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
133 |
import_function_data t' ctxt' |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
134 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
135 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
136 |
val all_function_data = Item_Net.content o get_function |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
137 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
138 |
fun add_function_data (data as FunctionCtxData {fs, termination, ...}) = |
33373 | 139 |
FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
140 |
#> store_termination_rule termination |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
141 |
|
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 |
(* Simp rules for termination proofs *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
144 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
145 |
structure Termination_Simps = Named_Thms |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
146 |
( |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
147 |
val name = "termination_simp" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
148 |
val description = "Simplification rule for termination proofs" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
149 |
); |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
150 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
151 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
152 |
(* Default Termination Prover *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
153 |
|
33519 | 154 |
structure TerminationProver = Generic_Data |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
155 |
( |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
156 |
type T = Proof.context -> Proof.method |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
157 |
val empty = (fn _ => error "Termination prover not configured") |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
158 |
val extend = I |
33519 | 159 |
fun merge (a, b) = b (* FIXME ? *) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
160 |
); |
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 |
val set_termination_prover = TerminationProver.put |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
163 |
val get_termination_prover = TerminationProver.get o Context.Proof |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
164 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
165 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
166 |
(* Configuration management *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
167 |
datatype function_opt |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
168 |
= Sequential |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
169 |
| Default of string |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
170 |
| DomIntros |
33101 | 171 |
| No_Partials |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
172 |
| Tailrec |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
173 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
174 |
datatype function_config |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
175 |
= FunctionConfig of |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
176 |
{ |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
177 |
sequential: bool, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
178 |
default: string, |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
179 |
domintros: bool, |
33101 | 180 |
partials: bool, |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
181 |
tailrec: bool |
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 |
|
33101 | 184 |
fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) = |
185 |
FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec} |
|
186 |
| apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials, tailrec}) = |
|
187 |
FunctionConfig {sequential=sequential, default=d, domintros=domintros, partials=partials, tailrec=tailrec} |
|
188 |
| apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials, tailrec}) = |
|
189 |
FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials, tailrec=tailrec} |
|
190 |
| apply_opt Tailrec (FunctionConfig {sequential, default, domintros, partials, tailrec}) = |
|
191 |
FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=partials, tailrec=true} |
|
192 |
| apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials, tailrec}) = |
|
193 |
FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false, tailrec=true} |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
194 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
195 |
val default_config = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
196 |
FunctionConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), |
33101 | 197 |
domintros=false, partials=true, tailrec=false } |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
198 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
199 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
200 |
(* Analyzing function equations *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
201 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
202 |
fun split_def ctxt geq = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
203 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
204 |
fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
205 |
val qs = Term.strip_qnt_vars "all" geq |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
206 |
val imp = Term.strip_qnt_body "all" geq |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
207 |
val (gs, eq) = Logic.strip_horn imp |
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 |
val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
210 |
handle TERM _ => error (input_error "Not an equation") |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
211 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
212 |
val (head, args) = strip_comb f_args |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
213 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
214 |
val fname = fst (dest_Free head) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
215 |
handle TERM _ => error (input_error "Head symbol must not be a bound variable") |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
216 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
217 |
(fname, qs, gs, args, rhs) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
218 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
219 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
220 |
(* Check for all sorts of errors in the input *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
221 |
fun check_defs ctxt fixes eqs = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
222 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
223 |
val fnames = map (fst o fst) fixes |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
224 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
225 |
fun check geq = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
226 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
227 |
fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
228 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
229 |
val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
230 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
231 |
val _ = fname mem fnames |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
232 |
orelse input_error |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
233 |
("Head symbol of left hand side must be " |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
234 |
^ plural "" "one out of " fnames ^ commas_quote fnames) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
235 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
236 |
val _ = length args > 0 orelse input_error "Function has no arguments:" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
237 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
238 |
fun add_bvs t is = add_loose_bnos (t, 0, is) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
239 |
val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs [])) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
240 |
|> map (fst o nth (rev qs)) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
241 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
242 |
val _ = null rvs orelse input_error |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
243 |
("Variable" ^ plural " " "s " rvs ^ commas_quote rvs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
244 |
^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:") |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
245 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
246 |
val _ = forall (not o Term.exists_subterm |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
247 |
(fn Free (n, _) => n mem fnames | _ => false)) (gs @ args) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
248 |
orelse input_error "Defined function may not occur in premises or arguments" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
249 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
250 |
val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
251 |
val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
252 |
val _ = null funvars |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
253 |
orelse (warning (cat_lines |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
254 |
["Bound variable" ^ plural " " "s " funvars |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
255 |
^ commas_quote (map fst funvars) ^ |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
256 |
" occur" ^ plural "s" "" funvars ^ " in function position.", |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
257 |
"Misspelled constructor???"]); true) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
258 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
259 |
(fname, length args) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
260 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
261 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
262 |
val _ = AList.group (op =) (map check eqs) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
263 |
|> map (fn (fname, ars) => |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
264 |
length (distinct (op =) ars) = 1 |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
265 |
orelse error ("Function " ^ quote fname ^ |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
266 |
" has different numbers of arguments in different equations")) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
267 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
268 |
fun check_sorts ((fname, fT), _) = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
269 |
Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
270 |
orelse error (cat_lines |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
271 |
["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
272 |
setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT]) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
273 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
274 |
val _ = map check_sorts fixes |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
275 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
276 |
() |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
277 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
278 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
279 |
(* Preprocessors *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
280 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
281 |
type fixes = ((string * typ) * mixfix) list |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
282 |
type 'a spec = (Attrib.binding * 'a list) list |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
283 |
type preproc = function_config -> Proof.context -> fixes -> term spec |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
284 |
-> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
285 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
286 |
val fname_of = fst o dest_Free o fst o strip_comb o fst |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
287 |
o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
288 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
289 |
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
|
290 |
| mk_case_names _ n 0 = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
291 |
| mk_case_names _ n 1 = [n] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
292 |
| 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
|
293 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
294 |
fun empty_preproc check _ ctxt fixes spec = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
295 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
296 |
val (bnds, tss) = split_list spec |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
297 |
val ts = flat tss |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
298 |
val _ = check ctxt fixes ts |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
299 |
val fnames = map (fst o fst) fixes |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
300 |
val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts |
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 sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
303 |
(indices ~~ xs) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
304 |
|> map (map snd) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
305 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
306 |
(* using theorem names for case name currently disabled *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
307 |
val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
308 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
309 |
(ts, curry op ~~ bnds o Library.unflat tss, sort, cnames) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
310 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
311 |
|
33519 | 312 |
structure Preprocessor = Generic_Data |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
313 |
( |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
314 |
type T = preproc |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
315 |
val empty : T = empty_preproc check_defs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
316 |
val extend = I |
33519 | 317 |
fun merge (a, _) = a |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
318 |
); |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
319 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
320 |
val get_preproc = Preprocessor.get o Context.Proof |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
321 |
val set_preproc = Preprocessor.map o K |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
322 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
323 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
324 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
325 |
local |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
326 |
structure P = OuterParse and K = OuterKeyword |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
327 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
328 |
val option_parser = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
329 |
P.group "option" ((P.reserved "sequential" >> K Sequential) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
330 |
|| ((P.reserved "default" |-- P.term) >> Default) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
331 |
|| (P.reserved "domintros" >> K DomIntros) |
33101 | 332 |
|| (P.reserved "no_partials" >> K No_Partials) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
333 |
|| (P.reserved "tailrec" >> K Tailrec)) |
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 |
fun config_parser default = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
336 |
(Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") []) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
337 |
>> (fn opts => fold apply_opt opts default) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
338 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
339 |
fun function_parser default_cfg = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
340 |
config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
341 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
342 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
343 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
344 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
345 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
346 |