# HG changeset patch # User wenzelm # Date 1256680643 -3600 # Node ID 46e47aa1558fe213b8bffde467ea89985cb6852c # Parent 65232054ffd01f074f9c13bc632fc0fc11456977 eliminated some old folds; diff -r 65232054ffd0 -r 46e47aa1558f src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Tue Oct 27 22:56:14 2009 +0100 +++ b/src/HOL/Tools/refute.ML Tue Oct 27 22:57:23 2009 +0100 @@ -430,9 +430,8 @@ (* (Term.indexname * Term.typ) list *) val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t)) in - Library.foldl (fn (t', ((x, i), T)) => - (Term.all T) $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) - (t, vars) + fold (fn ((x, i), T) => fn t' => + Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t end; (* ------------------------------------------------------------------------- *) @@ -765,60 +764,55 @@ val _ = tracing "Adding axioms..." val axioms = Theory.all_axioms_of thy fun collect_this_axiom (axname, ax) axs = - let - val ax' = unfold_defs thy ax - in - if member (op aconv) axs ax' then axs - else (tracing axname; collect_term_axioms (ax' :: axs, ax')) - end - (* Term.term list * Term.typ -> Term.term list *) - and collect_sort_axioms (axs, T) = - let - (* string list *) - val sort = (case T of - TFree (_, sort) => sort - | TVar (_, sort) => sort - | _ => raise REFUTE ("collect_axioms", "type " ^ - Syntax.string_of_typ_global thy T ^ " is not a variable")) - (* obtain axioms for all superclasses *) - val superclasses = sort @ (maps (Sign.super_classes thy) sort) - (* merely an optimization, because 'collect_this_axiom' disallows *) - (* duplicate axioms anyway: *) - val superclasses = distinct (op =) superclasses - val class_axioms = maps (fn class => map (fn ax => - ("<" ^ class ^ ">", Thm.prop_of ax)) - (#axioms (AxClass.get_info thy class) handle ERROR _ => [])) - superclasses - (* replace the (at most one) schematic type variable in each axiom *) - (* by the actual type 'T' *) - val monomorphic_class_axioms = map (fn (axname, ax) => - (case Term.add_tvars ax [] of - [] => - (axname, ax) - | [(idx, S)] => - (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) - | _ => - raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ - Syntax.string_of_term_global thy ax ^ - ") contains more than one type variable"))) - class_axioms - in - fold collect_this_axiom monomorphic_class_axioms axs - end - (* Term.term list * Term.typ -> Term.term list *) - and collect_type_axioms (axs, T) = + let + val ax' = unfold_defs thy ax + in + if member (op aconv) axs ax' then axs + else (tracing axname; collect_term_axioms ax' (ax' :: axs)) + end + and collect_sort_axioms T axs = + let + val sort = + (case T of + TFree (_, sort) => sort + | TVar (_, sort) => sort + | _ => raise REFUTE ("collect_axioms", + "type " ^ Syntax.string_of_typ_global thy T ^ " is not a variable")) + (* obtain axioms for all superclasses *) + val superclasses = sort @ maps (Sign.super_classes thy) sort + (* merely an optimization, because 'collect_this_axiom' disallows *) + (* duplicate axioms anyway: *) + val superclasses = distinct (op =) superclasses + val class_axioms = maps (fn class => map (fn ax => + ("<" ^ class ^ ">", Thm.prop_of ax)) + (#axioms (AxClass.get_info thy class) handle ERROR _ => [])) + superclasses + (* replace the (at most one) schematic type variable in each axiom *) + (* by the actual type 'T' *) + val monomorphic_class_axioms = map (fn (axname, ax) => + (case Term.add_tvars ax [] of + [] => (axname, ax) + | [(idx, S)] => (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) + | _ => + raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ + Syntax.string_of_term_global thy ax ^ + ") contains more than one type variable"))) + class_axioms + in + fold collect_this_axiom monomorphic_class_axioms axs + end + and collect_type_axioms T axs = case T of (* simple types *) - Type ("prop", []) => axs - | Type ("fun", [T1, T2]) => collect_type_axioms - (collect_type_axioms (axs, T1), T2) + Type ("prop", []) => axs + | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs) (* axiomatic type classes *) - | Type ("itself", [T1]) => collect_type_axioms (axs, T1) - | Type (s, Ts) => + | Type ("itself", [T1]) => collect_type_axioms T1 axs + | Type (s, Ts) => (case Datatype.get_info thy s of SOME info => (* inductive datatype *) (* only collect relevant type axioms for the argument types *) - Library.foldl collect_type_axioms (axs, Ts) + fold collect_type_axioms Ts axs | NONE => (case get_typedef thy T of SOME (axname, ax) => @@ -826,20 +820,19 @@ | NONE => (* unspecified type, perhaps introduced with "typedecl" *) (* at least collect relevant type axioms for the argument types *) - Library.foldl collect_type_axioms (axs, Ts))) - (* axiomatic type classes *) - | TFree _ => collect_sort_axioms (axs, T) + fold collect_type_axioms Ts axs)) (* axiomatic type classes *) - | TVar _ => collect_sort_axioms (axs, T) - (* Term.term list * Term.term -> Term.term list *) - and collect_term_axioms (axs, t) = + | TFree _ => collect_sort_axioms T axs + (* axiomatic type classes *) + | TVar _ => collect_sort_axioms T axs + and collect_term_axioms t axs = case t of (* Pure *) Const (@{const_name all}, _) => axs | Const (@{const_name "=="}, _) => axs | Const (@{const_name "==>"}, _) => axs (* axiomatic type classes *) - | Const (@{const_name TYPE}, T) => collect_type_axioms (axs, T) + | Const (@{const_name TYPE}, T) => collect_type_axioms T axs (* HOL *) | Const (@{const_name Trueprop}, _) => axs | Const (@{const_name Not}, _) => axs @@ -847,7 +840,7 @@ | Const (@{const_name True}, _) => axs (* redundant, since 'False' is also an IDT constructor *) | Const (@{const_name False}, _) => axs - | Const (@{const_name undefined}, T) => collect_type_axioms (axs, T) + | Const (@{const_name undefined}, T) => collect_type_axioms T axs | Const (@{const_name The}, T) => let val ax = specialize_type thy (@{const_name The}, T) @@ -862,74 +855,68 @@ in collect_this_axiom ("Hilbert_Choice.someI", ax) axs end - | Const (@{const_name All}, T) => collect_type_axioms (axs, T) - | Const (@{const_name Ex}, T) => collect_type_axioms (axs, T) - | Const (@{const_name "op ="}, T) => collect_type_axioms (axs, T) + | Const (@{const_name All}, T) => collect_type_axioms T axs + | Const (@{const_name Ex}, T) => collect_type_axioms T axs + | Const (@{const_name "op ="}, T) => collect_type_axioms T axs | Const (@{const_name "op &"}, _) => axs | Const (@{const_name "op |"}, _) => axs | Const (@{const_name "op -->"}, _) => axs (* sets *) - | Const (@{const_name Collect}, T) => collect_type_axioms (axs, T) - | Const (@{const_name "op :"}, T) => collect_type_axioms (axs, T) + | Const (@{const_name Collect}, T) => collect_type_axioms T axs + | Const (@{const_name "op :"}, T) => collect_type_axioms T axs (* other optimizations *) - | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms (axs, T) + | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs | Const (@{const_name Finite_Set.finite}, T) => - collect_type_axioms (axs, T) + collect_type_axioms T axs | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => - collect_type_axioms (axs, T) + collect_type_axioms T axs | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => - collect_type_axioms (axs, T) + collect_type_axioms T axs | Const (@{const_name HOL.minus}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => - collect_type_axioms (axs, T) + collect_type_axioms T axs | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => - collect_type_axioms (axs, T) - | Const (@{const_name List.append}, T) => collect_type_axioms (axs, T) - | Const (@{const_name lfp}, T) => collect_type_axioms (axs, T) - | Const (@{const_name gfp}, T) => collect_type_axioms (axs, T) - | Const (@{const_name fst}, T) => collect_type_axioms (axs, T) - | Const (@{const_name snd}, T) => collect_type_axioms (axs, T) + collect_type_axioms T axs + | Const (@{const_name List.append}, T) => collect_type_axioms T axs + | Const (@{const_name lfp}, T) => collect_type_axioms T axs + | Const (@{const_name gfp}, T) => collect_type_axioms T axs + | Const (@{const_name fst}, T) => collect_type_axioms T axs + | Const (@{const_name snd}, T) => collect_type_axioms T axs (* simply-typed lambda calculus *) | Const (s, T) => if is_const_of_class thy (s, T) then (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *) (* and the class definition *) let - val class = Logic.class_of_const s + val class = Logic.class_of_const s val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class) - val ax_in = SOME (specialize_type thy (s, T) of_class) + val ax_in = SOME (specialize_type thy (s, T) of_class) (* type match may fail due to sort constraints *) handle Type.TYPE_MATCH => NONE - val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax)) - ax_in - val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) - (get_classdef thy class) + val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax)) ax_in + val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) (get_classdef thy class) in - collect_type_axioms (fold collect_this_axiom - (map_filter I [ax_1, ax_2]) axs, T) + collect_type_axioms T (fold collect_this_axiom (map_filter I [ax_1, ax_2]) axs) end else if is_IDT_constructor thy (s, T) orelse is_IDT_recursor thy (s, T) then (* only collect relevant type axioms *) - collect_type_axioms (axs, T) + collect_type_axioms T axs else (* other constants should have been unfolded, with some *) (* exceptions: e.g. Abs_xxx/Rep_xxx functions for *) (* typedefs, or type-class related constants *) (* only collect relevant type axioms *) - collect_type_axioms (axs, T) - | Free (_, T) => collect_type_axioms (axs, T) - | Var (_, T) => collect_type_axioms (axs, T) - | Bound i => axs - | Abs (_, T, body) => collect_term_axioms - (collect_type_axioms (axs, T), body) - | t1 $ t2 => collect_term_axioms - (collect_term_axioms (axs, t1), t2) - (* Term.term list *) - val result = map close_form (collect_term_axioms ([], t)) + collect_type_axioms T axs + | Free (_, T) => collect_type_axioms T axs + | Var (_, T) => collect_type_axioms T axs + | Bound _ => axs + | Abs (_, T, body) => collect_term_axioms body (collect_type_axioms T axs) + | t1 $ t2 => collect_term_axioms t2 (collect_term_axioms t1 axs) + val result = map close_form (collect_term_axioms t []) val _ = tracing " ...done." in result @@ -1037,7 +1024,7 @@ fun size_of_typ T = case AList.lookup (op =) sizes (string_of_typ T) of SOME n => n - | NONE => minsize + | NONE => minsize in map (fn T => (T, size_of_typ T)) xs end; @@ -1091,13 +1078,13 @@ case next (maxsize-minsize) 0 0 diffs of SOME diffs' => (* merge with those types for which the size is fixed *) - SOME (snd (Library.foldl_map (fn (ds, (T, _)) => + SOME (fst (fold_map (fn (T, _) => fn ds => case AList.lookup (op =) sizes (string_of_typ T) of (* return the fixed size *) - SOME n => (ds, (T, n)) + SOME n => ((T, n), ds) (* consume the head of 'ds', add 'minsize' *) - | NONE => (tl ds, (T, minsize + hd ds))) - (diffs', xs))) + | NONE => ((T, minsize + hd ds), tl ds)) + xs diffs')) | NONE => NONE end; @@ -1154,8 +1141,7 @@ val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u) val axioms = collect_axioms thy u (* Term.typ list *) - val types = Library.foldl (fn (acc, t') => - uncurry (union (op =)) (acc, (ground_types thy t'))) ([], u :: axioms) + val types = fold (union (op =) o ground_types thy) (u :: axioms) [] val _ = tracing ("Ground types: " ^ (if null types then "none." else commas (map (Syntax.string_of_typ_global thy) types))) @@ -1194,15 +1180,15 @@ val _ = tracing ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") (* translate 'u' and all axioms *) - val ((model, args), intrs) = Library.foldl_map (fn ((m, a), t') => + val (intrs, (model, args)) = fold_map (fn t' => fn (m, a) => let val (i, m', a') = interpret thy m a t' in (* set 'def_eq' to 'true' *) - ((m', {maxvars = #maxvars a', def_eq = true, + (i, (m', {maxvars = #maxvars a', def_eq = true, next_idx = #next_idx a', bounds = #bounds a', - wellformed = #wellformed a'}), i) - end) ((init_model, init_args), u :: axioms) + wellformed = #wellformed a'})) + end) (u :: axioms) (init_model, init_args) (* make 'u' either true or false, and make all axioms true, and *) (* add the well-formedness side condition *) val fm_u = (if negate then toFalse else toTrue) (hd intrs) @@ -1306,10 +1292,9 @@ (* (Term.indexname * Term.typ) list *) val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t)) (* Term.term *) - val ex_closure = Library.foldl (fn (t', ((x, i), T)) => - (HOLogic.exists_const T) $ - Abs (x, T, abstract_over (Var ((x, i), T), t'))) - (t, vars) + val ex_closure = fold (fn ((x, i), T) => fn t' => + HOLogic.exists_const T $ + Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t (* Note: If 't' is of type 'propT' (rather than 'boolT'), applying *) (* 'HOLogic.exists_const' is not type-correct. However, this is not *) (* really a problem as long as 'find_model' still interprets the *) @@ -1730,8 +1715,8 @@ (* create all constants of type 'T' *) val constants = make_constants thy model T (* interpret the 'body' separately for each constant *) - val ((model', args'), bodies) = Library.foldl_map - (fn ((m, a), c) => + val (bodies, (model', args')) = fold_map + (fn c => fn (m, a) => let (* add 'c' to 'bounds' *) val (i', m', a') = interpret thy m {maxvars = #maxvars a, @@ -1740,15 +1725,15 @@ in (* keep the new model m' and 'next_idx' and 'wellformed', *) (* but use old 'bounds' *) - ((m', {maxvars = maxvars, def_eq = def_eq, + (i', (m', {maxvars = maxvars, def_eq = def_eq, next_idx = #next_idx a', bounds = bounds, - wellformed = #wellformed a'}), i') + wellformed = #wellformed a'})) end) - ((model, args), constants) + constants (model, args) in SOME (Node bodies, model', args') end - | t1 $ t2 => + | t1 $ t2 => let (* interpret 't1' and 't2' separately *) val (intr1, model1, args1) = interpret thy model args t1 @@ -2209,14 +2194,14 @@ Node (replicate size (make_undef ds)) end (* returns the interpretation for a constructor *) - fun make_constr (offset, []) = - if offset= total") - | make_constr (offset, d::ds) = + | make_constr (d::ds) offset = let (* Term.typ *) val dT = typ_of_dtyp descr typ_assoc d @@ -2225,8 +2210,8 @@ (* for the IDT) *) val terms' = canonical_terms typs' dT (* sanity check *) - val _ = if length terms' <> - size_of_type thy (typs', []) dT + val _ = + if length terms' <> size_of_type thy (typs', []) dT then raise REFUTE ("IDT_constructor_interpreter", "length of terms' is not equal to old size") @@ -2236,46 +2221,52 @@ (* for the IDT) *) val terms = canonical_terms typs dT (* sanity check *) - val _ = if length terms <> size_of_type thy (typs, []) dT + val _ = + if length terms <> size_of_type thy (typs, []) dT then raise REFUTE ("IDT_constructor_interpreter", "length of terms is not equal to current size") else () (* sanity check *) - val _ = if length terms < length terms' then + val _ = + if length terms < length terms' then raise REFUTE ("IDT_constructor_interpreter", "current size is less than old size") else () (* sanity check: every element of terms' must also be *) (* present in terms *) - val _ = if List.all (member op= terms) terms' then () + val _ = + if List.all (member (op =) terms) terms' then () else raise REFUTE ("IDT_constructor_interpreter", "element has disappeared") (* sanity check: the order on elements of terms' is *) (* the same in terms, for those elements *) - val _ = let + val _ = + let fun search (x::xs) (y::ys) = - if x = y then search xs ys else search (x::xs) ys + if x = y then search xs ys else search (x::xs) ys | search (x::xs) [] = - raise REFUTE ("IDT_constructor_interpreter", - "element order not preserved") + raise REFUTE ("IDT_constructor_interpreter", + "element order not preserved") | search [] _ = () in search terms' terms end (* int * interpretation list *) - val (new_offset, intrs) = Library.foldl_map (fn (off, t_elem) => - (* if 't_elem' existed at the previous depth, *) - (* proceed recursively, otherwise map the entire *) - (* subtree to "undefined" *) - if t_elem mem terms' then - make_constr (off, ds) - else - (off, make_undef ds)) (offset, terms) + val (intrs, new_offset) = + fold_map (fn t_elem => fn off => + (* if 't_elem' existed at the previous depth, *) + (* proceed recursively, otherwise map the entire *) + (* subtree to "undefined" *) + if t_elem mem terms' then + make_constr ds off + else + (make_undef ds, off)) + terms offset in - (new_offset, Node intrs) + (Node intrs, new_offset) end in - SOME (snd (make_constr (offset, ctypes)), model, args) + SOME (fst (make_constr ctypes offset), model, args) end end | NONE => (* body type is not an inductive datatype *) @@ -2329,12 +2320,12 @@ else (* mconstrs_count = length params *) let (* interpret each parameter separately *) - val ((model', args'), p_intrs) = Library.foldl_map (fn ((m, a), p) => + val (p_intrs, (model', args')) = fold_map (fn p => fn (m, a) => let val (i, m', a') = interpret thy m a p in - ((m', a'), i) - end) ((model, args), params) + (i, (m', a')) + end) params (model, args) val (typs, _) = model' (* 'index' is /not/ necessarily the index of the IDT that *) (* the recursion operator is associated with, but merely *) @@ -2437,14 +2428,14 @@ end) descr (* associate constructors with corresponding parameters *) (* (int * (interpretation * interpretation) list) list *) - val (p_intrs', mc_p_intrs) = Library.foldl_map - (fn (p_intrs', (idx, c_intrs)) => + val (mc_p_intrs, p_intrs') = fold_map + (fn (idx, c_intrs) => fn p_intrs' => let val len = length c_intrs in - (List.drop (p_intrs', len), - (idx, c_intrs ~~ List.take (p_intrs', len))) - end) (p_intrs, mc_intrs) + ((idx, c_intrs ~~ List.take (p_intrs', len)), + List.drop (p_intrs', len)) + end) mc_intrs p_intrs (* sanity check: no 'p_intr' may be left afterwards *) val _ = if p_intrs' <> [] then raise REFUTE ("IDT_recursion_interpreter", @@ -2669,15 +2660,15 @@ let (* interpretation -> int *) fun number_of_elements (Node xs) = - Library.foldl (fn (n, x) => - if x=TT then - n+1 - else if x=FF then - n - else - raise REFUTE ("Finite_Set_card_interpreter", - "interpretation for set type does not yield a Boolean")) - (0, xs) + fold (fn x => fn n => + if x = TT then + n + 1 + else if x = FF then + n + else + raise REFUTE ("Finite_Set_card_interpreter", + "interpretation for set type does not yield a Boolean")) + xs 0 | number_of_elements (Leaf _) = raise REFUTE ("Finite_Set_card_interpreter", "interpretation for set type is a leaf") @@ -2882,7 +2873,7 @@ (* of width 'size_elem' and depth 'length_list' (with 'size_list' *) (* nodes total) *) (* (int * (int * int)) list *) - val (_, lenoff_lists) = Library.foldl_map (fn ((offsets, off), elem) => + val (lenoff_lists, _) = fold_map (fn elem => fn (offsets, off) => (* corresponds to a pre-order traversal of the tree *) let val len = length offsets @@ -2891,10 +2882,10 @@ in if len < list_length then (* go to first child node *) - ((off :: offsets, off * size_elem), assoc) + (assoc, (off :: offsets, off * size_elem)) else if off mod size_elem < size_elem - 1 then (* go to next sibling node *) - ((offsets, off + 1), assoc) + (assoc, (offsets, off + 1)) else (* go back up the stack until we find a level where we can go *) (* to the next sibling node *) @@ -2906,12 +2897,12 @@ [] => (* we're at the last node in the tree; the next value *) (* won't be used anyway *) - (([], 0), assoc) + (assoc, ([], 0)) | off'::offs' => (* go to next sibling node *) - ((offs', off' + 1), assoc) + (assoc, (offs', off' + 1)) end - end) (([], 0), elements) + end) elements ([], 0) (* we also need the reverse association (from length/offset to *) (* index) *) val lenoff'_lists = map Library.swap lenoff_lists @@ -3248,7 +3239,7 @@ print thy (typs, []) dT (List.nth (consts, n)) assignment end) (cargs ~~ args) in - SOME (Library.foldl op$ (cTerm, argsTerms)) + SOME (list_comb (cTerm, argsTerms)) end end | NONE => (* not an inductive datatype *)