# HG changeset patch # User blanchet # Date 1411566385 -7200 # Node ID 0b94858325a50b9f7dc5d19e45422d1268545920 # Parent e4e34dfc3e68d595f85be6463d0a568291046c50 interleave (co)datatypes in the right order w.r.t. dependencies diff -r e4e34dfc3e68 -r 0b94858325a5 src/HOL/Tools/SMT/smt_datatypes.ML --- a/src/HOL/Tools/SMT/smt_datatypes.ML Wed Sep 24 15:46:24 2014 +0200 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML Wed Sep 24 15:46:25 2014 +0200 @@ -7,9 +7,9 @@ signature SMT_DATATYPES = sig - val add_decls: BNF_Util.fp_kind -> typ -> - (typ * (term * term list) list) list list * Proof.context -> - (typ * (term * term list) list) list list * Proof.context + val add_decls: BNF_Util.fp_kind list -> typ -> + (BNF_Util.fp_kind * (typ * (term * term list) list)) list list * Proof.context -> + (BNF_Util.fp_kind * (typ * (term * term list) list)) list list * Proof.context end; structure SMT_Datatypes: SMT_DATATYPES = @@ -63,49 +63,47 @@ val extN = "_ext" (* cf. "HOL/Tools/typedef.ML" *) -fun get_decls fp T n Ts ctxt = +fun get_decls fps T n Ts ctxt = let fun maybe_typedef () = (case Typedef.get_info ctxt n of [] => ([], ctxt) - | info :: _ => (get_typedef_decl info T Ts, ctxt)) + | info :: _ => (map (pair (hd fps)) (get_typedef_decl info T Ts), ctxt)) in (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of - SOME {fp = fp', fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} => - if fp' = fp then + SOME {fp, fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} => + if member (op =) fps fp then let val ns = map (fst o dest_Type) fp_Ts val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns val Xs = map #X mutual_fp_sugars val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars - fun is_nested_co_recursive (T as Type _) = - BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs T + (* FIXME: allow nested recursion to same FP kind *) + fun is_nested_co_recursive (T as Type _) = BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs T | is_nested_co_recursive _ = false in if exists (exists (exists is_nested_co_recursive)) ctrXs_Tsss then maybe_typedef () - else get_ctr_sugar_decl ctr_sugar T Ts ctxt + else get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair fp) end else ([], ctxt) | NONE => - if fp = BNF_Util.Least_FP then - if String.isSuffix extN n then - (* for records (FIXME: hack) *) - (case Ctr_Sugar.ctr_sugar_of ctxt n of - SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt - | NONE => maybe_typedef ()) - else - maybe_typedef () + if String.isSuffix extN n then + (* for records (FIXME: hack) *) + (case Ctr_Sugar.ctr_sugar_of ctxt n of + SOME ctr_sugar => + get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair (hd fps)) + | NONE => maybe_typedef ()) else - ([], ctxt)) + maybe_typedef ()) end -fun add_decls fp T (declss, ctxt) = +fun add_decls fps T (declss, ctxt) = let - fun declared T = exists (exists (equal T o fst)) - fun declared' T = exists (exists (equal T o fst) o snd) - fun depends ds = exists (member (op =) (map fst ds)) + fun declared T = exists (exists (equal T o fst o snd)) + fun declared' T = exists (exists (equal T o fst o snd) o snd) + fun depends ds = exists (member (op =) (map (fst o snd) ds)) fun add (TFree _) = I | add (TVar _) = I @@ -113,14 +111,16 @@ fold add (Term.body_type T :: Term.binder_types T) | add @{typ bool} = I | add (T as Type (n, Ts)) = (fn (dss, ctxt1) => - if declared T declss orelse declared' T dss then (dss, ctxt1) - else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1) + if declared T declss orelse declared' T dss then + (dss, ctxt1) + else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then + (dss, ctxt1) else - (case get_decls fp T n Ts ctxt1 of + (case get_decls fps T n Ts ctxt1 of ([], _) => (dss, ctxt1) | (ds, ctxt2) => let - val constrTs = maps (map (snd o Term.dest_Const o fst) o snd) ds + val constrTs = maps (map (snd o Term.dest_Const o fst) o snd o snd) ds val Us = fold (union (op =) o Term.binder_types) constrTs [] fun ins [] = [(Us, ds)] diff -r e4e34dfc3e68 -r 0b94858325a5 src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Wed Sep 24 15:46:24 2014 +0200 +++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Sep 24 15:46:25 2014 +0200 @@ -19,8 +19,7 @@ type sign = { logic: string, sorts: string list, - lfp_dtyps: (string * (string * (string * string) list) list) list list, - gfp_dtyps: (string * (string * (string * string) list) list) list list, + dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list, funcs: (string * (string list * string)) list } type config = { logic: term list -> string, @@ -62,8 +61,7 @@ type sign = { logic: string, sorts: string list, - lfp_dtyps: (string * (string * (string * string) list) list) list list, - gfp_dtyps: (string * (string * (string * string) list) list) list list, + dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list, funcs: (string * (string list * string)) list } type config = { @@ -116,11 +114,10 @@ val terms' = Termtab.update (t, (name, sort)) terms in (name, (names', typs, terms')) end) -fun sign_of logic lfp_dtyps gfp_dtyps (_, typs, terms) = { +fun sign_of logic dtyps (_, typs, terms) = { logic = logic, sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [], - lfp_dtyps = lfp_dtyps, - gfp_dtyps = gfp_dtyps, + dtyps = dtyps, funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []} fun replay_data_of ctxt ll_defs rules assms (_, typs, terms) = @@ -142,21 +139,15 @@ fun collect_co_datatypes fp_kinds (tr_context, ctxt) ts = let - val (lfp_declss, ctxt') = + val (fp_decls, ctxt') = ([], ctxt) - |> member (op =) fp_kinds BNF_Util.Least_FP - ? fold (Term.fold_types (SMT_Datatypes.add_decls BNF_Util.Least_FP)) ts - val (gfp_declss, ctxt'') = - ([], ctxt') - |> member (op =) fp_kinds BNF_Util.Greatest_FP - ? fold (Term.fold_types (SMT_Datatypes.add_decls BNF_Util.Greatest_FP)) ts + |> fold (Term.fold_types (SMT_Datatypes.add_decls fp_kinds)) ts + |>> flat - val fp_declsss = [lfp_declss, gfp_declss] - - fun is_decl_typ T = exists (exists (exists (equal T o fst))) fp_declsss + fun is_decl_typ T = exists (equal T o fst o snd) fp_decls fun add_typ' T proper = - (case SMT_Builtin.dest_builtin_typ ctxt'' T of + (case SMT_Builtin.dest_builtin_typ ctxt' T of SOME n => pair n | NONE => add_typ T proper) @@ -165,17 +156,18 @@ in add_fun sel NONE ##>> add_typ' T (not (is_decl_typ T)) end fun tr_constr (constr, selects) = add_fun constr NONE ##>> fold_map tr_select selects - fun tr_typ (T, cases) = add_typ' T false ##>> fold_map tr_constr cases + fun tr_typ (fp, (T, cases)) = + add_typ' T false ##>> fold_map tr_constr cases #>> pair fp - val (lfp_declss', tr_context') = fold_map (fold_map tr_typ) lfp_declss tr_context - val (gfp_declss', tr_context'') = fold_map (fold_map tr_typ) gfp_declss tr_context' + val (fp_decls', tr_context') = fold_map tr_typ fp_decls tr_context fun add (constr, selects) = Termtab.update (constr, length selects) #> fold (Termtab.update o rpair 1) selects - val funcs = fold (fold (fold (fold add o snd))) fp_declsss Termtab.empty - in ((funcs, lfp_declss', gfp_declss', tr_context'', ctxt''), ts) end + val funcs = fold (fold add o snd o snd) fp_decls Termtab.empty + + in ((funcs, fp_decls', tr_context', ctxt'), ts) end (* FIXME: also return necessary (co)datatype theorems *) @@ -430,7 +422,7 @@ (** translation from Isabelle terms into SMT intermediate terms **) -fun intermediate logic lfp_dtyps gfp_dtyps builtin ctxt ts trx = +fun intermediate logic dtyps builtin ctxt ts trx = let fun transT (T as TFree _) = add_typ T true | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], [])) @@ -467,7 +459,7 @@ end val (us, trx') = fold_map trans ts trx - in ((sign_of (logic ts) lfp_dtyps gfp_dtyps trx', us), trx') end + in ((sign_of (logic ts) dtyps trx', us), trx') end (* translation *) @@ -496,11 +488,11 @@ val {logic, fp_kinds, serialize} = get_config ctxt fun no_dtyps (tr_context, ctxt) ts = - ((Termtab.empty, [], [], tr_context, ctxt), ts) + ((Termtab.empty, [], tr_context, ctxt), ts) val ts1 = map (Envir.beta_eta_contract o SMT_Util.prop_of o snd) ithms - val ((funcs, lfp_dtyps, gfp_dtyps, tr_context, ctxt1), ts2) = + val ((funcs, dtyps, tr_context, ctxt1), ts2) = ((empty_tr_context, ctxt), ts1) |-> (if null fp_kinds then no_dtyps else collect_co_datatypes fp_kinds) @@ -527,9 +519,10 @@ val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3 |>> apfst (cons fun_app_eq) +val _ = dtyps : (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list (*###*) in (ts4, tr_context) - |-> intermediate logic lfp_dtyps gfp_dtyps (builtin SMT_Builtin.dest_builtin) ctxt2 + |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2 |>> uncurry (serialize smt_options comments) ||> replay_data_of ctxt2 ll_defs rewrite_rules ithms end diff -r e4e34dfc3e68 -r 0b94858325a5 src/HOL/Tools/SMT/smtlib_interface.ML --- a/src/HOL/Tools/SMT/smtlib_interface.ML Wed Sep 24 15:46:24 2014 +0200 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Wed Sep 24 15:46:25 2014 +0200 @@ -133,18 +133,17 @@ fun assert_name_of_index i = assert_prefix ^ string_of_int i fun assert_index_of_name s = the_default ~1 (Int.fromString (unprefix assert_prefix s)) -fun serialize smt_options comments {logic, sorts, lfp_dtyps, gfp_dtyps, funcs} ts = +fun sdtyp (fp, dtyps) = + Buffer.add (enclose ("(declare-" ^ BNF_FP_Util.co_prefix fp ^ "datatypes () (") "))\n" + (space_implode "\n " (map sdatatype dtyps))) + +fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts = Buffer.empty |> fold (Buffer.add o enclose "; " "\n") comments |> fold (fn (k, v) => Buffer.add ("(set-option " ^ k ^ " " ^ v ^ ")\n")) smt_options |> Buffer.add logic |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts) - |> (if null lfp_dtyps then I - else Buffer.add (enclose "(declare-datatypes () (" "))\n" - (space_implode "\n " (maps (map sdatatype) lfp_dtyps)))) - |> (if null gfp_dtyps then I - else Buffer.add (enclose "(declare-codatatypes () (" "))\n" - (space_implode "\n " (maps (map sdatatype) gfp_dtyps)))) + |> fold sdtyp (AList.coalesce (op =) dtyps) |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun) (sort (fast_string_ord o pairself fst) funcs) |> fold (fn (i, t) => Buffer.add (enclose "(assert " ")\n"