diff --git a/doc/changelog/13-misc/17794-coercion_hook.rst b/doc/changelog/13-misc/17794-coercion_hook.rst new file mode 100644 index 0000000000000..f47c1ad333ff9 --- /dev/null +++ b/doc/changelog/13-misc/17794-coercion_hook.rst @@ -0,0 +1,5 @@ +- **Added:** + a hook in the coercion mechanism to enable programming coercions in + external metalanguages such as Ltac, Ltac2, Elpi or OCaml plugins + (`#17794 `_, + by Pierre Roux). diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 41e81f1e911f2..b1a84a7f1fec8 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -622,6 +622,13 @@ let lookup_reversible_path_to_common_point env sigma ~src_expected ~src_inferred in aux r +type hook = env -> evar_map -> flags:Evarconv.unify_flags -> constr -> + inferred:types -> expected:types -> (evar_map * constr) option +let hook = Summary.ref ~name:"coercion_hook" + (fun _ _ ~flags _ ~inferred ~expected -> None) +let get_hook () = !hook +let set_hook f = hook := f + let add_reverse_coercion env sigma v'_ty v_ty v' v = match Coqlib.lib_ref_opt "core.coercion.reverse_coercion" with | None -> sigma, v' @@ -657,7 +664,10 @@ let inh_coerce_to_fail ?(use_coercions=true) flags env sigma rigidonly v v_ty ta unify_leq_delay ~flags env sigma v'_ty target_type, v', trace with (Evarconv.UnableToUnify _ | Not_found) as exn -> let _, info = Exninfo.capture exn in - Exninfo.iraise (NoCoercion,info) + (* 3 if none of the above works, try hook *) + match !hook env sigma ~flags v ~inferred:v_ty ~expected:target_type with + | Some (sigma, r) -> (sigma, r, ReplaceCoe r) + | None -> Exninfo.iraise (NoCoercion,info) let default_flags_of env = default_flags_of TransparentState.full diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 8b35603dcb65f..9672a3e2969db 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -58,6 +58,10 @@ val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool -> resolve_tc:boo val inh_pattern_coerce_to : ?loc:Loc.t -> env -> cases_pattern -> inductive -> inductive -> cases_pattern +type hook = env -> evar_map -> flags:Evarconv.unify_flags -> constr -> + inferred:types -> expected:types -> (evar_map * constr) option +val get_hook : unit -> hook +val set_hook : hook -> unit type delayed_app_body