Streamlined syntax for printing existential types, consistent with pa…

…rsing. Some tests cleanup.

README.md

@@ -25,7 +25,7 @@ Version 2.0 goals -- version targets may be reassigned:
 - [x] `when` clauses for patterns, currently only for numerical inequalities. (v1.2)
 - [x] Include negative numerical constraints (from `assert false`) as positive facts in numerical abduction, using disjunction elimination. (v1.2)
 - [x] Add inequalities with a variable as one side and `min` as LHS or `max` as RHS to the numerical sort. (v1.2)
-- [+] Flagship example: AVL tree from OCaml standard library (height imbalance limited by 2). (v1.2)
+- [x] Flagship example: AVL tree from OCaml standard library (height imbalance limited by 2). (v1.2)
 - [_] Solver directives in .gadt source code -- exposing the options available from the command-line interface. (v1.3)
 - [_] Or-patterns `p1 | p2` introducing disjunctions in premises, either eliminated by disjunction elimination or expanded by implication clause duplication -- depending on user-level option; preserved in exported code. (v1.3)
 - [_] Export Haskell code. (v1.3)

doc/invargent-manual.tm

@@ -824,6 +824,17 @@
     parameters. In rare cases a weaker postcondition but a more general
     invariant can be beneficial.
 
+    <item*|<verbatim|-show_extypes>>Show datatypes encoding existential
+    types, and their identifiers with uses of existential types. The type
+    system in InvarGenT encodes existential types as GADT types, but this
+    representation is hidden from the user. Using <verbatim|-show_extypes>
+    exposes the representation as follows. The encodings are exported in
+    <verbatim|.gadti> files as regular datatypes named <verbatim|exN>, and
+    existential types are printed using syntax
+    <verbatim|<math|\<exists\>>N:<math|\<ldots\>>> instead of
+    <math|\<exists\>\<ldots\>>, where <verbatim|N> is the identifier of an
+    existential type.
+
     <item*|<verbatim|-passing_ineq_trs>>Include inequalities in conclusion
     when solving numerical abduction. This setting leads to more inequalities
     being tried for addition in numeric abduction answer.

examples/avl_tree.gadti.target

@@ -20,78 +20,39 @@ external val compare : ∀a. a → a → LinOrder
 
 val height : ∀n, a. Avl (a, n) → Num n
 
-newtype Ex1 : num * num * type
-
-newcons Ex1 : ∀i, k, n, a[n=max (i + 1, k + 1)].Avl (a, n) ⟶
-   Ex1 (k, i, a)
-
 val create :
    ∀k, n, a[0 ≤ n ∧ 0 ≤ k ∧ n ≤ k + 2 ∧ k ≤ n + 2].
-   Avl (a, k) → a → Avl (a, n) →
-     ∃1:i[i=max (k + 1, n + 1)].Avl (a, i)
+   Avl (a, k) → a → Avl (a, n) → ∃i[i=max (k + 1, n + 1)].Avl (a, i)
 
 val singleton : ∀a. a → Avl (a, 1)
 
-newtype Ex4 : num * type
-
-newcons Ex4 : ∀k, n, a[k + 3 ≤ n ∧ n ≤ k + 4].Avl (a, n) ⟶
-   Ex4 (k, a)
-
 val rotr :
    ∀n, a[0 ≤ n].
