X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=9de1f0f5c27203258e4512d6bab0a5e9b8f7598d;hb=ccb09743430d585f773eb83ad9a18d1dbdda07ed;hp=125b66ed35cbd73a945a20a99f4d9d90df1dd8ac;hpb=a5edfb2ab4773a6b162f1458fa4497b4296f2444;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 125b66ed3..9de1f0f5c 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -557,9 +557,12 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty = raise (TypeCheckerFailure (lazy (Printf.sprintf - ("Appl: wrong parameter-type, expected\n%s\nfound\n%s") - (NCicPp.ppterm ~subst ~metasenv ~context s) - (NCicPp.ppterm ~subst ~metasenv ~context ty_arg)))) + ("Appl: wrong application of %s: the parameter %s has type"^^ + "\n%s\nbut it 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 @@ -678,17 +681,20 @@ 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 ~context ty_he); + prerr_endline ("HEAD: " ^ NCicPp.ppterm ~subst ~metasenv ~context ty_he); prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm - ~context) (List.map snd args_with_ty))); + ~subst ~metasenv ~context) (List.map snd args_with_ty))); prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm - ~context) (List.map fst args_with_ty))); + ~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 (_,_,Ref.Ind tyno) as r,outtype,term,pl) -> let outsort = typeof_aux context outtype in - let leftno = E.get_indty_leftno r in + let inductive,leftno,itl,_,_ = E.get_checked_indtys r in + let constructorsno = + let _,_,_,cl = List.nth itl tyno in List.length cl + in let parameters, arguments = let ty = R.whd ~subst context (typeof_aux context term) in let r',tl = @@ -719,16 +725,9 @@ let rec typeof ~subst ~metasenv context term = 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 - let _,name,ty,cl = List.nth itl i in - let cl_len = List.length cl in - leftno, cl_len - in if List.length pl <> constructorsno then raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match"))); let j,branches_ok,p_ty, exp_p_ty = @@ -904,27 +903,43 @@ 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 _)) -> + (* TODO: we should pass all these parameters since we + * have them already *) + 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 @@ -936,7 +951,7 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl = 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 + let tys = List.rev (List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl) in ignore (List.fold_right (fun (_,_,_,cl) i -> @@ -1051,7 +1066,7 @@ and guarded_by_destructors ~subst ~metasenv context recfuns t = ) fl true *) -and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false +and guarded_by_constructors ~subst ~metasenv _ _ _ _ _ _ _ = true and recursive_args ~subst ~metasenv context n nn te = match R.whd context te with @@ -1152,8 +1167,6 @@ and type_of_constant ((Ref.Ref (_,uri,_)) as ref) = 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 match cobj, ref with