1.1 --- a/src/HOL/Tools/refute.ML Tue Mar 15 17:07:41 2005 +0100
1.2 +++ b/src/HOL/Tools/refute.ML Thu Mar 17 01:40:18 2005 +0100
1.3 @@ -100,7 +100,7 @@
1.4
1.5 (* 'a tree * 'b tree -> ('a * 'b) tree *)
1.6
1.7 - fun tree_pair (t1,t2) =
1.8 + fun tree_pair (t1, t2) =
1.9 case t1 of
1.10 Leaf x =>
1.11 (case t2 of
1.12 @@ -240,7 +240,7 @@
1.13 if null typs then
1.14 "empty universe (no type variables in term)\n"
1.15 else
1.16 - "Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs) ^ "\n"
1.17 + "Size of types: " ^ commas (map (fn (T, i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs) ^ "\n"
1.18 val show_consts_msg =
1.19 if not (!show_consts) andalso Library.exists (is_Const o fst) terms then
1.20 "set \"show_consts\" to show the interpretation of constants\n"
1.21 @@ -250,7 +250,7 @@
1.22 if null terms then
1.23 "empty interpretation (no free variables in term)\n"
1.24 else
1.25 - space_implode "\n" (List.mapPartial (fn (t,intr) =>
1.26 + space_implode "\n" (List.mapPartial (fn (t, intr) =>
1.27 (* print constants only if 'show_consts' is true *)
1.28 if (!show_consts) orelse not (is_Const t) then
1.29 SOME (Sign.string_of_term (sign_of thy) t ^ ": " ^ Sign.string_of_term (sign_of thy) (print thy model t intr assignment))
1.30 @@ -1055,7 +1055,7 @@
1.31 val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
1.32 (* Term.term *)
1.33 val ex_closure = Library.foldl
1.34 - (fn (t', ((x,i),T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
1.35 + (fn (t', ((x, i), T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
1.36 (t, vars)
1.37 (* If 't' is of type 'propT' (rather than 'boolT'), applying *)
1.38 (* 'HOLogic.exists_const' is not type-correct. However, this *)
1.39 @@ -1117,7 +1117,7 @@
1.40 map (fn x => [x]) xs
1.41 | pick_all n xs =
1.42 let val rec_pick = pick_all (n-1) xs in
1.43 - Library.foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.44 + Library.foldl (fn (acc, x) => (cons_list x rec_pick) @ acc) ([], xs)
1.45 end
1.46 in
1.47 case intr of
1.48 @@ -1134,11 +1134,11 @@
1.49
1.50 fun size_of_type intr =
1.51 let
1.52 - (* power(a,b) computes a^b, for a>=0, b>=0 *)
1.53 + (* power (a, b) computes a^b, for a>=0, b>=0 *)
1.54 (* int * int -> int *)
1.55 - fun power (a,0) = 1
1.56 - | power (a,1) = a
1.57 - | power (a,b) = let val ab = power(a, b div 2) in ab * ab * power(a, b mod 2) end
1.58 + fun power (a, 0) = 1
1.59 + | power (a, 1) = a
1.60 + | power (a, b) = let val ab = power(a, b div 2) in ab * ab * power(a, b mod 2) end
1.61 in
1.62 case intr of
1.63 Leaf xs => length xs
1.64 @@ -1270,7 +1270,7 @@
1.65 map (fn x => [x]) xs
1.66 | pick_all (xs::xss) =
1.67 let val rec_pick = pick_all xss in
1.68 - Library.foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.69 + Library.foldl (fn (acc, x) => (cons_list x rec_pick) @ acc) ([], xs)
1.70 end
1.71 | pick_all _ =
1.72 raise REFUTE ("interpretation_apply", "empty list (in pick_all)")
1.73 @@ -1307,7 +1307,7 @@
1.74
1.75 (* int list -> int *)
1.76
1.77 - fun sum xs = Library.foldl op+ (0, xs);
1.78 + fun sum xs = foldl op+ 0 xs;
1.79
1.80 (* ------------------------------------------------------------------------- *)
1.81 (* product: returns the product of a list 'xs' of integers *)
1.82 @@ -1315,7 +1315,7 @@
1.83
1.84 (* int list -> int *)
1.85
1.86 - fun product xs = Library.foldl op* (1, xs);
1.87 + fun product xs = foldl op* 1 xs;
1.88
1.89 (* ------------------------------------------------------------------------- *)
1.90 (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *)
1.91 @@ -1750,6 +1750,7 @@
1.92 (* int option -- only recursive IDTs have an associated depth *)
1.93 val depth = assoc (typs, Type (s', Ts'))
1.94 val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s', Ts'), n-1)))
1.95 + (* returns an interpretation where everything is mapped to "undefined" *)
1.96 (* DatatypeAux.dtyp list -> interpretation *)
1.97 fun make_undef [] =
1.98 Leaf (replicate total False)
1.99 @@ -1782,14 +1783,14 @@
1.100 raise REFUTE ("IDT_constructor_interpreter", "current size is less than old size")
1.101 else
1.102 ()
1.103 - (* elements that exist at the previous depth are mapped to a defined *)
1.104 - (* value, while new elements are mapped to "undefined" by the *)
1.105 - (* recursive constructor *)
1.106 (* int * interpretation list *)
1.107 val (new_offset, intrs) = foldl_map make_constr (offset, replicate size' ds)
1.108 (* interpretation list *)
1.109 val undefs = replicate (size - size') (make_undef ds)
1.110 in
1.111 + (* elements that exist at the previous depth are mapped to a defined *)
1.112 + (* value, while new elements are mapped to "undefined" by the *)
1.113 + (* recursive constructor *)
1.114 (new_offset, Node (intrs @ undefs))
1.115 end
1.116 (* extends the interpretation for a constructor (both recursive *)
1.117 @@ -1799,7 +1800,7 @@
1.118 let
1.119 (* returns the k-th unit vector of length n *)
1.120 (* int * int -> interpretation *)
1.121 - fun unit_vector (k,n) =
1.122 + fun unit_vector (k, n) =
1.123 Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.124 (* int *)
1.125 val k = find_index_eq True xs
1.126 @@ -1812,7 +1813,7 @@
1.127 else
1.128 (* if the element was already mapped to a defined value, map it *)
1.129 (* to the same value again, just extend the length of the leaf, *)
1.130 - (* do not increment offset *)
1.131 + (* do not increment the 'offset' *)
1.132 (offset, unit_vector (k+1, total))
1.133 end
1.134 | extend_constr (_, [], Node _) =
1.135 @@ -1842,14 +1843,8 @@
1.136 (* DatatypeAux.dtyp list -> bool *)
1.137 fun is_rec_constr ds =
1.138 Library.exists DatatypeAux.is_rec_type ds
1.139 - (* constructors before 'Const (s, T)' generate elements of the datatype, *)
1.140 - (* and if the constructor is recursive, then non-recursive constructors *)
1.141 - (* after it generate further elements *)
1.142 - val offset = size_of_dtyp thy typs' descr typ_assoc constrs1 +
1.143 - (if is_rec_constr ctypes then
1.144 - size_of_dtyp thy typs' descr typ_assoc (List.filter (not o is_rec_constr o snd) cs)
1.145 - else
1.146 - 0)
1.147 + (* constructors before 'Const (s, T)' generate elements of the datatype *)
1.148 + val offset = size_of_dtyp thy typs' descr typ_assoc constrs1
1.149 in
1.150 case depth of
1.151 NONE => (* equivalent to a depth of 1 *)
1.152 @@ -2011,7 +2006,6 @@
1.153 fun toList arr =
1.154 Array.foldr op:: [] arr
1.155 in
1.156 - (* TODO writeln ("REC-OP: " ^ makestring (Node (toList INTRS))); *)
1.157 SOME (Node (toList INTRS), model', args')
1.158 end
1.159 end
1.160 @@ -2343,9 +2337,7 @@
1.161 fun get_constr_args (cname, cargs) =
1.162 let
1.163 val cTerm = Const (cname, (map (typ_of_dtyp descr typ_assoc) cargs) ---> Type (s, Ts))
1.164 - (*TODO val _ = writeln ("cTerm: " ^ makestring cTerm) *)
1.165 val (iC, _, _) = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
1.166 - (*TODO val _ = writeln ("iC: " ^ makestring iC) *)
1.167 (* interpretation -> int list option *)
1.168 fun get_args (Leaf xs) =
1.169 if find_index_eq True xs = element then