diff options
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 348 |
1 files changed, 298 insertions, 50 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 196bb16f32..5fec55fea1 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -28,8 +28,9 @@ open Util open Pp open Names open Constr -open Vars +open Declarations open Environ +open Vars open Esubst let stats = ref false @@ -303,6 +304,7 @@ and fterm = | FProd of Name.t * fconstr * constr * fconstr subs | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs + | FInt of Uint63.t | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED @@ -335,19 +337,22 @@ type clos_infos = { i_flags : reds; i_cache : infos_cache } -type clos_tab = fconstr KeyTable.t +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 @@ -358,7 +363,7 @@ 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 - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _ | Zprimitive _) :: _ | [] -> Zapp v :: s (* Collapse the shifts in the stack *) @@ -366,20 +371,20 @@ let zshift n s = match (n,s) with (0,_) -> s | (_,Zshift(k)::s) -> Zshift(n+k)::s - | (_,(ZcaseT _ | Zproj _ | Zfix _ | Zapp _ | Zupdate _) :: _) | _,[] -> 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 - | (ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> 0 + | (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 = match ft.term with - | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)) -> ft + | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _) -> 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))} @@ -411,7 +416,7 @@ let compact_stack head stk = (** The stack contains [Zupdate] marks only if in sharing mode *) let _ = update ~share:true m h'.norm h'.term in strip_rec depth s - | ((ZcaseT _ | Zproj _ | Zfix _ | Zapp _) :: _ | []) as stk -> zshift depth stk + | ((ZcaseT _ | Zproj _ | Zfix _ | Zapp _ | Zprimitive _) :: _ | []) as stk -> zshift depth stk in strip_rec 0 stk @@ -447,6 +452,7 @@ let mk_clos e t = | Meta _ | Sort _ -> { norm = Norm; term = FAtom t } | Ind kn -> { norm = Norm; term = FInd kn } | Construct kn -> { norm = Cstr; term = FConstruct kn } + | Int i -> {norm = Cstr; term = FInt i} | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> {norm = Red; term = FCLOS(t,e)} @@ -465,32 +471,34 @@ let mk_clos_vect env v = match v with let ref_value_cache ({ i_cache = cache; _ }) tab ref = try - Some (KeyTable.find tab ref) + 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_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 + 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 - let v = inject body in - KeyTable.add tab ref v; - Some v - with - | Not_found (* List.assoc *) - | NotEvaluableConst _ (* Const *) - -> None + KeyTable.add tab ref v; v (* The inverse of mk_clos: move back to constr *) let rec to_constr lfts v = @@ -559,6 +567,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 @@ -607,6 +619,10 @@ let rec zip m stk = | Zupdate(rf)::s -> (** The stack contains [Zupdate] marks only if in sharing mode *) zip (update ~share:true rf m.norm m.term) s + | Zprimitive(_op,c,rargs,kargs)::s -> + let args = List.rev_append rargs (m::List.map snd kargs) in + let f = {norm = Red;term = FFlex (ConstKey c)} in + zip {norm=neutr m.norm; term = FApp (f, Array.of_list args)} s let fapp_stack (m,stk) = zip m stk @@ -628,7 +644,7 @@ let strip_update_shift_app_red head stk = | 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 - | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) as stk -> + | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk -> (depth,List.rev rstk, stk) in strip_rec [] head 0 stk @@ -656,7 +672,7 @@ let get_nth_arg head n stk = | 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 - | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) as s -> (None, List.rev rstk @ s) in + | ((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. @@ -678,24 +694,70 @@ let rec get_args n tys f e = function else (* more lambdas *) let etys = List.skipn na tys in get_args (n-na) etys f (subs_cons(l,e)) s - | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) as stk -> + | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk -> (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 _ | 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}|]] +(* 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 {norm = h.norm;term=FApp(h, args)} depth kargs s' + end + | Zupdate(m) :: s -> + strip_rec rnargs (update ~share:true m h.norm h.term) depth kargs s + | (Zprimitive _ | ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> assert false + in strip_rec [] {norm = Red;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 = 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 _) :: _ | []) as stk -> stk + | ((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 @@ -712,7 +774,7 @@ let rec try_drop_parameters depth n = function | [] -> if Int.equal n 0 then [] else raise Not_found - | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _) :: _ -> 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 = @@ -757,7 +819,7 @@ let rec project_nth_arg n = function let q = Array.length args in if n >= q then project_nth_arg (n - q) s else (* n < q *) args.(n) - | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zshift _) :: _ | [] -> assert false + | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zshift _ | Zprimitive _) :: _ | [] -> assert false (* After drop_parameters we have a purely applicative stack *) @@ -814,7 +876,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 *) @@ -828,7 +890,7 @@ and knht info e t 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) + | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _) -> (mk_clos e t, stk) | CoFix cfx -> { norm = Cstr; term = FCoFix (cfx,e) }, stk | Lambda _ -> { norm = Cstr; term = mk_lambda e t }, stk | Prod (n, t, c) -> @@ -837,6 +899,162 @@ and knht info e t stk = { 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 +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 = {norm = Norm; 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 := { norm = Norm; 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 := { norm = Cstr; term = FConstruct (Univ.in_punivs ct) }; + ffalse := { norm = Cstr; 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 := { norm = Cstr; term = FConstruct (Univ.in_punivs c0) }; + fC1 := { norm = Cstr; 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 := { norm = Cstr; 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 := { norm = Cstr; term = FConstruct (Univ.in_punivs cEq) }; + fLt := { norm = Cstr; term = FConstruct (Univ.in_punivs cLt) }; + fGt := { norm = Cstr; 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 := { norm = Cstr; 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; + { norm = Norm; term = FInt i } + + let mkBool env b = + check_bool env; + if b then !ftrue else !ffalse + + let mkCarry env b e = + check_carry env; + {norm = Cstr; + term = FApp ((if b then !fC1 else !fC0),[|!fint;e|])} + + let mkIntPair env e1 e2 = + check_pair env; + { norm = Cstr; 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) (************************************************************************) @@ -849,16 +1067,21 @@ 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 @@ -884,13 +1107,32 @@ let rec knr info tab m stk = | (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info tab fxe fxbd (args@stk') - | (_,args, ((Zapp _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] as 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 info.i_cache.i_sigma ev with Some c -> knit info tab env c stk | None -> (m,stk)) + | 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 = {norm = Whnf; term = FFlex (ConstKey c)} in + let m = {norm = Whnf; 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) @@ -927,6 +1169,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 @@ -972,7 +1220,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 *) @@ -1015,9 +1263,9 @@ 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 + else Undef None | RelKey _ -> ref_value_cache info tab key |