summaryrefslogtreecommitdiff
path: root/checker/closure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/closure.ml')
-rw-r--r--checker/closure.ml257
1 files changed, 19 insertions, 238 deletions
diff --git a/checker/closure.ml b/checker/closure.ml
index da25b3b3..033e2bd7 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: closure.ml 9983 2007-07-12 17:15:22Z barras $ *)
-
open Util
open Pp
open Term
@@ -54,6 +52,9 @@ type transparent_state = Idpred.t * Cpred.t
let all_opaque = (Idpred.empty, Cpred.empty)
let all_transparent = (Idpred.full, Cpred.full)
+let is_transparent_variable (ids, _) id = Idpred.mem id ids
+let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
+
module type RedFlagsSig = sig
type reds
type red_kind
@@ -65,11 +66,8 @@ module type RedFlagsSig = sig
val fVAR : identifier -> red_kind
val no_red : reds
val red_add : reds -> red_kind -> reds
- val red_sub : reds -> red_kind -> reds
- val red_add_transparent : reds -> transparent_state -> reds
val mkflags : red_kind list -> reds
val red_set : reds -> red_kind -> bool
- val red_get_const : reds -> bool * evaluable_global_reference list
end
module RedFlags = (struct
@@ -114,21 +112,6 @@ module RedFlags = (struct
let (l1,l2) = red.r_const in
{ red with r_const = Idpred.add id l1, l2 }
- let red_sub red = function
- | BETA -> { red with r_beta = false }
- | DELTA -> { red with r_delta = false }
- | CONST kn ->
- let (l1,l2) = red.r_const in
- { red with r_const = l1, Cpred.remove kn l2 }
- | IOTA -> { red with r_iota = false }
- | ZETA -> { red with r_zeta = false }
- | VAR id ->
- let (l1,l2) = red.r_const in
- { red with r_const = Idpred.remove id l1, l2 }
-
- let red_add_transparent red tr =
- { red with r_const = tr }
-
let mkflags = List.fold_left red_add no_red
let red_set red = function
@@ -146,160 +129,14 @@ module RedFlags = (struct
| DELTA -> (* Used for Rel/Var defined in context *)
incr_cnt red.r_delta delta
- let red_get_const red =
- let p1,p2 = red.r_const in
- let (b1,l1) = Idpred.elements p1 in
- let (b2,l2) = Cpred.elements p2 in
- if b1=b2 then
- let l1' = List.map (fun x -> EvalVarRef x) l1 in
- let l2' = List.map (fun x -> EvalConstRef x) l2 in
- (b1, l1' @ l2')
- else error "unrepresentable pair of predicate"
-
end : RedFlagsSig)
open RedFlags
let betadeltaiota = mkflags [fBETA;fDELTA;fZETA;fIOTA]
let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA]
-let betaiota = mkflags [fBETA;fIOTA]
-let beta = mkflags [fBETA]
let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
-let unfold_red kn =
- let flag = match kn with
- | EvalVarRef id -> fVAR id
- | EvalConstRef kn -> fCONST kn
- in (* Remove fZETA for finer behaviour ? *)
- mkflags [fBETA;flag;fIOTA;fZETA]
-
-(************************* Obsolète
-(* [r_const=(true,cl)] means all constants but those in [cl] *)
-(* [r_const=(false,cl)] means only those in [cl] *)
-type reds = {
- r_beta : bool;
- r_const : bool * constant_path list * identifier list;
- r_zeta : bool;
- r_evar : bool;
- r_iota : bool }
-
-let betadeltaiota_red = {
- r_beta = true;
- r_const = true,[],[];
- r_zeta = true;
- r_evar = true;
- r_iota = true }
-
-let betaiota_red = {
- r_beta = true;
- r_const = false,[],[];
- r_zeta = false;
- r_evar = false;
- r_iota = true }
-
-let beta_red = {
- r_beta = true;
- r_const = false,[],[];
- r_zeta = false;
- r_evar = false;
- r_iota = false }
-
-let no_red = {
- r_beta = false;
- r_const = false,[],[];
- r_zeta = false;
- r_evar = false;
- r_iota = false }
-
-let betaiotazeta_red = {
- r_beta = true;
- r_const = false,[],[];
- r_zeta = true;
- r_evar = false;
- r_iota = true }
-
-let unfold_red kn =
- let c = match kn with
- | EvalVarRef id -> false,[],[id]
- | EvalConstRef kn -> false,[kn],[]
- in {
- r_beta = true;
- r_const = c;
- r_zeta = true; (* false for finer behaviour ? *)
- r_evar = false;
- r_iota = true }
-
-(* Sets of reduction kinds.
- Main rule: delta implies all consts (both global (= by
- kernel_name) and local (= by Rel or Var)), all evars, and zeta (= letin's).
- Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
- a LetIn expression is Letin reduction *)
-
-type red_kind =
- BETA | DELTA | ZETA | IOTA
- | CONST of constant_path list | CONSTBUT of constant_path list
- | VAR of identifier | VARBUT of identifier
-
-let rec red_add red = function
- | BETA -> { red with r_beta = true }
- | DELTA ->
- (match red.r_const with
- | _,_::_,[] | _,[],_::_ -> error "Conflict in the reduction flags"
- | _ -> { red with r_const = true,[],[]; r_zeta = true; r_evar = true })
- | CONST cl ->
- (match red.r_const with
- | true,_,_ -> error "Conflict in the reduction flags"
- | _,l1,l2 -> { red with r_const = false, list_union cl l1, l2 })
- | CONSTBUT cl ->
- (match red.r_const with
- | false,_::_,_ | false,_,_::_ ->
- error "Conflict in the reduction flags"
- | _,l1,l2 ->
- { red with r_const = true, list_union cl l1, l2;
- r_zeta = true; r_evar = true })
- | IOTA -> { red with r_iota = true }
- | ZETA -> { red with r_zeta = true }
- | VAR id ->
- (match red.r_const with
- | true,_,_ -> error "Conflict in the reduction flags"
- | _,l1,l2 -> { red with r_const = false, l1, list_union [id] l2 })
- | VARBUT cl ->
- (match red.r_const with
- | false,_::_,_ | false,_,_::_ ->
- error "Conflict in the reduction flags"
- | _,l1,l2 ->
- { red with r_const = true, l1, list_union [cl] l2;
- r_zeta = true; r_evar = true })
-
-let red_delta_set red =
- let b,_,_ = red.r_const in b
-
-let red_local_const = red_delta_set
-
-(* to know if a redex is allowed, only a subset of red_kind is used ... *)
-let red_set red = function
- | BETA -> incr_cnt red.r_beta beta
- | CONST [kn] ->
- let (b,l,_) = red.r_const in
- let c = List.mem kn l in
- incr_cnt ((b & not c) or (c & not b)) delta
- | VAR id -> (* En attendant d'avoir des kn pour les Var *)
- let (b,_,l) = red.r_const in
- let c = List.mem id l in
- incr_cnt ((b & not c) or (c & not b)) delta
- | ZETA -> incr_cnt red.r_zeta zeta
- | EVAR -> incr_cnt red.r_zeta evar
- | IOTA -> incr_cnt red.r_iota iota
- | DELTA -> red_delta_set red (*Used for Rel/Var defined in context*)
- (* Not for internal use *)
- | CONST _ | CONSTBUT _ | VAR _ | VARBUT _ -> failwith "not implemented"
-
-(* Gives the constant list *)
-let red_get_const red =
- let b,l1,l2 = red.r_const in
- let l1' = List.map (fun x -> EvalConstRef x) l1 in
- let l2' = List.map (fun x -> EvalVarRef x) l2 in
- b, l1' @ l2'
-fin obsolète **************)
+
(* specification of the reduction function *)
@@ -336,8 +173,6 @@ type 'a infos = {
i_vars : (identifier * constr) list;
i_tab : (table_key, 'a) Hashtbl.t }
-let info_flags info = info.i_flags
-
let ref_value_cache info ref =
try
Some (Hashtbl.find info.i_tab ref)
@@ -447,9 +282,6 @@ and fterm =
let fterm_of v = v.term
let set_norm v = v.norm <- Norm
-let is_val v = v.norm = Norm
-
-let mk_atom c = {norm=Norm;term=FAtom c}
(* Could issue a warning if no is still Red, pointing out that we loose
sharing. *)
@@ -472,7 +304,6 @@ type stack_member =
and stack = stack_member list
-let empty_stack = []
let append_stack v s =
if Array.length v = 0 then s else
match s with
@@ -486,52 +317,6 @@ let zshift n s =
| (_,Zshift(k)::s) -> Zshift(n+k)::s
| _ -> Zshift(n)::s
-let rec stack_args_size = function
- | Zapp v :: s -> Array.length v + stack_args_size s
- | Zshift(_)::s -> stack_args_size s
- | Zupdate(_)::s -> stack_args_size s
- | _ -> 0
-
-(* When used as an argument stack (only Zapp can appear) *)
-let rec decomp_stack = function
- | Zapp v :: s ->
- (match Array.length v with
- 0 -> decomp_stack s
- | 1 -> Some (v.(0), s)
- | _ ->
- Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s)))
- | _ -> None
-let array_of_stack s =
- let rec stackrec = function
- | [] -> []
- | Zapp args :: s -> args :: (stackrec s)
- | _ -> assert false
- in Array.concat (stackrec s)
-let rec stack_assign s p c = match s with
- | Zapp args :: s ->
- let q = Array.length args in
- if p >= q then
- Zapp args :: stack_assign s (p-q) c
- else
- (let nargs = Array.copy args in
- nargs.(p) <- c;
- Zapp nargs :: s)
- | _ -> s
-let rec stack_tail p s =
- if p = 0 then s else
- match s with
- | Zapp args :: s ->
- let q = Array.length args in
- if p >= q then stack_tail (p-q) s
- else Zapp (Array.sub args p (q-p)) :: s
- | _ -> failwith "stack_tail"
-let rec stack_nth s p = match s with
- | Zapp args :: s ->
- let q = Array.length args in
- if p >= q then stack_nth s (p-q)
- else args.(p)
- | _ -> raise Not_found
-
(* Lifting. Preserves sharing (useful only for cell with norm=Red).
lft_fconstr always create a new cell, while lift_fconstr avoids it
when the lift is 0. *)
@@ -643,7 +428,7 @@ let optimise_closure env c =
let (c',(_,s)) = compact_constr (0,[]) c 1 in
let env' =
Array.map (fun i -> clos_rel env i) (Array.of_list s) in
- (subs_cons (env', ESID 0),c')
+ (subs_cons (env', subs_id 0),c')
let mk_lambda env t =
let (env,t) = optimise_closure env t in
@@ -774,7 +559,7 @@ let term_of_fconstr =
| FFix(fx,e) when is_subs_id e & is_lift_id lfts -> Fix fx
| FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> CoFix cfx
| _ -> to_constr term_of_fconstr_lift lfts v in
- term_of_fconstr_lift ELID
+ term_of_fconstr_lift el_id
@@ -809,16 +594,6 @@ let fapp_stack (m,stk) = zip m stk
(strip_update_shift, through get_arg). *)
(* optimised for the case where there are no shifts... *)
-let strip_update_shift head stk =
- assert (head.norm <> Red);
- let rec strip_rec h depth = function
- | Zshift(k)::s -> strip_rec (lift_fconstr k h) (depth+k) s
- | Zupdate(m)::s ->
- strip_rec (update m (h.norm,h.term)) depth s
- | stk -> (depth,stk) in
- strip_rec head 0 stk
-
-(* optimised for the case where there are no shifts... *)
let strip_update_shift_app head stk =
assert (head.norm <> Red);
let rec strip_rec rstk h depth = function
@@ -835,15 +610,15 @@ let strip_update_shift_app head stk =
let get_nth_arg head n stk =
assert (head.norm <> Red);
- let rec strip_rec rstk h depth n = function
+ let rec strip_rec rstk h n = function
| Zshift(k) as e :: s ->
- strip_rec (e::rstk) (lift_fconstr k h) (depth+k) n s
+ strip_rec (e::rstk) (lift_fconstr k h) n s
| Zapp args::s' ->
let q = Array.length args in
if n >= q
then
strip_rec (Zapp args::rstk)
- {norm=h.norm;term=FApp(h,args)} depth (n-q) s'
+ {norm=h.norm;term=FApp(h,args)} (n-q) s'
else
let bef = Array.sub args 0 n in
let aft = Array.sub args (n+1) (q-n-1) in
@@ -851,9 +626,9 @@ let get_nth_arg head n stk =
List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in
(Some (stk', args.(n)), append_stack aft s')
| Zupdate(m)::s ->
- strip_rec rstk (update m (h.norm,h.term)) depth n s
+ strip_rec rstk (update m (h.norm,h.term)) n s
| s -> (None, List.rev rstk @ s) in
- strip_rec [] head 0 n stk
+ strip_rec [] head n stk
(* Beta reduction: look for an applied argument in the stack.
Since the encountered update marks are removed, h must be a whnf *)
@@ -876,6 +651,12 @@ let rec get_args n tys f e stk =
get_args (n-na) etys f (subs_cons(l,e)) s
| _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
+(* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
+let rec eta_expand_stack = function
+ | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ as e) :: s ->
+ e :: eta_expand_stack s
+ | [] ->
+ [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]]
(* Iota reduction: extract the arguments to be passed to the Case
branches *)
@@ -1025,7 +806,7 @@ let kh info v stk = fapp_stack(kni info v stk)
let whd_val info v =
with_stats (lazy (term_of_fconstr (kh info v [])))
-let inject = mk_clos (ESID 0)
+let inject = mk_clos (subs_id 0)
let whd_stack infos m stk =
let k = kni infos m stk in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 05:07:45 +0000