From 73b49101cb8f83bc54fd2dc3c862b42c00ad13b5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 26 Nov 2010 13:18:50 +0000 Subject: [PATCH] - 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. --- matita/components/ng_refiner/nCicUnification.ml | 17 ++++++++++++++--- matita/components/ng_tactics/nTactics.ml | 1 + 2 files changed, 15 insertions(+), 3 deletions(-) diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml index 5500abcbf..a74172ca0 100644 --- a/matita/components/ng_refiner/nCicUnification.ml +++ b/matita/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 @@ -866,7 +877,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 diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index 15e77f094..9c9f0d73a 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -542,6 +542,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status = `LeftToRight -> "eq" ^ suffix ^ "_r" | `RightToLeft -> "eq" ^ suffix in + let what = Ast.Appl [what; Ast.Implicit `Vector] in block_tac [ select_tac ~where ~job:(`Substexpand 2) true; exact_tac -- 2.39.2