gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
authorblanchet
Wed Sep 24 15:46:23 2014 +0200 (2014-09-24)
changeset 58427cc1bab5558b0
parent 58426 cac802846ff1
child 58428 e4e34dfc3e68
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
src/HOL/Tools/SMT/smt_datatypes.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:11 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:23 2014 +0200
     1.3 @@ -61,24 +61,29 @@
     1.4  
     1.5  (* collection of declarations *)
     1.6  
     1.7 -(* Simplification: We assume that every type that is not a codatatype is a datatype (or a
     1.8 -   record). *)
     1.9 -fun fp_kind_of ctxt n =
    1.10 -  (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
    1.11 -    SOME {fp, ...} => fp
    1.12 -  | NONE => BNF_Util.Least_FP)
    1.13 +val extN = "_ext" (* cf. "HOL/Tools/typedef.ML" *)
    1.14  
    1.15  fun get_decls fp T n Ts ctxt =
    1.16    let
    1.17 -    fun fallback () =
    1.18 +    fun maybe_typedef () =
    1.19        (case Typedef.get_info ctxt n of
    1.20          [] => ([], ctxt)
    1.21        | info :: _ => (get_typedef_decl info T Ts, ctxt))
    1.22    in
    1.23 -    (case Ctr_Sugar.ctr_sugar_of ctxt n of
    1.24 -      SOME (ctr_sugar as {T = U as Type (_, Us), ...}) =>
    1.25 -      if fp_kind_of ctxt n = fp then get_ctr_sugar_decl ctr_sugar T Ts ctxt else fallback ()
    1.26 -    | NONE => fallback ())
    1.27 +    (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
    1.28 +      SOME {fp = fp', ctr_sugar, ...} =>
    1.29 +      if fp' = fp then get_ctr_sugar_decl ctr_sugar T Ts ctxt else ([], ctxt)
    1.30 +    | NONE =>
    1.31 +      if fp = BNF_Util.Least_FP then
    1.32 +        if String.isSuffix extN n then
    1.33 +          (* for records (FIXME: hack) *)
    1.34 +          (case Ctr_Sugar.ctr_sugar_of ctxt n of
    1.35 +            SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
    1.36 +          | NONE => maybe_typedef ())
    1.37 +        else
    1.38 +          maybe_typedef ()
    1.39 +      else
    1.40 +        ([], ctxt))
    1.41    end
    1.42  
    1.43  fun add_decls fp T (declss, ctxt) =