# HG changeset patch # User wenzelm # Date 1342367627 -7200 # Node ID 94a7dc2276e4cea32b180a5bd2d4215368fc4940 # Parent a0d8abca8d7ab5f29db3213381b7a9527d7fb936 prefer canonical fold_rev; diff -r a0d8abca8d7a -r 94a7dc2276e4 src/Pure/search.ML --- a/src/Pure/search.ML Sun Jul 15 17:27:19 2012 +0200 +++ b/src/Pure/search.ML Sun Jul 15 17:53:47 2012 +0200 @@ -255,9 +255,9 @@ *) (*Insertion into priority queue of states, marked with level *) -fun insert_with_level (lnth: int*int*thm, []) = [lnth] - | insert_with_level ((l,m,th), (l',n,th')::nths) = - if n next (List.foldr insert_with_level nprfs (map cost nonsats)) + => next (fold_rev (insert_with_level o cost) nonsats nprfs) | (sats,_) => some_of_list sats) end and next [] = NONE diff -r a0d8abca8d7a -r 94a7dc2276e4 src/Pure/term.ML --- a/src/Pure/term.ML Sun Jul 15 17:27:19 2012 +0200 +++ b/src/Pure/term.ML Sun Jul 15 17:53:47 2012 +0200 @@ -147,7 +147,7 @@ val aconv_untyped: term * term -> bool val could_unify: term * term -> bool val strip_abs_eta: int -> term -> (string * typ) list * term - val match_bvars: (term * term) * (string * string) list -> (string * string) list + val match_bvars: (term * term) -> (string * string) list -> (string * string) list val map_abs_vars: (string -> string) -> term -> term val rename_abs: term -> term -> term -> term option val is_open: term -> bool @@ -611,7 +611,7 @@ | match_bvs(_,_,al) = al; (* strip abstractions created by parameters *) -fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al); +fun match_bvars (s,t) al = match_bvs(strip_abs_body s, strip_abs_body t, al); fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t) diff -r a0d8abca8d7a -r 94a7dc2276e4 src/Pure/thm.ML --- a/src/Pure/thm.ML Sun Jul 15 17:27:19 2012 +0200 +++ b/src/Pure/thm.ML Sun Jul 15 17:53:47 2012 +0200 @@ -1562,7 +1562,7 @@ (*Function to rename bounds/unknowns in the argument, lifted over B*) fun rename_bvars dpairs = - rename_bvs (List.foldr Term.match_bvars [] dpairs) dpairs; + rename_bvs (fold_rev Term.match_bvars dpairs []) dpairs; (*** RESOLUTION ***) diff -r a0d8abca8d7a -r 94a7dc2276e4 src/Pure/unify.ML --- a/src/Pure/unify.ML Sun Jul 15 17:27:19 2012 +0200 +++ b/src/Pure/unify.ML Sun Jul 15 17:53:47 2012 +0200 @@ -273,11 +273,11 @@ Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to do so caused numerous problems with no compensating advantage. *) -fun SIMPL0 thy (dp0, (env,flexflex,flexrigid)) : Envir.env * dpair list * dpair list = +fun SIMPL0 thy dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list = let val (dp as (rbinder, t, u), env) = head_norm_dpair thy (env, dp0); fun SIMRANDS (f $ t, g $ u, env) = - SIMPL0 thy ((rbinder, t, u), SIMRANDS (f, g, env)) + SIMPL0 thy (rbinder, t, u) (SIMRANDS (f, g, env)) | SIMRANDS (t as _$_, _, _) = raise TERM ("SIMPL: operands mismatch", [t, u]) | SIMRANDS (t, u as _ $ _, _) = @@ -318,7 +318,7 @@ Clever would be to re-do just the affected dpairs*) fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list = let - val all as (env', flexflex, flexrigid) = List.foldr (SIMPL0 thy) (env, [], []) dpairs; + val all as (env', flexflex, flexrigid) = fold_rev (SIMPL0 thy) dpairs (env, [], []); val dps = flexrigid @ flexflex; in if exists (fn (_, t, u) => changed (env', t) orelse changed (env', u)) dps @@ -496,7 +496,7 @@ in change 0 end; (*Change indices, delete the argument if it contains a banned Bound*) -fun change_arg banned ({j, t, T}, args) : flarg list = +fun change_arg banned {j, t, T} args : flarg list = if rigid_bound (0, banned) t then args (*delete argument!*) else {j = j, t = change_bnos banned t, T = T} :: args; @@ -528,7 +528,7 @@ val (Var (v, T), ts) = strip_comb t; val (Ts, U) = strip_type env T and js = length ts - 1 downto 0; - val args = sort_args (List.foldr (change_arg banned) [] (flexargs (js, ts, Ts))) + val args = sort_args (fold_rev (change_arg banned) (flexargs (js, ts, Ts)) []) val ts' = map #t args; in if decreasing (length Ts) args then (env, (list_comb (Var (v, T), ts'))) @@ -579,7 +579,7 @@ eliminates trivial tpairs like t=t, as well as repeated ones trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t Resulting tpairs MAY NOT be in normal form: assignments may occur here.*) -fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs)) : Envir.env * (term * term) list = +fun add_ffpair thy (rbinder,t0,u0) (env,tpairs) : Envir.env * (term * term) list = let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0; @@ -627,7 +627,7 @@ SIMPL thy (env, dpairs)); in (case flexrigid of - [] => SOME (List.foldr (add_ffpair thy) (env', []) flexflex, reseq) + [] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq) | dp :: frigid' => if tdepth > search_bnd then (warning "Unification bound exceeded"; Seq.pull reseq) @@ -664,7 +664,7 @@ Unlike Huet (1975), does not smash together all variables of same type -- requires more work yet gives a less general unifier (fewer variables). Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *) -fun smash_flexflex1 ((t, u), env) : Envir.env = +fun smash_flexflex1 (t, u) env : Envir.env = let val vT as (v, T) = var_head_of (env, t) and wU as (w, U) = var_head_of (env, u); @@ -678,7 +678,7 @@ (*Smash all flex-flexpairs. Should allow selection of pairs by a predicate?*) fun smash_flexflex (env, tpairs) : Envir.env = - List.foldr smash_flexflex1 env tpairs; + fold_rev smash_flexflex1 tpairs env; (*Returns unifiers with no remaining disagreement pairs*) fun smash_unifiers thy tus env =