From f73f3c53867131d80e3d9e03cb9923c73d3340dc Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 1 May 2024 01:05:04 -0500
Subject: [PATCH] init

---
 .envrc     |  1 +
 .gitignore |  4 ++++
 Makefile   | 15 ++++++++++++++
 T.mod      |  5 +++++
 T.sig      | 14 +++++++++++++
 flake.lock | 58 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 flake.nix  |  6 ++++++
 7 files changed, 103 insertions(+)
 create mode 100644 .envrc
 create mode 100644 .gitignore
 create mode 100644 Makefile
 create mode 100644 T.mod
 create mode 100644 T.sig
 create mode 100644 flake.lock
 create mode 100644 flake.nix

diff --git a/.envrc b/.envrc
new file mode 100644
index 0000000..3550a30
--- /dev/null
+++ b/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..ee95bb3
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,4 @@
+.direnv
+*.lp
+*.lpo
+depend
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..940919a
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,15 @@
+.PHONY: T
+all: T
+
+T: T.lp
+
+%.lpo : %.mod %.sig
+	tjcc $*
+
+%.lp : %.lpo
+	tjlink $*
+
+-include depend
+depend: *.mod *.sig
+	tjdepend *.mod > depend-stage
+	mv depend-stage depend
diff --git a/T.mod b/T.mod
new file mode 100644
index 0000000..90f0951
--- /dev/null
+++ b/T.mod
@@ -0,0 +1,5 @@
+module T.
+
+
+
+/* vim: set ft=lprolog : */
diff --git a/T.sig b/T.sig
new file mode 100644
index 0000000..f348a3e
--- /dev/null
+++ b/T.sig
@@ -0,0 +1,14 @@
+sig T.
+
+kind ty type.
+kind tm type.
+
+type nat ty.
+type arr (ty -> ty) -> ty.
+
+type zero tm.
+type suc tm -> tm.
+type lam string -> ty -> tm -> tm.
+type ap tm -> tm -> tm.
+
+
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..3ab3a32
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,58 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
+        "type": "github"
+      },
+      "original": {
+        "id": "flake-utils",
+        "type": "indirect"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1663551060,
+        "narHash": "sha256-e2SR4cVx9p7aW/XnVsGsWZBplApA9ZJUjc0fejJhnYo=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "8a5b9ee7b7a2b38267c9481f5c629c015108ab0d",
+        "type": "github"
+      },
+      "original": {
+        "id": "nixpkgs",
+        "type": "indirect"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..0cf3651
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,6 @@
+{
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let pkgs = import nixpkgs { inherit system; };
+      in { devShell = pkgs.mkShell { packages = with pkgs; [ teyjus ]; }; });
+}