Test proof-irrelevance and parameterised records systematically

packages/coln-compiler/test/Main.hs

@@ -35,7 +35,13 @@ knownFailingElaboratorTests :: [String]
 knownFailingElaboratorTests = []
 
 knownFailingTypeScriptTests :: [String]
-knownFailingTypeScriptTests = ["equality", "equality-prop", "rule-literals"]
+knownFailingTypeScriptTests =
+  [ "equality"
+  , "equality-prop"
+  , "equality-record"
+  , "equality-record-nested"
+  , "rule-literals"
+  ]
 
 main :: IO ()
 main = defaultMain =<< goldenTests

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-prop-prop.coln

@@ -0,0 +1,9 @@
+theory T := sig
+  A : Prop
+  B : A -> Prop
+  C : (a : A) -> B a -> Prop
+  f : (a : A) -> (b : B a) -> C a b
+end
+
+realm TRealm @ T
+end

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-prop-prop.output

@@ -0,0 +1,45 @@
+-- elaborated
+global entry named T
+type: Theory
+value: sig
+  A : Prop
+  B : A -> Prop
+  C : (a : A) -> B a -> Prop
+  f : (a : A) -> (b : B a) -> C a b
+end
+realm named TRealm
+generators: node
+  A = rel []
+  B = rel [a : TRealm.A []]
+  C = rel [a : TRealm.A [], b : TRealm.B [a := a]]
+  f = (fun [a : TRealm.A [], b : TRealm.B [a := a]] -> TRealm.C [
+    a := a,
+    b := b
+  ])
+end
+lowered: flatrealm
+  entities
+    table ℜ.A := []
+    table ℜ.B := [.a : ℜ.A]
+    table ℜ.C := [.a : ℜ.A, .b : ℜ.B]
+    table ℜ.f := [.a : ℜ.A, .b : ℜ.B, .c : ℜ.C] primarykey [.a, .b]
+  end
+  rules
+    enforced ℜ.A.foreignKey := ℜ.A [] ⊢ ⊤
+    enforced ℜ.B.foreignKey a := ℜ.B [.a ↦ a] ⊢ a ∈ ℜ.A []
+    enforced ℜ.C.foreignKey a b := ℜ.C [.a ↦ a, .b ↦ b] ⊢ a ∈ ℜ.A [] ∧ b ∈ ℜ.B [
+      .a ↦ a
+    ]
+    enforced ℜ.f.foreignKey a b c := ℜ.f [
+      .a ↦ a,
+      .b ↦ b,
+      .c ↦ c
+    ] ⊢ a ∈ ℜ.A [] ∧ b ∈ ℜ.B [.a ↦ a] ∧ c ∈ ℜ.C [.a ↦ a, .b ↦ b]
+    monitored ℜ.f.total a b := a ∈ ℜ.A [] ∧ b ∈ ℜ.B [.a ↦ a] ⊢ ℜ.f [
+      .a ↦ a,
+      .b ↦ b
+    ]
+  end
+end
+
+-- messages

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-prop-prop.ts.output/T.ts

@@ -0,0 +1,15 @@
+import * as runtime from "@coln-project/runtime";
+
+export interface View {
+  A: runtime.ColnSet.View;
+  B: (x: runtime.Value) => runtime.ColnSet.View;
+  C: (x: runtime.Value) => (x: runtime.Value) => runtime.ColnSet.View;
+  f: (x: runtime.Value) => (x: runtime.Value) => runtime.ColnRef.View;
+}
+
+export interface Transaction extends View {
+  A: runtime.ColnSet.Transaction;
+  B: (x: runtime.Value) => runtime.ColnSet.Transaction;
+  C: (x: runtime.Value) => (x: runtime.Value) => runtime.ColnSet.Transaction;
+  f: (x: runtime.Value) => (x: runtime.Value) => runtime.ColnRef.Transaction;
+}

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-prop-prop.ts.output/TRealm.json

