src/HOL/Tools/refute.ML
changeset 15335 f81e6e24351f
parent 15334 d5a92997dc1b
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Nov 25 19:25:03 2004 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Nov 25 20:33:35 2004 +0100
     1.3 @@ -376,6 +376,26 @@
     1.4  (* ------------------------------------------------------------------------- *)
     1.5  
     1.6  (* ------------------------------------------------------------------------- *)
     1.7 +(* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type        *)
     1.8 +(*              ('Term.typ'), given type parameters for the data type's type *)
     1.9 +(*              arguments                                                    *)
    1.10 +(* ------------------------------------------------------------------------- *)
    1.11 +
    1.12 +	(* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
    1.13 +
    1.14 +	fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
    1.15 +		(* replace a 'DtTFree' variable by the associated type *)
    1.16 +		(the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
    1.17 +	  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
    1.18 +		let
    1.19 +			val (s, ds, _) = (the o assoc) (descr, i)
    1.20 +		in
    1.21 +			Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.22 +		end
    1.23 +	  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
    1.24 +		Type (s, map (typ_of_dtyp descr typ_assoc) ds);
    1.25 +
    1.26 +(* ------------------------------------------------------------------------- *)
    1.27  (* collect_axioms: collects (monomorphic, universally quantified versions    *)
    1.28  (*                 of) all HOL axioms that are relevant w.r.t 't'            *)
    1.29  (* ------------------------------------------------------------------------- *)
    1.30 @@ -691,18 +711,6 @@
    1.31  									raise REFUTE ("ground_types", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable")
    1.32  								else
    1.33  									())
    1.34 -							(* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
    1.35 -							fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
    1.36 -								(* replace a 'DtTFree' variable by the associated type *)
    1.37 -								(the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
    1.38 -							  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
    1.39 -								let
    1.40 -									val (s, ds, _) = (the o assoc) (descr, i)
    1.41 -								in
    1.42 -									Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.43 -								end
    1.44 -							  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
    1.45 -								Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.46  							(* if the current type is a recursive IDT (i.e. a depth is required), add it to 'acc' *)
    1.47  							val acc' = (if Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
    1.48  									T ins acc
    1.49 @@ -1128,6 +1136,40 @@
    1.50  			(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
    1.51  	end;
    1.52  
    1.53 +(* ------------------------------------------------------------------------- *)
    1.54 +(* sum: returns the sum of a list 'xs' of integers                           *)
    1.55 +(* ------------------------------------------------------------------------- *)
    1.56 +
    1.57 +	(* int list -> int *)
    1.58 +
    1.59 +	fun sum xs = foldl op+ (0, xs);
    1.60 +
    1.61 +(* ------------------------------------------------------------------------- *)
    1.62 +(* product: returns the product of a list 'xs' of integers                   *)
    1.63 +(* ------------------------------------------------------------------------- *)
    1.64 +
    1.65 +	(* int list -> int *)
    1.66 +
    1.67 +	fun product xs = foldl op* (1, xs);
    1.68 +
    1.69 +(* ------------------------------------------------------------------------- *)
    1.70 +(* size_of_dtyp: the size of (an initial fragment of) a data type is the sum *)
    1.71 +(*               (over its constructors) of the product (over their          *)
    1.72 +(*               arguments) of the size of the argument types                *)
    1.73 +(* ------------------------------------------------------------------------- *)
    1.74 +
    1.75 +	(* theory -> (Term.typ * int) list -> DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> (string * DatatypeAux.dtyp list) list -> int *)
    1.76 +
    1.77 +	fun size_of_dtyp thy typ_sizes descr typ_assoc constructors =
    1.78 +		sum (map (fn (_, dtyps) =>
    1.79 +			product (map (fn dtyp =>
    1.80 +				let
    1.81 +					val T         = typ_of_dtyp descr typ_assoc dtyp
    1.82 +					val (i, _, _) = interpret thy (typ_sizes, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
    1.83 +				in
    1.84 +					size_of_type i
    1.85 +				end) dtyps)) constructors);
    1.86 +
    1.87  
    1.88  (* ------------------------------------------------------------------------- *)
    1.89  (* INTERPRETERS: Actual Interpreters                                         *)
    1.90 @@ -1437,34 +1479,6 @@
    1.91  	fun IDT_interpreter thy model args t =
    1.92  	let
    1.93  		val (typs, terms) = model
    1.94 -		(* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
    1.95 -		fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
    1.96 -			(* replace a 'DtTFree' variable by the associated type *)
    1.97 -			(the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
    1.98 -		  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
    1.99 -			let
   1.100 -				val (s, ds, _) = (the o assoc) (descr, i)
   1.101 -			in
   1.102 -				Type (s, map (typ_of_dtyp descr typ_assoc) ds)
   1.103 -			end
   1.104 -		  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
   1.105 -			Type (s, map (typ_of_dtyp descr typ_assoc) ds)
   1.106 -		(* int list -> int *)
   1.107 -		fun sum xs = foldl op+ (0, xs)
   1.108 -		(* int list -> int *)
   1.109 -		fun product xs = foldl op* (1, xs)
   1.110 -		(* the size of an IDT is the sum (over its constructors) of the        *)
   1.111 -		(* product (over their arguments) of the size of the argument type     *)
   1.112 -		(* (Term.typ * int) list -> DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> (string * DatatypeAux.dtyp list) list -> int *)
   1.113 -		fun size_of_dtyp typs descr typ_assoc constrs =
   1.114 -			sum (map (fn (_, ds) =>
   1.115 -				product (map (fn d =>
   1.116 -					let
   1.117 -						val T         = typ_of_dtyp descr typ_assoc d
   1.118 -						val (i, _, _) = interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.119 -					in
   1.120 -						size_of_type i
   1.121 -					end) ds)) constrs)
   1.122  		(* Term.typ -> (interpretation * model * arguments) option *)
   1.123  		fun interpret_variable (Type (s, Ts)) =
   1.124  			(case DatatypePackage.datatype_info thy s of
   1.125 @@ -1493,7 +1507,7 @@
   1.126  							(* if the model specifies a depth for the current type, decrement it to avoid infinite recursion *)
   1.127  							val typs'    = (case depth of None => typs | Some n => overwrite (typs, (Type (s, Ts), n-1)))
   1.128  							(* recursively compute the size of the datatype *)
   1.129 -							val size     = size_of_dtyp typs' descr typ_assoc constrs
   1.130 +							val size     = size_of_dtyp thy typs' descr typ_assoc constrs
   1.131  							val next_idx = #next_idx args
   1.132  							val next     = (if size=1 then next_idx else if size=2 then next_idx+1 else next_idx+size)  (* optimization for types with size 1 or size 2 *)
   1.133  							val _        = (if next-1>(#maxvars args) andalso (#maxvars args)>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
   1.134 @@ -1563,9 +1577,9 @@
   1.135  											val depth = assoc (typs, Type (s', Ts'))
   1.136  											val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s', Ts'), n-1)))
   1.137  											(* constructors before 'Const (s, T)' generate elements of the datatype *)
   1.138 -											val offset  = size_of_dtyp typs' descr typ_assoc constrs1
   1.139 +											val offset  = size_of_dtyp thy typs' descr typ_assoc constrs1
   1.140  											(* 'Const (s, T)' and constructors after it generate elements of the datatype *)
   1.141 -											val total   = offset + (size_of_dtyp typs' descr typ_assoc constrs2)
   1.142 +											val total   = offset + (size_of_dtyp thy typs' descr typ_assoc constrs2)
   1.143  											(* create an interpretation that corresponds to the constructor 'Const (s, T)' *)
   1.144  											(* by recursion over its argument types                                        *)
   1.145  											(* DatatypeAux.dtyp list -> interpretation *)
   1.146 @@ -1811,34 +1825,6 @@
   1.147  					(* int option -- only recursive IDTs have an associated depth *)
   1.148  					val depth = assoc (typs, Type (s, Ts))
   1.149  					val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s, Ts), n-1)))
   1.150 -					(* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
   1.151 -					fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
   1.152 -						(* replace a 'DtTFree' variable by the associated type *)
   1.153 -						(the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
   1.154 -					  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
   1.155 -						let
   1.156 -							val (s, ds, _) = (the o assoc) (descr, i)
   1.157 -						in
   1.158 -							Type (s, map (typ_of_dtyp descr typ_assoc) ds)
   1.159 -						end
   1.160 -					  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
   1.161 -						Type (s, map (typ_of_dtyp descr typ_assoc) ds)
   1.162 -					(* int list -> int *)
   1.163 -					fun sum xs = foldl op+ (0, xs)
   1.164 -					(* int list -> int *)
   1.165 -					fun product xs = foldl op* (1, xs)
   1.166 -					(* the size of an IDT is the sum (over its constructors) of the        *)
   1.167 -					(* product (over their arguments) of the size of the argument type     *)
   1.168 -					(* (Term.typ * int) list -> DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> (string * DatatypeAux.dtyp list) list -> int *)
   1.169 -					fun size_of_dtyp typs descr typ_assoc xs =
   1.170 -						sum (map (fn (_, ds) =>
   1.171 -							product (map (fn d =>
   1.172 -								let
   1.173 -									val T         = typ_of_dtyp descr typ_assoc d
   1.174 -									val (i, _, _) = interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.175 -					in
   1.176 -						size_of_type i
   1.177 -					end) ds)) xs)
   1.178  					(* int -> DatatypeAux.dtyp list -> Term.term list *)
   1.179  					fun make_args n [] =
   1.180  						if n<>0 then
   1.181 @@ -1861,7 +1847,7 @@
   1.182  						raise REFUTE ("IDT_printer", "invalid interpretation (value too large - not enough constructors)")
   1.183  					  | make_term n (c::cs) =
   1.184  						let
   1.185 -							val c_size = size_of_dtyp typs' descr typ_assoc [c]
   1.186 +							val c_size = size_of_dtyp thy typs' descr typ_assoc [c]
   1.187  						in
   1.188  							if n<c_size then
   1.189  								let