nominal2: comparison Nominal/Fv.thy

equal deleted inserted replaced

-:9911824a5396
+:ed89a26b7074
 ML {*
 datatype alpha_type = AlphaGen | AlphaRes | AlphaLst;
 *}
 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})
 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
 | is_atom_set _ _ = false;
 ML {*
 fun gather_binds binds =
 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) =
+fun find_bodys (sf, sbi, sty) =
-filter (fn (f, bi, _) => f = sf andalso bi = sbi) binds
+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
+val bodys = map ((map (fn (_, _, bo, _) => bo)) o find_bodys) nodups
 in
 nodups ~~ bodys
 end
 in
 map (map gather_binds_cons) binds
 end
 *}
 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"};
 fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];
 fun mk_union sets =
 ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}
 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)))
 end
 *}
 in
 ((bn, fvbn), eqs)
 end
 *}
+ML {* print_depth 100 *}
 ML {*
 fun fv_bns thy dt_info fv_frees rel_bns =
 let
 fun mk_fvbn_free (bn, ith, _) =
 let
 (* 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 *)
 ML {*
 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy =
 val args2 = map Free (names2 ~~ Ts);
 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
 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
 SOME f =>
 (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of
 if ((is_atom_set thy) o fastype_of) x then mk_atom_set x else
 if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset x else
 (* 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
 end;
 val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq
 (fv_c $ list_comb (c, args), mk_union (map fv_arg  (dts ~~ args ~~ arg_nos))))
 val alpha_rhs =
 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_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_in_comp_binds = filter (fn ((SOME _, i, _, _), _) => i = arg_no | _ => false) bind_pis;
-val rel_has_binds = filter (fn ((NONE, _, j), _) => j = arg_no
+val rel_has_binds = filter (fn ((NONE, _, j, _), _) => j = arg_no
-| ((SOME (_, false), _, 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;
+(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
 ([], [], [], []) =>
 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
 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;
 val lhs_binds = fv_binds args rbinds
 val lhs_arg = foldr1 HOLogic.mk_prod bound_args
 val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos);
 val fv = mk_compound_fv fvs;
 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
 end
 else
 val rhs_binds = fv_binds args2 rbinds;
 val rhs = mk_pair (rhs_binds, arg2);
 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
 end
 | _ => error "Fv.alpha: not supported binding structure"

changeset 1670	ed89a26b7074
parent 1669	9911824a5396
child 1672	94b8b70f7bc0