began work on inductives (this commit doesn't compile)

TODO.md

@@ -0,0 +1,5 @@
+# Inductives
+
+figure out model for terms, current one is nice but makes values incredibly inconvenient.
+
+Update rest of code to fit new terms, or remodel terms again with a global environment of inductive definitions, rather than introducing them in the terms. With this one could also index values by this inductive environment.

pi.ipkg

@@ -7,6 +7,8 @@ modules = Term
         , Check
         , Misc
         , Tests
+        , Parsing.Parse
+        , Parsing.Lex
 
 options = "-p contrib --warnpartial"
 

src/Misc.idr

@@ -5,6 +5,7 @@ import Control.Monad.Identity
 import Control.Monad.Either
 
 import Data.Nat
+import Data.Vect
 
 %default total
 
@@ -39,7 +40,7 @@ fresh = do
 
 public export
 logS : String -> PI ()
-logS = tell . (:: [])
+logS = tell . (`Prelude.Basics.(::)` [])
 
 public export
 lteTransp : LTE a b -> a = c -> b = d -> LTE c d
@@ -77,3 +78,15 @@ natEqDecid Z (S _)    = Left absurd
 natEqDecid (S n) (S m) = case natEqDecid n m of
                               Right p => Right (cong S p)
                               Left  p => Left  (p . prevEq n m)
+
+public export
+LTv : {m : _} -> (n : Nat) -> Vect m ty -> Type
+LTv {m = m} n _ = LT n m
+
+public export
+nat2Fin : (n : Nat) -> LT n m -> Fin m
+nat2Fin n p = natToFinLT n
+
+public export
+len : {n : _} -> Vect n ty -> Nat
+len {n = n} _ = n

src/Parsing/Lex.idr

@@ -0,0 +1 @@
+module Parsing.Lex

src/Parsing/Parse.idr

@@ -0,0 +1 @@
+module Parsing.Parse

src/Term.idr

@@ -1,27 +1,68 @@
 module Term
 
 import Data.Nat
+import Data.Vect
+import Data.Fin
 
 import Misc
 
 %default total
 
 {-
-  The type of terms is indexed by the size of the environment in which
+  Can things be ereased?
-  they are valid, that is, it is impossible to construct an ill-scoped term.
+-}
+
+
+mutual
+  {-
+    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.
+
+    It is also indexed by the number of tags of the defined inductive types.
+  -}
+  public export
+  data Term : (ctx : Index) -> (tags : Vect n Nat) -> Type where
+    TType  : Term n v                                         -- Type of types
+    TLam   : Term (S n) v -> Term n v                         -- Lambda     (λ _ . #0)
+    TPi    : Term n v -> Term (S n) v -> Term n v             -- Pi type    (∏ _ : #0 . #1 _ )
+    TApp   : Term n v -> Term n v -> Term n v                 -- Appliction
+    TVar   : Fin n -> Term n v                                -- Variable
+    TLet   : Term n v -> Term n v -> Term (S n) v -> Term n v -- Let        (let _ = #1 : #0 in #2)
+    TIDef  : Inductive m n v -> Term n (m :: v) -> Term n v   -- Inductive definition
+    TIType : Fin (len v) -> Term n v                          -- Inductive type
+    TIElim : Fin (len v) -> Term n v                          -- Inductive eliminator
+    TICons : (n : Fin (len v)) -> Fin (index n v) -> Term m v -- Inductive constructor
+
+
+  {-
+    The type of a constructor, indexed like terms
+  -}
+  public export
+  data Constructor : (ctx : Index) -> (tags : Vect n Nat) -> Type where
+    Tr   : Term n v      -> Constructor n v                          -- a term
+    Sum  : Constructor n v -> Constructor (S n) v -> Constructor n v -- Σ _ : #0 , #1
+
+
+  {-
+    The type of an inductive definition. It is a vector of constructors.
+It's indexed by the number of constructors as well as the indecies for terms.
+  -}
+  public export
+  Inductive : Nat -> Index -> Vect n Nat -> Type
+  Inductive cons ctx tags = Vect cons (Constructor ctx (cons :: tags))
+
+{-
+   Use some different brackets to make it easier to read
 -}
 public export
-data Term : (_ : Index) -> Type where
+Show (Term n v) where
-  TType   : Term n                              -- Type of types
+  show TType     = "Type"
-  TLam    : Term (S n) -> Term n                -- Lambda abstraction (λ _ . Scope)
+  show (TLam sc) = "Lam {" ++ show sc ++ "}"
-  TPi     : Term n -> Term (S n) -> Term n      -- Pi type            (∏ _ : A . B _ )
+  show (TPi  ty sc) = "Pi [" ++ show ty ++ "] [" ++ show sc ++ "]"
-  TApp    : Term n -> Term n -> Term n          -- Appliction
+  show (TApp f x) = "App (" ++ show f ++ ") (" ++ show x ++ ")"
-  TVar    : (n : Nat) -> LT n m -> Term m -- Variable
+  show (TVar i) = "Var " ++ show i
-
+  show (TLet tr ty sc) = "Let <" ++ show tr ++ "> : <" ++ show ty ++ "> in <" ++ show sc ++ ">"
-public export
+  show (TIDef _ t) = "IDef [...] in " ++ show t
-Show (Term n) where
+  show (TIType n) = "IType[#" ++ show n ++ "]"
-  show TType     = "TType"
+  show (TIElim n) = "IElim[#" ++ show n ++ "]"
-  show (TLam sc) = "TLam (" ++ show sc ++ ")"
+  show (TICons n m) = "ICons[#" ++ show n ++ "][#" ++ show m ++ "]"
-  show (TPi  ty sc) = "TPi (" ++ show ty ++ ") (" ++ show sc ++ ")"
-  show (TApp f x) = "TApp (" ++ show f ++ ") (" ++ show x ++ ")"
-  show (TVar i _) = "TVar " ++ show i