@@ -0,0 +1 @@
+{"entities":[{"path":[["TRealm"],["A"]],"value":{"entityVariant":{"tag":"table"},"columns":[],"primaryKey":null}},{"path":[["TRealm"],["B"]],"value":{"entityVariant":{"tag":"table"},"columns":[{"path":[["a"]],"type":{"tag":"rowId","path":[["TRealm"],["A"]]}}],"primaryKey":null}},{"path":[["TRealm"],["C"]],"value":{"entityVariant":{"tag":"table"},"columns":[{"path":[["a"]],"type":{"tag":"rowId","path":[["TRealm"],["A"]]}},{"path":[["b"]],"type":{"tag":"rowId","path":[["TRealm"],["B"]]}}],"primaryKey":null}},{"path":[["TRealm"],["f"]],"value":{"entityVariant":{"tag":"table"},"columns":[{"path":[["a"]],"type":{"tag":"rowId","path":[["TRealm"],["A"]]}},{"path":[["b"]],"type":{"tag":"rowId","path":[["TRealm"],["B"]]}},{"path":[["c"]],"type":{"tag":"rowId","path":[["TRealm"],["C"]]}}],"primaryKey":[[["a"]],[["b"]]]}}],"rules":[{"path":[["TRealm"],["A"],["foreignKey"]],"value":{"ruleVariant":"enforced","varNames":[],"varTypes":[],"antecedents":[{"tag":"atom","atom":{"entity":[["TRealm"],["A"]],"rowId":null,"values":[]}}],"consequents":[]}},{"path":[["TRealm"],["B"],["foreignKey"]],"value":{"ruleVariant":"enforced","varNames":[[["a"]]],"varTypes":[{"tag":"rowId","path":[["TRealm"],["A"]]}],"antecedents":[{"tag":"atom","atom":{"entity":[["TRealm"],["B"]],"rowId":null,"values":[{"column":0,"term":{"tag":"var","index":0}}]}}],"consequents":[{"tag":"atom","atom":{"entity":[["TRealm"],["A"]],"rowId":{"tag":"var","index":0},"values":[]}}]}},{"path":[["TRealm"],["C"],["foreignKey"]],"value":{"ruleVariant":"enforced","varNames":[[["a"]],[["b"]]],"varTypes":[{"tag":"rowId","path":[["TRealm"],["A"]]},{"tag":"rowId","path":[["TRealm"],["B"]]}],"antecedents":[{"tag":"atom","atom":{"entity":[["TRealm"],["C"]],"rowId":null,"values":[{"column":0,"term":{"tag":"var","index":0}},{"column":1,"term":{"tag":"var","index":1}}]}}],"consequents":[{"tag":"atom","atom":{"entity":[["TRealm"],["A"]],"rowId":{"tag":"var","index":0},"values":[]}},{"tag":"atom","atom":{"entity":[["TRealm"],["B"]],"rowId":{"tag":"var","index":1},"values":[{"column":0,"term":{"tag":"var","index":0}}]}}]}},{"path":[["TRealm"],["f"],["foreignKey"]],"value":{"ruleVariant":"enforced","varNames":[[["a"]],[["b"]],[["c"]]],"varTypes":[{"tag":"rowId","path":[["TRealm"],["A"]]},{"tag":"rowId","path":[["TRealm"],["B"]]},{"tag":"rowId","path":[["TRealm"],["C"]]}],"antecedents":[{"tag":"atom","atom":{"entity":[["TRealm"],["f"]],"rowId":null,"values":[{"column":0,"term":{"tag":"var","index":0}},{"column":1,"term":{"tag":"var","index":1}},{"column":2,"term":{"tag":"var","index":2}}]}}],"consequents":[{"tag":"atom","atom":{"entity":[["TRealm"],["A"]],"rowId":{"tag":"var","index":0},"values":[]}},{"tag":"atom","atom":{"entity":[["TRealm"],["B"]],"rowId":{"tag":"var","index":1},"values":[{"column":0,"term":{"tag":"var","index":0}}]}},{"tag":"atom","atom":{"entity":[["TRealm"],["C"]],"rowId":{"tag":"var","index":2},"values":[{"column":0,"term":{"tag":"var","index":0}},{"column":1,"term":{"tag":"var","index":1}}]}}]}},{"path":[["TRealm"],["f"],["total"]],"value":{"ruleVariant":"monitored","varNames":[[["a"]],[["b"]]],"varTypes":[{"tag":"rowId","path":[["TRealm"],["A"]]},{"tag":"rowId","path":[["TRealm"],["B"]]}],"antecedents":[{"tag":"atom","atom":{"entity":[["TRealm"],["A"]],"rowId":{"tag":"var","index":0},"values":[]}},{"tag":"atom","atom":{"entity":[["TRealm"],["B"]],"rowId":{"tag":"var","index":1},"values":[{"column":0,"term":{"tag":"var","index":0}}]}}],"consequents":[{"tag":"atom","atom":{"entity":[["TRealm"],["f"]],"rowId":null,"values":[{"column":0,"term":{"tag":"var","index":0}},{"column":1,"term":{"tag":"var","index":1}}]}}]}}]}

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-prop-prop.ts.output/TRealm.ts

