exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)
authorwebertj
Thu Nov 25 19:25:03 2004 +0100 (2004-11-25)
changeset 15334d5a92997dc1b
parent 15333 77b2bca7fcb5
child 15335 f81e6e24351f
exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Nov 25 19:04:32 2004 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Nov 25 19:25:03 2004 +0100
     1.3 @@ -27,13 +27,12 @@
     1.4  	type model
     1.5  	type arguments
     1.6  
     1.7 -	exception CANNOT_INTERPRET of Term.term
     1.8  	exception MAXVARS_EXCEEDED
     1.9  
    1.10  	val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory
    1.11  	val add_printer     : string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option) -> theory -> theory
    1.12  
    1.13 -	val interpret : theory -> model -> arguments -> Term.term -> (interpretation * model * arguments)  (* exception CANNOT_INTERPRET *)
    1.14 +	val interpret : theory -> model -> arguments -> Term.term -> (interpretation * model * arguments)
    1.15  
    1.16  	val print       : theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term
    1.17  	val print_model : theory -> model -> (int -> bool) -> string
    1.18 @@ -67,8 +66,6 @@
    1.19  	(* 'error'.                                                          *)
    1.20  	exception REFUTE of string * string;  (* ("in function", "cause") *)
    1.21  
    1.22 -	exception CANNOT_INTERPRET of Term.term;
    1.23 -
    1.24  	(* should be raised by an interpreter when more variables would be *)
    1.25  	(* required than allowed by 'maxvars'                              *)
    1.26  	exception MAXVARS_EXCEEDED;
    1.27 @@ -207,18 +204,16 @@
    1.28  
    1.29  
    1.30  (* ------------------------------------------------------------------------- *)
    1.31 -(* interpret: tries to interpret the term 't' using a suitable interpreter;  *)
    1.32 -(*            returns the interpretation and a (possibly extended) model     *)
    1.33 -(*            that keeps track of the interpretation of subterms             *)
    1.34 -(* Note: exception 'CANNOT_INTERPRET t' is raised if the term cannot be      *)
    1.35 -(*       interpreted by any interpreter                                      *)
    1.36 +(* interpret: interprets the term 't' using a suitable interpreter; returns  *)
    1.37 +(*            the interpretation and a (possibly extended) model that keeps  *)
    1.38 +(*            track of the interpretation of subterms                        *)
    1.39  (* ------------------------------------------------------------------------- *)
    1.40  
    1.41  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) *)
    1.42  
    1.43  	fun interpret thy model args t =
    1.44  		(case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of
    1.45 -		  None   => raise (CANNOT_INTERPRET t)
    1.46 +		  None   => raise REFUTE ("interpret", "unable to interpret term " ^ quote (Sign.string_of_term (sign_of thy) t))
    1.47  		| Some x => x);
    1.48  
    1.49  (* ------------------------------------------------------------------------- *)
    1.50 @@ -878,7 +873,7 @@
    1.51  				   else commas (map (Sign.string_of_typ (sign_of thy)) types)))
    1.52  			(* (Term.typ * int) list -> unit *)
    1.53  			fun find_model_loop universe =
    1.54 -			(let
    1.55 +			let
    1.56  				val init_model             = (universe, [])
    1.57  				val init_args              = {maxvars = maxvars, next_idx = 1, bounds = [], wellformed = True}
    1.58  				val _                      = immediate_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
    1.59 @@ -908,8 +903,6 @@
    1.60  					error ("SAT solver " ^ quote satsolver ^ " is not configured.")
    1.61  			end handle MAXVARS_EXCEEDED =>
    1.62  				writeln ("\nSearch terminated, number of Boolean variables (" ^ string_of_int maxvars ^ " allowed) exceeded.")
    1.63 -			| CANNOT_INTERPRET t' =>
    1.64 -				error ("Unable to interpret term " ^ Sign.string_of_term (sign_of thy) t'))
    1.65  			in
    1.66  				find_model_loop (first_universe types sizes minsize)
    1.67  			end
    1.68 @@ -1181,9 +1174,7 @@
    1.69  					(* we create 'size_of_type (interpret (... T1))' different copies *)
    1.70  					(* of the interpretation for 'T2', which are then combined into a *)
    1.71  					(* single new interpretation                                      *)
    1.72 -					val (i1, _, _) =
    1.73 -						(interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
    1.74 -						handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
    1.75 +					val (i1, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
    1.76  					(* make fresh copies, with different variable indices *)
    1.77  					(* 'idx': next variable index                         *)
    1.78  					(* 'n'  : number of copies                            *)
    1.79 @@ -1192,9 +1183,7 @@
    1.80  						(idx, [], True)
    1.81  					  | make_copies idx n =
    1.82  						let
    1.83 -							val (copy, _, new_args) =
    1.84 -								(interpret thy (typs, []) {maxvars = maxvars, next_idx = idx, bounds = [], wellformed = True} (Free ("dummy", T2))
    1.85 -								handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
    1.86 +							val (copy, _, new_args) = interpret thy (typs, []) {maxvars = maxvars, next_idx = idx, bounds = [], wellformed = True} (Free ("dummy", T2))
    1.87  							val (idx', copies, wf') = make_copies (#next_idx new_args) (n-1)
    1.88  						in
    1.89  							(idx', copy :: copies, SAnd (#wellformed new_args, wf'))
    1.90 @@ -1228,9 +1217,7 @@
    1.91  			| Abs (x, T, body) =>
    1.92  				let
    1.93  					(* create all constants of type 'T' *)
    1.94 -					val (i, _, _) =
    1.95 -						(interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
    1.96 -						handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
    1.97 +					val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
    1.98  					val constants = make_constants i
    1.99  					(* interpret the 'body' separately for each constant *)
   1.100  					val ((model', args'), bodies) = foldl_map
   1.101 @@ -1388,9 +1375,9 @@
   1.102  				Some (make_equality (i1, i2), m2, a2)
   1.103  			end
   1.104  		| Const ("op =", _) $ t1 =>
   1.105 -			(Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.106 +			Some (interpret thy model args (eta_expand t 1))
   1.107  		| Const ("op =", _) =>
   1.108 -			(Some (interpret thy model args (eta_expand t 2)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.109 +			Some (interpret thy model args (eta_expand t 2))
   1.110  		| Const ("op &", _) =>
   1.111  			Some (Node [Node [TT, FF], Node [FF, FF]], model, args)
   1.112  		| Const ("op |", _) =>
   1.113 @@ -1413,35 +1400,35 @@
   1.114  		| None =>
   1.115  			(case t of
   1.116  			  Free (x, Type ("set", [T])) =>
   1.117 -				(let
   1.118 +				let
   1.119  					val (intr, _, args') = interpret thy (typs, []) args (Free (x, T --> HOLogic.boolT))
   1.120  				in
   1.121  					Some (intr, (typs, (t, intr)::terms), args')
   1.122 -				end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.123 +				end
   1.124  			| Var ((x,i), Type ("set", [T])) =>
   1.125 -				(let
   1.126 +				let
   1.127  					val (intr, _, args') = interpret thy (typs, []) args (Var ((x,i), T --> HOLogic.boolT))
   1.128  				in
   1.129  					Some (intr, (typs, (t, intr)::terms), args')
   1.130 -				end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.131 +				end
   1.132  			| Const (s, Type ("set", [T])) =>
   1.133 -				(let
   1.134 +				let
   1.135  					val (intr, _, args') = interpret thy (typs, []) args (Const (s, T --> HOLogic.boolT))
   1.136  				in
   1.137  					Some (intr, (typs, (t, intr)::terms), args')
   1.138 -				end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.139 +				end
   1.140  			(* 'Collect' == identity *)
   1.141  			| Const ("Collect", _) $ t1 =>
   1.142  				Some (interpret thy model args t1)
   1.143  			| Const ("Collect", _) =>
   1.144 -				(Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.145 +				Some (interpret thy model args (eta_expand t 1))
   1.146  			(* 'op :' == application *)
   1.147  			| Const ("op :", _) $ t1 $ t2 =>
   1.148  				Some (interpret thy model args (t2 $ t1))
   1.149  			| Const ("op :", _) $ t1 =>
   1.150 -				(Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.151 +				Some (interpret thy model args (eta_expand t 1))
   1.152  			| Const ("op :", _) =>
   1.153 -				(Some (interpret thy model args (eta_expand t 2)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.154 +				Some (interpret thy model args (eta_expand t 2))
   1.155  			| _ => None)
   1.156  	end;
   1.157  
   1.158 @@ -1474,9 +1461,7 @@
   1.159  				product (map (fn d =>
   1.160  					let
   1.161  						val T         = typ_of_dtyp descr typ_assoc d
   1.162 -						val (i, _, _) =
   1.163 -							(interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.164 -							handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.165 +						val (i, _, _) = interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.166  					in
   1.167  						size_of_type i
   1.168  					end) ds)) constrs)
   1.169 @@ -1591,9 +1576,7 @@
   1.170  												let
   1.171  													(* compute the "new" size of the type 'd' *)
   1.172  													val T         = typ_of_dtyp descr typ_assoc d
   1.173 -													val (i, _, _) =
   1.174 -														(interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.175 -														handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.176 +													val (i, _, _) = interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.177  												in
   1.178  													(* all entries of the whole subtree are 'False' *)
   1.179  													Node (replicate (size_of_type i) (make_partial ds))
   1.180 @@ -1607,15 +1590,11 @@
   1.181  											  | make_constr (offset, d::ds) =
   1.182  												let
   1.183  													(* compute the "new" and "old" size of the type 'd' *)
   1.184 -													val T         = typ_of_dtyp descr typ_assoc d
   1.185 -													val (i, _, _) =
   1.186 -														(interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.187 -														handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.188 -													val (i', _, _) =
   1.189 -														(interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.190 -														handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.191 -													val size  = size_of_type i
   1.192 -													val size' = size_of_type i'
   1.193 +													val T          = typ_of_dtyp descr typ_assoc d
   1.194 +													val (i, _, _)  = interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.195 +													val (i', _, _) = interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.196 +													val size       = size_of_type i
   1.197 +													val size'      = size_of_type i'
   1.198  													val _ = if size<size' then
   1.199  															raise REFUTE ("IDT_interpreter", "internal error: new size < old size")
   1.200  														else
   1.201 @@ -1652,13 +1631,9 @@
   1.202  		case t of
   1.203  		  Const ("Finite_Set.card", Type ("fun", [Type ("set", [T]), Type ("nat", [])])) =>
   1.204  			let
   1.205 -				val (i_nat, _, _) =
   1.206 -					(interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
   1.207 -						handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.208 +				val (i_nat, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
   1.209  				val size_nat      = size_of_type i_nat
   1.210 -				val (i_set, _, _) =
   1.211 -					(interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("set", [T])))
   1.212 -						handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.213 +				val (i_set, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("set", [T])))
   1.214  				val constants     = make_constants i_set
   1.215  				(* interpretation -> int *)
   1.216  				fun number_of_elements (Node xs) =
   1.217 @@ -1721,7 +1696,7 @@
   1.218  		  Some T =>
   1.219  			(case T of
   1.220  			  Type ("fun", [T1, T2]) =>
   1.221 -				(let
   1.222 +				let
   1.223  					(* create all constants of type 'T1' *)
   1.224  					val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
   1.225  					val constants = make_constants i
   1.226 @@ -1743,7 +1718,7 @@
   1.227  					val HOLogic_insert    = Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
   1.228  				in
   1.229  					Some (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) (pairs, HOLogic_empty_set))
   1.230 -				end handle CANNOT_INTERPRET _ => None)
   1.231 +				end
   1.232  			| Type ("prop", [])      =>
   1.233  				(case index_from_interpretation intr of
   1.234  				  0 => Some (HOLogic.mk_Trueprop HOLogic.true_const)
   1.235 @@ -1768,7 +1743,7 @@
   1.236  	in
   1.237  		case typeof t of
   1.238  		  Some (Type ("set", [T])) =>
   1.239 -			(let
   1.240 +			let
   1.241  				(* create all constants of type 'T' *)
   1.242  				val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.243  				val constants = make_constants i
   1.244 @@ -1796,7 +1771,7 @@
   1.245  				val HOLogic_insert    = Const ("insert", T --> HOLogic_setT --> HOLogic_setT)
   1.246  			in
   1.247  				Some (foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) (HOLogic_empty_set, elements))
   1.248 -			end handle CANNOT_INTERPRET _ => None)
   1.249 +			end
   1.250  		| _ =>
   1.251  			None
   1.252  	end;
   1.253 @@ -1860,9 +1835,7 @@
   1.254  							product (map (fn d =>
   1.255  								let
   1.256  									val T         = typ_of_dtyp descr typ_assoc d
   1.257 -									val (i, _, _) =
   1.258 -										(interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.259 -										handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.260 +									val (i, _, _) = interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.261  					in
   1.262  						size_of_type i
   1.263  					end) ds)) xs)
   1.264 @@ -1875,9 +1848,7 @@
   1.265  					  | make_args n (d::ds) =
   1.266  						let
   1.267  							val dT        = typ_of_dtyp descr typ_assoc d
   1.268 -							val (i, _, _) =
   1.269 -								(interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", dT))
   1.270 -								handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
   1.271 +							val (i, _, _) = interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", dT))
   1.272  							val size      = size_of_type i
   1.273  							val consts    = make_constants i  (* we only need the (n mod size)-th element of *)
   1.274  								(* this list, so there might be a more efficient implementation that does not *)