src/HOL/Library/refute.ML

renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish

(*  Title:      HOL/Library/refute.ML
    Author:     Tjark Weber, TU Muenchen

Finite model generation for HOL formulas, using a SAT solver.
*)

signature REFUTE =
sig

  exception REFUTE of string * string

(* ------------------------------------------------------------------------- *)
(* Model/interpretation related code (translation HOL -> propositional logic *)
(* ------------------------------------------------------------------------- *)

  type params
  type interpretation
  type model
  type arguments

  exception MAXVARS_EXCEEDED

  val add_interpreter : string -> (Proof.context -> model -> arguments -> term ->
    (interpretation * model * arguments) option) -> theory -> theory
  val add_printer : string -> (Proof.context -> model -> typ ->
    interpretation -> (int -> bool) -> term option) -> theory -> theory

  val interpret : Proof.context -> model -> arguments -> term ->
    (interpretation * model * arguments)

  val print : Proof.context -> model -> typ -> interpretation -> (int -> bool) -> term
  val print_model : Proof.context -> model -> (int -> bool) -> string

(* ------------------------------------------------------------------------- *)
(* Interface                                                                 *)
(* ------------------------------------------------------------------------- *)

  val set_default_param  : (string * string) -> theory -> theory
  val get_default_param  : Proof.context -> string -> string option
  val get_default_params : Proof.context -> (string * string) list
  val actual_params      : Proof.context -> (string * string) list -> params

  val find_model :
    Proof.context -> params -> term list -> term -> bool -> string

  (* tries to find a model for a formula: *)
  val satisfy_term :
    Proof.context -> (string * string) list -> term list -> term -> string
  (* tries to find a model that refutes a formula: *)
  val refute_term :
    Proof.context -> (string * string) list -> term list -> term -> string
  val refute_goal :
    Proof.context -> (string * string) list -> thm -> int -> string

  val setup : theory -> theory

(* ------------------------------------------------------------------------- *)
(* Additional functions used by Nitpick (to be factored out)                 *)
(* ------------------------------------------------------------------------- *)

  val get_classdef : theory -> string -> (string * term) option
  val norm_rhs : term -> term
  val get_def : theory -> string * typ -> (string * term) option
  val get_typedef : theory -> typ -> (string * term) option
  val is_IDT_constructor : theory -> string * typ -> bool
  val is_IDT_recursor : theory -> string * typ -> bool
  val is_const_of_class: theory -> string * typ -> bool
  val string_of_typ : typ -> string
end;

structure Refute : REFUTE =
struct

open Prop_Logic;

(* 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;


(* ------------------------------------------------------------------------- *)
(* TREES                                                                     *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* tree: implements an arbitrarily (but finitely) branching tree as a list   *)
(*       of (lists of ...) elements                                          *)
(* ------------------------------------------------------------------------- *)

datatype 'a tree =
    Leaf of 'a
  | Node of ('a tree) list;

fun tree_map f tr =
  case tr of
    Leaf x  => Leaf (f x)
  | Node xs => Node (map (tree_map f) xs);

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      *)
(*         formula/model generation                                          *)
(*                                                                           *)
(* The following parameters are supported (and required (!), except for      *)
(* "sizes" and "expect"):                                                    *)
(*                                                                           *)
(* Name          Type    Description                                         *)
(*                                                                           *)
(* "sizes"       (string * int) list                                         *)
(*                       Size of ground types (e.g. 'a=2), or depth of IDTs. *)
(* "minsize"     int     If >0, minimal size of each ground type/IDT depth.  *)
(* "maxsize"     int     If >0, maximal size of each ground type/IDT depth.  *)
(* "maxvars"     int     If >0, use at most 'maxvars' Boolean variables      *)
(*                       when transforming the term into a propositional     *)
(*                       formula.                                            *)
(* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)
(* "satsolver"   string  SAT solver to be used.                              *)
(* "no_assms"    bool    If "true", assumptions in structured proofs are     *)
(*                       not considered.                                     *)
(* "expect"      string  Expected result ("genuine", "potential", "none", or *)
(*                       "unknown").                                         *)
(* ------------------------------------------------------------------------- *)

type params =
  {
    sizes    : (string * int) list,
    minsize  : int,
    maxsize  : int,
    maxvars  : int,
    maxtime  : int,
    satsolver: string,
    no_assms : bool,
    expect   : string
  };

(* ------------------------------------------------------------------------- *)
(* interpretation: a term's interpretation is given by a variable of type    *)
(*                 'interpretation'                                          *)
(* ------------------------------------------------------------------------- *)

type interpretation =
  prop_formula list tree;

(* ------------------------------------------------------------------------- *)
(* model: a model specifies the size of types and the interpretation of      *)
(*        terms                                                              *)
(* ------------------------------------------------------------------------- *)

type model =
  (typ * int) list * (term * interpretation) list;

(* ------------------------------------------------------------------------- *)
(* arguments: additional arguments required during interpretation of terms   *)
(* ------------------------------------------------------------------------- *)

type arguments =
  {
    (* just passed unchanged from 'params': *)
    maxvars   : int,
    (* whether to use 'make_equality' or 'make_def_equality': *)
    def_eq    : bool,
    (* the following may change during the translation: *)
    next_idx  : int,
    bounds    : interpretation list,
    wellformed: prop_formula
  };

structure Data = Theory_Data
(
  type T =
    {interpreters: (string * (Proof.context -> model -> arguments -> term ->
      (interpretation * model * arguments) option)) list,
     printers: (string * (Proof.context -> model -> typ -> interpretation ->
      (int -> bool) -> term option)) list,
     parameters: string Symtab.table};
  val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
  val extend = I;
  fun merge
    ({interpreters = in1, printers = pr1, parameters = pa1},
     {interpreters = in2, printers = pr2, parameters = pa2}) : T =
    {interpreters = AList.merge (op =) (K true) (in1, in2),
     printers = AList.merge (op =) (K true) (pr1, pr2),
     parameters = Symtab.merge (op =) (pa1, pa2)};
);

val get_data = Data.get o Proof_Context.theory_of;


(* ------------------------------------------------------------------------- *)
(* interpret: interprets the term 't' using a suitable interpreter; returns  *)
(*            the interpretation and a (possibly extended) model that keeps  *)
(*            track of the interpretation of subterms                        *)
(* ------------------------------------------------------------------------- *)

fun interpret ctxt model args t =
  case get_first (fn (_, f) => f ctxt model args t)
      (#interpreters (get_data ctxt)) of
    NONE => raise REFUTE ("interpret",
      "no interpreter for term " ^ quote (Syntax.string_of_term ctxt t))
  | SOME x => x;

(* ------------------------------------------------------------------------- *)
(* print: converts the interpretation 'intr', which must denote a term of    *)
(*        type 'T', into a term using a suitable printer                     *)
(* ------------------------------------------------------------------------- *)

fun print ctxt model T intr assignment =
  case get_first (fn (_, f) => f ctxt model T intr assignment)
      (#printers (get_data ctxt)) of
    NONE => raise REFUTE ("print",
      "no printer for type " ^ quote (Syntax.string_of_typ ctxt T))
  | SOME x => x;

(* ------------------------------------------------------------------------- *)
(* print_model: turns the model into a string, using a fixed interpretation  *)
(*              (given by an assignment for Boolean variables) and suitable  *)
(*              printers                                                     *)
(* ------------------------------------------------------------------------- *)

fun print_model ctxt 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) =>
          Syntax.string_of_typ ctxt T ^ ": " ^ string_of_int i) typs) ^ "\n"
    val show_consts_msg =
      if not (Config.get ctxt show_consts) andalso Library.exists (is_Const o fst) terms then
        "enable \"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
        cat_lines (map_filter (fn (t, intr) =>
          (* print constants only if 'show_consts' is true *)
          if Config.get ctxt show_consts orelse not (is_Const t) then
            SOME (Syntax.string_of_term ctxt t ^ ": " ^
              Syntax.string_of_term ctxt
                (print ctxt model (Term.type_of t) intr assignment))
          else
            NONE) terms) ^ "\n"
  in
    typs_msg ^ show_consts_msg ^ terms_msg
  end;


(* ------------------------------------------------------------------------- *)
(* PARAMETER MANAGEMENT                                                      *)
(* ------------------------------------------------------------------------- *)

fun add_interpreter name f = Data.map (fn {interpreters, printers, parameters} =>
  case AList.lookup (op =) interpreters name of
    NONE => {interpreters = (name, f) :: interpreters,
      printers = printers, parameters = parameters}
  | SOME _ => error ("Interpreter " ^ name ^ " already declared"));

fun add_printer name f = Data.map (fn {interpreters, printers, parameters} =>
  case AList.lookup (op =) printers name of
    NONE => {interpreters = interpreters,
      printers = (name, f) :: printers, parameters = parameters}
  | SOME _ => error ("Printer " ^ name ^ " already declared"));

(* ------------------------------------------------------------------------- *)
(* set_default_param: stores the '(name, value)' pair in Data's              *)
(*                    parameter table                                        *)
(* ------------------------------------------------------------------------- *)

fun set_default_param (name, value) = Data.map
  (fn {interpreters, printers, parameters} =>
    {interpreters = interpreters, printers = printers,
      parameters = Symtab.update (name, value) parameters});

(* ------------------------------------------------------------------------- *)
(* get_default_param: retrieves the value associated with 'name' from        *)
(*                    Data's parameter table                                 *)
(* ------------------------------------------------------------------------- *)

val get_default_param = Symtab.lookup o #parameters o get_data;

(* ------------------------------------------------------------------------- *)
(* get_default_params: returns a list of all '(name, value)' pairs that are  *)
(*                     stored in Data's parameter table                      *)
(* ------------------------------------------------------------------------- *)

val get_default_params = Symtab.dest o #parameters o get_data;

(* ------------------------------------------------------------------------- *)
(* actual_params: takes a (possibly empty) list 'params' of parameters that  *)
(*      override the default parameters currently specified, and             *)
(*      returns a record that can be passed to 'find_model'.                 *)
(* ------------------------------------------------------------------------- *)

fun actual_params ctxt override =
  let
    fun read_bool (parms, name) =
      case AList.lookup (op =) parms name of
        SOME "true" => true
      | SOME "false" => false
      | SOME s => error ("parameter " ^ quote name ^
          " (value is " ^ quote s ^ ") must be \"true\" or \"false\"")
      | NONE   => error ("parameter " ^ quote name ^
          " must be assigned a value")
    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")
    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: *)
    val allparams = override @ get_default_params ctxt
    val minsize = read_int (allparams, "minsize")
    val maxsize = read_int (allparams, "maxsize")
    val maxvars = read_int (allparams, "maxvars")
    val maxtime = read_int (allparams, "maxtime")
    val satsolver = read_string (allparams, "satsolver")
    val no_assms = read_bool (allparams, "no_assms")
    val expect = the_default "" (AList.lookup (op =) allparams "expect")
    (* 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 = map_filter
      (fn (name, value) => Option.map (pair name) (Int.fromString value))
      (filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
        andalso name<>"maxvars" andalso name<>"maxtime"
        andalso name<>"satsolver" andalso name<>"no_assms") allparams)
  in
    {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars,
      maxtime=maxtime, satsolver=satsolver, no_assms=no_assms, expect=expect}
  end;


(* ------------------------------------------------------------------------- *)
(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
(* ------------------------------------------------------------------------- *)

fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) =
    the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a))
  | typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) =
    Type (s, map (typ_of_dtyp descr typ_assoc) Us)
  | typ_of_dtyp descr typ_assoc (Datatype.DtRec i) =
    let val (s, ds, _) = the (AList.lookup (op =) descr i) in
      Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    end

val close_form = ATP_Util.close_form
val monomorphic_term = ATP_Util.monomorphic_term
val specialize_type = ATP_Util.specialize_type

(* ------------------------------------------------------------------------- *)
(* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that   *)
(*                    denotes membership to an axiomatic type class          *)
(* ------------------------------------------------------------------------- *)

fun is_const_of_class thy (s, _) =
  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'.                   *)
    member (op =) class_const_names s
  end;

(* ------------------------------------------------------------------------- *)
(* is_IDT_constructor: returns 'true' iff 'Const (s, T)' is the constructor  *)
(*                     of an inductive datatype in 'thy'                     *)
(* ------------------------------------------------------------------------- *)

fun is_IDT_constructor thy (s, T) =
  (case body_type T of
    Type (s', _) =>
      (case Datatype.get_constrs thy s' of
        SOME constrs =>
          List.exists (fn (cname, cty) =>
            cname = s andalso Sign.typ_instance thy (T, cty)) constrs
      | NONE => false)
  | _  => false);

(* ------------------------------------------------------------------------- *)
(* is_IDT_recursor: returns 'true' iff 'Const (s, T)' is the recursion       *)
(*                  operator of an inductive datatype in 'thy'               *)
(* ------------------------------------------------------------------------- *)

fun is_IDT_recursor thy (s, _) =
  let
    val rec_names = Symtab.fold (append o #rec_names o snd)
      (Datatype.get_all thy) []
  in
    (* I'm not quite sure if checking the name 's' is sufficient, *)
    (* or if we should also check the type 'T'.                   *)
    member (op =) rec_names s
  end;

(* ------------------------------------------------------------------------- *)
(* norm_rhs: 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

(* ------------------------------------------------------------------------- *)
(* get_def: looks up the definition of a constant                            *)
(* ------------------------------------------------------------------------- *)

fun get_def thy (s, T) =
  let
    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"   *)
(* ------------------------------------------------------------------------- *)

fun get_typedef thy T =
  let
    fun get_typedef_ax [] = NONE
      | get_typedef_ax ((axname, ax) :: axioms) =
          (let
            fun type_of_type_definition (Const (s', T')) =
                  if s'= @{const_name type_definition} then
                    SOME T'
                  else
                    NONE
              | type_of_type_definition (Free _) = NONE
              | type_of_type_definition (Var _) = NONE
              | type_of_type_definition (Bound _) = NONE
              | type_of_type_definition (Abs (_, _, body)) =
                  type_of_type_definition body
              | type_of_type_definition (t1 $ t2) =
                  (case type_of_type_definition t1 of
                    SOME x => SOME x
                  | NONE => type_of_type_definition t2)
          in
            case type_of_type_definition ax of
              SOME T' =>
                let
                  val T'' = domain_type (domain_type T')
                  val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty
                in
                  SOME (axname, monomorphic_term typeSubs ax)
                end
            | NONE => get_typedef_ax axioms
          end handle ERROR _         => get_typedef_ax axioms
                   | TERM _          => get_typedef_ax axioms
                   | Type.TYPE_MATCH => get_typedef_ax axioms)
  in
    get_typedef_ax (Theory.all_axioms_of thy)
  end;

(* ------------------------------------------------------------------------- *)
(* get_classdef: looks up the defining axiom for an axiomatic type class, as *)
(*               created by the "axclass" command                            *)
(* ------------------------------------------------------------------------- *)

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        *)
(*              normalizes the result term; certain constants are not        *)
(*              unfolded (cf. 'collect_axioms' and the various interpreters  *)
(*              below): if the interpretation respects a definition anyway,  *)
(*              that definition does not need to be unfolded                 *)
(* ------------------------------------------------------------------------- *)

(* 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
    fun unfold_loop t =
      case t of
      (* Pure *)
        Const (@{const_name Pure.all}, _) => t
      | Const (@{const_name Pure.eq}, _) => t
      | Const (@{const_name Pure.imp}, _) => t
      | Const (@{const_name Pure.type}, _) => t  (* axiomatic type classes *)
      (* HOL *)
      | Const (@{const_name Trueprop}, _) => t
      | Const (@{const_name Not}, _) => t
      | (* redundant, since 'True' is also an IDT constructor *)
        Const (@{const_name True}, _) => t
      | (* redundant, since 'False' is also an IDT constructor *)
        Const (@{const_name False}, _) => t
      | Const (@{const_name undefined}, _) => t
      | Const (@{const_name The}, _) => t
      | Const (@{const_name Hilbert_Choice.Eps}, _) => t
      | Const (@{const_name All}, _) => t
      | Const (@{const_name Ex}, _) => t
      | Const (@{const_name HOL.eq}, _) => t
      | Const (@{const_name HOL.conj}, _) => t
      | Const (@{const_name HOL.disj}, _) => t
      | Const (@{const_name HOL.implies}, _) => t
      (* sets *)
      | Const (@{const_name Collect}, _) => t
      | Const (@{const_name Set.member}, _) => t
      (* other optimizations *)
      | Const (@{const_name Finite_Set.card}, _) => t
      | Const (@{const_name Finite_Set.finite}, _) => t
      | Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
          Type ("fun", [@{typ nat}, @{typ bool}])])) => t
      | Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
          Type ("fun", [@{typ nat}, @{typ nat}])])) => t
      | Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
          Type ("fun", [@{typ nat}, @{typ nat}])])) => t
      | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
          Type ("fun", [@{typ nat}, @{typ nat}])])) => t
      | Const (@{const_name append}, _) => t
