enough for today

pi.ipkg

@@ -2,6 +2,7 @@ package pi
 
 modules = Term
         , Value
+        , Ctx
         , Normalize
         , Convert
         , Check

src/Ctx.idr

@@ -0,0 +1,18 @@
+module Ctx
+
+import Misc
+
+import Data.Nat
+
+%default total
+
+infixr 7 ::
+
+public export
+data Ctx : (Index -> Type) -> (_ : Index) -> Type where
+  Nil  : Ctx ty 0
+  (::) : ty n -> Ctx ty n -> Ctx ty (S n)
+
+public export
+data Closure : (Index -> Type) -> Type where
+  MkClosure : Ctx ty n -> ty n -> Closure ty

src/Misc.idr

@@ -14,8 +14,17 @@ Name = String
 
 public export
 PI : Type -> Type
-PI = Maybe
+PI = Either String
+
+public export
+oops : String -> PI a
+oops = Left
 
 public export
 lteTransp : LTE a b -> a = c -> b = d -> LTE c d
 lteTransp p Refl Refl = p
+
+public export
+lteS : {n : _} -> LTE n (S n)
+lteS {n = Z}   = LTEZero
+lteS {n = S n} = LTESucc lteS

src/Normalize.idr

@@ -1,3 +1,25 @@
 module Normalize
 
+import Term
+import Value
+import Ctx
+import Misc
+
+import Data.Nat
+
 %default total
+
+public export
+eval : List (Closure Term) -> Ctx Term n -> Term n -> PI NF
+eval stack ctx TType      = pure NType
+eval stack ctx (TVar n p) = pure NType
+
+eval stack ctx (TApp f x) = eval (MkClosure ctx x :: stack) ctx f
+eval _ _ _ = oops "eval"
+
+public export
+finalize : Term 0 -> PI NF
+finalize term = eval [] Nil term
+
+-- idris can't see that there is no case for TVar itself
+finalize (TVar n p) = void (succNotLTEzero p)

src/Term.idr

@@ -12,8 +12,7 @@ import Misc
 -}
 public export
 data Term : (_ : Index) -> Type where
-  TType   : Term n                         -- The type of types (type in type)
-  TDef    : Name -> Term n                 -- Axiomised term
+  TType   : Term n                         -- Type of types
   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
@@ -22,10 +21,9 @@ data Term : (_ : Index) -> Type where
 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)
+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
   =================
@@ -46,10 +44,10 @@ weaken p (TApp f x) = TApp (weaken p f) (weaken p x)
   Proving validity of new index
   =============================
 
-              r <= p           => (+mono)
-          r + q <= p + q       => (-mono)
-    (r + q) - p <= (p + q) - p => (lteTransp -+)
-    (r + q) - p <= q           ∎
+              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') =

src/Value.idr

@@ -7,6 +7,6 @@ import Misc
 
 public export
 data NF : Type where
-  NType : NF
-  NDef  : Name -> NF
-  NLam  : NF -> (Term 1 -> PI NF) -> NF
+  NType : NF                    -- Type of types
+  NLam  : NF    -> Term 1 -> NF -- Lambda abstraction
+  NPi   : NF    -> Term 1 -> NF -- Pi Type