eliminated old List.foldr and OldTerm operations;
authorwenzelm
Sat Oct 17 19:04:35 2009 +0200 (2009-10-17)
changeset 329742a1aaa2d9e64
parent 32973 12d830f131ac
child 32975 84d105ad5adb
eliminated old List.foldr and OldTerm operations;
misc tuning;
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Sat Oct 17 18:14:47 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Oct 17 19:04:35 2009 +0200
     1.3 @@ -1038,11 +1038,11 @@
     1.4  
     1.5  fun mk_comp f g =
     1.6    let
     1.7 -    val x = fastype_of g;
     1.8 -    val a = domain_type x;
     1.9 -    val b = range_type x;
    1.10 -    val c = range_type (fastype_of f);
    1.11 -    val T = (b --> c) --> ((a --> b) --> (a --> c))
    1.12 +    val X = fastype_of g;
    1.13 +    val A = domain_type X;
    1.14 +    val B = range_type X;
    1.15 +    val C = range_type (fastype_of f);
    1.16 +    val T = (B --> C) --> (A --> B) --> A --> C;
    1.17    in Const ("Fun.comp", T) $ f $ g end;
    1.18  
    1.19  fun mk_comp_id f =
    1.20 @@ -1295,7 +1295,7 @@
    1.21              Drule.standard (uathm RS updacc_noop_compE)]
    1.22            end;
    1.23  
    1.24 -        (*If f is constant then (f o g) = f. we know that K_skeleton
    1.25 +        (*If f is constant then (f o g) = f.  We know that K_skeleton
    1.26            only returns constant abstractions thus when we see an
    1.27            abstraction we can discard inner updates.*)
    1.28          fun add_upd (f as Abs _) fs = [f]
    1.29 @@ -1356,7 +1356,7 @@
    1.30  
    1.31  (* record_eq_simproc *)
    1.32  
    1.33 -(*Looks up the most specific record-equality.
    1.34 +(*Look up the most specific record-equality.
    1.35  
    1.36   Note on efficiency:
    1.37   Testing equality of records boils down to the test of equality of all components.
    1.38 @@ -1853,7 +1853,7 @@
    1.39      val names = map fst fields;
    1.40      val extN = full bname;
    1.41      val types = map snd fields;
    1.42 -    val alphas_fields = List.foldr OldTerm.add_typ_tfree_names [] types;
    1.43 +    val alphas_fields = fold Term.add_tfree_namesT types [];
    1.44      val alphas_ext = alphas inter alphas_fields;
    1.45      val len = length fields;
    1.46      val variants =
    1.47 @@ -1908,9 +1908,10 @@
    1.48      fun mk_rec args n =
    1.49        let
    1.50          val (args', more) = chop_last args;
    1.51 -        fun mk_ext' (((name, T), args), more) = mk_ext (name, T) (args @ [more]);
    1.52 +        fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
    1.53          fun build Ts =
    1.54 -          List.foldr mk_ext' more (Library.drop (n, extension_names ~~ Ts ~~ chunks parent_chunks args'));
    1.55 +          fold_rev mk_ext' (Library.drop (n, (extension_names ~~ Ts) ~~ chunks parent_chunks args'))
    1.56 +            more;
    1.57        in
    1.58          if more = HOLogic.unit
    1.59          then build (map recT (0 upto parent_len))
    1.60 @@ -2117,15 +2118,13 @@
    1.61           (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
    1.62        end;
    1.63  
    1.64 -    (* FIXME eliminate old List.foldr *)
    1.65 -
    1.66      val split_object_prop =
    1.67 -      let fun ALL vs t = List.foldr (fn ((v, T), t) => HOLogic.mk_all (v, T, t)) t vs
    1.68 -      in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0)) end;
    1.69 +      let val ALL = fold_rev (fn (v, T) => fn t => HOLogic.mk_all (v, T, t))
    1.70 +      in ALL [dest_Free r0] (P $ r0) === ALL (map dest_Free all_vars_more) (P $ r_rec0) end;
    1.71  
    1.72      val split_ex_prop =
    1.73 -      let fun EX vs t = List.foldr (fn ((v, T), t) => HOLogic.mk_exists (v, T, t)) t vs
    1.74 -      in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0)) end;
    1.75 +      let val EX = fold_rev (fn (v, T) => fn t => HOLogic.mk_exists (v, T, t))
    1.76 +      in EX [dest_Free r0] (P $ r0) === EX (map dest_Free all_vars_more) (P $ r_rec0) end;
    1.77  
    1.78      (*equality*)
    1.79      val equality_prop =
    1.80 @@ -2383,7 +2382,7 @@
    1.81      val init_env =
    1.82        (case parent of
    1.83          NONE => []
    1.84 -      | SOME (types, _) => List.foldr OldTerm.add_typ_tfrees [] types);
    1.85 +      | SOME (types, _) => fold Term.add_tfreesT types []);
    1.86  
    1.87  
    1.88      (* fields *)