diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 97 | ||||
| -rw-r--r-- | kernel/environ.ml | 26 | ||||
| -rw-r--r-- | kernel/environ.mli | 8 | ||||
| -rw-r--r-- | kernel/reduction.ml | 81 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 6 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 3 |
6 files changed, 141 insertions, 80 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index c558689595..95546a83e1 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -21,6 +21,8 @@ (* This file implements a lazy reduction for the Calculus of Inductive Constructions *) +[@@@ocaml.warning "+4"] + open CErrors open Util open Pp @@ -255,7 +257,7 @@ open Context.Named.Declaration let assoc_defined id env = match Environ.lookup_named id env with | LocalDef (_, c, _) -> c -| _ -> raise Not_found +| LocalAssum _ -> raise Not_found (**********************************************************************) (* Lazy reduction: the one used in kernel operations *) @@ -310,7 +312,7 @@ and fterm = 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 is_val v = match v.norm with Norm -> true | Cstr | Whnf | Red -> false let mk_atom c = {norm=Norm;term=FAtom c} let mk_red f = {norm=Red;term=f} @@ -359,20 +361,21 @@ 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 _) :: _ | [] -> + 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 _) :: _) | _,[] -> 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 + | (ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> 0 (* When used as an argument stack (only Zapp can appear) *) let rec decomp_stack = function @@ -382,12 +385,12 @@ let rec decomp_stack = function | 1 -> Some (v.(0), s) | _ -> Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) - | _ -> None + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> None let array_of_stack s = let rec stackrec = function | [] -> [] | Zapp args :: s -> args :: (stackrec s) - | _ -> assert false + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ -> assert false in Array.concat (stackrec s) let rec stack_assign s p c = match s with | Zapp args :: s -> @@ -398,7 +401,7 @@ let rec stack_assign s p c = match s with (let nargs = Array.copy args in nargs.(p) <- c; Zapp nargs :: s) - | _ -> s + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> s let rec stack_tail p s = if Int.equal p 0 then s else match s with @@ -406,13 +409,13 @@ let rec stack_tail p 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" + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> 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 _ | Zshift _ | Zupdate _) :: _ | [] -> 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 @@ -426,7 +429,7 @@ let rec lft_fconstr n ft = | FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))} | FLIFT(k,m) -> lft_fconstr (n+k) m | FLOCKED -> assert false - | FFlex _ | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _ + | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _ | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)} let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f @@ -451,13 +454,14 @@ 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 - | stk -> zshift depth stk in + | ((ZcaseT _ | Zproj _ | Zfix _ | Zapp _) :: _ | []) 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 m.norm with Red -> true | Norm | Whnf | Cstr -> false end then let s' = compact_stack m s in let _ = m.term <- FLOCKED in @@ -469,12 +473,12 @@ let mk_lambda env t = FLambda(List.length rvars, List.rev rvars, t', env) let destFLambda clos_fun t = - match 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)}) - | _ -> assert false - (* t must be a FLambda and binding list cannot be empty *) + 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)}) + | _ -> assert false +(* t must be a FLambda and binding list cannot be empty *) (* Optimization: do not enclose variables in a closure. Makes variable access much faster *) @@ -602,7 +606,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 @@ -664,15 +668,17 @@ 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 - | stk -> (depth,List.rev rstk, stk) in + | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) 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 head.norm 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 head.norm 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 @@ -690,14 +696,13 @@ 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 - | s -> (None, List.rev rstk @ s) in + | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) 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 get_args n tys f e s @@ -713,7 +718,8 @@ 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 _) :: _ | []) 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 @@ -725,19 +731,17 @@ let rec eta_expand_stack = function (* 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 _) :: _ | []) 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 @@ -748,7 +752,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 _) :: _ -> assert false (* strip_update_shift_app only produces Zapp and Zshift items *) let drop_parameters depth n argstk = @@ -788,13 +792,12 @@ let eta_expand_ind_stack env ind m s (f, s') = 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 _) :: _ | [] -> assert false (* After drop_parameters we have a purely applicative stack *) @@ -809,7 +812,7 @@ 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 + match [@ocaml.warning "-4"] fix with | FFix (((reci,i),(_,_,bds as rdcl)),env) -> (bds.(i), (fun j -> { norm = Cstr; term = FFix (((reci,j),rdcl),env) }), @@ -900,7 +903,7 @@ let rec knr info tab m stk = 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 @@ -918,17 +921,17 @@ 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 _) :: _ | [] 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)) - | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FApp _ | FProj _ + | FLOCKED | FRel _ | FAtom _ | FFlex (RelKey _ | ConstKey _ | VarKey _) | FInd _ | FApp _ | FProj _ | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ | FCLOS _ -> (m, stk) @@ -1057,4 +1060,4 @@ let unfold_reference info tab key = if red_set info.i_flags (fVAR i) then ref_value_cache info tab key else None - | _ -> ref_value_cache info tab key + | RelKey _ -> ref_value_cache info tab key diff --git a/kernel/environ.ml b/kernel/environ.ml index cdb8836ed2..f61dd0c101 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -424,6 +424,16 @@ let constant_value_and_type env (kn, u) = in b', subst_instance_constr u cb.const_type, cst +let body_of_constant_body env cb = + let otab = opaque_tables env in + match cb.const_body with + | Undef _ -> + None + | Def c -> + Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) + | OpaqueDef o -> + Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb) + (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) @@ -676,6 +686,22 @@ let is_polymorphic env r = | IndRef ind -> polymorphic_ind ind env | ConstructRef cstr -> polymorphic_ind (inductive_of_constructor cstr) env +let is_template_polymorphic env r = + let open Names.GlobRef in + match r with + | VarRef _id -> false + | ConstRef _c -> false + | IndRef ind -> template_polymorphic_ind ind env + | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env + +let is_type_in_type env r = + let open Names.GlobRef in + match r with + | VarRef _id -> false + | ConstRef c -> type_in_type_constant c env + | IndRef ind -> type_in_type_ind ind env + | ConstructRef cstr -> type_in_type_ind (inductive_of_constructor cstr) env + (*spiwack: the following functions assemble the pieces of the retroknowledge note that the "consistent" register function is available in the module Safetyping, Environ only synchronizes the proactive and the reactive parts*) diff --git a/kernel/environ.mli b/kernel/environ.mli index 53a2eae7e1..c285f907fc 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -206,6 +206,12 @@ val constant_value_and_type : env -> Constant.t puniverses -> polymorphic *) val constant_context : env -> Constant.t -> Univ.AUContext.t +(** Returns the body of the constant if it has any, and the polymorphic context + it lives in. For monomorphic constant, the latter is empty, and for + polymorphic constants, the term contains De Bruijn universe variables that + need to be instantiated. *) +val body_of_constant_body : env -> constant_body -> (Constr.constr * Univ.AUContext.t) option + (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) @@ -315,6 +321,8 @@ val apply_to_hyp : named_context_val -> variable -> val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val val is_polymorphic : env -> Names.GlobRef.t -> bool +val is_template_polymorphic : env -> GlobRef.t -> bool +val is_type_in_type : env -> GlobRef.t -> bool open Retroknowledge (** functions manipulating the retroknowledge diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 18697d07e5..5515ff9767 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -68,7 +68,7 @@ type lft_constr_stack_elt = Zlapp of (lift * fconstr) array | Zlproj of Projection.Repr.t * lift | Zlfix of (lift * fconstr) * lft_constr_stack - | Zlcase of case_info * lift * fconstr * fconstr array + | Zlcase of case_info * lift * constr * constr array * fconstr subs and lft_constr_stack = lft_constr_stack_elt list let rec zlapp v = function @@ -102,7 +102,7 @@ let pure_stack lfts stk = let (lfx,pa) = pure_rec l a in (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,e),(l,pstk)) -> - (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk)) + (l,Zlcase(ci,l,p,br,e)::pstk)) in snd (pure_rec lfts stk) @@ -288,31 +288,13 @@ let conv_table_key infos k1 k2 cuniv = | RelKey n, RelKey n' when Int.equal n n' -> cuniv | _ -> raise NotConvertible -let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = - let rec cmp_rec pstk1 pstk2 cuniv = - match (pstk1,pstk2) with - | (z1::s1, z2::s2) -> - let cu1 = cmp_rec s1 s2 cuniv in - (match (z1,z2) with - | (Zlapp a1,Zlapp a2) -> - Array.fold_right2 f a1 a2 cu1 - | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> - if not (Projection.Repr.equal c1 c2) then - raise NotConvertible - else cu1 - | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> - let cu2 = f fx1 fx2 cu1 in - cmp_rec a1 a2 cu2 - | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) -> - if not (fmind ci1.ci_ind ci2.ci_ind) then - raise NotConvertible; - let cu2 = f (l1,p1) (l2,p2) cu1 in - Array.fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2 - | _ -> assert false) - | _ -> cuniv in - if compare_stack_shape stk1 stk2 then - cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv - else raise NotConvertible +exception IrregularPatternShape + +let rec skip_pattern n c = + if Int.equal n 0 then c + else match kind c with + | Lambda (_, _, c) -> skip_pattern (pred n) c + | _ -> raise IrregularPatternShape type conv_tab = { cnv_inf : clos_infos; @@ -611,10 +593,31 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | FProd _ | FEvar _), _ -> raise NotConvertible and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = - compare_stacks - (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv) - (eq_ind) - lft1 stk1 lft2 stk2 cuniv + let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in + let rec cmp_rec pstk1 pstk2 cuniv = + match (pstk1,pstk2) with + | (z1::s1, z2::s2) -> + let cu1 = cmp_rec s1 s2 cuniv in + (match (z1,z2) with + | (Zlapp a1,Zlapp a2) -> + Array.fold_right2 f a1 a2 cu1 + | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> + if not (Projection.Repr.equal c1 c2) then + raise NotConvertible + else cu1 + | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> + let cu2 = f fx1 fx2 cu1 in + cmp_rec a1 a2 cu2 + | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) -> + if not (eq_ind ci1.ci_ind ci2.ci_ind) then + raise NotConvertible; + let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in + convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2 + | _ -> assert false) + | _ -> cuniv in + if compare_stack_shape stk1 stk2 then + cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv + else raise NotConvertible and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = let lv1 = Array.length v1 in @@ -629,6 +632,22 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = fold 0 cuniv else raise NotConvertible +and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv = + (** Skip comparison of the pattern types. We know that the two terms are + living in a common type, thus this check is useless. *) + let fold n c1 c2 cuniv = match skip_pattern n c1, skip_pattern n c2 with + | (c1, c2) -> + let lft1 = el_liftn n lft1 in + let lft2 = el_liftn n lft2 in + let e1 = subs_liftn n e1 in + let e2 = subs_liftn n e2 in + ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv + | exception IrregularPatternShape -> + (** Might happen due to a shape invariant that is not enforced *) + ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv + in + Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv + let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 12f9592ab7..779e05ee0c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -194,6 +194,10 @@ let set_engagement c senv = let set_typing_flags c senv = { senv with env = Environ.set_typing_flags c senv.env } +let set_share_reduction b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with share_reduction = b } senv + (** Check that the engagement [c] expected by a library matches the current (initial) one *) let check_engagement env expected_impredicative_set = @@ -1190,7 +1194,7 @@ loaded by side-effect once and for all (like it is done in OCaml). Would this be correct with respect to undo's and stuff ? *) -let set_strategy e k l = { e with env = +let set_strategy k l e = { e with env = (Environ.set_oracle e.env (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) } diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 26fa91adbd..443b5cfd73 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -137,6 +137,7 @@ val add_constraints : (** Setting the type theory flavor *) val set_engagement : Declarations.engagement -> safe_transformer0 val set_typing_flags : Declarations.typing_flags -> safe_transformer0 +val set_share_reduction : bool -> safe_transformer0 (** {6 Interactive module functions } *) @@ -217,4 +218,4 @@ val register : val register_inline : Constant.t -> safe_transformer0 val set_strategy : - safe_environment -> Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_environment + Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0 |