X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.mli;h=30094f7f2b7d2b7f0c6a1db9bd2d8794317a222f;hb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;hp=9fde49d9e22c6273a4ac46965498821de5b1eaf0;hpb=211f0ab4ee4c22c98147067987874b0b5a800b5b;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli
index 9fde49d9e..30094f7f2 100644
--- a/helm/ocaml/cic_unification/cicUnification.mli
+++ b/helm/ocaml/cic_unification/cicUnification.mli
@@ -27,6 +27,9 @@ exception UnificationFailed
 exception Free
 exception OccurCheck
 
+val delift : 
+ Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv
+
 (* The entry (i,t) in a substitution means that *)
 (* (META i) have been instantiated with t.      *)
 type substitution = (int * Cic.term) list
@@ -35,11 +38,37 @@ type substitution = (int * Cic.term) list
 (* unifies [t1] and [t2] in a context [context]. *)
 (* Only the metavariables declared in [metasenv] *)
 (* can be used in [t1] and [t2].                 *)
+(* The returned substitution can be directly     *)
+(* withouth first unwinding it.                  *)
 val fo_unif :
-  (int * Cic.term) list -> Cic.context -> Cic.term -> Cic.term -> substitution
+  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+   substitution * Cic.metasenv
+
+(* fo_unif_subst metasenv subst context t1 t2    *)
+(* unifies [t1] and [t2] in a context [context]  *)
+(* and with [subst] as the current substitution  *)
+(* (i.e. unifies ([subst] [t1]) and              *)
+(* ([subst] [t2]) in a context                   *)
+(* ([subst] [context]) using the metasenv        *)
+(* ([subst] [metasenv])                          *)
+(* Only the metavariables declared in [metasenv] *)
+(* can be used in [t1] and [t2].                 *)
+(* [subst] and the substitution returned are not *)
+(* unwinded.                                     *)
+(*CSC: fare un tipo unione Unwinded o ToUnwind e fare gestire la
+ cosa all'apply_subst!!!*)
+val fo_unif_subst :
+  substitution -> Cic.context -> Cic.metasenv -> Cic.term -> Cic.term ->
+   substitution * Cic.metasenv
+
+(* unwind_subst metasenv subst                         *)
+(* unwinds [subst] w.r.t. itself.                      *)
+(* It can restrict some metavariable in the [metasenv] *)
+val unwind_subst : Cic.metasenv -> substitution -> substitution * Cic.metasenv
 
-(* apply_subst subst t                    *)
-(* applies the substitution [sust] to [t] *)
+(* apply_subst subst t                     *)
+(* applies the substitution [subst] to [t] *)
+(* [subst] must be already unwinded        *)
 val apply_subst : substitution -> Cic.term -> Cic.term
 
 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
@@ -51,5 +80,6 @@ val apply_subst : substitution -> Cic.term -> Cic.term
 (*  eta-expansions have been performed and the head of the new          *)
 (*  application has been unified with (META [meta_to_reduce]):          *)
 (*  during the unwinding the eta-expansions are undone.                 *)
+(* [subst] must be already unwinded                                     *)
 val apply_subst_reducing :
  substitution -> (int * int) option -> Cic.term -> Cic.term