src/HOL/Tools/SMT/smt_datatypes.ML
changeset 58429 0b94858325a5
parent 58428 e4e34dfc3e68
child 58430 73df5884edcf
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:24 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:25 2014 +0200
     1.3 @@ -7,9 +7,9 @@
     1.4  
     1.5  signature SMT_DATATYPES =
     1.6  sig
     1.7 -  val add_decls: BNF_Util.fp_kind -> typ ->
     1.8 -    (typ * (term * term list) list) list list * Proof.context ->
     1.9 -    (typ * (term * term list) list) list list * Proof.context
    1.10 +  val add_decls: BNF_Util.fp_kind list -> typ ->
    1.11 +    (BNF_Util.fp_kind * (typ * (term * term list) list)) list list * Proof.context ->
    1.12 +    (BNF_Util.fp_kind * (typ * (term * term list) list)) list list * Proof.context
    1.13  end;
    1.14  
    1.15  structure SMT_Datatypes: SMT_DATATYPES =
    1.16 @@ -63,49 +63,47 @@
    1.17  
    1.18  val extN = "_ext" (* cf. "HOL/Tools/typedef.ML" *)
    1.19  
    1.20 -fun get_decls fp T n Ts ctxt =
    1.21 +fun get_decls fps T n Ts ctxt =
    1.22    let
    1.23      fun maybe_typedef () =
    1.24        (case Typedef.get_info ctxt n of
    1.25          [] => ([], ctxt)
    1.26 -      | info :: _ => (get_typedef_decl info T Ts, ctxt))
    1.27 +      | info :: _ => (map (pair (hd fps)) (get_typedef_decl info T Ts), ctxt))
    1.28    in
    1.29      (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
    1.30 -      SOME {fp = fp', fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} =>
    1.31 -      if fp' = fp then
    1.32 +      SOME {fp, fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} =>
    1.33 +      if member (op =) fps fp then
    1.34          let
    1.35            val ns = map (fst o dest_Type) fp_Ts
    1.36            val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns
    1.37            val Xs = map #X mutual_fp_sugars
    1.38            val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars
    1.39  
    1.40 -          fun is_nested_co_recursive (T as Type _) =
    1.41 -              BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs T
    1.42 +          (* FIXME: allow nested recursion to same FP kind *)
    1.43 +          fun is_nested_co_recursive (T as Type _) = BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs T
    1.44              | is_nested_co_recursive _ = false
    1.45          in
    1.46            if exists (exists (exists is_nested_co_recursive)) ctrXs_Tsss then maybe_typedef ()
    1.47 -          else get_ctr_sugar_decl ctr_sugar T Ts ctxt
    1.48 +          else get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair fp)
    1.49          end
    1.50        else
    1.51          ([], ctxt)
    1.52      | NONE =>
    1.53 -      if fp = BNF_Util.Least_FP then
    1.54 -        if String.isSuffix extN n then
    1.55 -          (* for records (FIXME: hack) *)
    1.56 -          (case Ctr_Sugar.ctr_sugar_of ctxt n of
    1.57 -            SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
    1.58 -          | NONE => maybe_typedef ())
    1.59 -        else
    1.60 -          maybe_typedef ()
    1.61 +      if String.isSuffix extN n then
    1.62 +        (* for records (FIXME: hack) *)
    1.63 +        (case Ctr_Sugar.ctr_sugar_of ctxt n of
    1.64 +          SOME ctr_sugar =>
    1.65 +          get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair (hd fps))
    1.66 +        | NONE => maybe_typedef ())
    1.67        else
    1.68 -        ([], ctxt))
    1.69 +        maybe_typedef ())
    1.70    end
    1.71  
    1.72 -fun add_decls fp T (declss, ctxt) =
    1.73 +fun add_decls fps T (declss, ctxt) =
    1.74    let
    1.75 -    fun declared T = exists (exists (equal T o fst))
    1.76 -    fun declared' T = exists (exists (equal T o fst) o snd)
    1.77 -    fun depends ds = exists (member (op =) (map fst ds))
    1.78 +    fun declared T = exists (exists (equal T o fst o snd))
    1.79 +    fun declared' T = exists (exists (equal T o fst o snd) o snd)
    1.80 +    fun depends ds = exists (member (op =) (map (fst o snd) ds))
    1.81  
    1.82      fun add (TFree _) = I
    1.83        | add (TVar _) = I
    1.84 @@ -113,14 +111,16 @@
    1.85            fold add (Term.body_type T :: Term.binder_types T)
    1.86        | add @{typ bool} = I
    1.87        | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
    1.88 -          if declared T declss orelse declared' T dss then (dss, ctxt1)
    1.89 -          else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
    1.90 +          if declared T declss orelse declared' T dss then
    1.91 +            (dss, ctxt1)
    1.92 +          else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then
    1.93 +            (dss, ctxt1)
    1.94            else
    1.95 -            (case get_decls fp T n Ts ctxt1 of
    1.96 +            (case get_decls fps T n Ts ctxt1 of
    1.97                ([], _) => (dss, ctxt1)
    1.98              | (ds, ctxt2) =>
    1.99                  let
   1.100 -                  val constrTs = maps (map (snd o Term.dest_Const o fst) o snd) ds
   1.101 +                  val constrTs = maps (map (snd o Term.dest_Const o fst) o snd o snd) ds
   1.102                    val Us = fold (union (op =) o Term.binder_types) constrTs []
   1.103  
   1.104                    fun ins [] = [(Us, ds)]