DECLARE PLUGIN "coq-elpi.cs"

{

open Elpi
open Elpi_plugin
open Coq_elpi_arg_syntax
open Coq_elpi_vernacular

let elpi_cs_hook program env sigma ((proji, u), params1, c1) (t2, args2) =
	  let loc = API.Ast.Loc.initial "(unknown)" in
	  let atts = [] in
     let rhs = Reductionops.Stack.zip sigma (t2, Reductionops.Stack.append_app_list args2 Reductionops.Stack.empty) in
     let sigma, (goal_ty, _) = Evarutil.new_type_evar env sigma Evd.UnivRigid in
	  let sigma, goal = Evarutil.new_evar env sigma goal_ty in
	  let goal_evar, _ = EConstr.destEvar sigma goal in
    let nparams = Structures.Structure.projection_nparams proji in
	  let query ~depth state =
		 let state, (loc, q), gls =
      let lhs = match params1 with
        | Some params1 -> EConstr.mkApp (EConstr.mkConstU (proji, u), Array.of_list params1)
        | None -> EConstr.mkConstU (proji, u) in
			Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [lhs; rhs])
			  ~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, _) ->
		 begin 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 constant = EConstr.to_constr sigma goal in
			  let args_goal, t = Reduction.whd_decompose_lambda env constant in
			  let args_type = List.rev_map Context.Rel.Declaration.get_type args_goal in
			  let args_type = List.map EConstr.of_constr args_type in
           let args = snd (Constr.decompose_app_list t) in
           let params, projs = CList.chop nparams args in
           let i = Structures.Structure.projection_number env proji in
           let lhs = List.nth projs i in
			  let lhs = EConstr.of_constr lhs in
			  let _, sk1 = EConstr.decompose_app sigma lhs in
			  let open Structures.CanonicalSolution in
			  Some (sigma, {
				 constant = EConstr.of_constr constant;
				 abstractions_ty = args_type;
				 body = lhs;
				 nparams;
				 params = List.map EConstr.of_constr params;
				 cvalue_abstraction = None;
				 cvalue_arguments = Array.to_list sk1})
			else None
		 | API.Execute.NoMoreSteps
		 | API.Execute.Failure -> None
		 end

open Elpi
open Elpi_plugin
open Coq_elpi_arg_syntax
open Coq_elpi_vernacular

[%%if coq = "8.20"]
let adapt_hook f : Evarconv.hook = fun env sigma (s,l,t) x -> f env sigma (s,Some l,t) x
[%%else]
let adapt_hook f : Evarconv.hook = f
[%%endif]

let add_cs_hook =
  let cs_hook_program = Summary.ref ~name:"elpi-cs" None in
  let cs_hook env sigma proj pat =
    match !cs_hook_program with
    | None -> None
    | Some h -> elpi_cs_hook h env sigma proj pat in
  let name = "elpi-cs" in
  Evarconv.register_hook ~name (adapt_hook cs_hook);
  let inCs =
    let cache program =
      cs_hook_program := Some program;
      Evarconv.activate_hook ~name in
    let open Libobject in
    declare_object
    @@ superglobal_object_nodischarge "ELPI-CS" ~cache ~subst:None in
  fun program -> Lib.add_leaf (inCs program)

}

VERNAC COMMAND EXTEND ElpiCS CLASSIFIED AS SIDEFF
| #[ atts = any_attribute ] [ "Elpi" "CS" qualified_name(p) ] -> {
     let () = ignore_unknown_attributes atts in
     add_cs_hook (snd p) }
END
