diff options
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 758 |
1 files changed, 505 insertions, 253 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 819a66c190..412637c4b6 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -21,13 +21,17 @@ (* This file implements a lazy reduction for the Calculus of Inductive Constructions *) +[@@@ocaml.warning "+4"] + open CErrors open Util open Pp open Names open Constr -open Vars +open Declarations +open Context open Environ +open Vars open Esubst let stats = ref false @@ -70,11 +74,8 @@ let with_stats c = end else Lazy.force c -let all_opaque = (Id.Pred.empty, Cpred.empty) -let all_transparent = (Id.Pred.full, Cpred.full) - -let is_transparent_variable (ids, _) id = Id.Pred.mem id ids -let is_transparent_constant (_, csts) cst = Cpred.mem cst csts +let all_opaque = TransparentState.empty +let all_transparent = TransparentState.full module type RedFlagsSig = sig type reds @@ -91,24 +92,26 @@ module type RedFlagsSig = sig 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 red_transparent : reds -> transparent_state + val red_add_transparent : reds -> TransparentState.t -> reds + val red_transparent : reds -> TransparentState.t val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool val red_projection : reds -> Projection.t -> bool end -module RedFlags = (struct +module RedFlags : RedFlagsSig = struct (* [r_const=(true,cl)] means all constants but those in [cl] *) (* [r_const=(false,cl)] means only those in [cl] *) (* [r_delta=true] just mean [r_const=(true,[])] *) + open TransparentState + type reds = { r_beta : bool; r_delta : bool; r_eta : bool; - r_const : transparent_state; + r_const : TransparentState.t; r_zeta : bool; r_match : bool; r_fix : bool; @@ -141,30 +144,30 @@ module RedFlags = (struct | ETA -> { red with r_eta = true } | DELTA -> { red with r_delta = true; r_const = all_transparent } | CONST kn -> - let (l1,l2) = red.r_const in - { red with r_const = l1, Cpred.add kn l2 } + let r = red.r_const in + { red with r_const = { r with tr_cst = Cpred.add kn r.tr_cst } } | MATCH -> { red with r_match = true } | FIX -> { red with r_fix = true } | COFIX -> { red with r_cofix = true } | ZETA -> { red with r_zeta = true } | VAR id -> - let (l1,l2) = red.r_const in - { red with r_const = Id.Pred.add id l1, l2 } + let r = red.r_const in + { red with r_const = { r with tr_var = Id.Pred.add id r.tr_var } } let red_sub red = function | BETA -> { red with r_beta = false } | ETA -> { red with r_eta = 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 } + let r = red.r_const in + { red with r_const = { r with tr_cst = Cpred.remove kn r.tr_cst } } | MATCH -> { red with r_match = false } | FIX -> { red with r_fix = false } | COFIX -> { red with r_cofix = false } | ZETA -> { red with r_zeta = false } | VAR id -> - let (l1,l2) = red.r_const in - { red with r_const = Id.Pred.remove id l1, l2 } + let r = red.r_const in + { red with r_const = { r with tr_var = Id.Pred.remove id r.tr_var } } let red_transparent red = red.r_const @@ -177,12 +180,10 @@ module RedFlags = (struct | BETA -> incr_cnt red.r_beta beta | ETA -> incr_cnt red.r_eta eta | CONST kn -> - let (_,l) = red.r_const in - let c = Cpred.mem kn l in + let c = is_transparent_constant red.r_const kn in incr_cnt c delta | VAR id -> (* En attendant d'avoir des kn pour les Var *) - let (l,_) = red.r_const in - let c = Id.Pred.mem id l in + let c = is_transparent_variable red.r_const id in incr_cnt c delta | ZETA -> incr_cnt red.r_zeta zeta | MATCH -> incr_cnt red.r_match nb_match @@ -195,7 +196,7 @@ module RedFlags = (struct if Projection.unfolded p then true else red_set red (fCONST (Projection.constant p)) -end : RedFlagsSig) +end open RedFlags @@ -224,11 +225,6 @@ let unfold_red kn = * abstractions, storing a representation (of type 'a) of the body of * this constant or abstraction. * * i_tab is the cache table of the results - * * 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 is the array of free rel variables together with their optional - * body * * 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,73 +252,11 @@ end module KeyTable = Hashtbl.Make(IdKeyHash) -let eq_table_key = IdKeyHash.equal - -type 'a infos_tab = 'a KeyTable.t - -type 'a infos_cache = { - i_repr : 'a infos -> 'a infos_tab -> constr -> 'a; - i_env : env; - i_sigma : existential -> constr option; - i_rels : (Constr.rel_declaration * lazy_val) Range.t; - i_share : bool; -} - -and 'a infos = { - i_flags : reds; - i_cache : 'a infos_cache } - -let info_flags info = info.i_flags -let info_env info = info.i_cache.i_env - open Context.Named.Declaration let assoc_defined id env = match Environ.lookup_named id env with | LocalDef (_, c, _) -> c -| _ -> raise Not_found - -let ref_value_cache ({i_cache = cache;_} as infos) tab ref = - try - Some (KeyTable.find tab ref) - with Not_found -> - try - let body = - match ref with - | RelKey n -> - let open! Context.Rel.Declaration in - let i = n - 1 in - let (d, _) = - try Range.get cache.i_rels i - with Invalid_argument _ -> raise Not_found - in - begin match d with - | LocalAssum _ -> raise Not_found - | LocalDef (_, t, _) -> lift n t - end - | VarKey id -> assoc_defined id cache.i_env - | ConstKey cst -> constant_value_in cache.i_env cst - in - let v = cache.i_repr infos tab body in - KeyTable.add tab ref v; - Some v - with - | Not_found (* List.assoc *) - | NotEvaluableConst _ (* Const *) - -> None - -let evar_value cache ev = - cache.i_sigma ev - -let create ~repr ~share flgs env evars = - let cache = - { i_repr = repr; - i_env = env; - i_sigma = evars; - i_rels = env.env_rel_context.env_rel_map; - i_share = share; - } - in { i_flags = flgs; i_cache = cache } - +| LocalAssum _ -> raise Not_found (**********************************************************************) (* Lazy reduction: the one used in kernel operations *) @@ -349,12 +283,63 @@ let create ~repr ~share flgs env evars = type red_state = Norm | Cstr | Whnf | Red let neutr = function - | (Whnf|Norm) -> Whnf - | (Red|Cstr) -> Red + | Whnf|Norm -> Whnf + | Red|Cstr -> Red + +type optrel = Unknown | KnownR | KnownI + +let opt_of_rel = function + | Sorts.Relevant -> KnownR + | Sorts.Irrelevant -> KnownI + +module Mark : sig + + type t + + val mark : red_state -> optrel -> t + val relevance : t -> optrel + val red_state : t -> red_state + + val neutr : t -> t + + val set_norm : t -> t + +end = struct + type t = int + + let[@inline] of_state = function + | Norm -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11 + + let[@inline] of_relevance = function + | Unknown -> 0 + | KnownR -> 0b01 + | KnownI -> 0b10 + + let[@inline] mark state relevance = (of_state state) * 4 + (of_relevance relevance) + + let[@inline] relevance x = match x land 0b11 with + | 0b00 -> Unknown + | 0b01 -> KnownR + | 0b10 -> KnownI + | _ -> assert false + + let[@inline] red_state x = match x land 0b1100 with + | 0b0000 -> Norm + | 0b0100 -> Cstr + | 0b1000 -> Whnf + | 0b1100 -> Red + | _ -> assert false + + let[@inline] neutr x = x lor 0b1000 (* Whnf|Norm -> Whnf | Red|Cstr -> Red *) + + let[@inline] set_norm x = x land 0b0011 +end +let mark = Mark.mark type fconstr = { - mutable norm: red_state; - mutable term: fterm } + mutable mark : Mark.t; + mutable term: fterm; +} and fterm = | FRel of int @@ -367,38 +352,59 @@ and fterm = | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) - | FLambda of int * (Name.t * constr) list * constr * fconstr subs - | FProd of Name.t * fconstr * fconstr - | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs + | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs + | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs + | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs + | FInt of Uint63.t | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED let fterm_of v = v.term -let set_norm v = v.norm <- Norm -let is_val v = match v.norm with Norm -> true | _ -> false +let set_norm v = v.mark <- Mark.set_norm v.mark +let is_val v = match Mark.red_state v.mark with Norm -> true | Cstr | Whnf | Red -> false -let mk_atom c = {norm=Norm;term=FAtom c} -let mk_red f = {norm=Red;term=f} +let mk_atom c = {mark=mark Norm Unknown;term=FAtom c} +let mk_red f = {mark=mark Red Unknown;term=f} (* Could issue a warning if no is still Red, pointing out that we loose sharing. *) -let update ~share v1 no t = +let update ~share v1 mark t = if share then - (v1.norm <- no; + (v1.mark <- mark; v1.term <- t; v1) - else {norm=no;term=t} + else {mark;term=t;} + +(** Reduction cache *) + +type infos_cache = { + i_env : env; + i_sigma : existential -> constr option; + i_share : bool; +} + +type clos_infos = { + i_flags : reds; + i_cache : infos_cache } + +type clos_tab = fconstr constant_def KeyTable.t + +let info_flags info = info.i_flags +let info_env info = info.i_cache.i_env (**********************************************************************) (* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) +type 'a next_native_args = (CPrimitives.arg_kind * 'a) list type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of Projection.Repr.t | Zfix of fconstr * stack + | Zprimitive of CPrimitives.t * pconstant * fconstr list * fconstr next_native_args + (* operator, constr def, arguments already seen (in rev order), next arguments *) | Zshift of int | Zupdate of fconstr @@ -409,75 +415,39 @@ let append_stack v s = if Int.equal (Array.length v) 0 then s else match s with | Zapp l :: s -> Zapp (Array.append v l) :: s - | _ -> Zapp v :: s + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _ | Zprimitive _) :: _ | [] -> + Zapp v :: s (* Collapse the shifts in the stack *) let zshift n s = match (n,s) with (0,_) -> s | (_,Zshift(k)::s) -> Zshift(n+k)::s - | _ -> Zshift(n)::s + | (_,(ZcaseT _ | Zproj _ | Zfix _ | Zapp _ | Zupdate _ | Zprimitive _) :: _) | _,[] -> 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 Int.equal 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 + | (ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | [] -> 0 (* 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. *) let rec lft_fconstr n ft = + let r = Mark.relevance ft.mark in match ft.term with - | (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))} - | FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))} + | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _) -> ft + | FRel i -> {mark=mark Norm r;term=FRel(i+n)} + | FLambda(k,tys,f,e) -> {mark=mark Cstr r; term=FLambda(k,tys,f,subs_shft(n,e))} + | FFix(fx,e) -> + {mark=mark Cstr r; term=FFix(fx,subs_shft(n,e))} + | FCoFix(cfx,e) -> + {mark=mark Cstr r; term=FCoFix(cfx,subs_shft(n,e))} | FLIFT(k,m) -> lft_fconstr (n+k) m | FLOCKED -> assert false - | FFlex _ | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _ - | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)} + | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _ + | FLetIn _ | FEvar _ | FCLOS _ -> {mark=ft.mark; term=FLIFT(n,ft)} let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f let lift_fconstr_vect k v = @@ -486,9 +456,9 @@ let lift_fconstr_vect k v = let clos_rel e i = match expand_rel i e with | Inl(n,mt) -> lift_fconstr n mt - | Inr(k,None) -> {norm=Norm; term= FRel k} + | Inr(k,None) -> {mark=mark Norm Unknown; term= FRel k} | Inr(k,Some p) -> - lift_fconstr (k-p) {norm=Red;term=FFlex(RelKey p)} + lift_fconstr (k-p) {mark=mark Red Unknown;term=FFlex(RelKey p)} (* since the head may be reducible, we might introduce lifts of 0 *) let compact_stack head stk = @@ -499,15 +469,16 @@ let compact_stack head stk = lost by the update operation *) let h' = lft_fconstr depth head in (** The stack contains [Zupdate] marks only if in sharing mode *) - let _ = update ~share:true m h'.norm h'.term in + let _ = update ~share:true m h'.mark h'.term in strip_rec depth s - | stk -> zshift depth stk in + | ((ZcaseT _ | Zproj _ | Zfix _ | Zapp _ | Zprimitive _) :: _ | []) as stk -> zshift depth stk + in strip_rec 0 stk (* Put an update mark in the stack, only if needed *) let zupdate info m s = let share = info.i_cache.i_share in - if share && begin match m.norm with Red -> true | _ -> false end + if share && begin match Mark.red_state m.mark with Red -> true | Norm | Whnf | Cstr -> false end then let s' = compact_stack m s in let _ = m.term <- FLOCKED in @@ -519,25 +490,28 @@ let mk_lambda env t = FLambda(List.length rvars, List.rev rvars, t', env) let destFLambda clos_fun t = - match t.term with + match [@ocaml.warning "-4"] t.term with FLambda(_,[(na,ty)],b,e) -> (na,clos_fun e ty,clos_fun (subs_lift e) b) | FLambda(n,(na,ty)::tys,b,e) -> - (na,clos_fun e ty,{norm=Cstr;term=FLambda(n-1,tys,b,subs_lift e)}) + (na,clos_fun e ty,{mark=t.mark;term=FLambda(n-1,tys,b,subs_lift e)}) | _ -> assert false - (* t must be a FLambda and binding list cannot be empty *) + (* t must be a FLambda and binding list cannot be empty *) (* Optimization: do not enclose variables in a closure. Makes variable access much faster *) let mk_clos e t = match kind t with | Rel i -> clos_rel e i - | Var x -> { norm = Red; term = FFlex (VarKey x) } - | Const c -> { norm = Red; term = FFlex (ConstKey c) } - | Meta _ | Sort _ -> { norm = Norm; term = FAtom t } - | Ind kn -> { norm = Norm; term = FInd kn } - | Construct kn -> { norm = Cstr; term = FConstruct kn } + | Var x -> {mark = mark Red Unknown; term = FFlex (VarKey x) } + | Const c -> {mark = mark Red Unknown; term = FFlex (ConstKey c) } + | Meta _ | Sort _ -> {mark = mark Norm KnownR; term = FAtom t } + | Ind kn -> {mark = mark Norm KnownR; term = FInd kn } + | Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn } + | Int i -> {mark = mark Cstr Unknown; term = FInt i} | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> - {norm = Red; term = FCLOS(t,e)} + {mark = mark Red Unknown; term = FCLOS(t,e)} + +let inject c = mk_clos (subs_id 0) c (** Hand-unrolling of the map function to bypass the call to the generic array allocation *) @@ -550,6 +524,37 @@ let mk_clos_vect env v = match v with [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|] | v -> Array.Fun1.map mk_clos env v +let ref_value_cache ({ i_cache = cache; _ }) tab ref = + try + KeyTable.find tab ref + with Not_found -> + let v = + try + let body = + match ref with + | RelKey n -> + let open! Context.Rel.Declaration in + let i = n - 1 in + let (d, _) = + try Range.get cache.i_env.env_rel_context.env_rel_map i + with Invalid_argument _ -> raise Not_found + in + begin match d with + | LocalAssum _ -> raise Not_found + | LocalDef (_, t, _) -> lift n t + end + | VarKey id -> assoc_defined id cache.i_env + | ConstKey cst -> constant_value_in cache.i_env cst + in + Def (inject body) + with + | NotEvaluableConst (IsPrimitive op) (* Const *) -> Primitive op + | Not_found (* List.assoc *) + | NotEvaluableConst _ (* Const *) + -> Undef None + in + KeyTable.add tab ref v; v + (* The inverse of mk_clos: move back to constr *) let rec to_constr lfts v = match v.term with @@ -602,9 +607,12 @@ let rec to_constr lfts v = let tys = List.mapi (fun i (na, c) -> na, subst_constr (subs_liftn i subs) c) tys in let f = subst_constr (subs_liftn len subs) f in Term.compose_lam (List.rev tys) f - | FProd (n,t,c) -> - mkProd (n, to_constr lfts t, - to_constr (el_lift lfts) c) + | FProd (n, t, c, e) -> + if is_subs_id e && is_lift_id lfts then + mkProd (n, to_constr lfts t, c) + else + let subs' = comp_subs lfts e in + mkProd (n, to_constr lfts t, subst_constr (subs_lift subs') c) | FLetIn (n,b,t,f,e) -> let subs = comp_subs (el_lift lfts) (subs_lift e) in mkLetIn (n, to_constr lfts b, @@ -614,6 +622,10 @@ let rec to_constr lfts v = let subs = comp_subs lfts env in mkEvar(ev,Array.map (fun a -> subst_constr subs a) args) | FLIFT (k,a) -> to_constr (el_shft k lfts) a + + | FInt i -> + Constr.mkInt i + | FCLOS (t,env) -> if is_subs_id env && is_lift_id lfts then t else @@ -621,7 +633,7 @@ let rec to_constr lfts v = subst_constr subs t | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*) -and subst_constr subst c = match Constr.kind c with +and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with | Rel i -> begin match expand_rel i subst with | Inl (k, lazy v) -> Vars.lift k v @@ -649,19 +661,25 @@ let rec fstrong unfreeze_fun lfts v = let rec zip m stk = match stk with | [] -> m - | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s + | Zapp args :: s -> zip {mark=Mark.neutr m.mark; term=FApp(m, args)} s | ZcaseT(ci,p,br,e)::s -> let t = FCaseT(ci, p, m, br, e) in - zip {norm=neutr m.norm; term=t} s + let mark = mark (neutr (Mark.red_state m.mark)) Unknown in + zip {mark; term=t} s | Zproj p :: s -> - zip {norm=neutr m.norm; term=FProj(Projection.make p true,m)} s + let mark = mark (neutr (Mark.red_state m.mark)) Unknown in + zip {mark; term=FProj(Projection.make p true,m)} s | Zfix(fx,par)::s -> zip fx (par @ append_stack [|m|] s) | Zshift(n)::s -> zip (lift_fconstr n m) s | Zupdate(rf)::s -> (** The stack contains [Zupdate] marks only if in sharing mode *) - zip (update ~share:true rf m.norm m.term) s + zip (update ~share:true rf m.mark m.term) s + | Zprimitive(_op,c,rargs,kargs)::s -> + let args = List.rev_append rargs (m::List.map snd kargs) in + let f = {mark = mark Red Unknown;term = FFlex (ConstKey c)} in + zip {mark=mark (neutr (Mark.red_state m.mark)) KnownR; term = FApp (f, Array.of_list args)} s let fapp_stack (m,stk) = zip m stk @@ -679,19 +697,21 @@ let strip_update_shift_app_red head stk = strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s | (Zapp args :: s) -> strip_rec (Zapp args :: rstk) - {norm=h.norm;term=FApp(h,args)} depth s + {mark=h.mark;term=FApp(h,args)} depth s | Zupdate(m)::s -> (** The stack contains [Zupdate] marks only if in sharing mode *) - strip_rec rstk (update ~share:true m h.norm h.term) depth s - | stk -> (depth,List.rev rstk, stk) in + strip_rec rstk (update ~share:true m h.mark h.term) depth s + | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk -> + (depth,List.rev rstk, stk) + in strip_rec [] head 0 stk let strip_update_shift_app head stack = - assert (match head.norm with Red -> false | _ -> true); + assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true); strip_update_shift_app_red head stack let get_nth_arg head n stk = - assert (match head.norm with Red -> false | _ -> true); + assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true); let rec strip_rec rstk h n = function | Zshift(k) as e :: s -> strip_rec (e::rstk) (lift_fconstr k h) n s @@ -699,7 +719,7 @@ let get_nth_arg head n stk = let q = Array.length args in if n >= q then - strip_rec (Zapp args::rstk) {norm=h.norm;term=FApp(h,args)} (n-q) s' + strip_rec (Zapp args::rstk) {mark=h.mark;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 @@ -708,17 +728,16 @@ let get_nth_arg head n stk = (Some (stk', args.(n)), append_stack aft s') | Zupdate(m)::s -> (** The stack contains [Zupdate] mark only if in sharing mode *) - strip_rec rstk (update ~share:true m h.norm h.term) n s - | s -> (None, List.rev rstk @ s) in + strip_rec rstk (update ~share:true m h.mark h.term) n s + | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as s -> (None, List.rev rstk @ s) in 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 *) -let rec get_args n tys f e stk = - match stk with - Zupdate r :: s -> +let rec get_args n tys f e = function + | Zupdate r :: s -> (** The stack contains [Zupdate] mark only if in sharing mode *) - let _hd = update ~share:true r Cstr (FLambda(n,tys,f,e)) in + let _hd = update ~share:true r (mark Cstr (Mark.relevance r.mark)) (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 @@ -732,31 +751,76 @@ let rec get_args n tys f e stk = else (* more lambdas *) let etys = List.skipn na tys in get_args (n-na) etys f (subs_cons(l,e)) s - | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk) + | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk -> + (Inr {mark=mark Cstr Unknown;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 _ | ZcaseT _ | Zproj _ - | Zshift _ | Zupdate _ as e) :: s -> + | Zshift _ | Zupdate _ | Zprimitive _ as e) :: s -> e :: eta_expand_stack s | [] -> - [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]] + [Zshift 1; Zapp [|{mark=mark Norm Unknown; term= FRel 1}|]] + +(* Get the arguments of a native operator *) +let rec skip_native_args rargs nargs = + match nargs with + | (kd, a) :: nargs' -> + if kd = CPrimitives.Kwhnf then rargs, nargs + else skip_native_args (a::rargs) nargs' + | [] -> rargs, [] + +let get_native_args op c stk = + let kargs = CPrimitives.kind op in + let rec get_args rnargs kargs args = + match kargs, args with + | kd::kargs, a::args -> get_args ((kd,a)::rnargs) kargs args + | _, _ -> rnargs, kargs, args in + let rec strip_rec rnargs h depth kargs = function + | Zshift k :: s -> + strip_rec (List.map (fun (kd,f) -> kd,lift_fconstr k f) rnargs) + (lift_fconstr k h) (depth+k) kargs s + | Zapp args :: s' -> + begin match get_args rnargs kargs (Array.to_list args) with + | rnargs, [], [] -> + (skip_native_args [] (List.rev rnargs), s') + | rnargs, [], eargs -> + (skip_native_args [] (List.rev rnargs), + Zapp (Array.of_list eargs) :: s') + | rnargs, kargs, _ -> + strip_rec rnargs {mark = h.mark;term=FApp(h, args)} depth kargs s' + end + | Zupdate(m) :: s -> + strip_rec rnargs (update ~share:true m h.mark h.term) depth kargs s + | (Zprimitive _ | ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> assert false + in strip_rec [] {mark = mark Red Unknown;term = FFlex(ConstKey c)} 0 kargs stk + +let get_native_args1 op c stk = + match get_native_args op c stk with + | ((rargs, (kd,a):: nargs), stk) -> + assert (kd = CPrimitives.Kwhnf); + (rargs, a, nargs, stk) + | _ -> assert false + +let check_native_args op stk = + let nargs = CPrimitives.arity op in + let rargs = stack_args_size stk in + nargs <= rargs + (* Iota reduction: extract the arguments to be passed to the Case branches *) -let rec reloc_rargs_rec depth stk = - match stk with - Zapp args :: s -> - Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s - | Zshift(k)::s -> if Int.equal k depth then s else reloc_rargs_rec (depth-k) s - | _ -> stk +let rec reloc_rargs_rec depth = function + | Zapp args :: s -> + Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s + | Zshift(k)::s -> if Int.equal k depth then s else reloc_rargs_rec (depth-k) s + | ((ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zprimitive _) :: _ | []) as stk -> stk let reloc_rargs depth stk = if Int.equal depth 0 then stk else reloc_rargs_rec depth stk -let rec try_drop_parameters depth n argstk = - match argstk with - Zapp args::s -> +let rec try_drop_parameters depth n = function + | Zapp args::s -> let q = Array.length args in if n > q then try_drop_parameters depth (n-q) s else if Int.equal n q then reloc_rargs depth s @@ -767,7 +831,7 @@ let rec try_drop_parameters depth n argstk = | [] -> if Int.equal n 0 then [] else raise Not_found - | _ -> assert false + | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zprimitive _) :: _ -> assert false (* strip_update_shift_app only produces Zapp and Zshift items *) let drop_parameters depth n argstk = @@ -800,20 +864,19 @@ let eta_expand_ind_stack env ind m s (f, s') = (** Try to drop the params, might fail on partially applied constructors. *) let argss = try_drop_parameters depth pars args in let hstack = Array.map (fun p -> - { norm = Red; (* right can't be a constructor though *) + { mark = mark Red Unknown; (* right can't be a constructor though *) term = FProj (Projection.make p true, right) }) projs in argss, [Zapp hstack] | None -> raise Not_found (* disallow eta-exp for non-primitive records *) -let rec project_nth_arg n argstk = - match argstk with +let rec project_nth_arg n = function | Zapp args :: s -> let q = Array.length args in if n >= q then project_nth_arg (n - q) s else (* n < q *) args.(n) - | _ -> assert false + | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zshift _ | Zprimitive _) :: _ | [] -> assert false (* After drop_parameters we have a purely applicative stack *) @@ -828,14 +891,16 @@ let rec project_nth_arg n argstk = (* does not deal with FLIFT *) let contract_fix_vect fix = let (thisbody, make_body, env, nfix) = - match fix with - | FFix (((reci,i),(_,_,bds as rdcl)),env) -> + match [@ocaml.warning "-4"] fix with + | FFix (((reci,i),(nas,_,bds as rdcl)),env) -> (bds.(i), - (fun j -> { norm = Cstr; term = FFix (((reci,j),rdcl),env) }), + (fun j -> { mark = mark Cstr (opt_of_rel nas.(j).binder_relevance); + term = FFix (((reci,j),rdcl),env) }), env, Array.length bds) - | FCoFix ((i,(_,_,bds as rdcl)),env) -> + | FCoFix ((i,(nas,_,bds as rdcl)),env) -> (bds.(i), - (fun j -> { norm = Cstr; term = FCoFix ((j,rdcl),env) }), + (fun j -> { mark = mark Cstr (opt_of_rel nas.(j).binder_relevance); + term = FCoFix ((j,rdcl),env) }), env, Array.length bds) | _ -> assert false in @@ -859,7 +924,7 @@ let rec knh info m stk = | FLOCKED -> assert false | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk)) | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk) - | FFix(((ri,n),(_,_,_)),_) -> + | FFix(((ri,n),_),_) -> (match get_nth_arg m ri.(n) stk with (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk') | (None, stk') -> (m,stk')) @@ -870,7 +935,7 @@ let rec knh info m stk = (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| - FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) -> + FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _) -> (m, stk) (* The same for pure terms *) @@ -880,19 +945,175 @@ and knht info e t stk = knht info e a (append_stack (mk_clos_vect e b) stk) | Case(ci,p,t,br) -> knht info e t (ZcaseT(ci, p, br, e)::stk) - | Fix fx -> knh info { norm = Cstr; term = FFix (fx, e) } stk + | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk | Cast(a,_,_) -> knht info e a stk | Rel n -> knh info (clos_rel e n) stk - | Proj (p, c) -> knh info { norm = Red; term = FProj (p, mk_clos e c) } stk - | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> (mk_clos e t, stk) - | CoFix cfx -> { norm = Cstr; term = FCoFix (cfx,e) }, stk - | Lambda _ -> { norm = Cstr; term = mk_lambda e t }, stk + | Proj (p, c) -> knh info { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk + | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _) -> (mk_clos e t, stk) + | CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk + | Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk | Prod (n, t, c) -> - { norm = Whnf; term = FProd (n, mk_clos e t, mk_clos (subs_lift e) c) }, stk + { mark = mark Whnf KnownR; term = FProd (n, mk_clos e t, c, e) }, stk | LetIn (n,b,t,c) -> - { norm = Red; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk - | Evar ev -> { norm = Red; term = FEvar (ev, e) }, stk + { mark = mark Red Unknown; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk + | Evar ev -> { mark = mark Red Unknown; term = FEvar (ev, e) }, stk + +let inject c = mk_clos (subs_id 0) c +(************************************************************************) +(* Reduction of Native operators *) + +open Primred + +module FNativeEntries = + struct + type elem = fconstr + type args = fconstr array + type evd = unit + + let get = Array.get + + let get_int () e = + match [@ocaml.warning "-4"] e.term with + | FInt i -> i + | _ -> raise Primred.NativeDestKO + + let dummy = {mark = mark Norm KnownR; term = FRel 0} + + let current_retro = ref Retroknowledge.empty + let defined_int = ref false + let fint = ref dummy + + let init_int retro = + match retro.Retroknowledge.retro_int63 with + | Some c -> + defined_int := true; + fint := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } + | None -> defined_int := false + + let defined_bool = ref false + let ftrue = ref dummy + let ffalse = ref dummy + + let init_bool retro = + match retro.Retroknowledge.retro_bool with + | Some (ct,cf) -> + defined_bool := true; + ftrue := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs ct) }; + ffalse := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cf) } + | None -> defined_bool :=false + + let defined_carry = ref false + let fC0 = ref dummy + let fC1 = ref dummy + + let init_carry retro = + match retro.Retroknowledge.retro_carry with + | Some(c0,c1) -> + defined_carry := true; + fC0 := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs c0) }; + fC1 := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs c1) } + | None -> defined_carry := false + + let defined_pair = ref false + let fPair = ref dummy + + let init_pair retro = + match retro.Retroknowledge.retro_pair with + | Some c -> + defined_pair := true; + fPair := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs c) } + | None -> defined_pair := false + + let defined_cmp = ref false + let fEq = ref dummy + let fLt = ref dummy + let fGt = ref dummy + + let init_cmp retro = + match retro.Retroknowledge.retro_cmp with + | Some (cEq, cLt, cGt) -> + defined_cmp := true; + fEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cEq) }; + fLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cLt) }; + fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) } + | None -> defined_cmp := false + + let defined_refl = ref false + + let frefl = ref dummy + + let init_refl retro = + match retro.Retroknowledge.retro_refl with + | Some crefl -> + defined_refl := true; + frefl := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs crefl) } + | None -> defined_refl := false + + let init env = + current_retro := env.retroknowledge; + init_int !current_retro; + init_bool !current_retro; + init_carry !current_retro; + init_pair !current_retro; + init_cmp !current_retro; + init_refl !current_retro + + let check_env env = + if not (!current_retro == env.retroknowledge) then init env + + let check_int env = + check_env env; + assert (!defined_int) + + let check_bool env = + check_env env; + assert (!defined_bool) + + let check_carry env = + check_env env; + assert (!defined_carry && !defined_int) + + let check_pair env = + check_env env; + assert (!defined_pair && !defined_int) + + let check_cmp env = + check_env env; + assert (!defined_cmp) + + let mkInt env i = + check_int env; + { mark = mark Norm KnownR; term = FInt i } + + let mkBool env b = + check_bool env; + if b then !ftrue else !ffalse + + let mkCarry env b e = + check_carry env; + {mark = mark Cstr KnownR; + term = FApp ((if b then !fC1 else !fC0),[|!fint;e|])} + + let mkIntPair env e1 e2 = + check_pair env; + { mark = mark Cstr KnownR; term = FApp(!fPair, [|!fint;!fint;e1;e2|]) } + + let mkLt env = + check_cmp env; + !fLt + + let mkEq env = + check_cmp env; + !fEq + + let mkGt env = + check_cmp env; + !fGt + + end + +module FredNative = RedNative(FNativeEntries) (************************************************************************) @@ -905,21 +1126,26 @@ let rec knr info tab m stk = | Inr lam, s -> (lam,s)) | FFlex(ConstKey (kn,_ as c)) when red_set info.i_flags (fCONST kn) -> (match ref_value_cache info tab (ConstKey c) with - Some v -> kni info tab v stk - | None -> (set_norm m; (m,stk))) + | Def v -> kni info tab v stk + | Primitive op when check_native_args op stk -> + let rargs, a, nargs, stk = get_native_args1 op c stk in + kni info tab a (Zprimitive(op,c,rargs,nargs)::stk) + | Undef _ | OpaqueDef _ | Primitive _ -> (set_norm m; (m,stk))) | FFlex(VarKey id) when red_set info.i_flags (fVAR id) -> (match ref_value_cache info tab (VarKey id) with - Some v -> kni info tab v stk - | None -> (set_norm m; (m,stk))) + | Def v -> kni info tab v stk + | Primitive _ -> assert false + | OpaqueDef _ | Undef _ -> (set_norm m; (m,stk))) | FFlex(RelKey k) when red_set info.i_flags fDELTA -> (match ref_value_cache info tab (RelKey k) with - Some v -> kni info tab v stk - | None -> (set_norm m; (m,stk))) + | Def v -> kni info tab v stk + | Primitive _ -> assert false + | OpaqueDef _ | Undef _ -> (set_norm m; (m,stk))) | FConstruct((_ind,c),_u) -> let use_match = red_set info.i_flags fMATCH in let use_fix = red_set info.i_flags fFIX in if use_match || use_fix then - (match strip_update_shift_app m stk with + (match [@ocaml.warning "-4"] strip_update_shift_app m stk with | (depth, args, ZcaseT(ci,_,br,e)::s) when use_match -> assert (ci.ci_npar>=0); let rargs = drop_parameters depth ci.ci_npar args in @@ -937,17 +1163,36 @@ let rec knr info tab m stk = else (m,stk) | FCoFix _ when red_set info.i_flags fCOFIX -> (match strip_update_shift_app m stk with - (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> + | (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info tab fxe fxbd (args@stk') - | (_,args,s) -> (m,args@s)) + | (_,args, ((Zapp _ | Zfix _ | Zshift _ | Zupdate _ | Zprimitive _) :: _ | [] as s)) -> (m,args@s)) | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA -> knit info tab (subs_cons([|v|],e)) bd stk | FEvar(ev,env) -> - (match evar_value info.i_cache ev with + (match info.i_cache.i_sigma ev with Some c -> knit info tab env c stk | None -> (m,stk)) - | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FApp _ | FProj _ + | FInt _ -> + (match [@ocaml.warning "-4"] strip_update_shift_app m stk with + | (_, _, Zprimitive(op,c,rargs,nargs)::s) -> + let (rargs, nargs) = skip_native_args (m::rargs) nargs in + begin match nargs with + | [] -> + let args = Array.of_list (List.rev rargs) in + begin match FredNative.red_prim (info_env info) () op args with + | Some m -> kni info tab m s + | None -> + let f = {mark = mark Whnf KnownR; term = FFlex (ConstKey c)} in + let m = {mark = mark Whnf KnownR; term = FApp(f,args)} in + (m,s) + end + | (kd,a)::nargs -> + assert (kd = CPrimitives.Kwhnf); + kni info tab a (Zprimitive(op,c,rargs,nargs)::s) + end + | (_, _, s) -> (m, s)) + | FLOCKED | FRel _ | FAtom _ | FFlex (RelKey _ | ConstKey _ | VarKey _) | FInd _ | FApp _ | FProj _ | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ | FCLOS _ -> (m, stk) @@ -983,6 +1228,12 @@ let rec zip_term zfun m stk = zip_term zfun (lift n m) s | Zupdate(_rf)::s -> zip_term zfun m s + | Zprimitive(_,c,rargs, kargs)::s -> + let kargs = List.map (fun (_,a) -> zfun a) kargs in + let args = + List.fold_left (fun args a -> zfun a ::args) (m::kargs) rargs in + let h = mkApp (mkConstU c, Array.of_list args) in + zip_term zfun h s (* Computes the strong normal form of a term. 1- Calls kni @@ -1002,17 +1253,17 @@ and norm_head info tab m = if is_val m then (incr prune; term_of_fconstr m) else match m.term with | FLambda(_n,tys,f,e) -> - let (e',rvtys) = - List.fold_left (fun (e,ctxt) (na,ty) -> - (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt)) - (e,[]) tys in - let bd = kl info tab (mk_clos e' f) in - List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys + let (e',info,rvtys) = + List.fold_left (fun (e,info,ctxt) (na,ty) -> + (subs_lift e, info, (na,kl info tab (mk_clos e ty))::ctxt)) + (e,info,[]) tys in + let bd = kl info tab (mk_clos e' f) in + List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys | FLetIn(na,a,b,f,e) -> let c = mk_clos (subs_lift e) f in mkLetIn(na, kl info tab a, kl info tab b, kl info tab c) - | FProd(na,dom,rng) -> - mkProd(na, kl info tab dom, kl info tab rng) + | FProd(na,dom,rng,e) -> + mkProd(na, kl info tab dom, kl info tab (mk_clos (subs_lift e) rng)) | FCoFix((n,(na,tys,bds)),e) -> let ftys = Array.Fun1.map mk_clos e tys in let fbds = @@ -1028,7 +1279,7 @@ and norm_head info tab m = | FProj (p,c) -> mkProj (p, kl info tab c) | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _ - | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m + | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ | FInt _ -> term_of_fconstr m (* Initialization and then normalization *) @@ -1040,9 +1291,7 @@ let whd_val info tab v = let norm_val info tab v = with_stats (lazy (kl info tab v)) -let inject c = mk_clos (subs_id 0) c - -let whd_stack infos tab m stk = match m.norm with +let whd_stack infos tab m stk = match Mark.red_state m.mark with | Whnf | Norm -> (** No need to perform [kni] nor to unlock updates because every head subterm of [m] is [Whnf] or [Norm] *) @@ -1052,19 +1301,19 @@ let whd_stack infos tab m stk = match m.norm with let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k -(* cache of constants: the body is computed only when needed. *) -type clos_infos = fconstr infos - let create_clos_infos ?(evars=fun _ -> None) flgs env = let share = (Environ.typing_flags env).Declarations.share_reduction in - create ~share ~repr:(fun _ _ c -> inject c) flgs env evars + let cache = { + i_env = env; + i_sigma = evars; + i_share = share; + } in + { i_flags = flgs; i_cache = cache } let create_tab () = KeyTable.create 17 let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env -let env_of_infos infos = infos.i_cache.i_env - let infos_with_reds infos reds = { infos with i_flags = reds } @@ -1073,9 +1322,12 @@ let unfold_reference info tab key = | ConstKey (kn,_) -> if red_set info.i_flags (fCONST kn) then ref_value_cache info tab key - else None + else Undef None | VarKey i -> if red_set info.i_flags (fVAR i) then ref_value_cache info tab key - else None - | _ -> ref_value_cache info tab key + else Undef None + | RelKey _ -> ref_value_cache info tab key + +let relevance_of f = Mark.relevance f.mark +let set_relevance r f = f.mark <- Mark.mark (Mark.red_state f.mark) (opt_of_rel r) |