--- a/Nominal/Fv.thy Tue Mar 23 11:43:09 2010 +0100
+++ b/Nominal/Fv.thy Tue Mar 23 16:28:29 2010 +0100
@@ -278,15 +278,15 @@
end
*}
+ML AList.lookup
+
(* We assume no bindings in the type on which bn is defined *)
(* TODO: currently works only with current fv_bn function *)
ML {*
-fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) =
+fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn (fvbn, (bn, ith_dtyp, args_in_bns)) =
let
val {descr, sorts, ...} = dt_info;
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
- val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
- val fvbn = Free (fvbn_name, fastype_of (nth fv_frees ith_dtyp));
fun fv_bn_constr (cname, dts) args_in_bn =
let
val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -296,16 +296,18 @@
fun fv_arg ((dt, x), arg_no) =
let
val ty = fastype_of x
+ val _ = tracing (PolyML.makestring args_in_bn);
+ val _ = tracing (PolyML.makestring bn_fvbn);
in
- if arg_no mem args_in_bn then
- (if is_rec_type dt then
- (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.")
- else @{term "{} :: atom set"}) else
- if is_atom thy ty then mk_single_atom x else
- if is_atom_set thy ty then mk_atom_set x else
- if is_atom_fset thy ty then mk_atom_fset x else
- if is_rec_type dt then nth fv_frees (body_index dt) $ x else
- @{term "{} :: atom set"}
+ case AList.lookup (op=) args_in_bn arg_no of
+ SOME NONE => @{term "{} :: atom set"}
+ | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
+ | NONE =>
+ if is_atom thy ty then mk_single_atom x else
+ if is_atom_set thy ty then mk_atom_set x else
+ if is_atom_fset thy ty then mk_atom_fset x else
+ if is_rec_type dt then nth fv_frees (body_index dt) $ x else
+ @{term "{} :: atom set"}
end;
val arg_nos = 0 upto (length dts - 1)
in
@@ -315,20 +317,33 @@
val (_, (_, _, constrs)) = nth descr ith_dtyp;
val eqs = map2i fv_bn_constr constrs args_in_bns
in
- ((bn, fvbn), (fvbn_name, eqs))
+ ((bn, fvbn), eqs)
end
*}
ML {*
-fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) =
+fun fv_bns thy dt_info fv_frees rel_bns =
+let
+ fun mk_fvbn_free (bn, ith, _) =
+ let
+ val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
+ in
+ (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))
+ end;
+ val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free rel_bns);
+ val bn_fvbn = (map (fn (bn, _, _) => bn) rel_bns) ~~ fvbn_frees
+ val (l1, l2) = split_list (map (fv_bn thy dt_info fv_frees bn_fvbn) (fvbn_frees ~~ rel_bns));
+in
+ (l1, (fvbn_names ~~ l2))
+end
+*}
+
+
+ML {*
+fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees bn_alphabn ((bn, ith_dtyp, args_in_bns), (alpha_bn_free, is_rec)) =
let
val {descr, sorts, ...} = dt_info;
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
- val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
- val alpha_bn_type =
- (*if is_rec then @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} else*)
- nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool};
- val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type);
val pi = Free("pi", @{typ perm})
fun alpha_bn_constr (cname, dts) args_in_bn =
let
@@ -345,12 +360,12 @@
val argty = fastype_of arg;
val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty);
in
- if is_rec_type dt then
- if arg_no mem args_in_bn then alpha_bn_free $ arg $ arg2
- else (nth alpha_frees (body_index dt)) $ arg $ arg2
- else
- if arg_no mem args_in_bn then @{term True}
- else HOLogic.mk_eq (arg, arg2)
+ case AList.lookup (op=) args_in_bn arg_no of
+ SOME NONE => @{term True}
+ | SOME (SOME f) => (the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2
+ | NONE =>
+ if is_rec_type dt then (nth alpha_frees (body_index dt)) $ arg $ arg2
+ else HOLogic.mk_eq (arg, arg2)
end
val arg_nos = 0 upto (length dts - 1)
val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))
@@ -361,10 +376,33 @@
val (_, (_, _, constrs)) = nth descr ith_dtyp;
val eqs = map2i alpha_bn_constr constrs args_in_bns
in
- ((bn, alpha_bn_free), (alpha_bn_name, eqs))
+ ((bn, alpha_bn_free), eqs)
end
*}
+ML {*
+fun alpha_bns thy dt_info alpha_frees rel_bns bns_rec =
+let
+ val {descr, sorts, ...} = dt_info;
+ fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+ fun mk_alphabn_free (bn, ith, _) =
+ let
+ val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
+ val alphabn_type = nth_dtyp ith --> nth_dtyp ith --> @{typ bool};
+ val alphabn_free = Free(alphabn_name, alphabn_type);
+ in
+ (alphabn_name, alphabn_free)
+ end;
+ val (alphabn_names, alphabn_frees) = split_list (map mk_alphabn_free rel_bns);
+ val bn_alphabn = (map (fn (bn, _, _) => bn) rel_bns) ~~ alphabn_frees;
+ val pair = split_list (map (alpha_bn thy dt_info alpha_frees bn_alphabn)
+ (rel_bns ~~ (alphabn_frees ~~ bns_rec)))
+in
+ (alphabn_names, pair)
+end
+*}
+
+
(* Checks that a list of bindings contains only compatible ones *)
ML {*
fun bns_same l =
@@ -384,7 +422,7 @@
val fv_frees = map Free (fv_names ~~ fv_types);
val nr_bns = non_rec_binds bindsall;
val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;
- val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns);
+ val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns;
val fvbns = map snd bn_fv_bns;
val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
@@ -393,8 +431,8 @@
val alpha_frees = map Free (alpha_names ~~ alpha_types);
(* We assume that a bn is either recursive or not *)
val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;
- val (bn_alpha_bns, alpha_bn_names_eqs) = split_list (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec))
- val (alpha_bn_names, alpha_bn_eqs) = split_list alpha_bn_names_eqs;
+ val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) =
+ alpha_bns thy dt_info alpha_frees bns bns_rec
val alpha_bn_frees = map snd bn_alpha_bns;
val alpha_bn_types = map fastype_of alpha_bn_frees;
fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =