diff --git a/README.md b/README.md index e44ac82..b6bb6d9 100644 --- a/README.md +++ b/README.md @@ -22,12 +22,12 @@ A dependently typed system # TODO -* Repl - * Defs - * Performence optimisation + * Parsing !!! (this is like 90% of the time currently lmao) * Memoize normalisation and conversion somehow? +* Repl + * Universes * Implicit arguments diff --git a/makefile b/makefile index 0b15bd4..0281e1e 100644 --- a/makefile +++ b/makefile @@ -1,6 +1,8 @@ .PHONY: all run all: idris2 --build pi.ipkg +clean: + idris2 --clean pi.ipkg run: ./build/exec/pi test: diff --git a/pi.ipkg b/pi.ipkg index 10a86ec..5d64b60 100644 --- a/pi.ipkg +++ b/pi.ipkg @@ -5,7 +5,6 @@ modules = Core.Check , Core.Misc , Core.Normalize , Core.Term - , Core.Tests , Core.Value , Parser.Parse diff --git a/src/Core/Check.idr b/src/Core/Check.idr index d2218be..b355644 100644 --- a/src/Core/Check.idr +++ b/src/Core/Check.idr @@ -5,6 +5,8 @@ import Control.Monad.Either import Control.Monad.Identity import Data.Vect import Data.Fin +import Data.IOArray +import Data.IORef import Core.Term import Core.Value @@ -12,21 +14,27 @@ import Core.Normalize import Core.Misc import Core.Convert - %default total - + -- extend environment, used to ensure environment is always in normal form -extV : Ctx n -> Value -> PI (Ctx (S n)) +extV : {auto deftrs : RefA DTR Value} + -> {auto frst : Ref NST Nat} + -> Ctx n -> Value -> PI (Ctx (S n)) extV ctx val = whnf val >>= pure . (`Data.Vect.(::)` ctx) -- to extend, closure env, term -extT : Ctx m -> Ctx n -> Term n -> PI (Ctx (S m)) +extT : {auto deftrs : RefA DTR Value} + -> {auto frst : Ref NST Nat} + -> Ctx m -> Ctx n -> Term n -> PI (Ctx (S m)) extT ctx env = extV ctx . VClos env mutual public export -- terms types expected term - check : Ctx n -> Ctx n -> Value -> Term n -> PI Bool + check : {auto deftrs : RefA DTR Value} + -> {auto deftys : RefA DTY Value} + -> {auto frst : Ref NST Nat} + -> Ctx n -> Ctx n -> Value -> Term n -> PI Bool check trs tys xpt' tr = do xpt <- whnf xpt' case tr of @@ -49,7 +57,11 @@ mutual _ => convert xpt =<< infer trs tys tr -- terms types term - infer : Ctx n -> Ctx n -> Term n -> PI Value + public export + infer : {auto deftrs : RefA DTR Value} + -> {auto deftys : RefA DTY Value} + -> {auto frst : Ref NST Nat} + -> Ctx n -> Ctx n -> Term n -> PI Value infer trs tys TType = pure VType infer trs tys TTop = pure VType infer trs tys TBot = pure VType @@ -57,14 +69,19 @@ mutual infer trs tys TStar = pure VTop infer trs tys TZero = pure VNat infer trs tys (TVar i) = pure (index i tys) + infer trs tys (TDef i) = do + res <- getArr DTY i + case res of + Just x => pure x + Nothing => oops "TDef type lookup" infer trs tys (TApp f x) = infer trs tys f >>= whnf >>= - \case - VClos env (TPi a b) => do - guardS ("app x:\n" ++ show !(whnf (VClos env a))) =<< check trs tys (VClos env a) x - tr <- whnf (VClos trs x) - pure (VClos (tr :: env) b) + \case + VClos env (TPi a b) => do + guardS ("app x:\n" ++ show !(whnf (VClos env a))) =<< check trs tys (VClos env a) x + tr <- whnf (VClos trs x) + pure (VClos (tr :: env) b) - _ => oops "expected infer pi" + _ => oops "expected infer pi" infer trs tys (TPi a b) = do v <- VGen <$> fresh @@ -141,6 +158,9 @@ mutual infer trs tys x = oops ("cannot infer type " ++ show x) public export -typecheck : Term 0 -> Term 0 -> Either String (Bool, List String) +typecheck : {auto deftrs : RefA DTR Value} + -> {auto deftys : RefA DTY Value} + -> {auto frst : Ref NST Nat} + -> Term 0 -> Term 0 -> IO (Either String Bool) typecheck tr ty = resolve $ (&&) <$> check [] [] VType ty <*> delay <$> check [] [] (VClos [] ty) tr diff --git a/src/Core/Convert.idr b/src/Core/Convert.idr index 0713d25..4187f19 100644 --- a/src/Core/Convert.idr +++ b/src/Core/Convert.idr @@ -11,102 +11,100 @@ import Control.Monad.Either import Data.Nat import Data.Vect +import Data.IOArray +import Data.IORef %default total public export -convert : Value -> Value -> PI Bool +convert : {auto deftrs : RefA DTR Value} + -> {auto frst : Ref NST Nat} + -> Value -> Value -> PI Bool convert u1 u2 = do u1' <- whnf u1 u2' <- whnf u2 - logS ("checking equality of terms '" ++ show u1 ++ "' and '" ++ show u2 ++ "'.") - logS ("with value representations '" ++ show u1' ++ "' and '" ++ show u2' ++ "'.") - assert_total $ -- :( - case (u1', u2') of - (VType, VType) => pure True - (VTop, VTop) => pure True - (VStar, VStar) => pure True - (VBot, VBot) => pure True - (VNat, VNat) => pure True + assert_total $ case (u1', u2') of + (VType, VType) => pure True + (VTop, VTop) => pure True + (VStar, VStar) => pure True + (VBot, VBot) => pure True + (VNat, VNat) => pure True - (VGen k1, VGen k2) => pure (k1 == k2) + (VGen k1, VGen k2) => pure (k1 == k2) - (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 <*> delay <$> convert x1 x2 + (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 <*> delay <$> convert x1 x2 - (VClos env1 (TLam sc1), VClos env2 (TLam sc2)) => do - v <- VGen <$> fresh - convert (VClos (v :: env1) sc1) (VClos (v :: env2) sc2) + (VClos env1 (TLam sc1), VClos env2 (TLam sc2)) => do + v <- VGen <$> fresh + convert (VClos (v :: env1) sc1) (VClos (v :: env2) sc2) - (VClos env1 (TPi a1 b1), VClos env2 (TPi a2 b2)) => do - v <- VGen <$> fresh - guardS (show a1 ++ " | " ++ show a2) =<< convert (VClos env1 a1) (VClos env2 a2) - convert (VClos (v :: env1) b1) (VClos (v :: env2) b2) + (VClos env1 (TPi a1 b1), VClos env2 (TPi a2 b2)) => do + v <- VGen <$> fresh + (&&) <$> convert (VClos env1 a1) (VClos env2 a2) + <*> delay <$> convert (VClos (v :: env1) b1) (VClos (v :: env2) b2) - (VClos env1 (TSigma a1 b1), VClos env2 (TSigma a2 b2)) => do - termGuard env1 env2 a1 a2 - termConv env1 env2 b1 b2 + (VClos env1 (TSigma a1 b1), VClos env2 (TSigma a2 b2)) => do + termGuard env1 env2 a1 a2 + termConv env1 env2 b1 b2 - (VClos env1 (TPair a1 b1), VClos env2 (TPair a2 b2)) => do - termGuard env1 env2 a1 a2 - termConv env1 env2 b1 b2 + (VClos env1 (TPair a1 b1), VClos env2 (TPair a2 b2)) => do + termGuard env1 env2 a1 a2 + termConv env1 env2 b1 b2 - (VClos env1 (TId ty1 a1 b1), VClos env2 (TId ty2 a2 b2)) => do - termGuard env1 env2 ty1 ty2 - termGuard env1 env2 a1 a2 - termConv env1 env2 b1 b2 - - (VClos env1 (TRefl ty1 tr1), VClos env2 (TRefl ty2 tr2)) => do - termGuard env1 env2 ty1 ty2 - termConv env1 env2 tr1 tr2 + (VClos env1 (TId ty1 a1 b1), VClos env2 (TId ty2 a2 b2)) => do + termGuard env1 env2 ty1 ty2 + termGuard env1 env2 a1 a2 + termConv env1 env2 b1 b2 + + (VClos env1 (TRefl ty1 tr1), VClos env2 (TRefl ty2 tr2)) => do + termGuard env1 env2 ty1 ty2 + termConv env1 env2 tr1 tr2 - (VClos env1 (TNatInd c1 z1 s1), VClos env2 (TNatInd c2 z2 s2)) => do - termGuard env1 env2 c1 c2 - termGuard env1 env2 z1 z2 - termConv env1 env2 s1 s2 + (VClos env1 (TNatInd c1 z1 s1), VClos env2 (TNatInd c2 z2 s2)) => do + termGuard env1 env2 c1 c2 + termGuard env1 env2 z1 z2 + termConv env1 env2 s1 s2 - (VClos _ TZero, VClos _ TZero) => pure True + (VClos _ TZero, VClos _ TZero) => pure True - (VClos env1 (TSuc n1), VClos env2 (TSuc n2)) => do - termConv env1 env2 n1 n2 + (VClos env1 (TSuc n1), VClos env2 (TSuc n2)) => do + termConv env1 env2 n1 n2 - (VClos env1 (TJ ty1 a1 b1 c1 d1), VClos env2 (TJ ty2 a2 b2 c2 d2)) => do - termGuard env1 env2 ty1 ty2 - termGuard env1 env2 a1 a2 - termGuard env1 env2 b1 b2 - termGuard env1 env2 c1 c2 - termConv env1 env2 d1 d2 + (VClos env1 (TJ ty1 a1 b1 c1 d1), VClos env2 (TJ ty2 a2 b2 c2 d2)) => do + termGuard env1 env2 ty1 ty2 + termGuard env1 env2 a1 a2 + termGuard env1 env2 b1 b2 + termGuard env1 env2 c1 c2 + termConv env1 env2 d1 d2 - (VClos env1 (TSigInd a1 b1 c1 f1), VClos env2 (TSigInd a2 b2 c2 f2)) => do - termGuard env1 env2 a1 a2 - termGuard env1 env2 b1 b2 - termGuard env1 env2 c1 c2 - termConv env1 env2 f1 f2 + (VClos env1 (TSigInd a1 b1 c1 f1), VClos env2 (TSigInd a2 b2 c2 f2)) => do + termGuard env1 env2 a1 a2 + termGuard env1 env2 b1 b2 + termGuard env1 env2 c1 c2 + termConv env1 env2 f1 f2 - (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => termConv env1 env2 c1 c2 + (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => termConv env1 env2 c1 c2 - (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do - termGuard env1 env2 c1 c2 - termConv env1 env2 st1 st2 + (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do + termGuard env1 env2 c1 c2 + termConv env1 env2 st1 st2 - -- η rules - -- fresh cannot appear in vsc, so this is fine - (vsc, VClos env (TLam (TApp sc (TVar 0)))) => do - v <- VGen <$> fresh - convert vsc (VClos (v :: env) sc) - (VClos env (TLam (TApp sc (TVar 0))), vsc) => do - v <- VGen <$> fresh - convert vsc (VClos (v :: env) sc) + -- η rules + -- fresh cannot appear in vsc, so this is fine + (vsc, VClos env (TLam (TApp sc (TVar 0)))) => do + v <- VGen <$> fresh + convert vsc (VClos (v :: env) sc) + (VClos env (TLam (TApp sc (TVar 0))), vsc) => do + v <- VGen <$> fresh + convert vsc (VClos (v :: env) sc) - -- VApp - -- (VApp v1 v2 , VClos env (TApp t1 t2)) => (&&) <$> convert v1 (VClos env t1) <*> delay <$> convert v1 (VClos env t1) - -- (VClos env (TApp t1 t2), VApp v1 v2) => (&&) <$> convert v1 (VClos env t1) <*> delay <$> convert v1 (VClos env t1) - - (v1, v2) => oops ("cannot convert \n" ++ show v1 ++ "\n\n" ++ show v2) - where - termConv : Ctx n -> Ctx m -> Term n -> Term m -> PI Bool - termConv env1 env2 a1 a2 = do - a1' <- eval env1 a1 - a2' <- eval env2 a2 - convert a1' a2' - termGuard : Ctx n -> Ctx m -> Term n -> Term m -> PI () - termGuard env1 env2 a1 a2 = guardS "termGuard" =<< termConv env1 env2 a1 a2 + (v1, v2) => oops ("cannot convert \n" ++ show v1 ++ "\n\n" ++ show v2) +where + termConv : Ctx n -> Ctx m -> Term n -> Term m -> PI Bool + termConv env1 env2 a1 a2 = do + a1' <- eval env1 a1 + a2' <- eval env2 a2 + convert a1' a2' + termGuard : Ctx n -> Ctx m -> Term n -> Term m -> PI () + termGuard env1 env2 a1 a2 = termConv env1 env2 a1 a2 >>= + guardS ("cannot convert \n" ++ show a1 ++ "\n\n" ++ show a2) diff --git a/src/Core/Misc.idr b/src/Core/Misc.idr index dfdac45..9dcb371 100644 --- a/src/Core/Misc.idr +++ b/src/Core/Misc.idr @@ -6,6 +6,8 @@ import Control.Monad.Either import Data.Nat import Data.Vect +import Data.IORef +import Data.IOArray %default total @@ -19,13 +21,46 @@ Name = String public export PI : Type -> Type -PI = EitherT String (RWS () (List String) Nat) +PI = EitherT String IO public export -resolve : PI a -> Either String (a, List String) -resolve a = case runRWS (runEitherT a) () 0 of - (Left e, _) => Left e - (Right r, _, s) => Right (r, s) +data NST : Type where +public export +data DTY : Type where +public export +data DTR : Type where + +public export +data RefP : Type -> Type -> Type where + MkRefP : (label : Type) -> a -> RefP label a + +public export +RefA : Type -> Type -> Type +RefA label a = RefP label (IOArray a) + +public export +Ref : Type -> Type -> Type +Ref label a = RefP label (IORef a) + +public export +getRef : HasIO io => (label : Type) -> {auto ref : Ref label a} -> io a +getRef _ {ref = MkRefP _ ref} = readIORef ref + +public export +putRef : HasIO io => (label : Type) -> {auto ref : Ref label a} -> a -> io () +putRef _ {ref = MkRefP _ ref} = writeIORef ref + +public export +getArr : HasIO io => (label : Type) -> {auto ref : RefA label a} -> Int -> io (Maybe a) +getArr _ {ref = MkRefP _ ref} = readArray ref + +public export +putArr : HasIO io => (label : Type) -> {auto ref : RefA label a} -> Int -> a -> io Bool +putArr _ {ref = MkRefP _ ref} = writeArray ref + +public export +resolve : PI a -> IO (Either String a) +resolve a = runEitherT a public export oops : String -> PI a @@ -36,19 +71,9 @@ guardS : String -> Bool -> PI () guardS str True = pure () guardS str False = oops str - public export -fresh : PI Nat +fresh : {auto frst : Ref NST Nat} -> PI Nat fresh = do - i <- get - put (S i) + i <- getRef NST + putRef NST (S i) pure i - -public export -logS : String -> PI () -logS = tell . (`Prelude.(::)` []) - -public export -headM : Vect n a -> Maybe a -headM [] = Nothing -headM (x :: _) = Just x diff --git a/src/Core/Normalize.idr b/src/Core/Normalize.idr index 9066146..4d866fd 100644 --- a/src/Core/Normalize.idr +++ b/src/Core/Normalize.idr @@ -10,12 +10,16 @@ import Control.Monad.Either import Data.Nat import Data.Vect +import Data.IOArray +import Data.IORef %default total mutual public export - app : Value -> Value -> PI Value + app : {auto deftrs : RefA DTR Value} + -> {auto frst : Ref NST Nat} + -> Value -> Value -> PI Value app (VClos env (TLam sc)) x = eval (x :: env) sc app (VClos env (TTopInd c st)) VTop = eval env st @@ -36,8 +40,15 @@ mutual app f x = pure (VApp f x) public export - eval : Ctx n -> Term n -> PI Value - eval env (TVar i) = pure (index i env) + eval : {auto deftrs : RefA DTR Value} + -> {auto frst : Ref NST Nat} + -> Ctx n -> Term n -> PI Value + eval env (TVar i) = pure (index i env) + eval env (TDef i) = do + res <- getArr DTR i + case res of + Just x => pure x + Nothing => oops "TDef term lookup" eval env TType = pure VType eval env TTop = pure VTop eval env TStar = pure VStar @@ -55,7 +66,9 @@ mutual eval env tr = pure (VClos env tr) public export - whnf : Value -> PI Value + whnf : {auto deftrs : RefA DTR Value} + -> {auto frst : Ref NST Nat} + -> Value -> PI Value whnf (VClos env tr) = eval env tr whnf (VApp f x) = do f' <- whnf f diff --git a/src/Core/Term.idr b/src/Core/Term.idr index d5528fd..8cab18a 100644 --- a/src/Core/Term.idr +++ b/src/Core/Term.idr @@ -9,6 +9,9 @@ import Core.Misc {- 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. + + Defs are used for performance reasons and are not implemented in a type safe manner. + if a def is not in scope the checker will scream at you. -} public export data Term : (_ : Index) -> Type where @@ -40,8 +43,11 @@ data Term : (_ : Index) -> Type where TPi : Term n -> Term (S n) -> Term n -- Pi type (∏ _ : A . B _ ) TApp : Term n -> Term n -> Term n -- Appliction + TVar : Fin n -> Term n -- Variable + TDef : Int -> Term n -- Def Variable + infixl 3 `TApp` public export @@ -76,6 +82,7 @@ Show (Term n) where show (TApp f x) = "(" ++ show f ++ ") TApp (" ++ show x ++ ")" show (TVar i) = "Var " ++ show i + show (TDef i) = "Def " ++ show i public export weakTr : Term n -> Term (S n) @@ -105,6 +112,7 @@ weakTr = go 0 go n (TVar i) = if weaken i < n then TVar (weaken i) else TVar (FS i) + go n (TDef i) = TDef i public export weakTr2 : Term n -> Term (2+n) diff --git a/src/Core/Tests.idr b/src/Core/Tests.idr deleted file mode 100644 index 1ff9b3b..0000000 --- a/src/Core/Tests.idr +++ /dev/null @@ -1,155 +0,0 @@ -module Core.Tests - -import Core.Term -import Core.Check -import Core.Convert -import Core.Misc -import Core.Normalize -import Core.Value - -import Control.Monad.RWS -import Control.Monad.Identity -import Control.Monad.Either - -import Data.Fin - -%default total - -{- λA. λx. x : ∏ (A : Type) → A → A -} -test_id : Either String (Bool, List String) -test_id = typecheck (TLam (TLam (TVar 0))) - (TPi TType (TPi (TVar 0) (TVar 1))) - -{- λA. λB. λf. λx. f x : ∏ (A : Type) ∏ (B : A → Type) ∏ (f : ∏ (x : A) B x) ∏ (x : A) B x -} -test_app : Either String (Bool, List String) -test_app = typecheck (TLam (TLam (TLam (TLam (TVar 1 `TApp` TVar 0))))) - (TPi TType - (TPi (TPi (TVar 0) TType) - (TPi (TPi (TVar 1) (TVar 1 `TApp` TVar 0)) - (TPi (TVar 2) (TVar 2 `TApp` TVar 0))))) - -{- λf. λx. f x ≃ λf. λx. (λy. f y) x -} -eta_test : Either String (Bool, List String) -eta_test = resolve action - where - action : PI Bool - action = do - x <- eval ctx0 (TLam (TLam (TVar 1 `TApp` TVar 0))) - y <- eval ctx0 (TLam (TLam (TLam (TVar 2 `TApp` TVar 0) `TApp` TVar 0))) - convert x y - -addition : Term 0 -addition = TNatInd (TLam (TPi TNat TNat)) - (TLam (TVar 0)) - (TLam {-n-} (TLam {-n+-} (TLam {-m-} (TSuc (TVar 1 `TApp` TVar 0))))) - -additionty : Term 0 -additionty = TPi TNat (TPi TNat TNat) - -additionty_test : Either String (Bool, List String) -additionty_test = typecheck additionty TType - -addition_test : Either String (Bool, List String) -addition_test = typecheck addition additionty - -{- 2 + 1 = 3 -} -addition_compute_test : Either String (Bool, List String) -addition_compute_test = resolve action - where - action : PI Bool - action = do - x <- eval ctx0 (addition `TApp` TSuc (TSuc TZero) `TApp` TSuc TZero) - y <- eval ctx0 (TSuc (TSuc (TSuc TZero))) - convert x y - -multi : Term 0 -multi = TNatInd (TLam (TPi TNat TNat)) - (TLam TZero) - (TLam {-n-} (TLam {-n*-} (TLam {-m-} (weakTr3 addition `TApp` TVar 0 `TApp` (TVar 1 `TApp` TVar 0))))) - -multity : Term 0 -multity = TPi TNat (TPi TNat TNat) - -multity_test : Either String (Bool, List String) -multity_test = typecheck multity TType - -multi_test : Either String (Bool, List String) -multi_test = typecheck multi multity - -{- 2 * 3 = 6 -} -multi_compute_test : Either String (Bool, List String) -multi_compute_test = resolve action - where - action : PI Bool - action = do - x <- eval ctx0 (multi `TApp` TSuc (TSuc TZero) `TApp` TSuc (TSuc (TSuc TZero))) - y <- eval ctx0 (TSuc (TSuc (TSuc (TSuc (TSuc (TSuc TZero)))))) - convert x y - --- no, not that kind -unit_test : Either String (Bool, List String) -unit_test = typecheck TStar TTop - -absurd_test : Either String (Bool, List String) -absurd_test = typecheck (TLam (TBotInd (TLam (TVar 1)))) (TPi TType (TPi TBot (TVar 1))) - -pr1ty : Term 0 -pr1ty = TPi TType {- A : Type -} - (TPi (TPi (TVar 0) TType) {- B : A → Type -} - (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -} - (TVar 2))) - -pr1 : Term 0 -pr1 = TLam {- A : Type -} - (TLam {- B : A → Type -} - (TSigInd (TVar 1) (TVar 0) (TLam {-ΣAB-} (TVar 2)) (TLam (TLam (TVar 1))))) - -pr1ty_test : Either String (Bool, List String) -pr1ty_test = typecheck pr1ty TType - -pr1_test : Either String (Bool, List String) -pr1_test = typecheck pr1 pr1ty - -pr2ty : Term 0 -pr2ty = TPi TType {- A : Type -} - (TPi (TPi (TVar 0) TType) {- B : A → Type -} - (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -} - (TVar 1 `TApp` (TSigInd (TVar 2) (TVar 1) (TLam (TVar 3)) (TLam (TLam (TVar 1))) `TApp` TVar 0)))) - -pr2 : Term 0 -pr2 = TLam {- A : Type -} - (TLam {- B : A → Type -} - (TSigInd (TVar 1) - (TVar 0) - (TLam {-ΣAB-} - (TVar 1 `TApp` (TSigInd (TVar 2) (TVar 1) (TLam (TVar 3)) (TLam (TLam (TVar 1))) `TApp` TVar 0))) - (TLam (TLam (TVar 0))))) - -pr2ty_test : Either String (Bool, List String) -pr2ty_test = typecheck pr2ty TType - -pr2_test : Either String (Bool, List String) -pr2_test = typecheck pr2 pr2ty - -pr2ty_let : Term 0 -pr2ty_let = TLet pr1ty pr1 {- pr1 : pr1ty -} - (TPi TType {- A : Type -} - (TPi (TPi (TVar 0) TType) {- B : A → Type -} - (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -} - (TVar 1 `TApp` (TVar 3 `TApp` TVar 2 `TApp` TVar 1 `TApp` TVar 0))))) - -pr2_let : Term 0 -pr2_let = TLet pr1ty pr1 {- pr1 : pr1ty -} - (TLam {- A : Type -} - (TLam {- B : A → Type -} - (TSigInd (TVar 1) - (TVar 0) - (TLam {-ΣAB-} - (TVar 1 `TApp` (TVar 3 `TApp` TVar 2 `TApp` TVar 1 `TApp` TVar 0))) - (TLam (TLam (TVar 0)))))) - -pr2ty_let_test : Either String (Bool, List String) -pr2ty_let_test = typecheck pr2ty_let TType - -pr2_let_test : Either String (Bool, List String) -pr2_let_test = typecheck pr2_let pr2ty_let diff --git a/src/Main.idr b/src/Main.idr index 2d77fa4..9607846 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -2,22 +2,59 @@ module Main import Core.Check import Core.Term +import Core.Value +import Core.Normalize +import Core.Misc import Parser.Parse +import Control.Monad.Either import Data.Vect import Data.String +import Data.IORef +import Data.IOArray import System import System.File -unwrap : {a : Type} -> Show a => Either a b -> IO b -unwrap {a = a} = \case +smartPrint : {a : Type} -> Show a => a -> IO () +smartPrint {a = String} = putStrLn +smartPrint {a = _} = printLn + +isTrue : String -> Bool -> IO () +isTrue _ True = pure () +isTrue str False = putStrLn str >> exitFailure + +unwrapCC : {a : Type} -> Show a => IO b -> Either a b -> IO b +unwrapCC {a = a} iob = \case Left e => do - case a of - String => putStrLn e - _ => printLn e - exitFailure + smartPrint e + iob Right s => pure s +unwrap : {a : Type} -> Show a => Either a b -> IO b +unwrap = unwrapCC exitFailure + +createNST : IO (Ref NST Nat) +createNST = do + nstIoRef <- newIORef 0 + pure (MkRefP NST nstIoRef) + +createDTX : (label : Type) -> Int -> IO (RefA label Value) +createDTX label n = do + arr <- newArray n + pure (MkRefP label arr) + +typeCheck : {auto deftrs : RefA DTR Value} + -> {auto deftys : RefA DTY Value} + -> {auto frst : Ref NST Nat} + -> Int -> List (Term 0, Term 0) -> IO () +typeCheck i [] = pure () +typeCheck i ((ty, tr) :: defs) = do + vty <- unwrap =<< resolve (eval [] ty) + vtr <- unwrap =<< resolve (eval [] tr) + isTrue "putArr DTY" =<< putArr DTY i vty + isTrue "putArr DTR" =<< putArr DTR i vtr + typeCheck (i+1) defs + replRead : IO String replRead = do line <- getLine @@ -27,19 +64,40 @@ replRead = do ":exit" => exitSuccess _ => pure line -repl : (n : Nat) -> Vect n String -> IO () -repl n env = do +repl : {auto deftrs : RefA DTR Value} + -> {auto deftys : RefA DTY Value} + -> {auto frst : Ref NST Nat} + -> List String -> IO a +repl strs = do line <- replRead - printLn =<< unwrap (parseEnv n env line) - repl n env + term <- unwrapCC (repl strs) (parseEnv strs line) + type <- unwrapCC (repl strs) =<< resolve (whnf =<< infer [] [] term) + val <- unwrapCC (repl strs) =<< resolve (whnf =<< eval [] term) + putStr "inferred type: " + printLn type + putStr "weak head normal form: " + printLn val + repl strs main : IO () main = getArgs >>= \case - (_ :: x :: _) => do - putStr (x ++ ": ") - res <- readFile x >>= unwrap >>= unwrap . parsetoplevel - >>= unwrap . (`typecheck` TTop) - if fst res - then putStrLn ("Success !") - else unwrap (Left res) - _ => repl 0 [] + (_ :: x :: xs) => do + putStrLn (x ++ ": ") + putStr "Parsing: " + (strs, res) <- readFile x >>= unwrap >>= unwrap . toplevel + putStrLn " OK!" + let rlen = cast (length res) + nst <- createNST + dtr <- createDTX DTR rlen + dty <- createDTX DTY rlen + putStr "Typechecking: " + typeCheck 0 res + putStrLn "OK!" + case xs of + ("repl" :: _) => repl strs + _ => exitSuccess + _ => do + nst <- createNST + dtr <- createDTX DTR 0 + dty <- createDTX DTY 0 + repl [] diff --git a/src/Parser/Parse.idr b/src/Parser/Parse.idr index b3aeed9..de717a5 100644 --- a/src/Parser/Parse.idr +++ b/src/Parser/Parse.idr @@ -211,40 +211,40 @@ lexPi str = {- Basic idea, parsing has a list of the identifiers to convert to -} {- de bruijn indecies, and a Nat to keep track of context size -} mutual - expr : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - expr n env = tpi n env - <|> tsigma n env - <|> tarr n env - <|> (do - e <- expr1 n env - tapp n env e <|> pure e) + expr : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + expr defs n env = tpi defs n env + <|> tsigma defs n env + <|> tarr defs n env + <|> (do + e <- expr1 defs n env + tapp defs n env e <|> pure e) - expr1 : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - expr1 n env = ttopind n env - <|> tbotind n env - <|> tsuc n env - <|> tnatind n env - <|> tsigind n env - <|> tid n env - <|> trefl n env - <|> tj n env - <|> (do - t <- term n env - tapp n env t <|> pure t) + expr1 : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + expr1 defs n env = ttopind defs n env + <|> tbotind defs n env + <|> tsuc defs n env + <|> tnatind defs n env + <|> tsigind defs n env + <|> tid defs n env + <|> trefl defs n env + <|> tj defs n env + <|> (do + t <- term defs n env + tapp defs n env t <|> pure t) - term : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - term n env = ttype - <|> ttop - <|> tstar - <|> tbot - <|> tnat - <|> tnum - <|> tpair n env - <|> tlet n env - <|> tlam n env - <|> tvar n env - <|> paren n env + term : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + term defs n env = ttype + <|> ttop + <|> tstar + <|> tbot + <|> tnat + <|> tnum + <|> tpair defs n env + <|> tlet defs n env + <|> tlam defs n env + <|> tvar defs n env + <|> paren defs n env ttype : Grammar () PiToken True (Term n) ttype = match PTType >> pure TType @@ -255,22 +255,22 @@ mutual tstar : Grammar () PiToken True (Term n) tstar = match PTStar >> pure TStar - ttopind : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - ttopind n env = do + ttopind : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + ttopind defs n env = do match PTTopInd commit - c <- term n env - st <- term n env + c <- term defs n env + st <- term defs n env pure (TTopInd c st) tbot : Grammar () PiToken True (Term n) tbot = match PTBot >> pure TBot - tbotind : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tbotind n env = do + tbotind : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tbotind defs n env = do match PTBotInd commit - c <- term n env + c <- term defs n env pure (TBotInd c) tnat : Grammar () PiToken True (Term n) @@ -285,162 +285,161 @@ mutual conv 0 = TZero conv (S n) = TSuc (conv n) - tsuc : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tsuc n env = do + tsuc : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tsuc defs n env = do match PTSuc commit - TSuc <$> term n env + TSuc <$> term defs n env - tnatind : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tnatind n env = do + tnatind : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tnatind defs n env = do match PTNatInd commit - c <- term n env - z <- term n env - s <- term n env + c <- term defs n env + z <- term defs n env + s <- term defs n env pure (TNatInd c z s) - tsigma : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tsigma n env = do + tsigma : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tsigma defs n env = do match PTSigma commit match PTLParen arg <- match PTIdentifier match PTColon - a <- expr n env + a <- expr defs n env match PTRParen - b <- expr (S n) (arg :: env) + b <- expr defs (S n) (arg :: env) pure (TSigma a (TLam b)) - tpair : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tpair n env = do + tpair : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tpair defs n env = do match PTLParen - x <- expr n env + x <- expr defs n env match PTComma commit - y <- expr n env + y <- expr defs n env match PTRParen pure (TPair x y) - tsigind : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tsigind n env = do + tsigind : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tsigind defs n env = do match PTSigInd commit - a <- term n env - b <- term n env - c <- term n env - f <- term n env + a <- term defs n env + b <- term defs n env + c <- term defs n env + f <- term defs n env pure (TSigInd a b c f) - tid : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tid n env = do + tid : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tid defs n env = do match PTId commit - ty <- term n env - a <- term n env - b <- term n env + ty <- term defs n env + a <- term defs n env + b <- term defs n env pure (TId ty a b) - trefl : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - trefl n env = do + trefl : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + trefl defs n env = do match PTRefl commit - ty <- term n env - tr <- term n env + ty <- term defs n env + tr <- term defs n env pure (TRefl ty tr) - tj : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tj n env = do + tj : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tj defs n env = do match PTJ commit - ty <- term n env - a <- term n env - b <- term n env - c <- term n env - d <- term n env + ty <- term defs n env + a <- term defs n env + b <- term defs n env + c <- term defs n env + d <- term defs n env pure (TJ ty a b c d) - tlet : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tlet n env = do + tlet : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tlet defs n env = do match PTLet commit arg <- match PTIdentifier match PTColon - ty <- expr n env + ty <- expr defs n env match PTDefEq - tr <- expr n env + tr <- expr defs n env match PTIn - tri <- expr (S n) (arg :: env) + tri <- expr defs (S n) (arg :: env) pure (TLet ty tr tri) - tlam : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tlam n env = do + tlam : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tlam defs n env = do match PTLambda commit arg <- match PTIdentifier match PTDot - e <- expr (S n) (arg :: env) + e <- expr defs (S n) (arg :: env) pure (TLam e) - tpi : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tpi n env = do + tpi : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tpi defs n env = do match PTPi commit match PTLParen arg <- match PTIdentifier match PTColon - a <- expr n env + a <- expr defs n env match PTRParen - b <- expr (S n) (arg :: env) + b <- expr defs (S n) (arg :: env) pure (TPi a b) - tarr : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tarr n env = do - l <- expr1 n env + tarr : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tarr defs n env = do + l <- expr1 defs n env match PTArrow commit - r <- expr (S n) ("" :: env) + r <- expr defs (S n) ("" :: env) pure (TPi l r) - tapp : (n : Nat) -> Vect n String -> Term n -> Grammar () PiToken True (Term n) - tapp n env e1 = do - e2 <- term n env - tapp1 n env (TApp e1 e2) + tapp : List String -> (n : Nat) -> Vect n String -> Term n -> Grammar () PiToken True (Term n) + tapp defs n env e1 = do + e2 <- term defs n env + tapp1 defs n env (TApp e1 e2) - tapp1 : (n : Nat) -> Vect n String -> Term n -> Grammar () PiToken False (Term n) - tapp1 n env e = tapp n env e <|> pure e + tapp1 : List String -> (n : Nat) -> Vect n String -> Term n -> Grammar () PiToken False (Term n) + tapp1 defs n env e = tapp defs n env e <|> pure e - tvar : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - tvar n env = do + tvar : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + tvar defs n env = do str <- match PTIdentifier commit - fromMaybe (fail ("'" ++ str ++ "' not in env")) (pure . TVar <$> findIndex (== str) env) + fromMaybe (fromMaybe (fail ("'" ++ str ++ "' not idefs n env")) + (pure . TDef . cast . finToInteger <$> findIndex (== str) defs)) + (pure . TVar <$> findIndex (== str) env) - paren : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) - paren n env = do + paren : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) + paren defs n env = do match PTLParen commit - e <- expr n env + e <- expr defs n env match PTRParen pure e -definitions : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) -definitions n env = do +definitions : List String -> Grammar () PiToken True (List String, List (Term 0, Term 0)) +definitions defs = do match PTLet commit arg <- match PTIdentifier match PTColon - ty <- expr n env + ty <- expr defs 0 [] match PTDefEq - tr <- expr n env - next <- definitions (S n) (arg :: env) <|> pure TStar - pure (TLet ty tr next) + tr <- expr defs 0 [] + next <- definitions (arg :: defs) <|> pure ([], []) + pure (arg :: fst next, (ty, tr) :: snd next) -toplevel : Grammar () PiToken True (Term 0) -toplevel = definitions 0 [] - -parsePi : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) -> List (WithBounds PiToken) -> Either String (Term n) -parsePi n env parseEntry toks = +parsePi : List String -> Grammar () PiToken True a -> List (WithBounds PiToken) -> Either String a +parsePi defs parseEntry toks = case parse parseEntry $ filter (not . ignored) toks of Right (l, []) => Right l Right (_, l) => Left ("contains tokens that were not consumed: " ++ show l) @@ -452,20 +451,20 @@ parsePi n env parseEntry toks = public export -parse : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) -> String -> Either String (Term n) -parse n env parseEntry x = +parse : List String -> Grammar () PiToken True a -> String -> Either String a +parse defs parseEntry x = case lexPi x of - Just toks => parsePi n env parseEntry toks + Just toks => parsePi defs parseEntry toks Nothing => Left "Failed to lex." public export parse0 : String -> Either String (Term 0) -parse0 = parse 0 [] (expr 0 []) +parse0 = parse [] (expr [] 0 []) public export -parseEnv : (n : Nat) -> Vect n String -> String -> Either String (Term n) -parseEnv n env = parse n env (expr n env) +parseEnv : List String -> String -> Either String (Term 0) +parseEnv defs = parse defs (expr defs 0 []) public export -parsetoplevel : String -> Either String (Term 0) -parsetoplevel = parse 0 [] (toplevel) +toplevel : String -> Either String (List String, List (Term 0, Term 0)) +toplevel = parse [] (definitions []) diff --git a/src/Parser/Tests.idr b/src/Parser/Tests.idr deleted file mode 100644 index ffa4823..0000000 --- a/src/Parser/Tests.idr +++ /dev/null @@ -1,89 +0,0 @@ -module Parser.Tests - -import Core.Term -import Core.Check -import Core.Convert -import Core.Misc -import Core.Normalize -import Core.Value - -import Control.Monad.RWS -import Control.Monad.Identity -import Control.Monad.Either - -import Data.Fin - -import Parser.Parse - -%default total - -convCheck : Term 0 -> Term 0 -> Either String (Bool, List String) -convCheck a b = resolve action - where - action : PI Bool - action = do - x <- eval ctx0 a - y <- eval ctx0 b - convert x y - -{- λA. λx. x : ∏ (A : Type) → A → A -} -test_id : Either String (Bool, List String) -test_id = do - ty <- parse0 "Π ( A : Type ) A → A" - tr <- parse0 "λA.λx.x" - typecheck tr ty - -{- λA. λB. λf. λx. f x : ∏ (A : Type) ∏ (B : A → Type) ∏ (f : ∏ (x : A) B x) ∏ (x : A) B x -} -test_app : Either String (Bool, List String) -test_app = do - ty <- parse0 "Π (A : Type) Π (B : A → Type) Π (f : Π (x : A) B x) Π (x : A) B x" - tr <- parse0 "λA. λB. λf. λx. f x" - typecheck tr ty - -{- λf. f ≃ λf. λx. f x -} -eta_test : Either String (Bool, List String) -eta_test = do - a <- parse0 "λf. f" - b <- parse0 "λf. λx. f x" - convCheck a b - -additionty_test : Either String (Bool, List String) -additionty_test = do - ty <- parse0 "ℕ → ℕ → ℕ" - typecheck ty TType - -addition_test : Either String (Bool, List String) -addition_test = do - ty <- parse0 "ℕ → ℕ → ℕ" - tr <- parse0 "ℕ-ind (λ_. ℕ → ℕ) (λx.x) (λn.λnp.λm. suc (np m))" - typecheck tr ty - --- no, not that kind -unit_test : Either String (Bool, List String) -unit_test = do - ty <- parse0 "⊤" - tr <- parse0 "★" - typecheck tr ty - -absurd_test : Either String (Bool, List String) -absurd_test = do - ty <- parse0 "Π(A : Type) ⊥ → A" - tr <- parse0 "λA. ⊥-ind (λ_. A)" - typecheck tr ty - - -pr1_test : Either String (Bool, List String) -pr1_test = do - tr <- parse0 $ "let pr1 : Π (A : Type) Π (B : A → Type) (Σ (a : A) B a) → A" - ++ "≔ λA.λB. Σ-ind A B (λ_. A) (λa.λBa. a)" - ++ "in ★" - typecheck tr TTop - -pr1_pr2_test : Either String (Bool, List String) -pr1_pr2_test = do - tr <- parse0 $ "let pr1 : Π (A : Type) Π (B : A → Type) (Σ (a : A) B a) → A" - ++ "≔ λA.λB. Σ-ind A B (λ_. A) (λa.λBa. a)" - ++ "in let pr2 : Π (A : Type) Π (B : A → Type) Π (s : Σ (a : A) B a) B (pr1 A B s)" - ++ "≔ λA.λB. Σ-ind A B (λs. B (pr1 A B s)) (λa.λBa. Ba)" - ++ "in ★" - typecheck tr TTop diff --git a/tests/id1.pi b/tests/id1.pi new file mode 100644 index 0000000..ede76bf --- /dev/null +++ b/tests/id1.pi @@ -0,0 +1,3 @@ +let transport : Π (A : Type) Π (f : A → Type) Π (x : A) Π (y : A) + Id A x y → f x → f y + ≔ λA.λf.λx.λy. J A x y (λa.λb.λ_. f a → f b) (λa.a) diff --git a/tests/id2.pi b/tests/id2.pi new file mode 100644 index 0000000..d6b25af --- /dev/null +++ b/tests/id2.pi @@ -0,0 +1,3 @@ +let ap : Π (A : Type) Π (B : Type) Π (f : A → B) + Π (x : A) Π (y : A) Id A x y → Id B (f x) (f y) + ≔ λA.λB.λf.λx.λy. J A x y (λa.λb.λ_. Id B (f a) (f b)) (refl B (f x))