Add tests for type specifications

Author: mrjazzybread

test/typechecking/type_specs/dune

@@ -0,0 +1,3 @@
+(include ../../utils/dune.common)
+
+(include dune.inc)

test/typechecking/type_specs/dune.inc

@@ -0,0 +1,24 @@
+(rule
+(targets _gospel)
+   (action (run mkdir -p _gospel))) ; create the compilation directory.
+   (rule
+ (deps
+  %{bin:gospel}
+  (:checker %{project_root}/test/utils/testchecker.exe)
+       _gospel)
+ (action
+  (with-outputs-to positive.mli.output
+   (run %{checker} %{dep:positive.mli}))))
+
+(rule
+ (alias runtest)
+ (action
+  (diff positive.mli positive.mli.output)))
+
+(rule
+ (alias test-cmis)
+ (action
+  (chdir %{project_root}
+   ; Syntax sanity check
+   (run ocamlc -c %{dep:positive.mli}))))
+

test/typechecking/type_specs/positive.mli

@@ -0,0 +1,21 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  GOSPEL -- A Specification Language for OCaml                          *)
+(*                                                                        *)
+(*  Copyright (c) 2018- The VOCaL Project                                 *)
+(*                                                                        *)
+(*  This software is free software, distributed under the MIT license     *)
+(*  (as described in file LICENSE enclosed).                              *)
+(**************************************************************************)
+
+(*@ type nat = integer
+     with x invariant x >= 0
+    and positive_fraction = fraction
+      with x invariant
+        forall r. let _ = { res = r; f = x } in r > 0
+    and negative_fraction = fraction
+      with x invariant
+        forall r. let _ = { res = r; f = x } in r < 0
+    and compute = { res : integer; f : fraction }
+      with x invariant x.res = x.res = (x.f.n1 / x.f.n2)
+    and fraction = { n1 : integer; n2 : nat } *)