--- a/src/HOL/Nunchaku/Tools/nunchaku_collect.ML Wed Oct 26 16:15:37 2016 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_collect.ML Wed Oct 26 17:32:50 2016 +0200
@@ -35,7 +35,7 @@
datatype isa_command =
ITVal of typ * (int option * int option)
- | ICopy of isa_type_spec
+ | ITypedef of isa_type_spec
| IQuotient of isa_type_spec
| ICoData of BNF_Util.fp_kind * isa_co_data_spec list
| IVal of term
@@ -96,7 +96,7 @@
datatype isa_command =
ITVal of typ * (int option * int option)
-| ICopy of isa_type_spec
+| ITypedef of isa_type_spec
| IQuotient of isa_type_spec
| ICoData of BNF_Util.fp_kind * isa_co_data_spec list
| IVal of term
@@ -211,7 +211,7 @@
@{const_name implies}, @{const_name Not}, @{const_name The}, @{const_name The_unsafe},
@{const_name True}];
-datatype type_classification = Builtin | TVal | Copy | Quotient | Co_Datatype;
+datatype type_classification = Builtin | TVal | Typedef | Quotient | Co_Datatype;
fun classify_type_name ctxt T_name =
if is_type_builtin T_name then
@@ -229,10 +229,10 @@
SOME _ => Quotient
| NONE =>
if T_name = @{type_name set} then
- Copy
+ Typedef
else
(case Typedef.get_info ctxt T_name of
- _ :: _ => Copy
+ _ :: _ => Typedef
| [] => TVal))));
fun fp_kind_of_ctr_sugar_kind Ctr_Sugar.Codatatype = BNF_Util.Greatest_FP
@@ -270,17 +270,17 @@
(qtyp, rtyp, equiv_rel, abs, rep)
end);
-fun copy_of ctxt T_name =
+fun typedef_of ctxt T_name =
if T_name = @{type_name set} then
let
val A = Logic.varifyT_global @{typ 'a};
val absT = Type (@{type_name set}, [A]);
val repT = A --> HOLogic.boolT;
- val wrt = Abs (Name.uu, repT, @{const True});
+ val pred = Abs (Name.uu, repT, @{const True});
val abs = Const (@{const_name Collect}, repT --> absT);
val rep = Const (@{const_name rmember}, absT --> repT);
in
- (absT, repT, wrt, abs, rep)
+ (absT, repT, pred, abs, rep)
end
else
(case Typedef.get_info ctxt T_name of
@@ -291,14 +291,15 @@
let
val absT = Logic.varifyT_global abs_type;
val repT = Logic.varifyT_global rep_type;
- val wrt = Thm.prop_of Rep
+ val set = Thm.prop_of Rep
|> HOLogic.dest_Trueprop
|> HOLogic.dest_mem
|> snd;
+ val pred = Abs (Name.uu, repT, HOLogic.mk_mem (Bound 0, set));
val abs = Const (Abs_name, repT --> absT);
val rep = Const (Rep_name, absT --> repT);
in
- (absT, repT, wrt, abs, rep)
+ (absT, repT, pred, abs, rep)
end);
fun is_co_datatype_ctr ctxt (s, T) =
@@ -365,44 +366,44 @@
(_, _, _, _, Const (s', _)) => s' = s)
| _ => false);
-fun is_maybe_copy_abs ctxt absT_name s =
+fun is_maybe_typedef_abs ctxt absT_name s =
if absT_name = @{type_name set} then
s = @{const_name Collect}
else
- (case try (copy_of ctxt) absT_name of
+ (case try (typedef_of ctxt) absT_name of
SOME (_, _, _, Const (s', _), _) => s' = s
| NONE => false);
-fun is_maybe_copy_rep ctxt absT_name s =
+fun is_maybe_typedef_rep ctxt absT_name s =
if absT_name = @{type_name set} then
s = @{const_name rmember}
else
- (case try (copy_of ctxt) absT_name of
+ (case try (typedef_of ctxt) absT_name of
SOME (_, _, _, _, Const (s', _)) => s' = s
| NONE => false);
-fun is_copy_abs ctxt (s, T) =
+fun is_typedef_abs ctxt (s, T) =
(case T of
Type (@{type_name fun}, [_, Type (absT_name, _)]) =>
- classify_type_name ctxt absT_name = Copy andalso is_maybe_copy_abs ctxt absT_name s
+ classify_type_name ctxt absT_name = Typedef andalso is_maybe_typedef_abs ctxt absT_name s
| _ => false);
-fun is_copy_rep ctxt (s, T) =
+fun is_typedef_rep ctxt (s, T) =
(case T of
Type (@{type_name fun}, [Type (absT_name, _), _]) =>
- classify_type_name ctxt absT_name = Copy andalso is_maybe_copy_rep ctxt absT_name s
+ classify_type_name ctxt absT_name = Typedef andalso is_maybe_typedef_rep ctxt absT_name s
| _ => false);
-fun is_stale_copy_abs ctxt (s, T) =
+fun is_stale_typedef_abs ctxt (s, T) =
(case T of
Type (@{type_name fun}, [_, Type (absT_name, _)]) =>
- classify_type_name ctxt absT_name <> Copy andalso is_maybe_copy_abs ctxt absT_name s
+ classify_type_name ctxt absT_name <> Typedef andalso is_maybe_typedef_abs ctxt absT_name s
| _ => false);
-fun is_stale_copy_rep ctxt (s, T) =
+fun is_stale_typedef_rep ctxt (s, T) =
(case T of
Type (@{type_name fun}, [Type (absT_name, _), _]) =>
- classify_type_name ctxt absT_name <> Copy andalso is_maybe_copy_rep ctxt absT_name s
+ classify_type_name ctxt absT_name <> Typedef andalso is_maybe_typedef_rep ctxt absT_name s
| _ => false);
fun instantiate_constant_types_in_term ctxt csts target =
@@ -551,7 +552,7 @@
#> map Thm.prop_of;
fun keys_of _ (ITVal (T, _)) = [key_of_typ T]
- | keys_of _ (ICopy {abs_typ, ...}) = [key_of_typ abs_typ]
+ | keys_of _ (ITypedef {abs_typ, ...}) = [key_of_typ abs_typ]
| keys_of _ (IQuotient {abs_typ, ...}) = [key_of_typ abs_typ]
| keys_of _ (ICoData (_, specs)) = map (key_of_typ o #typ) specs
| keys_of ctxt (IVal const) = [key_of_const ctxt const]
@@ -570,7 +571,7 @@
fold (add_keys ctxt) props [] |> subtract (op =) (map (key_of_const ctxt) consts);
fun deps_of _ (ITVal _) = []
- | deps_of ctxt (ICopy {wrt, ...}) = add_keys ctxt wrt []
+ | deps_of ctxt (ITypedef {wrt, ...}) = add_keys ctxt wrt []
| deps_of ctxt (IQuotient {wrt, ...}) = add_keys ctxt wrt []
| deps_of ctxt (ICoData (_, specs)) = maps (co_data_spec_deps_of ctxt) specs
| deps_of _ (IVal const) = add_type_keys (fastype_of const) []
@@ -646,7 +647,7 @@
val typedecls = filter (can (fn ITVal _ => ())) cmds;
val (mixed, complete) =
- (filter (can (fn ICopy _ => () | IQuotient _ => () | ICoData _ => () | IVal _ => ()
+ (filter (can (fn ITypedef _ => () | IQuotient _ => () | ICoData _ => () | IVal _ => ()
| ICoPred _ => () | IRec _ => () | ISpec _ => ())) cmds, true)
|> sort_problem;
val axioms = filter (can (fn IAxiom _ => ())) cmds;
@@ -657,7 +658,7 @@
end;
fun group_of (ITVal _) = 1
- | group_of (ICopy _) = 2
+ | group_of (ITypedef _) = 2
| group_of (IQuotient _) = 3
| group_of (ICoData _) = 4
| group_of (IVal _) = 5
@@ -876,7 +877,7 @@
val seenT = T :: seenT;
val seens = (seenS, seenT, seen);
- fun consider_quotient_or_copy tuple_of s =
+ fun consider_quotient_or_typedef iquotient_or_itypedef tuple_of s =
let
val (T0, repT0, wrt0, abs0, rep0) = tuple_of ctxt s;
val tyenv = Sign.typ_match thy (T0, T) Vartab.empty;
@@ -887,7 +888,7 @@
val abs = subst abs0;
val rep = subst rep0;
in
- apsnd (cons (ICopy {abs_typ = T, rep_typ = repT, wrt = wrt, abs = abs,
+ apsnd (cons (iquotient_or_itypedef {abs_typ = T, rep_typ = repT, wrt = wrt, abs = abs,
rep = rep}))
#> consider_term (depth + 1) wrt
end;
@@ -910,8 +911,8 @@
((seenS, union (op =) fpTs seenT, seen), ICoData (fp, specs) :: problem))
#> fold (fold (consider_type (depth + 1) o fastype_of)) ctrss
end
- | Quotient => consider_quotient_or_copy quotient_of s
- | Copy => consider_quotient_or_copy copy_of s
+ | Quotient => consider_quotient_or_typedef IQuotient quotient_of s
+ | Typedef => consider_quotient_or_typedef ITypedef typedef_of s
| TVal => apsnd (cons (ITVal (T, card_of T)))))
end
and consider_term depth t =
@@ -936,10 +937,10 @@
Const (x as (s, T)) =>
(if is_const_builtin s orelse is_co_datatype_ctr ctxt x orelse
is_co_datatype_case ctxt x orelse is_quotient_abs ctxt x orelse
- is_quotient_rep ctxt x orelse is_copy_abs ctxt x orelse
- is_copy_rep ctxt x then
+ is_quotient_rep ctxt x orelse is_typedef_abs ctxt x orelse
+ is_typedef_rep ctxt x then
(seens, problem)
- else if is_stale_copy_abs ctxt x orelse is_stale_copy_rep ctxt x then
+ else if is_stale_typedef_abs ctxt x orelse is_stale_typedef_rep ctxt x then
raise UNSUPPORTED_FUNC t
else
(case spec_rules_of ctxt x of
@@ -1086,7 +1087,7 @@
fun str_of_isa_command ctxt (ITVal (T, cards)) =
"type " ^ Syntax.string_of_typ ctxt T ^ str_of_isa_cards_suffix cards
- | str_of_isa_command ctxt (ICopy spec) = "copy " ^ str_of_isa_type_spec ctxt spec
+ | str_of_isa_command ctxt (ITypedef spec) = "typedef " ^ str_of_isa_type_spec ctxt spec
| str_of_isa_command ctxt (IQuotient spec) = "quotient " ^ str_of_isa_type_spec ctxt spec
| str_of_isa_command ctxt (ICoData (fp, specs)) =
BNF_Util.case_fp fp "data" "codata" ^ " " ^ str_of_and_list (str_of_isa_co_data_spec ctxt) specs
--- a/src/HOL/Nunchaku/Tools/nunchaku_problem.ML Wed Oct 26 16:15:37 2016 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_problem.ML Wed Oct 26 17:32:50 2016 +0200
@@ -19,10 +19,11 @@
| NMatch of tm * (ident * tm list * tm) list
| NApp of tm * tm
- type nun_type_spec =
+ type nun_copy_spec =
{abs_ty: ty,
rep_ty: ty,
- wrt: tm,
+ subset: tm option,
+ quotient: tm option,
abs: tm,
rep: tm}
@@ -44,8 +45,7 @@
datatype nun_command =
NTVal of ty * (int option * int option)
- | NCopy of nun_type_spec
- | NQuotient of nun_type_spec
+ | NCopy of nun_copy_spec
| NData of nun_co_data_spec list
| NCodata of nun_co_data_spec list
| NVal of tm * ty
@@ -116,6 +116,7 @@
val nun_rparen: string
val nun_semicolon: string
val nun_spec: string
+ val nun_subset: string
val nun_then: string
val nun_true: string
val nun_type: string
@@ -125,7 +126,6 @@
val nun_val: string
val nun_wf: string
val nun_with: string
- val nun_wrt: string
val nun__witness_of: string
val ident_of_str: string -> ident
@@ -192,10 +192,11 @@
| NMatch of tm * (ident * tm list * tm) list
| NApp of tm * tm;
-type nun_type_spec =
+type nun_copy_spec =
{abs_ty: ty,
rep_ty: ty,
- wrt: tm,
+ subset: tm option,
+ quotient: tm option,
abs: tm,
rep: tm};
@@ -217,8 +218,7 @@
datatype nun_command =
NTVal of ty * (int option * int option)
-| NCopy of nun_type_spec
-| NQuotient of nun_type_spec
+| NCopy of nun_copy_spec
| NData of nun_co_data_spec list
| NCodata of nun_co_data_spec list
| NVal of tm * ty
@@ -289,6 +289,7 @@
val nun_rparen = ")";
val nun_semicolon = ";";
val nun_spec = "spec";
+val nun_subset = "subset";
val nun_then = "then";
val nun_true = "true";
val nun_type = "type";
@@ -298,7 +299,6 @@
val nun_val = "val";
val nun_wf = "wf";
val nun_with = "with";
-val nun_wrt = "wrt";
val nun__witness_of = "_witness_of";
val nun_parens = enclose nun_lparen nun_rparen;
@@ -415,6 +415,9 @@
([], app)
| strip_nun_binders _ tm = ([], tm);
+fun fold_map_option _ NONE = pair NONE
+ | fold_map_option f (SOME x) = f x #>> SOME;
+
fun fold_map_ty_idents f (NType (id, tys)) =
f id
##>> fold_map (fold_map_ty_idents f) tys
@@ -446,14 +449,15 @@
##>> fold_map_tm_idents f arg
#>> NApp;
-fun fold_map_nun_type_spec_idents f {abs_ty, rep_ty, wrt, abs, rep} =
+fun fold_map_nun_copy_spec_idents f {abs_ty, rep_ty, subset, quotient, abs, rep} =
fold_map_ty_idents f abs_ty
##>> fold_map_ty_idents f rep_ty
- ##>> fold_map_tm_idents f wrt
+ ##>> fold_map_option (fold_map_tm_idents f) subset
+ ##>> fold_map_option (fold_map_tm_idents f) quotient
##>> fold_map_tm_idents f abs
##>> fold_map_tm_idents f rep
- #>> (fn ((((abs_ty, rep_ty), wrt), abs), rep) =>
- {abs_ty = abs_ty, rep_ty = rep_ty, wrt = wrt, abs = abs, rep = rep});
+ #>> (fn (((((abs_ty, rep_ty), subset), quotient), abs), rep) =>
+ {abs_ty = abs_ty, rep_ty = rep_ty, subset = subset, quotient = quotient, abs = abs, rep = rep});
fun fold_map_nun_ctr_spec_idents f {ctr, arg_tys} =
fold_map_tm_idents f ctr
@@ -479,11 +483,8 @@
fold_map_ty_idents f ty
#>> (rpair cards #> NTVal)
| fold_map_nun_command_idents f (NCopy spec) =
- fold_map_nun_type_spec_idents f spec
+ fold_map_nun_copy_spec_idents f spec
#>> NCopy
- | fold_map_nun_command_idents f (NQuotient spec) =
- fold_map_nun_type_spec_idents f spec
- #>> NQuotient
| fold_map_nun_command_idents f (NData specs) =
fold_map (fold_map_nun_co_data_spec_idents f) specs
#>> NData
@@ -727,13 +728,18 @@
str_of_ident id ^ " " ^ nun_colon ^ " " ^
fold (K (prefix (nun_type ^ " " ^ nun_arrow ^ " "))) tys nun_type;
-fun is_triv_wrt (NAbs (_, body)) = is_triv_wrt body
- | is_triv_wrt (NConst (id, _, _)) = (id = nun_true)
- | is_triv_wrt _ = false;
+fun is_triv_subset (NAbs (_, body)) = is_triv_subset body
+ | is_triv_subset (NConst (id, _, _)) = (id = nun_true)
+ | is_triv_subset _ = false;
-fun str_of_nun_type_spec {abs_ty, rep_ty, wrt, abs, rep} =
+fun str_of_nun_copy_spec {abs_ty, rep_ty, subset, quotient, abs, rep} =
str_of_ty abs_ty ^ " " ^ nun_assign ^ " " ^ str_of_ty rep_ty ^
- (if is_triv_wrt wrt then "" else "\n " ^ nun_wrt ^ " " ^ str_of_tm wrt) ^
+ (case subset of
+ NONE => ""
+ | SOME s => if is_triv_subset s then "" else "\n " ^ nun_subset ^ " " ^ str_of_tm s) ^
+ (case quotient of
+ NONE => ""
+ | SOME q => "\n " ^ nun_quotient ^ " " ^ str_of_tm q) ^
"\n " ^ nun_abstract ^ " " ^ str_of_tm abs ^ "\n " ^ nun_concrete ^ " " ^ str_of_tm rep;
fun str_of_nun_ctr_spec {ctr, arg_tys} =
@@ -762,8 +768,7 @@
fun str_of_nun_command (NTVal (ty, cards)) =
nun_val ^ " " ^ str_of_tval ty ^ str_of_nun_cards_suffix cards
- | str_of_nun_command (NCopy spec) = nun_copy ^ " " ^ str_of_nun_type_spec spec
- | str_of_nun_command (NQuotient spec) = nun_quotient ^ " " ^ str_of_nun_type_spec spec
+ | str_of_nun_command (NCopy spec) = nun_copy ^ " " ^ str_of_nun_copy_spec spec
| str_of_nun_command (NData specs) =
nun_data ^ " " ^ str_of_nun_and_list str_of_nun_co_data_spec specs
| str_of_nun_command (NCodata specs) =
--- a/src/HOL/Nunchaku/Tools/nunchaku_translate.ML Wed Oct 26 16:15:37 2016 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_translate.ML Wed Oct 26 17:32:50 2016 +0200
@@ -144,9 +144,13 @@
val tm_of_isa = gen_tm_of_isa false;
val prop_of_isa = gen_tm_of_isa true;
-fun nun_type_spec_of_isa ctxt {abs_typ, rep_typ, wrt, abs, rep} =
- {abs_ty = ty_of_isa abs_typ, rep_ty = ty_of_isa rep_typ, wrt = tm_of_isa ctxt wrt,
- abs = tm_of_isa ctxt abs, rep = tm_of_isa ctxt rep};
+fun nun_copy_spec_of_isa_typedef ctxt {abs_typ, rep_typ, wrt, abs, rep} =
+ {abs_ty = ty_of_isa abs_typ, rep_ty = ty_of_isa rep_typ, subset = SOME (tm_of_isa ctxt wrt),
+ quotient = NONE, abs = tm_of_isa ctxt abs, rep = tm_of_isa ctxt rep};
+
+fun nun_copy_spec_of_isa_quotient ctxt {abs_typ, rep_typ, wrt, abs, rep} =
+ {abs_ty = ty_of_isa abs_typ, rep_ty = ty_of_isa rep_typ, subset = NONE,
+ quotient = SOME (tm_of_isa ctxt wrt), abs = tm_of_isa ctxt abs, rep = tm_of_isa ctxt rep};
fun nun_ctr_of_isa ctxt ctr =
{ctr = tm_of_isa ctxt ctr, arg_tys = map ty_of_isa (binder_types (fastype_of ctr))};
@@ -168,8 +172,8 @@
fun cmd_of cmd =
(case cmd of
ITVal (T, cards) => NTVal (ty_of_isa T, cards)
- | ICopy spec => NCopy (nun_type_spec_of_isa ctxt spec)
- | IQuotient spec => NQuotient (nun_type_spec_of_isa ctxt spec)
+ | ITypedef spec => NCopy (nun_copy_spec_of_isa_typedef ctxt spec)
+ | IQuotient spec => NCopy (nun_copy_spec_of_isa_quotient ctxt spec)
| ICoData (fp, specs) =>
BNF_Util.case_fp fp NData NCodata (map (nun_co_data_spec_of_isa ctxt) specs)
| IVal t => NVal (tm_of_isa ctxt t, ty_of_isa (fastype_of t))