src/HOL/Tools/refute.ML
changeset 33243 17014b1b9353
parent 33063 4d462963a7db
child 33246 46e47aa1558f
     1.1 --- a/src/HOL/Tools/refute.ML	Tue Oct 27 17:19:31 2009 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Tue Oct 27 17:34:00 2009 +0100
     1.3 @@ -25,16 +25,15 @@
     1.4  
     1.5    exception MAXVARS_EXCEEDED
     1.6  
     1.7 -  val add_interpreter : string -> (theory -> model -> arguments -> Term.term ->
     1.8 +  val add_interpreter : string -> (theory -> model -> arguments -> term ->
     1.9      (interpretation * model * arguments) option) -> theory -> theory
    1.10 -  val add_printer     : string -> (theory -> model -> Term.typ ->
    1.11 -    interpretation -> (int -> bool) -> Term.term option) -> theory -> theory
    1.12 +  val add_printer     : string -> (theory -> model -> typ ->
    1.13 +    interpretation -> (int -> bool) -> term option) -> theory -> theory
    1.14  
    1.15 -  val interpret : theory -> model -> arguments -> Term.term ->
    1.16 +  val interpret : theory -> model -> arguments -> term ->
    1.17      (interpretation * model * arguments)
    1.18  
    1.19 -  val print       : theory -> model -> Term.typ -> interpretation ->
    1.20 -    (int -> bool) -> Term.term
    1.21 +  val print       : theory -> model -> typ -> interpretation -> (int -> bool) -> term
    1.22    val print_model : theory -> model -> (int -> bool) -> string
    1.23  
    1.24  (* ------------------------------------------------------------------------- *)
    1.25 @@ -46,10 +45,10 @@
    1.26    val get_default_params : theory -> (string * string) list
    1.27    val actual_params      : theory -> (string * string) list -> params
    1.28  
    1.29 -  val find_model : theory -> params -> Term.term -> bool -> unit
    1.30 +  val find_model : theory -> params -> term -> bool -> unit
    1.31  
    1.32    (* tries to find a model for a formula: *)
    1.33 -  val satisfy_term   : theory -> (string * string) list -> Term.term -> unit
    1.34 +  val satisfy_term   : theory -> (string * string) list -> term -> unit
    1.35    (* tries to find a model that refutes a formula: *)
    1.36    val refute_term : theory -> (string * string) list -> term -> unit
    1.37    val refute_goal : theory -> (string * string) list -> thm -> int -> unit
    1.38 @@ -60,20 +59,18 @@
    1.39  (* Additional functions used by Nitpick (to be factored out)                 *)
    1.40  (* ------------------------------------------------------------------------- *)
    1.41  
    1.42 -  val close_form : Term.term -> Term.term
    1.43 -  val get_classdef : theory -> string -> (string * Term.term) option
    1.44 -  val norm_rhs : Term.term -> Term.term
    1.45 -  val get_def : theory -> string * Term.typ -> (string * Term.term) option
    1.46 -  val get_typedef : theory -> Term.typ -> (string * Term.term) option
    1.47 -  val is_IDT_constructor : theory -> string * Term.typ -> bool
    1.48 -  val is_IDT_recursor : theory -> string * Term.typ -> bool
    1.49 -  val is_const_of_class: theory -> string * Term.typ -> bool
    1.50 -  val monomorphic_term : Type.tyenv -> Term.term -> Term.term
    1.51 -  val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term
    1.52 -  val string_of_typ : Term.typ -> string
    1.53 -  val typ_of_dtyp :
    1.54 -    Datatype.descr -> (Datatype.dtyp * Term.typ) list -> Datatype.dtyp
    1.55 -    -> Term.typ
    1.56 +  val close_form : term -> term
    1.57 +  val get_classdef : theory -> string -> (string * term) option
    1.58 +  val norm_rhs : term -> term
    1.59 +  val get_def : theory -> string * typ -> (string * term) option
    1.60 +  val get_typedef : theory -> typ -> (string * term) option
    1.61 +  val is_IDT_constructor : theory -> string * typ -> bool
    1.62 +  val is_IDT_recursor : theory -> string * typ -> bool
    1.63 +  val is_const_of_class: theory -> string * typ -> bool
    1.64 +  val monomorphic_term : Type.tyenv -> term -> term
    1.65 +  val specialize_type : theory -> (string * typ) -> term -> term
    1.66 +  val string_of_typ : typ -> string
    1.67 +  val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
    1.68  end;  (* signature REFUTE *)
    1.69  
    1.70  structure Refute : REFUTE =
    1.71 @@ -185,7 +182,7 @@
    1.72  (* ------------------------------------------------------------------------- *)
    1.73  
    1.74    type model =
    1.75 -    (Term.typ * int) list * (Term.term * interpretation) list;
    1.76 +    (typ * int) list * (term * interpretation) list;
    1.77  
    1.78  (* ------------------------------------------------------------------------- *)
    1.79  (* arguments: additional arguments required during interpretation of terms   *)
    1.80 @@ -207,10 +204,10 @@
    1.81    structure RefuteData = TheoryDataFun
    1.82    (
    1.83      type T =
    1.84 -      {interpreters: (string * (theory -> model -> arguments -> Term.term ->
    1.85 +      {interpreters: (string * (theory -> model -> arguments -> term ->
    1.86          (interpretation * model * arguments) option)) list,
    1.87 -       printers: (string * (theory -> model -> Term.typ -> interpretation ->
    1.88 -        (int -> bool) -> Term.term option)) list,
    1.89 +       printers: (string * (theory -> model -> typ -> interpretation ->
    1.90 +        (int -> bool) -> term option)) list,
    1.91         parameters: string Symtab.table};
    1.92      val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
    1.93      val copy = I;