-   (Avl (a, n + 3), a, Avl (a, n)) → ∃4:k[n + 3 ≤ k ∧
+   (Avl (a, n + 3), a, Avl (a, n)) → ∃k[n + 3 ≤ k ∧
      k ≤ n + 4].Avl (a, k)
 
-newtype Ex7 : num * type
-
-newcons Ex7 : ∀k, n, a[k + 3 ≤ n ∧ n ≤ k + 4].Avl (a, n) ⟶
-   Ex7 (k, a)
-
 val rotl :
    ∀n, a[0 ≤ n].
-   (Avl (a, n), a, Avl (a, n + 3)) → ∃7:k[n + 3 ≤ k ∧
+   (Avl (a, n), a, Avl (a, n + 3)) → ∃k[n + 3 ≤ k ∧
      k ≤ n + 4].Avl (a, k)
 
-newtype Ex11 : num * type
-
-newcons Ex11 : ∀k, n, a[n ≤ k + 1 ∧ 1 ≤ n ∧ k ≤ n].Avl (a, n)
-   ⟶ Ex11 (k, a)
-
 val add :
    ∀n, a.
-   a → Avl (a, n) → ∃11:k[k ≤ n + 1 ∧ 1 ≤ k ∧
-     n ≤ k].Avl (a, k)
+   a → Avl (a, n) → ∃k[k ≤ n + 1 ∧ 1 ≤ k ∧ n ≤ k].Avl (a, k)
 
 val mem : ∀n, a. a → Avl (a, n) → Bool
 
 val min_binding : ∀n, a[1 ≤ n]. Avl (a, n) → a
 
-newtype Ex13 : num * type
-
-newcons Ex13 : ∀k, n, a[n ≤ k + 1 ∧ k + 2 ≤ 2 n ∧
-   k ≤ n].Avl (a, k) ⟶ Ex13 (n, a)
-
 val remove_min_binding :
    ∀n, a[1 ≤ n].
-   Avl (a, n) → ∃13:k[n ≤ k + 1 ∧ k + 2 ≤ 2 n ∧
-     k ≤ n].Avl (a, k)
-
-newtype Ex15 : num * num * type
-
-newcons Ex15 : ∀i, k, n, a[n ≤ k + i ∧ i ≤ n ∧ k ≤ n ∧
-   n≤max (i + 1, k + 1)].Avl (a, n) ⟶ Ex15 (k, i, a)
+   Avl (a, n) → ∃k[n ≤ k + 1 ∧ k + 2 ≤ 2 n ∧ k ≤ n].Avl (a, k)
 
 val merge :
    ∀k, n, a[n ≤ k + 2 ∧ k ≤ n + 2].
-   (Avl (a, n), Avl (a, k)) → ∃15:i[i ≤ n + k ∧ k ≤ i ∧
-     n ≤ i ∧ i≤max (k + 1, n + 1)].Avl (a, i)
-
-newtype Ex19 : num * type
-
-newcons Ex19 : ∀k, n, a[k ≤ n + 1 ∧ 0 ≤ n ∧ n ≤ k].Avl (a, n)
-   ⟶ Ex19 (k, a)
+   (Avl (a, n), Avl (a, k)) → ∃i[i ≤ n + k ∧ k ≤ i ∧ n ≤ i ∧
+     i≤max (k + 1, n + 1)].Avl (a, i)
 
 val remove :
    ∀n, a.
-   a → Avl (a, n) → ∃19:k[n ≤ k + 1 ∧ 0 ≤ k ∧
-     k ≤ n].Avl (a, k)
+   a → Avl (a, n) → ∃k[n ≤ k + 1 ∧ 0 ≤ k ∧ k ≤ n].Avl (a, k)

examples/binary_upper_bound.gadti.target

@@ -6,12 +6,7 @@ newcons PZero : ∀n[0 ≤ n].Binary n ⟶ Binary (2 n)
 
 newcons POne : ∀n[0 ≤ n].Binary n ⟶ Binary (2 n + 1)
 
-newtype Ex4 : num * num
-
-newcons Ex4 : ∀i, k, n[n ≤ k + i ∧ i ≤ n ∧ k ≤ n].Binary n ⟶
-   Ex4 (k, i)
-
 val ub :
    ∀k, n.
-   Binary k → Binary n → ∃4:i[i ≤ n + k ∧ k ≤ i ∧
+   Binary k → Binary n → ∃i[i ≤ n + k ∧ k ≤ i ∧
      n ≤ i].Binary i

examples/equational_reas.gadti.target

@@ -17,11 +17,7 @@ newcons Here : ∀b.Place b * Place b ⟶ Nearby (b, b)
 newcons Transitive : ∀a, b, c.Nearby (a, b) * Nearby (b, c) ⟶
    Nearby (a, c)
 
-newtype Ex1 : type
-
-newcons Ex1 : ∀a, b[].(Place b, Nearby (a, b)) ⟶ Ex1 a
-
-external wander : ∀a. Place a → ∃1:b.(Place b, Nearby (a, b))
+external wander : ∀a. Place a → ∃b.(Place b, Nearby (a, b))
 
 newtype Meet : type * type
 

examples/filter.gadti.target

@@ -4,10 +4,6 @@ newcons LNil : ∀a. List (a, 0)
 
 newcons LCons : ∀n, a[0 ≤ n].a * List (a, n) ⟶ List (a, n + 1)
 
-newtype Ex2 : num * type
-
-newcons Ex2 : ∀k, n, a[0 ≤ k ∧ k ≤ n].List (a, k) ⟶ Ex2 (n, a)
-
 val filter :
    ∀n, a.
-   (a → Bool) → List (a, n) → ∃2:k[0 ≤ k ∧ k ≤ n].List (a, k)
+   (a → Bool) → List (a, n) → ∃k[0 ≤ k ∧ k ≤ n].List (a, k)

examples/filter_map.gadti.target

@@ -4,11 +4,7 @@ newcons LNil : ∀a. List (a, 0)
 
 newcons LCons : ∀n, a[0 ≤ n].a * List (a, n) ⟶ List (a, n + 1)
 
-newtype Ex2 : num * type
-
-newcons Ex2 : ∀k, n, a[0 ≤ k ∧ k ≤ n].List (a, k) ⟶ Ex2 (n, a)
-
 val filter :
    ∀n, a, b.
-   (a → Bool) → (a → b) → List (a, n) → ∃2:k[0 ≤ k ∧
+   (a → Bool) → (a → b) → List (a, n) → ∃k[0 ≤ k ∧
      k ≤ n].List (b, k)

examples/mutual_recursion_eval.gadti.target

@@ -2,19 +2,11 @@ newtype Term : type
 
 newtype Calc
 
-newtype Ex1
-
-newcons Ex1 : ∀k.Num k ⟶ ∃1:k.Num k
-
-external val mult : ∀i, j. Num i → Num j → ∃1:k.Num k
+external val mult : ∀i, j. Num i → Num j → ∃k.Num k
 
 external val is_zero : ∀i. Num i → Bool
 
-newtype Ex2
-
-newcons Ex2 : ∀k.Num k ⟶ ∃2:k.Num k
-
-external val cond : ∀i, j. Bool → Num i → Num j → ∃2:k.Num k
+external val cond : ∀i, j. Bool → Num i → Num j → ∃k.Num k
 
 newcons Lit : ∀k.Num k ⟶ Calc
 
@@ -36,10 +28,6 @@ newcons Snd : ∀a, b.Term ((a, b)) ⟶ Term b
 
 val snd : ∀a, b. (a, b) → b
 
-newtype Ex3
-
-newcons Ex3 : ∀n.Num n ⟶ Ex3
-
-val calc : Calc → ∃3:n.Num n
+val calc : Calc → ∃n.Num n
 
 val eval : ∀a. Term a → a

examples/mutual_recursion_eval_docs.gadti.target

@@ -4,21 +4,13 @@ newtype Term : type
 (** Expressions representing computations on tuples. *)
 newtype Calc
 
-newtype Ex1
-
-newcons Ex1 : ∀k.Num k ⟶ ∃1:k.Num k
-
 (** Multiplication packs the result into existential type. *)
-external val mult : ∀i, j. Num i → Num j → ∃1:k.Num k
+external val mult : ∀i, j. Num i → Num j → ∃k.Num k
 
 external val is_zero : ∀i. Num i → Bool
 
-newtype Ex2
-
-newcons Ex2 : ∀k.Num k ⟶ ∃2:k.Num k
-
 (** Conditional is eager -- computes all its arguments. *)
-external val cond : ∀i, j. Bool → Num i → Num j → ∃2:k.Num k
+external val cond : ∀i, j. Bool → Num i → Num j → ∃k.Num k
 
 (** Numerical constants. *)
 newcons Lit : ∀k.Num k ⟶ Calc
@@ -47,12 +39,8 @@ newcons Snd : ∀a, b.Term ((a, b)) ⟶ Term b
 (** Small definition. *)
 val snd : ∀a, b. (a, b) → b
 
-newtype Ex3
-
-newcons Ex3 : ∀n.Num n ⟶ Ex3
-
 (** Exposing multiple mutually recursive definitions is tricky, it would
     be easier to only expose the external one. *)
-val calc : Calc → ∃3:n.Num n
+val calc : Calc → ∃n.Num n
 
 val eval : ∀a. Term a → a

examples/mutual_simple_recursion_eval.gadti.target

@@ -4,11 +4,7 @@ newtype Calc
 
 external val is_zero : ∀i. Num i → Bool
 
-newtype Ex1
-
-newcons Ex1 : ∀k.Num k ⟶ ∃1:k.Num k
-
-external val cond : ∀i, j. Bool → Num i → Num j → ∃1:k.Num k
+external val cond : ∀i, j. Bool → Num i → Num j → ∃k.Num k
 
 newcons Lit : ∀k.Num k ⟶ Calc
 
@@ -20,10 +16,6 @@ newcons If : ∀a.Term Bool * Term a * Term a ⟶ Term a
 
 val snd : ∀a, b. (a, b) → b
 
-newtype Ex2
-
-newcons Ex2 : ∀n.Num n ⟶ Ex2
-
-val calc : Calc → ∃2:n.Num n
+val calc : Calc → ∃n.Num n
 
 val eval : ∀a. Term a → a