|
| 1 | +DECLARE PLUGIN "coq-elpi-cs.plugin" |
| 2 | + |
| 3 | +{ |
| 4 | + |
| 5 | +open Elpi |
| 6 | +open Elpi_plugin |
| 7 | +open Coq_elpi_arg_syntax |
| 8 | +open Coq_elpi_vernacular |
| 9 | +module Evarconv = Evarconv |
| 10 | +module Evarconv_hacked = Evarconv_hacked |
| 11 | + |
| 12 | + |
| 13 | +let elpi_cs_hook program env sigma lhs rhs = |
| 14 | + let (lhead, largs) = EConstr.decompose_app sigma lhs in |
| 15 | + let (rhead, rargs) = EConstr.decompose_app sigma rhs in |
| 16 | + if (EConstr.isConst sigma lhead && Structures.Structure.is_projection (fst (EConstr.destConst sigma lhead))) || |
| 17 | + (EConstr.isConst sigma rhead && Structures.Structure.is_projection (fst (EConstr.destConst sigma rhead))) |
| 18 | + then begin |
| 19 | + let loc = API.Ast.Loc.initial "(unknown)" in |
| 20 | + let atts = [] in |
| 21 | + (*let sigma, ty = Typing.type_of env sigma lhs in*) |
| 22 | + let sigma, (ty, _) = Evarutil.new_type_evar env sigma Evd.univ_flexible in |
| 23 | + let { Coqlib.eq } = Coqlib.build_coq_eq_data () in |
| 24 | + let sigma, eq = EConstr.fresh_global env sigma eq in |
| 25 | + let t = EConstr.mkApp (eq,[|ty;lhs;rhs|]) in |
| 26 | + let sigma, goal = Evarutil.new_evar env sigma t in |
| 27 | + let goal_evar, _ = EConstr.destEvar sigma goal in |
| 28 | + let query ~depth state = |
| 29 | + let state, (loc, q), gls = |
| 30 | + Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve []) |
| 31 | + ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in |
| 32 | + let state, qatts = atts2impl loc Summary.Stage.Interp ~depth state atts q in |
| 33 | + let state = API.State.set Coq_elpi_builtins.tactic_mode state true in |
| 34 | + state, (loc, qatts), gls |
| 35 | + in |
| 36 | + match Interp.get_and_compile program with |
| 37 | + | None -> None |
| 38 | + | Some (cprogram, _) -> |
| 39 | + match Interp.run ~static_check:false cprogram (`Fun query) with |
| 40 | + | API.Execute.Success solution -> |
| 41 | + let gls = Evar.Set.singleton goal_evar in |
| 42 | + let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in |
| 43 | + let ty_evar, _ = EConstr.destEvar sigma ty in |
| 44 | + Some (Evd.remove (Evd.remove sigma ty_evar) goal_evar) |
| 45 | + | API.Execute.NoMoreSteps |
| 46 | + | API.Execute.Failure -> None |
| 47 | + | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None |
| 48 | + end |
| 49 | + else None |
| 50 | + |
| 51 | +let add_cs_hook = |
| 52 | + let cs_hook_program = Summary.ref ~name:"elpi-cs" None in |
| 53 | + let cs_hook env sigma proj pat = |
| 54 | + Feedback.msg_info (Pp.str "run"); |
| 55 | + match !cs_hook_program with |
| 56 | + | None -> None |
| 57 | + | Some h -> elpi_cs_hook h env sigma proj pat in |
| 58 | + let name = "elpi-cs" in |
| 59 | + Evarconv_hacked.register_hook ~name cs_hook; |
| 60 | + let inCs = |
| 61 | + let cache program = |
| 62 | + cs_hook_program := Some program; |
| 63 | + Feedback.msg_info (Pp.str "activate"); |
| 64 | + |
| 65 | + Evarconv_hacked.activate_hook ~name in |
| 66 | + let open Libobject in |
| 67 | + declare_object |
| 68 | + @@ superglobal_object_nodischarge "ELPI-CS" ~cache ~subst:None in |
| 69 | + fun program -> Lib.add_leaf (inCs program) |
| 70 | + |
| 71 | +} |
| 72 | + |
| 73 | +VERNAC COMMAND EXTEND ElpiCS CLASSIFIED AS SIDEFF |
| 74 | +| #[ atts = any_attribute ] [ "Elpi" "CSFallbackTactic" qualified_name(p) ] -> { |
| 75 | + let () = ignore_unknown_attributes atts in |
| 76 | + add_cs_hook (snd p) } |
| 77 | +| #[ atts = any_attribute ] [ "Elpi" "Override" "CS" qualified_name(p) ] -> { |
| 78 | + Evarconv.set_evar_conv Evarconv_hacked.evar_conv_x } |
| 79 | + |
| 80 | +END |
0 commit comments