From b5b653d8880924fe05233f4eb160a189c8a995b8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 25 Oct 2005 08:22:12 +0000 Subject: [PATCH] Bug fixed: the current substitution and metasenv were not propagated to the check_allowed_sort_elimination function. As a result: 1. useless metas were opened by the apply tactic 2. sometimes unification failed --- .../cic_proof_checking/cicTypeChecker.ml | 30 +++++++++++-------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 18de8af5e..b24c5fc8e 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1263,16 +1263,18 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = args coInductiveTypeURI ) fl true -and check_allowed_sort_elimination ~logger context uri i need_dummy ind - arity1 arity2 ugraph = +and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i + need_dummy ind arity1 arity2 ugraph = let module C = Cic in let module U = UriManager in - match (CicReduction.whd context arity1, CicReduction.whd context arity2) with + match (CicReduction.whd ~subst context arity1, CicReduction.whd ~subst context arity2) with (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) -> - let b,ugraph1 = CicReduction.are_convertible context so1 so2 ugraph in + let b,ugraph1 = + CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in if b then - check_allowed_sort_elimination ~logger context uri i need_dummy - (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1 + check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i + need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 + ugraph1 else false,ugraph1 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph @@ -1322,11 +1324,12 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph (* TASSI: da verificare *) | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy -> - let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in + let b,ugraph1 = + CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in if not b then false,ugraph1 else - (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with + (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with C.Sort C.Prop -> true,ugraph1 | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in @@ -1343,11 +1346,12 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta))) when not need_dummy -> - let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in + let b,ugraph1 = + CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in if not b then false,ugraph1 else - (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with + (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with C.Sort C.Prop | C.Sort C.Set -> true,ugraph1 | C.Sort C.CProp -> true,ugraph1 @@ -1377,7 +1381,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind ) | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy -> (* TASSI: da verificare *) - CicReduction.are_convertible context so ind ugraph + CicReduction.are_convertible ~subst ~metasenv context so ind ugraph | (_,_) -> false,ugraph and type_of_branch context argsno need_dummy outtype term constype = @@ -1741,8 +1745,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let type_of_sort_of_ind_ty,ugraph3 = type_of_aux ~logger context sort_of_ind_type ugraph2 in let b,ugraph4 = - check_allowed_sort_elimination ~logger context uri i need_dummy - sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3 + check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i + need_dummy sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3 in if not b then raise -- 2.39.2