CS app

.gitignore

@@ -48,3 +48,4 @@ META
 apps/coercion/src/coq_elpi_coercion_hook.ml
 .filestoinstall
 apps/tc/src/coq_elpi_tc_hook.ml
+apps/cs/src/coq_elpi_cs_hook.ml

Makefile

@@ -21,7 +21,7 @@ export ELPIDIR
 
 DEPS=$(ELPIDIR)/elpi.cmxa $(ELPIDIR)/elpi.cma
 
-APPS=$(addprefix apps/, derive eltac NES locker coercion tc)
+APPS=$(addprefix apps/, derive eltac NES locker coercion cs tc)
 
 ifeq "$(COQ_ELPI_ALREADY_INSTALLED)" ""
 DOCDEP=build

_CoqProject

@@ -29,6 +29,11 @@
 -R apps/coercion/tests          elpi.apps.tc.coercion
 -I apps/coercion/src
 
+# CS
+-R apps/cs/theories       elpi.apps.cs
+-R apps/cs/tests          elpi.apps.tc.cs
+-I apps/cs/src
+
 # Type classes
 -R apps/tc/theories       elpi.apps.tc
 -R apps/tc/tests          elpi.apps.tc.tests

apps/cs/Makefile

@@ -0,0 +1,40 @@
+# detection of coq
+ifeq "$(COQBIN)" ""
+COQBIN := $(shell which coqc >/dev/null 2>&1 && dirname `which coqc`)
+endif
+ifeq "$(COQBIN)" ""
+$(error Coq not found, make sure it is installed in your PATH or set COQBIN)
+else
+$(info Using coq found in $(COQBIN), from COQBIN or PATH)
+endif
+export COQBIN := $(COQBIN)/
+
+all: build test
+
+build: Makefile.coq
+	@$(MAKE) --no-print-directory -f Makefile.coq
+
+test: Makefile.test.coq
+	@$(MAKE) --no-print-directory -f Makefile.test.coq
+
+theories/%.vo: force
+	@$(MAKE) --no-print-directory -f Makefile.coq $@
+tests/%.vo: force build Makefile.test.coq
+	@$(MAKE) --no-print-directory -f Makefile.test.coq $@
+examples/%.vo: force build Makefile.test.coq
+	@$(MAKE) --no-print-directory -f Makefile.test.coq $@
+
+Makefile.coq Makefile.coq.conf: _CoqProject
+	@$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq
+	@$(MAKE) --no-print-directory -f Makefile.coq .merlin
+Makefile.test.coq Makefile.test.coq.conf: _CoqProject.test
+	@$(COQBIN)/coq_makefile -f _CoqProject.test -o Makefile.test.coq
+
+clean: Makefile.coq Makefile.test.coq
+	@$(MAKE) -f Makefile.coq $@
+	@$(MAKE) -f Makefile.test.coq $@
+
+.PHONY: force all build test
+
+install:
+	@$(MAKE) -f Makefile.coq $@

apps/cs/Makefile.coq.local

@@ -0,0 +1,10 @@
+CAMLPKGS+= -package coq-elpi.elpi
+
+ifeq "$(shell which cygpath >/dev/null 2>&1)" ""
+OCAMLFINDSEP=:
+else
+OCAMLFINDSEP=;
+endif
+
+OCAMLPATH:=../../src/$(OCAMLFINDSEP)$(OCAMLPATH)
+export OCAMLPATH

apps/cs/README.md

@@ -0,0 +1,44 @@
+# Canonical solution
+
+The `canonical_solution` app enables to program Coq canonical structure solutions in Elpi.
+
+This app is experimental.
+
+## The cs predicate
+
+The `cs` predicate lives in the database `cs.db`
+
+```elpi
+% predicate [cs Ctx Lhs Rhs] used to unify Lhs with Rhs, with
+% - [Ctx] is the context
+% - [Lhs] and [Rhs] are the terms to unify
+:index (0 6 6)
+pred cs i:goal-ctx, o:term, o:term.
+```
+
+By addings rules for this predicate one can recover from a CS instance search failure
+error, that is when `Lhs` and `Rhs` are not unifiable using a canonical structure registered
+by Coq.
+
+## Simple example of canonical solution
+
+This example declares a structure `S` with a projection `sort` and declares
+a canonical solution for `nat` in `S`.
+
+```coq
+From elpi.apps Require Import cs.
+From Coq Require Import Bool.
+
+Structure S : Type :=
+  { sort :> Type }.
+
+Elpi Accumulate cs.db lp:{{
+
+cs _ {{ sort lp:Sol }} {{ nat }} :-
+  Sol = {{ Build_S nat }}.
+
+}}.
+Elpi Typecheck canonical_solution.
+
+Check eq_refl _ : (sort _) = nat.
+```

