summaryrefslogtreecommitdiff
path: root/pretyping/cbv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cbv.ml')
-rw-r--r--pretyping/cbv.ml80
1 files changed, 50 insertions, 30 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 08ec25be..21bbede0 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -1,19 +1,15 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Util
-open Pp
-open Term
open Names
-open Environ
-open Univ
-open Evd
-open Conv_oracle
+open Term
+open Vars
open Closure
open Esubst
@@ -46,10 +42,10 @@ type cbv_value =
| VAL of int * constr
| STACK of int * cbv_value * cbv_stack
| CBN of constr * cbv_value subs
- | LAM of int * (name * constr) list * constr * cbv_value subs
+ | LAM of int * (Name.t * constr) list * constr * cbv_value subs
| FIXP of fixpoint * cbv_value subs * cbv_value array
| COFIXP of cofixpoint * cbv_value subs * cbv_value array
- | CONSTR of constructor * cbv_value array
+ | CONSTR of constructor puniverses * cbv_value array
(* type of terms with a hole. This hole can appear only under App or Case.
* TOP means the term is considered without context
@@ -63,6 +59,8 @@ type cbv_value =
* the subs S, pat is information on the patterns of the Case
* (Weak reduction: we propagate the sub only when the selected branch
* is determined)
+ * PROJ(p,pb,stk) means the term is in a primitive projection p, itself in stk.
+ * pb is the associated projection body
*
* Important remark: the APPs should be collapsed:
* (APP (l,(APP ...))) forbidden
@@ -71,6 +69,7 @@ and cbv_stack =
| TOP
| APP of cbv_value array * cbv_stack
| CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
+ | PROJ of projection * Declarations.projection_body * cbv_stack
(* les vars pourraient etre des constr,
cela permet de retarder les lift: utile ?? *)
@@ -90,7 +89,7 @@ let rec shift_value n = function
| CONSTR (c,args) ->
CONSTR (c, Array.map (shift_value n) args)
let shift_value n v =
- if n = 0 then v else shift_value n v
+ if Int.equal n 0 then v else shift_value n v
(* Contracts a fixpoint: given a fixpoint and a bindings,
* returns the corresponding fixpoint body, and the bindings in which
@@ -111,11 +110,11 @@ let contract_cofixp env (i,(_,_,bds as bodies)) =
let make_constr_ref n = function
| RelKey p -> mkRel (n+p)
| VarKey id -> mkVar id
- | ConstKey cst -> mkConst cst
+ | ConstKey cst -> mkConstU cst
(* Adds an application list. Collapse APPs! *)
let stack_app appl stack =
- if Array.length appl = 0 then stack else
+ if Int.equal (Array.length appl) 0 then stack else
match stack with
| APP(args,stk) -> APP(Array.append appl args,stk)
| _ -> APP(appl, stack)
@@ -125,6 +124,7 @@ let rec stack_concat stk1 stk2 =
TOP -> stk2
| APP(v,stk1') -> APP(v,stack_concat stk1' stk2)
| CASE(c,b,i,s,stk1') -> CASE(c,b,i,s,stack_concat stk1' stk2)
+ | PROJ (p,pinfo,stk1') -> PROJ (p,pinfo,stack_concat stk1' stk2)
(* merge stacks when there is no shifts in between *)
let mkSTACK = function
@@ -140,7 +140,7 @@ open RedFlags
let red_set_ref flags = function
| RelKey _ -> red_set flags fDELTA
| VarKey id -> red_set flags (fVAR id)
- | ConstKey sp -> red_set flags (fCONST sp)
+ | ConstKey (sp,_) -> red_set flags (fCONST sp)
(* Transfer application lists from a value to the stack
* useful because fixpoints may be totally applied in several times.
@@ -178,9 +178,9 @@ let cofixp_reducible flgs _ stk =
(* The main recursive functions
*
- * Go under applications and cases (pushed in the stack), expand head
- * constants or substitued de Bruijn, and try to make appear a
- * constructor, a lambda or a fixp in the head. If not, it is a value
+ * Go under applications and cases/projections (pushed in the stack),
+ * expand head constants or substitued de Bruijn, and try to a make a
+ * constructor, a lambda or a fixp appear in the head. If not, it is a value
* and is completely computed here. The head redexes are NOT reduced:
* the function returns the pair of a cbv_value and its stack. *
* Invariant: if the result of norm_head is CONSTR or (CO)FIXP, it last
@@ -197,7 +197,17 @@ let rec norm_head info env t stack =
norm_head info env head (stack_app nargs stack)
| Case (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
| Cast (ct,_,_) -> norm_head info env ct stack
-
+
+ | Proj (p, c) ->
+ let p' =
+ if red_set (info_flags info) (fCONST (Projection.constant p))
+ && red_set (info_flags info) fBETA
+ then Projection.unfold p
+ else p
+ in
+ let pinfo = Environ.lookup_projection p (info_env info) in
+ norm_head info env c (PROJ (p', pinfo, stack))
+
(* constants, axioms
* the first pattern is CRUCIAL, n=0 happens very often:
* when reducing closed terms, n is always 0 *)
@@ -222,10 +232,10 @@ let rec norm_head info env t stack =
let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in
norm_head info env' c stack
else
- (CBN(t,env), stack) (* Considérer une coupure commutative ? *)
+ (CBN(t,env), stack) (* Should we consider a commutative cut ? *)
| Evar ev ->
- (match evar_value info ev with
+ (match evar_value info.i_cache ev with
Some c -> norm_head info env c stack
| None -> (VAL(0, t), stack))
@@ -255,19 +265,21 @@ and norm_head_ref k info env stack normt =
* we build a value.
*)
and cbv_stack_term info stack env t =
- match norm_head info env t stack with
- (* a lambda meets an application -> BETA *)
- | (LAM (nlams,ctxt,b,env), APP (args, stk))
+ cbv_stack_value info env (norm_head info env t stack)
+
+and cbv_stack_value info env = function
+ (* a lambda meets an application -> BETA *)
+ | (LAM (nlams,ctxt,b,env), APP (args, stk))
when red_set (info_flags info) fBETA ->
- let nargs = Array.length args in
- if nargs == nlams then
+ let nargs = Array.length args in
+ if nargs == nlams then
cbv_stack_term info stk (subs_cons(args,env)) b
else if nlams < nargs then
let env' = subs_cons(Array.sub args 0 nlams, env) in
let eargs = Array.sub args nlams (nargs-nlams) in
cbv_stack_term info (APP(eargs,stk)) env' b
else
- let ctxt' = list_skipn nargs ctxt in
+ let ctxt' = List.skipn nargs ctxt in
LAM(nlams-nargs,ctxt', b, subs_cons(args,env))
(* a Fix applied enough -> IOTA *)
@@ -283,22 +295,28 @@ and cbv_stack_term info stack env t =
cbv_stack_term info stk envf redfix
(* constructor in a Case -> IOTA *)
- | (CONSTR((sp,n),[||]), APP(args,CASE(_,br,ci,env,stk)))
+ | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk)))
when red_set (info_flags info) fIOTA ->
let cargs =
Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
cbv_stack_term info (stack_app cargs stk) env br.(n-1)
(* constructor of arity 0 in a Case -> IOTA *)
- | (CONSTR((_,n),[||]), CASE(_,br,_,env,stk))
+ | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk))
when red_set (info_flags info) fIOTA ->
cbv_stack_term info stk env br.(n-1)
+ (* constructor in a Projection -> IOTA *)
+ | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk)))
+ when red_set (info_flags info) fIOTA && Projection.unfolded p ->
+ let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in
+ cbv_stack_value info env (arg, stk)
+
(* may be reduced later by application *)
| (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl)
| (COFIXP(cofix,env,[||]), APP(appl,TOP)) -> COFIXP(cofix,env,appl)
| (CONSTR(c,[||]), APP(appl,TOP)) -> CONSTR(c,appl)
-
+
(* definitely a value *)
| (head,stk) -> mkSTACK(head, stk)
@@ -316,6 +334,8 @@ let rec apply_stack info t = function
(mkCase (ci, cbv_norm_term info env ty, t,
Array.map (cbv_norm_term info env) br))
st
+ | PROJ (p, pinfo, st) ->
+ apply_stack info (mkProj (p, t)) st
(* performs the reduction on a constr, and returns a constr *)
and cbv_norm_term info env t =
@@ -333,7 +353,7 @@ and cbv_norm_value info = function (* reduction under binders *)
map_constr_with_binders subs_lift (cbv_norm_term info) env t
| LAM (n,ctxt,b,env) ->
let nctxt =
- list_map_i (fun i (x,ty) ->
+ List.map_i (fun i (x,ty) ->
(x,cbv_norm_term info (subs_liftn i env) ty)) 0 ctxt in
compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b)
| FIXP ((lij,(names,lty,bds)),env,args) ->
@@ -352,7 +372,7 @@ and cbv_norm_value info = function (* reduction under binders *)
(subs_liftn (Array.length lty) env)) bds)),
Array.map (cbv_norm_value info) args)
| CONSTR (c,args) ->
- mkApp(mkConstruct c, Array.map (cbv_norm_value info) args)
+ mkApp(mkConstructU c, Array.map (cbv_norm_value info) args)
(* with profiling *)
let cbv_norm infos constr =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 22:47:55 +0000