From 437ebce4198f3237df1f67d3037e9fa7b06789aa Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 22 Aug 2009 14:45:18 +0000 Subject: Transfers to checker ("let"s in inductive arities + Coq root read-only). - Support for let's in the signature of the arity of an inductive type was in the kernel part of commit 12273, - Support for binding Coq root read-only in -R option was in commit 12220. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12288 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/checker.ml | 7 ------- checker/declarations.ml | 4 ++++ checker/declarations.mli | 3 +++ checker/indtypes.ml | 7 ++++++- checker/inductive.ml | 16 ++++++++++------ checker/reduction.ml | 9 +++++++++ checker/reduction.mli | 3 +++ checker/term.ml | 2 +- 8 files changed, 36 insertions(+), 15 deletions(-) (limited to 'checker') diff --git a/checker/checker.ml b/checker/checker.ml index b982456aa..85ad129c9 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -90,23 +90,16 @@ let includes = ref [] let push_include (s, alias) = includes := (s,alias,false) :: !includes let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes -let check_coq_overwriting p = - if string_of_id (list_last (repr_dirpath p)) = "Coq" then - error "The \"Coq\" logical root directory is reserved for the Coq library" - let set_default_include d = push_include (d, Check.default_root_prefix) let set_default_rec_include d = let p = Check.default_root_prefix in - check_coq_overwriting p; push_rec_include (d, p) let set_include d p = let p = dirpath_of_string p in - check_coq_overwriting p; push_include (d,p) let set_rec_include d p = let p = dirpath_of_string p in - check_coq_overwriting p; push_rec_include(d,p) (* Initializes the LoadPath *) diff --git a/checker/declarations.ml b/checker/declarations.ml index 1ccdf8ea4..67f44c4d3 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -486,6 +486,9 @@ type one_inductive_body = { (* Number of expected real arguments of the type (no let, no params) *) mind_nrealargs : int; + (* Length of realargs context (with let, no params) *) + mind_nrealargs_ctxt : int; + (* List of allowed elimination sorts *) mind_kelim : sorts_family list; @@ -584,6 +587,7 @@ let subst_mind_packet sub mbp = mind_arity = subst_arity sub mbp.mind_arity; mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; + mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; mind_kelim = mbp.mind_kelim; mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); mind_nb_constant = mbp.mind_nb_constant; diff --git a/checker/declarations.mli b/checker/declarations.mli index b376151ca..c5b676bda 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -86,6 +86,9 @@ type one_inductive_body = { (* Number of expected real arguments of the type (no let, no params) *) mind_nrealargs : int; + (* Length of realargs context (with let, no params) *) + mind_nrealargs_ctxt : int; + (* List of allowed elimination sorts *) mind_kelim : sorts_family list; diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 4c9b3d61d..9ff21bc3f 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -136,6 +136,7 @@ let small_unit constrsinfos = (* check information related to inductive arity *) let typecheck_arity env params inds = let nparamargs = rel_context_nhyps params in + let nparamdecls = rel_context_length params in let check_arity arctxt = function Monomorphic mar -> let ar = mar.mind_user_arity in @@ -154,8 +155,12 @@ let typecheck_arity env params inds = (* Arities (with params) are typed-checked here *) let arity = check_arity ar_ctxt ind.mind_arity in (* mind_nrealargs *) - if ind.mind_nrealargs <> rel_context_nhyps ar_ctxt - nparamargs then + let nrealargs = rel_context_nhyps ar_ctxt - nparamargs in + if ind.mind_nrealargs <> nrealargs then failwith "bad number of real inductive arguments"; + let nrealargs_ctxt = rel_context_length ar_ctxt - nparamdecls in + if ind.mind_nrealargs_ctxt <> nrealargs_ctxt then + failwith "bad length of real inductive arguments signature"; (* We do not need to generate the universe of full_arity; if later, after the validation of the inductive definition, full_arity is used as argument or subject to cast, an diff --git a/checker/inductive.ml b/checker/inductive.ml index 05ab5a846..f1c8bea2a 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -253,16 +253,20 @@ let get_instantiated_arity (mib,mip) params = let elim_sorts (_,mip) = mip.mind_kelim -let rel_list n m = - let rec reln l p = - if p>m then l else reln (Rel(n+p)::l) (p+1) +let extended_rel_list n hyps = + let rec reln l p = function + | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps + | (_,Some _,_) :: hyps -> reln l (p+1) hyps + | [] -> l in - reln [] 1 + reln [] 1 hyps let build_dependent_inductive ind (_,mip) params = - let nrealargs = mip.mind_nrealargs in + let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in applist - (Ind ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs)) + (Ind ind, + List.map (lift mip.mind_nrealargs_ctxt) params + @ extended_rel_list 0 realargs) (* This exception is local *) exception LocalArity of (sorts_family * sorts_family * arity_error) option diff --git a/checker/reduction.ml b/checker/reduction.ml index c398f0a41..d81cfe352 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -107,6 +107,15 @@ let beta_appvect c v = | _ -> applist (substl env t, stack) in stacklam [] c (Array.to_list v) +let betazeta_appvect n c v = + let rec stacklam n env t stack = + if n = 0 then applist (substl env t, stack) else + match t, stack with + Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl + | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack + | _ -> anomaly "Not enough lambda/let's" in + stacklam n [] c (Array.to_list v) + (********************************************************************) (* Conversion *) (********************************************************************) diff --git a/checker/reduction.mli b/checker/reduction.mli index eb50ae32e..47590edb3 100644 --- a/checker/reduction.mli +++ b/checker/reduction.mli @@ -40,6 +40,9 @@ val vm_conv : conv_pb -> constr conversion_function (* Builds an application node, reducing beta redexes it may produce. *) val beta_appvect : constr -> constr array -> constr +(* Builds an application node, reducing the [n] first beta-zeta redexes. *) +val betazeta_appvect : int -> constr -> constr array -> constr + (* Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> constr -> constr list -> constr diff --git a/checker/term.ml b/checker/term.ml index f245d1551..f5b2496c8 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -28,7 +28,7 @@ type metavariable = int type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle type case_printing = - { ind_nargs : int; (* number of real args of the inductive type *) + { ind_nargs : int; (* length of the arity of the inductive type *) style : case_style } type case_info = { ci_ind : inductive; -- cgit v1.2.3