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 000000000000..f47c1ad333ff --- /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 41e81f1e911f..6fe035977d55 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -622,6 +622,30 @@ 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 all_hooks = ref (CString.Map.empty : hook CString.Map.t) + +let register_hook ~name ?(override=false) h = + if not override && CString.Map.mem name !all_hooks then + CErrors.anomaly ~label:"Coercion.register_hook" + Pp.(str "Hook already registered: \"" ++ str name ++ str "\"."); + all_hooks := CString.Map.add name h !all_hooks + +let active_hooks = Summary.ref ~name:"coercion_hooks" ([] : string list) + +let deactivate_hook ~name = + active_hooks := List.filter (fun s -> not (String.equal s name)) !active_hooks + +let activate_hook ~name = + assert (CString.Map.mem name !all_hooks); + deactivate_hook ~name; + active_hooks := name :: !active_hooks + +let active_hooks () = + List.map (fun name -> CString.Map.get name !all_hooks) !active_hooks + 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 +681,16 @@ 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 *) + let hook_res = + List.fold_left + (fun r h -> + if r <> None then r else + h env sigma ~flags v ~inferred:v_ty ~expected:target_type) + None (active_hooks ()) in + match hook_res 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 8b35603dcb65..12371a97ba09 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -58,6 +58,25 @@ 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 + +(** A plugin can override the coercion mechanism by registering a hook here. + Note that these hooks will only be trigerred when no direct or reversible + coercion applies. + Newly registered hooks are not active by default, see [activate_hook] below. + The same hook cannot be registered twice, except if [override] is [true]. + Beware that this addition is not persistent, it is up to the plugin to use + libobject if needed. *) +val register_hook : name:string -> ?override:bool -> hook -> unit + +(** Activate a previously registered hook. + Most recently activated hooks are tried first. *) +val activate_hook : name:string -> unit + +(** Deactivate a hook. If the hook wasn't registered/active, + this does nothing. *) +val deactivate_hook : name:string -> unit type delayed_app_body