summaryrefslogtreecommitdiff
path: root/kernel/closure.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /kernel/closure.ml
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'kernel/closure.ml')
-rw-r--r--kernel/closure.ml95
1 files changed, 43 insertions, 52 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 1a635ccf..8e16a922 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: closure.ml,v 1.54.2.1 2004/07/16 19:30:23 herbelin Exp $ *)
+(* $Id: closure.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
open Util
open Pp
@@ -16,7 +16,6 @@ open Declarations
open Environ
open Esubst
-
let stats = ref false
let share = ref true
@@ -52,10 +51,8 @@ let with_stats c =
end else
Lazy.force c
-type transparent_state = Idpred.t * KNpred.t
-
-let all_opaque = (Idpred.empty, KNpred.empty)
-let all_transparent = (Idpred.full, KNpred.full)
+let all_opaque = (Idpred.empty, Cpred.empty)
+let all_transparent = (Idpred.full, Cpred.full)
module type RedFlagsSig = sig
type reds
@@ -110,7 +107,7 @@ module RedFlags = (struct
| DELTA -> { red with r_delta = true; r_const = all_transparent }
| CONST kn ->
let (l1,l2) = red.r_const in
- { red with r_const = l1, KNpred.add kn l2 }
+ { red with r_const = l1, Cpred.add kn l2 }
| IOTA -> { red with r_iota = true }
| ZETA -> { red with r_zeta = true }
| VAR id ->
@@ -122,7 +119,7 @@ module RedFlags = (struct
| DELTA -> { red with r_delta = false }
| CONST kn ->
let (l1,l2) = red.r_const in
- { red with r_const = l1, KNpred.remove kn l2 }
+ { red with r_const = l1, Cpred.remove kn l2 }
| IOTA -> { red with r_iota = false }
| ZETA -> { red with r_zeta = false }
| VAR id ->
@@ -138,7 +135,7 @@ module RedFlags = (struct
| BETA -> incr_cnt red.r_beta beta
| CONST kn ->
let (_,l) = red.r_const in
- let c = KNpred.mem kn l in
+ let c = Cpred.mem kn l in
incr_cnt c delta
| VAR id -> (* En attendant d'avoir des kn pour les Var *)
let (l,_) = red.r_const in
@@ -152,7 +149,7 @@ module RedFlags = (struct
let red_get_const red =
let p1,p2 = red.r_const in
let (b1,l1) = Idpred.elements p1 in
- let (b2,l2) = KNpred.elements p2 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
@@ -326,11 +323,7 @@ fin obsolète **************)
* instantiations (cbv or lazy) are.
*)
-type table_key =
- | ConstKey of constant
- | VarKey of identifier
- | FarRelKey of int
- (* FarRel: index in the rel_context part of _initial_ environment *)
+type table_key = id_key
type 'a infos = {
i_flags : reds;
@@ -349,7 +342,7 @@ let ref_value_cache info ref =
try
let body =
match ref with
- | FarRelKey n ->
+ | RelKey n ->
let (s,l) = info.i_rels in lift n (List.assoc (s-n) l)
| VarKey id -> List.assoc id info.i_vars
| ConstKey cst -> constant_value info.i_env cst
@@ -364,22 +357,22 @@ let ref_value_cache info ref =
let defined_vars flags env =
(* if red_local_const (snd flags) then*)
- fold_named_context
- (fun env (id,b,t) e ->
+ Sign.fold_named_context
+ (fun (id,b,_) e ->
match b with
| None -> e
| Some body -> (id, body)::e)
- env ~init:[]
+ (named_context env) ~init:[]
(* else []*)
let defined_rels flags env =
(* if red_local_const (snd flags) then*)
- fold_rel_context
- (fun env (id,b,t) (i,subs) ->
+ Sign.fold_rel_context
+ (fun (id,b,t) (i,subs) ->
match b with
| None -> (i+1, subs)
| Some body -> (i+1, (i,body) :: subs))
- env ~init:(0,[])
+ (rel_context env) ~init:(0,[])
(* else (0,[])*)
@@ -519,7 +512,7 @@ type fconstr = {
and fterm =
| FRel of int
| FAtom of constr (* Metas and Sorts *)
- | FCast of fconstr * fconstr
+ | FCast of fconstr * cast_kind * fconstr
| FFlex of table_key
| FInd of inductive
| FConstruct of constructor
@@ -539,6 +532,8 @@ 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. *)
let update v1 (no,t) =
@@ -553,7 +548,7 @@ let update v1 (no,t) =
when the lift is 0. *)
let rec lft_fconstr n ft =
match ft.term with
- | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FAtom _) -> ft
+ | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)) -> ft
| FRel i -> {norm=Norm;term=FRel(i+n)}
| FLambda(k,tys,f,e) -> {norm=Cstr; term=FLambda(k,tys,f,subs_shft(n,e))}
| FFix(fx,e) -> {norm=Cstr; term=FFix(fx,subs_shft(n,e))}
@@ -573,7 +568,7 @@ let clos_rel e i =
| Inl(n,mt) -> lift_fconstr n mt
| Inr(k,None) -> {norm=Norm; term= FRel k}
| Inr(k,Some p) ->
- lift_fconstr (k-p) {norm=Norm;term=FFlex(FarRelKey p)}
+ lift_fconstr (k-p) {norm=Norm;term=FFlex(RelKey p)}
(* since the head may be reducible, we might introduce lifts of 0 *)
let compact_stack head stk =
@@ -608,10 +603,10 @@ let rec compact_constr (lg, subs as s) c k =
| Evar(ev,v) ->
let (v',s) = compact_vect s v k in
if v==v' then c,s else mkEvar(ev,v'),s
- | Cast(a,b) ->
+ | Cast(a,ck,b) ->
let (a',s) = compact_constr s a k in
let (b',s) = compact_constr s b k in
- if a==a' && b==b' then c,s else mkCast(a',b'), s
+ if a==a' && b==b' then c,s else mkCast(a', ck, b'), s
| App(f,v) ->
let (f',s) = compact_constr s f k in
let (v',s) = compact_vect s v k in
@@ -664,7 +659,7 @@ let optimise_closure env c =
(env',c')
let mk_lambda env t =
-(* let (env,t) = optimise_closure env t in*)
+ let (env,t) = optimise_closure env t in
let (rvars,t') = decompose_lam t in
FLambda(List.length rvars, List.rev rvars, t', env)
@@ -698,9 +693,9 @@ let mk_clos_deep clos_fun env t =
match kind_of_term t with
| (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) ->
mk_clos env t
- | Cast (a,b) ->
+ | Cast (a,k,b) ->
{ norm = Red;
- term = FCast (clos_fun env a, clos_fun env b)}
+ term = FCast (clos_fun env a, k, clos_fun env b)}
| App (f,v) ->
{ norm = Red;
term = FApp (clos_fun env f, Array.map (clos_fun env) v) }
@@ -730,15 +725,11 @@ let mk_clos2 = mk_clos_deep mk_clos
let rec to_constr constr_fun lfts v =
match v.term with
| FRel i -> mkRel (reloc_rel i lfts)
- | FFlex (FarRelKey p) -> mkRel (reloc_rel p lfts)
+ | FFlex (RelKey p) -> mkRel (reloc_rel p lfts)
| FFlex (VarKey x) -> mkVar x
- | FAtom c ->
- (match kind_of_term c with
- | Sort s -> mkSort s
- | Meta m -> mkMeta m
- | _ -> assert false)
- | FCast (a,b) ->
- mkCast (constr_fun lfts a, constr_fun lfts b)
+ | FAtom c -> exliftn lfts c
+ | FCast (a,k,b) ->
+ mkCast (constr_fun lfts a, k, constr_fun lfts b)
| FFlex (ConstKey op) -> mkConst op
| FInd op -> mkInd op
| FConstruct op -> mkConstruct op
@@ -808,23 +799,23 @@ let rec fstrong unfreeze_fun lfts v =
to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v)
*)
-let rec zip zfun m stk =
+let rec zip m stk =
match stk with
| [] -> m
| Zapp args :: s ->
let args = Array.of_list args in
- zip zfun {norm=neutr m.norm; term=FApp(m, Array.map zfun args)} s
+ zip {norm=neutr m.norm; term=FApp(m, args)} s
| Zcase(ci,p,br)::s ->
- let t = FCases(ci, zfun p, m, Array.map zfun br) in
- zip zfun {norm=neutr m.norm; term=t} s
+ let t = FCases(ci, p, m, br) in
+ zip {norm=neutr m.norm; term=t} s
| Zfix(fx,par)::s ->
- zip zfun fx (par @ append_stack_list ([m], s))
+ zip fx (par @ append_stack_list ([m], s))
| Zshift(n)::s ->
- zip zfun (lift_fconstr n m) s
+ zip (lift_fconstr n m) s
| Zupdate(rf)::s ->
- zip zfun (update rf (m.norm,m.term)) s
+ zip (update rf (m.norm,m.term)) s
-let fapp_stack (m,stk) = zip (fun x -> x) m stk
+let fapp_stack (m,stk) = zip m stk
(*********************************************************************)
@@ -849,7 +840,7 @@ let strip_update_shift_app head stk =
let rec strip_rec rstk h depth = function
| Zshift(k) as e :: s ->
strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s
- | (Zapp args :: s) as stk ->
+ | (Zapp args :: s) ->
strip_rec (Zapp args :: rstk)
{norm=h.norm;term=FApp(h,Array.of_list args)} depth s
| Zupdate(m)::s ->
@@ -892,7 +883,7 @@ let get_arg h stk =
let rec get_args n tys f e stk =
match stk with
Zupdate r :: s ->
- let hd = update r (Cstr,FLambda(n,tys,f,e)) in
+ let _hd = update r (Cstr,FLambda(n,tys,f,e)) in
get_args n tys f e s
| Zshift k :: s ->
get_args n tys f (subs_shft (k,e)) s
@@ -985,7 +976,7 @@ let rec knh m stk =
(match get_nth_arg m ri.(n) stk with
(Some(pars,arg),stk') -> knh arg (Zfix(m,pars)::stk')
| (None, stk') -> (m,stk'))
- | FCast(t,_) -> knh t stk
+ | FCast(t,_,_) -> knh t stk
(* cases where knh stops *)
| (FFlex _|FLetIn _|FConstruct _|FEvar _|
FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) ->
@@ -999,7 +990,7 @@ and knht e t stk =
| Case(ci,p,t,br) ->
knht e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk)
| Fix _ -> knh (mk_clos2 e t) stk
- | Cast(a,b) -> knht e a stk
+ | Cast(a,_,_) -> knht e a stk
| Rel n -> knh (clos_rel e n) stk
| (Lambda _|Prod _|Construct _|CoFix _|Ind _|
LetIn _|Const _|Var _|Evar _|Meta _|Sort _) ->
@@ -1023,8 +1014,8 @@ let rec knr info m stk =
(match ref_value_cache info (VarKey id) with
Some v -> kni info v stk
| None -> (set_norm m; (m,stk)))
- | FFlex(FarRelKey k) when red_set info.i_flags fDELTA ->
- (match ref_value_cache info (FarRelKey k) with
+ | FFlex(RelKey k) when red_set info.i_flags fDELTA ->
+ (match ref_value_cache info (RelKey k) with
Some v -> kni info v stk
| None -> (set_norm m; (m,stk)))
| FConstruct(ind,c) when red_set info.i_flags fIOTA ->