From 3928102abd95778d390e2790fdb7ac2ae3567813 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 23 Apr 2008 16:41:37 +0000 Subject: [PATCH] ported the instantiate-left-params-to-calculate-rec-args patch from the old to the new kernel, to test the patch properly some steps of substitution inside a possibly blocked fix are performed, this should be in general avoided without good checks (still to understand) --- .../components/ng_kernel/nCicTypeChecker.ml | 230 ++++++++++++------ 1 file changed, 149 insertions(+), 81 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index e96169e3e..6dceca87f 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -26,9 +26,9 @@ let shift_k e (c,rf,x,safes) = e::c,List.map (fun (k,v) -> k+1,v) rf,x+1,List.map ((+)1) safes ;; -(* $Id: cicTypeChecker.ml 8213 2008-03-13 18:48:26Z sacerdot $ *) - - +let shift_k_add_1_safe e (c,rf,x,safes) = + e::c,List.map (fun (k,v) -> k+1,v) rf,x+1,1::List.map ((+)1) safes +;; (* (* the boolean h means already protected *) @@ -294,7 +294,7 @@ let rec split_prods ~subst context n te = | (_, _) -> raise (AssertFailure (lazy "split_prods")) ;; -let debruijn ?(cb=fun _ _ -> ()) uri number_of_types = +let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context = let rec aux k t = let res = match t with @@ -309,7 +309,7 @@ let debruijn ?(cb=fun _ _ -> ()) uri number_of_types = in cb t res; res in - aux 0 + aux (List.length context) ;; let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) = @@ -371,20 +371,44 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty = aux ty_he args_with_ty ;; -let fix_lefts_in_constrs ~subst uri paramsno tyl i = - let len = List.length tyl in - let _,_,arity,cl = List.nth tyl i in - let tys = List.map (fun (_,n,ty,_) -> n,C.Decl ty) tyl in - let cl' = - List.map - (fun (_,id,ty) -> - let debruijnedty = debruijn uri len ty in - id, snd (split_prods ~subst tys paramsno ty), - snd (split_prods ~subst tys paramsno debruijnedty)) - cl +(* instantiate_parameters ps (x1:T1)...(xn:Tn)C *) +(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *) +let rec instantiate_parameters params c = + match c, params with + | c,[] -> c + | C.Prod (_,_,ta), he::tl -> instantiate_parameters tl (S.subst he ta) + | t,l -> raise (AssertFailure (lazy "1")) +;; + +let specialize_inductive_type ~subst context ty_term = + match R.whd ~subst context ty_term with + | C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref) + | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref) :: _ ) as ty -> + 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) -> + let arity = instantiate_parameters left_args arity in + let cl = + List.map (fun (rel, name, ty) -> + rel, name, instantiate_parameters left_args ty) + cl + in + rel, name, arity, cl) + itl + in + is_ind, leftno, itl, attrs, i + | _ -> assert false +;; + +let fix_lefts_in_constrs ~subst r_uri r_len context ty_term = + let _,_,itl,_,i = specialize_inductive_type ~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 in - let lefts = fst (split_prods ~subst [] paramsno arity) in - lefts@tys, len, cl' + List.map (fun (_,name,arity,_) -> name, C.Decl arity) itl, cl ;; exception DoesOccur;; @@ -445,14 +469,6 @@ let rec weakly_positive ~subst context n nn uri te = | _ -> raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) -(* instantiate_parameters ps (x1:T1)...(xn:Tn)C *) -(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *) -and instantiate_parameters params c = - match c, params with - | c,[] -> c - | C.Prod (_,_,ta), he::tl -> instantiate_parameters tl (S.subst he ta) - | t,l -> raise (AssertFailure (lazy "1")) - and strictly_positive ~subst context n nn te = match R.whd context te with | t when does_not_occur ~subst context n nn t -> true @@ -864,7 +880,7 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl = (fun (_,_,_,cl) i -> List.iter (fun (_,name,te) -> - let debruijnedte = debruijn uri len te in + let debruijnedte = debruijn uri len [] te in ignore (typeof ~subst ~metasenv tys debruijnedte); (* let's check also the positivity conditions *) if @@ -888,9 +904,13 @@ and eat_lambdas ~subst ~metasenv context n te = raise (AssertFailure (lazy (Printf.sprintf "9 (%d, %s)" n (NCicPp.ppterm ~subst ~metasenv ~context te)))) -and guarded_by_destructors ~subst ~metasenv context recfuns t = +and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = let recursor f k t = NCicUtils.fold shift_k k (fun k () -> f k) () t in let rec aux (context, recfuns, x, safes as k) t = +(* + prerr_endline ("GB: " ^ NCicPp.ppterm ~metasenv ~subst ~context t + ^ " " ^ String.concat "," (List.map (fun i -> NCicPp.ppterm ~metasenv ~subst ~context (C.Rel i)) safes)); + *) match R.whd ~subst context t with (* TODO: use ~delta:false as mush as poss*) | C.Rel m as t when List.mem_assoc m recfuns -> raise (NotGuarded (lazy @@ -908,31 +928,52 @@ and guarded_by_destructors ~subst ~metasenv context recfuns t = " is a partial application of a fix"))) else let rec_arg = List.nth tl rec_no in - if not (is_really_smaller ~subst ~metasenv k rec_arg) then - raise (NotGuarded (lazy - (NCicPp.ppterm ~context ~subst ~metasenv rec_arg ^ " not smaller"))); + if not (is_really_smaller r_uri r_len ~subst ~metasenv k rec_arg) then + raise (NotGuarded (lazy (Printf.sprintf ("Recursive call %s, %s is not" + ^^ " smaller.\ncontext:\n%s") (NCicPp.ppterm ~context ~subst ~metasenv + t) (NCicPp.ppterm ~context ~subst ~metasenv rec_arg) + (NCicPp.ppcontext ~subst ~metasenv context)))); List.iter (aux k) tl - (* - | C.Appl (C.Const ((Ref.Ref (_,_,Ref.Fix (i,j))) as r)::args) -> - List.iter (aux k) args; - let fixes,_,_ = E.get_checked_fixes r in - let _,_,_,_,bo = List.nth fixes i in - let bo_wout_lam, context = eat_lambdas ~subst ~metasenv context j in - (* debruijna body..... *) assert false -*) + | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,j))) as r)::args) + when List.length args > j + (* TODO: extra check really usueful?? *) + && List.exists (fun (k,_) -> List.exists (fun t -> not (does_not_occur ~subst context k (k+1) t)) args) recfuns + && is_really_smaller r_uri r_len ~subst ~metasenv k (List.nth args j) -> + let fl,_,_ = E.get_checked_fixes r in + let ctx_tys, bos = + List.split (List.map (fun (_,name,_,ty,bo) -> (name, C.Decl ty), bo) fl) + in + let bo = List.nth bos i in + let bo = debruijn uri (List.length fl) context bo in + let args, rest = HExtlib.split_nth j args in + let bo = + (* TODO: here we should check which args are passed around ... *) + if j > 0 then R.head_beta_reduce ~upto:j (C.Appl (bo::args)) else bo + in + let bo, context_rec = eat_lambdas ~subst ~metasenv context 1 bo in + let bo = + if rest = [] then bo else + let rest = List.tl rest in if rest <> [] then C.Appl (bo::rest) else bo + in + let k = context@ctx_tys, recfuns, x, safes in + aux (shift_k_add_1_safe (List.hd context_rec) k) bo | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t -> (match R.whd ~subst context term with | C.Rel m | C.Appl (C.Rel m :: _ ) as t when List.mem m safes || m = x -> - let isinductive, paramsno, tl, _, i = E.get_checked_indtys ref in + (* TODO: add CoInd to references so that this call is useless *) + let isinductive, _, _, _, _ = E.get_checked_indtys ref in if not isinductive then recursor aux k t else - let c_ctx,len,cl = fix_lefts_in_constrs ~subst uri paramsno tl i in + let ty = typeof ~subst ~metasenv context term in + let itl_ctx,cl = fix_lefts_in_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 - (fun p (_,_,bruijnedc) -> - let rl = recursive_args ~subst ~metasenv c_ctx 0 len bruijnedc in + (fun p (_,dc) -> + let rl = recursive_args ~subst ~metasenv dc_ctx start stop dc in let p, k = get_new_safes ~subst k p rl in aux k p) pl cl @@ -988,6 +1029,10 @@ and recursive_args ~subst ~metasenv context n nn te = match R.whd context te with | C.Rel _ | C.Appl _ -> [] | C.Prod (name,so,de) -> +(* + prerr_endline ("RA: " ^ NCicPp.ppterm ~subst ~metasenv ~context so + ^ " == " ^ string_of_bool (not (does_not_occur ~subst context n nn so))); + *) (not (does_not_occur ~subst context n nn so)) :: (recursive_args ~subst ~metasenv ((name,(C.Decl so))::context) (n+1) (nn + 1) de) @@ -1001,7 +1046,13 @@ and get_new_safes ~subst (context, recfuns, x, safes as k) p rl = let safes = (if b then [0] else []) @ safes in get_new_safes ~subst (shift_k (name,(C.Decl so)) (context, recfuns, x, safes)) ta tl - | C.Meta _ as e, _ | e, [] -> e, k + | C.Meta _ as e, _ | e, [] -> +(* + prerr_endline ("GNS: " ^ String.concat "," + (List.map (fun i -> + NCicPp.ppterm ~subst ~metasenv:[] ~context (C.Rel i)) safes)); + *) + e, k | _ -> raise (AssertFailure (lazy "Ill formed pattern")) and split_prods ~subst context n te = @@ -1011,13 +1062,15 @@ and split_prods ~subst context n te = split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta | _ -> raise (AssertFailure (lazy "split_prods")) -and is_really_smaller ~subst ~metasenv (context, recfuns, x, safes as k) te = +and is_really_smaller + r_uri r_len ~subst ~metasenv (context, recfuns, x, safes as k) te += match R.whd ~subst context te with | C.Rel m when List.mem m safes -> true | C.Lambda (name, s, t) -> - is_really_smaller ~subst ~metasenv (shift_k (name, C.Decl s) k) t + is_really_smaller r_uri r_len ~subst ~metasenv (shift_k (name,C.Decl s) k) t | C.Appl (he::_) -> - is_really_smaller ~subst ~metasenv k he + is_really_smaller r_uri r_len ~subst ~metasenv k he | C.Appl _ | C.Rel _ | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false @@ -1044,18 +1097,22 @@ and is_really_smaller ~subst ~metasenv (context, recfuns, x, safes as k) te = | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) -> (match term with | C.Rel m | C.Appl (C.Rel m :: _ ) when List.mem m safes || m = x -> - let isinductive, paramsno, tl, _, i = E.get_checked_indtys ref in + (* TODO: add CoInd to references so that this call is useless *) + let isinductive, _, _, _, _ = E.get_checked_indtys ref in if not isinductive then - List.for_all (is_really_smaller ~subst ~metasenv k) pl + List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl else - let c_ctx,len,cl = fix_lefts_in_constrs ~subst uri paramsno tl i in + 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 List.for_all2 - (fun p (_,_,debruijnedte) -> - let rl'=recursive_args ~subst ~metasenv c_ctx 0 len debruijnedte in - let e, k = get_new_safes ~subst k p rl' in - is_really_smaller ~subst ~metasenv k e) - pl cl - | _ -> List.for_all (is_really_smaller ~subst ~metasenv k) pl) + (fun p (_,dc) -> + let rl = recursive_args ~subst ~metasenv dc_ctx start stop dc in + let e, k = get_new_safes ~subst k p rl in + is_really_smaller r_uri r_len ~subst ~metasenv k e) + pl dcl + | _ -> List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl) | _ -> assert false and returns_a_coinductive ~subst context ty = @@ -1116,33 +1173,44 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = ((name,(C.Decl (S.lift len ty)))::types, k::kl,len+1) ) ([],[],0) fl in - List.iter (fun (_,name,x,ty,bo) -> - let bo = debruijn uri len bo in - let ty_bo = typeof ~subst ~metasenv types bo in - if not (R.are_convertible ~subst ~metasenv types ty_bo (S.lift len ty)) - then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies"))) - else - if inductive then begin - let m, context = eat_lambdas ~subst ~metasenv types (x + 1) bo in - (* guarded by destructors conditions D{f,k,x,M} *) - let rec enum_from k = - function [] -> [] | v::tl -> (k,v)::enum_from (k+1) tl + List.iter (fun (_,name,x,ty,bo) -> + let bo = debruijn uri len [] bo in + let ty_bo = typeof ~subst ~metasenv types bo in + if not (R.are_convertible ~subst ~metasenv types ty_bo (S.lift len ty)) + then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies"))) + else + if inductive then begin + let m, context = eat_lambdas ~subst ~metasenv types (x + 1) bo in + let r_uri, r_len = + let he = + match List.hd context with _,C.Decl t -> t | _ -> assert false in - guarded_by_destructors - ~subst ~metasenv context (enum_from (x+2) kl) m - end else - match returns_a_coinductive ~subst [] ty with - | None -> + match R.whd ~subst (List.tl context) he with + | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) + | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) :: _) -> + let _,_,itl,_,_ = E.get_checked_indtys ref in + uri, List.length itl + | _ -> assert false + in + (* guarded by destructors conditions D{f,k,x,M} *) + let rec enum_from k = + function [] -> [] | v::tl -> (k,v)::enum_from (k+1) tl + in + guarded_by_destructors r_uri r_len + ~subst ~metasenv context (enum_from (x+2) kl) m + 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 0 len false bo [] uri) + then 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 0 len false bo [] uri) - then - raise (TypeCheckerFailure - (lazy "CoFix: not guarded by constructors")) - ) fl + (lazy "CoFix: not guarded by constructors")) + ) fl let typecheck_obj = check_obj_well_typed;; -- 2.39.2