(* UNSOUND
      | Const (@{const_name lfp}, _) => t
      | Const (@{const_name gfp}, _) => t
*)
      | Const (@{const_name fst}, _) => t
      | Const (@{const_name snd}, _) => t
      (* simply-typed lambda calculus *)
      | Const (s, T) =>
          (if is_IDT_constructor thy (s, T)
            orelse is_IDT_recursor thy (s, T) then
            t  (* do not unfold IDT constructors/recursors *)
          (* unfold the constant if there is a defining equation *)
          else
            case get_def thy (s, T) of
              SOME ((*axname*) _, rhs) =>
              (* Note: if the term to be unfolded (i.e. 'Const (s, T)')  *)
              (* occurs on the right-hand side of the equation, i.e. in  *)
              (* 'rhs', we must not use this equation to unfold, because *)
              (* that would loop.  Here would be the right place to      *)
              (* check this.  However, getting this really right seems   *)
              (* difficult because the user may state arbitrary axioms,  *)
              (* which could interact with overloading to create loops.  *)
              ((*tracing (" unfolding: " ^ axname);*)
               unfold_loop rhs)
            | NONE => t)
      | Free _ => t
      | Var _ => t
      | Bound _ => t
      | 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: currently we use "inverse" functions to the definitional         *)
(*       mechanisms provided by Isabelle/HOL, e.g. for "axclass",         *)
(*       "typedef", "definition".  A more general approach could consider *)
(*       *every* axiom of the theory and collect it if it has a constant/ *)
(*       type/typeclass in common with the term 't'.                      *)

