From 40b089be6e557aad47f8d6e196da9a80f4ac8082 Mon Sep 17 00:00:00 2001 From: depsterr Date: Fri, 13 May 2022 19:46:05 +0200 Subject: [PATCH] it works ! a lot has changed --- pi.ipkg | 2 +- src/Check.idr | 59 +++++++++++++++++++++++++++++++++++++++++++ src/Convert.idr | 42 +++++++++++++++++++++++++++++++ src/Ctx.idr | 40 ----------------------------- src/Misc.idr | 25 ++++++++++++++++-- src/Normalize.idr | 64 ++++++++++++++++++----------------------------- src/Term.idr | 34 +++++++++++++++---------- src/Tests.idr | 23 +++++++++++++++++ src/Value.idr | 34 +++++++++++++------------ 9 files changed, 211 insertions(+), 112 deletions(-) delete mode 100644 src/Ctx.idr create mode 100644 src/Tests.idr diff --git a/pi.ipkg b/pi.ipkg index 1e59915..2502d42 100644 --- a/pi.ipkg +++ b/pi.ipkg @@ -2,11 +2,11 @@ package pi modules = Term , Value - , Ctx , Normalize , Convert , Check , Misc + , Tests options = "-p contrib --warnpartial" diff --git a/src/Check.idr b/src/Check.idr index e69de29..f2df073 100644 --- a/src/Check.idr +++ b/src/Check.idr @@ -0,0 +1,59 @@ +module Check + +import Control.Monad.RWS +import Control.Monad.Either +import Control.Monad.Identity +import Data.Vect +import Data.Fin + +import Term +import Value +import Normalize +import Misc +import Convert + + +%default total + +mutual + public export + -- terms types expected term + check : Ctx n -> Ctx n -> Value -> Term n -> PI Bool + check trs tys xpt' tr = do + xpt <- whnf xpt' + case tr of + TLam sc => case xpt of + VClos env (TPi a b) => do + v <- VGen <$> fresh + check (v :: trs) (VClos env a :: tys) (VClos (v :: env) b) sc + _ => oops "expected pi" + + TPi a b => case xpt of + VType => do + v <- VGen <$> fresh + (&&) <$> check trs tys VType a + <*> delay <$> check (v :: trs) (VClos trs a :: tys) VType b + + + _ => oops "expected type" + + _ => convert xpt =<< infer trs tys tr + + -- terms types term + infer : Ctx n -> Ctx n -> Term n -> PI Value + infer trs tys (TVar i _) = pure (index (natToFinLT i) tys) + infer trs tys TType = pure VType + infer trs tys (TApp f x) = infer trs tys f >>= whnf >>= + \case + VClos env (TPi a b) => do + if !(check trs tys (VClos env a) x) + then pure (VClos (VClos trs x :: env) b) + else oops "application" + + _ => oops "expected infer pi" + infer trs tys _ = oops "cannot infer type" + +public export +typecheck : Term 0 -> Term 0 -> Either String (Bool, List String) +typecheck tr ty = resolve $ (&&) <$> check [] [] VType ty + <*> delay <$> check [] [] (VClos [] ty) tr diff --git a/src/Convert.idr b/src/Convert.idr index e69de29..6946278 100644 --- a/src/Convert.idr +++ b/src/Convert.idr @@ -0,0 +1,42 @@ +module Convert + +import Term +import Value +import Misc +import Normalize + +import Control.Monad.RWS +import Control.Monad.Identity +import Control.Monad.Either + +import Data.Nat +import Data.Vect + +%default total + +public export +convert : 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 + (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 + <*> delay <$> convert x1 x2 + (VGen k1, VGen k2) => pure (k1 == k2) + + (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 + (&&) <$> convert (VClos env1 a1) + (VClos env2 a2) + <*> delay <$> convert (VClos (v :: env1) b1) + (VClos (v :: env2) b2) + _ => pure False diff --git a/src/Ctx.idr b/src/Ctx.idr deleted file mode 100644 index a782f78..0000000 --- a/src/Ctx.idr +++ /dev/null @@ -1,40 +0,0 @@ -module Ctx - -import Misc - -import Data.Nat - -%default total - -infixr 7 :: - -public export -data Ctx : (Index -> Type) -> Index -> Type where - Nil : Ctx ty 0 - (::) : {n : _} -> ty n -> Ctx ty n -> Ctx ty (S n) - --- indexed by amount of free variables -public export -data Closure : (Index -> Type) -> Index -> Type where - MkClosure : {n : _} -> Ctx ty n -> ty (m + n) -> Closure ty m - -public export -enclose : {n : _} -> ty n -> Closure ty n -enclose {n = n} ty = MkClosure Nil (rewrite plusZeroRightNeutral n in ty) - -public export -lookup : {m : _} -> (n : Nat) -> Ctx ty m -> LT n m -> ty (minus m (S n)) -lookup {m = S m} Z (x :: _) _ = rewrite minusZeroRight m in x -lookup (S n) (_ :: ctx) (LTESucc p) = lookup n ctx p - -public export -strengthen : Ctx ty (S n) -> Ctx ty n -strengthen (_ :: ctx) = ctx - -public export -strengthenTo : {n,m : _} -> Ctx ty m -> LTE n m -> Ctx ty n -strengthenTo {n = Z} _ _ = Nil -strengthenTo (x :: ctx) (LTESucc p) - = case lteSplit p of - Left Refl => x :: ctx - Right p2 => strengthenTo ctx p2 diff --git a/src/Misc.idr b/src/Misc.idr index ce0be6b..86b2b6b 100644 --- a/src/Misc.idr +++ b/src/Misc.idr @@ -1,5 +1,9 @@ module Misc +import Control.Monad.RWS +import Control.Monad.Identity +import Control.Monad.Either + import Data.Nat %default total @@ -14,11 +18,28 @@ Name = String public export PI : Type -> Type -PI = Either String +PI = EitherT String (RWS () (List String) Nat) + +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) public export oops : String -> PI a -oops = Left +oops = left + +public export +fresh : PI Nat +fresh = do + i <- get + put (S i) + pure i + +public export +logS : String -> PI () +logS = tell . (:: []) public export lteTransp : LTE a b -> a = c -> b = d -> LTE c d diff --git a/src/Normalize.idr b/src/Normalize.idr index 1d00053..273c37f 100644 --- a/src/Normalize.idr +++ b/src/Normalize.idr @@ -2,54 +2,38 @@ module Normalize import Term import Value -import Ctx import Misc +import Control.Monad.RWS +import Control.Monad.Identity +import Control.Monad.Either + import Data.Nat +import Data.Vect %default total --- There is some nasty assert_total here since I cannot solve the halting problem - -public export -asTerm : NF -> Term 0 -asTerm NType = TType -asTerm (NLam ty sc) = TLam (asTerm ty) sc -asTerm (NPi ty sc) = TPi (asTerm ty) sc - -public export -fromNF : NF -> Glue -fromNF nf = MkGlue (asTerm nf) (const (pure nf)) - -substStep : {n,m : _} -> Term m -> LTE m n -> Term (S n) -> Term n -substStep {m = m} tr p tr' = case tr' of -- case somehow needed for idris not to loop over metavariable - TType => TType - (TLam ty sc) => TLam (substStep tr p ty) (substStep tr (lteSuccRight p) sc) - (TPi ty sc) => TPi (substStep tr p ty) (substStep tr (lteSuccRight p) sc) - (TApp f x) => TApp (substStep tr p f) (substStep tr p x) - (TVar i p) => case natEqDecid m i of - Left p => ?que1 - Right p => ?que2 - mutual - evalClosure : {n : Nat} -> Closure Term 0 -> PI (Term n) - evalClosure (MkClosure ctx term) = eval [] ctx term >>= pure . weaken0 . asTerm + public export + app : Value -> Value -> PI Value + app (VClos env (TLam sc)) x = eval (x :: env) sc + app f x = pure (VApp f x) public export - eval : {n : Nat} -> List (Closure Term 0) -> Ctx Term n -> Term n -> PI NF - eval stack env TType = pure NType - - -- dirty - eval (thunk :: stack) env (TLam _ sc) = eval stack (!(assert_total (evalClosure thunk)) :: env) sc - - eval stack env (TApp f x) = eval (MkClosure env x :: stack) env x - - eval stack env (TVar m p) = assert_total $ eval stack (strengthenTo env minusLte) (lookup m env p) - - eval stack env (TPi ty sc) = ?idk - - eval [] env (TLam ty sc) = ?what + eval : Ctx n -> Term n -> PI Value + eval env (TVar i _) = pure (index (natToFinLT i) env) + eval env (TApp f x) = do + f' <- eval env f + x' <- eval env x + assert_total (app f' x') -- :( + eval env TType = pure VType + eval env tr = pure (VClos env tr) public export -fromTerm : Term 0 -> Glue -fromTerm term = MkGlue term (eval [] Nil) +whnf : Value -> PI Value +whnf (VApp f x) = do + f' <- whnf f + x' <- whnf x + app f' x' +whnf (VClos env tr) = eval env tr +whnf v = pure v diff --git a/src/Term.idr b/src/Term.idr index ef79a66..16e8f93 100644 --- a/src/Term.idr +++ b/src/Term.idr @@ -12,17 +12,25 @@ import Misc -} public export data Term : (_ : Index) -> Type where - 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 - TVar : (n : Nat) -> LT n m -> Term m -- Variable + 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 public export weaken : {p, q : _} -> LTE p q -> Term p -> Term q weaken _ TType = TType -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 (TLam sc) = TLam (weaken (LTESucc p) sc) +weaken p (TPi a bx) = TPi (weaken p a) (weaken (LTESucc p) bx) weaken p (TApp f x) = TApp (weaken p f) (weaken p x) {- Getting new index @@ -50,11 +58,11 @@ weaken p (TApp f x) = TApp (weaken p f) (weaken p x) (r + q) - p < q ∎ -} -weaken {p = S p} {q = S q} (LTESucc p1) (TVar r p2') = +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))) + LTESucc p2 => TVar (minus (r + q) p) + (LTESucc (lteTransp (minusLteMonotone (plusLteMonotoneRight q r p p2)) Refl (minusPlus p))) + -public export -weaken0 : {n : _} -> Term 0 -> Term n -weaken0 = weaken LTEZero +weaken1 : {n : _} -> Term n -> Term (S n) +weaken1 = weaken lteS diff --git a/src/Tests.idr b/src/Tests.idr new file mode 100644 index 0000000..5673397 --- /dev/null +++ b/src/Tests.idr @@ -0,0 +1,23 @@ +module Tests + +import Term +import Check +import Check + +import Data.Nat + +%default total + +a : {p, q : Nat} -> lt p q = True -> LT p q +a {p} {q} eq = ltReflectsLT p q eq + +test1 : Either String (Bool, List String) +test1 = typecheck (TLam (TLam (TVar 0 (a Refl)))) + (TPi TType (TPi (TVar 0 (a Refl)) (TVar 1 (a Refl)))) + +test2 : Either String (Bool, List String) +test2 = typecheck (TLam (TLam (TLam (TLam (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl))))))) + (TPi TType + (TPi (TPi (TVar 0 (a Refl)) TType) + (TPi (TPi (TVar 1 (a Refl)) (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl)))) + (TPi (TVar 2 (a Refl)) (TApp (TVar 2 (a Refl)) (TVar 0 (a Refl))))))) diff --git a/src/Value.idr b/src/Value.idr index 9a32f47..02ee5af 100644 --- a/src/Value.idr +++ b/src/Value.idr @@ -2,24 +2,26 @@ module Value import Term import Misc -import Ctx + +import Data.Vect %default total -public export -data NF : Type where - NType : NF -- Type of types - NLam : NF -> Term 1 -> NF -- Lambda abstraction - NPi : NF -> Term 1 -> NF -- Pi Type +mutual + public export + data Value : Type where + VType : Value + VGen : Nat -> Value + VApp : Value -> Value -> Value + VClos : Ctx n -> Term n -> Value + + public export + Ctx : Index -> Type + Ctx i = Vect i Value public export -data Glue : Type where - MkGlue : Term 0 -> (Term 0 -> PI NF) -> Glue - -public export -getTerm : Glue -> Term 0 -getTerm (MkGlue term _) = term - -public export -getNF : Glue -> PI NF -getNF (MkGlue term f) = f term +Show Value where + show VType = "VType" + show (VGen i) = "VGen " ++ show i + show (VApp f x) = "VApp (" ++ show f ++ ") (" ++ show x ++ ")" + show (VClos e t) = "VClos (" ++ assert_total (show e) ++ ") (" ++ show t ++ ")"