Removing the datatype declaration of "order" allows the standard General.order
authorpaulson
Fri Mar 19 10:42:38 2004 +0100 (2004-03-19)
changeset 14472cba7c0a3ffb3
parent 14471 5688b05b2575
child 14473 846c237bd9b3
Removing the datatype declaration of "order" allows the standard General.order
to be used. Thus we can use Int.compare and String.compare instead of the
slower home-grown versions.
src/Pure/General/heap.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/net_rules.ML
src/Pure/Proof/extraction.ML
src/Pure/display.ML
src/Pure/library.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/General/heap.ML	Wed Mar 17 14:00:45 2004 +0100
     1.2 +++ b/src/Pure/General/heap.ML	Fri Mar 19 10:42:38 2004 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4    | merge (Empty, h) = h
     1.5    | merge (h1 as Heap (_, x1, a1, b1), h2 as Heap (_, x2, a2, b2)) =
     1.6        (case ord (x1, x2) of
     1.7 -        Library.GREATER => heap x2 a2 (merge (h1, b2))
     1.8 +        GREATER => heap x2 a2 (merge (h1, b2))
     1.9        | _ => heap x1 a1 (merge (b1, h2)));
    1.10  
    1.11  fun insert (x, h) = merge (Heap (1, x, Empty, Empty), h);
     2.1 --- a/src/Pure/Isar/context_rules.ML	Wed Mar 17 14:00:45 2004 +0100
     2.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Mar 19 10:42:38 2004 +0100
     2.3 @@ -115,7 +115,7 @@
     2.4      fun prt_kind (i, b) =
     2.5        Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
     2.6          (mapfilter (fn (_, (k, th)) => if k = (i, b) then Some (prt x th) else None)
     2.7 -          (sort (int_ord o pairself fst) rules));
     2.8 +          (sort (Int.compare o pairself fst) rules));
     2.9    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    2.10  
    2.11  
    2.12 @@ -175,8 +175,10 @@
    2.13        if k = k' then untaglist rest
    2.14        else x :: untaglist rest;
    2.15  
    2.16 -fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
    2.17 -fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
    2.18 +fun orderlist brls = 
    2.19 +    untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls);
    2.20 +fun orderlist_no_weight brls = 
    2.21 +    untaglist (sort (Int.compare o pairself (snd o fst)) brls);
    2.22  
    2.23  fun may_unify weighted t net =
    2.24    map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));
     3.1 --- a/src/Pure/Isar/net_rules.ML	Wed Mar 17 14:00:45 2004 +0100
     3.2 +++ b/src/Pure/Isar/net_rules.ML	Fri Mar 19 10:42:38 2004 +0100
     3.3 @@ -38,7 +38,8 @@
     3.4  fun rules (Rules {rules = rs, ...}) = rs;
     3.5  
     3.6  fun retrieve (Rules {rules, net, ...}) tm =
     3.7 -  Tactic.untaglist ((Library.sort (int_ord o pairself #1) (Net.unify_term net tm)));
     3.8 +  Tactic.untaglist 
     3.9 +     ((Library.sort (Int.compare o pairself #1) (Net.unify_term net tm)));
    3.10  
    3.11  
    3.12  (* build rules *)
     4.1 --- a/src/Pure/Proof/extraction.ML	Wed Mar 17 14:00:45 2004 +0100
     4.2 +++ b/src/Pure/Proof/extraction.ML	Fri Mar 19 10:42:38 2004 +0100
     4.3 @@ -110,7 +110,7 @@
     4.4            Pattern.unify (sign, env, [pairself rew p])) (env', prems')
     4.5        in Some (Envir.norm_term env'' (inc (ren tm2)))
     4.6        end handle Pattern.MATCH => None | Pattern.Unif => None)
     4.7 -        (sort (int_ord o pairself fst)
     4.8 +        (sort (Int.compare o pairself fst)
     4.9            (Net.match_term rules (Pattern.eta_contract tm)));
    4.10  
    4.11    in rew end;
     5.1 --- a/src/Pure/display.ML	Wed Mar 17 14:00:45 2004 +0100
     5.2 +++ b/src/Pure/display.ML	Fri Mar 19 10:42:38 2004 +0100
     5.3 @@ -287,7 +287,7 @@
     5.4    | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
     5.5    | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
     5.6  
     5.7 -fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
     5.8 +fun sort_idxs vs = map (apsnd (sort (prod_ord String.compare Int.compare))) vs;
     5.9  fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
    5.10  
    5.11  fun consts_of t = sort_cnsts (add_consts (t, []));
     6.1 --- a/src/Pure/library.ML	Wed Mar 17 14:00:45 2004 +0100
     6.2 +++ b/src/Pure/library.ML	Fri Mar 19 10:42:38 2004 +0100
     6.3 @@ -228,7 +228,6 @@
     6.4    val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list
     6.5  
     6.6    (*orders*)
     6.7 -  datatype order = LESS | EQUAL | GREATER
     6.8    val rev_order: order -> order
     6.9    val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
    6.10    val int_ord: int * int -> order
    6.11 @@ -1073,8 +1072,6 @@
    6.12  
    6.13  (** orders **)
    6.14  
    6.15 -datatype order = LESS | EQUAL | GREATER;
    6.16 -
    6.17  fun rev_order LESS = GREATER
    6.18    | rev_order EQUAL = EQUAL
    6.19    | rev_order GREATER = LESS;
    6.20 @@ -1085,11 +1082,13 @@
    6.21    else if rel (y, x) then GREATER
    6.22    else EQUAL;
    6.23  
    6.24 +(*Better to use Int.compare*)
    6.25  fun int_ord (i, j: int) =
    6.26    if i < j then LESS
    6.27    else if i = j then EQUAL
    6.28    else GREATER;
    6.29  
    6.30 +(*Better to use String.compare*)
    6.31  fun string_ord (a, b: string) =
    6.32    if a < b then LESS
    6.33    else if a = b then EQUAL
     7.1 --- a/src/Pure/term.ML	Wed Mar 17 14:00:45 2004 +0100
     7.2 +++ b/src/Pure/term.ML	Fri Mar 19 10:42:38 2004 +0100
     7.3 @@ -191,6 +191,7 @@
     7.4    val typs_ord: typ list * typ list -> order
     7.5    val term_ord: term * term -> order
     7.6    val terms_ord: term list * term list -> order
     7.7 +  val hd_ord: term * term -> order
     7.8    val termless: term * term -> bool
     7.9    val dummy_patternN: string
    7.10    val no_dummy_patterns: term -> term
    7.11 @@ -984,17 +985,17 @@
    7.12  (** type and term orders **)
    7.13  
    7.14  fun indexname_ord ((x, i), (y, j)) =
    7.15 -  (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
    7.16 +  (case Int.compare (i, j) of EQUAL => String.compare (x, y) | ord => ord);
    7.17  
    7.18 -val sort_ord = list_ord string_ord;
    7.19 +val sort_ord = list_ord String.compare;
    7.20  
    7.21  
    7.22  (* typ_ord *)
    7.23  
    7.24 -fun typ_ord (Type x, Type y) = prod_ord string_ord typs_ord (x, y)
    7.25 +fun typ_ord (Type x, Type y) = prod_ord String.compare typs_ord (x, y)
    7.26    | typ_ord (Type _, _) = GREATER
    7.27    | typ_ord (TFree _, Type _) = LESS
    7.28 -  | typ_ord (TFree x, TFree y) = prod_ord string_ord sort_ord (x, y)
    7.29 +  | typ_ord (TFree x, TFree y) = prod_ord String.compare sort_ord (x, y)
    7.30    | typ_ord (TFree _, TVar _) = GREATER
    7.31    | typ_ord (TVar _, Type _) = LESS
    7.32    | typ_ord (TVar _, TFree _) = LESS
    7.33 @@ -1019,14 +1020,14 @@
    7.34  fun term_ord (Abs (_, T, t), Abs(_, U, u)) =
    7.35        (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
    7.36    | term_ord (t, u) =
    7.37 -      (case int_ord (size_of_term t, size_of_term u) of
    7.38 +      (case Int.compare (size_of_term t, size_of_term u) of
    7.39          EQUAL =>
    7.40            let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
    7.41              (case hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord)
    7.42            end
    7.43        | ord => ord)
    7.44  and hd_ord (f, g) =
    7.45 -  prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
    7.46 +  prod_ord (prod_ord indexname_ord typ_ord) Int.compare (dest_hd f, dest_hd g)
    7.47  and terms_ord (ts, us) = list_ord term_ord (ts, us);
    7.48  
    7.49  fun termless tu = (term_ord tu = LESS);