132 |
132 |
133 |
133 |
134 |
134 |
135 (* preprocessing *) |
135 (* preprocessing *) |
136 |
136 |
137 (** FIXME **) |
137 (** datatype declarations **) |
138 |
|
139 local |
|
140 (* |
|
141 force eta-expansion for constructors and selectors, |
|
142 add missing datatype selectors via hypothetical definitions, |
|
143 also return necessary datatype and record theorems |
|
144 *) |
|
145 in |
|
146 |
138 |
147 fun collect_datatypes_and_records (tr_context, ctxt) ts = |
139 fun collect_datatypes_and_records (tr_context, ctxt) ts = |
148 (([], tr_context, ctxt), ts) |
140 let |
149 |
141 val (declss, ctxt') = |
150 end |
142 fold (Term.fold_types SMT_Datatypes.add_decls) ts ([], ctxt) |
|
143 |
|
144 fun is_decl_typ T = exists (exists (equal T o fst)) declss |
|
145 |
|
146 fun add_typ' T proper = |
|
147 (case SMT_Builtin.dest_builtin_typ ctxt' T of |
|
148 SOME n => pair n |
|
149 | NONE => add_typ T proper) |
|
150 |
|
151 fun tr_select sel = |
|
152 let val T = Term.range_type (Term.fastype_of sel) |
|
153 in add_fun sel NONE ##>> add_typ' T (not (is_decl_typ T)) end |
|
154 fun tr_constr (constr, selects) = |
|
155 add_fun constr NONE ##>> fold_map tr_select selects |
|
156 fun tr_typ (T, cases) = add_typ' T false ##>> fold_map tr_constr cases |
|
157 val (declss', tr_context') = fold_map (fold_map tr_typ) declss tr_context |
|
158 |
|
159 fun add (constr, selects) = |
|
160 Termtab.update (constr, length selects) #> |
|
161 fold (Termtab.update o rpair 1) selects |
|
162 val funcs = fold (fold (fold add o snd)) declss Termtab.empty |
|
163 |
|
164 in ((funcs, declss', tr_context', ctxt'), ts) end |
|
165 (* FIXME: also return necessary datatype and record theorems *) |
151 |
166 |
152 |
167 |
153 (** eta-expand quantifiers, let expressions and built-ins *) |
168 (** eta-expand quantifiers, let expressions and built-ins *) |
154 |
169 |
155 local |
170 local |
172 |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts |
187 |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts |
173 |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts |
188 |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts |
174 end |
189 end |
175 in |
190 in |
176 |
191 |
177 fun eta_expand ctxt = |
192 fun eta_expand ctxt funcs = |
178 let |
193 let |
|
194 fun exp_func t T ts = |
|
195 (case Termtab.lookup funcs t of |
|
196 SOME k => |
|
197 Term.list_comb (t, ts) |
|
198 |> k <> length ts ? expf k (length ts) T |
|
199 | NONE => Term.list_comb (t, ts)) |
|
200 |
179 fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a |
201 fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a |
180 | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t |
202 | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t |
181 | expand (q as Const (@{const_name All}, T)) = exp2 T q |
203 | expand (q as Const (@{const_name All}, T)) = exp2 T q |
182 | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a |
204 | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a |
183 | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp T t |
205 | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp T t |
194 (u as Const (c as (_, T)), ts) => |
216 (u as Const (c as (_, T)), ts) => |
195 (case SMT_Builtin.dest_builtin ctxt c ts of |
217 (case SMT_Builtin.dest_builtin ctxt c ts of |
196 SOME (_, k, us, mk) => |
218 SOME (_, k, us, mk) => |
197 if k = length us then mk (map expand us) |
219 if k = length us then mk (map expand us) |
198 else expf k (length ts) T (mk (map expand us)) |
220 else expf k (length ts) T (mk (map expand us)) |
199 | NONE => Term.list_comb (u, map expand ts)) |
221 | NONE => exp_func u T (map expand ts)) |
|
222 | (u as Free (_, T), ts) => exp_func u T (map expand ts) |
200 | (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts) |
223 | (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts) |
201 | (u, ts) => Term.list_comb (u, map expand ts)) |
224 | (u, ts) => Term.list_comb (u, map expand ts)) |
202 |
225 |
203 and abs_expand (n, T, t) = Abs (n, T, expand t) |
226 and abs_expand (n, T, t) = Abs (n, T, expand t) |
204 |
227 |
528 val {prefixes, is_fol, header, has_datatypes, serialize} = get_config ctxt |
551 val {prefixes, is_fol, header, has_datatypes, serialize} = get_config ctxt |
529 |
552 |
530 val with_datatypes = |
553 val with_datatypes = |
531 has_datatypes andalso Config.get ctxt SMT_Config.datatypes |
554 has_datatypes andalso Config.get ctxt SMT_Config.datatypes |
532 |
555 |
533 fun no_dtyps (tr_context, ctxt) ts = (([], tr_context, ctxt), ts) |
556 fun no_dtyps (tr_context, ctxt) ts = |
|
557 ((Termtab.empty, [], tr_context, ctxt), ts) |
534 |
558 |
535 val ts1 = map (Envir.beta_eta_contract o SMT_Utils.prop_of o snd) ithms |
559 val ts1 = map (Envir.beta_eta_contract o SMT_Utils.prop_of o snd) ithms |
536 |
560 |
537 val ((dtyps, tr_context, ctxt1), ts2) = |
561 val ((funcs, dtyps, tr_context, ctxt1), ts2) = |
538 ((make_tr_context prefixes, ctxt), ts1) |
562 ((make_tr_context prefixes, ctxt), ts1) |
539 |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps) |
563 |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps) |
540 |
564 |
541 val (ctxt2, ts3) = |
565 val (ctxt2, ts3) = |
542 ts2 |
566 ts2 |
543 |> eta_expand ctxt1 |
567 |> eta_expand ctxt1 funcs |
544 |> lift_lambdas ctxt1 |
568 |> lift_lambdas ctxt1 |
545 ||> intro_explicit_application |
569 ||> intro_explicit_application |
546 |
570 |
547 val ((rewrite_rules, extra_thms, builtin), ts4) = |
571 val ((rewrite_rules, extra_thms, builtin), ts4) = |
548 (if is_fol then folify ctxt2 else pair ([], [], I)) ts3 |
572 (if is_fol then folify ctxt2 else pair ([], [], I)) ts3 |