@@ -0,0 +1,69 @@
+import schema from "./TRealm.json";
+export {schema};
+import * as runtime from "@coln-project/runtime";
+import * as T from "./T.ts";
+
+export class View {
+  root: T.View;
+
+  constructor(store: runtime.StoreHandle) {
+    this.root = {
+      A: (new runtime.RowIdSet.View(store, "TRealm.A", [])),
+      B: (a: runtime.Value) => {
+        return (new runtime.RowIdSet.View(store, "TRealm.B", [a]));
+      },
+      C: (a: runtime.Value) => {
+        return (b: runtime.Value) => {
+          return (new runtime.RowIdSet.View(store, "TRealm.C", [a, b]));
+        };
+      },
+      f: (a: runtime.Value) => {
+        return (b: runtime.Value) => {
+          return (new runtime.TableCellRef.View(store, "TRealm.f", [a, b]));
+        };
+      }
+    };
+  }
+}
+
+export class Transaction extends View {
+  root: T.Transaction;
+
+  constructor(
+    store: runtime.StoreHandle,
+    transaction: runtime.TransactionHandle
+  ) {
+    super(store);
+    this.root = {
+      A: (new runtime.RowIdSet.Transaction(store, "TRealm.A", [], transaction)),
+      B: (a: runtime.Value) => {
+        return (new runtime.RowIdSet.Transaction(
+          store,
+          "TRealm.B",
+          [a],
+          transaction
+        ));
+      },
+      C: (a: runtime.Value) => {
+        return (b: runtime.Value) => {
+          return (new runtime.RowIdSet.Transaction(
+            store,
+            "TRealm.C",
+            [a, b],
+            transaction
+          ));
+        };
+      },
+      f: (a: runtime.Value) => {
+        return (b: runtime.Value) => {
+          return (new runtime.TableCellRef.Transaction(
+            store,
+            "TRealm.f",
+            [a, b],
+            transaction
+          ));
+        };
+      }
+    };
+  }
+}

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-prop-set.coln

@@ -0,0 +1,9 @@
+theory T := sig
+  A : Prop
+  B : A -> Prop
+  C : (a : A) -> B a -> Set
+  f : (a : A) -> (b : B a) -> C a b
+end
+
+realm TRealm @ T
+end

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-prop-set.output

