author | wenzelm |
Fri, 24 Sep 2010 15:53:13 +0200 | |
changeset 39687 | 4e9b6ada3a21 |
parent 39360 | cdf2c3341422 |
child 40722 | 441260986b63 |
permissions | -rw-r--r-- |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Nitpick/nitpick_preproc.ML |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
3 |
Copyright 2008, 2009, 2010 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
4 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
5 |
Nitpick's HOL preprocessor. |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
6 |
*) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
7 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
8 |
signature NITPICK_PREPROC = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
9 |
sig |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
10 |
type hol_context = Nitpick_HOL.hol_context |
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
11 |
val preprocess_formulas : |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
12 |
hol_context -> (typ option * bool option) list |
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
13 |
-> (typ option * bool option) list -> term list -> term |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
14 |
-> term list * term list * bool * bool * bool |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35807
diff
changeset
|
15 |
end; |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
16 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
17 |
structure Nitpick_Preproc : NITPICK_PREPROC = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
18 |
struct |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
19 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
20 |
open Nitpick_Util |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
21 |
open Nitpick_HOL |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
22 |
open Nitpick_Mono |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
23 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
24 |
fun is_positive_existential polar quant_s = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
25 |
(polar = Pos andalso quant_s = @{const_name Ex}) orelse |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
26 |
(polar = Neg andalso quant_s <> @{const_name Ex}) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
27 |
|
37271 | 28 |
val is_descr = |
39360
cdf2c3341422
eliminate more clutter related to "fast_descrs" optimization
blanchet
parents:
39359
diff
changeset
|
29 |
member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The}] |
37271 | 30 |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
31 |
(** Binary coding of integers **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
32 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
33 |
(* If a formula contains a numeral whose absolute value is more than this |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
34 |
threshold, the unary coding is likely not to work well and we prefer the |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
35 |
binary coding. *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
36 |
val binary_int_threshold = 3 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
37 |
|
35718 | 38 |
val may_use_binary_ints = |
39 |
let |
|
40 |
fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) = |
|
41 |
aux def t1 andalso aux false t2 |
|
42 |
| aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2 |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
43 |
| aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = |
35718 | 44 |
aux def t1 andalso aux false t2 |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset
|
45 |
| aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2 |
35718 | 46 |
| aux def (t1 $ t2) = aux def t1 andalso aux def t2 |
47 |
| aux def (t as Const (s, _)) = |
|
48 |
(not def orelse t <> @{const Suc}) andalso |
|
49 |
not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, |
|
50 |
@{const_name nat_gcd}, @{const_name nat_lcm}, |
|
51 |
@{const_name Frac}, @{const_name norm_frac}] s) |
|
52 |
| aux def (Abs (_, _, t')) = aux def t' |
|
53 |
| aux _ _ = true |
|
54 |
in aux end |
|
55 |
val should_use_binary_ints = |
|
56 |
let |
|
57 |
fun aux (t1 $ t2) = aux t1 orelse aux t2 |
|
58 |
| aux (Const (s, T)) = |
|
59 |
((s = @{const_name times} orelse s = @{const_name div}) andalso |
|
60 |
is_integer_type (body_type T)) orelse |
|
61 |
(String.isPrefix numeral_prefix s andalso |
|
62 |
let val n = the (Int.fromString (unprefix numeral_prefix s)) in |
|
63 |
n < ~ binary_int_threshold orelse n > binary_int_threshold |
|
64 |
end) |
|
65 |
| aux (Abs (_, _, t')) = aux t' |
|
66 |
| aux _ = false |
|
67 |
in aux end |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
68 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
69 |
(** Uncurrying **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
70 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
71 |
fun add_to_uncurry_table ctxt t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
72 |
let |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
73 |
val thy = ProofContext.theory_of ctxt |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
74 |
fun aux (t1 $ t2) args table = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
75 |
let val table = aux t2 [] table in aux t1 (t2 :: args) table end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
76 |
| aux (Abs (_, _, t')) _ table = aux t' [] table |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
77 |
| aux (t as Const (x as (s, _))) args table = |
39359 | 78 |
if is_built_in_const thy [(NONE, true)] x orelse |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
79 |
is_constr_like ctxt x orelse |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
80 |
is_sel s orelse s = @{const_name Sigma} then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
81 |
table |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
82 |
else |
36384 | 83 |
Termtab.map_default (t, 65536) (Integer.min (length args)) table |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
84 |
| aux _ _ table = table |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
85 |
in aux t [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
86 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
87 |
fun uncurry_prefix_for k j = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
88 |
uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
89 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
90 |
fun uncurry_term table t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
91 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
92 |
fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args) |
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
93 |
| aux (Abs (s, T, t')) args = s_betapplys [] (Abs (s, T, aux t' []), args) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
94 |
| aux (t as Const (s, T)) args = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
95 |
(case Termtab.lookup table t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
96 |
SOME n => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
97 |
if n >= 2 then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
98 |
let |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
99 |
val arg_Ts = strip_n_binders n T |> fst |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
100 |
val j = |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
101 |
if is_iterator_type (hd arg_Ts) then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
102 |
1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
103 |
else case find_index (not_equal bool_T) arg_Ts of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
104 |
~1 => n |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
105 |
| j => j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
106 |
val ((before_args, tuple_args), after_args) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
107 |
args |> chop n |>> chop j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
108 |
val ((before_arg_Ts, tuple_arg_Ts), rest_T) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
109 |
T |> strip_n_binders n |>> chop j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
110 |
val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
111 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
112 |
if n - j < 2 then |
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
113 |
s_betapplys [] (t, args) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
114 |
else |
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
115 |
s_betapplys [] |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
116 |
(Const (uncurry_prefix_for (n - j) j ^ s, |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
117 |
before_arg_Ts ---> tuple_T --> rest_T), |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
118 |
before_args @ [mk_flat_tuple tuple_T tuple_args] @ |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
119 |
after_args) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
120 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
121 |
else |
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
122 |
s_betapplys [] (t, args) |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
123 |
| NONE => s_betapplys [] (t, args)) |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
124 |
| aux t args = s_betapplys [] (t, args) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
125 |
in aux t [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
126 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
127 |
(** Boxing **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
128 |
|
39359 | 129 |
fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, ...}) def orig_t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
130 |
let |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
131 |
fun box_relational_operator_type (Type (@{type_name fun}, Ts)) = |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
132 |
Type (@{type_name fun}, map box_relational_operator_type Ts) |
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
38170
diff
changeset
|
133 |
| box_relational_operator_type (Type (@{type_name prod}, Ts)) = |
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
38170
diff
changeset
|
134 |
Type (@{type_name prod}, map (box_type hol_ctxt InPair) Ts) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
135 |
| box_relational_operator_type T = T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
136 |
fun add_boxed_types_for_var (z as (_, T)) (T', t') = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
137 |
case t' of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
138 |
Var z' => z' = z ? insert (op =) T' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
139 |
| Const (@{const_name Pair}, _) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
140 |
(case T' of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
141 |
Type (_, [T1, T2]) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
142 |
fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
143 |
| _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
144 |
\add_boxed_types_for_var", [T'], [])) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
145 |
| _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
146 |
fun box_var_in_def new_Ts old_Ts t (z as (_, T)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
147 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
148 |
@{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
149 |
| Const (s0, _) $ t1 $ _ => |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
150 |
if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
151 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
152 |
val (t', args) = strip_comb t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
153 |
val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
154 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
155 |
case fold (add_boxed_types_for_var z) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
156 |
(fst (strip_n_binders (length args) T') ~~ args) [] of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
157 |
[T''] => T'' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
158 |
| _ => T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
159 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
160 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
161 |
T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
162 |
| _ => T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
163 |
and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
164 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
165 |
val abs_T' = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
166 |
if polar = Neut orelse is_positive_existential polar quant_s then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
167 |
box_type hol_ctxt InFunLHS abs_T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
168 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
169 |
abs_T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
170 |
val body_T = body_type quant_T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
171 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
172 |
Const (quant_s, (abs_T' --> body_T) --> body_T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
173 |
$ Abs (abs_s, abs_T', |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
174 |
t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
175 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
176 |
and do_equals new_Ts old_Ts s0 T0 t1 t2 = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
177 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
178 |
val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
179 |
val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2) |
37704
c6161bee8486
adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
blanchet
parents:
37678
diff
changeset
|
180 |
val T = if def then T1 |
c6161bee8486
adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
blanchet
parents:
37678
diff
changeset
|
181 |
else [T1, T2] |> sort (int_ord o pairself size_of_typ) |> hd |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
182 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
183 |
list_comb (Const (s0, T --> T --> body_type T0), |
35384 | 184 |
map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2]) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
185 |
end |
37271 | 186 |
and do_descr s T = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
187 |
let val T1 = box_type hol_ctxt InFunLHS (range_type T) in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
188 |
Const (s, (T1 --> bool_T) --> T1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
189 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
190 |
and do_term new_Ts old_Ts polar t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
191 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
192 |
Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
193 |
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
194 |
| Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
195 |
do_equals new_Ts old_Ts s0 T0 t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
196 |
| @{const "==>"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
197 |
@{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
198 |
$ do_term new_Ts old_Ts polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
199 |
| @{const Pure.conjunction} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
200 |
@{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
201 |
$ do_term new_Ts old_Ts polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
202 |
| @{const Trueprop} $ t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
203 |
@{const Trueprop} $ do_term new_Ts old_Ts polar t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
204 |
| @{const Not} $ t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
205 |
@{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
206 |
| Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
207 |
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
208 |
| Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
209 |
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
210 |
| Const (s0 as @{const_name HOL.eq}, T0) $ t1 $ t2 => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
211 |
do_equals new_Ts old_Ts s0 T0 t1 t2 |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
212 |
| @{const HOL.conj} $ t1 $ t2 => |
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
213 |
@{const HOL.conj} $ do_term new_Ts old_Ts polar t1 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
214 |
$ do_term new_Ts old_Ts polar t2 |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
215 |
| @{const HOL.disj} $ t1 $ t2 => |
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
216 |
@{const HOL.disj} $ do_term new_Ts old_Ts polar t1 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
217 |
$ do_term new_Ts old_Ts polar t2 |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset
|
218 |
| @{const HOL.implies} $ t1 $ t2 => |
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset
|
219 |
@{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
220 |
$ do_term new_Ts old_Ts polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
221 |
| Const (x as (s, T)) => |
37271 | 222 |
if is_descr s then |
223 |
do_descr s T |
|
224 |
else |
|
225 |
Const (s, if s = @{const_name converse} orelse |
|
226 |
s = @{const_name trancl} then |
|
227 |
box_relational_operator_type T |
|
228 |
else if String.isPrefix quot_normal_prefix s then |
|
229 |
let val T' = box_type hol_ctxt InFunLHS (domain_type T) in |
|
230 |
T' --> T' |
|
231 |
end |
|
39359 | 232 |
else if is_built_in_const thy stds x orelse |
37271 | 233 |
s = @{const_name Sigma} then |
234 |
T |
|
235 |
else if is_constr_like ctxt x then |
|
236 |
box_type hol_ctxt InConstr T |
|
237 |
else if is_sel s orelse is_rep_fun ctxt x then |
|
238 |
box_type hol_ctxt InSel T |
|
239 |
else |
|
240 |
box_type hol_ctxt InExpr T) |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
241 |
| t1 $ Abs (s, T, t2') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
242 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
243 |
val t1 = do_term new_Ts old_Ts Neut t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
244 |
val T1 = fastype_of1 (new_Ts, t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
245 |
val (s1, Ts1) = dest_Type T1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
246 |
val T' = hd (snd (dest_Type (hd Ts1))) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
247 |
val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
248 |
val T2 = fastype_of1 (new_Ts, t2) |
35384 | 249 |
val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
250 |
in |
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
251 |
s_betapply new_Ts (if s1 = @{type_name fun} then |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
252 |
t1 |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
253 |
else |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
254 |
select_nth_constr_arg ctxt stds |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
255 |
(@{const_name FunBox}, |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
256 |
Type (@{type_name fun}, Ts1) --> T1) t1 0 |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
257 |
(Type (@{type_name fun}, Ts1)), t2) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
258 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
259 |
| t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
260 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
261 |
val t1 = do_term new_Ts old_Ts Neut t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
262 |
val T1 = fastype_of1 (new_Ts, t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
263 |
val (s1, Ts1) = dest_Type T1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
264 |
val t2 = do_term new_Ts old_Ts Neut t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
265 |
val T2 = fastype_of1 (new_Ts, t2) |
35384 | 266 |
val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
267 |
in |
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
268 |
s_betapply new_Ts (if s1 = @{type_name fun} then |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
269 |
t1 |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
270 |
else |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
271 |
select_nth_constr_arg ctxt stds |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
272 |
(@{const_name FunBox}, |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
273 |
Type (@{type_name fun}, Ts1) --> T1) t1 0 |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
274 |
(Type (@{type_name fun}, Ts1)), t2) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
275 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
276 |
| Free (s, T) => Free (s, box_type hol_ctxt InExpr T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
277 |
| Var (z as (x, T)) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
278 |
Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
279 |
else box_type hol_ctxt InExpr T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
280 |
| Bound _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
281 |
| Abs (s, T, t') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
282 |
Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
283 |
in do_term [] [] Pos orig_t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
284 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
285 |
(** Destruction of constructors **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
286 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
287 |
val val_var_prefix = nitpick_prefix ^ "v" |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
288 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
289 |
fun fresh_value_var Ts k n j t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
290 |
Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
291 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
292 |
fun has_heavy_bounds_or_vars Ts t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
293 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
294 |
fun aux [] = false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
295 |
| aux [T] = is_fun_type T orelse is_pair_type T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
296 |
| aux _ = true |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
297 |
in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
298 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
299 |
fun pull_out_constr_comb ({ctxt, stds, ...} : hol_context) Ts relax k level t |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
300 |
args seen = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
301 |
let val t_comb = list_comb (t, args) in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
302 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
303 |
Const x => |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
304 |
if not relax andalso is_constr ctxt stds x andalso |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
305 |
not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
306 |
has_heavy_bounds_or_vars Ts t_comb andalso |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
307 |
not (loose_bvar (t_comb, level)) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
308 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
309 |
val (j, seen) = case find_index (curry (op =) t_comb) seen of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
310 |
~1 => (0, t_comb :: seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
311 |
| j => (j, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
312 |
in (fresh_value_var Ts k (length seen) j t_comb, seen) end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
313 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
314 |
(t_comb, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
315 |
| _ => (t_comb, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
316 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
317 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
318 |
fun equations_for_pulled_out_constrs mk_eq Ts k seen = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
319 |
let val n = length seen in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
320 |
map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
321 |
(index_seq 0 n) seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
322 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
323 |
|
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
324 |
fun pull_out_universal_constrs hol_ctxt def t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
325 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
326 |
val k = maxidx_of_term t + 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
327 |
fun do_term Ts def t args seen = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
328 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
329 |
(t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
330 |
do_eq_or_imp Ts true def t0 t1 t2 seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
331 |
| (t0 as @{const "==>"}) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
332 |
if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
333 |
| (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
334 |
do_eq_or_imp Ts true def t0 t1 t2 seen |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset
|
335 |
| (t0 as @{const HOL.implies}) $ t1 $ t2 => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
336 |
do_eq_or_imp Ts false def t0 t1 t2 seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
337 |
| Abs (s, T, t') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
338 |
let val (t', seen) = do_term (T :: Ts) def t' [] seen in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
339 |
(list_comb (Abs (s, T, t'), args), seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
340 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
341 |
| t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
342 |
let val (t2, seen) = do_term Ts def t2 [] seen in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
343 |
do_term Ts def t1 (t2 :: args) seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
344 |
end |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
345 |
| _ => pull_out_constr_comb hol_ctxt Ts def k 0 t args seen |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
346 |
and do_eq_or_imp Ts eq def t0 t1 t2 seen = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
347 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
348 |
val (t2, seen) = if eq andalso def then (t2, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
349 |
else do_term Ts false t2 [] seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
350 |
val (t1, seen) = do_term Ts false t1 [] seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
351 |
in (t0 $ t1 $ t2, seen) end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
352 |
val (concl, seen) = do_term [] def t [] [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
353 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
354 |
Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
355 |
seen, concl) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
356 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
357 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
358 |
fun mk_exists v t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
359 |
HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
360 |
|
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
361 |
fun pull_out_existential_constrs hol_ctxt t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
362 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
363 |
val k = maxidx_of_term t + 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
364 |
fun aux Ts num_exists t args seen = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
365 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
366 |
(t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
367 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
368 |
val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
369 |
val n = length seen' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
370 |
fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
371 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
372 |
(equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
373 |
|> List.foldl s_conj t1 |> fold mk_exists (vars ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
374 |
|> curry3 Abs s1 T1 |> curry (op $) t0, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
375 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
376 |
| t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
377 |
let val (t2, seen) = aux Ts num_exists t2 [] seen in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
378 |
aux Ts num_exists t1 (t2 :: args) seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
379 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
380 |
| Abs (s, T, t') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
381 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
382 |
val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
383 |
in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
384 |
| _ => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
385 |
if num_exists > 0 then |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
386 |
pull_out_constr_comb hol_ctxt Ts false k num_exists t args seen |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
387 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
388 |
(list_comb (t, args), seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
389 |
in aux [] 0 t [] [] |> fst end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
390 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
391 |
fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
392 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
393 |
val num_occs_of_var = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
394 |
fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
395 |
| _ => I) t (K 0) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
396 |
fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
397 |
aux_eq careful true t0 t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
398 |
| aux careful ((t0 as @{const "==>"}) $ t1 $ t2) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
399 |
t0 $ aux false t1 $ aux careful t2 |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
400 |
| aux careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
401 |
aux_eq careful true t0 t1 t2 |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset
|
402 |
| aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
403 |
t0 $ aux false t1 $ aux careful t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
404 |
| aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
405 |
| aux careful (t1 $ t2) = aux careful t1 $ aux careful t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
406 |
| aux _ t = t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
407 |
and aux_eq careful pass1 t0 t1 t2 = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
408 |
((if careful then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
409 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
410 |
else if axiom andalso is_Var t2 andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
411 |
num_occs_of_var (dest_Var t2) = 1 then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
412 |
@{const True} |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
413 |
else case strip_comb t2 of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
414 |
(* The first case is not as general as it could be. *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
415 |
(Const (@{const_name PairBox}, _), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
416 |
[Const (@{const_name fst}, _) $ Var z1, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
417 |
Const (@{const_name snd}, _) $ Var z2]) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
418 |
if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True} |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
419 |
else raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
420 |
| (Const (x as (s, T)), args) => |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
421 |
let |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
422 |
val (arg_Ts, dataT) = strip_type T |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
423 |
val n = length arg_Ts |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
424 |
in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
425 |
if length args = n andalso |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
426 |
(is_constr ctxt stds x orelse s = @{const_name Pair} orelse |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
427 |
x = (@{const_name Suc}, nat_T --> nat_T)) andalso |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
428 |
(not careful orelse not (is_Var t1) orelse |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
429 |
String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then |
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
430 |
s_let "l" (n + 1) dataT bool_T |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
431 |
(fn t1 => discriminate_value hol_ctxt x t1 :: |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
432 |
map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
433 |
|> foldr1 s_conj) t1 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
434 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
435 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
436 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
437 |
| _ => raise SAME ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
438 |
|> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
439 |
handle SAME () => if pass1 then aux_eq careful false t0 t2 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
440 |
else t0 $ aux false t2 $ aux false t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
441 |
and sel_eq x t n nth_T nth_t = |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
442 |
HOLogic.eq_const nth_T $ nth_t |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
443 |
$ select_nth_constr_arg ctxt stds x t n nth_T |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
444 |
|> aux false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
445 |
in aux axiom t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
446 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
447 |
(** Destruction of universal and existential equalities **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
448 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
449 |
fun curry_assms (@{const "==>"} $ (@{const Trueprop} |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
450 |
$ (@{const HOL.conj} $ t1 $ t2)) $ t3) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
451 |
curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
452 |
| curry_assms (@{const "==>"} $ t1 $ t2) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
453 |
@{const "==>"} $ curry_assms t1 $ curry_assms t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
454 |
| curry_assms t = t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
455 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
456 |
val destroy_universal_equalities = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
457 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
458 |
fun aux prems zs t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
459 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
460 |
@{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
461 |
| _ => Logic.list_implies (rev prems, t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
462 |
and aux_implies prems zs t1 t2 = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
463 |
case t1 of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
464 |
Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2 |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
465 |
| @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
466 |
aux_eq prems zs z t' t1 t2 |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
467 |
| @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
468 |
aux_eq prems zs z t' t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
469 |
| _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
470 |
and aux_eq prems zs z t' t1 t2 = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
471 |
if not (member (op =) zs z) andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
472 |
not (exists_subterm (curry (op =) (Var z)) t') then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
473 |
aux prems zs (subst_free [(Var z, t')] t2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
474 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
475 |
aux (t1 :: prems) (Term.add_vars t1 zs) t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
476 |
in aux [] [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
477 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
478 |
fun find_bound_assign ctxt stds j = |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
479 |
let |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
480 |
fun do_term _ [] = NONE |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
481 |
| do_term seen (t :: ts) = |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
482 |
let |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
483 |
fun do_eq pass1 t1 t2 = |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
484 |
(if loose_bvar1 (t2, j) then |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
485 |
if pass1 then do_eq false t2 t1 else raise SAME () |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
486 |
else case t1 of |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
487 |
Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME () |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
488 |
| Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' => |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
489 |
if j' = j andalso |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
490 |
s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
491 |
SOME (construct_value ctxt stds |
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
492 |
(@{const_name FunBox}, T2 --> T1) [t2], |
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
493 |
ts @ seen) |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
494 |
else |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
495 |
raise SAME () |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
496 |
| _ => raise SAME ()) |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
497 |
handle SAME () => do_term (t :: seen) ts |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
498 |
in |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
499 |
case t of |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
500 |
Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_eq true t1 t2 |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
501 |
| _ => do_term (t :: seen) ts |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
502 |
end |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
503 |
in do_term end |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
504 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
505 |
fun subst_one_bound j arg t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
506 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
507 |
fun aux (Bound i, lev) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
508 |
if i < lev then raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
509 |
else if i = lev then incr_boundvars (lev - j) arg |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
510 |
else Bound (i - 1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
511 |
| aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
512 |
| aux (f $ t, lev) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
513 |
(aux (f, lev) $ (aux (t, lev) handle SAME () => t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
514 |
handle SAME () => f $ aux (t, lev)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
515 |
| aux _ = raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
516 |
in aux (t, j) handle SAME () => t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
517 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
518 |
fun destroy_existential_equalities ({ctxt, stds, ...} : hol_context) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
519 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
520 |
fun kill [] [] ts = foldr1 s_conj ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
521 |
| kill (s :: ss) (T :: Ts) ts = |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
522 |
(case find_bound_assign ctxt stds (length ss) [] ts of |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
523 |
SOME (_, []) => @{const True} |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
524 |
| SOME (arg_t, ts) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
525 |
kill ss Ts (map (subst_one_bound (length ss) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
526 |
(incr_bv (~1, length ss + 1, arg_t))) ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
527 |
| NONE => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
528 |
Const (@{const_name Ex}, (T --> bool_T) --> bool_T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
529 |
$ Abs (s, T, kill ss Ts ts)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
530 |
| kill _ _ _ = raise UnequalLengths |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
531 |
fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
532 |
gather (ss @ [s1]) (Ts @ [T1]) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
533 |
| gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
534 |
| gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
535 |
| gather [] [] t = t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
536 |
| gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
537 |
in gather [] [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
538 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
539 |
(** Skolemization **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
540 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
541 |
fun skolem_prefix_for k j = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
542 |
skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
543 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
544 |
fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...}) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
545 |
skolem_depth = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
546 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
547 |
val incrs = map (Integer.add 1) |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
548 |
fun aux ss Ts js skolemizable polar t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
549 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
550 |
fun do_quantifier quant_s quant_T abs_s abs_T t = |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
551 |
(if not (loose_bvar1 (t, 0)) then |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
552 |
aux ss Ts js skolemizable polar (incr_boundvars ~1 t) |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
553 |
else if is_positive_existential polar quant_s then |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
554 |
let |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
555 |
val j = length (!skolems) + 1 |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
556 |
val (js', (ss', Ts')) = |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
557 |
js ~~ (ss ~~ Ts) |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
558 |
|> filter (fn (j, _) => loose_bvar1 (t, j + 1)) |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
559 |
|> ListPair.unzip ||> ListPair.unzip |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
560 |
in |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
561 |
if skolemizable andalso length js' <= skolem_depth then |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
562 |
let |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
563 |
val sko_s = skolem_prefix_for (length js') j ^ abs_s |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
564 |
val _ = Unsynchronized.change skolems (cons (sko_s, ss')) |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
565 |
val sko_t = list_comb (Const (sko_s, rev Ts' ---> abs_T), |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
566 |
map Bound (rev js')) |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
567 |
val abs_t = Abs (abs_s, abs_T, |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
568 |
aux ss Ts (incrs js) skolemizable polar t) |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
569 |
in |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
570 |
if null js' then |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
571 |
s_betapply Ts (abs_t, sko_t) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
572 |
else |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
573 |
Const (@{const_name Let}, abs_T --> quant_T) $ sko_t |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
574 |
$ abs_t |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
575 |
end |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
576 |
else |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
577 |
raise SAME () |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
578 |
end |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
579 |
else |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
580 |
raise SAME ()) |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
581 |
handle SAME () => |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
582 |
Const (quant_s, quant_T) |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
583 |
$ Abs (abs_s, abs_T, |
38166
28bb89672cc7
fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
blanchet
parents:
38165
diff
changeset
|
584 |
aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js) |
28bb89672cc7
fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
blanchet
parents:
38165
diff
changeset
|
585 |
(skolemizable andalso |
28bb89672cc7
fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
blanchet
parents:
38165
diff
changeset
|
586 |
not (is_higher_order_type abs_T)) polar t) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
587 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
588 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
589 |
Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
590 |
do_quantifier s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
591 |
| @{const "==>"} $ t1 $ t2 => |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
592 |
@{const "==>"} $ aux ss Ts js skolemizable (flip_polarity polar) t1 |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
593 |
$ aux ss Ts js skolemizable polar t2 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
594 |
| @{const Pure.conjunction} $ t1 $ t2 => |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
595 |
@{const Pure.conjunction} $ aux ss Ts js skolemizable polar t1 |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
596 |
$ aux ss Ts js skolemizable polar t2 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
597 |
| @{const Trueprop} $ t1 => |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
598 |
@{const Trueprop} $ aux ss Ts js skolemizable polar t1 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
599 |
| @{const Not} $ t1 => |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
600 |
@{const Not} $ aux ss Ts js skolemizable (flip_polarity polar) t1 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
601 |
| Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
602 |
do_quantifier s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
603 |
| Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
604 |
do_quantifier s0 T0 s1 T1 t1 |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
605 |
| @{const HOL.conj} $ t1 $ t2 => |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
606 |
s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2)) |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
607 |
| @{const HOL.disj} $ t1 $ t2 => |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
608 |
s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2)) |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset
|
609 |
| @{const HOL.implies} $ t1 $ t2 => |
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset
|
610 |
@{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1 |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
611 |
$ aux ss Ts js skolemizable polar t2 |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
612 |
| (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 => |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
613 |
t0 $ t1 $ aux ss Ts js skolemizable polar t2 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
614 |
| Const (x as (s, T)) => |
38205
37a7272cb453
handle inductive predicates correctly after change in "def" semantics
blanchet
parents:
38204
diff
changeset
|
615 |
if is_real_inductive_pred hol_ctxt x andalso |
37a7272cb453
handle inductive predicates correctly after change in "def" semantics
blanchet
parents:
38204
diff
changeset
|
616 |
not (is_real_equational_fun hol_ctxt x) andalso |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
617 |
not (is_well_founded_inductive_pred hol_ctxt x) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
618 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
619 |
val gfp = (fixpoint_kind_of_const thy def_table x = Gfp) |
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
620 |
val (pref, connective) = |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
621 |
if gfp then (lbfp_prefix, @{const HOL.disj}) |
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
622 |
else (ubfp_prefix, @{const HOL.conj}) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
623 |
fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
624 |
|> aux ss Ts js skolemizable polar |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
625 |
fun neg () = Const (pref ^ s, T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
626 |
in |
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
627 |
case polar |> gfp ? flip_polarity of |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
628 |
Pos => pos () |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
629 |
| Neg => neg () |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
630 |
| Neut => |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
631 |
let |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
632 |
val arg_Ts = binder_types T |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
633 |
fun app f = |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
634 |
list_comb (f (), map Bound (length arg_Ts - 1 downto 0)) |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
635 |
in |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
636 |
List.foldr absdummy (connective $ app pos $ app neg) arg_Ts |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
637 |
end |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
638 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
639 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
640 |
Const x |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
641 |
| t1 $ t2 => |
38166
28bb89672cc7
fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
blanchet
parents:
38165
diff
changeset
|
642 |
s_betapply Ts (aux ss Ts js false polar t1, |
28bb89672cc7
fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
blanchet
parents:
38165
diff
changeset
|
643 |
aux ss Ts js false Neut t2) |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
644 |
| Abs (s, T, t1) => |
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
645 |
Abs (s, T, aux ss Ts (incrs js) skolemizable polar t1) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
646 |
| _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
647 |
end |
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
648 |
in aux [] [] [] true Pos end |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
649 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
650 |
(** Function specialization **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
651 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
652 |
fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
653 |
| params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1 |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
654 |
| params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
655 |
snd (strip_comb t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
656 |
| params_in_equation _ = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
657 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
658 |
fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
659 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
660 |
val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
661 |
+ 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
662 |
val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
663 |
val fixed_params = filter_indices fixed_js (params_in_equation t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
664 |
fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
665 |
| aux args (t1 $ t2) = aux (aux [] t2 :: args) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
666 |
| aux args t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
667 |
if t = Const x then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
668 |
list_comb (Const x', extra_args @ filter_out_indices fixed_js args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
669 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
670 |
let val j = find_index (curry (op =) t) fixed_params in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
671 |
list_comb (if j >= 0 then nth fixed_args j else t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
672 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
673 |
in aux [] t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
674 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
675 |
fun static_args_in_term ({ersatz_table, ...} : hol_context) x t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
676 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
677 |
fun fun_calls (Abs (_, _, t)) _ = fun_calls t [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
678 |
| fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
679 |
| fun_calls t args = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
680 |
(case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
681 |
Const (x' as (s', T')) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
682 |
x = x' orelse (case AList.lookup (op =) ersatz_table s' of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
683 |
SOME s'' => x = (s'', T') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
684 |
| NONE => false) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
685 |
| _ => false) ? cons args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
686 |
fun call_sets [] [] vs = [vs] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
687 |
| call_sets [] uss vs = vs :: call_sets uss [] [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
688 |
| call_sets ([] :: _) _ _ = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
689 |
| call_sets ((t :: ts) :: tss) uss vs = |
39687 | 690 |
Ord_List.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
691 |
val sets = call_sets (fun_calls t [] []) [] [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
692 |
val indexed_sets = sets ~~ (index_seq 0 (length sets)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
693 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
694 |
fold_rev (fn (set, j) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
695 |
case set of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
696 |
[Var _] => AList.lookup (op =) indexed_sets set = SOME j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
697 |
? cons (j, NONE) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
698 |
| [t as Const _] => cons (j, SOME t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
699 |
| [t as Free _] => cons (j, SOME t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
700 |
| _ => I) indexed_sets [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
701 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
702 |
fun static_args_in_terms hol_ctxt x = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
703 |
map (static_args_in_term hol_ctxt x) |
39687 | 704 |
#> fold1 (Ord_List.inter (prod_ord int_ord (option_ord Term_Ord.term_ord))) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
705 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
706 |
fun overlapping_indices [] _ = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
707 |
| overlapping_indices _ [] = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
708 |
| overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
709 |
if j1 < j2 then overlapping_indices ps1' ps2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
710 |
else if j1 > j2 then overlapping_indices ps1 ps2' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
711 |
else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
712 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
713 |
fun is_eligible_arg Ts t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
714 |
let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
715 |
null bad_Ts orelse |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
716 |
(is_higher_order_type (fastype_of1 (Ts, t)) andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
717 |
forall (not o is_higher_order_type) bad_Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
718 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
719 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
720 |
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
721 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
722 |
(* If a constant's definition is picked up deeper than this threshold, we |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
723 |
prevent excessive specialization by not specializing it. *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
724 |
val special_max_depth = 20 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
725 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
726 |
val bound_var_prefix = "b" |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
727 |
|
38165
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset
|
728 |
fun special_fun_aconv ((x1, js1, ts1), (x2, js2, ts2)) = |
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset
|
729 |
x1 = x2 andalso js1 = js2 andalso length ts1 = length ts2 andalso |
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset
|
730 |
forall (op aconv) (ts1 ~~ ts2) |
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset
|
731 |
|
38204 | 732 |
fun specialize_consts_in_term |
39359 | 733 |
(hol_ctxt as {ctxt, thy, stds, specialize, def_table, simp_table, |
734 |
special_funs, ...}) def depth t = |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
735 |
if not specialize orelse depth > special_max_depth then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
736 |
t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
737 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
738 |
let |
38206 | 739 |
val blacklist = |
740 |
if def then case term_under_def t of Const x => [x] | _ => [] else [] |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
741 |
fun aux args Ts (Const (x as (s, T))) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
742 |
((if not (member (op =) blacklist x) andalso not (null args) andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
743 |
not (String.isPrefix special_prefix s) andalso |
39359 | 744 |
not (is_built_in_const thy stds x) andalso |
38204 | 745 |
(is_equational_fun_but_no_plain_def hol_ctxt x orelse |
746 |
(is_some (def_of_const thy def_table x) andalso |
|
747 |
not (is_of_class_const thy x) andalso |
|
748 |
not (is_constr ctxt stds x) andalso |
|
749 |
not (is_choice_spec_fun hol_ctxt x))) then |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
750 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
751 |
val eligible_args = filter (is_eligible_arg Ts o snd) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
752 |
(index_seq 0 (length args) ~~ args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
753 |
val _ = not (null eligible_args) orelse raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
754 |
val old_axs = equational_fun_axioms hol_ctxt x |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
755 |
|> map (destroy_existential_equalities hol_ctxt) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
756 |
val static_params = static_args_in_terms hol_ctxt x old_axs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
757 |
val fixed_js = overlapping_indices static_params eligible_args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
758 |
val _ = not (null fixed_js) orelse raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
759 |
val fixed_args = filter_indices fixed_js args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
760 |
val vars = fold Term.add_vars fixed_args [] |
35408 | 761 |
|> sort (Term_Ord.fast_indexname_ord o pairself fst) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
762 |
val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
763 |
fixed_args [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
764 |
|> sort int_ord |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
765 |
val live_args = filter_out_indices fixed_js args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
766 |
val extra_args = map Var vars @ map Bound bound_js @ live_args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
767 |
val extra_Ts = map snd vars @ filter_indices bound_js Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
768 |
val k = maxidx_of_term t + 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
769 |
fun var_for_bound_no j = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
770 |
Var ((bound_var_prefix ^ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
771 |
nat_subscript (find_index (curry (op =) j) bound_js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
772 |
+ 1), k), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
773 |
nth Ts j) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
774 |
val fixed_args_in_axiom = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
775 |
map (curry subst_bounds |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
776 |
(map var_for_bound_no (index_seq 0 (length Ts)))) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
777 |
fixed_args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
778 |
in |
38165
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset
|
779 |
case AList.lookup special_fun_aconv (!special_funs) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
780 |
(x, fixed_js, fixed_args_in_axiom) of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
781 |
SOME x' => list_comb (Const x', extra_args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
782 |
| NONE => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
783 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
784 |
val extra_args_in_axiom = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
785 |
map Var vars @ map var_for_bound_no bound_js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
786 |
val x' as (s', _) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
787 |
(special_prefix_for (length (!special_funs) + 1) ^ s, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
788 |
extra_Ts @ filter_out_indices fixed_js (binder_types T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
789 |
---> body_type T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
790 |
val new_axs = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
791 |
map (specialize_fun_axiom x x' fixed_js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
792 |
fixed_args_in_axiom extra_args_in_axiom) old_axs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
793 |
val _ = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
794 |
Unsynchronized.change special_funs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
795 |
(cons ((x, fixed_js, fixed_args_in_axiom), x')) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
796 |
val _ = add_simps simp_table s' new_axs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
797 |
in list_comb (Const x', extra_args) end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
798 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
799 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
800 |
raise SAME ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
801 |
handle SAME () => list_comb (Const x, args)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
802 |
| aux args Ts (Abs (s, T, t)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
803 |
list_comb (Abs (s, T, aux [] (T :: Ts) t), args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
804 |
| aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
805 |
| aux args _ t = list_comb (t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
806 |
in aux [] [] t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
807 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
808 |
type special_triple = int list * term list * styp |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
809 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
810 |
val cong_var_prefix = "c" |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
811 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
812 |
fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
813 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
814 |
val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
815 |
val Ts = binder_types T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
816 |
val max_j = fold (fold Integer.max) [js1, js2] ~1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
817 |
val (eqs, (args1, args2)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
818 |
fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
819 |
(js1 ~~ ts1, js2 ~~ ts2) of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
820 |
(SOME t1, SOME t2) => apfst (cons (t1, t2)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
821 |
| (SOME t1, NONE) => apsnd (apsnd (cons t1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
822 |
| (NONE, SOME t2) => apsnd (apfst (cons t2)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
823 |
| (NONE, NONE) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
824 |
let val v = Var ((cong_var_prefix ^ nat_subscript j, 0), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
825 |
nth Ts j) in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
826 |
apsnd (pairself (cons v)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
827 |
end) (max_j downto 0) ([], ([], [])) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
828 |
in |
38165
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset
|
829 |
Logic.list_implies (eqs |> filter_out (op aconv) |> distinct (op =) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
830 |
|> map Logic.mk_equals, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
831 |
Logic.mk_equals (list_comb (Const x1, bounds1 @ args1), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
832 |
list_comb (Const x2, bounds2 @ args2))) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
833 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
834 |
|
38170 | 835 |
fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) ts = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
836 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
837 |
val groups = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
838 |
!special_funs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
839 |
|> map (fn ((x, js, ts), x') => (x, (js, ts, x'))) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
840 |
|> AList.group (op =) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
841 |
|> filter_out (is_equational_fun_surely_complete hol_ctxt o fst) |
38170 | 842 |
|> map (fn (x, zs) => |
843 |
(x, zs |> member (op =) ts (Const x) ? cons ([], [], x))) |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
844 |
fun generality (js, _, _) = ~(length js) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
845 |
fun is_more_specific (j1, t1, x1) (j2, t2, x2) = |
38165
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset
|
846 |
x1 <> x2 andalso length j2 < length j1 andalso |
39687 | 847 |
Ord_List.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
848 |
fun do_pass_1 _ [] [_] [_] = I |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
849 |
| do_pass_1 T skipped _ [] = do_pass_2 T skipped |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
850 |
| do_pass_1 T skipped all (z :: zs) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
851 |
case filter (is_more_specific z) all |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
852 |
|> sort (int_ord o pairself generality) of |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
853 |
[] => do_pass_1 T (z :: skipped) all zs |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
854 |
| (z' :: _) => cons (special_congruence_axiom T z z') |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
855 |
#> do_pass_1 T skipped all zs |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
856 |
and do_pass_2 _ [] = I |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
857 |
| do_pass_2 T (z :: zs) = |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
858 |
fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
859 |
in fold (fn ((_, T), zs) => do_pass_1 T [] zs zs) groups [] end |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
860 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
861 |
(** Axiom selection **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
862 |
|
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
863 |
fun defined_free_by_assumption t = |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
864 |
let |
38170 | 865 |
fun do_equals x def = |
866 |
if exists_subterm (curry (op aconv) (Free x)) def then NONE else SOME x |
|
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
867 |
in |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
868 |
case t of |
38170 | 869 |
Const (@{const_name "=="}, _) $ Free x $ def => do_equals x def |
870 |
| @{const Trueprop} $ (Const (@{const_name "=="}, _) $ Free x $ def) => |
|
871 |
do_equals x def |
|
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
872 |
| _ => NONE |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
873 |
end |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
874 |
|
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
875 |
fun assumption_exclusively_defines_free assm_ts t = |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
876 |
case defined_free_by_assumption t of |
38170 | 877 |
SOME x => |
878 |
length (filter ((fn SOME x' => x = x' | NONE => false) |
|
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
879 |
o defined_free_by_assumption) assm_ts) = 1 |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
880 |
| NONE => false |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
881 |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
882 |
fun all_table_entries table = Symtab.fold (append o snd) table [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
883 |
fun extra_table table s = Symtab.make [(s, all_table_entries table)] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
884 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
885 |
fun eval_axiom_for_term j t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
886 |
Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
887 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
888 |
val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
889 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
890 |
(* Prevents divergence in case of cyclic or infinite axiom dependencies. *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
891 |
val axioms_max_depth = 255 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
892 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
893 |
fun axioms_for_term |
35311 | 894 |
(hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms, |
39359 | 895 |
evals, def_table, nondef_table, choice_spec_table, |
896 |
user_nondefs, ...}) assm_ts neg_t = |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
897 |
let |
38170 | 898 |
val (def_assm_ts, nondef_assm_ts) = |
899 |
List.partition (assumption_exclusively_defines_free assm_ts) assm_ts |
|
900 |
val def_assm_table = map (`(the o defined_free_by_assumption)) def_assm_ts |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
901 |
type accumulator = styp list * (term list * term list) |
38206 | 902 |
fun add_axiom get app def depth t (accum as (seen, axs)) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
903 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
904 |
val t = t |> unfold_defs_in_term hol_ctxt |
38206 | 905 |
|> skolemize_term_and_more hol_ctxt ~1 (* FIXME: why ~1? *) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
906 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
907 |
if is_trivial_equation t then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
908 |
accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
909 |
else |
38206 | 910 |
let val t' = t |> specialize_consts_in_term hol_ctxt def depth in |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
911 |
if exists (member (op aconv) (get axs)) [t, t'] then accum |
38170 | 912 |
else add_axioms_for_term (depth + 1) t' (seen, app (cons t') axs) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
913 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
914 |
end |
38206 | 915 |
and add_def_axiom depth = add_axiom fst apfst true depth |
916 |
and add_nondef_axiom depth = add_axiom snd apsnd false depth |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
917 |
and add_maybe_def_axiom depth t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
918 |
(if head_of t <> @{const "==>"} then add_def_axiom |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
919 |
else add_nondef_axiom) depth t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
920 |
and add_eq_axiom depth t = |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
921 |
(if is_constr_pattern_formula ctxt t then add_def_axiom |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
922 |
else add_nondef_axiom) depth t |
38170 | 923 |
and add_axioms_for_term depth t (accum as (seen, axs)) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
924 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
925 |
t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
926 |
| Const (x as (s, T)) => |
39359 | 927 |
(if member (op aconv) seen t orelse is_built_in_const thy stds x then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
928 |
accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
929 |
else |
38170 | 930 |
let val accum = (t :: seen, axs) in |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
931 |
if depth > axioms_max_depth then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
932 |
raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
933 |
\add_axioms_for_term", |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
934 |
"too many nested axioms (" ^ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
935 |
string_of_int depth ^ ")") |
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset
|
936 |
else if is_of_class_const thy x then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
937 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
938 |
val class = Logic.class_of_const s |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
939 |
val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
940 |
class) |
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36389
diff
changeset
|
941 |
val ax1 = try (specialize_type thy x) of_class |
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36389
diff
changeset
|
942 |
val ax2 = Option.map (specialize_type thy x o snd) |
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset
|
943 |
(get_class_def thy class) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
944 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
945 |
fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2]) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
946 |
accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
947 |
end |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
948 |
else if is_constr ctxt stds x then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
949 |
accum |
37271 | 950 |
else if is_descr (original_name s) then |
951 |
fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x) |
|
952 |
accum |
|
38202
379fb08da97b
prevent the expansion of too large definitions -- use equations for these instead
blanchet
parents:
38190
diff
changeset
|
953 |
else if is_equational_fun_but_no_plain_def hol_ctxt x then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
954 |
fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
955 |
accum |
35807
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35718
diff
changeset
|
956 |
else if is_choice_spec_fun hol_ctxt x then |
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35718
diff
changeset
|
957 |
fold (add_nondef_axiom depth) |
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35718
diff
changeset
|
958 |
(nondef_props_for_const thy true choice_spec_table x) accum |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
959 |
else if is_abs_fun ctxt x then |
38215
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
960 |
accum |> fold (add_nondef_axiom depth) |
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
961 |
(nondef_props_for_const thy false nondef_table x) |
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset
|
962 |
|> (is_funky_typedef ctxt (range_type T) orelse |
38215
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
963 |
range_type T = nat_T) |
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
964 |
? fold (add_maybe_def_axiom depth) |
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
965 |
(nondef_props_for_const thy true |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
966 |
(extra_table def_table s) x) |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
967 |
else if is_rep_fun ctxt x then |
38215
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
968 |
accum |> fold (add_nondef_axiom depth) |
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
969 |
(nondef_props_for_const thy false nondef_table x) |
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset
|
970 |
|> (is_funky_typedef ctxt (range_type T) orelse |
38215
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
971 |
range_type T = nat_T) |
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
972 |
? fold (add_maybe_def_axiom depth) |
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
973 |
(nondef_props_for_const thy true |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
974 |
(extra_table def_table s) x) |
38215
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
975 |
|> add_axioms_for_term depth |
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
976 |
(Const (mate_of_rep_fun ctxt x)) |
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
977 |
|> fold (add_def_axiom depth) |
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset
|
978 |
(inverse_axioms_for_rep_fun ctxt x) |
37253 | 979 |
else if s = @{const_name TYPE} then |
980 |
accum |
|
38202
379fb08da97b
prevent the expansion of too large definitions -- use equations for these instead
blanchet
parents:
38190
diff
changeset
|
981 |
else case def_of_const thy def_table x of |
39345 | 982 |
SOME _ => |
38202
379fb08da97b
prevent the expansion of too large definitions -- use equations for these instead
blanchet
parents:
38190
diff
changeset
|
983 |
fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) |
379fb08da97b
prevent the expansion of too large definitions -- use equations for these instead
blanchet
parents:
38190
diff
changeset
|
984 |
accum |
379fb08da97b
prevent the expansion of too large definitions -- use equations for these instead
blanchet
parents:
38190
diff
changeset
|
985 |
| NONE => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
986 |
accum |> user_axioms <> SOME false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
987 |
? fold (add_nondef_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
988 |
(nondef_props_for_const thy false nondef_table x) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
989 |
end) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
990 |
|> add_axioms_for_type depth T |
38170 | 991 |
| Free (x as (_, T)) => |
992 |
(if member (op aconv) seen t then |
|
993 |
accum |
|
994 |
else case AList.lookup (op =) def_assm_table x of |
|
995 |
SOME t => add_def_axiom depth t accum |
|
996 |
| NONE => accum) |
|
997 |
|> add_axioms_for_type depth T |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
998 |
| Var (_, T) => add_axioms_for_type depth T accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
999 |
| Bound _ => accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1000 |
| Abs (_, T, t) => accum |> add_axioms_for_term depth t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1001 |
|> add_axioms_for_type depth T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1002 |
and add_axioms_for_type depth T = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1003 |
case T of |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1004 |
Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts |
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
38170
diff
changeset
|
1005 |
| Type (@{type_name prod}, Ts) => fold (add_axioms_for_type depth) Ts |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1006 |
| @{typ prop} => I |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1007 |
| @{typ bool} => I |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1008 |
| TFree (_, S) => add_axioms_for_sort depth T S |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1009 |
| TVar (_, S) => add_axioms_for_sort depth T S |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1010 |
| Type (z as (_, Ts)) => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1011 |
fold (add_axioms_for_type depth) Ts |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1012 |
#> (if is_pure_typedef ctxt T then |
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1013 |
fold (add_maybe_def_axiom depth) (optimized_typedef_axioms ctxt z) |
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset
|
1014 |
else if is_quot_type ctxt T then |
35311 | 1015 |
fold (add_def_axiom depth) |
1016 |
(optimized_quot_type_axioms ctxt stds z) |
|
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset
|
1017 |
else if max_bisim_depth >= 0 andalso is_codatatype ctxt T then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1018 |
fold (add_maybe_def_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1019 |
(codatatype_bisim_axioms hol_ctxt T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1020 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1021 |
I) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1022 |
and add_axioms_for_sort depth T S = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1023 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1024 |
val supers = Sign.complete_sort thy S |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1025 |
val class_axioms = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1026 |
maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1027 |
handle ERROR _ => [])) supers |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1028 |
val monomorphic_class_axioms = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1029 |
map (fn t => case Term.add_tvars t [] of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1030 |
[] => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1031 |
| [(x, S)] => |
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36389
diff
changeset
|
1032 |
monomorphic_term (Vartab.make [(x, (S, T))]) t |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1033 |
| _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1034 |
\add_axioms_for_sort", [t])) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1035 |
class_axioms |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1036 |
in fold (add_nondef_axiom depth) monomorphic_class_axioms end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1037 |
val (mono_user_nondefs, poly_user_nondefs) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1038 |
List.partition (null o Term.hidden_polymorphism) user_nondefs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1039 |
val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1040 |
evals |
38170 | 1041 |
val (seen, (defs, nondefs)) = |
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1042 |
([], ([], [])) |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1043 |
|> add_axioms_for_term 1 neg_t |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1044 |
|> fold_rev (add_nondef_axiom 1) nondef_assm_ts |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1045 |
|> fold_rev (add_def_axiom 1) eval_axioms |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1046 |
|> user_axioms = SOME true ? fold (add_nondef_axiom 1) mono_user_nondefs |
38170 | 1047 |
val defs = defs @ special_congruence_axioms hol_ctxt seen |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1048 |
val got_all_mono_user_axioms = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1049 |
(user_axioms = SOME true orelse null mono_user_nondefs) |
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1050 |
in |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1051 |
(neg_t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs) |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1052 |
end |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1053 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1054 |
(** Simplification of constructor/selector terms **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1055 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1056 |
fun simplify_constrs_and_sels ctxt t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1057 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1058 |
fun is_nth_sel_on t' n (Const (s, _) $ t) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1059 |
(t = t' andalso is_sel_like_and_no_discr s andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1060 |
sel_no_from_name s = n) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1061 |
| is_nth_sel_on _ _ _ = false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1062 |
fun do_term (Const (@{const_name Rep_Frac}, _) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1063 |
$ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1064 |
| do_term (Const (@{const_name Abs_Frac}, _) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1065 |
$ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1066 |
| do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1067 |
| do_term (t as Const (x as (s, T))) (args as _ :: _) = |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1068 |
((if is_constr_like ctxt x then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1069 |
if length args = num_binder_types T then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1070 |
case hd args of |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1071 |
Const (_, T') $ t' => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1072 |
if domain_type T' = body_type T andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1073 |
forall (uncurry (is_nth_sel_on t')) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1074 |
(index_seq 0 (length args) ~~ args) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1075 |
t' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1076 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1077 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1078 |
| _ => raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1079 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1080 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1081 |
else if is_sel_like_and_no_discr s then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1082 |
case strip_comb (hd args) of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1083 |
(Const (x' as (s', T')), ts') => |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1084 |
if is_constr_like ctxt x' andalso |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1085 |
constr_name_for_sel_like s = s' andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1086 |
not (exists is_pair_type (binder_types T')) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1087 |
list_comb (nth ts' (sel_no_from_name s), tl args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1088 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1089 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1090 |
| _ => raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1091 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1092 |
raise SAME ()) |
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1093 |
handle SAME () => s_betapplys [] (t, args)) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1094 |
| do_term (Abs (s, T, t')) args = |
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1095 |
s_betapplys [] (Abs (s, T, do_term t' []), args) |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1096 |
| do_term t args = s_betapplys [] (t, args) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1097 |
in do_term t [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1098 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1099 |
(** Quantifier massaging: Distributing quantifiers **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1100 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1101 |
fun distribute_quantifiers t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1102 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1103 |
(t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1104 |
(case t1 of |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
1105 |
(t10 as @{const HOL.conj}) $ t11 $ t12 => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1106 |
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1107 |
$ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1108 |
| (t10 as @{const Not}) $ t11 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1109 |
t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1110 |
$ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1111 |
| t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1112 |
if not (loose_bvar1 (t1, 0)) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1113 |
distribute_quantifiers (incr_boundvars ~1 t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1114 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1115 |
t0 $ Abs (s, T1, distribute_quantifiers t1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1116 |
| (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1117 |
(case distribute_quantifiers t1 of |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
1118 |
(t10 as @{const HOL.disj}) $ t11 $ t12 => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1119 |
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1120 |
$ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset
|
1121 |
| (t10 as @{const HOL.implies}) $ t11 $ t12 => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1122 |
t10 $ distribute_quantifiers (Const (@{const_name All}, T0) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1123 |
$ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1124 |
$ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1125 |
| (t10 as @{const Not}) $ t11 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1126 |
t10 $ distribute_quantifiers (Const (@{const_name All}, T0) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1127 |
$ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1128 |
| t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1129 |
if not (loose_bvar1 (t1, 0)) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1130 |
distribute_quantifiers (incr_boundvars ~1 t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1131 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1132 |
t0 $ Abs (s, T1, distribute_quantifiers t1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1133 |
| t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1134 |
| Abs (s, T, t') => Abs (s, T, distribute_quantifiers t') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1135 |
| _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1136 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1137 |
(** Quantifier massaging: Pushing quantifiers inward **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1138 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1139 |
fun renumber_bounds j n f t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1140 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1141 |
t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1142 |
| Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1143 |
| Bound j' => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1144 |
Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1145 |
| _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1146 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1147 |
(* Maximum number of quantifiers in a cluster for which the exponential |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1148 |
algorithm is used. Larger clusters use a heuristic inspired by Claessen & |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1149 |
Soerensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1150 |
paper). *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1151 |
val quantifier_cluster_threshold = 7 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1152 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1153 |
val push_quantifiers_inward = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1154 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1155 |
fun aux quant_s ss Ts t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1156 |
(case t of |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1157 |
Const (s0, _) $ Abs (s1, T1, t1 as _ $ _) => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1158 |
if s0 = quant_s then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1159 |
aux s0 (s1 :: ss) (T1 :: Ts) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1160 |
else if quant_s = "" andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1161 |
(s0 = @{const_name All} orelse s0 = @{const_name Ex}) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1162 |
aux s0 [s1] [T1] t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1163 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1164 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1165 |
| _ => raise SAME ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1166 |
handle SAME () => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1167 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1168 |
t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1169 |
if quant_s = "" then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1170 |
aux "" [] [] t1 $ aux "" [] [] t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1171 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1172 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1173 |
val typical_card = 4 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1174 |
fun big_union proj ps = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1175 |
fold (fold (insert (op =)) o proj) ps [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1176 |
val (ts, connective) = strip_any_connective t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1177 |
val T_costs = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1178 |
map (bounded_card_of_type 65536 typical_card []) Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1179 |
val t_costs = map size_of_term ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1180 |
val num_Ts = length Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1181 |
val flip = curry (op -) (num_Ts - 1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1182 |
val t_boundss = map (map flip o loose_bnos) ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1183 |
fun merge costly_boundss [] = costly_boundss |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1184 |
| merge costly_boundss (j :: js) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1185 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1186 |
val (yeas, nays) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1187 |
List.partition (fn (bounds, _) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1188 |
member (op =) bounds j) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1189 |
costly_boundss |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1190 |
val yeas_bounds = big_union fst yeas |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1191 |
val yeas_cost = Integer.sum (map snd yeas) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1192 |
* nth T_costs j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1193 |
in merge ((yeas_bounds, yeas_cost) :: nays) js end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1194 |
val cost = Integer.sum o map snd oo merge |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1195 |
fun heuristically_best_permutation _ [] = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1196 |
| heuristically_best_permutation costly_boundss js = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1197 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1198 |
val (costly_boundss, (j, js)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1199 |
js |> map (`(merge costly_boundss o single)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1200 |
|> sort (int_ord |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1201 |
o pairself (Integer.sum o map snd o fst)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1202 |
|> split_list |>> hd ||> pairf hd tl |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1203 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1204 |
j :: heuristically_best_permutation costly_boundss js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1205 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1206 |
val js = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1207 |
if length Ts <= quantifier_cluster_threshold then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1208 |
all_permutations (index_seq 0 num_Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1209 |
|> map (`(cost (t_boundss ~~ t_costs))) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1210 |
|> sort (int_ord o pairself fst) |> hd |> snd |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1211 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1212 |
heuristically_best_permutation (t_boundss ~~ t_costs) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1213 |
(index_seq 0 num_Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1214 |
val back_js = map (fn j => find_index (curry (op =) j) js) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1215 |
(index_seq 0 num_Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1216 |
val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1217 |
ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1218 |
fun mk_connection [] = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1219 |
raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1220 |
\mk_connection", "") |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1221 |
| mk_connection ts_cum_bounds = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1222 |
ts_cum_bounds |> map fst |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1223 |
|> foldr1 (fn (t1, t2) => connective $ t1 $ t2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1224 |
fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1225 |
| build ts_cum_bounds (j :: js) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1226 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1227 |
val (yeas, nays) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1228 |
List.partition (fn (_, bounds) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1229 |
member (op =) bounds j) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1230 |
ts_cum_bounds |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1231 |
||> map (apfst (incr_boundvars ~1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1232 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1233 |
if null yeas then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1234 |
build nays js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1235 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1236 |
let val T = nth Ts (flip j) in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1237 |
build ((Const (quant_s, (T --> bool_T) --> bool_T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1238 |
$ Abs (nth ss (flip j), T, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1239 |
mk_connection yeas), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1240 |
big_union snd yeas) :: nays) js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1241 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1242 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1243 |
in build (ts ~~ t_boundss) js end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1244 |
| Abs (s, T, t') => Abs (s, T, aux "" [] [] t') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1245 |
| _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1246 |
in aux "" [] [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1247 |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1248 |
(** Inference of finite functions **) |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1249 |
|
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1250 |
fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1251 |
(nondef_ts, def_ts) = |
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1252 |
if forall (curry (op =) (SOME false) o snd) finitizes then |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1253 |
(nondef_ts, def_ts) |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1254 |
else |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1255 |
let |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1256 |
val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1257 |
|> filter_out (fn Type (@{type_name fun_box}, _) => true |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1258 |
| @{typ signed_bit} => true |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1259 |
| @{typ unsigned_bit} => true |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1260 |
| T => is_small_finite_type hol_ctxt T orelse |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1261 |
triple_lookup (type_match thy) monos T |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1262 |
= SOME (SOME false)) |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1263 |
in |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1264 |
fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) |
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset
|
1265 |
end |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1266 |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1267 |
(** Preprocessor entry point **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1268 |
|
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset
|
1269 |
val max_skolem_depth = 3 |
36389
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset
|
1270 |
|
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1271 |
fun preprocess_formulas |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1272 |
(hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes, |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1273 |
...}) finitizes monos assm_ts neg_t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1274 |
let |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1275 |
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) = |
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1276 |
neg_t |> unfold_defs_in_term hol_ctxt |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1277 |
|> close_form |
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1278 |
|> skolemize_term_and_more hol_ctxt max_skolem_depth |
38206 | 1279 |
|> specialize_consts_in_term hol_ctxt false 0 |
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset
|
1280 |
|> axioms_for_term hol_ctxt assm_ts |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1281 |
val binarize = |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1282 |
is_standard_datatype thy stds nat_T andalso |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1283 |
case binary_ints of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1284 |
SOME false => false |
35718 | 1285 |
| _ => forall (may_use_binary_ints false) nondef_ts andalso |
1286 |
forall (may_use_binary_ints true) def_ts andalso |
|
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1287 |
(binary_ints = SOME true orelse |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1288 |
exists should_use_binary_ints (nondef_ts @ def_ts)) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1289 |
val box = exists (not_equal (SOME false) o snd) boxes |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1290 |
val table = |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1291 |
Termtab.empty |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1292 |
|> box ? fold (add_to_uncurry_table ctxt) (nondef_ts @ def_ts) |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1293 |
fun do_rest def = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1294 |
binarize ? binarize_nat_and_int_in_term |
36388 | 1295 |
#> box ? uncurry_term table |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1296 |
#> box ? box_fun_and_pair_in_term hol_ctxt def |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1297 |
#> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1298 |
#> pull_out_existential_constrs hol_ctxt |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1299 |
#> destroy_pulled_out_constrs hol_ctxt def) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1300 |
#> curry_assms |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1301 |
#> destroy_universal_equalities |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1302 |
#> destroy_existential_equalities hol_ctxt |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1303 |
#> simplify_constrs_and_sels ctxt |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1304 |
#> distribute_quantifiers |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1305 |
#> push_quantifiers_inward |
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35070
diff
changeset
|
1306 |
#> close_form |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1307 |
#> Term.map_abs_vars shortest_name |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1308 |
val nondef_ts = map (do_rest false) nondef_ts |
35384 | 1309 |
val def_ts = map (do_rest true) def_ts |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1310 |
val (nondef_ts, def_ts) = |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1311 |
finitize_all_types_of_funs hol_ctxt binarize finitizes monos |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1312 |
(nondef_ts, def_ts) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1313 |
in |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1314 |
(nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1315 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1316 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1317 |
end; |