# HG changeset patch # User wenzelm # Date 1175621051 -7200 # Node ID 1565d476a9e2a73e8bd97ac8263d4f3767ffef8c # Parent 535ae9dd4c4590775ebe68ced94384ca1248bd16 removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation); diff -r 535ae9dd4c45 -r 1565d476a9e2 src/HOL/Library/sct.ML --- a/src/HOL/Library/sct.ML Tue Apr 03 19:24:10 2007 +0200 +++ b/src/HOL/Library/sct.ML Tue Apr 03 19:24:11 2007 +0200 @@ -101,7 +101,7 @@ end | dest_all_ex t = ([],t) -fun dist_vars [] vs = (assert (null vs) "dist_vars"; []) +fun dist_vars [] vs = (null vs orelse error "dist_vars"; []) | dist_vars (T::Ts) vs = case find_index (fn v => fastype_of v = T) vs of ~1 => Free ("", T) :: dist_vars Ts vs diff -r 535ae9dd4c45 -r 1565d476a9e2 src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Tue Apr 03 19:24:10 2007 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Tue Apr 03 19:24:11 2007 +0200 @@ -93,24 +93,24 @@ val fname = fst (dest_Free head) handle TERM _ => error (input_error invalid_head_msg) - val _ = assert (fname mem fnames) (input_error invalid_head_msg) + val _ = fname mem fnames orelse error (input_error invalid_head_msg) fun add_bvs t is = add_loose_bnos (t, 0, is) val rvs = (add_bvs rhs [] \\ fold add_bvs args []) |> map (fst o nth (rev qs)) - val _ = assert (null rvs) (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs + val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")) - val _ = assert (forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs) - (input_error "Recursive Calls not allowed in premises") + val _ = forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs orelse + error (input_error "Recursive Calls not allowed in premises") val k = length args val arities' = case Symtab.lookup arities fname of NONE => Symtab.update (fname, k) arities - | SOME i => (assert (i = k) - (input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")); + | SOME i => (i = k orelse + error (input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")); arities) in ((fname, qs, gs, args, rhs), arities') diff -r 535ae9dd4c45 -r 1565d476a9e2 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Tue Apr 03 19:24:10 2007 +0200 +++ b/src/HOL/Tools/refute.ML Tue Apr 03 19:24:11 2007 +0200 @@ -14,67 +14,67 @@ signature REFUTE = sig - exception REFUTE of string * string + exception REFUTE of string * string (* ------------------------------------------------------------------------- *) (* Model/interpretation related code (translation HOL -> propositional logic *) (* ------------------------------------------------------------------------- *) - type params - type interpretation - type model - type arguments + type params + type interpretation + type model + type arguments - exception MAXVARS_EXCEEDED + exception MAXVARS_EXCEEDED - val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option) -> theory -> theory - val add_printer : string -> (theory -> model -> Term.term -> - interpretation -> (int -> bool) -> Term.term option) -> theory -> theory + val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option) -> theory -> theory + val add_printer : string -> (theory -> model -> Term.term -> + interpretation -> (int -> bool) -> Term.term option) -> theory -> theory - val interpret : theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) + val interpret : theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) - val print : theory -> model -> Term.term -> interpretation -> - (int -> bool) -> Term.term - val print_model : theory -> model -> (int -> bool) -> string + val print : theory -> model -> Term.term -> interpretation -> + (int -> bool) -> Term.term + val print_model : theory -> model -> (int -> bool) -> string (* ------------------------------------------------------------------------- *) (* Interface *) (* ------------------------------------------------------------------------- *) - val set_default_param : (string * string) -> theory -> theory - val get_default_param : theory -> string -> string option - val get_default_params : theory -> (string * string) list - val actual_params : theory -> (string * string) list -> params + val set_default_param : (string * string) -> theory -> theory + val get_default_param : theory -> string -> string option + val get_default_params : theory -> (string * string) list + val actual_params : theory -> (string * string) list -> params - val find_model : theory -> params -> Term.term -> bool -> unit + val find_model : theory -> params -> Term.term -> bool -> unit - (* tries to find a model for a formula: *) - val satisfy_term : theory -> (string * string) list -> Term.term -> unit - (* tries to find a model that refutes a formula: *) - val refute_term : theory -> (string * string) list -> Term.term -> unit - val refute_subgoal : - theory -> (string * string) list -> Thm.thm -> int -> unit + (* tries to find a model for a formula: *) + val satisfy_term : theory -> (string * string) list -> Term.term -> unit + (* tries to find a model that refutes a formula: *) + val refute_term : theory -> (string * string) list -> Term.term -> unit + val refute_subgoal : + theory -> (string * string) list -> Thm.thm -> int -> unit - val setup : theory -> theory + val setup : theory -> theory end; (* signature REFUTE *) 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 *) @@ -85,43 +85,43 @@ (* 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 = - let - fun itl (e, Leaf x) = f(e,x) - | itl (e, Node xs) = Library.foldl (tree_foldl f) (e,xs) - in - itl - end; + fun tree_foldl f = + let + fun itl (e, Leaf x) = f(e,x) + | itl (e, Node xs) = Library.foldl (tree_foldl f) (e,xs) + in + 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 => - (case t2 of - Leaf y => Leaf (x,y) - | Node _ => raise REFUTE ("tree_pair", - "trees are of different height (second tree is higher)")) - | Node xs => - (case t2 of - (* '~~' will raise an exception if the number of branches in *) - (* both trees is different at the current node *) - Node ys => Node (map tree_pair (xs ~~ ys)) - | Leaf _ => raise REFUTE ("tree_pair", - "trees are of different height (first tree is higher)")); + 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 => + (case t2 of + (* '~~' will raise an exception if the number of branches in *) + (* both trees is different at the current node *) + Node ys => Node (map tree_pair (xs ~~ ys)) + | Leaf _ => raise REFUTE ("tree_pair", + "trees are of different height (first tree is higher)")); (* ------------------------------------------------------------------------- *) (* params: parameters that control the translation into a propositional *) @@ -143,76 +143,76 @@ (* "satsolver" string SAT solver to be used. *) (* ------------------------------------------------------------------------- *) - type params = - { - sizes : (string * int) list, - minsize : int, - maxsize : int, - maxvars : int, - maxtime : int, - satsolver: string - }; + type params = + { + sizes : (string * int) list, + minsize : int, + maxsize : int, + maxvars : int, + maxtime : int, + satsolver: string + }; (* ------------------------------------------------------------------------- *) (* interpretation: a term's interpretation is given by a variable of type *) (* 'interpretation' *) (* ------------------------------------------------------------------------- *) - 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 = - (Term.typ * int) list * (Term.term * interpretation) list; + type model = + (Term.typ * int) list * (Term.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 RefuteDataArgs = - struct - val name = "HOL/refute"; - type T = - {interpreters: (string * (theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option)) list, - printers: (string * (theory -> model -> Term.term -> interpretation -> - (int -> bool) -> Term.term option)) list, - parameters: string Symtab.table}; - val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; - val copy = I; - val extend = I; - fun merge _ - ({interpreters = in1, printers = pr1, parameters = pa1}, - {interpreters = in2, printers = pr2, parameters = pa2}) = - {interpreters = AList.merge (op =) (K true) (in1, in2), - printers = AList.merge (op =) (K true) (pr1, pr2), - parameters = Symtab.merge (op=) (pa1, pa2)}; - fun print sg {interpreters, printers, parameters} = - Pretty.writeln (Pretty.chunks - [Pretty.strs ("default parameters:" :: List.concat (map - (fn (name, value) => [name, "=", value]) (Symtab.dest parameters))), - Pretty.strs ("interpreters:" :: map fst interpreters), - Pretty.strs ("printers:" :: map fst printers)]); - end; + structure RefuteDataArgs = + struct + val name = "HOL/refute"; + type T = + {interpreters: (string * (theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option)) list, + printers: (string * (theory -> model -> Term.term -> interpretation -> + (int -> bool) -> Term.term option)) list, + parameters: string Symtab.table}; + val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; + val copy = I; + val extend = I; + fun merge _ + ({interpreters = in1, printers = pr1, parameters = pa1}, + {interpreters = in2, printers = pr2, parameters = pa2}) = + {interpreters = AList.merge (op =) (K true) (in1, in2), + printers = AList.merge (op =) (K true) (pr1, pr2), + parameters = Symtab.merge (op=) (pa1, pa2)}; + fun print sg {interpreters, printers, parameters} = + Pretty.writeln (Pretty.chunks + [Pretty.strs ("default parameters:" :: List.concat (map + (fn (name, value) => [name, "=", value]) (Symtab.dest parameters))), + Pretty.strs ("interpreters:" :: map fst interpreters), + Pretty.strs ("printers:" :: map fst printers)]); + end; - structure RefuteData = TheoryDataFun(RefuteDataArgs); + structure RefuteData = TheoryDataFun(RefuteDataArgs); (* ------------------------------------------------------------------------- *) @@ -221,30 +221,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) - (#interpreters (RefuteData.get thy)) of - NONE => raise REFUTE ("interpret", - "no interpreter for term " ^ quote (Sign.string_of_term thy t)) - | SOME x => x; + 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 (Sign.string_of_term thy t)) + | SOME x => x; (* ------------------------------------------------------------------------- *) (* print: converts the constant denoted by the term 't' into a term using a *) (* suitable printer *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> - Term.term *) + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> + Term.term *) - fun print thy model t intr assignment = - case get_first (fn (_, f) => f thy model t intr assignment) - (#printers (RefuteData.get thy)) of - NONE => raise REFUTE ("print", - "no printer for term " ^ quote (Sign.string_of_term thy t)) - | SOME x => x; + 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 term " ^ quote (Sign.string_of_term thy t)) + | SOME x => x; (* ------------------------------------------------------------------------- *) (* print_model: turns the model into a string, using a fixed interpretation *) @@ -252,105 +252,105 @@ (* printers *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> (int -> bool) -> string *) + (* theory -> model -> (int -> bool) -> string *) - fun print_model thy model assignment = - let - val (typs, terms) = model - val typs_msg = - if null typs then - "empty universe (no type variables in term)\n" - else - "Size of types: " ^ commas (map (fn (T, i) => - Sign.string_of_typ thy T ^ ": " ^ string_of_int i) typs) ^ "\n" - val show_consts_msg = - if not (!show_consts) andalso Library.exists (is_Const o fst) terms then - "set \"show_consts\" to show the interpretation of constants\n" - else - "" - val terms_msg = - if null terms then - "empty interpretation (no free variables in term)\n" - else - space_implode "\n" (List.mapPartial (fn (t, intr) => - (* print constants only if 'show_consts' is true *) - if (!show_consts) orelse not (is_Const t) then - SOME (Sign.string_of_term thy t ^ ": " ^ - Sign.string_of_term thy (print thy model t intr assignment)) - else - NONE) terms) ^ "\n" - in - typs_msg ^ show_consts_msg ^ terms_msg - end; + fun print_model thy model assignment = + let + val (typs, terms) = model + val typs_msg = + if null typs then + "empty universe (no type variables in term)\n" + else + "Size of types: " ^ commas (map (fn (T, i) => + Sign.string_of_typ thy T ^ ": " ^ string_of_int i) typs) ^ "\n" + val show_consts_msg = + if not (!show_consts) andalso Library.exists (is_Const o fst) terms then + "set \"show_consts\" to show the interpretation of constants\n" + else + "" + val terms_msg = + if null terms then + "empty interpretation (no free variables in term)\n" + else + space_implode "\n" (List.mapPartial (fn (t, intr) => + (* print constants only if 'show_consts' is true *) + if (!show_consts) orelse not (is_Const t) then + SOME (Sign.string_of_term thy t ^ ": " ^ + Sign.string_of_term thy (print thy model t intr assignment)) + else + NONE) terms) ^ "\n" + in + typs_msg ^ show_consts_msg ^ terms_msg + end; (* ------------------------------------------------------------------------- *) (* 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 = - 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 - | SOME _ => error ("Interpreter " ^ name ^ " already declared") - end; + 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 + | SOME _ => error ("Interpreter " ^ name ^ " already declared") + end; - (* string -> (theory -> model -> Term.term -> interpretation -> - (int -> bool) -> Term.term option) -> theory -> theory *) + (* string -> (theory -> model -> Term.term -> interpretation -> + (int -> bool) -> Term.term option) -> theory -> theory *) - 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 - | SOME _ => error ("Printer " ^ name ^ " already declared") - end; + 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 + | SOME _ => error ("Printer " ^ name ^ " already declared") + end; (* ------------------------------------------------------------------------- *) (* set_default_param: stores the '(name, value)' pair in RefuteData's *) (* parameter table *) (* ------------------------------------------------------------------------- *) - (* (string * string) -> theory -> theory *) + (* (string * string) -> theory -> theory *) - fun set_default_param (name, value) thy = - let - val {interpreters, printers, parameters} = RefuteData.get thy - in - RefuteData.put (case Symtab.lookup parameters name of - NONE => - {interpreters = interpreters, printers = printers, - parameters = Symtab.extend (parameters, [(name, value)])} - | SOME _ => - {interpreters = interpreters, printers = printers, - parameters = Symtab.update (name, value) parameters}) thy - end; + fun set_default_param (name, value) thy = + let + val {interpreters, printers, parameters} = RefuteData.get thy + in + RefuteData.put (case Symtab.lookup parameters name of + NONE => + {interpreters = interpreters, printers = printers, + parameters = Symtab.extend (parameters, [(name, value)])} + | SOME _ => + {interpreters = interpreters, printers = printers, + parameters = Symtab.update (name, value) parameters}) thy + end; (* ------------------------------------------------------------------------- *) (* 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 *) @@ -358,59 +358,59 @@ (* 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 = - let - (* (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 ^ - " 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 ^ - " 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") - (* string *) - val satsolver = read_string (allparams, "satsolver") - (* all remaining parameters of the form "string=int" are collected in *) - (* 'sizes' *) - (* TODO: it is currently not possible to specify a size for a type *) - (* whose name is one of the other parameters (e.g. 'maxvars') *) - (* (string * int) list *) - val sizes = List.mapPartial - (fn (name, value) => Option.map (pair name) (Int.fromString value)) - (List.filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize" - andalso name<>"maxvars" andalso name<>"maxtime" - andalso name<>"satsolver") allparams) - in - {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars, - maxtime=maxtime, satsolver=satsolver} - end; + fun actual_params thy override = + let + (* (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 ^ + " 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 ^ + " 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") + (* string *) + val satsolver = read_string (allparams, "satsolver") + (* all remaining parameters of the form "string=int" are collected in *) + (* 'sizes' *) + (* TODO: it is currently not possible to specify a size for a type *) + (* whose name is one of the other parameters (e.g. 'maxvars') *) + (* (string * int) list *) + val sizes = List.mapPartial + (fn (name, value) => Option.map (pair name) (Int.fromString value)) + (List.filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize" + andalso name<>"maxvars" andalso name<>"maxtime" + andalso name<>"satsolver") allparams) + in + {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars, + maxtime=maxtime, satsolver=satsolver} + end; (* ------------------------------------------------------------------------- *) (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) (* ------------------------------------------------------------------------- *) - (* (''a * 'b) list -> ''a -> 'b *) + (* (''a * 'b) list -> ''a -> 'b *) - fun lookup xs key = - Option.valOf (AList.lookup (op =) xs key); + fun lookup xs key = + Option.valOf (AList.lookup (op =) xs key); (* ------------------------------------------------------------------------- *) (* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type *) @@ -418,55 +418,55 @@ (* arguments *) (* ------------------------------------------------------------------------- *) - (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> - DatatypeAux.dtyp -> Term.typ *) + (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> + DatatypeAux.dtyp -> Term.typ *) - fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) = - (* replace a 'DtTFree' variable by the associated type *) - lookup typ_assoc (DatatypeAux.DtTFree a) - | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) = - Type (s, map (typ_of_dtyp descr typ_assoc) ds) - | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) = - let - val (s, ds, _) = lookup descr i - in - Type (s, map (typ_of_dtyp descr typ_assoc) ds) - end; + fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) = + (* replace a 'DtTFree' variable by the associated type *) + lookup typ_assoc (DatatypeAux.DtTFree a) + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) = + Type (s, map (typ_of_dtyp descr typ_assoc) ds) + | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) = + let + val (s, ds, _) = lookup 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 = - let - (* (Term.indexname * Term.typ) list *) - val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t)) - in - Library.foldl (fn (t', ((x, i), T)) => - (Term.all T) $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) - (t, vars) - end; + fun close_form t = + let + (* (Term.indexname * Term.typ) list *) + val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t)) + in + Library.foldl (fn (t', ((x, i), T)) => + (Term.all T) $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) + (t, vars) + end; (* ------------------------------------------------------------------------- *) (* monomorphic_term: applies a type substitution 'typeSubs' for all type *) (* variables in a term 't' *) (* ------------------------------------------------------------------------- *) - (* Type.tyenv -> Term.term -> Term.term *) + (* Type.tyenv -> Term.term -> Term.term *) - fun monomorphic_term typeSubs t = - map_types (map_type_tvar - (fn v => - case Type.lookup (typeSubs, v) of - NONE => - (* schematic type variable not instantiated *) - raise REFUTE ("monomorphic_term", - "no substitution for type variable " ^ fst (fst v) ^ - " in term " ^ Display.raw_string_of_term t) - | SOME typ => - typ)) t; + fun monomorphic_term typeSubs t = + map_types (map_type_tvar + (fn v => + case Type.lookup (typeSubs, v) of + NONE => + (* schematic type variable not instantiated *) + raise REFUTE ("monomorphic_term", + "no substitution for type variable " ^ fst (fst v) ^ + " in term " ^ Display.raw_string_of_term t) + | SOME typ => + typ)) t; (* ------------------------------------------------------------------------- *) (* specialize_type: given a constant 's' of type 'T', which is a subterm of *) @@ -475,186 +475,186 @@ (* match the type 'T' (may raise Type.TYPE_MATCH) *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * Term.typ) -> Term.term -> Term.term *) + (* theory -> (string * Term.typ) -> Term.term -> Term.term *) - fun specialize_type thy (s, T) t = - let - fun find_typeSubs (Const (s', T')) = - if s=s' then - SOME (Sign.typ_match thy (T', T) Vartab.empty) - handle Type.TYPE_MATCH => NONE - else - NONE - | find_typeSubs (Free _) = NONE - | find_typeSubs (Var _) = NONE - | find_typeSubs (Bound _) = NONE - | find_typeSubs (Abs (_, _, body)) = find_typeSubs body - | find_typeSubs (t1 $ t2) = - (case find_typeSubs t1 of SOME x => SOME x - | NONE => find_typeSubs t2) - in - case find_typeSubs t of - SOME typeSubs => - monomorphic_term typeSubs t - | NONE => - (* no match found - perhaps due to sort constraints *) - raise Type.TYPE_MATCH - end; + fun specialize_type thy (s, T) t = + let + fun find_typeSubs (Const (s', T')) = + if s=s' then + SOME (Sign.typ_match thy (T', T) Vartab.empty) + handle Type.TYPE_MATCH => NONE + else + NONE + | find_typeSubs (Free _) = NONE + | find_typeSubs (Var _) = NONE + | find_typeSubs (Bound _) = NONE + | find_typeSubs (Abs (_, _, body)) = find_typeSubs body + | find_typeSubs (t1 $ t2) = + (case find_typeSubs t1 of SOME x => SOME x + | NONE => find_typeSubs t2) + in + case find_typeSubs t of + SOME typeSubs => + monomorphic_term typeSubs t + | NONE => + (* no match found - perhaps due to sort constraints *) + raise Type.TYPE_MATCH + end; (* ------------------------------------------------------------------------- *) (* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that *) (* 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) = - let - val class_const_names = map Logic.const_of_class (Sign.all_classes thy) - in - (* I'm not quite sure if checking the name 's' is sufficient, *) - (* or if we should also check the type 'T'. *) - s mem_string class_const_names - end; + fun is_const_of_class thy (s, T) = + let + val class_const_names = map Logic.const_of_class (Sign.all_classes thy) + in + (* I'm not quite sure if checking the name 's' is sufficient, *) + (* or if we should also check the type 'T'. *) + s mem_string class_const_names + end; (* ------------------------------------------------------------------------- *) (* is_IDT_constructor: returns 'true' iff 'Const (s, T)' is the constructor *) (* 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', _) => - (case DatatypePackage.get_datatype_constrs thy s' of - SOME constrs => - List.exists (fn (cname, cty) => - cname = s andalso Sign.typ_instance thy (T, cty)) constrs - | NONE => - false) - | _ => - false); + fun is_IDT_constructor thy (s, T) = + (case body_type T of + Type (s', _) => + (case DatatypePackage.get_datatype_constrs thy s' of + SOME constrs => + 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) = - let - val rec_names = Symtab.fold (append o #rec_names o snd) - (DatatypePackage.get_datatypes thy) [] - in - (* I'm not quite sure if checking the name 's' is sufficient, *) - (* or if we should also check the type 'T'. *) - s mem_string rec_names - end; + fun is_IDT_recursor thy (s, T) = + let + val rec_names = Symtab.fold (append o #rec_names o snd) + (DatatypePackage.get_datatypes thy) [] + in + (* I'm not quite sure if checking the name 's' is sufficient, *) + (* or if we should also check the type 'T'. *) + s mem_string rec_names + end; (* ------------------------------------------------------------------------- *) (* get_def: looks up the definition of a constant, as created by "constdefs" *) (* ------------------------------------------------------------------------- *) - (* theory -> string * Term.typ -> (string * Term.term) option *) + (* theory -> string * Term.typ -> (string * Term.term) option *) - fun get_def thy (s, T) = - let - (* maps f ?t1 ... ?tn == rhs to %t1...tn. rhs *) - 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]) - val (lhs, rhs) = Logic.dest_equals eqn - val (_, args) = Term.strip_comb lhs - in - fold lambda (rev args) rhs - end - (* (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' - 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; + fun get_def thy (s, T) = + let + (* maps f ?t1 ... ?tn == rhs to %t1...tn. rhs *) + 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]) + val (lhs, rhs) = Logic.dest_equals eqn + val (_, args) = Term.strip_comb lhs + in + fold lambda (rev args) rhs + end + (* (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' + 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; (* ------------------------------------------------------------------------- *) (* get_typedef: looks up the definition of a type, as created by "typedef" *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * Term.typ) -> (string * Term.term) option *) + (* theory -> (string * Term.typ) -> (string * Term.term) option *) - 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'="Typedef.type_definition" then - SOME T' - else - NONE - | type_of_type_definition (Free _) = NONE - | type_of_type_definition (Var _) = NONE - | type_of_type_definition (Bound _) = NONE - | type_of_type_definition (Abs (_, _, body)) = - type_of_type_definition body - | type_of_type_definition (t1 $ t2) = - (case type_of_type_definition t1 of - SOME x => SOME x - | NONE => type_of_type_definition t2) - in - case type_of_type_definition ax of - SOME T' => - let - val T'' = (domain_type o domain_type) T' - val typeSubs = 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 - | MATCH => get_typedef_ax axioms - | Type.TYPE_MATCH => get_typedef_ax axioms) - in - get_typedef_ax (Theory.all_axioms_of thy) - end; + 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'="Typedef.type_definition" then + SOME T' + else + NONE + | type_of_type_definition (Free _) = NONE + | type_of_type_definition (Var _) = NONE + | type_of_type_definition (Bound _) = NONE + | type_of_type_definition (Abs (_, _, body)) = + type_of_type_definition body + | type_of_type_definition (t1 $ t2) = + (case type_of_type_definition t1 of + SOME x => SOME x + | NONE => type_of_type_definition t2) + in + case type_of_type_definition ax of + SOME T' => + let + val T'' = (domain_type o domain_type) T' + val typeSubs = 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 + | MATCH => get_typedef_ax axioms + | Type.TYPE_MATCH => get_typedef_ax axioms) + in + get_typedef_ax (Theory.all_axioms_of thy) + end; (* ------------------------------------------------------------------------- *) (* get_classdef: looks up the defining axiom for an axiomatic type class, as *) (* created by the "axclass" command *) (* ------------------------------------------------------------------------- *) - (* theory -> string -> (string * Term.term) option *) + (* theory -> string -> (string * Term.term) option *) - fun get_classdef thy class = - let - val axname = class ^ "_class_def" - in - Option.map (pair axname) - (AList.lookup (op =) (Theory.all_axioms_of thy) axname) - end; + fun get_classdef thy class = + let + val axname = class ^ "_class_def" + in + Option.map (pair axname) + (AList.lookup (op =) (Theory.all_axioms_of thy) axname) + end; (* ------------------------------------------------------------------------- *) (* unfold_defs: unfolds all defined constants in a term 't', beta-eta *) @@ -664,293 +664,293 @@ (* 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 = - let - (* Term.term -> Term.term *) - fun unfold_loop t = - case t of - (* Pure *) - Const ("all", _) => t - | Const ("==", _) => t - | Const ("==>", _) => t - | Const ("TYPE", _) => t (* axiomatic type classes *) - (* HOL *) - | Const ("Trueprop", _) => t - | Const ("Not", _) => t - | (* redundant, since 'True' is also an IDT constructor *) - Const ("True", _) => t - | (* redundant, since 'False' is also an IDT constructor *) - Const ("False", _) => t - | Const ("arbitrary", _) => t - | Const ("The", _) => t - | Const ("Hilbert_Choice.Eps", _) => t - | Const ("All", _) => t - | Const ("Ex", _) => t - | Const ("op =", _) => t - | Const ("op &", _) => t - | Const ("op |", _) => t - | Const ("op -->", _) => t - (* sets *) - | Const ("Collect", _) => t - | Const ("op :", _) => t - (* other optimizations *) - | Const ("Finite_Set.card", _) => t - | Const ("Finite_Set.Finites", _) => t - | Const ("Finite_Set.finite", _) => t - | Const ("Orderings.less", Type ("fun", [Type ("nat", []), - Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t - | Const ("HOL.plus", Type ("fun", [Type ("nat", []), - Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t - | Const ("HOL.minus", Type ("fun", [Type ("nat", []), - Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t - | Const ("HOL.times", Type ("fun", [Type ("nat", []), - Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t - | Const ("List.op @", _) => t - | Const ("Lfp.lfp", _) => t - | Const ("Gfp.gfp", _) => t - | Const ("fst", _) => t - | Const ("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. *) - ((*immediate_output (" 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) - val result = Envir.beta_eta_contract (unfold_loop t) - in - result - end; + fun unfold_defs thy t = + let + (* Term.term -> Term.term *) + fun unfold_loop t = + case t of + (* Pure *) + Const ("all", _) => t + | Const ("==", _) => t + | Const ("==>", _) => t + | Const ("TYPE", _) => t (* axiomatic type classes *) + (* HOL *) + | Const ("Trueprop", _) => t + | Const ("Not", _) => t + | (* redundant, since 'True' is also an IDT constructor *) + Const ("True", _) => t + | (* redundant, since 'False' is also an IDT constructor *) + Const ("False", _) => t + | Const ("arbitrary", _) => t + | Const ("The", _) => t + | Const ("Hilbert_Choice.Eps", _) => t + | Const ("All", _) => t + | Const ("Ex", _) => t + | Const ("op =", _) => t + | Const ("op &", _) => t + | Const ("op |", _) => t + | Const ("op -->", _) => t + (* sets *) + | Const ("Collect", _) => t + | Const ("op :", _) => t + (* other optimizations *) + | Const ("Finite_Set.card", _) => t + | Const ("Finite_Set.Finites", _) => t + | Const ("Finite_Set.finite", _) => t + | Const ("Orderings.less", Type ("fun", [Type ("nat", []), + Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t + | Const ("HOL.plus", Type ("fun", [Type ("nat", []), + Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t + | Const ("HOL.minus", Type ("fun", [Type ("nat", []), + Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t + | Const ("HOL.times", Type ("fun", [Type ("nat", []), + Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t + | Const ("List.op @", _) => t + | Const ("Lfp.lfp", _) => t + | Const ("Gfp.gfp", _) => t + | Const ("fst", _) => t + | Const ("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. *) + ((*immediate_output (" 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) + val result = Envir.beta_eta_contract (unfold_loop t) + in + result + end; (* ------------------------------------------------------------------------- *) (* collect_axioms: collects (monomorphic, universally quantified, unfolded *) (* 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", "constdefs". 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", "constdefs". 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 = - let - val _ = immediate_output "Adding axioms..." - (* (string * Term.term) list *) - val axioms = Theory.all_axioms_of thy - (* string * Term.term -> Term.term list -> Term.term list *) - fun collect_this_axiom (axname, ax) axs = - let - val ax' = unfold_defs thy ax - in - if member (op aconv) axs ax' then - axs - else ( - immediate_output (" " ^ axname); - collect_term_axioms (ax' :: axs, ax') - ) - end - (* Term.term list * Term.typ -> Term.term list *) - and collect_sort_axioms (axs, T) = - let - (* string list *) - val sort = (case T of - TFree (_, sort) => sort - | TVar (_, sort) => sort - | _ => raise REFUTE ("collect_axioms", "type " ^ - Sign.string_of_typ thy T ^ " is not a variable")) - (* obtain axioms for all superclasses *) - val superclasses = sort @ (maps (Sign.super_classes thy) sort) - (* merely an optimization, because 'collect_this_axiom' disallows *) - (* duplicate axioms anyway: *) - val superclasses = distinct (op =) superclasses - val class_axioms = maps (fn class => map (fn ax => - ("<" ^ class ^ ">", Thm.prop_of ax)) - (#axioms (AxClass.get_definition thy class) handle ERROR _ => [])) - superclasses - (* replace the (at most one) schematic type variable in each axiom *) - (* by the actual type 'T' *) - val monomorphic_class_axioms = map (fn (axname, ax) => - (case Term.term_tvars ax of - [] => - (axname, ax) - | [(idx, S)] => - (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) - | _ => - raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ - Sign.string_of_term thy ax ^ - ") contains more than one type variable"))) - class_axioms - in - fold collect_this_axiom monomorphic_class_axioms axs - end - (* Term.term list * Term.typ -> Term.term list *) - and collect_type_axioms (axs, T) = - case T of - (* simple types *) - Type ("prop", []) => axs - | Type ("fun", [T1, T2]) => collect_type_axioms - (collect_type_axioms (axs, T1), T2) - | Type ("set", [T1]) => collect_type_axioms (axs, T1) - (* axiomatic type classes *) - | Type ("itself", [T1]) => collect_type_axioms (axs, T1) - | Type (s, Ts) => - (case DatatypePackage.get_datatype thy s of - SOME info => (* inductive datatype *) - (* only collect relevant type axioms for the argument types *) - Library.foldl collect_type_axioms (axs, Ts) - | NONE => - (case get_typedef thy T of - SOME (axname, ax) => - collect_this_axiom (axname, ax) axs - | NONE => - (* unspecified type, perhaps introduced with "typedecl" *) - (* at least collect relevant type axioms for the argument types *) - Library.foldl collect_type_axioms (axs, Ts))) - (* axiomatic type classes *) - | TFree _ => collect_sort_axioms (axs, T) - (* axiomatic type classes *) - | TVar _ => collect_sort_axioms (axs, T) - (* Term.term list * Term.term -> Term.term list *) - and collect_term_axioms (axs, t) = - case t of - (* Pure *) - Const ("all", _) => axs - | Const ("==", _) => axs - | Const ("==>", _) => axs - (* axiomatic type classes *) - | Const ("TYPE", T) => collect_type_axioms (axs, T) - (* HOL *) - | Const ("Trueprop", _) => axs - | Const ("Not", _) => axs - (* redundant, since 'True' is also an IDT constructor *) - | Const ("True", _) => axs - (* redundant, since 'False' is also an IDT constructor *) - | Const ("False", _) => axs - | Const ("arbitrary", T) => collect_type_axioms (axs, T) - | Const ("The", T) => - let - val ax = specialize_type thy ("The", T) - (lookup axioms "HOL.the_eq_trivial") - in - collect_this_axiom ("HOL.the_eq_trivial", ax) axs - end - | Const ("Hilbert_Choice.Eps", T) => - let - val ax = specialize_type thy ("Hilbert_Choice.Eps", T) - (lookup axioms "Hilbert_Choice.someI") - in - collect_this_axiom ("Hilbert_Choice.someI", ax) axs - end - | Const ("All", T) => collect_type_axioms (axs, T) - | Const ("Ex", T) => collect_type_axioms (axs, T) - | Const ("op =", T) => collect_type_axioms (axs, T) - | Const ("op &", _) => axs - | Const ("op |", _) => axs - | Const ("op -->", _) => axs - (* sets *) - | Const ("Collect", T) => collect_type_axioms (axs, T) - | Const ("op :", T) => collect_type_axioms (axs, T) - (* other optimizations *) - | Const ("Finite_Set.card", T) => collect_type_axioms (axs, T) - | Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T) - | Const ("Finite_Set.finite", T) => collect_type_axioms (axs, T) - | Const ("Orderings.less", T as Type ("fun", [Type ("nat", []), - Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => - collect_type_axioms (axs, T) - | Const ("HOL.plus", T as Type ("fun", [Type ("nat", []), - Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => - collect_type_axioms (axs, T) - | Const ("HOL.minus", T as Type ("fun", [Type ("nat", []), - Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => - collect_type_axioms (axs, T) - | Const ("HOL.times", T as Type ("fun", [Type ("nat", []), - Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => - collect_type_axioms (axs, T) - | Const ("List.op @", T) => collect_type_axioms (axs, T) - | Const ("Lfp.lfp", T) => collect_type_axioms (axs, T) - | Const ("Gfp.gfp", T) => collect_type_axioms (axs, T) - | Const ("fst", T) => collect_type_axioms (axs, T) - | Const ("snd", T) => collect_type_axioms (axs, T) - (* simply-typed lambda calculus *) - | Const (s, T) => - if is_const_of_class thy (s, T) then - (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *) - (* and the class definition *) - let - val class = Logic.class_of_const s - val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class) - val ax_in = SOME (specialize_type thy (s, T) inclass) - (* type match may fail due to sort constraints *) - handle Type.TYPE_MATCH => NONE - val ax_1 = Option.map (fn ax => (Sign.string_of_term thy ax, ax)) - ax_in - val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) - (get_classdef thy class) - in - collect_type_axioms (fold collect_this_axiom - (map_filter I [ax_1, ax_2]) axs, T) - end - else if is_IDT_constructor thy (s, T) - orelse is_IDT_recursor thy (s, T) then - (* only collect relevant type axioms *) - collect_type_axioms (axs, T) - else - (* other constants should have been unfolded, with some *) - (* exceptions: e.g. Abs_xxx/Rep_xxx functions for *) - (* typedefs, or type-class related constants *) - (* only collect relevant type axioms *) - collect_type_axioms (axs, T) - | Free (_, T) => collect_type_axioms (axs, T) - | Var (_, T) => collect_type_axioms (axs, T) - | Bound i => axs - | Abs (_, T, body) => collect_term_axioms - (collect_type_axioms (axs, T), body) - | t1 $ t2 => collect_term_axioms - (collect_term_axioms (axs, t1), t2) - (* Term.term list *) - val result = map close_form (collect_term_axioms ([], t)) - val _ = writeln " ...done." - in - result - end; + fun collect_axioms thy t = + let + val _ = immediate_output "Adding axioms..." + (* (string * Term.term) list *) + val axioms = Theory.all_axioms_of thy + (* string * Term.term -> Term.term list -> Term.term list *) + fun collect_this_axiom (axname, ax) axs = + let + val ax' = unfold_defs thy ax + in + if member (op aconv) axs ax' then + axs + else ( + immediate_output (" " ^ axname); + collect_term_axioms (ax' :: axs, ax') + ) + end + (* Term.term list * Term.typ -> Term.term list *) + and collect_sort_axioms (axs, T) = + let + (* string list *) + val sort = (case T of + TFree (_, sort) => sort + | TVar (_, sort) => sort + | _ => raise REFUTE ("collect_axioms", "type " ^ + Sign.string_of_typ thy T ^ " is not a variable")) + (* obtain axioms for all superclasses *) + val superclasses = sort @ (maps (Sign.super_classes thy) sort) + (* merely an optimization, because 'collect_this_axiom' disallows *) + (* duplicate axioms anyway: *) + val superclasses = distinct (op =) superclasses + val class_axioms = maps (fn class => map (fn ax => + ("<" ^ class ^ ">", Thm.prop_of ax)) + (#axioms (AxClass.get_definition thy class) handle ERROR _ => [])) + superclasses + (* replace the (at most one) schematic type variable in each axiom *) + (* by the actual type 'T' *) + val monomorphic_class_axioms = map (fn (axname, ax) => + (case Term.term_tvars ax of + [] => + (axname, ax) + | [(idx, S)] => + (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) + | _ => + raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ + Sign.string_of_term thy ax ^ + ") contains more than one type variable"))) + class_axioms + in + fold collect_this_axiom monomorphic_class_axioms axs + end + (* Term.term list * Term.typ -> Term.term list *) + and collect_type_axioms (axs, T) = + case T of + (* simple types *) + Type ("prop", []) => axs + | Type ("fun", [T1, T2]) => collect_type_axioms + (collect_type_axioms (axs, T1), T2) + | Type ("set", [T1]) => collect_type_axioms (axs, T1) + (* axiomatic type classes *) + | Type ("itself", [T1]) => collect_type_axioms (axs, T1) + | Type (s, Ts) => + (case DatatypePackage.get_datatype thy s of + SOME info => (* inductive datatype *) + (* only collect relevant type axioms for the argument types *) + Library.foldl collect_type_axioms (axs, Ts) + | NONE => + (case get_typedef thy T of + SOME (axname, ax) => + collect_this_axiom (axname, ax) axs + | NONE => + (* unspecified type, perhaps introduced with "typedecl" *) + (* at least collect relevant type axioms for the argument types *) + Library.foldl collect_type_axioms (axs, Ts))) + (* axiomatic type classes *) + | TFree _ => collect_sort_axioms (axs, T) + (* axiomatic type classes *) + | TVar _ => collect_sort_axioms (axs, T) + (* Term.term list * Term.term -> Term.term list *) + and collect_term_axioms (axs, t) = + case t of + (* Pure *) + Const ("all", _) => axs + | Const ("==", _) => axs + | Const ("==>", _) => axs + (* axiomatic type classes *) + | Const ("TYPE", T) => collect_type_axioms (axs, T) + (* HOL *) + | Const ("Trueprop", _) => axs + | Const ("Not", _) => axs + (* redundant, since 'True' is also an IDT constructor *) + | Const ("True", _) => axs + (* redundant, since 'False' is also an IDT constructor *) + | Const ("False", _) => axs + | Const ("arbitrary", T) => collect_type_axioms (axs, T) + | Const ("The", T) => + let + val ax = specialize_type thy ("The", T) + (lookup axioms "HOL.the_eq_trivial") + in + collect_this_axiom ("HOL.the_eq_trivial", ax) axs + end + | Const ("Hilbert_Choice.Eps", T) => + let + val ax = specialize_type thy ("Hilbert_Choice.Eps", T) + (lookup axioms "Hilbert_Choice.someI") + in + collect_this_axiom ("Hilbert_Choice.someI", ax) axs + end + | Const ("All", T) => collect_type_axioms (axs, T) + | Const ("Ex", T) => collect_type_axioms (axs, T) + | Const ("op =", T) => collect_type_axioms (axs, T) + | Const ("op &", _) => axs + | Const ("op |", _) => axs + | Const ("op -->", _) => axs + (* sets *) + | Const ("Collect", T) => collect_type_axioms (axs, T) + | Const ("op :", T) => collect_type_axioms (axs, T) + (* other optimizations *) + | Const ("Finite_Set.card", T) => collect_type_axioms (axs, T) + | Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T) + | Const ("Finite_Set.finite", T) => collect_type_axioms (axs, T) + | Const ("Orderings.less", T as Type ("fun", [Type ("nat", []), + Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => + collect_type_axioms (axs, T) + | Const ("HOL.plus", T as Type ("fun", [Type ("nat", []), + Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => + collect_type_axioms (axs, T) + | Const ("HOL.minus", T as Type ("fun", [Type ("nat", []), + Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => + collect_type_axioms (axs, T) + | Const ("HOL.times", T as Type ("fun", [Type ("nat", []), + Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => + collect_type_axioms (axs, T) + | Const ("List.op @", T) => collect_type_axioms (axs, T) + | Const ("Lfp.lfp", T) => collect_type_axioms (axs, T) + | Const ("Gfp.gfp", T) => collect_type_axioms (axs, T) + | Const ("fst", T) => collect_type_axioms (axs, T) + | Const ("snd", T) => collect_type_axioms (axs, T) + (* simply-typed lambda calculus *) + | Const (s, T) => + if is_const_of_class thy (s, T) then + (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *) + (* and the class definition *) + let + val class = Logic.class_of_const s + val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class) + val ax_in = SOME (specialize_type thy (s, T) inclass) + (* type match may fail due to sort constraints *) + handle Type.TYPE_MATCH => NONE + val ax_1 = Option.map (fn ax => (Sign.string_of_term thy ax, ax)) + ax_in + val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) + (get_classdef thy class) + in + collect_type_axioms (fold collect_this_axiom + (map_filter I [ax_1, ax_2]) axs, T) + end + else if is_IDT_constructor thy (s, T) + orelse is_IDT_recursor thy (s, T) then + (* only collect relevant type axioms *) + collect_type_axioms (axs, T) + else + (* other constants should have been unfolded, with some *) + (* exceptions: e.g. Abs_xxx/Rep_xxx functions for *) + (* typedefs, or type-class related constants *) + (* only collect relevant type axioms *) + collect_type_axioms (axs, T) + | Free (_, T) => collect_type_axioms (axs, T) + | Var (_, T) => collect_type_axioms (axs, T) + | Bound i => axs + | Abs (_, T, body) => collect_term_axioms + (collect_type_axioms (axs, T), body) + | t1 $ t2 => collect_term_axioms + (collect_term_axioms (axs, t1), t2) + (* Term.term list *) + val result = map close_form (collect_term_axioms ([], t)) + val _ = writeln " ...done." + in + result + end; (* ------------------------------------------------------------------------- *) (* ground_types: collects all ground types in a term (including argument *) @@ -960,61 +960,61 @@ (* are considered. *) (* ------------------------------------------------------------------------- *) - (* theory -> Term.term -> Term.typ list *) + (* theory -> Term.term -> Term.typ list *) - fun ground_types thy t = - let - (* Term.typ * Term.typ list -> Term.typ list *) - fun collect_types (T, acc) = - if T mem acc then - acc (* prevent infinite recursion (for IDTs) *) - else - (case T of - Type ("fun", [T1, T2]) => collect_types (T1, collect_types (T2, acc)) - | Type ("prop", []) => acc - | Type ("set", [T1]) => collect_types (T1, acc) - | Type (s, Ts) => - (case DatatypePackage.get_datatype thy s of - SOME info => (* inductive datatype *) - let - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = lookup descr index - val typ_assoc = dtyps ~~ Ts - (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) - val _ = (if Library.exists (fn d => - case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("ground_types", "datatype argument (for type " - ^ Sign.string_of_typ thy (Type (s, Ts)) - ^ ") is not a variable") - else - ()) - (* if the current type is a recursive IDT (i.e. a depth is *) - (* required), add it to 'acc' *) - val acc' = (if Library.exists (fn (_, ds) => Library.exists - DatatypeAux.is_rec_type ds) constrs then - insert (op =) T acc - else - acc) - (* collect argument types *) - val acc_args = foldr collect_types acc' Ts - (* collect constructor types *) - val acc_constrs = foldr collect_types acc_args (List.concat - (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) - constrs)) - in - acc_constrs - end - | NONE => - (* not an inductive datatype, e.g. defined via "typedef" or *) - (* "typedecl" *) - insert (op =) T (foldr collect_types acc Ts)) - | TFree _ => insert (op =) T acc - | TVar _ => insert (op =) T acc) - in - it_term_types collect_types (t, []) - end; + fun ground_types thy t = + let + (* Term.typ * Term.typ list -> Term.typ list *) + fun collect_types (T, acc) = + if T mem acc then + acc (* prevent infinite recursion (for IDTs) *) + else + (case T of + Type ("fun", [T1, T2]) => collect_types (T1, collect_types (T2, acc)) + | Type ("prop", []) => acc + | Type ("set", [T1]) => collect_types (T1, acc) + | Type (s, Ts) => + (case DatatypePackage.get_datatype thy s of + SOME info => (* inductive datatype *) + let + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = lookup descr index + val typ_assoc = dtyps ~~ Ts + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = (if Library.exists (fn d => + case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("ground_types", "datatype argument (for type " + ^ Sign.string_of_typ thy (Type (s, Ts)) + ^ ") is not a variable") + else + ()) + (* if the current type is a recursive IDT (i.e. a depth is *) + (* required), add it to 'acc' *) + val acc' = (if Library.exists (fn (_, ds) => Library.exists + DatatypeAux.is_rec_type ds) constrs then + insert (op =) T acc + else + acc) + (* collect argument types *) + val acc_args = foldr collect_types acc' Ts + (* collect constructor types *) + val acc_constrs = foldr collect_types acc_args (List.concat + (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) + constrs)) + in + acc_constrs + end + | NONE => + (* not an inductive datatype, e.g. defined via "typedef" or *) + (* "typedecl" *) + insert (op =) T (foldr collect_types acc Ts)) + | TFree _ => insert (op =) T acc + | TVar _ => insert (op =) T acc) + in + it_term_types collect_types (t, []) + end; (* ------------------------------------------------------------------------- *) (* string_of_typ: (rather naive) conversion from types to strings, used to *) @@ -1023,11 +1023,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 *) @@ -1035,17 +1035,17 @@ (* '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 = - let - fun size_of_typ T = - case AList.lookup (op =) sizes (string_of_typ T) of - SOME n => n - | NONE => minsize - in - map (fn T => (T, size_of_typ T)) xs - end; + fun first_universe xs sizes minsize = + let + fun size_of_typ T = + case AList.lookup (op =) sizes (string_of_typ T) of + SOME n => n + | NONE => minsize + in + map (fn T => (T, size_of_typ T)) xs + end; (* ------------------------------------------------------------------------- *) (* next_universe: enumerates all universes (i.e. assignments of sizes to *) @@ -1054,70 +1054,70 @@ (* 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 = - 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 - | 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)) - (* 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 - | 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 *) - | next max len sum (x1::x2::xs) = - if x1>0 andalso (x2 n-minsize) mutables - in - case next (maxsize-minsize) 0 0 diffs of - SOME diffs' => - (* merge with those types for which the size is fixed *) - SOME (snd (foldl_map (fn (ds, (T, _)) => - case AList.lookup (op =) sizes (string_of_typ T) of - (* return the fixed size *) - SOME n => (ds, (T, n)) - (* consume the head of 'ds', add 'minsize' *) - | NONE => (tl ds, (T, minsize + hd ds))) - (diffs', xs))) - | NONE => - NONE - end; + 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 + | 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)) + (* 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 + | 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 *) + | next max len sum (x1::x2::xs) = + if x1>0 andalso (x2 n-minsize) mutables + in + case next (maxsize-minsize) 0 0 diffs of + SOME diffs' => + (* merge with those types for which the size is fixed *) + SOME (snd (foldl_map (fn (ds, (T, _)) => + case AList.lookup (op =) sizes (string_of_typ T) of + (* return the fixed size *) + SOME n => (ds, (T, n)) + (* consume the head of 'ds', add 'minsize' *) + | NONE => (tl ds, (T, minsize + hd ds))) + (diffs', xs))) + | NONE => + NONE + end; (* ------------------------------------------------------------------------- *) (* toTrue: converts the interpretation of a Boolean value to a propositional *) (* formula that is true iff the interpretation denotes "true" *) (* ------------------------------------------------------------------------- *) - (* interpretation -> prop_formula *) + (* 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 *) @@ -1125,12 +1125,12 @@ (* 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, *) @@ -1142,121 +1142,121 @@ (* 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} t - negate = - let - (* unit -> unit *) - fun wrapper () = - let - val u = unfold_defs thy t - val _ = writeln ("Unfolded term: " ^ Sign.string_of_term thy u) - val axioms = collect_axioms thy u - (* Term.typ list *) - val types = Library.foldl (fn (acc, t') => - acc union (ground_types thy t')) ([], u :: axioms) - val _ = writeln ("Ground types: " - ^ (if null types then "none." - else commas (map (Sign.string_of_typ 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 _ = if Library.exists (fn - Type (s, _) => - (case DatatypePackage.get_datatype thy s of - SOME info => (* inductive datatype *) - let - val index = #index info - val descr = #descr info - val (_, _, constrs) = lookup descr index - in - (* recursive datatype? *) - Library.exists (fn (_, ds) => - Library.exists DatatypeAux.is_rec_type ds) constrs - end - | NONE => false) - | _ => false) types then - warning ("Term contains a recursive datatype; " - ^ "countermodel(s) may be spurious!") - else - () - (* (Term.typ * int) list -> unit *) - fun find_model_loop universe = - let - val init_model = (universe, []) - val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1, - bounds = [], wellformed = True} - val _ = immediate_output ("Translating term (sizes: " - ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") - (* translate 'u' and all axioms *) - val ((model, args), intrs) = foldl_map (fn ((m, a), t') => - let - val (i, m', a') = interpret thy m a t' - in - (* set 'def_eq' to 'true' *) - ((m', {maxvars = #maxvars a', def_eq = true, - next_idx = #next_idx a', bounds = #bounds a', - wellformed = #wellformed a'}), i) - end) ((init_model, init_args), u :: axioms) - (* 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] - in - immediate_output " invoking SAT solver..."; - (case SatSolver.invoke_solver satsolver fm of - SatSolver.SATISFIABLE assignment => - (writeln " model found!"; - writeln ("*** Model found: ***\n" ^ print_model thy model - (fn i => case assignment i of SOME b => b | NONE => true))) - | SatSolver.UNSATISFIABLE _ => - (immediate_output " no model exists.\n"; - case next_universe universe sizes minsize maxsize of - SOME universe' => find_model_loop universe' - | NONE => writeln - "Search terminated, no larger universe within the given limits.") - | SatSolver.UNKNOWN => - (immediate_output " no model found.\n"; - case next_universe universe sizes minsize maxsize of - SOME universe' => find_model_loop universe' - | NONE => writeln - "Search terminated, no larger universe within the given limits.") - ) handle SatSolver.NOT_CONFIGURED => - error ("SAT solver " ^ quote satsolver ^ " is not configured.") - end handle MAXVARS_EXCEEDED => - writeln ("\nSearch terminated, number of Boolean variables (" - ^ string_of_int maxvars ^ " allowed) exceeded.") - in - find_model_loop (first_universe types sizes minsize) - end - in - (* some parameter sanity checks *) - assert (minsize>=1) - ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1"); - assert (maxsize>=1) - ("\"maxsize\" is " ^ string_of_int maxsize ^ ", must be at least 1"); - assert (maxsize>=minsize) - ("\"maxsize\" (=" ^ string_of_int maxsize ^ - ") is less than \"minsize\" (=" ^ string_of_int minsize ^ ")."); - assert (maxvars>=0) - ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0"); - assert (maxtime>=0) - ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0"); - (* enter loop with or without time limit *) - writeln ("Trying to find a model that " - ^ (if negate then "refutes" else "satisfies") ^ ": " - ^ Sign.string_of_term thy t); - if maxtime>0 then ( - interrupt_timeout (Time.fromSeconds (Int.toLarge maxtime)) - wrapper () - handle Interrupt => - writeln ("\nSearch terminated, time limit (" ^ string_of_int maxtime - ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.") - ) else - wrapper () - end; + fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver} t + negate = + let + (* unit -> unit *) + fun wrapper () = + let + val u = unfold_defs thy t + val _ = writeln ("Unfolded term: " ^ Sign.string_of_term thy u) + val axioms = collect_axioms thy u + (* Term.typ list *) + val types = Library.foldl (fn (acc, t') => + acc union (ground_types thy t')) ([], u :: axioms) + val _ = writeln ("Ground types: " + ^ (if null types then "none." + else commas (map (Sign.string_of_typ 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 _ = if Library.exists (fn + Type (s, _) => + (case DatatypePackage.get_datatype thy s of + SOME info => (* inductive datatype *) + let + val index = #index info + val descr = #descr info + val (_, _, constrs) = lookup descr index + in + (* recursive datatype? *) + Library.exists (fn (_, ds) => + Library.exists DatatypeAux.is_rec_type ds) constrs + end + | NONE => false) + | _ => false) types then + warning ("Term contains a recursive datatype; " + ^ "countermodel(s) may be spurious!") + else + () + (* (Term.typ * int) list -> unit *) + fun find_model_loop universe = + let + val init_model = (universe, []) + val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1, + bounds = [], wellformed = True} + val _ = immediate_output ("Translating term (sizes: " + ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") + (* translate 'u' and all axioms *) + val ((model, args), intrs) = foldl_map (fn ((m, a), t') => + let + val (i, m', a') = interpret thy m a t' + in + (* set 'def_eq' to 'true' *) + ((m', {maxvars = #maxvars a', def_eq = true, + next_idx = #next_idx a', bounds = #bounds a', + wellformed = #wellformed a'}), i) + end) ((init_model, init_args), u :: axioms) + (* 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] + in + immediate_output " invoking SAT solver..."; + (case SatSolver.invoke_solver satsolver fm of + SatSolver.SATISFIABLE assignment => + (writeln " model found!"; + writeln ("*** Model found: ***\n" ^ print_model thy model + (fn i => case assignment i of SOME b => b | NONE => true))) + | SatSolver.UNSATISFIABLE _ => + (immediate_output " no model exists.\n"; + case next_universe universe sizes minsize maxsize of + SOME universe' => find_model_loop universe' + | NONE => writeln + "Search terminated, no larger universe within the given limits.") + | SatSolver.UNKNOWN => + (immediate_output " no model found.\n"; + case next_universe universe sizes minsize maxsize of + SOME universe' => find_model_loop universe' + | NONE => writeln + "Search terminated, no larger universe within the given limits.") + ) handle SatSolver.NOT_CONFIGURED => + error ("SAT solver " ^ quote satsolver ^ " is not configured.") + end handle MAXVARS_EXCEEDED => + writeln ("\nSearch terminated, number of Boolean variables (" + ^ string_of_int maxvars ^ " allowed) exceeded.") + in + find_model_loop (first_universe types sizes minsize) + 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 *) + writeln ("Trying to find a model that " + ^ (if negate then "refutes" else "satisfies") ^ ": " + ^ Sign.string_of_term thy t); + if maxtime>0 then ( + interrupt_timeout (Time.fromSeconds (Int.toLarge maxtime)) + wrapper () + handle Interrupt => + writeln ("\nSearch terminated, time limit (" ^ string_of_int maxtime + ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.") + ) else + wrapper () + end; (* ------------------------------------------------------------------------- *) @@ -1269,10 +1269,10 @@ (* parameters *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * string) list -> Term.term -> unit *) + (* theory -> (string * string) list -> Term.term -> unit *) - fun satisfy_term thy params t = - find_model thy (actual_params thy params) t false; + fun satisfy_term thy params t = + find_model thy (actual_params thy params) t false; (* ------------------------------------------------------------------------- *) (* refute_term: calls 'find_model' to find a model that refutes 't' *) @@ -1280,57 +1280,57 @@ (* parameters *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * string) list -> Term.term -> unit *) + (* theory -> (string * string) list -> Term.term -> unit *) - fun refute_term thy params t = - let - (* disallow schematic type variables, since we cannot properly negate *) - (* terms containing them (their logical meaning is that there EXISTS a *) - (* type s.t. ...; to refute such a formula, we would have to show that *) - (* for ALL types, not ...) *) - val _ = assert (null (term_tvars t)) - "Term to be refuted contains schematic type variables" + fun refute_term thy params t = + let + (* disallow schematic type variables, since we cannot properly negate *) + (* terms containing them (their logical meaning is that there EXISTS a *) + (* type s.t. ...; to refute such a formula, we would have to show that *) + (* for ALL types, not ...) *) + val _ = null (term_tvars t) orelse + error "Term to be refuted contains schematic type variables" - (* existential closure over schematic variables *) - (* (Term.indexname * Term.typ) list *) - val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t)) - (* Term.term *) - val ex_closure = Library.foldl (fn (t', ((x, i), T)) => - (HOLogic.exists_const T) $ - Abs (x, T, abstract_over (Var ((x, i), T), t'))) - (t, vars) - (* Note: If 't' is of type 'propT' (rather than 'boolT'), applying *) - (* 'HOLogic.exists_const' is not type-correct. However, this is not *) - (* really a problem as long as 'find_model' still interprets the *) - (* resulting term correctly, without checking its type. *) + (* existential closure over schematic variables *) + (* (Term.indexname * Term.typ) list *) + val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t)) + (* Term.term *) + val ex_closure = Library.foldl (fn (t', ((x, i), T)) => + (HOLogic.exists_const T) $ + Abs (x, T, abstract_over (Var ((x, i), T), t'))) + (t, vars) + (* Note: If 't' is of type 'propT' (rather than 'boolT'), applying *) + (* 'HOLogic.exists_const' is not type-correct. However, this is not *) + (* really a problem as long as 'find_model' still interprets the *) + (* resulting term correctly, without checking its type. *) - (* replace outermost universally quantified variables by Free's: *) - (* refuting a term with Free's is generally faster than refuting a *) - (* term with (nested) quantifiers, because quantifiers are expanded, *) - (* while the SAT solver searches for an interpretation for Free's. *) - (* Also we get more information back that way, namely an *) - (* interpretation which includes values for the (formerly) *) - (* quantified variables. *) - (* maps !!x1...xn. !xk...xm. t to t *) - fun strip_all_body (Const ("all", _) $ Abs (_, _, t)) = strip_all_body t - | strip_all_body (Const ("Trueprop", _) $ t) = strip_all_body t - | strip_all_body (Const ("All", _) $ Abs (_, _, 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 ("all", _) $ Abs (a, T, t)) = - (a, T) :: strip_all_vars t - | strip_all_vars (Const ("Trueprop", _) $ t) = - strip_all_vars t - | strip_all_vars (Const ("All", _) $ Abs (a, T, t)) = - (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 subst_t = Term.subst_bounds (map Free frees, strip_t) - in - find_model thy (actual_params thy params) subst_t true - end; + (* replace outermost universally quantified variables by Free's: *) + (* refuting a term with Free's is generally faster than refuting a *) + (* term with (nested) quantifiers, because quantifiers are expanded, *) + (* while the SAT solver searches for an interpretation for Free's. *) + (* Also we get more information back that way, namely an *) + (* interpretation which includes values for the (formerly) *) + (* quantified variables. *) + (* maps !!x1...xn. !xk...xm. t to t *) + fun strip_all_body (Const ("all", _) $ Abs (_, _, t)) = strip_all_body t + | strip_all_body (Const ("Trueprop", _) $ t) = strip_all_body t + | strip_all_body (Const ("All", _) $ Abs (_, _, 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 ("all", _) $ Abs (a, T, t)) = + (a, T) :: strip_all_vars t + | strip_all_vars (Const ("Trueprop", _) $ t) = + strip_all_vars t + | strip_all_vars (Const ("All", _) $ Abs (a, T, t)) = + (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 subst_t = Term.subst_bounds (map Free frees, strip_t) + in + find_model thy (actual_params thy params) subst_t true + end; (* ------------------------------------------------------------------------- *) (* refute_subgoal: calls 'refute_term' on a specific subgoal *) @@ -1339,10 +1339,10 @@ (* subgoal : 0-based index specifying the subgoal number *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * string) list -> Thm.thm -> int -> unit *) + (* theory -> (string * string) list -> Thm.thm -> int -> unit *) - fun refute_subgoal thy params thm subgoal = - refute_term thy params (List.nth (Thm.prems_of thm, subgoal)); + fun refute_subgoal thy params thm subgoal = + refute_term thy params (List.nth (Thm.prems_of thm, subgoal)); (* ------------------------------------------------------------------------- *) @@ -1355,71 +1355,71 @@ (* 'True'/'False' only (no Boolean variables) *) (* ------------------------------------------------------------------------- *) - (* interpretation -> interpretation list *) + (* interpretation -> interpretation list *) - fun make_constants intr = - 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 -> interpretation list *) - fun unit_vectors_acc k vs = - if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs) - in - unit_vectors_acc 1 [] - end - (* 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 - Library.foldl (fn (acc, x) => map (cons x) rec_pick @ acc) ([], xs) - end - in - case intr of - Leaf xs => unit_vectors (length xs) - | Node xs => map (fn xs' => Node xs') (pick_all (length xs) - (make_constants (hd xs))) - end; + fun make_constants intr = + 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 -> interpretation list *) + fun unit_vectors_acc k vs = + if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs) + in + unit_vectors_acc 1 [] + end + (* 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 + Library.foldl (fn (acc, x) => map (cons x) rec_pick @ acc) ([], xs) + end + in + case intr of + Leaf xs => unit_vectors (length xs) + | Node xs => map (fn xs' => Node xs') (pick_all (length xs) + (make_constants (hd xs))) + end; (* ------------------------------------------------------------------------- *) (* size_of_type: returns the number of constants in a type (i.e. 'length *) (* (make_constants intr)', but implemented more efficiently) *) (* ------------------------------------------------------------------------- *) - (* interpretation -> int *) + (* interpretation -> int *) - fun size_of_type intr = - let - (* power (a, b) computes a^b, for a>=0, b>=0 *) - (* int * int -> int *) - fun power (a, 0) = 1 - | power (a, 1) = a - | power (a, b) = let val ab = power(a, b div 2) in - ab * ab * power(a, b mod 2) - end - in - case intr of - Leaf xs => length xs - | Node xs => power (size_of_type (hd xs), length xs) - end; + fun size_of_type intr = + let + (* power (a, b) computes a^b, for a>=0, b>=0 *) + (* int * int -> int *) + fun power (a, 0) = 1 + | power (a, 1) = a + | power (a, b) = let val ab = power(a, b div 2) in + ab * ab * power(a, b mod 2) + end + in + case intr of + Leaf xs => length xs + | Node xs => power (size_of_type (hd xs), length xs) + end; (* ------------------------------------------------------------------------- *) (* TT/FF: interpretations that denote "true" or "false", respectively *) (* ------------------------------------------------------------------------- *) - (* interpretation *) + (* 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) *) @@ -1432,51 +1432,51 @@ (* '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) = - 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")) - | Node xs => - (case i2 of - Leaf _ => raise REFUTE ("make_equality", - "first interpretation is higher") - | Node ys => PropLogic.all (map equal (xs ~~ ys)))) - (* interpretation * interpretation -> prop_formula *) - fun not_equal (i1, i2) = - (case i1 of - Leaf xs => - (case i2 of - (* 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)))) - in - (* a value may be undefined; therefore 'not_equal' is not just the *) - (* negation of 'equal' *) - Leaf [equal (i1, i2), not_equal (i1, i2)] - end; + 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")) + | Node xs => + (case i2 of + Leaf _ => raise REFUTE ("make_equality", + "first interpretation is higher") + | Node ys => PropLogic.all (map equal (xs ~~ ys)))) + (* interpretation * interpretation -> prop_formula *) + fun not_equal (i1, i2) = + (case i1 of + Leaf xs => + (case i2 of + (* 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)))) + in + (* a value may be undefined; therefore 'not_equal' is not just the *) + (* negation of 'equal' *) + Leaf [equal (i1, i2), not_equal (i1, i2)] + end; (* ------------------------------------------------------------------------- *) (* make_def_equality: returns an interpretation that denotes (extensional) *) @@ -1487,30 +1487,30 @@ (* to an undefined interpretation. *) (* ------------------------------------------------------------------------- *) - (* interpretation * interpretation -> interpretation *) + (* interpretation * interpretation -> interpretation *) - 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")) - | Node xs => - (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 - Leaf [eq, SNot eq] - end; + 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")) + | Node xs => + (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 + Leaf [eq, SNot eq] + end; (* ------------------------------------------------------------------------- *) (* interpretation_apply: returns an interpretation that denotes the result *) @@ -1518,86 +1518,86 @@ (* argument denoted by 'i2' *) (* ------------------------------------------------------------------------- *) - (* interpretation * interpretation -> interpretation *) + (* interpretation * interpretation -> interpretation *) - fun interpretation_apply (i1, i2) = - let - (* interpretation * interpretation -> interpretation *) - fun interpretation_disjunction (tr1,tr2) = - tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) - (tree_pair (tr1,tr2)) - (* prop_formula * interpretation -> interpretation *) - fun prop_formula_times_interpretation (fm,tr) = - tree_map (map (fn x => SAnd (fm,x))) tr - (* prop_formula list * interpretation list -> interpretation *) - fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) = - prop_formula_times_interpretation (fm,tr) - | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) = - interpretation_disjunction (prop_formula_times_interpretation (fm,tr), - prop_formula_list_dot_product_interpretation_list (fms,trees)) - | prop_formula_list_dot_product_interpretation_list (_,_) = - raise REFUTE ("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 - (* 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 - | pick_all (xs::xss) = - let val rec_pick = pick_all xss in - Library.foldl (fn (acc, x) => (cons_list x rec_pick) @ acc) ([], 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 - | interpretation_to_prop_formula_list (Node 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") - | Node xs => - prop_formula_list_dot_product_interpretation_list - (interpretation_to_prop_formula_list i2, xs) - end; + fun interpretation_apply (i1, i2) = + let + (* interpretation * interpretation -> interpretation *) + fun interpretation_disjunction (tr1,tr2) = + tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) + (tree_pair (tr1,tr2)) + (* prop_formula * interpretation -> interpretation *) + fun prop_formula_times_interpretation (fm,tr) = + tree_map (map (fn x => SAnd (fm,x))) tr + (* prop_formula list * interpretation list -> interpretation *) + fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) = + prop_formula_times_interpretation (fm,tr) + | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) = + interpretation_disjunction (prop_formula_times_interpretation (fm,tr), + prop_formula_list_dot_product_interpretation_list (fms,trees)) + | prop_formula_list_dot_product_interpretation_list (_,_) = + raise REFUTE ("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 + (* 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 + | pick_all (xs::xss) = + let val rec_pick = pick_all xss in + Library.foldl (fn (acc, x) => (cons_list x rec_pick) @ acc) ([], 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 + | interpretation_to_prop_formula_list (Node 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") + | Node 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 = - let - val Ts = Term.binder_types (Term.fastype_of t) - val t' = Term.incr_boundvars i t - in - foldr (fn (T, term) => Abs ("", T, term)) - (Term.list_comb (t', map Bound (i-1 downto 0))) (List.take (Ts, i)) - end; + fun eta_expand t i = + let + val Ts = Term.binder_types (Term.fastype_of t) + val t' = Term.incr_boundvars i t + in + foldr (fn (T, term) => Abs ("", T, term)) + (Term.list_comb (t', map Bound (i-1 downto 0))) (List.take (Ts, i)) + end; (* ------------------------------------------------------------------------- *) (* sum: returns the sum of a list 'xs' of integers *) (* ------------------------------------------------------------------------- *) - (* int list -> int *) + (* int list -> int *) - fun sum xs = foldl op+ 0 xs; + fun sum xs = foldl op+ 0 xs; (* ------------------------------------------------------------------------- *) (* product: returns the product of a list 'xs' of integers *) (* ------------------------------------------------------------------------- *) - (* int list -> int *) + (* int list -> int *) - fun product xs = foldl op* 1 xs; + fun product xs = foldl op* 1 xs; (* ------------------------------------------------------------------------- *) (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *) @@ -1605,1594 +1605,1594 @@ (* their arguments) of the size of the argument types *) (* ------------------------------------------------------------------------- *) - (* theory -> (Term.typ * int) list -> DatatypeAux.descr -> - (DatatypeAux.dtyp * Term.typ) list -> - (string * DatatypeAux.dtyp list) list -> int *) + (* theory -> (Term.typ * int) list -> DatatypeAux.descr -> + (DatatypeAux.dtyp * Term.typ) list -> + (string * DatatypeAux.dtyp list) list -> int *) - fun size_of_dtyp thy typ_sizes descr typ_assoc constructors = - sum (map (fn (_, dtyps) => - product (map (fn dtyp => - let - val T = typ_of_dtyp descr typ_assoc dtyp - val (i, _, _) = interpret thy (typ_sizes, []) - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", T)) - in - size_of_type i - end) dtyps)) constructors); + fun size_of_dtyp thy typ_sizes descr typ_assoc constructors = + sum (map (fn (_, dtyps) => + product (map (fn dtyp => + let + val T = typ_of_dtyp descr typ_assoc dtyp + val (i, _, _) = interpret thy (typ_sizes, []) + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", T)) + in + size_of_type i + end) 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 = - let - 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 lookup 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 - case T of - Type ("fun", [T1, T2]) => - let - (* we create 'size_of_type (interpret (... T1))' different copies *) - (* of the interpretation for 'T2', which are then combined into a *) - (* single new interpretation *) - val (i1, _, _) = interpret thy model {maxvars=0, def_eq=false, - next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1)) - (* 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 i1) - (* combine copies into a single interpretation *) - val intr = Node copies - in - (* extend the model, increase 'next_idx', add well-formedness *) - (* condition *) - SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, - 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) - | 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 (i, _, _) = interpret thy model {maxvars=0, def_eq=false, - next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) - val constants = make_constants i - (* interpret the 'body' separately for each constant *) - val ((model', args'), bodies) = foldl_map - (fn ((m, a), c) => - let - (* add 'c' to 'bounds' *) - val (i', m', a') = interpret thy m {maxvars = #maxvars a, - 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' *) - ((m', {maxvars = maxvars, def_eq = def_eq, - next_idx = #next_idx a', bounds = bounds, - wellformed = #wellformed a'}), i') - end) - ((model, args), constants) - in - SOME (Node bodies, model', args') - end - | t1 $ t2 => - let - (* 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; + fun stlc_interpreter thy model args t = + let + 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 lookup 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 + case T of + Type ("fun", [T1, T2]) => + let + (* we create 'size_of_type (interpret (... T1))' different copies *) + (* of the interpretation for 'T2', which are then combined into a *) + (* single new interpretation *) + val (i1, _, _) = interpret thy model {maxvars=0, def_eq=false, + next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1)) + (* 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 i1) + (* combine copies into a single interpretation *) + val intr = Node copies + in + (* extend the model, increase 'next_idx', add well-formedness *) + (* condition *) + SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, + 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) + | 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 (i, _, _) = interpret thy model {maxvars=0, def_eq=false, + next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) + val constants = make_constants i + (* interpret the 'body' separately for each constant *) + val ((model', args'), bodies) = foldl_map + (fn ((m, a), c) => + let + (* add 'c' to 'bounds' *) + val (i', m', a') = interpret thy m {maxvars = #maxvars a, + 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' *) + ((m', {maxvars = maxvars, def_eq = def_eq, + next_idx = #next_idx a', bounds = bounds, + wellformed = #wellformed a'}), i') + end) + ((model, args), constants) + in + SOME (Node bodies, model', args') + end + | t1 $ t2 => + let + (* 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 ("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 - | _ => - raise REFUTE ("Pure_interpreter", - "\"all\" is followed by a non-function") - end - | Const ("all", _) => - SOME (interpret thy model args (eta_expand t 1)) - | Const ("==", _) $ t1 $ t2 => - let - val (i1, m1, a1) = interpret thy model args t1 - val (i2, m2, a2) = interpret thy m1 a1 t2 - in - (* we use either 'make_def_equality' or 'make_equality' *) - SOME ((if #def_eq args then make_def_equality else make_equality) - (i1, i2), m2, a2) - end - | Const ("==", _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) - | Const ("==", _) => - SOME (interpret thy model args (eta_expand t 2)) - | Const ("==>", _) $ t1 $ t2 => - (* 3-valued logic *) - let - val (i1, m1, a1) = interpret thy model args t1 - val (i2, m2, a2) = interpret thy m1 a1 t2 - val fmTrue = PropLogic.SOr (toFalse i1, toTrue i2) - val fmFalse = PropLogic.SAnd (toTrue i1, toFalse i2) - in - SOME (Leaf [fmTrue, fmFalse], m2, a2) - end - | Const ("==>", _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) - | Const ("==>", _) => - SOME (interpret thy model args (eta_expand t 2)) - | _ => NONE; + fun Pure_interpreter thy model args t = + case t of + Const ("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 + | _ => + raise REFUTE ("Pure_interpreter", + "\"all\" is followed by a non-function") + end + | Const ("all", _) => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("==", _) $ t1 $ t2 => + let + val (i1, m1, a1) = interpret thy model args t1 + val (i2, m2, a2) = interpret thy m1 a1 t2 + in + (* we use either 'make_def_equality' or 'make_equality' *) + SOME ((if #def_eq args then make_def_equality else make_equality) + (i1, i2), m2, a2) + end + | Const ("==", _) $ t1 => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("==", _) => + SOME (interpret thy model args (eta_expand t 2)) + | Const ("==>", _) $ t1 $ t2 => + (* 3-valued logic *) + let + val (i1, m1, a1) = interpret thy model args t1 + val (i2, m2, a2) = interpret thy m1 a1 t2 + val fmTrue = PropLogic.SOr (toFalse i1, toTrue i2) + val fmFalse = PropLogic.SAnd (toTrue i1, toFalse i2) + in + SOME (Leaf [fmTrue, fmFalse], m2, a2) + end + | Const ("==>", _) $ t1 => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("==>", _) => + SOME (interpret thy model args (eta_expand t 2)) + | _ => 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 ("Trueprop", _) => - SOME (Node [TT, FF], model, args) - | Const ("Not", _) => - SOME (Node [FF, TT], model, args) - (* redundant, since 'True' is also an IDT constructor *) - | Const ("True", _) => - SOME (TT, model, args) - (* redundant, since 'False' is also an IDT constructor *) - | Const ("False", _) => - SOME (FF, model, args) - | Const ("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 - | _ => - raise REFUTE ("HOLogic_interpreter", - "\"All\" is followed by a non-function") - end - | Const ("All", _) => - SOME (interpret thy model args (eta_expand t 1)) - | Const ("Ex", _) $ t1 => - let - val (i, m, a) = interpret thy model args t1 - in - case i of - Node xs => - (* 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 ("Ex", _) => - SOME (interpret thy model args (eta_expand t 1)) - | Const ("op =", _) $ 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 ("op =", _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) - | Const ("op =", _) => - SOME (interpret thy model args (eta_expand t 2)) - | Const ("op &", _) $ t1 $ t2 => - (* 3-valued logic *) - let - val (i1, m1, a1) = interpret thy model args t1 - val (i2, m2, a2) = interpret thy m1 a1 t2 - val fmTrue = PropLogic.SAnd (toTrue i1, toTrue i2) - val fmFalse = PropLogic.SOr (toFalse i1, toFalse i2) - in - SOME (Leaf [fmTrue, fmFalse], m2, a2) - end - | Const ("op &", _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) - | Const ("op &", _) => - SOME (interpret thy model args (eta_expand t 2)) - (* this would make "undef" propagate, even for formulae like *) - (* "False & undef": *) - (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *) - | Const ("op |", _) $ t1 $ t2 => - (* 3-valued logic *) - let - val (i1, m1, a1) = interpret thy model args t1 - val (i2, m2, a2) = interpret thy m1 a1 t2 - val fmTrue = PropLogic.SOr (toTrue i1, toTrue i2) - val fmFalse = PropLogic.SAnd (toFalse i1, toFalse i2) - in - SOME (Leaf [fmTrue, fmFalse], m2, a2) - end - | Const ("op |", _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) - | Const ("op |", _) => - SOME (interpret thy model args (eta_expand t 2)) - (* this would make "undef" propagate, even for formulae like *) - (* "True | undef": *) - (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *) - | Const ("op -->", _) $ t1 $ t2 => (* similar to "==>" (Pure) *) - (* 3-valued logic *) - let - val (i1, m1, a1) = interpret thy model args t1 - val (i2, m2, a2) = interpret thy m1 a1 t2 - val fmTrue = PropLogic.SOr (toFalse i1, toTrue i2) - val fmFalse = PropLogic.SAnd (toTrue i1, toFalse i2) - in - SOME (Leaf [fmTrue, fmFalse], m2, a2) - end - | Const ("op -->", _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) - | Const ("op -->", _) => - SOME (interpret thy model args (eta_expand t 2)) - (* this would make "undef" propagate, even for formulae like *) - (* "False --> undef": *) - (* SOME (Node [Node [TT, FF], Node [TT, TT]], model, args) *) - | _ => NONE; + 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 ("Trueprop", _) => + SOME (Node [TT, FF], model, args) + | Const ("Not", _) => + SOME (Node [FF, TT], model, args) + (* redundant, since 'True' is also an IDT constructor *) + | Const ("True", _) => + SOME (TT, model, args) + (* redundant, since 'False' is also an IDT constructor *) + | Const ("False", _) => + SOME (FF, model, args) + | Const ("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 + | _ => + raise REFUTE ("HOLogic_interpreter", + "\"All\" is followed by a non-function") + end + | Const ("All", _) => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("Ex", _) $ t1 => + let + val (i, m, a) = interpret thy model args t1 + in + case i of + Node xs => + (* 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 ("Ex", _) => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("op =", _) $ 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 ("op =", _) $ t1 => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("op =", _) => + SOME (interpret thy model args (eta_expand t 2)) + | Const ("op &", _) $ t1 $ t2 => + (* 3-valued logic *) + let + val (i1, m1, a1) = interpret thy model args t1 + val (i2, m2, a2) = interpret thy m1 a1 t2 + val fmTrue = PropLogic.SAnd (toTrue i1, toTrue i2) + val fmFalse = PropLogic.SOr (toFalse i1, toFalse i2) + in + SOME (Leaf [fmTrue, fmFalse], m2, a2) + end + | Const ("op &", _) $ t1 => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("op &", _) => + SOME (interpret thy model args (eta_expand t 2)) + (* this would make "undef" propagate, even for formulae like *) + (* "False & undef": *) + (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *) + | Const ("op |", _) $ t1 $ t2 => + (* 3-valued logic *) + let + val (i1, m1, a1) = interpret thy model args t1 + val (i2, m2, a2) = interpret thy m1 a1 t2 + val fmTrue = PropLogic.SOr (toTrue i1, toTrue i2) + val fmFalse = PropLogic.SAnd (toFalse i1, toFalse i2) + in + SOME (Leaf [fmTrue, fmFalse], m2, a2) + end + | Const ("op |", _) $ t1 => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("op |", _) => + SOME (interpret thy model args (eta_expand t 2)) + (* this would make "undef" propagate, even for formulae like *) + (* "True | undef": *) + (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *) + | Const ("op -->", _) $ t1 $ t2 => (* similar to "==>" (Pure) *) + (* 3-valued logic *) + let + val (i1, m1, a1) = interpret thy model args t1 + val (i2, m2, a2) = interpret thy m1 a1 t2 + val fmTrue = PropLogic.SOr (toFalse i1, toTrue i2) + val fmFalse = PropLogic.SAnd (toTrue i1, toFalse i2) + in + SOME (Leaf [fmTrue, fmFalse], m2, a2) + end + | Const ("op -->", _) $ t1 => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("op -->", _) => + SOME (interpret thy model args (eta_expand t 2)) + (* this would make "undef" propagate, even for formulae like *) + (* "False --> undef": *) + (* SOME (Node [Node [TT, FF], Node [TT, TT]], model, args) *) + | _ => 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 = - (* "T set" is isomorphic to "T --> bool" *) - let - val (typs, terms) = model - in - case AList.lookup (op =) terms t of - SOME intr => - (* return an existing interpretation *) - SOME (intr, model, args) - | NONE => - (case t of - Free (x, Type ("set", [T])) => - let - val (intr, _, args') = - interpret thy (typs, []) args (Free (x, T --> HOLogic.boolT)) - in - SOME (intr, (typs, (t, intr)::terms), args') - end - | Var ((x, i), Type ("set", [T])) => - let - val (intr, _, args') = - interpret thy (typs, []) args (Var ((x,i), T --> HOLogic.boolT)) - in - SOME (intr, (typs, (t, intr)::terms), args') - end - | Const (s, Type ("set", [T])) => - let - val (intr, _, args') = - interpret thy (typs, []) args (Const (s, T --> HOLogic.boolT)) - in - SOME (intr, (typs, (t, intr)::terms), args') - end - (* 'Collect' == identity *) - | Const ("Collect", _) $ t1 => - SOME (interpret thy model args t1) - | Const ("Collect", _) => - SOME (interpret thy model args (eta_expand t 1)) - (* 'op :' == application *) - | Const ("op :", _) $ t1 $ t2 => - SOME (interpret thy model args (t2 $ t1)) - | Const ("op :", _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) - | Const ("op :", _) => - SOME (interpret thy model args (eta_expand t 2)) - | _ => NONE) - end; + fun set_interpreter thy model args t = + (* "T set" is isomorphic to "T --> bool" *) + let + val (typs, terms) = model + in + case AList.lookup (op =) terms t of + SOME intr => + (* return an existing interpretation *) + SOME (intr, model, args) + | NONE => + (case t of + Free (x, Type ("set", [T])) => + let + val (intr, _, args') = + interpret thy (typs, []) args (Free (x, T --> HOLogic.boolT)) + in + SOME (intr, (typs, (t, intr)::terms), args') + end + | Var ((x, i), Type ("set", [T])) => + let + val (intr, _, args') = + interpret thy (typs, []) args (Var ((x,i), T --> HOLogic.boolT)) + in + SOME (intr, (typs, (t, intr)::terms), args') + end + | Const (s, Type ("set", [T])) => + let + val (intr, _, args') = + interpret thy (typs, []) args (Const (s, T --> HOLogic.boolT)) + in + SOME (intr, (typs, (t, intr)::terms), args') + end + (* 'Collect' == identity *) + | Const ("Collect", _) $ t1 => + SOME (interpret thy model args t1) + | Const ("Collect", _) => + SOME (interpret thy model args (eta_expand t 1)) + (* 'op :' == application *) + | Const ("op :", _) $ t1 $ t2 => + SOME (interpret thy model args (t2 $ t1)) + | Const ("op :", _) $ t1 => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("op :", _) => + 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 *) - (* interprets variables and constants whose type is an IDT; *) - (* constructors of IDTs however are properly interpreted by *) - (* 'IDT_constructor_interpreter' *) + (* interprets variables and constants whose type is an IDT; *) + (* constructors of IDTs however are properly interpreted by *) + (* 'IDT_constructor_interpreter' *) - 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 DatatypePackage.get_datatype 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)) - 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) = lookup descr index - val typ_assoc = dtyps ~~ Ts - (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) - val _ = (if Library.exists (fn d => - case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("IDT_interpreter", - "datatype argument (for type " - ^ Sign.string_of_typ 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 - in - case AList.lookup (op =) terms t of - SOME intr => - (* 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) - end; + 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 DatatypePackage.get_datatype 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)) + 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) = lookup descr index + val typ_assoc = dtyps ~~ Ts + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = (if Library.exists (fn d => + case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_interpreter", + "datatype argument (for type " + ^ Sign.string_of_typ 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 + in + case AList.lookup (op =) terms t of + SOME intr => + (* 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) + end; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) + (* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - fun IDT_constructor_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) - | NONE => - (case t of - Const (s, T) => - (case body_type T of - Type (s', Ts') => - (case DatatypePackage.get_datatype thy s' of - SOME info => (* body type is an inductive datatype *) - let - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = lookup descr index - val typ_assoc = dtyps ~~ Ts' - (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) - val _ = (if Library.exists (fn d => - case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("IDT_constructor_interpreter", - "datatype argument (for type " - ^ Sign.string_of_typ 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 - (* compute the total size of the datatype (with the *) - (* current depth) *) - val (i, _, _) = interpret thy (typs, []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", Type (s', Ts'))) - val total = size_of_type i - (* int option -- only /recursive/ IDTs have an associated *) - (* depth *) - val depth = AList.lookup (op =) typs (Type (s', Ts')) - val typs' = (case depth of NONE => typs | SOME n => - AList.update (op =) (Type (s', Ts'), n-1) typs) - (* returns an interpretation where everything is mapped to *) - (* "undefined" *) - (* DatatypeAux.dtyp list -> interpretation *) - fun make_undef [] = - Leaf (replicate total False) - | make_undef (d::ds) = - let - (* compute the current size of the type 'd' *) - val T = typ_of_dtyp descr typ_assoc d - val (i, _, _) = interpret thy (typs, []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", T)) - val size = size_of_type i - in - Node (replicate size (make_undef ds)) - end - (* returns the interpretation for a constructor at depth 1 *) - (* int * DatatypeAux.dtyp list -> int * interpretation *) - fun make_constr (offset, []) = - if offset= total") - | make_constr (offset, d::ds) = - let - (* compute the current and the old size of the type 'd' *) - val T = typ_of_dtyp descr typ_assoc d - val (i, _, _) = interpret thy (typs, []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", T)) - val size = size_of_type i - val (i', _, _) = interpret thy (typs', []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", T)) - val size' = size_of_type i' - (* sanity check *) - val _ = if size < size' then - raise REFUTE ("IDT_constructor_interpreter", - "current size is less than old size") - else () - (* int * interpretation list *) - val (new_offset, intrs) = foldl_map make_constr - (offset, replicate size' ds) - (* interpretation list *) - val undefs = replicate (size - size') (make_undef ds) - in - (* elements that exist at the previous depth are *) - (* mapped to a defined value, while new elements are *) - (* mapped to "undefined" by the recursive constructor *) - (new_offset, Node (intrs @ undefs)) - end - (* extends the interpretation for a constructor (both *) - (* recursive and non-recursive) obtained at depth n (n>=1) *) - (* to depth n+1 *) - (* int * DatatypeAux.dtyp list * interpretation - -> int * interpretation *) - fun extend_constr (offset, [], Leaf xs) = - 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 *) - val k = find_index_eq True xs - in - if k=(~1) then - (* if the element was mapped to "undefined" before, *) - (* map it to the value given by 'offset' now (and *) - (* extend the length of the leaf) *) - (offset+1, unit_vector (offset+1, total)) - else - (* if the element was already mapped to a defined *) - (* value, map it to the same value again, just *) - (* extend the length of the leaf, do not increment *) - (* the 'offset' *) - (offset, unit_vector (k+1, total)) - end - | extend_constr (_, [], Node _) = - raise REFUTE ("IDT_constructor_interpreter", - "interpretation for constructor (with no arguments left)" - ^ " is a node") - | extend_constr (offset, d::ds, Node xs) = - let - (* compute the size of the type 'd' *) - val T = typ_of_dtyp descr typ_assoc d - val (i, _, _) = interpret thy (typs, []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", T)) - val size = size_of_type i - (* sanity check *) - val _ = if size < length xs then - raise REFUTE ("IDT_constructor_interpreter", - "new size of type is less than old size") - else () - (* extend the existing interpretations *) - (* int * interpretation list *) - val (new_offset, intrs) = foldl_map (fn (off, i) => - extend_constr (off, ds, i)) (offset, xs) - (* new elements of the type 'd' are mapped to *) - (* "undefined" *) - val undefs = replicate (size - length xs) (make_undef ds) - in - (new_offset, Node (intrs @ undefs)) - end - | extend_constr (_, d::ds, Leaf _) = - raise REFUTE ("IDT_constructor_interpreter", - "interpretation for constructor (with arguments left)" - ^ " is a leaf") - (* returns 'true' iff the constructor has a recursive *) - (* argument *) - (* DatatypeAux.dtyp list -> bool *) - fun is_rec_constr ds = - Library.exists DatatypeAux.is_rec_type ds - (* constructors before 'Const (s, T)' generate elements of *) - (* the datatype *) - val offset = size_of_dtyp thy typs' descr typ_assoc constrs1 - in - case depth of - NONE => (* equivalent to a depth of 1 *) - SOME (snd (make_constr (offset, ctypes)), model, args) - | SOME 0 => - raise REFUTE ("IDT_constructor_interpreter", "depth is 0") - | SOME 1 => - SOME (snd (make_constr (offset, ctypes)), model, args) - | SOME n => (* n > 1 *) - let - (* interpret the constructor at depth-1 *) - val (iC, _, _) = interpret thy (typs', []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Const (s, T)) - (* elements generated by the constructor at depth-1 *) - (* must be added to 'offset' *) - (* interpretation -> int *) - fun number_of_defined_elements (Leaf xs) = - if find_index_eq True xs = (~1) then 0 else 1 - | number_of_defined_elements (Node xs) = - sum (map number_of_defined_elements xs) - (* int *) - val offset' = offset + number_of_defined_elements iC - in - SOME (snd (extend_constr (offset', ctypes, iC)), model, - args) - end - end - end - | 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) - end; + fun IDT_constructor_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) + | NONE => + (case t of + Const (s, T) => + (case body_type T of + Type (s', Ts') => + (case DatatypePackage.get_datatype thy s' of + SOME info => (* body type is an inductive datatype *) + let + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = lookup descr index + val typ_assoc = dtyps ~~ Ts' + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = (if Library.exists (fn d => + case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_constructor_interpreter", + "datatype argument (for type " + ^ Sign.string_of_typ 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 + (* compute the total size of the datatype (with the *) + (* current depth) *) + val (i, _, _) = interpret thy (typs, []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", Type (s', Ts'))) + val total = size_of_type i + (* int option -- only /recursive/ IDTs have an associated *) + (* depth *) + val depth = AList.lookup (op =) typs (Type (s', Ts')) + val typs' = (case depth of NONE => typs | SOME n => + AList.update (op =) (Type (s', Ts'), n-1) typs) + (* returns an interpretation where everything is mapped to *) + (* "undefined" *) + (* DatatypeAux.dtyp list -> interpretation *) + fun make_undef [] = + Leaf (replicate total False) + | make_undef (d::ds) = + let + (* compute the current size of the type 'd' *) + val T = typ_of_dtyp descr typ_assoc d + val (i, _, _) = interpret thy (typs, []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", T)) + val size = size_of_type i + in + Node (replicate size (make_undef ds)) + end + (* returns the interpretation for a constructor at depth 1 *) + (* int * DatatypeAux.dtyp list -> int * interpretation *) + fun make_constr (offset, []) = + if offset= total") + | make_constr (offset, d::ds) = + let + (* compute the current and the old size of the type 'd' *) + val T = typ_of_dtyp descr typ_assoc d + val (i, _, _) = interpret thy (typs, []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", T)) + val size = size_of_type i + val (i', _, _) = interpret thy (typs', []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", T)) + val size' = size_of_type i' + (* sanity check *) + val _ = if size < size' then + raise REFUTE ("IDT_constructor_interpreter", + "current size is less than old size") + else () + (* int * interpretation list *) + val (new_offset, intrs) = foldl_map make_constr + (offset, replicate size' ds) + (* interpretation list *) + val undefs = replicate (size - size') (make_undef ds) + in + (* elements that exist at the previous depth are *) + (* mapped to a defined value, while new elements are *) + (* mapped to "undefined" by the recursive constructor *) + (new_offset, Node (intrs @ undefs)) + end + (* extends the interpretation for a constructor (both *) + (* recursive and non-recursive) obtained at depth n (n>=1) *) + (* to depth n+1 *) + (* int * DatatypeAux.dtyp list * interpretation + -> int * interpretation *) + fun extend_constr (offset, [], Leaf xs) = + 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 *) + val k = find_index_eq True xs + in + if k=(~1) then + (* if the element was mapped to "undefined" before, *) + (* map it to the value given by 'offset' now (and *) + (* extend the length of the leaf) *) + (offset+1, unit_vector (offset+1, total)) + else + (* if the element was already mapped to a defined *) + (* value, map it to the same value again, just *) + (* extend the length of the leaf, do not increment *) + (* the 'offset' *) + (offset, unit_vector (k+1, total)) + end + | extend_constr (_, [], Node _) = + raise REFUTE ("IDT_constructor_interpreter", + "interpretation for constructor (with no arguments left)" + ^ " is a node") + | extend_constr (offset, d::ds, Node xs) = + let + (* compute the size of the type 'd' *) + val T = typ_of_dtyp descr typ_assoc d + val (i, _, _) = interpret thy (typs, []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", T)) + val size = size_of_type i + (* sanity check *) + val _ = if size < length xs then + raise REFUTE ("IDT_constructor_interpreter", + "new size of type is less than old size") + else () + (* extend the existing interpretations *) + (* int * interpretation list *) + val (new_offset, intrs) = foldl_map (fn (off, i) => + extend_constr (off, ds, i)) (offset, xs) + (* new elements of the type 'd' are mapped to *) + (* "undefined" *) + val undefs = replicate (size - length xs) (make_undef ds) + in + (new_offset, Node (intrs @ undefs)) + end + | extend_constr (_, d::ds, Leaf _) = + raise REFUTE ("IDT_constructor_interpreter", + "interpretation for constructor (with arguments left)" + ^ " is a leaf") + (* returns 'true' iff the constructor has a recursive *) + (* argument *) + (* DatatypeAux.dtyp list -> bool *) + fun is_rec_constr ds = + Library.exists DatatypeAux.is_rec_type ds + (* constructors before 'Const (s, T)' generate elements of *) + (* the datatype *) + val offset = size_of_dtyp thy typs' descr typ_assoc constrs1 + in + case depth of + NONE => (* equivalent to a depth of 1 *) + SOME (snd (make_constr (offset, ctypes)), model, args) + | SOME 0 => + raise REFUTE ("IDT_constructor_interpreter", "depth is 0") + | SOME 1 => + SOME (snd (make_constr (offset, ctypes)), model, args) + | SOME n => (* n > 1 *) + let + (* interpret the constructor at depth-1 *) + val (iC, _, _) = interpret thy (typs', []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Const (s, T)) + (* elements generated by the constructor at depth-1 *) + (* must be added to 'offset' *) + (* interpretation -> int *) + fun number_of_defined_elements (Leaf xs) = + if find_index_eq True xs = (~1) then 0 else 1 + | number_of_defined_elements (Node xs) = + sum (map number_of_defined_elements xs) + (* int *) + val offset' = offset + number_of_defined_elements iC + in + SOME (snd (extend_constr (offset', ctypes, iC)), model, + args) + end + end + end + | 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) + 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) => - (* iterate over all datatypes in 'thy' *) - Symtab.fold (fn (_, info) => fn result => - case result of - SOME _ => - result (* just keep 'result' *) - | NONE => - if member (op =) (#rec_names info) s then - (* we do have a recursion operator of the datatype given by *) - (* 'info', or of a mutually recursive datatype *) - let - val index = #index info - val descr = #descr info - val (dtname, dtyps, _) = lookup descr index - (* number of all constructors, including those of different *) - (* (mutually recursive) datatypes within the same descriptor *) - (* 'descr' *) - val mconstrs_count = sum (map (fn (_, (_, _, cs)) => length cs) - descr) - val params_count = length params - (* the type of a recursion operator: *) - (* [T1, ..., Tn, IDT] ---> Tresult *) - val IDT = List.nth (binder_types T, mconstrs_count) - in - if (fst o dest_Type) IDT <> dtname then - (* recursion operator of a mutually recursive datatype *) - NONE - else if mconstrs_count < params_count then - (* too many actual parameters; for now we'll use the *) - (* 'stlc_interpreter' to strip off one application *) - NONE - else if mconstrs_count > params_count 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 - params_count))) - else (* mconstrs_count = params_count *) - let - (* interpret each parameter separately *) - val ((model', args'), p_intrs) = foldl_map (fn ((m, a), p) => - let - val (i, m', a') = interpret thy m a p - in - ((m', a'), i) - end) ((model, args), params) - val (typs, _) = model' - val typ_assoc = dtyps ~~ (snd o dest_Type) IDT - (* 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 - (DatatypeAux.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 - (* the recursion operator is a function that maps every *) - (* element of the inductive datatype (and of mutually *) - (* recursive types) to an element of some result type; an *) - (* array entry of NONE means that the actual result has *) - (* not been computed yet *) - (* (int * interpretation option Array.array) list *) - val INTRS = map (fn (idx, _) => - let - val T = typ_of_dtyp descr typ_assoc - (DatatypeAux.DtRec idx) - val (i, _, _) = interpret thy (typs, []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", T)) - val size = size_of_type i - in - (idx, Array.array (size, NONE)) - end) descr - (* 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_eq True xs = elem then - SOME [] - else - NONE - | get_args (Node xs) elem = - let - (* interpretation * 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 element " - ^ string_of_int elem ^ " in datatype " - ^ Sign.string_of_typ thy IDT ^ " (datatype index " - ^ string_of_int idx ^ ")") - | 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, lookup mc_intrs idx) - end - (* returns the number of constructors in datatypes that *) - (* occur in the descriptor 'descr' before the datatype *) - (* given by 'idx' *) - fun get_coffset idx = - let - fun get_coffset_acc _ [] = - raise REFUTE ("IDT_recursion_interpreter", "index " - ^ string_of_int idx ^ " not found in descriptor") - | get_coffset_acc sum ((i, (_, _, cs))::descr') = - if i=idx then - sum - else - get_coffset_acc (sum + length cs) descr' - in - get_coffset_acc 0 descr - end - (* computes one entry in INTRS, 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 = - case Array.sub (lookup INTRS idx, elem) of - SOME result => - (* simply return the previously computed result *) - result - | NONE => - let - (* int * int list *) - val (c, args) = get_cargs idx elem - (* interpretation * int list -> interpretation *) - fun select_subtree (tr, []) = - tr (* return the whole tree *) - | select_subtree (Leaf _, _) = - raise REFUTE ("IDT_recursion_interpreter", - "interpretation for parameter is a leaf; " - ^ "cannot select a subtree") - | select_subtree (Node tr, x::xs) = - select_subtree (List.nth (tr, x), xs) - (* select the correct subtree of the parameter *) - (* corresponding to constructor 'c' *) - val p_intr = select_subtree (List.nth - (p_intrs, get_coffset idx + c), args) - (* find the indices of the constructor's recursive *) - (* arguments *) - val (_, _, constrs) = lookup descr idx - val constr_args = (snd o List.nth) (constrs, c) - val rec_args = List.filter - (DatatypeAux.is_rec_type o fst) (constr_args ~~ args) - val rec_args' = map (fn (dtyp, elem) => - (DatatypeAux.dest_DtRec dtyp, elem)) rec_args - (* apply 'p_intr' to recursively computed results *) - val result = foldl (fn ((idx, elem), intr) => - interpretation_apply (intr, - compute_array_entry idx elem)) p_intr rec_args' - (* update 'INTRS' *) - val _ = Array.update (lookup INTRS idx, elem, - SOME result) - in - result - end - (* compute all entries in INTRS for the current datatype *) - (* (given by 'index') *) - (* TODO: we can use Array.modifyi instead once PolyML's *) - (* Array signature conforms to the ML standard *) - (* (int * 'a -> 'a) -> 'a array -> unit *) - fun modifyi f arr = - let - val size = Array.length arr - fun modifyi_loop i = - if i < size then ( - Array.update (arr, i, f (i, Array.sub (arr, i))); - modifyi_loop (i+1) - ) else - () - in - modifyi_loop 0 - end - val _ = modifyi (fn (i, _) => - SOME (compute_array_entry index i)) (lookup INTRS index) - (* 'a Array.array -> 'a list *) - fun toList arr = - Array.foldr op:: [] arr - in - (* return the part of 'INTRS' that corresponds to the *) - (* current datatype *) - SOME ((Node o map Option.valOf o toList o lookup INTRS) - index, model', args') - end - end - else - NONE (* not a recursion operator of this datatype *) - ) (DatatypePackage.get_datatypes thy) NONE - | _ => (* head of term is not a constant *) - NONE; + 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' *) + | NONE => + if member (op =) (#rec_names info) s then + (* we do have a recursion operator of the datatype given by *) + (* 'info', or of a mutually recursive datatype *) + let + val index = #index info + val descr = #descr info + val (dtname, dtyps, _) = lookup descr index + (* number of all constructors, including those of different *) + (* (mutually recursive) datatypes within the same descriptor *) + (* 'descr' *) + val mconstrs_count = sum (map (fn (_, (_, _, cs)) => length cs) + descr) + val params_count = length params + (* the type of a recursion operator: *) + (* [T1, ..., Tn, IDT] ---> Tresult *) + val IDT = List.nth (binder_types T, mconstrs_count) + in + if (fst o dest_Type) IDT <> dtname then + (* recursion operator of a mutually recursive datatype *) + NONE + else if mconstrs_count < params_count then + (* too many actual parameters; for now we'll use the *) + (* 'stlc_interpreter' to strip off one application *) + NONE + else if mconstrs_count > params_count 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 - params_count))) + else (* mconstrs_count = params_count *) + let + (* interpret each parameter separately *) + val ((model', args'), p_intrs) = foldl_map (fn ((m, a), p) => + let + val (i, m', a') = interpret thy m a p + in + ((m', a'), i) + end) ((model, args), params) + val (typs, _) = model' + val typ_assoc = dtyps ~~ (snd o dest_Type) IDT + (* 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 + (DatatypeAux.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 + (* the recursion operator is a function that maps every *) + (* element of the inductive datatype (and of mutually *) + (* recursive types) to an element of some result type; an *) + (* array entry of NONE means that the actual result has *) + (* not been computed yet *) + (* (int * interpretation option Array.array) list *) + val INTRS = map (fn (idx, _) => + let + val T = typ_of_dtyp descr typ_assoc + (DatatypeAux.DtRec idx) + val (i, _, _) = interpret thy (typs, []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", T)) + val size = size_of_type i + in + (idx, Array.array (size, NONE)) + end) descr + (* 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_eq True xs = elem then + SOME [] + else + NONE + | get_args (Node xs) elem = + let + (* interpretation * 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 element " + ^ string_of_int elem ^ " in datatype " + ^ Sign.string_of_typ thy IDT ^ " (datatype index " + ^ string_of_int idx ^ ")") + | 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, lookup mc_intrs idx) + end + (* returns the number of constructors in datatypes that *) + (* occur in the descriptor 'descr' before the datatype *) + (* given by 'idx' *) + fun get_coffset idx = + let + fun get_coffset_acc _ [] = + raise REFUTE ("IDT_recursion_interpreter", "index " + ^ string_of_int idx ^ " not found in descriptor") + | get_coffset_acc sum ((i, (_, _, cs))::descr') = + if i=idx then + sum + else + get_coffset_acc (sum + length cs) descr' + in + get_coffset_acc 0 descr + end + (* computes one entry in INTRS, 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 = + case Array.sub (lookup INTRS idx, elem) of + SOME result => + (* simply return the previously computed result *) + result + | NONE => + let + (* int * int list *) + val (c, args) = get_cargs idx elem + (* interpretation * int list -> interpretation *) + fun select_subtree (tr, []) = + tr (* return the whole tree *) + | select_subtree (Leaf _, _) = + raise REFUTE ("IDT_recursion_interpreter", + "interpretation for parameter is a leaf; " + ^ "cannot select a subtree") + | select_subtree (Node tr, x::xs) = + select_subtree (List.nth (tr, x), xs) + (* select the correct subtree of the parameter *) + (* corresponding to constructor 'c' *) + val p_intr = select_subtree (List.nth + (p_intrs, get_coffset idx + c), args) + (* find the indices of the constructor's recursive *) + (* arguments *) + val (_, _, constrs) = lookup descr idx + val constr_args = (snd o List.nth) (constrs, c) + val rec_args = List.filter + (DatatypeAux.is_rec_type o fst) (constr_args ~~ args) + val rec_args' = map (fn (dtyp, elem) => + (DatatypeAux.dest_DtRec dtyp, elem)) rec_args + (* apply 'p_intr' to recursively computed results *) + val result = foldl (fn ((idx, elem), intr) => + interpretation_apply (intr, + compute_array_entry idx elem)) p_intr rec_args' + (* update 'INTRS' *) + val _ = Array.update (lookup INTRS idx, elem, + SOME result) + in + result + end + (* compute all entries in INTRS for the current datatype *) + (* (given by 'index') *) + (* TODO: we can use Array.modifyi instead once PolyML's *) + (* Array signature conforms to the ML standard *) + (* (int * 'a -> 'a) -> 'a array -> unit *) + fun modifyi f arr = + let + val size = Array.length arr + fun modifyi_loop i = + if i < size then ( + Array.update (arr, i, f (i, Array.sub (arr, i))); + modifyi_loop (i+1) + ) else + () + in + modifyi_loop 0 + end + val _ = modifyi (fn (i, _) => + SOME (compute_array_entry index i)) (lookup INTRS index) + (* 'a Array.array -> 'a list *) + fun toList arr = + Array.foldr op:: [] arr + in + (* return the part of 'INTRS' that corresponds to the *) + (* current datatype *) + SOME ((Node o map Option.valOf o toList o lookup INTRS) + index, model', args') + end + end + else + NONE (* not a recursion operator of this datatype *) + ) (DatatypePackage.get_datatypes thy) 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 *) - (* 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 ("Finite_Set.card", - Type ("fun", [Type ("set", [T]), Type ("nat", [])])) => - let - val (i_nat, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", Type ("nat", []))) - val size_nat = size_of_type i_nat - val (i_set, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", Type ("set", [T]))) - val constants = make_constants i_set - (* interpretation -> int *) - fun number_of_elements (Node xs) = - Library.foldl (fn (n, x) => - if x=TT then - n+1 - else if x=FF then - n - else - raise REFUTE ("Finite_Set_card_interpreter", - "interpretation for set type does not yield a Boolean")) - (0, xs) - | number_of_elements (Leaf _) = - raise REFUTE ("Finite_Set_card_interpreter", - "interpretation for set type is a leaf") - (* takes an interpretation for a set and returns an interpretation *) - (* for a 'nat' *) - (* interpretation -> interpretation *) - fun card i = - let - val n = number_of_elements i - in - if n - NONE; + fun Finite_Set_card_interpreter thy model args t = + case t of + Const ("Finite_Set.card", + Type ("fun", [Type ("set", [T]), Type ("nat", [])])) => + let + val (i_nat, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", Type ("nat", []))) + val size_nat = size_of_type i_nat + val (i_set, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", Type ("set", [T]))) + val constants = make_constants i_set + (* interpretation -> int *) + fun number_of_elements (Node xs) = + Library.foldl (fn (n, x) => + if x=TT then + n+1 + else if x=FF then + n + else + raise REFUTE ("Finite_Set_card_interpreter", + "interpretation for set type does not yield a Boolean")) + (0, xs) + | number_of_elements (Leaf _) = + raise REFUTE ("Finite_Set_card_interpreter", + "interpretation for set type is a leaf") + (* takes an interpretation for a set and returns an interpretation *) + (* for a 'nat' *) + (* interpretation -> interpretation *) + fun card i = + let + val n = number_of_elements i + in + if n + NONE; - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) + (* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) - (* only an optimization: 'Finites' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) + (* only an optimization: 'Finites' could in principle be interpreted with *) + (* interpreters available already (using its definition), but the code *) + (* below is more efficient *) - fun Finite_Set_Finites_interpreter thy model args t = - case t of - Const ("Finite_Set.Finites", Type ("set", [Type ("set", [T])])) => - let - val (i_set, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", Type ("set", [T]))) - val size_set = size_of_type i_set - in - (* we only consider finite models anyway, hence EVERY set is in *) - (* "Finites" *) - SOME (Node (replicate size_set TT), model, args) - end - | _ => - NONE; + fun Finite_Set_Finites_interpreter thy model args t = + case t of + Const ("Finite_Set.Finites", Type ("set", [Type ("set", [T])])) => + let + val (i_set, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", Type ("set", [T]))) + val size_set = size_of_type i_set + in + (* we only consider finite models anyway, hence EVERY set is in *) + (* "Finites" *) + SOME (Node (replicate size_set TT), 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: '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 ("Finite_Set.finite", - Type ("fun", [Type ("set", [T]), Type ("bool", [])])) $ _ => - (* we only consider finite models anyway, hence EVERY set is *) - (* "finite" *) - SOME (TT, model, args) - | Const ("Finite_Set.finite", - Type ("fun", [Type ("set", [T]), Type ("bool", [])])) => - let - val (i_set, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", Type ("set", [T]))) - val size_set = size_of_type i_set - in - (* we only consider finite models anyway, hence EVERY set is *) - (* "finite" *) - SOME (Node (replicate size_set TT), model, args) - end - | _ => - NONE; + fun Finite_Set_finite_interpreter thy model args t = + case t of + Const ("Finite_Set.finite", + Type ("fun", [Type ("set", [T]), Type ("bool", [])])) $ _ => + (* we only consider finite models anyway, hence EVERY set is *) + (* "finite" *) + SOME (TT, model, args) + | Const ("Finite_Set.finite", + Type ("fun", [Type ("set", [T]), Type ("bool", [])])) => + let + val (i_set, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", Type ("set", [T]))) + val size_set = size_of_type i_set + in + (* we only consider finite models anyway, hence EVERY set is *) + (* "finite" *) + SOME (Node (replicate size_set TT), 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: 'Orderings.less' could in principle be *) - (* interpreted with interpreters available already (using its definition), *) - (* but the code below is more efficient *) + (* only an optimization: 'Orderings.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 ("Orderings.less", Type ("fun", [Type ("nat", []), - Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => - let - val (i_nat, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", Type ("nat", []))) - val size_nat = size_of_type i_nat - (* int -> interpretation *) - (* the 'n'-th nat is not less than the first 'n' nats, while it *) - (* is less than the remaining 'size_nat - n' nats *) - fun less n = Node ((replicate n FF) @ (replicate (size_nat - n) TT)) - in - SOME (Node (map less (1 upto size_nat)), model, args) - end - | _ => - NONE; + fun Nat_less_interpreter thy model args t = + case t of + Const ("Orderings.less", Type ("fun", [Type ("nat", []), + Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => + let + val (i_nat, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", Type ("nat", []))) + val size_nat = size_of_type i_nat + (* int -> interpretation *) + (* the 'n'-th nat is not less than the first 'n' nats, while it *) + (* is less than the remaining 'size_nat - n' nats *) + fun less n = Node ((replicate n FF) @ (replicate (size_nat - n) TT)) + in + SOME (Node (map less (1 upto size_nat)), 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: 'HOL.plus' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) + (* only an optimization: 'HOL.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 ("HOL.plus", Type ("fun", [Type ("nat", []), - Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => - let - val (i_nat, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", Type ("nat", []))) - val size_nat = size_of_type i_nat - (* int -> int -> interpretation *) - fun plus m n = - let - val element = (m+n)+1 - in - if element > size_nat then - Leaf (replicate size_nat False) - else - Leaf ((replicate (element-1) False) @ True :: - (replicate (size_nat - element) False)) - end - in - SOME (Node (map (fn m => Node (map (plus m) (0 upto size_nat-1))) - (0 upto size_nat-1)), model, args) - end - | _ => - NONE; + fun Nat_plus_interpreter thy model args t = + case t of + Const ("HOL.plus", Type ("fun", [Type ("nat", []), + Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => + let + val (i_nat, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", Type ("nat", []))) + val size_nat = size_of_type i_nat + (* int -> int -> interpretation *) + fun plus m n = + let + val element = (m+n)+1 + in + if element > size_nat then + Leaf (replicate size_nat False) + else + Leaf ((replicate (element-1) False) @ True :: + (replicate (size_nat - element) False)) + end + in + SOME (Node (map (fn m => Node (map (plus m) (0 upto size_nat-1))) + (0 upto size_nat-1)), 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: 'HOL.minus' could in principle be interpreted *) - (* with interpreters available already (using its definition), but the *) - (* code below is more efficient *) + (* only an optimization: 'HOL.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 ("HOL.minus", Type ("fun", [Type ("nat", []), - Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => - let - val (i_nat, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", Type ("nat", []))) - val size_nat = size_of_type i_nat - (* int -> int -> interpretation *) - fun minus m n = - let - val element = Int.max (m-n, 0) + 1 - in - Leaf ((replicate (element-1) False) @ True :: - (replicate (size_nat - element) False)) - end - in - SOME (Node (map (fn m => Node (map (minus m) (0 upto size_nat-1))) - (0 upto size_nat-1)), model, args) - end - | _ => - NONE; + fun Nat_minus_interpreter thy model args t = + case t of + Const ("HOL.minus", Type ("fun", [Type ("nat", []), + Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => + let + val (i_nat, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", Type ("nat", []))) + val size_nat = size_of_type i_nat + (* int -> int -> interpretation *) + fun minus m n = + let + val element = Int.max (m-n, 0) + 1 + in + Leaf ((replicate (element-1) False) @ True :: + (replicate (size_nat - element) False)) + end + in + SOME (Node (map (fn m => Node (map (minus m) (0 upto size_nat-1))) + (0 upto size_nat-1)), 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: 'HOL.times' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) + (* only an optimization: 'HOL.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 ("HOL.times", Type ("fun", [Type ("nat", []), - Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => - let - val (i_nat, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", Type ("nat", []))) - val size_nat = size_of_type i_nat - (* nat -> nat -> interpretation *) - fun mult m n = - let - val element = (m*n)+1 - in - if element > size_nat then - Leaf (replicate size_nat False) - else - Leaf ((replicate (element-1) False) @ True :: - (replicate (size_nat - element) False)) - end - in - SOME (Node (map (fn m => Node (map (mult m) (0 upto size_nat-1))) - (0 upto size_nat-1)), model, args) - end - | _ => - NONE; + fun Nat_times_interpreter thy model args t = + case t of + Const ("HOL.times", Type ("fun", [Type ("nat", []), + Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => + let + val (i_nat, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", Type ("nat", []))) + val size_nat = size_of_type i_nat + (* nat -> nat -> interpretation *) + fun mult m n = + let + val element = (m*n)+1 + in + if element > size_nat then + Leaf (replicate size_nat False) + else + Leaf ((replicate (element-1) False) @ True :: + (replicate (size_nat - element) False)) + end + in + SOME (Node (map (fn m => Node (map (mult m) (0 upto size_nat-1))) + (0 upto size_nat-1)), 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: 'op @' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) + (* only an optimization: 'op @' 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 ("List.op @", Type ("fun", [Type ("List.list", [T]), Type ("fun", - [Type ("List.list", [_]), Type ("List.list", [_])])])) => - let - val (i_elem, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", T)) - val size_elem = size_of_type i_elem - val (i_list, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", Type ("List.list", [T]))) - val size_list = size_of_type i_list - (* power (a, b) computes a^b, for a>=0, b>=0 *) - (* int * int -> int *) - fun power (a, 0) = 1 - | power (a, 1) = a - | power (a, b) = - let val ab = power(a, b div 2) in ab * ab * power(a, b mod 2) end - (* log (a, b) computes floor(log_a(b)), i.e. the largest integer x *) - (* s.t. a^x <= b, for a>=2, b>=1 *) - (* int * int -> int *) - fun log (a, b) = - let - fun logloop (ax, x) = - if ax > b then x-1 else logloop (a * ax, x+1) - in - logloop (1, 0) - end - (* nat -> nat -> interpretation *) - fun append m n = - let - (* The following formula depends on the order in which lists are *) - (* enumerated by the 'IDT_constructor_interpreter'. It took me *) - (* a little while to come up with this formula. *) - val element = n + m * (if size_elem = 1 then 1 - else power (size_elem, log (size_elem, n+1))) + 1 - in - if element > size_list then - Leaf (replicate size_list False) - else - Leaf ((replicate (element-1) False) @ True :: - (replicate (size_list - element) False)) - end - in - SOME (Node (map (fn m => Node (map (append m) (0 upto size_list-1))) - (0 upto size_list-1)), model, args) - end - | _ => - NONE; + fun List_append_interpreter thy model args t = + case t of + Const ("List.op @", Type ("fun", [Type ("List.list", [T]), Type ("fun", + [Type ("List.list", [_]), Type ("List.list", [_])])])) => + let + val (i_elem, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", T)) + val size_elem = size_of_type i_elem + val (i_list, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", Type ("List.list", [T]))) + val size_list = size_of_type i_list + (* power (a, b) computes a^b, for a>=0, b>=0 *) + (* int * int -> int *) + fun power (a, 0) = 1 + | power (a, 1) = a + | power (a, b) = + let val ab = power(a, b div 2) in ab * ab * power(a, b mod 2) end + (* log (a, b) computes floor(log_a(b)), i.e. the largest integer x *) + (* s.t. a^x <= b, for a>=2, b>=1 *) + (* int * int -> int *) + fun log (a, b) = + let + fun logloop (ax, x) = + if ax > b then x-1 else logloop (a * ax, x+1) + in + logloop (1, 0) + end + (* nat -> nat -> interpretation *) + fun append m n = + let + (* The following formula depends on the order in which lists are *) + (* enumerated by the 'IDT_constructor_interpreter'. It took me *) + (* a little while to come up with this formula. *) + val element = n + m * (if size_elem = 1 then 1 + else power (size_elem, log (size_elem, n+1))) + 1 + in + if element > size_list then + Leaf (replicate size_list False) + else + Leaf ((replicate (element-1) False) @ True :: + (replicate (size_list - element) False)) + end + in + SOME (Node (map (fn m => Node (map (append m) (0 upto size_list-1))) + (0 upto size_list-1)), 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: '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_lfp_interpreter thy model args t = - case t of - Const ("Lfp.lfp", Type ("fun", [Type ("fun", - [Type ("set", [T]), Type ("set", [_])]), Type ("set", [_])])) => - let - val (i_elem, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", T)) - val size_elem = size_of_type i_elem - (* 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_set, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", Type ("set", [T]))) - val i_sets = make_constants i_set - (* all functions that map sets to sets *) - val (i_fun, _, _) = interpret thy model {maxvars=0, def_eq=false, - next_idx=1, bounds=[], wellformed=True} (Free ("dummy", - Type ("fun", [Type ("set", [T]), Type ("set", [T])]))) - val i_funs = make_constants i_fun - (* "lfp(f) == Inter({u. f(u) <= u})" *) - (* interpretation * interpretation -> bool *) - fun is_subset (Node subs, Node sups) = - List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT)) - (subs ~~ sups) - | is_subset (_, _) = - raise REFUTE ("Lfp_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)) - | intersection (_, _) = - raise REFUTE ("Lfp_lfp_interpreter", - "intersection: interpretation for set is not a node") - (* interpretation -> interpretaion *) - fun lfp (Node resultsets) = - foldl (fn ((set, resultset), acc) => - if is_subset (resultset, set) then - intersection (acc, set) - else - acc) i_univ (i_sets ~~ resultsets) - | lfp _ = - raise REFUTE ("Lfp_lfp_interpreter", - "lfp: interpretation for function is not a node") - in - SOME (Node (map lfp i_funs), model, args) - end - | _ => - NONE; + fun Lfp_lfp_interpreter thy model args t = + case t of + Const ("Lfp.lfp", Type ("fun", [Type ("fun", + [Type ("set", [T]), Type ("set", [_])]), Type ("set", [_])])) => + let + val (i_elem, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", T)) + val size_elem = size_of_type i_elem + (* 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_set, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", Type ("set", [T]))) + val i_sets = make_constants i_set + (* all functions that map sets to sets *) + val (i_fun, _, _) = interpret thy model {maxvars=0, def_eq=false, + next_idx=1, bounds=[], wellformed=True} (Free ("dummy", + Type ("fun", [Type ("set", [T]), Type ("set", [T])]))) + val i_funs = make_constants i_fun + (* "lfp(f) == Inter({u. f(u) <= u})" *) + (* interpretation * interpretation -> bool *) + fun is_subset (Node subs, Node sups) = + List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT)) + (subs ~~ sups) + | is_subset (_, _) = + raise REFUTE ("Lfp_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)) + | intersection (_, _) = + raise REFUTE ("Lfp_lfp_interpreter", + "intersection: interpretation for set is not a node") + (* interpretation -> interpretaion *) + fun lfp (Node resultsets) = + foldl (fn ((set, resultset), acc) => + if is_subset (resultset, set) then + intersection (acc, set) + else + acc) i_univ (i_sets ~~ resultsets) + | lfp _ = + raise REFUTE ("Lfp_lfp_interpreter", + "lfp: interpretation for function is not a node") + in + SOME (Node (map lfp 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: '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_gfp_interpreter thy model args t = - case t of - Const ("Gfp.gfp", Type ("fun", [Type ("fun", - [Type ("set", [T]), Type ("set", [_])]), Type ("set", [_])])) => - let nonfix union (* because "union" is used below *) - val (i_elem, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", T)) - val size_elem = size_of_type i_elem - (* 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_set, _, _) = interpret thy model - {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", Type ("set", [T]))) - val i_sets = make_constants i_set - (* all functions that map sets to sets *) - val (i_fun, _, _) = interpret thy model {maxvars=0, def_eq=false, - next_idx=1, bounds=[], wellformed=True} (Free ("dummy", - Type ("fun", [Type ("set", [T]), Type ("set", [T])]))) - val i_funs = make_constants i_fun - (* "gfp(f) == Union({u. u <= f(u)})" *) - (* interpretation * interpretation -> bool *) - fun is_subset (Node subs, Node sups) = - List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT)) - (subs ~~ sups) - | is_subset (_, _) = - raise REFUTE ("Gfp_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_gfp_interpreter", - "union: interpretation for set is not a node") - (* interpretation -> interpretaion *) - fun gfp (Node resultsets) = - foldl (fn ((set, resultset), acc) => - if is_subset (set, resultset) then - union (acc, set) - else - acc) i_univ (i_sets ~~ resultsets) - | gfp _ = - raise REFUTE ("Gfp_gfp_interpreter", - "gfp: interpretation for function is not a node") - in - SOME (Node (map gfp i_funs), model, args) - end - | _ => - NONE; + fun Gfp_gfp_interpreter thy model args t = + case t of + Const ("Gfp.gfp", Type ("fun", [Type ("fun", + [Type ("set", [T]), Type ("set", [_])]), Type ("set", [_])])) => + let nonfix union (* because "union" is used below *) + val (i_elem, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", T)) + val size_elem = size_of_type i_elem + (* 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_set, _, _) = interpret thy model + {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", Type ("set", [T]))) + val i_sets = make_constants i_set + (* all functions that map sets to sets *) + val (i_fun, _, _) = interpret thy model {maxvars=0, def_eq=false, + next_idx=1, bounds=[], wellformed=True} (Free ("dummy", + Type ("fun", [Type ("set", [T]), Type ("set", [T])]))) + val i_funs = make_constants i_fun + (* "gfp(f) == Union({u. u <= f(u)})" *) + (* interpretation * interpretation -> bool *) + fun is_subset (Node subs, Node sups) = + List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT)) + (subs ~~ sups) + | is_subset (_, _) = + raise REFUTE ("Gfp_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_gfp_interpreter", + "union: interpretation for set is not a node") + (* interpretation -> interpretaion *) + fun gfp (Node resultsets) = + foldl (fn ((set, resultset), acc) => + if is_subset (set, resultset) then + union (acc, set) + else + acc) i_univ (i_sets ~~ resultsets) + | gfp _ = + raise REFUTE ("Gfp_gfp_interpreter", + "gfp: interpretation for function is not a node") + 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 ("fst", Type ("fun", [Type ("*", [T, U]), _])) => - let - val (iT, _, _) = interpret thy model {maxvars=0, def_eq=false, - next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) - val is_T = make_constants iT - val (iU, _, _) = interpret thy model {maxvars=0, def_eq=false, - next_idx=1, bounds=[], wellformed=True} (Free ("dummy", U)) - val size_U = size_of_type iU - in - SOME (Node (List.concat (map (replicate size_U) is_T)), model, args) - end - | _ => - NONE; + fun Product_Type_fst_interpreter thy model args t = + case t of + Const ("fst", Type ("fun", [Type ("*", [T, U]), _])) => + let + val (iT, _, _) = interpret thy model {maxvars=0, def_eq=false, + next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) + val is_T = make_constants iT + val (iU, _, _) = interpret thy model {maxvars=0, def_eq=false, + next_idx=1, bounds=[], wellformed=True} (Free ("dummy", U)) + val size_U = size_of_type iU + in + SOME (Node (List.concat (map (replicate size_U) is_T)), 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: '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 ("snd", Type ("fun", [Type ("*", [T, U]), _])) => - let - val (iT, _, _) = interpret thy model {maxvars=0, def_eq=false, - next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) - val size_T = size_of_type iT - val (iU, _, _) = interpret thy model {maxvars=0, def_eq=false, - next_idx=1, bounds=[], wellformed=True} (Free ("dummy", U)) - val is_U = make_constants iU - in - SOME (Node (List.concat (replicate size_T is_U)), model, args) - end - | _ => - NONE; + fun Product_Type_snd_interpreter thy model args t = + case t of + Const ("snd", Type ("fun", [Type ("*", [T, U]), _])) => + let + val (iT, _, _) = interpret thy model {maxvars=0, def_eq=false, + next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) + val size_T = size_of_type iT + val (iU, _, _) = interpret thy model {maxvars=0, def_eq=false, + next_idx=1, bounds=[], wellformed=True} (Free ("dummy", U)) + val is_U = make_constants iU + in + SOME (Node (List.concat (replicate size_T is_U)), model, args) + end + | _ => + NONE; (* ------------------------------------------------------------------------- *) (* PRINTERS *) (* ------------------------------------------------------------------------- *) - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> - Term.term option *) + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> + Term.term option *) - fun stlc_printer thy model t intr assignment = - let - (* Term.term -> Term.typ option *) - fun typeof (Free (_, T)) = SOME T - | typeof (Var (_, T)) = SOME T - | typeof (Const (_, T)) = SOME T - | typeof _ = NONE - (* string -> string *) - fun strip_leading_quote s = - (implode o (fn [] => [] | 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 - | string_of_typ (TVar ((x,i), _)) = - strip_leading_quote x ^ string_of_int i - (* interpretation -> int *) - fun index_from_interpretation (Leaf xs) = - find_index (PropLogic.eval assignment) xs - | index_from_interpretation _ = - raise REFUTE ("stlc_printer", - "interpretation for ground type is not a leaf") - in - case typeof t of - SOME T => - (case T of - Type ("fun", [T1, T2]) => - let - (* create all constants of type 'T1' *) - val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, - next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1)) - val constants = make_constants i - (* interpretation list *) - val results = (case intr of - Node xs => xs - | _ => raise REFUTE ("stlc_printer", - "interpretation for function type is a leaf")) - (* Term.term list *) - val pairs = map (fn (arg, result) => - HOLogic.mk_prod - (print thy model (Free ("dummy", T1)) arg assignment, - print thy model (Free ("dummy", T2)) result assignment)) - (constants ~~ results) - (* Term.typ *) - val HOLogic_prodT = HOLogic.mk_prodT (T1, T2) - val HOLogic_setT = HOLogic.mk_setT HOLogic_prodT - (* Term.term *) - val HOLogic_empty_set = Const ("{}", HOLogic_setT) - val HOLogic_insert = - Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) - in - SOME (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) - HOLogic_empty_set pairs) - end - | Type ("prop", []) => - (case index_from_interpretation intr of - ~1 => SOME (HOLogic.mk_Trueprop (Const ("arbitrary", 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 ("arbitrary", 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 ("arbitrary", 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 ("arbitrary", T)) - else - SOME (Const (string_of_typ T ^ - string_of_int (index_from_interpretation intr), T))) - | NONE => - NONE - end; + fun stlc_printer thy model t intr assignment = + let + (* Term.term -> Term.typ option *) + fun typeof (Free (_, T)) = SOME T + | typeof (Var (_, T)) = SOME T + | typeof (Const (_, T)) = SOME T + | typeof _ = NONE + (* string -> string *) + fun strip_leading_quote s = + (implode o (fn [] => [] | 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 + | string_of_typ (TVar ((x,i), _)) = + strip_leading_quote x ^ string_of_int i + (* interpretation -> int *) + fun index_from_interpretation (Leaf xs) = + find_index (PropLogic.eval assignment) xs + | index_from_interpretation _ = + raise REFUTE ("stlc_printer", + "interpretation for ground type is not a leaf") + in + case typeof t of + SOME T => + (case T of + Type ("fun", [T1, T2]) => + let + (* create all constants of type 'T1' *) + val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, + next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1)) + val constants = make_constants i + (* interpretation list *) + val results = (case intr of + Node xs => xs + | _ => raise REFUTE ("stlc_printer", + "interpretation for function type is a leaf")) + (* Term.term list *) + val pairs = map (fn (arg, result) => + HOLogic.mk_prod + (print thy model (Free ("dummy", T1)) arg assignment, + print thy model (Free ("dummy", T2)) result assignment)) + (constants ~~ results) + (* Term.typ *) + val HOLogic_prodT = HOLogic.mk_prodT (T1, T2) + val HOLogic_setT = HOLogic.mk_setT HOLogic_prodT + (* Term.term *) + val HOLogic_empty_set = Const ("{}", HOLogic_setT) + val HOLogic_insert = + Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) + in + SOME (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) + HOLogic_empty_set pairs) + end + | Type ("prop", []) => + (case index_from_interpretation intr of + ~1 => SOME (HOLogic.mk_Trueprop (Const ("arbitrary", 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 ("arbitrary", 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 ("arbitrary", 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 ("arbitrary", T)) + else + SOME (Const (string_of_typ T ^ + string_of_int (index_from_interpretation intr), T))) + | NONE => + NONE + end; - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> - string option *) + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> + string option *) - fun set_printer thy model t intr assignment = - let - (* Term.term -> Term.typ option *) - fun typeof (Free (_, T)) = SOME T - | typeof (Var (_, T)) = SOME T - | typeof (Const (_, T)) = SOME T - | typeof _ = NONE - in - case typeof t of - SOME (Type ("set", [T])) => - let - (* create all constants of type 'T' *) - val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, - next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) - val constants = make_constants i - (* interpretation list *) - val results = (case intr of - Node xs => xs - | _ => raise REFUTE ("set_printer", - "interpretation for set type is a leaf")) - (* Term.term list *) - val elements = List.mapPartial (fn (arg, result) => - case result of - Leaf [fmTrue, fmFalse] => - if PropLogic.eval assignment fmTrue then - SOME (print thy model (Free ("dummy", T)) arg assignment) - else (* if PropLogic.eval assignment fmFalse then *) - NONE - | _ => - raise REFUTE ("set_printer", - "illegal interpretation for a Boolean value")) - (constants ~~ results) - (* Term.typ *) - val HOLogic_setT = HOLogic.mk_setT T - (* Term.term *) - val HOLogic_empty_set = Const ("{}", HOLogic_setT) - val HOLogic_insert = - Const ("insert", T --> HOLogic_setT --> HOLogic_setT) - in - SOME (Library.foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) - (HOLogic_empty_set, elements)) - end - | _ => - NONE - end; + fun set_printer thy model t intr assignment = + let + (* Term.term -> Term.typ option *) + fun typeof (Free (_, T)) = SOME T + | typeof (Var (_, T)) = SOME T + | typeof (Const (_, T)) = SOME T + | typeof _ = NONE + in + case typeof t of + SOME (Type ("set", [T])) => + let + (* create all constants of type 'T' *) + val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, + next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) + val constants = make_constants i + (* interpretation list *) + val results = (case intr of + Node xs => xs + | _ => raise REFUTE ("set_printer", + "interpretation for set type is a leaf")) + (* Term.term list *) + val elements = List.mapPartial (fn (arg, result) => + case result of + Leaf [fmTrue, fmFalse] => + if PropLogic.eval assignment fmTrue then + SOME (print thy model (Free ("dummy", T)) arg assignment) + else (* if PropLogic.eval assignment fmFalse then *) + NONE + | _ => + raise REFUTE ("set_printer", + "illegal interpretation for a Boolean value")) + (constants ~~ results) + (* Term.typ *) + val HOLogic_setT = HOLogic.mk_setT T + (* Term.term *) + val HOLogic_empty_set = Const ("{}", HOLogic_setT) + val HOLogic_insert = + Const ("insert", T --> HOLogic_setT --> HOLogic_setT) + in + SOME (Library.foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) + (HOLogic_empty_set, elements)) + end + | _ => + NONE + end; - (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> - Term.term option *) + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> + Term.term option *) - fun IDT_printer thy model t intr assignment = - let - (* Term.term -> Term.typ option *) - fun typeof (Free (_, T)) = SOME T - | typeof (Var (_, T)) = SOME T - | typeof (Const (_, T)) = SOME T - | typeof _ = NONE - in - case typeof t of - SOME (Type (s, Ts)) => - (case DatatypePackage.get_datatype thy s of - SOME info => (* inductive datatype *) - let - val (typs, _) = model - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = lookup descr index - val typ_assoc = dtyps ~~ Ts - (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) - val _ = (if Library.exists (fn d => - case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("IDT_printer", "datatype argument (for type " ^ - Sign.string_of_typ 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 ("arbitrary", 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 *) - (* string * DatatypeAux.dtyp list -> - (Term.term * int list) option *) - fun get_constr_args (cname, cargs) = - 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_eq 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 - Option.map (fn args => (cTerm, cargs, args)) (get_args iC) - end - (* Term.term * DatatypeAux.dtyp list * int list *) - val (cTerm, cargs, args) = - (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 - val (i, _, _) = interpret thy (typs, []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], wellformed=True} - (Free ("dummy", dT)) - (* 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 i - in - print thy (typs, []) (Free ("dummy", dT)) - (List.nth (consts, n)) assignment - end) (cargs ~~ args) - in - SOME (Library.foldl op$ (cTerm, argsTerms)) - end - end - | NONE => (* not an inductive datatype *) - NONE) - | _ => (* a (free or schematic) type variable *) - NONE - end; + fun IDT_printer thy model t intr assignment = + let + (* Term.term -> Term.typ option *) + fun typeof (Free (_, T)) = SOME T + | typeof (Var (_, T)) = SOME T + | typeof (Const (_, T)) = SOME T + | typeof _ = NONE + in + case typeof t of + SOME (Type (s, Ts)) => + (case DatatypePackage.get_datatype thy s of + SOME info => (* inductive datatype *) + let + val (typs, _) = model + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = lookup descr index + val typ_assoc = dtyps ~~ Ts + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = (if Library.exists (fn d => + case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_printer", "datatype argument (for type " ^ + Sign.string_of_typ 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 ("arbitrary", 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 *) + (* string * DatatypeAux.dtyp list -> + (Term.term * int list) option *) + fun get_constr_args (cname, cargs) = + 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_eq 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 + Option.map (fn args => (cTerm, cargs, args)) (get_args iC) + end + (* Term.term * DatatypeAux.dtyp list * int list *) + val (cTerm, cargs, args) = + (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 + val (i, _, _) = interpret thy (typs, []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], wellformed=True} + (Free ("dummy", dT)) + (* 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 i + in + print thy (typs, []) (Free ("dummy", dT)) + (List.nth (consts, n)) assignment + end) (cargs ~~ args) + in + SOME (Library.foldl op$ (cTerm, argsTerms)) + end + end + | NONE => (* not an inductive datatype *) + NONE) + | _ => (* a (free or schematic) type variable *) + NONE + end; (* ------------------------------------------------------------------------- *) @@ -3207,31 +3207,31 @@ (* subterms that are then passed to other interpreters! *) (* ------------------------------------------------------------------------- *) - (* (theory -> theory) list *) + (* (theory -> theory) list *) - val setup = - RefuteData.init #> - 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.Finites" Finite_Set_Finites_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.op @" List_append_interpreter #> - add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #> - add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #> - add_interpreter "fst" Product_Type_fst_interpreter #> - add_interpreter "snd" Product_Type_snd_interpreter #> - add_printer "stlc" stlc_printer #> - add_printer "set" set_printer #> - add_printer "IDT" IDT_printer; + val setup = + RefuteData.init #> + 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.Finites" Finite_Set_Finites_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.op @" List_append_interpreter #> + add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #> + add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #> + add_interpreter "fst" Product_Type_fst_interpreter #> + add_interpreter "snd" Product_Type_snd_interpreter #> + add_printer "stlc" stlc_printer #> + add_printer "set" set_printer #> + add_printer "IDT" IDT_printer; end (* structure Refute *) diff -r 535ae9dd4c45 -r 1565d476a9e2 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Tue Apr 03 19:24:10 2007 +0200 +++ b/src/HOL/Tools/sat_solver.ML Tue Apr 03 19:24:11 2007 +0200 @@ -8,47 +8,47 @@ signature SAT_SOLVER = sig - exception NOT_CONFIGURED + exception NOT_CONFIGURED - type assignment = int -> bool option - type proof = int list Inttab.table * int - datatype result = SATISFIABLE of assignment - | UNSATISFIABLE of proof option - | UNKNOWN - type solver = PropLogic.prop_formula -> result + type assignment = int -> bool option + type proof = int list Inttab.table * int + datatype result = SATISFIABLE of assignment + | UNSATISFIABLE of proof option + | UNKNOWN + type solver = PropLogic.prop_formula -> result - (* auxiliary functions to create external SAT solvers *) - val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit - val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit - val read_std_result_file : Path.T -> string * string * string -> result - val make_external_solver : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver + (* auxiliary functions to create external SAT solvers *) + val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit + val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit + val read_std_result_file : Path.T -> string * string * string -> result + val make_external_solver : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver - val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula + val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula - (* generic solver interface *) - val solvers : (string * solver) list ref - val add_solver : string * solver -> unit - val invoke_solver : string -> solver (* exception Option *) + (* generic solver interface *) + val solvers : (string * solver) list ref + val add_solver : string * solver -> unit + val invoke_solver : string -> solver (* exception Option *) end; structure SatSolver : SAT_SOLVER = struct - open PropLogic; + open PropLogic; (* ------------------------------------------------------------------------- *) (* should be raised by an external SAT solver to indicate that the solver is *) (* not configured properly *) (* ------------------------------------------------------------------------- *) - exception NOT_CONFIGURED; + exception NOT_CONFIGURED; (* ------------------------------------------------------------------------- *) (* type of partial (satisfying) assignments: 'a i = NONE' means that 'a' is *) (* a satisfying assignment regardless of the value of variable 'i' *) (* ------------------------------------------------------------------------- *) - type assignment = int -> bool option; + type assignment = int -> bool option; (* ------------------------------------------------------------------------- *) (* a proof of unsatisfiability, to be interpreted as follows: each integer *) @@ -65,7 +65,7 @@ (* but do not need to be consecutive. *) (* ------------------------------------------------------------------------- *) - type proof = int list Inttab.table * int; + type proof = int list Inttab.table * int; (* ------------------------------------------------------------------------- *) (* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying *) @@ -73,16 +73,16 @@ (* 'UNSATISFIABLE', a proof of unsatisfiability may be returned *) (* ------------------------------------------------------------------------- *) - datatype result = SATISFIABLE of assignment - | UNSATISFIABLE of proof option - | UNKNOWN; + datatype result = SATISFIABLE of assignment + | UNSATISFIABLE of proof option + | UNKNOWN; (* ------------------------------------------------------------------------- *) (* type of SAT solvers: given a propositional formula, a satisfying *) (* assignment may be returned *) (* ------------------------------------------------------------------------- *) - type solver = prop_formula -> result; + type solver = prop_formula -> result; (* ------------------------------------------------------------------------- *) (* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic *) @@ -92,56 +92,56 @@ (* Note: 'fm' must be given in CNF. *) (* ------------------------------------------------------------------------- *) - (* Path.T -> prop_formula -> unit *) + (* Path.T -> prop_formula -> unit *) - fun write_dimacs_cnf_file path fm = - let - (* prop_formula -> prop_formula *) - fun cnf_True_False_elim True = - Or (BoolVar 1, Not (BoolVar 1)) - | cnf_True_False_elim False = - And (BoolVar 1, Not (BoolVar 1)) - | cnf_True_False_elim fm = - fm (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *) - (* prop_formula -> int *) - fun cnf_number_of_clauses (And (fm1,fm2)) = - (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) - | cnf_number_of_clauses _ = - 1 - (* prop_formula -> string list *) - fun cnf_string fm = - let - (* prop_formula -> string list -> string list *) - fun cnf_string_acc True acc = - error "formula is not in CNF" - | cnf_string_acc False acc = - error "formula is not in CNF" - | cnf_string_acc (BoolVar i) acc = - (assert (i>=1) "formula contains a variable index less than 1"; - string_of_int i :: acc) - | cnf_string_acc (Not (BoolVar i)) acc = - "-" :: cnf_string_acc (BoolVar i) acc - | cnf_string_acc (Not _) acc = - error "formula is not in CNF" - | cnf_string_acc (Or (fm1,fm2)) acc = - cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc) - | cnf_string_acc (And (fm1,fm2)) acc = - cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc) - in - cnf_string_acc fm [] - end - val fm' = cnf_True_False_elim fm - val number_of_vars = maxidx fm' - val number_of_clauses = cnf_number_of_clauses fm' - in - File.write path - ("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^ - "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n"); - File.append_list path - (cnf_string fm'); - File.append path - " 0\n" - end; + fun write_dimacs_cnf_file path fm = + let + (* prop_formula -> prop_formula *) + fun cnf_True_False_elim True = + Or (BoolVar 1, Not (BoolVar 1)) + | cnf_True_False_elim False = + And (BoolVar 1, Not (BoolVar 1)) + | cnf_True_False_elim fm = + fm (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *) + (* prop_formula -> int *) + fun cnf_number_of_clauses (And (fm1,fm2)) = + (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) + | cnf_number_of_clauses _ = + 1 + (* prop_formula -> string list *) + fun cnf_string fm = + let + (* prop_formula -> string list -> string list *) + fun cnf_string_acc True acc = + error "formula is not in CNF" + | cnf_string_acc False acc = + error "formula is not in CNF" + | cnf_string_acc (BoolVar i) acc = + (i>=1 orelse error "formula contains a variable index less than 1"; + string_of_int i :: acc) + | cnf_string_acc (Not (BoolVar i)) acc = + "-" :: cnf_string_acc (BoolVar i) acc + | cnf_string_acc (Not _) acc = + error "formula is not in CNF" + | cnf_string_acc (Or (fm1,fm2)) acc = + cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc) + | cnf_string_acc (And (fm1,fm2)) acc = + cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc) + in + cnf_string_acc fm [] + end + val fm' = cnf_True_False_elim fm + val number_of_vars = maxidx fm' + val number_of_clauses = cnf_number_of_clauses fm' + in + File.write path + ("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^ + "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n"); + File.append_list path + (cnf_string fm'); + File.append path + " 0\n" + end; (* ------------------------------------------------------------------------- *) (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic *) @@ -150,54 +150,54 @@ (* Note: 'fm' must not contain a variable index less than 1. *) (* ------------------------------------------------------------------------- *) - (* Path.T -> prop_formula -> unit *) + (* Path.T -> prop_formula -> unit *) - fun write_dimacs_sat_file path fm = - let - (* prop_formula -> string list *) - fun sat_string fm = - let - (* prop_formula -> string list -> string list *) - fun sat_string_acc True acc = - "*()" :: acc - | sat_string_acc False acc = - "+()" :: acc - | sat_string_acc (BoolVar i) acc = - (assert (i>=1) "formula contains a variable index less than 1"; - string_of_int i :: acc) - | sat_string_acc (Not (BoolVar i)) acc = - "-" :: sat_string_acc (BoolVar i) acc - | sat_string_acc (Not fm) acc = - "-(" :: sat_string_acc fm (")" :: acc) - | sat_string_acc (Or (fm1,fm2)) acc = - "+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc)) - | sat_string_acc (And (fm1,fm2)) acc = - "*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc)) - (* optimization to make use of n-ary disjunction/conjunction *) - (* prop_formula -> string list -> string list *) - and sat_string_acc_or (Or (fm1,fm2)) acc = - sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc) - | sat_string_acc_or fm acc = - sat_string_acc fm acc - (* prop_formula -> string list -> string list *) - and sat_string_acc_and (And (fm1,fm2)) acc = - sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc) - | sat_string_acc_and fm acc = - sat_string_acc fm acc - in - sat_string_acc fm [] - end - val number_of_vars = Int.max (maxidx fm, 1) - in - File.write path - ("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^ - "p sat " ^ string_of_int number_of_vars ^ "\n" ^ - "("); - File.append_list path - (sat_string fm); - File.append path - ")\n" - end; + fun write_dimacs_sat_file path fm = + let + (* prop_formula -> string list *) + fun sat_string fm = + let + (* prop_formula -> string list -> string list *) + fun sat_string_acc True acc = + "*()" :: acc + | sat_string_acc False acc = + "+()" :: acc + | sat_string_acc (BoolVar i) acc = + (i>=1 orelse error "formula contains a variable index less than 1"; + string_of_int i :: acc) + | sat_string_acc (Not (BoolVar i)) acc = + "-" :: sat_string_acc (BoolVar i) acc + | sat_string_acc (Not fm) acc = + "-(" :: sat_string_acc fm (")" :: acc) + | sat_string_acc (Or (fm1,fm2)) acc = + "+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc)) + | sat_string_acc (And (fm1,fm2)) acc = + "*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc)) + (* optimization to make use of n-ary disjunction/conjunction *) + (* prop_formula -> string list -> string list *) + and sat_string_acc_or (Or (fm1,fm2)) acc = + sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc) + | sat_string_acc_or fm acc = + sat_string_acc fm acc + (* prop_formula -> string list -> string list *) + and sat_string_acc_and (And (fm1,fm2)) acc = + sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc) + | sat_string_acc_and fm acc = + sat_string_acc fm acc + in + sat_string_acc fm [] + end + val number_of_vars = Int.max (maxidx fm, 1) + in + File.write path + ("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^ + "p sat " ^ string_of_int number_of_vars ^ "\n" ^ + "("); + File.append_list path + (sat_string fm); + File.append path + ")\n" + end; (* ------------------------------------------------------------------------- *) (* read_std_result_file: scans a SAT solver's output file for a satisfying *) @@ -213,149 +213,149 @@ (* value of i is taken to be unspecified. *) (* ------------------------------------------------------------------------- *) - (* Path.T -> string * string * string -> result *) + (* Path.T -> string * string * string -> result *) - fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) = - let - (* string -> int list *) - fun int_list_from_string s = - List.mapPartial Int.fromString (space_explode " " s) - (* int list -> assignment *) - fun assignment_from_list [] i = - NONE (* the SAT solver didn't provide a value for this variable *) - | assignment_from_list (x::xs) i = - if x=i then (SOME true) - else if x=(~i) then (SOME false) - else assignment_from_list xs i - (* int list -> string list -> assignment *) - fun parse_assignment xs [] = - assignment_from_list xs - | parse_assignment xs (line::lines) = - if String.isPrefix assignment_prefix line then - parse_assignment (xs @ int_list_from_string line) lines - else - assignment_from_list xs - (* string -> string -> bool *) - fun is_substring needle haystack = - let - val length1 = String.size needle - val length2 = String.size haystack - in - if length2 < length1 then - false - else if needle = String.substring (haystack, 0, length1) then - true - else is_substring needle (String.substring (haystack, 1, length2-1)) - end - (* string list -> result *) - fun parse_lines [] = - UNKNOWN - | parse_lines (line::lines) = - if is_substring unsatisfiable line then - UNSATISFIABLE NONE - else if is_substring satisfiable line then - SATISFIABLE (parse_assignment [] lines) - else - parse_lines lines - in - (parse_lines o (List.filter (fn l => l <> "")) o split_lines o File.read) path - end; + fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) = + let + (* string -> int list *) + fun int_list_from_string s = + List.mapPartial Int.fromString (space_explode " " s) + (* int list -> assignment *) + fun assignment_from_list [] i = + NONE (* the SAT solver didn't provide a value for this variable *) + | assignment_from_list (x::xs) i = + if x=i then (SOME true) + else if x=(~i) then (SOME false) + else assignment_from_list xs i + (* int list -> string list -> assignment *) + fun parse_assignment xs [] = + assignment_from_list xs + | parse_assignment xs (line::lines) = + if String.isPrefix assignment_prefix line then + parse_assignment (xs @ int_list_from_string line) lines + else + assignment_from_list xs + (* string -> string -> bool *) + fun is_substring needle haystack = + let + val length1 = String.size needle + val length2 = String.size haystack + in + if length2 < length1 then + false + else if needle = String.substring (haystack, 0, length1) then + true + else is_substring needle (String.substring (haystack, 1, length2-1)) + end + (* string list -> result *) + fun parse_lines [] = + UNKNOWN + | parse_lines (line::lines) = + if is_substring unsatisfiable line then + UNSATISFIABLE NONE + else if is_substring satisfiable line then + SATISFIABLE (parse_assignment [] lines) + else + parse_lines lines + in + (parse_lines o (List.filter (fn l => l <> "")) o split_lines o File.read) path + end; (* ------------------------------------------------------------------------- *) (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn' *) (* ------------------------------------------------------------------------- *) - (* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *) + (* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *) - fun make_external_solver cmd writefn readfn fm = - (writefn fm; system cmd; readfn ()); + fun make_external_solver cmd writefn readfn fm = + (writefn fm; system cmd; readfn ()); (* ------------------------------------------------------------------------- *) (* read_dimacs_cnf_file: returns a propositional formula that corresponds to *) (* a SAT problem given in DIMACS CNF format *) (* ------------------------------------------------------------------------- *) - (* Path.T -> PropLogic.prop_formula *) + (* Path.T -> PropLogic.prop_formula *) - fun read_dimacs_cnf_file path = - let - (* string list -> string list *) - fun filter_preamble [] = - error "problem line not found in DIMACS CNF file" - | filter_preamble (line::lines) = - if String.isPrefix "c " line orelse line = "c" then - (* ignore comments *) - filter_preamble lines - else if String.isPrefix "p " line then - (* ignore the problem line (which must be the last line of the preamble) *) - (* Ignoring the problem line implies that if the file contains more clauses *) - (* or variables than specified in its preamble, we will accept it anyway. *) - lines - else - error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \"" - (* string -> int *) - fun int_from_string s = - case Int.fromString s of - SOME i => i - | NONE => error ("token " ^ quote s ^ "in DIMACS CNF file is not a number") - (* int list -> int list list *) - fun clauses xs = - let - val (xs1, xs2) = take_prefix (fn i => i <> 0) xs - in - case xs2 of - [] => [xs1] - | (0::[]) => [xs1] - | (0::tl) => xs1 :: clauses tl - | _ => sys_error "this cannot happen" - end - (* int -> PropLogic.prop_formula *) - fun literal_from_int i = - (assert (i<>0) "variable index in DIMACS CNF file is 0"; - if i>0 then - PropLogic.BoolVar i - else - PropLogic.Not (PropLogic.BoolVar (~i))) - (* PropLogic.prop_formula list -> PropLogic.prop_formula *) - fun disjunction [] = - error "empty clause in DIMACS CNF file" - | disjunction (x::xs) = - (case xs of - [] => x - | _ => PropLogic.Or (x, disjunction xs)) - (* PropLogic.prop_formula list -> PropLogic.prop_formula *) - fun conjunction [] = - error "no clause in DIMACS CNF file" - | conjunction (x::xs) = - (case xs of - [] => x - | _ => PropLogic.And (x, conjunction xs)) - in - (conjunction - o (map disjunction) - o (map (map literal_from_int)) - o clauses - o (map int_from_string) - o List.concat - o (map (String.fields (fn c => c mem [#" ", #"\t", #"\n"]))) - o filter_preamble - o (List.filter (fn l => l <> "")) - o split_lines - o File.read) - path - end; + fun read_dimacs_cnf_file path = + let + (* string list -> string list *) + fun filter_preamble [] = + error "problem line not found in DIMACS CNF file" + | filter_preamble (line::lines) = + if String.isPrefix "c " line orelse line = "c" then + (* ignore comments *) + filter_preamble lines + else if String.isPrefix "p " line then + (* ignore the problem line (which must be the last line of the preamble) *) + (* Ignoring the problem line implies that if the file contains more clauses *) + (* or variables than specified in its preamble, we will accept it anyway. *) + lines + else + error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \"" + (* string -> int *) + fun int_from_string s = + case Int.fromString s of + SOME i => i + | NONE => error ("token " ^ quote s ^ "in DIMACS CNF file is not a number") + (* int list -> int list list *) + fun clauses xs = + let + val (xs1, xs2) = take_prefix (fn i => i <> 0) xs + in + case xs2 of + [] => [xs1] + | (0::[]) => [xs1] + | (0::tl) => xs1 :: clauses tl + | _ => sys_error "this cannot happen" + end + (* int -> PropLogic.prop_formula *) + fun literal_from_int i = + (i<>0 orelse error "variable index in DIMACS CNF file is 0"; + if i>0 then + PropLogic.BoolVar i + else + PropLogic.Not (PropLogic.BoolVar (~i))) + (* PropLogic.prop_formula list -> PropLogic.prop_formula *) + fun disjunction [] = + error "empty clause in DIMACS CNF file" + | disjunction (x::xs) = + (case xs of + [] => x + | _ => PropLogic.Or (x, disjunction xs)) + (* PropLogic.prop_formula list -> PropLogic.prop_formula *) + fun conjunction [] = + error "no clause in DIMACS CNF file" + | conjunction (x::xs) = + (case xs of + [] => x + | _ => PropLogic.And (x, conjunction xs)) + in + (conjunction + o (map disjunction) + o (map (map literal_from_int)) + o clauses + o (map int_from_string) + o List.concat + o (map (String.fields (fn c => c mem [#" ", #"\t", #"\n"]))) + o filter_preamble + o (List.filter (fn l => l <> "")) + o split_lines + o File.read) + path + end; (* ------------------------------------------------------------------------- *) (* solvers: a (reference to a) table of all registered SAT solvers *) (* ------------------------------------------------------------------------- *) - val solvers = ref ([] : (string * solver) list); + val solvers = ref ([] : (string * solver) list); (* ------------------------------------------------------------------------- *) (* add_solver: updates 'solvers' by adding a new solver *) (* ------------------------------------------------------------------------- *) - (* string * solver -> unit *) + (* string * solver -> unit *) fun add_solver (name, new_solver) = let @@ -371,10 +371,10 @@ (* raised. *) (* ------------------------------------------------------------------------- *) - (* string -> solver *) + (* string -> solver *) - fun invoke_solver name = - (the o AList.lookup (op =) (!solvers)) name; + fun invoke_solver name = + (the o AList.lookup (op =) (!solvers)) name; end; (* SatSolver *) @@ -389,40 +389,40 @@ (* ------------------------------------------------------------------------- *) let - fun enum_solver fm = - let - (* int list *) - val indices = PropLogic.indices fm - (* int list -> int list -> int list option *) - (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *) - fun next_list _ ([]:int list) = - NONE - | next_list [] (y::ys) = - SOME [y] - | next_list (x::xs) (y::ys) = - if x=y then - (* reset the bit, continue *) - next_list xs ys - else - (* set the lowest bit that wasn't set before, keep the higher bits *) - SOME (y::x::xs) - (* int list -> int -> bool *) - fun assignment_from_list xs i = - i mem xs - (* int list -> SatSolver.result *) - fun solver_loop xs = - if PropLogic.eval (assignment_from_list xs) fm then - SatSolver.SATISFIABLE (SOME o (assignment_from_list xs)) - else - (case next_list xs indices of - SOME xs' => solver_loop xs' - | NONE => SatSolver.UNSATISFIABLE NONE) - in - (* start with the "first" assignment (all variables are interpreted as 'false') *) - solver_loop [] - end + fun enum_solver fm = + let + (* int list *) + val indices = PropLogic.indices fm + (* int list -> int list -> int list option *) + (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *) + fun next_list _ ([]:int list) = + NONE + | next_list [] (y::ys) = + SOME [y] + | next_list (x::xs) (y::ys) = + if x=y then + (* reset the bit, continue *) + next_list xs ys + else + (* set the lowest bit that wasn't set before, keep the higher bits *) + SOME (y::x::xs) + (* int list -> int -> bool *) + fun assignment_from_list xs i = + i mem xs + (* int list -> SatSolver.result *) + fun solver_loop xs = + if PropLogic.eval (assignment_from_list xs) fm then + SatSolver.SATISFIABLE (SOME o (assignment_from_list xs)) + else + (case next_list xs indices of + SOME xs' => solver_loop xs' + | NONE => SatSolver.UNSATISFIABLE NONE) + in + (* start with the "first" assignment (all variables are interpreted as 'false') *) + solver_loop [] + end in - SatSolver.add_solver ("enumerate", enum_solver) + SatSolver.add_solver ("enumerate", enum_solver) end; (* ------------------------------------------------------------------------- *) @@ -432,86 +432,86 @@ (* ------------------------------------------------------------------------- *) let - local - open PropLogic - in - fun dpll_solver fm = - let - (* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *) - (* but that sometimes leads to worse performance due to the *) - (* introduction of additional variables. *) - val fm' = PropLogic.nnf fm - (* int list *) - val indices = PropLogic.indices fm' - (* int list -> int -> prop_formula *) - fun partial_var_eval [] i = BoolVar i - | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i - (* int list -> prop_formula -> prop_formula *) - fun partial_eval xs True = True - | partial_eval xs False = False - | partial_eval xs (BoolVar i) = partial_var_eval xs i - | partial_eval xs (Not fm) = SNot (partial_eval xs fm) - | partial_eval xs (Or (fm1, fm2)) = SOr (partial_eval xs fm1, partial_eval xs fm2) - | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2) - (* prop_formula -> int list *) - fun forced_vars True = [] - | forced_vars False = [] - | forced_vars (BoolVar i) = [i] - | forced_vars (Not (BoolVar i)) = [~i] - | forced_vars (Or (fm1, fm2)) = (forced_vars fm1) inter_int (forced_vars fm2) - | forced_vars (And (fm1, fm2)) = (forced_vars fm1) union_int (forced_vars fm2) - (* Above, i *and* ~i may be forced. In this case the first occurrence takes *) - (* precedence, and the next partial evaluation of the formula returns 'False'. *) - | forced_vars _ = error "formula is not in negation normal form" - (* int list -> prop_formula -> (int list * prop_formula) *) - fun eval_and_force xs fm = - let - val fm' = partial_eval xs fm - val xs' = forced_vars fm' - in - if null xs' then - (xs, fm') - else - eval_and_force (xs@xs') fm' (* xs and xs' should be distinct, so '@' here should have *) - (* the same effect as 'union_int' *) - end - (* int list -> int option *) - fun fresh_var xs = - Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices - (* int list -> prop_formula -> int list option *) - (* partial assignment 'xs' *) - fun dpll xs fm = - let - val (xs', fm') = eval_and_force xs fm - in - case fm' of - True => SOME xs' - | False => NONE - | _ => - let - val x = valOf (fresh_var xs') (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *) - in - case dpll (x::xs') fm' of (* passing fm' rather than fm should save some simplification work *) - SOME xs'' => SOME xs'' - | NONE => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *) - end - end - (* int list -> assignment *) - fun assignment_from_list [] i = - NONE (* the DPLL procedure didn't provide a value for this variable *) - | assignment_from_list (x::xs) i = - if x=i then (SOME true) - else if x=(~i) then (SOME false) - else assignment_from_list xs i - in - (* initially, no variable is interpreted yet *) - case dpll [] fm' of - SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment) - | NONE => SatSolver.UNSATISFIABLE NONE - end - end (* local *) + local + open PropLogic + in + fun dpll_solver fm = + let + (* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *) + (* but that sometimes leads to worse performance due to the *) + (* introduction of additional variables. *) + val fm' = PropLogic.nnf fm + (* int list *) + val indices = PropLogic.indices fm' + (* int list -> int -> prop_formula *) + fun partial_var_eval [] i = BoolVar i + | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i + (* int list -> prop_formula -> prop_formula *) + fun partial_eval xs True = True + | partial_eval xs False = False + | partial_eval xs (BoolVar i) = partial_var_eval xs i + | partial_eval xs (Not fm) = SNot (partial_eval xs fm) + | partial_eval xs (Or (fm1, fm2)) = SOr (partial_eval xs fm1, partial_eval xs fm2) + | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2) + (* prop_formula -> int list *) + fun forced_vars True = [] + | forced_vars False = [] + | forced_vars (BoolVar i) = [i] + | forced_vars (Not (BoolVar i)) = [~i] + | forced_vars (Or (fm1, fm2)) = (forced_vars fm1) inter_int (forced_vars fm2) + | forced_vars (And (fm1, fm2)) = (forced_vars fm1) union_int (forced_vars fm2) + (* Above, i *and* ~i may be forced. In this case the first occurrence takes *) + (* precedence, and the next partial evaluation of the formula returns 'False'. *) + | forced_vars _ = error "formula is not in negation normal form" + (* int list -> prop_formula -> (int list * prop_formula) *) + fun eval_and_force xs fm = + let + val fm' = partial_eval xs fm + val xs' = forced_vars fm' + in + if null xs' then + (xs, fm') + else + eval_and_force (xs@xs') fm' (* xs and xs' should be distinct, so '@' here should have *) + (* the same effect as 'union_int' *) + end + (* int list -> int option *) + fun fresh_var xs = + Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices + (* int list -> prop_formula -> int list option *) + (* partial assignment 'xs' *) + fun dpll xs fm = + let + val (xs', fm') = eval_and_force xs fm + in + case fm' of + True => SOME xs' + | False => NONE + | _ => + let + val x = valOf (fresh_var xs') (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *) + in + case dpll (x::xs') fm' of (* passing fm' rather than fm should save some simplification work *) + SOME xs'' => SOME xs'' + | NONE => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *) + end + end + (* int list -> assignment *) + fun assignment_from_list [] i = + NONE (* the DPLL procedure didn't provide a value for this variable *) + | assignment_from_list (x::xs) i = + if x=i then (SOME true) + else if x=(~i) then (SOME false) + else assignment_from_list xs i + in + (* initially, no variable is interpreted yet *) + case dpll [] fm' of + SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment) + | NONE => SatSolver.UNSATISFIABLE NONE + end + end (* local *) in - SatSolver.add_solver ("dpll", dpll_solver) + SatSolver.add_solver ("dpll", dpll_solver) end; (* ------------------------------------------------------------------------- *) @@ -521,28 +521,28 @@ (* ------------------------------------------------------------------------- *) let - fun auto_solver fm = - let - fun loop [] = - SatSolver.UNKNOWN - | loop ((name, solver)::solvers) = - if name="auto" then - (* do not call solver "auto" from within "auto" *) - loop solvers - else ( - (if name="dpll" orelse name="enumerate" then - warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.") - else - tracing ("Using SAT solver " ^ quote name ^ ".")); - (* apply 'solver' to 'fm' *) - solver fm - handle SatSolver.NOT_CONFIGURED => loop solvers - ) - in - loop (!SatSolver.solvers) - end + fun auto_solver fm = + let + fun loop [] = + SatSolver.UNKNOWN + | loop ((name, solver)::solvers) = + if name="auto" then + (* do not call solver "auto" from within "auto" *) + loop solvers + else ( + (if name="dpll" orelse name="enumerate" then + warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.") + else + tracing ("Using SAT solver " ^ quote name ^ ".")); + (* apply 'solver' to 'fm' *) + solver fm + handle SatSolver.NOT_CONFIGURED => loop solvers + ) + in + loop (!SatSolver.solvers) + end in - SatSolver.add_solver ("auto", auto_solver) + SatSolver.add_solver ("auto", auto_solver) end; (* ------------------------------------------------------------------------- *) @@ -565,210 +565,210 @@ (* from 0 to n-1 (where n is the number of clauses in the formula). *) let - exception INVALID_PROOF of string - fun minisat_with_proofs fm = - let - val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () - val inpath = File.tmp_path (Path.explode "isabelle.cnf") - val outpath = File.tmp_path (Path.explode "result") - val proofpath = File.tmp_path (Path.explode "result.prf") - val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null" - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm - fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () - val cnf = PropLogic.defcnf fm - val result = SatSolver.make_external_solver cmd writefn readfn cnf - val _ = try File.rm inpath - val _ = try File.rm outpath - in case result of - SatSolver.UNSATISFIABLE NONE => - (let - (* string list *) - val proof_lines = (split_lines o File.read) proofpath - handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\"" - (* representation of clauses as ordered lists of literals (with duplicates removed) *) - (* prop_formula -> int list *) - fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) = - OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2) - | clause_to_lit_list (PropLogic.BoolVar i) = - [i] - | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = - [~i] - | clause_to_lit_list _ = - raise INVALID_PROOF "Error: invalid clause in CNF formula." - (* prop_formula -> int *) - fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = - cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 - | cnf_number_of_clauses _ = - 1 - val number_of_clauses = cnf_number_of_clauses cnf - (* int list array *) - val clauses = Array.array (number_of_clauses, []) - (* initialize the 'clauses' array *) - (* prop_formula * int -> int *) - fun init_array (PropLogic.And (fm1, fm2), n) = - init_array (fm2, init_array (fm1, n)) - | init_array (fm, n) = - (Array.update (clauses, n, clause_to_lit_list fm); n+1) - val _ = init_array (cnf, 0) - (* optimization for the common case where MiniSat "R"s clauses in their *) - (* original order: *) - val last_ref_clause = ref (number_of_clauses - 1) - (* search the 'clauses' array for the given list of literals 'lits', *) - (* starting at index '!last_ref_clause + 1' *) - (* int list -> int option *) - fun original_clause_id lits = - let - fun original_clause_id_from index = - if index = number_of_clauses then - (* search from beginning again *) - original_clause_id_from 0 - (* both 'lits' and the list of literals used in 'clauses' are sorted, so *) - (* testing for equality should suffice -- barring duplicate literals *) - else if Array.sub (clauses, index) = lits then ( - (* success *) - last_ref_clause := index; - SOME index - ) else if index = !last_ref_clause then - (* failure *) - NONE - else - (* continue search *) - original_clause_id_from (index + 1) - in - original_clause_id_from (!last_ref_clause + 1) - end - (* string -> int *) - fun int_from_string s = ( - case Int.fromString s of - SOME i => i - | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") - ) - (* parse the proof file *) - val clause_table = ref (Inttab.empty : int list Inttab.table) - val empty_id = ref ~1 - (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *) - (* our proof format, where original clauses are numbered starting from 0 *) - val clause_id_map = ref (Inttab.empty : int Inttab.table) - fun sat_to_proof id = ( - case Inttab.lookup (!clause_id_map) id of - SOME id' => id' - | NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.") - ) - val next_id = ref (number_of_clauses - 1) - (* string list -> unit *) - fun process_tokens [] = - () - | process_tokens (tok::toks) = - if tok="R" then ( - case toks of - id::sep::lits => - let - val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"." - val cid = int_from_string id - val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") - val ls = sort int_ord (map int_from_string lits) - val proof_id = case original_clause_id ls of - SOME orig_id => orig_id - | NONE => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.") - in - (* extend the mapping of clause IDs with this newly defined ID *) - clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) - handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").") - (* the proof itself doesn't change *) - end - | _ => - raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens." - ) else if tok="C" then ( - case toks of - id::sep::ids => - let - val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"." - val cid = int_from_string id - val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") - (* ignore the pivot literals in MiniSat's trace *) - fun unevens [] = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs." - | unevens (x :: []) = x :: [] - | unevens (x :: _ :: xs) = x :: unevens xs - val rs = (map sat_to_proof o unevens o map int_from_string) ids - (* extend the mapping of clause IDs with this newly defined ID *) - val proof_id = inc next_id - val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) - handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").") - in - (* update clause table *) - clause_table := Inttab.update_new (proof_id, rs) (!clause_table) - handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.") - end - | _ => - raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens." - ) else if tok="D" then ( - case toks of - [id] => - let - val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"." - val _ = sat_to_proof (int_from_string id) - in - (* simply ignore "D" *) - () - end - | _ => - raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens." - ) else if tok="X" then ( - case toks of - [id1, id2] => - let - val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement." - val _ = sat_to_proof (int_from_string id1) - val new_empty_id = sat_to_proof (int_from_string id2) - in - (* update conflict id *) - empty_id := new_empty_id - end - | _ => - raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens." - ) else - raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") - (* string list -> unit *) - fun process_lines [] = - () - | process_lines (l::ls) = ( - process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); - process_lines ls - ) - (* proof *) - val _ = process_lines proof_lines - val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." - in - SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) - end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) - | result => - result - end + exception INVALID_PROOF of string + fun minisat_with_proofs fm = + let + val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () + val inpath = File.tmp_path (Path.explode "isabelle.cnf") + val outpath = File.tmp_path (Path.explode "result") + val proofpath = File.tmp_path (Path.explode "result.prf") + val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null" + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm + fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () + val cnf = PropLogic.defcnf fm + val result = SatSolver.make_external_solver cmd writefn readfn cnf + val _ = try File.rm inpath + val _ = try File.rm outpath + in case result of + SatSolver.UNSATISFIABLE NONE => + (let + (* string list *) + val proof_lines = (split_lines o File.read) proofpath + handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\"" + (* representation of clauses as ordered lists of literals (with duplicates removed) *) + (* prop_formula -> int list *) + fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) = + OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2) + | clause_to_lit_list (PropLogic.BoolVar i) = + [i] + | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = + [~i] + | clause_to_lit_list _ = + raise INVALID_PROOF "Error: invalid clause in CNF formula." + (* prop_formula -> int *) + fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = + cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 + | cnf_number_of_clauses _ = + 1 + val number_of_clauses = cnf_number_of_clauses cnf + (* int list array *) + val clauses = Array.array (number_of_clauses, []) + (* initialize the 'clauses' array *) + (* prop_formula * int -> int *) + fun init_array (PropLogic.And (fm1, fm2), n) = + init_array (fm2, init_array (fm1, n)) + | init_array (fm, n) = + (Array.update (clauses, n, clause_to_lit_list fm); n+1) + val _ = init_array (cnf, 0) + (* optimization for the common case where MiniSat "R"s clauses in their *) + (* original order: *) + val last_ref_clause = ref (number_of_clauses - 1) + (* search the 'clauses' array for the given list of literals 'lits', *) + (* starting at index '!last_ref_clause + 1' *) + (* int list -> int option *) + fun original_clause_id lits = + let + fun original_clause_id_from index = + if index = number_of_clauses then + (* search from beginning again *) + original_clause_id_from 0 + (* both 'lits' and the list of literals used in 'clauses' are sorted, so *) + (* testing for equality should suffice -- barring duplicate literals *) + else if Array.sub (clauses, index) = lits then ( + (* success *) + last_ref_clause := index; + SOME index + ) else if index = !last_ref_clause then + (* failure *) + NONE + else + (* continue search *) + original_clause_id_from (index + 1) + in + original_clause_id_from (!last_ref_clause + 1) + end + (* string -> int *) + fun int_from_string s = ( + case Int.fromString s of + SOME i => i + | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") + ) + (* parse the proof file *) + val clause_table = ref (Inttab.empty : int list Inttab.table) + val empty_id = ref ~1 + (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *) + (* our proof format, where original clauses are numbered starting from 0 *) + val clause_id_map = ref (Inttab.empty : int Inttab.table) + fun sat_to_proof id = ( + case Inttab.lookup (!clause_id_map) id of + SOME id' => id' + | NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.") + ) + val next_id = ref (number_of_clauses - 1) + (* string list -> unit *) + fun process_tokens [] = + () + | process_tokens (tok::toks) = + if tok="R" then ( + case toks of + id::sep::lits => + let + val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"." + val cid = int_from_string id + val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") + val ls = sort int_ord (map int_from_string lits) + val proof_id = case original_clause_id ls of + SOME orig_id => orig_id + | NONE => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.") + in + (* extend the mapping of clause IDs with this newly defined ID *) + clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) + handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").") + (* the proof itself doesn't change *) + end + | _ => + raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens." + ) else if tok="C" then ( + case toks of + id::sep::ids => + let + val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"." + val cid = int_from_string id + val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") + (* ignore the pivot literals in MiniSat's trace *) + fun unevens [] = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs." + | unevens (x :: []) = x :: [] + | unevens (x :: _ :: xs) = x :: unevens xs + val rs = (map sat_to_proof o unevens o map int_from_string) ids + (* extend the mapping of clause IDs with this newly defined ID *) + val proof_id = inc next_id + val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) + handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").") + in + (* update clause table *) + clause_table := Inttab.update_new (proof_id, rs) (!clause_table) + handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.") + end + | _ => + raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens." + ) else if tok="D" then ( + case toks of + [id] => + let + val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"." + val _ = sat_to_proof (int_from_string id) + in + (* simply ignore "D" *) + () + end + | _ => + raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens." + ) else if tok="X" then ( + case toks of + [id1, id2] => + let + val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement." + val _ = sat_to_proof (int_from_string id1) + val new_empty_id = sat_to_proof (int_from_string id2) + in + (* update conflict id *) + empty_id := new_empty_id + end + | _ => + raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens." + ) else + raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") + (* string list -> unit *) + fun process_lines [] = + () + | process_lines (l::ls) = ( + process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); + process_lines ls + ) + (* proof *) + val _ = process_lines proof_lines + val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." + in + SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) + end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) + | result => + result + end in - SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs) + SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs) end; let - fun minisat fm = - let - val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () - val inpath = File.tmp_path (Path.explode "isabelle.cnf") - val outpath = File.tmp_path (Path.explode "result") - val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null" - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) - fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () - val result = SatSolver.make_external_solver cmd writefn readfn fm - val _ = try File.rm inpath - val _ = try File.rm outpath - in - result - end + fun minisat fm = + let + val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () + val inpath = File.tmp_path (Path.explode "isabelle.cnf") + val outpath = File.tmp_path (Path.explode "result") + val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null" + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) + fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () + val result = SatSolver.make_external_solver cmd writefn readfn fm + val _ = try File.rm inpath + val _ = try File.rm outpath + in + result + end in - SatSolver.add_solver ("minisat", minisat) + SatSolver.add_solver ("minisat", minisat) end; (* ------------------------------------------------------------------------- *) @@ -787,150 +787,150 @@ (* that the latter is preferred by the "auto" solver *) let - exception INVALID_PROOF of string - fun zchaff_with_proofs fm = - case SatSolver.invoke_solver "zchaff" fm of - SatSolver.UNSATISFIABLE NONE => - (let - (* string list *) - val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace")) - handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" - (* PropLogic.prop_formula -> int *) - fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 - | cnf_number_of_clauses _ = 1 - (* string -> int *) - fun int_from_string s = ( - case Int.fromString s of - SOME i => i - | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") - ) - (* parse the "resolve_trace" file *) - val clause_offset = ref ~1 - val clause_table = ref (Inttab.empty : int list Inttab.table) - val empty_id = ref ~1 - (* string list -> unit *) - fun process_tokens [] = - () - | process_tokens (tok::toks) = - if tok="CL:" then ( - case toks of - id::sep::ids => - let - val _ = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".") - val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".") - val cid = int_from_string id - val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") - val rs = map int_from_string ids - in - (* update clause table *) - clause_table := Inttab.update_new (cid, rs) (!clause_table) - handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.") - end - | _ => - raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens." - ) else if tok="VAR:" then ( - case toks of - id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits => - let - val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".") - (* set 'clause_offset' to the largest used clause ID *) - val _ = if !clause_offset = ~1 then clause_offset := - (case Inttab.max_key (!clause_table) of - SOME id => id - | NONE => cnf_number_of_clauses (PropLogic.defcnf fm) - 1 (* the first clause ID is 0, not 1 *)) - else - () - val vid = int_from_string id - val _ = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).") - val _ = int_from_string levid - val _ = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).") - val _ = int_from_string valid - val _ = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).") - val aid = int_from_string anteid - val _ = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).") - val ls = map int_from_string lits - (* convert the data provided by zChaff to our resolution-style proof format *) - (* each "VAR:" line defines a unit clause, the resolvents are implicitly *) - (* given by the literals in the antecedent clause *) - (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *) - val cid = !clause_offset + vid - (* the low bit of each literal gives its sign (positive/negative), therefore *) - (* we have to divide each literal by 2 to obtain the proper variable ID; then *) - (* we add '!clause_offset' to obtain the ID of the corresponding unit clause *) - val vids = filter (not_equal vid) (map (fn l => l div 2) ls) - val rs = aid :: map (fn v => !clause_offset + v) vids - in - (* update clause table *) - clause_table := Inttab.update_new (cid, rs) (!clause_table) - handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.") - end - | _ => - raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens." - ) else if tok="CONF:" then ( - case toks of - id::sep::ids => - let - val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified." - val cid = int_from_string id - val _ = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).") - val ls = map int_from_string ids - (* the conflict clause must be resolved with the unit clauses *) - (* for its literals to obtain the empty clause *) - val vids = map (fn l => l div 2) ls - val rs = cid :: map (fn v => !clause_offset + v) vids - val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1 - in - (* update clause table and conflict id *) - clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table) - handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined."); - empty_id := new_empty_id - end - | _ => - raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens." - ) else - raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") - (* string list -> unit *) - fun process_lines [] = - () - | process_lines (l::ls) = ( - process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); - process_lines ls - ) - (* proof *) - val _ = process_lines proof_lines - val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." - in - SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) - end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) - | result => - result + exception INVALID_PROOF of string + fun zchaff_with_proofs fm = + case SatSolver.invoke_solver "zchaff" fm of + SatSolver.UNSATISFIABLE NONE => + (let + (* string list *) + val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace")) + handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" + (* PropLogic.prop_formula -> int *) + fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 + | cnf_number_of_clauses _ = 1 + (* string -> int *) + fun int_from_string s = ( + case Int.fromString s of + SOME i => i + | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") + ) + (* parse the "resolve_trace" file *) + val clause_offset = ref ~1 + val clause_table = ref (Inttab.empty : int list Inttab.table) + val empty_id = ref ~1 + (* string list -> unit *) + fun process_tokens [] = + () + | process_tokens (tok::toks) = + if tok="CL:" then ( + case toks of + id::sep::ids => + let + val _ = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".") + val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".") + val cid = int_from_string id + val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") + val rs = map int_from_string ids + in + (* update clause table *) + clause_table := Inttab.update_new (cid, rs) (!clause_table) + handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.") + end + | _ => + raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens." + ) else if tok="VAR:" then ( + case toks of + id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits => + let + val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".") + (* set 'clause_offset' to the largest used clause ID *) + val _ = if !clause_offset = ~1 then clause_offset := + (case Inttab.max_key (!clause_table) of + SOME id => id + | NONE => cnf_number_of_clauses (PropLogic.defcnf fm) - 1 (* the first clause ID is 0, not 1 *)) + else + () + val vid = int_from_string id + val _ = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).") + val _ = int_from_string levid + val _ = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).") + val _ = int_from_string valid + val _ = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).") + val aid = int_from_string anteid + val _ = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).") + val ls = map int_from_string lits + (* convert the data provided by zChaff to our resolution-style proof format *) + (* each "VAR:" line defines a unit clause, the resolvents are implicitly *) + (* given by the literals in the antecedent clause *) + (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *) + val cid = !clause_offset + vid + (* the low bit of each literal gives its sign (positive/negative), therefore *) + (* we have to divide each literal by 2 to obtain the proper variable ID; then *) + (* we add '!clause_offset' to obtain the ID of the corresponding unit clause *) + val vids = filter (not_equal vid) (map (fn l => l div 2) ls) + val rs = aid :: map (fn v => !clause_offset + v) vids + in + (* update clause table *) + clause_table := Inttab.update_new (cid, rs) (!clause_table) + handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.") + end + | _ => + raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens." + ) else if tok="CONF:" then ( + case toks of + id::sep::ids => + let + val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified." + val cid = int_from_string id + val _ = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).") + val ls = map int_from_string ids + (* the conflict clause must be resolved with the unit clauses *) + (* for its literals to obtain the empty clause *) + val vids = map (fn l => l div 2) ls + val rs = cid :: map (fn v => !clause_offset + v) vids + val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1 + in + (* update clause table and conflict id *) + clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table) + handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined."); + empty_id := new_empty_id + end + | _ => + raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens." + ) else + raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") + (* string list -> unit *) + fun process_lines [] = + () + | process_lines (l::ls) = ( + process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); + process_lines ls + ) + (* proof *) + val _ = process_lines proof_lines + val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." + in + SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) + end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) + | result => + result in - SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs) + SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs) end; let - fun zchaff fm = - let - val _ = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () - val _ = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso - (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else () - (* both versions of zChaff appear to have the same interface, so we do *) - (* not actually need to distinguish between them in the following code *) - val inpath = File.tmp_path (Path.explode "isabelle.cnf") - val outpath = File.tmp_path (Path.explode "result") - val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) - fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () - val result = SatSolver.make_external_solver cmd writefn readfn fm - val _ = try File.rm inpath - val _ = try File.rm outpath - in - result - end + fun zchaff fm = + let + val _ = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () + val _ = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso + (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else () + (* both versions of zChaff appear to have the same interface, so we do *) + (* not actually need to distinguish between them in the following code *) + val inpath = File.tmp_path (Path.explode "isabelle.cnf") + val outpath = File.tmp_path (Path.explode "result") + val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) + fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () + val result = SatSolver.make_external_solver cmd writefn readfn fm + val _ = try File.rm inpath + val _ = try File.rm outpath + in + result + end in - SatSolver.add_solver ("zchaff", zchaff) + SatSolver.add_solver ("zchaff", zchaff) end; (* ------------------------------------------------------------------------- *) @@ -938,24 +938,24 @@ (* ------------------------------------------------------------------------- *) let - fun berkmin fm = - let - val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else () - val inpath = File.tmp_path (Path.explode "isabelle.cnf") - val outpath = File.tmp_path (Path.explode "result") - val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) - fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () - val result = SatSolver.make_external_solver cmd writefn readfn fm - val _ = try File.rm inpath - val _ = try File.rm outpath - in - result - end + fun berkmin fm = + let + val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else () + val inpath = File.tmp_path (Path.explode "isabelle.cnf") + val outpath = File.tmp_path (Path.explode "result") + val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) + fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () + val result = SatSolver.make_external_solver cmd writefn readfn fm + val _ = try File.rm inpath + val _ = try File.rm outpath + in + result + end in - SatSolver.add_solver ("berkmin", berkmin) + SatSolver.add_solver ("berkmin", berkmin) end; (* ------------------------------------------------------------------------- *) @@ -963,24 +963,24 @@ (* ------------------------------------------------------------------------- *) let - fun jerusat fm = - let - val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () - val inpath = File.tmp_path (Path.explode "isabelle.cnf") - val outpath = File.tmp_path (Path.explode "result") - val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) - fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () - val result = SatSolver.make_external_solver cmd writefn readfn fm - val _ = try File.rm inpath - val _ = try File.rm outpath - in - result - end + fun jerusat fm = + let + val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () + val inpath = File.tmp_path (Path.explode "isabelle.cnf") + val outpath = File.tmp_path (Path.explode "result") + val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) + fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () + val result = SatSolver.make_external_solver cmd writefn readfn fm + val _ = try File.rm inpath + val _ = try File.rm outpath + in + result + end in - SatSolver.add_solver ("jerusat", jerusat) + SatSolver.add_solver ("jerusat", jerusat) end; (* ------------------------------------------------------------------------- *) @@ -989,9 +989,9 @@ (* let - fun mysolver fm = ... + fun mysolver fm = ... in - SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED)); -- register the solver + SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED)); -- register the solver end; -- the solver is now available as SatSolver.invoke_solver "myname" diff -r 535ae9dd4c45 -r 1565d476a9e2 src/Pure/General/secure.ML --- a/src/Pure/General/secure.ML Tue Apr 03 19:24:10 2007 +0200 +++ b/src/Pure/General/secure.ML Tue Apr 03 19:24:11 2007 +0200 @@ -9,7 +9,6 @@ sig val set_secure: unit -> unit val is_secure: unit -> bool - val deny_secure: string -> unit val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit val use: string -> unit @@ -28,7 +27,7 @@ fun set_secure () = secure := true; fun is_secure () = ! secure; -fun deny_secure msg = deny (is_secure ()) msg; +fun deny_secure msg = if is_secure () then error msg else (); (** critical operations **) diff -r 535ae9dd4c45 -r 1565d476a9e2 src/Pure/library.ML --- a/src/Pure/library.ML Tue Apr 03 19:24:10 2007 +0200 +++ b/src/Pure/library.ML Tue Apr 03 19:24:11 2007 +0200 @@ -46,8 +46,6 @@ exception ERROR of string val error: string -> 'a val cat_error: string -> string -> 'a - val assert: bool -> string -> unit - val deny: bool -> string -> unit val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit (*pairs*) @@ -327,9 +325,6 @@ fun cat_error "" msg = error msg | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2); -fun assert p msg = if p then () else error msg; -fun deny p msg = if p then error msg else (); - fun assert_all pred list msg = let fun ass [] = () diff -r 535ae9dd4c45 -r 1565d476a9e2 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Tue Apr 03 19:24:10 2007 +0200 +++ b/src/ZF/Tools/inductive_package.ML Tue Apr 03 19:24:11 2007 +0200 @@ -135,8 +135,8 @@ val fp_rhs = Fp.oper $ dom_sum $ fp_abs - val dummy = List.app (fn rec_hd => deny (Logic.occs (rec_hd, fp_rhs)) - "Illegal occurrence of recursion operator") + val dummy = List.app (fn rec_hd => (Logic.occs (rec_hd, fp_rhs) andalso + error "Illegal occurrence of recursion operator"; ())) rec_hds; (*** Make the new theory ***) @@ -153,12 +153,6 @@ writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name) else (); - (*Forbid the inductive definition structure from clashing with a theory - name. This restriction may become obsolete as ML is de-emphasized.*) - val dummy = deny (big_rec_base_name mem (Context.names_of thy)) - ("Definition " ^ big_rec_base_name ^ - " would clash with the theory of the same name!"); - (*Big_rec... is the union of the mutually recursive sets*) val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); diff -r 535ae9dd4c45 -r 1565d476a9e2 src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Tue Apr 03 19:24:10 2007 +0200 +++ b/src/ZF/ind_syntax.ML Tue Apr 03 19:24:11 2007 +0200 @@ -45,9 +45,9 @@ fun chk_prem rec_hd (Const("op &",_) $ _ $ _) = error"Premises may not be conjuctive" | chk_prem rec_hd (Const("op :",_) $ t $ X) = - deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol" + (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ()) | chk_prem rec_hd t = - deny (Logic.occs(rec_hd,t)) "Recursion term in side formula"; + (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ()); (*Return the conclusion of a rule, of the form t:X*) fun rule_concl rl =