@@ -0,0 +1,45 @@
+-- elaborated
+global entry named T
+type: Theory
+value: sig
+  A : Prop
+  B : A -> Prop
+  C : (a : A) -> B a -> Set
+  f : (a : A) -> (b : B a) -> C a b
+end
+realm named TRealm
+generators: node
+  A = rel []
+  B = rel [a : TRealm.A []]
+  C = rel [a : TRealm.A [], b : TRealm.B [a := a]]
+  f = (fun [a : TRealm.A [], b : TRealm.B [a := a]] -> TRealm.C [
+    a := a,
+    b := b
+  ])
+end
+lowered: flatrealm
+  entities
+    table ℜ.A := []
+    table ℜ.B := [.a : ℜ.A]
+    table ℜ.C := [.a : ℜ.A, .b : ℜ.B]
+    table ℜ.f := [.a : ℜ.A, .b : ℜ.B, .c : ℜ.C] primarykey [.a, .b]
+  end
+  rules
+    enforced ℜ.A.foreignKey := ℜ.A [] ⊢ ⊤
+    enforced ℜ.B.foreignKey a := ℜ.B [.a ↦ a] ⊢ a ∈ ℜ.A []
+    enforced ℜ.C.foreignKey a b := ℜ.C [.a ↦ a, .b ↦ b] ⊢ a ∈ ℜ.A [] ∧ b ∈ ℜ.B [
+      .a ↦ a
+    ]
+    enforced ℜ.f.foreignKey a b c := ℜ.f [
+      .a ↦ a,
+      .b ↦ b,
+      .c ↦ c
+    ] ⊢ a ∈ ℜ.A [] ∧ b ∈ ℜ.B [.a ↦ a] ∧ c ∈ ℜ.C [.a ↦ a, .b ↦ b]
+    monitored ℜ.f.total a b := a ∈ ℜ.A [] ∧ b ∈ ℜ.B [.a ↦ a] ⊢ ℜ.f [
+      .a ↦ a,
+      .b ↦ b
+    ]
+  end
+end
+
+-- messages

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-prop-set.ts.output/T.ts

@@ -0,0 +1,15 @@
+import * as runtime from "@coln-project/runtime";
+
+export interface View {
+  A: runtime.ColnSet.View;
+  B: (x: runtime.Value) => runtime.ColnSet.View;
+  C: (x: runtime.Value) => (x: runtime.Value) => runtime.ColnSet.View;
+  f: (x: runtime.Value) => (x: runtime.Value) => runtime.ColnRef.View;
+}
+
+export interface Transaction extends View {
+  A: runtime.ColnSet.Transaction;
+  B: (x: runtime.Value) => runtime.ColnSet.Transaction;
+  C: (x: runtime.Value) => (x: runtime.Value) => runtime.ColnSet.Transaction;
+  f: (x: runtime.Value) => (x: runtime.Value) => runtime.ColnRef.Transaction;
+}

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-prop-set.ts.output/TRealm.json

