X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=dfb014c20d8ada6c609823153632d701b299cee2;hb=c25986cdbd05f0c06d93f850453b5f82695b7814;hp=96b2f9186fcc7ebfcec7714e9a35f6d1fe66df0a;hpb=e457ababc4cb5b75540cfa131a30fdee3f9bc0ed;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 96b2f9186..dfb014c20 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -239,70 +239,6 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^ (UriManager.string_of_uri uri)))) -(* Main function to checks the correctness of a mutual *) -(* inductive block definition. This is the function *) -(* exported to the proof-engine. *) -and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = - let module U = UriManager in - (* let's check if the arity of the inductive types are well *) - (* formed *) - let ugrap1 = List.fold_left - (fun ugraph (_,_,x,_) -> let _,ugraph' = - type_of ~logger x ugraph in ugraph') - ugraph itl in - - (* let's check if the types of the inductive constructors *) - (* are well formed. *) - (* In order not to use type_of_aux we put the types of the *) - (* mutual inductive types at the head of the types of the *) - (* constructors using Prods *) - let len = List.length itl in - let tys = - List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in - let _,ugraph2 = - List.fold_right - (fun (_,_,_,cl) (i,ugraph) -> - let ugraph'' = - List.fold_left - (fun ugraph (name,te) -> - let debruijnedte = debruijn uri len te in - let augmented_term = - List.fold_right - (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i)) - itl debruijnedte - in - let _,ugraph' = type_of ~logger augmented_term ugraph in - (* let's check also the positivity conditions *) - if - not - (are_all_occurrences_positive tys uri indparamsno i 0 len - debruijnedte) - then - begin - prerr_endline (UriManager.string_of_uri uri); - prerr_endline (string_of_int (List.length tys)); - raise - (TypeCheckerFailure - (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) end - else - ugraph' - ) ugraph cl in - (i + 1),ugraph'' - ) itl (1,ugrap1) - in - ugraph2 - -(* Main function to checks the correctness of a mutual *) -(* inductive block definition. *) -and check_mutual_inductive_defs uri obj ugraph = - match obj with - Cic.InductiveDefinition (itl, params, indparamsno, _) -> - typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph - | _ -> - raise (TypeCheckerFailure ( - lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - (* 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. *) @@ -584,7 +520,7 @@ let debruijn ?(cb=fun _ _ -> ()) uri number_of_types = aux 0 ;; -let sort_of_prod ~subst context (name,s) (t1, t2) = +let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) = let t1 = R.whd ~subst context t1 in let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in match t1, t2 with @@ -599,27 +535,45 @@ let sort_of_prod ~subst context (name,s) (t1, t2) = | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf "Prod: expected two sorts, found = %s, %s" - (NCicPp.ppterm t1) (NCicPp.ppterm t2)))) + (NCicPp.ppterm ~subst ~metasenv ~context t1) + (NCicPp.ppterm ~subst ~metasenv ~context t2)))) ;; -let eat_prods ~subst ~metasenv context ty_he args_with_ty = +let eat_prods ~subst ~metasenv context he ty_he args_with_ty = let rec aux ty_he = function | [] -> ty_he | (arg, ty_arg)::tl -> - (match R.whd ~subst context ty_he with + 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)); +*) if R.are_convertible ~subst ~metasenv context ty_arg s then aux (S.subst ~avoid_beta_redexes:true arg t) tl else raise (TypeCheckerFailure (lazy (Printf.sprintf - ("Appl: wrong parameter-type, expected %s, found %s") - (NCicPp.ppterm ty_arg) (NCicPp.ppterm s)))) + ("Appl: wrong application of %s: the parameter %s has type"^^ + "\n%s\nbut is should have type \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)))) | _ -> raise (TypeCheckerFailure - (lazy "Appl: this is not a function, it cannot be applied"))) + (lazy (Printf.sprintf + "Appl: %s is not a function, it cannot be applied" + (NCicPp.ppterm ~subst ~metasenv ~context + (let res = List.length tl in + let eaten = List.length args_with_ty - res in + (NCic.Appl + (he::List.map fst + (fst (HExtlib.split_nth eaten args_with_ty))))))))) in aux ty_he args_with_ty ;; @@ -637,7 +591,7 @@ let fix_lefts_in_constrs ~subst uri paramsno tyl i = cl in let lefts = fst (split_prods ~subst [] paramsno arity) in - tys@lefts, len, cl' + lefts@tys, len, cl' ;; exception DoesOccur;; @@ -664,10 +618,12 @@ let does_not_occur ~subst context n nn t = with DoesOccur -> false ;; -exception NotGuarded;; +exception NotGuarded of string Lazy.t;; let rec typeof ~subst ~metasenv context term = - let rec typeof_aux context = function + let rec typeof_aux context = + fun t -> (*prerr_endline (NCicPp.ppterm ~context t); *) + match t with | C.Rel n -> (try match List.nth context (n - 1) with @@ -678,22 +634,22 @@ let rec typeof ~subst ~metasenv context term = | C.Sort s -> C.Sort (C.Type 0) | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found")) | C.Meta (n,l) as t -> - let canonical_context,ty = + let canonical_ctx,ty = try let _,c,_,ty = U.lookup_subst n subst in c,ty with U.Subst_not_found _ -> try 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 t)))) + "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t)))) in - check_metasenv_consistency t context canonical_context l; + check_metasenv_consistency t ~subst ~metasenv context canonical_ctx l; S.subst_meta l ty | C.Const ref -> type_of_constant ref | C.Prod (name,s,t) -> let sort1 = typeof_aux context s in let sort2 = typeof_aux ((name,(C.Decl s))::context) t in - sort_of_prod ~subst context (name,s) (sort1,sort2) + sort_of_prod ~metasenv ~subst context (name,s) (sort1,sort2) | C.Lambda (n,s,t) -> let sort = typeof_aux context s in (match R.whd ~subst context sort with @@ -703,26 +659,37 @@ 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 s) (NCicPp.ppterm sort))))); + "of type %s") (NCicPp.ppterm ~subst ~metasenv ~context s) + (NCicPp.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) -> let ty_t = typeof_aux context t in + let _ = typeof_aux context ty in if not (R.are_convertible ~subst ~metasenv context ty ty_t) then raise (TypeCheckerFailure (lazy (Printf.sprintf "The type of %s is %s but it is expected to be %s" - (NCicPp.ppterm t) (NCicPp.ppterm ty_t) (NCicPp.ppterm ty)))) + (NCicPp.ppterm ~subst ~metasenv ~context t) + (NCicPp.ppterm ~subst ~metasenv ~context ty_t) + (NCicPp.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 | C.Appl (he::(_::_ as args)) -> let ty_he = typeof_aux context he in let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in - eat_prods ~subst ~metasenv context ty_he args_with_ty +(* + prerr_endline ("HEAD: " ^ NCicPp.ppterm ~subst ~metasenv ~context ty_he); + prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm + ~subst ~metasenv ~context) (List.map snd args_with_ty))); + prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm + ~subst ~metasenv ~context) (List.map fst args_with_ty))); +*) + eat_prods ~subst ~metasenv context he ty_he args_with_ty | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2")) - | C.Match (Ref.Ref (dummy_depth,uri,Ref.Ind tyno) as r,outtype,term,pl) -> + | C.Match (Ref.Ref (_,_,Ref.Ind tyno) as r,outtype,term,pl) -> let outsort = typeof_aux context outtype in let leftno = E.get_indty_leftno r in let parameters, arguments = @@ -735,27 +702,28 @@ let rec typeof ~subst ~metasenv context term = raise (TypeCheckerFailure (lazy (Printf.sprintf "Case analysis: analysed term %s is not an inductive one" - (NCicPp.ppterm term)))) in + (NCicPp.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 ty) (NCicPp.ppterm (C.Const r'))))) + (NCicPp.ppterm ~subst ~metasenv ~context ty) + (NCicPp.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 ty)))) in + raise (TypeCheckerFailure (lazy (Printf.sprintf + "%s is partially applied" + (NCicPp.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 else C.Appl ((C.Const r)::parameters) in let type_of_sort_of_ind_ty = typeof_aux context sort_of_ind_type in - if not (check_allowed_sort_elimination ~subst ~metasenv r context - sort_of_ind_type type_of_sort_of_ind_ty outsort) - then raise (TypeCheckerFailure (lazy ("Sort elimination not allowed"))); + check_allowed_sort_elimination ~subst ~metasenv r context + sort_of_ind_type type_of_sort_of_ind_ty outsort; (* let's check if the type of branches are right *) let leftno,constructorsno = let inductive,leftno,itl,_,i = E.get_checked_indtys r in @@ -765,32 +733,38 @@ let rec typeof ~subst ~metasenv context term = in if List.length pl <> constructorsno then raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match"))); - let j,branches_ok = + let j,branches_ok,p_ty, exp_p_ty = List.fold_left - (fun (j,b) p -> + (fun (j,b,old_p_ty,old_exp_p_ty) p -> if b then let cons = - let cons = Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)) in + let cons = Ref.mk_constructor j r in if parameters = [] then C.Const cons else C.Appl (C.Const cons::parameters) in let ty_p = typeof_aux context p in let ty_cons = typeof_aux context cons in let ty_branch = - type_of_branch ~subst context leftno outtype cons ty_cons 0 in - j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch + type_of_branch ~subst context leftno outtype cons ty_cons 0 + in + j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch, + ty_p, ty_branch else - j,false - ) (1,true) pl - in - if not branches_ok then - raise - (TypeCheckerFailure - (lazy (Printf.sprintf "Branch for constructor %s has wrong type" - (NCicPp.ppterm (C.Const - (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)))))))); - let res = outtype::arguments@[term] in - R.head_beta_reduce (C.Appl res) + j,false,old_p_ty,old_exp_p_ty + ) (1,true,C.Sort C.Prop,C.Sort C.Prop) pl + in + if not branches_ok then + raise + (TypeCheckerFailure + (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^ + "has type %s\nnot convertible with %s") + (NCicPp.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)))); + let res = outtype::arguments@[term] in + R.head_beta_reduce (C.Appl res) | C.Match _ -> assert false and type_of_branch ~subst context leftno outty cons tycons liftno = @@ -813,7 +787,9 @@ let rec typeof ~subst ~metasenv context term = (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - with the actual context *) - and check_metasenv_consistency term context canonical_context l = + and check_metasenv_consistency + ~subst ~metasenv term context canonical_context l + = match l with | shift, NCic.Irl n -> let context = snd (HExtlib.split_nth shift context) in @@ -823,10 +799,11 @@ let rec typeof ~subst ~metasenv context term = | _,_,[] -> raise (AssertFailure (lazy (Printf.sprintf "Local and canonical context %s have different lengths" - (NCicPp.ppterm term)))) + (NCicPp.ppterm ~subst ~context ~metasenv term)))) | m,[],_::_ -> raise (TypeCheckerFailure (lazy (Printf.sprintf - "Unbound variable -%d in %s" m (NCicPp.ppterm term)))) + "Unbound variable -%d in %s" m + (NCicPp.ppterm ~subst ~metasenv ~context term)))) | m,t::tl,ct::ctl -> (match t,ct with (_,C.Decl t1), (_,C.Decl t2) @@ -838,15 +815,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 term) (NCicPp.ppterm t2) (NCicPp.ppterm t1) - ))) + (NCicPp.ppterm ~subst ~metasenv ~context term) + (NCicPp.ppterm ~subst ~metasenv ~context t2) + (NCicPp.ppterm ~subst ~metasenv ~context t1)))) | _,_ -> raise - (TypeCheckerFailure - (lazy (Printf.sprintf + (TypeCheckerFailure (lazy (Printf.sprintf ("Not well typed metavariable local context for %s: " ^^ "a definition expected, but a declaration found") - (NCicPp.ppterm term))))); + (NCicPp.ppterm ~subst ~metasenv ~context term))))); compare (m - 1,tl,ctl) in compare (n,context,canonical_context) @@ -890,7 +867,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 ct) (NCicPp.ppterm t)))) + (NCicPp.ppterm ~subst ~metasenv ~context ct) + (NCicPp.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 @@ -898,13 +876,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 ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t)))) + (NCicPp.ppterm ~subst ~metasenv ~context ct) + (NCicPp.ppterm ~subst ~metasenv ~context t) + (NCicPp.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 term)))) + (NCicPp.ppterm ~subst ~metasenv ~context term)))) and is_non_informative context paramsno c = let rec aux context c = @@ -926,60 +906,104 @@ let rec typeof ~subst ~metasenv context term = let arity2 = R.whd ~subst context arity2 in match arity1,arity2 with | C.Prod (name,so1,de1), C.Prod (_,so2,de2) -> - R.are_convertible ~subst ~metasenv context so1 so2 && - aux ((name, C.Decl so1)::context) - (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2 + 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) + ))); + aux ((name, C.Decl so1)::context) + (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2 | C.Sort _, C.Prod (name,so,ta) -> - (R.are_convertible ~subst ~metasenv context so ind && - match arity1,ta with - | (C.Sort (C.CProp | C.Type _), C.Sort _) - | (C.Sort C.Prop, C.Sort C.Prop) -> true - | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) -> - let inductive,leftno,itl,_,i = E.get_checked_indtys r in - let itl_len = List.length itl in - let _,name,ty,cl = List.nth itl i in - let cl_len = List.length cl in - (* is it a singleton or empty non recursive and non informative - definition? *) - cl_len = 0 || - (itl_len = 1 && cl_len = 1 && - is_non_informative [name,C.Decl ty] leftno - (let _,_,x = List.nth cl 0 in x)) - | _,_ -> false) - | _,_ -> false + 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) + ))); + (match arity1,ta with + | (C.Sort (C.CProp | C.Type _), C.Sort _) + | (C.Sort C.Prop, C.Sort C.Prop) -> () + | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) -> + let inductive,leftno,itl,_,i = E.get_checked_indtys r in + let itl_len = List.length itl in + let _,name,ty,cl = List.nth itl i in + let cl_len = List.length cl in + (* is it a singleton or empty non recursive and non informative + definition? *) + if not + (cl_len = 0 || + (itl_len = 1 && cl_len = 1 && + is_non_informative [name,C.Decl ty] leftno + (let _,_,x = List.nth cl 0 in x))) + then + raise (TypeCheckerFailure (lazy + ("Sort elimination not allowed"))); + | _,_ -> ()) + | _,_ -> () in aux in typeof_aux context term -and check_mutual_inductive_defs _ = assert false +and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl = + (* let's check if the arity of the inductive types are well formed *) + List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl; + (* let's check if the types of the inductive constructors are well formed. *) + let len = List.length tyl in + let tys = List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in + ignore + (List.fold_right + (fun (_,_,_,cl) i -> + List.iter + (fun (_,name,te) -> + let debruijnedte = debruijn uri len te in + ignore (typeof ~subst ~metasenv tys debruijnedte); + (* let's check also the positivity conditions *) + if false (* + not + (are_all_occurrences_positive tys uri indparamsno i 0 len + debruijnedte) *) + then + raise + (TypeCheckerFailure + (lazy ("Non positive occurence in "^NUri.string_of_uri uri)))) + cl; + i + 1) + tyl 1) -and eat_lambdas ~subst context n te = +and eat_lambdas ~subst ~metasenv context n te = match (n, R.whd ~subst context te) with | (0, _) -> (te, context) | (n, C.Lambda (name,so,ta)) when n > 0 -> - eat_lambdas ~subst ((name,(C.Decl so))::context) (n - 1) ta + eat_lambdas ~subst ~metasenv ((name,(C.Decl so))::context) (n - 1) ta | (n, te) -> - raise (AssertFailure - (lazy (Printf.sprintf "9 (%d, %s)" n (NCicPp.ppterm te)))) + raise (AssertFailure (lazy (Printf.sprintf "9 (%d, %s)" n + (NCicPp.ppterm ~subst ~metasenv ~context te)))) -and guarded_by_destructors ~subst context recfuns t = +and guarded_by_destructors ~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) = function - | C.Rel m when List.mem_assoc m recfuns -> raise NotGuarded + | C.Rel m as t when List.mem_assoc m recfuns -> + raise (NotGuarded (lazy + (NCicPp.ppterm ~subst ~metasenv ~context t ^ " passed around"))) | C.Rel m -> (match List.nth context (m-1) with | _,C.Decl _ -> () | _,C.Def (bo,_) -> aux (context, recfuns, x, safes) (S.lift m bo)) | C.Meta _ -> () - | C.Appl ((C.Rel m)::tl) when List.mem_assoc m recfuns -> + | C.Appl ((C.Rel m)::tl) as t when List.mem_assoc m recfuns -> let rec_no = List.assoc m recfuns in - if not (List.length tl > rec_no) then raise NotGuarded + if not (List.length tl > rec_no) then + raise (NotGuarded (lazy + (NCicPp.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 ~subst k rec_arg) then raise - NotGuarded; + if not (is_really_smaller ~subst ~metasenv k rec_arg) then + raise (NotGuarded (lazy + (NCicPp.ppterm ~context ~subst ~metasenv rec_arg ^ " not smaller"))); List.iter (aux k) tl | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t -> (match R.whd ~subst context term with @@ -993,15 +1017,15 @@ and guarded_by_destructors ~subst context recfuns t = List.iter (aux k) args; List.iter2 (fun p (_,_,bruijnedc) -> - let rl = recursive_args ~subst c_ctx 0 len bruijnedc in + let rl = recursive_args ~subst ~metasenv c_ctx 0 len bruijnedc in let p, k = get_new_safes ~subst k p rl in aux k p) pl cl | _ -> recursor aux k t) | t -> recursor aux k t in - try aux (context, recfuns, 1, []) t;true - with NotGuarded -> false + try aux (context, recfuns, 1, []) t + with NotGuarded s -> raise (TypeCheckerFailure s) (* | C.Fix (_, fl) -> @@ -1043,15 +1067,18 @@ and guarded_by_destructors ~subst context recfuns t = ) fl true *) -and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false +and guarded_by_constructors ~subst ~metasenv _ _ _ _ _ _ _ = true -and recursive_args ~subst context n nn te = +and recursive_args ~subst ~metasenv context n nn te = match R.whd context te with - | C.Rel _ -> [] + | C.Rel _ | C.Appl _ -> [] | C.Prod (name,so,de) -> (not (does_not_occur ~subst context n nn so)) :: - (recursive_args ~subst ((name,(C.Decl so))::context) (n+1) (nn + 1) de) - | _ -> raise (AssertFailure (lazy ("recursive_args"))) + (recursive_args ~subst ~metasenv + ((name,(C.Decl so))::context) (n+1) (nn + 1) de) + | t -> + raise (AssertFailure (lazy ("recursive_args:" ^ NCicPp.ppterm ~subst + ~metasenv ~context:[] t))) and get_new_safes ~subst (context, recfuns, x, safes as k) p rl = match R.whd ~subst context p, rl with @@ -1069,7 +1096,7 @@ 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 (context, recfuns, x, safes as k) te = +and is_really_smaller ~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.Rel _ -> false @@ -1082,7 +1109,7 @@ and is_really_smaller ~subst (context, recfuns, x, safes as k) te = (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) (*CSC: solo perche' non abbiamo trovato controesempi *) (*TASSI: da capire soprattutto se he è un altro fix che non ha ridotto...*) - is_really_smaller ~subst k he + is_really_smaller ~subst ~metasenv k he | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false (*| C.Fix (_, fl) -> @@ -1111,16 +1138,16 @@ and is_really_smaller ~subst (context, recfuns, x, safes as k) te = | 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 if not isinductive then - List.for_all (is_really_smaller ~subst k) pl + List.for_all (is_really_smaller ~subst ~metasenv k) pl else let c_ctx,len,cl = fix_lefts_in_constrs ~subst uri paramsno tl i in List.for_all2 (fun p (_,_,debruijnedte) -> - let rl' = recursive_args ~subst c_ctx 0 len debruijnedte in + 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 k e) + is_really_smaller ~subst ~metasenv k e) pl cl - | _ -> List.for_all (is_really_smaller ~subst k) pl) + | _ -> List.for_all (is_really_smaller ~subst ~metasenv k) pl) and returns_a_coinductive ~subst context ty = match R.whd ~subst context ty with @@ -1132,67 +1159,52 @@ and returns_a_coinductive ~subst context ty = returns_a_coinductive ~subst ((n,C.Decl so)::context) de | _ -> None -and type_of_constant ref = -assert false (* +and type_of_constant ((Ref.Ref (_,uri,_)) as ref) = let cobj = - match E.get_obj uri with - | true, cobj -> cobj - | false, uobj -> - logger#log (`Start_type_checking uri) ; - let ugraph1_dust = - typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in - try - CicEnvironment.set_type_checking_info uri ; - logger#log (`Type_checking_completed uri) ; - (match CicEnvironment.is_type_checked ~trust:false ugraph uri with - CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph') - | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError - ) - with - (* - this is raised if set_type_checking_info is called on an object - that has no associated universe file. If we are in univ_maker - phase this is OK since univ_maker will properly commit the - object. - *) - Invalid_argument s -> - (*debug_print (lazy s);*) - uobj,ugraph1_dust + match E.get_obj uri with + | true, cobj -> cobj + | false, uobj -> + !logger (`Start_type_checking uri); + check_obj_well_typed uobj; + E.add_obj uobj; + !logger (`Type_checking_completed uri); + if not (fst (E.get_obj uri)) then + raise (AssertFailure (lazy "environment error")); + uobj in -CASO COSTRUTTORE - match cobj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,arity,_) = List.nth dl i in - arity,ugraph1 - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri))) -CASO TIPO INDUTTIVO - match cobj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,_,cl) = List.nth dl i in - let (_,ty) = List.nth cl (j-1) in - ty,ugraph1 - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) -CASO COSTANTE -CASO FIX/COFIX -*) + match cobj, ref with + | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind i) -> + let _,_,arity,_ = List.nth tl i in arity + | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j)) -> + let _,_,_,cl = List.nth tl i in + let _,_,arity = List.nth cl (j-1) in + arity + | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,_,(Ref.Fix (i,_)|Ref.CoFix i)) -> + let _,_,_,arity,_ = List.nth fl i in + arity + | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,_,(Ref.Def |Ref.Decl)) -> ty + | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference")) -and typecheck_obj0 (uri,height,metasenv,subst,kind) = +and check_obj_well_typed (uri,height,metasenv,subst,kind) = (* CSC: here we should typecheck the metasenv and the subst *) assert (metasenv = [] && subst = []); match kind with | C.Constant (_,_,Some te,ty,_) -> +(* + prerr_endline ("TY: " ^ NCicPp.ppterm ~subst ~metasenv ~context:[] ty); + prerr_endline ("BO: " ^ NCicPp.ppterm ~subst ~metasenv ~context:[] te); +*) let _ = typeof ~subst ~metasenv [] ty in let ty_te = typeof ~subst ~metasenv [] te in +(* prerr_endline "XXXX"; *) if not (R.are_convertible ~subst ~metasenv [] ty_te ty) then raise (TypeCheckerFailure (lazy (Printf.sprintf "the type of the body is not the one expected:\n%s\nvs\n%s" - (NCicPp.ppterm ty_te) (NCicPp.ppterm ty)))) + (NCicPp.ppterm ~subst ~metasenv ~context:[] ty_te) + (NCicPp.ppterm ~subst ~metasenv ~context:[] ty)))) | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty) - | C.Inductive _ as obj -> check_mutual_inductive_defs uri obj + | 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 = List.fold_left @@ -1202,19 +1214,19 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) = ) ([],[],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 types (x + 1) bo in + 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 in - if not (guarded_by_destructors - ~subst context (enum_from (x+1) kl) m) then - raise(TypeCheckerFailure(lazy("Fix: not guarded by destructors"))) + guarded_by_destructors + ~subst ~metasenv context (enum_from (x+2) kl) m end else match returns_a_coinductive ~subst [] ty with | None -> @@ -1222,16 +1234,13 @@ and typecheck_obj0 (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 + if not (guarded_by_constructors ~subst ~metasenv types 0 len false bo [] uri) then raise (TypeCheckerFailure (lazy "CoFix: not guarded by constructors")) ) fl -let typecheck_obj (*uri*) obj = assert false (* - let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in - let ugraph, univlist, obj = CicUnivUtils.clean_and_fill uri obj ugraph in - CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist) -*) -;; +let typecheck_obj = check_obj_well_typed;; + +(* EOF *)