DECLARE PLUGIN "coq-elpi.coercion"

{

open Elpi
open Elpi_plugin
open Coq_elpi_arg_syntax
open Coq_elpi_vernacular

let relevant = EConstr.ERelevance.relevant
let anonR = Context.make_annot Names.Name.Anonymous EConstr.ERelevance.irrelevant 
let nameR x = Context.make_annot (Names.Name.Name x) EConstr.ERelevance.irrelevant 
let annotR x = Context.make_annot x EConstr.ERelevance.irrelevant 
let build_expected_type env sigma expected =
  match expected with
  | Coercion.Type t -> sigma, t, false
  | Coercion.Product ->
    let (sigma, (source, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible in
    let (sigma, (target, _)) =
      let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (EConstr.annotR (Names.Name (Namegen.default_dependent_ident)) , source)) env in
      Evarutil.new_type_evar env sigma Evd.univ_flexible in
    sigma, EConstr.mkProd (annotR (Names.Name (Namegen.default_type_ident)), source, target), true
  | Coercion.Sort -> let (sigma, t) = Evarutil.new_Type sigma in sigma, t, true
let return s g t = Some (s,g,t)

let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
  let loc = API.Ast.Loc.initial "(unknown)" in
  let atts = [] in
  let sigma, expected, retype = build_expected_type env sigma expected in
  let sigma, goal = Evarutil.new_evar env sigma expected in
  let goal_evar, _ = EConstr.destEvar sigma goal in
  let query ~depth state =
    let state, (loc, q), gls =
      Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [v; inferred])
        ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in
    let state, qatts = atts2impl loc Summary.Stage.Interp ~depth state atts q in
    let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
    state, (loc, qatts), gls
  in
  match Interp.get_and_compile program with
  | None -> None
  | Some (cprogram, _) ->
    match Interp.run ~static_check:false cprogram (`Fun query) with
    | API.Execute.Success solution ->
      let gls = Evar.Set.singleton goal_evar in
      let sigma, _, _ = Coq_elpi_HOAS.solution2evd ~eta_contract_solution:false sigma solution gls in
      if Evd.is_defined sigma goal_evar then
        let t = if retype then Retyping.get_type_of env sigma goal else expected in
        return sigma goal t
      else
        None
    | API.Execute.NoMoreSteps
    | API.Execute.Failure -> None
    | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None

let add_coercion_hook =
  let coercion_hook_program = Summary.ref ~name:"elpi-coercion" None in
  let coercion_hook env sigma ~flags v ~inferred ~expected =
    match !coercion_hook_program with
    | None -> None
    | Some h -> elpi_coercion_hook h env sigma ~flags v ~inferred ~expected in
  let name = "elpi-coercion" in
  Coercion.register_hook ~name coercion_hook;
  let inCoercion =
    let cache program =
      coercion_hook_program := Some program;
      Coercion.activate_hook ~name in
    let open Libobject in
    declare_object
    @@ superglobal_object_nodischarge "ELPI-COERCION" ~cache ~subst:None in
  fun program -> Lib.add_leaf (inCoercion program)

}

VERNAC COMMAND EXTEND ElpiCoercion CLASSIFIED AS SIDEFF
| #[ atts = any_attribute ] [ "Elpi" "CoercionFallbackTactic" qualified_name(p) ] -> {
     let () = ignore_unknown_attributes atts in
     add_coercion_hook (snd p) }

END