TC solver

.vscode/settings.json

@@ -27,7 +27,6 @@
         "src/coq_elpi_vernacular_syntax.ml": true,
         "**/Makefile.coq": true,
         "**/Makefile.coq.conf": true,
-        "**/.merlin": true
     },
     "restructuredtext.confPath": "${workspaceFolder}/alectryon/recipes/sphinx",
     "ocaml.server.args": [

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

@@ -18,6 +18,12 @@
 -R apps/eltac/tests    elpi.apps.eltac.tests
 -R apps/eltac/examples elpi.apps.eltac.examples
 -R apps/coercion/theories elpi.apps.coercion
+-R apps/coercion/theories       elpi.apps.coercion
+-R apps/coercion/tests          elpi.apps.tc.coercion
+-R apps/coercion/elpi           elpi.apps.coercion
+-R apps/tc/theories       elpi.apps.tc
+-R apps/tc/tests          elpi.apps.tc.tests
+-R apps/tc/elpi           elpi.apps.tc
 
 theories/elpi.v
 theories/wip/memoization.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,19 @@
+CAMLPKGS+= -package coq-elpi.elpi
+OCAMLPATH:=../../src/:$(OCAMLPATH)
+export OCAMLPATH
+
+# detection of elpi
+ifeq "$(ELPIDIR)" ""
+ELPIDIR=$(shell ocamlfind query elpi 2>/dev/null)
+endif
+ifeq "$(ELPIDIR)" ""
+$(error Elpi not found, make sure it is installed in your PATH or set ELPIDIR)
+endif
+export ELPIDIR
+
+merlin-hook::
+	echo "S $(abspath $(ELPIDIR))" >> .merlin
+	echo "B $(abspath $(ELPIDIR))" >> .merlin
+	if [ "$(ELPIDIR)" != "elpi/findlib/elpi" ]; then\
+		echo "PKG elpi" >> .merlin;\
+	fi

apps/tc/_CoqProject

@@ -0,0 +1,16 @@
+# 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 elpi       elpi.apps.tc
+
+src/coq_elpi_tc_hook.mlg
+src/coq_elpi_class_tactics_hacked.ml
+src/elpi_tc_plugin.mlpack
+
+-I src/
+src/META.coq-elpi-tc
+
+theories/tc.v

apps/tc/_CoqProject.test

@@ -0,0 +1,48 @@
+# Hack to see Coq-Elpi even if it is not installed yet
+-Q ../../theories elpi
+-I ../../src
+
+-Q elpi     elpi.apps.tc
+-R theories elpi.apps
+-R tests    elpi.apps.tc.tests
+-I src
+
+tests/premisesSort/sortCode.v
+tests/premisesSort/sort1.v
+# tests/premisesSort/sort2.v
+# tests/premisesSort/sort3.v
+# tests/premisesSort/sort4.v
+tests/included_proof.v
+# tests/goalDispatch.v
+
+# Import order of instances
+tests/importOrder/sameOrderCommand.v
+tests/importOrder/f1.v
+tests/importOrder/f2a.v
+tests/importOrder/f2b.v
+# tests/importOrder/f3a.v
+# tests/importOrder/f3b.v
+# tests/importOrder/f3c.v
+# tests/importOrder/f3d.v
+# tests/importOrder/f3e.v
+# tests/importOrder/f3f.v
+# tests/importOrder/f3g.v
+
+tests/nobacktrack.v
+tests/removeEta.v
+tests/patternFragment.v
+tests/contextDeepHierarchy.v
+tests/mode_no_repetion.v
+# tests/test_commands_API.v
+tests/section_in_out.v
+tests/eqSimplDef.v
+tests/eqSimpl.v
+
+tests/injTest.v
+# Test with light version of base.v of stdpp
+tests/stdppInj.v
+tests/stdppInjClassic.v
+tests/test.v
+
+# Test with base.v of stdpp
+# tests/bigTest.v

apps/tc/elpi/alias.elpi

@@ -0,0 +1,15 @@
+pred alias i:term, o:term.
+
+pred replace-with-alias.aux i:list term, o:list term, o:bool.
+replace-with-alias.aux [] [] ff.
+replace-with-alias.aux [X | Xs] [Y | Ys] B :-
+  replace-with-alias X Y B', 
+  replace-with-alias.aux Xs Ys B'',
+  or B' B'' B.
+
+pred replace-with-alias i:term, o:term, o:bool.
+replace-with-alias A Sol tt :- alias A Sol', 
+  replace-with-alias Sol' Sol _.
+replace-with-alias (app ToReplace) (app Sol) A :- 
+  replace-with-alias.aux ToReplace Sol A.
+replace-with-alias A A ff.

apps/tc/elpi/base.elpi

@@ -0,0 +1,67 @@
+% [count L X R] counts the occurrences of X in L
+pred count i:list A, i:A, o:int.
+count [] _ 0.
+count [A | TL] A R :- count TL A X, R is (X + 1).
+count [_ | TL] A R :- count TL A R.
+
+pred expected-found i:A, i:A. 
+expected-found Expected Found :- 
+  Expected = Found; 
+  halt "Assertion error"
+  "\nExpected :" Expected
+  "\nFound    :" Found.
+
+pred last-no-error i:list A, o:A.
+last-no-error A B :-
+  (std.last [] _ :- !, fail) => std.last A B.
+
+% [find L F R] returns the first R in L such that (F R) is valid
+pred find i:list A, i:(A -> prop), o:A.
+find [] _ _ :- std.fatal-error "find element not found".
+find [R | _] F R :- F R.
+find [_ | L] F R :- find L F R.
+
+pred find-opt i:list A, i:(A -> prop), o:(option A).
+find-opt [] _ none.
+find-opt [R | _] F (some R) :- F R.
+find-opt [_ | L] F R :- find-opt L F R.
+
+pred for-loop i:int, i:int, i:(int -> prop).
+for-loop A A _.
+for-loop A B _ :- A > B, std.fatal-error "first param should be smaller then the sencond one".
+for-loop A B F :- F A, for-loop {calc (A + 1)} B F.
+
+pred list-init i:int, i:(int -> A -> prop), o:list A.
+list-init N _ _ :- N < 0, std.fatal-error "list-init negative length".
+list-init 0 _ [] :- !.
+list-init N F [A | TL] :-
+  F N A, N1 is N - 1, list-init N1 F TL.
+
+pred for-loop0 i:int, i:(int -> prop).
+for-loop0 B F :- for-loop 0 B F.
+
+pred args->str-list i:list argument, o: list string.
+args->str-list L Res :-
+  std.map L (x\r\ str r = x) Res.
+
+pred or i:bool, i:bool, o:bool.
+or ff ff ff :- !. 
+or _ _ tt.
+
+pred neg i:bool, o:bool.
+neg tt ff.
+neg ff tt.
+
+pred fail->bool i:prop, o:bool.
+fail->bool P ff :- P, !.
+fail->bool _ tt.
+
+pred sep.
+sep :- coq.say "---------------------------------".
+
+pred do i:list prop.
+do [].
+do [P|PS] :- P, do PS.
+
+pred do-once i:prop. 
+do-once A :- A, !.