register Isabelle selectors as SMT selectors when possible
authorblanchet
Wed Sep 17 21:35:58 2014 +0200 (2014-09-17)
changeset 58362cf32eb8001b8
parent 58361 7f2b3b6f6ad1
child 58363 a5c08cd60a3f
register Isabelle selectors as SMT selectors when possible
src/HOL/Tools/SMT/smt_datatypes.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 17 17:32:27 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 17 21:35:58 2014 +0200
     1.3 @@ -15,21 +15,30 @@
     1.4  structure SMT_Datatypes: SMT_DATATYPES =
     1.5  struct
     1.6  
     1.7 -fun mk_selectors T Ts =
     1.8 -  Variable.variant_fixes (replicate (length Ts) "select")
     1.9 -  #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
    1.10 +fun mk_selectors T Ts sels =
    1.11 +  if null sels then
    1.12 +    Variable.variant_fixes (replicate (length Ts) "select")
    1.13 +    #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
    1.14 +  else
    1.15 +    pair sels
    1.16  
    1.17  
    1.18  (* free constructor type declarations *)
    1.19  
    1.20 -fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
    1.21 +fun get_ctr_sugar_decl ({ctrs = ctrs0, selss = selss0, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
    1.22    let
    1.23 -    fun mk_constr ctr0 =
    1.24 -      let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in
    1.25 -        mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr
    1.26 +    fun mk_constr ctr0 sels0 =
    1.27 +      let
    1.28 +        val sels = map (Ctr_Sugar.mk_disc_or_sel Ts) sels0
    1.29 +        val ctr = Ctr_Sugar.mk_ctr Ts ctr0
    1.30 +        val binder_Ts = binder_types (fastype_of ctr)
    1.31 +      in
    1.32 +        mk_selectors T binder_Ts sels #>> pair ctr
    1.33        end
    1.34 +
    1.35 +    val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0
    1.36    in
    1.37 -    fold_map mk_constr ctrs ctxt
    1.38 +    Ctr_Sugar_Util.fold_map2 mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
    1.39      |>> (pair T #> single)
    1.40    end
    1.41