--- a/src/HOL/Tools/SMT/smt_translate.ML Tue Jun 20 17:28:17 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Tue Jun 20 17:31:29 2017 +0200
@@ -12,7 +12,6 @@
datatype sterm =
SVar of int |
SApp of string * sterm list |
- SLet of string * sterm * sterm |
SQua of squant * string list * sterm spattern list * sterm
(*translation configuration*)
@@ -47,12 +46,12 @@
datatype squant = SForall | SExists
-datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
+datatype 'a spattern =
+ SPat of 'a list | SNoPat of 'a list
datatype sterm =
SVar of int |
SApp of string * sterm list |
- SLet of string * sterm * sterm |
SQua of squant * string list * sterm spattern list * sterm
@@ -204,7 +203,6 @@
| expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a
| expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t
| expand (q as Const (@{const_name Ex}, T)) = exp2 T q
- | expand (Const (@{const_name Let}, _) $ t $ u) = expand (Term.betapply (u, t))
| expand (Const (@{const_name Let}, T) $ t) =
let val U = Term.domain_type (Term.range_type T)
in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end
@@ -213,7 +211,9 @@
in Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U, Bound 0 $ Bound 1)) end
| expand t =
(case Term.strip_comb t of
- (u as Const (c as (_, T)), ts) =>
+ (Const (@{const_name Let}, _), t1 :: t2 :: ts) =>
+ Term.betapplys (Term.betapply (expand t2, expand t1), map expand ts)
+ | (u as Const (c as (_, T)), ts) =>
(case SMT_Builtin.dest_builtin ctxt c ts of
SOME (_, k, us, mk) =>
if k = length us then mk (map expand us)
@@ -438,8 +438,6 @@
fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
| NONE => raise TERM ("unsupported quantifier", [t]))
- | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
- transT T ##>> trans t1 ##>> trans t2 #>> (fn ((U, u1), u2) => SLet (U, u1, u2))
| (u as Const (c as (_, T)), ts) =>
(case builtin ctxt c ts of
SOME (n, _, us, _) => fold_map trans us #>> app n
@@ -516,7 +514,6 @@
val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
|>> apfst (cons fun_app_eq)
-val _ = dtyps : (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list (*###*)
in
(ts4, tr_context)
|-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
--- a/src/Pure/Isar/code.ML Tue Jun 20 17:28:17 2017 +0200
+++ b/src/Pure/Isar/code.ML Tue Jun 20 17:31:29 2017 +0200
@@ -165,17 +165,18 @@
fun case_consts_of (Constructors (_, case_consts)) = case_consts
| case_consts_of (Abstractor _) = [];
+
(* functions *)
-datatype fun_spec = Eqns_Default of (thm * bool) list * (thm * bool) list lazy
+datatype fun_spec = Unimplemented
+ | Eqns_Default of (thm * bool) list * (thm * bool) list lazy
(* (cache for default equations, lazy computation of default equations)
-- helps to restore natural order of default equations *)
| Eqns of (thm * bool) list
- | None
| Proj of (term * string) * bool
| Abstr of (thm * string) * bool;
-val initial_fun_spec = Eqns_Default ([], Lazy.value []);
+val default_fun_spec = Eqns_Default ([], Lazy.value []);
fun is_default (Eqns_Default _) = true
| is_default (Proj (_, default)) = default
@@ -190,9 +191,9 @@
datatype spec = Spec of {
history_concluded: bool,
- functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
+ types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
(*with explicit history*),
- types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
+ functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
(*with explicit history*),
cases: ((int * (int * string option list)) * thm) Symtab.table,
undefineds: unit Symtab.table
@@ -201,6 +202,8 @@
fun make_spec (history_concluded, (functions, (types, (cases, undefineds)))) =
Spec { history_concluded = history_concluded, functions = functions, types = types,
cases = cases, undefineds = undefineds };
+val empty_spec =
+ make_spec (false, (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty))));
fun map_spec f (Spec { history_concluded = history_concluded,
functions = functions, types = types, cases = cases, undefineds = undefineds }) =
make_spec (f (history_concluded, (functions, (types, (cases, undefineds)))));
@@ -224,20 +227,20 @@
val invalidated_case_consts = union (op =) (case_consts_of' types1) (case_consts_of' types2)
|> subtract (op =) (maps case_consts_of all_datatype_specs)
val functions = Symtab.join (K merge_functions) (functions1, functions2)
- |> fold (fn c => Symtab.map_entry c (apfst (K (true, initial_fun_spec)))) all_constructors;
+ |> fold (fn c => Symtab.map_entry c (apfst (K (true, default_fun_spec)))) all_constructors;
val cases = Symtab.merge (K true) (cases1, cases2)
|> fold Symtab.delete invalidated_case_consts;
val undefineds = Symtab.merge (K true) (undefineds1, undefineds2);
in make_spec (false, (functions, (types, (cases, undefineds)))) end;
fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
-fun the_functions (Spec { functions, ... }) = functions;
-fun the_types (Spec { types, ... }) = types;
-fun the_cases (Spec { cases, ... }) = cases;
-fun the_undefineds (Spec { undefineds, ... }) = undefineds;
+fun types_of (Spec { types, ... }) = types;
+fun functions_of (Spec { functions, ... }) = functions;
+fun cases_of (Spec { cases, ... }) = cases;
+fun undefineds_of (Spec { undefineds, ... }) = undefineds;
val map_history_concluded = map_spec o apfst;
val map_functions = map_spec o apsnd o apfst;
-val map_typs = map_spec o apsnd o apsnd o apfst;
+val map_types = map_spec o apsnd o apsnd o apfst;
val map_cases = map_spec o apsnd o apsnd o apsnd o apfst;
val map_undefineds = map_spec o apsnd o apsnd o apsnd o apsnd;
@@ -282,8 +285,7 @@
structure Code_Data = Theory_Data
(
type T = spec * (data * theory) option Synchronized.var;
- val empty = (make_spec (false, (Symtab.empty,
- (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
+ val empty = (empty_spec, empty_dataref ());
val extend : T -> T = apsnd (K (empty_dataref ()));
fun merge ((spec1, _), (spec2, _)) =
(merge_spec (spec1, spec2), empty_dataref ());
@@ -294,24 +296,24 @@
(* access to executable code *)
-val the_exec : theory -> spec = fst o Code_Data.get;
+val spec_of : theory -> spec = fst o Code_Data.get;
-fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
+fun map_spec_purge f = Code_Data.map (fn (spec, _) => (f spec, empty_dataref ()));
-fun change_fun_spec c f = (map_exec_purge o map_functions
- o (Symtab.map_default (c, ((false, initial_fun_spec), [])))
+fun change_fun_spec c f = (map_spec_purge o map_functions
+ o (Symtab.map_default (c, ((false, default_fun_spec), [])))
o apfst) (fn (_, spec) => (true, f spec));
(* tackling equation history *)
-fun continue_history thy = if (history_concluded o the_exec) thy
+fun continue_history thy = if (history_concluded o spec_of) thy
then thy
|> (Code_Data.map o apfst o map_history_concluded) (K false)
|> SOME
else NONE;
-fun conclude_history thy = if (history_concluded o the_exec) thy
+fun conclude_history thy = if (history_concluded o spec_of) thy
then NONE
else thy
|> (Code_Data.map o apfst)
@@ -349,7 +351,7 @@
(** foundation **)
-(* datatypes *)
+(* types *)
fun no_constr thy s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c
^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s);
@@ -394,7 +396,7 @@
val constructors = map (inst vs o snd) raw_constructors;
in (tyco, (map (rpair []) vs, constructors)) end;
-fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
+fun get_type_entry thy tyco = case these (Symtab.lookup ((types_of o spec_of) thy) tyco)
of (_, entry) :: _ => SOME entry
| _ => NONE;
@@ -704,7 +706,7 @@
(v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts;
val inst = map2 (fn (v, sort) => fn (_, sort') =>
(((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping;
- val subst = (map_types o map_type_tfree)
+ val subst = (Term.map_types o map_type_tfree)
(fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v)));
in
thm
@@ -783,15 +785,17 @@
val cert_thm = Conjunction.intr_balanced (map rewrite_head thms');
in Equations (cert_thm, propers) end;
-fun cert_of_proj thy c tyco =
+fun cert_of_proj ctxt c tyco =
let
+ val thy = Proof_Context.theory_of ctxt
val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco;
val _ = if c = rep then () else
error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
in Projection (mk_proj tyco vs ty abs rep, tyco) end;
-fun cert_of_abs thy tyco c raw_abs_thm =
+fun cert_of_abs ctxt tyco c raw_abs_thm =
let
+ val thy = Proof_Context.theory_of ctxt;
val abs_thm = singleton (canonize_thms thy) raw_abs_thm;
val _ = assert_abs_eqn thy (SOME tyco) abs_thm;
val _ = if c = const_abs_eqn thy abs_thm then ()
@@ -906,9 +910,9 @@
(* code certificate access with preprocessing *)
fun retrieve_raw thy c =
- Symtab.lookup ((the_functions o the_exec) thy) c
+ Symtab.lookup ((functions_of o spec_of) thy) c
|> Option.map (snd o fst)
- |> the_default None
+ |> the_default Unimplemented
fun eqn_conv conv ct =
let
@@ -939,30 +943,28 @@
end;
fun get_cert ctxt functrans c =
- let
- val thy = Proof_Context.theory_of ctxt;
- in
- case retrieve_raw thy c of
- Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy
- |> cert_of_eqns_preprocess ctxt functrans c
- | Eqns eqns => eqns
- |> cert_of_eqns_preprocess ctxt functrans c
- | None => nothing_cert ctxt c
- | Proj ((_, tyco), _) => cert_of_proj thy c tyco
- | Abstr ((abs_thm, tyco), _) => abs_thm
- |> preprocess Conv.arg_conv ctxt
- |> cert_of_abs thy tyco c
- end;
+ case retrieve_raw (Proof_Context.theory_of ctxt) c of
+ Unimplemented => nothing_cert ctxt c
+ | Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy
+ |> cert_of_eqns_preprocess ctxt functrans c
+ | Eqns eqns => eqns
+ |> cert_of_eqns_preprocess ctxt functrans c
+ | Proj ((_, tyco), _) => cert_of_proj ctxt c tyco
+ | Abstr ((abs_thm, tyco), _) => abs_thm
+ |> preprocess Conv.arg_conv ctxt
+ |> cert_of_abs ctxt tyco c;
-(* cases *)
+(* case certificates *)
-fun case_certificate thm =
+local
+
+fun raw_case_cert thm =
let
val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm;
- val _ = case head of Free _ => true
- | Var _ => true
+ val _ = case head of Free _ => ()
+ | Var _ => ()
| _ => raise TERM ("case_cert", []);
val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr;
val (Const (case_const, _), raw_params) = strip_comb case_expr;
@@ -993,16 +995,20 @@
| analyze cases = analyze_cases cases;
in (case_const, (n, analyze cases)) end;
-fun case_cert thm = case_certificate thm
+in
+
+fun case_cert thm = raw_case_cert thm
handle Bind => error "bad case certificate"
| TERM _ => error "bad case certificate";
+end;
+
fun get_case_scheme thy =
- Option.map fst o (Symtab.lookup o the_cases o the_exec) thy;
+ Option.map fst o (Symtab.lookup o cases_of o spec_of) thy;
fun get_case_cong thy =
- Option.map snd o (Symtab.lookup o the_cases o the_exec) thy;
+ Option.map snd o (Symtab.lookup o cases_of o spec_of) thy;
-val undefineds = Symtab.keys o the_undefineds o the_exec;
+val undefineds = Symtab.keys o undefineds_of o spec_of;
(* diagnostic *)
@@ -1010,14 +1016,14 @@
fun print_codesetup thy =
let
val ctxt = Proof_Context.init_global thy;
- val exec = the_exec thy;
+ val spec = spec_of thy;
fun pretty_equations const thms =
(Pretty.block o Pretty.fbreaks)
(Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
fun pretty_function (const, Eqns_Default (_, eqns_lazy)) =
pretty_equations const (map fst (Lazy.force eqns_lazy))
- | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
- | pretty_function (const, None) = pretty_equations const []
+ | pretty_function (const, Eqns eqns) =
+ pretty_equations const (map fst eqns)
| pretty_function (const, Proj ((proj, _), _)) = Pretty.block
[Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
| pretty_function (const, Abstr ((thm, _), _)) = pretty_equations const [thm];
@@ -1042,17 +1048,18 @@
| pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [
Pretty.str (string_of_const thy const), Pretty.str "with",
(Pretty.block o Pretty.commas o map (Pretty.str o pretty_caseparam)) cos];
- val functions = the_functions exec
+ val functions = functions_of spec
|> Symtab.dest
|> (map o apsnd) (snd o fst)
+ |> filter (fn (_, Unimplemented) => false | _ => true)
|> sort (string_ord o apply2 fst);
- val datatypes = the_types exec
+ val datatypes = types_of spec
|> Symtab.dest
|> map (fn (tyco, (_, (vs, spec)) :: _) =>
((tyco, vs), constructors_of spec))
|> sort (string_ord o apply2 (fst o fst));
- val cases = Symtab.dest ((the_cases o the_exec) thy);
- val undefineds = Symtab.keys ((the_undefineds o the_exec) thy);
+ val cases = Symtab.dest ((cases_of o spec_of) thy);
+ val undefineds = Symtab.keys ((undefineds_of o spec_of) thy);
in
Pretty.writeln_chunks [
Pretty.block (
@@ -1100,7 +1107,7 @@
fun update_subsume verbose (thm, proper) eqns =
let
val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
- o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
+ o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
val args = args_of thm;
val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1);
fun matches_args args' =
@@ -1118,9 +1125,9 @@
in (thm, proper) :: filter_out drop eqns end;
fun natural_order eqns =
(eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns []))
- fun add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
+ fun add_eqn' true Unimplemented = Eqns_Default (natural_order [(thm, proper)])
+ | add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
(*this restores the natural order and drops syntactic redundancies*)
- | add_eqn' true None = Eqns_Default (natural_order [(thm, proper)])
| add_eqn' true fun_spec = fun_spec
| add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns)
| add_eqn' false _ = Eqns [(thm, proper)];
@@ -1179,11 +1186,11 @@
fun generic_del_eqn strictness thm thy = case mk_eqn strictness thy (thm, true)
of SOME (thm, _) =>
let
- fun del_eqn' (Eqns_Default _) = initial_fun_spec
+ fun del_eqn' (Eqns_Default _) = default_fun_spec
| del_eqn' (Eqns eqns) =
let
val eqns' = filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns
- in if null eqns' then None else Eqns eqns' end
+ in if null eqns' then Unimplemented else Eqns eqns' end
| del_eqn' spec = spec
in change_fun_spec (const_eqn thy thm) del_eqn' thy end
| NONE => thy;
@@ -1191,7 +1198,7 @@
val del_eqn_silent = generic_del_eqn Silent;
val del_eqn = generic_del_eqn Liberal;
-fun del_eqns c = change_fun_spec c (K None);
+fun del_eqns c = change_fun_spec c (K Unimplemented);
fun del_exception c = change_fun_spec c (K (Eqns []));
@@ -1231,16 +1238,16 @@
then insert (op =) case_const cases
else cases)
| register_for_constructors (x as Abstractor _) = x;
- val register_type = (map_typs o Symtab.map)
+ val register_type = (map_types o Symtab.map)
(K ((map o apsnd o apsnd) register_for_constructors));
in
thy
|> `(fn thy => case_cong thy case_const entry)
- |-> (fn cong => map_exec_purge (register_case cong #> register_type))
+ |-> (fn cong => map_spec_purge (register_case cong #> register_type))
end;
fun add_undefined c thy =
- (map_exec_purge o map_undefineds) (Symtab.update (c, ())) thy;
+ (map_spec_purge o map_undefineds) (Symtab.update (c, ())) thy;
(* types *)
@@ -1248,7 +1255,7 @@
fun register_type (tyco, vs_spec) thy =
let
val (old_constrs, some_old_proj) =
- case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
+ case these (Symtab.lookup ((types_of o spec_of) thy) tyco)
of (_, (_, Constructors (cos, _))) :: _ => (map fst cos, NONE)
| (_, (_, Abstractor ((co, _), (proj, _)))) :: _ => ([co], SOME proj)
| [] => ([], NONE);
@@ -1259,7 +1266,7 @@
(fn (c, ((_, spec), _)) =>
if member (op =) (the_list (associated_abstype spec)) tyco
then insert (op =) c else I)
- ((the_functions o the_exec) thy) [old_proj];
+ ((functions_of o spec_of) thy) [old_proj];
fun drop_outdated_cases cases = fold Symtab.delete_safe
(Symtab.fold (fn (c, ((_, (_, cos)), _)) =>
if exists (member (op =) old_constrs) (map_filter I cos)
@@ -1267,8 +1274,8 @@
in
thy
|> fold del_eqns (outdated_funs1 @ outdated_funs2)
- |> map_exec_purge
- ((map_typs o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
+ |> map_spec_purge
+ ((map_types o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
#> map_cases drop_outdated_cases)
end;