From 8a218c35f9bde765a73f14867a294c874f9dc15c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 29 Nov 2010 12:54:09 +0000 Subject: [PATCH] Back-porting from new Matita: - GREAT: when unifying ?1 : Type[i] with ?2: Type[j] the unifier randomly tried to instantiate ?1 with ?2 even when j > i, yielding to an unification error later on. In turn, this created that horrible behaviour of rewriting that failed if you did not pass enough types to the lemma. - in rewriting the argument is now automatically saturated These two fixes together allow most of the time to write simply >f as we did in the old system. --- .../components/ng_refiner/nCicUnification.ml | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index e2f6a7090..fcc76b0ad 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -382,8 +382,8 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap = | _ -> let lty = NCicSubstitution.subst_meta lc ty in pp (lazy ("On the types: " ^ - ppterm ~metasenv ~subst ~context lty ^ "=<=" ^ - ppterm ~metasenv ~subst ~context ty_t)); + ppterm ~metasenv ~subst ~context ty_t ^ "=<=" ^ + ppterm ~metasenv ~subst ~context lty)); let metasenv, subst = unify rdb false metasenv subst context ty_t lty false in @@ -559,6 +559,17 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) -> instantiate rdb test_eq_only metasenv subst context m lc' (NCicReduction.head_beta_reduce ~subst t1) (not swap) + | C.Meta (n,lc), C.Meta (m,lc') when + let _,_,tyn = NCicUtils.lookup_meta n metasenv in + let _,_,tym = NCicUtils.lookup_meta m metasenv in + let tyn = NCicSubstitution.subst_meta lc tyn in + let tym = NCicSubstitution.subst_meta lc tym in + match tyn,tym with + NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 -> + NCicEnvironment.universe_lt u1 u2 + | _,_ -> false -> + instantiate rdb test_eq_only metasenv subst context m lc' + (NCicReduction.head_beta_reduce ~subst t1) (not swap) | C.Meta (n,lc), t -> instantiate rdb test_eq_only metasenv subst context n lc (NCicReduction.head_beta_reduce ~subst t) swap @@ -865,7 +876,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = | KeepReducing _ -> assert false | KeepReducingThis _ -> assert (not (norm1 && norm2)); - unif_machines metasenv subst (small_delta_step ~subst m1 m2) + unif_machines metasenv subst (small_delta_step ~subst m1 m2) | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2)) -> unif_machines metasenv subst (small_delta_step ~subst m1 m2) | UnificationFailure msg -- 2.39.2