Browse Source

Fix most warnings.

We compile with `-Wall -Wno-name-shadowing`, mostly because
-Wname-shadowing is very annoying.
hydraz 1 year ago
parent
commit
357b4802ce
11 changed files with 68 additions and 53 deletions
  1. 1 0
      dtt.cabal
  2. 1 7
      src/Main.hs
  3. 38 19
      src/Parser.hs
  4. 1 0
      src/Syntax/Pretty.hs
  5. 1 1
      src/Syntax/Refresh.hs
  6. 1 1
      src/Syntax/Subst.hs
  7. 1 1
      src/Types/Context.hs
  8. 0 1
      src/Types/Equality.hs
  9. 10 9
      src/Types/Infer.hs
  10. 5 0
      src/Types/Normalise.hs
  11. 9 14
      src/Types/Unify.hs

+ 1 - 0
dtt.cabal

@@ -24,3 +24,4 @@ executable dtt
   hs-source-dirs:      src
   default-language:    Haskell2010
   default-extensions:  FlexibleContexts
+  ghc-options: -Wall -Wno-name-shadowing

+ 1 - 7
src/Main.hs

@@ -1,16 +1,10 @@
 module Main where
 
-import Syntax.Subst
-import Syntax.Refresh
-import Syntax
-
-import Types.Normalise
 import Types.Context
 import Types.Infer
 
-import Parser.Lexer
-import Parser
 import Text.Parsec
+import Parser
 
 import Data.These
 

+ 38 - 19
src/Parser.hs

@@ -2,57 +2,76 @@
 module Parser where
 
 import Text.Parsec.String
+import Text.Parsec.Expr
 import Text.Parsec
 import Parser.Lexer
 
 import Syntax
 
-term' :: Parser Term
-term' = set <|> try (parens typeHint) <|> parens term <|> pi <|> lam <|> lett <|> var where
+typeP' :: Parser Type
+typeP' = set <|> pi <|> var where
   set = reserved "Set" *> (Set . fromInteger <$> integer)
-  var = Variable . Name <$> identifier
-  typeHint = do
-    nm <- term
-    colon
-    TypeHint nm <$> term
   pi = do
     reserved "Π" <|> reserved "forall"
     (nm, ty) <- parens $ do
       nm <- Name <$> identifier
       colon
-      (nm,) <$> term
+      (nm,) <$> typeP
     reservedOp "->"
-    Pi nm ty <$> term
+    Pi nm ty <$> typeP
+    <?> "relevant dependent (Π) type"
+
+typeP :: Parser Type
+typeP = typeOpP where
+  typeOpP = buildExpressionParser table type' <?> "type"
+  type' = foldl1 App <$> many1 typeP'
+  table = [ [ binary "->" arrow AssocRight ]]
+  binary n f a = flip Infix a $ do
+    reservedOp n
+    pure f
+  arrow :: Type -> Type -> Type
+  arrow a g = Pi Irrelevant a g
+
+termP' :: Parser Term
+termP' = try (parens typePHint) <|> parens termP <|> lam <|> lett <|> var where
+  typePHint = do
+    nm <- termP
+    colon
+    TypeHint nm <$> typeP
   lam = do
     reservedOp "\\"
     (nm, ty) <- parens $ do
       nm <- Name <$> identifier
       colon
-      (nm,) <$> term
+      (nm,) <$> typeP
     reservedOp "."
-    Lam nm ty <$> term
+    Lam nm ty <$> termP
   lett = do
     reserved "let"
     nm <- Name <$> identifier
     reservedOp "="
-    val <- term
+    val <- termP
     reservedOp ";"
-    Let nm val <$> term
+    Let nm val <$> termP
+
+var :: Parser Term
+var = Variable . Name <$> identifier
 
-term = foldl1 App <$> many1 term'
+termP :: Parser Term
+termP = foldl1 App <$> many1 termP'
 
