src/HOL/Tools/SMT/smt_datatypes.ML
changeset 58361 7f2b3b6f6ad1
parent 58360 dee1fd1cc631
child 58362 cf32eb8001b8
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 17 16:53:39 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 17 17:32:27 2014 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Sascha Boehme, TU Muenchen
     1.5  
     1.6  Collector functions for common type declarations and their representation
     1.7 -as algebraic datatypes.
     1.8 +as (co)algebraic datatypes.
     1.9  *)
    1.10  
    1.11  signature SMT_DATATYPES =
    1.12 @@ -55,13 +55,25 @@
    1.13  fun declared declss T = exists (exists (equal T o fst)) declss
    1.14  fun declared' dss T = exists (exists (equal T o fst) o snd) dss
    1.15  
    1.16 -fun get_decls T n Ts ctxt =
    1.17 -  (case Ctr_Sugar.ctr_sugar_of ctxt n of
    1.18 -    SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
    1.19 -  | NONE =>
    1.20 +(* Simplification: We assume that every type that is not a codatatype is a datatype (or a
    1.21 +   record). *)
    1.22 +fun fp_kind_of ctxt n =
    1.23 +  (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
    1.24 +    SOME {fp, ...} => fp
    1.25 +  | NONE => BNF_Util.Least_FP)
    1.26 +
    1.27 +fun get_decls fp T n Ts ctxt =
    1.28 +  let
    1.29 +    fun fallback () =
    1.30        (case Typedef.get_info ctxt n of
    1.31          [] => ([], ctxt)
    1.32 -      | info :: _ => (get_typedef_decl info T Ts, ctxt)))
    1.33 +      | info :: _ => (get_typedef_decl info T Ts, ctxt))
    1.34 +  in
    1.35 +    (case Ctr_Sugar.ctr_sugar_of ctxt n of
    1.36 +      SOME ctr_sugar =>
    1.37 +      if fp_kind_of ctxt n = fp then get_ctr_sugar_decl ctr_sugar T Ts ctxt else fallback ()
    1.38 +    | NONE => fallback ())
    1.39 +  end
    1.40  
    1.41  fun add_decls fp T (declss, ctxt) =
    1.42    let
    1.43 @@ -76,7 +88,7 @@
    1.44            if declared declss T orelse declared' dss T then (dss, ctxt1)
    1.45            else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
    1.46            else
    1.47 -            (case get_decls T n Ts ctxt1 of
    1.48 +            (case get_decls fp T n Ts ctxt1 of
    1.49                ([], _) => (dss, ctxt1)
    1.50              | (ds, ctxt2) =>
    1.51                  let