From 9f66cc89caf70d20a0e4c0d55796da6082d60976 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 15 Apr 2008 20:10:44 +0000 Subject: [PATCH] 1. bug fixed: the context must be type-checked before using it in type_of_aux'. Otherwise get_cooked_obj raises Not_found in Deannotate 2. big improvement in guarded_by_destructors: when a fix applied to a safe argument is found in the body of another fix, the body of the inner fix is check adding the recusrive formal parameter as an additional safe argument. --- .../cic_proof_checking/cicTypeChecker.ml | 98 ++++++++++++++----- 1 file changed, 75 insertions(+), 23 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 285536700..ffb53c236 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -347,6 +347,10 @@ and weakly_positive context n nn uri te = | C.Lambda (name,so,ta) -> C.Lambda (name, subst_inductive_type_with_dummy_mutind so, subst_inductive_type_with_dummy_mutind ta) + | C.LetIn (name,so,ty,ta) -> + C.LetIn (name, subst_inductive_type_with_dummy_mutind so, + subst_inductive_type_with_dummy_mutind ty, + subst_inductive_type_with_dummy_mutind ta) | C.Appl tl -> C.Appl (List.map subst_inductive_type_with_dummy_mutind tl) | C.MutCase (uri,i,outtype,term,pl) -> @@ -369,6 +373,13 @@ and weakly_positive context n nn uri te = exp_named_subst in C.Const (uri,exp_named_subst') + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map + (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) + exp_named_subst + in + C.Var (uri,exp_named_subst') | C.MutInd (uri,typeno,exp_named_subst) -> let exp_named_subst' = List.map @@ -460,7 +471,6 @@ and strictly_positive context n nn te = List.fold_right (fun x i -> i && does_not_occur context n nn x) arguments true && - (*CSC: MEGAPATCH3 (sara' quella giusta?)*) List.fold_right (fun x i -> i && @@ -737,6 +747,8 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = (*CSC: cfr guarded_by_destructors *) let module C = Cic in let module U = UriManager in + (*CSC: we could perform beta-iota(-zeta?) immediately, and + delta only on-demand when it fails without *) match CicReduction.whd ~subst context te with C.Rel m when List.mem m safes -> true | C.Rel _ -> false @@ -919,10 +931,10 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = x_plus_len safes' bo ) fl true -and guarded_by_destructors ~subst context n nn kl x safes = +and guarded_by_destructors ~subst context n nn kl x safes t = let module C = Cic in let module U = UriManager in - function + match CicReduction.whd ~subst context t with C.Rel m when m > n && m <= nn -> false | C.Rel m -> (match List.nth context (m-1) with @@ -960,10 +972,6 @@ and guarded_by_destructors ~subst context n nn kl x safes = i && guarded_by_destructors ~subst context n nn kl x safes param ) tl true && check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k) - | C.Appl tl -> - List.fold_right - (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t) - tl true | C.Var (_,exp_named_subst) | C.Const (_,exp_named_subst) | C.MutInd (_,_,exp_named_subst) @@ -1023,11 +1031,11 @@ and guarded_by_destructors ~subst context n nn kl x safes = (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right (fun (p,(_,c,brujinedc)) i -> + i && let rl' = recursive_args lefts_and_tys 0 len brujinedc in let (e,safes',n',nn',x',context') = get_new_safes ~subst context p c rl' safes n nn x in - i && guarded_by_destructors ~subst context' n' nn' kl x' safes' e ) pl_and_cl true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> @@ -1098,24 +1106,45 @@ and guarded_by_destructors ~subst context n nn kl x safes = (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p) pl true ) - | C.Fix (_, fl) -> + | C.Appl (C.Fix (fixno, fl)::_) | C.Fix (fixno,fl) as t-> + let l = match t with C.Appl (_::tl) -> tl | _ -> [] in let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - and x_plus_len = x + len - and tys,_ = + let n_plus_len = n + len in + let nn_plus_len = nn + len in + let x_plus_len = x + len in + let tys,_ = List.fold_left (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl - and safes' = List.map (fun x -> x + len) safes in - List.fold_right - (fun (_,_,ty,bo) i -> - i && guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty && - guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl - x_plus_len safes' bo - ) fl true + ) ([],0) fl in + let safes' = List.map (fun x -> x + len) safes in + List.for_all + (guarded_by_destructors ~subst context n nn kl x safes) l && + snd (List.fold_left + (fun (fixno',i) (_,recno,ty,bo) -> + fixno'+1, + i && + guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty && + if + fixno' = fixno && + List.length l > recno && + (*case where the recursive argument is already really_smaller *) + check_is_really_smaller_arg ~subst context n nn kl x safes + (List.nth l recno) + then + let bo_without_lambdas,_,context = + eat_lambdas ~subst (tys@context) (recno+1) bo + in + (* we assume the formal argument to be safe *) + guarded_by_destructors ~subst context (n_plus_len+recno+1) + (nn_plus_len+recno+1) kl (x_plus_len+recno+1) + (1::List.map (fun x -> x+recno+1) safes') + bo_without_lambdas + else + guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len + kl x_plus_len safes' bo + ) (0,true) fl) | C.CoFix (_, fl) -> let len = List.length fl in let n_plus_len = n + len @@ -1135,6 +1164,10 @@ and guarded_by_destructors ~subst context n nn kl x safes = guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl x_plus_len safes' bo ) fl true + | C.Appl tl -> + List.fold_right + (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t) + tl true (* the boolean h means already protected *) (* args is the list of arguments the type of the constructor that may be *) @@ -1935,7 +1968,7 @@ end; (len + eaten) kl 1 [] m) then raise (TypeCheckerFailure - (lazy ("Fix: not guarded by destructors"))) + (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t))) else ugraph2 end @@ -2301,4 +2334,23 @@ let check_allowed_sort_elimination uri i s1 s2 = CicUniv.empty_ugraph) ;; -Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);; +Deannotate.type_of_aux' := + fun context t -> + (*CSC: we need to type-check the context to avoid Not_found in + get_cooked_obj in CicReduction. However, this implementation may + be very inefficient, since we may type-check the same context + O(n^2) times. On the other hand, type-checking the context in Deannotate + would be a cost to pay not only for Coq objects. *) + ignore ( + List.fold_right + (fun el context -> + (match el with + None -> () + | Some (_,Cic.Decl ty) -> + ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph) + | Some (_,Cic.Def (bo,ty)) -> + ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph); + ignore (type_of_aux' [] context bo CicUniv.oblivion_ugraph)); + el::context + ) context []); + fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);; -- 2.39.2