aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-08-22 14:45:18 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-08-22 14:45:18 +0000
commit437ebce4198f3237df1f67d3037e9fa7b06789aa (patch)
treeb1f01277adb40c47cdb2cc04b7c0b44628936569 /checker
parent85046457054d78ee657fc4366ca014e453b6908b (diff)
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
Diffstat (limited to 'checker')
-rw-r--r--checker/checker.ml7
-rw-r--r--checker/declarations.ml4
-rw-r--r--checker/declarations.mli3
-rw-r--r--checker/indtypes.ml7
-rw-r--r--checker/inductive.ml16
-rw-r--r--checker/reduction.ml9
-rw-r--r--checker/reduction.mli3
-rw-r--r--checker/term.ml2
8 files changed, 36 insertions, 15 deletions
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;