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