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      Utils.comparison) * (* ordering *)
   7     Cic.metasenv *       (* environment for metas *)
   8     Cic.term list        (* arguments *)
   9 ;;
  10
  11 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
  12
  13
  14 exception MatchingFailure
  15
  16 val matching:
  17   Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
  18   CicUniv.universe_graph ->
  19   Cic.substitution * Cic.metasenv * CicUniv.universe_graph
  20
  21 val unification:
  22   Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
  23   CicUniv.universe_graph ->
  24   Cic.substitution * Cic.metasenv * CicUniv.universe_graph
  25
  26
  27 (**
  28    Performs the beta expansion of the term "where" w.r.t. "what",
  29    i.e. returns the list of all the terms t s.t. "(t what) = where".
  30 *)
  31 val beta_expand:
  32   ?metas_ok:bool -> ?match_only:bool -> Cic.term -> Cic.term -> Cic.term ->
  33   Cic.context -> Cic.metasenv -> CicUniv.universe_graph ->
  34   (Cic.term * Cic.substitution * Cic.metasenv * CicUniv.universe_graph) list
  35
  36
  37 (**
  38    scans the context to find all Declarations "left = right"; returns a
  39    list of tuples (proof, (type, left, right), newmetas). Uses
  40    PrimitiveTactics.new_metasenv_for_apply to replace bound variables with
  41    fresh metas...
  42 *)
  43 val find_equalities:
  44   ?eq_uri:UriManager.uri -> Cic.context -> ProofEngineTypes.proof ->
  45   equality list * int
  46
  47
  48 exception TermIsNotAnEquality;;
  49
  50 (**
  51    raises TermIsNotAnEquality if term is not an equation.
  52    The first Cic.term is a proof of the equation
  53 *)
  54 val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term ->
  55   equality
  56
  57 (**
  58    superposition_left env target source
  59    returns a list of new clauses inferred with a left superposition step
  60    the negative equation "target" and the positive equation "source"
  61 *)
  62 val superposition_left: environment -> equality -> equality -> equality list
  63
  64 (**
  65    superposition_right newmeta env target source
  66    returns a list of new clauses inferred with a right superposition step
  67    the positive equations "target" and "source"
  68    "newmeta" is the first free meta index, i.e. the first number above the
  69    highest meta index: its updated value is also returned
  70 *)
  71 val superposition_right:
  72   int -> environment -> equality -> equality -> int * equality list
  73
  74 val demodulation: int -> environment -> equality -> equality -> int * equality
  75
  76 val meta_convertibility_eq: equality -> equality -> bool
  77
  78 val is_identity: environment -> equality -> bool
  79
  80 val string_of_equality: ?env:environment -> equality -> string
  81
  82 val subsumption: environment -> equality -> equality -> bool
  83
  84 val metas_of_term: Cic.term -> int list
  85
  86 val fix_metas: int -> equality -> int * equality
  87
  88 val extract_differing_subterms:
  89   Cic.term -> Cic.term -> (Cic.term * Cic.term) option