From 267fbbcd1b8c54ce7faafd48cface965d0f6c37b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 17:31:41 +0000 Subject: [PATCH] This commit avoids cleaning dummy dependent types in the arities of inductive types. This is an overkilling solution to the problem of avoiding cleaning dummy dependent types in the left products in the arities of inductive types. The left products should be _syntactically_ the same as those of the constructors. Otherwise, error reporting is incorrect. --- .../components/cic_unification/cicRefine.ml | 20 +++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 5aa96944d..45c2d26ea 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -322,7 +322,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | _ -> raise (AssertFailure (lazy "Wrong number of arguments"))) | _ -> raise (AssertFailure (lazy "Prod or MutInd expected")) -and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t +and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t ugraph = let rec type_of_aux subst metasenv context t ugraph = @@ -1745,10 +1745,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* substituted_t,substituted_ty,substituted_metasenv *) (* ANDREA: spostare tutta questa robaccia da un altra parte *) let cleaned_t = - FreshNamesGenerator.clean_dummy_dependent_types substituted_t in + if clean_dummy_dependent_types then + FreshNamesGenerator.clean_dummy_dependent_types substituted_t + else substituted_t in let cleaned_ty = - FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in + if clean_dummy_dependent_types then + FreshNamesGenerator.clean_dummy_dependent_types substituted_ty + else substituted_ty in let cleaned_metasenv = + if clean_dummy_dependent_types then List.map (function (n,context,ty) -> let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in @@ -1768,6 +1773,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in (n,context',ty') ) substituted_metasenv + else + substituted_metasenv in (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) ;; @@ -1926,7 +1933,12 @@ let typecheck metasenv uri obj ~localization_tbl = List.fold_right (fun (name,b,ty,cl) (metasenv,ugraph,res) -> let ty',_,metasenv,ugraph = - type_of_aux' ~localization_tbl metasenv [] ty ugraph + (* clean_dummy_dependent_types: false to avoid cleaning the names + of the left products, that must be identical to those of the + constructors; however, non-left products should probably be + cleaned *) + type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl + metasenv [] ty ugraph in metasenv,ugraph,(name,b,ty',cl)::res ) tys (metasenv,ugraph,[]) in -- 2.39.2