From 7bf119d0c9d56ca0cb75c448beebf57bba7c8c6e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 1 Apr 2008 17:01:45 +0000 Subject: [PATCH] 1) added get_checked_indtys that returns the whole block of inductive types 2) type checking of Match almost finished --- .../components/ng_kernel/nCicEnvironment.ml | 9 + .../components/ng_kernel/nCicEnvironment.mli | 7 +- .../components/ng_kernel/nCicTypeChecker.ml | 705 +++++++----------- 3 files changed, 277 insertions(+), 444 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 02b3baab6..4a6a21d9d 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -24,6 +24,15 @@ let get_checked_def = function | _ -> prerr_endline "get_checked_def on a non def"; assert false ;; +let get_checked_indtys = function + | NReference.Ref (_, uri, NReference.Ind n) -> + (match get_checked_obj uri with + | _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) -> + inductive,leftno,tys,att,n + | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false) + | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false +;; + let get_checked_fix_or_cofix b = function | NReference.Ref (_, uri, NReference.Fix (fixno,_)) -> (match get_checked_obj uri with diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 225a4aea2..53e6a6ffe 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -28,10 +28,15 @@ val get_checked_obj: NUri.uri -> NCic.obj -val get_checked_def: +val get_checked_def: NReference.reference -> NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int +(* the last integer is the index of the inductive type in the reference *) +val get_checked_indtys: + NReference.reference -> + bool * int * NCic.inductiveType list * NCic.i_attr * int + val get_checked_fix: NReference.reference -> NCic.relevance * string * NCic.term * NCic.term * NCic.f_attr * int diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index a010d9ea1..0299df7a7 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -149,7 +149,7 @@ and does_not_occur ?(subst=[]) context n nn te = (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl in List.fold_right (fun (_,_,ty,bo) i -> @@ -165,7 +165,7 @@ and does_not_occur ?(subst=[]) context n nn te = (fun (types,len) (n,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl in List.fold_right (fun (_,ty,bo) i -> @@ -256,8 +256,8 @@ and weakly_positive context n nn uri te = (n + 1) (nn + 1) uri dest | C.Prod (name,source,dest) -> does_not_occur context n nn - (subst_inductive_type_with_dummy_mutind source)&& - weakly_positive ((Some (name,(C.Decl source)))::context) + (subst_inductive_type_with_dummy_mutind source)&& + weakly_positive ((Some (name,(C.Decl source)))::context) (n + 1) (nn + 1) uri dest | _ -> raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) @@ -290,16 +290,16 @@ and strictly_positive context n nn te = List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> let (ok,paramsno,ity,cl,name) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with C.InductiveDefinition (tl,_,paramsno,_) -> - let (name,_,ity,cl) = List.nth tl i in + let (name,_,ity,cl) = List.nth tl i in (List.length tl = 1, paramsno, ity, cl, name) (* (true, paramsno, ity, cl, name) *) | _ -> - raise - (TypeCheckerFailure - (lazy ("Unknown inductive type:" ^ U.string_of_uri uri))) + raise + (TypeCheckerFailure + (lazy ("Unknown inductive type:" ^ U.string_of_uri uri))) in let (params,arguments) = split tl paramsno in let lifted_params = List.map (CicSubstitution.lift 1) params in @@ -404,32 +404,32 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = let _,ugraph2 = List.fold_right (fun (_,_,_,cl) (i,ugraph) -> - let ugraph'' = + let ugraph'' = List.fold_left (fun ugraph (name,te) -> let debrujinedte = debrujin_constructor uri len te in let augmented_term = - List.fold_right - (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i)) - itl debrujinedte + List.fold_right + (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i)) + itl debrujinedte 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 + not + (are_all_occurrences_positive tys uri indparamsno i 0 len debrujinedte) then begin prerr_endline (UriManager.string_of_uri uri); prerr_endline (string_of_int (List.length tys)); - raise - (TypeCheckerFailure + raise + (TypeCheckerFailure (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) end else - ugraph' + ugraph' ) ugraph cl in - (i + 1),ugraph'' + (i + 1),ugraph'' ) itl (1,ugrap1) in ugraph2 @@ -439,11 +439,11 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = 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 + typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph | _ -> - raise (TypeCheckerFailure ( - lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) + raise (TypeCheckerFailure ( + lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) and recursive_args context n nn te = let module C = Cic in @@ -565,7 +565,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = (match term with C.Rel m when List.mem m safes || m = x -> let (lefts_and_tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tl,_,paramsno,_) -> let tys = @@ -683,7 +683,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,_,ty,bo) i -> @@ -701,7 +701,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = (fun (types,len) (n,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> @@ -766,7 +766,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = (match CicReduction.whd ~subst context term with C.Rel m when List.mem m safes || m = x -> let (lefts_and_tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tl,_,paramsno,_) -> let len = List.length tl in @@ -823,7 +823,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = ) pl_and_cl true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> let (lefts_and_tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tl,_,paramsno,_) -> let (_,isinductive,_,cl) = List.nth tl i in @@ -899,7 +899,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,_,ty,bo) i -> @@ -917,7 +917,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = (fun (types,len) (n,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> @@ -955,11 +955,11 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) -> let consty = - let obj,_ = - try - CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri - with Not_found -> assert false - in + let obj,_ = + try + CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri + with Not_found -> assert false + in match obj with C.InductiveDefinition (itl,_,_,_) -> let (_,_,_,cl) = List.nth itl i in @@ -1075,7 +1075,7 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = (fun (types,len) (n,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl in List.fold_right (fun (_,ty,bo) i -> @@ -1122,7 +1122,7 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl in List.fold_right (fun (_,_,ty,bo) i -> @@ -1139,7 +1139,7 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = (fun (types,len) (n,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl in List.fold_right (fun (_,ty,bo) i -> @@ -1149,89 +1149,6 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = args coInductiveTypeURI ) fl true -and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i - need_dummy ind arity1 arity2 ugraph = - let module C = Cic in - let module U = UriManager in - let arity1 = CicReduction.whd ~subst context arity1 in - let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy = - match arity1, CicReduction.whd ~subst context arity2 with - (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) -> - let b,ugraph1 = - CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in - if b then - check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i - need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 - ugraph1 - else - false,ugraph1 - | (C.Sort _, C.Prod (name,so,ta)) when not need_dummy -> - let b,ugraph1 = - CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in - if not b then - false,ugraph1 - else - check_allowed_sort_elimination_aux ugraph1 - ((Some (name,C.Decl so))::context) ta true - | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph - | (C.Sort C.Prop, C.Sort C.Set) - | (C.Sort C.Prop, C.Sort C.CProp) - | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy -> - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (itl,_,paramsno,_) -> - let itl_len = List.length itl in - let (name,_,ty,cl) = List.nth itl i in - let cl_len = List.length cl in - if (cl_len = 0 || (itl_len = 1 && cl_len = 1)) then - let non_informative,ugraph = - if cl_len = 0 then true,ugraph - else - is_non_informative ~logger [Some (C.Name name,C.Decl ty)] - paramsno (snd (List.nth cl 0)) ugraph - in - (* is it a singleton or empty non recursive and non informative - definition? *) - non_informative, ugraph - else - false,ugraph - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - ) - | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph - | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph - | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph - | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph - | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph - | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph - | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _))) - when need_dummy -> - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (itl,_,paramsno,_) -> - let tys = - List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl - in - let (_,_,_,cl) = List.nth itl i in - (List.fold_right - (fun (_,x) (i,ugraph) -> - if i then - is_small ~logger tys paramsno x ugraph - else - false,ugraph - ) cl (true,ugraph)) - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - ) - | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph - | (_,_) -> false,ugraph - in - check_allowed_sort_elimination_aux ugraph context arity2 need_dummy - and type_of_branch ~subst context argsno need_dummy outtype term constype = let module C = Cic in let module R = CicReduction in @@ -1259,11 +1176,6 @@ and type_of_branch ~subst context argsno need_dummy outtype term constype = (CicSubstitution.lift 1 outtype) term' de) | _ -> raise (AssertFailure (lazy "20")) -(* 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 returns_a_coinductive ~subst context ty = let module C = Cic in match CicReduction.whd ~subst context ty with @@ -1285,7 +1197,7 @@ with the actual context *) ) | C.Appl ((C.MutInd (uri,i,_))::_) -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + match o with C.InductiveDefinition (itl,_,_,_) -> let (_,is_inductive,_,_) = List.nth itl i in if is_inductive then None else (Some uri) @@ -1301,37 +1213,6 @@ with the actual context *) in type_of_aux ~logger context t ugraph -(* is a small constructor? *) -(*CSC: ottimizzare calcolando staticamente *) -and is_small_or_non_informative ~condition ~logger context paramsno c ugraph = - let rec is_small_or_non_informative_aux ~logger context c ugraph = - let module C = Cic in - match CicReduction.whd context c with - C.Prod (n,so,de) -> - let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in - let b = condition s in - if b then - is_small_or_non_informative_aux - ~logger ((Some (n,(C.Decl so)))::context) de ugraph1 - else - false,ugraph1 - | _ -> true,ugraph (*CSC: we trust the type-checker *) - in - let (context',dx) = split_prods ~subst:[] context paramsno c in - is_small_or_non_informative_aux ~logger context' dx ugraph - -and is_small ~logger = - is_small_or_non_informative - ~condition:(fun s -> s=Cic.Sort Cic.Prop || s=Cic.Sort Cic.Set) - ~logger - -and is_non_informative ~logger = - is_small_or_non_informative - ~condition:(fun s -> s=Cic.Sort Cic.Prop) - ~logger - -and type_of ~logger t ugraph = - type_of_aux' ~logger [] [] t ugraph ;; (** wrappers which instantiate fresh loggers *) @@ -1357,9 +1238,18 @@ Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUn module C = NCic module R = NCicReduction +module Ref = NReference module S = NCicSubstitution module U = NCicUtils +module E = NCicEnvironment +let rec split_prods ~subst context n te = + match (n, R.whd ~subst context te) with + | (0, _) -> context,te + | (n, C.Prod (name,so,ta)) when n > 0 -> + split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta + | (_, _) -> raise (AssertFailure (lazy "split_prods")) +;; let sort_of_prod ~subst context (name,s) (t1, t2) = let t1 = R.whd ~subst context t1 in @@ -1387,21 +1277,20 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty = | C.Prod (n,s,t) -> if R.are_convertible ~subst ~metasenv context ty_arg s then aux (S.subst ~avoid_beta_redexes:true arg t) tl - else + else raise (TypeCheckerFailure - (lazy (Printf.sprintf + (lazy (Printf.sprintf ("Appl: wrong parameter-type, expected %s, found %s") (NCicPp.ppterm ty_arg) (NCicPp.ppterm s)))) | _ -> raise (TypeCheckerFailure - (lazy "Appl: this is not a function, it cannot be applied"))) + (lazy "Appl: this is not a function, it cannot be applied"))) in aux ty_he args_with_ty ;; - let rec typeof ~subst ~metasenv context term = let rec typeof_aux context = function | C.Rel n -> @@ -1441,7 +1330,7 @@ let rec typeof ~subst ~metasenv context term = "the source %s should be a type; instead it is a term " ^^ "of type %s") (NCicPp.ppterm s) (NCicPp.ppterm sort))))); let ty = typeof_aux ((n,(C.Decl s))::context) t in - C.Prod (n,s,ty) + C.Prod (n,s,ty) | C.LetIn (n,ty,t,bo) -> let ty_t = typeof_aux context t in if not (R.are_convertible ~subst ~metasenv context ty ty_t) then @@ -1458,197 +1347,82 @@ let rec typeof ~subst ~metasenv context term = 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 | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2")) - | C.Match (r,outtype,term,pl) -> -assert false (* FINQUI + | C.Match (Ref.Ref (dummy_depth,uri,Ref.Ind tyno) as r,outtype,term,pl) -> let outsort = typeof_aux context outtype in - let (need_dummy, k) = - let rec guess_args context t = - let outtype = R.whd ~subst context t in - match outtype with - C.Sort _ -> (true, 0) - | C.Prod (name, s, t) -> - let (b, n) = - guess_args ((Some (name,(C.Decl s)))::context) t in - if n = 0 then - (* last prod before sort *) - match CicReduction.whd ~subst context s with -(*CSC: for _ see comment below about the missing named_exp_subst ?????????? *) - C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> - (false, 1) -(*CSC: for _ see comment below about the missing named_exp_subst ?????????? *) - | C.Appl ((C.MutInd (uri',i',_)) :: _) - when U.eq uri' uri && i' = i -> (false, 1) - | _ -> (true, 1) - else - (b, n + 1) - | _ -> - raise - (TypeCheckerFailure - (lazy (sprintf - "Malformed case analasys' output type %s" - (CicPp.ppterm outtype)))) - in -(* - let (parameters, arguments, exp_named_subst),ugraph2 = - let ty,ugraph2 = type_of_aux context term ugraph1 in - match R.whd ~subst context ty with - (*CSC manca il caso dei CAST *) -(*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *) -(*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *) -(*CSC: Hint: nella DTD servono per gli stylesheet. *) - C.MutInd (uri',i',exp_named_subst) as typ -> - if U.eq uri uri' && i = i' then - ([],[],exp_named_subst),ugraph2 - else - raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri) i))) - | C.Appl - ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> - if U.eq uri uri' && i = i' then - let params,args = - split tl (List.length tl - k) - in (params,args,exp_named_subst),ugraph2 - else - raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysys: analysed term type is %s, "^ - "but is expected to be (an application of) "^ - "%s#1/%d{_}") - (CicPp.ppterm typ') (U.string_of_uri uri) i))) - | _ -> - raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysis: "^ - "analysed term %s is not an inductive one") - (CicPp.ppterm term)))) -*) - let (b, k) = guess_args context outsort in - if not b then (b, k - 1) else (b, k) in - let (parameters, arguments, exp_named_subst),ugraph2 = - let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in - match R.whd ~subst context ty with - C.MutInd (uri',i',exp_named_subst) as typ -> - if U.eq uri uri' && i = i' then - ([],[],exp_named_subst),ugraph2 - else raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))) - | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) -> - if U.eq uri uri' && i = i' then - let params,args = - split tl (List.length tl - k) - in (params,args,exp_named_subst),ugraph2 - else raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))) + let leftno = E.get_indty_leftno r in + let parameters, arguments = + let ty = R.whd ~subst context (typeof_aux context term) in + let r',tl = + match ty with + C.Const (Ref.Ref (_,_,Ref.Ind _) as r') -> r',[] + | C.Appl (C.Const (Ref.Ref (_,_,Ref.Ind _) as r') :: tl) -> r',tl | _ -> - raise - (TypeCheckerFailure - (lazy (sprintf - "Case analysis: analysed term %s is not an inductive one" - (CicPp.ppterm term)))) - in - (* - let's control if the sort elimination is allowed: - [(I q1 ... qr)|B] - *) - let sort_of_ind_type = - if parameters = [] then - C.MutInd (uri,i,exp_named_subst) + raise + (TypeCheckerFailure (lazy (Printf.sprintf + "Case analysis: analysed term %s is not an inductive one" + (NCicPp.ppterm 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'))))) else - C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters) - in - let type_of_sort_of_ind_ty,ugraph3 = - type_of_aux ~logger context sort_of_ind_type ugraph2 in - let b,ugraph4 = - check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i - need_dummy sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3 - in - if not b then - raise - (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed"))); - (* let's check if the type of branches are right *) - let parsno,constructorsno = - let obj,_ = - try - CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri - with Not_found -> assert false - in - match obj with - C.InductiveDefinition (il,_,parsno,_) -> - let _,_,_,cl = - try List.nth il i with Failure _ -> assert false - in - parsno, List.length cl - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) + try HExtlib.split_nth leftno tl + with + Failure _ -> + raise (TypeCheckerFailure (lazy (Printf.sprintf + "%s is partially applied" (NCicPp.ppterm 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"))); + (* 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 case analysis"))) ; - let (_,branches_ok,ugraph5) = + raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match"))); + let j,branches_ok = List.fold_left - (fun (j,b,ugraph) p -> - if b then - let cons = - if parameters = [] then - (C.MutConstruct (uri,i,j,exp_named_subst)) - else - (C.Appl - (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) + (fun (j,b) p -> + if b then + let cons = + let cons = Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)) in + if parameters = [] then C.Const cons + else C.Appl (C.Const cons::parameters) in - let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in - let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in - (* 2 is skipped *) - let ty_branch = - type_of_branch ~subst context parsno need_dummy outtype cons - ty_cons in - let b1,ugraph4 = - R.are_convertible - ~subst ~metasenv context ty_p ty_branch ugraph3 - in -(* Debugging code -if not b1 then -begin -prerr_endline ("\n!OUTTYPE= " ^ CicPp.ppterm outtype); -prerr_endline ("!CONS= " ^ CicPp.ppterm cons); -prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons); -prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch); -end; -*) - if not b1 then - debug_print (lazy - ("#### " ^ CicPp.ppterm ty_p ^ - " <==> " ^ CicPp.ppterm ty_branch)); - (j + 1,b1,ugraph4) - else - (j,false,ugraph) - ) (1,true,ugraph4) pl + 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 in + j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch + else + j,false + ) (1,true) pl in if not branches_ok then raise - (TypeCheckerFailure (lazy "Case analysys: wrong branch type")); - let arguments' = - if not need_dummy then outtype::arguments@[term] - else outtype::arguments in - let outtype = - if need_dummy && arguments = [] then outtype - else CicReduction.head_beta_reduce (C.Appl arguments') - in - outtype,ugraph5 - *) + (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) + | C.Match _ -> assert false + + and type_of_branch ~subst context leftno outty cons tycons = assert false + (* 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 = match l with | shift, NCic.Irl n -> @@ -1670,16 +1444,16 @@ end; | (_,C.Def (_,t1)), (_,C.Decl t2) -> if not (R.are_convertible ~subst ~metasenv tl t1 t2) then raise - (TypeCheckerFailure - (lazy (Printf.sprintf + (TypeCheckerFailure + (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) ))) | _,_ -> 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))))); @@ -1722,25 +1496,70 @@ end; if not (R.are_convertible ~subst ~metasenv context optimized_t ct) then raise - (TypeCheckerFailure - (lazy (Printf.sprintf + (TypeCheckerFailure + (lazy (Printf.sprintf ("Not well typed metavariable local context: " ^^ "expected a term convertible with %s, found %s") (NCicPp.ppterm ct) (NCicPp.ppterm 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 + if not (R.are_convertible ~subst ~metasenv context type_t ct) then raise (TypeCheckerFailure - (lazy (Printf.sprintf + (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 ct) (NCicPp.ppterm t) (NCicPp.ppterm 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)))) + + and is_non_informative context paramsno c = + let rec aux context c = + match R.whd context c with + | C.Prod (n,so,de) -> + let s = typeof_aux context so in + s = C.Sort C.Prop && aux ((n,(C.Decl so))::context) de + | _ -> true in + let context',dx = split_prods ~subst:[] context paramsno c in + aux context' dx + + and check_allowed_sort_elimination ~subst ~metasenv r = + let mkapp he arg = + match he with + | C.Appl l -> C.Appl (l @ [arg]) + | t -> C.Appl [t;arg] in + let rec aux context ind arity1 arity2 = + let arity1 = R.whd ~subst context arity1 in + 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 + | 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 + in + aux + in typeof_aux context term @@ -1751,43 +1570,43 @@ and type_of_constant ref = assert false (* USARE typecheck_obj0 *) match CicEnvironment.is_type_checked ~trust:true ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj uobj -> - logger#log (`Start_type_checking uri) ; + 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 + 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 in CASO COSTRUTTORE match cobj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,arity,_) = List.nth dl i in - arity,ugraph1 + C.InductiveDefinition (dl,_,_,_) -> + let (_,_,arity,_) = List.nth dl i in + arity,ugraph1 | _ -> - raise (TypeCheckerFailure + 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 + C.InductiveDefinition (dl,_,_,_) -> + let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty,ugraph1 | _ -> - raise (TypeCheckerFailure + raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) *) @@ -1840,88 +1659,88 @@ and typecheck_obj0 = function let _,ugraph1 = type_of_aux ~logger context ty ugraph in (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, k::kl,ugraph1,len+1) - ) ([],[],ugraph,0) fl + ) ([],[],ugraph,0) fl in let ugraph2 = - List.fold_left + List.fold_left (fun ugraph (name,x,ty,bo) -> - let ty_bo,ugraph1 = - type_of_aux ~logger (types@context) bo ugraph - in - let b,ugraph2 = - R.are_convertible ~subst ~metasenv (types@context) - ty_bo (CicSubstitution.lift len ty) ugraph1 in - if b then - begin - let (m, eaten, context') = - eat_lambdas ~subst (types @ context) (x + 1) bo - in - (* - let's control the guarded by - destructors conditions D{f,k,x,M} - *) - if not (guarded_by_destructors ~subst context' eaten - (len + eaten) kl 1 [] m) then - raise - (TypeCheckerFailure - (lazy ("Fix: not guarded by destructors"))) - else - ugraph2 - end + let ty_bo,ugraph1 = + type_of_aux ~logger (types@context) bo ugraph + in + let b,ugraph2 = + R.are_convertible ~subst ~metasenv (types@context) + ty_bo (CicSubstitution.lift len ty) ugraph1 in + if b then + begin + let (m, eaten, context') = + eat_lambdas ~subst (types @ context) (x + 1) bo + in + (* + let's control the guarded by + destructors conditions D{f,k,x,M} + *) + if not (guarded_by_destructors ~subst context' eaten + (len + eaten) kl 1 [] m) then + raise + (TypeCheckerFailure + (lazy ("Fix: not guarded by destructors"))) + else + ugraph2 + end else - raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies"))) + raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies"))) ) ugraph1 fl in - (*CSC: controlli mancanti solo su D{f,k,x,M} *) + (*CSC: controlli mancanti solo su D{f,k,x,M} *) let (_,_,ty,_) = List.nth fl i in - ty,ugraph2 + ty,ugraph2 | C.CoFix (i,fl) -> let types,ugraph1,len = - List.fold_left - (fun (l,ugraph,len) (n,ty,_) -> + List.fold_left + (fun (l,ugraph,len) (n,ty,_) -> let _,ugraph1 = - type_of_aux ~logger context ty ugraph in - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l, + type_of_aux ~logger context ty ugraph in + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l, ugraph1,len+1) - ) ([],ugraph,0) fl + ) ([],ugraph,0) fl in let ugraph2 = - List.fold_left + List.fold_left (fun ugraph (_,ty,bo) -> - let ty_bo,ugraph1 = - type_of_aux ~logger (types @ context) bo ugraph - in - let b,ugraph2 = - R.are_convertible ~subst ~metasenv (types @ context) ty_bo - (CicSubstitution.lift len ty) ugraph1 - in - if b then - begin - (* let's control that the returned type is coinductive *) - match returns_a_coinductive ~subst context ty with - None -> - raise - (TypeCheckerFailure - (lazy "CoFix: does not return a coinductive type")) - | Some uri -> - (* - let's control the guarded by constructors - conditions C{f,M} - *) - if not (guarded_by_constructors ~subst + let ty_bo,ugraph1 = + type_of_aux ~logger (types @ context) bo ugraph + in + let b,ugraph2 = + R.are_convertible ~subst ~metasenv (types @ context) ty_bo + (CicSubstitution.lift len ty) ugraph1 + in + if b then + begin + (* let's control that the returned type is coinductive *) + match returns_a_coinductive ~subst context ty with + None -> + raise + (TypeCheckerFailure + (lazy "CoFix: does not return a coinductive type")) + | Some uri -> + (* + let's control the guarded by constructors + conditions C{f,M} + *) + if not (guarded_by_constructors ~subst (types @ context) 0 len false bo [] uri) then - raise - (TypeCheckerFailure - (lazy "CoFix: not guarded by constructors")) - else - ugraph2 - end - else - raise - (TypeCheckerFailure (lazy "CoFix: ill-typed bodies")) + raise + (TypeCheckerFailure + (lazy "CoFix: not guarded by constructors")) + else + ugraph2 + end + else + raise + (TypeCheckerFailure (lazy "CoFix: ill-typed bodies")) ) ugraph1 fl in let (_,ty,_) = List.nth fl i in - ty,ugraph2 + ty,ugraph2 *) -- 2.39.2