--- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 15:46:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 15:53:07 2010 -0800
@@ -168,7 +168,6 @@
map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
fun one_con (con,args,mx) : cons =
(Binding.name_of con, (* FIXME preverse binding (!?) *)
- mx,
ListPair.map (fn ((lazy,sel,tp),vn) =>
mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
(args, Datatype_Prop.make_tnames (map third args)));
@@ -245,7 +244,6 @@
map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
fun one_con (con,args,mx) : cons =
(Binding.name_of con, (* FIXME preverse binding (!?) *)
- mx,
ListPair.map (fn ((lazy,sel,tp),vn) =>
mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
(args, Datatype_Prop.make_tnames (map third args))
--- a/src/HOLCF/Tools/Domain/domain_library.ML Tue Mar 02 15:46:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Tue Mar 02 15:53:07 2010 -0800
@@ -93,7 +93,7 @@
(* Domain specifications *)
eqtype arg;
- type cons = string * mixfix * arg list;
+ type cons = string * arg list;
type eq = (string * typ list) * cons list;
val mk_arg : (bool * Datatype.dtyp) * string -> arg;
val is_lazy : arg -> bool;
@@ -189,7 +189,6 @@
type cons =
string * (* operator name of constr *)
- mixfix * (* mixfix syntax of constructor *)
arg list; (* argument list *)
type eq =
@@ -227,7 +226,7 @@
fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds;
fun dtyp_of_arg ((lazy, D), _) = if lazy then mk_uD D else D;
-fun dtyp_of_cons (_, _, args) = big_sprodD (map dtyp_of_arg args);
+fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args);
fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons);
@@ -331,8 +330,8 @@
else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
fun when_body cons funarg =
let
- fun one_fun n (_,_,[] ) = /\ "dummy" (funarg(1,n))
- | one_fun n (_,_,args) = let
+ fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n))
+ | one_fun n (_,args) = let
val l2 = length args;
fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t))
else I) (Bound(l2-m));
@@ -342,7 +341,7 @@
(args,
fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
) end;
- in (if length cons = 1 andalso length(third(hd cons)) <= 1
+ in (if length cons = 1 andalso length(snd (hd cons)) <= 1
then mk_strictify else I)
(foldr1 mk_sscase (mapn one_fun 1 cons)) end;
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Mar 02 15:46:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Mar 02 15:53:07 2010 -0800
@@ -179,7 +179,7 @@
fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict");
val axs_take_strict = map get_take_strict dnames;
- fun one_take_app (con, _, args) =
+ fun one_take_app (con, args) =
let
fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
fun one_rhs arg =
@@ -263,7 +263,7 @@
val dnames = map (fst o fst) eqs;
val x_name = idx_name dnames "x";
- fun one_con (con, _, args) =
+ fun one_con (con, args) =
let
val nonrec_args = filter_out is_rec args;
val rec_args = filter is_rec args;
@@ -343,7 +343,7 @@
maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
local
- fun one_con p (con, _, args) =
+ fun one_con p (con, args) =
let
val P_names = map P_name (1 upto (length dnames));
val vns = Name.variant_list P_names (map vname args);
@@ -367,7 +367,7 @@
fun ind_prems_tac prems = EVERY
(maps (fn cons =>
(resolve_tac prems 1 ::
- maps (fn (_,_,args) =>
+ maps (fn (_,args) =>
resolve_tac prems 1 ::
map (K(atac 1)) (nonlazy args) @
map (K(atac 1)) (filter is_rec args))
@@ -382,7 +382,7 @@
((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse
rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns)
(lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
- ) o third) cons;
+ ) o snd) cons;
fun all_rec_to ns = rec_to forall not all_rec_to ns;
fun warn (n,cons) =
if all_rec_to [] false (n,cons)
@@ -414,7 +414,7 @@
(* FIXME! case_UU_tac *)
case_UU_tac context (prems @ con_rews) 1
(List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
- fun con_tacs (con, _, args) =
+ fun con_tacs (con, args) =
asm_simp_tac take_ss 1 ::
map arg_tac (filter is_nonlazy_rec args) @
[resolve_tac prems 1] @
@@ -490,7 +490,7 @@
etac disjE 1,
asm_simp_tac (HOL_ss addsimps con_rews) 1,
asm_simp_tac take_ss 1];
- fun con_tacs ctxt (con, _, args) =
+ fun con_tacs ctxt (con, args) =
asm_simp_tac take_ss 1 ::
maps (arg_tacs ctxt) (nonlazy_rec args);
fun foo_tacs ctxt n (cons, cases) =