diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /checker/closure.ml | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'checker/closure.ml')
-rw-r--r-- | checker/closure.ml | 257 |
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 |