diff -r e3799716b733 -r 5b38730f3e12 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Sep 02 14:19:15 2010 +0200 +++ b/src/HOL/Tools/refute.ML Thu Sep 02 16:31:50 2010 +0200 @@ -72,22 +72,24 @@ val is_const_of_class: theory -> string * typ -> bool val string_of_typ : typ -> string val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ -end; (* signature REFUTE *) +end; + structure Refute : REFUTE = struct - open PropLogic; +open PropLogic; - (* We use 'REFUTE' only for internal error conditions that should *) - (* never occur in the first place (i.e. errors caused by bugs in our *) - (* code). Otherwise (e.g. to indicate invalid input data) we use *) - (* 'error'. *) - exception REFUTE of string * string; (* ("in function", "cause") *) +(* We use 'REFUTE' only for internal error conditions that should *) +(* never occur in the first place (i.e. errors caused by bugs in our *) +(* code). Otherwise (e.g. to indicate invalid input data) we use *) +(* 'error'. *) +exception REFUTE of string * string; (* ("in function", "cause") *) - (* should be raised by an interpreter when more variables would be *) - (* required than allowed by 'maxvars' *) - exception MAXVARS_EXCEEDED; +(* should be raised by an interpreter when more variables would be *) +(* required than allowed by 'maxvars' *) +exception MAXVARS_EXCEEDED; + (* ------------------------------------------------------------------------- *) (* TREES *) @@ -98,20 +100,20 @@ (* of (lists of ...) elements *) (* ------------------------------------------------------------------------- *) - datatype 'a tree = - Leaf of 'a - | Node of ('a tree) list; +datatype 'a tree = + Leaf of 'a + | Node of ('a tree) list; - (* ('a -> 'b) -> 'a tree -> 'b tree *) +(* ('a -> 'b) -> 'a tree -> 'b tree *) - fun tree_map f tr = - case tr of - Leaf x => Leaf (f x) - | Node xs => Node (map (tree_map f) xs); +fun tree_map f tr = + case tr of + Leaf x => Leaf (f x) + | Node xs => Node (map (tree_map f) xs); - (* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *) +(* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *) - fun tree_foldl f = +fun tree_foldl f = let fun itl (e, Leaf x) = f(e,x) | itl (e, Node xs) = Library.foldl (tree_foldl f) (e,xs) @@ -119,16 +121,16 @@ itl end; - (* 'a tree * 'b tree -> ('a * 'b) tree *) +(* 'a tree * 'b tree -> ('a * 'b) tree *) - fun tree_pair (t1, t2) = - case t1 of - Leaf x => +fun tree_pair (t1, t2) = + case t1 of + Leaf x => (case t2 of Leaf y => Leaf (x,y) | Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)")) - | Node xs => + | Node xs => (case t2 of (* '~~' will raise an exception if the number of branches in *) (* both trees is different at the current node *) @@ -160,68 +162,68 @@ (* "unknown"). *) (* ------------------------------------------------------------------------- *) - type params = - { - sizes : (string * int) list, - minsize : int, - maxsize : int, - maxvars : int, - maxtime : int, - satsolver: string, - no_assms : bool, - expect : string - }; +type params = + { + sizes : (string * int) list, + minsize : int, + maxsize : int, + maxvars : int, + maxtime : int, + satsolver: string, + no_assms : bool, + expect : string + }; (* ------------------------------------------------------------------------- *) (* interpretation: a term's interpretation is given by a variable of type *) (* 'interpretation' *) (* ------------------------------------------------------------------------- *) - type interpretation = - prop_formula list tree; +type interpretation = + prop_formula list tree; (* ------------------------------------------------------------------------- *) (* model: a model specifies the size of types and the interpretation of *) (* terms *) (* ------------------------------------------------------------------------- *) - type model = - (typ * int) list * (term * interpretation) list; +type model = + (typ * int) list * (term * interpretation) list; (* ------------------------------------------------------------------------- *) (* arguments: additional arguments required during interpretation of terms *) (* ------------------------------------------------------------------------- *) - type arguments = - { - (* just passed unchanged from 'params': *) - maxvars : int, - (* whether to use 'make_equality' or 'make_def_equality': *) - def_eq : bool, - (* the following may change during the translation: *) - next_idx : int, - bounds : interpretation list, - wellformed: prop_formula - }; +type arguments = + { + (* just passed unchanged from 'params': *) + maxvars : int, + (* whether to use 'make_equality' or 'make_def_equality': *) + def_eq : bool, + (* the following may change during the translation: *) + next_idx : int, + bounds : interpretation list, + wellformed: prop_formula + }; - structure RefuteData = Theory_Data - ( - type T = - {interpreters: (string * (theory -> model -> arguments -> term -> - (interpretation * model * arguments) option)) list, - printers: (string * (theory -> model -> typ -> interpretation -> - (int -> bool) -> term option)) list, - parameters: string Symtab.table}; - val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; - val extend = I; - fun merge - ({interpreters = in1, printers = pr1, parameters = pa1}, - {interpreters = in2, printers = pr2, parameters = pa2}) : T = - {interpreters = AList.merge (op =) (K true) (in1, in2), - printers = AList.merge (op =) (K true) (pr1, pr2), - parameters = Symtab.merge (op=) (pa1, pa2)}; - ); +structure RefuteData = Theory_Data +( + type T = + {interpreters: (string * (theory -> model -> arguments -> term -> + (interpretation * model * arguments) option)) list, + printers: (string * (theory -> model -> typ -> interpretation -> + (int -> bool) -> term option)) list, + parameters: string Symtab.table}; + val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; + val extend = I; + fun merge + ({interpreters = in1, printers = pr1, parameters = pa1}, + {interpreters = in2, printers = pr2, parameters = pa2}) : T = + {interpreters = AList.merge (op =) (K true) (in1, in2), + printers = AList.merge (op =) (K true) (pr1, pr2), + parameters = Symtab.merge (op=) (pa1, pa2)}; +); (* ------------------------------------------------------------------------- *) @@ -230,30 +232,30 @@ (* track of the interpretation of subterms *) (* ------------------------------------------------------------------------- *) - (* 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) +fun interpret thy model args t = + case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of - NONE => raise REFUTE ("interpret", - "no interpreter for term " ^ quote (Syntax.string_of_term_global thy t)) - | SOME x => x; + NONE => raise REFUTE ("interpret", + "no interpreter for term " ^ quote (Syntax.string_of_term_global thy t)) + | SOME x => x; (* ------------------------------------------------------------------------- *) (* print: converts the interpretation 'intr', which must denote a term of *) (* type 'T', into a term using a suitable printer *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> Term.typ -> interpretation -> (int -> bool) -> - Term.term *) +(* theory -> model -> Term.typ -> interpretation -> (int -> bool) -> + Term.term *) - fun print thy model T intr assignment = - case get_first (fn (_, f) => f thy model T intr assignment) +fun print thy model T intr assignment = + case get_first (fn (_, f) => f thy model T intr assignment) (#printers (RefuteData.get thy)) of - NONE => raise REFUTE ("print", - "no printer for type " ^ quote (Syntax.string_of_typ_global thy T)) - | SOME x => x; + NONE => raise REFUTE ("print", + "no printer for type " ^ quote (Syntax.string_of_typ_global thy T)) + | SOME x => x; (* ------------------------------------------------------------------------- *) (* print_model: turns the model into a string, using a fixed interpretation *) @@ -261,9 +263,9 @@ (* printers *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> (int -> bool) -> string *) +(* theory -> model -> (int -> bool) -> string *) - fun print_model thy model assignment = +fun print_model thy model assignment = let val (typs, terms) = model val typs_msg = @@ -298,29 +300,29 @@ (* PARAMETER MANAGEMENT *) (* ------------------------------------------------------------------------- *) - (* string -> (theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option) -> theory -> theory *) +(* string -> (theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option) -> theory -> theory *) - fun add_interpreter name f thy = +fun add_interpreter name f thy = let val {interpreters, printers, parameters} = RefuteData.get thy in case AList.lookup (op =) interpreters name of - NONE => RefuteData.put {interpreters = (name, f) :: interpreters, - printers = printers, parameters = parameters} thy + NONE => RefuteData.put {interpreters = (name, f) :: interpreters, + printers = printers, parameters = parameters} thy | SOME _ => error ("Interpreter " ^ name ^ " already declared") end; - (* string -> (theory -> model -> Term.typ -> interpretation -> - (int -> bool) -> Term.term option) -> theory -> theory *) +(* string -> (theory -> model -> Term.typ -> interpretation -> + (int -> bool) -> Term.term option) -> theory -> theory *) - fun add_printer name f thy = +fun add_printer name f thy = let val {interpreters, printers, parameters} = RefuteData.get thy in case AList.lookup (op =) printers name of - NONE => RefuteData.put {interpreters = interpreters, - printers = (name, f) :: printers, parameters = parameters} thy + NONE => RefuteData.put {interpreters = interpreters, + printers = (name, f) :: printers, parameters = parameters} thy | SOME _ => error ("Printer " ^ name ^ " already declared") end; @@ -329,30 +331,30 @@ (* parameter table *) (* ------------------------------------------------------------------------- *) - (* (string * string) -> theory -> theory *) +(* (string * string) -> theory -> theory *) - fun set_default_param (name, value) = RefuteData.map - (fn {interpreters, printers, parameters} => - {interpreters = interpreters, printers = printers, - parameters = Symtab.update (name, value) parameters}); +fun set_default_param (name, value) = RefuteData.map + (fn {interpreters, printers, parameters} => + {interpreters = interpreters, printers = printers, + parameters = Symtab.update (name, value) parameters}); (* ------------------------------------------------------------------------- *) (* get_default_param: retrieves the value associated with 'name' from *) (* RefuteData's parameter table *) (* ------------------------------------------------------------------------- *) - (* theory -> string -> string option *) +(* theory -> string -> string option *) - val get_default_param = Symtab.lookup o #parameters o RefuteData.get; +val get_default_param = Symtab.lookup o #parameters o RefuteData.get; (* ------------------------------------------------------------------------- *) (* get_default_params: returns a list of all '(name, value)' pairs that are *) (* stored in RefuteData's parameter table *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * string) list *) +(* theory -> (string * string) list *) - val get_default_params = Symtab.dest o #parameters o RefuteData.get; +val get_default_params = Symtab.dest o #parameters o RefuteData.get; (* ------------------------------------------------------------------------- *) (* actual_params: takes a (possibly empty) list 'params' of parameters that *) @@ -360,9 +362,9 @@ (* returns a record that can be passed to 'find_model'. *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * string) list -> params *) +(* theory -> (string * string) list -> params *) - fun actual_params thy override = +fun actual_params thy override = let (* (string * string) list * string -> bool *) fun read_bool (parms, name) = @@ -370,32 +372,33 @@ SOME "true" => true | SOME "false" => false | SOME s => error ("parameter " ^ quote name ^ - " (value is " ^ quote s ^ ") must be \"true\" or \"false\"") + " (value is " ^ quote s ^ ") must be \"true\" or \"false\"") | NONE => error ("parameter " ^ quote name ^ " must be assigned a value") (* (string * string) list * string -> int *) fun read_int (parms, name) = case AList.lookup (op =) parms name of - SOME s => (case Int.fromString s of - SOME i => i - | NONE => error ("parameter " ^ quote name ^ - " (value is " ^ quote s ^ ") must be an integer value")) - | NONE => error ("parameter " ^ quote name ^ + SOME s => + (case Int.fromString s of + SOME i => i + | NONE => error ("parameter " ^ quote name ^ + " (value is " ^ quote s ^ ") must be an integer value")) + | NONE => error ("parameter " ^ quote name ^ " must be assigned a value") (* (string * string) list * string -> string *) fun read_string (parms, name) = case AList.lookup (op =) parms name of SOME s => s - | NONE => error ("parameter " ^ quote name ^ + | NONE => error ("parameter " ^ quote name ^ " must be assigned a value") (* 'override' first, defaults last: *) (* (string * string) list *) val allparams = override @ (get_default_params thy) (* 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") + 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") val no_assms = read_bool (allparams, "no_assms") @@ -405,7 +408,7 @@ (* 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 = map_filter + val sizes = map_filter (fn (name, value) => Option.map (pair name) (Int.fromString value)) (filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize" andalso name<>"maxvars" andalso name<>"maxtime" @@ -420,25 +423,25 @@ (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) (* ------------------------------------------------------------------------- *) - fun typ_of_dtyp descr typ_assoc (Datatype_Aux.DtTFree a) = - (* replace a 'DtTFree' variable by the associated type *) - the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a)) - | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, ds)) = - Type (s, map (typ_of_dtyp descr typ_assoc) ds) - | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) = - let - val (s, ds, _) = the (AList.lookup (op =) descr i) - in +fun typ_of_dtyp descr typ_assoc (Datatype_Aux.DtTFree a) = + (* replace a 'DtTFree' variable by the associated type *) + the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a)) + | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, ds)) = Type (s, map (typ_of_dtyp descr typ_assoc) ds) - end; + | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) = + let + val (s, ds, _) = the (AList.lookup (op =) descr i) + in + Type (s, map (typ_of_dtyp descr typ_assoc) ds) + end; (* ------------------------------------------------------------------------- *) (* close_form: universal closure over schematic variables in 't' *) (* ------------------------------------------------------------------------- *) - (* Term.term -> Term.term *) +(* Term.term -> Term.term *) - fun close_form t = +fun close_form t = let (* (Term.indexname * Term.typ) list *) val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t)) @@ -455,9 +458,9 @@ (* denotes membership to an axiomatic type class *) (* ------------------------------------------------------------------------- *) - (* theory -> string * Term.typ -> bool *) +(* theory -> string * Term.typ -> bool *) - fun is_const_of_class thy (s, T) = +fun is_const_of_class thy (s, T) = let val class_const_names = map Logic.const_of_class (Sign.all_classes thy) in @@ -471,28 +474,26 @@ (* of an inductive datatype in 'thy' *) (* ------------------------------------------------------------------------- *) - (* theory -> string * Term.typ -> bool *) +(* theory -> string * Term.typ -> bool *) - fun is_IDT_constructor thy (s, T) = - (case body_type T of - Type (s', _) => +fun is_IDT_constructor thy (s, T) = + (case body_type T of + Type (s', _) => (case Datatype.get_constrs thy s' of SOME constrs => - List.exists (fn (cname, cty) => - cname = s andalso Sign.typ_instance thy (T, cty)) constrs - | NONE => - false) - | _ => - false); + List.exists (fn (cname, cty) => + cname = s andalso Sign.typ_instance thy (T, cty)) constrs + | NONE => false) + | _ => false); (* ------------------------------------------------------------------------- *) (* is_IDT_recursor: returns 'true' iff 'Const (s, T)' is the recursion *) (* operator of an inductive datatype in 'thy' *) (* ------------------------------------------------------------------------- *) - (* theory -> string * Term.typ -> bool *) +(* theory -> string * Term.typ -> bool *) - fun is_IDT_recursor thy (s, T) = +fun is_IDT_recursor thy (s, T) = let val rec_names = Symtab.fold (append o #rec_names o snd) (Datatype.get_all thy) [] @@ -506,12 +507,12 @@ (* norm_rhs: maps f ?t1 ... ?tn == rhs to %t1...tn. rhs *) (* ------------------------------------------------------------------------- *) - fun norm_rhs eqn = +fun norm_rhs eqn = let fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t)) - | lambda v t = raise TERM ("lambda", [v, t]) + | lambda v t = raise TERM ("lambda", [v, t]) val (lhs, rhs) = Logic.dest_equals eqn - val (_, args) = Term.strip_comb lhs + val (_, args) = Term.strip_comb lhs in fold lambda (rev args) rhs end @@ -520,31 +521,31 @@ (* get_def: looks up the definition of a constant *) (* ------------------------------------------------------------------------- *) - (* theory -> string * Term.typ -> (string * Term.term) option *) +(* theory -> string * Term.typ -> (string * Term.term) option *) - fun get_def thy (s, T) = +fun get_def thy (s, T) = let (* (string * Term.term) list -> (string * Term.term) option *) fun get_def_ax [] = NONE | get_def_ax ((axname, ax) :: axioms) = - (let - val (lhs, _) = Logic.dest_equals ax (* equations only *) - val c = Term.head_of lhs - val (s', T') = Term.dest_Const c - in - if s=s' then - let - val typeSubs = Sign.typ_match thy (T', T) Vartab.empty - val ax' = monomorphic_term typeSubs ax - val rhs = norm_rhs ax' + (let + val (lhs, _) = Logic.dest_equals ax (* equations only *) + val c = Term.head_of lhs + val (s', T') = Term.dest_Const c in - SOME (axname, rhs) - end - else - get_def_ax axioms - end handle ERROR _ => get_def_ax axioms - | TERM _ => get_def_ax axioms - | Type.TYPE_MATCH => get_def_ax axioms) + if s=s' then + let + val typeSubs = Sign.typ_match thy (T', T) Vartab.empty + val ax' = monomorphic_term typeSubs ax + val rhs = norm_rhs ax' + in + SOME (axname, rhs) + end + else + get_def_ax axioms + end handle ERROR _ => get_def_ax axioms + | TERM _ => get_def_ax axioms + | Type.TYPE_MATCH => get_def_ax axioms) in get_def_ax (Theory.all_axioms_of thy) end; @@ -553,43 +554,42 @@ (* get_typedef: looks up the definition of a type, as created by "typedef" *) (* ------------------------------------------------------------------------- *) - (* theory -> Term.typ -> (string * Term.term) option *) +(* theory -> Term.typ -> (string * Term.term) option *) - fun get_typedef thy T = +fun get_typedef thy T = let (* (string * Term.term) list -> (string * Term.term) option *) fun get_typedef_ax [] = NONE | get_typedef_ax ((axname, ax) :: axioms) = - (let - (* Term.term -> Term.typ option *) - fun type_of_type_definition (Const (s', T')) = - if s'= @{const_name 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 = Sign.typ_match thy (T'', T) Vartab.empty + (let + (* Term.term -> Term.typ option *) + fun type_of_type_definition (Const (s', T')) = + if s'= @{const_name 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 - SOME (axname, monomorphic_term typeSubs ax) - end - | NONE => - get_typedef_ax axioms - end handle ERROR _ => get_typedef_ax axioms - | TERM _ => get_typedef_ax axioms - | Type.TYPE_MATCH => get_typedef_ax axioms) + case type_of_type_definition ax of + SOME T' => + let + val T'' = (domain_type o domain_type) T' + val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty + in + SOME (axname, monomorphic_term typeSubs ax) + end + | NONE => get_typedef_ax axioms + end handle ERROR _ => get_typedef_ax axioms + | TERM _ => get_typedef_ax axioms + | Type.TYPE_MATCH => get_typedef_ax axioms) in get_typedef_ax (Theory.all_axioms_of thy) end; @@ -599,9 +599,9 @@ (* created by the "axclass" command *) (* ------------------------------------------------------------------------- *) - (* theory -> string -> (string * Term.term) option *) +(* theory -> string -> (string * Term.term) option *) - fun get_classdef thy class = +fun get_classdef thy class = let val axname = class ^ "_class_def" in @@ -617,15 +617,15 @@ (* that definition does not need to be unfolded *) (* ------------------------------------------------------------------------- *) - (* theory -> Term.term -> Term.term *) +(* theory -> Term.term -> Term.term *) - (* Note: we could intertwine unfolding of constants and beta-(eta-) *) - (* normalization; this would save some unfolding for terms where *) - (* constants are eliminated by beta-reduction (e.g. 'K c1 c2'). On *) - (* the other hand, this would cause additional work for terms where *) - (* constants are duplicated by beta-reduction (e.g. 'S c1 c2 c3'). *) +(* Note: we could intertwine unfolding of constants and beta-(eta-) *) +(* normalization; this would save some unfolding for terms where *) +(* constants are eliminated by beta-reduction (e.g. 'K c1 c2'). On *) +(* the other hand, this would cause additional work for terms where *) +(* constants are duplicated by beta-reduction (e.g. 'S c1 c2 c3'). *) - fun unfold_defs thy t = +fun unfold_defs thy t = let (* Term.term -> Term.term *) fun unfold_loop t = @@ -658,13 +658,13 @@ | Const (@{const_name Finite_Set.card}, _) => t | Const (@{const_name Finite_Set.finite}, _) => t | Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat}, - Type ("fun", [@{typ nat}, @{typ bool}])])) => t + Type ("fun", [@{typ nat}, @{typ bool}])])) => t | Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat}, - Type ("fun", [@{typ nat}, @{typ nat}])])) => t + Type ("fun", [@{typ nat}, @{typ nat}])])) => t | Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat}, - Type ("fun", [@{typ nat}, @{typ nat}])])) => t + Type ("fun", [@{typ nat}, @{typ nat}])])) => t | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat}, - Type ("fun", [@{typ nat}, @{typ nat}])])) => t + Type ("fun", [@{typ nat}, @{typ nat}])])) => t | Const (@{const_name List.append}, _) => t (* UNSOUND | Const (@{const_name lfp}, _) => t @@ -674,27 +674,28 @@ | Const (@{const_name snd}, _) => t (* simply-typed lambda calculus *) | Const (s, T) => - (if is_IDT_constructor thy (s, T) - orelse is_IDT_recursor thy (s, T) then - t (* do not unfold IDT constructors/recursors *) - (* unfold the constant if there is a defining equation *) - else case get_def thy (s, T) of - SOME (axname, rhs) => - (* Note: if the term to be unfolded (i.e. 'Const (s, T)') *) - (* occurs on the right-hand side of the equation, i.e. in *) - (* 'rhs', we must not use this equation to unfold, because *) - (* that would loop. Here would be the right place to *) - (* check this. However, getting this really right seems *) - (* difficult because the user may state arbitrary axioms, *) - (* which could interact with overloading to create loops. *) - ((*tracing (" unfolding: " ^ axname);*) - unfold_loop rhs) - | NONE => t) - | Free _ => t - | Var _ => t - | Bound _ => t + (if is_IDT_constructor thy (s, T) + orelse is_IDT_recursor thy (s, T) then + t (* do not unfold IDT constructors/recursors *) + (* unfold the constant if there is a defining equation *) + else + case get_def thy (s, T) of + SOME (axname, rhs) => + (* Note: if the term to be unfolded (i.e. 'Const (s, T)') *) + (* occurs on the right-hand side of the equation, i.e. in *) + (* 'rhs', we must not use this equation to unfold, because *) + (* that would loop. Here would be the right place to *) + (* check this. However, getting this really right seems *) + (* difficult because the user may state arbitrary axioms, *) + (* which could interact with overloading to create loops. *) + ((*tracing (" unfolding: " ^ axname);*) + unfold_loop rhs) + | NONE => t) + | Free _ => t + | Var _ => t + | Bound _ => t | Abs (s, T, body) => Abs (s, T, unfold_loop body) - | t1 $ t2 => (unfold_loop t1) $ (unfold_loop t2) + | t1 $ t2 => (unfold_loop t1) $ (unfold_loop t2) val result = Envir.beta_eta_contract (unfold_loop t) in result @@ -705,27 +706,27 @@ (* versions of) all HOL axioms that are relevant w.r.t 't' *) (* ------------------------------------------------------------------------- *) - (* Note: 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 *) +(* Note: 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 *) - (* Note: currently we use "inverse" functions to the definitional *) - (* mechanisms provided by Isabelle/HOL, e.g. for "axclass", *) - (* "typedef", "definition". A more general approach could consider *) - (* *every* axiom of the theory and collect it if it has a constant/ *) - (* type/typeclass in common with the term 't'. *) +(* Note: currently we use "inverse" functions to the definitional *) +(* mechanisms provided by Isabelle/HOL, e.g. for "axclass", *) +(* "typedef", "definition". A more general approach could consider *) +(* *every* axiom of the theory and collect it if it has a constant/ *) +(* type/typeclass in common with the term 't'. *) - (* theory -> Term.term -> Term.term list *) +(* 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. *) +(* 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. *) - (* To avoid collecting the same axiom multiple times, we use an *) - (* accumulator 'axs' which contains all axioms collected so far. *) +(* To avoid collecting the same axiom multiple times, we use an *) +(* accumulator 'axs' which contains all axioms collected so far. *) - fun collect_axioms thy t = +fun collect_axioms thy t = let val _ = tracing "Adding axioms..." val axioms = Theory.all_axioms_of thy @@ -782,7 +783,7 @@ | NONE => (case get_typedef thy T of SOME (axname, ax) => - collect_this_axiom (axname, ax) axs + collect_this_axiom (axname, ax) axs | NONE => (* unspecified type, perhaps introduced with "typedecl" *) (* at least collect relevant type axioms for the argument types *) @@ -808,19 +809,19 @@ | Const (@{const_name False}, _) => axs | Const (@{const_name undefined}, T) => collect_type_axioms T axs | Const (@{const_name The}, T) => - let - val ax = specialize_type thy (@{const_name The}, T) - (the (AList.lookup (op =) axioms "HOL.the_eq_trivial")) - in - collect_this_axiom ("HOL.the_eq_trivial", ax) axs - end + let + val ax = specialize_type thy (@{const_name The}, T) + (the (AList.lookup (op =) axioms "HOL.the_eq_trivial")) + in + collect_this_axiom ("HOL.the_eq_trivial", ax) axs + end | Const (@{const_name Hilbert_Choice.Eps}, T) => - let - val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T) - (the (AList.lookup (op =) axioms "Hilbert_Choice.someI")) - in - collect_this_axiom ("Hilbert_Choice.someI", ax) axs - end + let + val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T) + (the (AList.lookup (op =) axioms "Hilbert_Choice.someI")) + in + collect_this_axiom ("Hilbert_Choice.someI", ax) axs + end | Const (@{const_name All}, T) => collect_type_axioms T axs | Const (@{const_name Ex}, T) => collect_type_axioms T axs | Const (@{const_name HOL.eq}, T) => collect_type_axioms T axs @@ -898,70 +899,70 @@ (* and all mutually recursive IDTs are considered. *) (* ------------------------------------------------------------------------- *) - fun ground_types thy t = +fun ground_types thy t = let fun collect_types T acc = (case T of Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc) - | Type ("prop", []) => acc - | Type (s, Ts) => - (case Datatype.get_info thy s of - SOME info => (* inductive datatype *) - let - val index = #index info - val descr = #descr info - val (_, typs, _) = the (AList.lookup (op =) descr index) - val typ_assoc = typs ~~ Ts - (* sanity check: every element in 'dtyps' must be a *) - (* 'DtTFree' *) - val _ = if Library.exists (fn d => - case d of Datatype_Aux.DtTFree _ => false | _ => true) typs then - raise REFUTE ("ground_types", "datatype argument (for type " - ^ Syntax.string_of_typ_global thy T ^ ") is not a variable") - else () - (* required for mutually recursive datatypes; those need to *) - (* be added even if they are an instance of an otherwise non- *) - (* recursive datatype *) - fun collect_dtyp d acc = - let - val dT = typ_of_dtyp descr typ_assoc d - in - case d of - Datatype_Aux.DtTFree _ => - collect_types dT acc - | Datatype_Aux.DtType (_, ds) => - collect_types dT (fold_rev collect_dtyp ds acc) - | Datatype_Aux.DtRec i => - if member (op =) acc dT then - acc (* prevent infinite recursion *) - else + | Type ("prop", []) => acc + | Type (s, Ts) => + (case Datatype.get_info thy s of + SOME info => (* inductive datatype *) + let + val index = #index info + val descr = #descr info + val (_, typs, _) = the (AList.lookup (op =) descr index) + val typ_assoc = typs ~~ Ts + (* sanity check: every element in 'dtyps' must be a *) + (* 'DtTFree' *) + val _ = if Library.exists (fn d => + case d of Datatype_Aux.DtTFree _ => false | _ => true) typs then + raise REFUTE ("ground_types", "datatype argument (for type " + ^ Syntax.string_of_typ_global thy T ^ ") is not a variable") + else () + (* required for mutually recursive datatypes; those need to *) + (* be added even if they are an instance of an otherwise non- *) + (* recursive datatype *) + fun collect_dtyp d acc = let - val (_, dtyps, dconstrs) = the (AList.lookup (op =) descr i) - (* if the current type is a recursive IDT (i.e. a depth *) - (* is required), add it to 'acc' *) - val acc_dT = if Library.exists (fn (_, ds) => - Library.exists Datatype_Aux.is_rec_type ds) dconstrs then - insert (op =) dT acc - else acc - (* collect argument types *) - val acc_dtyps = fold_rev collect_dtyp dtyps acc_dT - (* collect constructor types *) - val acc_dconstrs = fold_rev collect_dtyp (maps snd dconstrs) acc_dtyps + val dT = typ_of_dtyp descr typ_assoc d in - acc_dconstrs + case d of + Datatype_Aux.DtTFree _ => + collect_types dT acc + | Datatype_Aux.DtType (_, ds) => + collect_types dT (fold_rev collect_dtyp ds acc) + | Datatype_Aux.DtRec i => + if member (op =) acc dT then + acc (* prevent infinite recursion *) + else + let + val (_, dtyps, dconstrs) = the (AList.lookup (op =) descr i) + (* if the current type is a recursive IDT (i.e. a depth *) + (* is required), add it to 'acc' *) + val acc_dT = if Library.exists (fn (_, ds) => + Library.exists Datatype_Aux.is_rec_type ds) dconstrs then + insert (op =) dT acc + else acc + (* collect argument types *) + val acc_dtyps = fold_rev collect_dtyp dtyps acc_dT + (* collect constructor types *) + val acc_dconstrs = fold_rev collect_dtyp (maps snd dconstrs) acc_dtyps + in + acc_dconstrs + end end - end - in - (* argument types 'Ts' could be added here, but they are also *) - (* added by 'collect_dtyp' automatically *) - collect_dtyp (Datatype_Aux.DtRec index) acc - end - | NONE => - (* not an inductive datatype, e.g. defined via "typedef" or *) - (* "typedecl" *) - insert (op =) T (fold collect_types Ts acc)) - | TFree _ => insert (op =) T acc - | TVar _ => insert (op =) T acc) + in + (* argument types 'Ts' could be added here, but they are also *) + (* added by 'collect_dtyp' automatically *) + collect_dtyp (Datatype_Aux.DtRec index) acc + end + | NONE => + (* not an inductive datatype, e.g. defined via "typedef" or *) + (* "typedecl" *) + insert (op =) T (fold collect_types Ts acc)) + | TFree _ => insert (op =) T acc + | TVar _ => insert (op =) T acc) in fold_types collect_types t [] end; @@ -973,11 +974,11 @@ (* list") are identified. *) (* ------------------------------------------------------------------------- *) - (* Term.typ -> string *) +(* Term.typ -> string *) - fun string_of_typ (Type (s, _)) = s - | string_of_typ (TFree (s, _)) = s - | string_of_typ (TVar ((s,_), _)) = s; +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 *) @@ -985,9 +986,9 @@ (* 'sizes' *) (* ------------------------------------------------------------------------- *) - (* Term.typ list -> (string * int) list -> int -> (Term.typ * int) list *) +(* Term.typ list -> (string * int) list -> int -> (Term.typ * int) list *) - fun first_universe xs sizes minsize = +fun first_universe xs sizes minsize = let fun size_of_typ T = case AList.lookup (op =) sizes (string_of_typ T) of @@ -1004,39 +1005,39 @@ (* type may have a fixed size given in 'sizes' *) (* ------------------------------------------------------------------------- *) - (* (Term.typ * int) list -> (string * int) list -> int -> int -> - (Term.typ * int) list option *) +(* (Term.typ * int) list -> (string * int) list -> int -> int -> + (Term.typ * int) list option *) - fun next_universe xs sizes minsize maxsize = +fun next_universe xs sizes minsize maxsize = let (* 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 + if sum = 0 then + SOME [] + else + NONE | make_first max len sum = - if sum<=max orelse max<0 then - Option.map (fn xs' => sum :: xs') (make_first max (len-1) 0) - else - Option.map (fn xs' => max :: xs') (make_first max (len-1) (sum-max)) + if sum <= max orelse max < 0 then + Option.map (fn xs' => sum :: xs') (make_first max (len-1) 0) + else + Option.map (fn xs' => max :: xs') (make_first max (len-1) (sum-max)) (* enumerates all int lists with a fixed length, where 0<=x<='max' for *) (* all list elements x (unless 'max'<0) *) (* int -> int -> int -> int list -> int list option *) fun next max len sum [] = - NONE + NONE | next max len sum [x] = - (* we've reached the last list element, so there's no shift possible *) - make_first max (len+1) (sum+x+1) (* increment 'sum' by 1 *) + (* we've reached the last list element, so there's no shift possible *) + make_first max (len+1) (sum+x+1) (* increment 'sum' by 1 *) | next max len sum (x1::x2::xs) = - if x1>0 andalso (x20 andalso (x2 - (* merge with those types for which the size is fixed *) - SOME (fst (fold_map (fn (T, _) => fn ds => - case AList.lookup (op =) sizes (string_of_typ T) of - (* return the fixed size *) - SOME n => ((T, n), ds) - (* consume the head of 'ds', add 'minsize' *) - | NONE => ((T, minsize + hd ds), tl ds)) - xs diffs')) - | NONE => - NONE + (* merge with those types for which the size is fixed *) + SOME (fst (fold_map (fn (T, _) => fn ds => + case AList.lookup (op =) sizes (string_of_typ T) of + (* return the fixed size *) + SOME n => ((T, n), ds) + (* consume the head of 'ds', add 'minsize' *) + | NONE => ((T, minsize + hd ds), tl ds)) + xs diffs')) + | NONE => NONE end; (* ------------------------------------------------------------------------- *) @@ -1061,12 +1061,10 @@ (* formula that is true iff the interpretation denotes "true" *) (* ------------------------------------------------------------------------- *) - (* interpretation -> prop_formula *) +(* interpretation -> prop_formula *) - fun toTrue (Leaf [fm, _]) = - fm - | toTrue _ = - raise REFUTE ("toTrue", "interpretation does not denote a Boolean value"); +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 *) @@ -1074,12 +1072,10 @@ (* denotes "false" *) (* ------------------------------------------------------------------------- *) - (* interpretation -> prop_formula *) +(* interpretation -> prop_formula *) - fun toFalse (Leaf [_, fm]) = - fm - | toFalse _ = - raise REFUTE ("toFalse", "interpretation does not denote a Boolean value"); +fun toFalse (Leaf [_, fm]) = fm + | toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value"); (* ------------------------------------------------------------------------- *) (* find_model: repeatedly calls 'interpret' with appropriate parameters, *) @@ -1092,10 +1088,11 @@ (* negate : if true, find a model that makes 't' false (rather than true) *) (* ------------------------------------------------------------------------- *) - (* theory -> params -> Term.term -> bool -> unit *) +(* theory -> params -> Term.term -> bool -> unit *) - fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver, - no_assms, expect} assm_ts t negate = +fun find_model thy + {sizes, minsize, maxsize, maxvars, maxtime, satsolver, no_assms, expect} + assm_ts t negate = let (* string -> unit *) fun check_expect outcome_code = @@ -1103,141 +1100,142 @@ else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") (* unit -> unit *) fun wrapper () = - let - val timer = Timer.startRealTimer () - val t = if no_assms then t - else if negate then Logic.list_implies (assm_ts, t) - else Logic.mk_conjunction_list (t :: assm_ts) - val u = unfold_defs thy t - val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u) - val axioms = collect_axioms thy u - (* Term.typ list *) - val types = fold (union (op =) o ground_types thy) (u :: axioms) [] - val _ = tracing ("Ground types: " - ^ (if null types then "none." - else commas (map (Syntax.string_of_typ_global thy) types))) - (* we can only consider fragments of recursive IDTs, so we issue a *) - (* warning if the formula contains a recursive IDT *) - (* TODO: no warning needed for /positive/ occurrences of IDTs *) - val maybe_spurious = Library.exists (fn - Type (s, _) => - (case Datatype.get_info thy s of - SOME info => (* inductive datatype *) - let - val index = #index info - val descr = #descr info - val (_, _, constrs) = the (AList.lookup (op =) descr index) - in - (* recursive datatype? *) - Library.exists (fn (_, ds) => - Library.exists Datatype_Aux.is_rec_type ds) constrs - end - | NONE => false) - | _ => false) types - val _ = if maybe_spurious then - warning ("Term contains a recursive datatype; " - ^ "countermodel(s) may be spurious!") - else - () - (* (Term.typ * int) list -> string *) - fun find_model_loop universe = let - val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer) - val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime - orelse raise TimeLimit.TimeOut - val init_model = (universe, []) - val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1, - bounds = [], wellformed = True} - val _ = tracing ("Translating term (sizes: " - ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") - (* translate 'u' and all axioms *) - val (intrs, (model, args)) = fold_map (fn t' => fn (m, a) => + val timer = Timer.startRealTimer () + val t = + if no_assms then t + else if negate then Logic.list_implies (assm_ts, t) + else Logic.mk_conjunction_list (t :: assm_ts) + val u = unfold_defs thy t + val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u) + val axioms = collect_axioms thy u + (* Term.typ list *) + val types = fold (union (op =) o ground_types thy) (u :: axioms) [] + val _ = tracing ("Ground types: " + ^ (if null types then "none." + else commas (map (Syntax.string_of_typ_global thy) types))) + (* we can only consider fragments of recursive IDTs, so we issue a *) + (* warning if the formula contains a recursive IDT *) + (* TODO: no warning needed for /positive/ occurrences of IDTs *) + val maybe_spurious = Library.exists (fn + Type (s, _) => + (case Datatype.get_info thy s of + SOME info => (* inductive datatype *) + let + val index = #index info + val descr = #descr info + val (_, _, constrs) = the (AList.lookup (op =) descr index) + in + (* recursive datatype? *) + Library.exists (fn (_, ds) => + Library.exists Datatype_Aux.is_rec_type ds) constrs + end + | NONE => false) + | _ => false) types + val _ = + if maybe_spurious then + warning ("Term contains a recursive datatype; " + ^ "countermodel(s) may be spurious!") + else + () + (* (Term.typ * int) list -> string *) + fun find_model_loop universe = let - val (i, m', a') = interpret thy m a t' + val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer) + val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime + orelse raise TimeLimit.TimeOut + val init_model = (universe, []) + val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1, + bounds = [], wellformed = True} + val _ = tracing ("Translating term (sizes: " + ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") + (* translate 'u' and all axioms *) + val (intrs, (model, args)) = fold_map (fn t' => fn (m, a) => + let + val (i, m', a') = interpret thy m a t' + in + (* set 'def_eq' to 'true' *) + (i, (m', {maxvars = #maxvars a', def_eq = true, + next_idx = #next_idx a', bounds = #bounds a', + wellformed = #wellformed a'})) + end) (u :: axioms) (init_model, init_args) + (* make 'u' either true or false, and make all axioms true, and *) + (* add the well-formedness side condition *) + val fm_u = (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_u] + val _ = + (if satsolver = "dpll" orelse satsolver = "enumerate" then + warning ("Using SAT solver " ^ quote satsolver ^ + "; for better performance, consider installing an \ + \external solver.") + else ()); + val solver = + SatSolver.invoke_solver satsolver + handle Option.Option => + error ("Unknown SAT solver: " ^ quote satsolver ^ + ". Available solvers: " ^ + commas (map (quote o fst) (!SatSolver.solvers)) ^ ".") in - (* set 'def_eq' to 'true' *) - (i, (m', {maxvars = #maxvars a', def_eq = true, - next_idx = #next_idx a', bounds = #bounds a', - wellformed = #wellformed a'})) - end) (u :: axioms) (init_model, init_args) - (* make 'u' either true or false, and make all axioms true, and *) - (* add the well-formedness side condition *) - val fm_u = (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_u] - val _ = - (if satsolver = "dpll" orelse satsolver = "enumerate" then - warning ("Using SAT solver " ^ quote satsolver ^ - "; for better performance, consider installing an \ - \external solver.") - else - ()); - val solver = - SatSolver.invoke_solver satsolver - handle Option.Option => - error ("Unknown SAT solver: " ^ quote satsolver ^ - ". Available solvers: " ^ - commas (map (quote o fst) (!SatSolver.solvers)) ^ ".") - in - priority "Invoking SAT solver..."; - (case solver fm of - SatSolver.SATISFIABLE assignment => - (priority ("*** Model found: ***\n" ^ print_model thy model - (fn i => case assignment i of SOME b => b | NONE => true)); - if maybe_spurious then "potential" else "genuine") - | SatSolver.UNSATISFIABLE _ => - (priority "No model exists."; - case next_universe universe sizes minsize maxsize of - SOME universe' => find_model_loop universe' - | NONE => (priority - "Search terminated, no larger universe within the given limits."; - "none")) - | SatSolver.UNKNOWN => - (priority "No model found."; - case next_universe universe sizes minsize maxsize of - SOME universe' => find_model_loop universe' - | NONE => (priority - "Search terminated, no larger universe within the given limits."; - "unknown")) - ) handle SatSolver.NOT_CONFIGURED => - (error ("SAT solver " ^ quote satsolver ^ " is not configured."); - "unknown") - end handle MAXVARS_EXCEEDED => - (priority ("Search terminated, number of Boolean variables (" - ^ string_of_int maxvars ^ " allowed) exceeded."); - "unknown") + priority "Invoking SAT solver..."; + (case solver fm of + SatSolver.SATISFIABLE assignment => + (priority ("*** Model found: ***\n" ^ print_model thy model + (fn i => case assignment i of SOME b => b | NONE => true)); + if maybe_spurious then "potential" else "genuine") + | SatSolver.UNSATISFIABLE _ => + (priority "No model exists."; + case next_universe universe sizes minsize maxsize of + SOME universe' => find_model_loop universe' + | NONE => (priority + "Search terminated, no larger universe within the given limits."; + "none")) + | SatSolver.UNKNOWN => + (priority "No model found."; + case next_universe universe sizes minsize maxsize of + SOME universe' => find_model_loop universe' + | NONE => (priority + "Search terminated, no larger universe within the given limits."; + "unknown"))) handle SatSolver.NOT_CONFIGURED => + (error ("SAT solver " ^ quote satsolver ^ " is not configured."); + "unknown") + end + handle MAXVARS_EXCEEDED => + (priority ("Search terminated, number of Boolean variables (" + ^ string_of_int maxvars ^ " allowed) exceeded."); + "unknown") + val outcome_code = find_model_loop (first_universe types sizes minsize) in check_expect outcome_code end - in - (* some parameter sanity checks *) - minsize>=1 orelse - error ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1"); - maxsize>=1 orelse - error ("\"maxsize\" is " ^ string_of_int maxsize ^ ", must be at least 1"); - maxsize>=minsize orelse - error ("\"maxsize\" (=" ^ string_of_int maxsize ^ - ") is less than \"minsize\" (=" ^ string_of_int minsize ^ ")."); - maxvars>=0 orelse - error ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0"); - maxtime>=0 orelse - error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0"); - (* enter loop with or without time limit *) - priority ("Trying to find a model that " - ^ (if negate then "refutes" else "satisfies") ^ ": " - ^ Syntax.string_of_term_global thy t); - if maxtime>0 then ( - TimeLimit.timeLimit (Time.fromSeconds maxtime) - wrapper () - handle TimeLimit.TimeOut => - (priority ("Search terminated, time limit (" ^ - string_of_int maxtime - ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded."); - check_expect "unknown") - ) else + in + (* some parameter sanity checks *) + minsize>=1 orelse + error ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1"); + maxsize>=1 orelse + error ("\"maxsize\" is " ^ string_of_int maxsize ^ ", must be at least 1"); + maxsize>=minsize orelse + error ("\"maxsize\" (=" ^ string_of_int maxsize ^ + ") is less than \"minsize\" (=" ^ string_of_int minsize ^ ")."); + maxvars>=0 orelse + error ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0"); + maxtime>=0 orelse + error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0"); + (* enter loop with or without time limit *) + priority ("Trying to find a model that " + ^ (if negate then "refutes" else "satisfies") ^ ": " + ^ Syntax.string_of_term_global thy t); + if maxtime > 0 then ( + TimeLimit.timeLimit (Time.fromSeconds maxtime) wrapper () - end; + handle TimeLimit.TimeOut => + (priority ("Search terminated, time limit (" ^ + string_of_int maxtime + ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded."); + check_expect "unknown") + ) else wrapper () + end; (* ------------------------------------------------------------------------- *) @@ -1250,10 +1248,10 @@ (* parameters *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *) +(* theory -> (string * string) list -> Term.term list -> Term.term -> unit *) - fun satisfy_term thy params assm_ts t = - find_model thy (actual_params thy params) assm_ts t false; +fun satisfy_term thy params assm_ts t = + find_model thy (actual_params thy params) assm_ts t false; (* ------------------------------------------------------------------------- *) (* refute_term: calls 'find_model' to find a model that refutes 't' *) @@ -1261,9 +1259,9 @@ (* parameters *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *) +(* theory -> (string * string) list -> Term.term list -> Term.term -> unit *) - fun refute_term thy params assm_ts t = +fun refute_term thy params assm_ts t = let (* disallow schematic type variables, since we cannot properly negate *) (* terms containing them (their logical meaning is that there EXISTS a *) @@ -1293,23 +1291,22 @@ (* quantified variables. *) (* maps !!x1...xn. !xk...xm. t to t *) fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) = - strip_all_body t + strip_all_body t | strip_all_body (Const (@{const_name Trueprop}, _) $ t) = - strip_all_body t + strip_all_body t | strip_all_body (Const (@{const_name All}, _) $ Abs (_, _, t)) = - strip_all_body t + strip_all_body t | strip_all_body t = t (* maps !!x1...xn. !xk...xm. t to [x1, ..., xn, xk, ..., xm] *) fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) = - (a, T) :: strip_all_vars t + (a, T) :: strip_all_vars t | strip_all_vars (Const (@{const_name Trueprop}, _) $ t) = - strip_all_vars t + strip_all_vars t | strip_all_vars (Const (@{const_name All}, _) $ Abs (a, T, t)) = - (a, T) :: strip_all_vars t - | strip_all_vars t = - [] : (string * typ) list + (a, T) :: strip_all_vars t + | strip_all_vars t = [] : (string * typ) list val strip_t = strip_all_body ex_closure - val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure) + val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure) val subst_t = Term.subst_bounds (map Free frees, strip_t) in find_model thy (actual_params thy params) assm_ts subst_t true @@ -1319,7 +1316,7 @@ (* refute_goal *) (* ------------------------------------------------------------------------- *) - fun refute_goal ctxt params th i = +fun refute_goal ctxt params th i = let val t = th |> prop_of in @@ -1346,39 +1343,38 @@ (* variables) *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> Term.typ -> interpretation list *) +(* theory -> model -> Term.typ -> interpretation list *) - fun make_constants thy model T = +fun make_constants thy model T = let (* 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 *) - fun unit_vectors_loop k = - if k>n then [] else unit_vector (k,n) :: unit_vectors_loop (k+1) - in - unit_vectors_loop 1 - end + 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 *) + fun unit_vectors_loop k = + if k>n then [] else unit_vector (k,n) :: unit_vectors_loop (k+1) + in + unit_vectors_loop 1 + end (* 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 single xs + fun pick_all 1 xs = map single xs | pick_all n xs = - let val rec_pick = pick_all (n-1) xs in - maps (fn x => map (cons x) rec_pick) xs - end + let val rec_pick = pick_all (n - 1) xs in + maps (fn x => map (cons x) rec_pick) xs + end (* returns all constant interpretations that have the same tree *) (* structure as the interpretation argument *) (* interpretation -> interpretation list *) fun make_constants_intr (Leaf xs) = unit_vectors (length xs) | make_constants_intr (Node xs) = map Node (pick_all (length xs) - (make_constants_intr (hd xs))) + (make_constants_intr (hd xs))) (* obtain the interpretation for a variable of type 'T' *) val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) @@ -1390,11 +1386,12 @@ (* power: 'power (a, b)' computes a^b, for a>=0, b>=0 *) (* ------------------------------------------------------------------------- *) - (* int * int -> int *) +(* int * int -> int *) - fun power (a, 0) = 1 - | power (a, 1) = a - | power (a, b) = let val ab = power(a, b div 2) in +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; @@ -1403,17 +1400,17 @@ (* (make_constants T)', but implemented more efficiently) *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> Term.typ -> int *) +(* theory -> model -> Term.typ -> int *) - (* returns 0 for an empty ground type or a function type with empty *) - (* codomain, but fails for a function type with empty domain -- *) - (* admissibility of datatype constructor argument types (see "Inductive *) - (* datatypes in HOL - lessons learned ...", S. Berghofer, M. Wenzel, *) - (* TPHOLs 99) ensures that recursive, possibly empty, datatype fragments *) - (* never occur as the domain of a function type that is the type of a *) - (* constructor argument *) +(* returns 0 for an empty ground type or a function type with empty *) +(* codomain, but fails for a function type with empty domain -- *) +(* admissibility of datatype constructor argument types (see "Inductive *) +(* datatypes in HOL - lessons learned ...", S. Berghofer, M. Wenzel, *) +(* TPHOLs 99) ensures that recursive, possibly empty, datatype fragments *) +(* never occur as the domain of a function type that is the type of a *) +(* constructor argument *) - fun size_of_type thy model T = +fun size_of_type thy model T = let (* returns the number of elements that have the same tree structure as a *) (* given interpretation *) @@ -1430,11 +1427,11 @@ (* TT/FF: interpretations that denote "true" or "false", respectively *) (* ------------------------------------------------------------------------- *) - (* interpretation *) +(* interpretation *) - val TT = Leaf [True, False]; +val TT = Leaf [True, False]; - val FF = Leaf [False, True]; +val FF = Leaf [False, True]; (* ------------------------------------------------------------------------- *) (* make_equality: returns an interpretation that denotes (extensional) *) @@ -1447,46 +1444,46 @@ (* 'not_equal' to another interpretation *) (* ------------------------------------------------------------------------- *) - (* 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. *) +(* 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 *) +(* interpretation * interpretation -> interpretation *) - fun make_equality (i1, i2) = +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) (* defined and equal *) - | Node _ => raise REFUTE ("make_equality", - "second interpretation is higher")) + (case i2 of + Leaf ys => PropLogic.dot_product (xs, ys) (* defined and 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.all (map equal (xs ~~ ys)))) + (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 - (* defined and not equal *) - Leaf ys => PropLogic.all ((PropLogic.exists xs) - :: (PropLogic.exists ys) - :: (map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys))) - | Node _ => raise REFUTE ("make_equality", - "second interpretation is higher")) + (case i2 of + (* defined and not equal *) + Leaf ys => PropLogic.all ((PropLogic.exists xs) + :: (PropLogic.exists ys) + :: (map (fn (x,y) => SOr (SNot x, SNot y)) (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.exists (map not_equal (xs ~~ ys)))) + (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' *) @@ -1502,25 +1499,25 @@ (* to an undefined interpretation. *) (* ------------------------------------------------------------------------- *) - (* interpretation * interpretation -> interpretation *) +(* interpretation * interpretation -> interpretation *) - fun make_def_equality (i1, i2) = +fun make_def_equality (i1, i2) = let (* interpretation * interpretation -> prop_formula *) fun equal (i1, i2) = (case i1 of Leaf xs => - (case i2 of - (* defined and equal, or both undefined *) - Leaf ys => SOr (PropLogic.dot_product (xs, ys), - SAnd (PropLogic.all (map SNot xs), PropLogic.all (map SNot ys))) - | Node _ => raise REFUTE ("make_def_equality", - "second interpretation is higher")) + (case i2 of + (* defined and equal, or both undefined *) + Leaf ys => SOr (PropLogic.dot_product (xs, ys), + SAnd (PropLogic.all (map SNot xs), PropLogic.all (map SNot ys))) + | Node _ => raise REFUTE ("make_def_equality", + "second interpretation is higher")) | Node xs => - (case i2 of - Leaf _ => raise REFUTE ("make_def_equality", - "first interpretation is higher") - | Node ys => PropLogic.all (map equal (xs ~~ ys)))) + (case i2 of + Leaf _ => raise REFUTE ("make_def_equality", + "first interpretation is higher") + | Node ys => PropLogic.all (map equal (xs ~~ ys)))) (* interpretation *) val eq = equal (i1, i2) in @@ -1533,9 +1530,9 @@ (* argument denoted by 'i2' *) (* ------------------------------------------------------------------------- *) - (* interpretation * interpretation -> interpretation *) +(* interpretation * interpretation -> interpretation *) - fun interpretation_apply (i1, i2) = +fun interpretation_apply (i1, i2) = let (* interpretation * interpretation -> interpretation *) fun interpretation_disjunction (tr1,tr2) = @@ -1546,50 +1543,46 @@ 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_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)) + 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 ("interpretation_apply", "empty list (in dot product)") + raise REFUTE ("interpretation_apply", "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 (cons x) xss + fun cons_list x xss = map (cons x) 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 single xs + fun pick_all [xs] = map single xs | pick_all (xs::xss) = - let val rec_pick = pick_all xss in - maps (fn x => map (cons x) rec_pick) xs - end - | pick_all _ = - raise REFUTE ("interpretation_apply", "empty list (in pick_all)") + let val rec_pick = pick_all xss in + maps (fn x => map (cons x) rec_pick) xs + end + | pick_all _ = raise REFUTE ("interpretation_apply", "empty list (in pick_all)") (* interpretation -> prop_formula list *) - fun interpretation_to_prop_formula_list (Leaf xs) = - xs + 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)) + map PropLogic.all (pick_all + (map interpretation_to_prop_formula_list trees)) in case i1 of Leaf _ => - raise REFUTE ("interpretation_apply", "first interpretation is a leaf") + raise REFUTE ("interpretation_apply", "first interpretation is a leaf") | Node xs => - prop_formula_list_dot_product_interpretation_list - (interpretation_to_prop_formula_list i2, xs) + prop_formula_list_dot_product_interpretation_list + (interpretation_to_prop_formula_list i2, xs) end; (* ------------------------------------------------------------------------- *) (* eta_expand: eta-expands a term 't' by adding 'i' lambda abstractions *) (* ------------------------------------------------------------------------- *) - (* Term.term -> int -> Term.term *) +(* Term.term -> int -> Term.term *) - fun eta_expand t i = +fun eta_expand t i = let val Ts = Term.binder_types (Term.fastype_of t) val t' = Term.incr_boundvars i t @@ -1605,167 +1598,163 @@ (* their arguments) of the size of the argument types *) (* ------------------------------------------------------------------------- *) - fun size_of_dtyp thy typ_sizes descr typ_assoc constructors = - Integer.sum (map (fn (_, dtyps) => - Integer.prod (map (size_of_type thy (typ_sizes, []) o - (typ_of_dtyp descr typ_assoc)) dtyps)) - constructors); +fun size_of_dtyp thy typ_sizes descr typ_assoc constructors = + Integer.sum (map (fn (_, dtyps) => + Integer.prod (map (size_of_type thy (typ_sizes, []) o + (typ_of_dtyp descr typ_assoc)) dtyps)) + constructors); (* ------------------------------------------------------------------------- *) (* INTERPRETERS: Actual Interpreters *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* 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 *) +(* simply typed lambda calculus: Isabelle's basic term syntax, with type *) +(* variables, function types, and propT *) - fun stlc_interpreter thy model args t = +fun stlc_interpreter thy model args t = let - val (typs, terms) = model + val (typs, terms) = model val {maxvars, def_eq, 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 - (* the model must specify a size for ground types *) - val size = if T = Term.propT then 2 - else the (AList.lookup (op =) typs T) - val next = next_idx+size - (* check if 'maxvars' is large enough *) - val _ = (if next-1>maxvars andalso maxvars>0 then - raise MAXVARS_EXCEEDED else ()) - (* prop_formula list *) - val fms = 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 *) - val wf = one_of_two_false fms + (* unit -> (interpretation * model * arguments) option *) + fun interpret_groundtype () = + let + (* the model must specify a size for ground types *) + val size = + if T = Term.propT then 2 + else the (AList.lookup (op =) typs T) + val next = next_idx + size + (* check if 'maxvars' is large enough *) + val _ = (if next - 1 > maxvars andalso maxvars > 0 then + raise MAXVARS_EXCEEDED else ()) + (* prop_formula list *) + val fms = 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 *) + val wf = one_of_two_false fms + in + (* extend the model, increase 'next_idx', add well-formedness *) + (* condition *) + SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, + def_eq = def_eq, next_idx = next, bounds = bounds, + wellformed = SAnd (wellformed, wf)}) + end in - (* extend the model, increase 'next_idx', add well-formedness *) - (* condition *) - SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, - def_eq = def_eq, next_idx = next, bounds = bounds, - wellformed = SAnd (wellformed, wf)}) + case T of + Type ("fun", [T1, T2]) => + let + (* we create 'size_of_type ... T1' different copies of the *) + (* interpretation for 'T2', which are then combined into a single *) + (* new interpretation *) + (* 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, def_eq = false, next_idx = idx, + bounds = [], wellformed = True} (Free ("dummy", T2)) + 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 thy model T1) + (* 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, + def_eq = def_eq, next_idx = next, bounds = bounds, + wellformed = SAnd (wellformed, wf)}) + end + | Type _ => interpret_groundtype () + | TFree _ => interpret_groundtype () + | TVar _ => interpret_groundtype () end - in - case T of - Type ("fun", [T1, T2]) => - let - (* we create 'size_of_type ... T1' different copies of the *) - (* interpretation for 'T2', which are then combined into a single *) - (* new interpretation *) - (* 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, def_eq = false, next_idx = idx, - bounds = [], wellformed = True} (Free ("dummy", T2)) - 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 thy model T1) - (* 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, - def_eq = def_eq, next_idx = next, bounds = bounds, - wellformed = SAnd (wellformed, wf)}) - end - | Type _ => interpret_groundtype () - | TFree _ => interpret_groundtype () - | TVar _ => interpret_groundtype () - end in case AList.lookup (op =) terms t of SOME intr => - (* return an existing interpretation *) - SOME (intr, model, args) + (* 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 (List.nth (#bounds args, i), model, args) - | Abs (x, T, body) => - let - (* create all constants of type 'T' *) - val constants = make_constants thy model T - (* interpret the 'body' separately for each constant *) - val (bodies, (model', args')) = fold_map - (fn c => fn (m, a) => - let - (* add 'c' to 'bounds' *) - val (i', m', a') = interpret thy m {maxvars = #maxvars a, - def_eq = #def_eq 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' *) - (i', (m', {maxvars = maxvars, def_eq = def_eq, - next_idx = #next_idx a', bounds = bounds, - wellformed = #wellformed a'})) - end) - constants (model, args) - in - SOME (Node bodies, model', args') - end - | t1 $ t2 => - let - (* 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) + (case t of + Const (_, T) => interpret_groundterm T + | Free (_, T) => interpret_groundterm T + | Var (_, T) => interpret_groundterm T + | Bound i => SOME (List.nth (#bounds args, i), model, args) + | Abs (x, T, body) => + let + (* create all constants of type 'T' *) + val constants = make_constants thy model T + (* interpret the 'body' separately for each constant *) + val (bodies, (model', args')) = fold_map + (fn c => fn (m, a) => + let + (* add 'c' to 'bounds' *) + val (i', m', a') = interpret thy m {maxvars = #maxvars a, + def_eq = #def_eq 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' *) + (i', (m', {maxvars = maxvars, def_eq = def_eq, + next_idx = #next_idx a', bounds = bounds, + wellformed = #wellformed a'})) + end) + constants (model, args) + in + SOME (Node bodies, model', args') + end + | t1 $ t2 => + let + (* 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 *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - fun Pure_interpreter thy model args t = - case t of - Const (@{const_name all}, _) $ t1 => +fun Pure_interpreter thy model args t = + case t of + Const (@{const_name all}, _) $ t1 => let val (i, m, a) = interpret thy model args t1 in case i of Node xs => - (* 3-valued logic *) - let - val fmTrue = PropLogic.all (map toTrue xs) - val fmFalse = PropLogic.exists (map toFalse xs) - in - SOME (Leaf [fmTrue, fmFalse], m, a) - end + (* 3-valued logic *) + 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 followed by a non-function") end - | Const (@{const_name all}, _) => + | Const (@{const_name all}, _) => SOME (interpret thy model args (eta_expand t 1)) - | Const (@{const_name "=="}, _) $ t1 $ t2 => + | Const (@{const_name "=="}, _) $ t1 $ t2 => let val (i1, m1, a1) = interpret thy model args t1 val (i2, m2, a2) = interpret thy m1 a1 t2 @@ -1774,11 +1763,11 @@ SOME ((if #def_eq args then make_def_equality else make_equality) (i1, i2), m2, a2) end - | Const (@{const_name "=="}, _) $ t1 => + | Const (@{const_name "=="}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const (@{const_name "=="}, _) => + | Const (@{const_name "=="}, _) => SOME (interpret thy model args (eta_expand t 2)) - | Const (@{const_name "==>"}, _) $ t1 $ t2 => + | Const (@{const_name "==>"}, _) $ t1 $ t2 => (* 3-valued logic *) let val (i1, m1, a1) = interpret thy model args t1 @@ -1788,80 +1777,80 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const (@{const_name "==>"}, _) $ t1 => + | Const (@{const_name "==>"}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const (@{const_name "==>"}, _) => + | Const (@{const_name "==>"}, _) => SOME (interpret thy model args (eta_expand t 2)) - | _ => NONE; + | _ => NONE; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* 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. In HOL however, logical constants can themselves be *) - (* arguments. They are then translated using eta-expansion. *) - case t of - Const (@{const_name Trueprop}, _) => +fun HOLogic_interpreter thy model args t = +(* Providing interpretations directly is more efficient than unfolding the *) +(* logical constants. In HOL however, logical constants can themselves be *) +(* arguments. They are then translated using eta-expansion. *) + case t of + Const (@{const_name Trueprop}, _) => SOME (Node [TT, FF], model, args) - | Const (@{const_name Not}, _) => + | Const (@{const_name Not}, _) => SOME (Node [FF, TT], model, args) - (* redundant, since 'True' is also an IDT constructor *) - | Const (@{const_name True}, _) => + (* redundant, since 'True' is also an IDT constructor *) + | Const (@{const_name True}, _) => SOME (TT, model, args) - (* redundant, since 'False' is also an IDT constructor *) - | Const (@{const_name False}, _) => + (* redundant, since 'False' is also an IDT constructor *) + | Const (@{const_name False}, _) => SOME (FF, model, args) - | Const (@{const_name All}, _) $ t1 => (* similar to "all" (Pure) *) + | Const (@{const_name All}, _) $ t1 => (* similar to "all" (Pure) *) let val (i, m, a) = interpret thy model args t1 in case i of Node xs => - (* 3-valued logic *) - let - val fmTrue = PropLogic.all (map toTrue xs) - val fmFalse = PropLogic.exists (map toFalse xs) - in - SOME (Leaf [fmTrue, fmFalse], m, a) - end + (* 3-valued logic *) + 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 followed by a non-function") end - | Const (@{const_name All}, _) => + | Const (@{const_name All}, _) => SOME (interpret thy model args (eta_expand t 1)) - | Const (@{const_name Ex}, _) $ t1 => + | Const (@{const_name Ex}, _) $ t1 => let val (i, m, a) = interpret thy model args t1 in case i of Node xs => - (* 3-valued logic *) - let - val fmTrue = PropLogic.exists (map toTrue xs) - val fmFalse = PropLogic.all (map toFalse xs) - in - SOME (Leaf [fmTrue, fmFalse], m, a) - end + (* 3-valued logic *) + 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 followed by a non-function") end - | Const (@{const_name Ex}, _) => + | Const (@{const_name Ex}, _) => SOME (interpret thy model args (eta_expand t 1)) - | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to "==" (Pure) *) + | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to "==" (Pure) *) 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 (@{const_name HOL.eq}, _) $ t1 => + | Const (@{const_name HOL.eq}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const (@{const_name HOL.eq}, _) => + | Const (@{const_name HOL.eq}, _) => SOME (interpret thy model args (eta_expand t 2)) - | Const (@{const_name HOL.conj}, _) $ t1 $ t2 => + | Const (@{const_name HOL.conj}, _) $ t1 $ t2 => (* 3-valued logic *) let val (i1, m1, a1) = interpret thy model args t1 @@ -1871,14 +1860,14 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const (@{const_name HOL.conj}, _) $ t1 => + | Const (@{const_name HOL.conj}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const (@{const_name HOL.conj}, _) => + | Const (@{const_name HOL.conj}, _) => SOME (interpret thy model args (eta_expand t 2)) (* this would make "undef" propagate, even for formulae like *) (* "False & undef": *) (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *) - | Const (@{const_name HOL.disj}, _) $ t1 $ t2 => + | Const (@{const_name HOL.disj}, _) $ t1 $ t2 => (* 3-valued logic *) let val (i1, m1, a1) = interpret thy model args t1 @@ -1888,14 +1877,14 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const (@{const_name HOL.disj}, _) $ t1 => + | Const (@{const_name HOL.disj}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const (@{const_name HOL.disj}, _) => + | Const (@{const_name HOL.disj}, _) => SOME (interpret thy model args (eta_expand t 2)) (* this would make "undef" propagate, even for formulae like *) (* "True | undef": *) (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *) - | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *) + | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *) (* 3-valued logic *) let val (i1, m1, a1) = interpret thy model args t1 @@ -1905,117 +1894,119 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const (@{const_name HOL.implies}, _) $ t1 => + | Const (@{const_name HOL.implies}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const (@{const_name HOL.implies}, _) => + | Const (@{const_name HOL.implies}, _) => SOME (interpret thy model args (eta_expand t 2)) (* this would make "undef" propagate, even for formulae like *) (* "False --> undef": *) (* SOME (Node [Node [TT, FF], Node [TT, TT]], model, args) *) - | _ => NONE; + | _ => NONE; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* interprets variables and constants whose type is an IDT (this is *) - (* relatively easy and merely requires us to compute the size of the IDT); *) - (* constructors of IDTs however are properly interpreted by *) - (* 'IDT_constructor_interpreter' *) +(* interprets variables and constants whose type is an IDT (this is *) +(* relatively easy and merely requires us to compute the size of the IDT); *) +(* constructors of IDTs however are properly interpreted by *) +(* 'IDT_constructor_interpreter' *) - fun IDT_interpreter thy model args t = +fun IDT_interpreter thy model args t = let val (typs, terms) = model (* Term.typ -> (interpretation * model * arguments) option *) fun interpret_term (Type (s, Ts)) = - (case Datatype.get_info thy s of - SOME info => (* inductive datatype *) - let - (* int option -- only recursive IDTs have an associated depth *) - val depth = AList.lookup (op =) typs (Type (s, Ts)) - (* sanity check: depth must be at least 0 *) - val _ = (case depth of SOME n => - if n<0 then - raise REFUTE ("IDT_interpreter", "negative depth") - else () - | _ => ()) - in - (* termination condition to avoid infinite recursion *) - if depth = (SOME 0) then - (* return a leaf of size 0 *) - SOME (Leaf [], model, args) - else - let - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = the (AList.lookup (op =) 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 Datatype_Aux.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("IDT_interpreter", - "datatype argument (for type " - ^ Syntax.string_of_typ_global 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 => - AList.update (op =) (Type (s, Ts), n-1) typs - (* recursively compute the size of the datatype *) - val size = size_of_dtyp thy typs' descr typ_assoc constrs - val next_idx = #next_idx args - val next = next_idx+size - (* check if 'maxvars' is large enough *) - val _ = (if next-1 > #maxvars args andalso - #maxvars args > 0 then raise MAXVARS_EXCEEDED else ()) - (* prop_formula list *) - val fms = 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 *) - val wf = one_of_two_false fms - in - (* extend the model, increase 'next_idx', add well-formedness *) - (* condition *) - SOME (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, - def_eq = #def_eq args, next_idx = next, bounds = #bounds args, - wellformed = SAnd (#wellformed args, wf)}) - end - end - | NONE => (* not an inductive datatype *) - NONE) + (case Datatype.get_info thy s of + SOME info => (* inductive datatype *) + let + (* int option -- only recursive IDTs have an associated depth *) + val depth = AList.lookup (op =) typs (Type (s, Ts)) + (* sanity check: depth must be at least 0 *) + val _ = + (case depth of SOME n => + if n < 0 then + raise REFUTE ("IDT_interpreter", "negative depth") + else () + | _ => ()) + in + (* termination condition to avoid infinite recursion *) + if depth = (SOME 0) then + (* return a leaf of size 0 *) + SOME (Leaf [], model, args) + else + let + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = the (AList.lookup (op =) 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 Datatype_Aux.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_interpreter", + "datatype argument (for type " + ^ Syntax.string_of_typ_global 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 => + AList.update (op =) (Type (s, Ts), n-1) typs + (* recursively compute the size of the datatype *) + val size = size_of_dtyp thy typs' descr typ_assoc constrs + val next_idx = #next_idx args + val next = next_idx+size + (* check if 'maxvars' is large enough *) + val _ = (if next-1 > #maxvars args andalso + #maxvars args > 0 then raise MAXVARS_EXCEEDED else ()) + (* prop_formula list *) + val fms = 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 *) + val wf = one_of_two_false fms + in + (* extend the model, increase 'next_idx', add well-formedness *) + (* condition *) + SOME (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, + def_eq = #def_eq args, next_idx = next, bounds = #bounds args, + wellformed = SAnd (#wellformed args, wf)}) + end + end + | NONE => (* not an inductive datatype *) + NONE) | interpret_term _ = (* a (free or schematic) type variable *) - NONE + NONE in case AList.lookup (op =) terms t of SOME intr => - (* return an existing interpretation *) - SOME (intr, model, args) + (* return an existing interpretation *) + SOME (intr, model, args) | NONE => - (case t of - Free (_, T) => interpret_term T - | Var (_, T) => interpret_term T - | Const (_, T) => interpret_term T - | _ => NONE) + (case t of + Free (_, T) => interpret_term T + | Var (_, T) => interpret_term T + | Const (_, T) => interpret_term T + | _ => NONE) end; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* This function imposes an order on the elements of a datatype fragment *) - (* as follows: C_i x_1 ... x_n < C_j y_1 ... y_m iff i < j or *) - (* (x_1, ..., x_n) < (y_1, ..., y_m). With this order, a constructor is *) - (* a function C_i that maps some argument indices x_1, ..., x_n to the *) - (* datatype element given by index C_i x_1 ... x_n. The idea remains the *) - (* same for recursive datatypes, although the computation of indices gets *) - (* a little tricky. *) +(* This function imposes an order on the elements of a datatype fragment *) +(* as follows: C_i x_1 ... x_n < C_j y_1 ... y_m iff i < j or *) +(* (x_1, ..., x_n) < (y_1, ..., y_m). With this order, a constructor is *) +(* a function C_i that maps some argument indices x_1, ..., x_n to the *) +(* datatype element given by index C_i x_1 ... x_n. The idea remains the *) +(* same for recursive datatypes, although the computation of indices gets *) +(* a little tricky. *) - fun IDT_constructor_interpreter thy model args t = +fun IDT_constructor_interpreter thy model args t = let (* returns a list of canonical representations for terms of the type 'T' *) (* It would be nice if we could just use 'print' for this, but 'print' *) @@ -2023,638 +2014,637 @@ (* lead to infinite recursion when we have (mutually) recursive IDTs. *) (* (Term.typ * int) list -> Term.typ -> Term.term list *) fun canonical_terms typs T = - (case T of - Type ("fun", [T1, T2]) => - (* 'T2' might contain a recursive IDT, so we cannot use 'print' (at *) - (* least not for 'T2' *) - let - (* 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 single xs - | pick_all n xs = - let val rec_pick = pick_all (n-1) xs in - maps (fn x => map (cons x) rec_pick) xs + (case T of + Type ("fun", [T1, T2]) => + (* 'T2' might contain a recursive IDT, so we cannot use 'print' (at *) + (* least not for 'T2' *) + let + (* 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 single xs + | pick_all n xs = + let val rec_pick = pick_all (n-1) xs in + maps (fn x => map (cons x) rec_pick) xs + end + (* ["x1", ..., "xn"] *) + val terms1 = canonical_terms typs T1 + (* ["y1", ..., "ym"] *) + val terms2 = canonical_terms typs T2 + (* [[("x1", "y1"), ..., ("xn", "y1")], ..., *) + (* [("x1", "ym"), ..., ("xn", "ym")]] *) + val functions = map (curry (op ~~) terms1) + (pick_all (length terms1) terms2) + (* [["(x1, y1)", ..., "(xn, y1)"], ..., *) + (* ["(x1, ym)", ..., "(xn, ym)"]] *) + val pairss = map (map HOLogic.mk_prod) functions + (* 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 (@{const_abbrev Set.empty}, HOLogic_setT) + val HOLogic_insert = + Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) + in + (* functions as graphs, i.e. as a (HOL) set of pairs "(x, y)" *) + map (fn ps => fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) ps + HOLogic_empty_set) pairss end - (* ["x1", ..., "xn"] *) - val terms1 = canonical_terms typs T1 - (* ["y1", ..., "ym"] *) - val terms2 = canonical_terms typs T2 - (* [[("x1", "y1"), ..., ("xn", "y1")], ..., *) - (* [("x1", "ym"), ..., ("xn", "ym")]] *) - val functions = map (curry (op ~~) terms1) - (pick_all (length terms1) terms2) - (* [["(x1, y1)", ..., "(xn, y1)"], ..., *) - (* ["(x1, ym)", ..., "(xn, ym)"]] *) - val pairss = map (map HOLogic.mk_prod) functions - (* 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 (@{const_abbrev Set.empty}, HOLogic_setT) - val HOLogic_insert = - Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) - in - (* functions as graphs, i.e. as a (HOL) set of pairs "(x, y)" *) - map (fn ps => fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) ps - HOLogic_empty_set) pairss - end | Type (s, Ts) => - (case Datatype.get_info thy s of - SOME info => - (case AList.lookup (op =) typs T of - SOME 0 => - (* termination condition to avoid infinite recursion *) - [] (* at depth 0, every IDT is empty *) - | _ => - let - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = the (AList.lookup (op =) 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 Datatype_Aux.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("IDT_constructor_interpreter", - "datatype argument (for type " - ^ Syntax.string_of_typ_global thy T - ^ ") is not a variable") - else () - (* decrement depth for the IDT 'T' *) - val typs' = (case AList.lookup (op =) typs T of NONE => typs - | SOME n => AList.update (op =) (T, n-1) typs) - fun constructor_terms terms [] = terms - | constructor_terms terms (d::ds) = + (case Datatype.get_info thy s of + SOME info => + (case AList.lookup (op =) typs T of + SOME 0 => + (* termination condition to avoid infinite recursion *) + [] (* at depth 0, every IDT is empty *) + | _ => let - val dT = typ_of_dtyp descr typ_assoc d - val d_terms = canonical_terms typs' dT + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = the (AList.lookup (op =) 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 Datatype_Aux.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_constructor_interpreter", + "datatype argument (for type " + ^ Syntax.string_of_typ_global thy T + ^ ") is not a variable") + else () + (* decrement depth for the IDT 'T' *) + val typs' = + (case AList.lookup (op =) typs T of NONE => typs + | SOME n => AList.update (op =) (T, n-1) typs) + fun constructor_terms terms [] = terms + | constructor_terms terms (d::ds) = + let + val dT = typ_of_dtyp descr typ_assoc d + val d_terms = canonical_terms typs' dT + in + (* C_i x_1 ... x_n < C_i y_1 ... y_n if *) + (* (x_1, ..., x_n) < (y_1, ..., y_n) *) + constructor_terms + (map_product (curry op $) terms d_terms) ds + end in - (* C_i x_1 ... x_n < C_i y_1 ... y_n if *) - (* (x_1, ..., x_n) < (y_1, ..., y_n) *) - constructor_terms - (map_product (curry op $) terms d_terms) ds - end - in - (* C_i ... < C_j ... if i < j *) - maps (fn (cname, ctyps) => - let - val cTerm = Const (cname, - map (typ_of_dtyp descr typ_assoc) ctyps ---> T) - in - constructor_terms [cTerm] ctyps - end) constrs - end) - | NONE => - (* not an inductive datatype; in this case the argument types in *) - (* 'Ts' may not be IDTs either, so 'print' should be safe *) + (* C_i ... < C_j ... if i < j *) + maps (fn (cname, ctyps) => + let + val cTerm = Const (cname, + map (typ_of_dtyp descr typ_assoc) ctyps ---> T) + in + constructor_terms [cTerm] ctyps + end) constrs + end) + | NONE => + (* not an inductive datatype; in this case the argument types in *) + (* 'Ts' may not be IDTs either, so 'print' should be safe *) + map (fn intr => print thy (typs, []) T intr (K false)) + (make_constants thy (typs, []) T)) + | _ => (* TFree ..., TVar ... *) map (fn intr => print thy (typs, []) T intr (K false)) (make_constants thy (typs, []) T)) - | _ => (* TFree ..., TVar ... *) - map (fn intr => print thy (typs, []) T intr (K false)) - (make_constants thy (typs, []) T)) val (typs, terms) = model in case AList.lookup (op =) terms t of SOME intr => - (* return an existing interpretation *) - SOME (intr, model, args) + (* return an existing interpretation *) + SOME (intr, model, args) | NONE => - (case t of - Const (s, T) => - (case body_type T of - Type (s', Ts') => - (case Datatype.get_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 (AList.lookup (op =) 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 Datatype_Aux.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("IDT_constructor_interpreter", - "datatype argument (for type " - ^ Syntax.string_of_typ_global 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 Sign.typ_instance 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 - | (_, ctypes)::cs => - let - (* int option -- only /recursive/ IDTs have an associated *) - (* depth *) - val depth = AList.lookup (op =) typs (Type (s', Ts')) - (* this should never happen: at depth 0, this IDT fragment *) - (* is definitely empty, and in this case we don't need to *) - (* interpret its constructors *) - val _ = (case depth of SOME 0 => - raise REFUTE ("IDT_constructor_interpreter", - "depth is 0") - | _ => ()) - val typs' = (case depth of NONE => typs | SOME n => - AList.update (op =) (Type (s', Ts'), n-1) typs) - (* elements of the datatype come before elements generated *) - (* by 'Const (s, T)' iff they are generated by a *) - (* constructor in constrs1 *) - val offset = size_of_dtyp thy typs' descr typ_assoc constrs1 - (* compute the total (current) size of the datatype *) - val total = offset + - size_of_dtyp thy typs' descr typ_assoc constrs2 - (* sanity check *) - val _ = if total <> size_of_type thy (typs, []) - (Type (s', Ts')) then - raise REFUTE ("IDT_constructor_interpreter", - "total is not equal to current size") - else () - (* returns an interpretation where everything is mapped to *) - (* an "undefined" element of the datatype *) - fun make_undef [] = - Leaf (replicate total False) - | make_undef (d::ds) = + (case t of + Const (s, T) => + (case body_type T of + Type (s', Ts') => + (case Datatype.get_info thy s' of + SOME info => (* body type is an inductive datatype *) let - (* compute the current size of the type 'd' *) - val dT = typ_of_dtyp descr typ_assoc d - val size = size_of_type thy (typs, []) dT - in - Node (replicate size (make_undef ds)) - end - (* returns the interpretation for a constructor *) - fun make_constr [] offset = - if offset < total then - (Leaf (replicate offset False @ True :: - (replicate (total - offset - 1) False)), offset + 1) - else - raise REFUTE ("IDT_constructor_interpreter", - "offset >= total") - | make_constr (d::ds) offset = - let - (* Term.typ *) - val dT = typ_of_dtyp descr typ_assoc d - (* compute canonical term representations for all *) - (* elements of the type 'd' (with the reduced depth *) - (* for the IDT) *) - val terms' = canonical_terms typs' dT - (* sanity check *) - val _ = - if length terms' <> size_of_type thy (typs', []) dT + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = the (AList.lookup (op =) 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 Datatype_Aux.DtTFree _ => false | _ => true) dtyps then raise REFUTE ("IDT_constructor_interpreter", - "length of terms' is not equal to old size") - else () - (* compute canonical term representations for all *) - (* elements of the type 'd' (with the current depth *) - (* for the IDT) *) - val terms = canonical_terms typs dT - (* sanity check *) - val _ = - if length terms <> size_of_type thy (typs, []) dT - then - raise REFUTE ("IDT_constructor_interpreter", - "length of terms is not equal to current size") - else () - (* sanity check *) - val _ = - if length terms < length terms' then - raise REFUTE ("IDT_constructor_interpreter", - "current size is less than old size") + "datatype argument (for type " + ^ Syntax.string_of_typ_global thy (Type (s', Ts')) + ^ ") is not a variable") else () - (* sanity check: every element of terms' must also be *) - (* present in terms *) - val _ = - if forall (member (op =) terms) terms' then () - else - raise REFUTE ("IDT_constructor_interpreter", - "element has disappeared") - (* sanity check: the order on elements of terms' is *) - (* the same in terms, for those elements *) - val _ = - let - fun search (x::xs) (y::ys) = - if x = y then search xs ys else search (x::xs) ys - | search (x::xs) [] = + (* split the constructors into those occuring before/after *) + (* 'Const (s, T)' *) + val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) => + not (cname = s andalso Sign.typ_instance 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 + | (_, ctypes)::cs => + let + (* int option -- only /recursive/ IDTs have an associated *) + (* depth *) + val depth = AList.lookup (op =) typs (Type (s', Ts')) + (* this should never happen: at depth 0, this IDT fragment *) + (* is definitely empty, and in this case we don't need to *) + (* interpret its constructors *) + val _ = (case depth of SOME 0 => + raise REFUTE ("IDT_constructor_interpreter", + "depth is 0") + | _ => ()) + val typs' = (case depth of NONE => typs | SOME n => + AList.update (op =) (Type (s', Ts'), n-1) typs) + (* elements of the datatype come before elements generated *) + (* by 'Const (s, T)' iff they are generated by a *) + (* constructor in constrs1 *) + val offset = size_of_dtyp thy typs' descr typ_assoc constrs1 + (* compute the total (current) size of the datatype *) + val total = offset + + size_of_dtyp thy typs' descr typ_assoc constrs2 + (* sanity check *) + val _ = if total <> size_of_type thy (typs, []) + (Type (s', Ts')) then raise REFUTE ("IDT_constructor_interpreter", - "element order not preserved") - | search [] _ = () - in search terms' terms end - (* int * interpretation list *) - val (intrs, new_offset) = - fold_map (fn t_elem => fn off => - (* if 't_elem' existed at the previous depth, *) - (* proceed recursively, otherwise map the entire *) - (* subtree to "undefined" *) - if member (op =) terms' t_elem then - make_constr ds off - else - (make_undef ds, off)) - terms offset - in - (Node intrs, new_offset) + "total is not equal to current size") + else () + (* returns an interpretation where everything is mapped to *) + (* an "undefined" element of the datatype *) + fun make_undef [] = Leaf (replicate total False) + | make_undef (d::ds) = + let + (* compute the current size of the type 'd' *) + val dT = typ_of_dtyp descr typ_assoc d + val size = size_of_type thy (typs, []) dT + in + Node (replicate size (make_undef ds)) + end + (* returns the interpretation for a constructor *) + fun make_constr [] offset = + if offset < total then + (Leaf (replicate offset False @ True :: + (replicate (total - offset - 1) False)), offset + 1) + else + raise REFUTE ("IDT_constructor_interpreter", + "offset >= total") + | make_constr (d::ds) offset = + let + (* Term.typ *) + val dT = typ_of_dtyp descr typ_assoc d + (* compute canonical term representations for all *) + (* elements of the type 'd' (with the reduced depth *) + (* for the IDT) *) + val terms' = canonical_terms typs' dT + (* sanity check *) + val _ = + if length terms' <> size_of_type thy (typs', []) dT + then + raise REFUTE ("IDT_constructor_interpreter", + "length of terms' is not equal to old size") + else () + (* compute canonical term representations for all *) + (* elements of the type 'd' (with the current depth *) + (* for the IDT) *) + val terms = canonical_terms typs dT + (* sanity check *) + val _ = + if length terms <> size_of_type thy (typs, []) dT + then + raise REFUTE ("IDT_constructor_interpreter", + "length of terms is not equal to current size") + else () + (* sanity check *) + val _ = + if length terms < length terms' then + raise REFUTE ("IDT_constructor_interpreter", + "current size is less than old size") + else () + (* sanity check: every element of terms' must also be *) + (* present in terms *) + val _ = + if forall (member (op =) terms) terms' then () + else + raise REFUTE ("IDT_constructor_interpreter", + "element has disappeared") + (* sanity check: the order on elements of terms' is *) + (* the same in terms, for those elements *) + val _ = + let + fun search (x::xs) (y::ys) = + if x = y then search xs ys else search (x::xs) ys + | search (x::xs) [] = + raise REFUTE ("IDT_constructor_interpreter", + "element order not preserved") + | search [] _ = () + in search terms' terms end + (* int * interpretation list *) + val (intrs, new_offset) = + fold_map (fn t_elem => fn off => + (* if 't_elem' existed at the previous depth, *) + (* proceed recursively, otherwise map the entire *) + (* subtree to "undefined" *) + if member (op =) terms' t_elem then + make_constr ds off + else + (make_undef ds, off)) + terms offset + in + (Node intrs, new_offset) + end + in + SOME (fst (make_constr ctypes offset), model, args) + end end - in - SOME (fst (make_constr ctypes offset), model, args) - end - end - | NONE => (* body type is not an inductive datatype *) - NONE) - | _ => (* body type is a (free or schematic) type variable *) + | NONE => (* body type is not an inductive datatype *) + NONE) + | _ => (* body type is a (free or schematic) type variable *) + NONE) + | _ => (* term is not a constant *) NONE) - | _ => (* term is not a constant *) - NONE) end; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* Difficult code ahead. Make sure you understand the *) - (* 'IDT_constructor_interpreter' and the order in which it enumerates *) - (* elements of an IDT before you try to understand this function. *) +(* Difficult code ahead. Make sure you understand the *) +(* 'IDT_constructor_interpreter' and the order in which it enumerates *) +(* elements of an IDT before you try to understand this function. *) - fun IDT_recursion_interpreter thy model args t = - (* careful: here we descend arbitrarily deep into 't', possibly before *) - (* any other interpreter for atomic terms has had a chance to look at *) - (* 't' *) - case strip_comb t of - (Const (s, T), params) => +fun IDT_recursion_interpreter thy model args t = + (* careful: here we descend arbitrarily deep into 't', possibly before *) + (* any other interpreter for atomic terms has had a chance to look at *) + (* 't' *) + case strip_comb t of + (Const (s, T), params) => (* iterate over all datatypes in 'thy' *) Symtab.fold (fn (_, info) => fn result => case result of SOME _ => - result (* just keep 'result' *) + result (* just keep 'result' *) | NONE => - if member (op =) (#rec_names info) s then - (* we do have a recursion operator of one of the (mutually *) - (* recursive) datatypes given by 'info' *) - let - (* number of all constructors, including those of different *) - (* (mutually recursive) datatypes within the same descriptor *) - val mconstrs_count = - Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info)) - in - if mconstrs_count < length params then - (* too many actual parameters; for now we'll use the *) - (* 'stlc_interpreter' to strip off one application *) - NONE - else if mconstrs_count > length params then - (* too few actual parameters; we use eta expansion *) - (* Note that the resulting expansion of lambda abstractions *) - (* by the 'stlc_interpreter' may be rather slow (depending *) - (* on the argument types and the size of the IDT, of *) - (* course). *) - SOME (interpret thy model args (eta_expand t - (mconstrs_count - length params))) - else (* mconstrs_count = length params *) - let - (* interpret each parameter separately *) - val (p_intrs, (model', args')) = fold_map (fn p => fn (m, a) => - let - val (i, m', a') = interpret thy m a p - in - (i, (m', a')) - end) params (model, args) - val (typs, _) = model' - (* 'index' is /not/ necessarily the index of the IDT that *) - (* the recursion operator is associated with, but merely *) - (* the index of some mutually recursive IDT *) - val index = #index info - val descr = #descr info - val (_, dtyps, _) = the (AList.lookup (op =) descr index) - (* sanity check: we assume that the order of constructors *) - (* in 'descr' is the same as the order of *) - (* corresponding parameters, otherwise the *) - (* association code below won't match the *) - (* right constructors/parameters; we also *) - (* assume that the order of recursion *) - (* operators in '#rec_names info' is the *) - (* same as the order of corresponding *) - (* datatypes in 'descr' *) - val _ = if map fst descr <> (0 upto (length descr - 1)) then - raise REFUTE ("IDT_recursion_interpreter", - "order of constructors and corresponding parameters/" ^ - "recursion operators and corresponding datatypes " ^ - "different?") - else () - (* sanity check: every element in 'dtyps' must be a *) - (* 'DtTFree' *) - val _ = if Library.exists (fn d => - case d of Datatype_Aux.DtTFree _ => false - | _ => true) dtyps - then - raise REFUTE ("IDT_recursion_interpreter", - "datatype argument is not a variable") - else () - (* the type of a recursion operator is *) - (* [T1, ..., Tn, IDT] ---> Tresult *) - val IDT = List.nth (binder_types T, mconstrs_count) - (* by our assumption on the order of recursion operators *) - (* and datatypes, this is the index of the datatype *) - (* corresponding to the given recursion operator *) - val idt_index = find_index (fn s' => s' = s) (#rec_names info) - (* mutually recursive types must have the same type *) - (* parameters, unless the mutual recursion comes from *) - (* indirect recursion *) - fun rec_typ_assoc acc [] = - acc - | rec_typ_assoc acc ((d, T)::xs) = - (case AList.lookup op= acc d of - NONE => - (case d of - Datatype_Aux.DtTFree _ => - (* add the association, proceed *) - rec_typ_assoc ((d, T)::acc) xs - | Datatype_Aux.DtType (s, ds) => - let - val (s', Ts) = dest_Type T - in - if s=s' then - rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs) - else - raise REFUTE ("IDT_recursion_interpreter", - "DtType/Type mismatch") - end - | Datatype_Aux.DtRec i => - let - val (_, ds, _) = the (AList.lookup (op =) descr i) - val (_, Ts) = dest_Type T - in - rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs) - end) - | SOME T' => - if T=T' then - (* ignore the association since it's already *) - (* present, proceed *) - rec_typ_assoc acc xs - else + if member (op =) (#rec_names info) s then + (* we do have a recursion operator of one of the (mutually *) + (* recursive) datatypes given by 'info' *) + let + (* number of all constructors, including those of different *) + (* (mutually recursive) datatypes within the same descriptor *) + val mconstrs_count = + Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info)) + in + if mconstrs_count < length params then + (* too many actual parameters; for now we'll use the *) + (* 'stlc_interpreter' to strip off one application *) + NONE + else if mconstrs_count > length params then + (* too few actual parameters; we use eta expansion *) + (* Note that the resulting expansion of lambda abstractions *) + (* by the 'stlc_interpreter' may be rather slow (depending *) + (* on the argument types and the size of the IDT, of *) + (* course). *) + SOME (interpret thy model args (eta_expand t + (mconstrs_count - length params))) + else (* mconstrs_count = length params *) + let + (* interpret each parameter separately *) + val (p_intrs, (model', args')) = fold_map (fn p => fn (m, a) => + let + val (i, m', a') = interpret thy m a p + in + (i, (m', a')) + end) params (model, args) + val (typs, _) = model' + (* 'index' is /not/ necessarily the index of the IDT that *) + (* the recursion operator is associated with, but merely *) + (* the index of some mutually recursive IDT *) + val index = #index info + val descr = #descr info + val (_, dtyps, _) = the (AList.lookup (op =) descr index) + (* sanity check: we assume that the order of constructors *) + (* in 'descr' is the same as the order of *) + (* corresponding parameters, otherwise the *) + (* association code below won't match the *) + (* right constructors/parameters; we also *) + (* assume that the order of recursion *) + (* operators in '#rec_names info' is the *) + (* same as the order of corresponding *) + (* datatypes in 'descr' *) + val _ = if map fst descr <> (0 upto (length descr - 1)) then + raise REFUTE ("IDT_recursion_interpreter", + "order of constructors and corresponding parameters/" ^ + "recursion operators and corresponding datatypes " ^ + "different?") + else () + (* sanity check: every element in 'dtyps' must be a *) + (* 'DtTFree' *) + val _ = + if Library.exists (fn d => + case d of Datatype_Aux.DtTFree _ => false + | _ => true) dtyps + then raise REFUTE ("IDT_recursion_interpreter", - "different type associations for the same dtyp")) - val typ_assoc = filter - (fn (Datatype_Aux.DtTFree _, _) => true | (_, _) => false) - (rec_typ_assoc [] - (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT)) - (* sanity check: typ_assoc must associate types to the *) - (* elements of 'dtyps' (and only to those) *) - val _ = if not (eq_set (op =) (dtyps, map fst typ_assoc)) - then - raise REFUTE ("IDT_recursion_interpreter", - "type association has extra/missing elements") - else () - (* interpret each constructor in the descriptor (including *) - (* those of mutually recursive datatypes) *) - (* (int * interpretation list) list *) - val mc_intrs = map (fn (idx, (_, _, cs)) => - let - val c_return_typ = typ_of_dtyp descr typ_assoc - (Datatype_Aux.DtRec idx) - in - (idx, map (fn (cname, cargs) => - (#1 o interpret thy (typs, []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], - wellformed=True}) (Const (cname, map (typ_of_dtyp - descr typ_assoc) cargs ---> c_return_typ))) cs) - end) descr - (* associate constructors with corresponding parameters *) - (* (int * (interpretation * interpretation) list) list *) - val (mc_p_intrs, p_intrs') = fold_map - (fn (idx, c_intrs) => fn p_intrs' => + "datatype argument is not a variable") + else () + (* the type of a recursion operator is *) + (* [T1, ..., Tn, IDT] ---> Tresult *) + val IDT = List.nth (binder_types T, mconstrs_count) + (* by our assumption on the order of recursion operators *) + (* and datatypes, this is the index of the datatype *) + (* corresponding to the given recursion operator *) + val idt_index = find_index (fn s' => s' = s) (#rec_names info) + (* mutually recursive types must have the same type *) + (* parameters, unless the mutual recursion comes from *) + (* indirect recursion *) + fun rec_typ_assoc acc [] = acc + | rec_typ_assoc acc ((d, T)::xs) = + (case AList.lookup op= acc d of + NONE => + (case d of + Datatype_Aux.DtTFree _ => + (* add the association, proceed *) + rec_typ_assoc ((d, T)::acc) xs + | Datatype_Aux.DtType (s, ds) => + let + val (s', Ts) = dest_Type T + in + if s=s' then + rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs) + else + raise REFUTE ("IDT_recursion_interpreter", + "DtType/Type mismatch") + end + | Datatype_Aux.DtRec i => + let + val (_, ds, _) = the (AList.lookup (op =) descr i) + val (_, Ts) = dest_Type T + in + rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs) + end) + | SOME T' => + if T=T' then + (* ignore the association since it's already *) + (* present, proceed *) + rec_typ_assoc acc xs + else + raise REFUTE ("IDT_recursion_interpreter", + "different type associations for the same dtyp")) + val typ_assoc = filter + (fn (Datatype_Aux.DtTFree _, _) => true | (_, _) => false) + (rec_typ_assoc [] + (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT)) + (* sanity check: typ_assoc must associate types to the *) + (* elements of 'dtyps' (and only to those) *) + val _ = + if not (eq_set (op =) (dtyps, map fst typ_assoc)) + then + raise REFUTE ("IDT_recursion_interpreter", + "type association has extra/missing elements") + else () + (* interpret each constructor in the descriptor (including *) + (* those of mutually recursive datatypes) *) + (* (int * interpretation list) list *) + val mc_intrs = map (fn (idx, (_, _, cs)) => let - val len = length c_intrs + val c_return_typ = typ_of_dtyp descr typ_assoc + (Datatype_Aux.DtRec idx) in - ((idx, c_intrs ~~ List.take (p_intrs', len)), - List.drop (p_intrs', len)) - end) mc_intrs p_intrs - (* sanity check: no 'p_intr' may be left afterwards *) - val _ = if p_intrs' <> [] then - raise REFUTE ("IDT_recursion_interpreter", - "more parameter than constructor interpretations") - else () - (* The recursion operator, applied to 'mconstrs_count' *) - (* arguments, is a function that maps every element of the *) - (* inductive datatype to an element of some result type. *) - (* Recursion operators for mutually recursive IDTs are *) - (* translated simultaneously. *) - (* Since the order on datatype elements is given by an *) - (* order on constructors (and then by the order on *) - (* argument tuples), we can simply copy corresponding *) - (* subtrees from 'p_intrs', in the order in which they are *) - (* given. *) - (* interpretation * interpretation -> interpretation list *) - fun ci_pi (Leaf xs, pi) = - (* if the constructor does not match the arguments to a *) - (* defined element of the IDT, the corresponding value *) - (* of the parameter must be ignored *) - if List.exists (equal True) xs then [pi] else [] - | ci_pi (Node xs, Node ys) = - maps ci_pi (xs ~~ ys) - | ci_pi (Node _, Leaf _) = - raise REFUTE ("IDT_recursion_interpreter", - "constructor takes more arguments than the " ^ - "associated parameter") - (* (int * interpretation list) list *) - val rec_operators = map (fn (idx, c_p_intrs) => - (idx, maps ci_pi c_p_intrs)) mc_p_intrs - (* sanity check: every recursion operator must provide as *) - (* many values as the corresponding datatype *) - (* has elements *) - val _ = map (fn (idx, intrs) => - let - val T = typ_of_dtyp descr typ_assoc - (Datatype_Aux.DtRec idx) - in - if length intrs <> size_of_type thy (typs, []) T then + (idx, map (fn (cname, cargs) => + (#1 o interpret thy (typs, []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], + wellformed=True}) (Const (cname, map (typ_of_dtyp + descr typ_assoc) cargs ---> c_return_typ))) cs) + end) descr + (* associate constructors with corresponding parameters *) + (* (int * (interpretation * interpretation) list) list *) + val (mc_p_intrs, p_intrs') = fold_map + (fn (idx, c_intrs) => fn p_intrs' => + let + val len = length c_intrs + in + ((idx, c_intrs ~~ List.take (p_intrs', len)), + List.drop (p_intrs', len)) + end) mc_intrs p_intrs + (* sanity check: no 'p_intr' may be left afterwards *) + val _ = + if p_intrs' <> [] then raise REFUTE ("IDT_recursion_interpreter", - "wrong number of interpretations for rec. operator") + "more parameter than constructor interpretations") else () - end) rec_operators - (* For non-recursive datatypes, we are pretty much done at *) - (* this point. For recursive datatypes however, we still *) - (* need to apply the interpretations in 'rec_operators' to *) - (* (recursively obtained) interpretations for recursive *) - (* constructor arguments. To do so more efficiently, we *) - (* copy 'rec_operators' into arrays first. Each Boolean *) - (* indicates whether the recursive arguments have been *) - (* considered already. *) - (* (int * (bool * interpretation) Array.array) list *) - val REC_OPERATORS = map (fn (idx, intrs) => - (idx, Array.fromList (map (pair false) intrs))) - rec_operators - (* takes an interpretation, and if some leaf of this *) - (* interpretation is the 'elem'-th element of the type, *) - (* the indices of the arguments leading to this leaf are *) - (* returned *) - (* interpretation -> int -> int list option *) - fun get_args (Leaf xs) elem = - if find_index (fn x => x = True) xs = elem then - SOME [] - else - NONE - | get_args (Node xs) elem = - let - (* interpretation list * int -> int list option *) - fun search ([], _) = - NONE - | search (x::xs, n) = - (case get_args x elem of - SOME result => SOME (n::result) - | NONE => search (xs, n+1)) - in - search (xs, 0) - end - (* returns the index of the constructor and indices for *) - (* its arguments that generate the 'elem'-th element of *) - (* the datatype given by 'idx' *) - (* int -> int -> int * int list *) - fun get_cargs idx elem = - let - (* int * interpretation list -> int * int list *) - fun get_cargs_rec (_, []) = - raise REFUTE ("IDT_recursion_interpreter", - "no matching constructor found for datatype element") - | get_cargs_rec (n, x::xs) = - (case get_args x elem of - SOME args => (n, args) - | NONE => get_cargs_rec (n+1, xs)) - in - get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx)) - end - (* computes one entry in 'REC_OPERATORS', and recursively *) - (* all entries needed for it, where 'idx' gives the *) - (* datatype and 'elem' the element of it *) - (* int -> int -> interpretation *) - fun compute_array_entry idx elem = - let - val arr = the (AList.lookup (op =) REC_OPERATORS idx) - val (flag, intr) = Array.sub (arr, elem) - in - if flag then - (* simply return the previously computed result *) - intr - else - (* we have to apply 'intr' to interpretations for all *) - (* recursive arguments *) + (* The recursion operator, applied to 'mconstrs_count' *) + (* arguments, is a function that maps every element of the *) + (* inductive datatype to an element of some result type. *) + (* Recursion operators for mutually recursive IDTs are *) + (* translated simultaneously. *) + (* Since the order on datatype elements is given by an *) + (* order on constructors (and then by the order on *) + (* argument tuples), we can simply copy corresponding *) + (* subtrees from 'p_intrs', in the order in which they are *) + (* given. *) + (* interpretation * interpretation -> interpretation list *) + fun ci_pi (Leaf xs, pi) = + (* if the constructor does not match the arguments to a *) + (* defined element of the IDT, the corresponding value *) + (* of the parameter must be ignored *) + if List.exists (equal True) xs then [pi] else [] + | ci_pi (Node xs, Node ys) = maps ci_pi (xs ~~ ys) + | ci_pi (Node _, Leaf _) = + raise REFUTE ("IDT_recursion_interpreter", + "constructor takes more arguments than the " ^ + "associated parameter") + (* (int * interpretation list) list *) + val rec_operators = map (fn (idx, c_p_intrs) => + (idx, maps ci_pi c_p_intrs)) mc_p_intrs + (* sanity check: every recursion operator must provide as *) + (* many values as the corresponding datatype *) + (* has elements *) + val _ = map (fn (idx, intrs) => + let + val T = typ_of_dtyp descr typ_assoc + (Datatype_Aux.DtRec idx) + in + if length intrs <> size_of_type thy (typs, []) T then + raise REFUTE ("IDT_recursion_interpreter", + "wrong number of interpretations for rec. operator") + else () + end) rec_operators + (* For non-recursive datatypes, we are pretty much done at *) + (* this point. For recursive datatypes however, we still *) + (* need to apply the interpretations in 'rec_operators' to *) + (* (recursively obtained) interpretations for recursive *) + (* constructor arguments. To do so more efficiently, we *) + (* copy 'rec_operators' into arrays first. Each Boolean *) + (* indicates whether the recursive arguments have been *) + (* considered already. *) + (* (int * (bool * interpretation) Array.array) list *) + val REC_OPERATORS = map (fn (idx, intrs) => + (idx, Array.fromList (map (pair false) intrs))) + rec_operators + (* takes an interpretation, and if some leaf of this *) + (* interpretation is the 'elem'-th element of the type, *) + (* the indices of the arguments leading to this leaf are *) + (* returned *) + (* interpretation -> int -> int list option *) + fun get_args (Leaf xs) elem = + if find_index (fn x => x = True) xs = elem then + SOME [] + else + NONE + | get_args (Node xs) elem = + let + (* interpretation list * int -> int list option *) + fun search ([], _) = + NONE + | search (x::xs, n) = + (case get_args x elem of + SOME result => SOME (n::result) + | NONE => search (xs, n+1)) + in + search (xs, 0) + end + (* returns the index of the constructor and indices for *) + (* its arguments that generate the 'elem'-th element of *) + (* the datatype given by 'idx' *) + (* int -> int -> int * int list *) + fun get_cargs idx elem = let - (* int * int list *) - val (c, args) = get_cargs idx elem - (* find the indices of the constructor's /recursive/ *) - (* arguments *) - val (_, _, constrs) = the (AList.lookup (op =) descr idx) - val (_, dtyps) = List.nth (constrs, c) - val rec_dtyps_args = filter - (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args) - (* map those indices to interpretations *) - val rec_dtyps_intrs = map (fn (dtyp, arg) => + (* int * interpretation list -> int * int list *) + fun get_cargs_rec (_, []) = + raise REFUTE ("IDT_recursion_interpreter", + "no matching constructor found for datatype element") + | get_cargs_rec (n, x::xs) = + (case get_args x elem of + SOME args => (n, args) + | NONE => get_cargs_rec (n+1, xs)) + in + get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx)) + end + (* computes one entry in 'REC_OPERATORS', and recursively *) + (* all entries needed for it, where 'idx' gives the *) + (* datatype and 'elem' the element of it *) + (* int -> int -> interpretation *) + fun compute_array_entry idx elem = + let + val arr = the (AList.lookup (op =) REC_OPERATORS idx) + val (flag, intr) = Array.sub (arr, elem) + in + if flag then + (* simply return the previously computed result *) + intr + else + (* we have to apply 'intr' to interpretations for all *) + (* recursive arguments *) let - val dT = typ_of_dtyp descr typ_assoc dtyp - val consts = make_constants thy (typs, []) dT - val arg_i = List.nth (consts, arg) + (* int * int list *) + val (c, args) = get_cargs idx elem + (* find the indices of the constructor's /recursive/ *) + (* arguments *) + val (_, _, constrs) = the (AList.lookup (op =) descr idx) + val (_, dtyps) = List.nth (constrs, c) + val rec_dtyps_args = filter + (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args) + (* map those indices to interpretations *) + val rec_dtyps_intrs = map (fn (dtyp, arg) => + let + val dT = typ_of_dtyp descr typ_assoc dtyp + val consts = make_constants thy (typs, []) dT + val arg_i = List.nth (consts, arg) + in + (dtyp, arg_i) + end) rec_dtyps_args + (* takes the dtyp and interpretation of an element, *) + (* and computes the interpretation for the *) + (* corresponding recursive argument *) + fun rec_intr (Datatype_Aux.DtRec i) (Leaf xs) = + (* recursive argument is "rec_i params elem" *) + compute_array_entry i (find_index (fn x => x = True) xs) + | rec_intr (Datatype_Aux.DtRec _) (Node _) = + raise REFUTE ("IDT_recursion_interpreter", + "interpretation for IDT is a node") + | rec_intr (Datatype_Aux.DtType ("fun", [dt1, dt2])) (Node xs) = + (* recursive argument is something like *) + (* "\x::dt1. rec_? params (elem x)" *) + Node (map (rec_intr dt2) xs) + | rec_intr (Datatype_Aux.DtType ("fun", [_, _])) (Leaf _) = + raise REFUTE ("IDT_recursion_interpreter", + "interpretation for function dtyp is a leaf") + | rec_intr _ _ = + (* admissibility ensures that every recursive type *) + (* is of the form 'Dt_1 -> ... -> Dt_k -> *) + (* (DtRec i)' *) + raise REFUTE ("IDT_recursion_interpreter", + "non-recursive codomain in recursive dtyp") + (* obtain interpretations for recursive arguments *) + (* interpretation list *) + val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs + (* apply 'intr' to all recursive arguments *) + val result = fold (fn arg_i => fn i => + interpretation_apply (i, arg_i)) arg_intrs intr + (* update 'REC_OPERATORS' *) + val _ = Array.update (arr, elem, (true, result)) in - (dtyp, arg_i) - end) rec_dtyps_args - (* takes the dtyp and interpretation of an element, *) - (* and computes the interpretation for the *) - (* corresponding recursive argument *) - fun rec_intr (Datatype_Aux.DtRec i) (Leaf xs) = - (* recursive argument is "rec_i params elem" *) - compute_array_entry i (find_index (fn x => x = True) xs) - | rec_intr (Datatype_Aux.DtRec _) (Node _) = - raise REFUTE ("IDT_recursion_interpreter", - "interpretation for IDT is a node") - | rec_intr (Datatype_Aux.DtType ("fun", [dt1, dt2])) - (Node xs) = - (* recursive argument is something like *) - (* "\x::dt1. rec_? params (elem x)" *) - Node (map (rec_intr dt2) xs) - | rec_intr (Datatype_Aux.DtType ("fun", [_, _])) - (Leaf _) = + result + end + end + val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index)) + (* sanity check: the size of 'IDT' should be 'idt_size' *) + val _ = + if idt_size <> size_of_type thy (typs, []) IDT then raise REFUTE ("IDT_recursion_interpreter", - "interpretation for function dtyp is a leaf") - | rec_intr _ _ = - (* admissibility ensures that every recursive type *) - (* is of the form 'Dt_1 -> ... -> Dt_k -> *) - (* (DtRec i)' *) - raise REFUTE ("IDT_recursion_interpreter", - "non-recursive codomain in recursive dtyp") - (* obtain interpretations for recursive arguments *) - (* interpretation list *) - val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs - (* apply 'intr' to all recursive arguments *) - val result = fold (fn arg_i => fn i => - interpretation_apply (i, arg_i)) arg_intrs intr - (* update 'REC_OPERATORS' *) - val _ = Array.update (arr, elem, (true, result)) - in - result - end + "unexpected size of IDT (wrong type associated?)") + else () + (* interpretation *) + val rec_op = Node (map_range (compute_array_entry idt_index) idt_size) + in + SOME (rec_op, model', args') end - val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index)) - (* sanity check: the size of 'IDT' should be 'idt_size' *) - val _ = if idt_size <> size_of_type thy (typs, []) IDT then - raise REFUTE ("IDT_recursion_interpreter", - "unexpected size of IDT (wrong type associated?)") - else () - (* interpretation *) - val rec_op = Node (map_range (compute_array_entry idt_index) idt_size) - in - SOME (rec_op, model', args') - end - end - else - NONE (* not a recursion operator of this datatype *) + end + else + NONE (* not a recursion operator of this datatype *) ) (Datatype.get_all thy) NONE - | _ => (* head of term is not a constant *) - NONE; + | _ => (* head of term is not a constant *) + NONE; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - fun set_interpreter thy model args t = +fun set_interpreter thy model args t = let val (typs, terms) = model in case AList.lookup (op =) terms t of SOME intr => - (* return an existing interpretation *) - SOME (intr, model, args) + (* return an existing interpretation *) + SOME (intr, model, args) | NONE => - (case t of - (* 'Collect' == identity *) - Const (@{const_name Collect}, _) $ t1 => - SOME (interpret thy model args t1) - | Const (@{const_name Collect}, _) => - SOME (interpret thy model args (eta_expand t 1)) - (* 'op :' == application *) - | Const (@{const_name Set.member}, _) $ t1 $ t2 => - SOME (interpret thy model args (t2 $ t1)) - | Const (@{const_name Set.member}, _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) - | Const (@{const_name Set.member}, _) => - SOME (interpret thy model args (eta_expand t 2)) - | _ => NONE) + (case t of + (* 'Collect' == identity *) + Const (@{const_name Collect}, _) $ t1 => + SOME (interpret thy model args t1) + | Const (@{const_name Collect}, _) => + SOME (interpret thy model args (eta_expand t 1)) + (* 'op :' == application *) + | Const (@{const_name Set.member}, _) $ t1 $ t2 => + SOME (interpret thy model args (t2 $ t1)) + | Const (@{const_name Set.member}, _) $ t1 => + SOME (interpret thy model args (eta_expand t 1)) + | Const (@{const_name Set.member}, _) => + SOME (interpret thy model args (eta_expand t 2)) + | _ => NONE) end; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* 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 more efficient *) +(* only an optimization: 'card' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) - fun Finite_Set_card_interpreter thy model args t = - case t of - Const (@{const_name Finite_Set.card}, - Type ("fun", [Type ("fun", [T, @{typ bool}]), - @{typ nat}])) => +fun Finite_Set_card_interpreter thy model args t = + case t of + Const (@{const_name Finite_Set.card}, + Type ("fun", [Type ("fun", [T, @{typ bool}]), @{typ nat}])) => let (* interpretation -> int *) fun number_of_elements (Node xs) = @@ -2668,8 +2658,8 @@ "interpretation for set type does not yield a Boolean")) xs 0 | number_of_elements (Leaf _) = - raise REFUTE ("Finite_Set_card_interpreter", - "interpretation for set type is a leaf") + raise REFUTE ("Finite_Set_card_interpreter", + "interpretation for set type is a leaf") val size_of_nat = size_of_type thy model (@{typ nat}) (* takes an interpretation for a set and returns an interpretation *) (* for a 'nat' denoting the set's cardinality *) @@ -2678,7 +2668,7 @@ let val n = number_of_elements i in - if n - NONE; + | _ => NONE; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* only an optimization: 'finite' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) +(* only an optimization: 'finite' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) - fun Finite_Set_finite_interpreter thy model args t = - case t of - Const (@{const_name Finite_Set.finite}, - Type ("fun", [Type ("fun", [T, @{typ bool}]), - @{typ bool}])) $ _ => +fun Finite_Set_finite_interpreter thy model args t = + case t of + Const (@{const_name Finite_Set.finite}, + Type ("fun", [Type ("fun", [T, @{typ bool}]), + @{typ bool}])) $ _ => (* we only consider finite models anyway, hence EVERY set is *) (* "finite" *) SOME (TT, model, args) - | Const (@{const_name Finite_Set.finite}, - Type ("fun", [Type ("fun", [T, @{typ bool}]), - @{typ bool}])) => + | Const (@{const_name Finite_Set.finite}, + Type ("fun", [Type ("fun", [T, @{typ bool}]), + @{typ bool}])) => let val size_of_set = size_of_type thy model (Type ("fun", [T, HOLogic.boolT])) @@ -2718,19 +2707,18 @@ (* "finite" *) SOME (Node (replicate size_of_set TT), model, args) end - | _ => - NONE; + | _ => NONE; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* only an optimization: 'less' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) +(* only an optimization: 'less' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) - fun Nat_less_interpreter thy model args t = - case t of - Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat}, +fun Nat_less_interpreter thy model args t = + case t of + Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat}, Type ("fun", [@{typ nat}, @{typ bool}])])) => let val size_of_nat = size_of_type thy model (@{typ nat}) @@ -2741,19 +2729,18 @@ in SOME (Node (map less (1 upto size_of_nat)), model, args) end - | _ => - NONE; + | _ => NONE; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* only an optimization: 'plus' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) +(* only an optimization: 'plus' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) - fun Nat_plus_interpreter thy model args t = - case t of - Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat}, +fun Nat_plus_interpreter thy model args t = + case t of + Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat}, Type ("fun", [@{typ nat}, @{typ nat}])])) => let val size_of_nat = size_of_type thy model (@{typ nat}) @@ -2772,19 +2759,18 @@ SOME (Node (map_range (fn m => Node (map_range (plus m) size_of_nat)) size_of_nat), model, args) end - | _ => - NONE; + | _ => NONE; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* only an optimization: 'minus' could in principle be interpreted *) - (* with interpreters available already (using its definition), but the *) - (* code below is more efficient *) +(* only an optimization: 'minus' could in principle be interpreted *) +(* with interpreters available already (using its definition), but the *) +(* code below is more efficient *) - fun Nat_minus_interpreter thy model args t = - case t of - Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat}, +fun Nat_minus_interpreter thy model args t = + case t of + Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat}, Type ("fun", [@{typ nat}, @{typ nat}])])) => let val size_of_nat = size_of_type thy model (@{typ nat}) @@ -2800,19 +2786,18 @@ SOME (Node (map_range (fn m => Node (map_range (minus m) size_of_nat)) size_of_nat), model, args) end - | _ => - NONE; + | _ => NONE; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* only an optimization: 'times' could in principle be interpreted *) - (* with interpreters available already (using its definition), but the *) - (* code below is more efficient *) +(* only an optimization: 'times' could in principle be interpreted *) +(* with interpreters available already (using its definition), but the *) +(* code below is more efficient *) - fun Nat_times_interpreter thy model args t = - case t of - Const (@{const_name Groups.times}, Type ("fun", [@{typ nat}, +fun Nat_times_interpreter thy model args t = + case t of + Const (@{const_name Groups.times}, Type ("fun", [@{typ nat}, Type ("fun", [@{typ nat}, @{typ nat}])])) => let val size_of_nat = size_of_type thy model (@{typ nat}) @@ -2831,25 +2816,25 @@ SOME (Node (map_range (fn m => Node (map_range (mult m) size_of_nat)) size_of_nat), model, args) end - | _ => - NONE; + | _ => NONE; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* only an optimization: 'append' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) +(* only an optimization: 'append' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) - fun List_append_interpreter thy model args t = - case t of - Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun", +fun List_append_interpreter thy model args t = + case t of + Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun", [Type ("List.list", [_]), Type ("List.list", [_])])])) => let - val size_elem = size_of_type thy model T - val size_list = size_of_type thy model (Type ("List.list", [T])) + val size_elem = size_of_type thy model T + val size_list = size_of_type thy model (Type ("List.list", [T])) (* maximal length of lists; 0 if we only consider the empty list *) - val list_length = let + val list_length = + let (* int -> int -> int -> int *) fun list_length_acc len lists total = if lists = total then @@ -2893,12 +2878,12 @@ in case offsets' of [] => - (* we're at the last node in the tree; the next value *) - (* won't be used anyway *) - (assoc, ([], 0)) + (* we're at the last node in the tree; the next value *) + (* won't be used anyway *) + (assoc, ([], 0)) | off'::offs' => - (* go to next sibling node *) - (assoc, (offs', off' + 1)) + (* go to next sibling node *) + (assoc, (offs', off' + 1)) end end) elements ([], 0) (* we also need the reverse association (from length/offset to *) @@ -2913,36 +2898,35 @@ val len_elem = len_m + len_n val off_elem = off_m * power (size_elem, len_n) + off_n in - case AList.lookup op= lenoff'_lists (len_elem, off_elem) of + case AList.lookup op= lenoff'_lists (len_elem, off_elem) of NONE => - (* undefined *) - Leaf (replicate size_list False) + (* undefined *) + Leaf (replicate size_list False) | SOME element => - Leaf ((replicate element False) @ True :: - (replicate (size_list - element - 1) False)) + Leaf ((replicate element False) @ True :: + (replicate (size_list - element - 1) False)) end in SOME (Node (map (fn m => Node (map (append m) elements)) elements), model, args) end - | _ => - NONE; + | _ => NONE; (* UNSOUND - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* only an optimization: 'lfp' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) +(* only an optimization: 'lfp' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) - fun lfp_interpreter thy model args t = - case t of - Const (@{const_name lfp}, Type ("fun", [Type ("fun", - [Type ("fun", [T, @{typ bool}]), - Type ("fun", [_, @{typ bool}])]), - Type ("fun", [_, @{typ bool}])])) => +fun lfp_interpreter thy model args t = + case t of + Const (@{const_name lfp}, Type ("fun", [Type ("fun", + [Type ("fun", [T, @{typ bool}]), + Type ("fun", [_, @{typ bool}])]), + Type ("fun", [_, @{typ bool}])])) => let val size_elem = size_of_type thy model T (* the universe (i.e. the set that contains every element) *) @@ -2957,294 +2941,296 @@ (* "lfp(f) == Inter({u. f(u) <= u})" *) (* interpretation * interpretation -> bool *) fun is_subset (Node subs, Node sups) = - forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) - (subs ~~ sups) + forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups) | is_subset (_, _) = - raise REFUTE ("lfp_interpreter", - "is_subset: interpretation for set is not a node") + raise REFUTE ("lfp_interpreter", + "is_subset: interpretation for set is not a node") (* interpretation * interpretation -> interpretation *) fun intersection (Node xs, Node ys) = - Node (map (fn (x, y) => if x=TT andalso y=TT then TT else FF) - (xs ~~ ys)) + Node (map (fn (x, y) => if x=TT andalso y=TT then TT else FF) + (xs ~~ ys)) | intersection (_, _) = - raise REFUTE ("lfp_interpreter", - "intersection: interpretation for set is not a node") + raise REFUTE ("lfp_interpreter", + "intersection: interpretation for set is not a node") (* interpretation -> interpretaion *) fun lfp (Node resultsets) = - fold (fn (set, resultset) => fn acc => - if is_subset (resultset, set) then - intersection (acc, set) - else - acc) (i_sets ~~ resultsets) i_univ + fold (fn (set, resultset) => fn acc => + if is_subset (resultset, set) then + intersection (acc, set) + else + acc) (i_sets ~~ resultsets) i_univ | lfp _ = - raise REFUTE ("lfp_interpreter", - "lfp: interpretation for function is not a node") + raise REFUTE ("lfp_interpreter", + "lfp: interpretation for function is not a node") in SOME (Node (map lfp i_funs), model, args) end - | _ => - NONE; + | _ => NONE; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* only an optimization: 'gfp' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) +(* only an optimization: 'gfp' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) - fun gfp_interpreter thy model args t = - case t of - Const (@{const_name gfp}, Type ("fun", [Type ("fun", - [Type ("fun", [T, @{typ bool}]), - Type ("fun", [_, @{typ bool}])]), - Type ("fun", [_, @{typ bool}])])) => - let - val size_elem = size_of_type thy model T - (* the universe (i.e. the set that contains every element) *) - val i_univ = Node (replicate size_elem TT) - (* all sets with elements from type 'T' *) - val i_sets = - make_constants thy model (Type ("fun", [T, HOLogic.boolT])) - (* all functions that map sets to sets *) - val i_funs = make_constants thy model (Type ("fun", - [Type ("fun", [T, HOLogic.boolT]), - Type ("fun", [T, HOLogic.boolT])])) - (* "gfp(f) == Union({u. u <= f(u)})" *) - (* interpretation * interpretation -> bool *) - fun is_subset (Node subs, Node sups) = - forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) - (subs ~~ sups) - | is_subset (_, _) = - raise REFUTE ("gfp_interpreter", - "is_subset: interpretation for set is not a node") - (* interpretation * interpretation -> interpretation *) - fun union (Node xs, Node ys) = +fun gfp_interpreter thy model args t = + case t of + Const (@{const_name gfp}, Type ("fun", [Type ("fun", + [Type ("fun", [T, @{typ bool}]), + Type ("fun", [_, @{typ bool}])]), + Type ("fun", [_, @{typ bool}])])) => + let + val size_elem = size_of_type thy model T + (* the universe (i.e. the set that contains every element) *) + val i_univ = Node (replicate size_elem TT) + (* all sets with elements from type 'T' *) + val i_sets = + make_constants thy model (Type ("fun", [T, HOLogic.boolT])) + (* all functions that map sets to sets *) + val i_funs = make_constants thy model (Type ("fun", + [Type ("fun", [T, HOLogic.boolT]), + Type ("fun", [T, HOLogic.boolT])])) + (* "gfp(f) == Union({u. u <= f(u)})" *) + (* interpretation * interpretation -> bool *) + fun is_subset (Node subs, Node sups) = + forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) + (subs ~~ sups) + | is_subset (_, _) = + raise REFUTE ("gfp_interpreter", + "is_subset: interpretation for set is not a node") + (* interpretation * interpretation -> interpretation *) + fun union (Node xs, Node ys) = Node (map (fn (x,y) => if x=TT orelse y=TT then TT else FF) (xs ~~ ys)) - | union (_, _) = - raise REFUTE ("gfp_interpreter", - "union: interpretation for set is not a node") - (* interpretation -> interpretaion *) - fun gfp (Node resultsets) = - fold (fn (set, resultset) => fn acc => - if is_subset (set, resultset) then - union (acc, set) - else - acc) (i_sets ~~ resultsets) i_univ - | gfp _ = + | union (_, _) = + raise REFUTE ("gfp_interpreter", + "union: interpretation for set is not a node") + (* interpretation -> interpretaion *) + fun gfp (Node resultsets) = + fold (fn (set, resultset) => fn acc => + if is_subset (set, resultset) then + union (acc, set) + else + acc) (i_sets ~~ resultsets) i_univ + | gfp _ = raise REFUTE ("gfp_interpreter", "gfp: interpretation for function is not a node") - in - SOME (Node (map gfp i_funs), model, args) - end - | _ => - NONE; + in + SOME (Node (map gfp i_funs), model, args) + end + | _ => NONE; *) - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* only an optimization: 'fst' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) +(* only an optimization: 'fst' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) - fun Product_Type_fst_interpreter thy model args t = - case t of - Const (@{const_name fst}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) => +fun Product_Type_fst_interpreter thy model args t = + case t of + Const (@{const_name fst}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) => let val constants_T = make_constants thy model T - val size_U = size_of_type thy model U + val size_U = size_of_type thy model U in SOME (Node (maps (replicate size_U) constants_T), model, args) end - | _ => - NONE; + | _ => NONE; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) +(* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* only an optimization: 'snd' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) +(* only an optimization: 'snd' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) - fun Product_Type_snd_interpreter thy model args t = - case t of - Const (@{const_name snd}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) => +fun Product_Type_snd_interpreter thy model args t = + case t of + Const (@{const_name snd}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) => let - val size_T = size_of_type thy model T + val size_T = size_of_type thy model T val constants_U = make_constants thy model U in SOME (Node (flat (replicate size_T constants_U)), model, args) end - | _ => - NONE; + | _ => NONE; (* ------------------------------------------------------------------------- *) (* PRINTERS *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> Term.typ -> interpretation -> (int -> bool) -> - Term.term option *) +(* theory -> model -> Term.typ -> interpretation -> (int -> bool) -> + Term.term option *) - fun stlc_printer thy model T intr assignment = +fun stlc_printer thy model T intr assignment = let (* 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 (Type (s, _)) = s - | string_of_typ (TFree (x, _)) = strip_leading_quote x + 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 + strip_leading_quote x ^ string_of_int i (* interpretation -> int *) fun index_from_interpretation (Leaf xs) = - find_index (PropLogic.eval assignment) xs + find_index (PropLogic.eval assignment) xs | index_from_interpretation _ = - raise REFUTE ("stlc_printer", - "interpretation for ground type is not a leaf") + raise REFUTE ("stlc_printer", + "interpretation for ground type is not a leaf") in case T of Type ("fun", [T1, T2]) => - let - (* create all constants of type 'T1' *) - val constants = make_constants thy model T1 - (* 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 T1 arg assignment, - print thy model 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 (@{const_abbrev Set.empty}, HOLogic_setT) - val HOLogic_insert = - Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) - in - SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set) - end - | Type ("prop", []) => - (case index_from_interpretation intr of - ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT))) - | 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 _ => if index_from_interpretation intr = (~1) then - SOME (Const (@{const_name undefined}, T)) - else - SOME (Const (string_of_typ T ^ - string_of_int (index_from_interpretation intr), T)) - | TFree _ => if index_from_interpretation intr = (~1) then - SOME (Const (@{const_name undefined}, T)) - else - SOME (Const (string_of_typ T ^ - string_of_int (index_from_interpretation intr), T)) - | TVar _ => if index_from_interpretation intr = (~1) then - SOME (Const (@{const_name undefined}, T)) - else - SOME (Const (string_of_typ T ^ - string_of_int (index_from_interpretation intr), T)) + let + (* create all constants of type 'T1' *) + val constants = make_constants thy model T1 + (* 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 T1 arg assignment, + print thy model 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 (@{const_abbrev Set.empty}, HOLogic_setT) + val HOLogic_insert = + Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) + in + SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set) + end + | Type ("prop", []) => + (case index_from_interpretation intr of + ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT))) + | 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 _ => + if index_from_interpretation intr = (~1) then + SOME (Const (@{const_name undefined}, T)) + else + SOME (Const (string_of_typ T ^ + string_of_int (index_from_interpretation intr), T)) + | TFree _ => + if index_from_interpretation intr = (~1) then + SOME (Const (@{const_name undefined}, T)) + else + SOME (Const (string_of_typ T ^ + string_of_int (index_from_interpretation intr), T)) + | TVar _ => + if index_from_interpretation intr = (~1) then + SOME (Const (@{const_name undefined}, T)) + else + SOME (Const (string_of_typ T ^ + string_of_int (index_from_interpretation intr), T)) end; - (* theory -> model -> Term.typ -> interpretation -> (int -> bool) -> - Term.term option *) +(* theory -> model -> Term.typ -> interpretation -> (int -> bool) -> + Term.term option *) - fun IDT_printer thy model T intr assignment = - (case T of - Type (s, Ts) => +fun IDT_printer thy model T intr assignment = + (case T of + Type (s, Ts) => (case Datatype.get_info thy s of SOME info => (* inductive datatype *) - let - val (typs, _) = model - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = the (AList.lookup (op =) 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 Datatype_Aux.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("IDT_printer", "datatype argument (for type " ^ - Syntax.string_of_typ_global 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")) - in - if element < 0 then - SOME (Const (@{const_name undefined}, Type (s, Ts))) - else let - (* takes a datatype constructor, and if for some arguments this *) - (* constructor generates the datatype's element that is given by *) - (* 'element', returns the constructor (as a term) as well as the *) - (* indices of the arguments *) - fun get_constr_args (cname, cargs) = + let + val (typs, _) = model + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = the (AList.lookup (op =) 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 Datatype_Aux.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_printer", "datatype argument (for type " ^ + Syntax.string_of_typ_global 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")) + in + if element < 0 then + SOME (Const (@{const_name undefined}, Type (s, Ts))) + else let - val cTerm = Const (cname, - map (typ_of_dtyp descr typ_assoc) cargs ---> Type (s, Ts)) - val (iC, _, _) = interpret thy (typs, []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm - (* interpretation -> int list option *) - fun get_args (Leaf xs) = - if find_index (fn x => x = True) xs = element then - SOME [] - else - NONE - | get_args (Node xs) = + (* takes a datatype constructor, and if for some arguments this *) + (* constructor generates the datatype's element that is given by *) + (* 'element', returns the constructor (as a term) as well as the *) + (* indices of the arguments *) + fun get_constr_args (cname, cargs) = let - (* interpretation * int -> int list option *) - fun search ([], _) = - NONE - | search (x::xs, n) = - (case get_args x of - SOME result => SOME (n::result) - | NONE => search (xs, n+1)) + val cTerm = Const (cname, + map (typ_of_dtyp descr typ_assoc) cargs ---> Type (s, Ts)) + val (iC, _, _) = interpret thy (typs, []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm + (* interpretation -> int list option *) + fun get_args (Leaf xs) = + if find_index (fn x => x = True) xs = element then + SOME [] + else + NONE + | get_args (Node xs) = + let + (* interpretation * int -> int list option *) + fun search ([], _) = + NONE + | search (x::xs, n) = + (case get_args x of + SOME result => SOME (n::result) + | NONE => search (xs, n+1)) + in + search (xs, 0) + end in - search (xs, 0) + Option.map (fn args => (cTerm, cargs, args)) (get_args iC) end + val (cTerm, cargs, args) = + (* we could speed things up by computing the correct *) + (* constructor directly (rather than testing all *) + (* constructors), based on the order in which constructors *) + (* generate elements of datatypes; the current implementation *) + (* of 'IDT_printer' however is independent of the internals *) + (* of 'IDT_constructor_interpreter' *) + (case get_first get_constr_args constrs of + SOME x => x + | NONE => raise REFUTE ("IDT_printer", + "no matching constructor found for element " ^ + string_of_int element)) + val argsTerms = map (fn (d, n) => + let + val dT = typ_of_dtyp descr typ_assoc d + (* we only need the n-th element of this list, so there *) + (* might be a more efficient implementation that does not *) + (* generate all constants *) + val consts = make_constants thy (typs, []) dT + in + print thy (typs, []) dT (List.nth (consts, n)) assignment + end) (cargs ~~ args) in - Option.map (fn args => (cTerm, cargs, args)) (get_args iC) + SOME (list_comb (cTerm, argsTerms)) end - val (cTerm, cargs, args) = - (* we could speed things up by computing the correct *) - (* constructor directly (rather than testing all *) - (* constructors), based on the order in which constructors *) - (* generate elements of datatypes; the current implementation *) - (* of 'IDT_printer' however is independent of the internals *) - (* of 'IDT_constructor_interpreter' *) - (case get_first get_constr_args constrs of - SOME x => x - | NONE => raise REFUTE ("IDT_printer", - "no matching constructor found for element " ^ - string_of_int element)) - val argsTerms = map (fn (d, n) => - let - val dT = typ_of_dtyp descr typ_assoc d - (* we only need the n-th element of this list, so there *) - (* might be a more efficient implementation that does not *) - (* generate all constants *) - val consts = make_constants thy (typs, []) dT - in - print thy (typs, []) dT (List.nth (consts, n)) assignment - end) (cargs ~~ args) - in - SOME (list_comb (cTerm, argsTerms)) end - end | NONE => (* not an inductive datatype *) - NONE) - | _ => (* a (free or schematic) type variable *) + NONE) + | _ => (* a (free or schematic) type variable *) NONE); @@ -3260,28 +3246,29 @@ (* subterms that are then passed to other interpreters! *) (* ------------------------------------------------------------------------- *) - val setup = - 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 "IDT_constructor" IDT_constructor_interpreter #> - add_interpreter "IDT_recursion" IDT_recursion_interpreter #> - add_interpreter "Finite_Set.card" Finite_Set_card_interpreter #> - add_interpreter "Finite_Set.finite" Finite_Set_finite_interpreter #> - add_interpreter "Nat_Orderings.less" Nat_less_interpreter #> - add_interpreter "Nat_HOL.plus" Nat_plus_interpreter #> - add_interpreter "Nat_HOL.minus" Nat_minus_interpreter #> - add_interpreter "Nat_HOL.times" Nat_times_interpreter #> - add_interpreter "List.append" List_append_interpreter #> +val setup = + 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 "IDT_constructor" IDT_constructor_interpreter #> + add_interpreter "IDT_recursion" IDT_recursion_interpreter #> + add_interpreter "Finite_Set.card" Finite_Set_card_interpreter #> + add_interpreter "Finite_Set.finite" Finite_Set_finite_interpreter #> + add_interpreter "Nat_Orderings.less" Nat_less_interpreter #> + add_interpreter "Nat_HOL.plus" Nat_plus_interpreter #> + add_interpreter "Nat_HOL.minus" Nat_minus_interpreter #> + add_interpreter "Nat_HOL.times" Nat_times_interpreter #> + add_interpreter "List.append" List_append_interpreter #> (* UNSOUND - add_interpreter "lfp" lfp_interpreter #> - add_interpreter "gfp" gfp_interpreter #> + add_interpreter "lfp" lfp_interpreter #> + add_interpreter "gfp" gfp_interpreter #> *) - add_interpreter "Product_Type.fst" Product_Type_fst_interpreter #> - add_interpreter "Product_Type.snd" Product_Type_snd_interpreter #> - add_printer "stlc" stlc_printer #> - add_printer "IDT" IDT_printer; + add_interpreter "Product_Type.fst" Product_Type_fst_interpreter #> + add_interpreter "Product_Type.snd" Product_Type_snd_interpreter #> + add_printer "stlc" stlc_printer #> + add_printer "IDT" IDT_printer; -end (* structure Refute *) +end; +