From b934a94a5d005f9d8e668ef49ec83487090a787b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 26 Jul 2006 15:50:54 +0000 Subject: [PATCH] Patch to the unification to make the case (i l) vs (t l) work when i is an inductive type and (t l) must be subject to weak head reduction. --- components/cic_unification/cicUnification.ml | 32 ++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml index 437d541ea..44712199e 100644 --- a/components/cic_unification/cicUnification.ml +++ b/components/cic_unification/cicUnification.ml @@ -625,6 +625,28 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ fo_unif_subst test_equality_only subst context metasenv redappl1 redappl2 ugraph) + (*CSC: This is necessary because of the "elim H" tactic + where the type of H is only reducible to an + inductive type. This could be extended from inductive + types to any rigid term. However, the code is + duplicated in two places: inside applications and + outside them. Probably it would be better to + work with lambda-bar terms instead. *) + | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn + | (_, Cic.MutInd _::_) -> + let t1' = R.whd ~subst context t1 in + (match t1' with + C.Appl (C.MutInd _::_) -> + fo_unif_subst test_equality_only + subst context metasenv t1' t2 ugraph + | _ -> raise (UnificationFailure (lazy "88"))) + | (Cic.MutInd _::_,_) -> + let t2' = R.whd ~subst context t2 in + (match t2' with + C.Appl (C.MutInd _::_) -> + fo_unif_subst test_equality_only + subst context metasenv t1 t2' ugraph + | _ -> raise (UnificationFailure (lazy "99"))) | _ -> raise exn))) | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> let subst', metasenv',ugraph1 = @@ -669,6 +691,16 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ in fo_unif_subst test_equality_only subst context metasenv beta_expanded (C.Meta (i,l)) ugraph1 +(* Works iff there are no arguments applied to it; similar to the + case below + | (_, C.MutInd _) -> + let t1' = R.whd ~subst context t1 in + (match t1' with + C.MutInd _ -> + fo_unif_subst test_equality_only + subst context metasenv t1' t2 ugraph + | _ -> raise (UnificationFailure (lazy "8"))) +*) (* The following idea could be exploited again; right now we have no longer any example requiring it | (C.Prod _, t2) -> -- 2.39.2