interleave (co)datatypes in the right order w.r.t. dependencies
authorblanchet
Wed Sep 24 15:46:25 2014 +0200 (2014-09-24)
changeset 584290b94858325a5
parent 58428 e4e34dfc3e68
child 58430 73df5884edcf
interleave (co)datatypes in the right order w.r.t. dependencies
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 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)]
     2.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Sep 24 15:46:24 2014 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Sep 24 15:46:25 2014 +0200
     2.3 @@ -19,8 +19,7 @@
     2.4    type sign = {
     2.5      logic: string,
     2.6      sorts: string list,
     2.7 -    lfp_dtyps: (string * (string * (string * string) list) list) list list,
     2.8 -    gfp_dtyps: (string * (string * (string * string) list) list) list list,
     2.9 +    dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
    2.10      funcs: (string * (string list * string)) list }
    2.11    type config = {
    2.12      logic: term list -> string,
    2.13 @@ -62,8 +61,7 @@
    2.14  type sign = {
    2.15    logic: string,
    2.16    sorts: string list,
    2.17 -  lfp_dtyps: (string * (string * (string * string) list) list) list list,
    2.18 -  gfp_dtyps: (string * (string * (string * string) list) list) list list,
    2.19 +  dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
    2.20    funcs: (string * (string list * string)) list }
    2.21  
    2.22  type config = {
    2.23 @@ -116,11 +114,10 @@
    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 lfp_dtyps gfp_dtyps (_, typs, terms) = {
    2.28 +fun sign_of logic dtyps (_, typs, terms) = {
    2.29    logic = logic,
    2.30    sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
    2.31 -  lfp_dtyps = lfp_dtyps,
    2.32 -  gfp_dtyps = gfp_dtyps,
    2.33 +  dtyps = 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 @@ -142,21 +139,15 @@
    2.38  
    2.39  fun collect_co_datatypes fp_kinds (tr_context, ctxt) ts =
    2.40    let
    2.41 -    val (lfp_declss, ctxt') =
    2.42 +    val (fp_decls, ctxt') =
    2.43        ([], ctxt)
    2.44 -      |> member (op =) fp_kinds BNF_Util.Least_FP
    2.45 -        ? fold (Term.fold_types (SMT_Datatypes.add_decls BNF_Util.Least_FP)) ts
    2.46 -    val (gfp_declss, ctxt'') =
    2.47 -      ([], ctxt')
    2.48 -      |> member (op =) fp_kinds BNF_Util.Greatest_FP
    2.49 -        ? fold (Term.fold_types (SMT_Datatypes.add_decls BNF_Util.Greatest_FP)) ts
    2.50 +      |> fold (Term.fold_types (SMT_Datatypes.add_decls fp_kinds)) ts
    2.51 +      |>> flat
    2.52  
    2.53 -    val fp_declsss = [lfp_declss, gfp_declss]
    2.54 -
    2.55 -    fun is_decl_typ T = exists (exists (exists (equal T o fst))) fp_declsss
    2.56 +    fun is_decl_typ T = exists (equal T o fst o snd) fp_decls
    2.57  
    2.58      fun add_typ' T proper =
    2.59 -      (case SMT_Builtin.dest_builtin_typ ctxt'' T of
    2.60 +      (case SMT_Builtin.dest_builtin_typ ctxt' T of
    2.61          SOME n => pair n
    2.62        | NONE => add_typ T proper)
    2.63  
    2.64 @@ -165,17 +156,18 @@
    2.65        in add_fun sel NONE ##>> add_typ' T (not (is_decl_typ T)) end
    2.66      fun tr_constr (constr, selects) =
    2.67        add_fun constr NONE ##>> fold_map tr_select selects
    2.68 -    fun tr_typ (T, cases) = add_typ' T false ##>> fold_map tr_constr cases
    2.69 +    fun tr_typ (fp, (T, cases)) =
    2.70 +      add_typ' T false ##>> fold_map tr_constr cases #>> pair fp
    2.71  
    2.72 -    val (lfp_declss', tr_context') = fold_map (fold_map tr_typ) lfp_declss tr_context
    2.73 -    val (gfp_declss', tr_context'') = fold_map (fold_map tr_typ) gfp_declss tr_context'
    2.74 +    val (fp_decls', tr_context') = fold_map tr_typ fp_decls tr_context
    2.75  
    2.76      fun add (constr, selects) =
    2.77        Termtab.update (constr, length selects) #>
    2.78        fold (Termtab.update o rpair 1) selects
    2.79  
    2.80 -    val funcs = fold (fold (fold (fold add o snd))) fp_declsss Termtab.empty
    2.81 -  in ((funcs, lfp_declss', gfp_declss', tr_context'', ctxt''), ts) end
    2.82 +    val funcs = fold (fold add o snd o snd) fp_decls Termtab.empty
    2.83 +
    2.84 +  in ((funcs, fp_decls', tr_context', ctxt'), ts) end
    2.85      (* FIXME: also return necessary (co)datatype theorems *)
    2.86  
    2.87  
    2.88 @@ -430,7 +422,7 @@
    2.89  
    2.90  (** translation from Isabelle terms into SMT intermediate terms **)
    2.91  
    2.92 -fun intermediate logic lfp_dtyps gfp_dtyps builtin ctxt ts trx =
    2.93 +fun intermediate logic dtyps builtin ctxt ts trx =
    2.94    let
    2.95      fun transT (T as TFree _) = add_typ T true
    2.96        | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
    2.97 @@ -467,7 +459,7 @@
    2.98        end
    2.99  
   2.100      val (us, trx') = fold_map trans ts trx
   2.101 -  in ((sign_of (logic ts) lfp_dtyps gfp_dtyps trx', us), trx') end
   2.102 +  in ((sign_of (logic ts) dtyps trx', us), trx') end
   2.103  
   2.104  
   2.105  (* translation *)
   2.106 @@ -496,11 +488,11 @@
   2.107      val {logic, fp_kinds, serialize} = get_config ctxt
   2.108  
   2.109      fun no_dtyps (tr_context, ctxt) ts =
   2.110 -      ((Termtab.empty, [], [], tr_context, ctxt), ts)
   2.111 +      ((Termtab.empty, [], tr_context, ctxt), ts)
   2.112  
   2.113      val ts1 = map (Envir.beta_eta_contract o SMT_Util.prop_of o snd) ithms
   2.114  
   2.115 -    val ((funcs, lfp_dtyps, gfp_dtyps, tr_context, ctxt1), ts2) =
   2.116 +    val ((funcs, dtyps, tr_context, ctxt1), ts2) =
   2.117        ((empty_tr_context, ctxt), ts1)
   2.118        |-> (if null fp_kinds then no_dtyps else collect_co_datatypes fp_kinds)
   2.119  
   2.120 @@ -527,9 +519,10 @@
   2.121  
   2.122      val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
   2.123        |>> apfst (cons fun_app_eq)
   2.124 +val _ = dtyps : (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list (*###*)
   2.125    in
   2.126      (ts4, tr_context)
   2.127 -    |-> intermediate logic lfp_dtyps gfp_dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
   2.128 +    |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
   2.129      |>> uncurry (serialize smt_options comments)
   2.130      ||> replay_data_of ctxt2 ll_defs rewrite_rules ithms
   2.131    end
     3.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Sep 24 15:46:24 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Sep 24 15:46:25 2014 +0200
     3.3 @@ -133,18 +133,17 @@
     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, lfp_dtyps, gfp_dtyps, funcs} ts =
     3.8 +fun sdtyp (fp, dtyps) =
     3.9 +  Buffer.add (enclose ("(declare-" ^ BNF_FP_Util.co_prefix fp ^ "datatypes () (") "))\n"
    3.10 +    (space_implode "\n  " (map sdatatype dtyps)))
    3.11 +
    3.12 +fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts =
    3.13    Buffer.empty
    3.14    |> fold (Buffer.add o enclose "; " "\n") comments
    3.15    |> fold (fn (k, v) => Buffer.add ("(set-option " ^ k ^ " " ^ v ^ ")\n")) smt_options
    3.16    |> Buffer.add logic
    3.17    |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts)
    3.18 -  |> (if null lfp_dtyps then I
    3.19 -    else Buffer.add (enclose "(declare-datatypes () (" "))\n"
    3.20 -      (space_implode "\n  " (maps (map sdatatype) lfp_dtyps))))
    3.21 -  |> (if null gfp_dtyps then I
    3.22 -    else Buffer.add (enclose "(declare-codatatypes () (" "))\n"
    3.23 -      (space_implode "\n  " (maps (map sdatatype) gfp_dtyps))))
    3.24 +  |> fold sdtyp (AList.coalesce (op =) dtyps)
    3.25    |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun)
    3.26        (sort (fast_string_ord o pairself fst) funcs)
    3.27    |> fold (fn (i, t) => Buffer.add (enclose "(assert " ")\n"