added codatatype support for CVC4
authorblanchet
Wed Sep 17 17:32:27 2014 +0200 (2014-09-17)
changeset 583617f2b3b6f6ad1
parent 58360 dee1fd1cc631
child 58362 cf32eb8001b8
added codatatype support for CVC4
src/HOL/Tools/SMT/smt_datatypes.ML
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smtlib_interface.ML
     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
     2.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Sep 17 16:53:39 2014 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Sep 17 17:32:27 2014 +0200
     2.3 @@ -19,7 +19,8 @@
     2.4    type sign = {
     2.5      logic: string,
     2.6      sorts: string list,
     2.7 -    dtyps: (string * (string * (string * string) list) list) list list,
     2.8 +    lfp_dtyps: (string * (string * (string * string) list) list) list list,
     2.9 +    gfp_dtyps: (string * (string * (string * string) list) list) list list,
    2.10      funcs: (string * (string list * string)) list }
    2.11    type config = {
    2.12      logic: term list -> string,
    2.13 @@ -61,7 +62,8 @@
    2.14  type sign = {
    2.15    logic: string,
    2.16    sorts: string list,
    2.17 -  dtyps: (string * (string * (string * string) list) list) list list,
    2.18 +  lfp_dtyps: (string * (string * (string * string) list) list) list list,
    2.19 +  gfp_dtyps: (string * (string * (string * string) list) list) list list,
    2.20    funcs: (string * (string list * string)) list }
    2.21  
    2.22  type config = {
    2.23 @@ -114,10 +116,11 @@
    2.24          val terms' = Termtab.update (t, (name, sort)) terms
    2.25        in (name, (names', typs, terms')) end)
    2.26  
    2.27 -fun sign_of logic dtyps (_, typs, terms) = {
    2.28 +fun sign_of logic lfp_dtyps gfp_dtyps (_, typs, terms) = {
    2.29    logic = logic,
    2.30    sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
    2.31 -  dtyps = dtyps,
    2.32 +  lfp_dtyps = lfp_dtyps,
    2.33 +  gfp_dtyps = gfp_dtyps,
    2.34    funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []}
    2.35  
    2.36  fun replay_data_of ctxt ll_defs rules assms (_, typs, terms) =
    2.37 @@ -135,17 +138,25 @@
    2.38  
    2.39  (* preprocessing *)
    2.40  
    2.41 -(** datatype declarations **)
    2.42 +(** (co)datatype declarations **)
    2.43  
    2.44 -fun collect_datatypes_and_records (tr_context, ctxt) ts =
    2.45 +fun collect_co_datatypes fp_kinds (tr_context, ctxt) ts =
    2.46    let
    2.47 -    val (declss, ctxt') =
    2.48 -      fold (Term.fold_types (SMT_Datatypes.add_decls BNF_Util.Least_FP)) ts ([], ctxt)
    2.49 +    val (lfp_declss, ctxt') =
    2.50 +      ([], ctxt)
    2.51 +      |> member (op =) fp_kinds BNF_Util.Least_FP
    2.52 +        ? fold (Term.fold_types (SMT_Datatypes.add_decls BNF_Util.Least_FP)) ts
    2.53 +    val (gfp_declss, ctxt'') =
    2.54 +      ([], ctxt')
    2.55 +      |> member (op =) fp_kinds BNF_Util.Greatest_FP
    2.56 +        ? fold (Term.fold_types (SMT_Datatypes.add_decls BNF_Util.Greatest_FP)) ts
    2.57  
    2.58 -    fun is_decl_typ T = exists (exists (equal T o fst)) declss
    2.59 +    val fp_declsss = [lfp_declss, gfp_declss]
    2.60 +
    2.61 +    fun is_decl_typ T = exists (exists (exists (equal T o fst))) fp_declsss
    2.62  
    2.63      fun add_typ' T proper =
    2.64 -      (case SMT_Builtin.dest_builtin_typ ctxt' T of
    2.65 +      (case SMT_Builtin.dest_builtin_typ ctxt'' T of
    2.66          SOME n => pair n
    2.67        | NONE => add_typ T proper)
    2.68  
    2.69 @@ -155,14 +166,17 @@
    2.70      fun tr_constr (constr, selects) =
    2.71        add_fun constr NONE ##>> fold_map tr_select selects
    2.72      fun tr_typ (T, cases) = add_typ' T false ##>> fold_map tr_constr cases
    2.73 -    val (declss', tr_context') = fold_map (fold_map tr_typ) declss tr_context
    2.74 +
    2.75 +    val (lfp_declss', tr_context') = fold_map (fold_map tr_typ) lfp_declss tr_context
    2.76 +    val (gfp_declss', tr_context'') = fold_map (fold_map tr_typ) gfp_declss tr_context'
    2.77  
    2.78      fun add (constr, selects) =
    2.79        Termtab.update (constr, length selects) #>
    2.80        fold (Termtab.update o rpair 1) selects
    2.81 -    val funcs = fold (fold (fold add o snd)) declss Termtab.empty
    2.82 -  in ((funcs, declss', tr_context', ctxt'), ts) end
    2.83 -    (* FIXME: also return necessary datatype and record theorems *)
    2.84 +
    2.85 +    val funcs = fold (fold (fold (fold add o snd))) fp_declsss Termtab.empty
    2.86 +  in ((funcs, lfp_declss', gfp_declss', tr_context'', ctxt''), ts) end
    2.87 +    (* FIXME: also return necessary (co)datatype theorems *)
    2.88  
    2.89  
    2.90  (** eta-expand quantifiers, let expressions and built-ins *)
    2.91 @@ -416,7 +430,7 @@
    2.92  
    2.93  (** translation from Isabelle terms into SMT intermediate terms **)
    2.94  
    2.95 -fun intermediate logic dtyps builtin ctxt ts trx =
    2.96 +fun intermediate logic lfp_dtyps gfp_dtyps builtin ctxt ts trx =
    2.97    let
    2.98      fun transT (T as TFree _) = add_typ T true
    2.99        | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
   2.100 @@ -453,7 +467,7 @@
   2.101        end
   2.102  
   2.103      val (us, trx') = fold_map trans ts trx
   2.104 -  in ((sign_of (logic ts) dtyps trx', us), trx') end
   2.105 +  in ((sign_of (logic ts) lfp_dtyps gfp_dtyps trx', us), trx') end
   2.106  
   2.107  
   2.108  (* translation *)
   2.109 @@ -482,14 +496,13 @@
   2.110      val {logic, fp_kinds, serialize} = get_config ctxt
   2.111  
   2.112      fun no_dtyps (tr_context, ctxt) ts =
   2.113 -      ((Termtab.empty, [], tr_context, ctxt), ts)
   2.114 +      ((Termtab.empty, [], [], tr_context, ctxt), ts)
   2.115  
   2.116      val ts1 = map (Envir.beta_eta_contract o SMT_Util.prop_of o snd) ithms
   2.117  
   2.118 -    val ((funcs, dtyps, tr_context, ctxt1), ts2) =
   2.119 +    val ((funcs, lfp_dtyps, gfp_dtyps, tr_context, ctxt1), ts2) =
   2.120        ((empty_tr_context, ctxt), ts1)
   2.121 -      |-> (if member (op =) fp_kinds BNF_Util.Least_FP then collect_datatypes_and_records
   2.122 -        else no_dtyps)
   2.123 +      |-> (if null fp_kinds then no_dtyps else collect_co_datatypes fp_kinds)
   2.124  
   2.125      fun is_binder (Const (@{const_name Let}, _) $ _) = true
   2.126        | is_binder t = Lambda_Lifting.is_quantifier t
   2.127 @@ -516,7 +529,7 @@
   2.128        |>> apfst (cons fun_app_eq)
   2.129    in
   2.130      (ts4, tr_context)
   2.131 -    |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
   2.132 +    |-> intermediate logic lfp_dtyps gfp_dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
   2.133      |>> uncurry (serialize smt_options comments)
   2.134      ||> replay_data_of ctxt2 ll_defs rewrite_rules ithms
   2.135    end
     3.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Sep 17 16:53:39 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Sep 17 17:32:27 2014 +0200
     3.3 @@ -133,15 +133,18 @@
     3.4  fun assert_name_of_index i = assert_prefix ^ string_of_int i
     3.5  fun assert_index_of_name s = the_default ~1 (Int.fromString (unprefix assert_prefix s))
     3.6  
     3.7 -fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts =
     3.8 +fun serialize smt_options comments {logic, sorts, lfp_dtyps, gfp_dtyps, funcs} ts =
     3.9    Buffer.empty
    3.10    |> fold (Buffer.add o enclose "; " "\n") comments
    3.11    |> fold (fn (k, v) => Buffer.add ("(set-option " ^ k ^ " " ^ v ^ ")\n")) smt_options
    3.12    |> Buffer.add logic
    3.13    |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts)
    3.14 -  |> (if null dtyps then I
    3.15 +  |> (if null lfp_dtyps then I
    3.16      else Buffer.add (enclose "(declare-datatypes () (" "))\n"
    3.17 -      (space_implode "\n  " (maps (map sdatatype) dtyps))))
    3.18 +      (space_implode "\n  " (maps (map sdatatype) lfp_dtyps))))
    3.19 +  |> (if null gfp_dtyps then I
    3.20 +    else Buffer.add (enclose "(declare-codatatypes () (" "))\n"
    3.21 +      (space_implode "\n  " (maps (map sdatatype) gfp_dtyps))))
    3.22    |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun)
    3.23        (sort (fast_string_ord o pairself fst) funcs)
    3.24    |> fold (fn (i, t) => Buffer.add (enclose "(assert " ")\n"