@@ -0,0 +1 @@
+{"entities":[{"path":[["TRealm"],["A"]],"value":{"entityVariant":{"tag":"table"},"columns":[],"primaryKey":null}},{"path":[["TRealm"],["B"]],"value":{"entityVariant":{"tag":"table"},"columns":[{"path":[["a"]],"type":{"tag":"rowId","path":[["TRealm"],["A"]]}}],"primaryKey":null}},{"path":[["TRealm"],["C"]],"value":{"entityVariant":{"tag":"table"},"columns":[{"path":[["a"]],"type":{"tag":"rowId","path":[["TRealm"],["A"]]}},{"path":[["b"]],"type":{"tag":"rowId","path":[["TRealm"],["B"]]}}],"primaryKey":null}},{"path":[["TRealm"],["f"]],"value":{"entityVariant":{"tag":"table"},"columns":[{"path":[["a"]],"type":{"tag":"rowId","path":[["TRealm"],["A"]]}},{"path":[["b"]],"type":{"tag":"rowId","path":[["TRealm"],["B"]]}},{"path":[["c"]],"type":{"tag":"rowId","path":[["TRealm"],["C"]]}}],"primaryKey":[[["a"]],[["b"]]]}}],"rules":[{"path":[["TRealm"],["A"],["foreignKey"]],"value":{"ruleVariant":"enforced","varNames":[],"varTypes":[],"antecedents":[{"tag":"atom","atom":{"entity":[["TRealm"],["A"]],"rowId":null,"values":[]}}],"consequents":[]}},{"path":[["TRealm"],["B"],["foreignKey"]],"value":{"ruleVariant":"enforced","varNames":[[["a"]]],"varTypes":[{"tag":"rowId","path":[["TRealm"],["A"]]}],"antecedents":[{"tag":"atom","atom":{"entity":[["TRealm"],["B"]],"rowId":null,"values":[{"column":0,"term":{"tag":"var","index":0}}]}}],"consequents":[{"tag":"atom","atom":{"entity":[["TRealm"],["A"]],"rowId":{"tag":"var","index":0},"values":[]}}]}},{"path":[["TRealm"],["C"],["foreignKey"]],"value":{"ruleVariant":"enforced","varNames":[[["a"]],[["b"]]],"varTypes":[{"tag":"rowId","path":[["TRealm"],["A"]]},{"tag":"rowId","path":[["TRealm"],["B"]]}],"antecedents":[{"tag":"atom","atom":{"entity":[["TRealm"],["C"]],"rowId":null,"values":[{"column":0,"term":{"tag":"var","index":0}},{"column":1,"term":{"tag":"var","index":1}}]}}],"consequents":[{"tag":"atom","atom":{"entity":[["TRealm"],["A"]],"rowId":{"tag":"var","index":0},"values":[]}},{"tag":"atom","atom":{"entity":[["TRealm"],["B"]],"rowId":{"tag":"var","index":1},"values":[{"column":0,"term":{"tag":"var","index":0}}]}}]}},{"path":[["TRealm"],["f"],["foreignKey"]],"value":{"ruleVariant":"enforced","varNames":[[["a"]],[["b"]],[["c"]]],"varTypes":[{"tag":"rowId","path":[["TRealm"],["A"]]},{"tag":"rowId","path":[["TRealm"],["B"]]},{"tag":"rowId","path":[["TRealm"],["C"]]}],"antecedents":[{"tag":"atom","atom":{"entity":[["TRealm"],["f"]],"rowId":null,"values":[{"column":0,"term":{"tag":"var","index":0}},{"column":1,"term":{"tag":"var","index":1}},{"column":2,"term":{"tag":"var","index":2}}]}}],"consequents":[{"tag":"atom","atom":{"entity":[["TRealm"],["A"]],"rowId":{"tag":"var","index":0},"values":[]}},{"tag":"atom","atom":{"entity":[["TRealm"],["B"]],"rowId":{"tag":"var","index":1},"values":[{"column":0,"term":{"tag":"var","index":0}}]}},{"tag":"atom","atom":{"entity":[["TRealm"],["C"]],"rowId":{"tag":"var","index":2},"values":[{"column":0,"term":{"tag":"var","index":0}},{"column":1,"term":{"tag":"var","index":1}}]}}]}},{"path":[["TRealm"],["f"],["total"]],"value":{"ruleVariant":"monitored","varNames":[[["a"]],[["b"]]],"varTypes":[{"tag":"rowId","path":[["TRealm"],["A"]]},{"tag":"rowId","path":[["TRealm"],["B"]]}],"antecedents":[{"tag":"atom","atom":{"entity":[["TRealm"],["A"]],"rowId":{"tag":"var","index":0},"values":[]}},{"tag":"atom","atom":{"entity":[["TRealm"],["B"]],"rowId":{"tag":"var","index":1},"values":[{"column":0,"term":{"tag":"var","index":0}}]}}],"consequents":[{"tag":"atom","atom":{"entity":[["TRealm"],["f"]],"rowId":null,"values":[{"column":0,"term":{"tag":"var","index":0}},{"column":1,"term":{"tag":"var","index":1}}]}}]}}]}

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-prop-set.ts.output/TRealm.ts

@@ -0,0 +1,69 @@
+import schema from "./TRealm.json";
+export {schema};
+import * as runtime from "@coln-project/runtime";
+import * as T from "./T.ts";
+
+export class View {
+  root: T.View;
+
+  constructor(store: runtime.StoreHandle) {
+    this.root = {
+      A: (new runtime.RowIdSet.View(store, "TRealm.A", [])),
+      B: (a: runtime.Value) => {
+        return (new runtime.RowIdSet.View(store, "TRealm.B", [a]));
+      },
+      C: (a: runtime.Value) => {
+        return (b: runtime.Value) => {
+          return (new runtime.RowIdSet.View(store, "TRealm.C", [a, b]));
+        };
+      },
+      f: (a: runtime.Value) => {
+        return (b: runtime.Value) => {
+          return (new runtime.TableCellRef.View(store, "TRealm.f", [a, b]));
+        };
+      }
+    };
+  }
+}
+
+export class Transaction extends View {
+  root: T.Transaction;
+
+  constructor(
+    store: runtime.StoreHandle,
+    transaction: runtime.TransactionHandle
+  ) {
+    super(store);
+    this.root = {
+      A: (new runtime.RowIdSet.Transaction(store, "TRealm.A", [], transaction)),
+      B: (a: runtime.Value) => {
+        return (new runtime.RowIdSet.Transaction(
+          store,
+          "TRealm.B",
+          [a],
+          transaction
+        ));
+      },
+      C: (a: runtime.Value) => {
+        return (b: runtime.Value) => {
+          return (new runtime.RowIdSet.Transaction(
+            store,
+            "TRealm.C",
+            [a, b],
+            transaction
+          ));
+        };
+      },
+      f: (a: runtime.Value) => {
+        return (b: runtime.Value) => {
+          return (new runtime.TableCellRef.Transaction(
+            store,
+            "TRealm.f",
+            [a, b],
+            transaction
+          ));
+        };
+      }
+    };
+  }
+}

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-set-prop.coln

