From b62f68bac9f053187dc95e7d78f706a074249872 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 4 Oct 2000 13:37:32 +0000 Subject: Touche finale à la réduction du let in dans conv et closure MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@647 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/closure.ml | 54 +++++++++++++++++++++++++++++----------------------- kernel/closure.mli | 2 +- kernel/reduction.ml | 18 +++++++++++++----- kernel/reduction.mli | 4 +++- 4 files changed, 47 insertions(+), 31 deletions(-) (limited to 'kernel') diff --git a/kernel/closure.ml b/kernel/closure.ml index f18d7e077..71bfa0778 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -224,10 +224,8 @@ let rec exp_rel lams k subs = | (_, LIFT (n,l)) -> exp_rel (n+lams) (k-n) l | (_, SHIFT (n,s)) -> exp_rel (n+lams) k s | (_, ESID n) when k<=n -> Inr(lams+k,None) - | (_, ESID n) -> Inr(lams+k,None) -(* TO DEBUG | (_, ESID n) -> Inr(lams+k,Some (k-n)) -*) + let expand_rel k subs = exp_rel 0 k subs (* Flags of reduction and cache of constants: 'a is a type that may be @@ -239,6 +237,9 @@ let expand_rel k subs = exp_rel 0 k subs * * i_repr is the function to get the representation from the current * state of the cache and the body of the constant. The result * is stored in the table. + * * i_rels = (4,[(1,c);(3,d)]) means there are 4 free rel variables + * and only those with index 1 and 3 have bodies which are c and d resp. + * * i_vars is the list of _defined_ named variables. * * ref_value_cache searchs in the tab, otherwise uses i_repr to * compute the result and store it in the table. If the constant can't @@ -256,7 +257,7 @@ type table_key = type ('a, 'b) infos = { i_flags : flags; - i_repr : ('a, 'b) infos -> int -> constr -> 'a; + i_repr : ('a, 'b) infos -> constr -> 'a; i_env : env; i_evc : 'b evar_map; i_rels : int * (int * constr) list; @@ -268,14 +269,15 @@ let ref_value_cache info ref = Some (Hashtbl.find info.i_tab ref) with Not_found -> try - let n, body = + let body = match ref with - | FarRelBinding n -> let (s,l) = info.i_rels in (n, List.assoc (s-n) l) - | VarBinding id -> 0, List.assoc id info.i_vars - | EvarBinding evc -> 0, existential_value info.i_evc evc - | ConstBinding cst -> 0, constant_value info.i_env cst + | FarRelBinding n -> + let (s,l) = info.i_rels in lift n (List.assoc (s-n) l) + | VarBinding id -> List.assoc id info.i_vars + | EvarBinding evc -> existential_value info.i_evc evc + | ConstBinding cst -> constant_value info.i_env cst in - let v = info.i_repr info n body in + let v = info.i_repr info body in Hashtbl.add info.i_tab ref v; Some v with @@ -285,7 +287,7 @@ let ref_value_cache info ref = -> None let make_constr_ref n = function - | FarRelBinding _ -> mkRel n + | FarRelBinding p -> mkRel (n+p) | VarBinding id -> mkVar id | EvarBinding evc -> mkEvar evc | ConstBinding cst -> mkConst cst @@ -518,7 +520,7 @@ let rec norm_head info env t stack = | Inr (n,None) -> (VAL(0, mkRel n), stack) | Inr (n,Some p) -> - norm_head_ref n info env stack (FarRelBinding p)) + norm_head_ref (n-p) info env stack (FarRelBinding p)) | IsVar id -> norm_head_ref 0 info env stack (VarBinding id) @@ -672,7 +674,7 @@ type 'a cbv_infos = (cbv_value, 'a) infos (* constant bodies are normalized at the first expansion *) let create_cbv_infos flgs env sigma = { i_flags = flgs; - i_repr = (fun old_info n c -> cbv_stack_term old_info TOP (ESID (-n)) c); + i_repr = (fun old_info c -> cbv_stack_term old_info TOP (ESID (0)) c); i_env = env; i_evc = sigma; i_rels = defined_rels flgs env; @@ -732,7 +734,9 @@ and frreference = | FConst of section_path | FEvar of existential_key | FVar of identifier - | FFarRel of int * int + | FFarRel of int (* index in the rel_context part of _initial_ environment *) + +let reloc_flex r el = r (* let typed_map f t = f (body_of_type t), level_of_type t @@ -804,7 +808,8 @@ let rec traverse_term env t = | Inl (lams,v) -> (lift_frterm lams v) | Inr (k,None) -> { norm = true; term = FRel k } | Inr (k,Some p) -> - { norm = false; term = FFlex (FFarRel (k,p), [||]) }) + lift_frterm (k-p) + { norm = false; term = FFlex (FFarRel p, [||]) }) | IsVar x -> { norm = false; term = FFlex (FVar x, [||]) } | IsMeta _ | IsSort _ | IsXtra _ -> { norm = true; term = FAtom t } | IsCast (a,b) -> @@ -864,7 +869,7 @@ let rec lift_term_of_freeze lfts v = match v.term with | FRel i -> mkRel (reloc_rel i lfts) | FFlex (FVar x, v) -> assert (v=[||]); mkVar x - | FFlex (FFarRel (i,p), v) -> assert (v=[||]); mkRel (reloc_rel i lfts) + | FFlex (FFarRel p, v) -> assert (v=[||]); mkRel (reloc_rel p lfts) | FAtom c -> c | FCast (a,b) -> mkCast (lift_term_of_freeze lfts a, lift_term_of_freeze lfts b) @@ -919,7 +924,7 @@ let applist_of_freeze appl = Array.to_list (Array.map term_of_freeze appl) let rec fstrong unfreeze_fun lfts v = match (unfreeze_fun v).term with | FRel i -> mkRel (reloc_rel i lfts) - | FFlex (FFarRel (i,p), v) -> assert (v=[||]); mkRel (reloc_rel i lfts) + | FFlex (FFarRel p, v) -> assert (v=[||]); mkRel (reloc_rel p lfts) | FFlex (FVar x, v) -> assert (v=[||]); mkVar x | FAtom c -> c | FCast (a,b) -> @@ -1091,12 +1096,12 @@ and whnf_frterm info ft = lift_frterm 0 udef | None -> { norm = true; term = t } else ft - | FFlex (FFarRel (n,k),_) as t -> + | FFlex (FFarRel k,_) as t -> if red_under info.i_flags DELTA then match ref_value_cache info (FarRelBinding k) with | Some def -> let udef = unfreeze info def in - lift_frterm n udef + lift_frterm 0 udef | None -> { norm = true; term = t } else ft @@ -1120,7 +1125,7 @@ and whnf_frterm info ft = | FLetIn (na,b,fd,fc,d,subs) -> let c = unfreeze info b in if red_under info.i_flags LETIN then - contract_subst 0 d subs c + whnf_frterm info (contract_subst 0 d subs c) else { norm = false; term = FLetIn (na,c,fd,fc,d,subs) } @@ -1164,7 +1169,8 @@ and whnf_term info env t = { norm = true; term = FRel n } | Inr (n,Some k) -> whnf_frterm info - { norm = false; term = FFlex (FFarRel (n,k), [||]) }) + (lift_frterm (n-k) + { norm = false; term = FFlex (FFarRel k, [||]) })) | IsVar x -> whnf_frterm info { norm = false; term = FFlex (FVar x, [||]) } @@ -1234,8 +1240,8 @@ let search_frozen_value info f vars = match f with ref_value_cache info (EvarBinding (op,Array.map (norm_val info) vars)) | FVar id -> ref_value_cache info (VarBinding id) - | FFarRel (n,p) -> - ref_value_cache info (FarRelBinding (n+p)) + | FFarRel p -> + ref_value_cache info (FarRelBinding p) (* cache of constants: the body is computed only when needed. *) @@ -1244,7 +1250,7 @@ type 'a clos_infos = (fconstr, 'a) infos let create_clos_infos flgs env sigma = { i_flags = flgs; - i_repr = (fun old_info n c -> freeze (ESID (-n)) c); + i_repr = (fun old_info c -> freeze (ESID (0)) c); i_env = env; i_evc = sigma; i_rels = defined_rels flgs env; diff --git a/kernel/closure.mli b/kernel/closure.mli index 4c1846039..4fb41382c 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -156,7 +156,7 @@ and frreference = | FConst of section_path | FEvar of existential_key | FVar of identifier - | FFarRel of int * int + | FFarRel of int val frterm_of : freeze -> frterm val is_val : freeze -> bool diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 827956fd5..c169e9d18 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -165,6 +165,7 @@ let betadeltaeta = [BETA;DELTA;EVAR;ETA] let betadeltaiota = [BETA;DELTA;EVAR;IOTA] let betadeltaiotaeta = [BETA;DELTA;EVAR;IOTA;ETA] let betaiotaevar = [BETA;IOTA;EVAR] +let betaeta = [BETA;ETA] *) (* Compact Implementation *) @@ -193,6 +194,7 @@ let betadeltaiota = fbeta lor fdelta lor fletin lor fevar lor fiota let betadeltaiota_nolet = fbeta lor fdelta lor fevar lor fiota let betadeltaiotaeta = fbeta lor fdelta lor fletin lor fevar lor fiota lor feta let betaiotaevar = fbeta lor fiota lor fevar +let betaetalet = fbeta lor feta lor fletin (* Beta Reduction tools *) @@ -380,13 +382,19 @@ let whd_beta_state = local_whd_state_gen beta let whd_beta_stack x = appterm_of_stack (whd_beta_state (x, empty_stack)) let whd_beta x = app_stack (whd_beta_state (x,empty_stack)) +(* Nouveau ! *) +let whd_betaetalet_state = local_whd_state_gen betaetalet +let whd_betaetalet_stack x = + appterm_of_stack (whd_betaetalet_state (x, empty_stack)) +let whd_betaetalet x = app_stack (whd_betaetalet_state (x,empty_stack)) + (* 2. Delta Reduction Functions *) (* let whd_delta_state env sigma = let rec whrec (x, l as s) = match kind_of_term x with - | IsConst const when evaluable_constant env x -> + | IsConst const when evaluable_constant env const -> whrec (constant_value env const, l) | IsEvar (ev,args) when Evd.is_defined sigma ev -> whrec (existential_value sigma (ev,args), l) @@ -409,7 +417,7 @@ let whd_betadelta_state env sigma = let rec whrec (x, l as s) = match kind_of_term x with | IsConst const -> - if evaluable_constant env x then + if evaluable_constant env const then whrec (constant_value env const, l) else s @@ -467,7 +475,7 @@ let whd_betaevar env sigma c = let whd_betadeltaeta_state env sigma = let rec whrec (x, l as s) = match kind_of_term x with - | IsConst const when evaluable_constant env x -> + | IsConst const when evaluable_constant env const -> whrec (constant_value env const, l) | IsEvar (ev,args) when Evd.is_defined sigma ev -> whrec (existential_value sigma (ev,args), l) @@ -585,7 +593,7 @@ let whd_betaiotaevar env sigma x = let whd_betadeltaiota_state env sigma = let rec whrec (x, stack as s) = match kind_of_term x with - | IsConst const when evaluable_constant env x -> + | IsConst const when evaluable_constant env const -> whrec (constant_value env const, stack) | IsEvar (ev,args) when Evd.is_defined sigma ev -> whrec (existential_value sigma (ev,args), stack) @@ -623,7 +631,7 @@ let whd_betadeltaiota env sigma x = let whd_betadeltaiotaeta_state env sigma = let rec whrec (x, stack as s) = match kind_of_term x with - | IsConst const when evaluable_constant env x -> + | IsConst const when evaluable_constant env const -> whrec (constant_value env const, stack) | IsEvar (ev,args) when Evd.is_defined sigma ev -> whrec (existential_value sigma (ev,args), stack) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index ebf456301..e6dd5c25c 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -73,15 +73,17 @@ val nf_betadeltaiota : 'a reduction_function val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function val whd_betadeltaiota : 'a contextual_reduction_function +val whd_betaetalet : local_reduction_function val whd_beta_stack : local_stack_reduction_function val whd_betaiota_stack : local_stack_reduction_function val whd_betadeltaiota_stack : 'a contextual_stack_reduction_function +val whd_betaetalet_stack : local_stack_reduction_function val whd_beta_state : local_state_reduction_function val whd_betaiota_state : local_state_reduction_function val whd_betadeltaiota_state : 'a contextual_state_reduction_function - +val whd_betaetalet_state : local_state_reduction_function (*s Head normal forms *) -- cgit v1.2.3