use 'ctr_sugar' abstraction in SMT(2)
authorblanchet
Thu Jun 12 01:00:49 2014 +0200 (2014-06-12)
changeset 57226c22ad39c3b4b
parent 57225 ff69e42ccf92
child 57227 4c2156fdfe71
use 'ctr_sugar' abstraction in SMT(2)
src/HOL/SMT.thy
src/HOL/SMT2.thy
src/HOL/Tools/SMT/smt_datatypes.ML
src/HOL/Tools/SMT2/smt2_datatypes.ML
     1.1 --- a/src/HOL/SMT.thy	Thu Jun 12 01:00:49 2014 +0200
     1.2 +++ b/src/HOL/SMT.thy	Thu Jun 12 01:00:49 2014 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
     1.5  
     1.6  theory SMT
     1.7 -imports Record
     1.8 +imports List
     1.9  keywords "smt_status" :: diag
    1.10  begin
    1.11  
     2.1 --- a/src/HOL/SMT2.thy	Thu Jun 12 01:00:49 2014 +0200
     2.2 +++ b/src/HOL/SMT2.thy	Thu Jun 12 01:00:49 2014 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2 *}
     2.5  
     2.6  theory SMT2
     2.7 -imports Record
     2.8 +imports List
     2.9  keywords "smt2_status" :: diag
    2.10  begin
    2.11  
     3.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Thu Jun 12 01:00:49 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Thu Jun 12 01:00:49 2014 +0200
     3.3 @@ -17,56 +17,23 @@
     3.4  
     3.5  val lhs_head_of = Term.head_of o fst o Logic.dest_equals o Thm.prop_of
     3.6  
     3.7 -fun mk_selectors T Ts ctxt =
     3.8 -  let
     3.9 -    val (sels, ctxt') =
    3.10 -      Variable.variant_fixes (replicate (length Ts) "select") ctxt
    3.11 -  in (map2 (fn n => fn U => Free (n, T --> U)) sels Ts, ctxt') end
    3.12 +fun mk_selectors T Ts =
    3.13 +  Variable.variant_fixes (replicate (length Ts) "select")
    3.14 +  #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
    3.15  
    3.16  
    3.17 -(* datatype declarations *)
    3.18 -
    3.19 -fun get_datatype_decl ({descr, ...} : Datatype.info) n Ts ctxt =
    3.20 -  let
    3.21 -    fun get_vars (_, (m, vs, _)) = if m = n then SOME vs else NONE
    3.22 -    val vars = the (get_first get_vars descr) ~~ Ts
    3.23 -    val lookup_var = the o AList.lookup (op =) vars
    3.24 -
    3.25 -    fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt
    3.26 -      | typ_of (Datatype.DtType (m, dts)) = Type (m, map typ_of dts)
    3.27 -      | typ_of (Datatype.DtRec i) =
    3.28 -          the (AList.lookup (op =) descr i)
    3.29 -          |> (fn (m, dts, _) => Type (m, map typ_of dts))
    3.30 -
    3.31 -    fun mk_constr T (m, dts) ctxt =
    3.32 -      let
    3.33 -        val Ts = map typ_of dts
    3.34 -        val constr = Const (m, Ts ---> T)
    3.35 -        val (selects, ctxt') = mk_selectors T Ts ctxt
    3.36 -      in ((constr, selects), ctxt') end
    3.37 +(* free constructor type declarations *)
    3.38  
    3.39 -    fun mk_decl (i, (_, _, constrs)) ctxt =
    3.40 -      let
    3.41 -        val T = typ_of (Datatype.DtRec i)
    3.42 -        val (css, ctxt') = fold_map (mk_constr T) constrs ctxt
    3.43 -      in ((T, css), ctxt') end
    3.44 -
    3.45 -  in fold_map mk_decl descr ctxt end
    3.46 -
    3.47 -
    3.48 -(* record declarations *)
    3.49 -
    3.50 -val record_name_of = Long_Name.implode o fst o split_last o Long_Name.explode
    3.51 -
    3.52 -fun get_record_decl ({ext_def, ...} : Record.info) T ctxt =
    3.53 +fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
    3.54    let
    3.55 -    val (con, _) = Term.dest_Const (lhs_head_of ext_def)
    3.56 -    val (fields, more) = Record.get_extT_fields (Proof_Context.theory_of ctxt) T
    3.57 -    val fieldTs = map snd fields @ [snd more]
    3.58 -
    3.59 -    val constr = Const (con, fieldTs ---> T)
    3.60 -    val (selects, ctxt') = mk_selectors T fieldTs ctxt
    3.61 -  in ((T, [(constr, selects)]), ctxt') end
    3.62 +    fun mk_constr ctr0 =
    3.63 +      let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in
    3.64 +        mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr
    3.65 +      end
    3.66 +  in
    3.67 +    fold_map mk_constr ctrs ctxt
    3.68 +    |>> (pair T #> single)
    3.69 +  end
    3.70  
    3.71  
    3.72  (* typedef declarations *)
    3.73 @@ -91,18 +58,12 @@
    3.74  fun declared' dss T = exists (exists (equal T o fst) o snd) dss
    3.75  
    3.76  fun get_decls T n Ts ctxt =
    3.77 -  let val thy = Proof_Context.theory_of ctxt
    3.78 -  in
    3.79 -    (case Datatype.get_info thy n of
    3.80 -      SOME info => get_datatype_decl info n Ts ctxt
    3.81 -    | NONE =>
    3.82 -        (case Record.get_info thy (record_name_of n) of
    3.83 -          SOME info => get_record_decl info T ctxt |>> single
    3.84 -        | NONE =>
    3.85 -            (case Typedef.get_info ctxt n of
    3.86 -              [] => ([], ctxt)
    3.87 -            | info :: _ => (get_typedef_decl info T Ts, ctxt))))
    3.88 -  end
    3.89 +  (case Ctr_Sugar.ctr_sugar_of ctxt n of
    3.90 +    SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
    3.91 +  | NONE =>
    3.92 +      (case Typedef.get_info ctxt n of
    3.93 +        [] => ([], ctxt)
    3.94 +      | info :: _ => (get_typedef_decl info T Ts, ctxt)))
    3.95  
    3.96  fun add_decls T (declss, ctxt) =
    3.97    let
    3.98 @@ -132,5 +93,4 @@
    3.99              in fold add Us (ins dss, ctxt2) end))
   3.100    in add T ([], ctxt) |>> append declss o map snd end
   3.101  
   3.102 -
   3.103  end
     4.1 --- a/src/HOL/Tools/SMT2/smt2_datatypes.ML	Thu Jun 12 01:00:49 2014 +0200
     4.2 +++ b/src/HOL/Tools/SMT2/smt2_datatypes.ML	Thu Jun 12 01:00:49 2014 +0200
     4.3 @@ -15,57 +15,23 @@
     4.4  structure SMT2_Datatypes: SMT2_DATATYPES =
     4.5  struct
     4.6  
     4.7 -val lhs_head_of = Term.head_of o fst o Logic.dest_equals o Thm.prop_of
     4.8 -
     4.9 -fun mk_selectors T Ts ctxt =
    4.10 -  let
    4.11 -    val (sels, ctxt') = Variable.variant_fixes (replicate (length Ts) "select") ctxt
    4.12 -  in (map2 (fn n => fn U => Free (n, T --> U)) sels Ts, ctxt') end
    4.13 +fun mk_selectors T Ts =
    4.14 +  Variable.variant_fixes (replicate (length Ts) "select")
    4.15 +  #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
    4.16  
    4.17  
    4.18 -(* datatype declarations *)
    4.19 -
    4.20 -fun get_datatype_decl ({descr, ...} : Datatype.info) n Ts ctxt =
    4.21 -  let
    4.22 -    fun get_vars (_, (m, vs, _)) = if m = n then SOME vs else NONE
    4.23 -    val vars = the (get_first get_vars descr) ~~ Ts
    4.24 -    val lookup_var = the o AList.lookup (op =) vars
    4.25 -
    4.26 -    fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt
    4.27 -      | typ_of (Datatype.DtType (m, dts)) = Type (m, map typ_of dts)
    4.28 -      | typ_of (Datatype.DtRec i) =
    4.29 -          the (AList.lookup (op =) descr i)
    4.30 -          |> (fn (m, dts, _) => Type (m, map typ_of dts))
    4.31 -
    4.32 -    fun mk_constr T (m, dts) ctxt =
    4.33 -      let
    4.34 -        val Ts = map typ_of dts
    4.35 -        val constr = Const (m, Ts ---> T)
    4.36 -        val (selects, ctxt') = mk_selectors T Ts ctxt
    4.37 -      in ((constr, selects), ctxt') end
    4.38 +(* free constructor type declarations *)
    4.39  
    4.40 -    fun mk_decl (i, (_, _, constrs)) ctxt =
    4.41 -      let
    4.42 -        val T = typ_of (Datatype.DtRec i)
    4.43 -        val (css, ctxt') = fold_map (mk_constr T) constrs ctxt
    4.44 -      in ((T, css), ctxt') end
    4.45 -
    4.46 -  in fold_map mk_decl descr ctxt end
    4.47 -
    4.48 -
    4.49 -(* record declarations *)
    4.50 -
    4.51 -val record_name_of = Long_Name.implode o fst o split_last o Long_Name.explode
    4.52 -
    4.53 -fun get_record_decl ({ext_def, ...} : Record.info) T ctxt =
    4.54 +fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
    4.55    let
    4.56 -    val (con, _) = Term.dest_Const (lhs_head_of ext_def)
    4.57 -    val (fields, more) = Record.get_extT_fields (Proof_Context.theory_of ctxt) T
    4.58 -    val fieldTs = map snd fields @ [snd more]
    4.59 -
    4.60 -    val constr = Const (con, fieldTs ---> T)
    4.61 -    val (selects, ctxt') = mk_selectors T fieldTs ctxt
    4.62 -  in ((T, [(constr, selects)]), ctxt') end
    4.63 +    fun mk_constr ctr0 =
    4.64 +      let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in
    4.65 +        mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr
    4.66 +      end
    4.67 +  in
    4.68 +    fold_map mk_constr ctrs ctxt
    4.69 +    |>> (pair T #> single)
    4.70 +  end
    4.71  
    4.72  
    4.73  (* typedef declarations *)
    4.74 @@ -90,18 +56,12 @@
    4.75  fun declared' dss T = exists (exists (equal T o fst) o snd) dss
    4.76  
    4.77  fun get_decls T n Ts ctxt =
    4.78 -  let val thy = Proof_Context.theory_of ctxt
    4.79 -  in
    4.80 -    (case Datatype.get_info thy n of
    4.81 -      SOME info => get_datatype_decl info n Ts ctxt
    4.82 -    | NONE =>
    4.83 -        (case Record.get_info thy (record_name_of n) of
    4.84 -          SOME info => get_record_decl info T ctxt |>> single
    4.85 -        | NONE =>
    4.86 -            (case Typedef.get_info ctxt n of
    4.87 -              [] => ([], ctxt)
    4.88 -            | info :: _ => (get_typedef_decl info T Ts, ctxt))))
    4.89 -  end
    4.90 +  (case Ctr_Sugar.ctr_sugar_of ctxt n of
    4.91 +    SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
    4.92 +  | NONE =>
    4.93 +      (case Typedef.get_info ctxt n of
    4.94 +        [] => ([], ctxt)
    4.95 +      | info :: _ => (get_typedef_decl info T Ts, ctxt)))
    4.96  
    4.97  fun add_decls T (declss, ctxt) =
    4.98    let
    4.99 @@ -120,8 +80,7 @@
   4.100                ([], _) => (dss, ctxt1)
   4.101              | (ds, ctxt2) =>
   4.102                  let
   4.103 -                  val constrTs =
   4.104 -                    maps (map (snd o Term.dest_Const o fst) o snd) ds
   4.105 +                  val constrTs = maps (map (snd o Term.dest_Const o fst) o snd) ds
   4.106                    val Us = fold (union (op =) o Term.binder_types) constrTs []
   4.107  
   4.108                    fun ins [] = [(Us, ds)]