From 368e29a00a7c592464ebfe93b45f10bad9dc20b0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 20 May 2020 11:50:02 +0200
Subject: [PATCH] [pure] [lsp] Try to recover unit testing of pure interface

PR #289 silently removed important unit tests in the Pure module.

We try to recover them, but indeed, they don't work, as it seems the
library handling API introduced in #289 is lacking in terms of how it
can be used. There seem to be many problems with the new system in
terms of what a language server needs, in particular regarding
assumptions about the underlying file system.
---
 .travis.yml      |  2 +-
 GNUmakefile      |  6 +++++-
 src/pure/dune    |  2 ++
 src/pure/foo.lp  |  0
 src/pure/pure.ml | 56 ++++++++++++++++++++++++++++++++++++++++++++++++
 5 files changed, 64 insertions(+), 2 deletions(-)
 create mode 100644 src/pure/foo.lp

diff --git a/.travis.yml b/.travis.yml
index 0f23a721e..b390c3747 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -9,7 +9,7 @@ env:
   global:
   - OPAMJOBS="2"
   - OPAMYES="true"
-  - TEST_TARGETS="real_tests"
+  - TEST_TARGETS="real_tests unit-tests"
   matrix:
   - OCAML_VERSION=4.05.0
   - OCAML_VERSION=4.06.0
diff --git a/GNUmakefile b/GNUmakefile
index 18f62ca73..5da5d676d 100644
--- a/GNUmakefile
+++ b/GNUmakefile
@@ -19,7 +19,11 @@ LAMBDAPI     = dune exec -- lambdapi check --lib-root lib
 OK_TESTFILES = $(sort $(wildcard tests/OK/*.dk tests/OK/*.lp))
 KO_TESTFILES = $(sort $(wildcard tests/KO/*.dk tests/KO/*.lp))
 
-.PHONY: tests
+.PHONY: tests unit-tests
+
+unit-tests:
+	@dune build runtest
+
 tests: bin
 	@printf "## OK tests ##\n"
 	@for file in $(OK_TESTFILES) ; do \
diff --git a/src/pure/dune b/src/pure/dune
index ef5018355..429a1ca3b 100644
--- a/src/pure/dune
+++ b/src/pure/dune
@@ -2,4 +2,6 @@
  (name pure)
  (public_name lambdapi.pure)
  (modules pure)
+ (inline_tests (deps foo.lp))
+ (preprocess (pps ppx_inline_test))
  (libraries stdlib-shims core))
diff --git a/src/pure/foo.lp b/src/pure/foo.lp
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/pure/pure.ml b/src/pure/pure.ml
index 84d06123b..73b1a4f4f 100644
--- a/src/pure/pure.ml
+++ b/src/pure/pure.ml
@@ -96,3 +96,59 @@ let end_proof : proof_state -> command_result = fun s ->
 let get_symbols : state -> (Terms.sym * Pos.popt) StrMap.t = fun s ->
   Time.restore (fst s);
   !(Sign.((current_sign ()).sign_symbols))
+
+(* Equality on *)
+let test_file = "./foo.lp"
+
+let%test _ =
+  let st = initial_state test_file in
+  let (c,_) = parse_text st test_file "constant symbol B : TYPE" in
+  List.equal Command.equal c c
+
+(* Equality not *)
+let%test _ =
+  let st = initial_state test_file in
+  let (c,_) = parse_text st test_file "constant symbol B : TYPE" in
+  let (d,_) = parse_text st test_file "constant symbol C : TYPE" in
+  not (List.equal Command.equal c d)
+
+(* Equality is not sensitive to whitespace *)
+let%test _ =
+  let st = initial_state test_file in
+  let (c,_) = parse_text st test_file "constant   symbol  B : TYPE" in
+  let (d,_) = parse_text st test_file "  constant symbol B :   TYPE " in
+  List.equal Command.equal c d
+
+(* More complex test stressing most commands *)
+let%test _ =
+  let st = initial_state test_file in
+  let (c,_) = parse_text st test_file
+                (* copied from tests/OK/foo.lp. keep in sync. *)
+"constant symbol B : TYPE
+
+constant symbol true  : B
+constant symbol false : B
+
+symbol neg : B ⇒ B
+
+rule neg true  → false
+rule neg false → true
+
+constant symbol Prop : TYPE
+
+injective symbol P : Prop ⇒ TYPE
+
+constant symbol eq : B ⇒ B ⇒ Prop
+constant symbol refl b : P (eq b b)
+
+constant symbol case (p : B⇒Prop) : P (p true) ⇒ P (p false) ⇒ ∀b, P b
+
+theorem notK : ∀b, P (eq (neg (neg b)) b)
+proof
+  assume b
+  apply case (λb, eq (neg (neg b)) b)
+  apply refl
+  apply refl
+qed
+" in
+  List.equal Command.equal c c