X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=7e9cd70b206dcde2d7fe22ab6fb4044b775c7ca5;hb=30704126796b07213d6da3ca25156d82e761d554;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..7e9cd70b2 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -608,6 +608,11 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty = | (arg, ty_arg)::tl -> (match R.whd ~subst context ty_he with | C.Prod (n,s,t) -> +(* + prerr_endline (NCicPp.ppterm ~context s ^ " - Vs - " ^ NCicPp.ppterm + ~context ty_arg); + prerr_endline (NCicPp.ppterm ~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 @@ -664,10 +669,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 @@ -720,9 +727,16 @@ let rec typeof ~subst ~metasenv context term = | 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 +(* + prerr_endline ("HEAD: " ^ NCicPp.ppterm ~context ty_he); + prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm + ~context) (List.map snd args_with_ty))); + prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm + ~context) (List.map fst args_with_ty))); +*) eat_prods ~subst ~metasenv context 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 = @@ -765,32 +779,36 @@ 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 (C.Const + (Ref.mk_constructor j r))) + (NCicPp.ppterm ~context (List.nth pl (j-1))) + (NCicPp.ppterm ~context p_ty) (NCicPp.ppterm ~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 = @@ -953,7 +971,7 @@ let rec typeof ~subst ~metasenv context term = in typeof_aux context term -and check_mutual_inductive_defs _ = assert false +and check_mutual_inductive_defs _ = () and eat_lambdas ~subst context n te = match (n, R.whd ~subst context te) with @@ -967,19 +985,24 @@ and eat_lambdas ~subst context n te = and guarded_by_destructors ~subst 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 ~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 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 k rec_arg) then + raise (NotGuarded (lazy + (NCicPp.ppterm ~context ~subst 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 @@ -1000,8 +1023,8 @@ and guarded_by_destructors ~subst context recfuns t = | _ -> 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) -> @@ -1132,67 +1155,48 @@ 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 ty); + prerr_endline ("BO: " ^ NCicPp.ppterm 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)))) | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty) - | C.Inductive _ as obj -> check_mutual_inductive_defs uri obj + | C.Inductive _ as obj -> check_mutual_inductive_defs obj | C.Fixpoint (inductive,fl,_) -> let types,kl,len = List.fold_left @@ -1202,6 +1206,7 @@ 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"))) @@ -1212,9 +1217,7 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) = 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 context (enum_from (x+1) kl) m; end else match returns_a_coinductive ~subst [] ty with | None -> @@ -1229,9 +1232,6 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) = (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 *)