apps/cs/_CoqProject

@@ -0,0 +1,15 @@
+# Hack to see Coq-Elpi even if it is not installed yet
+-Q ../../theories elpi
+-I ../../src
+-docroot elpi.apps
+
+-R theories   elpi.apps
+
+src/evarconv_hacked.ml
+src/coq_elpi_cs_hook.mlg
+src/elpi_cs_plugin.mlpack
+
+-I src/
+src/META.coq-elpi-cs
+
+theories/cs.v

apps/cs/_CoqProject.test

@@ -0,0 +1,11 @@
+# Hack to see Coq-Elpi even if it is not installed yet
+-Q ../../theories elpi
+-I ../../src
+-docroot elpi.apps
+
+-R theories elpi.apps
+-R tests    elpi.apps.cs.tests
+
+tests/test_cs.v
+
+-I src

apps/cs/src/META.coq-elpi-cs

@@ -0,0 +1,10 @@
+
+package "plugin" (
+  directory = "."
+  requires = "coq-core.plugins.ltac coq-elpi.elpi"
+  archive(byte) = "elpi_cs_plugin.cma"
+  archive(native) = "elpi_cs_plugin.cmxa"
+  plugin(byte) = "elpi_cs_plugin.cma"
+  plugin(native) = "elpi_cs_plugin.cmxs"
+)
+directory = "."

apps/cs/src/coq_elpi_cs_hook.mlg

@@ -0,0 +1,80 @@
+DECLARE PLUGIN "coq-elpi-cs.plugin"
+
+{
+
+open Elpi
+open Elpi_plugin
+open Coq_elpi_arg_syntax
+open Coq_elpi_vernacular
+module Evarconv = Evarconv
+module Evarconv_hacked = Evarconv_hacked
+
+
+let elpi_cs_hook program env sigma lhs rhs =
+  let (lhead, largs) = EConstr.decompose_app sigma lhs in
+  let (rhead, rargs) = EConstr.decompose_app sigma rhs in
+  if (EConstr.isConst sigma lhead && Structures.Structure.is_projection (fst (EConstr.destConst sigma lhead))) || 
+	 (EConstr.isConst sigma rhead && Structures.Structure.is_projection (fst (EConstr.destConst sigma rhead)))
+  then begin
+	  let loc = API.Ast.Loc.initial "(unknown)" in
+	  let atts = [] in
+	  (*let sigma, ty = Typing.type_of env sigma lhs in*)
+	  let sigma, (ty, _) = Evarutil.new_type_evar env sigma Evd.univ_flexible in
+	  let { Coqlib.eq } = Coqlib.build_coq_eq_data () in
+	  let sigma, eq = EConstr.fresh_global env sigma eq in
+	  let t = EConstr.mkApp (eq,[|ty;lhs;rhs|]) in
+	  let sigma, goal = Evarutil.new_evar env sigma t 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 [])
+			  ~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 sigma solution gls in
+			let ty_evar, _ = EConstr.destEvar sigma ty in
+			  Some (Evd.remove (Evd.remove sigma ty_evar) goal_evar)
+		 | API.Execute.NoMoreSteps
+		 | API.Execute.Failure -> None
+    | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None
+  end
+  else None
+
+let add_cs_hook =
+  let cs_hook_program = Summary.ref ~name:"elpi-cs" None in
+  let cs_hook env sigma proj pat =
+	Feedback.msg_info (Pp.str "run");
+    match !cs_hook_program with
+    | None -> None
+    | Some h -> elpi_cs_hook h env sigma proj pat in
+  let name = "elpi-cs" in
+  Evarconv_hacked.register_hook ~name cs_hook;
+  let inCs =
+    let cache program =
+      cs_hook_program := Some program;
+	Feedback.msg_info (Pp.str "activate");
+
+      Evarconv_hacked.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" "CSFallbackTactic" qualified_name(p) ] -> {
+     let () = ignore_unknown_attributes atts in
+     add_cs_hook (snd p) }
+| #[ atts = any_attribute ] [ "Elpi" "Override" "CS" qualified_name(p) ] -> {
+     Evarconv.set_evar_conv Evarconv_hacked.evar_conv_x }
+
+END

apps/cs/src/elpi_cs_plugin.mlpack

@@ -0,0 +1,2 @@
+Evarconv_hacked
+Coq_elpi_cs_hook