From e46885466c473f4519a210edbe744d71e54af675 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 22 Jan 2004 10:29:33 +0000 Subject: [PATCH] split into this and cicMetaSubst.mli --- helm/ocaml/cic_unification/cicUnification.mli | 41 +++---------------- 1 file changed, 6 insertions(+), 35 deletions(-) diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli index 30094f7f2..40b9f8ef7 100644 --- a/helm/ocaml/cic_unification/cicUnification.mli +++ b/helm/ocaml/cic_unification/cicUnification.mli @@ -23,16 +23,8 @@ * http://cs.unibo.it/helm/. *) -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 +exception AssertFailure of string +exception UnificationFailure of string (* fo_unif metasenv context t1 t2 *) (* unifies [t1] and [t2] in a context [context]. *) @@ -42,7 +34,7 @@ type substitution = (int * Cic.term) list (* withouth first unwinding it. *) val fo_unif : Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> - substitution * Cic.metasenv + CicMetaSubst.substitution * Cic.metasenv (* fo_unif_subst metasenv subst context t1 t2 *) (* unifies [t1] and [t2] in a context [context] *) @@ -58,28 +50,7 @@ val fo_unif : (*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 [subst] to [t] *) -(* [subst] must be already unwinded *) -val apply_subst : substitution -> Cic.term -> Cic.term + CicMetaSubst.substitution -> + Cic.context -> Cic.metasenv -> Cic.term -> Cic.term -> + CicMetaSubst.substitution * Cic.metasenv -(* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) -(* performs as (apply_subst subst t) until it finds an application of *) -(* (META [mtr]) that, once unwinding is performed, creates a new *) -(* beta-redex; in this case up to [reductions_no] consecutive *) -(* beta-reductions are performed. *) -(* Hint: this function is usually called when [reductions_no] *) -(* 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 -- 2.39.2