# HG changeset patch # User Cezary Kaliszyk # Date 1269673871 -3600 # Node ID ed89a26b70748d27e3fe461707f159d4cc82713f # Parent 9911824a53962fdd2c8ca68148fd27468951d10b Fv/Alpha now takes into account Alpha_Type given from the parser. diff -r 9911824a5396 -r ed89a26b7074 Nominal/ExTySch.thy --- a/Nominal/ExTySch.thy Sat Mar 27 06:51:13 2010 +0100 +++ b/Nominal/ExTySch.thy Sat Mar 27 08:11:11 2010 +0100 @@ -5,6 +5,7 @@ (* Type Schemes *) atom_decl name +(*ML {* val _ = alpha_type := AlphaRes *}*) nominal_datatype t = Var "name" | Fun "t" "t" diff -r 9911824a5396 -r ed89a26b7074 Nominal/Fv.thy --- a/Nominal/Fv.thy Sat Mar 27 06:51:13 2010 +0100 +++ b/Nominal/Fv.thy Sat Mar 27 08:11:11 2010 +0100 @@ -140,6 +140,19 @@ *} ML {* +fun atyp_const AlphaGen = @{const_name alpha_gen} + | atyp_const AlphaRes = @{const_name alpha_res} + | atyp_const AlphaLst = @{const_name alpha_lst} +*} + +(* TODO: make sure that parser checks that bindings are compatible *) +ML {* +fun alpha_const_for_binds [] = atyp_const AlphaGen + | alpha_const_for_binds ((NONE, _, _, at) :: t) = atyp_const at + | alpha_const_for_binds ((SOME (_, _), _, _, at) :: _) = atyp_const at +*} + +ML {* fun is_atom thy typ = Sign.of_sort thy (typ, @{sort at}) @@ -167,11 +180,11 @@ let fun gather_binds_cons binds = let - val common = map (fn (f, bi, _) => (f, bi)) binds + val common = map (fn (f, bi, _, aty) => (f, bi, aty)) binds val nodups = distinct (op =) common - fun find_bodys (sf, sbi) = - filter (fn (f, bi, _) => f = sf andalso bi = sbi) binds - val bodys = map ((map (fn (_, _, bo) => bo)) o find_bodys) nodups + fun find_bodys (sf, sbi, sty) = + filter (fn (f, bi, _, aty) => f = sf andalso bi = sbi andalso aty = sty) binds + val bodys = map ((map (fn (_, _, bo, _) => bo)) o find_bodys) nodups in nodups ~~ bodys end @@ -182,11 +195,13 @@ ML {* fun un_gather_binds_cons binds = - flat (map (fn (((f, bi), bos), pi) => map (fn bo => ((f, bi, bo), pi)) bos) binds) + flat (map (fn (((f, bi, aty), bos), pi) => map (fn bo => ((f, bi, bo, aty), pi)) bos) binds) *} ML {* open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); +*} +ML {* (* TODO: It is the same as one in 'nominal_atoms' *) fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom}); val noatoms = @{term "{} :: atom set"}; @@ -263,7 +278,7 @@ ML {* fun non_rec_binds l = let - fun is_non_rec (SOME (f, false), _, _) = SOME f + fun is_non_rec (SOME (f, false), _, _, _) = SOME f | is_non_rec _ = NONE in distinct (op =) (map_filter is_non_rec (flat (flat l))) @@ -311,6 +326,7 @@ end *} +ML {* print_depth 100 *} ML {* fun fv_bns thy dt_info fv_frees rel_bns = let @@ -390,7 +406,7 @@ (* Checks that a list of bindings contains only compatible ones *) ML {* fun bns_same l = - length (distinct (op =) (map (fn ((b, _, _), _) => b) l)) = 1 + length (distinct (op =) (map (fn ((b, _, _, atyp), _) => (b, atyp)) l)) = 1 *} (* TODO: Notice datatypes without bindings and replace alpha with equality *) @@ -441,16 +457,16 @@ val fv_c = nth fv_frees ith_dtyp; val alpha = nth alpha_frees ith_dtyp; val arg_nos = 0 upto (length dts - 1) - fun fv_bind args (NONE, i, _) = + fun fv_bind args (NONE, i, _, _) = if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else (* TODO we do not know what to do with non-atomizable things *) @{term "{} :: atom set"} - | fv_bind args (SOME (f, _), i, _) = f $ (nth args i); + | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i); fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) - fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE + fun find_nonrec_binder j (SOME (f, false), i, _, _) = if i = j then SOME f else NONE | find_nonrec_binder _ _ = NONE fun fv_arg ((dt, x), arg_no) = case get_first (find_nonrec_binder arg_no) bindcs of @@ -468,7 +484,7 @@ (* TODO we do not know what to do with non-atomizable things *) @{term "{} :: atom set"}; (* If i = j then we generate it only once *) - val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; + val relevant = filter (fn (_, i, j, _) => ((i = arg_no) orelse (j = arg_no))) bindcs; val sub = fv_binds args relevant in mk_diff arg sub @@ -479,13 +495,13 @@ HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); fun alpha_arg ((dt, arg_no), (arg, arg2)) = let - val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis; - val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis; - val rel_has_binds = filter (fn ((NONE, _, j), _) => j = arg_no - | ((SOME (_, false), _, j), _) => j = arg_no + val rel_in_simp_binds = filter (fn ((NONE, i, _, _), _) => i = arg_no | _ => false) bind_pis; + val rel_in_comp_binds = filter (fn ((SOME _, i, _, _), _) => i = arg_no | _ => false) bind_pis; + val rel_has_binds = filter (fn ((NONE, _, j, _), _) => j = arg_no + | ((SOME (_, false), _, j, _), _) => j = arg_no | _ => false) bind_pis; - val rel_has_rec_binds = filter - (fn ((SOME (_, true), _, j), _) => j = arg_no | _ => false) bind_pis; + val rel_has_rec_binds = filter + (fn ((SOME (_, true), _, j, _), _) => j = arg_no | _ => false) bind_pis; in case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds, rel_has_rec_binds) of ([], [], [], []) => @@ -493,12 +509,12 @@ else (HOLogic.mk_eq (arg, arg2)) | (_, [], [], []) => @{term True} | ([], [], [], _) => @{term True} - | ([], ((((SOME (bn, is_rec)), _, _), _) :: _), [], []) => + | ([], ((((SOME (bn, is_rec)), _, _, atyp), _) :: _), [], []) => if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else if is_rec then let val (rbinds, rpis) = split_list rel_in_comp_binds - val bound_in_nos = map (fn (_, _, i) => i) rbinds + val bound_in_nos = map (fn (_, _, i, _) => i) rbinds val bound_in_ty_nos = map (fn i => body_index (nth dts i)) bound_in_nos; val bound_args = arg :: map (nth args) bound_in_nos; val bound_args2 = arg2 :: map (nth args2) bound_in_nos; @@ -513,7 +529,7 @@ val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos); val alpha = mk_compound_alpha alphas; val pi = foldr1 add_perm (distinct (op =) rpis); - val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; + val alpha_gen_pre = Const (atyp_const atyp, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; val alpha_gen = Syntax.check_term lthy alpha_gen_pre in alpha_gen @@ -535,7 +551,8 @@ val alpha = nth alpha_frees (body_index dt); val fv = nth fv_frees (body_index dt); val pi = foldr1 add_perm (distinct (op =) rpis); - val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; + val alpha_const = alpha_const_for_binds rbinds; + val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; val alpha_gen = Syntax.check_term lthy alpha_gen_pre in alpha_gen diff -r 9911824a5396 -r ed89a26b7074 Nominal/Nominal2_Supp.thy --- a/Nominal/Nominal2_Supp.thy Sat Mar 27 06:51:13 2010 +0100 +++ b/Nominal/Nominal2_Supp.thy Sat Mar 27 08:11:11 2010 +0100 @@ -415,7 +415,7 @@ apply(rule conjI) prefer 2 apply(auto)[1] -apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2)) +apply (metis permute_atom_def_raw permute_minus_cancel(2)) defer apply(rule psubset_card_mono) apply(simp add: finite_supp) diff -r 9911824a5396 -r ed89a26b7074 Nominal/Parser.thy --- a/Nominal/Parser.thy Sat Mar 27 06:51:13 2010 +0100 +++ b/Nominal/Parser.thy Sat Mar 27 08:11:11 2010 +0100 @@ -141,10 +141,14 @@ end *} +ML {* +fun apfst3 f (a, b, c) = (f a, b, c) +*} + ML {* fun rawify_binds dts_env cnstrs_env bn_fun_env binds = - map (map (map (map (fn (opt_trm, i, j) => - (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j))))) binds + map (map (map (map (fn (opt_trm, i, j, aty) => + (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j, aty))))) binds *} ML {* @@ -152,8 +156,6 @@ | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y *} -ML {* @{term "{x, y}"} *} -ML range_type ML {* fun strip_union t = case t of @@ -291,9 +293,6 @@ ML {* val cheat_fv_rsp = Unsynchronized.ref false *} ML {* val cheat_const_rsp = Unsynchronized.ref false *} -ML {* fun map_option _ NONE = NONE - | map_option f (SOME x) = SOME (f x) *} - (* nominal_datatype2 does the following things in order: 1) define the raw datatype 2) define the raw binding functions @@ -340,7 +339,7 @@ val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) = raw_nominal_decls dts bn_funs bn_eqs binds lthy val morphism_2_1 = ProofContext.export_morphism lthy2 lthy - fun export_fun f (t, l) = (f t, map (map (apsnd (map_option f))) l); + fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_1)))) raw_bns; val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc @@ -572,6 +571,7 @@ ML {* val recursive = Unsynchronized.ref false +val alpha_type = Unsynchronized.ref AlphaGen *} ML {* @@ -602,7 +602,8 @@ end in - map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)) + map (map (map (map (fn (a, b, c) => (a, b, c, !alpha_type))))) + (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) end *}