Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Ppopen CErrorsopen Utilopen Namesopen Constropen EConstropen Genredexpropen Patternopen Reductionopsopen Tacredopen RedFlags
let warn_vm_disabled = CWarnings.create ~name:"vm-compute-disabled" ~category:CWarnings.CoreCategories.bytecode_compiler (fun () -> strbrk "vm_compute disabled at configure time; falling back to cbv.")
(* call by value normalisation function using the virtual machine *)let cbv_vm env sigma c = if (Environ.typing_flags env).enable_VM then let ctyp = Retyping.get_type_of env sigma c in Vnorm.cbv_vm env sigma c ctyp else begin warn_vm_disabled (); compute env sigma c end
let warn_native_compute_disabled = CWarnings.create_in Nativeconv.w_native_disabled (fun () -> strbrk "native_compute disabled at configure time; falling back to vm_compute.")
let cbv_native env sigma c = if (Environ.typing_flags env).enable_native_compiler then let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c ctyp else (warn_native_compute_disabled (); cbv_vm env sigma c)
let { Goptions.get = simplIsCbn } = Goptions.declare_bool_option_and_ref ~key:["SimplIsCbn"] ~value:false ()
let set_strategy_one ref l = Global.set_strategy (Evaluable.to_kevaluable ref) l
let cache_strategy (_,str) = List.iter (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql) str
let subst_strategy (subs,(local,obj)) = local, List.Smart.map (fun (k,ql as entry) -> let ql' = List.Smart.map (Tacred.subst_evaluable_reference subs) ql in if ql==ql' then entry else (k,ql')) obj
let map_strategy f l = let l' = List.fold_right (fun (lev,ql) str -> let ql' = List.fold_right (fun q ql -> match f q with Some q' -> q' :: ql | None -> ql) ql [] in if List.is_empty ql' then str else (lev,ql')::str) l [] in if List.is_empty l' then None else Some (false,l')
let classify_strategy (local,_) = let open Libobject in if local then Dispose else Substitute
let disch_ref ref = match ref with | Evaluable.EvalConstRef c -> Some ref | Evaluable.EvalProjectionRef p -> let p = Global.discharge_proj_repr p in Some (Evaluable.EvalProjectionRef p) | Evaluable.EvalVarRef id -> if Global.is_in_section (GlobRef.VarRef id) then None else Some ref
let discharge_strategy (local,obj) = if local then None else map_strategy disch_ref obj
type strategy_obj = bool * (Conv_oracle.level * Evaluable.t list) list
let inStrategy : strategy_obj -> Libobject.obj = let open Libobject in declare_object {(default_object "STRATEGY") with cache_function = cache_strategy; load_function = (fun _ obj -> cache_strategy obj); subst_function = subst_strategy; discharge_function = discharge_strategy; classify_function = classify_strategy; }
let check_not_fully_opaque l ref = match ref, l with | Evaluable.EvalConstRef sp, Conv_oracle.Opaque -> () | Evaluable.EvalConstRef sp, _ -> if Environ.mem_constant sp (Global.env ()) && Declareops.is_opaque (Global.lookup_constant sp) (* FIXME *) then user_err (str "Cannot make" ++ spc () ++ Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque.") | _ -> ()
let set_strategy local str = List.iter (fun (l,refs) -> List.iter (check_not_fully_opaque l) refs) str; Lib.add_leaf (inStrategy (local,str))
(* Generic reduction: reduction functions used in reduction tactics *)
module User =struct
type ('raw, 'glb) user_red_spec = { ured_intern : Constrintern.ltac_sign -> 'raw -> 'glb; ured_subst : Mod_subst.substitution -> 'glb -> 'glb; ured_eval : 'glb -> e_reduction_function * cast_kind; ured_rprint : Environ.env -> Evd.evar_map -> 'raw -> Pp.t; ured_gprint : Environ.env -> Evd.evar_map -> 'glb -> Pp.t;}
type 'a spec = Spec : ('raw, 'glb) user_red_spec -> ('raw * 'glb) spec
module Dyn = Dyn.Make()
module Map = Dyn.Map(struct type 'a t = 'a spec end)
let map = ref Map.empty
type ('a, 'b) user_red = UserRed : ('a * 'b) Dyn.tag -> ('a, 'b) user_red
type 'a user_red_expr =| RawRed : ('a * 'b) Dyn.tag * 'a -> Genarg.rlevel user_red_expr| GlbRed : ('a * 'b) Dyn.tag * 'b -> Genarg.glevel user_red_expr
let create (type raw glb) name (red : (raw, glb) user_red_spec) = let tag : (raw * glb) Dyn.tag = Dyn.create name in let () = map := Map.add tag (Spec red) !map in UserRed tag
let make (type a b) (tag : (a, b) user_red) (v : a) : Genarg.rlevel user_red_expr = let UserRed tag = tag in RawRed (tag, v)
let get tag = let (Spec decl) = Map.find tag !map in decl
end
type 'a user_red_expr = 'a User.user_red_expr
type raw_red_expr = Genarg.rlevel user_red_expr Genredexpr.raw_red_exprtype glob_red_expr = Genarg.glevel user_red_expr Genredexpr.glob_red_exprtype red_expr = (constr, Evaluable.t, constr_pattern, int, Genarg.glevel user_red_expr) red_expr_gen
type red_expr_val = (constr, Evaluable.t, constr_pattern, int, strength * RedFlags.reds, Genarg.glevel user_red_expr) red_expr_gen0
let intern_user_red_expr ist usr = let User.RawRed (tag, v) = usr in let decl = User.get tag in User.GlbRed (tag, decl.User.ured_intern ist v)
let subst_user_red_expr subst usr = let User.GlbRed (tag, v) = usr in let decl = User.get tag in User.GlbRed (tag, decl.User.ured_subst subst v)
let eval_user_red_expr usr = let User.GlbRed (tag, v) = usr in let decl = User.get tag in decl.User.ured_eval v
let pr_raw_user_red_expr env sigma usr = let User.RawRed (tag, v) = usr in let decl = User.get tag in decl.User.ured_rprint env sigma v
let pr_glob_user_red_expr env sigma usr = let User.GlbRed (tag, v) = usr in let decl = User.get tag in decl.User.ured_gprint env sigma v
let make_flag_constant env = function | Evaluable.EvalVarRef id -> [fVAR id] | Evaluable.EvalConstRef sp -> begin match Structures.PrimitiveProjections.find_opt sp with | None -> [fCONST sp] | Some p -> [fCONST sp; fPROJ p] end | Evaluable.EvalProjectionRef p -> [fPROJ p; fCONST (Environ.projection_repr_constant env p)]
let make_flag env f = let red = no_red in let red = if f.rBeta then red_add red fBETA else red in let red = if f.rMatch then red_add red fMATCH else red in let red = if f.rFix then red_add red fFIX else red in let red = if f.rCofix then red_add red fCOFIX else red in let red = if f.rZeta then red_add red fZETA else red in let red = if f.rDelta then (* All but rConst *) let red = red_add red fDELTA in let red = red_add_transparent red (Conv_oracle.get_transp_state (Environ.oracle env)) in List.fold_right (fun v red -> red_sub_list red (make_flag_constant env v)) f.rConst red else (* Only rConst *) let red = red_add red fDELTA in List.fold_right (fun v red -> red_add_list red (make_flag_constant env v)) f.rConst red in f.rStrength, red
(* table of custom reductino fonctions, not synchronized, filled via ML calls to [declare_reduction] *)let reduction_tab = ref String.Map.empty
(* table of custom reduction expressions, synchronized, filled by command Declare Reduction *)let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
let declare_reduction s f = if String.Map.mem s !reduction_tab || String.Map.mem s (Summary.Ref.get red_expr_tab) then user_err (str "There is already a reduction expression of name " ++ str s ++ str ".") else reduction_tab := String.Map.add s f !reduction_tab
let check_custom = function | ExtraRedExpr s -> if not (String.Map.mem s !reduction_tab || String.Map.mem s (Summary.Ref.get red_expr_tab)) then user_err (str "Reference to undefined reduction expression " ++ str s ++ str ".") |_ -> ()
let decl_red_expr s e = if String.Map.mem s !reduction_tab || String.Map.mem s (Summary.Ref.get red_expr_tab) then user_err (str "There is already a reduction expression of name " ++ str s ++ str ".") else begin check_custom e; let open Summary.Ref in red_expr_tab := String.Map.add s e !red_expr_tab end
let out_arg = function | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") | Locus.ArgArg x -> x
let check_occurrences occs = match occs with | Locus.OnlyOccurrences (n::_ as nl) when n < 0 -> Locus.AllOccurrencesBut (List.map abs nl) | Locus.OnlyOccurrences nl when List.exists (fun n -> n < 0) nl -> CErrors.user_err Pp.(str "Illegal negative occurrence number.") | Locus.OnlyOccurrences _ | Locus.AllOccurrencesBut _ | Locus.NoOccurrences | Locus.AllOccurrences | Locus.AtLeastOneOccurrence -> occs
let out_occurrences occs = let occs = Locusops.occurrences_map (List.map out_arg) occs in check_occurrences occs
let out_with_occurrences (occs,c) = (out_occurrences occs, c)
let e_red f env evm c = evm, f env evm c
let contextualize f = function | Some (occs,c) -> let l = check_occurrences occs in fun env sigma r -> let b,c = match c with | Inl r -> true,PRef (global_of_evaluable_reference env r) | Inr c -> false,c in sigma, contextually b (l,c) (fun _ -> f) env sigma r | None -> e_red f
let warn_simpl_unfolding_modifiers = CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:CWarnings.CoreCategories.tactics (fun () -> Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.")
let rec eval_red_expr env = function| Simpl (f, o) -> let () = if not (simplIsCbn () || List.is_empty f.rConst) then warn_simpl_unfolding_modifiers () in let f = if simplIsCbn () then make_flag env f else f.rStrength, RedFlags.all (* dummy *) in Simpl (f, o)| Cbv f -> Cbv (make_flag env f)| Cbn f -> Cbn (make_flag env f)| Lazy f -> Lazy (make_flag env f)| ExtraRedExpr s -> let open Summary.Ref in begin match String.Map.find s !red_expr_tab with | e -> eval_red_expr env e | exception Not_found -> ExtraRedExpr s (* delay to runtime interpretation *) end| (Red | Hnf | Unfold _ | Fold _ | Pattern _ | CbvVm _ | CbvNative _ | UserRed _) as e -> e
let red_product_exn env sigma c = match red_product env sigma c with | None -> user_err Pp.(str "No head constant to reduce.") | Some c -> c
let pattern_occs occs env sigma c = match pattern_occs occs env sigma c with| NoChange -> sigma, c| Changed (sigma, c) -> sigma, c
let reduction_of_red_expr_val = function | Red -> (e_red red_product_exn, DEFAULTcast) | Hnf -> (e_red hnf_constr,DEFAULTcast) | Simpl ((w,f),o) -> let am = match w, simplIsCbn () with | Norm, true -> Cbn.norm_cbn f | Norm, false -> simpl | Head, true -> Cbn.whd_cbn f | Head, false -> whd_simpl in (contextualize am o,DEFAULTcast) | Cbv (Norm, f) -> (e_red (cbv_norm_flags ~strong:true f),DEFAULTcast) | Cbv (Head, f) -> (e_red (cbv_norm_flags ~strong:false f),DEFAULTcast) | Cbn (w,f) -> let cbn = match w with Norm -> Cbn.norm_cbn | Head -> Cbn.whd_cbn in (e_red (cbn f), DEFAULTcast) | Lazy (w,f) -> let redf = match w with Norm -> clos_norm_flags | Head -> clos_whd_flags in (e_red (redf f),DEFAULTcast) | Unfold ubinds -> (e_red (unfoldn (List.map (on_fst check_occurrences) ubinds)),DEFAULTcast) | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) | Pattern lp -> (pattern_occs (List.map (on_fst check_occurrences) lp),DEFAULTcast) | ExtraRedExpr s -> (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast) with Not_found -> user_err (str "Unknown user-defined reduction \"" ++ str s ++ str "\".")) | CbvVm o -> (contextualize cbv_vm o, VMcast) | CbvNative o -> (contextualize cbv_native o, NATIVEcast) | UserRed usr -> eval_user_red_expr usr
let reduction_of_red_expr env r = reduction_of_red_expr_val (eval_red_expr env r)
(* Possibly equip a reduction with the occurrences mentioned in an occurrence clause *)
let error_illegal_clause () = CErrors.user_err Pp.(str "\"at\" clause not supported in presence of an occurrence clause.")
let error_multiple_patterns () = CErrors.user_err Pp.(str "\"at\" clause in occurences not supported with multiple patterns or references.")
let error_illegal_non_atomic_clause () = CErrors.user_err Pp.(str "\"at\" clause not supported in presence of a non atomic \"in\" clause.")
let error_at_in_occurrences_not_supported () = CErrors.user_err Pp.(str "\"at\" clause not supported for this reduction tactic.")
let bind_red_expr_occurrences occs nbcl redexp = let open Locus in let has_at_clause = function | Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l | Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l | Simpl (_,Some (occl,_)) -> occl != AllOccurrences | _ -> false in if occs == AllOccurrences then if nbcl > 1 && has_at_clause redexp then error_illegal_non_atomic_clause () else redexp else match redexp with | Unfold (_::_::_) -> error_multiple_patterns () | Unfold [(occl,c)] -> if occl != AllOccurrences then error_illegal_clause () else Unfold [(occs,c)] | Pattern (_::_::_) -> error_multiple_patterns () | Pattern [(occl,c)] -> if occl != AllOccurrences then error_illegal_clause () else Pattern [(occs,c)] | Simpl (f,Some (occl,c)) -> if occl != AllOccurrences then error_illegal_clause () else Simpl (f,Some (occs,c)) | CbvVm (Some (occl,c)) -> if occl != AllOccurrences then error_illegal_clause () else CbvVm (Some (occs,c)) | CbvNative (Some (occl,c)) -> if occl != AllOccurrences then error_illegal_clause () else CbvNative (Some (occs,c)) | Red | Hnf | Cbv _ | Lazy _ | Cbn _ | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None | UserRed _ -> error_at_in_occurrences_not_supported () | Unfold [] | Pattern [] -> assert false
let reduction_of_red_expr_val ?occs r = let r = match occs with | None -> r | Some (occs, nbcl) -> bind_red_expr_occurrences occs nbcl r in reduction_of_red_expr_val r
let subst_mps subst c = EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
let subst_red_expr subs = let env = Global.env () in let sigma = Evd.from_env env in Redops.map_red_expr_gen (subst_mps subs) (Tacred.subst_evaluable_reference subs) (Patternops.subst_pattern env sigma subs) (subst_user_red_expr subs)
let inReduction : bool * string * red_expr -> Libobject.obj = let open Libobject in declare_object {(default_object "REDUCTION") with cache_function = (fun (_,s,e) -> decl_red_expr s e); load_function = (fun _ (_,s,e) -> decl_red_expr s e); subst_function = (fun (subs,(b,s,e)) -> b,s,subst_red_expr subs e); classify_function = (fun ((b,_,_)) -> if b then Dispose else Substitute) }
let declare_red_expr locality s expr = Lib.add_leaf (inReduction (locality,s,expr))
let make0 ?dyn name = let wit = Genarg.make0 name in let () = Geninterp.register_val0 wit dyn in wit
let wit_red_expr = make0 "redexpr"
module Intern = struct open CAst open Constrexpr open Libnames
let evalref_of_globref ?loc r = let () = (* only dump section variables not proof context variables (broken if variables got renamed) *) let is_proof_variable = match r with | GlobRef.VarRef x -> (try ignore (Global.lookup_named x); false with Not_found -> true) | _ -> false in if not is_proof_variable then Dumpglob.add_glob ?loc r in Tacred.evaluable_of_global_reference ?loc r
type ('constr,'ref,'pat) intern_env = { strict_check : bool; local_ref : qualid -> 'ref option; global_ref : ?short:lident -> Evaluable.t -> 'ref; intern_constr : constr_expr -> 'constr; ltac_sign : Constrintern.ltac_sign; intern_pattern : constr_expr -> 'pat; pattern_of_glob : Glob_term.glob_constr -> 'pat; }
let intern_global_reference ist qid = match ist.local_ref qid with | Some v -> v | None -> let r = try Smartlocate.locate_global_with_alias ~head:true qid with | Not_found as exn -> if not ist.strict_check && qualid_is_ident qid then let id = qualid_basename qid in GlobRef.VarRef id else let _, info = Exninfo.capture exn in Nametab.error_global_not_found ~info qid in let short = if qualid_is_ident qid && not ist.strict_check then Some (make ?loc:qid.CAst.loc @@ qualid_basename qid) else None in let r = evalref_of_globref ?loc:qid.loc r in ist.global_ref ?short r
let intern_evaluable ist = function | {v=AN qid} -> intern_global_reference ist qid | {v=ByNotation (ntn,sc);loc} -> let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in let r = Notation.interp_notation_as_global_reference ?loc ~head:true check ntn sc in let r = evalref_of_globref ?loc r in ist.global_ref r
let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let interp_ref r = try Inl (intern_evaluable ist r) with e when CErrors.noncritical e -> (* Compatibility. In practice, this means that the code above is useless. Still the idea of having either an evaluable ref or a pattern seems interesting, with "head" reduction in case of an evaluable ref, and "strong" reduction in the subterm matched when a pattern *) let r = match r with | {CAst.v=AN r} -> r | {loc} -> (qualid_of_path ?loc (Nametab.path_of_global (Smartlocate.smart_global r))) in let loc = r.loc in let c = Constrintern.interp_reference ist.ltac_sign r in match DAst.get c with | GRef (r,None) -> let r = evalref_of_globref ?loc r in Inl (ist.global_ref r) | GVar id -> let r = evalref_of_globref (GlobRef.VarRef id) in Inl (ist.global_ref r) | _ -> Inr (ist.pattern_of_glob c) in let p = match p with | Inl r -> interp_ref r | Inr { v = CAppExpl((r,None),[]) } -> (* We interpret similarly @ref and ref *) interp_ref (make @@ AN r) | Inr c -> Inr (ist.intern_pattern c) in (l, p)
let intern_constr_with_occurrences ist (l,c) = (l,ist.intern_constr c)
let intern_flag ist red = { red with rConst = List.map (intern_evaluable ist) red.rConst }
let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
let intern_red_expr ist = function | Unfold l -> Unfold (List.map (intern_unfold ist) l) | Fold l -> Fold (List.map ist.intern_constr l) | Cbv f -> Cbv (intern_flag ist f) | Cbn f -> Cbn (intern_flag ist f) | Lazy f -> Lazy (intern_flag ist f) | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l) | Simpl (f,o) -> Simpl (intern_flag ist f, Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | (Red | Hnf | ExtraRedExpr _ as r ) -> r | UserRed usr -> UserRed (intern_user_red_expr ist.ltac_sign usr)
let intern_constr env c = Constrintern.intern_gen WithoutTypeConstraint ~strict_check:true env (Evd.from_env env) c
let intern_pattern env c = Constrintern.intern_gen WithoutTypeConstraint ~strict_check:true ~pattern_mode:true env (Evd.from_env env) c
let from_env env = { strict_check = true; local_ref = (fun _ -> None); global_ref = (fun ?short:_ r -> r); intern_constr = intern_constr env; ltac_sign = Constrintern.empty_ltac_sign; pattern_of_glob = (fun c -> c); intern_pattern = intern_pattern env; }
end
module Interp = struct
type ('constr,'evref,'pat,'usr) interp_env = { interp_occurrence_var : lident -> int list; interp_constr : Environ.env -> Evd.evar_map -> 'constr -> Evd.evar_map * EConstr.constr; interp_constr_list : Environ.env -> Evd.evar_map -> 'constr -> Evd.evar_map * EConstr.constr list; interp_evaluable : Environ.env -> Evd.evar_map -> 'evref -> Evaluable.t; interp_pattern : Environ.env -> Evd.evar_map -> 'pat -> constr_pattern; interp_evaluable_or_pattern : Environ.env -> Evd.evar_map -> 'evref -> (Evaluable.t, constr_pattern) Util.union; }
let interp_occurrences ist occs = let open Locus in let map = function | ArgArg x -> [x] | ArgVar lid -> ist.interp_occurrence_var lid in Locusops.occurrences_map (List.concat_map map) occs
let interp_constr_with_occurrences ist env sigma (occs,c) = let (sigma,c_interp) = ist.interp_constr env sigma c in sigma , (interp_occurrences ist occs, c_interp)
let interp_evaluable ist env sigma r = ist.interp_evaluable env sigma r
let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, p) = let p = match p with | Inr p -> Inr (ist.interp_pattern env sigma p) | Inl r -> ist.interp_evaluable_or_pattern env sigma r in interp_occurrences ist occs, p
let interp_unfold ist env sigma (occs,qid) = (interp_occurrences ist occs,interp_evaluable ist env sigma qid)
let interp_flag ist env sigma red = { red with rConst = List.map (interp_evaluable ist env sigma) red.rConst }
let interp_red_expr ist env sigma = function | Unfold l -> sigma , Unfold (List.map (interp_unfold ist env sigma) l) | Fold l -> let (sigma,l_interp) = List.fold_left_map (ist.interp_constr_list env) sigma l in sigma , Fold (List.flatten l_interp) | Cbv f -> sigma , Cbv (interp_flag ist env sigma f) | Cbn f -> sigma , Cbn (interp_flag ist env sigma f) | Lazy f -> sigma , Lazy (interp_flag ist env sigma f) | Pattern l -> let (sigma,l_interp) = Evd.Monad.List.map_right (fun c sigma -> interp_constr_with_occurrences ist env sigma c) l sigma in sigma , Pattern l_interp | Simpl (f,o) -> sigma , Simpl (interp_flag ist env sigma f, Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) | CbvVm o -> sigma , CbvVm (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) | CbvNative o -> sigma , CbvNative (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) | (Red | Hnf | ExtraRedExpr _ | UserRed _ as r) -> sigma , r
let interp_constr env sigma c = let flags = Pretyping.all_and_fail_flags in Pretyping.understand_ltac flags env sigma Glob_ops.empty_lvar WithoutTypeConstraint c
let interp_constr_list env sigma c = let sigma, c = interp_constr env sigma c in sigma, [c]
let interp_pattern env sigma c = let flags = { Pretyping.no_classes_no_fail_inference_flags with expand_evars = false } in let sigma, c = Pretyping.understand_ltac flags env sigma Glob_ops.empty_lvar WithoutTypeConstraint c in Patternops.legacy_bad_pattern_of_constr env sigma c
let without_ltac = { interp_occurrence_var = (fun lid -> user_err ?loc:lid.loc (str "Unbound variable " ++ Id.print lid.v ++ str ".")); interp_constr; interp_constr_list; interp_evaluable = (fun _ _ x -> x); interp_pattern; interp_evaluable_or_pattern = (fun _ _ r -> Inl r); }
end
let interp_redexp_no_ltac env sigma r = let r = Intern.(intern_red_expr (from_env env) r) in Interp.(interp_red_expr without_ltac) env sigma r