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=907dd8b6cf3c8e8254f5adb165980d86b37904d6;hpb=c37379cd56f14844c5ce165086dd1901f83758b0;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 907dd8b6c..dfb014c20 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -539,11 +539,11 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) = (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 - " @@ -557,13 +557,23 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty = raise (TypeCheckerFailure (lazy (Printf.sprintf - ("Appl: wrong parameter-type, expected %s, found %s") - (NCicPp.ppterm ~subst ~metasenv ~context ty_arg) + ("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 ;; @@ -671,13 +681,13 @@ 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 ty_he 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 @@ -712,9 +722,8 @@ 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 @@ -750,8 +759,8 @@ let rec typeof ~subst ~metasenv context term = (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 r))) - (NCicPp.ppterm ~metasenv ~subst ~context (List.nth pl (j-1))) + (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 @@ -897,27 +906,41 @@ 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 @@ -1044,7 +1067,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