-toplevel :: Parser Toplevel
-toplevel = postulate <|> define <|> Eval <$> term where
+toplevelP :: Parser Toplevel
+toplevelP = postulate <|> define <|> Eval <$> termP where
   postulate = do
     reserved "postulate"
     x <- Name <$> identifier
     reservedOp ":"
-    Postulate x <$> term
+    Postulate x <$> typeP'
   define = do
     reserved "define"
     x <- Name <$> identifier
     reservedOp ":="
-    Define x <$> term
+    Define x <$> termP
 
 program :: Parser Program
-program = sepBy1 toplevel dot <* eof
+program = sepBy1 toplevelP dot <* eof

+ 1 - 0
src/Syntax/Pretty.hs

@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
 module Syntax.Pretty where
 
 import Syntax

+ 1 - 1
src/Syntax/Refresh.hs

@@ -14,5 +14,5 @@ freshStr = (alpha !!) <$> fresh
 
 refresh :: Member Fresh r => Var -> Eff r Var
 refresh (Name x) = Refresh x <$> fresh
-refresh (Refresh x k) = Refresh x <$> fresh
+refresh (Refresh x _) = Refresh x <$> fresh
 refresh Irrelevant = Refresh <$> freshStr <*> fresh

+ 1 - 1
src/Syntax/Subst.hs

@@ -10,7 +10,7 @@ import Syntax
 
 freeIn :: Term -> S.Set Var
 freeIn (Variable k) = S.singleton k
-freeIn (Set k) = S.empty
+freeIn (Set _) = S.empty
 freeIn (TypeHint x t) = freeIn x `S.union` freeIn t
 freeIn (Pi v t s) = freeIn t `S.union` (freeIn s S.\\ S.singleton v)
 freeIn (Lam v t s) = freeIn t `S.union` (freeIn s S.\\ S.singleton v)

+ 1 - 1
src/Types/Context.hs

@@ -17,7 +17,7 @@ import Control.Monad.Freer.Reader
 import Control.Monad.Freer
 
 newtype Context
-  = Context { getContext :: Map.Map Var (These Type Term) }
+  = Context (Map.Map Var (These Type Term))
   deriving Show
 
 insertType :: (Var, Type) -> Context -> Context

+ 0 - 1
src/Types/Equality.hs

@@ -4,7 +4,6 @@ module Types.Equality where
 import qualified Types.Normalise as N
 import Types.Context
 
-import Syntax.Refresh
 import Syntax.Subst
 import Syntax
 

+ 10 - 9
src/Types/Infer.hs

@@ -6,7 +6,6 @@ import Types.Equality
 import Types.Context
 import Types.Unify
 
-import Syntax.Refresh
 import Syntax.Subst
 import Syntax
 
@@ -15,7 +14,6 @@ import Control.Monad.Freer.Reader
 import Control.Monad.Freer.Fresh
 import Control.Monad.Freer
 
-import Debug.Trace
 import Data.These
 
 import Control.Monad
@@ -44,10 +42,10 @@ infer = \case
       inferSet ty
     pure $ Set (k1 `max` k2)
   Lam x t b -> do
-    inferSet t
+    _ <- inferSet t
     Pi x t <$> local (insertType (x, t)) (infer b)
   Let x t b -> do
-    inferSet t
+    _ <- inferSet t
     local (insertType (x, t)) $ infer b
   App e1 e2 -> do
     t1 <- infer e1
@@ -58,6 +56,10 @@ infer = \case
         N.normalise =<< subst [(vr, e2)] o
       e -> throwError (ExpectedPi e)
 
+assertEquality :: ( Member Fresh r
+                  , Member (Exc TypeError) r
+                  , Member (Reader Context) r )
+               => Type -> Type -> Eff r ()
 assertEquality t1 t2 = do
   x <- equal t1 t2
   if x then pure () else do
