From a0a94c1340a63cdb824507b973393882666ba52a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 19 Feb 2009 13:13:14 +0100 Subject: Imported Upstream version 8.2-1+dfsg --- kernel/closure.ml | 34 ++++++++++++++++++++++------------ kernel/closure.mli | 11 +++++++---- kernel/reduction.ml | 40 +++++++++++++++++++++------------------- kernel/reduction.mli | 19 +++++++++++-------- 4 files changed, 61 insertions(+), 43 deletions(-) (limited to 'kernel') diff --git a/kernel/closure.ml b/kernel/closure.ml index b85be204..a184c128 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: closure.ml 10819 2008-04-20 18:14:44Z msozeau $ *) +(* $Id: closure.ml 11897 2009-02-09 19:28:02Z barras $ *) open Util open Pp @@ -28,7 +28,8 @@ let iota = ref 0 let prune = ref 0 let reset () = - beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0 + beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; evar := 0; + prune := 0 let stop() = msgnl (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ @@ -83,7 +84,6 @@ module RedFlags = (struct r_delta : bool; r_const : transparent_state; r_zeta : bool; - r_evar : bool; r_iota : bool } type red_kind = BETA | DELTA | IOTA | ZETA @@ -99,7 +99,6 @@ module RedFlags = (struct r_delta = false; r_const = all_opaque; r_zeta = false; - r_evar = false; r_iota = false } let red_add red = function @@ -201,6 +200,7 @@ type 'a infos = { i_flags : reds; i_repr : 'a infos -> constr -> 'a; i_env : env; + i_sigma : existential -> constr option; i_rels : int * (int * constr) list; i_vars : (identifier * constr) list; i_tab : (table_key, 'a) Hashtbl.t } @@ -227,6 +227,9 @@ let ref_value_cache info ref = | NotEvaluableConst _ (* Const *) -> None +let evar_value info ev = + info.i_sigma ev + let defined_vars flags env = (* if red_local_const (snd flags) then*) Sign.fold_named_context @@ -259,10 +262,11 @@ let rec mind_equiv env (kn1,i1) (kn2,i2) = let mind_equiv_infos info = mind_equiv info.i_env -let create mk_cl flgs env = +let create mk_cl flgs env evars = { i_flags = flgs; i_repr = mk_cl; i_env = env; + i_sigma = evars; i_rels = defined_rels flgs env; i_vars = defined_vars flgs env; i_tab = Hashtbl.create 17 } @@ -314,7 +318,7 @@ and fterm = | FLambda of int * (name * constr) list * constr * fconstr subs | FProd of name * fconstr * fconstr | FLetIn of name * fconstr * fconstr * constr * fconstr subs - | FEvar of existential_key * fconstr array + | FEvar of existential * fconstr subs | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED @@ -581,8 +585,8 @@ let mk_clos_deep clos_fun env t = | LetIn (n,b,t,c) -> { norm = Red; term = FLetIn (n, clos_fun env b, clos_fun env t, c, env) } - | Evar(ev,args) -> - { norm = Whnf; term = FEvar(ev,Array.map (clos_fun env) args) } + | Evar ev -> + { norm = Red; term = FEvar(ev,env) } (* A better mk_clos? *) let mk_clos2 = mk_clos_deep mk_clos @@ -632,7 +636,8 @@ let rec to_constr constr_fun lfts v = mkLetIn (n, constr_fun lfts b, constr_fun lfts t, constr_fun (el_lift lfts) fc) - | FEvar (ev,args) -> mkEvar(ev,Array.map (constr_fun lfts) args) + | FEvar ((ev,args),env) -> + mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args) | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a | FCLOS (t,env) -> let fr = mk_clos2 env t in @@ -891,6 +896,10 @@ let rec knr info m stk = | (_,args,s) -> (m,args@s)) | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA -> knit info (subs_cons([|v|],e)) bd stk + | FEvar(ev,env) -> + (match evar_value info ev with + Some c -> knit info env c stk + | None -> (m,stk)) | _ -> (m,stk) (* Computes the weak head normal form of a term *) @@ -959,7 +968,8 @@ and norm_head info m = let fbds = Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in mkFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) fbds)) - | FEvar(i,args) -> mkEvar(i, Array.map (kl info) args) + | FEvar((i,args),env) -> + mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args) | t -> term_of_fconstr m (* Initialization and then normalization *) @@ -982,7 +992,7 @@ let whd_stack infos m stk = (* cache of constants: the body is computed only when needed. *) type clos_infos = fconstr infos -let create_clos_infos flgs env = - create (fun _ -> inject) flgs env +let create_clos_infos ?(evars=fun _ -> None) flgs env = + create (fun _ -> inject) flgs env evars let unfold_reference = ref_value_cache diff --git a/kernel/closure.mli b/kernel/closure.mli index c814baad..a80f7a62 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: closure.mli 10652 2008-03-10 21:52:06Z herbelin $ i*) +(*i $Id: closure.mli 11897 2009-02-09 19:28:02Z barras $ i*) (*i*) open Pp @@ -85,7 +85,9 @@ type table_key = id_key type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option val info_flags: 'a infos -> reds -val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos +val create: ('a infos -> constr -> 'a) -> reds -> env -> + (existential -> constr option) -> 'a infos +val evar_value : 'a infos -> existential -> constr option (************************************************************************) (*s Lazy reduction. *) @@ -111,7 +113,7 @@ type fterm = | FLambda of int * (name * constr) list * constr * fconstr subs | FProd of name * fconstr * fconstr | FLetIn of name * fconstr * fconstr * constr * fconstr subs - | FEvar of existential_key * fconstr array + | FEvar of existential * fconstr subs | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED @@ -156,7 +158,8 @@ val destFLambda : (* Global and local constant cache *) type clos_infos -val create_clos_infos : reds -> env -> clos_infos +val create_clos_infos : + ?evars:(existential->constr option) -> reds -> env -> clos_infos (* Reduction function *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 43ef3a98..76b32463 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reduction.ml 10930 2008-05-15 10:50:32Z barras $ *) +(* $Id: reduction.ml 11897 2009-02-09 19:28:02Z barras $ *) open Util open Names @@ -248,10 +248,12 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv = then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | _ -> raise NotConvertible) - | (FEvar (ev1,args1), FEvar (ev2,args2)) -> + | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) -> if ev1=ev2 then let u1 = convert_stacks infos lft1 lft2 v1 v2 cuniv in - convert_vect infos el1 el2 args1 args2 u1 + convert_vect infos el1 el2 + (Array.map (mk_clos env1) args1) + (Array.map (mk_clos env2) args2) u1 else raise NotConvertible (* 2 index known to be bound to no constant *) @@ -382,29 +384,29 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv = fold 0 cuniv else raise NotConvertible -let clos_fconv trans cv_pb env t1 t2 = - let infos = trans, create_clos_infos betaiotazeta env in +let clos_fconv trans cv_pb evars env t1 t2 = + let infos = trans, create_clos_infos ~evars betaiotazeta env in ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty -let trans_fconv reds cv_pb env t1 t2 = +let trans_fconv reds cv_pb evars env t1 t2 = if eq_constr t1 t2 then Constraint.empty - else clos_fconv reds cv_pb env t1 t2 + else clos_fconv reds cv_pb evars env t1 t2 -let trans_conv_cmp conv reds = trans_fconv reds conv -let trans_conv reds = trans_fconv reds CONV -let trans_conv_leq reds = trans_fconv reds CUMUL +let trans_conv_cmp conv reds = trans_fconv reds conv (fun _->None) +let trans_conv ?(evars=fun _->None) reds = trans_fconv reds CONV evars +let trans_conv_leq ?(evars=fun _->None) reds = trans_fconv reds CUMUL evars let fconv = trans_fconv (Idpred.full, Cpred.full) -let conv_cmp = fconv -let conv = fconv CONV -let conv_leq = fconv CUMUL +let conv_cmp cv_pb = fconv cv_pb (fun _->None) +let conv ?(evars=fun _->None) = fconv CONV evars +let conv_leq ?(evars=fun _->None) = fconv CUMUL evars -let conv_leq_vecti env v1 v2 = +let conv_leq_vecti ?(evars=fun _->None) env v1 v2 = array_fold_left2_i (fun i c t1 t2 -> let c' = - try conv_leq env t1 t2 + try conv_leq ~evars env t1 t2 with NotConvertible -> raise (NotConvertibleVect i) in Constraint.union c c') Constraint.empty @@ -413,17 +415,17 @@ let conv_leq_vecti env v1 v2 = (* option for conversion *) -let vm_conv = ref fconv +let vm_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None)) let set_vm_conv f = vm_conv := f let vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> (* If compilation fails, fall-back to closure conversion *) - fconv cv_pb env t1 t2 + fconv cv_pb (fun _->None) env t1 t2 -let default_conv = ref fconv +let default_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None)) let set_default_conv f = default_conv := f @@ -432,7 +434,7 @@ let default_conv cv_pb env t1 t2 = !default_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> (* If compilation fails, fall-back to closure conversion *) - fconv cv_pb env t1 t2 + fconv cv_pb (fun _->None) env t1 t2 let default_conv_leq = default_conv CUMUL (* diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 3b9eb315..d8658d43 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: reduction.mli 10840 2008-04-23 21:29:34Z herbelin $ i*) +(*i $Id: reduction.mli 11897 2009-02-09 19:28:02Z barras $ i*) (*i*) open Term @@ -40,15 +40,18 @@ val conv_sort : sorts conversion_function val conv_sort_leq : sorts conversion_function val trans_conv_cmp : conv_pb -> constr trans_conversion_function - -val trans_conv : constr trans_conversion_function -val trans_conv_leq : types trans_conversion_function +val trans_conv : + ?evars:(existential->constr option) -> constr trans_conversion_function +val trans_conv_leq : + ?evars:(existential->constr option) -> types trans_conversion_function val conv_cmp : conv_pb -> constr conversion_function - -val conv : constr conversion_function -val conv_leq : types conversion_function -val conv_leq_vecti : types array conversion_function +val conv : + ?evars:(existential->constr option) -> constr conversion_function +val conv_leq : + ?evars:(existential->constr option) -> types conversion_function +val conv_leq_vecti : + ?evars:(existential->constr option) -> types array conversion_function (* option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit -- cgit v1.2.3