remove unused mixfix component from type cons
authorhuffman
Tue Mar 02 15:53:07 2010 -0800 (2010-03-02)
changeset 3552147eec4da124a
parent 35520 f433f18d4c41
child 35522 f9714c7c0837
remove unused mixfix component from type cons
src/HOLCF/Tools/Domain/domain_extender.ML
src/HOLCF/Tools/Domain/domain_library.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 15:46:23 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 15:53:07 2010 -0800
     1.3 @@ -168,7 +168,6 @@
     1.4          map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     1.5      fun one_con (con,args,mx) : cons =
     1.6          (Binding.name_of con,  (* FIXME preverse binding (!?) *)
     1.7 -         mx,
     1.8           ListPair.map (fn ((lazy,sel,tp),vn) =>
     1.9             mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
    1.10                        (args, Datatype_Prop.make_tnames (map third args)));
    1.11 @@ -245,7 +244,6 @@
    1.12          map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
    1.13      fun one_con (con,args,mx) : cons =
    1.14          (Binding.name_of con,   (* FIXME preverse binding (!?) *)
    1.15 -         mx,
    1.16           ListPair.map (fn ((lazy,sel,tp),vn) =>
    1.17             mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
    1.18                        (args, Datatype_Prop.make_tnames (map third args))
     2.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 15:46:23 2010 -0800
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 15:53:07 2010 -0800
     2.3 @@ -93,7 +93,7 @@
     2.4  
     2.5        (* Domain specifications *)
     2.6        eqtype arg;
     2.7 -  type cons = string * mixfix * arg list;
     2.8 +  type cons = string * arg list;
     2.9    type eq = (string * typ list) * cons list;
    2.10    val mk_arg : (bool * Datatype.dtyp) * string -> arg;
    2.11    val is_lazy : arg -> bool;
    2.12 @@ -189,7 +189,6 @@
    2.13  
    2.14  type cons =
    2.15       string *         (* operator name of constr *)
    2.16 -     mixfix *         (* mixfix syntax of constructor *)
    2.17       arg list;        (* argument list      *)
    2.18  
    2.19  type eq =
    2.20 @@ -227,7 +226,7 @@
    2.21  fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds;
    2.22  
    2.23  fun dtyp_of_arg ((lazy, D), _) = if lazy then mk_uD D else D;
    2.24 -fun dtyp_of_cons (_, _, args) = big_sprodD (map dtyp_of_arg args);
    2.25 +fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args);
    2.26  fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons);
    2.27  
    2.28  
    2.29 @@ -331,8 +330,8 @@
    2.30                       else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
    2.31  fun when_body cons funarg =
    2.32      let
    2.33 -      fun one_fun n (_,_,[]  ) = /\ "dummy" (funarg(1,n))
    2.34 -        | one_fun n (_,_,args) = let
    2.35 +      fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
    2.36 +        | one_fun n (_,args) = let
    2.37              val l2 = length args;
    2.38              fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t))
    2.39                                else I) (Bound(l2-m));
    2.40 @@ -342,7 +341,7 @@
    2.41                    (args,
    2.42                  fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
    2.43                 ) end;
    2.44 -    in (if length cons = 1 andalso length(third(hd cons)) <= 1
    2.45 +    in (if length cons = 1 andalso length(snd (hd cons)) <= 1
    2.46          then mk_strictify else I)
    2.47           (foldr1 mk_sscase (mapn one_fun 1 cons)) end;
    2.48  
     3.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 15:46:23 2010 -0800
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 15:53:07 2010 -0800
     3.3 @@ -179,7 +179,7 @@
     3.4    fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict");
     3.5    val axs_take_strict = map get_take_strict dnames;
     3.6  
     3.7 -  fun one_take_app (con, _, args) =
     3.8 +  fun one_take_app (con, args) =
     3.9      let
    3.10        fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
    3.11        fun one_rhs arg =
    3.12 @@ -263,7 +263,7 @@
    3.13    val dnames = map (fst o fst) eqs;
    3.14    val x_name = idx_name dnames "x"; 
    3.15  
    3.16 -  fun one_con (con, _, args) =
    3.17 +  fun one_con (con, args) =
    3.18      let
    3.19        val nonrec_args = filter_out is_rec args;
    3.20        val    rec_args = filter is_rec args;
    3.21 @@ -343,7 +343,7 @@
    3.22      maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
    3.23  
    3.24  local
    3.25 -  fun one_con p (con, _, args) =
    3.26 +  fun one_con p (con, args) =
    3.27      let
    3.28        val P_names = map P_name (1 upto (length dnames));
    3.29        val vns = Name.variant_list P_names (map vname args);
    3.30 @@ -367,7 +367,7 @@
    3.31    fun ind_prems_tac prems = EVERY
    3.32      (maps (fn cons =>
    3.33        (resolve_tac prems 1 ::
    3.34 -        maps (fn (_,_,args) => 
    3.35 +        maps (fn (_,args) => 
    3.36            resolve_tac prems 1 ::
    3.37            map (K(atac 1)) (nonlazy args) @
    3.38            map (K(atac 1)) (filter is_rec args))
    3.39 @@ -382,7 +382,7 @@
    3.40            ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
    3.41              rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
    3.42                (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
    3.43 -          ) o third) cons;
    3.44 +          ) o snd) cons;
    3.45      fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
    3.46      fun warn (n,cons) =
    3.47        if all_rec_to [] false (n,cons)
    3.48 @@ -414,7 +414,7 @@
    3.49                          (* FIXME! case_UU_tac *)
    3.50              case_UU_tac context (prems @ con_rews) 1
    3.51                (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
    3.52 -          fun con_tacs (con, _, args) = 
    3.53 +          fun con_tacs (con, args) = 
    3.54              asm_simp_tac take_ss 1 ::
    3.55              map arg_tac (filter is_nonlazy_rec args) @
    3.56              [resolve_tac prems 1] @
    3.57 @@ -490,7 +490,7 @@
    3.58                etac disjE 1,
    3.59                asm_simp_tac (HOL_ss addsimps con_rews) 1,
    3.60                asm_simp_tac take_ss 1];
    3.61 -            fun con_tacs ctxt (con, _, args) =
    3.62 +            fun con_tacs ctxt (con, args) =
    3.63                asm_simp_tac take_ss 1 ::
    3.64                maps (arg_tacs ctxt) (nonlazy_rec args);
    3.65              fun foo_tacs ctxt n (cons, cases) =