X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=877c33d23edf73c5c09a5c274afd1cfe60898564;hb=80f3756848ca8b178255f717794c5c2358d5d585;hp=1d34d3835697eb42121b9a449e6b79735e3f2e59;hpb=bace52692eba06fca2cc37857b61dadf5d280ffe;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 1d34d3835..877c33d23 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,26 +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 = - 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;; @@ -734,7 +731,6 @@ and eat_or_subst_lambdas ~subst ~metasenv n te to_be_subst args and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = let recursor f k t = U.fold shift_k k (fun k () -> f k) () t in let rec aux (context, recfuns, x as k) t = - let t = R.whd ~delta:max_int ~subst context t in (* prerr_endline ("GB:\n" ^ PP.ppcontext ~subst ~metasenv context^ @@ -772,7 +768,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 @@ -825,10 +821,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 @@ -848,7 +843,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 @@ -864,16 +859,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 -> @@ -893,20 +889,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 @@ -937,9 +934,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) -> @@ -951,9 +948,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 @@ -967,8 +963,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 @@ -1014,13 +1010,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 -> @@ -1030,7 +1027,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 @@ -1055,15 +1052,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;;