--- 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
--- 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
*}