@@ -0,0 +1,9 @@
+theory T := sig
+  A : Prop
+  B : A -> Set
+  C : (a : A) -> B a -> Prop
+  f : (a : A) -> (b : B a) -> C a b
+end
+
+realm TRealm @ T
+end

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-set-prop.output

@@ -0,0 +1,45 @@
+-- elaborated
+global entry named T
+type: Theory
+value: sig
+  A : Prop
+  B : A -> Set
+  C : (a : A) -> B a -> Prop
+  f : (a : A) -> (b : B a) -> C a b
+end
+realm named TRealm
+generators: node
+  A = rel []
+  B = rel [a : TRealm.A []]
+  C = rel [a : TRealm.A [], b : TRealm.B [a := a]]
+  f = (fun [a : TRealm.A [], b : TRealm.B [a := a]] -> TRealm.C [
+    a := a,
+    b := b
+  ])
+end
+lowered: flatrealm
+  entities
+    table ℜ.A := []
+    table ℜ.B := [.a : ℜ.A]
+    table ℜ.C := [.a : ℜ.A, .b : ℜ.B]
+    table ℜ.f := [.a : ℜ.A, .b : ℜ.B, .c : ℜ.C] primarykey [.a, .b]
+  end
+  rules
+    enforced ℜ.A.foreignKey := ℜ.A [] ⊢ ⊤
+    enforced ℜ.B.foreignKey a := ℜ.B [.a ↦ a] ⊢ a ∈ ℜ.A []
+    enforced ℜ.C.foreignKey a b := ℜ.C [.a ↦ a, .b ↦ b] ⊢ a ∈ ℜ.A [] ∧ b ∈ ℜ.B [
+      .a ↦ a
+    ]
+    enforced ℜ.f.foreignKey a b c := ℜ.f [
+      .a ↦ a,
+      .b ↦ b,
+      .c ↦ c
+    ] ⊢ a ∈ ℜ.A [] ∧ b ∈ ℜ.B [.a ↦ a] ∧ c ∈ ℜ.C [.a ↦ a, .b ↦ b]
+    monitored ℜ.f.total a b := a ∈ ℜ.A [] ∧ b ∈ ℜ.B [.a ↦ a] ⊢ ℜ.f [
+      .a ↦ a,
+      .b ↦ b
+    ]
+  end
+end
+
+-- messages

packages/coln-compiler/test/golden/basic-ir/dependent-function-argument-prop-set-prop.ts.output/T.ts

@@ -0,0 +1,15 @@
+import * as runtime from "@coln-project/runtime";
+
+export interface View {
+  A: runtime.ColnSet.View;
+  B: (x: runtime.Value) => runtime.ColnSet.View;
+  C: (x: runtime.Value) => (x: runtime.Value) => runtime.ColnSet.View;
+  f: (x: runtime.Value) => (x: runtime.Value) => runtime.ColnRef.View;
+}
+
+export interface Transaction extends View {
+  A: runtime.ColnSet.Transaction;
+  B: (x: runtime.Value) => runtime.ColnSet.Transaction;
+  C: (x: runtime.Value) => (x: runtime.Value) => runtime.ColnSet.Transaction;
+  f: (x: runtime.Value) => (x: runtime.Value) => runtime.ColnRef.Transaction;
+}