X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.mli;h=4bb43ea8fa2761538273c750d5d7f7896445b0e4;hb=259a4a2080cc5af5b20da1cd9133eb32f28c5d8f;hp=4e1fe2c0adc5cc2d68fcacf75c545be274e7cea3;hpb=d8c8060ad0cfc9b93ce919b6662383a230192840;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 4e1fe2c0a..4bb43ea8f 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -1,15 +1,42 @@ type equality = - Cic.term * (* proof *) - (Cic.term * (* type *) - Cic.term * (* left side *) - Cic.term) * (* right side *) - Cic.metasenv * (* environment for metas *) - Cic.term list (* arguments *) -;; + int * (* weight *) + proof * + (Cic.term * (* type *) + Cic.term * (* left side *) + Cic.term * (* right side *) + Utils.comparison) * (* ordering *) + Cic.metasenv * (* environment for metas *) + Cic.term list (* arguments *) -type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; +and proof = + | NoProof + | BasicProof of Cic.term + | ProofBlock of + Cic.substitution * UriManager.uri * + (Cic.name * Cic.term) * Cic.term * + (* name, ty, eq_ty, left, right *) +(* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *) + (Utils.pos * equality) * proof + | ProofGoalBlock of proof * proof (* equality *) + | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof +type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph + + +exception MatchingFailure + +val matching: + Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> + CicUniv.universe_graph -> + Cic.substitution * Cic.metasenv * CicUniv.universe_graph + +val unification: + Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> + CicUniv.universe_graph -> + Cic.substitution * Cic.metasenv * CicUniv.universe_graph + + (** Performs the beta expansion of the term "where" w.r.t. "what", i.e. returns the list of all the terms t s.t. "(t what) = where". @@ -40,12 +67,14 @@ exception TermIsNotAnEquality;; val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term -> equality +val term_is_equality: ?eq_uri:UriManager.uri -> Cic.term -> bool + (** superposition_left env target source returns a list of new clauses inferred with a left superposition step the negative equation "target" and the positive equation "source" *) -val superposition_left: environment -> equality -> equality -> equality list +(* val superposition_left: environment -> equality -> equality -> equality list *) (** superposition_right newmeta env target source @@ -54,13 +83,30 @@ val superposition_left: environment -> equality -> equality -> equality list "newmeta" is the first free meta index, i.e. the first number above the highest meta index: its updated value is also returned *) -val superposition_right: - int -> environment -> equality -> equality -> int * equality list +(* val superposition_right: *) +(* int -> environment -> equality -> equality -> int * equality list *) -val demodulation: int -> environment -> equality -> equality -> int * equality +(* val demodulation: int -> environment -> equality -> equality -> int * equality *) +val meta_convertibility: Cic.term -> Cic.term -> bool + val meta_convertibility_eq: equality -> equality -> bool val is_identity: environment -> equality -> bool +val string_of_equality: ?env:environment -> equality -> string +(* val subsumption: environment -> equality -> equality -> bool *) + +val metas_of_term: Cic.term -> int list + +val fix_metas: int -> equality -> int * equality + +val extract_differing_subterms: + Cic.term -> Cic.term -> (Cic.term * Cic.term) option + +val build_proof_term: equality -> Cic.term + +val find_library_equalities: + dbd:HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> + equality list * int