# HG changeset patch # User webertj # Date 1111020018 -3600 # Node ID c01f11cd08f9b65b48c5f7bd96c5f1e4067f2a25 # Parent f855fd163b62ef1ff722e960c7eeb401aa7bd2c0 Bugfix related to the interpretation of IDT constructors diff -r f855fd163b62 -r c01f11cd08f9 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Tue Mar 15 17:07:41 2005 +0100 +++ b/src/HOL/Tools/refute.ML Thu Mar 17 01:40:18 2005 +0100 @@ -100,7 +100,7 @@ (* 'a tree * 'b tree -> ('a * 'b) tree *) - fun tree_pair (t1,t2) = + fun tree_pair (t1, t2) = case t1 of Leaf x => (case t2 of @@ -240,7 +240,7 @@ if null typs then "empty universe (no type variables in term)\n" else - "Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs) ^ "\n" + "Size of types: " ^ commas (map (fn (T, i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs) ^ "\n" val show_consts_msg = if not (!show_consts) andalso Library.exists (is_Const o fst) terms then "set \"show_consts\" to show the interpretation of constants\n" @@ -250,7 +250,7 @@ if null terms then "empty interpretation (no free variables in term)\n" else - space_implode "\n" (List.mapPartial (fn (t,intr) => + space_implode "\n" (List.mapPartial (fn (t, intr) => (* print constants only if 'show_consts' is true *) if (!show_consts) orelse not (is_Const t) then SOME (Sign.string_of_term (sign_of thy) t ^ ": " ^ Sign.string_of_term (sign_of thy) (print thy model t intr assignment)) @@ -1055,7 +1055,7 @@ val vars = sort_wrt (fst o fst) (map dest_Var (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'))) + (fn (t', ((x, i), T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) (t, vars) (* If 't' is of type 'propT' (rather than 'boolT'), applying *) (* 'HOLogic.exists_const' is not type-correct. However, this *) @@ -1117,7 +1117,7 @@ map (fn x => [x]) xs | pick_all n xs = let val rec_pick = pick_all (n-1) xs in - Library.foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs) + Library.foldl (fn (acc, x) => (cons_list x rec_pick) @ acc) ([], xs) end in case intr of @@ -1134,11 +1134,11 @@ fun size_of_type intr = let - (* power(a,b) computes a^b, for a>=0, b>=0 *) + (* power (a, b) computes a^b, for a>=0, b>=0 *) (* int * int -> int *) - fun power (a,0) = 1 - | power (a,1) = a - | power (a,b) = let val ab = power(a, b div 2) in ab * ab * power(a, b mod 2) end + fun power (a, 0) = 1 + | power (a, 1) = a + | power (a, b) = let val ab = power(a, b div 2) in ab * ab * power(a, b mod 2) end in case intr of Leaf xs => length xs @@ -1270,7 +1270,7 @@ map (fn x => [x]) xs | pick_all (xs::xss) = let val rec_pick = pick_all xss in - Library.foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs) + Library.foldl (fn (acc, x) => (cons_list x rec_pick) @ acc) ([], xs) end | pick_all _ = raise REFUTE ("interpretation_apply", "empty list (in pick_all)") @@ -1307,7 +1307,7 @@ (* int list -> int *) - fun sum xs = Library.foldl op+ (0, xs); + fun sum xs = foldl op+ 0 xs; (* ------------------------------------------------------------------------- *) (* product: returns the product of a list 'xs' of integers *) @@ -1315,7 +1315,7 @@ (* int list -> int *) - fun product xs = Library.foldl op* (1, xs); + fun product xs = foldl op* 1 xs; (* ------------------------------------------------------------------------- *) (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *) @@ -1750,6 +1750,7 @@ (* int option -- only recursive IDTs have an associated depth *) val depth = assoc (typs, Type (s', Ts')) val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s', Ts'), n-1))) + (* returns an interpretation where everything is mapped to "undefined" *) (* DatatypeAux.dtyp list -> interpretation *) fun make_undef [] = Leaf (replicate total False) @@ -1782,14 +1783,14 @@ raise REFUTE ("IDT_constructor_interpreter", "current size is less than old size") else () - (* elements that exist at the previous depth are mapped to a defined *) - (* value, while new elements are mapped to "undefined" by the *) - (* recursive constructor *) (* int * interpretation list *) val (new_offset, intrs) = foldl_map make_constr (offset, replicate size' ds) (* interpretation list *) val undefs = replicate (size - size') (make_undef ds) in + (* elements that exist at the previous depth are mapped to a defined *) + (* value, while new elements are mapped to "undefined" by the *) + (* recursive constructor *) (new_offset, Node (intrs @ undefs)) end (* extends the interpretation for a constructor (both recursive *) @@ -1799,7 +1800,7 @@ let (* returns the k-th unit vector of length n *) (* int * int -> interpretation *) - fun unit_vector (k,n) = + fun unit_vector (k, n) = Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) (* int *) val k = find_index_eq True xs @@ -1812,7 +1813,7 @@ else (* if the element was already mapped to a defined value, map it *) (* to the same value again, just extend the length of the leaf, *) - (* do not increment offset *) + (* do not increment the 'offset' *) (offset, unit_vector (k+1, total)) end | extend_constr (_, [], Node _) = @@ -1842,14 +1843,8 @@ (* DatatypeAux.dtyp list -> bool *) fun is_rec_constr ds = Library.exists DatatypeAux.is_rec_type ds - (* constructors before 'Const (s, T)' generate elements of the datatype, *) - (* and if the constructor is recursive, then non-recursive constructors *) - (* after it generate further elements *) - val offset = size_of_dtyp thy typs' descr typ_assoc constrs1 + - (if is_rec_constr ctypes then - size_of_dtyp thy typs' descr typ_assoc (List.filter (not o is_rec_constr o snd) cs) - else - 0) + (* constructors before 'Const (s, T)' generate elements of the datatype *) + val offset = size_of_dtyp thy typs' descr typ_assoc constrs1 in case depth of NONE => (* equivalent to a depth of 1 *) @@ -2011,7 +2006,6 @@ fun toList arr = Array.foldr op:: [] arr in - (* TODO writeln ("REC-OP: " ^ makestring (Node (toList INTRS))); *) SOME (Node (toList INTRS), model', args') end end @@ -2343,9 +2337,7 @@ fun get_constr_args (cname, cargs) = let val cTerm = Const (cname, (map (typ_of_dtyp descr typ_assoc) cargs) ---> Type (s, Ts)) - (*TODO val _ = writeln ("cTerm: " ^ makestring cTerm) *) val (iC, _, _) = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm - (*TODO val _ = writeln ("iC: " ^ makestring iC) *) (* interpretation -> int list option *) fun get_args (Leaf xs) = if find_index_eq True xs = element then