src/HOL/Tools/refute.ML
changeset 17314 04e21a27c0ad
parent 17274 746bb4c56800
child 17412 e26cb20ef0cc
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Sep 08 16:08:50 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Sep 08 16:09:23 2005 +0200
     1.3 @@ -271,7 +271,7 @@
     1.4  	let
     1.5  		val {interpreters, printers, parameters} = RefuteData.get thy
     1.6  	in
     1.7 -		case assoc (interpreters, name) of
     1.8 +		case AList.lookup (op =) interpreters name of
     1.9  		  NONE   => RefuteData.put {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} thy
    1.10  		| SOME _ => error ("Interpreter " ^ name ^ " already declared")
    1.11  	end;
    1.12 @@ -282,7 +282,7 @@
    1.13  	let
    1.14  		val {interpreters, printers, parameters} = RefuteData.get thy
    1.15  	in
    1.16 -		case assoc (printers, name) of
    1.17 +		case AList.lookup (op =) printers name of
    1.18  		  NONE   => RefuteData.put {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} thy
    1.19  		| SOME _ => error ("Printer " ^ name ^ " already declared")
    1.20  	end;
    1.21 @@ -335,14 +335,14 @@
    1.22  	let
    1.23  		(* (string * string) list * string -> int *)
    1.24  		fun read_int (parms, name) =
    1.25 -			case assoc_string (parms, name) of
    1.26 +			case AList.lookup (op =) parms name of
    1.27  			  SOME s => (case Int.fromString s of
    1.28  				  SOME i => i
    1.29  				| NONE   => error ("parameter " ^ quote name ^ " (value is " ^ quote s ^ ") must be an integer value"))
    1.30  			| NONE   => error ("parameter " ^ quote name ^ " must be assigned a value")
    1.31  		(* (string * string) list * string -> string *)
    1.32  		fun read_string (parms, name) =
    1.33 -			case assoc_string (parms, name) of
    1.34 +			case AList.lookup (op =) parms name of
    1.35  			  SOME s => s
    1.36  			| NONE   => error ("parameter " ^ quote name ^ " must be assigned a value")
    1.37  		(* (string * string) list *)
    1.38 @@ -382,12 +382,12 @@
    1.39  
    1.40  	fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
    1.41  		(* replace a 'DtTFree' variable by the associated type *)
    1.42 -		(valOf o assoc) (typ_assoc, DatatypeAux.DtTFree a)
    1.43 +		(the o AList.lookup (op =) typ_assoc) (DatatypeAux.DtTFree a)
    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  	  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
    1.47  		let
    1.48 -			val (s, ds, _) = (valOf o assoc) (descr, i)
    1.49 +			val (s, ds, _) = (the o AList.lookup (op =) descr) i
    1.50  		in
    1.51  			Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.52  		end;
    1.53 @@ -590,7 +590,7 @@
    1.54  			| Const ("arbitrary", T)          => collect_type_axioms (axs, T)
    1.55  			| Const ("The", T)                =>
    1.56  				let
    1.57 -					val ax = specialize_type (("The", T), (valOf o assoc) (axioms, "HOL.the_eq_trivial"))
    1.58 +					val ax = specialize_type (("The", T), (the o AList.lookup (op =) axioms) "HOL.the_eq_trivial")
    1.59  				in
    1.60  					if mem_term (ax, axs) then
    1.61  						collect_type_axioms (axs, T)
    1.62 @@ -600,7 +600,8 @@
    1.63  				end
    1.64  			| Const ("Hilbert_Choice.Eps", T) =>
    1.65  				let
    1.66 -					val ax = specialize_type (("Hilbert_Choice.Eps", T), (valOf o assoc) (axioms, "Hilbert_Choice.someI"))
    1.67 +					val ax = specialize_type (("Hilbert_Choice.Eps", T),
    1.68 +                      (the o AList.lookup (op =) axioms) "Hilbert_Choice.someI")
    1.69  				in
    1.70  					if mem_term (ax, axs) then
    1.71  						collect_type_axioms (axs, T)
    1.72 @@ -690,7 +691,8 @@
    1.73  							val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
    1.74  							(* Term.term option *)
    1.75  							val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
    1.76 -							val intro_ax   = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, s ^ ".intro")) handle Type.TYPE_MATCH => NONE)
    1.77 +							val intro_ax   = (Option.map (fn t => specialize_type ((s, T), t))
    1.78 +								(AList.lookup (op =) axioms (class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
    1.79  							val axs'       = (case ofclass_ax of NONE => axs | SOME ax => if mem_term (ax, axs) then
    1.80  									(* collect relevant type axioms *)
    1.81  									collect_type_axioms (axs, T)
    1.82 @@ -776,7 +778,7 @@
    1.83  						let
    1.84  							val index               = #index info
    1.85  							val descr               = #descr info
    1.86 -							val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
    1.87 +							val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
    1.88  							val typ_assoc           = dtyps ~~ Ts
    1.89  							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
    1.90  							val _ = (if Library.exists (fn d =>
    1.91 @@ -829,7 +831,7 @@
    1.92  	fun first_universe xs sizes minsize =
    1.93  	let
    1.94  		fun size_of_typ T =
    1.95 -			case assoc (sizes, string_of_typ T) of
    1.96 +			case AList.lookup (op =) sizes (string_of_typ T) of
    1.97  			  SOME n => n
    1.98  			| NONE   => minsize
    1.99  	in
   1.100 @@ -876,7 +878,7 @@
   1.101  				(* continue search *)
   1.102  				next max (len+1) (sum+x1) (x2::xs)
   1.103  		(* only consider those types for which the size is not fixed *)
   1.104 -		val mutables = List.filter (fn (T, _) => assoc (sizes, string_of_typ T) = NONE) xs
   1.105 +		val mutables = List.filter (not o (AList.defined (op =) sizes) o string_of_typ o fst) xs
   1.106  		(* subtract 'minsize' from every size (will be added again at the end) *)
   1.107  		val diffs = map (fn (_, n) => n-minsize) mutables
   1.108  	in
   1.109 @@ -884,7 +886,7 @@
   1.110  		  SOME diffs' =>
   1.111  			(* merge with those types for which the size is fixed *)
   1.112  			SOME (snd (foldl_map (fn (ds, (T, _)) =>
   1.113 -				case assoc (sizes, string_of_typ T) of
   1.114 +				case AList.lookup (op =) sizes (string_of_typ T) of
   1.115  				  SOME n => (ds, (T, n))                    (* return the fixed size *)
   1.116  				| NONE   => (tl ds, (T, minsize + hd ds)))  (* consume the head of 'ds', add 'minsize' *)
   1.117  				(diffs', xs)))
   1.118 @@ -949,7 +951,7 @@
   1.119  						let
   1.120  							val index           = #index info
   1.121  							val descr           = #descr info
   1.122 -							val (_, _, constrs) = (valOf o assoc) (descr, index)
   1.123 +							val (_, _, constrs) = (the o AList.lookup (op =) descr) index
   1.124  						in
   1.125  							(* recursive datatype? *)
   1.126  							Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs
   1.127 @@ -1358,7 +1360,7 @@
   1.128  			(* unit -> (interpretation * model * arguments) option *)
   1.129  			fun interpret_groundtype () =
   1.130  			let
   1.131 -				val size = (if T = Term.propT then 2 else (valOf o assoc) (typs, T))                    (* the model MUST specify a size for ground types *)
   1.132 +				val size = (if T = Term.propT then 2 else (the o AList.lookup (op =) typs) T)                    (* the model MUST specify a size for ground types *)
   1.133  				val next = next_idx+size
   1.134  				val _    = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
   1.135  				(* prop_formula list *)
   1.136 @@ -1407,7 +1409,7 @@
   1.137  			| TVar  _ => interpret_groundtype ()
   1.138  		end
   1.139  	in
   1.140 -		case assoc (terms, t) of
   1.141 +		case AList.lookup (op =) terms t of
   1.142  		  SOME intr =>
   1.143  			(* return an existing interpretation *)
   1.144  			SOME (intr, model, args)
   1.145 @@ -1598,7 +1600,7 @@
   1.146  	let
   1.147  		val (typs, terms) = model
   1.148  	in
   1.149 -		case assoc (terms, t) of
   1.150 +		case AList.lookup (op =) terms t of
   1.151  		  SOME intr =>
   1.152  			(* return an existing interpretation *)
   1.153  			SOME (intr, model, args)
   1.154 @@ -1651,7 +1653,7 @@
   1.155  			  SOME info =>  (* inductive datatype *)
   1.156  				let
   1.157  					(* int option -- only recursive IDTs have an associated depth *)
   1.158 -					val depth = assoc (typs, Type (s, Ts))
   1.159 +					val depth = AList.lookup (op =) typs (Type (s, Ts))
   1.160  				in
   1.161  					if depth = (SOME 0) then  (* termination condition to avoid infinite recursion *)
   1.162  						(* return a leaf of size 0 *)
   1.163 @@ -1660,7 +1662,7 @@
   1.164  						let
   1.165  							val index               = #index info
   1.166  							val descr               = #descr info
   1.167 -							val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
   1.168 +							val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
   1.169  							val typ_assoc           = dtyps ~~ Ts
   1.170  							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.171  							val _ = (if Library.exists (fn d =>
   1.172 @@ -1670,7 +1672,8 @@
   1.173  								else
   1.174  									())
   1.175  							(* if the model specifies a depth for the current type, decrement it to avoid infinite recursion *)
   1.176 -							val typs'    = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s, Ts), n-1)))
   1.177 +							val typs'    = case depth of NONE => typs | SOME n =>
   1.178 +								AList.update (op =) (Type (s, Ts), n-1) typs
   1.179  							(* recursively compute the size of the datatype *)
   1.180  							val size     = size_of_dtyp thy typs' descr typ_assoc constrs
   1.181  							val next_idx = #next_idx args
   1.182 @@ -1695,7 +1698,7 @@
   1.183  		  | interpret_term _ =  (* a (free or schematic) type variable *)
   1.184  			NONE
   1.185  	in
   1.186 -		case assoc (terms, t) of
   1.187 +		case AList.lookup (op =) terms t of
   1.188  		  SOME intr =>
   1.189  			(* return an existing interpretation *)
   1.190  			SOME (intr, model, args)
   1.191 @@ -1713,7 +1716,7 @@
   1.192  	let
   1.193  		val (typs, terms) = model
   1.194  	in
   1.195 -		case assoc (terms, t) of
   1.196 +		case AList.lookup (op =) terms t of
   1.197  		  SOME intr =>
   1.198  			(* return an existing interpretation *)
   1.199  			SOME (intr, model, args)
   1.200 @@ -1727,7 +1730,7 @@
   1.201  						let
   1.202  							val index               = #index info
   1.203  							val descr               = #descr info
   1.204 -							val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
   1.205 +							val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
   1.206  							val typ_assoc           = dtyps ~~ Ts'
   1.207  							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.208  							val _ = (if Library.exists (fn d =>
   1.209 @@ -1751,8 +1754,9 @@
   1.210  									val (i, _, _) = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type (s', Ts')))
   1.211  									val total     = size_of_type i
   1.212  									(* int option -- only recursive IDTs have an associated depth *)
   1.213 -									val depth = assoc (typs, Type (s', Ts'))
   1.214 -									val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s', Ts'), n-1)))
   1.215 +									val depth = AList.lookup (op =) typs (Type (s', Ts'))
   1.216 +									val typs' = (case depth of NONE => typs | SOME n =>
   1.217 +										AList.update (op =) (Type (s', Ts'), n-1) typs)
   1.218  									(* returns an interpretation where everything is mapped to "undefined" *)
   1.219  									(* DatatypeAux.dtyp list -> interpretation *)
   1.220  									fun make_undef [] =
   1.221 @@ -1904,7 +1908,7 @@
   1.222  						let
   1.223  							val index              = #index info
   1.224  							val descr              = #descr info
   1.225 -							val (dtname, dtyps, _) = (valOf o assoc) (descr, index)
   1.226 +							val (dtname, dtyps, _) = (the o AList.lookup (op =) descr) index
   1.227  							(* number of all constructors, including those of different           *)
   1.228  							(* (mutually recursive) datatypes within the same descriptor 'descr'  *)
   1.229  							val mconstrs_count     = sum (map (fn (_, (_, _, cs)) => length cs) descr)
   1.230 @@ -1995,7 +1999,7 @@
   1.231  												  SOME args => (n, args)
   1.232  												| NONE      => get_cargs_rec (n+1, xs))
   1.233  										in
   1.234 -											get_cargs_rec (0, (valOf o assoc) (mc_intrs, idx))
   1.235 +											get_cargs_rec (0, (the o AList.lookup (op =) mc_intrs) idx)
   1.236  										end
   1.237  									(* returns the number of constructors in datatypes that occur in *)
   1.238  									(* the descriptor 'descr' before the datatype given by 'idx'     *)
   1.239 @@ -2015,7 +2019,7 @@
   1.240  									(* where 'idx' gives the datatype and 'elem' the element of it             *)
   1.241  									(* int -> int -> interpretation *)
   1.242  									fun compute_array_entry idx elem =
   1.243 -										case Array.sub ((valOf o assoc) (INTRS, idx), elem) of
   1.244 +										case Array.sub ((the o AList.lookup (op =) INTRS) idx, elem) of
   1.245  										  SOME result =>
   1.246  											(* simply return the previously computed result *)
   1.247  											result
   1.248 @@ -2033,7 +2037,7 @@
   1.249  												(* select the correct subtree of the parameter corresponding to constructor 'c' *)
   1.250  												val p_intr = select_subtree (List.nth (p_intrs, get_coffset idx + c), args)
   1.251  												(* find the indices of the constructor's recursive arguments *)
   1.252 -												val (_, _, constrs) = (valOf o assoc) (descr, idx)
   1.253 +												val (_, _, constrs) = (the o AList.lookup (op =) descr) idx
   1.254  												val constr_args     = (snd o List.nth) (constrs, c)
   1.255  												val rec_args        = List.filter (DatatypeAux.is_rec_type o fst) (constr_args ~~ args)
   1.256  												val rec_args'       = map (fn (dtyp, elem) => (DatatypeAux.dest_DtRec dtyp, elem)) rec_args
   1.257 @@ -2041,7 +2045,7 @@
   1.258  												val result = foldl (fn ((idx, elem), intr) =>
   1.259  													interpretation_apply (intr, compute_array_entry idx elem)) p_intr rec_args'
   1.260  												(* update 'INTRS' *)
   1.261 -												val _ = Array.update ((valOf o assoc) (INTRS, idx), elem, SOME result)
   1.262 +												val _ = Array.update ((the o AList.lookup (op =) INTRS) idx, elem, SOME result)
   1.263  											in
   1.264  												result
   1.265  											end
   1.266 @@ -2060,13 +2064,13 @@
   1.267  										in
   1.268  											modifyi_loop 0
   1.269  										end
   1.270 -									val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((valOf o assoc) (INTRS, index))
   1.271 +									val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((the o AList.lookup (op =) INTRS) index)
   1.272  									(* 'a Array.array -> 'a list *)
   1.273  									fun toList arr =
   1.274  										Array.foldr op:: [] arr
   1.275  								in
   1.276  									(* return the part of 'INTRS' that corresponds to the current datatype *)
   1.277 -									SOME ((Node o (map valOf) o toList o valOf o assoc) (INTRS, index), model', args')
   1.278 +									SOME ((Node o map the o toList o the o AList.lookup (op =) INTRS) index, model', args')
   1.279  								end
   1.280  						end
   1.281  					else
   1.282 @@ -2515,7 +2519,7 @@
   1.283  					val (typs, _)           = model
   1.284  					val index               = #index info
   1.285  					val descr               = #descr info
   1.286 -					val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
   1.287 +					val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
   1.288  					val typ_assoc           = dtyps ~~ Ts
   1.289  					(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.290  					val _ = (if Library.exists (fn d =>