diff --git a/language.cabal b/language.cabal index a290bc3..6ae9e12 100644 --- a/language.cabal +++ b/language.cabal @@ -36,6 +36,7 @@ executable language Renamer.Renamer TypeChecker.TypeChecker AnnForall + OrderDefs TypeChecker.TypeCheckerHm TypeChecker.TypeCheckerBidir TypeChecker.TypeCheckerIr @@ -90,6 +91,7 @@ Test-suite language-testsuite Grammar.Skel Grammar.ErrM Grammar.Layout + OrderDefs Auxiliary Monomorphizer.Monomorphizer Monomorphizer.MonomorphizerIr diff --git a/src/Main.hs b/src/Main.hs index c870d8b..9e4e677 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -2,46 +2,38 @@ module Main where -import AnnForall (annotateForall) -import Codegen.Codegen (generateCode) -import Compiler (compile) -import Control.Monad (when, (<=<)) -import Data.List.Extra (isSuffixOf) -import Data.Maybe (fromJust, isNothing) -import Desugar.Desugar (desugar) -import GHC.IO.Handle.Text (hPutStrLn) -import Grammar.ErrM (Err) -import Grammar.Layout (resolveLayout) -import Grammar.Par (myLexer, pProgram) -import Grammar.Print (Print, printTree) -import LambdaLifter (lambdaLift) -import Monomorphizer.Monomorphizer (monomorphize) -import Renamer.Renamer (rename) -import ReportForall (reportForall) -import System.Console.GetOpt ( - ArgDescr (NoArg, ReqArg), - ArgOrder (RequireOrder), - OptDescr (Option), - getOpt, - usageInfo, - ) -import System.Directory ( - createDirectory, - doesPathExist, - getDirectoryContents, - removeDirectoryRecursive, - setCurrentDirectory, - ) -import System.Environment (getArgs) -import System.Exit ( - ExitCode (ExitFailure), - exitFailure, - exitSuccess, - exitWith, - ) -import System.IO (stderr) -import System.Process (spawnCommand, waitForProcess) -import TypeChecker.TypeChecker (TypeChecker (Bi, Hm), typecheck) +import AnnForall (annotateForall) +import Codegen.Codegen (generateCode) +import Compiler (compile) +import Control.Monad (when, (<=<)) +import Data.List.Extra (isSuffixOf) +import Data.Maybe (fromJust, isNothing) +import Desugar.Desugar (desugar) +import GHC.IO.Handle.Text (hPutStrLn) +import Grammar.ErrM (Err) +import Grammar.Layout (resolveLayout) +import Grammar.Par (myLexer, pProgram) +import Grammar.Print (Print, printTree) +import LambdaLifter (lambdaLift) +import Monomorphizer.Monomorphizer (monomorphize) +import OrderDefs (orderDefs) +import Renamer.Renamer (rename) +import ReportForall (reportForall) +import System.Console.GetOpt (ArgDescr (NoArg, ReqArg), + ArgOrder (RequireOrder), + OptDescr (Option), getOpt, + usageInfo) +import System.Directory (createDirectory, doesPathExist, + getDirectoryContents, + removeDirectoryRecursive, + setCurrentDirectory) +import System.Environment (getArgs) +import System.Exit (ExitCode (ExitFailure), + exitFailure, exitSuccess, + exitWith) +import System.IO (stderr) +import System.Process (spawnCommand, waitForProcess) +import TypeChecker.TypeChecker (TypeChecker (Bi, Hm), typecheck) main :: IO () main = getArgs >>= parseArgs >>= uncurry main' @@ -93,12 +85,12 @@ chooseTypechecker s options = options{typechecker = tc} tc = case s of "hm" -> pure Hm "bi" -> pure Bi - _ -> Nothing + _ -> Nothing data Options = Options - { help :: Bool - , debug :: Bool - , gc :: Bool + { help :: Bool + , debug :: Bool + , gc :: Bool , typechecker :: Maybe TypeChecker } @@ -112,7 +104,7 @@ main' opts s = file <- readFile s printToErr "-- Parse Tree -- " - parsed <- fromErr . pProgram . resolveLayout True $ myLexer (file ++ prelude) + parsed <- fromErr . pProgram . resolveLayout True $ myLexer file -- (file ++ prelude) log parsed printToErr "-- Desugar --" @@ -125,7 +117,7 @@ main' opts s = log renamed printToErr "\n-- TypeChecker --" - typechecked <- fromErr $ typecheck (fromJust opts.typechecker) renamed + typechecked <- fromErr $ typecheck (fromJust opts.typechecker) (orderDefs renamed) log typechecked printToErr "\n-- Lambda Lifter --" diff --git a/src/OrderDefs.hs b/src/OrderDefs.hs new file mode 100644 index 0000000..079512b --- /dev/null +++ b/src/OrderDefs.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE LambdaCase #-} + +module OrderDefs where + +import Control.Monad.State (State, execState, get, modify, when) +import Data.Function (on) +import Data.List (partition, sortBy) +import Data.Set (Set) +import qualified Data.Set as Set +import Grammar.Abs + +orderDefs :: Program -> Program +orderDefs (Program defs) = + Program $ not_binds ++ map DBind (has_sig ++ orderBinds no_sig) + + where + (has_sig, no_sig) = partition (\(Bind n _ _) -> elem n sig_names) + [ b | DBind b <- defs] + sig_names = [ n | DSig (Sig n _) <- defs ] + not_binds = flip filter defs $ \case DBind _ -> False + _ -> True + +orderBinds :: [Bind] -> [Bind] +orderBinds binds = sortBy (on compare countUniqueCalls) binds + where + bind_names = [ n | Bind n _ _ <- binds] + + countUniqueCalls :: Bind -> Int + countUniqueCalls (Bind n _ e) = + Set.size $ execState (go e) (Set.singleton n) + where + go :: Exp -> State (Set LIdent) () + go exp = get >>= \called -> case exp of + EVar x -> when (Set.notMember x called && elem x bind_names) $ + modify (Set.insert x) + EApp e1 e2 -> on (>>) go e1 e2 + EAdd e1 e2 -> on (>>) go e1 e2 + ELet (Bind _ _ e) e' -> on (>>) go e e' + EAbs _ e -> go e + ECase e bs -> go e >> mapM_ (\(Branch _ e) -> go e) bs + EAnn e _ -> go e + EInj _ -> pure () + ELit _ -> pure () diff --git a/src/TypeChecker/TypeCheckerBidir.hs b/src/TypeChecker/TypeCheckerBidir.hs index cb35bac..fcef885 100644 --- a/src/TypeChecker/TypeCheckerBidir.hs +++ b/src/TypeChecker/TypeCheckerBidir.hs @@ -11,7 +11,7 @@ import Control.Applicative (Applicative (liftA2), (<|>)) import Control.Monad.Except (ExceptT, MonadError (throwError), forM, runExceptT, unless, zipWithM, zipWithM_) -import Control.Monad.Extra (fromMaybeM) +import Control.Monad.Extra (fromMaybeM, ifM) import Control.Monad.State (MonadState, State, evalState, gets, modify) import Data.Coerce (coerce) @@ -52,11 +52,12 @@ type Env = Seq EnvElem -- | Ordered context -- Γ ::= ・| Γ, α | Γ, ά | Γ, ▶ ά | Γ, x:A data Cxt = Cxt - { env :: Env -- ^ Local scope context Γ - , sig :: Map LIdent Type -- ^ Top-level signatures x : A - , binds :: Map LIdent Exp -- ^ Top-level binds x : e - , next_tevar :: Int -- ^ Counter to distinguish ά - , data_injs :: Map UIdent Type -- ^ Data injections (constructors) K/inj : A + { env :: Env -- ^ Local scope context Γ + , sig :: Map LIdent Type -- ^ Top-level signatures x : A + , binds :: Map LIdent Exp -- ^ Top-level binds x : e + , next_tevar :: Int -- ^ Counter to distinguish ά + , data_injs :: Map UIdent Type -- ^ Data injections (constructors) K/inj : A + , currentBind :: LIdent -- ^ Used for recursive functions } deriving (Show, Eq) newtype Tc a = Tc { runTc :: ExceptT String (State Cxt) a } @@ -77,6 +78,7 @@ initCxt defs = Cxt | DData (Data _ injs) <- defs , Inj name t <- injs ] + , currentBind = "" } where unboundedTVars = uncurry (Set.\\) . go (mempty, mempty) @@ -102,6 +104,7 @@ typecheckBinds cxt = flip evalState cxt typecheckBind :: Bind -> Tc (T.Bind' Type) typecheckBind (Bind name vars rhs) = do + modify $ \cxt -> cxt { currentBind = name } bind'@(T.Bind (name, typ) _ _) <- lookupSig name >>= \case Just t -> do (rhs', _) <- check (foldr EAbs rhs vars) t @@ -297,14 +300,16 @@ checkPattern patt t_patt = case patt of infer :: Exp -> Tc (T.ExpT' Type) infer (ELit lit) = apply (T.ELit lit, litType lit) --- Γ ∋ (x : A) Γ ∌ (x : A) --- ------------- Var --------------------- Var' +-- Γ ∋ (x : A) Γ ⊢ rec(x) +-- ------------- Var --------------------- VarRec -- Γ ⊢ x ↓ A ⊣ Γ Γ ⊢ x ↓ ά ⊣ Γ,(x : ά) infer (EVar x) = do - a <- fromMaybeM extend $ liftA2 (<|>) (lookupEnv x) (lookupSig x) + a <- ifM (gets $ (x==) . currentBind) varRec var apply (T.EVar (coerce x), a) where - extend = do + var = maybeToRightM "Can't infer" =<< + liftA2 (<|>) (lookupEnv x) (lookupSig x) + varRec = do alpha <- TEVar <$> fresh insertEnv (EnvVar x alpha) pure alpha