Merge pull request #650 from FissoreD/tc-all-in-namespace

[TC] all tc predicates are inside a tc namespace

.github/workflows/doc.yml

@@ -34,7 +34,7 @@ jobs:
         opam repo add coq-dev https://coq.inria.fr/opam/core-dev
         opam repo add extra-dev https://coq.inria.fr/opam/extra-dev
         opam update
-        opam install coq-serapi . coq-core.8.19.1
+        opam install coq-serapi ./coq-elpi.opam coq-core.8.19.1
         sudo apt-get update
         sudo apt-get install python3-pip -y
         pip3 install git+https://github.com/cpitclaudel/alectryon.git@c8ab1ec

.github/workflows/main.yml

@@ -25,40 +25,27 @@ env:
   OPAM_SUITE: ${{ inputs.suite }}
 
 jobs:
+
   build:
     runs-on: ubuntu-latest
     strategy:
-      fail-fast: false
+      #fail-fast: false
       matrix:
-        coq_version: [ '8.19' , '8.20' , 'dev' ]
+        coq_version: [ '8.19.2' , '8.20+rc1' , 'dev' ]
         ocaml_version:
-          - '4.14-flambda'
-    steps:
-    - uses: actions/checkout@v2
-    - uses: coq-community/docker-coq-action@v1
-      with:
-        opam_file: './coq-elpi.opam'
-        coq_version: ${{ matrix.coq_version }}
-        ocaml_version: ${{ matrix.ocaml_version }}
-        export: 'OPAMWITHTEST'
-        install: |
-          startGroup "Install dependencies"
-            opam pin add -n -y -k path $PACKAGE $WORKDIR
-            opam update -y
-            opam install -y -j 2 $PACKAGE --deps-only
-          endGroup
-      env:
-        OPAMWITHTEST: 'true'
-
-  play:
-    runs-on: ubuntu-latest
+          - '4.14.x'
+          - '5.2.x'
     steps:
     - uses: actions/checkout@v2
     - uses: avsm/setup-ocaml@v2
       with:
-        ocaml-compiler: 5.1.x
-    - run: |
-        opam install ./coq-elpi.opam
+        ocaml-compiler: ${{ matrix.ocaml_version }}
+    - run: opam repo add coq-dev https://coq.inria.fr/opam/core-dev
+    - run: opam install coq-core.${{ matrix.coq_version }}
+    - run: opam install coq-stdlib.${{ matrix.coq_version }}
+    - run: opam install ./coq-elpi.opam --deps-only --with-test -y
+    - run: opam exec make build
+    - run: opam exec make test
 
   release:
     runs-on: ubuntu-latest

.gitignore

@@ -52,4 +52,7 @@ apps/cs/src/coq_elpi_cs_hook.ml
 
 *.timing
 _build
-tmp.out
+tmp.out
+coq-elpi-tests.opam
+coq-elpi-tests.install
+coq-elpi.install

apps/NES/tests/dune

@@ -1,5 +1,6 @@
 (coq.theory
  (name elpi.apps.NES.tests)
+ (package coq-elpi-tests)
  (theories elpi elpi.apps.NES))
 
 (include_subdirs qualified)

apps/derive/tests/dune

@@ -1,5 +1,6 @@
 (coq.theory
  (name elpi.apps.derive.tests)
+ (package coq-elpi-tests)
  (flags -w -default-output-directory)
  (theories elpi elpi.apps.derive))
 

apps/eltac/tests/dune

@@ -1,5 +1,6 @@
 (coq.theory
  (name elpi.apps.eltac.tests)
+ (package coq-elpi-tests)
  (theories elpi elpi.apps.eltac))
 
 (include_subdirs qualified)

apps/locker/tests/dune

@@ -1,5 +1,6 @@
 (coq.theory
  (name elpi.apps.locker.tests)
+ (package coq-elpi-tests)
  (theories elpi elpi.apps.locker))
 
 (include_subdirs qualified)

apps/tc/elpi/WIP/force_llam.elpi

@@ -23,9 +23,9 @@ namespace force-llam {
   % of other premises. 
   compile-conclusion ff Goal Proof HOPremisesIn HOPremisesOut Premises Clause :-
     coq.safe-dest-app Goal Class Args,
-    get-mode {get-TC-of-inst-type Class} Modes,
+    tc.get-mode {tc.get-TC-of-inst-type Class} Modes,
     force-llam.modes Modes Args ForceLlam,
-    make-tc Goal Proof Premises ff Clause1, 
+    tc.make-tc Goal Proof Premises ff Clause1, 
     Prems = [HOPremisesIn, ForceLlam, [Clause1], HOPremisesOut],
     std.flatten Prems AllPremises,
     Clause = do AllPremises.

apps/tc/elpi/WIP/modes.elpi

@@ -34,7 +34,7 @@ pred add-modes i:gref.
 :if "add-modes"
 add-modes GR :-
   % the hint mode is added only if not exists
-  if (not (class GR _ _)) (
+  if (not (tc.class GR _ _)) (
     coq.env.typeof GR Ty,
     coq.hints.modes GR "typeclass_instances" ModesProv,
     if (ModesProv = []) (Modes = [{make-last-hint-mode-input Ty}]) (Modes = ModesProv),

apps/tc/elpi/alias.elpi

@@ -1,19 +1,21 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
-pred alias i:term, o:term.
+namespace tc {
+  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.
-
-%  [replace-with-alias T T1 Changed] T1 is T where aliases are replaced
-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.
+  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.
+
+  %  [replace-with-alias T T1 Changed] T1 is T where aliases are replaced
+  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.
+}