From b53a575821637f7ed33589d3aa2fa1007cf7cf7c Mon Sep 17 00:00:00 2001 From: depsterr Date: Tue, 7 Jun 2022 14:53:24 +0200 Subject: [PATCH] began work on inductives (this commit doesn't compile) --- TODO.md | 5 +++ pi.ipkg | 2 ++ src/Misc.idr | 15 ++++++++- src/Parsing/Lex.idr | 1 + src/Parsing/Parse.idr | 1 + src/Term.idr | 73 +++++++++++++++++++++++++++++++++---------- 6 files changed, 80 insertions(+), 17 deletions(-) create mode 100644 TODO.md create mode 100644 src/Parsing/Lex.idr create mode 100644 src/Parsing/Parse.idr diff --git a/TODO.md b/TODO.md new file mode 100644 index 0000000..606b94f --- /dev/null +++ b/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. diff --git a/pi.ipkg b/pi.ipkg index 2502d42..17b9e02 100644 --- a/pi.ipkg +++ b/pi.ipkg @@ -7,6 +7,8 @@ modules = Term , Check , Misc , Tests + , Parsing.Parse + , Parsing.Lex options = "-p contrib --warnpartial" diff --git a/src/Misc.idr b/src/Misc.idr index 86b2b6b..4ef3963 100644 --- a/src/Misc.idr +++ b/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 diff --git a/src/Parsing/Lex.idr b/src/Parsing/Lex.idr new file mode 100644 index 0000000..e31a156 --- /dev/null +++ b/src/Parsing/Lex.idr @@ -0,0 +1 @@ +module Parsing.Lex diff --git a/src/Parsing/Parse.idr b/src/Parsing/Parse.idr new file mode 100644 index 0000000..4a56dd8 --- /dev/null +++ b/src/Parsing/Parse.idr @@ -0,0 +1 @@ +module Parsing.Parse diff --git a/src/Term.idr b/src/Term.idr index bed2d83..4bb3715 100644 --- a/src/Term.idr +++ b/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 - they are valid, that is, it is impossible to construct an ill-scoped term. + Can things be ereased? +-} + + +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 - TType : Term n -- Type of types - TLam : Term (S n) -> Term n -- Lambda abstraction (λ _ . Scope) - TPi : Term n -> Term (S n) -> Term n -- Pi type (∏ _ : A . B _ ) - TApp : Term n -> Term n -> Term n -- Appliction - TVar : (n : Nat) -> LT n m -> Term m -- Variable - -public export -Show (Term n) where - show TType = "TType" - show (TLam sc) = "TLam (" ++ show sc ++ ")" - show (TPi ty sc) = "TPi (" ++ show ty ++ ") (" ++ show sc ++ ")" - show (TApp f x) = "TApp (" ++ show f ++ ") (" ++ show x ++ ")" - show (TVar i _) = "TVar " ++ show i +Show (Term n v) where + show TType = "Type" + show (TLam sc) = "Lam {" ++ show sc ++ "}" + show (TPi ty sc) = "Pi [" ++ show ty ++ "] [" ++ show sc ++ "]" + show (TApp f x) = "App (" ++ show f ++ ") (" ++ show x ++ ")" + show (TVar i) = "Var " ++ show i + show (TLet tr ty sc) = "Let <" ++ show tr ++ "> : <" ++ show ty ++ "> in <" ++ show sc ++ ">" + show (TIDef _ t) = "IDef [...] in " ++ show t + show (TIType n) = "IType[#" ++ show n ++ "]" + show (TIElim n) = "IElim[#" ++ show n ++ "]" + show (TICons n m) = "ICons[#" ++ show n ++ "][#" ++ show m ++ "]"