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=df6255e5f045a272f41eadbf3dc123d7bb762f5a;hpb=9dac09ff867a3ec6298c85df95579b199da54d27;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index df6255e5f..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. *) @@ -603,16 +539,17 @@ 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 ~context s ^ " - Vs - " ^ NCicPp.ppterm + prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context s ^ " - Vs - " + ^ NCicPp.ppterm ~subst ~metasenv ~context ty_arg); - prerr_endline (NCicPp.ppterm ~context (S.subst ~avoid_beta_redexes:true arg t)); + 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 @@ -620,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 ;; @@ -718,6 +665,7 @@ let rec typeof ~subst ~metasenv context term = 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 @@ -733,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 @@ -774,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 @@ -812,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 @@ -959,34 +906,72 @@ 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 _ = () +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 ~metasenv context n te = match (n, R.whd ~subst context te) with @@ -1082,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 @@ -1205,18 +1190,21 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = 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"; +(* 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 ~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 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