# HG changeset patch # User blanchet # Date 1477495970 -7200 # Node ID 0af9926e130397ebc31331d3ac23142f29f01310 # Parent 89da169f66fa423874ea505fe243dc747ba4422d adapted Nunchaku's input syntax to new design decisions diff -r 89da169f66fa -r 0af9926e1303 src/HOL/Nunchaku/Tools/nunchaku_collect.ML --- 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 diff -r 89da169f66fa -r 0af9926e1303 src/HOL/Nunchaku/Tools/nunchaku_problem.ML --- 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) = diff -r 89da169f66fa -r 0af9926e1303 src/HOL/Nunchaku/Tools/nunchaku_translate.ML --- 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))