--- a/src/HOL/SMT.thy Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/SMT.thy Thu Jun 12 01:00:49 2014 +0200
@@ -5,7 +5,7 @@
header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
theory SMT
-imports Record
+imports List
keywords "smt_status" :: diag
begin
--- a/src/HOL/SMT2.thy Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/SMT2.thy Thu Jun 12 01:00:49 2014 +0200
@@ -5,7 +5,7 @@
header {* Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2 *}
theory SMT2
-imports Record
+imports List
keywords "smt2_status" :: diag
begin
--- a/src/HOL/Tools/SMT/smt_datatypes.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML Thu Jun 12 01:00:49 2014 +0200
@@ -17,56 +17,23 @@
val lhs_head_of = Term.head_of o fst o Logic.dest_equals o Thm.prop_of
-fun mk_selectors T Ts ctxt =
- let
- val (sels, ctxt') =
- Variable.variant_fixes (replicate (length Ts) "select") ctxt
- in (map2 (fn n => fn U => Free (n, T --> U)) sels Ts, ctxt') end
+fun mk_selectors T Ts =
+ Variable.variant_fixes (replicate (length Ts) "select")
+ #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
-(* datatype declarations *)
-
-fun get_datatype_decl ({descr, ...} : Datatype.info) n Ts ctxt =
- let
- fun get_vars (_, (m, vs, _)) = if m = n then SOME vs else NONE
- val vars = the (get_first get_vars descr) ~~ Ts
- val lookup_var = the o AList.lookup (op =) vars
-
- fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt
- | typ_of (Datatype.DtType (m, dts)) = Type (m, map typ_of dts)
- | typ_of (Datatype.DtRec i) =
- the (AList.lookup (op =) descr i)
- |> (fn (m, dts, _) => Type (m, map typ_of dts))
-
- fun mk_constr T (m, dts) ctxt =
- let
- val Ts = map typ_of dts
- val constr = Const (m, Ts ---> T)
- val (selects, ctxt') = mk_selectors T Ts ctxt
- in ((constr, selects), ctxt') end
+(* free constructor type declarations *)
- fun mk_decl (i, (_, _, constrs)) ctxt =
- let
- val T = typ_of (Datatype.DtRec i)
- val (css, ctxt') = fold_map (mk_constr T) constrs ctxt
- in ((T, css), ctxt') end
-
- in fold_map mk_decl descr ctxt end
-
-
-(* record declarations *)
-
-val record_name_of = Long_Name.implode o fst o split_last o Long_Name.explode
-
-fun get_record_decl ({ext_def, ...} : Record.info) T ctxt =
+fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
let
- val (con, _) = Term.dest_Const (lhs_head_of ext_def)
- val (fields, more) = Record.get_extT_fields (Proof_Context.theory_of ctxt) T
- val fieldTs = map snd fields @ [snd more]
-
- val constr = Const (con, fieldTs ---> T)
- val (selects, ctxt') = mk_selectors T fieldTs ctxt
- in ((T, [(constr, selects)]), ctxt') end
+ fun mk_constr ctr0 =
+ let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in
+ mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr
+ end
+ in
+ fold_map mk_constr ctrs ctxt
+ |>> (pair T #> single)
+ end
(* typedef declarations *)
@@ -91,18 +58,12 @@
fun declared' dss T = exists (exists (equal T o fst) o snd) dss
fun get_decls T n Ts ctxt =
- let val thy = Proof_Context.theory_of ctxt
- in
- (case Datatype.get_info thy n of
- SOME info => get_datatype_decl info n Ts ctxt
- | NONE =>
- (case Record.get_info thy (record_name_of n) of
- SOME info => get_record_decl info T ctxt |>> single
- | NONE =>
- (case Typedef.get_info ctxt n of
- [] => ([], ctxt)
- | info :: _ => (get_typedef_decl info T Ts, ctxt))))
- end
+ (case Ctr_Sugar.ctr_sugar_of ctxt n of
+ SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
+ | NONE =>
+ (case Typedef.get_info ctxt n of
+ [] => ([], ctxt)
+ | info :: _ => (get_typedef_decl info T Ts, ctxt)))
fun add_decls T (declss, ctxt) =
let
@@ -132,5 +93,4 @@
in fold add Us (ins dss, ctxt2) end))
in add T ([], ctxt) |>> append declss o map snd end
-
end
--- a/src/HOL/Tools/SMT2/smt2_datatypes.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_datatypes.ML Thu Jun 12 01:00:49 2014 +0200
@@ -15,57 +15,23 @@
structure SMT2_Datatypes: SMT2_DATATYPES =
struct
-val lhs_head_of = Term.head_of o fst o Logic.dest_equals o Thm.prop_of
-
-fun mk_selectors T Ts ctxt =
- let
- val (sels, ctxt') = Variable.variant_fixes (replicate (length Ts) "select") ctxt
- in (map2 (fn n => fn U => Free (n, T --> U)) sels Ts, ctxt') end
+fun mk_selectors T Ts =
+ Variable.variant_fixes (replicate (length Ts) "select")
+ #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
-(* datatype declarations *)
-
-fun get_datatype_decl ({descr, ...} : Datatype.info) n Ts ctxt =
- let
- fun get_vars (_, (m, vs, _)) = if m = n then SOME vs else NONE
- val vars = the (get_first get_vars descr) ~~ Ts
- val lookup_var = the o AList.lookup (op =) vars
-
- fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt
- | typ_of (Datatype.DtType (m, dts)) = Type (m, map typ_of dts)
- | typ_of (Datatype.DtRec i) =
- the (AList.lookup (op =) descr i)
- |> (fn (m, dts, _) => Type (m, map typ_of dts))
-
- fun mk_constr T (m, dts) ctxt =
- let
- val Ts = map typ_of dts
- val constr = Const (m, Ts ---> T)
- val (selects, ctxt') = mk_selectors T Ts ctxt
- in ((constr, selects), ctxt') end
+(* free constructor type declarations *)
- fun mk_decl (i, (_, _, constrs)) ctxt =
- let
- val T = typ_of (Datatype.DtRec i)
- val (css, ctxt') = fold_map (mk_constr T) constrs ctxt
- in ((T, css), ctxt') end
-
- in fold_map mk_decl descr ctxt end
-
-
-(* record declarations *)
-
-val record_name_of = Long_Name.implode o fst o split_last o Long_Name.explode
-
-fun get_record_decl ({ext_def, ...} : Record.info) T ctxt =
+fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
let
- val (con, _) = Term.dest_Const (lhs_head_of ext_def)
- val (fields, more) = Record.get_extT_fields (Proof_Context.theory_of ctxt) T
- val fieldTs = map snd fields @ [snd more]
-
- val constr = Const (con, fieldTs ---> T)
- val (selects, ctxt') = mk_selectors T fieldTs ctxt
- in ((T, [(constr, selects)]), ctxt') end
+ fun mk_constr ctr0 =
+ let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in
+ mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr
+ end
+ in
+ fold_map mk_constr ctrs ctxt
+ |>> (pair T #> single)
+ end
(* typedef declarations *)
@@ -90,18 +56,12 @@
fun declared' dss T = exists (exists (equal T o fst) o snd) dss
fun get_decls T n Ts ctxt =
- let val thy = Proof_Context.theory_of ctxt
- in
- (case Datatype.get_info thy n of
- SOME info => get_datatype_decl info n Ts ctxt
- | NONE =>
- (case Record.get_info thy (record_name_of n) of
- SOME info => get_record_decl info T ctxt |>> single
- | NONE =>
- (case Typedef.get_info ctxt n of
- [] => ([], ctxt)
- | info :: _ => (get_typedef_decl info T Ts, ctxt))))
- end
+ (case Ctr_Sugar.ctr_sugar_of ctxt n of
+ SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
+ | NONE =>
+ (case Typedef.get_info ctxt n of
+ [] => ([], ctxt)
+ | info :: _ => (get_typedef_decl info T Ts, ctxt)))
fun add_decls T (declss, ctxt) =
let
@@ -120,8 +80,7 @@
([], _) => (dss, ctxt1)
| (ds, ctxt2) =>
let
- val constrTs =
- maps (map (snd o Term.dest_Const o fst) o snd) ds
+ val constrTs = maps (map (snd o Term.dest_Const o fst) o snd) ds
val Us = fold (union (op =) o Term.binder_types) constrTs []
fun ins [] = [(Us, ds)]