TC solver 2

.gitignore

@@ -46,4 +46,5 @@ META
 *.cache
 
 apps/coercion/src/coq_elpi_coercion_hook.ml
-.filestoinstall
+.filestoinstall
+apps/tc/src/coq_elpi_tc_hook.ml

Makefile

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

_CoqProject

@@ -8,23 +8,42 @@
 -Q tests    elpi.tests
 -Q elpi     elpi
 
+# Derive
 -R apps/derive/theories elpi.apps
 -R apps/derive/tests    elpi.apps.derive.tests
 -R apps/derive/examples elpi.apps.derive.examples
+
+# NES
 -R apps/NES/theories elpi.apps
 -R apps/NES/tests    elpi.apps.NES.tests
 -R apps/NES/examples elpi.apps.NES.examples
+
+# Eltac
 -R apps/eltac/theories elpi.apps.eltac
 -R apps/eltac/tests    elpi.apps.eltac.tests
 -R apps/eltac/examples elpi.apps.eltac.examples
--R apps/coercion/theories elpi.apps.coercion
 
+# Coercion
+-R apps/coercion/theories       elpi.apps.coercion
+-R apps/coercion/tests          elpi.apps.tc.coercion
+-I apps/coercion/src
+
+# Type classes
+-R apps/tc/theories       elpi.apps
+-R apps/tc/tests          elpi.apps.tc.tests
+-R apps/tc/elpi           elpi.apps.tc
+-I apps/tc/src
+
+# Coq-elpi 
 theories/elpi.v
 theories/wip/memoization.v
 
 -I src
+
 src/META.coq-elpi
 
+src/coq_elpi_graph.mli
+src/coq_elpi_graph.ml
 src/coq_elpi_vernacular_syntax.mlg
 src/coq_elpi_vernacular.ml
 src/coq_elpi_vernacular.mli

_CoqProject.test

@@ -53,3 +53,4 @@ tests/test_link_order_import1.v
 tests/test_link_order_import2.v
 tests/test_link_order_import3.v
 tests/test_query_extra_dep.v
+tests/test_toposort.v

apps/tc/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/tc/Makefile.coq.local

@@ -0,0 +1,3 @@
+CAMLPKGS+= -package coq-elpi.elpi
+OCAMLPATH:=../../src/:$(OCAMLPATH)
+export OCAMLPATH