helm/ocaml/paramodulation/inference.mli

   1 type equality =
   2     Cic.term *     (* proof *)
   3     (Cic.term *    (* type *)
   4      Cic.term *    (* left side *)
   5      Cic.term) *   (* right side *)
   6     Cic.metasenv * (* environment for metas *)
   7     Cic.term list  (* arguments *)
   8 ;;
   9
  10 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
  11
  12
  13 (**
  14    Performs the beta expansion of the term "where" w.r.t. "what",
  15    i.e. returns the list of all the terms t s.t. "(t what) = where".
  16 *)
  17 val beta_expand:
  18   ?metas_ok:bool -> ?match_only:bool -> Cic.term -> Cic.term -> Cic.term ->
  19   Cic.context -> Cic.metasenv -> CicUniv.universe_graph ->
  20   (Cic.term * Cic.substitution * Cic.metasenv * CicUniv.universe_graph) list
  21
  22
  23 (**
  24    scans the context to find all Declarations "left = right"; returns a
  25    list of tuples (proof, (type, left, right), newmetas). Uses
  26    PrimitiveTactics.new_metasenv_for_apply to replace bound variables with
  27    fresh metas...
  28 *)
  29 val find_equalities:
  30   ?eq_uri:UriManager.uri -> Cic.context -> ProofEngineTypes.proof ->
  31   equality list * int
  32
  33
  34 exception TermIsNotAnEquality;;
  35
  36 (**
  37    raises TermIsNotAnEquality if term is not an equation.
  38    The first Cic.term is a proof of the equation
  39 *)
  40 val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term ->
  41   equality
  42
  43 (**
  44    superposition_left env target source
  45    returns a list of new clauses inferred with a left superposition step
  46    the negative equation "target" and the positive equation "source"
  47 *)
  48 val superposition_left: environment -> equality -> equality -> equality list
  49
  50 (**
  51    superposition_right newmeta env target source
  52    returns a list of new clauses inferred with a right superposition step
  53    the positive equations "target" and "source"
  54    "newmeta" is the first free meta index, i.e. the first number above the
  55    highest meta index: its updated value is also returned
  56 *)
  57 val superposition_right:
  58   int -> environment -> equality -> equality -> int * equality list
  59
  60 val demodulation: int -> environment -> equality -> equality -> int * equality
  61
  62 val meta_convertibility_eq: equality -> equality -> bool
  63
  64 val is_identity: environment -> equality -> bool
  65
  66