# HG changeset patch # User webertj # Date 1085587432 -7200 # Node ID e8ccb13d7774d708c3ed682eab32f45eda37c0fb # Parent b42ad431cbae4f55711415ff359e0d7acb371f75 major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them) diff -r b42ad431cbae -r e8ccb13d7774 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Wed May 26 17:43:52 2004 +0200 +++ b/src/HOL/Tools/refute.ML Wed May 26 18:03:52 2004 +0200 @@ -6,10 +6,7 @@ Finite model generation for HOL formulae, using a SAT solver. *) -(* ------------------------------------------------------------------------- *) -(* TODO: Change parameter handling so that only supported parameters can be *) -(* set, and specify defaults here, rather than in HOL/Main.thy. *) -(* ------------------------------------------------------------------------- *) +(* TODO: case, rec, size for IDTs are not supported yet *) (* ------------------------------------------------------------------------- *) (* Declares the 'REFUTE' signature as well as a structure 'Refute'. *) @@ -22,22 +19,23 @@ exception REFUTE of string * string (* ------------------------------------------------------------------------- *) -(* Model/interpretation related code (translation HOL -> boolean formula) *) +(* Model/interpretation related code (translation HOL -> propositional logic *) (* ------------------------------------------------------------------------- *) - exception CANNOT_INTERPRET - + type params type interpretation type model type arguments - val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory - val add_printer : string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory + exception CANNOT_INTERPRET of Term.term + exception MAXVARS_EXCEEDED - val interpret : theory -> model -> arguments -> Term.term -> interpretation * model * arguments (* exception CANNOT_INTERPRET *) - val is_satisfying_model : model -> interpretation -> bool -> PropLogic.prop_formula + val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory + val add_printer : string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option) -> theory -> theory - val print : theory -> model -> Term.term -> interpretation -> (int -> bool) -> string + val interpret : theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) (* exception CANNOT_INTERPRET *) + + val print : theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term val print_model : theory -> model -> (int -> bool) -> string (* ------------------------------------------------------------------------- *) @@ -47,9 +45,9 @@ val set_default_param : (string * string) -> theory -> theory val get_default_param : theory -> string -> string option val get_default_params : theory -> (string * string) list - val actual_params : theory -> (string * string) list -> (int * int * int * string) + val actual_params : theory -> (string * string) list -> params - val find_model : theory -> (int * int * int * string) -> Term.term -> bool -> unit + val find_model : theory -> params -> Term.term -> bool -> unit val satisfy_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model for a formula *) val refute_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model that refutes a formula *) @@ -69,11 +67,11 @@ (* 'error'. *) exception REFUTE of string * string; (* ("in function", "cause") *) -(* ------------------------------------------------------------------------- *) -(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) -(* ------------------------------------------------------------------------- *) + exception CANNOT_INTERPRET of Term.term; - exception CANNOT_INTERPRET; + (* should be raised by an interpreter when more variables would be *) + (* required than allowed by 'maxvars' *) + exception MAXVARS_EXCEEDED; (* ------------------------------------------------------------------------- *) (* TREES *) @@ -115,12 +113,43 @@ | Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)")) | Node xs => (case t2 of - (* '~~' will raise an exception if the number of branches in both trees is different at the current node *) + (* '~~' will raise an exception if the number of branches in *) + (* both trees is different at the current node *) Node ys => Node (map tree_pair (xs ~~ ys)) | Leaf _ => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)")); (* ------------------------------------------------------------------------- *) +(* params: parameters that control the translation into a propositional *) +(* formula/model generation *) +(* *) +(* The following parameters are supported (and required (!), except for *) +(* "sizes"): *) +(* *) +(* Name Type Description *) +(* *) +(* "sizes" (string * int) list *) +(* Size of ground types (e.g. 'a=2), or depth of IDTs. *) +(* "minsize" int If >0, minimal size of each ground type/IDT depth. *) +(* "maxsize" int If >0, maximal size of each ground type/IDT depth. *) +(* "maxvars" int If >0, use at most 'maxvars' Boolean variables *) +(* when transforming the term into a propositional *) +(* formula. *) +(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *) +(* "satsolver" string SAT solver to be used. *) +(* ------------------------------------------------------------------------- *) + + type params = + { + sizes : (string * int) list, + minsize : int, + maxsize : int, + maxvars : int, + maxtime : int, + satsolver: string + }; + +(* ------------------------------------------------------------------------- *) (* interpretation: a term's interpretation is given by a variable of type *) (* 'interpretation' *) (* ------------------------------------------------------------------------- *) @@ -139,9 +168,16 @@ (* ------------------------------------------------------------------------- *) (* arguments: additional arguments required during interpretation of terms *) (* ------------------------------------------------------------------------- *) - + type arguments = - {next_idx: int, bounds: interpretation list, wellformed: prop_formula}; + { + (* just passed unchanged from 'params' *) + maxvars : int, + (* these may change during the translation *) + next_idx : int, + bounds : interpretation list, + wellformed: prop_formula + }; structure RefuteDataArgs = @@ -149,7 +185,7 @@ val name = "HOL/refute"; type T = {interpreters: (string * (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option)) list, - printers: (string * (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option)) list, + printers: (string * (theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option)) list, parameters: string Symtab.table}; val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; val copy = I; @@ -174,97 +210,62 @@ (* interpret: tries to interpret the term 't' using a suitable interpreter; *) (* returns the interpretation and a (possibly extended) model *) (* that keeps track of the interpretation of subterms *) -(* Note: exception 'CANNOT_INTERPRETE' is raised if the term cannot be *) +(* Note: exception 'CANNOT_INTERPRET t' is raised if the term cannot be *) (* interpreted by any interpreter *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> arguments -> Term.term -> interpretation * model * arguments *) + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) *) fun interpret thy model args t = (case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of - None => - (std_output "\n"; warning ("Unable to interpret term:\n" ^ Sign.string_of_term (sign_of thy) t); - raise CANNOT_INTERPRET) + None => raise (CANNOT_INTERPRET t) | Some x => x); (* ------------------------------------------------------------------------- *) -(* print: tries to print the constant denoted by the term 't' using a *) -(* suitable printer *) +(* print: tries to convert the constant denoted by the term 't' into a term *) +(* using a suitable printer *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string *) + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term *) fun print thy model t intr assignment = (case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) of - None => "<>" - | Some s => s); - -(* ------------------------------------------------------------------------- *) -(* is_satisfying_model: returns a propositional formula that is true iff the *) -(* given interpretation denotes 'satisfy', and the model meets certain *) -(* well-formedness properties *) -(* ------------------------------------------------------------------------- *) - - (* model -> interpretation -> bool -> PropLogic.prop_formula *) - - fun is_satisfying_model model intr satisfy = - let - (* prop_formula list -> prop_formula *) - fun oneoutoftwofalse [] = True - | oneoutoftwofalse (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), oneoutoftwofalse xs) - (* prop_formula list -> prop_formula *) - fun exactly1true xs = SAnd (PropLogic.exists xs, oneoutoftwofalse xs) - (* ------------------------------------------------------------------------- *) - (* restrict_to_single_element: returns a propositional formula that is true *) - (* iff the interpretation denotes a single element of its corresponding *) - (* type, i.e. iff at each leaf, one and only one formula is true *) - (* ------------------------------------------------------------------------- *) - (* interpretation -> prop_formula *) - fun restrict_to_single_element (Leaf [BoolVar i, Not (BoolVar j)]) = - if (i=j) then - True (* optimization for boolean variables *) - else - raise REFUTE ("is_satisfying_model", "boolean variables in leaf have different indices") - | restrict_to_single_element (Leaf xs) = - exactly1true xs - | restrict_to_single_element (Node trees) = - PropLogic.all (map restrict_to_single_element trees) - in - (* a term of type 'bool' is represented as a 2-element leaf, where *) - (* the term is true iff the leaf's first element is true, and false *) - (* iff the leaf's second element is true *) - case intr of - Leaf [fmT,fmF] => - (* well-formedness properties and formula 'fmT'/'fmF' *) - SAnd (PropLogic.all (map (restrict_to_single_element o snd) (snd model)), if satisfy then fmT else fmF) - | _ => - raise REFUTE ("is_satisfying_model", "interpretation does not denote a boolean value") - end; + None => Const ("<>", fastype_of t) + | Some x => x); (* ------------------------------------------------------------------------- *) (* print_model: turns the model into a string, using a fixed interpretation *) -(* (given by an assignment for boolean variables) and suitable *) +(* (given by an assignment for Boolean variables) and suitable *) (* printers *) (* ------------------------------------------------------------------------- *) + (* theory -> model -> (int -> bool) -> string *) + fun print_model thy model assignment = let val (typs, terms) = model + val typs_msg = + if null typs then + "empty universe (no type variables in term)\n" + else + "Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs) ^ "\n" + val show_consts_msg = + if not (!show_consts) andalso Library.exists (is_Const o fst) terms then + "set \"show_consts\" to show the interpretation of constants\n" + else + "" + val terms_msg = + if null terms then + "empty interpretation (no free variables in term)\n" + else + space_implode "\n" (mapfilter (fn (t,intr) => + (* print constants only if 'show_consts' is true *) + if (!show_consts) orelse not (is_Const t) then + Some (Sign.string_of_term (sign_of thy) t ^ ": " ^ Sign.string_of_term (sign_of thy) (print thy model t intr assignment)) + else + None) terms) ^ "\n" in - (if null typs then - "empty universe (no type variables in term)" - else - "Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs)) - ^ "\n" - ^ (if null terms then - "empty interpretation (no free variables in term)" - else - space_implode "\n" (map - (fn (t,intr) => - Sign.string_of_term (sign_of thy) t ^ ": " ^ print thy model t intr assignment) - terms) - ) - ^ "\n" + typs_msg ^ show_consts_msg ^ terms_msg end; @@ -283,7 +284,7 @@ | Some _ => error ("Interpreter " ^ name ^ " already declared") end; - (* string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory *) + (* string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option) -> theory -> theory *) fun add_printer name f thy = let @@ -333,25 +334,12 @@ (* ------------------------------------------------------------------------- *) (* actual_params: takes a (possibly empty) list 'params' of parameters that *) (* override the default parameters currently specified in 'thy', and *) -(* returns a tuple that can be passed to 'find_model'. *) -(* *) -(* The following parameters are supported (and required!): *) -(* *) -(* Name Type Description *) -(* *) -(* "minsize" int Only search for models with size at least *) -(* 'minsize'. *) -(* "maxsize" int If >0, only search for models with size at most *) -(* 'maxsize'. *) -(* "maxvars" int If >0, use at most 'maxvars' boolean variables *) -(* when transforming the term into a propositional *) -(* formula. *) -(* "satsolver" string SAT solver to be used. *) +(* returns a record that can be passed to 'find_model'. *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * string) list -> (int * int * int * string) *) + (* theory -> (string * string) list -> params *) - fun actual_params thy params = + fun actual_params thy override = let (* (string * string) list * string -> int *) fun read_int (parms, name) = @@ -366,147 +354,591 @@ Some s => s | None => error ("parameter " ^ quote name ^ " must be assigned a value") (* (string * string) list *) - val allparams = params @ (get_default_params thy) (* 'params' first, defaults last (to override) *) + val allparams = override @ (get_default_params thy) (* 'override' first, defaults last *) (* int *) val minsize = read_int (allparams, "minsize") val maxsize = read_int (allparams, "maxsize") val maxvars = read_int (allparams, "maxvars") + val maxtime = read_int (allparams, "maxtime") (* string *) val satsolver = read_string (allparams, "satsolver") + (* all remaining parameters of the form "string=int" are collected in *) + (* 'sizes' *) + (* TODO: it is currently not possible to specify a size for a type *) + (* whose name is one of the other parameters (e.g. 'maxvars') *) + (* (string * int) list *) + val sizes = mapfilter + (fn (name,value) => (case Int.fromString value of SOME i => Some (name, i) | NONE => None)) + (filter (fn (name,_) => name<>"minsize" andalso name<>"maxsize" andalso name<>"maxvars" andalso name<>"maxtime" andalso name<>"satsolver") + allparams) in - (minsize, maxsize, maxvars, satsolver) + {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars, maxtime=maxtime, satsolver=satsolver} + end; + + +(* ------------------------------------------------------------------------- *) +(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) +(* ------------------------------------------------------------------------- *) + +(* ------------------------------------------------------------------------- *) +(* collect_axioms: collects (monomorphic, universally quantified versions *) +(* of) all HOL axioms that are relevant w.r.t 't' *) +(* ------------------------------------------------------------------------- *) + + (* TODO: to make the collection of axioms more easily extensible, this *) + (* function could be based on user-supplied "axiom collectors", *) + (* similar to 'interpret'/interpreters or 'print'/printers *) + + (* theory -> Term.term -> Term.term list *) + + (* Which axioms are "relevant" for a particular term/type goes hand in *) + (* hand with the interpretation of that term/type by its interpreter (see *) + (* way below): if the interpretation respects an axiom anyway, the axiom *) + (* does not need to be added as a constraint here. *) + + (* When an axiom is added as relevant, further axioms may need to be *) + (* added as well (e.g. when a constant is defined in terms of other *) + (* constants). To avoid infinite recursion (which should not happen for *) + (* constants anyway, but it could happen for "typedef"-related axioms, *) + (* since they contain the type again), we use an accumulator 'axs' and *) + (* add a relevant axiom only if it is not in 'axs' yet. *) + + fun collect_axioms thy t = + let + val _ = std_output "Adding axioms..." + (* (string * Term.term) list *) + val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy)) + (* given a constant 's' of type 'T', which is a subterm of 't', where *) + (* 't' has a (possibly) more general type, the schematic type *) + (* variables in 't' are instantiated to match the type 'T' *) + (* (string * Term.typ) * Term.term -> Term.term *) + fun specialize_type ((s, T), t) = + let + fun find_typeSubs (Const (s', T')) = + (if s=s' then + Some (Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))) + else + None + handle Type.TYPE_MATCH => None) + | find_typeSubs (Free _) = None + | find_typeSubs (Var _) = None + | find_typeSubs (Bound _) = None + | find_typeSubs (Abs (_, _, body)) = find_typeSubs body + | find_typeSubs (t1 $ t2) = (case find_typeSubs t1 of Some x => Some x | None => find_typeSubs t2) + val typeSubs = (case find_typeSubs t of + Some x => x + | None => raise REFUTE ("collect_axioms", "no type instantiation found for " ^ quote s ^ " in " ^ Sign.string_of_term (sign_of thy) t)) + in + map_term_types + (map_type_tvar + (fn (v,_) => + case Vartab.lookup (typeSubs, v) of + None => + (* schematic type variable not instantiated *) + raise REFUTE ("collect_axioms", "term " ^ Sign.string_of_term (sign_of thy) t ^ " still has a polymorphic type (after instantiating type of " ^ quote s ^ ")") + | Some typ => + typ)) + t + end + (* Term.term list * Term.typ -> Term.term list *) + fun collect_type_axioms (axs, T) = + case T of + (* simple types *) + Type ("prop", []) => axs + | Type ("fun", [T1, T2]) => collect_type_axioms (collect_type_axioms (axs, T1), T2) + | Type ("set", [T1]) => collect_type_axioms (axs, T1) + | Type (s, Ts) => + let + (* look up the definition of a type, as created by "typedef" *) + (* (string * Term.term) list -> (string * Term.term) option *) + fun get_typedefn [] = + None + | get_typedefn ((axname,ax)::axms) = + (let + (* Term.term -> Term.typ option *) + fun type_of_type_definition (Const (s', T')) = + if s'="Typedef.type_definition" then + Some T' + else + None + | type_of_type_definition (Free _) = None + | type_of_type_definition (Var _) = None + | type_of_type_definition (Bound _) = None + | type_of_type_definition (Abs (_, _, body)) = type_of_type_definition body + | type_of_type_definition (t1 $ t2) = (case type_of_type_definition t1 of Some x => Some x | None => type_of_type_definition t2) + in + case type_of_type_definition ax of + Some T' => + let + val T'' = (domain_type o domain_type) T' + val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T'', T)) + val unvar_ax = map_term_types + (map_type_tvar + (fn (v,_) => + case Vartab.lookup (typeSubs, v) of + None => + (* schematic type variable not instantiated *) + raise ERROR + | Some typ => + typ)) + ax + in + Some (axname, unvar_ax) + end + | None => + get_typedefn axms + end + handle ERROR => get_typedefn axms + | MATCH => get_typedefn axms + | Type.TYPE_MATCH => get_typedefn axms) + in + case DatatypePackage.datatype_info thy s of + Some info => (* inductive datatype *) + (* only collect relevant type axioms for the argument types *) + foldl collect_type_axioms (axs, Ts) + | None => + (case get_typedefn axioms of + Some (axname, ax) => + if mem_term (ax, axs) then + (* collect relevant type axioms for the argument types *) + foldl collect_type_axioms (axs, Ts) + else + (std_output (" " ^ axname); + collect_term_axioms (ax :: axs, ax)) + | None => + (* at least collect relevant type axioms for the argument types *) + foldl collect_type_axioms (axs, Ts)) + end + (* TODO: include sort axioms *) + | TFree (_, sorts) => ((*if not (null sorts) then std_output " *ignoring sorts*" else ();*) axs) + | TVar (_, sorts) => ((*if not (null sorts) then std_output " *ignoring sorts*" else ();*) axs) + (* Term.term list * Term.term -> Term.term list *) + and collect_term_axioms (axs, t) = + case t of + (* Pure *) + Const ("all", _) => axs + | Const ("==", _) => axs + | Const ("==>", _) => axs + (* HOL *) + | Const ("Trueprop", _) => axs + | Const ("Not", _) => axs + | Const ("True", _) => axs (* redundant, since 'True' is also an IDT constructor *) + | Const ("False", _) => axs (* redundant, since 'False' is also an IDT constructor *) + | Const ("arbitrary", T) => collect_type_axioms (axs, T) + | Const ("The", T) => + let + val ax = specialize_type (("The", T), (the o assoc) (axioms, "HOL.the_eq_trivial")) + in + if mem_term (ax, axs) then + collect_type_axioms (axs, T) + else + (std_output " HOL.the_eq_trivial"; + collect_term_axioms (ax :: axs, ax)) + end + | Const ("Hilbert_Choice.Eps", T) => + let + val ax = specialize_type (("Hilbert_Choice.Eps", T), (the o assoc) (axioms, "Hilbert_Choice.someI")) + in + if mem_term (ax, axs) then + collect_type_axioms (axs, T) + else + (std_output " Hilbert_Choice.someI"; + collect_term_axioms (ax :: axs, ax)) + end + | Const ("All", _) $ t1 => collect_term_axioms (axs, t1) + | Const ("Ex", _) $ t1 => collect_term_axioms (axs, t1) + | Const ("op =", T) => collect_type_axioms (axs, T) + | Const ("op &", _) => axs + | Const ("op |", _) => axs + | Const ("op -->", _) => axs + (* sets *) + | Const ("Collect", T) => collect_type_axioms (axs, T) + | Const ("op :", T) => collect_type_axioms (axs, T) + (* other optimizations *) + | Const ("Finite_Set.card", T) => collect_type_axioms (axs, T) + (* simply-typed lambda calculus *) + | Const (s, T) => + let + (* look up the definition of a constant, as created by "constdefs" *) + (* string -> Term.typ -> (string * Term.term) list -> (string * Term.term) option *) + fun get_defn [] = + None + | get_defn ((axname,ax)::axms) = + (let + val (lhs, _) = Logic.dest_equals ax (* equations only *) + val c = head_of lhs + val (s', T') = dest_Const c + in + if s=s' then + let + val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T)) + val unvar_ax = map_term_types + (map_type_tvar + (fn (v,_) => + case Vartab.lookup (typeSubs, v) of + None => + (* schematic type variable not instantiated *) + raise ERROR + | Some typ => + typ)) + ax + in + Some (axname, unvar_ax) + end + else + get_defn axms + end + handle ERROR => get_defn axms + | TERM _ => get_defn axms + | Type.TYPE_MATCH => get_defn axms) + (* unit -> bool *) + fun is_IDT_constructor () = + (case body_type T of + Type (s', _) => + (case DatatypePackage.constrs_of thy s' of + Some constrs => + Library.exists (fn c => + (case c of + Const (cname, ctype) => + cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy), T, ctype) + | _ => + raise REFUTE ("collect_axioms", "IDT constructor is not a constant"))) + constrs + | None => + false) + | _ => + false) + (* unit -> bool *) + fun is_IDT_recursor () = + (* the type of a recursion operator: [T1,...,Tn,IDT]--->TResult (where *) + (* the T1,...,Tn depend on the types of the datatype's constructors) *) + ((case last_elem (binder_types T) of + Type (s', _) => + (case DatatypePackage.datatype_info thy s' of + Some info => + (* TODO: I'm not quite sute if comparing the names is sufficient, or if *) + (* we should also check the type *) + s mem (#rec_names info) + | None => (* not an inductive datatype *) + false) + | _ => (* a (free or schematic) type variable *) + false) + handle LIST "last_elem" => false) (* not even a function type *) + in + if is_IDT_constructor () orelse is_IDT_recursor () then + (* only collect relevant type axioms *) + collect_type_axioms (axs, T) + else + (case get_defn axioms of + Some (axname, ax) => + if mem_term (ax, axs) then + (* collect relevant type axioms *) + collect_type_axioms (axs, T) + else + (std_output (" " ^ axname); + collect_term_axioms (ax :: axs, ax)) + | None => + (* collect relevant type axioms *) + collect_type_axioms (axs, T)) + end + | Free (_, T) => collect_type_axioms (axs, T) + | Var (_, T) => collect_type_axioms (axs, T) + | Bound i => axs + | Abs (_, T, body) => collect_term_axioms (collect_type_axioms (axs, T), body) + | t1 $ t2 => collect_term_axioms (collect_term_axioms (axs, t1), t2) + (* universal closure over schematic variables *) + (* Term.term -> Term.term *) + fun close_form t = + let + (* (Term.indexname * Term.typ) list *) + val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t)) + in + foldl + (fn (t', ((x,i),T)) => (Term.all T) $ Abs (x, T, abstract_over (Var((x,i),T), t'))) + (t, vars) + end + (* Term.term list *) + val result = map close_form (collect_term_axioms ([], t)) + val _ = writeln " ...done." + in + result end; (* ------------------------------------------------------------------------- *) -(* find_model: repeatedly calls 'invoke_propgen' with appropriate *) -(* parameters, applies the SAT solver, and (in case a model is *) -(* found) displays the model to the user *) -(* thy : the current theory *) -(* minsize : the minimal size of the model *) -(* maxsize : the maximal size of the model *) -(* maxvars : the maximal number of boolean variables to be used *) -(* satsolver: the name of the SAT solver to be used *) -(* satisfy : if 'True', search for a model that makes 't' true; otherwise *) -(* search for a model that makes 't' false *) +(* ground_types: collects all ground types in a term (including argument *) +(* types of other types), suppressing duplicates. Does not *) +(* return function types, set types, non-recursive IDTs, or *) +(* 'propT'. For IDTs, also the argument types of constructors *) +(* are considered. *) +(* ------------------------------------------------------------------------- *) + + (* theory -> Term.term -> Term.typ list *) + + fun ground_types thy t = + let + (* Term.typ * Term.typ list -> Term.typ list *) + fun collect_types (T, acc) = + if T mem acc then + acc (* prevent infinite recursion (for IDTs) *) + else + (case T of + Type ("fun", [T1, T2]) => collect_types (T1, collect_types (T2, acc)) + | Type ("prop", []) => acc + | Type ("set", [T1]) => collect_types (T1, acc) + | Type (s, Ts) => + (case DatatypePackage.datatype_info thy s of + Some info => (* inductive datatype *) + let + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = (the o assoc) (descr, index) + val typ_assoc = dtyps ~~ Ts + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = (if Library.exists (fn d => + case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("ground_types", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable") + else + ()) + (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *) + fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) = + (* replace a 'DtTFree' variable by the associated type *) + (the o assoc) (typ_assoc, DatatypeAux.DtTFree a) + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) = + let + val (s, ds, _) = (the o assoc) (descr, i) + in + Type (s, map (typ_of_dtyp descr typ_assoc) ds) + end + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) = + Type (s, map (typ_of_dtyp descr typ_assoc) ds) + (* if the current type is a recursive IDT (i.e. a depth is required), add it to 'acc' *) + val acc' = (if Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then + T ins acc + else + acc) + (* collect argument types *) + val acc_args = foldr collect_types (Ts, acc') + (* collect constructor types *) + val acc_constrs = foldr collect_types (flat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs), acc_args) + in + acc_constrs + end + | None => (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *) + T ins (foldr collect_types (Ts, acc))) + | TFree _ => T ins acc + | TVar _ => T ins acc) + in + it_term_types collect_types (t, []) + end; + +(* ------------------------------------------------------------------------- *) +(* string_of_typ: (rather naive) conversion from types to strings, used to *) +(* look up the size of a type in 'sizes'. Parameterized *) +(* types with different parameters (e.g. "'a list" vs. "bool *) +(* list") are identified. *) +(* ------------------------------------------------------------------------- *) + + (* Term.typ -> string *) + + fun string_of_typ (Type (s, _)) = s + | string_of_typ (TFree (s, _)) = s + | string_of_typ (TVar ((s,_), _)) = s; + +(* ------------------------------------------------------------------------- *) +(* first_universe: returns the "first" (i.e. smallest) universe by assigning *) +(* 'minsize' to every type for which no size is specified in *) +(* 'sizes' *) +(* ------------------------------------------------------------------------- *) + + (* Term.typ list -> (string * int) list -> int -> (Term.typ * int) list *) + + fun first_universe xs sizes minsize = + let + fun size_of_typ T = + case assoc (sizes, string_of_typ T) of + Some n => n + | None => minsize + in + map (fn T => (T, size_of_typ T)) xs + end; + +(* ------------------------------------------------------------------------- *) +(* next_universe: enumerates all universes (i.e. assignments of sizes to *) +(* types), where the minimal size of a type is given by *) +(* 'minsize', the maximal size is given by 'maxsize', and a *) +(* type may have a fixed size given in 'sizes' *) (* ------------------------------------------------------------------------- *) - (* theory -> (int * int * int * string) -> Term.term -> bool -> unit *) + (* (Term.typ * int) list -> (string * int) list -> int -> int -> (Term.typ * int) list option *) - fun find_model thy (minsize, maxsize, maxvars, satsolver) t satisfy = + fun next_universe xs sizes minsize maxsize = let - (* Term.typ list *) - val tvars = map (fn (i,s) => TVar(i,s)) (term_tvars t) - val tfrees = map (fn (x,s) => TFree(x,s)) (term_tfrees t) - (* int -> unit *) - fun find_model_loop size = - (* 'maxsize=0' means "search for arbitrary large models" *) - if size>maxsize andalso maxsize<>0 then - writeln ("Search terminated: maxsize=" ^ string_of_int maxsize ^ " exceeded.") + (* int -> int list -> int list option *) + fun add1 _ [] = + None (* overflow *) + | add1 max (x::xs) = + if x 0 :: xs') (add1 max xs) (* carry-over *) + (* int -> int list * int list -> int list option *) + fun shift _ (_, []) = + None + | shift max (zeros, x::xs) = + if x=0 then + shift max (0::zeros, xs) else - let - (* ------------------------------------------------------------------------- *) - (* make_universes: given a list 'xs' of "types" and a universe size 'size', *) - (* this function returns all possible partitions of the universe into *) - (* the "types" in 'xs' such that no "type" is empty. If 'size' is less *) - (* than 'length xs', the returned list of partitions is empty. *) - (* Otherwise, if the list 'xs' is empty, then the returned list of *) - (* partitions contains only the empty list, regardless of 'size'. *) - (* ------------------------------------------------------------------------- *) - (* 'a list -> int -> ('a * int) list list *) - fun make_universes xs size = + apsome (fn xs' => (x-1) :: (zeros @ xs')) (add1 max xs) + (* creates the "first" list of length 'len', where the sum of all list *) + (* elements is 'sum', and the length of the list is 'len' *) + (* int -> int -> int -> int list option *) + fun make_first 0 sum _ = + if sum=0 then + Some [] + else + None + | make_first len sum max = + if sum<=max orelse max<0 then + apsome (fn xs' => sum :: xs') (make_first (len-1) 0 max) + else + apsome (fn xs' => max :: xs') (make_first (len-1) (sum-max) max) + (* enumerates all int lists with a fixed length, where 0<=x<='max' for *) + (* all list elements x (unless 'max'<0) *) + (* int -> int list -> int list option *) + fun next max xs = + (case shift max ([], xs) of + Some xs' => + Some xs' + | None => let - (* 'a list -> int -> int -> ('a * int) list list *) - fun make_partitions_loop (x::xs) 0 total = - map (fn us => ((x,0)::us)) (make_partitions xs total) - | make_partitions_loop (x::xs) first total = - (map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total) - | make_partitions_loop _ _ _ = - raise REFUTE ("find_model", "empty list (in make_partitions_loop)") - and - (* 'a list -> int -> ('a * int) list list *) - make_partitions [x] size = - (* we must use all remaining elements on the type 'x', so there is only one partition *) - [[(x,size)]] - | make_partitions (x::xs) 0 = - (* there are no elements left in the universe, so there is only one partition *) - [map (fn t => (t,0)) (x::xs)] - | make_partitions (x::xs) size = - (* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *) - make_partitions_loop (x::xs) size size - | make_partitions _ _ = - raise REFUTE ("find_model", "empty list (in make_partitions)") - val len = length xs + val (len, sum) = foldl (fn ((l, s), x) => (l+1, s+x)) ((0, 0), xs) in - if size map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len)) - end - (* ('a * int) list -> bool *) - fun find_interpretation xs = - let - val init_model = (xs, []) - val init_args = {next_idx = 1, bounds = [], wellformed = True} - val (intr, model, args) = interpret thy init_model init_args t - val fm = SAnd (#wellformed args, is_satisfying_model model intr satisfy) - val usedvars = maxidx fm - in - (* 'maxvars=0' means "use as many variables as necessary" *) - if usedvars>maxvars andalso maxvars<>0 then - (writeln ("\nSearch terminated: " ^ string_of_int usedvars ^ " boolean variables used (only " ^ string_of_int maxvars ^ " allowed)."); - true) - else - ( - std_output " invoking SAT solver..."; - case SatSolver.invoke_solver satsolver fm of - None => - (std_output (" error: SAT solver " ^ quote satsolver ^ " not configured.\n"); - true) - | Some None => - (std_output " no model found.\n"; - false) - | Some (Some assignment) => - (writeln ("\nModel found:\n" ^ print_model thy model assignment); - true) - ) - end handle CANNOT_INTERPRET => true - (* TODO: change this to false once the ability to interpret terms depends on the universe *) + make_first len (sum+1) max (* increment 'sum' by 1 *) + end) + (* only consider those types for which the size is not fixed *) + val mutables = filter (fn (T, _) => assoc (sizes, string_of_typ T) = None) xs + (* subtract 'minsize' from every size (will be added again at the end) *) + val diffs = map (fn (_, n) => n-minsize) mutables + in + case next (maxsize-minsize) diffs of + Some diffs' => + (* merge with those types for which the size is fixed *) + Some (snd (foldl_map (fn (ds, (T, _)) => + case assoc (sizes, string_of_typ T) of + Some n => (ds, (T, n)) (* return the fixed size *) + | None => (tl ds, (T, minsize + (hd ds)))) (* consume the head of 'ds', add 'minsize' *) + (diffs', xs))) + | None => + None + end; + +(* ------------------------------------------------------------------------- *) +(* toTrue: converts the interpretation of a Boolean value to a propositional *) +(* formula that is true iff the interpretation denotes "true" *) +(* ------------------------------------------------------------------------- *) + + (* interpretation -> prop_formula *) + + fun toTrue (Leaf [fm,_]) = fm + | toTrue _ = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value"); + +(* ------------------------------------------------------------------------- *) +(* toFalse: converts the interpretation of a Boolean value to a *) +(* propositional formula that is true iff the interpretation *) +(* denotes "false" *) +(* ------------------------------------------------------------------------- *) + + (* interpretation -> prop_formula *) + + fun toFalse (Leaf [_,fm]) = fm + | toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value"); + +(* ------------------------------------------------------------------------- *) +(* find_model: repeatedly calls 'interpret' with appropriate parameters, *) +(* applies a SAT solver, and (in case a model is found) displays *) +(* the model to the user by calling 'print_model' *) +(* thy : the current theory *) +(* {...} : parameters that control the translation/model generation *) +(* t : term to be translated into a propositional formula *) +(* negate : if true, find a model that makes 't' false (rather than true) *) +(* Note: exception 'TimeOut' is raised if the algorithm does not terminate *) +(* within 'maxtime' seconds (if 'maxtime' >0) *) +(* ------------------------------------------------------------------------- *) + + (* theory -> params -> Term.term -> bool -> unit *) + + fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver} t negate = + let + (* unit -> unit *) + fun wrapper () = + let + (* Term.term list *) + val axioms = collect_axioms thy t + (* Term.typ list *) + val types = foldl (fn (acc, t') => acc union (ground_types thy t')) ([], t :: axioms) + val _ = writeln ("Ground types: " + ^ (if null types then "none." + else commas (map (Sign.string_of_typ (sign_of thy)) types))) + (* (Term.typ * int) list -> unit *) + fun find_model_loop universe = + (let + val init_model = (universe, []) + val init_args = {maxvars = maxvars, next_idx = 1, bounds = [], wellformed = True} + val _ = std_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") + (* translate 't' and all axioms *) + val ((model, args), intrs) = foldl_map (fn ((m, a), t') => + let + val (i, m', a') = interpret thy m a t' + in + ((m', a'), i) + end) ((init_model, init_args), t :: axioms) + (* make 't' either true or false, and make all axioms true, and *) + (* add the well-formedness side condition *) + val fm_t = (if negate then toFalse else toTrue) (hd intrs) + val fm_ax = PropLogic.all (map toTrue (tl intrs)) + val fm = PropLogic.all [#wellformed args, fm_ax, fm_t] in - case make_universes (tvars@tfrees) size of - [] => - (writeln ("Searching for a model of size " ^ string_of_int size ^ ": cannot make every type non-empty (model is too small)."); - find_model_loop (size+1)) - | [[]] => - (std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term..."); - if find_interpretation [] then - () - else - writeln ("Search terminated: no type variables in term.")) - | us => - let - fun loop [] = - find_model_loop (size+1) - | loop (u::us) = - (std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term..."); - if find_interpretation u then () else loop us) - in - loop us - end + std_output " invoking SAT solver..."; + case SatSolver.invoke_solver satsolver fm of + None => + error ("SAT solver " ^ quote satsolver ^ " not configured.") + | Some None => + (std_output " no model found.\n"; + case next_universe universe sizes minsize maxsize of + Some universe' => find_model_loop universe' + | None => writeln "Search terminated, no larger universe within the given limits.") + | Some (Some assignment) => + writeln ("\n*** Model found: ***\n" ^ print_model thy model assignment) + end handle MAXVARS_EXCEEDED => + writeln ("\nSearch terminated, number of Boolean variables (" ^ string_of_int maxvars ^ " allowed) exceeded.") + | CANNOT_INTERPRET t' => + error ("Unable to interpret term " ^ Sign.string_of_term (sign_of thy) t')) + in + find_model_loop (first_universe types sizes minsize) end - in - writeln ("Trying to find a model that " - ^ (if satisfy then "satisfies" else "refutes") - ^ ": " ^ (Sign.string_of_term (sign_of thy) t)); - if minsize<1 then - writeln "\"minsize\" is less than 1; starting search with size 1." - else (); - find_model_loop (Int.max (minsize,1)) - end; + in + (* some parameter sanity checks *) + assert (minsize>=1) ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1"); + assert (maxsize>=1) ("\"maxsize\" is " ^ string_of_int maxsize ^ ", must be at least 1"); + assert (maxsize>=minsize) ("\"maxsize\" (=" ^ string_of_int maxsize ^ ") is less than \"minsize\" (=" ^ string_of_int minsize ^ ")."); + assert (maxvars>=0) ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0"); + assert (maxtime>=0) ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0"); + (* enter loop with/without time limit *) + writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": " + ^ Sign.string_of_term (sign_of thy) t); + if maxtime>0 then + (* TODO: this only works with SML/NJ *) + ((*TimeLimit.timeLimit (Time.fromSeconds (Int32.fromInt maxtime))*) + wrapper () + (*handle TimeLimit.TimeOut => + writeln ("\nSearch terminated, time limit (" + ^ string_of_int maxtime ^ " second" + ^ (if maxtime=1 then "" else "s") + ^ ") exceeded.")*)) + else + wrapper () + end; (* ------------------------------------------------------------------------- *) @@ -522,7 +954,7 @@ (* theory -> (string * string) list -> Term.term -> unit *) fun satisfy_term thy params t = - find_model thy (actual_params thy params) t true; + find_model thy (actual_params thy params) t false; (* ------------------------------------------------------------------------- *) (* refute_term: calls 'find_model' to find a model that refutes 't' *) @@ -534,7 +966,10 @@ fun refute_term thy params t = let - (* disallow schematic type variables, since we cannot properly negate terms containing them *) + (* disallow schematic type variables, since we cannot properly negate *) + (* terms containing them (their logical meaning is that there EXISTS a *) + (* type s.t. ...; to refute such a formula, we would have to show that *) + (* for ALL types, not ...) *) val _ = assert (null (term_tvars t)) "Term to be refuted contains schematic type variables" (* existential closure over schematic variables *) (* (Term.indexname * Term.typ) list *) @@ -545,11 +980,11 @@ (t, vars) (* If 't' is of type 'propT' (rather than 'boolT'), applying *) (* 'HOLogic.exists_const' is not type-correct. However, this *) - (* isn't really a problem as long as 'find_model' still *) + (* is not really a problem as long as 'find_model' still *) (* interprets the resulting term correctly, without checking *) (* its type. *) in - find_model thy (actual_params thy params) ex_closure false + find_model thy (actual_params thy params) ex_closure true end; (* ------------------------------------------------------------------------- *) @@ -569,986 +1004,16 @@ (* INTERPRETERS *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - - fun var_typevar_interpreter thy model args t = - let - fun is_var (Free _) = true - | is_var (Var _) = true - | is_var _ = false - fun typeof (Free (_,T)) = T - | typeof (Var (_,T)) = T - | typeof _ = raise REFUTE ("var_typevar_interpreter", "term is not a variable") - fun is_typevar (TFree _) = true - | is_typevar (TVar _) = true - | is_typevar _ = false - val (sizes, intrs) = model - in - if is_var t andalso is_typevar (typeof t) then - (case assoc (intrs, t) of - Some intr => Some (intr, model, args) - | None => - let - val size = (the o assoc) (sizes, typeof t) (* the model MUST specify a size for type variables *) - val idx = #next_idx args - val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1)))) - val next = (if size=2 then idx+1 else idx+size) - in - (* extend the model, increase 'next_idx' *) - Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args}) - end) - else - None - end; - - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - - fun var_funtype_interpreter thy model args t = - let - fun is_var (Free _) = true - | is_var (Var _) = true - | is_var _ = false - fun typeof (Free (_,T)) = T - | typeof (Var (_,T)) = T - | typeof _ = raise REFUTE ("var_funtype_interpreter", "term is not a variable") - fun stringof (Free (x,_)) = x - | stringof (Var ((x,_), _)) = x - | stringof _ = raise REFUTE ("var_funtype_interpreter", "term is not a variable") - fun is_funtype (Type ("fun", [_,_])) = true - | is_funtype _ = false - val (sizes, intrs) = model - in - if is_var t andalso is_funtype (typeof t) then - (case assoc (intrs, t) of - Some intr => Some (intr, model, args) - | None => - let - val T1 = domain_type (typeof t) - val T2 = range_type (typeof t) - (* we create 'size_of_interpretation (interpret (... T1))' different copies *) - (* of the tree for 'T2', which are then combined into a single new tree *) - val (i1, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (stringof t, T1)) - (* power(a,b) computes a^b, for a>=0, b>=0 *) - (* int * int -> int *) - fun power (a,0) = 1 - | power (a,1) = a - | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end - fun size_of_interpretation (Leaf xs) = length xs - | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs) - val size = size_of_interpretation i1 - (* make fresh copies, with different variable indices *) - (* int -> int -> (int * interpretation list *) - fun make_copies idx 0 = - (idx, []) - | make_copies idx n = - let - val (copy, _, args) = interpret thy (sizes, []) {next_idx = idx, bounds = [], wellformed=True} (Free (stringof t, T2)) - val (next, copies) = make_copies (#next_idx args) (n-1) - in - (next, copy :: copies) - end - val (idx, copies) = make_copies (#next_idx args) (size_of_interpretation i1) - (* combine copies into a single tree *) - val intr = Node copies - in - (* extend the model, increase 'next_idx' *) - Some (intr, (sizes, (t, intr)::intrs), {next_idx = idx, bounds = #bounds args, wellformed = #wellformed args}) - end) - else - None - end; - - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - - fun var_settype_interpreter thy model args t = - let - val (sizes, intrs) = model - in - case t of - Free (x, Type ("set", [T])) => - (case assoc (intrs, t) of - Some intr => Some (intr, model, args) - | None => - let - val (intr, _, args') = interpret thy model args (Free (x, Type ("fun", [T, Type ("bool", [])]))) - in - Some (intr, (sizes, (t, intr)::intrs), args') - end) - | Var ((x,i), Type ("set", [T])) => - (case assoc (intrs, t) of - Some intr => Some (intr, model, args) - | None => - let - val (intr, _, args') = interpret thy model args (Var ((x,i), Type ("fun", [T, Type ("bool", [])]))) - in - Some (intr, (sizes, (t, intr)::intrs), args') - end) - | _ => None - end; - - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - - fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds (args:arguments)), model, args) - | boundvar_interpreter thy model args _ = None; - - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - - fun abstraction_interpreter thy model args (Abs (x, T, t)) = - let - val (sizes, intrs) = model - (* create all constants of type T *) - val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (x, T)) - (* returns a list with all unit vectors of length n *) - (* int -> interpretation list *) - fun unit_vectors n = - let - (* returns the k-th unit vector of length n *) - (* int * int -> interpretation *) - fun unit_vector (k,n) = - Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) - (* int -> interpretation list -> interpretation list *) - fun unit_vectors_acc k vs = - if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs) - in - unit_vectors_acc 1 [] - end - (* concatenates 'x' with every list in 'xss', returning a new list of lists *) - (* 'a -> 'a list list -> 'a list list *) - fun cons_list x xss = - map (fn xs => x::xs) xss - (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *) - (* int -> 'a list -> 'a list list *) - fun pick_all 1 xs = - map (fn x => [x]) xs - | pick_all n xs = - let val rec_pick = pick_all (n-1) xs in - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs) - end - (* interpretation -> interpretation list *) - fun make_constants (Leaf xs) = - unit_vectors (length xs) - | make_constants (Node xs) = - map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) - (* interpret the body 't' separately for each constant *) - val ((model', args'), bodies) = foldl_map - (fn ((m,a), c) => - let - (* add 'c' to 'bounds' *) - val (i',m',a') = interpret thy m {next_idx = #next_idx a, bounds = c::(#bounds a), wellformed = #wellformed a} t - in - (* keep the new model m' and 'next_idx', but use old 'bounds' *) - ((m',{next_idx = #next_idx a', bounds = #bounds a, wellformed = #wellformed a'}), i') - end) - ((model,args), make_constants i) - in - Some (Node bodies, model', args') - end - | abstraction_interpreter thy model args _ = None; - - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - - fun apply_interpreter thy model args (t1 $ t2) = - let - (* auxiliary functions *) - (* interpretation * interpretation -> interpretation *) - fun interpretation_disjunction (tr1,tr2) = - tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2)) - (* prop_formula * interpretation -> interpretation *) - fun prop_formula_times_interpretation (fm,tr) = - tree_map (map (fn x => SAnd (fm,x))) tr - (* prop_formula list * interpretation list -> interpretation *) - fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) = - prop_formula_times_interpretation (fm,tr) - | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) = - interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees)) - | prop_formula_list_dot_product_interpretation_list (_,_) = - raise REFUTE ("apply_interpreter", "empty list (in dot product)") - (* concatenates 'x' with every list in 'xss', returning a new list of lists *) - (* 'a -> 'a list list -> 'a list list *) - fun cons_list x xss = - map (fn xs => x::xs) xss - (* returns a list of lists, each one consisting of one element from each element of 'xss' *) - (* 'a list list -> 'a list list *) - fun pick_all [xs] = - map (fn x => [x]) xs - | pick_all (xs::xss) = - let val rec_pick = pick_all xss in - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs) - end - | pick_all _ = - raise REFUTE ("apply_interpreter", "empty list (in pick_all)") - (* interpretation -> prop_formula list *) - fun interpretation_to_prop_formula_list (Leaf xs) = - xs - | interpretation_to_prop_formula_list (Node trees) = - map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees)) - (* interpretation * interpretation -> interpretation *) - fun interpretation_apply (tr1,tr2) = - (case tr1 of - Leaf _ => - raise REFUTE ("apply_interpreter", "first interpretation is a leaf") - | Node xs => - prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list tr2, xs)) - (* interpret 't1' and 't2' *) - val (intr1, model1, args1) = interpret thy model args t1 - val (intr2, model2, args2) = interpret thy model1 args1 t2 - in - Some (interpretation_apply (intr1,intr2), model2, args2) - end - | apply_interpreter thy model args _ = None; - - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - - fun const_unfold_interpreter thy model args t = - (* ------------------------------------------------------------------------- *) - (* We unfold constants for which a defining equation is given as an axiom. *) - (* A polymorphic axiom's type variables are instantiated. Eta-expansion is *) - (* performed only if necessary; arguments in the axiom that are present as *) - (* actual arguments in 't' are simply substituted. If more actual than *) - (* formal arguments are present, the constant is *not* unfolded, so that *) - (* other interpreters (that may just not have looked into the term far *) - (* enough yet) may be applied first (after 'apply_interpreter' gets rid of *) - (* one argument). *) - (* ------------------------------------------------------------------------- *) - let - val (head, actuals) = strip_comb t - val actuals_count = length actuals - in - case head of - Const (s,T) => - let - (* (string * Term.term) list *) - val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy)) - (* Term.term * Term.term list * Term.term list -> Term.term *) - (* term, formal arguments, actual arguments *) - fun normalize (t, [], []) = t - | normalize (t, [], y::ys) = raise REFUTE ("const_unfold_interpreter", "more actual than formal parameters") - | normalize (t, x::xs, []) = normalize (lambda x t, xs, []) (* eta-expansion *) - | normalize (t, x::xs, y::ys) = normalize (betapply (lambda x t, y), xs, ys) (* substitution *) - (* string -> Term.typ -> (string * Term.term) list -> Term.term option *) - fun get_defn s T [] = - None - | get_defn s T ((_,ax)::axms) = - (let - val (lhs, rhs) = Logic.dest_equals ax (* equations only *) - val (c, formals) = strip_comb lhs - val (s', T') = dest_Const c - in - if (s=s') andalso (actuals_count <= length formals) then - let - val varT' = Type.varifyT T' (* for polymorphic definitions *) - val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (varT', T)) - val varRhs = map_term_types Type.varifyT rhs - val varFormals = map (map_term_types Type.varifyT) formals - val rhs' = normalize (varRhs, varFormals, actuals) - val unvarRhs = map_term_types - (map_type_tvar - (fn (v,_) => - case Vartab.lookup (typeSubs, v) of - None => - raise REFUTE ("const_unfold_interpreter", "schematic type variable " ^ (fst v) ^ "not instantiated (in definition of " ^ quote s ^ ")") - | Some typ => - typ)) - rhs' - in - Some unvarRhs - end - else - get_defn s T axms - end - handle TERM _ => get_defn s T axms - | Type.TYPE_MATCH => get_defn s T axms) - in - case get_defn s T axioms of - Some t' => Some (interpret thy model args t') - | None => None - end - | _ => None - end; - - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - - fun Pure_interpreter thy model args t = - let - fun toTrue (Leaf [fm,_]) = fm - | toTrue _ = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value") - fun toFalse (Leaf [_,fm]) = fm - | toFalse _ = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value") - in - case t of - (*Const ("Goal", _) $ t1 => - Some (interpret thy model args t1) |*) - Const ("all", _) $ t1 => - let - val (i,m,a) = (interpret thy model args t1) - in - case i of - Node xs => - let - val fmTrue = PropLogic.all (map toTrue xs) - val fmFalse = PropLogic.exists (map toFalse xs) - in - Some (Leaf [fmTrue, fmFalse], m, a) - end - | _ => - raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function") - end - | Const ("==", _) $ t1 $ t2 => - let - val (i1,m1,a1) = interpret thy model args t1 - val (i2,m2,a2) = interpret thy m1 a1 t2 - (* interpretation * interpretation -> prop_formula *) - fun interpret_equal (tr1,tr2) = - (case tr1 of - Leaf x => - (case tr2 of - Leaf y => PropLogic.dot_product (x,y) - | _ => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher")) - | Node xs => - (case tr2 of - Leaf _ => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher") - (* extensionality: two functions are equal iff they are equal for every element *) - | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys)))) - (* interpretation * interpretation -> prop_formula *) - fun interpret_unequal (tr1,tr2) = - (case tr1 of - Leaf x => - (case tr2 of - Leaf y => - let - fun unequal [] ([],_) = - False - | unequal (x::xs) (y::ys1, ys2) = - SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2)) - | unequal _ _ = - raise REFUTE ("Pure_interpreter", "\"==\": leafs have different width") - in - unequal x (y,[]) - end - | _ => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher")) - | Node xs => - (case tr2 of - Leaf _ => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher") - (* extensionality: two functions are unequal iff there exist unequal elements *) - | Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys)))) - val fmTrue = interpret_equal (i1,i2) - val fmFalse = interpret_unequal (i1,i2) - in - Some (Leaf [fmTrue, fmFalse], m2, a2) - end - | Const ("==>", _) $ t1 $ t2 => - let - val (i1,m1,a1) = interpret thy model args t1 - val (i2,m2,a2) = interpret thy m1 a1 t2 - val fmTrue = SOr (toFalse i1, toTrue i2) - val fmFalse = SAnd (toTrue i1, toFalse i2) - in - Some (Leaf [fmTrue, fmFalse], m2, a2) - end - | _ => None - end; - - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - - fun HOLogic_interpreter thy model args t = - (* ------------------------------------------------------------------------- *) - (* Providing interpretations directly is more efficient than unfolding the *) - (* logical constants; however, we need versions for constants with arguments *) - (* (to avoid unfolding) as well as versions for constants without arguments *) - (* (since in HOL, logical constants can themselves be arguments) *) - (* ------------------------------------------------------------------------- *) - let - fun eta_expand t i = - let - val Ts = binder_types (fastype_of t) - in - foldr (fn (T, t) => Abs ("", T, t)) - (take (i, Ts), list_comb (t, map Bound (i-1 downto 0))) - end - val TT = Leaf [True, False] - val FF = Leaf [False, True] - fun toTrue (Leaf [fm,_]) = fm - | toTrue _ = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value") - fun toFalse (Leaf [_,fm]) = fm - | toFalse _ = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value") - in - case t of - Const ("Trueprop", _) $ t1 => - Some (interpret thy model args t1) - | Const ("Trueprop", _) => - Some (Node [TT, FF], model, args) - | Const ("Not", _) $ t1 => - apply_interpreter thy model args t - | Const ("Not", _) => - Some (Node [FF, TT], model, args) - | Const ("True", _) => - Some (TT, model, args) - | Const ("False", _) => - Some (FF, model, args) - | Const ("arbitrary", T) => - (* treat 'arbitrary' just like a free variable of the same type *) - (case assoc (snd model, t) of - Some intr => - Some (intr, model, args) - | None => - let - val (sizes, intrs) = model - val (intr, _, a) = interpret thy (sizes, []) args (Free ("", T)) - in - Some (intr, (sizes, (t,intr)::intrs), a) - end) - | Const ("The", _) $ t1 => - apply_interpreter thy model args t - | Const ("The", T as Type ("fun", [_, T'])) => - (* treat 'The' like a free variable, but with a fixed interpretation for boolean *) - (* functions that map exactly one constant of type T' to True *) - (case assoc (snd model, t) of - Some intr => - Some (intr, model, args) - | None => - let - val (sizes, intrs) = model - val (intr, _, a) = interpret thy (sizes, []) args (Free ("", T)) - (* create all constants of type T' => bool, ... *) - val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("", Type ("fun", [T', Type ("bool",[])]))) - (* ... and all constants of type T' *) - val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("", T')) - (* returns a list with all unit vectors of length n *) - (* int -> interpretation list *) - fun unit_vectors n = - let - (* returns the k-th unit vector of length n *) - (* int * int -> interpretation *) - fun unit_vector (k,n) = - Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) - (* int -> interpretation list -> interpretation list *) - fun unit_vectors_acc k vs = - if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs) - in - unit_vectors_acc 1 [] - end - (* concatenates 'x' with every list in 'xss', returning a new list of lists *) - (* 'a -> 'a list list -> 'a list list *) - fun cons_list x xss = - map (fn xs => x::xs) xss - (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *) - (* int -> 'a list -> 'a list list *) - fun pick_all 1 xs = - map (fn x => [x]) xs - | pick_all n xs = - let val rec_pick = pick_all (n-1) xs in - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs) - end - (* interpretation -> interpretation list *) - fun make_constants (Leaf xs) = - unit_vectors (length xs) - | make_constants (Node xs) = - map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) - val constantsFun = make_constants intrFun - val constantsT' = make_constants intrT' - (* interpretation -> interpretation list -> interpretation option *) - fun the_val (Node xs) cs = - let - val TrueCount = foldl (fn (n,x) => if toTrue x = True then n+1 else n) (0,xs) - fun findThe (x::xs) (c::cs) = - if toTrue x = True then - c - else - findThe xs cs - | findThe _ _ = - raise REFUTE ("HOLogic_interpreter", "\"The\": not found") - in - if TrueCount=1 then - Some (findThe xs cs) - else - None - end - | the_val _ _ = - raise REFUTE ("HOLogic_interpreter", "\"The\": function interpreted as a leaf") - in - case intr of - Node xs => - let - (* replace interpretation 'x' by the interpretation determined by 'f' *) - val intrThe = Node (map (fn (x,f) => if_none (the_val f constantsT') x) (xs ~~ constantsFun)) - in - Some (intrThe, (sizes, (t,intrThe)::intrs), a) - end - | _ => - raise REFUTE ("HOLogic_interpreter", "\"The\": interpretation is a leaf") - end) - | Const ("Hilbert_Choice.Eps", _) $ t1 => - apply_interpreter thy model args t - | Const ("Hilbert_Choice.Eps", T as Type ("fun", [_, T'])) => - (* treat 'The' like a free variable, but with a fixed interpretation for boolean *) - (* functions that map exactly one constant of type T' to True *) - (case assoc (snd model, t) of - Some intr => - Some (intr, model, args) - | None => - let - val (sizes, intrs) = model - val (intr, _, a) = interpret thy (sizes, []) args (Free ("", T)) - (* create all constants of type T' => bool, ... *) - val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("", Type ("fun", [T', Type ("bool",[])]))) - (* ... and all constants of type T' *) - val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("", T')) - (* returns a list with all unit vectors of length n *) - (* int -> interpretation list *) - fun unit_vectors n = - let - (* returns the k-th unit vector of length n *) - (* int * int -> interpretation *) - fun unit_vector (k,n) = - Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) - (* int -> interpretation list -> interpretation list *) - fun unit_vectors_acc k vs = - if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs) - in - unit_vectors_acc 1 [] - end - (* concatenates 'x' with every list in 'xss', returning a new list of lists *) - (* 'a -> 'a list list -> 'a list list *) - fun cons_list x xss = - map (fn xs => x::xs) xss - (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *) - (* int -> 'a list -> 'a list list *) - fun pick_all 1 xs = - map (fn x => [x]) xs - | pick_all n xs = - let val rec_pick = pick_all (n-1) xs in - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs) - end - (* interpretation -> interpretation list *) - fun make_constants (Leaf xs) = - unit_vectors (length xs) - | make_constants (Node xs) = - map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) - val constantsFun = make_constants intrFun - val constantsT' = make_constants intrT' - (* interpretation -> interpretation list -> interpretation list *) - fun true_values (Node xs) cs = - mapfilter (fn (x,c) => if toTrue x = True then Some c else None) (xs~~cs) - | true_values _ _ = - raise REFUTE ("HOLogic_interpreter", "\"Eps\": function interpreted as a leaf") - in - case intr of - Node xs => - let - val (wf, intrsEps) = foldl_map (fn (w,(x,f)) => - case true_values f constantsT' of - [] => (w, x) (* no value mapped to true -> no restriction *) - | [c] => (w, c) (* one value mapped to true -> that's the one *) - | cs => - let - (* interpretation * interpretation -> prop_formula *) - fun interpret_equal (tr1,tr2) = - (case tr1 of - Leaf x => - (case tr2 of - Leaf y => PropLogic.dot_product (x,y) - | _ => raise REFUTE ("HOLogic_interpreter", "\"Eps\": second tree is higher")) - | Node xs => - (case tr2 of - Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"Eps\": first tree is higher") - (* extensionality: two functions are equal iff they are equal for every element *) - | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys)))) - in - (SAnd (w, PropLogic.exists (map (fn c => interpret_equal (x,c)) cs)), x) (* impose restrictions on x *) - end - ) - (#wellformed a, xs ~~ constantsFun) - val intrEps = Node intrsEps - in - Some (intrEps, (sizes, (t,intrEps)::intrs), {next_idx = #next_idx a, bounds = #bounds a, wellformed = wf}) - end - | _ => - raise REFUTE ("HOLogic_interpreter", "\"Eps\": interpretation is a leaf") - end) - | Const ("All", _) $ t1 => - let - val (i,m,a) = interpret thy model args t1 - in - case i of - Node xs => - let - val fmTrue = PropLogic.all (map toTrue xs) - val fmFalse = PropLogic.exists (map toFalse xs) - in - Some (Leaf [fmTrue, fmFalse], m, a) - end - | _ => - raise REFUTE ("HOLogic_interpreter", "\"All\" is not followed by a function") - end - | Const ("All", _) => - Some (interpret thy model args (eta_expand t 1)) - | Const ("Ex", _) $ t1 => - let - val (i,m,a) = interpret thy model args t1 - in - case i of - Node xs => - let - val fmTrue = PropLogic.exists (map toTrue xs) - val fmFalse = PropLogic.all (map toFalse xs) - in - Some (Leaf [fmTrue, fmFalse], m, a) - end - | _ => - raise REFUTE ("HOLogic_interpreter", "\"Ex\" is not followed by a function") - end - | Const ("Ex", _) => - Some (interpret thy model args (eta_expand t 1)) - | Const ("Ex1", _) $ t1 => - let - val (i,m,a) = interpret thy model args t1 - in - case i of - Node xs => - let - (* interpretation list -> prop_formula *) - fun allfalse [] = True - | allfalse (x::xs) = SAnd (toFalse x, allfalse xs) - (* interpretation list -> prop_formula *) - fun exactly1true [] = False - | exactly1true (x::xs) = SOr (SAnd (toTrue x, allfalse xs), SAnd (toFalse x, exactly1true xs)) - (* interpretation list -> prop_formula *) - fun atleast2true [] = False - | atleast2true (x::xs) = SOr (SAnd (toTrue x, PropLogic.exists (map toTrue xs)), atleast2true xs) - val fmTrue = exactly1true xs - val fmFalse = SOr (allfalse xs, atleast2true xs) - in - Some (Leaf [fmTrue, fmFalse], m, a) - end - | _ => - raise REFUTE ("HOLogic_interpreter", "\"Ex1\" is not followed by a function") - end - | Const ("Ex1", _) => - Some (interpret thy model args (eta_expand t 1)) - | Const ("op =", _) $ t1 $ t2 => - let - val (i1,m1,a1) = interpret thy model args t1 - val (i2,m2,a2) = interpret thy m1 a1 t2 - (* interpretation * interpretation -> prop_formula *) - fun interpret_equal (tr1,tr2) = - (case tr1 of - Leaf x => - (case tr2 of - Leaf y => PropLogic.dot_product (x,y) - | _ => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher")) - | Node xs => - (case tr2 of - Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher") - (* extensionality: two functions are equal iff they are equal for every element *) - | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys)))) - (* interpretation * interpretation -> prop_formula *) - fun interpret_unequal (tr1,tr2) = - (case tr1 of - Leaf x => - (case tr2 of - Leaf y => - let - fun unequal [] ([],_) = - False - | unequal (x::xs) (y::ys1, ys2) = - SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2)) - | unequal _ _ = - raise REFUTE ("HOLogic_interpreter", "\"==\": leafs have different width") - in - unequal x (y,[]) - end - | _ => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher")) - | Node xs => - (case tr2 of - Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher") - (* extensionality: two functions are unequal iff there exist unequal elements *) - | Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys)))) - val fmTrue = interpret_equal (i1,i2) - val fmFalse = interpret_unequal (i1,i2) - in - Some (Leaf [fmTrue, fmFalse], m2, a2) - end - | Const ("op =", _) $ t1 => - Some (interpret thy model args (eta_expand t 1)) - | Const ("op =", _) => - Some (interpret thy model args (eta_expand t 2)) - | Const ("op &", _) $ t1 $ t2 => - apply_interpreter thy model args t - | Const ("op &", _) $ t1 => - apply_interpreter thy model args t - | Const ("op &", _) => - Some (Node [Node [TT, FF], Node [FF, FF]], model, args) - | Const ("op |", _) $ t1 $ t2 => - apply_interpreter thy model args t - | Const ("op |", _) $ t1 => - apply_interpreter thy model args t - | Const ("op |", _) => - Some (Node [Node [TT, TT], Node [TT, FF]], model, args) - | Const ("op -->", _) $ t1 $ t2 => - apply_interpreter thy model args t - | Const ("op -->", _) $ t1 => - apply_interpreter thy model args t - | Const ("op -->", _) => - Some (Node [Node [TT, FF], Node [TT, TT]], model, args) - | Const ("Collect", _) $ t1 => - (* Collect == identity *) - Some (interpret thy model args t1) - | Const ("Collect", _) => - Some (interpret thy model args (eta_expand t 1)) - | Const ("op :", _) $ t1 $ t2 => - (* op: == application *) - Some (interpret thy model args (t2 $ t1)) - | Const ("op :", _) $ t1 => - Some (interpret thy model args (eta_expand t 1)) - | Const ("op :", _) => - Some (interpret thy model args (eta_expand t 2)) - | _ => None - end; - - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - - fun IDT_interpreter thy model args t = - let - fun is_var (Free _) = true - | is_var (Var _) = true - | is_var _ = false - fun typeof (Free (_,T)) = T - | typeof (Var (_,T)) = T - | typeof _ = raise REFUTE ("var_IDT_interpreter", "term is not a variable") - val (sizes, intrs) = model - (* power(a,b) computes a^b, for a>=0, b>=0 *) - (* int * int -> int *) - fun power (a,0) = 1 - | power (a,1) = a - | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end - (* interpretation -> int *) - fun size_of_interpretation (Leaf xs) = length xs - | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs) - (* Term.typ -> int *) - fun size_of_type T = - let - val (i,_,_) = interpret thy model args (Free ("", T)) - in - size_of_interpretation i - end - (* int list -> int *) - fun sum xs = foldl op+ (0, xs) - (* int list -> int *) - fun product xs = foldl op* (1, xs) - (* DatatypeAux.dtyp * Term.typ -> DatatypeAux.dtyp -> Term.typ *) - fun typ_of_dtyp typ_assoc (DatatypeAux.DtTFree a) = - the (assoc (typ_assoc, DatatypeAux.DtTFree a)) - | typ_of_dtyp typ_assoc (DatatypeAux.DtRec i) = - raise REFUTE ("var_IDT_interpreter", "recursive datatype") - | typ_of_dtyp typ_assoc (DatatypeAux.DtType (s, ds)) = - Type (s, map (typ_of_dtyp typ_assoc) ds) - in - if is_var t then - (case typeof t of - Type (s, Ts) => - (case DatatypePackage.datatype_info thy s of - Some info => (* inductive datatype *) - let - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = the (assoc (descr, index)) - in - if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then - raise REFUTE ("var_IDT_interpreter", "recursive datatype argument") - else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then - None (* recursive datatype (requires an infinite model) *) - else - case assoc (intrs, t) of - Some intr => Some (intr, model, args) - | None => - let - val typ_assoc = dtyps ~~ Ts - val size = sum (map (fn (_,ds) => - product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) constrs) - val idx = #next_idx args - (* for us, an IDT has no "internal structure" -- its interpretation is just a leaf *) - val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1)))) - val next = (if size=2 then idx+1 else idx+size) - in - (* extend the model, increase 'next_idx' *) - Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args}) - end - end - | None => None) - | _ => None) - else - let - val (head, params) = strip_comb t (* look into applications to avoid unfolding *) - in - (case head of - Const (c, T) => - (case body_type T of - Type (s, Ts) => - (case DatatypePackage.datatype_info thy s of - Some info => (* inductive datatype *) - let - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = the (assoc (descr, index)) - in - if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then - raise REFUTE ("var_IDT_interpreter", "recursive datatype argument") - else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then - None (* recursive datatype (requires an infinite model) *) - else - (case take_prefix (fn (c',_) => c' <> c) constrs of - (_, []) => - None (* unknown constructor *) - | (prevs, _) => - if null params then - let - val typ_assoc = dtyps ~~ Ts - val offset = sum (map (fn (_,ds) => - product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) prevs) - val (i,_,_) = interpret thy model args (Free ("", T)) - (* int * interpretation -> int * interpretation *) - fun replace (offset, Leaf xs) = - (* replace the offset-th element by True, all others by False, inc. offset by 1 *) - (offset+1, Leaf (snd (foldl_map (fn (n,_) => (n+1, if n=offset then True else False)) (0, xs)))) - | replace (offset, Node xs) = - let - val (offset', xs') = foldl_map replace (offset, xs) - in - (offset', Node xs') - end - val (_,intr) = replace (offset, i) - in - Some (intr, model, args) - end - else - apply_interpreter thy model args t) (* avoid unfolding by calling 'apply_interpreter' directly *) - end - | None => None) - | _ => None) - | _ => None) - end - end; - - (* ------------------------------------------------------------------------- *) -(* PRINTERS *) +(* make_constants: returns all interpretations that have the same tree *) +(* structure as 'intr', but consist of unit vectors with *) +(* 'True'/'False' only (no Boolean variables) *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *) + (* interpretation -> interpretation list *) - fun var_typevar_printer thy model t intr assignment = - let - fun is_var (Free _) = true - | is_var (Var _) = true - | is_var _ = false - fun typeof (Free (_,T)) = T - | typeof (Var (_,T)) = T - | typeof _ = raise REFUTE ("var_typevar_printer", "term is not a variable") - fun is_typevar (TFree _) = true - | is_typevar (TVar _) = true - | is_typevar _ = false - in - if is_var t andalso is_typevar (typeof t) then - let - (* interpretation -> int *) - fun index_from_interpretation (Leaf xs) = - let - val idx = find_index (PropLogic.eval assignment) xs - in - if idx<0 then - raise REFUTE ("var_typevar_printer", "illegal interpretation: no value assigned") - else - idx - end - | index_from_interpretation _ = - raise REFUTE ("var_typevar_printer", "interpretation is not a leaf") - (* string -> string *) - fun strip_leading_quote s = - (implode o (fn (x::xs) => if x="'" then xs else (x::xs)) o explode) s - (* Term.typ -> string *) - fun string_of_typ (TFree (x,_)) = strip_leading_quote x - | string_of_typ (TVar ((x,i),_)) = strip_leading_quote x ^ string_of_int i - | string_of_typ _ = raise REFUTE ("var_typevar_printer", "type is not a type variable") - in - Some (string_of_typ (typeof t) ^ string_of_int (index_from_interpretation intr)) - end - else - None - end; - - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *) - - fun var_funtype_printer thy model t intr assignment = + fun make_constants intr = let - fun is_var (Free _) = true - | is_var (Var _) = true - | is_var _ = false - fun typeof (Free (_,T)) = T - | typeof (Var (_,T)) = T - | typeof _ = raise REFUTE ("var_funtype_printer", "term is not a variable") - fun is_funtype (Type ("fun", [_,_])) = true - | is_funtype _ = false - in - if is_var t andalso is_funtype (typeof t) then - let - val T1 = domain_type (typeof t) - val T2 = range_type (typeof t) - val (sizes, _) = model - (* create all constants of type T1 *) - val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_funtype_printer", T1)) - (* returns a list with all unit vectors of length n *) - (* int -> interpretation list *) - fun unit_vectors n = - let - (* returns the k-th unit vector of length n *) - (* int * int -> interpretation *) - fun unit_vector (k,n) = - Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) - (* int -> interpretation list -> interpretation list *) - fun unit_vectors_acc k vs = - if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs) - in - unit_vectors_acc 1 [] - end - (* concatenates 'x' with every list in 'xss', returning a new list of lists *) - (* 'a -> 'a list list -> 'a list list *) - fun cons_list x xss = - map (fn xs => x::xs) xss - (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *) - (* int -> 'a list -> 'a list list *) - fun pick_all 1 xs = - map (fn x => [x]) xs - | pick_all n xs = - let val rec_pick = pick_all (n-1) xs in - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs) - end - (* interpretation -> interpretation list *) - fun make_constants (Leaf xs) = - unit_vectors (length xs) - | make_constants (Node xs) = - map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) - (* interpretation list *) - val results = (case intr of - Node xs => xs - | _ => raise REFUTE ("var_funtype_printer", "interpretation is a leaf")) - (* string list *) - val strings = map - (fn (argi,resulti) => print thy model (Free ("var_funtype_printer", T1)) argi assignment - ^ "\\" - ^ print thy model (Free ("var_funtype_printer", T2)) resulti assignment) - ((make_constants i) ~~ results) - in - Some (enclose "(" ")" (commas strings)) - end - else - None - end; - - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *) - - fun var_settype_printer thy model t intr assignment = - let - val (sizes, _) = model (* returns a list with all unit vectors of length n *) (* int -> interpretation list *) fun unit_vectors n = @@ -1575,205 +1040,875 @@ let val rec_pick = pick_all (n-1) xs in foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs) end - (* interpretation -> interpretation list *) - fun make_constants (Leaf xs) = - unit_vectors (length xs) - | make_constants (Node xs) = - map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) + in + case intr of + Leaf xs => unit_vectors (length xs) + | Node xs => map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) + end; + +(* ------------------------------------------------------------------------- *) +(* size_of_type: returns the number of constants in a type (i.e. 'length *) +(* (make_constants intr)', but implemented more efficiently) *) +(* ------------------------------------------------------------------------- *) + + (* interpretation -> int *) + + fun size_of_type intr = + let + (* power(a,b) computes a^b, for a>=0, b>=0 *) + (* int * int -> int *) + fun power (a,0) = 1 + | power (a,1) = a + | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end + in + case intr of + Leaf xs => length xs + | Node xs => power (size_of_type (hd xs), length xs) + end; + +(* ------------------------------------------------------------------------- *) +(* TT/FF: interpretations that denote "true" or "false", respectively *) +(* ------------------------------------------------------------------------- *) + + (* interpretation *) + + val TT = Leaf [True, False]; + + val FF = Leaf [False, True]; + +(* ------------------------------------------------------------------------- *) +(* make_equality: returns an interpretation that denotes (extensional) *) +(* equality of two interpretations *) +(* ------------------------------------------------------------------------- *) + + (* We could in principle represent '=' on a type T by a particular *) + (* interpretation. However, the size of that interpretation is quadratic *) + (* in the size of T. Therefore comparing the interpretations 'i1' and *) + (* 'i2' directly is more efficient than constructing the interpretation *) + (* for equality on T first, and "applying" this interpretation to 'i1' *) + (* and 'i2' in the usual way (cf. 'interpretation_apply') then. *) + + (* interpretation * interpretation -> interpretation *) + + fun make_equality (i1, i2) = + let + (* interpretation * interpretation -> prop_formula *) + fun equal (i1, i2) = + (case i1 of + Leaf xs => + (case i2 of + Leaf ys => PropLogic.dot_product (xs, ys) + | Node _ => raise REFUTE ("make_equality", "second interpretation is higher")) + | Node xs => + (case i2 of + Leaf _ => raise REFUTE ("make_equality", "first interpretation is higher") + | Node ys => PropLogic.all (map equal (xs ~~ ys)))) + (* interpretation * interpretation -> prop_formula *) + fun not_equal (i1, i2) = + (case i1 of + Leaf xs => + (case i2 of + Leaf ys => PropLogic.all ((PropLogic.exists xs) :: (PropLogic.exists ys) :: + (map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys))) (* defined and not equal *) + | Node _ => raise REFUTE ("make_equality", "second interpretation is higher")) + | Node xs => + (case i2 of + Leaf _ => raise REFUTE ("make_equality", "first interpretation is higher") + | Node ys => PropLogic.exists (map not_equal (xs ~~ ys)))) in + (* a value may be undefined; therefore 'not_equal' is not just the *) + (* negation of 'equal': *) + (* - two interpretations are 'equal' iff they are both defined and *) + (* denote the same value *) + (* - two interpretations are 'not_equal' iff they are both defined at *) + (* least partially, and a defined part denotes different values *) + (* - an undefined interpretation is neither 'equal' nor 'not_equal' to *) + (* another value *) + Leaf [equal (i1, i2), not_equal (i1, i2)] + end; + + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + (* simply typed lambda calculus: Isabelle's basic term syntax, with type *) + (* variables, function types, and propT *) + + fun stlc_interpreter thy model args t = + let + val (typs, terms) = model + val {maxvars, next_idx, bounds, wellformed} = args + (* Term.typ -> (interpretation * model * arguments) option *) + fun interpret_groundterm T = + let + (* unit -> (interpretation * model * arguments) option *) + fun interpret_groundtype () = + let + val size = (if T = Term.propT then 2 else (the o assoc) (typs, T)) (* the model MUST specify a size for ground types *) + val next = (if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 2 *) + val _ = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *) + (* prop_formula list *) + val fms = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)] + else (map BoolVar (next_idx upto (next_idx+size-1)))) + (* interpretation *) + val intr = Leaf fms + (* prop_formula list -> prop_formula *) + fun one_of_two_false [] = True + | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false xs) + (* prop_formula list -> prop_formula *) + fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs) + (* prop_formula *) + val wf = (if size=2 then True else exactly_one_true fms) + in + (* extend the model, increase 'next_idx', add well-formedness condition *) + Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)}) + end + in + case T of + Type ("fun", [T1, T2]) => + let + (* we create 'size_of_type (interpret (... T1))' different copies *) + (* of the interpretation for 'T2', which are then combined into a *) + (* single new interpretation *) + val (i1, _, _) = + (interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1)) + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + (* make fresh copies, with different variable indices *) + (* 'idx': next variable index *) + (* 'n' : number of copies *) + (* int -> int -> (int * interpretation list * prop_formula *) + fun make_copies idx 0 = + (idx, [], True) + | make_copies idx n = + let + val (copy, _, new_args) = + (interpret thy (typs, []) {maxvars = maxvars, next_idx = idx, bounds = [], wellformed = True} (Free ("dummy", T2)) + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + val (idx', copies, wf') = make_copies (#next_idx new_args) (n-1) + in + (idx', copy :: copies, SAnd (#wellformed new_args, wf')) + end + val (next, copies, wf) = make_copies next_idx (size_of_type i1) + (* combine copies into a single interpretation *) + val intr = Node copies + in + (* extend the model, increase 'next_idx', add well-formedness condition *) + Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)}) + end + | Type _ => interpret_groundtype () + | TFree _ => interpret_groundtype () + | TVar _ => interpret_groundtype () + end + in + case assoc (terms, t) of + Some intr => + (* return an existing interpretation *) + Some (intr, model, args) + | None => + (case t of + Const (_, T) => + interpret_groundterm T + | Free (_, T) => + interpret_groundterm T + | Var (_, T) => + interpret_groundterm T + | Bound i => + Some (nth_elem (i, #bounds args), model, args) + | Abs (x, T, body) => + let + (* create all constants of type 'T' *) + val (i, _, _) = + (interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + val constants = make_constants i + (* interpret the 'body' separately for each constant *) + val ((model', args'), bodies) = foldl_map + (fn ((m,a), c) => + let + (* add 'c' to 'bounds' *) + val (i', m', a') = interpret thy m {maxvars = #maxvars a, next_idx = #next_idx a, bounds = (c :: #bounds a), wellformed = #wellformed a} body + in + (* keep the new model m' and 'next_idx' and 'wellformed', but use old 'bounds' *) + ((m', {maxvars = maxvars, next_idx = #next_idx a', bounds = bounds, wellformed = #wellformed a'}), i') + end) + ((model, args), constants) + in + Some (Node bodies, model', args') + end + | t1 $ t2 => + let + (* auxiliary functions *) + (* interpretation * interpretation -> interpretation *) + fun interpretation_disjunction (tr1,tr2) = + tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2)) + (* prop_formula * interpretation -> interpretation *) + fun prop_formula_times_interpretation (fm,tr) = + tree_map (map (fn x => SAnd (fm,x))) tr + (* prop_formula list * interpretation list -> interpretation *) + fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) = + prop_formula_times_interpretation (fm,tr) + | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) = + interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees)) + | prop_formula_list_dot_product_interpretation_list (_,_) = + raise REFUTE ("stlc_interpreter", "empty list (in dot product)") + (* concatenates 'x' with every list in 'xss', returning a new list of lists *) + (* 'a -> 'a list list -> 'a list list *) + fun cons_list x xss = + map (fn xs => x::xs) xss + (* returns a list of lists, each one consisting of one element from each element of 'xss' *) + (* 'a list list -> 'a list list *) + fun pick_all [xs] = + map (fn x => [x]) xs + | pick_all (xs::xss) = + let val rec_pick = pick_all xss in + foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs) + end + | pick_all _ = + raise REFUTE ("stlc_interpreter", "empty list (in pick_all)") + (* interpretation -> prop_formula list *) + fun interpretation_to_prop_formula_list (Leaf xs) = + xs + | interpretation_to_prop_formula_list (Node trees) = + map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees)) + (* interpretation * interpretation -> interpretation *) + fun interpretation_apply (tr1,tr2) = + (case tr1 of + Leaf _ => + raise REFUTE ("stlc_interpreter", "first interpretation is a leaf") + | Node xs => + prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list tr2, xs)) + (* interpret 't1' and 't2' separately *) + val (intr1, model1, args1) = interpret thy model args t1 + val (intr2, model2, args2) = interpret thy model1 args1 t2 + in + Some (interpretation_apply (intr1,intr2), model2, args2) + end) + end; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun Pure_interpreter thy model args t = case t of - Free (x, Type ("set", [T])) => + Const ("all", _) $ t1 => (* in the meta-logic, 'all' MUST be followed by an argument term *) + let + val (i, m, a) = interpret thy model args t1 + in + case i of + Node xs => + let + val fmTrue = PropLogic.all (map toTrue xs) + val fmFalse = PropLogic.exists (map toFalse xs) + in + Some (Leaf [fmTrue, fmFalse], m, a) + end + | _ => + raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function") + end + | Const ("==", _) $ t1 $ t2 => + let + val (i1, m1, a1) = interpret thy model args t1 + val (i2, m2, a2) = interpret thy m1 a1 t2 + in + Some (make_equality (i1, i2), m2, a2) + end + | Const ("==>", _) => (* simpler than translating 'Const ("==>", _) $ t1 $ t2' *) + Some (Node [Node [TT, FF], Node [TT, TT]], model, args) + | _ => None; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun HOLogic_interpreter thy model args t = + let + (* Term.term -> int -> Term.term *) + fun eta_expand t i = + let + val Ts = binder_types (fastype_of t) + in + foldr (fn (T, t) => Abs ("", T, t)) + (take (i, Ts), list_comb (t, map Bound (i-1 downto 0))) + end + in + (* ------------------------------------------------------------------------- *) + (* Providing interpretations directly is more efficient than unfolding the *) + (* logical constants. IN HOL however, logical constants can themselves be *) + (* arguments. "All" and "Ex" are then translated just like any other *) + (* constant, with the relevant axiom being added by 'collect_axioms'. *) + (* ------------------------------------------------------------------------- *) + case t of + Const ("Trueprop", _) => + Some (Node [TT, FF], model, args) + | Const ("Not", _) => + Some (Node [FF, TT], model, args) + | Const ("True", _) => (* redundant, since 'True' is also an IDT constructor *) + Some (TT, model, args) + | Const ("False", _) => (* redundant, since 'False' is also an IDT constructor *) + Some (FF, model, args) + | Const ("All", _) $ t1 => let - (* interpretation list *) - val results = (case intr of - Node xs => xs - | _ => raise REFUTE ("var_settype_printer", "interpretation is a leaf")) - (* create all constants of type T *) - val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T)) - (* string list *) - val strings = mapfilter - (fn (argi,Leaf [fmTrue,fmFalse]) => - if PropLogic.eval assignment fmTrue then - Some (print thy model (Free ("x", T)) argi assignment) - else if PropLogic.eval assignment fmFalse then - None + val (i, m, a) = interpret thy model args t1 + in + case i of + Node xs => + let + val fmTrue = PropLogic.all (map toTrue xs) + val fmFalse = PropLogic.exists (map toFalse xs) + in + Some (Leaf [fmTrue, fmFalse], m, a) + end + | _ => + raise REFUTE ("HOLogic_interpreter", "\"All\" is not followed by a function") + end + | Const ("Ex", _) $ t1 => + let + val (i, m, a) = interpret thy model args t1 + in + case i of + Node xs => + let + val fmTrue = PropLogic.exists (map toTrue xs) + val fmFalse = PropLogic.all (map toFalse xs) + in + Some (Leaf [fmTrue, fmFalse], m, a) + end + | _ => + raise REFUTE ("HOLogic_interpreter", "\"Ex\" is not followed by a function") + end + | Const ("op =", _) $ t1 $ t2 => + let + val (i1, m1, a1) = interpret thy model args t1 + val (i2, m2, a2) = interpret thy m1 a1 t2 + in + Some (make_equality (i1, i2), m2, a2) + end + | Const ("op =", _) $ t1 => + (Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + | Const ("op =", _) => + (Some (interpret thy model args (eta_expand t 2)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + | Const ("op &", _) => + Some (Node [Node [TT, FF], Node [FF, FF]], model, args) + | Const ("op |", _) => + Some (Node [Node [TT, TT], Node [TT, FF]], model, args) + | Const ("op -->", _) => + Some (Node [Node [TT, FF], Node [TT, TT]], model, args) + | _ => None + end; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun set_interpreter thy model args t = + (* "T set" is isomorphic to "T --> bool" *) + let + val (typs, terms) = model + (* Term.term -> int -> Term.term *) + fun eta_expand t i = + let + val Ts = binder_types (fastype_of t) + in + foldr (fn (T, t) => Abs ("", T, t)) + (take (i, Ts), list_comb (t, map Bound (i-1 downto 0))) + end + in + case assoc (terms, t) of + Some intr => + (* return an existing interpretation *) + Some (intr, model, args) + | None => + (case t of + Free (x, Type ("set", [T])) => + (let + val (intr, _, args') = interpret thy (typs, []) args (Free (x, T --> HOLogic.boolT)) + in + Some (intr, (typs, (t, intr)::terms), args') + end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + | Var ((x,i), Type ("set", [T])) => + (let + val (intr, _, args') = interpret thy (typs, []) args (Var ((x,i), T --> HOLogic.boolT)) + in + Some (intr, (typs, (t, intr)::terms), args') + end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + | Const (s, Type ("set", [T])) => + (let + val (intr, _, args') = interpret thy (typs, []) args (Const (s, T --> HOLogic.boolT)) + in + Some (intr, (typs, (t, intr)::terms), args') + end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + (* 'Collect' == identity *) + | Const ("Collect", _) $ t1 => + Some (interpret thy model args t1) + | Const ("Collect", _) => + (Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + (* 'op :' == application *) + | Const ("op :", _) $ t1 $ t2 => + Some (interpret thy model args (t2 $ t1)) + | Const ("op :", _) $ t1 => + (Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + | Const ("op :", _) => + (Some (interpret thy model args (eta_expand t 2)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + | _ => None) + end; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun IDT_interpreter thy model args t = + let + val (typs, terms) = model + (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *) + fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) = + (* replace a 'DtTFree' variable by the associated type *) + (the o assoc) (typ_assoc, DatatypeAux.DtTFree a) + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) = + let + val (s, ds, _) = (the o assoc) (descr, i) + in + Type (s, map (typ_of_dtyp descr typ_assoc) ds) + end + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) = + Type (s, map (typ_of_dtyp descr typ_assoc) ds) + (* int list -> int *) + fun sum xs = foldl op+ (0, xs) + (* int list -> int *) + fun product xs = foldl op* (1, xs) + (* the size of an IDT is the sum (over its constructors) of the *) + (* product (over their arguments) of the size of the argument type *) + (* (Term.typ * int) list -> DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> (string * DatatypeAux.dtyp list) list -> int *) + fun size_of_dtyp typs descr typ_assoc constrs = + sum (map (fn (_, ds) => + product (map (fn d => + let + val T = typ_of_dtyp descr typ_assoc d + val (i, _, _) = + (interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + in + size_of_type i + end) ds)) constrs) + (* Term.typ -> (interpretation * model * arguments) option *) + fun interpret_variable (Type (s, Ts)) = + (case DatatypePackage.datatype_info thy s of + Some info => (* inductive datatype *) + let + val (typs, terms) = model + (* int option -- only recursive IDTs have an associated depth *) + val depth = assoc (typs, Type (s, Ts)) + in + if depth = (Some 0) then (* termination condition to avoid infinite recursion *) + (* return a leaf of size 0 *) + Some (Leaf [], model, args) + else + let + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = (the o assoc) (descr, index) + val typ_assoc = dtyps ~~ Ts + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = (if Library.exists (fn d => + case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_interpreter", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable") + else + ()) + (* if the model specifies a depth for the current type, decrement it to avoid infinite recursion *) + val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s, Ts), n-1))) + (* recursively compute the size of the datatype *) + val size = size_of_dtyp typs' descr typ_assoc constrs + val next_idx = #next_idx args + val next = (if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 2 *) + val _ = (if next-1>(#maxvars args) andalso (#maxvars args)>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *) + (* prop_formula list *) + val fms = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)] + else (map BoolVar (next_idx upto (next_idx+size-1)))) + (* interpretation *) + val intr = Leaf fms + (* prop_formula list -> prop_formula *) + fun one_of_two_false [] = True + | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false xs) + (* prop_formula list -> prop_formula *) + fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs) + (* prop_formula *) + val wf = (if size=2 then True else exactly_one_true fms) + in + (* extend the model, increase 'next_idx', add well-formedness condition *) + Some (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, next_idx = next, bounds = #bounds args, wellformed = SAnd (#wellformed args, wf)}) + end + end + | None => (* not an inductive datatype *) + None) + | interpret_variable _ = (* a (free or schematic) type variable *) + None + in + case assoc (terms, t) of + Some intr => + (* return an existing interpretation *) + Some (intr, model, args) + | None => + (case t of + Free (_, T) => interpret_variable T + | Var (_, T) => interpret_variable T + | Const (s, T) => + (* TODO: case, recursion, size *) + let + (* unit -> (interpretation * model * arguments) option *) + fun interpret_constructor () = + (case body_type T of + Type (s', Ts') => + (case DatatypePackage.datatype_info thy s' of + Some info => (* body type is an inductive datatype *) + let + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = (the o assoc) (descr, index) + val typ_assoc = dtyps ~~ Ts' + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = (if Library.exists (fn d => + case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_interpreter", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s', Ts')) ^ ") is not a variable") + else + ()) + (* split the constructors into those occuring before/after 'Const (s, T)' *) + val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) => + not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy), T, + map (typ_of_dtyp descr typ_assoc) ctypes ---> Type (s', Ts')))) constrs + in + case constrs2 of + [] => + (* 'Const (s, T)' is not a constructor of this datatype *) + None + | c::cs => + let + (* int option -- only recursive IDTs have an associated depth *) + val depth = assoc (typs, Type (s', Ts')) + val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s', Ts'), n-1))) + (* constructors before 'Const (s, T)' generate elements of the datatype *) + val offset = size_of_dtyp typs' descr typ_assoc constrs1 + (* 'Const (s, T)' and constructors after it generate elements of the datatype *) + val total = offset + (size_of_dtyp typs' descr typ_assoc constrs2) + (* create an interpretation that corresponds to the constructor 'Const (s, T)' *) + (* by recursion over its argument types *) + (* DatatypeAux.dtyp list -> interpretation *) + fun make_partial [] = + (* all entries of the leaf are 'False' *) + Leaf (replicate total False) + | make_partial (d::ds) = + let + (* compute the "new" size of the type 'd' *) + val T = typ_of_dtyp descr typ_assoc d + val (i, _, _) = + (interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + in + (* all entries of the whole subtree are 'False' *) + Node (replicate (size_of_type i) (make_partial ds)) + end + (* int * DatatypeAux.dtyp list -> int * interpretation *) + fun make_constr (offset, []) = + if offset= total") + | make_constr (offset, d::ds) = + let + (* compute the "new" and "old" size of the type 'd' *) + val T = typ_of_dtyp descr typ_assoc d + val (i, _, _) = + (interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + val (i', _, _) = + (interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + val size = size_of_type i + val size' = size_of_type i' + val _ = if size (* body type is not an inductive datatype *) + None) + | _ => (* body type is a (free or schematic) type variable *) + None) + in + case interpret_constructor () of + Some x => Some x + | None => interpret_variable T + end + | _ => None) + end; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + (* only an optimization: 'card' could in principle be interpreted with *) + (* interpreters available already (using its definition), but the code *) + (* below is much more efficient *) + + fun Finite_Set_card_interpreter thy model args t = + case t of + Const ("Finite_Set.card", Type ("fun", [Type ("set", [T]), Type ("nat", [])])) => + let + val (i_nat, _, _) = + (interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", []))) + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + val size_nat = size_of_type i_nat + val (i_set, _, _) = + (interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("set", [T]))) + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + val constants = make_constants i_set + (* interpretation -> int *) + fun number_of_elements (Node xs) = + foldl (fn (n, x) => + 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) + | number_of_elements (Leaf _) = + raise REFUTE ("Finite_Set_card_interpreter", "interpretation for set type is a leaf") + (* takes an interpretation for a set and returns an interpretation for a 'nat' *) + (* interpretation -> interpretation *) + fun card i = + let + val n = number_of_elements i + in + if n + | _ => + None; + + +(* ------------------------------------------------------------------------- *) +(* PRINTERS *) +(* ------------------------------------------------------------------------- *) + + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option *) + + fun stlc_printer thy model t intr assignment = + let + (* Term.term -> Term.typ option *) + fun typeof (Free (_, T)) = Some T + | typeof (Var (_, T)) = Some T + | typeof (Const (_, T)) = Some T + | typeof _ = None + (* string -> string *) + fun strip_leading_quote s = + (implode o (fn ss => case ss of [] => [] | x::xs => if x="'" then xs else ss) o explode) s + (* Term.typ -> string *) + fun string_of_typ (Type (s, _)) = s + | string_of_typ (TFree (x, _)) = strip_leading_quote x + | string_of_typ (TVar ((x,i), _)) = strip_leading_quote x ^ string_of_int i + (* interpretation -> int *) + fun index_from_interpretation (Leaf xs) = let - (* interpretation list *) - val results = (case intr of - Node xs => xs - | _ => raise REFUTE ("var_settype_printer", "interpretation is a leaf")) - (* create all constants of type T *) - val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T)) - (* string list *) - val strings = mapfilter - (fn (argi,Leaf [fmTrue,fmFalse]) => - if PropLogic.eval assignment fmTrue then - Some (print thy model (Free ("var_settype_printer", T)) argi assignment) - else if PropLogic.eval assignment fmTrue then - None - else - raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned")) - ((make_constants i) ~~ results) + val idx = find_index (PropLogic.eval assignment) xs in - Some (enclose "{" "}" (commas strings)) + if idx<0 then + raise REFUTE ("stlc_printer", "illegal interpretation: no value assigned (SAT solver unsound?)") + else + idx end - | _ => None + | index_from_interpretation _ = + raise REFUTE ("stlc_printer", "interpretation for ground type is not a leaf") + in + case typeof t of + Some T => + (case T of + Type ("fun", [T1, T2]) => + (let + (* create all constants of type 'T1' *) + val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1)) + val constants = make_constants i + (* interpretation list *) + val results = (case intr of + Node xs => xs + | _ => raise REFUTE ("stlc_printer", "interpretation for function type is a leaf")) + (* Term.term list *) + val pairs = map (fn (arg, result) => + HOLogic.mk_prod + (print thy model (Free ("dummy", T1)) arg assignment, + print thy model (Free ("dummy", T2)) result assignment)) + (constants ~~ results) + (* Term.typ *) + val HOLogic_prodT = HOLogic.mk_prodT (T1, T2) + val HOLogic_setT = HOLogic.mk_setT HOLogic_prodT + (* Term.term *) + val HOLogic_empty_set = Const ("{}", HOLogic_setT) + val HOLogic_insert = Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) + in + Some (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) (pairs, HOLogic_empty_set)) + end handle CANNOT_INTERPRET _ => None) + | Type ("prop", []) => + (case index_from_interpretation intr of + 0 => Some (HOLogic.mk_Trueprop HOLogic.true_const) + | 1 => Some (HOLogic.mk_Trueprop HOLogic.false_const) + | _ => raise REFUTE ("stlc_interpreter", "illegal interpretation for a propositional value")) + | Type _ => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T)) + | TFree _ => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T)) + | TVar _ => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))) + | None => + None end; (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *) - fun HOLogic_printer thy model t intr assignment = - case t of - (* 'arbitrary', 'The', 'Hilbert_Choice.Eps' are printed like free variables of the same type *) - Const ("arbitrary", T) => - Some (print thy model (Free ("", T)) intr assignment) - | Const ("The", T) => - Some (print thy model (Free ("", T)) intr assignment) - | Const ("Hilbert_Choice.Eps", T) => - Some (print thy model (Free ("", T)) intr assignment) + fun set_printer thy model t intr assignment = + let + (* Term.term -> Term.typ option *) + fun typeof (Free (_, T)) = Some T + | typeof (Var (_, T)) = Some T + | typeof (Const (_, T)) = Some T + | typeof _ = None + in + case typeof t of + Some (Type ("set", [T])) => + (let + (* create all constants of type 'T' *) + val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) + val constants = make_constants i + (* interpretation list *) + val results = (case intr of + Node xs => xs + | _ => raise REFUTE ("set_printer", "interpretation for set type is a leaf")) + (* Term.term list *) + val elements = mapfilter (fn (arg, result) => + case result of + Leaf [fmTrue, fmFalse] => + if PropLogic.eval assignment fmTrue then + Some (print thy model (Free ("dummy", T)) arg assignment) + else if PropLogic.eval assignment fmFalse then + None + else + raise REFUTE ("set_printer", "illegal interpretation: no value assigned (SAT solver unsound?)") + | _ => + raise REFUTE ("set_printer", "illegal interpretation for a Boolean value")) + (constants ~~ results) + (* Term.typ *) + val HOLogic_setT = HOLogic.mk_setT T + (* Term.term *) + val HOLogic_empty_set = Const ("{}", HOLogic_setT) + val HOLogic_insert = Const ("insert", T --> HOLogic_setT --> HOLogic_setT) + in + Some (foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) (HOLogic_empty_set, elements)) + end handle CANNOT_INTERPRET _ => None) | _ => - None; + None + end; - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *) + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option *) - fun var_IDT_printer thy model t intr assignment = + fun IDT_printer thy model t intr assignment = let - fun is_var (Free _) = true - | is_var (Var _) = true - | is_var _ = false - fun typeof (Free (_,T)) = T - | typeof (Var (_,T)) = T - | typeof _ = raise REFUTE ("var_IDT_printer", "term is not a variable") + (* Term.term -> Term.typ option *) + fun typeof (Free (_, T)) = Some T + | typeof (Var (_, T)) = Some T + | typeof (Const (_, T)) = Some T + | typeof _ = None in - if is_var t then - (case typeof t of - Type (s, Ts) => - (case DatatypePackage.datatype_info thy s of - Some info => (* inductive datatype *) - let - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = the (assoc (descr, index)) + case typeof t of + Some (Type (s, Ts)) => + (case DatatypePackage.datatype_info thy s of + Some info => (* inductive datatype *) + let + val (typs, _) = model + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = (the o assoc) (descr, index) + val typ_assoc = dtyps ~~ Ts + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = (if Library.exists (fn d => + case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_printer", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable") + else + ()) + (* the index of the element in the datatype *) + val element = (case intr of + Leaf xs => find_index (PropLogic.eval assignment) xs + | Node _ => raise REFUTE ("IDT_printer", "interpretation is not a leaf")) + val _ = (if element<0 then raise REFUTE ("IDT_printer", "invalid interpretation (no value assigned)") else ()) + (* int option -- only recursive IDTs have an associated depth *) + val depth = assoc (typs, Type (s, Ts)) + val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s, Ts), n-1))) + (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *) + fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) = + (* replace a 'DtTFree' variable by the associated type *) + (the o assoc) (typ_assoc, DatatypeAux.DtTFree a) + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) = + let + val (s, ds, _) = (the o assoc) (descr, i) + in + Type (s, map (typ_of_dtyp descr typ_assoc) ds) + end + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) = + Type (s, map (typ_of_dtyp descr typ_assoc) ds) + (* int list -> int *) + fun sum xs = foldl op+ (0, xs) + (* int list -> int *) + fun product xs = foldl op* (1, xs) + (* the size of an IDT is the sum (over its constructors) of the *) + (* product (over their arguments) of the size of the argument type *) + (* (Term.typ * int) list -> DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> (string * DatatypeAux.dtyp list) list -> int *) + fun size_of_dtyp typs descr typ_assoc xs = + sum (map (fn (_, ds) => + product (map (fn d => + let + val T = typ_of_dtyp descr typ_assoc d + val (i, _, _) = + (interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) in - if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then - raise REFUTE ("var_IDT_printer", "recursive datatype argument") - else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then - None (* recursive datatype (requires an infinite model) *) + size_of_type i + end) ds)) xs) + (* int -> DatatypeAux.dtyp list -> Term.term list *) + fun make_args n [] = + if n<>0 then + raise REFUTE ("IDT_printer", "error computing the element: remainder is not 0") else + [] + | make_args n (d::ds) = let - val (sizes, _) = model - val typ_assoc = dtyps ~~ Ts - (* interpretation -> int *) - fun index_from_interpretation (Leaf xs) = + val dT = typ_of_dtyp descr typ_assoc d + val (i, _, _) = + (interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", dT)) + handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t) + val size = size_of_type i + val consts = make_constants i (* we only need the (n mod size)-th element of *) + (* this list, so there might be a more efficient implementation that does not *) + (* generate all constants *) + in + (print thy (typs', []) (Free ("dummy", dT)) (nth_elem (n mod size, consts)) assignment)::(make_args (n div size) ds) + end + (* int -> (string * DatatypeAux.dtyp list) list -> Term.term *) + fun make_term _ [] = + raise REFUTE ("IDT_printer", "invalid interpretation (value too large - not enough constructors)") + | make_term n (c::cs) = + let + val c_size = size_of_dtyp typs' descr typ_assoc [c] + in + if n Type (s, Ts)) in - if idx<0 then - raise REFUTE ("var_IDT_printer", "illegal interpretation: no value assigned") - else - idx + foldl op$ (c_term, rev (make_args n (rev cargs))) end - | index_from_interpretation _ = - raise REFUTE ("var_IDT_printer", "interpretation is not a leaf") - (* string -> string *) - fun unqualify s = - implode (snd (take_suffix (fn c => c <> ".") (explode s))) - (* DatatypeAux.dtyp -> Term.typ *) - fun typ_of_dtyp (DatatypeAux.DtTFree a) = - the (assoc (typ_assoc, DatatypeAux.DtTFree a)) - | typ_of_dtyp (DatatypeAux.DtRec i) = - raise REFUTE ("var_IDT_printer", "recursive datatype") - | typ_of_dtyp (DatatypeAux.DtType (s, ds)) = - Type (s, map typ_of_dtyp ds) - fun sum xs = foldl op+ (0, xs) - fun product xs = foldl op* (1, xs) - (* power(a,b) computes a^b, for a>=0, b>=0 *) - (* int * int -> int *) - fun power (a,0) = 1 - | power (a,1) = a - | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end - fun size_of_interpretation (Leaf xs) = length xs - | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs) - fun size_of_type T = - let - val (i,_,_) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("", T)) - in - size_of_interpretation i - end - (* returns a list with all unit vectors of length n *) - (* int -> interpretation list *) - fun unit_vectors n = - let - (* returns the k-th unit vector of length n *) - (* int * int -> interpretation *) - fun unit_vector (k,n) = - Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) - (* int -> interpretation list -> interpretation list *) - fun unit_vectors_acc k vs = - if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs) - in - unit_vectors_acc 1 [] - end - (* concatenates 'x' with every list in 'xss', returning a new list of lists *) - (* 'a -> 'a list list -> 'a list list *) - fun cons_list x xss = - map (fn xs => x::xs) xss - (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *) - (* int -> 'a list -> 'a list list *) - fun pick_all 1 xs = - map (fn x => [x]) xs - | pick_all n xs = - let val rec_pick = pick_all (n-1) xs in - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs) - end - (* interpretation -> interpretation list *) - fun make_constants (Leaf xs) = - unit_vectors (length xs) - | make_constants (Node xs) = - map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) - (* DatatypeAux.dtyp list -> int -> string *) - fun string_of_inductive_type_cargs [] n = - if n<>0 then - raise REFUTE ("var_IDT_printer", "internal error computing the element index for an inductive type") - else - "" - | string_of_inductive_type_cargs (d::ds) n = - let - val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d)) ds) - val T = typ_of_dtyp d - val (i,_,_) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("", T)) - val constants = make_constants i - in - " " - ^ (print thy model (Free ("", T)) (nth_elem (n div size_ds, constants)) assignment) - ^ (string_of_inductive_type_cargs ds (n mod size_ds)) - end - (* (string * DatatypeAux.dtyp list) list -> int -> string *) - fun string_of_inductive_type_constrs [] n = - raise REFUTE ("var_IDT_printer", "inductive type has fewer elements than needed") - | string_of_inductive_type_constrs ((c,ds)::cs) n = - let - val size = product (map (fn d => size_of_type (typ_of_dtyp d)) ds) - in - if n < size then - (unqualify c) ^ (string_of_inductive_type_cargs ds n) - else - string_of_inductive_type_constrs cs (n - size) - end - in - Some (string_of_inductive_type_constrs constrs (index_from_interpretation intr)) + else + make_term (n-c_size) cs end - end - | None => None) - | _ => None) - else + in + Some (make_term element constrs) + end + | None => (* not an inductive datatype *) + None) + | _ => (* a (free or schematic) type variable *) None end; @@ -1786,27 +1921,22 @@ (* ------------------------------------------------------------------------- *) (* Note: the interpreters and printers are used in reverse order; however, *) (* an interpreter that can handle non-atomic terms ends up being *) -(* applied before other interpreters are applied to subterms! *) +(* applied before the 'stlc_interpreter' breaks the term apart into *) +(* subterms that are then passed to other interpreters! *) (* ------------------------------------------------------------------------- *) (* (theory -> theory) list *) val setup = [RefuteData.init, - add_interpreter "var_typevar" var_typevar_interpreter, - add_interpreter "var_funtype" var_funtype_interpreter, - add_interpreter "var_settype" var_settype_interpreter, - add_interpreter "boundvar" boundvar_interpreter, - add_interpreter "abstraction" abstraction_interpreter, - add_interpreter "apply" apply_interpreter, - add_interpreter "const_unfold" const_unfold_interpreter, - add_interpreter "Pure" Pure_interpreter, - add_interpreter "HOLogic" HOLogic_interpreter, - add_interpreter "IDT" IDT_interpreter, - add_printer "var_typevar" var_typevar_printer, - add_printer "var_funtype" var_funtype_printer, - add_printer "var_settype" var_settype_printer, - add_printer "HOLogic" HOLogic_printer, - add_printer "var_IDT" var_IDT_printer]; + add_interpreter "stlc" stlc_interpreter, + add_interpreter "Pure" Pure_interpreter, + add_interpreter "HOLogic" HOLogic_interpreter, + add_interpreter "set" set_interpreter, + add_interpreter "IDT" IDT_interpreter, + add_interpreter "Finite_Set.card" Finite_Set_card_interpreter, + add_printer "stlc" stlc_printer, + add_printer "set" set_printer, + add_printer "IDT" IDT_printer]; end