Revert "Merge branch 'typechecking' into codegen-martin-3"

This reverts commit e000e5159f, reversing
changes made to 3ac8377fa0.

Grammar.cf

@@ -1,7 +1,4 @@
-Program. Program ::= [Def] ;
 
-DExp.  Def ::= Ident ":" Type
-               Ident [Ident] "=" Exp ;
 
 Program. Program ::= [Bind];
 

Makefile

@@ -1,7 +1,7 @@
 .PHONY : sdist clean
 
 language : src/Grammar/Test
-	cabal install --installdir=. --overwrite-policy=always
+	cabal install --installdir=.
 
 src/Grammar/Test.hs src/Grammar/Lex.x src/Grammar/Par.y : Grammar.cf
 	bnfc -o src -d $<

language

@@ -1 +0,0 @@
-/home/sebastian/.cabal/store/ghc-9.4.4/language-0.1.0.0-e-language-b98a5580bec9e5cee0ea5d675b3788bf6eec0b9eb955374c9ba250c1d3b935fc/bin/language

language.cabal

@@ -17,7 +17,7 @@ extra-source-files:
 
 
 common warnings
-    ghc-options: -W
+    ghc-options: -Wall
 
 executable language
     import:           warnings

src/Abs.hs

@@ -1,20 +0,0 @@
-{-# LANGUAGE TypeFamilies, StandaloneDeriving #-}
-
-module Abs where
-
-data Exp eps
-    = EInt (XInt eps) Integer
-    | EId (XId eps) String
-    | EAdd (XAdd eps) (Exp eps) (Exp eps)
-    | EApp (XApp eps) (Exp eps) (Exp eps)
-    | EAbs (XAbs eps) String (Exp eps)
-    | EExp (XExp eps)
-
-newtype Ident = Ident String
-
-type family XInt eps
-type family XId  eps
-type family XAdd eps
-type family XApp eps
-type family XAbs eps
-type family XExp eps

src/Interpreter.hs

@@ -1,10 +1,14 @@
 {-# LANGUAGE LambdaCase #-}
-
 module Interpreter where
 
-import           Control.Monad.Except    (Except, MonadError (throwError))
+import           Control.Applicative     (Applicative)
-
+import           Control.Monad.Except    (Except, MonadError (throwError),
+                                          liftEither)
+import           Data.Either.Combinators (maybeToRight)
+import           Data.Map                (Map)
+import qualified Data.Map                as Map
 import           Grammar.Abs
+import           Grammar.Print           (printTree)
 
 interpret :: Program -> Except String Integer
 interpret (Program e) =

src/NewAbs.hs

@@ -1,29 +0,0 @@
-{-# LANGUAGE GADTs, LambdaCase #-}
-
-module NewAbs where
-
-import Grammar.Abs ( Ident(..), Type )
-
-data CExp where
-    CId  :: Type -> Ident -> CExp
-    CInt :: Type -> Int -> CExp
-    CAdd :: Type -> CExp -> CExp -> CExp
-    CAbs :: Type -> Ident -> Type -> CExp -> CExp
-    CApp :: Type -> CExp -> CExp -> CExp 
-
-instance Show CExp where
-    show :: CExp -> String
-    show = \case
-        CId _ (Ident a) -> show a
-        CInt _ i -> show i
-        CAdd _ e1 e2 -> show e1 <> " + " <> show e2
-        CAbs t1 i t2 e -> appendType t1 $ show "\\" <> show i <> " : " <> show t2 <> ". " <> show e
-        CApp _ e1 e2 -> show e1 <> " " <> show e2
-
-appendType :: Type -> String -> String
-appendType t s = s <> " : " <> show t
-
-data CDef = CDef Ident Type Ident [Ident] CExp
-    deriving Show
-
-newtype CProgram = CProgram [CDef]

src/Rename/Renamer.hs

@@ -1,96 +0,0 @@
-{-# LANGUAGE OverloadedRecordDot, LambdaCase, TypeFamilies, PatternSynonyms #-}
-
-module Rename.Renamer where
-
-import Abs
-
-import qualified Grammar.Abs as A
-import           Grammar.ErrM         (Err)
-import           Control.Monad.Except (throwError)
-import           Grammar.Print        (printTree)
-import           Control.Monad.State
-import qualified Data.Map as M
-import           Data.Map (Map)
-import qualified Data.Set as S
-import           Data.Set (Set)
-
------------------- DATA TYPES ------------------
-
-type Rn a = StateT Env Err a
-
-data Env = Env { uniques :: Map String Unique
-               , nextUnique :: Unique
-               , sig :: Set String
-               }
-
-newtype Unique = Unique Int
-    deriving Enum
-
-data Name = Nu Unique | Ni String
-
-initEnv :: Env
-initEnv = Env
-        { uniques    = mempty
-        , nextUnique = Unique 0
-        , sig        = mempty
-        }
-
-findBind :: String -> Rn Name
-findBind x = lookupUnique x >>= \case
-    Just u  -> pure $ Nu u
-    Nothing -> gets (S.member x . sig) >>= \case
-      False -> throwError ("Unbound variable " ++ printTree x)
-      True  -> pure $ Ni x
-
-newUnique :: String -> Rn Unique
-newUnique x = do
-  u <- gets nextUnique
-  modify $ \env -> env { nextUnique = succ u
-                       , uniques = M.insert x u env.uniques }
-  return u
-
-lookupUnique :: String -> Rn (Maybe Unique)
-lookupUnique x = gets (M.lookup x . uniques)
-
-renameDef :: Def -> Rn Def
-renameDef = \case
-  DExp x t _ xs e -> do
-    newSig x
-    xs' <- mapM newUnique xs
-    e'  <- renameExp e
-    let e'' = foldr ($) e' . zipWith R.EAbs xs' $ fromTree t
-    pure . R.DBind $ R.Bind x t e''
-
-renameExp :: A.Exp -> Rn ExpRE
-renameExp e =
-    case e of
-   A.EInt i -> pure (EIntR i)
-   A.EId (A.Ident str) -> flip EIdR str <$> findBind str
-   A.EAdd e1 e2 -> EAppR <$> renameExp e1 <*> renameExp e2
-   A.EApp e1 e2 -> EAppR <$> renameExp e1 <*> renameExp e2
-   A.EAbs (A.Ident x) e -> do
-       x' <- newUnique x
-       e' <- renameExp e
-       pure $ EAbsR x' x e'
-
-data R
-type ExpRE = Exp R
-
-type instance XInt R = ()
-type instance XId  R = Name
-type instance XAdd R = ()
-type instance XApp R = ()
-type instance XAbs R = Unique
-type instance XExp R = ()
-
-pattern EIntR :: Integer -> ExpRE
-pattern EIntR i = EInt () i
-
-pattern EIdR :: Name -> String -> ExpRE
-pattern EIdR n s = EId n s
-
-pattern EAppR :: ExpRE -> ExpRE -> ExpRE
-pattern EAppR e1 e2 = EApp () e1 e2
-
-pattern EAbsR :: Unique -> String -> ExpRE -> ExpRE
-pattern EAbsR u n e = EAbs u n e

src/TypeChecker.hs

@@ -1,129 +0,0 @@
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE OverloadedRecordDot #-}
-
-module TypeChecker (typecheck) where
-
-import Grammar.Abs
-import Grammar.ErrM ( Err )
-import NewAbs
-import Data.Map (Map)
-import Data.Map qualified as Map
-import Control.Monad.Reader
-import Control.Monad.Except
-import Data.List (isPrefixOf)
-import Control.Applicative ((<|>))
-
-type Check a = ReaderT Context Err a
-
-data Context = Ctx { sig :: Map Ident Type
-                   , env :: [Map Ident Type]
-                   }
-
-initEnv :: Context
-initEnv = Ctx { sig = mempty
-              , env = mempty
-              }
-
-run :: Check a -> Either String a
-run = flip runReaderT initEnv
-
-typecheck :: Program -> Err Program
-typecheck prg = case run $ checkProg prg of
-                  Left err -> fail err
-                  Right _ -> pure prg
-
-
-checkProg :: Program -> Check CProgram
-checkProg (Program ds) = undefined
-    
-checkDef :: Def -> Check CDef
-checkDef (DExp i1 TInt i2 args e) = undefined
-checkDef (DExp i1 (TPol i) i2 args e) = undefined
-checkDef (DExp i1 (TFun xs) i2 args e) = do
-        when (i1 /= i2) (fail $ "Mismatched names: " <> show i1 <> " != " <> show i2)
-        case compare (length xs - 1) (length args) of
-          LT -> fail $ "Too many arguments, got " <> show (length args) <> " expected " <> show (length xs)
-          _ -> do
-              let vars = Map.fromList $ zip args xs
-              e' <- local (\r -> r { env =  [vars] }) (checkExp e)
-              return $ CDef i1 (TFun xs) i2 args e'
-
-checkExp :: Exp -> Check CExp
-checkExp = \case
-
-    EInt i -> pure $ CInt TInt (fromIntegral i)
-
-    EAdd e1 e2 -> do
-        e1' <- checkExp e1
-        e2' <- checkExp e2
-        let t1 = getType e1'
-        let t2 = getType e2'
-        when (t1 /= t2) (fail $ "Different types occured, got " <> show t1 <> " and " <> show t2)
-        return $ CAdd t1 e1' e2'
-
-    EId i -> do
-        asks (lookupEnv i) >>= \case
-            Right t -> return $ CId t i
-            Left _ -> asks (lookupSig i) >>= \case
-                Right t -> return $ CId t i
-                Left x -> fail x
-
-    EAbs i t e -> do
-        e' <- local (\r -> r { env = Map.singleton i t : r.env }) (checkExp e)
-        return $ CAbs (TFun [t, getType e']) i t e'
-
-    EApp e1 e2 -> do
-        e1' <- checkExp e1
-        e2' <- checkExp e2
-        let retT = applyType (getType e1') (getType e2')
-        case retT of
-          Left x -> fail x
-          Right t -> return $ CApp t e1' e2'
-
-lookupSig :: Ident -> Context -> Err Type
-lookupSig i (Ctx s _) = case Map.lookup i s of
-                  Nothing -> throwError $ "Undefined function: " <> show i
-                  Just x -> pure x
-
-lookupEnv :: Ident -> Context -> Err Type
-lookupEnv i (Ctx _ []) = throwError $ "Unbound variable: " <> show i
-lookupEnv i (Ctx s (e:es)) = case Map.lookup i e of
-                  Nothing -> lookupEnv i (Ctx s es)
-                  Just x -> pure x
-
-
-applyType :: Type -> Type -> Err Type
-applyType (TFun (x:xs)) t = case t of
-    (TFun ys) -> if ys `isPrefixOf` (x:xs)
-                         then return . TFun $ drop (length ys) (x:xs)
-                         else fail $ "Mismatched types, expected " <> show x <> " got " <> show TInt
-applyType t1 t2 = fail $ "Can not apply " <> show t1 <> " to " <> show t2
-
-class ExtractType a where
-    getType :: a -> Type
-
-instance ExtractType CExp where
-    getType = \case
-        CId t _ -> t
-        CInt t _ -> t
-        CAdd t _ _ -> t
-        CAbs t _ _ _ -> t
-        CApp t _ _ -> t
-
--- | λx : Int. x + 3 + 5
-customLambda1 :: Exp
-customLambda1 = EAbs (Ident "x") TInt (EAdd (EId (Ident "x")) (EAdd (EInt 3) (EInt 5)))
-
-customLambda2 :: Exp
-customLambda2 = EAbs (Ident "x") (TFun [TInt, TInt]) (EId (Ident "f"))
-
--- | main : Int 
---   main = λx : Int. x + 3 + 5
-customPrg1 :: Program
-customPrg1 = Program [DExp (Ident "main") TInt (Ident "main") [] customLambda1]
-
--- | main : Int -> Int
---   main = λx : Int. x + 3 + 5
-customPrg2 :: Program
-customPrg2 = Program [DExp (Ident "main") (TFun [TInt, TInt]) (Ident "main") [] customLambda2]

test_program

@@ -1,2 +0,0 @@
-main : Int
-main = (\x : Int. x + x + 3) ((\x : Int. x) 2)