(* 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.          *)

local

fun get_axiom thy xname =
  Name_Space.check (Context.Theory thy) (Theory.axiom_table thy) (xname, Position.none);

val the_eq_trivial = get_axiom @{theory HOL} "the_eq_trivial";
val someI = get_axiom @{theory Hilbert_Choice} "someI";

in

fun collect_axioms ctxt t =
  let
    val thy = Proof_Context.theory_of ctxt
    val _ = tracing "Adding axioms..."
    val axioms = Theory.all_axioms_of thy
    fun collect_this_axiom (axname, ax) axs =
      let
        val ax' = unfold_defs thy ax
      in
        if member (op aconv) axs ax' then axs
        else (tracing axname; collect_term_axioms ax' (ax' :: axs))
      end
    and collect_sort_axioms T axs =
      let
        val sort =
          (case T of
            TFree (_, sort) => sort
          | TVar (_, sort)  => sort
          | _ => raise REFUTE ("collect_axioms",
              "type " ^ Syntax.string_of_typ ctxt 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_info 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.add_tvars ax [] of
            [] => (axname, ax)
          | [(idx, S)] => (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
          | _ =>
            raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^
              Syntax.string_of_term ctxt ax ^
              ") contains more than one type variable")))
          class_axioms
      in
        fold collect_this_axiom monomorphic_class_axioms axs
      end
    and collect_type_axioms T axs =
      case T of
      (* simple types *)
        Type (@{type_name prop}, []) => axs
      | Type (@{type_name fun}, [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
      | Type (@{type_name set}, [T1]) => collect_type_axioms T1 axs
      (* axiomatic type classes *)
      | Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
      | Type (s, Ts) =>
        (case Datatype.get_info thy s of
          SOME _ =>  (* inductive datatype *)
            (* only collect relevant type axioms for the argument types *)
            fold collect_type_axioms Ts axs
        | 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 *)
            fold collect_type_axioms Ts axs))
      (* axiomatic type classes *)
      | TFree _ => collect_sort_axioms T axs
      (* axiomatic type classes *)
      | TVar _ => collect_sort_axioms T axs
    and collect_term_axioms t axs =
      case t of
      (* Pure *)
        Const (@{const_name Pure.all}, _) => axs
      | Const (@{const_name Pure.eq}, _) => axs
      | Const (@{const_name Pure.imp}, _) => axs
      (* axiomatic type classes *)
      | Const (@{const_name Pure.type}, T) => collect_type_axioms T axs
      (* HOL *)
      | Const (@{const_name Trueprop}, _) => axs
      | Const (@{const_name Not}, _) => axs
      (* redundant, since 'True' is also an IDT constructor *)
      | Const (@{const_name True}, _) => axs
      (* redundant, since 'False' is also an IDT constructor *)
      | Const (@{const_name False}, _) => axs
      | Const (@{const_name undefined}, T) => collect_type_axioms T axs
      | Const (@{const_name The}, T) =>
          let
            val ax = specialize_type thy (@{const_name The}, T) (#2 the_eq_trivial)
          in
            collect_this_axiom (#1 the_eq_trivial, ax) axs
          end
      | Const (@{const_name Hilbert_Choice.Eps}, T) =>
          let
            val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T) (#2 someI)
          in
            collect_this_axiom (#1 someI, ax) axs
          end
      | Const (@{const_name All}, T) => collect_type_axioms T axs
      | Const (@{const_name Ex}, T) => collect_type_axioms T axs
      | Const (@{const_name HOL.eq}, T) => collect_type_axioms T axs
      | Const (@{const_name HOL.conj}, _) => axs
      | Const (@{const_name HOL.disj}, _) => axs
      | Const (@{const_name HOL.implies}, _) => axs
      (* sets *)
      | Const (@{const_name Collect}, T) => collect_type_axioms T axs
      | Const (@{const_name Set.member}, T) => collect_type_axioms T axs
      (* other optimizations *)
      | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
      | Const (@{const_name Finite_Set.finite}, T) =>
        collect_type_axioms T axs
      | Const (@{const_name Orderings.less}, T as Type ("fun", [@{typ nat},
        Type ("fun", [@{typ nat}, @{typ bool}])])) =>
          collect_type_axioms T axs
      | Const (@{const_name Groups.plus}, T as Type ("fun", [@{typ nat},
        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
          collect_type_axioms T axs
      | Const (@{const_name Groups.minus}, T as Type ("fun", [@{typ nat},
        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
          collect_type_axioms T axs
      | Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat},
        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
          collect_type_axioms T axs
      | Const (@{const_name append}, T) => collect_type_axioms T axs
(* UNSOUND
      | Const (@{const_name lfp}, T) => collect_type_axioms T axs
      | Const (@{const_name gfp}, T) => collect_type_axioms T axs
*)
      | Const (@{const_name fst}, T) => collect_type_axioms T axs
      | Const (@{const_name snd}, T) => collect_type_axioms T axs
      (* 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 of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class)
              val ax_in = SOME (specialize_type thy (s, T) of_class)
                (* type match may fail due to sort constraints *)
                handle Type.TYPE_MATCH => NONE
              val ax_1 = Option.map (fn ax => (Syntax.string_of_term ctxt ax, ax)) ax_in
              val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) (get_classdef thy class)
            in
              collect_type_axioms T (fold collect_this_axiom (map_filter I [ax_1, ax_2]) axs)
            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 T axs
          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 T axs
      | Free (_, T) => collect_type_axioms T axs
      | Var (_, T) => collect_type_axioms T axs
      | Bound _ => axs
      | Abs (_, T, body) => collect_term_axioms body (collect_type_axioms T axs)
      | t1 $ t2 => collect_term_axioms t2 (collect_term_axioms t1 axs)
    val result = map close_form (collect_term_axioms t [])
    val _ = tracing " ...done."
  in
    result
  end;

end;

(* ------------------------------------------------------------------------- *)
(* ground_types: collects all ground types in a term (including argument     *)
(*               types of other types), suppressing duplicates.  Does not    *)
(*               return function types, set types, non-recursive IDTs, or    *)
(*               'propT'.  For IDTs, also the argument types of constructors *)
(*               and all mutually recursive IDTs are considered.             *)
(* ------------------------------------------------------------------------- *)

fun ground_types ctxt t =
  let
    val thy = Proof_Context.theory_of ctxt
    fun collect_types T acc =
      (case T of
        Type (@{type_name fun}, [T1, T2]) => collect_types T1 (collect_types T2 acc)
      | Type (@{type_name prop}, []) => acc
      | Type (@{type_name set}, [T1]) => collect_types T1 acc
      | Type (s, Ts) =>
          (case Datatype.get_info thy s of
            SOME info =>  (* inductive datatype *)
              let
                val index = #index info
                val descr = #descr info
                val (_, typs, _) = the (AList.lookup (op =) descr index)
                val typ_assoc = typs ~~ Ts
                (* sanity check: every element in 'dtyps' must be a *)
                (* 'DtTFree'                                        *)
                val _ = if Library.exists (fn d =>
                  case d of Datatype.DtTFree _ => false | _ => true) typs then
                  raise REFUTE ("ground_types", "datatype argument (for type "
                    ^ Syntax.string_of_typ ctxt T ^ ") is not a variable")
                else ()
                (* required for mutually recursive datatypes; those need to   *)
                (* be added even if they are an instance of an otherwise non- *)
                (* recursive datatype                                         *)
                fun collect_dtyp d acc =
                  let
                    val dT = typ_of_dtyp descr typ_assoc d
                  in
                    case d of
                      Datatype.DtTFree _ =>
                      collect_types dT acc
                    | Datatype.DtType (_, ds) =>
                      collect_types dT (fold_rev collect_dtyp ds acc)
                    | Datatype.DtRec i =>
                      if member (op =) acc dT then
                        acc  (* prevent infinite recursion *)
                      else
                        let
                          val (_, dtyps, dconstrs) = the (AList.lookup (op =) descr i)
                          (* if the current type is a recursive IDT (i.e. a depth *)
                          (* is required), add it to 'acc'                        *)
                          val acc_dT = if Library.exists (fn (_, ds) =>
                            Library.exists Datatype_Aux.is_rec_type ds) dconstrs then
                              insert (op =) dT acc
                            else acc
                          (* collect argument types *)
                          val acc_dtyps = fold_rev collect_dtyp dtyps acc_dT
                          (* collect constructor types *)
                          val acc_dconstrs = fold_rev collect_dtyp (maps snd dconstrs) acc_dtyps
                        in
                          acc_dconstrs
                        end
                  end
              in
                (* argument types 'Ts' could be added here, but they are also *)
                (* added by 'collect_dtyp' automatically                      *)
                collect_dtyp (Datatype.DtRec index) acc
              end
          | NONE =>
            (* not an inductive datatype, e.g. defined via "typedef" or *)
            (* "typedecl"                                               *)
            insert (op =) T (fold collect_types Ts acc))
      | TFree _ => insert (op =) T acc
      | TVar _ => insert (op =) T acc)
  in
    fold_types collect_types t []
  end;

(* ------------------------------------------------------------------------- *)
(* string_of_typ: (rather naive) conversion from types to strings, used to   *)
(*                look up the size of a type in 'sizes'.  Parameterized      *)
(*                types with different parameters (e.g. "'a list" vs. "bool  *)
(*                list") are identified.                                     *)
(* ------------------------------------------------------------------------- *)

fun string_of_typ (Type (s, _))     = s
  | string_of_typ (TFree (s, _))    = s
  | string_of_typ (TVar ((s,_), _)) = s;

(* ------------------------------------------------------------------------- *)
(* first_universe: returns the "first" (i.e. smallest) universe by assigning *)
(*                 'minsize' to every type for which no size is specified in *)
(*                 'sizes'                                                   *)
(* ------------------------------------------------------------------------- *)

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     *)
(*                types), where the minimal size of a type is given by       *)
(*                'minsize', the maximal size is given by 'maxsize', and a   *)
(*                type may have a fixed size given in 'sizes'                *)
(* ------------------------------------------------------------------------- *)

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'              *)
    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)                                *)
    fun next _ _ _ [] =
          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<max orelse max<0) then
            (* we can shift *)
            SOME (the (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
          else
            (* continue search *)
            next max (len+1) (sum+x1) (x2::xs)
    (* only consider those types for which the size is not fixed *)
    val mutables = filter_out (AList.defined (op =) sizes o string_of_typ o fst) xs
    (* subtract 'minsize' from every size (will be added again at the end) *)
    val diffs = map (fn (_, n) => n-minsize) mutables
  in
    case next (maxsize-minsize) 0 0 diffs of
      SOME diffs' =>
        (* merge with those types for which the size is fixed *)
        SOME (fst (fold_map (fn (T, _) => fn ds =>
          case AList.lookup (op =) sizes (string_of_typ T) of
          (* return the fixed size *)
            SOME n => ((T, n), ds)
          (* consume the head of 'ds', add 'minsize' *)
          | NONE   => ((T, minsize + hd ds), tl ds))
          xs diffs'))
    | NONE => NONE
  end;

(* ------------------------------------------------------------------------- *)
(* toTrue: converts the interpretation of a Boolean value to a propositional *)
(*         formula that is true iff the interpretation denotes "true"        *)
(* ------------------------------------------------------------------------- *)

fun toTrue (Leaf [fm, _]) = fm
  | toTrue _ = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value");

(* ------------------------------------------------------------------------- *)
(* toFalse: converts the interpretation of a Boolean value to a              *)
(*          propositional formula that is true iff the interpretation        *)
(*          denotes "false"                                                  *)
(* ------------------------------------------------------------------------- *)

fun toFalse (Leaf [_, fm]) = fm
  | toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value");

(* ------------------------------------------------------------------------- *)
(* find_model: repeatedly calls 'interpret' with appropriate parameters,     *)
(*             applies a SAT solver, and (in case a model is found) displays *)
(*             the model to the user by calling 'print_model'                *)
(* {...}     : parameters that control the translation/model generation      *)
(* assm_ts   : assumptions to be considered unless "no_assms" is specified   *)
(* t         : term to be translated into a propositional formula            *)
(* negate    : if true, find a model that makes 't' false (rather than true) *)
(* ------------------------------------------------------------------------- *)

fun find_model ctxt
    {sizes, minsize, maxsize, maxvars, maxtime, satsolver, no_assms, expect}
    assm_ts t negate =
  let
    val thy = Proof_Context.theory_of ctxt
    fun check_expect outcome_code =
      if expect = "" orelse outcome_code = expect then outcome_code
      else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
    fun wrapper () =
      let
        val timer = Timer.startRealTimer ()
        val t =
          if no_assms then t
          else if negate then Logic.list_implies (assm_ts, t)
          else Logic.mk_conjunction_list (t :: assm_ts)
        val u = unfold_defs thy t
        val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term ctxt u)
        val axioms = collect_axioms ctxt u
        val types = fold (union (op =) o ground_types ctxt) (u :: axioms) []
        val _ = tracing ("Ground types: "
          ^ (if null types then "none."
             else commas (map (Syntax.string_of_typ ctxt) types)))
        (* we can only consider fragments of recursive IDTs, so we issue a  *)
        (* warning if the formula contains a recursive IDT                  *)
        (* TODO: no warning needed for /positive/ occurrences of IDTs       *)
        val maybe_spurious = Library.exists (fn
            Type (s, _) =>
              (case Datatype.get_info thy s of
                SOME info =>  (* inductive datatype *)
                  let
                    val index           = #index info
                    val descr           = #descr info
                    val (_, _, constrs) = the (AList.lookup (op =) descr index)
                  in
                    (* recursive datatype? *)
                    Library.exists (fn (_, ds) =>
                      Library.exists Datatype_Aux.is_rec_type ds) constrs
                  end
              | NONE => false)
          | _ => false) types
        val _ =
          if maybe_spurious then
            warning ("Term contains a recursive datatype; "
              ^ "countermodel(s) may be spurious!")
          else
            ()
        fun find_model_loop universe =
          let
            val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
            val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime
                    orelse raise TimeLimit.TimeOut
            val init_model = (universe, [])
            val init_args  = {maxvars = maxvars, def_eq = false, next_idx = 1,
              bounds = [], wellformed = True}
            val _ = tracing ("Translating term (sizes: "
              ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
            (* translate 'u' and all axioms *)
            val (intrs, (model, args)) = fold_map (fn t' => fn (m, a) =>
              let
                val (i, m', a') = interpret ctxt m a t'
              in
                (* set 'def_eq' to 'true' *)
                (i, (m', {maxvars = #maxvars a', def_eq = true,
                  next_idx = #next_idx a', bounds = #bounds a',
                  wellformed = #wellformed a'}))