From 659d8c3d93c3279e08bc0cf56879037e066d9ca8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 May 2008 17:02:26 +0000 Subject: [PATCH] get_check_fix and cofix unified, bug regarding debruijnation of constructors types fixed everywhere. the constructor typs are debruinated wrt some inductive type uri an not wrt their own, thus a wrong context was created. guarded by constructors ported from the old kernel. --- .../components/ng_kernel/nCicEnvironment.ml | 6 +- .../components/ng_kernel/nCicEnvironment.mli | 6 +- .../components/ng_kernel/nCicReduction.ml | 4 +- .../components/ng_kernel/nCicTypeChecker.ml | 111 +++++++++--------- 4 files changed, 59 insertions(+), 68 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 1e2cd913e..5199dc20f 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -64,16 +64,14 @@ let get_checked_indtys = function | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false ;; -let get_checked_fix_or_cofix b = function +let get_checked_fixes_or_cofixes = function | NReference.Ref (_, uri, (NReference.Fix (fixno,_)|NReference.CoFix fixno))-> (match get_checked_obj uri with - | _,height,_,_, NCic.Fixpoint (is_fix,funcs,att) when is_fix = b -> + | _,height,_,_, NCic.Fixpoint (_,funcs,att) -> funcs, att, height | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false) | r -> prerr_endline ("get_checked_(co)fix on " ^ NReference.string_of_reference r); assert false ;; -let get_checked_fixes r = get_checked_fix_or_cofix true r;; -let get_checked_cofixes r = get_checked_fix_or_cofix false r;; let get_indty_leftno = function | NReference.Ref (_, uri, NReference.Ind _) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 07bd1b51c..deb7380f6 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -39,11 +39,7 @@ val get_checked_indtys: NReference.reference -> bool * int * NCic.inductiveType list * NCic.i_attr * int -val get_checked_fixes: - NReference.reference -> - NCic.inductiveFun list * NCic.f_attr * int - -val get_checked_cofixes: +val get_checked_fixes_or_cofixes: NReference.reference -> NCic.inductiveFun list * NCic.f_attr * int diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 118bc6911..46a81d620 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -401,7 +401,7 @@ module Reduction(RS : Strategy) = if delta > height then config else aux (0, [], body, s) | (_, _, NCic.Const (NReference.Ref (_,_,NReference.Fix (fixno,recindex)) as refer),s) as config -> - let fixes,_, height = NCicEnvironment.get_checked_fixes refer in + let fixes,_, height = NCicEnvironment.get_checked_fixes_or_cofixes refer in if delta > height then config else (match try Some (RS.from_stack (List.nth s recindex)) @@ -421,7 +421,7 @@ module Reduction(RS : Strategy) = | (k, e, NCic.Match (_,_,term,pl),s) as config -> let decofix = function | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix c)as refer),s)-> - let cofixes,_,_ = NCicEnvironment.get_checked_cofixes refer in + let cofixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in let _,_,_,_,body = List.nth cofixes c in reduce ~delta:0 ~subst context (0,[],body,s) | config -> config diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 739bfa6f9..ec70116a2 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -196,7 +196,6 @@ let rec instantiate_parameters params c = | t,l -> raise (AssertFailure (lazy "1")) ;; -(* specialized only constructors, arities are left untouched *) let specialize_inductive_type_constrs ~subst context ty_term = match R.whd ~subst context ty_term with | C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref) @@ -204,27 +203,24 @@ let specialize_inductive_type_constrs ~subst context ty_term = let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in let left_args,_ = HExtlib.split_nth leftno args in - let itl = - List.map (fun (rel, name, arity, cl) -> - rel, name, arity, - List.map (fun (rel, name, ty) -> - rel, name, instantiate_parameters left_args ty) - cl) - itl - in - is_ind, leftno, itl, attrs, i + let _,_,_,cl = List.nth itl i in + List.map + (fun (rel,name,ty) -> rel, name, instantiate_parameters left_args ty) cl | _ -> assert false ;; -let fix_lefts_in_constrs ~subst r_uri r_len context ty_term = - assert false; (* BUG, ask enrico *) - let _,_,itl,_,i = specialize_inductive_type_constrs ~subst context ty_term in - let _,_,_,cl = List.nth itl i in - let cl = - List.map (fun (_,id,ty) -> id, debruijn r_uri r_len context ty) cl +let specialize_and_abstract_constrs ~subst r_uri r_len context ty_term = + let cl = specialize_inductive_type_constrs ~subst context ty_term in + let len = List.length context in + let context_dcl = + match E.get_checked_obj r_uri with + | _,_,_,_, NCic.Inductive (_,_,tys,_) -> + context @ List.map (fun (_,name,arity,_) -> name,C.Decl arity) tys + | _ -> assert false in - (* since arities are closed they are not lifted *) - List.map (fun (_,name,arity,_) -> name, C.Decl arity) itl, cl + context_dcl, + List.map (fun (_,id,ty) -> id, debruijn r_uri r_len context ty) cl, + len, len + r_len ;; exception DoesOccur;; @@ -773,7 +769,7 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,recno))) as r)::args) -> if List.exists (fun t -> try aux k t;false with NotGuarded _ -> true) args then - let fl,_,_ = E.get_checked_fixes r in + let fl,_,_ = E.get_checked_fixes_or_cofixes r in let ctx_tys, bos = List.split (List.map (fun (_,name,_,ty,bo) -> (name, C.Decl ty), bo) fl) in @@ -826,10 +822,9 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = if not isinductive then recursor aux k t else let ty = typeof ~subst ~metasenv context term in - let itl_ctx,dcl = fix_lefts_in_constrs ~subst r_uri r_len context ty in + let dc_ctx, dcl, start, stop = + specialize_and_abstract_constrs ~subst r_uri r_len context ty in let args = match t with C.Appl (_::tl) -> tl | _ -> [] in - let dc_ctx = context @ itl_ctx in - let start, stop = List.length context, List.length context + r_len in aux k outtype; List.iter (aux k) args; List.iter2 @@ -849,7 +844,7 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = try aux (context, recfuns, 1) t with NotGuarded s -> raise (TypeCheckerFailure s) -and guarded_by_constructors ~subst ~metasenv context t indURI indlen = +and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn = let rec aux context n nn h te = match R.whd ~subst context te with | C.Rel m when m > n && m <= nn -> h @@ -865,16 +860,17 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen = | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> h && List.for_all (does_not_occur ~subst context n nn) tl | C.Const (Ref.Ref (_,_,Ref.Con _)) -> true - | C.Appl (C.Const (Ref.Ref (_,uri, Ref.Con (i,j)) as ref) :: tl) as t -> + | C.Appl (C.Const (Ref.Ref (_,uri, Ref.Con (_,j)) as ref) :: tl) as t -> let _, paramsno, _, _, _ = E.get_checked_indtys ref in let ty_t = typeof ~subst ~metasenv context t in - let tys, cl = fix_lefts_in_constrs ~subst indURI indlen context ty_t in - let len_ctx = List.length context in - let len_tys = List.length tys in - let context_c = context @ tys in - let _,c = List.nth cl (j-1) in - let rec_params = - recursive_args ~subst ~metasenv context_c len_ctx (len_ctx+len_tys) c in + let dc_ctx, dcl, start, stop = + specialize_and_abstract_constrs ~subst indURI indlen context ty_t in + let _, dc = List.nth dcl (j-1) in +(* + prerr_endline (PP.ppterm ~subst ~metasenv ~context:dc_ctx dc); + prerr_endline (PP.ppcontext ~subst ~metasenv dc_ctx); + *) + let rec_params = recursive_args ~subst ~metasenv dc_ctx start stop dc in let rec analyse_instantiated_type rec_spec args = match rec_spec, args with | h::rec_spec, he::args -> @@ -894,20 +890,21 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen = does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te && List.for_all (aux context n nn h) pl - | C.Const (Ref.Ref (_,_,(Ref.Fix _| Ref.CoFix _)) as ref) - | C.Appl(C.Const (Ref.Ref(_,_,(Ref.Fix _| Ref.CoFix _)) as ref) :: _) as t -> + | C.Const (Ref.Ref (_,u,(Ref.Fix _| Ref.CoFix _)) as ref) + | C.Appl(C.Const (Ref.Ref(_,u,(Ref.Fix _| Ref.CoFix _)) as ref) :: _) as t -> let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in - let fl,_,_ = E.get_checked_fixes ref in + let fl,_,_ = E.get_checked_fixes_or_cofixes ref in + let len = List.length fl in let tys = List.map (fun (_,n,_,ty,_) -> n, C.Decl ty) fl in List.for_all (does_not_occur ~subst context n nn) tl && List.for_all - (fun (_,_,_,ty,bo) -> - aux (context@tys) n nn h (debruijn indURI indlen context bo)) + (fun (_,_,_,_,bo) -> + aux (context@tys) n nn h (debruijn u len context bo)) fl | C.Const _ | C.Appl _ as t -> does_not_occur ~subst context n nn t in - aux context 0 indlen false t + aux context 0 nn false t and recursive_args ~subst ~metasenv context n nn te = match R.whd context te with @@ -938,9 +935,9 @@ and is_really_smaller is_really_smaller r_uri r_len ~subst ~metasenv (shift_k (name,C.Decl s) k) t | C.Appl (he::_) -> is_really_smaller r_uri r_len ~subst ~metasenv k he - | C.Appl _ | C.Rel _ | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false + | C.Appl [] | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false | C.Meta _ -> true | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) -> @@ -952,9 +949,8 @@ and is_really_smaller List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl else let ty = typeof ~subst ~metasenv context term in - let itl_ctx,dcl= fix_lefts_in_constrs ~subst r_uri r_len context ty in - let start, stop = List.length context, List.length context + r_len in - let dc_ctx = context @ itl_ctx in + let dc_ctx, dcl, start, stop = + specialize_and_abstract_constrs ~subst r_uri r_len context ty in List.for_all2 (fun p (_,dc) -> let rl = recursive_args ~subst ~metasenv dc_ctx start stop dc in @@ -968,8 +964,8 @@ and returns_a_coinductive ~subst context ty = match R.whd ~subst context ty with | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)::_) -> - let isinductive, _, _, _, _ = E.get_checked_indtys ref in - if isinductive then None else (Some uri) + let isinductive, _, itl, _, _ = E.get_checked_indtys ref in + if isinductive then None else (Some (uri,List.length itl)) | C.Prod (n,so,de) -> returns_a_coinductive ~subst ((n,C.Decl so)::context) de | _ -> None @@ -1015,13 +1011,14 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = | C.Inductive (is_ind, leftno, tyl, _) -> check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl | C.Fixpoint (inductive,fl,_) -> - let types, kl, len = + let types, kl = List.fold_left - (fun (types,kl,len) (_,name,k,ty,_) -> + (fun (types,kl) (_,name,k,ty,_) -> let _ = typeof ~subst ~metasenv [] ty in - ((name,(C.Decl (S.lift len ty)))::types, k::kl,len+1) - ) ([],[],0) fl + ((name,C.Decl ty)::types, k::kl) + ) ([],[]) fl in + let len = List.length types in let dfl, kl = List.split (List.map2 (fun (_,_,_,_,bo) rno -> @@ -1031,7 +1028,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = in List.iter2 (fun (_,name,x,ty,_) bo -> let ty_bo = typeof ~subst ~metasenv types bo in - if not (R.are_convertible ~subst ~metasenv types ty_bo (S.lift len ty)) + if not (R.are_convertible ~subst ~metasenv types ty_bo ty) then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies"))) else if inductive then begin @@ -1056,15 +1053,15 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = end else match returns_a_coinductive ~subst [] ty with | None -> - raise (TypeCheckerFailure - (lazy "CoFix: does not return a coinductive type")) - | Some uri -> - (* guarded by constructors conditions C{f,M} *) - if not - (guarded_by_constructors ~subst ~metasenv types bo uri len) - then - raise (TypeCheckerFailure - (lazy "CoFix: not guarded by constructors")) + raise (TypeCheckerFailure + (lazy "CoFix: does not return a coinductive type")) + | Some (r_uri, r_len) -> + (* guarded by constructors conditions C{f,M} *) + if not + (guarded_by_constructors ~subst ~metasenv types bo r_uri r_len len) + then + raise (TypeCheckerFailure + (lazy "CoFix: not guarded by constructors")) ) fl dfl let typecheck_obj = check_obj_well_typed;; -- 2.39.2