1.1 --- a/src/HOL/Tools/refute.ML Wed May 26 17:43:52 2004 +0200
1.2 +++ b/src/HOL/Tools/refute.ML Wed May 26 18:03:52 2004 +0200
1.3 @@ -6,10 +6,7 @@
1.4 Finite model generation for HOL formulae, using a SAT solver.
1.5 *)
1.6
1.7 -(* ------------------------------------------------------------------------- *)
1.8 -(* TODO: Change parameter handling so that only supported parameters can be *)
1.9 -(* set, and specify defaults here, rather than in HOL/Main.thy. *)
1.10 -(* ------------------------------------------------------------------------- *)
1.11 +(* TODO: case, rec, size for IDTs are not supported yet *)
1.12
1.13 (* ------------------------------------------------------------------------- *)
1.14 (* Declares the 'REFUTE' signature as well as a structure 'Refute'. *)
1.15 @@ -22,22 +19,23 @@
1.16 exception REFUTE of string * string
1.17
1.18 (* ------------------------------------------------------------------------- *)
1.19 -(* Model/interpretation related code (translation HOL -> boolean formula) *)
1.20 +(* Model/interpretation related code (translation HOL -> propositional logic *)
1.21 (* ------------------------------------------------------------------------- *)
1.22
1.23 - exception CANNOT_INTERPRET
1.24 -
1.25 + type params
1.26 type interpretation
1.27 type model
1.28 type arguments
1.29
1.30 - val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory
1.31 - val add_printer : string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory
1.32 + exception CANNOT_INTERPRET of Term.term
1.33 + exception MAXVARS_EXCEEDED
1.34
1.35 - val interpret : theory -> model -> arguments -> Term.term -> interpretation * model * arguments (* exception CANNOT_INTERPRET *)
1.36 - val is_satisfying_model : model -> interpretation -> bool -> PropLogic.prop_formula
1.37 + val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory
1.38 + val add_printer : string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option) -> theory -> theory
1.39
1.40 - val print : theory -> model -> Term.term -> interpretation -> (int -> bool) -> string
1.41 + val interpret : theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) (* exception CANNOT_INTERPRET *)
1.42 +
1.43 + val print : theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term
1.44 val print_model : theory -> model -> (int -> bool) -> string
1.45
1.46 (* ------------------------------------------------------------------------- *)
1.47 @@ -47,9 +45,9 @@
1.48 val set_default_param : (string * string) -> theory -> theory
1.49 val get_default_param : theory -> string -> string option
1.50 val get_default_params : theory -> (string * string) list
1.51 - val actual_params : theory -> (string * string) list -> (int * int * int * string)
1.52 + val actual_params : theory -> (string * string) list -> params
1.53
1.54 - val find_model : theory -> (int * int * int * string) -> Term.term -> bool -> unit
1.55 + val find_model : theory -> params -> Term.term -> bool -> unit
1.56
1.57 val satisfy_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model for a formula *)
1.58 val refute_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model that refutes a formula *)
1.59 @@ -69,11 +67,11 @@
1.60 (* 'error'. *)
1.61 exception REFUTE of string * string; (* ("in function", "cause") *)
1.62
1.63 -(* ------------------------------------------------------------------------- *)
1.64 -(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *)
1.65 -(* ------------------------------------------------------------------------- *)
1.66 + exception CANNOT_INTERPRET of Term.term;
1.67
1.68 - exception CANNOT_INTERPRET;
1.69 + (* should be raised by an interpreter when more variables would be *)
1.70 + (* required than allowed by 'maxvars' *)
1.71 + exception MAXVARS_EXCEEDED;
1.72
1.73 (* ------------------------------------------------------------------------- *)
1.74 (* TREES *)
1.75 @@ -115,12 +113,43 @@
1.76 | Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)"))
1.77 | Node xs =>
1.78 (case t2 of
1.79 - (* '~~' will raise an exception if the number of branches in both trees is different at the current node *)
1.80 + (* '~~' will raise an exception if the number of branches in *)
1.81 + (* both trees is different at the current node *)
1.82 Node ys => Node (map tree_pair (xs ~~ ys))
1.83 | Leaf _ => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
1.84
1.85
1.86 (* ------------------------------------------------------------------------- *)
1.87 +(* params: parameters that control the translation into a propositional *)
1.88 +(* formula/model generation *)
1.89 +(* *)
1.90 +(* The following parameters are supported (and required (!), except for *)
1.91 +(* "sizes"): *)
1.92 +(* *)
1.93 +(* Name Type Description *)
1.94 +(* *)
1.95 +(* "sizes" (string * int) list *)
1.96 +(* Size of ground types (e.g. 'a=2), or depth of IDTs. *)
1.97 +(* "minsize" int If >0, minimal size of each ground type/IDT depth. *)
1.98 +(* "maxsize" int If >0, maximal size of each ground type/IDT depth. *)
1.99 +(* "maxvars" int If >0, use at most 'maxvars' Boolean variables *)
1.100 +(* when transforming the term into a propositional *)
1.101 +(* formula. *)
1.102 +(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *)
1.103 +(* "satsolver" string SAT solver to be used. *)
1.104 +(* ------------------------------------------------------------------------- *)
1.105 +
1.106 + type params =
1.107 + {
1.108 + sizes : (string * int) list,
1.109 + minsize : int,
1.110 + maxsize : int,
1.111 + maxvars : int,
1.112 + maxtime : int,
1.113 + satsolver: string
1.114 + };
1.115 +
1.116 +(* ------------------------------------------------------------------------- *)
1.117 (* interpretation: a term's interpretation is given by a variable of type *)
1.118 (* 'interpretation' *)
1.119 (* ------------------------------------------------------------------------- *)
1.120 @@ -139,9 +168,16 @@
1.121 (* ------------------------------------------------------------------------- *)
1.122 (* arguments: additional arguments required during interpretation of terms *)
1.123 (* ------------------------------------------------------------------------- *)
1.124 -
1.125 +
1.126 type arguments =
1.127 - {next_idx: int, bounds: interpretation list, wellformed: prop_formula};
1.128 + {
1.129 + (* just passed unchanged from 'params' *)
1.130 + maxvars : int,
1.131 + (* these may change during the translation *)
1.132 + next_idx : int,
1.133 + bounds : interpretation list,
1.134 + wellformed: prop_formula
1.135 + };
1.136
1.137
1.138 structure RefuteDataArgs =
1.139 @@ -149,7 +185,7 @@
1.140 val name = "HOL/refute";
1.141 type T =
1.142 {interpreters: (string * (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option)) list,
1.143 - printers: (string * (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option)) list,
1.144 + printers: (string * (theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option)) list,
1.145 parameters: string Symtab.table};
1.146 val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
1.147 val copy = I;
1.148 @@ -174,97 +210,62 @@
1.149 (* interpret: tries to interpret the term 't' using a suitable interpreter; *)
1.150 (* returns the interpretation and a (possibly extended) model *)
1.151 (* that keeps track of the interpretation of subterms *)
1.152 -(* Note: exception 'CANNOT_INTERPRETE' is raised if the term cannot be *)
1.153 +(* Note: exception 'CANNOT_INTERPRET t' is raised if the term cannot be *)
1.154 (* interpreted by any interpreter *)
1.155 (* ------------------------------------------------------------------------- *)
1.156
1.157 - (* theory -> model -> arguments -> Term.term -> interpretation * model * arguments *)
1.158 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) *)
1.159
1.160 fun interpret thy model args t =
1.161 (case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of
1.162 - None =>
1.163 - (std_output "\n"; warning ("Unable to interpret term:\n" ^ Sign.string_of_term (sign_of thy) t);
1.164 - raise CANNOT_INTERPRET)
1.165 + None => raise (CANNOT_INTERPRET t)
1.166 | Some x => x);
1.167
1.168 (* ------------------------------------------------------------------------- *)
1.169 -(* print: tries to print the constant denoted by the term 't' using a *)
1.170 -(* suitable printer *)
1.171 +(* print: tries to convert the constant denoted by the term 't' into a term *)
1.172 +(* using a suitable printer *)
1.173 (* ------------------------------------------------------------------------- *)
1.174
1.175 - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string *)
1.176 + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term *)
1.177
1.178 fun print thy model t intr assignment =
1.179 (case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) of
1.180 - None => "<<no printer available>>"
1.181 - | Some s => s);
1.182 -
1.183 -(* ------------------------------------------------------------------------- *)
1.184 -(* is_satisfying_model: returns a propositional formula that is true iff the *)
1.185 -(* given interpretation denotes 'satisfy', and the model meets certain *)
1.186 -(* well-formedness properties *)
1.187 -(* ------------------------------------------------------------------------- *)
1.188 -
1.189 - (* model -> interpretation -> bool -> PropLogic.prop_formula *)
1.190 -
1.191 - fun is_satisfying_model model intr satisfy =
1.192 - let
1.193 - (* prop_formula list -> prop_formula *)
1.194 - fun oneoutoftwofalse [] = True
1.195 - | oneoutoftwofalse (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), oneoutoftwofalse xs)
1.196 - (* prop_formula list -> prop_formula *)
1.197 - fun exactly1true xs = SAnd (PropLogic.exists xs, oneoutoftwofalse xs)
1.198 - (* ------------------------------------------------------------------------- *)
1.199 - (* restrict_to_single_element: returns a propositional formula that is true *)
1.200 - (* iff the interpretation denotes a single element of its corresponding *)
1.201 - (* type, i.e. iff at each leaf, one and only one formula is true *)
1.202 - (* ------------------------------------------------------------------------- *)
1.203 - (* interpretation -> prop_formula *)
1.204 - fun restrict_to_single_element (Leaf [BoolVar i, Not (BoolVar j)]) =
1.205 - if (i=j) then
1.206 - True (* optimization for boolean variables *)
1.207 - else
1.208 - raise REFUTE ("is_satisfying_model", "boolean variables in leaf have different indices")
1.209 - | restrict_to_single_element (Leaf xs) =
1.210 - exactly1true xs
1.211 - | restrict_to_single_element (Node trees) =
1.212 - PropLogic.all (map restrict_to_single_element trees)
1.213 - in
1.214 - (* a term of type 'bool' is represented as a 2-element leaf, where *)
1.215 - (* the term is true iff the leaf's first element is true, and false *)
1.216 - (* iff the leaf's second element is true *)
1.217 - case intr of
1.218 - Leaf [fmT,fmF] =>
1.219 - (* well-formedness properties and formula 'fmT'/'fmF' *)
1.220 - SAnd (PropLogic.all (map (restrict_to_single_element o snd) (snd model)), if satisfy then fmT else fmF)
1.221 - | _ =>
1.222 - raise REFUTE ("is_satisfying_model", "interpretation does not denote a boolean value")
1.223 - end;
1.224 + None => Const ("<<no printer available>>", fastype_of t)
1.225 + | Some x => x);
1.226
1.227 (* ------------------------------------------------------------------------- *)
1.228 (* print_model: turns the model into a string, using a fixed interpretation *)
1.229 -(* (given by an assignment for boolean variables) and suitable *)
1.230 +(* (given by an assignment for Boolean variables) and suitable *)
1.231 (* printers *)
1.232 (* ------------------------------------------------------------------------- *)
1.233
1.234 + (* theory -> model -> (int -> bool) -> string *)
1.235 +
1.236 fun print_model thy model assignment =
1.237 let
1.238 val (typs, terms) = model
1.239 + val typs_msg =
1.240 + if null typs then
1.241 + "empty universe (no type variables in term)\n"
1.242 + else
1.243 + "Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs) ^ "\n"
1.244 + val show_consts_msg =
1.245 + if not (!show_consts) andalso Library.exists (is_Const o fst) terms then
1.246 + "set \"show_consts\" to show the interpretation of constants\n"
1.247 + else
1.248 + ""
1.249 + val terms_msg =
1.250 + if null terms then
1.251 + "empty interpretation (no free variables in term)\n"
1.252 + else
1.253 + space_implode "\n" (mapfilter (fn (t,intr) =>
1.254 + (* print constants only if 'show_consts' is true *)
1.255 + if (!show_consts) orelse not (is_Const t) then
1.256 + Some (Sign.string_of_term (sign_of thy) t ^ ": " ^ Sign.string_of_term (sign_of thy) (print thy model t intr assignment))
1.257 + else
1.258 + None) terms) ^ "\n"
1.259 in
1.260 - (if null typs then
1.261 - "empty universe (no type variables in term)"
1.262 - else
1.263 - "Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs))
1.264 - ^ "\n"
1.265 - ^ (if null terms then
1.266 - "empty interpretation (no free variables in term)"
1.267 - else
1.268 - space_implode "\n" (map
1.269 - (fn (t,intr) =>
1.270 - Sign.string_of_term (sign_of thy) t ^ ": " ^ print thy model t intr assignment)
1.271 - terms)
1.272 - )
1.273 - ^ "\n"
1.274 + typs_msg ^ show_consts_msg ^ terms_msg
1.275 end;
1.276
1.277
1.278 @@ -283,7 +284,7 @@
1.279 | Some _ => error ("Interpreter " ^ name ^ " already declared")
1.280 end;
1.281
1.282 - (* string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory *)
1.283 + (* string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option) -> theory -> theory *)
1.284
1.285 fun add_printer name f thy =
1.286 let
1.287 @@ -333,25 +334,12 @@
1.288 (* ------------------------------------------------------------------------- *)
1.289 (* actual_params: takes a (possibly empty) list 'params' of parameters that *)
1.290 (* override the default parameters currently specified in 'thy', and *)
1.291 -(* returns a tuple that can be passed to 'find_model'. *)
1.292 -(* *)
1.293 -(* The following parameters are supported (and required!): *)
1.294 -(* *)
1.295 -(* Name Type Description *)
1.296 -(* *)
1.297 -(* "minsize" int Only search for models with size at least *)
1.298 -(* 'minsize'. *)
1.299 -(* "maxsize" int If >0, only search for models with size at most *)
1.300 -(* 'maxsize'. *)
1.301 -(* "maxvars" int If >0, use at most 'maxvars' boolean variables *)
1.302 -(* when transforming the term into a propositional *)
1.303 -(* formula. *)
1.304 -(* "satsolver" string SAT solver to be used. *)
1.305 +(* returns a record that can be passed to 'find_model'. *)
1.306 (* ------------------------------------------------------------------------- *)
1.307
1.308 - (* theory -> (string * string) list -> (int * int * int * string) *)
1.309 + (* theory -> (string * string) list -> params *)
1.310
1.311 - fun actual_params thy params =
1.312 + fun actual_params thy override =
1.313 let
1.314 (* (string * string) list * string -> int *)
1.315 fun read_int (parms, name) =
1.316 @@ -366,147 +354,591 @@
1.317 Some s => s
1.318 | None => error ("parameter " ^ quote name ^ " must be assigned a value")
1.319 (* (string * string) list *)
1.320 - val allparams = params @ (get_default_params thy) (* 'params' first, defaults last (to override) *)
1.321 + val allparams = override @ (get_default_params thy) (* 'override' first, defaults last *)
1.322 (* int *)
1.323 val minsize = read_int (allparams, "minsize")
1.324 val maxsize = read_int (allparams, "maxsize")
1.325 val maxvars = read_int (allparams, "maxvars")
1.326 + val maxtime = read_int (allparams, "maxtime")
1.327 (* string *)
1.328 val satsolver = read_string (allparams, "satsolver")
1.329 + (* all remaining parameters of the form "string=int" are collected in *)
1.330 + (* 'sizes' *)
1.331 + (* TODO: it is currently not possible to specify a size for a type *)
1.332 + (* whose name is one of the other parameters (e.g. 'maxvars') *)
1.333 + (* (string * int) list *)
1.334 + val sizes = mapfilter
1.335 + (fn (name,value) => (case Int.fromString value of SOME i => Some (name, i) | NONE => None))
1.336 + (filter (fn (name,_) => name<>"minsize" andalso name<>"maxsize" andalso name<>"maxvars" andalso name<>"maxtime" andalso name<>"satsolver")
1.337 + allparams)
1.338 in
1.339 - (minsize, maxsize, maxvars, satsolver)
1.340 + {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars, maxtime=maxtime, satsolver=satsolver}
1.341 + end;
1.342 +
1.343 +
1.344 +(* ------------------------------------------------------------------------- *)
1.345 +(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *)
1.346 +(* ------------------------------------------------------------------------- *)
1.347 +
1.348 +(* ------------------------------------------------------------------------- *)
1.349 +(* collect_axioms: collects (monomorphic, universally quantified versions *)
1.350 +(* of) all HOL axioms that are relevant w.r.t 't' *)
1.351 +(* ------------------------------------------------------------------------- *)
1.352 +
1.353 + (* TODO: to make the collection of axioms more easily extensible, this *)
1.354 + (* function could be based on user-supplied "axiom collectors", *)
1.355 + (* similar to 'interpret'/interpreters or 'print'/printers *)
1.356 +
1.357 + (* theory -> Term.term -> Term.term list *)
1.358 +
1.359 + (* Which axioms are "relevant" for a particular term/type goes hand in *)
1.360 + (* hand with the interpretation of that term/type by its interpreter (see *)
1.361 + (* way below): if the interpretation respects an axiom anyway, the axiom *)
1.362 + (* does not need to be added as a constraint here. *)
1.363 +
1.364 + (* When an axiom is added as relevant, further axioms may need to be *)
1.365 + (* added as well (e.g. when a constant is defined in terms of other *)
1.366 + (* constants). To avoid infinite recursion (which should not happen for *)
1.367 + (* constants anyway, but it could happen for "typedef"-related axioms, *)
1.368 + (* since they contain the type again), we use an accumulator 'axs' and *)
1.369 + (* add a relevant axiom only if it is not in 'axs' yet. *)
1.370 +
1.371 + fun collect_axioms thy t =
1.372 + let
1.373 + val _ = std_output "Adding axioms..."
1.374 + (* (string * Term.term) list *)
1.375 + val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
1.376 + (* given a constant 's' of type 'T', which is a subterm of 't', where *)
1.377 + (* 't' has a (possibly) more general type, the schematic type *)
1.378 + (* variables in 't' are instantiated to match the type 'T' *)
1.379 + (* (string * Term.typ) * Term.term -> Term.term *)
1.380 + fun specialize_type ((s, T), t) =
1.381 + let
1.382 + fun find_typeSubs (Const (s', T')) =
1.383 + (if s=s' then
1.384 + Some (Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T)))
1.385 + else
1.386 + None
1.387 + handle Type.TYPE_MATCH => None)
1.388 + | find_typeSubs (Free _) = None
1.389 + | find_typeSubs (Var _) = None
1.390 + | find_typeSubs (Bound _) = None
1.391 + | find_typeSubs (Abs (_, _, body)) = find_typeSubs body
1.392 + | find_typeSubs (t1 $ t2) = (case find_typeSubs t1 of Some x => Some x | None => find_typeSubs t2)
1.393 + val typeSubs = (case find_typeSubs t of
1.394 + Some x => x
1.395 + | None => raise REFUTE ("collect_axioms", "no type instantiation found for " ^ quote s ^ " in " ^ Sign.string_of_term (sign_of thy) t))
1.396 + in
1.397 + map_term_types
1.398 + (map_type_tvar
1.399 + (fn (v,_) =>
1.400 + case Vartab.lookup (typeSubs, v) of
1.401 + None =>
1.402 + (* schematic type variable not instantiated *)
1.403 + raise REFUTE ("collect_axioms", "term " ^ Sign.string_of_term (sign_of thy) t ^ " still has a polymorphic type (after instantiating type of " ^ quote s ^ ")")
1.404 + | Some typ =>
1.405 + typ))
1.406 + t
1.407 + end
1.408 + (* Term.term list * Term.typ -> Term.term list *)
1.409 + fun collect_type_axioms (axs, T) =
1.410 + case T of
1.411 + (* simple types *)
1.412 + Type ("prop", []) => axs
1.413 + | Type ("fun", [T1, T2]) => collect_type_axioms (collect_type_axioms (axs, T1), T2)
1.414 + | Type ("set", [T1]) => collect_type_axioms (axs, T1)
1.415 + | Type (s, Ts) =>
1.416 + let
1.417 + (* look up the definition of a type, as created by "typedef" *)
1.418 + (* (string * Term.term) list -> (string * Term.term) option *)
1.419 + fun get_typedefn [] =
1.420 + None
1.421 + | get_typedefn ((axname,ax)::axms) =
1.422 + (let
1.423 + (* Term.term -> Term.typ option *)
1.424 + fun type_of_type_definition (Const (s', T')) =
1.425 + if s'="Typedef.type_definition" then
1.426 + Some T'
1.427 + else
1.428 + None
1.429 + | type_of_type_definition (Free _) = None
1.430 + | type_of_type_definition (Var _) = None
1.431 + | type_of_type_definition (Bound _) = None
1.432 + | type_of_type_definition (Abs (_, _, body)) = type_of_type_definition body
1.433 + | type_of_type_definition (t1 $ t2) = (case type_of_type_definition t1 of Some x => Some x | None => type_of_type_definition t2)
1.434 + in
1.435 + case type_of_type_definition ax of
1.436 + Some T' =>
1.437 + let
1.438 + val T'' = (domain_type o domain_type) T'
1.439 + val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T'', T))
1.440 + val unvar_ax = map_term_types
1.441 + (map_type_tvar
1.442 + (fn (v,_) =>
1.443 + case Vartab.lookup (typeSubs, v) of
1.444 + None =>
1.445 + (* schematic type variable not instantiated *)
1.446 + raise ERROR
1.447 + | Some typ =>
1.448 + typ))
1.449 + ax
1.450 + in
1.451 + Some (axname, unvar_ax)
1.452 + end
1.453 + | None =>
1.454 + get_typedefn axms
1.455 + end
1.456 + handle ERROR => get_typedefn axms
1.457 + | MATCH => get_typedefn axms
1.458 + | Type.TYPE_MATCH => get_typedefn axms)
1.459 + in
1.460 + case DatatypePackage.datatype_info thy s of
1.461 + Some info => (* inductive datatype *)
1.462 + (* only collect relevant type axioms for the argument types *)
1.463 + foldl collect_type_axioms (axs, Ts)
1.464 + | None =>
1.465 + (case get_typedefn axioms of
1.466 + Some (axname, ax) =>
1.467 + if mem_term (ax, axs) then
1.468 + (* collect relevant type axioms for the argument types *)
1.469 + foldl collect_type_axioms (axs, Ts)
1.470 + else
1.471 + (std_output (" " ^ axname);
1.472 + collect_term_axioms (ax :: axs, ax))
1.473 + | None =>
1.474 + (* at least collect relevant type axioms for the argument types *)
1.475 + foldl collect_type_axioms (axs, Ts))
1.476 + end
1.477 + (* TODO: include sort axioms *)
1.478 + | TFree (_, sorts) => ((*if not (null sorts) then std_output " *ignoring sorts*" else ();*) axs)
1.479 + | TVar (_, sorts) => ((*if not (null sorts) then std_output " *ignoring sorts*" else ();*) axs)
1.480 + (* Term.term list * Term.term -> Term.term list *)
1.481 + and collect_term_axioms (axs, t) =
1.482 + case t of
1.483 + (* Pure *)
1.484 + Const ("all", _) => axs
1.485 + | Const ("==", _) => axs
1.486 + | Const ("==>", _) => axs
1.487 + (* HOL *)
1.488 + | Const ("Trueprop", _) => axs
1.489 + | Const ("Not", _) => axs
1.490 + | Const ("True", _) => axs (* redundant, since 'True' is also an IDT constructor *)
1.491 + | Const ("False", _) => axs (* redundant, since 'False' is also an IDT constructor *)
1.492 + | Const ("arbitrary", T) => collect_type_axioms (axs, T)
1.493 + | Const ("The", T) =>
1.494 + let
1.495 + val ax = specialize_type (("The", T), (the o assoc) (axioms, "HOL.the_eq_trivial"))
1.496 + in
1.497 + if mem_term (ax, axs) then
1.498 + collect_type_axioms (axs, T)
1.499 + else
1.500 + (std_output " HOL.the_eq_trivial";
1.501 + collect_term_axioms (ax :: axs, ax))
1.502 + end
1.503 + | Const ("Hilbert_Choice.Eps", T) =>
1.504 + let
1.505 + val ax = specialize_type (("Hilbert_Choice.Eps", T), (the o assoc) (axioms, "Hilbert_Choice.someI"))
1.506 + in
1.507 + if mem_term (ax, axs) then
1.508 + collect_type_axioms (axs, T)
1.509 + else
1.510 + (std_output " Hilbert_Choice.someI";
1.511 + collect_term_axioms (ax :: axs, ax))
1.512 + end
1.513 + | Const ("All", _) $ t1 => collect_term_axioms (axs, t1)
1.514 + | Const ("Ex", _) $ t1 => collect_term_axioms (axs, t1)
1.515 + | Const ("op =", T) => collect_type_axioms (axs, T)
1.516 + | Const ("op &", _) => axs
1.517 + | Const ("op |", _) => axs
1.518 + | Const ("op -->", _) => axs
1.519 + (* sets *)
1.520 + | Const ("Collect", T) => collect_type_axioms (axs, T)
1.521 + | Const ("op :", T) => collect_type_axioms (axs, T)
1.522 + (* other optimizations *)
1.523 + | Const ("Finite_Set.card", T) => collect_type_axioms (axs, T)
1.524 + (* simply-typed lambda calculus *)
1.525 + | Const (s, T) =>
1.526 + let
1.527 + (* look up the definition of a constant, as created by "constdefs" *)
1.528 + (* string -> Term.typ -> (string * Term.term) list -> (string * Term.term) option *)
1.529 + fun get_defn [] =
1.530 + None
1.531 + | get_defn ((axname,ax)::axms) =
1.532 + (let
1.533 + val (lhs, _) = Logic.dest_equals ax (* equations only *)
1.534 + val c = head_of lhs
1.535 + val (s', T') = dest_Const c
1.536 + in
1.537 + if s=s' then
1.538 + let
1.539 + val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))
1.540 + val unvar_ax = map_term_types
1.541 + (map_type_tvar
1.542 + (fn (v,_) =>
1.543 + case Vartab.lookup (typeSubs, v) of
1.544 + None =>
1.545 + (* schematic type variable not instantiated *)
1.546 + raise ERROR
1.547 + | Some typ =>
1.548 + typ))
1.549 + ax
1.550 + in
1.551 + Some (axname, unvar_ax)
1.552 + end
1.553 + else
1.554 + get_defn axms
1.555 + end
1.556 + handle ERROR => get_defn axms
1.557 + | TERM _ => get_defn axms
1.558 + | Type.TYPE_MATCH => get_defn axms)
1.559 + (* unit -> bool *)
1.560 + fun is_IDT_constructor () =
1.561 + (case body_type T of
1.562 + Type (s', _) =>
1.563 + (case DatatypePackage.constrs_of thy s' of
1.564 + Some constrs =>
1.565 + Library.exists (fn c =>
1.566 + (case c of
1.567 + Const (cname, ctype) =>
1.568 + cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy), T, ctype)
1.569 + | _ =>
1.570 + raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
1.571 + constrs
1.572 + | None =>
1.573 + false)
1.574 + | _ =>
1.575 + false)
1.576 + (* unit -> bool *)
1.577 + fun is_IDT_recursor () =
1.578 + (* the type of a recursion operator: [T1,...,Tn,IDT]--->TResult (where *)
1.579 + (* the T1,...,Tn depend on the types of the datatype's constructors) *)
1.580 + ((case last_elem (binder_types T) of
1.581 + Type (s', _) =>
1.582 + (case DatatypePackage.datatype_info thy s' of
1.583 + Some info =>
1.584 + (* TODO: I'm not quite sute if comparing the names is sufficient, or if *)
1.585 + (* we should also check the type *)
1.586 + s mem (#rec_names info)
1.587 + | None => (* not an inductive datatype *)
1.588 + false)
1.589 + | _ => (* a (free or schematic) type variable *)
1.590 + false)
1.591 + handle LIST "last_elem" => false) (* not even a function type *)
1.592 + in
1.593 + if is_IDT_constructor () orelse is_IDT_recursor () then
1.594 + (* only collect relevant type axioms *)
1.595 + collect_type_axioms (axs, T)
1.596 + else
1.597 + (case get_defn axioms of
1.598 + Some (axname, ax) =>
1.599 + if mem_term (ax, axs) then
1.600 + (* collect relevant type axioms *)
1.601 + collect_type_axioms (axs, T)
1.602 + else
1.603 + (std_output (" " ^ axname);
1.604 + collect_term_axioms (ax :: axs, ax))
1.605 + | None =>
1.606 + (* collect relevant type axioms *)
1.607 + collect_type_axioms (axs, T))
1.608 + end
1.609 + | Free (_, T) => collect_type_axioms (axs, T)
1.610 + | Var (_, T) => collect_type_axioms (axs, T)
1.611 + | Bound i => axs
1.612 + | Abs (_, T, body) => collect_term_axioms (collect_type_axioms (axs, T), body)
1.613 + | t1 $ t2 => collect_term_axioms (collect_term_axioms (axs, t1), t2)
1.614 + (* universal closure over schematic variables *)
1.615 + (* Term.term -> Term.term *)
1.616 + fun close_form t =
1.617 + let
1.618 + (* (Term.indexname * Term.typ) list *)
1.619 + val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
1.620 + in
1.621 + foldl
1.622 + (fn (t', ((x,i),T)) => (Term.all T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
1.623 + (t, vars)
1.624 + end
1.625 + (* Term.term list *)
1.626 + val result = map close_form (collect_term_axioms ([], t))
1.627 + val _ = writeln " ...done."
1.628 + in
1.629 + result
1.630 end;
1.631
1.632 (* ------------------------------------------------------------------------- *)
1.633 -(* find_model: repeatedly calls 'invoke_propgen' with appropriate *)
1.634 -(* parameters, applies the SAT solver, and (in case a model is *)
1.635 -(* found) displays the model to the user *)
1.636 -(* thy : the current theory *)
1.637 -(* minsize : the minimal size of the model *)
1.638 -(* maxsize : the maximal size of the model *)
1.639 -(* maxvars : the maximal number of boolean variables to be used *)
1.640 -(* satsolver: the name of the SAT solver to be used *)
1.641 -(* satisfy : if 'True', search for a model that makes 't' true; otherwise *)
1.642 -(* search for a model that makes 't' false *)
1.643 +(* ground_types: collects all ground types in a term (including argument *)
1.644 +(* types of other types), suppressing duplicates. Does not *)
1.645 +(* return function types, set types, non-recursive IDTs, or *)
1.646 +(* 'propT'. For IDTs, also the argument types of constructors *)
1.647 +(* are considered. *)
1.648 +(* ------------------------------------------------------------------------- *)
1.649 +
1.650 + (* theory -> Term.term -> Term.typ list *)
1.651 +
1.652 + fun ground_types thy t =
1.653 + let
1.654 + (* Term.typ * Term.typ list -> Term.typ list *)
1.655 + fun collect_types (T, acc) =
1.656 + if T mem acc then
1.657 + acc (* prevent infinite recursion (for IDTs) *)
1.658 + else
1.659 + (case T of
1.660 + Type ("fun", [T1, T2]) => collect_types (T1, collect_types (T2, acc))
1.661 + | Type ("prop", []) => acc
1.662 + | Type ("set", [T1]) => collect_types (T1, acc)
1.663 + | Type (s, Ts) =>
1.664 + (case DatatypePackage.datatype_info thy s of
1.665 + Some info => (* inductive datatype *)
1.666 + let
1.667 + val index = #index info
1.668 + val descr = #descr info
1.669 + val (_, dtyps, constrs) = (the o assoc) (descr, index)
1.670 + val typ_assoc = dtyps ~~ Ts
1.671 + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
1.672 + val _ = (if Library.exists (fn d =>
1.673 + case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
1.674 + then
1.675 + raise REFUTE ("ground_types", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable")
1.676 + else
1.677 + ())
1.678 + (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
1.679 + fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
1.680 + (* replace a 'DtTFree' variable by the associated type *)
1.681 + (the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
1.682 + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
1.683 + let
1.684 + val (s, ds, _) = (the o assoc) (descr, i)
1.685 + in
1.686 + Type (s, map (typ_of_dtyp descr typ_assoc) ds)
1.687 + end
1.688 + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
1.689 + Type (s, map (typ_of_dtyp descr typ_assoc) ds)
1.690 + (* if the current type is a recursive IDT (i.e. a depth is required), add it to 'acc' *)
1.691 + val acc' = (if Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
1.692 + T ins acc
1.693 + else
1.694 + acc)
1.695 + (* collect argument types *)
1.696 + val acc_args = foldr collect_types (Ts, acc')
1.697 + (* collect constructor types *)
1.698 + val acc_constrs = foldr collect_types (flat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs), acc_args)
1.699 + in
1.700 + acc_constrs
1.701 + end
1.702 + | None => (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *)
1.703 + T ins (foldr collect_types (Ts, acc)))
1.704 + | TFree _ => T ins acc
1.705 + | TVar _ => T ins acc)
1.706 + in
1.707 + it_term_types collect_types (t, [])
1.708 + end;
1.709 +
1.710 +(* ------------------------------------------------------------------------- *)
1.711 +(* string_of_typ: (rather naive) conversion from types to strings, used to *)
1.712 +(* look up the size of a type in 'sizes'. Parameterized *)
1.713 +(* types with different parameters (e.g. "'a list" vs. "bool *)
1.714 +(* list") are identified. *)
1.715 +(* ------------------------------------------------------------------------- *)
1.716 +
1.717 + (* Term.typ -> string *)
1.718 +
1.719 + fun string_of_typ (Type (s, _)) = s
1.720 + | string_of_typ (TFree (s, _)) = s
1.721 + | string_of_typ (TVar ((s,_), _)) = s;
1.722 +
1.723 +(* ------------------------------------------------------------------------- *)
1.724 +(* first_universe: returns the "first" (i.e. smallest) universe by assigning *)
1.725 +(* 'minsize' to every type for which no size is specified in *)
1.726 +(* 'sizes' *)
1.727 +(* ------------------------------------------------------------------------- *)
1.728 +
1.729 + (* Term.typ list -> (string * int) list -> int -> (Term.typ * int) list *)
1.730 +
1.731 + fun first_universe xs sizes minsize =
1.732 + let
1.733 + fun size_of_typ T =
1.734 + case assoc (sizes, string_of_typ T) of
1.735 + Some n => n
1.736 + | None => minsize
1.737 + in
1.738 + map (fn T => (T, size_of_typ T)) xs
1.739 + end;
1.740 +
1.741 +(* ------------------------------------------------------------------------- *)
1.742 +(* next_universe: enumerates all universes (i.e. assignments of sizes to *)
1.743 +(* types), where the minimal size of a type is given by *)
1.744 +(* 'minsize', the maximal size is given by 'maxsize', and a *)
1.745 +(* type may have a fixed size given in 'sizes' *)
1.746 (* ------------------------------------------------------------------------- *)
1.747
1.748 - (* theory -> (int * int * int * string) -> Term.term -> bool -> unit *)
1.749 + (* (Term.typ * int) list -> (string * int) list -> int -> int -> (Term.typ * int) list option *)
1.750
1.751 - fun find_model thy (minsize, maxsize, maxvars, satsolver) t satisfy =
1.752 + fun next_universe xs sizes minsize maxsize =
1.753 let
1.754 - (* Term.typ list *)
1.755 - val tvars = map (fn (i,s) => TVar(i,s)) (term_tvars t)
1.756 - val tfrees = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
1.757 - (* int -> unit *)
1.758 - fun find_model_loop size =
1.759 - (* 'maxsize=0' means "search for arbitrary large models" *)
1.760 - if size>maxsize andalso maxsize<>0 then
1.761 - writeln ("Search terminated: maxsize=" ^ string_of_int maxsize ^ " exceeded.")
1.762 + (* int -> int list -> int list option *)
1.763 + fun add1 _ [] =
1.764 + None (* overflow *)
1.765 + | add1 max (x::xs) =
1.766 + if x<max orelse max<0 then
1.767 + Some ((x+1)::xs) (* add 1 to the head *)
1.768 + else
1.769 + apsome (fn xs' => 0 :: xs') (add1 max xs) (* carry-over *)
1.770 + (* int -> int list * int list -> int list option *)
1.771 + fun shift _ (_, []) =
1.772 + None
1.773 + | shift max (zeros, x::xs) =
1.774 + if x=0 then
1.775 + shift max (0::zeros, xs)
1.776 else
1.777 - let
1.778 - (* ------------------------------------------------------------------------- *)
1.779 - (* make_universes: given a list 'xs' of "types" and a universe size 'size', *)
1.780 - (* this function returns all possible partitions of the universe into *)
1.781 - (* the "types" in 'xs' such that no "type" is empty. If 'size' is less *)
1.782 - (* than 'length xs', the returned list of partitions is empty. *)
1.783 - (* Otherwise, if the list 'xs' is empty, then the returned list of *)
1.784 - (* partitions contains only the empty list, regardless of 'size'. *)
1.785 - (* ------------------------------------------------------------------------- *)
1.786 - (* 'a list -> int -> ('a * int) list list *)
1.787 - fun make_universes xs size =
1.788 + apsome (fn xs' => (x-1) :: (zeros @ xs')) (add1 max xs)
1.789 + (* creates the "first" list of length 'len', where the sum of all list *)
1.790 + (* elements is 'sum', and the length of the list is 'len' *)
1.791 + (* int -> int -> int -> int list option *)
1.792 + fun make_first 0 sum _ =
1.793 + if sum=0 then
1.794 + Some []
1.795 + else
1.796 + None
1.797 + | make_first len sum max =
1.798 + if sum<=max orelse max<0 then
1.799 + apsome (fn xs' => sum :: xs') (make_first (len-1) 0 max)
1.800 + else
1.801 + apsome (fn xs' => max :: xs') (make_first (len-1) (sum-max) max)
1.802 + (* enumerates all int lists with a fixed length, where 0<=x<='max' for *)
1.803 + (* all list elements x (unless 'max'<0) *)
1.804 + (* int -> int list -> int list option *)
1.805 + fun next max xs =
1.806 + (case shift max ([], xs) of
1.807 + Some xs' =>
1.808 + Some xs'
1.809 + | None =>
1.810 let
1.811 - (* 'a list -> int -> int -> ('a * int) list list *)
1.812 - fun make_partitions_loop (x::xs) 0 total =
1.813 - map (fn us => ((x,0)::us)) (make_partitions xs total)
1.814 - | make_partitions_loop (x::xs) first total =
1.815 - (map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
1.816 - | make_partitions_loop _ _ _ =
1.817 - raise REFUTE ("find_model", "empty list (in make_partitions_loop)")
1.818 - and
1.819 - (* 'a list -> int -> ('a * int) list list *)
1.820 - make_partitions [x] size =
1.821 - (* we must use all remaining elements on the type 'x', so there is only one partition *)
1.822 - [[(x,size)]]
1.823 - | make_partitions (x::xs) 0 =
1.824 - (* there are no elements left in the universe, so there is only one partition *)
1.825 - [map (fn t => (t,0)) (x::xs)]
1.826 - | make_partitions (x::xs) size =
1.827 - (* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
1.828 - make_partitions_loop (x::xs) size size
1.829 - | make_partitions _ _ =
1.830 - raise REFUTE ("find_model", "empty list (in make_partitions)")
1.831 - val len = length xs
1.832 + val (len, sum) = foldl (fn ((l, s), x) => (l+1, s+x)) ((0, 0), xs)
1.833 in
1.834 - if size<len then
1.835 - (* the universe isn't big enough to make every type non-empty *)
1.836 - []
1.837 - else if xs=[] then
1.838 - (* no types: return one universe, regardless of the size *)
1.839 - [[]]
1.840 - else
1.841 - (* partition into possibly empty types, then add 1 element to each type *)
1.842 - map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
1.843 - end
1.844 - (* ('a * int) list -> bool *)
1.845 - fun find_interpretation xs =
1.846 - let
1.847 - val init_model = (xs, [])
1.848 - val init_args = {next_idx = 1, bounds = [], wellformed = True}
1.849 - val (intr, model, args) = interpret thy init_model init_args t
1.850 - val fm = SAnd (#wellformed args, is_satisfying_model model intr satisfy)
1.851 - val usedvars = maxidx fm
1.852 - in
1.853 - (* 'maxvars=0' means "use as many variables as necessary" *)
1.854 - if usedvars>maxvars andalso maxvars<>0 then
1.855 - (writeln ("\nSearch terminated: " ^ string_of_int usedvars ^ " boolean variables used (only " ^ string_of_int maxvars ^ " allowed).");
1.856 - true)
1.857 - else
1.858 - (
1.859 - std_output " invoking SAT solver...";
1.860 - case SatSolver.invoke_solver satsolver fm of
1.861 - None =>
1.862 - (std_output (" error: SAT solver " ^ quote satsolver ^ " not configured.\n");
1.863 - true)
1.864 - | Some None =>
1.865 - (std_output " no model found.\n";
1.866 - false)
1.867 - | Some (Some assignment) =>
1.868 - (writeln ("\nModel found:\n" ^ print_model thy model assignment);
1.869 - true)
1.870 - )
1.871 - end handle CANNOT_INTERPRET => true
1.872 - (* TODO: change this to false once the ability to interpret terms depends on the universe *)
1.873 + make_first len (sum+1) max (* increment 'sum' by 1 *)
1.874 + end)
1.875 + (* only consider those types for which the size is not fixed *)
1.876 + val mutables = filter (fn (T, _) => assoc (sizes, string_of_typ T) = None) xs
1.877 + (* subtract 'minsize' from every size (will be added again at the end) *)
1.878 + val diffs = map (fn (_, n) => n-minsize) mutables
1.879 + in
1.880 + case next (maxsize-minsize) diffs of
1.881 + Some diffs' =>
1.882 + (* merge with those types for which the size is fixed *)
1.883 + Some (snd (foldl_map (fn (ds, (T, _)) =>
1.884 + case assoc (sizes, string_of_typ T) of
1.885 + Some n => (ds, (T, n)) (* return the fixed size *)
1.886 + | None => (tl ds, (T, minsize + (hd ds)))) (* consume the head of 'ds', add 'minsize' *)
1.887 + (diffs', xs)))
1.888 + | None =>
1.889 + None
1.890 + end;
1.891 +
1.892 +(* ------------------------------------------------------------------------- *)
1.893 +(* toTrue: converts the interpretation of a Boolean value to a propositional *)
1.894 +(* formula that is true iff the interpretation denotes "true" *)
1.895 +(* ------------------------------------------------------------------------- *)
1.896 +
1.897 + (* interpretation -> prop_formula *)
1.898 +
1.899 + fun toTrue (Leaf [fm,_]) = fm
1.900 + | toTrue _ = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value");
1.901 +
1.902 +(* ------------------------------------------------------------------------- *)
1.903 +(* toFalse: converts the interpretation of a Boolean value to a *)
1.904 +(* propositional formula that is true iff the interpretation *)
1.905 +(* denotes "false" *)
1.906 +(* ------------------------------------------------------------------------- *)
1.907 +
1.908 + (* interpretation -> prop_formula *)
1.909 +
1.910 + fun toFalse (Leaf [_,fm]) = fm
1.911 + | toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value");
1.912 +
1.913 +(* ------------------------------------------------------------------------- *)
1.914 +(* find_model: repeatedly calls 'interpret' with appropriate parameters, *)
1.915 +(* applies a SAT solver, and (in case a model is found) displays *)
1.916 +(* the model to the user by calling 'print_model' *)
1.917 +(* thy : the current theory *)
1.918 +(* {...} : parameters that control the translation/model generation *)
1.919 +(* t : term to be translated into a propositional formula *)
1.920 +(* negate : if true, find a model that makes 't' false (rather than true) *)
1.921 +(* Note: exception 'TimeOut' is raised if the algorithm does not terminate *)
1.922 +(* within 'maxtime' seconds (if 'maxtime' >0) *)
1.923 +(* ------------------------------------------------------------------------- *)
1.924 +
1.925 + (* theory -> params -> Term.term -> bool -> unit *)
1.926 +
1.927 + fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver} t negate =
1.928 + let
1.929 + (* unit -> unit *)
1.930 + fun wrapper () =
1.931 + let
1.932 + (* Term.term list *)
1.933 + val axioms = collect_axioms thy t
1.934 + (* Term.typ list *)
1.935 + val types = foldl (fn (acc, t') => acc union (ground_types thy t')) ([], t :: axioms)
1.936 + val _ = writeln ("Ground types: "
1.937 + ^ (if null types then "none."
1.938 + else commas (map (Sign.string_of_typ (sign_of thy)) types)))
1.939 + (* (Term.typ * int) list -> unit *)
1.940 + fun find_model_loop universe =
1.941 + (let
1.942 + val init_model = (universe, [])
1.943 + val init_args = {maxvars = maxvars, next_idx = 1, bounds = [], wellformed = True}
1.944 + val _ = std_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
1.945 + (* translate 't' and all axioms *)
1.946 + val ((model, args), intrs) = foldl_map (fn ((m, a), t') =>
1.947 + let
1.948 + val (i, m', a') = interpret thy m a t'
1.949 + in
1.950 + ((m', a'), i)
1.951 + end) ((init_model, init_args), t :: axioms)
1.952 + (* make 't' either true or false, and make all axioms true, and *)
1.953 + (* add the well-formedness side condition *)
1.954 + val fm_t = (if negate then toFalse else toTrue) (hd intrs)
1.955 + val fm_ax = PropLogic.all (map toTrue (tl intrs))
1.956 + val fm = PropLogic.all [#wellformed args, fm_ax, fm_t]
1.957 in
1.958 - case make_universes (tvars@tfrees) size of
1.959 - [] =>
1.960 - (writeln ("Searching for a model of size " ^ string_of_int size ^ ": cannot make every type non-empty (model is too small).");
1.961 - find_model_loop (size+1))
1.962 - | [[]] =>
1.963 - (std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term...");
1.964 - if find_interpretation [] then
1.965 - ()
1.966 - else
1.967 - writeln ("Search terminated: no type variables in term."))
1.968 - | us =>
1.969 - let
1.970 - fun loop [] =
1.971 - find_model_loop (size+1)
1.972 - | loop (u::us) =
1.973 - (std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term...");
1.974 - if find_interpretation u then () else loop us)
1.975 - in
1.976 - loop us
1.977 - end
1.978 + std_output " invoking SAT solver...";
1.979 + case SatSolver.invoke_solver satsolver fm of
1.980 + None =>
1.981 + error ("SAT solver " ^ quote satsolver ^ " not configured.")
1.982 + | Some None =>
1.983 + (std_output " no model found.\n";
1.984 + case next_universe universe sizes minsize maxsize of
1.985 + Some universe' => find_model_loop universe'
1.986 + | None => writeln "Search terminated, no larger universe within the given limits.")
1.987 + | Some (Some assignment) =>
1.988 + writeln ("\n*** Model found: ***\n" ^ print_model thy model assignment)
1.989 + end handle MAXVARS_EXCEEDED =>
1.990 + writeln ("\nSearch terminated, number of Boolean variables (" ^ string_of_int maxvars ^ " allowed) exceeded.")
1.991 + | CANNOT_INTERPRET t' =>
1.992 + error ("Unable to interpret term " ^ Sign.string_of_term (sign_of thy) t'))
1.993 + in
1.994 + find_model_loop (first_universe types sizes minsize)
1.995 end
1.996 - in
1.997 - writeln ("Trying to find a model that "
1.998 - ^ (if satisfy then "satisfies" else "refutes")
1.999 - ^ ": " ^ (Sign.string_of_term (sign_of thy) t));
1.1000 - if minsize<1 then
1.1001 - writeln "\"minsize\" is less than 1; starting search with size 1."
1.1002 - else ();
1.1003 - find_model_loop (Int.max (minsize,1))
1.1004 - end;
1.1005 + in
1.1006 + (* some parameter sanity checks *)
1.1007 + assert (minsize>=1) ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1");
1.1008 + assert (maxsize>=1) ("\"maxsize\" is " ^ string_of_int maxsize ^ ", must be at least 1");
1.1009 + assert (maxsize>=minsize) ("\"maxsize\" (=" ^ string_of_int maxsize ^ ") is less than \"minsize\" (=" ^ string_of_int minsize ^ ").");
1.1010 + assert (maxvars>=0) ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0");
1.1011 + assert (maxtime>=0) ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
1.1012 + (* enter loop with/without time limit *)
1.1013 + writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": "
1.1014 + ^ Sign.string_of_term (sign_of thy) t);
1.1015 + if maxtime>0 then
1.1016 + (* TODO: this only works with SML/NJ *)
1.1017 + ((*TimeLimit.timeLimit (Time.fromSeconds (Int32.fromInt maxtime))*)
1.1018 + wrapper ()
1.1019 + (*handle TimeLimit.TimeOut =>
1.1020 + writeln ("\nSearch terminated, time limit ("
1.1021 + ^ string_of_int maxtime ^ " second"
1.1022 + ^ (if maxtime=1 then "" else "s")
1.1023 + ^ ") exceeded.")*))
1.1024 + else
1.1025 + wrapper ()
1.1026 + end;
1.1027
1.1028
1.1029 (* ------------------------------------------------------------------------- *)
1.1030 @@ -522,7 +954,7 @@
1.1031 (* theory -> (string * string) list -> Term.term -> unit *)
1.1032
1.1033 fun satisfy_term thy params t =
1.1034 - find_model thy (actual_params thy params) t true;
1.1035 + find_model thy (actual_params thy params) t false;
1.1036
1.1037 (* ------------------------------------------------------------------------- *)
1.1038 (* refute_term: calls 'find_model' to find a model that refutes 't' *)
1.1039 @@ -534,7 +966,10 @@
1.1040
1.1041 fun refute_term thy params t =
1.1042 let
1.1043 - (* disallow schematic type variables, since we cannot properly negate terms containing them *)
1.1044 + (* disallow schematic type variables, since we cannot properly negate *)
1.1045 + (* terms containing them (their logical meaning is that there EXISTS a *)
1.1046 + (* type s.t. ...; to refute such a formula, we would have to show that *)
1.1047 + (* for ALL types, not ...) *)
1.1048 val _ = assert (null (term_tvars t)) "Term to be refuted contains schematic type variables"
1.1049 (* existential closure over schematic variables *)
1.1050 (* (Term.indexname * Term.typ) list *)
1.1051 @@ -545,11 +980,11 @@
1.1052 (t, vars)
1.1053 (* If 't' is of type 'propT' (rather than 'boolT'), applying *)
1.1054 (* 'HOLogic.exists_const' is not type-correct. However, this *)
1.1055 - (* isn't really a problem as long as 'find_model' still *)
1.1056 + (* is not really a problem as long as 'find_model' still *)
1.1057 (* interprets the resulting term correctly, without checking *)
1.1058 (* its type. *)
1.1059 in
1.1060 - find_model thy (actual_params thy params) ex_closure false
1.1061 + find_model thy (actual_params thy params) ex_closure true
1.1062 end;
1.1063
1.1064 (* ------------------------------------------------------------------------- *)
1.1065 @@ -569,986 +1004,16 @@
1.1066 (* INTERPRETERS *)
1.1067 (* ------------------------------------------------------------------------- *)
1.1068
1.1069 - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1070 -
1.1071 - fun var_typevar_interpreter thy model args t =
1.1072 - let
1.1073 - fun is_var (Free _) = true
1.1074 - | is_var (Var _) = true
1.1075 - | is_var _ = false
1.1076 - fun typeof (Free (_,T)) = T
1.1077 - | typeof (Var (_,T)) = T
1.1078 - | typeof _ = raise REFUTE ("var_typevar_interpreter", "term is not a variable")
1.1079 - fun is_typevar (TFree _) = true
1.1080 - | is_typevar (TVar _) = true
1.1081 - | is_typevar _ = false
1.1082 - val (sizes, intrs) = model
1.1083 - in
1.1084 - if is_var t andalso is_typevar (typeof t) then
1.1085 - (case assoc (intrs, t) of
1.1086 - Some intr => Some (intr, model, args)
1.1087 - | None =>
1.1088 - let
1.1089 - val size = (the o assoc) (sizes, typeof t) (* the model MUST specify a size for type variables *)
1.1090 - val idx = #next_idx args
1.1091 - val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1))))
1.1092 - val next = (if size=2 then idx+1 else idx+size)
1.1093 - in
1.1094 - (* extend the model, increase 'next_idx' *)
1.1095 - Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args})
1.1096 - end)
1.1097 - else
1.1098 - None
1.1099 - end;
1.1100 -
1.1101 - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1102 -
1.1103 - fun var_funtype_interpreter thy model args t =
1.1104 - let
1.1105 - fun is_var (Free _) = true
1.1106 - | is_var (Var _) = true
1.1107 - | is_var _ = false
1.1108 - fun typeof (Free (_,T)) = T
1.1109 - | typeof (Var (_,T)) = T
1.1110 - | typeof _ = raise REFUTE ("var_funtype_interpreter", "term is not a variable")
1.1111 - fun stringof (Free (x,_)) = x
1.1112 - | stringof (Var ((x,_), _)) = x
1.1113 - | stringof _ = raise REFUTE ("var_funtype_interpreter", "term is not a variable")
1.1114 - fun is_funtype (Type ("fun", [_,_])) = true
1.1115 - | is_funtype _ = false
1.1116 - val (sizes, intrs) = model
1.1117 - in
1.1118 - if is_var t andalso is_funtype (typeof t) then
1.1119 - (case assoc (intrs, t) of
1.1120 - Some intr => Some (intr, model, args)
1.1121 - | None =>
1.1122 - let
1.1123 - val T1 = domain_type (typeof t)
1.1124 - val T2 = range_type (typeof t)
1.1125 - (* we create 'size_of_interpretation (interpret (... T1))' different copies *)
1.1126 - (* of the tree for 'T2', which are then combined into a single new tree *)
1.1127 - val (i1, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (stringof t, T1))
1.1128 - (* power(a,b) computes a^b, for a>=0, b>=0 *)
1.1129 - (* int * int -> int *)
1.1130 - fun power (a,0) = 1
1.1131 - | power (a,1) = a
1.1132 - | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
1.1133 - fun size_of_interpretation (Leaf xs) = length xs
1.1134 - | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
1.1135 - val size = size_of_interpretation i1
1.1136 - (* make fresh copies, with different variable indices *)
1.1137 - (* int -> int -> (int * interpretation list *)
1.1138 - fun make_copies idx 0 =
1.1139 - (idx, [])
1.1140 - | make_copies idx n =
1.1141 - let
1.1142 - val (copy, _, args) = interpret thy (sizes, []) {next_idx = idx, bounds = [], wellformed=True} (Free (stringof t, T2))
1.1143 - val (next, copies) = make_copies (#next_idx args) (n-1)
1.1144 - in
1.1145 - (next, copy :: copies)
1.1146 - end
1.1147 - val (idx, copies) = make_copies (#next_idx args) (size_of_interpretation i1)
1.1148 - (* combine copies into a single tree *)
1.1149 - val intr = Node copies
1.1150 - in
1.1151 - (* extend the model, increase 'next_idx' *)
1.1152 - Some (intr, (sizes, (t, intr)::intrs), {next_idx = idx, bounds = #bounds args, wellformed = #wellformed args})
1.1153 - end)
1.1154 - else
1.1155 - None
1.1156 - end;
1.1157 -
1.1158 - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1159 -
1.1160 - fun var_settype_interpreter thy model args t =
1.1161 - let
1.1162 - val (sizes, intrs) = model
1.1163 - in
1.1164 - case t of
1.1165 - Free (x, Type ("set", [T])) =>
1.1166 - (case assoc (intrs, t) of
1.1167 - Some intr => Some (intr, model, args)
1.1168 - | None =>
1.1169 - let
1.1170 - val (intr, _, args') = interpret thy model args (Free (x, Type ("fun", [T, Type ("bool", [])])))
1.1171 - in
1.1172 - Some (intr, (sizes, (t, intr)::intrs), args')
1.1173 - end)
1.1174 - | Var ((x,i), Type ("set", [T])) =>
1.1175 - (case assoc (intrs, t) of
1.1176 - Some intr => Some (intr, model, args)
1.1177 - | None =>
1.1178 - let
1.1179 - val (intr, _, args') = interpret thy model args (Var ((x,i), Type ("fun", [T, Type ("bool", [])])))
1.1180 - in
1.1181 - Some (intr, (sizes, (t, intr)::intrs), args')
1.1182 - end)
1.1183 - | _ => None
1.1184 - end;
1.1185 -
1.1186 - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1187 -
1.1188 - fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds (args:arguments)), model, args)
1.1189 - | boundvar_interpreter thy model args _ = None;
1.1190 -
1.1191 - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1192 -
1.1193 - fun abstraction_interpreter thy model args (Abs (x, T, t)) =
1.1194 - let
1.1195 - val (sizes, intrs) = model
1.1196 - (* create all constants of type T *)
1.1197 - val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (x, T))
1.1198 - (* returns a list with all unit vectors of length n *)
1.1199 - (* int -> interpretation list *)
1.1200 - fun unit_vectors n =
1.1201 - let
1.1202 - (* returns the k-th unit vector of length n *)
1.1203 - (* int * int -> interpretation *)
1.1204 - fun unit_vector (k,n) =
1.1205 - Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.1206 - (* int -> interpretation list -> interpretation list *)
1.1207 - fun unit_vectors_acc k vs =
1.1208 - if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
1.1209 - in
1.1210 - unit_vectors_acc 1 []
1.1211 - end
1.1212 - (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.1213 - (* 'a -> 'a list list -> 'a list list *)
1.1214 - fun cons_list x xss =
1.1215 - map (fn xs => x::xs) xss
1.1216 - (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
1.1217 - (* int -> 'a list -> 'a list list *)
1.1218 - fun pick_all 1 xs =
1.1219 - map (fn x => [x]) xs
1.1220 - | pick_all n xs =
1.1221 - let val rec_pick = pick_all (n-1) xs in
1.1222 - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.1223 - end
1.1224 - (* interpretation -> interpretation list *)
1.1225 - fun make_constants (Leaf xs) =
1.1226 - unit_vectors (length xs)
1.1227 - | make_constants (Node xs) =
1.1228 - map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.1229 - (* interpret the body 't' separately for each constant *)
1.1230 - val ((model', args'), bodies) = foldl_map
1.1231 - (fn ((m,a), c) =>
1.1232 - let
1.1233 - (* add 'c' to 'bounds' *)
1.1234 - val (i',m',a') = interpret thy m {next_idx = #next_idx a, bounds = c::(#bounds a), wellformed = #wellformed a} t
1.1235 - in
1.1236 - (* keep the new model m' and 'next_idx', but use old 'bounds' *)
1.1237 - ((m',{next_idx = #next_idx a', bounds = #bounds a, wellformed = #wellformed a'}), i')
1.1238 - end)
1.1239 - ((model,args), make_constants i)
1.1240 - in
1.1241 - Some (Node bodies, model', args')
1.1242 - end
1.1243 - | abstraction_interpreter thy model args _ = None;
1.1244 -
1.1245 - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1246 -
1.1247 - fun apply_interpreter thy model args (t1 $ t2) =
1.1248 - let
1.1249 - (* auxiliary functions *)
1.1250 - (* interpretation * interpretation -> interpretation *)
1.1251 - fun interpretation_disjunction (tr1,tr2) =
1.1252 - tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
1.1253 - (* prop_formula * interpretation -> interpretation *)
1.1254 - fun prop_formula_times_interpretation (fm,tr) =
1.1255 - tree_map (map (fn x => SAnd (fm,x))) tr
1.1256 - (* prop_formula list * interpretation list -> interpretation *)
1.1257 - fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
1.1258 - prop_formula_times_interpretation (fm,tr)
1.1259 - | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
1.1260 - interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees))
1.1261 - | prop_formula_list_dot_product_interpretation_list (_,_) =
1.1262 - raise REFUTE ("apply_interpreter", "empty list (in dot product)")
1.1263 - (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.1264 - (* 'a -> 'a list list -> 'a list list *)
1.1265 - fun cons_list x xss =
1.1266 - map (fn xs => x::xs) xss
1.1267 - (* returns a list of lists, each one consisting of one element from each element of 'xss' *)
1.1268 - (* 'a list list -> 'a list list *)
1.1269 - fun pick_all [xs] =
1.1270 - map (fn x => [x]) xs
1.1271 - | pick_all (xs::xss) =
1.1272 - let val rec_pick = pick_all xss in
1.1273 - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.1274 - end
1.1275 - | pick_all _ =
1.1276 - raise REFUTE ("apply_interpreter", "empty list (in pick_all)")
1.1277 - (* interpretation -> prop_formula list *)
1.1278 - fun interpretation_to_prop_formula_list (Leaf xs) =
1.1279 - xs
1.1280 - | interpretation_to_prop_formula_list (Node trees) =
1.1281 - map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees))
1.1282 - (* interpretation * interpretation -> interpretation *)
1.1283 - fun interpretation_apply (tr1,tr2) =
1.1284 - (case tr1 of
1.1285 - Leaf _ =>
1.1286 - raise REFUTE ("apply_interpreter", "first interpretation is a leaf")
1.1287 - | Node xs =>
1.1288 - prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list tr2, xs))
1.1289 - (* interpret 't1' and 't2' *)
1.1290 - val (intr1, model1, args1) = interpret thy model args t1
1.1291 - val (intr2, model2, args2) = interpret thy model1 args1 t2
1.1292 - in
1.1293 - Some (interpretation_apply (intr1,intr2), model2, args2)
1.1294 - end
1.1295 - | apply_interpreter thy model args _ = None;
1.1296 -
1.1297 - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1298 -
1.1299 - fun const_unfold_interpreter thy model args t =
1.1300 - (* ------------------------------------------------------------------------- *)
1.1301 - (* We unfold constants for which a defining equation is given as an axiom. *)
1.1302 - (* A polymorphic axiom's type variables are instantiated. Eta-expansion is *)
1.1303 - (* performed only if necessary; arguments in the axiom that are present as *)
1.1304 - (* actual arguments in 't' are simply substituted. If more actual than *)
1.1305 - (* formal arguments are present, the constant is *not* unfolded, so that *)
1.1306 - (* other interpreters (that may just not have looked into the term far *)
1.1307 - (* enough yet) may be applied first (after 'apply_interpreter' gets rid of *)
1.1308 - (* one argument). *)
1.1309 - (* ------------------------------------------------------------------------- *)
1.1310 - let
1.1311 - val (head, actuals) = strip_comb t
1.1312 - val actuals_count = length actuals
1.1313 - in
1.1314 - case head of
1.1315 - Const (s,T) =>
1.1316 - let
1.1317 - (* (string * Term.term) list *)
1.1318 - val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
1.1319 - (* Term.term * Term.term list * Term.term list -> Term.term *)
1.1320 - (* term, formal arguments, actual arguments *)
1.1321 - fun normalize (t, [], []) = t
1.1322 - | normalize (t, [], y::ys) = raise REFUTE ("const_unfold_interpreter", "more actual than formal parameters")
1.1323 - | normalize (t, x::xs, []) = normalize (lambda x t, xs, []) (* eta-expansion *)
1.1324 - | normalize (t, x::xs, y::ys) = normalize (betapply (lambda x t, y), xs, ys) (* substitution *)
1.1325 - (* string -> Term.typ -> (string * Term.term) list -> Term.term option *)
1.1326 - fun get_defn s T [] =
1.1327 - None
1.1328 - | get_defn s T ((_,ax)::axms) =
1.1329 - (let
1.1330 - val (lhs, rhs) = Logic.dest_equals ax (* equations only *)
1.1331 - val (c, formals) = strip_comb lhs
1.1332 - val (s', T') = dest_Const c
1.1333 - in
1.1334 - if (s=s') andalso (actuals_count <= length formals) then
1.1335 - let
1.1336 - val varT' = Type.varifyT T' (* for polymorphic definitions *)
1.1337 - val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (varT', T))
1.1338 - val varRhs = map_term_types Type.varifyT rhs
1.1339 - val varFormals = map (map_term_types Type.varifyT) formals
1.1340 - val rhs' = normalize (varRhs, varFormals, actuals)
1.1341 - val unvarRhs = map_term_types
1.1342 - (map_type_tvar
1.1343 - (fn (v,_) =>
1.1344 - case Vartab.lookup (typeSubs, v) of
1.1345 - None =>
1.1346 - raise REFUTE ("const_unfold_interpreter", "schematic type variable " ^ (fst v) ^ "not instantiated (in definition of " ^ quote s ^ ")")
1.1347 - | Some typ =>
1.1348 - typ))
1.1349 - rhs'
1.1350 - in
1.1351 - Some unvarRhs
1.1352 - end
1.1353 - else
1.1354 - get_defn s T axms
1.1355 - end
1.1356 - handle TERM _ => get_defn s T axms
1.1357 - | Type.TYPE_MATCH => get_defn s T axms)
1.1358 - in
1.1359 - case get_defn s T axioms of
1.1360 - Some t' => Some (interpret thy model args t')
1.1361 - | None => None
1.1362 - end
1.1363 - | _ => None
1.1364 - end;
1.1365 -
1.1366 - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1367 -
1.1368 - fun Pure_interpreter thy model args t =
1.1369 - let
1.1370 - fun toTrue (Leaf [fm,_]) = fm
1.1371 - | toTrue _ = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value")
1.1372 - fun toFalse (Leaf [_,fm]) = fm
1.1373 - | toFalse _ = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value")
1.1374 - in
1.1375 - case t of
1.1376 - (*Const ("Goal", _) $ t1 =>
1.1377 - Some (interpret thy model args t1) |*)
1.1378 - Const ("all", _) $ t1 =>
1.1379 - let
1.1380 - val (i,m,a) = (interpret thy model args t1)
1.1381 - in
1.1382 - case i of
1.1383 - Node xs =>
1.1384 - let
1.1385 - val fmTrue = PropLogic.all (map toTrue xs)
1.1386 - val fmFalse = PropLogic.exists (map toFalse xs)
1.1387 - in
1.1388 - Some (Leaf [fmTrue, fmFalse], m, a)
1.1389 - end
1.1390 - | _ =>
1.1391 - raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function")
1.1392 - end
1.1393 - | Const ("==", _) $ t1 $ t2 =>
1.1394 - let
1.1395 - val (i1,m1,a1) = interpret thy model args t1
1.1396 - val (i2,m2,a2) = interpret thy m1 a1 t2
1.1397 - (* interpretation * interpretation -> prop_formula *)
1.1398 - fun interpret_equal (tr1,tr2) =
1.1399 - (case tr1 of
1.1400 - Leaf x =>
1.1401 - (case tr2 of
1.1402 - Leaf y => PropLogic.dot_product (x,y)
1.1403 - | _ => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher"))
1.1404 - | Node xs =>
1.1405 - (case tr2 of
1.1406 - Leaf _ => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher")
1.1407 - (* extensionality: two functions are equal iff they are equal for every element *)
1.1408 - | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
1.1409 - (* interpretation * interpretation -> prop_formula *)
1.1410 - fun interpret_unequal (tr1,tr2) =
1.1411 - (case tr1 of
1.1412 - Leaf x =>
1.1413 - (case tr2 of
1.1414 - Leaf y =>
1.1415 - let
1.1416 - fun unequal [] ([],_) =
1.1417 - False
1.1418 - | unequal (x::xs) (y::ys1, ys2) =
1.1419 - SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2))
1.1420 - | unequal _ _ =
1.1421 - raise REFUTE ("Pure_interpreter", "\"==\": leafs have different width")
1.1422 - in
1.1423 - unequal x (y,[])
1.1424 - end
1.1425 - | _ => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher"))
1.1426 - | Node xs =>
1.1427 - (case tr2 of
1.1428 - Leaf _ => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher")
1.1429 - (* extensionality: two functions are unequal iff there exist unequal elements *)
1.1430 - | Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys))))
1.1431 - val fmTrue = interpret_equal (i1,i2)
1.1432 - val fmFalse = interpret_unequal (i1,i2)
1.1433 - in
1.1434 - Some (Leaf [fmTrue, fmFalse], m2, a2)
1.1435 - end
1.1436 - | Const ("==>", _) $ t1 $ t2 =>
1.1437 - let
1.1438 - val (i1,m1,a1) = interpret thy model args t1
1.1439 - val (i2,m2,a2) = interpret thy m1 a1 t2
1.1440 - val fmTrue = SOr (toFalse i1, toTrue i2)
1.1441 - val fmFalse = SAnd (toTrue i1, toFalse i2)
1.1442 - in
1.1443 - Some (Leaf [fmTrue, fmFalse], m2, a2)
1.1444 - end
1.1445 - | _ => None
1.1446 - end;
1.1447 -
1.1448 - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1449 -
1.1450 - fun HOLogic_interpreter thy model args t =
1.1451 - (* ------------------------------------------------------------------------- *)
1.1452 - (* Providing interpretations directly is more efficient than unfolding the *)
1.1453 - (* logical constants; however, we need versions for constants with arguments *)
1.1454 - (* (to avoid unfolding) as well as versions for constants without arguments *)
1.1455 - (* (since in HOL, logical constants can themselves be arguments) *)
1.1456 - (* ------------------------------------------------------------------------- *)
1.1457 - let
1.1458 - fun eta_expand t i =
1.1459 - let
1.1460 - val Ts = binder_types (fastype_of t)
1.1461 - in
1.1462 - foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
1.1463 - (take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
1.1464 - end
1.1465 - val TT = Leaf [True, False]
1.1466 - val FF = Leaf [False, True]
1.1467 - fun toTrue (Leaf [fm,_]) = fm
1.1468 - | toTrue _ = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value")
1.1469 - fun toFalse (Leaf [_,fm]) = fm
1.1470 - | toFalse _ = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value")
1.1471 - in
1.1472 - case t of
1.1473 - Const ("Trueprop", _) $ t1 =>
1.1474 - Some (interpret thy model args t1)
1.1475 - | Const ("Trueprop", _) =>
1.1476 - Some (Node [TT, FF], model, args)
1.1477 - | Const ("Not", _) $ t1 =>
1.1478 - apply_interpreter thy model args t
1.1479 - | Const ("Not", _) =>
1.1480 - Some (Node [FF, TT], model, args)
1.1481 - | Const ("True", _) =>
1.1482 - Some (TT, model, args)
1.1483 - | Const ("False", _) =>
1.1484 - Some (FF, model, args)
1.1485 - | Const ("arbitrary", T) =>
1.1486 - (* treat 'arbitrary' just like a free variable of the same type *)
1.1487 - (case assoc (snd model, t) of
1.1488 - Some intr =>
1.1489 - Some (intr, model, args)
1.1490 - | None =>
1.1491 - let
1.1492 - val (sizes, intrs) = model
1.1493 - val (intr, _, a) = interpret thy (sizes, []) args (Free ("<arbitrary>", T))
1.1494 - in
1.1495 - Some (intr, (sizes, (t,intr)::intrs), a)
1.1496 - end)
1.1497 - | Const ("The", _) $ t1 =>
1.1498 - apply_interpreter thy model args t
1.1499 - | Const ("The", T as Type ("fun", [_, T'])) =>
1.1500 - (* treat 'The' like a free variable, but with a fixed interpretation for boolean *)
1.1501 - (* functions that map exactly one constant of type T' to True *)
1.1502 - (case assoc (snd model, t) of
1.1503 - Some intr =>
1.1504 - Some (intr, model, args)
1.1505 - | None =>
1.1506 - let
1.1507 - val (sizes, intrs) = model
1.1508 - val (intr, _, a) = interpret thy (sizes, []) args (Free ("<The>", T))
1.1509 - (* create all constants of type T' => bool, ... *)
1.1510 - val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<The>", Type ("fun", [T', Type ("bool",[])])))
1.1511 - (* ... and all constants of type T' *)
1.1512 - val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<The>", T'))
1.1513 - (* returns a list with all unit vectors of length n *)
1.1514 - (* int -> interpretation list *)
1.1515 - fun unit_vectors n =
1.1516 - let
1.1517 - (* returns the k-th unit vector of length n *)
1.1518 - (* int * int -> interpretation *)
1.1519 - fun unit_vector (k,n) =
1.1520 - Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.1521 - (* int -> interpretation list -> interpretation list *)
1.1522 - fun unit_vectors_acc k vs =
1.1523 - if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
1.1524 - in
1.1525 - unit_vectors_acc 1 []
1.1526 - end
1.1527 - (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.1528 - (* 'a -> 'a list list -> 'a list list *)
1.1529 - fun cons_list x xss =
1.1530 - map (fn xs => x::xs) xss
1.1531 - (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
1.1532 - (* int -> 'a list -> 'a list list *)
1.1533 - fun pick_all 1 xs =
1.1534 - map (fn x => [x]) xs
1.1535 - | pick_all n xs =
1.1536 - let val rec_pick = pick_all (n-1) xs in
1.1537 - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.1538 - end
1.1539 - (* interpretation -> interpretation list *)
1.1540 - fun make_constants (Leaf xs) =
1.1541 - unit_vectors (length xs)
1.1542 - | make_constants (Node xs) =
1.1543 - map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.1544 - val constantsFun = make_constants intrFun
1.1545 - val constantsT' = make_constants intrT'
1.1546 - (* interpretation -> interpretation list -> interpretation option *)
1.1547 - fun the_val (Node xs) cs =
1.1548 - let
1.1549 - val TrueCount = foldl (fn (n,x) => if toTrue x = True then n+1 else n) (0,xs)
1.1550 - fun findThe (x::xs) (c::cs) =
1.1551 - if toTrue x = True then
1.1552 - c
1.1553 - else
1.1554 - findThe xs cs
1.1555 - | findThe _ _ =
1.1556 - raise REFUTE ("HOLogic_interpreter", "\"The\": not found")
1.1557 - in
1.1558 - if TrueCount=1 then
1.1559 - Some (findThe xs cs)
1.1560 - else
1.1561 - None
1.1562 - end
1.1563 - | the_val _ _ =
1.1564 - raise REFUTE ("HOLogic_interpreter", "\"The\": function interpreted as a leaf")
1.1565 - in
1.1566 - case intr of
1.1567 - Node xs =>
1.1568 - let
1.1569 - (* replace interpretation 'x' by the interpretation determined by 'f' *)
1.1570 - val intrThe = Node (map (fn (x,f) => if_none (the_val f constantsT') x) (xs ~~ constantsFun))
1.1571 - in
1.1572 - Some (intrThe, (sizes, (t,intrThe)::intrs), a)
1.1573 - end
1.1574 - | _ =>
1.1575 - raise REFUTE ("HOLogic_interpreter", "\"The\": interpretation is a leaf")
1.1576 - end)
1.1577 - | Const ("Hilbert_Choice.Eps", _) $ t1 =>
1.1578 - apply_interpreter thy model args t
1.1579 - | Const ("Hilbert_Choice.Eps", T as Type ("fun", [_, T'])) =>
1.1580 - (* treat 'The' like a free variable, but with a fixed interpretation for boolean *)
1.1581 - (* functions that map exactly one constant of type T' to True *)
1.1582 - (case assoc (snd model, t) of
1.1583 - Some intr =>
1.1584 - Some (intr, model, args)
1.1585 - | None =>
1.1586 - let
1.1587 - val (sizes, intrs) = model
1.1588 - val (intr, _, a) = interpret thy (sizes, []) args (Free ("<Eps>", T))
1.1589 - (* create all constants of type T' => bool, ... *)
1.1590 - val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<Eps>", Type ("fun", [T', Type ("bool",[])])))
1.1591 - (* ... and all constants of type T' *)
1.1592 - val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<Eps>", T'))
1.1593 - (* returns a list with all unit vectors of length n *)
1.1594 - (* int -> interpretation list *)
1.1595 - fun unit_vectors n =
1.1596 - let
1.1597 - (* returns the k-th unit vector of length n *)
1.1598 - (* int * int -> interpretation *)
1.1599 - fun unit_vector (k,n) =
1.1600 - Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.1601 - (* int -> interpretation list -> interpretation list *)
1.1602 - fun unit_vectors_acc k vs =
1.1603 - if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
1.1604 - in
1.1605 - unit_vectors_acc 1 []
1.1606 - end
1.1607 - (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.1608 - (* 'a -> 'a list list -> 'a list list *)
1.1609 - fun cons_list x xss =
1.1610 - map (fn xs => x::xs) xss
1.1611 - (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
1.1612 - (* int -> 'a list -> 'a list list *)
1.1613 - fun pick_all 1 xs =
1.1614 - map (fn x => [x]) xs
1.1615 - | pick_all n xs =
1.1616 - let val rec_pick = pick_all (n-1) xs in
1.1617 - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.1618 - end
1.1619 - (* interpretation -> interpretation list *)
1.1620 - fun make_constants (Leaf xs) =
1.1621 - unit_vectors (length xs)
1.1622 - | make_constants (Node xs) =
1.1623 - map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.1624 - val constantsFun = make_constants intrFun
1.1625 - val constantsT' = make_constants intrT'
1.1626 - (* interpretation -> interpretation list -> interpretation list *)
1.1627 - fun true_values (Node xs) cs =
1.1628 - mapfilter (fn (x,c) => if toTrue x = True then Some c else None) (xs~~cs)
1.1629 - | true_values _ _ =
1.1630 - raise REFUTE ("HOLogic_interpreter", "\"Eps\": function interpreted as a leaf")
1.1631 - in
1.1632 - case intr of
1.1633 - Node xs =>
1.1634 - let
1.1635 - val (wf, intrsEps) = foldl_map (fn (w,(x,f)) =>
1.1636 - case true_values f constantsT' of
1.1637 - [] => (w, x) (* no value mapped to true -> no restriction *)
1.1638 - | [c] => (w, c) (* one value mapped to true -> that's the one *)
1.1639 - | cs =>
1.1640 - let
1.1641 - (* interpretation * interpretation -> prop_formula *)
1.1642 - fun interpret_equal (tr1,tr2) =
1.1643 - (case tr1 of
1.1644 - Leaf x =>
1.1645 - (case tr2 of
1.1646 - Leaf y => PropLogic.dot_product (x,y)
1.1647 - | _ => raise REFUTE ("HOLogic_interpreter", "\"Eps\": second tree is higher"))
1.1648 - | Node xs =>
1.1649 - (case tr2 of
1.1650 - Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"Eps\": first tree is higher")
1.1651 - (* extensionality: two functions are equal iff they are equal for every element *)
1.1652 - | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
1.1653 - in
1.1654 - (SAnd (w, PropLogic.exists (map (fn c => interpret_equal (x,c)) cs)), x) (* impose restrictions on x *)
1.1655 - end
1.1656 - )
1.1657 - (#wellformed a, xs ~~ constantsFun)
1.1658 - val intrEps = Node intrsEps
1.1659 - in
1.1660 - Some (intrEps, (sizes, (t,intrEps)::intrs), {next_idx = #next_idx a, bounds = #bounds a, wellformed = wf})
1.1661 - end
1.1662 - | _ =>
1.1663 - raise REFUTE ("HOLogic_interpreter", "\"Eps\": interpretation is a leaf")
1.1664 - end)
1.1665 - | Const ("All", _) $ t1 =>
1.1666 - let
1.1667 - val (i,m,a) = interpret thy model args t1
1.1668 - in
1.1669 - case i of
1.1670 - Node xs =>
1.1671 - let
1.1672 - val fmTrue = PropLogic.all (map toTrue xs)
1.1673 - val fmFalse = PropLogic.exists (map toFalse xs)
1.1674 - in
1.1675 - Some (Leaf [fmTrue, fmFalse], m, a)
1.1676 - end
1.1677 - | _ =>
1.1678 - raise REFUTE ("HOLogic_interpreter", "\"All\" is not followed by a function")
1.1679 - end
1.1680 - | Const ("All", _) =>
1.1681 - Some (interpret thy model args (eta_expand t 1))
1.1682 - | Const ("Ex", _) $ t1 =>
1.1683 - let
1.1684 - val (i,m,a) = interpret thy model args t1
1.1685 - in
1.1686 - case i of
1.1687 - Node xs =>
1.1688 - let
1.1689 - val fmTrue = PropLogic.exists (map toTrue xs)
1.1690 - val fmFalse = PropLogic.all (map toFalse xs)
1.1691 - in
1.1692 - Some (Leaf [fmTrue, fmFalse], m, a)
1.1693 - end
1.1694 - | _ =>
1.1695 - raise REFUTE ("HOLogic_interpreter", "\"Ex\" is not followed by a function")
1.1696 - end
1.1697 - | Const ("Ex", _) =>
1.1698 - Some (interpret thy model args (eta_expand t 1))
1.1699 - | Const ("Ex1", _) $ t1 =>
1.1700 - let
1.1701 - val (i,m,a) = interpret thy model args t1
1.1702 - in
1.1703 - case i of
1.1704 - Node xs =>
1.1705 - let
1.1706 - (* interpretation list -> prop_formula *)
1.1707 - fun allfalse [] = True
1.1708 - | allfalse (x::xs) = SAnd (toFalse x, allfalse xs)
1.1709 - (* interpretation list -> prop_formula *)
1.1710 - fun exactly1true [] = False
1.1711 - | exactly1true (x::xs) = SOr (SAnd (toTrue x, allfalse xs), SAnd (toFalse x, exactly1true xs))
1.1712 - (* interpretation list -> prop_formula *)
1.1713 - fun atleast2true [] = False
1.1714 - | atleast2true (x::xs) = SOr (SAnd (toTrue x, PropLogic.exists (map toTrue xs)), atleast2true xs)
1.1715 - val fmTrue = exactly1true xs
1.1716 - val fmFalse = SOr (allfalse xs, atleast2true xs)
1.1717 - in
1.1718 - Some (Leaf [fmTrue, fmFalse], m, a)
1.1719 - end
1.1720 - | _ =>
1.1721 - raise REFUTE ("HOLogic_interpreter", "\"Ex1\" is not followed by a function")
1.1722 - end
1.1723 - | Const ("Ex1", _) =>
1.1724 - Some (interpret thy model args (eta_expand t 1))
1.1725 - | Const ("op =", _) $ t1 $ t2 =>
1.1726 - let
1.1727 - val (i1,m1,a1) = interpret thy model args t1
1.1728 - val (i2,m2,a2) = interpret thy m1 a1 t2
1.1729 - (* interpretation * interpretation -> prop_formula *)
1.1730 - fun interpret_equal (tr1,tr2) =
1.1731 - (case tr1 of
1.1732 - Leaf x =>
1.1733 - (case tr2 of
1.1734 - Leaf y => PropLogic.dot_product (x,y)
1.1735 - | _ => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher"))
1.1736 - | Node xs =>
1.1737 - (case tr2 of
1.1738 - Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher")
1.1739 - (* extensionality: two functions are equal iff they are equal for every element *)
1.1740 - | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
1.1741 - (* interpretation * interpretation -> prop_formula *)
1.1742 - fun interpret_unequal (tr1,tr2) =
1.1743 - (case tr1 of
1.1744 - Leaf x =>
1.1745 - (case tr2 of
1.1746 - Leaf y =>
1.1747 - let
1.1748 - fun unequal [] ([],_) =
1.1749 - False
1.1750 - | unequal (x::xs) (y::ys1, ys2) =
1.1751 - SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2))
1.1752 - | unequal _ _ =
1.1753 - raise REFUTE ("HOLogic_interpreter", "\"==\": leafs have different width")
1.1754 - in
1.1755 - unequal x (y,[])
1.1756 - end
1.1757 - | _ => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher"))
1.1758 - | Node xs =>
1.1759 - (case tr2 of
1.1760 - Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher")
1.1761 - (* extensionality: two functions are unequal iff there exist unequal elements *)
1.1762 - | Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys))))
1.1763 - val fmTrue = interpret_equal (i1,i2)
1.1764 - val fmFalse = interpret_unequal (i1,i2)
1.1765 - in
1.1766 - Some (Leaf [fmTrue, fmFalse], m2, a2)
1.1767 - end
1.1768 - | Const ("op =", _) $ t1 =>
1.1769 - Some (interpret thy model args (eta_expand t 1))
1.1770 - | Const ("op =", _) =>
1.1771 - Some (interpret thy model args (eta_expand t 2))
1.1772 - | Const ("op &", _) $ t1 $ t2 =>
1.1773 - apply_interpreter thy model args t
1.1774 - | Const ("op &", _) $ t1 =>
1.1775 - apply_interpreter thy model args t
1.1776 - | Const ("op &", _) =>
1.1777 - Some (Node [Node [TT, FF], Node [FF, FF]], model, args)
1.1778 - | Const ("op |", _) $ t1 $ t2 =>
1.1779 - apply_interpreter thy model args t
1.1780 - | Const ("op |", _) $ t1 =>
1.1781 - apply_interpreter thy model args t
1.1782 - | Const ("op |", _) =>
1.1783 - Some (Node [Node [TT, TT], Node [TT, FF]], model, args)
1.1784 - | Const ("op -->", _) $ t1 $ t2 =>
1.1785 - apply_interpreter thy model args t
1.1786 - | Const ("op -->", _) $ t1 =>
1.1787 - apply_interpreter thy model args t
1.1788 - | Const ("op -->", _) =>
1.1789 - Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
1.1790 - | Const ("Collect", _) $ t1 =>
1.1791 - (* Collect == identity *)
1.1792 - Some (interpret thy model args t1)
1.1793 - | Const ("Collect", _) =>
1.1794 - Some (interpret thy model args (eta_expand t 1))
1.1795 - | Const ("op :", _) $ t1 $ t2 =>
1.1796 - (* op: == application *)
1.1797 - Some (interpret thy model args (t2 $ t1))
1.1798 - | Const ("op :", _) $ t1 =>
1.1799 - Some (interpret thy model args (eta_expand t 1))
1.1800 - | Const ("op :", _) =>
1.1801 - Some (interpret thy model args (eta_expand t 2))
1.1802 - | _ => None
1.1803 - end;
1.1804 -
1.1805 - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1806 -
1.1807 - fun IDT_interpreter thy model args t =
1.1808 - let
1.1809 - fun is_var (Free _) = true
1.1810 - | is_var (Var _) = true
1.1811 - | is_var _ = false
1.1812 - fun typeof (Free (_,T)) = T
1.1813 - | typeof (Var (_,T)) = T
1.1814 - | typeof _ = raise REFUTE ("var_IDT_interpreter", "term is not a variable")
1.1815 - val (sizes, intrs) = model
1.1816 - (* power(a,b) computes a^b, for a>=0, b>=0 *)
1.1817 - (* int * int -> int *)
1.1818 - fun power (a,0) = 1
1.1819 - | power (a,1) = a
1.1820 - | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
1.1821 - (* interpretation -> int *)
1.1822 - fun size_of_interpretation (Leaf xs) = length xs
1.1823 - | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
1.1824 - (* Term.typ -> int *)
1.1825 - fun size_of_type T =
1.1826 - let
1.1827 - val (i,_,_) = interpret thy model args (Free ("<IDT>", T))
1.1828 - in
1.1829 - size_of_interpretation i
1.1830 - end
1.1831 - (* int list -> int *)
1.1832 - fun sum xs = foldl op+ (0, xs)
1.1833 - (* int list -> int *)
1.1834 - fun product xs = foldl op* (1, xs)
1.1835 - (* DatatypeAux.dtyp * Term.typ -> DatatypeAux.dtyp -> Term.typ *)
1.1836 - fun typ_of_dtyp typ_assoc (DatatypeAux.DtTFree a) =
1.1837 - the (assoc (typ_assoc, DatatypeAux.DtTFree a))
1.1838 - | typ_of_dtyp typ_assoc (DatatypeAux.DtRec i) =
1.1839 - raise REFUTE ("var_IDT_interpreter", "recursive datatype")
1.1840 - | typ_of_dtyp typ_assoc (DatatypeAux.DtType (s, ds)) =
1.1841 - Type (s, map (typ_of_dtyp typ_assoc) ds)
1.1842 - in
1.1843 - if is_var t then
1.1844 - (case typeof t of
1.1845 - Type (s, Ts) =>
1.1846 - (case DatatypePackage.datatype_info thy s of
1.1847 - Some info => (* inductive datatype *)
1.1848 - let
1.1849 - val index = #index info
1.1850 - val descr = #descr info
1.1851 - val (_, dtyps, constrs) = the (assoc (descr, index))
1.1852 - in
1.1853 - if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
1.1854 - raise REFUTE ("var_IDT_interpreter", "recursive datatype argument")
1.1855 - else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
1.1856 - None (* recursive datatype (requires an infinite model) *)
1.1857 - else
1.1858 - case assoc (intrs, t) of
1.1859 - Some intr => Some (intr, model, args)
1.1860 - | None =>
1.1861 - let
1.1862 - val typ_assoc = dtyps ~~ Ts
1.1863 - val size = sum (map (fn (_,ds) =>
1.1864 - product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) constrs)
1.1865 - val idx = #next_idx args
1.1866 - (* for us, an IDT has no "internal structure" -- its interpretation is just a leaf *)
1.1867 - val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1))))
1.1868 - val next = (if size=2 then idx+1 else idx+size)
1.1869 - in
1.1870 - (* extend the model, increase 'next_idx' *)
1.1871 - Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args})
1.1872 - end
1.1873 - end
1.1874 - | None => None)
1.1875 - | _ => None)
1.1876 - else
1.1877 - let
1.1878 - val (head, params) = strip_comb t (* look into applications to avoid unfolding *)
1.1879 - in
1.1880 - (case head of
1.1881 - Const (c, T) =>
1.1882 - (case body_type T of
1.1883 - Type (s, Ts) =>
1.1884 - (case DatatypePackage.datatype_info thy s of
1.1885 - Some info => (* inductive datatype *)
1.1886 - let
1.1887 - val index = #index info
1.1888 - val descr = #descr info
1.1889 - val (_, dtyps, constrs) = the (assoc (descr, index))
1.1890 - in
1.1891 - if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
1.1892 - raise REFUTE ("var_IDT_interpreter", "recursive datatype argument")
1.1893 - else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
1.1894 - None (* recursive datatype (requires an infinite model) *)
1.1895 - else
1.1896 - (case take_prefix (fn (c',_) => c' <> c) constrs of
1.1897 - (_, []) =>
1.1898 - None (* unknown constructor *)
1.1899 - | (prevs, _) =>
1.1900 - if null params then
1.1901 - let
1.1902 - val typ_assoc = dtyps ~~ Ts
1.1903 - val offset = sum (map (fn (_,ds) =>
1.1904 - product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) prevs)
1.1905 - val (i,_,_) = interpret thy model args (Free ("<IDT>", T))
1.1906 - (* int * interpretation -> int * interpretation *)
1.1907 - fun replace (offset, Leaf xs) =
1.1908 - (* replace the offset-th element by True, all others by False, inc. offset by 1 *)
1.1909 - (offset+1, Leaf (snd (foldl_map (fn (n,_) => (n+1, if n=offset then True else False)) (0, xs))))
1.1910 - | replace (offset, Node xs) =
1.1911 - let
1.1912 - val (offset', xs') = foldl_map replace (offset, xs)
1.1913 - in
1.1914 - (offset', Node xs')
1.1915 - end
1.1916 - val (_,intr) = replace (offset, i)
1.1917 - in
1.1918 - Some (intr, model, args)
1.1919 - end
1.1920 - else
1.1921 - apply_interpreter thy model args t) (* avoid unfolding by calling 'apply_interpreter' directly *)
1.1922 - end
1.1923 - | None => None)
1.1924 - | _ => None)
1.1925 - | _ => None)
1.1926 - end
1.1927 - end;
1.1928 -
1.1929 -
1.1930 (* ------------------------------------------------------------------------- *)
1.1931 -(* PRINTERS *)
1.1932 +(* make_constants: returns all interpretations that have the same tree *)
1.1933 +(* structure as 'intr', but consist of unit vectors with *)
1.1934 +(* 'True'/'False' only (no Boolean variables) *)
1.1935 (* ------------------------------------------------------------------------- *)
1.1936
1.1937 - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
1.1938 + (* interpretation -> interpretation list *)
1.1939
1.1940 - fun var_typevar_printer thy model t intr assignment =
1.1941 - let
1.1942 - fun is_var (Free _) = true
1.1943 - | is_var (Var _) = true
1.1944 - | is_var _ = false
1.1945 - fun typeof (Free (_,T)) = T
1.1946 - | typeof (Var (_,T)) = T
1.1947 - | typeof _ = raise REFUTE ("var_typevar_printer", "term is not a variable")
1.1948 - fun is_typevar (TFree _) = true
1.1949 - | is_typevar (TVar _) = true
1.1950 - | is_typevar _ = false
1.1951 - in
1.1952 - if is_var t andalso is_typevar (typeof t) then
1.1953 - let
1.1954 - (* interpretation -> int *)
1.1955 - fun index_from_interpretation (Leaf xs) =
1.1956 - let
1.1957 - val idx = find_index (PropLogic.eval assignment) xs
1.1958 - in
1.1959 - if idx<0 then
1.1960 - raise REFUTE ("var_typevar_printer", "illegal interpretation: no value assigned")
1.1961 - else
1.1962 - idx
1.1963 - end
1.1964 - | index_from_interpretation _ =
1.1965 - raise REFUTE ("var_typevar_printer", "interpretation is not a leaf")
1.1966 - (* string -> string *)
1.1967 - fun strip_leading_quote s =
1.1968 - (implode o (fn (x::xs) => if x="'" then xs else (x::xs)) o explode) s
1.1969 - (* Term.typ -> string *)
1.1970 - fun string_of_typ (TFree (x,_)) = strip_leading_quote x
1.1971 - | string_of_typ (TVar ((x,i),_)) = strip_leading_quote x ^ string_of_int i
1.1972 - | string_of_typ _ = raise REFUTE ("var_typevar_printer", "type is not a type variable")
1.1973 - in
1.1974 - Some (string_of_typ (typeof t) ^ string_of_int (index_from_interpretation intr))
1.1975 - end
1.1976 - else
1.1977 - None
1.1978 - end;
1.1979 -
1.1980 - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
1.1981 -
1.1982 - fun var_funtype_printer thy model t intr assignment =
1.1983 + fun make_constants intr =
1.1984 let
1.1985 - fun is_var (Free _) = true
1.1986 - | is_var (Var _) = true
1.1987 - | is_var _ = false
1.1988 - fun typeof (Free (_,T)) = T
1.1989 - | typeof (Var (_,T)) = T
1.1990 - | typeof _ = raise REFUTE ("var_funtype_printer", "term is not a variable")
1.1991 - fun is_funtype (Type ("fun", [_,_])) = true
1.1992 - | is_funtype _ = false
1.1993 - in
1.1994 - if is_var t andalso is_funtype (typeof t) then
1.1995 - let
1.1996 - val T1 = domain_type (typeof t)
1.1997 - val T2 = range_type (typeof t)
1.1998 - val (sizes, _) = model
1.1999 - (* create all constants of type T1 *)
1.2000 - val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_funtype_printer", T1))
1.2001 - (* returns a list with all unit vectors of length n *)
1.2002 - (* int -> interpretation list *)
1.2003 - fun unit_vectors n =
1.2004 - let
1.2005 - (* returns the k-th unit vector of length n *)
1.2006 - (* int * int -> interpretation *)
1.2007 - fun unit_vector (k,n) =
1.2008 - Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.2009 - (* int -> interpretation list -> interpretation list *)
1.2010 - fun unit_vectors_acc k vs =
1.2011 - if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
1.2012 - in
1.2013 - unit_vectors_acc 1 []
1.2014 - end
1.2015 - (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.2016 - (* 'a -> 'a list list -> 'a list list *)
1.2017 - fun cons_list x xss =
1.2018 - map (fn xs => x::xs) xss
1.2019 - (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
1.2020 - (* int -> 'a list -> 'a list list *)
1.2021 - fun pick_all 1 xs =
1.2022 - map (fn x => [x]) xs
1.2023 - | pick_all n xs =
1.2024 - let val rec_pick = pick_all (n-1) xs in
1.2025 - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.2026 - end
1.2027 - (* interpretation -> interpretation list *)
1.2028 - fun make_constants (Leaf xs) =
1.2029 - unit_vectors (length xs)
1.2030 - | make_constants (Node xs) =
1.2031 - map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.2032 - (* interpretation list *)
1.2033 - val results = (case intr of
1.2034 - Node xs => xs
1.2035 - | _ => raise REFUTE ("var_funtype_printer", "interpretation is a leaf"))
1.2036 - (* string list *)
1.2037 - val strings = map
1.2038 - (fn (argi,resulti) => print thy model (Free ("var_funtype_printer", T1)) argi assignment
1.2039 - ^ "\\<mapsto>"
1.2040 - ^ print thy model (Free ("var_funtype_printer", T2)) resulti assignment)
1.2041 - ((make_constants i) ~~ results)
1.2042 - in
1.2043 - Some (enclose "(" ")" (commas strings))
1.2044 - end
1.2045 - else
1.2046 - None
1.2047 - end;
1.2048 -
1.2049 - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
1.2050 -
1.2051 - fun var_settype_printer thy model t intr assignment =
1.2052 - let
1.2053 - val (sizes, _) = model
1.2054 (* returns a list with all unit vectors of length n *)
1.2055 (* int -> interpretation list *)
1.2056 fun unit_vectors n =
1.2057 @@ -1575,205 +1040,875 @@
1.2058 let val rec_pick = pick_all (n-1) xs in
1.2059 foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.2060 end
1.2061 - (* interpretation -> interpretation list *)
1.2062 - fun make_constants (Leaf xs) =
1.2063 - unit_vectors (length xs)
1.2064 - | make_constants (Node xs) =
1.2065 - map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.2066 + in
1.2067 + case intr of
1.2068 + Leaf xs => unit_vectors (length xs)
1.2069 + | Node xs => map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.2070 + end;
1.2071 +
1.2072 +(* ------------------------------------------------------------------------- *)
1.2073 +(* size_of_type: returns the number of constants in a type (i.e. 'length *)
1.2074 +(* (make_constants intr)', but implemented more efficiently) *)
1.2075 +(* ------------------------------------------------------------------------- *)
1.2076 +
1.2077 + (* interpretation -> int *)
1.2078 +
1.2079 + fun size_of_type intr =
1.2080 + let
1.2081 + (* power(a,b) computes a^b, for a>=0, b>=0 *)
1.2082 + (* int * int -> int *)
1.2083 + fun power (a,0) = 1
1.2084 + | power (a,1) = a
1.2085 + | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
1.2086 + in
1.2087 + case intr of
1.2088 + Leaf xs => length xs
1.2089 + | Node xs => power (size_of_type (hd xs), length xs)
1.2090 + end;
1.2091 +
1.2092 +(* ------------------------------------------------------------------------- *)
1.2093 +(* TT/FF: interpretations that denote "true" or "false", respectively *)
1.2094 +(* ------------------------------------------------------------------------- *)
1.2095 +
1.2096 + (* interpretation *)
1.2097 +
1.2098 + val TT = Leaf [True, False];
1.2099 +
1.2100 + val FF = Leaf [False, True];
1.2101 +
1.2102 +(* ------------------------------------------------------------------------- *)
1.2103 +(* make_equality: returns an interpretation that denotes (extensional) *)
1.2104 +(* equality of two interpretations *)
1.2105 +(* ------------------------------------------------------------------------- *)
1.2106 +
1.2107 + (* We could in principle represent '=' on a type T by a particular *)
1.2108 + (* interpretation. However, the size of that interpretation is quadratic *)
1.2109 + (* in the size of T. Therefore comparing the interpretations 'i1' and *)
1.2110 + (* 'i2' directly is more efficient than constructing the interpretation *)
1.2111 + (* for equality on T first, and "applying" this interpretation to 'i1' *)
1.2112 + (* and 'i2' in the usual way (cf. 'interpretation_apply') then. *)
1.2113 +
1.2114 + (* interpretation * interpretation -> interpretation *)
1.2115 +
1.2116 + fun make_equality (i1, i2) =
1.2117 + let
1.2118 + (* interpretation * interpretation -> prop_formula *)
1.2119 + fun equal (i1, i2) =
1.2120 + (case i1 of
1.2121 + Leaf xs =>
1.2122 + (case i2 of
1.2123 + Leaf ys => PropLogic.dot_product (xs, ys)
1.2124 + | Node _ => raise REFUTE ("make_equality", "second interpretation is higher"))
1.2125 + | Node xs =>
1.2126 + (case i2 of
1.2127 + Leaf _ => raise REFUTE ("make_equality", "first interpretation is higher")
1.2128 + | Node ys => PropLogic.all (map equal (xs ~~ ys))))
1.2129 + (* interpretation * interpretation -> prop_formula *)
1.2130 + fun not_equal (i1, i2) =
1.2131 + (case i1 of
1.2132 + Leaf xs =>
1.2133 + (case i2 of
1.2134 + Leaf ys => PropLogic.all ((PropLogic.exists xs) :: (PropLogic.exists ys) ::
1.2135 + (map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys))) (* defined and not equal *)
1.2136 + | Node _ => raise REFUTE ("make_equality", "second interpretation is higher"))
1.2137 + | Node xs =>
1.2138 + (case i2 of
1.2139 + Leaf _ => raise REFUTE ("make_equality", "first interpretation is higher")
1.2140 + | Node ys => PropLogic.exists (map not_equal (xs ~~ ys))))
1.2141 in
1.2142 + (* a value may be undefined; therefore 'not_equal' is not just the *)
1.2143 + (* negation of 'equal': *)
1.2144 + (* - two interpretations are 'equal' iff they are both defined and *)
1.2145 + (* denote the same value *)
1.2146 + (* - two interpretations are 'not_equal' iff they are both defined at *)
1.2147 + (* least partially, and a defined part denotes different values *)
1.2148 + (* - an undefined interpretation is neither 'equal' nor 'not_equal' to *)
1.2149 + (* another value *)
1.2150 + Leaf [equal (i1, i2), not_equal (i1, i2)]
1.2151 + end;
1.2152 +
1.2153 +
1.2154 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.2155 +
1.2156 + (* simply typed lambda calculus: Isabelle's basic term syntax, with type *)
1.2157 + (* variables, function types, and propT *)
1.2158 +
1.2159 + fun stlc_interpreter thy model args t =
1.2160 + let
1.2161 + val (typs, terms) = model
1.2162 + val {maxvars, next_idx, bounds, wellformed} = args
1.2163 + (* Term.typ -> (interpretation * model * arguments) option *)
1.2164 + fun interpret_groundterm T =
1.2165 + let
1.2166 + (* unit -> (interpretation * model * arguments) option *)
1.2167 + fun interpret_groundtype () =
1.2168 + let
1.2169 + val size = (if T = Term.propT then 2 else (the o assoc) (typs, T)) (* the model MUST specify a size for ground types *)
1.2170 + val next = (if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 2 *)
1.2171 + val _ = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *)
1.2172 + (* prop_formula list *)
1.2173 + val fms = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
1.2174 + else (map BoolVar (next_idx upto (next_idx+size-1))))
1.2175 + (* interpretation *)
1.2176 + val intr = Leaf fms
1.2177 + (* prop_formula list -> prop_formula *)
1.2178 + fun one_of_two_false [] = True
1.2179 + | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false xs)
1.2180 + (* prop_formula list -> prop_formula *)
1.2181 + fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
1.2182 + (* prop_formula *)
1.2183 + val wf = (if size=2 then True else exactly_one_true fms)
1.2184 + in
1.2185 + (* extend the model, increase 'next_idx', add well-formedness condition *)
1.2186 + Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
1.2187 + end
1.2188 + in
1.2189 + case T of
1.2190 + Type ("fun", [T1, T2]) =>
1.2191 + let
1.2192 + (* we create 'size_of_type (interpret (... T1))' different copies *)
1.2193 + (* of the interpretation for 'T2', which are then combined into a *)
1.2194 + (* single new interpretation *)
1.2195 + val (i1, _, _) =
1.2196 + (interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
1.2197 + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2198 + (* make fresh copies, with different variable indices *)
1.2199 + (* 'idx': next variable index *)
1.2200 + (* 'n' : number of copies *)
1.2201 + (* int -> int -> (int * interpretation list * prop_formula *)
1.2202 + fun make_copies idx 0 =
1.2203 + (idx, [], True)
1.2204 + | make_copies idx n =
1.2205 + let
1.2206 + val (copy, _, new_args) =
1.2207 + (interpret thy (typs, []) {maxvars = maxvars, next_idx = idx, bounds = [], wellformed = True} (Free ("dummy", T2))
1.2208 + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2209 + val (idx', copies, wf') = make_copies (#next_idx new_args) (n-1)
1.2210 + in
1.2211 + (idx', copy :: copies, SAnd (#wellformed new_args, wf'))
1.2212 + end
1.2213 + val (next, copies, wf) = make_copies next_idx (size_of_type i1)
1.2214 + (* combine copies into a single interpretation *)
1.2215 + val intr = Node copies
1.2216 + in
1.2217 + (* extend the model, increase 'next_idx', add well-formedness condition *)
1.2218 + Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
1.2219 + end
1.2220 + | Type _ => interpret_groundtype ()
1.2221 + | TFree _ => interpret_groundtype ()
1.2222 + | TVar _ => interpret_groundtype ()
1.2223 + end
1.2224 + in
1.2225 + case assoc (terms, t) of
1.2226 + Some intr =>
1.2227 + (* return an existing interpretation *)
1.2228 + Some (intr, model, args)
1.2229 + | None =>
1.2230 + (case t of
1.2231 + Const (_, T) =>
1.2232 + interpret_groundterm T
1.2233 + | Free (_, T) =>
1.2234 + interpret_groundterm T
1.2235 + | Var (_, T) =>
1.2236 + interpret_groundterm T
1.2237 + | Bound i =>
1.2238 + Some (nth_elem (i, #bounds args), model, args)
1.2239 + | Abs (x, T, body) =>
1.2240 + let
1.2241 + (* create all constants of type 'T' *)
1.2242 + val (i, _, _) =
1.2243 + (interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
1.2244 + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2245 + val constants = make_constants i
1.2246 + (* interpret the 'body' separately for each constant *)
1.2247 + val ((model', args'), bodies) = foldl_map
1.2248 + (fn ((m,a), c) =>
1.2249 + let
1.2250 + (* add 'c' to 'bounds' *)
1.2251 + val (i', m', a') = interpret thy m {maxvars = #maxvars a, next_idx = #next_idx a, bounds = (c :: #bounds a), wellformed = #wellformed a} body
1.2252 + in
1.2253 + (* keep the new model m' and 'next_idx' and 'wellformed', but use old 'bounds' *)
1.2254 + ((m', {maxvars = maxvars, next_idx = #next_idx a', bounds = bounds, wellformed = #wellformed a'}), i')
1.2255 + end)
1.2256 + ((model, args), constants)
1.2257 + in
1.2258 + Some (Node bodies, model', args')
1.2259 + end
1.2260 + | t1 $ t2 =>
1.2261 + let
1.2262 + (* auxiliary functions *)
1.2263 + (* interpretation * interpretation -> interpretation *)
1.2264 + fun interpretation_disjunction (tr1,tr2) =
1.2265 + tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
1.2266 + (* prop_formula * interpretation -> interpretation *)
1.2267 + fun prop_formula_times_interpretation (fm,tr) =
1.2268 + tree_map (map (fn x => SAnd (fm,x))) tr
1.2269 + (* prop_formula list * interpretation list -> interpretation *)
1.2270 + fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
1.2271 + prop_formula_times_interpretation (fm,tr)
1.2272 + | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
1.2273 + interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees))
1.2274 + | prop_formula_list_dot_product_interpretation_list (_,_) =
1.2275 + raise REFUTE ("stlc_interpreter", "empty list (in dot product)")
1.2276 + (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.2277 + (* 'a -> 'a list list -> 'a list list *)
1.2278 + fun cons_list x xss =
1.2279 + map (fn xs => x::xs) xss
1.2280 + (* returns a list of lists, each one consisting of one element from each element of 'xss' *)
1.2281 + (* 'a list list -> 'a list list *)
1.2282 + fun pick_all [xs] =
1.2283 + map (fn x => [x]) xs
1.2284 + | pick_all (xs::xss) =
1.2285 + let val rec_pick = pick_all xss in
1.2286 + foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.2287 + end
1.2288 + | pick_all _ =
1.2289 + raise REFUTE ("stlc_interpreter", "empty list (in pick_all)")
1.2290 + (* interpretation -> prop_formula list *)
1.2291 + fun interpretation_to_prop_formula_list (Leaf xs) =
1.2292 + xs
1.2293 + | interpretation_to_prop_formula_list (Node trees) =
1.2294 + map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees))
1.2295 + (* interpretation * interpretation -> interpretation *)
1.2296 + fun interpretation_apply (tr1,tr2) =
1.2297 + (case tr1 of
1.2298 + Leaf _ =>
1.2299 + raise REFUTE ("stlc_interpreter", "first interpretation is a leaf")
1.2300 + | Node xs =>
1.2301 + prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list tr2, xs))
1.2302 + (* interpret 't1' and 't2' separately *)
1.2303 + val (intr1, model1, args1) = interpret thy model args t1
1.2304 + val (intr2, model2, args2) = interpret thy model1 args1 t2
1.2305 + in
1.2306 + Some (interpretation_apply (intr1,intr2), model2, args2)
1.2307 + end)
1.2308 + end;
1.2309 +
1.2310 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.2311 +
1.2312 + fun Pure_interpreter thy model args t =
1.2313 case t of
1.2314 - Free (x, Type ("set", [T])) =>
1.2315 + Const ("all", _) $ t1 => (* in the meta-logic, 'all' MUST be followed by an argument term *)
1.2316 + let
1.2317 + val (i, m, a) = interpret thy model args t1
1.2318 + in
1.2319 + case i of
1.2320 + Node xs =>
1.2321 + let
1.2322 + val fmTrue = PropLogic.all (map toTrue xs)
1.2323 + val fmFalse = PropLogic.exists (map toFalse xs)
1.2324 + in
1.2325 + Some (Leaf [fmTrue, fmFalse], m, a)
1.2326 + end
1.2327 + | _ =>
1.2328 + raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function")
1.2329 + end
1.2330 + | Const ("==", _) $ t1 $ t2 =>
1.2331 + let
1.2332 + val (i1, m1, a1) = interpret thy model args t1
1.2333 + val (i2, m2, a2) = interpret thy m1 a1 t2
1.2334 + in
1.2335 + Some (make_equality (i1, i2), m2, a2)
1.2336 + end
1.2337 + | Const ("==>", _) => (* simpler than translating 'Const ("==>", _) $ t1 $ t2' *)
1.2338 + Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
1.2339 + | _ => None;
1.2340 +
1.2341 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.2342 +
1.2343 + fun HOLogic_interpreter thy model args t =
1.2344 + let
1.2345 + (* Term.term -> int -> Term.term *)
1.2346 + fun eta_expand t i =
1.2347 + let
1.2348 + val Ts = binder_types (fastype_of t)
1.2349 + in
1.2350 + foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
1.2351 + (take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
1.2352 + end
1.2353 + in
1.2354 + (* ------------------------------------------------------------------------- *)
1.2355 + (* Providing interpretations directly is more efficient than unfolding the *)
1.2356 + (* logical constants. IN HOL however, logical constants can themselves be *)
1.2357 + (* arguments. "All" and "Ex" are then translated just like any other *)
1.2358 + (* constant, with the relevant axiom being added by 'collect_axioms'. *)
1.2359 + (* ------------------------------------------------------------------------- *)
1.2360 + case t of
1.2361 + Const ("Trueprop", _) =>
1.2362 + Some (Node [TT, FF], model, args)
1.2363 + | Const ("Not", _) =>
1.2364 + Some (Node [FF, TT], model, args)
1.2365 + | Const ("True", _) => (* redundant, since 'True' is also an IDT constructor *)
1.2366 + Some (TT, model, args)
1.2367 + | Const ("False", _) => (* redundant, since 'False' is also an IDT constructor *)
1.2368 + Some (FF, model, args)
1.2369 + | Const ("All", _) $ t1 =>
1.2370 let
1.2371 - (* interpretation list *)
1.2372 - val results = (case intr of
1.2373 - Node xs => xs
1.2374 - | _ => raise REFUTE ("var_settype_printer", "interpretation is a leaf"))
1.2375 - (* create all constants of type T *)
1.2376 - val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T))
1.2377 - (* string list *)
1.2378 - val strings = mapfilter
1.2379 - (fn (argi,Leaf [fmTrue,fmFalse]) =>
1.2380 - if PropLogic.eval assignment fmTrue then
1.2381 - Some (print thy model (Free ("x", T)) argi assignment)
1.2382 - else if PropLogic.eval assignment fmFalse then
1.2383 - None
1.2384 + val (i, m, a) = interpret thy model args t1
1.2385 + in
1.2386 + case i of
1.2387 + Node xs =>
1.2388 + let
1.2389 + val fmTrue = PropLogic.all (map toTrue xs)
1.2390 + val fmFalse = PropLogic.exists (map toFalse xs)
1.2391 + in
1.2392 + Some (Leaf [fmTrue, fmFalse], m, a)
1.2393 + end
1.2394 + | _ =>
1.2395 + raise REFUTE ("HOLogic_interpreter", "\"All\" is not followed by a function")
1.2396 + end
1.2397 + | Const ("Ex", _) $ t1 =>
1.2398 + let
1.2399 + val (i, m, a) = interpret thy model args t1
1.2400 + in
1.2401 + case i of
1.2402 + Node xs =>
1.2403 + let
1.2404 + val fmTrue = PropLogic.exists (map toTrue xs)
1.2405 + val fmFalse = PropLogic.all (map toFalse xs)
1.2406 + in
1.2407 + Some (Leaf [fmTrue, fmFalse], m, a)
1.2408 + end
1.2409 + | _ =>
1.2410 + raise REFUTE ("HOLogic_interpreter", "\"Ex\" is not followed by a function")
1.2411 + end
1.2412 + | Const ("op =", _) $ t1 $ t2 =>
1.2413 + let
1.2414 + val (i1, m1, a1) = interpret thy model args t1
1.2415 + val (i2, m2, a2) = interpret thy m1 a1 t2
1.2416 + in
1.2417 + Some (make_equality (i1, i2), m2, a2)
1.2418 + end
1.2419 + | Const ("op =", _) $ t1 =>
1.2420 + (Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2421 + | Const ("op =", _) =>
1.2422 + (Some (interpret thy model args (eta_expand t 2)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2423 + | Const ("op &", _) =>
1.2424 + Some (Node [Node [TT, FF], Node [FF, FF]], model, args)
1.2425 + | Const ("op |", _) =>
1.2426 + Some (Node [Node [TT, TT], Node [TT, FF]], model, args)
1.2427 + | Const ("op -->", _) =>
1.2428 + Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
1.2429 + | _ => None
1.2430 + end;
1.2431 +
1.2432 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.2433 +
1.2434 + fun set_interpreter thy model args t =
1.2435 + (* "T set" is isomorphic to "T --> bool" *)
1.2436 + let
1.2437 + val (typs, terms) = model
1.2438 + (* Term.term -> int -> Term.term *)
1.2439 + fun eta_expand t i =
1.2440 + let
1.2441 + val Ts = binder_types (fastype_of t)
1.2442 + in
1.2443 + foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
1.2444 + (take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
1.2445 + end
1.2446 + in
1.2447 + case assoc (terms, t) of
1.2448 + Some intr =>
1.2449 + (* return an existing interpretation *)
1.2450 + Some (intr, model, args)
1.2451 + | None =>
1.2452 + (case t of
1.2453 + Free (x, Type ("set", [T])) =>
1.2454 + (let
1.2455 + val (intr, _, args') = interpret thy (typs, []) args (Free (x, T --> HOLogic.boolT))
1.2456 + in
1.2457 + Some (intr, (typs, (t, intr)::terms), args')
1.2458 + end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2459 + | Var ((x,i), Type ("set", [T])) =>
1.2460 + (let
1.2461 + val (intr, _, args') = interpret thy (typs, []) args (Var ((x,i), T --> HOLogic.boolT))
1.2462 + in
1.2463 + Some (intr, (typs, (t, intr)::terms), args')
1.2464 + end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2465 + | Const (s, Type ("set", [T])) =>
1.2466 + (let
1.2467 + val (intr, _, args') = interpret thy (typs, []) args (Const (s, T --> HOLogic.boolT))
1.2468 + in
1.2469 + Some (intr, (typs, (t, intr)::terms), args')
1.2470 + end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2471 + (* 'Collect' == identity *)
1.2472 + | Const ("Collect", _) $ t1 =>
1.2473 + Some (interpret thy model args t1)
1.2474 + | Const ("Collect", _) =>
1.2475 + (Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2476 + (* 'op :' == application *)
1.2477 + | Const ("op :", _) $ t1 $ t2 =>
1.2478 + Some (interpret thy model args (t2 $ t1))
1.2479 + | Const ("op :", _) $ t1 =>
1.2480 + (Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2481 + | Const ("op :", _) =>
1.2482 + (Some (interpret thy model args (eta_expand t 2)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2483 + | _ => None)
1.2484 + end;
1.2485 +
1.2486 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.2487 +
1.2488 + fun IDT_interpreter thy model args t =
1.2489 + let
1.2490 + val (typs, terms) = model
1.2491 + (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
1.2492 + fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
1.2493 + (* replace a 'DtTFree' variable by the associated type *)
1.2494 + (the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
1.2495 + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
1.2496 + let
1.2497 + val (s, ds, _) = (the o assoc) (descr, i)
1.2498 + in
1.2499 + Type (s, map (typ_of_dtyp descr typ_assoc) ds)
1.2500 + end
1.2501 + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
1.2502 + Type (s, map (typ_of_dtyp descr typ_assoc) ds)
1.2503 + (* int list -> int *)
1.2504 + fun sum xs = foldl op+ (0, xs)
1.2505 + (* int list -> int *)
1.2506 + fun product xs = foldl op* (1, xs)
1.2507 + (* the size of an IDT is the sum (over its constructors) of the *)
1.2508 + (* product (over their arguments) of the size of the argument type *)
1.2509 + (* (Term.typ * int) list -> DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> (string * DatatypeAux.dtyp list) list -> int *)
1.2510 + fun size_of_dtyp typs descr typ_assoc constrs =
1.2511 + sum (map (fn (_, ds) =>
1.2512 + product (map (fn d =>
1.2513 + let
1.2514 + val T = typ_of_dtyp descr typ_assoc d
1.2515 + val (i, _, _) =
1.2516 + (interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
1.2517 + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2518 + in
1.2519 + size_of_type i
1.2520 + end) ds)) constrs)
1.2521 + (* Term.typ -> (interpretation * model * arguments) option *)
1.2522 + fun interpret_variable (Type (s, Ts)) =
1.2523 + (case DatatypePackage.datatype_info thy s of
1.2524 + Some info => (* inductive datatype *)
1.2525 + let
1.2526 + val (typs, terms) = model
1.2527 + (* int option -- only recursive IDTs have an associated depth *)
1.2528 + val depth = assoc (typs, Type (s, Ts))
1.2529 + in
1.2530 + if depth = (Some 0) then (* termination condition to avoid infinite recursion *)
1.2531 + (* return a leaf of size 0 *)
1.2532 + Some (Leaf [], model, args)
1.2533 + else
1.2534 + let
1.2535 + val index = #index info
1.2536 + val descr = #descr info
1.2537 + val (_, dtyps, constrs) = (the o assoc) (descr, index)
1.2538 + val typ_assoc = dtyps ~~ Ts
1.2539 + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
1.2540 + val _ = (if Library.exists (fn d =>
1.2541 + case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
1.2542 + then
1.2543 + raise REFUTE ("IDT_interpreter", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable")
1.2544 + else
1.2545 + ())
1.2546 + (* if the model specifies a depth for the current type, decrement it to avoid infinite recursion *)
1.2547 + val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s, Ts), n-1)))
1.2548 + (* recursively compute the size of the datatype *)
1.2549 + val size = size_of_dtyp typs' descr typ_assoc constrs
1.2550 + val next_idx = #next_idx args
1.2551 + val next = (if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 2 *)
1.2552 + val _ = (if next-1>(#maxvars args) andalso (#maxvars args)>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *)
1.2553 + (* prop_formula list *)
1.2554 + val fms = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
1.2555 + else (map BoolVar (next_idx upto (next_idx+size-1))))
1.2556 + (* interpretation *)
1.2557 + val intr = Leaf fms
1.2558 + (* prop_formula list -> prop_formula *)
1.2559 + fun one_of_two_false [] = True
1.2560 + | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false xs)
1.2561 + (* prop_formula list -> prop_formula *)
1.2562 + fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
1.2563 + (* prop_formula *)
1.2564 + val wf = (if size=2 then True else exactly_one_true fms)
1.2565 + in
1.2566 + (* extend the model, increase 'next_idx', add well-formedness condition *)
1.2567 + Some (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, next_idx = next, bounds = #bounds args, wellformed = SAnd (#wellformed args, wf)})
1.2568 + end
1.2569 + end
1.2570 + | None => (* not an inductive datatype *)
1.2571 + None)
1.2572 + | interpret_variable _ = (* a (free or schematic) type variable *)
1.2573 + None
1.2574 + in
1.2575 + case assoc (terms, t) of
1.2576 + Some intr =>
1.2577 + (* return an existing interpretation *)
1.2578 + Some (intr, model, args)
1.2579 + | None =>
1.2580 + (case t of
1.2581 + Free (_, T) => interpret_variable T
1.2582 + | Var (_, T) => interpret_variable T
1.2583 + | Const (s, T) =>
1.2584 + (* TODO: case, recursion, size *)
1.2585 + let
1.2586 + (* unit -> (interpretation * model * arguments) option *)
1.2587 + fun interpret_constructor () =
1.2588 + (case body_type T of
1.2589 + Type (s', Ts') =>
1.2590 + (case DatatypePackage.datatype_info thy s' of
1.2591 + Some info => (* body type is an inductive datatype *)
1.2592 + let
1.2593 + val index = #index info
1.2594 + val descr = #descr info
1.2595 + val (_, dtyps, constrs) = (the o assoc) (descr, index)
1.2596 + val typ_assoc = dtyps ~~ Ts'
1.2597 + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
1.2598 + val _ = (if Library.exists (fn d =>
1.2599 + case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
1.2600 + then
1.2601 + raise REFUTE ("IDT_interpreter", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s', Ts')) ^ ") is not a variable")
1.2602 + else
1.2603 + ())
1.2604 + (* split the constructors into those occuring before/after 'Const (s, T)' *)
1.2605 + val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
1.2606 + not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy), T,
1.2607 + map (typ_of_dtyp descr typ_assoc) ctypes ---> Type (s', Ts')))) constrs
1.2608 + in
1.2609 + case constrs2 of
1.2610 + [] =>
1.2611 + (* 'Const (s, T)' is not a constructor of this datatype *)
1.2612 + None
1.2613 + | c::cs =>
1.2614 + let
1.2615 + (* int option -- only recursive IDTs have an associated depth *)
1.2616 + val depth = assoc (typs, Type (s', Ts'))
1.2617 + val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s', Ts'), n-1)))
1.2618 + (* constructors before 'Const (s, T)' generate elements of the datatype *)
1.2619 + val offset = size_of_dtyp typs' descr typ_assoc constrs1
1.2620 + (* 'Const (s, T)' and constructors after it generate elements of the datatype *)
1.2621 + val total = offset + (size_of_dtyp typs' descr typ_assoc constrs2)
1.2622 + (* create an interpretation that corresponds to the constructor 'Const (s, T)' *)
1.2623 + (* by recursion over its argument types *)
1.2624 + (* DatatypeAux.dtyp list -> interpretation *)
1.2625 + fun make_partial [] =
1.2626 + (* all entries of the leaf are 'False' *)
1.2627 + Leaf (replicate total False)
1.2628 + | make_partial (d::ds) =
1.2629 + let
1.2630 + (* compute the "new" size of the type 'd' *)
1.2631 + val T = typ_of_dtyp descr typ_assoc d
1.2632 + val (i, _, _) =
1.2633 + (interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
1.2634 + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2635 + in
1.2636 + (* all entries of the whole subtree are 'False' *)
1.2637 + Node (replicate (size_of_type i) (make_partial ds))
1.2638 + end
1.2639 + (* int * DatatypeAux.dtyp list -> int * interpretation *)
1.2640 + fun make_constr (offset, []) =
1.2641 + if offset<total then
1.2642 + (offset+1, Leaf ((replicate offset False) @ True :: (replicate (total-offset-1) False)))
1.2643 + else
1.2644 + raise REFUTE ("IDT_interpreter", "internal error: offset >= total")
1.2645 + | make_constr (offset, d::ds) =
1.2646 + let
1.2647 + (* compute the "new" and "old" size of the type 'd' *)
1.2648 + val T = typ_of_dtyp descr typ_assoc d
1.2649 + val (i, _, _) =
1.2650 + (interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
1.2651 + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2652 + val (i', _, _) =
1.2653 + (interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
1.2654 + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2655 + val size = size_of_type i
1.2656 + val size' = size_of_type i'
1.2657 + val _ = if size<size' then
1.2658 + raise REFUTE ("IDT_interpreter", "internal error: new size < old size")
1.2659 + else
1.2660 + ()
1.2661 + val (new_offset, intrs) = foldl_map make_constr (offset, replicate size' ds)
1.2662 + in
1.2663 + (* the first size' elements of the type actually yield a result *)
1.2664 + (* element, while the remaining size-size' elements don't *)
1.2665 + (new_offset, Node (intrs @ (replicate (size-size') (make_partial ds))))
1.2666 + end
1.2667 + in
1.2668 + Some ((snd o make_constr) (offset, snd c), model, args)
1.2669 + end
1.2670 + end
1.2671 + | None => (* body type is not an inductive datatype *)
1.2672 + None)
1.2673 + | _ => (* body type is a (free or schematic) type variable *)
1.2674 + None)
1.2675 + in
1.2676 + case interpret_constructor () of
1.2677 + Some x => Some x
1.2678 + | None => interpret_variable T
1.2679 + end
1.2680 + | _ => None)
1.2681 + end;
1.2682 +
1.2683 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.2684 +
1.2685 + (* only an optimization: 'card' could in principle be interpreted with *)
1.2686 + (* interpreters available already (using its definition), but the code *)
1.2687 + (* below is much more efficient *)
1.2688 +
1.2689 + fun Finite_Set_card_interpreter thy model args t =
1.2690 + case t of
1.2691 + Const ("Finite_Set.card", Type ("fun", [Type ("set", [T]), Type ("nat", [])])) =>
1.2692 + let
1.2693 + val (i_nat, _, _) =
1.2694 + (interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
1.2695 + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2696 + val size_nat = size_of_type i_nat
1.2697 + val (i_set, _, _) =
1.2698 + (interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("set", [T])))
1.2699 + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2700 + val constants = make_constants i_set
1.2701 + (* interpretation -> int *)
1.2702 + fun number_of_elements (Node xs) =
1.2703 + foldl (fn (n, x) =>
1.2704 + if x=TT then n+1 else if x=FF then n else raise REFUTE ("Finite_Set_card_interpreter", "interpretation for set type does not yield a Boolean")) (0, xs)
1.2705 + | number_of_elements (Leaf _) =
1.2706 + raise REFUTE ("Finite_Set_card_interpreter", "interpretation for set type is a leaf")
1.2707 + (* takes an interpretation for a set and returns an interpretation for a 'nat' *)
1.2708 + (* interpretation -> interpretation *)
1.2709 + fun card i =
1.2710 + let
1.2711 + val n = number_of_elements i
1.2712 + in
1.2713 + if n<size_nat then
1.2714 + Leaf ((replicate n False) @ True :: (replicate (size_nat-n-1) False))
1.2715 else
1.2716 - raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned"))
1.2717 - ((make_constants i) ~~ results)
1.2718 + Leaf (replicate size_nat False)
1.2719 + end
1.2720 in
1.2721 - Some (enclose "{" "}" (commas strings))
1.2722 + Some (Node (map card constants), model, args)
1.2723 end
1.2724 - | Var ((x,i), Type ("set", [T])) =>
1.2725 + | _ =>
1.2726 + None;
1.2727 +
1.2728 +
1.2729 +(* ------------------------------------------------------------------------- *)
1.2730 +(* PRINTERS *)
1.2731 +(* ------------------------------------------------------------------------- *)
1.2732 +
1.2733 + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option *)
1.2734 +
1.2735 + fun stlc_printer thy model t intr assignment =
1.2736 + let
1.2737 + (* Term.term -> Term.typ option *)
1.2738 + fun typeof (Free (_, T)) = Some T
1.2739 + | typeof (Var (_, T)) = Some T
1.2740 + | typeof (Const (_, T)) = Some T
1.2741 + | typeof _ = None
1.2742 + (* string -> string *)
1.2743 + fun strip_leading_quote s =
1.2744 + (implode o (fn ss => case ss of [] => [] | x::xs => if x="'" then xs else ss) o explode) s
1.2745 + (* Term.typ -> string *)
1.2746 + fun string_of_typ (Type (s, _)) = s
1.2747 + | string_of_typ (TFree (x, _)) = strip_leading_quote x
1.2748 + | string_of_typ (TVar ((x,i), _)) = strip_leading_quote x ^ string_of_int i
1.2749 + (* interpretation -> int *)
1.2750 + fun index_from_interpretation (Leaf xs) =
1.2751 let
1.2752 - (* interpretation list *)
1.2753 - val results = (case intr of
1.2754 - Node xs => xs
1.2755 - | _ => raise REFUTE ("var_settype_printer", "interpretation is a leaf"))
1.2756 - (* create all constants of type T *)
1.2757 - val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T))
1.2758 - (* string list *)
1.2759 - val strings = mapfilter
1.2760 - (fn (argi,Leaf [fmTrue,fmFalse]) =>
1.2761 - if PropLogic.eval assignment fmTrue then
1.2762 - Some (print thy model (Free ("var_settype_printer", T)) argi assignment)
1.2763 - else if PropLogic.eval assignment fmTrue then
1.2764 - None
1.2765 - else
1.2766 - raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned"))
1.2767 - ((make_constants i) ~~ results)
1.2768 + val idx = find_index (PropLogic.eval assignment) xs
1.2769 in
1.2770 - Some (enclose "{" "}" (commas strings))
1.2771 + if idx<0 then
1.2772 + raise REFUTE ("stlc_printer", "illegal interpretation: no value assigned (SAT solver unsound?)")
1.2773 + else
1.2774 + idx
1.2775 end
1.2776 - | _ => None
1.2777 + | index_from_interpretation _ =
1.2778 + raise REFUTE ("stlc_printer", "interpretation for ground type is not a leaf")
1.2779 + in
1.2780 + case typeof t of
1.2781 + Some T =>
1.2782 + (case T of
1.2783 + Type ("fun", [T1, T2]) =>
1.2784 + (let
1.2785 + (* create all constants of type 'T1' *)
1.2786 + val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
1.2787 + val constants = make_constants i
1.2788 + (* interpretation list *)
1.2789 + val results = (case intr of
1.2790 + Node xs => xs
1.2791 + | _ => raise REFUTE ("stlc_printer", "interpretation for function type is a leaf"))
1.2792 + (* Term.term list *)
1.2793 + val pairs = map (fn (arg, result) =>
1.2794 + HOLogic.mk_prod
1.2795 + (print thy model (Free ("dummy", T1)) arg assignment,
1.2796 + print thy model (Free ("dummy", T2)) result assignment))
1.2797 + (constants ~~ results)
1.2798 + (* Term.typ *)
1.2799 + val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
1.2800 + val HOLogic_setT = HOLogic.mk_setT HOLogic_prodT
1.2801 + (* Term.term *)
1.2802 + val HOLogic_empty_set = Const ("{}", HOLogic_setT)
1.2803 + val HOLogic_insert = Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
1.2804 + in
1.2805 + Some (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) (pairs, HOLogic_empty_set))
1.2806 + end handle CANNOT_INTERPRET _ => None)
1.2807 + | Type ("prop", []) =>
1.2808 + (case index_from_interpretation intr of
1.2809 + 0 => Some (HOLogic.mk_Trueprop HOLogic.true_const)
1.2810 + | 1 => Some (HOLogic.mk_Trueprop HOLogic.false_const)
1.2811 + | _ => raise REFUTE ("stlc_interpreter", "illegal interpretation for a propositional value"))
1.2812 + | Type _ => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
1.2813 + | TFree _ => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
1.2814 + | TVar _ => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T)))
1.2815 + | None =>
1.2816 + None
1.2817 end;
1.2818
1.2819 (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
1.2820
1.2821 - fun HOLogic_printer thy model t intr assignment =
1.2822 - case t of
1.2823 - (* 'arbitrary', 'The', 'Hilbert_Choice.Eps' are printed like free variables of the same type *)
1.2824 - Const ("arbitrary", T) =>
1.2825 - Some (print thy model (Free ("<arbitrary>", T)) intr assignment)
1.2826 - | Const ("The", T) =>
1.2827 - Some (print thy model (Free ("<The>", T)) intr assignment)
1.2828 - | Const ("Hilbert_Choice.Eps", T) =>
1.2829 - Some (print thy model (Free ("<Eps>", T)) intr assignment)
1.2830 + fun set_printer thy model t intr assignment =
1.2831 + let
1.2832 + (* Term.term -> Term.typ option *)
1.2833 + fun typeof (Free (_, T)) = Some T
1.2834 + | typeof (Var (_, T)) = Some T
1.2835 + | typeof (Const (_, T)) = Some T
1.2836 + | typeof _ = None
1.2837 + in
1.2838 + case typeof t of
1.2839 + Some (Type ("set", [T])) =>
1.2840 + (let
1.2841 + (* create all constants of type 'T' *)
1.2842 + val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
1.2843 + val constants = make_constants i
1.2844 + (* interpretation list *)
1.2845 + val results = (case intr of
1.2846 + Node xs => xs
1.2847 + | _ => raise REFUTE ("set_printer", "interpretation for set type is a leaf"))
1.2848 + (* Term.term list *)
1.2849 + val elements = mapfilter (fn (arg, result) =>
1.2850 + case result of
1.2851 + Leaf [fmTrue, fmFalse] =>
1.2852 + if PropLogic.eval assignment fmTrue then
1.2853 + Some (print thy model (Free ("dummy", T)) arg assignment)
1.2854 + else if PropLogic.eval assignment fmFalse then
1.2855 + None
1.2856 + else
1.2857 + raise REFUTE ("set_printer", "illegal interpretation: no value assigned (SAT solver unsound?)")
1.2858 + | _ =>
1.2859 + raise REFUTE ("set_printer", "illegal interpretation for a Boolean value"))
1.2860 + (constants ~~ results)
1.2861 + (* Term.typ *)
1.2862 + val HOLogic_setT = HOLogic.mk_setT T
1.2863 + (* Term.term *)
1.2864 + val HOLogic_empty_set = Const ("{}", HOLogic_setT)
1.2865 + val HOLogic_insert = Const ("insert", T --> HOLogic_setT --> HOLogic_setT)
1.2866 + in
1.2867 + Some (foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) (HOLogic_empty_set, elements))
1.2868 + end handle CANNOT_INTERPRET _ => None)
1.2869 | _ =>
1.2870 - None;
1.2871 + None
1.2872 + end;
1.2873
1.2874 - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
1.2875 + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option *)
1.2876
1.2877 - fun var_IDT_printer thy model t intr assignment =
1.2878 + fun IDT_printer thy model t intr assignment =
1.2879 let
1.2880 - fun is_var (Free _) = true
1.2881 - | is_var (Var _) = true
1.2882 - | is_var _ = false
1.2883 - fun typeof (Free (_,T)) = T
1.2884 - | typeof (Var (_,T)) = T
1.2885 - | typeof _ = raise REFUTE ("var_IDT_printer", "term is not a variable")
1.2886 + (* Term.term -> Term.typ option *)
1.2887 + fun typeof (Free (_, T)) = Some T
1.2888 + | typeof (Var (_, T)) = Some T
1.2889 + | typeof (Const (_, T)) = Some T
1.2890 + | typeof _ = None
1.2891 in
1.2892 - if is_var t then
1.2893 - (case typeof t of
1.2894 - Type (s, Ts) =>
1.2895 - (case DatatypePackage.datatype_info thy s of
1.2896 - Some info => (* inductive datatype *)
1.2897 - let
1.2898 - val index = #index info
1.2899 - val descr = #descr info
1.2900 - val (_, dtyps, constrs) = the (assoc (descr, index))
1.2901 + case typeof t of
1.2902 + Some (Type (s, Ts)) =>
1.2903 + (case DatatypePackage.datatype_info thy s of
1.2904 + Some info => (* inductive datatype *)
1.2905 + let
1.2906 + val (typs, _) = model
1.2907 + val index = #index info
1.2908 + val descr = #descr info
1.2909 + val (_, dtyps, constrs) = (the o assoc) (descr, index)
1.2910 + val typ_assoc = dtyps ~~ Ts
1.2911 + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
1.2912 + val _ = (if Library.exists (fn d =>
1.2913 + case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
1.2914 + then
1.2915 + raise REFUTE ("IDT_printer", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable")
1.2916 + else
1.2917 + ())
1.2918 + (* the index of the element in the datatype *)
1.2919 + val element = (case intr of
1.2920 + Leaf xs => find_index (PropLogic.eval assignment) xs
1.2921 + | Node _ => raise REFUTE ("IDT_printer", "interpretation is not a leaf"))
1.2922 + val _ = (if element<0 then raise REFUTE ("IDT_printer", "invalid interpretation (no value assigned)") else ())
1.2923 + (* int option -- only recursive IDTs have an associated depth *)
1.2924 + val depth = assoc (typs, Type (s, Ts))
1.2925 + val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s, Ts), n-1)))
1.2926 + (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
1.2927 + fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
1.2928 + (* replace a 'DtTFree' variable by the associated type *)
1.2929 + (the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
1.2930 + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
1.2931 + let
1.2932 + val (s, ds, _) = (the o assoc) (descr, i)
1.2933 + in
1.2934 + Type (s, map (typ_of_dtyp descr typ_assoc) ds)
1.2935 + end
1.2936 + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
1.2937 + Type (s, map (typ_of_dtyp descr typ_assoc) ds)
1.2938 + (* int list -> int *)
1.2939 + fun sum xs = foldl op+ (0, xs)
1.2940 + (* int list -> int *)
1.2941 + fun product xs = foldl op* (1, xs)
1.2942 + (* the size of an IDT is the sum (over its constructors) of the *)
1.2943 + (* product (over their arguments) of the size of the argument type *)
1.2944 + (* (Term.typ * int) list -> DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> (string * DatatypeAux.dtyp list) list -> int *)
1.2945 + fun size_of_dtyp typs descr typ_assoc xs =
1.2946 + sum (map (fn (_, ds) =>
1.2947 + product (map (fn d =>
1.2948 + let
1.2949 + val T = typ_of_dtyp descr typ_assoc d
1.2950 + val (i, _, _) =
1.2951 + (interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
1.2952 + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2953 in
1.2954 - if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
1.2955 - raise REFUTE ("var_IDT_printer", "recursive datatype argument")
1.2956 - else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
1.2957 - None (* recursive datatype (requires an infinite model) *)
1.2958 + size_of_type i
1.2959 + end) ds)) xs)
1.2960 + (* int -> DatatypeAux.dtyp list -> Term.term list *)
1.2961 + fun make_args n [] =
1.2962 + if n<>0 then
1.2963 + raise REFUTE ("IDT_printer", "error computing the element: remainder is not 0")
1.2964 else
1.2965 + []
1.2966 + | make_args n (d::ds) =
1.2967 let
1.2968 - val (sizes, _) = model
1.2969 - val typ_assoc = dtyps ~~ Ts
1.2970 - (* interpretation -> int *)
1.2971 - fun index_from_interpretation (Leaf xs) =
1.2972 + val dT = typ_of_dtyp descr typ_assoc d
1.2973 + val (i, _, _) =
1.2974 + (interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", dT))
1.2975 + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
1.2976 + val size = size_of_type i
1.2977 + val consts = make_constants i (* we only need the (n mod size)-th element of *)
1.2978 + (* this list, so there might be a more efficient implementation that does not *)
1.2979 + (* generate all constants *)
1.2980 + in
1.2981 + (print thy (typs', []) (Free ("dummy", dT)) (nth_elem (n mod size, consts)) assignment)::(make_args (n div size) ds)
1.2982 + end
1.2983 + (* int -> (string * DatatypeAux.dtyp list) list -> Term.term *)
1.2984 + fun make_term _ [] =
1.2985 + raise REFUTE ("IDT_printer", "invalid interpretation (value too large - not enough constructors)")
1.2986 + | make_term n (c::cs) =
1.2987 + let
1.2988 + val c_size = size_of_dtyp typs' descr typ_assoc [c]
1.2989 + in
1.2990 + if n<c_size then
1.2991 let
1.2992 - val idx = find_index (PropLogic.eval assignment) xs
1.2993 + val (cname, cargs) = c
1.2994 + val c_term = Const (cname, (map (typ_of_dtyp descr typ_assoc) cargs) ---> Type (s, Ts))
1.2995 in
1.2996 - if idx<0 then
1.2997 - raise REFUTE ("var_IDT_printer", "illegal interpretation: no value assigned")
1.2998 - else
1.2999 - idx
1.3000 + foldl op$ (c_term, rev (make_args n (rev cargs)))
1.3001 end
1.3002 - | index_from_interpretation _ =
1.3003 - raise REFUTE ("var_IDT_printer", "interpretation is not a leaf")
1.3004 - (* string -> string *)
1.3005 - fun unqualify s =
1.3006 - implode (snd (take_suffix (fn c => c <> ".") (explode s)))
1.3007 - (* DatatypeAux.dtyp -> Term.typ *)
1.3008 - fun typ_of_dtyp (DatatypeAux.DtTFree a) =
1.3009 - the (assoc (typ_assoc, DatatypeAux.DtTFree a))
1.3010 - | typ_of_dtyp (DatatypeAux.DtRec i) =
1.3011 - raise REFUTE ("var_IDT_printer", "recursive datatype")
1.3012 - | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
1.3013 - Type (s, map typ_of_dtyp ds)
1.3014 - fun sum xs = foldl op+ (0, xs)
1.3015 - fun product xs = foldl op* (1, xs)
1.3016 - (* power(a,b) computes a^b, for a>=0, b>=0 *)
1.3017 - (* int * int -> int *)
1.3018 - fun power (a,0) = 1
1.3019 - | power (a,1) = a
1.3020 - | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
1.3021 - fun size_of_interpretation (Leaf xs) = length xs
1.3022 - | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
1.3023 - fun size_of_type T =
1.3024 - let
1.3025 - val (i,_,_) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<IDT>", T))
1.3026 - in
1.3027 - size_of_interpretation i
1.3028 - end
1.3029 - (* returns a list with all unit vectors of length n *)
1.3030 - (* int -> interpretation list *)
1.3031 - fun unit_vectors n =
1.3032 - let
1.3033 - (* returns the k-th unit vector of length n *)
1.3034 - (* int * int -> interpretation *)
1.3035 - fun unit_vector (k,n) =
1.3036 - Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.3037 - (* int -> interpretation list -> interpretation list *)
1.3038 - fun unit_vectors_acc k vs =
1.3039 - if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
1.3040 - in
1.3041 - unit_vectors_acc 1 []
1.3042 - end
1.3043 - (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.3044 - (* 'a -> 'a list list -> 'a list list *)
1.3045 - fun cons_list x xss =
1.3046 - map (fn xs => x::xs) xss
1.3047 - (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
1.3048 - (* int -> 'a list -> 'a list list *)
1.3049 - fun pick_all 1 xs =
1.3050 - map (fn x => [x]) xs
1.3051 - | pick_all n xs =
1.3052 - let val rec_pick = pick_all (n-1) xs in
1.3053 - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.3054 - end
1.3055 - (* interpretation -> interpretation list *)
1.3056 - fun make_constants (Leaf xs) =
1.3057 - unit_vectors (length xs)
1.3058 - | make_constants (Node xs) =
1.3059 - map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.3060 - (* DatatypeAux.dtyp list -> int -> string *)
1.3061 - fun string_of_inductive_type_cargs [] n =
1.3062 - if n<>0 then
1.3063 - raise REFUTE ("var_IDT_printer", "internal error computing the element index for an inductive type")
1.3064 - else
1.3065 - ""
1.3066 - | string_of_inductive_type_cargs (d::ds) n =
1.3067 - let
1.3068 - val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d)) ds)
1.3069 - val T = typ_of_dtyp d
1.3070 - val (i,_,_) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<IDT>", T))
1.3071 - val constants = make_constants i
1.3072 - in
1.3073 - " "
1.3074 - ^ (print thy model (Free ("<IDT>", T)) (nth_elem (n div size_ds, constants)) assignment)
1.3075 - ^ (string_of_inductive_type_cargs ds (n mod size_ds))
1.3076 - end
1.3077 - (* (string * DatatypeAux.dtyp list) list -> int -> string *)
1.3078 - fun string_of_inductive_type_constrs [] n =
1.3079 - raise REFUTE ("var_IDT_printer", "inductive type has fewer elements than needed")
1.3080 - | string_of_inductive_type_constrs ((c,ds)::cs) n =
1.3081 - let
1.3082 - val size = product (map (fn d => size_of_type (typ_of_dtyp d)) ds)
1.3083 - in
1.3084 - if n < size then
1.3085 - (unqualify c) ^ (string_of_inductive_type_cargs ds n)
1.3086 - else
1.3087 - string_of_inductive_type_constrs cs (n - size)
1.3088 - end
1.3089 - in
1.3090 - Some (string_of_inductive_type_constrs constrs (index_from_interpretation intr))
1.3091 + else
1.3092 + make_term (n-c_size) cs
1.3093 end
1.3094 - end
1.3095 - | None => None)
1.3096 - | _ => None)
1.3097 - else
1.3098 + in
1.3099 + Some (make_term element constrs)
1.3100 + end
1.3101 + | None => (* not an inductive datatype *)
1.3102 + None)
1.3103 + | _ => (* a (free or schematic) type variable *)
1.3104 None
1.3105 end;
1.3106
1.3107 @@ -1786,27 +1921,22 @@
1.3108 (* ------------------------------------------------------------------------- *)
1.3109 (* Note: the interpreters and printers are used in reverse order; however, *)
1.3110 (* an interpreter that can handle non-atomic terms ends up being *)
1.3111 -(* applied before other interpreters are applied to subterms! *)
1.3112 +(* applied before the 'stlc_interpreter' breaks the term apart into *)
1.3113 +(* subterms that are then passed to other interpreters! *)
1.3114 (* ------------------------------------------------------------------------- *)
1.3115
1.3116 (* (theory -> theory) list *)
1.3117
1.3118 val setup =
1.3119 [RefuteData.init,
1.3120 - add_interpreter "var_typevar" var_typevar_interpreter,
1.3121 - add_interpreter "var_funtype" var_funtype_interpreter,
1.3122 - add_interpreter "var_settype" var_settype_interpreter,
1.3123 - add_interpreter "boundvar" boundvar_interpreter,
1.3124 - add_interpreter "abstraction" abstraction_interpreter,
1.3125 - add_interpreter "apply" apply_interpreter,
1.3126 - add_interpreter "const_unfold" const_unfold_interpreter,
1.3127 - add_interpreter "Pure" Pure_interpreter,
1.3128 - add_interpreter "HOLogic" HOLogic_interpreter,
1.3129 - add_interpreter "IDT" IDT_interpreter,
1.3130 - add_printer "var_typevar" var_typevar_printer,
1.3131 - add_printer "var_funtype" var_funtype_printer,
1.3132 - add_printer "var_settype" var_settype_printer,
1.3133 - add_printer "HOLogic" HOLogic_printer,
1.3134 - add_printer "var_IDT" var_IDT_printer];
1.3135 + add_interpreter "stlc" stlc_interpreter,
1.3136 + add_interpreter "Pure" Pure_interpreter,
1.3137 + add_interpreter "HOLogic" HOLogic_interpreter,
1.3138 + add_interpreter "set" set_interpreter,
1.3139 + add_interpreter "IDT" IDT_interpreter,
1.3140 + add_interpreter "Finite_Set.card" Finite_Set_card_interpreter,
1.3141 + add_printer "stlc" stlc_printer,
1.3142 + add_printer "set" set_printer,
1.3143 + add_printer "IDT" IDT_printer];
1.3144
1.3145 end