@@ -71,7 +73,7 @@ inferSet :: ( Member (Exc TypeError) r
 inferSet t = do
   x <- infer t
   x' <- N.normalise x
-  case x of
+  case x' of
     Set k -> pure k
     x -> throwError (ExpectedType x)
 
@@ -91,10 +93,9 @@ checkProgram (Define v vl:xs) = do
       local (insertBoth (v, t, vl)) $ checkProgram xs
     Nothing -> local (insertBoth (v, ty, vl)) $ checkProgram xs
 
-
 checkProgram [Eval t] = do
   ctx <- ask
-  forM_ (toList ctx) $ \(n, vl) ->
+  forM_ (toList ctx) $ \(_, vl) ->
     case vl of
       These t v -> do
         t' <- infer v
@@ -103,12 +104,12 @@ checkProgram [Eval t] = do
   (ctx,) . Just <$> infer t
 
 checkProgram (Eval t:xs) = do
-  infer t
+  _ <- infer t
   checkProgram xs
 
 checkProgram [] = do
   ctx <- ask
-  forM_ (toList ctx) $ \(n, vl) ->
+  forM_ (toList ctx) $ \(_, vl) ->
     case vl of
       These t v -> do
         t' <- infer v

+ 5 - 0
src/Types/Normalise.hs

@@ -22,6 +22,7 @@ normalise = \case
     case val of
       Just t -> pure t
       Nothing -> pure (Variable x)
+  TypeHint vl t -> TypeHint <$> normalise vl <*> normalise t
   App x y -> do
     y' <- normalise y
     x' <- normalise x
@@ -39,3 +40,7 @@ normalise = \case
     t' <- normalise t
     local (insertType (v, t')) $
       Pi v t' <$> normalise s
+  Let n v b -> do
+    v' <- normalise v
+    local (insertValue (n, v')) $
+      normalise b

+ 9 - 14
src/Types/Unify.hs

@@ -16,13 +16,10 @@ import Control.Monad.Freer
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
 
-import Control.Monad
-import Debug.Trace
-
 type Subst = [(Var, Term)]
 
+singleton :: Var -> Term -> Subst
 singleton a b = [(a, b)]
-alpha = [1..] >>= flip replicateM ['a'..'z']
 
 unify :: ( Member (Exc TypeError) r
          , Member (Reader Context) r
@@ -48,15 +45,13 @@ unify t1 t2 = do
     (Let v1 t1 b1, Let v2 t2 b2) -> do
       (y, z) <- (,) <$> unify t1 t2 <*> unify b1 b2
       pure $ singleton v2 (Variable v1) ++ y ++ z
-    (a, Pi v1 t1 b1) -> do
-      id <- fresh
-      let x = Refresh (alpha !! id) id
-      pi' <- subst [(v1, Variable x)] b1
+    (a, Pi v1 _ b1) -> do
+      id <- refresh Irrelevant
+      pi' <- subst [(v1, Variable id)] b1
       unify a pi'
-    (Pi v1 t1 b1, a) -> do
-      id <- fresh
-      let x = Refresh (alpha !! id) id
-      pi' <- subst [(v1, Variable x)] b1
+    (Pi v1 _ b1, a) -> do
+      id <- refresh Irrelevant
+      pi' <- subst [(v1, Variable id)] b1
       unify pi' a
     (Set k, Set n) | k == n -> pure []
     (_, _) -> throwError (NotEqual t1' t2')
@@ -81,7 +76,7 @@ checkConsistent = checkConsistent' Map.empty where
                          then map
                          else Map.insert a b map
             in checkConsistent' map' xs
-  checkConsistent' map [] = pure ()
+  checkConsistent' _ [] = pure ()
   -- A type is said to be concrete if we already know either its
   -- type or its value.
   concrete v = do
@@ -92,5 +87,5 @@ checkConsistent = checkConsistent' Map.empty where
       _ -> False
 
 occurs :: Var -> Term -> Bool
-occurs v (Variable k) = False
+occurs _ (Variable _) = False
 occurs v x = v `Set.member` freeIn x