From 422943b59c046b00e4726c18163eeec62f4a82fb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 10 Feb 2004 12:07:08 +0000 Subject: [PATCH] Bug fixed: checking inductive type declarations with left parameters (e.g. le) lead to mistakes due to debrujin/undebrujin: terms to be debrujined must be closed and then left parameters can not be removed _before_ calling debrujin_constructor. --- .../cic_proof_checking/cicTypeChecker.ml | 41 ++++++++++--------- 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 9c9c0e58c..3f504ab79 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -604,13 +604,16 @@ and get_new_safes context p c rl safes n nn x = | (C.Prod _, (C.Rel _ as e), _) | (C.MutInd _, e, []) | (C.Appl _, e, []) -> (e,safes,n,nn,x,context) - | (_,_,_) -> + | (c,p,l) -> (* CSC: If the next exception is raised, it just means that *) (* CSC: the proof-assistant allows to use very strange things *) (* CSC: as a branch of a case whose type is a Prod. In *) (* CSC: particular, this means that a new (C.Prod, x,_) case *) (* CSC: must be considered in this match. (e.g. x = MutCase) *) - raise (AssertFailure "7") + raise + (AssertFailure + (Printf.sprintf "Get New Safes: c=%s ; p=%s" + (CicPp.ppterm c) (CicPp.ppterm p))) and split_prods context n te = let module C = Cic in @@ -841,17 +844,21 @@ and guarded_by_destructors context n nn kl x safes = let (tys,len,isinductive,paramsno,cl) = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> - let (_,isinductive,_,cl) = List.nth tl i in - let tys = - List.map (fun (n,_,ty,_) -> - Some(Cic.Name n,(Cic.Decl ty))) tl - in - let cl' = - List.map - (fun (id,ty) -> - (id, snd (split_prods tys paramsno ty))) cl + let len = List.length tl in + let (_,isinductive,_,cl) = List.nth tl i in + let tys = + List.map (fun (n,_,ty,_) -> + Some(Cic.Name n,(Cic.Decl ty))) tl in - (tys,List.length tl,isinductive,paramsno,cl') + let cl' = + List.map + (fun (id,ty) -> + let debrujinedty = debrujin_constructor uri len ty in + (id, snd (split_prods tys paramsno ty), + snd (split_prods tys paramsno debrujinedty) + )) cl + in + (tys,len,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ @@ -869,11 +876,8 @@ and guarded_by_destructors context n nn kl x safes = guarded_by_destructors context n nn kl x safes outtype && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right - (fun (p,(_,c)) i -> - let rl' = - let debrujinedte = debrujin_constructor uri len c in - recursive_args tys 0 len debrujinedte - in + (fun (p,(_,c,brujinedc)) i -> + let rl' = recursive_args tys 0 len brujinedc in let (e,safes',n',nn',x',context') = get_new_safes context p c rl' safes n nn x in @@ -1338,8 +1342,7 @@ and type_of_aux' metasenv context t = | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis") with _ -> - raise (TypeCheckerFailure - "unbound variable found in constructor type") + raise (TypeCheckerFailure "unbound variable") ) | C.Var (uri,exp_named_subst) -> incr fdebug ; -- 2.39.2