From bace52692eba06fca2cc37857b61dadf5d280ffe Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 May 2008 13:34:10 +0000 Subject: [PATCH] guarded_by_constructors implemented, some cleanup here and there. fix_lefts_in_constr fixed: the inductive type list was returned with constructors instantiated and debruijned, but with types whose arity was instantiated with lefts too. This is wrong since we want to use these types to build a context, that is closed, and will be put at the end of the actual context since debruijn will make uris point to those terms --- .../components/ng_kernel/nCicTypeChecker.ml | 557 +++++------------- 1 file changed, 150 insertions(+), 407 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index e05f145d3..1d34d3835 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -11,6 +11,14 @@ (* $Id: nCicReduction.ml 8250 2008-03-25 17:56:20Z tassi $ *) +module C = NCic +module R = NCicReduction +module Ref = NReference +module S = NCicSubstitution +module U = NCicUtils +module E = NCicEnvironment +module PP = NCicPp + (* web interface stuff *) let logger = @@ -53,35 +61,35 @@ let get_fixed_args i l = let shift_k e (c,rf,x) = e::c,List.map (fun (k,v) -> k+1,v) rf,x+1;; let string_of_recfuns ~subst ~metasenv ~context l = - let pp = NCicPp.ppterm ~subst ~metasenv ~context in + let pp = PP.ppterm ~subst ~metasenv ~context in let safe, rest = List.partition (function (_,Safe) -> true | _ -> false) l in - let dang, unf = List.partition (function (_,UnfFix _) -> false | _->true)rest in - "\n\tsafes: "^String.concat "," (List.map (fun (i,_)->pp (NCic.Rel i)) safe) ^ + let dang,unf = List.partition (function (_,UnfFix _)-> false | _->true)rest in + "\n\tsafes: "^String.concat "," (List.map (fun (i,_)->pp (C.Rel i)) safe) ^ "\n\tfix : "^String.concat "," (List.map - (function (i,UnfFix l)-> pp(NCic.Rel i)^"/"^String.concat "," (List.map + (function (i,UnfFix l)-> pp(C.Rel i)^"/"^String.concat "," (List.map string_of_bool l) | _ ->assert false) unf) ^ "\n\trec : "^String.concat "," (List.map - (function (i,Evil rno)->pp(NCic.Rel i)^"/"^string_of_int rno + (function (i,Evil rno)->pp(C.Rel i)^"/"^string_of_int rno | _ -> assert false) dang) ;; let fixed_args bos j n nn = let rec aux k acc = function - | NCic.Appl (NCic.Rel i::args) when i-k > n && i-k <= nn -> + | C.Appl (C.Rel i::args) when i-k > n && i-k <= nn -> let rec combine l1 l2 = match l1,l2 with [],[] -> [] | he1::tl1, he2::tl2 -> (he1,he2)::combine tl1 tl2 - | he::tl, [] -> (false,NCic.Rel ~-1)::combine tl [] (* dummy term *) + | he::tl, [] -> (false,C.Rel ~-1)::combine tl [] (* dummy term *) | [],_::_ -> assert false in let lefts, _ = HExtlib.split_nth (min j (List.length args)) args in - List.map (fun ((b,x),i) -> b && x = NCic.Rel (k-i)) + List.map (fun ((b,x),i) -> b && x = C.Rel (k-i)) (HExtlib.list_mapi (fun x i -> x,i) (combine acc lefts)) - | t -> NCicUtils.fold (fun _ k -> k+1) k aux acc t + | t -> U.fold (fun _ k -> k+1) k aux acc t in List.fold_left (aux 0) (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bos @@ -94,263 +102,6 @@ let rec list_iter_default2 f l1 def l2 = | a::ta, [] -> f a def; list_iter_default2 f ta def [] ;; - -(* -(* the boolean h means already protected *) -(* args is the list of arguments the type of the constructor that may be *) -(* found in head position must be applied to. *) -and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = - let module C = Cic in - (*CSC: There is a lot of code replication between the cases X and *) - (*CSC: (C.Appl X tl). Maybe it will be better to define a function *) - (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *) - match CicReduction.whd ~subst context te with - C.Rel m when m > n && m <= nn -> h - | C.Rel _ -> true - | C.Meta _ - | C.Sort _ - | C.Implicit _ - | C.Cast _ - | C.Prod _ - | C.LetIn _ -> - (* the term has just been type-checked *) - raise (AssertFailure (lazy "17")) - | C.Lambda (name,so,de) -> - does_not_occur ~subst context n nn so && - guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context) - (n + 1) (nn + 1) h de args coInductiveTypeURI - | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> - h && - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true - | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) -> - let consty = - let obj,_ = - try - CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri - with Not_found -> assert false - in - match obj with - C.InductiveDefinition (itl,_,_,_) -> - let (_,_,_,cl) = List.nth itl i in - let (_,cons) = List.nth cl (j - 1) in - CicSubstitution.subst_vars exp_named_subst cons - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) - in - let rec analyse_branch context ty te = - match CicReduction.whd ~subst context ty with - C.Meta _ -> raise (AssertFailure (lazy "34")) - | C.Rel _ - | C.Var _ - | C.Sort _ -> - does_not_occur ~subst context n nn te - | C.Implicit _ - | C.Cast _ -> - raise (AssertFailure (lazy "24"))(* due to type-checking *) - | C.Prod (name,so,de) -> - analyse_branch ((Some (name,(C.Decl so)))::context) de te - | C.Lambda _ - | C.LetIn _ -> - raise (AssertFailure (lazy "25"))(* due to type-checking *) - | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI -> - guarded_by_constructors ~subst context n nn true te [] - coInductiveTypeURI - | C.Appl ((C.MutInd (uri,_,_))::_) -> - guarded_by_constructors ~subst context n nn true te tl - coInductiveTypeURI - | C.Appl _ -> - does_not_occur ~subst context n nn te - | C.Const _ -> raise (AssertFailure (lazy "26")) - | C.MutInd (uri,_,_) when uri == coInductiveTypeURI -> - guarded_by_constructors ~subst context n nn true te [] - coInductiveTypeURI - | C.MutInd _ -> - does_not_occur ~subst context n nn te - | C.MutConstruct _ -> raise (AssertFailure (lazy "27")) - (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) - (*CSC: in head position. *) - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> - raise (AssertFailure (lazy "28"))(* due to type-checking *) - in - let rec analyse_instantiated_type context ty l = - match CicReduction.whd ~subst context ty with - C.Rel _ - | C.Var _ - | C.Meta _ - | C.Sort _ - | C.Implicit _ - | C.Cast _ -> raise (AssertFailure (lazy "29"))(* due to type-checking *) - | C.Prod (name,so,de) -> - begin - match l with - [] -> true - | he::tl -> - analyse_branch context so he && - analyse_instantiated_type - ((Some (name,(C.Decl so)))::context) de tl - end - | C.Lambda _ - | C.LetIn _ -> - raise (AssertFailure (lazy "30"))(* due to type-checking *) - | C.Appl _ -> - List.fold_left - (fun i x -> i && does_not_occur ~subst context n nn x) true l - | C.Const _ -> raise (AssertFailure (lazy "31")) - | C.MutInd _ -> - List.fold_left - (fun i x -> i && does_not_occur ~subst context n nn x) true l - | C.MutConstruct _ -> raise (AssertFailure (lazy "32")) - (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) - (*CSC: in head position. *) - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> - raise (AssertFailure (lazy "33"))(* due to type-checking *) - in - let rec instantiate_type args consty = - function - [] -> true - | tlhe::tltl as l -> - let consty' = CicReduction.whd ~subst context consty in - match args with - he::tl -> - begin - match consty' with - C.Prod (_,_,de) -> - let instantiated_de = CicSubstitution.subst he de in - (*CSC: siamo sicuri che non sia troppo forte? *) - does_not_occur ~subst context n nn tlhe & - instantiate_type tl instantiated_de tltl - | _ -> - (*CSC:We do not consider backbones with a MutCase, a *) - (*CSC:FixPoint, a CoFixPoint and so on in head position.*) - raise (AssertFailure (lazy "23")) - end - | [] -> analyse_instantiated_type context consty' l - (* These are all the other cases *) - in - instantiate_type args consty tl - | C.Appl ((C.CoFix (_,fl))::tl) -> - List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl && - let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys,_ = - List.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - in - List.fold_right - (fun (_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len - h bo args coInductiveTypeURI - ) fl true - | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) -> - List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl && - does_not_occur ~subst context n nn out && - does_not_occur ~subst context n nn te && - List.fold_right - (fun x i -> - i && - guarded_by_constructors ~subst context n nn h x args - coInductiveTypeURI - ) pl true - | C.Appl l -> - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true - | C.Var (_,exp_named_subst) - | C.Const (_,exp_named_subst) -> - List.fold_right - (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true - | C.MutInd _ -> assert false - | C.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right - (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true - | C.MutCase (_,_,out,te,pl) -> - does_not_occur ~subst context n nn out && - does_not_occur ~subst context n nn te && - List.fold_right - (fun x i -> - i && - guarded_by_constructors ~subst context n nn h x args - coInductiveTypeURI - ) pl true - | C.Fix (_,fl) -> - let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys,_ = - List.fold_left - (fun (types,len) (n,_,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - in - List.fold_right - (fun (_,_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - does_not_occur ~subst (tys@context) n_plus_len nn_plus_len bo - ) fl true - | C.CoFix (_,fl) -> - let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys,_ = - List.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - in - List.fold_right - (fun (_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len - h bo - args coInductiveTypeURI - ) fl true - - in - type_of_aux ~logger context t ugraph - -;; - -(** wrappers which instantiate fresh loggers *) - -(* check_allowed_sort_elimination uri i s1 s2 - This function is used outside the kernel to determine in advance whether - a MutCase will be allowed or not. - [uri,i] is the type of the term to match - [s1] is the sort of the term to eliminate (i.e. the head of the arity - of the inductive type [uri,i]) - [s2] is the sort of the goal (i.e. the head of the type of the outtype - of the MutCase) *) -let check_allowed_sort_elimination uri i s1 s2 = - fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[] - ~logger:(new CicLogger.logger) [] uri i true - (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2) - CicUniv.empty_ugraph) -;; - -Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);; - -*) - -module C = NCic -module R = NCicReduction -module Ref = NReference -module S = NCicSubstitution -module U = NCicUtils -module E = NCicEnvironment - let rec split_prods ~subst context n te = match (n, R.whd ~subst context te) with | (0, _) -> context,te @@ -364,13 +115,13 @@ let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context = let res = match t with | C.Meta (i,(s,C.Ctx l)) -> - let l1 = NCicUtils.sharing_map (aux (k-s)) l in + let l1 = U.sharing_map (aux (k-s)) l in if l1 == l then t else C.Meta (i,(s,C.Ctx l1)) | C.Meta _ -> t | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no))) | C.Const (Ref.Ref (_,uri1,Ref.Ind no)) when NUri.eq uri uri1 -> C.Rel (k + number_of_types - no) - | t -> NCicUtils.map (fun _ k -> k+1) k aux t + | t -> U.map (fun _ k -> k+1) k aux t in cb t res; res in @@ -392,8 +143,8 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) = | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf "Prod: expected two sorts, found = %s, %s" - (NCicPp.ppterm ~subst ~metasenv ~context t1) - (NCicPp.ppterm ~subst ~metasenv ~context t2)))) + (PP.ppterm ~subst ~metasenv ~context t1) + (PP.ppterm ~subst ~metasenv ~context t2)))) ;; let eat_prods ~subst ~metasenv context he ty_he args_with_ty = @@ -403,10 +154,10 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty = match R.whd ~subst context ty_he with | C.Prod (n,s,t) -> (* - prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context s ^ " - Vs - " - ^ NCicPp.ppterm ~subst ~metasenv - ~context ty_arg); - prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context (S.subst ~avoid_beta_redexes:true arg t)); + prerr_endline (PP.ppterm ~subst ~metasenv ~context s ^ " - Vs - " + ^ PP.ppterm ~subst ~metasenv ~context ty_arg); + prerr_endline (PP.ppterm ~subst ~metasenv ~context + (S.subst ~avoid_beta_redexes:true arg t)); *) if R.are_convertible ~subst ~metasenv context ty_arg s then aux (S.subst ~avoid_beta_redexes:true arg t) tl @@ -416,20 +167,20 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty = (lazy (Printf.sprintf ("Appl: wrong application of %s: the parameter %s has type"^^ "\n%s\nbut it should have type \n%s\nContext:\n%s\n") - (NCicPp.ppterm ~subst ~metasenv ~context he) - (NCicPp.ppterm ~subst ~metasenv ~context arg) - (NCicPp.ppterm ~subst ~metasenv ~context ty_arg) - (NCicPp.ppterm ~subst ~metasenv ~context s) - (NCicPp.ppcontext ~subst ~metasenv context)))) + (PP.ppterm ~subst ~metasenv ~context he) + (PP.ppterm ~subst ~metasenv ~context arg) + (PP.ppterm ~subst ~metasenv ~context ty_arg) + (PP.ppterm ~subst ~metasenv ~context s) + (PP.ppcontext ~subst ~metasenv context)))) | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf "Appl: %s is not a function, it cannot be applied" - (NCicPp.ppterm ~subst ~metasenv ~context + (PP.ppterm ~subst ~metasenv ~context (let res = List.length tl in let eaten = List.length args_with_ty - res in - (NCic.Appl + (C.Appl (he::List.map fst (fst (HExtlib.split_nth eaten args_with_ty))))))))) in @@ -445,7 +196,8 @@ let rec instantiate_parameters params c = | t,l -> raise (AssertFailure (lazy "1")) ;; -let specialize_inductive_type ~subst context ty_term = +(* 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) | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref) :: _ ) as ty -> @@ -454,13 +206,10 @@ let specialize_inductive_type ~subst context ty_term = 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 = + rel, name, arity, List.map (fun (rel, name, ty) -> rel, name, instantiate_parameters left_args ty) - cl - in - rel, name, arity, cl) + cl) itl in is_ind, leftno, itl, attrs, i @@ -468,11 +217,12 @@ let specialize_inductive_type ~subst context ty_term = ;; 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 _,_,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 in + (* since arities are closed they are not lifted *) List.map (fun (_,name,arity,_) -> name, C.Decl arity) itl, cl ;; @@ -555,7 +305,7 @@ and strictly_positive ~subst context n nn te = ok && List.for_all (does_not_occur ~subst context n nn) arguments && List.for_all - (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1) uri) cl + (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1) uri) cl | _ -> false (* the inductive type indexes are s.t. n < x <= nn *) @@ -572,7 +322,7 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te = | y -> raise (TypeCheckerFailure (lazy ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^ string_of_int indparamsno ^ " fixed) is not homogeneous in "^ - "appl:\n"^ NCicPp.ppterm ~context ~subst ~metasenv:[] reduct)))) + "appl:\n"^ PP.ppterm ~context ~subst ~metasenv:[] reduct)))) indparamsno tl in if last = 0 then @@ -597,7 +347,7 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te = | C.Prod (name,source,dest) -> if not (does_not_occur ~subst context n nn source) then raise (TypeCheckerFailure (lazy ("Non-positive occurrence in "^ - NCicPp.ppterm ~context ~metasenv:[] ~subst te))); + PP.ppterm ~context ~metasenv:[] ~subst te))); are_all_occurrences_positive ~subst ((name,C.Decl source)::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest | _ -> @@ -610,7 +360,7 @@ exception NotGuarded of string Lazy.t;; let rec typeof ~subst ~metasenv context term = let rec typeof_aux context = - fun t -> (*prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);*) + fun t -> (*prerr_endline (PP.ppterm ~metasenv ~subst ~context t);*) match t with | C.Rel n -> (try @@ -629,7 +379,7 @@ let rec typeof ~subst ~metasenv context term = let _,_,c,ty = U.lookup_meta n metasenv in c,ty with U.Meta_not_found _ -> raise (AssertFailure (lazy (Printf.sprintf - "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t)))) + "%s not found" (PP.ppterm ~subst ~metasenv ~context t)))) in check_metasenv_consistency t ~subst ~metasenv context canonical_ctx l; S.subst_meta l ty @@ -647,8 +397,8 @@ let rec typeof ~subst ~metasenv context term = (TypeCheckerFailure (lazy (Printf.sprintf ("Not well-typed lambda-abstraction: " ^^ "the source %s should be a type; instead it is a term " ^^ - "of type %s") (NCicPp.ppterm ~subst ~metasenv ~context s) - (NCicPp.ppterm ~subst ~metasenv ~context sort))))); + "of type %s") (PP.ppterm ~subst ~metasenv ~context s) + (PP.ppterm ~subst ~metasenv ~context sort))))); let ty = typeof_aux ((n,(C.Decl s))::context) t in C.Prod (n,s,ty) | C.LetIn (n,ty,t,bo) -> @@ -659,9 +409,9 @@ let rec typeof ~subst ~metasenv context term = (TypeCheckerFailure (lazy (Printf.sprintf "The type of %s is %s but it is expected to be %s" - (NCicPp.ppterm ~subst ~metasenv ~context t) - (NCicPp.ppterm ~subst ~metasenv ~context ty_t) - (NCicPp.ppterm ~subst ~metasenv ~context ty)))) + (PP.ppterm ~subst ~metasenv ~context t) + (PP.ppterm ~subst ~metasenv ~context ty_t) + (PP.ppterm ~subst ~metasenv ~context ty)))) else let ty_bo = typeof_aux ((n,C.Def (t,ty))::context) bo in S.subst ~avoid_beta_redexes:true t ty_bo @@ -669,10 +419,10 @@ let rec typeof ~subst ~metasenv context term = let ty_he = typeof_aux context he in let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in (* - prerr_endline ("HEAD: " ^ NCicPp.ppterm ~subst ~metasenv ~context ty_he); - prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm + prerr_endline ("HEAD: " ^ PP.ppterm ~subst ~metasenv ~context ty_he); + prerr_endline ("TARGS: " ^ String.concat " | " (List.map (PP.ppterm ~subst ~metasenv ~context) (List.map snd args_with_ty))); - prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm + prerr_endline ("ARGS: " ^ String.concat " | " (List.map (PP.ppterm ~subst ~metasenv ~context) (List.map fst args_with_ty))); *) eat_prods ~subst ~metasenv context he ty_he args_with_ty @@ -693,21 +443,21 @@ let rec typeof ~subst ~metasenv context term = raise (TypeCheckerFailure (lazy (Printf.sprintf "Case analysis: analysed term %s is not an inductive one" - (NCicPp.ppterm ~subst ~metasenv ~context term)))) in + (PP.ppterm ~subst ~metasenv ~context term)))) in if not (Ref.eq r r') then raise (TypeCheckerFailure (lazy (Printf.sprintf ("Case analysys: analysed term type is %s, but is expected " ^^ "to be (an application of) %s") - (NCicPp.ppterm ~subst ~metasenv ~context ty) - (NCicPp.ppterm ~subst ~metasenv ~context (C.Const r'))))) + (PP.ppterm ~subst ~metasenv ~context ty) + (PP.ppterm ~subst ~metasenv ~context (C.Const r'))))) else try HExtlib.split_nth leftno tl with Failure _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf "%s is partially applied" - (NCicPp.ppterm ~subst ~metasenv ~context ty)))) in + (PP.ppterm ~subst ~metasenv ~context ty)))) in (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *) let sort_of_ind_type = if parameters = [] then C.Const r @@ -743,11 +493,11 @@ let rec typeof ~subst ~metasenv context term = (TypeCheckerFailure (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^ "has type %s\nnot convertible with %s") - (NCicPp.ppterm ~subst ~metasenv ~context + (PP.ppterm ~subst ~metasenv ~context (C.Const (Ref.mk_constructor (j-1) r))) - (NCicPp.ppterm ~metasenv ~subst ~context (List.nth pl (j-2))) - (NCicPp.ppterm ~metasenv ~subst ~context p_ty) - (NCicPp.ppterm ~metasenv ~subst ~context exp_p_ty)))); + (PP.ppterm ~metasenv ~subst ~context (List.nth pl (j-2))) + (PP.ppterm ~metasenv ~subst ~context p_ty) + (PP.ppterm ~metasenv ~subst ~context exp_p_ty)))); let res = outtype::arguments@[term] in R.head_beta_reduce (C.Appl res) | C.Match _ -> assert false @@ -776,7 +526,7 @@ let rec typeof ~subst ~metasenv context term = ~subst ~metasenv term context canonical_context l = match l with - | shift, NCic.Irl n -> + | shift, C.Irl n -> let context = snd (HExtlib.split_nth shift context) in let rec compare = function | 0,_,[] -> () @@ -784,11 +534,11 @@ let rec typeof ~subst ~metasenv context term = | _,_,[] -> raise (AssertFailure (lazy (Printf.sprintf "Local and canonical context %s have different lengths" - (NCicPp.ppterm ~subst ~context ~metasenv term)))) + (PP.ppterm ~subst ~context ~metasenv term)))) | m,[],_::_ -> raise (TypeCheckerFailure (lazy (Printf.sprintf "Unbound variable -%d in %s" m - (NCicPp.ppterm ~subst ~metasenv ~context term)))) + (PP.ppterm ~subst ~metasenv ~context term)))) | m,t::tl,ct::ctl -> (match t,ct with (_,C.Decl t1), (_,C.Decl t2) @@ -800,15 +550,15 @@ let rec typeof ~subst ~metasenv context term = (lazy (Printf.sprintf ("Not well typed metavariable local context for %s: " ^^ "%s expected, which is not convertible with %s") - (NCicPp.ppterm ~subst ~metasenv ~context term) - (NCicPp.ppterm ~subst ~metasenv ~context t2) - (NCicPp.ppterm ~subst ~metasenv ~context t1)))) + (PP.ppterm ~subst ~metasenv ~context term) + (PP.ppterm ~subst ~metasenv ~context t2) + (PP.ppterm ~subst ~metasenv ~context t1)))) | _,_ -> raise (TypeCheckerFailure (lazy (Printf.sprintf ("Not well typed metavariable local context for %s: " ^^ "a definition expected, but a declaration found") - (NCicPp.ppterm ~subst ~metasenv ~context term))))); + (PP.ppterm ~subst ~metasenv ~context term))))); compare (m - 1,tl,ctl) in compare (n,context,canonical_context) @@ -852,8 +602,8 @@ let rec typeof ~subst ~metasenv context term = (lazy (Printf.sprintf ("Not well typed metavariable local context: " ^^ "expected a term convertible with %s, found %s") - (NCicPp.ppterm ~subst ~metasenv ~context ct) - (NCicPp.ppterm ~subst ~metasenv ~context t)))) + (PP.ppterm ~subst ~metasenv ~context ct) + (PP.ppterm ~subst ~metasenv ~context t)))) | t, (_,C.Decl ct) -> let type_t = typeof_aux context t in if not (R.are_convertible ~subst ~metasenv context type_t ct) then @@ -861,15 +611,15 @@ let rec typeof ~subst ~metasenv context term = (lazy (Printf.sprintf ("Not well typed metavariable local context: "^^ "expected a term of type %s, found %s of type %s") - (NCicPp.ppterm ~subst ~metasenv ~context ct) - (NCicPp.ppterm ~subst ~metasenv ~context t) - (NCicPp.ppterm ~subst ~metasenv ~context type_t)))) + (PP.ppterm ~subst ~metasenv ~context ct) + (PP.ppterm ~subst ~metasenv ~context t) + (PP.ppterm ~subst ~metasenv ~context type_t)))) ) l lifted_canonical_context with Invalid_argument _ -> raise (AssertFailure (lazy (Printf.sprintf "Local and canonical context %s have different lengths" - (NCicPp.ppterm ~subst ~metasenv ~context term)))) + (PP.ppterm ~subst ~metasenv ~context term)))) and is_non_informative context paramsno c = let rec aux context c = @@ -894,8 +644,8 @@ let rec typeof ~subst ~metasenv context term = if not (R.are_convertible ~subst ~metasenv context so1 so2) then raise (TypeCheckerFailure (lazy (Printf.sprintf "In outtype: expected %s, found %s" - (NCicPp.ppterm ~subst ~metasenv ~context so1) - (NCicPp.ppterm ~subst ~metasenv ~context so2) + (PP.ppterm ~subst ~metasenv ~context so1) + (PP.ppterm ~subst ~metasenv ~context so2) ))); aux ((name, C.Decl so1)::context) (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2 @@ -903,8 +653,8 @@ let rec typeof ~subst ~metasenv context term = if not (R.are_convertible ~subst ~metasenv context so ind) then raise (TypeCheckerFailure (lazy (Printf.sprintf "In outtype: expected %s, found %s" - (NCicPp.ppterm ~subst ~metasenv ~context ind) - (NCicPp.ppterm ~subst ~metasenv ~context so) + (PP.ppterm ~subst ~metasenv ~context ind) + (PP.ppterm ~subst ~metasenv ~context so) ))); (match arity1,ta with | (C.Sort (C.CProp | C.Type _), C.Sort _) @@ -967,7 +717,7 @@ and eat_lambdas ~subst ~metasenv context n te = eat_lambdas ~subst ~metasenv ((name,(C.Decl so))::context) (n - 1) ta | (n, te) -> raise (AssertFailure (lazy (Printf.sprintf "eat_lambdas (%d, %s)" n - (NCicPp.ppterm ~subst ~metasenv ~context te)))) + (PP.ppterm ~subst ~metasenv ~context te)))) and eat_or_subst_lambdas ~subst ~metasenv n te to_be_subst args (context, recfuns, x as k) @@ -982,34 +732,34 @@ and eat_or_subst_lambdas ~subst ~metasenv n te to_be_subst args | (_, te, _, _) -> te, k 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 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" ^ - NCicPp.ppcontext ~subst ~metasenv context^ - NCicPp.ppterm ~metasenv ~subst ~context t^ + PP.ppcontext ~subst ~metasenv context^ + PP.ppterm ~metasenv ~subst ~context t^ string_of_recfuns ~subst ~metasenv ~context recfuns); *) try match t with | C.Rel m as t when is_dangerous m recfuns -> raise (NotGuarded (lazy - (NCicPp.ppterm ~subst ~metasenv ~context t ^ + (PP.ppterm ~subst ~metasenv ~context t ^ " is a partial application of a fix"))) | C.Appl ((C.Rel m)::tl) as t when is_dangerous m recfuns -> let rec_no = get_recno m recfuns in if not (List.length tl > rec_no) then raise (NotGuarded (lazy - (NCicPp.ppterm ~context ~subst ~metasenv t ^ + (PP.ppterm ~context ~subst ~metasenv t ^ " is a partial application of a fix"))) else let rec_arg = List.nth tl rec_no in 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)))); + ^^ " smaller.\ncontext:\n%s") (PP.ppterm ~context ~subst ~metasenv + t) (PP.ppterm ~context ~subst ~metasenv rec_arg) + (PP.ppcontext ~subst ~metasenv context)))); List.iter (aux k) tl | C.Appl ((C.Rel m)::tl) when is_unfolded m recfuns -> let fixed_args = get_fixed_args m recfuns in @@ -1098,48 +848,66 @@ 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) -(* - | C.Fix (_, fl) -> - 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,_ = - 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 - | C.CoFix (_, fl) -> - 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,_ = - 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 -*) - -and guarded_by_constructors ~subst ~metasenv _ _ _ _ _ _ _ = true - +and guarded_by_constructors ~subst ~metasenv context t indURI indlen = + let rec aux context n nn h te = + match R.whd ~subst context te with + | C.Rel m when m > n && m <= nn -> h + | C.Rel _ | C.Meta _ -> true + | C.Sort _ + | C.Implicit _ + | C.Prod _ + | C.Const (Ref.Ref (_,_,Ref.Ind _)) + | C.LetIn _ -> raise (AssertFailure (lazy "17")) + | C.Lambda (name,so,de) -> + does_not_occur ~subst context n nn so && + aux ((name,C.Decl so)::context) (n + 1) (nn + 1) h de + | 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 -> + 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 rec analyse_instantiated_type rec_spec args = + match rec_spec, args with + | h::rec_spec, he::args -> + aux context n nn h he && analyse_instantiated_type rec_spec args + | _,[] -> true + | _ -> raise (AssertFailure (lazy + ("Too many args for constructor: " ^ String.concat " " + (List.map (fun x-> PP.ppterm ~subst ~metasenv ~context x) args)))) + in + let left, args = HExtlib.split_nth paramsno tl in + List.for_all (does_not_occur ~subst context n nn) left && + analyse_instantiated_type rec_params args + | C.Appl ((C.Match (_,out,te,pl))::_) + | C.Match (_,out,te,pl) as t -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in + List.for_all (does_not_occur ~subst context n nn) tl && + 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 -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in + let fl,_,_ = E.get_checked_fixes ref 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)) + fl + | C.Const _ + | C.Appl _ as t -> does_not_occur ~subst context n nn t + in + aux context 0 indlen false t + and recursive_args ~subst ~metasenv context n nn te = match R.whd context te with | C.Rel _ | C.Appl _ | C.Const _ -> [] @@ -1148,7 +916,7 @@ and recursive_args ~subst ~metasenv context n nn te = (recursive_args ~subst ~metasenv ((name,(C.Decl so))::context) (n+1) (nn + 1) de) | t -> - raise (AssertFailure (lazy ("recursive_args:" ^ NCicPp.ppterm ~subst + raise (AssertFailure (lazy ("recursive_args:" ^ PP.ppterm ~subst ~metasenv ~context:[] t))) and get_new_safes ~subst (context, recfuns, x as k) p rl = @@ -1160,13 +928,6 @@ and get_new_safes ~subst (context, recfuns, x as k) p rl = | C.Meta _ as e, _ | e, [] -> e, k | _ -> raise (AssertFailure (lazy "Ill formed pattern")) -and split_prods ~subst context n te = - match n, R.whd ~subst context te with - | 0, _ -> context,te - | n, C.Prod (name,so,ta) when n > 0 -> - split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta - | _ -> raise (AssertFailure (lazy "split_prods")) - and is_really_smaller r_uri r_len ~subst ~metasenv (context, recfuns, x as k) te = @@ -1180,24 +941,6 @@ and is_really_smaller | C.Rel _ | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false - (*| C.Fix (_, fl) -> - 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,_ = - 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 && - is_really_smaller ~subst (tys@context) n_plus_len nn_plus_len kl - x_plus_len safes' bo - ) fl true*) | C.Meta _ -> true | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) -> (match term with @@ -1265,8 +1008,8 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = raise (TypeCheckerFailure (lazy (Printf.sprintf ( "the type of the body is not convertible with the declared one.\n"^^ "inferred type:\n%s\nexpected type:\n%s") - (NCicPp.ppterm ~subst ~metasenv ~context:[] ty_te) - (NCicPp.ppterm ~subst ~metasenv ~context:[] ty)))) + (PP.ppterm ~subst ~metasenv ~context:[] ty_te) + (PP.ppterm ~subst ~metasenv ~context:[] ty)))) | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty) | C.Inductive (is_ind, leftno, tyl, _) -> check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl @@ -1316,8 +1059,8 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = (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) + if not + (guarded_by_constructors ~subst ~metasenv types bo uri len) then raise (TypeCheckerFailure (lazy "CoFix: not guarded by constructors")) -- 2.39.2