commit bdb30a2d6298508595f0abaa32cce582dd97dab9
Author: depsterr <depsterr@protonmail.com>
Date:   Sat Apr 23 15:18:06 2022 +0200

    initial commit

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..fc48728
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+build
+src/build
diff --git a/makefile b/makefile
new file mode 100644
index 0000000..28d688b
--- /dev/null
+++ b/makefile
@@ -0,0 +1,3 @@
+.PHONY: all
+all:
+	idris2 --build pi.ipkg
diff --git a/pi.ipkg b/pi.ipkg
new file mode 100644
index 0000000..c65eaec
--- /dev/null
+++ b/pi.ipkg
@@ -0,0 +1,15 @@
+package pi
+
+modules = Term
+        , Value
+        , Normalize
+        , Convert
+        , Check
+        , Misc
+
+options = "-p contrib --warnpartial"
+
+main = Main
+sourcedir = "src"
+
+executable = "addict"
diff --git a/src/Check.idr b/src/Check.idr
new file mode 100644
index 0000000..e69de29
diff --git a/src/Convert.idr b/src/Convert.idr
new file mode 100644
index 0000000..e69de29
diff --git a/src/Main.idr b/src/Main.idr
new file mode 100644
index 0000000..09b50ac
--- /dev/null
+++ b/src/Main.idr
@@ -0,0 +1,4 @@
+module Main
+
+main : IO ()
+main = pure ()
diff --git a/src/Misc.idr b/src/Misc.idr
new file mode 100644
index 0000000..672d569
--- /dev/null
+++ b/src/Misc.idr
@@ -0,0 +1,21 @@
+module Misc
+
+import Data.Nat
+
+%default total
+
+public export
+Index : Type
+Index = Nat
+
+public export
+Name : Type
+Name = String
+
+public export
+PI : Type -> Type
+PI = Maybe
+
+public export
+lteTransp : LTE a b -> a = c -> b = d -> LTE c d
+lteTransp p Refl Refl = p
diff --git a/src/Normalize.idr b/src/Normalize.idr
new file mode 100644
index 0000000..5e353c5
--- /dev/null
+++ b/src/Normalize.idr
@@ -0,0 +1,3 @@
+module Normalize
+
+%default total
diff --git a/src/Term.idr b/src/Term.idr
new file mode 100644
index 0000000..ac96d80
--- /dev/null
+++ b/src/Term.idr
@@ -0,0 +1,58 @@
+module Term
+
+import Data.Nat
+
+import Misc
+
+%default total
+
+{-
+  The type of terms is indexed by the size of the environment in which
+  they are valid, that is, it is impossible to construct an ill-scoped term.
+-}
+public export
+data Term : (_ : Index) -> Type where
+  TType   : Term n                         -- The type of types (type in type)
+  TDef    : Name -> Term n                 -- Axiomised term
+  TLam    : Term n -> Term (S n) -> Term n -- Lambda abstraction (λ Type -> Scope)
+  TPi     : Term n -> Term (S n) -> Term n -- Pi type            (∏ A    -> B a  )
+  TApp    : Term n -> Term n -> Term n     -- Appliction
+  TVar    : (n : Nat) -> LT n m -> Term m  -- Variable
+
+public export
+weaken : {p, q : _} -> LTE p q -> Term p -> Term q
+weaken _ TType    = TType
+weaken _ (TDef n) = TDef n
+weaken p (TLam ty sc) = TLam (weaken p ty) (weaken (LTESucc p) sc)
+weaken p (TPi  a  bx) = TLam (weaken p a ) (weaken (LTESucc p) bx)
+weaken p (TApp f x) = TApp (weaken p f) (weaken p x)
+{-
+  Getting new index
+  =================
+
+    New index is 
+
+      old + Δctx
+
+    in this case
+
+      r + (q - p)
+
+    which since p <= q is equivalent to
+
+      (r + q) - p
+
+
+  Proving validity of new index
+  =============================
+
+              r <= p           => (+mono)
+          r + q <= p + q       => (-mono)
+    (r + q) - p <= (p + q) - p => (lteTransp -+)
+    (r + q) - p <= q           ∎
+
+-}
+weaken {p = S p} {q = S q} (LTESucc p1) (TVar r p2') =
+  case p2' of 
+    LTESucc p2 => TVar (minus (r + q) p)
+      (LTESucc (lteTransp (minusLteMonotone (plusLteMonotoneRight q r p p2)) Refl (minusPlus p)))
diff --git a/src/Value.idr b/src/Value.idr
new file mode 100644
index 0000000..ac32ad8
--- /dev/null
+++ b/src/Value.idr
@@ -0,0 +1,12 @@
+module Value
+
+import Term
+import Misc
+
+%default total
+
+public export
+data NF : Type where
+  NType : NF
+  NDef  : Name -> NF
+  NLam  : NF -> (Term 1 -> PI NF) -> NF