tcenv' <- extendM tcenv (c,k)
return (tcenv',tsenv)
where k = foldr Karrow Klifted (map snd tbs)
- ch (Newtype (m,c) tbs rhs) =
+ -- TODO
+ ch (Newtype (m,c) tbs axiom rhs) =
do mn <- getMname
requireModulesEq m mn "newtype declaration" tdef False
tcenv' <- extendM tcenv (c,k)
(foldr tArrow
(foldl Tapp (Tcon (Just mn,c))
(map (Tvar . fst) utbs)) ts) tbs
- ch (tdef@(Newtype c tbs (Just t))) =
+ -- TODO
+ ch (tdef@(Newtype c tbs axiom (Just t))) =
do tvenv <- foldM extendM eempty tbs
k <- checkTy (tcenv,tvenv) t
- require (k==Klifted) ("bad kind:\n" ++ show tdef)
+ require (k `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
return cenv
- ch (tdef@(Newtype c tbs Nothing)) =
+ ch (tdef@(Newtype c tbs axiom Nothing)) =
{- should only occur for recursive Newtypes -}
return cenv
do mn <- getMname
requireModulesEq m mn "value definition" vdef True
k <- checkTy (tcenv,tvenv) t
- require (k==Klifted) ("unlifted kind in:\n" ++ show vdef)
+ require (k `eqKind` Klifted) ("unlifted kind in:\n" ++ show vdef)
t' <- checkExp env' e
requireM (equalTy tsenv t t')
("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++
do mn <- getMname
requireModulesEq m mn "value definition" vdef True
k <- checkTy (tcenv,tvenv) t
- require (k /= Kopen) ("open kind in:\n" ++ show vdef)
- require ((not top_level) || (k /= Kunlifted)) ("top-level unlifted kind in:\n" ++ show vdef)
+ require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
+ require ((not top_level) || (not (k `eqKind` Kunlifted))) ("top-level unlifted kind in:\n" ++ show vdef)
t' <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) e
requireM (equalTy tsenv t t')
("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++
k' <- checkTy (tcenv,tvenv) t
case t' of
Tforall (tv,k) t0 ->
- do require (k' <= k)
+ do require (k' `subKindOf` k)
("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++
"operator kind: " ++ show k ++ "\n" ++
"operand kind: " ++ show k')
{- check existentials -}
let (etvs,eks) = unzip etbs
let (etvs',eks') = unzip etbs'
- require (eks == eks')
+ require (all (uncurry eqKind)
+ (zip eks eks'))
("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
"kinds declared in data constructor: " ++ show eks ++
"kinds declared in case alternative: " ++ show eks')
k2 <- ch t2
case k1 of
Karrow k11 k12 ->
- do require (k2 <= k11)
+ do require (k2 `subKindOf` k11)
("kinds don't match in type application: " ++ show t ++ "\n" ++
"operator kind: " ++ show k11 ++ "\n" ++
"operand kind: " ++ show k2)
checkLit :: Lit -> CheckResult Ty
-checkLit lit =
+checkLit (Literal lit t) =
case lit of
- Lint _ t ->
+ -- TODO: restore commented-out stuff.
+ Lint _ ->
do {- require (elem t [tIntzh, {- tInt32zh,tInt64zh, -} tWordzh, {- tWord32zh,tWord64zh, -} tAddrzh, tCharzh])
("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
return t
- Lrational _ t ->
+ Lrational _ ->
do {- require (elem t [tFloatzh,tDoublezh])
("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
return t
- Lchar _ t ->
+ Lchar _ ->
do {- require (t == tCharzh)
("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
return t
- Lstring _ t ->
+ Lstring _ ->
do {- require (t == tAddrzh)
("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
return t
data Tdef
= Data (Qual Tcon) [Tbind] [Cdef]
- | Newtype (Qual Tcon) [Tbind] (Maybe Ty)
+ | Newtype (Qual Tcon) [Tbind] Axiom (Maybe Ty)
data Cdef
= Constr (Qual Dcon) [Tbind] [Ty]
+-- Newtype coercion
+type Axiom = (Qual Tcon, Kind)
+
data Vdefg
= Rec [Vdef]
| Nonrec Vdef
= Var (Qual Var)
| Dcon (Qual Dcon)
| Lit Lit
--- Why were type apps and value apps distinguished,
--- but not type lambdas and value lambdas?
| App Exp Exp
| Appt Exp Ty
| Lam Bind Exp
| Let Vdefg Exp
--- Ty is new
| Case Exp Vbind Ty [Alt] {- non-empty list -}
--- Renamed to Cast; switched order
| Cast Exp Ty
| Note String Exp
| External String Ty
| Kunlifted
| Kopen
| Karrow Kind Kind
- deriving (Eq)
-
-data Lit
- = Lint Integer Ty
- | Lrational Rational Ty
- | Lchar Char Ty
- | Lstring String Ty
- deriving (Eq) -- with nearlyEqualTy
-
--- new: Pnames
--- this requires at least one module name,
--- and possibly other hierarchical names
--- an alternative would be to flatten the
+ | Keq Ty Ty
+
+data Lit = Literal CoreLit Ty
+ deriving Eq -- with nearlyEqualTy
+
+data CoreLit = Lint Integer
+ | Lrational Rational
+ | Lchar Char
+ | Lstring String
+ deriving Eq
+
+-- Right now we represent module names as triples:
+-- (package name, hierarchical names, leaf name)
+-- An alternative to this would be to flatten the
-- module namespace, either when printing out
-- Core or (probably preferably) in a
-- preprocessor.
--- Maybe because the empty module name is a module name (represented as
--- Nothing.)
+-- The empty module name (as in an unqualified name)
+-- is represented as Nothing.
type Mname = Maybe AnMname
type AnMname = (Pname, [Id], Id)
type Id = String
+eqKind :: Kind -> Kind -> Bool
+eqKind Klifted Klifted = True
+eqKind Kunlifted Kunlifted = True
+eqKind Kopen Kopen = True
+eqKind (Karrow k1 k2) (Karrow l1 l2) = k1 `eqKind` l1
+ && k2 `eqKind` l2
+eqKind _ _ = False -- no Keq kind is ever equal to any other...
+ -- maybe ok for now?
+
--- tjc: I haven't looked at the rest of this file. ---
{- Doesn't expand out fully applied newtype synonyms
eqTy e1 e2 (Tapp t1a t1b) (Tapp t2a t2b) =
eqTy e1 e2 t1a t2a && eqTy e1 e2 t1b t2b
eqTy e1 e2 (Tforall (tv1,tk1) t1) (Tforall (tv2,tk2) t2) =
- tk1 == tk2 && eqTy (tv1:e1) (tv2:e2) t1 t2
+ tk1 `eqKind` tk2 && eqTy (tv1:e1) (tv2:e2) t1 t2
eqTy _ _ _ _ = False
instance Eq Ty where (==) = nearlyEqualTy
subKindOf :: Kind -> Kind -> Bool
_ `subKindOf` Kopen = True
-k1 `subKindOf` k2 = k1 == k2 -- doesn't worry about higher kinds
-
-instance Ord Kind where (<=) = subKindOf
+k1 `subKindOf` k2 = k1 `eqKind` k2 -- doesn't worry about higher kinds
baseKind :: Kind -> Bool
baseKind (Karrow _ _ ) = False
import Monad
import System.Environment
+import System.Cmd
+import System.Exit
import Core
import Printer
-import Parser
-import Lex
-import ParseGlue
+import ParsecParser
import Env
import Prims
import Check
import Prep
import Interp
-process (senv,modules) f =
+-- You may need to change this.
+baseDir = "../../libraries/"
+--------
+
+-- Code for checking that the external and GHC printers print the same results
+testFlag = "-t"
+
+validateResults :: FilePath -> FilePath -> IO ()
+validateResults origFile genFile = do
+ resultCode <- system $ "diff -u " ++ origFile ++ " " ++ genFile
+ putStrLn $ case resultCode of
+ ExitSuccess -> "Parse validated for " ++ origFile
+ ExitFailure 1 -> "Parse failed to validate for " ++ origFile
+ _ -> "Error diffing files: " ++ origFile ++ " " ++ genFile
+------------------------------------------------------------------------------
+
+process :: Bool -> (Check.Menv,[Module]) -> String -> IO (Check.Menv,[Module])
+process doTest (senv,modules) f =
do putStrLn ("Processing " ++ f)
- s <- readFile f
- case parse s 1 of
- OkP m -> do putStrLn "Parse succeeded"
- {- writeFile (f ++ ".parsed") (show m) -}
+ resultOrErr <- parseCore f
+ case resultOrErr of
+ Right m -> do
+ putStrLn "Parse succeeded"
+ let outF = f ++ ".parsed"
+ writeFile outF (show m)
+ when doTest $ (validateResults f outF)
case checkModule senv m of
OkC senv' ->
do putStrLn "Check succeeded"
FailC s ->
do putStrLn ("Check failed: " ++ s)
error "quit"
- FailP s -> do putStrLn ("Parse failed: " ++ s)
- error "quit"
+ Left err -> do putStrLn ("Parse failed: " ++ show err)
+ error "quit"
-main = do fname <- getSingleArg
- (_,modules) <- foldM process (initialEnv,[]) [fname] -- flist
+main = do args <- getArgs
+ let (doTest, fname) =
+ case args of
+ (f:fn:_) | f == testFlag -> (True,fn)
+ (fn:_) -> (False,fn)
+ _ -> error $
+ "usage: ./Driver [filename]"
+ mapM_ (process doTest (initialEnv,[])) (libs ++ [fname])
+ (_,modules) <- foldM (process doTest) (initialEnv,[]) (libs ++ [fname])
let result = evalProgram modules
putStrLn ("Result = " ++ show result)
putStrLn "All done"
--- TODO
--- see what breaks
- where flist = ["Main.hcr"]
- getSingleArg = getArgs >>= (\ a ->
- case a of
- (f:_) -> return f
- _ -> error $ "usage: ./Driver [filename]")
-{-
- ["PrelBase.hcr",
- "PrelMaybe.hcr",
- "PrelTup.hcr",
- "PrelList.hcr",
- "PrelShow.hcr",
- "PrelEnum.hcr",
- "PrelNum.hcr",
- "PrelST.hcr",
- "PrelArr.hcr",
- "PrelDynamic.hcr",
- "PrelReal.hcr",
- "PrelFloat.hcr",
- "PrelRead.hcr",
- "PrelIOBase.hcr",
- "PrelException.hcr",
- "PrelErr.hcr",
- "PrelConc.hcr",
- "PrelPtr.hcr",
- "PrelByteArr.hcr",
- "PrelPack.hcr",
- "PrelBits.hcr",
- "PrelWord.hcr",
- "PrelInt.hcr",
- "PrelCTypes.hcr",
- "PrelStable.hcr",
- "PrelCTypesISO.hcr",
- "Monad.hcr",
- "PrelStorable.hcr",
- "PrelMarshalAlloc.hcr",
- "PrelMarshalUtils.hcr",
- "PrelMarshalArray.hcr",
- "PrelCString.hcr",
- "PrelMarshalError.hcr",
- "PrelCError.hcr",
- "PrelPosix.hcr",
- "PrelHandle.hcr",
- "PrelIO.hcr",
- "Prelude.hcr",
- "Main.hcr" ]
-
--}
\ No newline at end of file
+ where libs = map (baseDir ++) ["./ghc-prim/GHC/Generics.hcr",
+ "./ghc-prim/GHC/PrimopWrappers.hcr",
+ "./ghc-prim/GHC/Bool.hcr",
+ "./ghc-prim/GHC/IntWord64.hcr",
+ "./base/GHC/Base.hcr",
+ "./base/GHC/List.hcr",
+ "./base/GHC/Enum.hcr",
+ "./base/GHC/Show.hcr",
+ "./base/GHC/Num.hcr",
+ "./base/GHC/ST.hcr",
+ "./base/GHC/Real.hcr",
+ "./base/GHC/STRef.hcr",
+ "./base/GHC/Arr.hcr",
+ "./base/GHC/Float.hcr",
+ "./base/GHC/Read.hcr",
+ "./base/GHC/Ptr.hcr",
+ "./base/GHC/Word.hcr",
+ "./base/GHC/Int.hcr",
+ "./base/GHC/Unicode.hcr",
+ "./base/GHC/IOBase.hcr",
+ "./base/GHC/Err.hcr",
+ "./base/GHC/Exception.hcr",
+ "./base/GHC/Stable.hcr",
+ "./base/GHC/Storable.hcr",
+ "./base/GHC/Pack.hcr",
+ "./base/GHC/Weak.hcr",
+ "./base/GHC/Handle.hcr",
+ "./base/GHC/IO.hcr",
+ "./base/GHC/Dotnet.hcr",
+ "./base/GHC/Environment.hcr",
+ "./base/GHC/Exts.hcr",
+ "./base/GHC/PArr.hcr",
+ "./base/GHC/TopHandler.hcr",
+ "./base/GHC/Desugar.hcr",
+ "./base/Data/Ord.hcr",
+ "./base/Data/Maybe.hcr",
+ "./base/Data/Bits.hcr",
+ "./base/Data/STRef/Lazy.hcr",
+ "./base/Data/Generics/Basics.hcr",
+ "./base/Data/Generics/Aliases.hcr",
+ "./base/Data/Generics/Twins.hcr",
+ "./base/Data/Generics/Instances.hcr",
+ "./base/Data/Generics/Text.hcr",
+ "./base/Data/Generics/Schemes.hcr",
+ "./base/Data/Tuple.hcr",
+ "./base/Data/String.hcr",
+ "./base/Data/Either.hcr",
+ "./base/Data/Char.hcr",
+ "./base/Data/List.hcr",
+ "./base/Data/HashTable.hcr",
+ "./base/Data/Typeable.hcr",
+ "./base/Data/Dynamic.hcr",
+ "./base/Data/Function.hcr",
+ "./base/Data/IORef.hcr",
+ "./base/Data/Fixed.hcr",
+ "./base/Data/Monoid.hcr",
+ "./base/Data/Ratio.hcr",
+ "./base/Data/STRef.hcr",
+ "./base/Data/Version.hcr",
+ "./base/Data/Complex.hcr",
+ "./base/Data/Unique.hcr",
+ "./base/Data/Foldable.hcr",
+ "./base/Data/Traversable.hcr"]
\ No newline at end of file
+{-# OPTIONS -XPatternGuards #-}
{-
Interprets the subset of well-typed Core programs for which
(a) All constructor and primop applications are saturated
evalExternal s vs = error "evalExternal undefined for now" -- etc.,etc.
evalLit :: Lit -> PrimValue
-evalLit l =
+evalLit (Literal l t) =
case l of
- Lint i (Tcon(_,"Intzh")) -> PIntzh i
- Lint i (Tcon(_,"Wordzh")) -> PWordzh i
- Lint i (Tcon(_,"Addrzh")) -> PAddrzh i
- Lint i (Tcon(_,"Charzh")) -> PCharzh i
- Lrational r (Tcon(_,"Floatzh")) -> PFloatzh r
- Lrational r (Tcon(_,"Doublezh")) -> PDoublezh r
- Lchar c (Tcon(_,"Charzh")) -> PCharzh (toEnum (ord c))
- Lstring s (Tcon(_,"Addrzh")) -> PAddrzh 0 -- should really be address of non-heap copy of C-format string s
+ Lint i | (Tcon(_,"Intzh")) <- t -> PIntzh i
+ Lint i | (Tcon(_,"Wordzh")) <- t -> PWordzh i
+ Lint i | (Tcon(_,"Addrzh")) <- t -> PAddrzh i
+ Lint i | (Tcon(_,"Charzh"))<- t -> PCharzh i
+ Lrational r | (Tcon(_,"Floatzh")) <- t -> PFloatzh r
+ Lrational r | (Tcon(_,"Doublezh")) <- t -> PDoublezh r
+ Lchar c | (Tcon(_,"Charzh")) <- t -> PCharzh (toEnum (ord c))
+ Lstring s | (Tcon(_,"Addrzh")) <- t -> PAddrzh 0 -- should really be address of non-heap copy of C-format string s
{- Utilities -}
-all: Check.hs Core.hs Driver.hs Env.hs Interp.hs Lex.hs ParseGlue.hs Parser.hs Prep.hs Prims.hs Printer.hs
+all: Check.hs Core.hs Driver.hs Env.hs Interp.hs ParsecParser.hs ParseGlue.hs Prep.hs Prims.hs Printer.hs
ghc --make -fglasgow-exts -o Driver Driver.hs
-Parser.hs: Parser.y
- happy -o Parser.hs Parser.y
\ No newline at end of file
+#Parser.hs: Parser.y
+# happy -ad -ihappy.debug -o Parser.hs Parser.y
\ No newline at end of file
-- ugh
splitModuleName mn =
let decoded = zDecodeString mn
- parts = filter (notElem '.') $ groupBy
+ -- Triple ugh.
+ -- We re-encode the individual parts so that:
+ -- main:Foo_Bar.Quux.baz
+ -- prints as:
+ -- main:FoozuBarziQuux.baz
+ -- and not:
+ -- main:Foo_BarziQuux.baz
+ parts = map zEncodeString $ filter (notElem '.') $ groupBy
(\ c1 c2 -> c1 /= '.' && c2 /= '.')
decoded in
(take (length parts - 1) parts, last parts)
--- /dev/null
+module ParsecParser where
+
+import Core
+import ParseGlue
+
+import Text.ParserCombinators.Parsec
+import Text.ParserCombinators.Parsec.Expr
+import qualified Text.ParserCombinators.Parsec.Token as P
+import Text.ParserCombinators.Parsec.Language
+import Data.Ratio
+
+parseCore :: FilePath -> IO (Either ParseError Module)
+parseCore = parseFromFile coreModule
+
+coreModule :: Parser Module
+coreModule = do
+ whiteSpace
+ reserved "module"
+ mName <- coreModuleName
+ whiteSpace
+ tdefs <- option [] coreTdefs
+ vdefGroups <- coreVdefGroups
+ eof
+ return $ Module mName tdefs vdefGroups
+
+coreModuleName :: Parser AnMname
+coreModuleName = do
+ pkgName <- corePackageName
+ char ':'
+ (modHierarchy,baseName) <- coreHierModuleNames
+ return (pkgName, modHierarchy, baseName)
+
+corePackageName :: Parser Pname
+corePackageName = identifier
+
+coreHierModuleNames :: Parser ([Id], Id)
+coreHierModuleNames = do
+ parentName <- upperName
+ return $ splitModuleName parentName
+
+upperName :: Parser Id
+upperName = do
+ firstChar <- upper
+ rest <- many (identLetter extCoreDef)
+ return $ firstChar:rest
+
+coreTdefs :: Parser [Tdef]
+coreTdefs = many coreTdef
+
+coreTdef :: Parser Tdef
+coreTdef = withSemi (try (try coreDataDecl <|> try coreNewtypeDecl))
+
+
+withSemi p = try p `withTerminator` ";"
+
+withTerminator p term = do
+ x <- try p
+ try $ symbol term
+ return x
+
+coreDataDecl :: Parser Tdef
+coreDataDecl = do
+ reserved "data"
+ tyCon <- coreQualifiedCon
+ whiteSpace -- important
+ tBinds <- coreTbinds
+ whiteSpace
+ symbol "="
+ whiteSpace
+ cDefs <- braces coreCdefs
+ return $ Data tyCon tBinds cDefs
+
+coreNewtypeDecl :: Parser Tdef
+coreNewtypeDecl = do
+ reserved "newtype"
+ tyCon <- coreQualifiedCon
+ whiteSpace
+ tBinds <- coreTbinds
+ symbol "^"
+ axiom <- coreAxiom
+ tyRep <- try coreTRep
+ return $ Newtype tyCon tBinds axiom tyRep
+
+coreQualifiedCon :: Parser (Mname, Id)
+coreQualifiedCon = coreQualifiedGen upperName
+
+coreQualifiedName = coreQualifiedGen identifier
+
+coreQualifiedGen p = do
+ maybeMname <- coreMaybeMname
+ theId <- p
+ return (maybeMname, theId)
+
+coreMaybeMname = optionMaybe coreMname
+
+coreRequiredQualifiedName = do
+ mname <- coreMname
+ theId <- identifier
+ return (Just mname, theId)
+
+coreMname = do
+-- Notice the '^' goes here:
+-- it's part of a variable *occurrence*, not a module name.
+ char '^'
+ nm <- try coreModuleName
+ symbol "."
+ return nm
+
+coreAxiom :: Parser Axiom
+coreAxiom = parens (do
+ coercionName <- coreQualifiedCon
+ whiteSpace
+ symbol "::"
+ whiteSpace
+ coercionKind <- coreKind
+ return (coercionName, coercionKind))
+
+coreTbinds :: Parser [Tbind]
+coreTbinds = many coreTbind
+
+coreTbindsGen :: CharParser () String -> Parser [Tbind]
+-- The "try" here is important. Otherwise, when parsing:
+-- "Node (^base:DataziTuple.Z3T)" (a cdef), we commit to
+-- parsing (^base...) as a tbind rather than a type.
+coreTbindsGen separator = many (try $ coreTbindGen separator)
+
+coreTbind :: Parser Tbind
+coreTbind = coreTbindGen whiteSpace
+
+coreTbindGen :: CharParser () a -> Parser Tbind
+coreTbindGen sep = (parens (do
+ sep
+ tyVar <- identifier
+ kind <- symbol "::" >> coreKind
+ return (tyVar, kind))) <|>
+ (sep >> identifier >>= (return . (\ tv -> (tv,Klifted))))
+
+coreCdefs :: Parser [Cdef]
+coreCdefs = sepBy1 coreCdef (symbol ";")
+
+coreCdef :: Parser Cdef
+coreCdef = do
+ dataConName <- coreQualifiedCon
+ whiteSpace -- important!
+ tBinds <- try $ coreTbindsGen (symbol "@")
+ -- This should be equivalent to (many coreAty)
+ -- But it isn't. WHY??
+ tys <- sepBy coreAty whiteSpace
+ return $ Constr dataConName tBinds tys
+
+coreTRep :: Parser (Maybe Ty)
+-- note that the "=" is inside here since if there's
+-- no rhs for the newtype, there's no "="
+coreTRep = optionMaybe (do
+ symbol "="
+ try coreType)
+
+coreType :: Parser Ty
+coreType = coreForallTy <|> (do
+ hd <- coreBty
+ -- whiteSpace is important!
+ whiteSpace
+ -- This says: If there is at least one ("-> ty"..) thing,
+ -- use it. If not, don't consume any input.
+ maybeRest <- option [] (many1 (symbol "->" >> coreType))
+ return $ case maybeRest of
+ [] -> hd
+ stuff -> foldl Tapp (Tcon tcArrow) (hd:stuff))
+
+coreBty :: Parser Ty
+coreBty = arrowThing coreAty coreAty whiteSpace Tapp
+
+arrowThing :: Parser a -> Parser a -> Parser b -> (a -> a -> a) -> Parser a
+arrowThing hdThing restThing sep op = do
+ hd <- hdThing
+ -- The "try" is necessary:
+ -- otherwise, parsing "T " fails rather
+ -- than returning "T".
+ maybeRest <- option [] (many1 (try (sep >> restThing)))
+ return $ case maybeRest of
+ [] -> hd
+ stuff -> foldl op hd maybeRest
+
+coreAppTy :: Parser Ty
+coreAppTy = do
+ bTy <- try coreBty
+ whiteSpace
+ aTy <- try coreAty
+ return $ Tapp bTy aTy
+
+coreAty = try coreTcon <|> try coreTvar <|> parens coreType
+
+coreTvar :: Parser Ty
+coreTvar = try identifier >>= (return . Tvar)
+
+coreTcon :: Parser Ty
+-- TODO: Change the grammar
+-- A Tcon can be an uppercase type constructor
+-- or a lowercase (always qualified) coercion variable
+coreTcon = (try coreQualifiedCon <|> coreRequiredQualifiedName)
+ >>= (return . Tcon)
+
+coreTyApp :: Parser Ty
+coreTyApp = do
+ operTy <- coreType
+ randTy <- coreType
+ return $ Tapp operTy randTy
+
+coreFunTy :: Parser Ty
+coreFunTy = do
+ argTy <- coreBty
+ whiteSpace
+ symbol "->"
+ whiteSpace
+ resTy <- coreType
+ return $ tArrow argTy resTy
+
+coreForallTy :: Parser Ty
+coreForallTy = do
+ reserved "forall"
+ tBinds <- many1 coreTbind
+ symbol "."
+ bodyTy <- coreType
+ return $ foldr Tforall bodyTy tBinds
+
+-- TODO: similar to coreType. should refactor
+coreKind :: Parser Kind
+coreKind = do
+ hd <- coreAtomicKind
+ maybeRest <- option [] (many1 (symbol "->" >> coreKind))
+ return $ case maybeRest of
+ [] -> hd
+ stuff -> foldl Karrow hd maybeRest
+
+coreAtomicKind = try liftedKind <|> try unliftedKind
+ <|> try openKind <|> try (parens equalityKind)
+ <|> try (parens coreKind)
+
+liftedKind = do
+ symbol "*"
+ return Klifted
+
+unliftedKind = do
+ symbol "#"
+ return Kunlifted
+
+openKind = do
+ symbol "?"
+ return Kopen
+
+equalityKind = do
+ ty1 <- coreBty
+ symbol ":=:"
+ ty2 <- coreBty
+ return $ Keq ty1 ty2
+coreVdefGroups :: Parser [Vdefg]
+coreVdefGroups = option [] (do
+ theFirstVdef <- coreVdefg
+ symbol ";"
+ others <- coreVdefGroups
+ return $ theFirstVdef:others)
+
+coreVdefg :: Parser Vdefg
+coreVdefg = coreRecVdef <|> coreNonrecVdef
+
+coreRecVdef = do
+ reserved "rec"
+ braces (sepBy1 coreVdef (symbol ";")) >>= (return . Rec)
+
+coreNonrecVdef = coreVdef >>= (return . Nonrec)
+
+coreVdef = do
+ (vdefLhs, vdefTy) <- topVbind
+ whiteSpace
+ symbol "="
+ whiteSpace
+ vdefRhs <- coreFullExp
+ return $ Vdef (vdefLhs, vdefTy, vdefRhs)
+
+coreAtomicExp :: Parser Exp
+coreAtomicExp = do
+-- For stupid reasons, the whiteSpace is necessary.
+-- Without it, (pt coreAppExp "w ^a:B.C ") doesn't work.
+ whiteSpace
+ res <- choice [ try coreVar,
+ coreDcon,
+ try coreLit,
+ parens coreFullExp ]
+ whiteSpace
+ return res
+
+coreFullExp = (choice [coreLam, coreLet,
+ coreCase, coreCast, coreNote, coreExternal]) <|> (try coreAppExp)
+-- The "try" is necessary so that we backtrack
+-- when we see a var (that is not an app)
+ <|> coreAtomicExp
+
+coreAppExp = do
+-- notes:
+-- it's important to have a separate coreAtomicExp (that any app exp
+-- begins with) and to define the args in terms of many1.
+-- previously, coreAppExp could parse either an atomic exp (an app with
+-- 0 arguments) or an app with >= 1 arguments, but that led to ambiguity.
+ oper <- try coreAtomicExp
+ whiteSpace
+ args <- many1 (whiteSpace >> ((coreAtomicExp >>= (return . Left)) <|>
+ -- note this MUST be coreAty, not coreType, because otherwise:
+ -- "A @ B c" gets parsed as "A @ (B c)"
+ ((symbol "@" >> coreAty) >>= (return . Right))))
+ return $ foldl (\ op ->
+ either (App op) (Appt op)) oper args
+
+coreVar = ((try coreQualifiedName) <|> (identifier >>= (return . unqual)))
+ >>= (return . Var)
+coreDcon = coreQualifiedCon >>= (return . Dcon)
+
+coreLit :: Parser Exp
+coreLit = parens (coreLiteral >>= (return . Lit))
+
+coreLiteral :: Parser Lit
+coreLiteral = do
+ l <- try aLit
+ symbol "::"
+ t <- coreType
+ return $ Literal l t
+
+coreLam = do
+ symbol "\\"
+ binds <- coreLambdaBinds
+ symbol "->"
+ body <- coreFullExp
+ return $ foldr Lam body binds
+coreLet = do
+ reserved "let"
+ vdefg <- coreVdefg
+ whiteSpace
+ reserved "in"
+ body <- coreFullExp
+ return $ Let vdefg body
+coreCase = do
+ reserved "case"
+ ty <- coreAty
+ scrut <- coreAtomicExp
+ reserved "of"
+ vBind <- parens lambdaBind
+ alts <- coreAlts
+ return $ Case scrut vBind ty alts
+coreCast = do
+ reserved "cast"
+ whiteSpace
+-- The parens are CRUCIAL, o/w it's ambiguous
+ body <- try (parens coreFullExp)
+ whiteSpace
+ ty <- try coreAty
+ return $ Cast body ty
+coreNote = do
+ reserved "note"
+ s <- stringLiteral
+ e <- coreFullExp
+ return $ Note s e
+coreExternal = do
+ reserved "external"
+ -- TODO: This isn't in the grammar, but GHC
+ -- always prints "external ccall". investigate...
+ symbol "ccall"
+ s <- stringLiteral
+ t <- coreAty
+ return $ External s t
+
+coreLambdaBinds = many1 coreBind
+
+coreBind = coreTbinding <|> coreVbind
+
+coreTbinding = try coreAtTbind >>= (return . Tb)
+coreVbind = parens (lambdaBind >>= (return . Vb))
+
+coreAtTbind = (symbol "@") >> coreTbind
+
+topVbind = aCoreVbind coreQualifiedName
+lambdaBind = aCoreVbind identifier
+
+aCoreVbind idP = do
+ nm <- idP
+ symbol "::"
+ t <- coreType
+ return (nm, t)
+
+
+aLit :: Parser CoreLit
+aLit = intOrRatLit <|> charLit <|> stringLit
+
+intOrRatLit :: Parser CoreLit
+intOrRatLit = do
+ -- Int and lit combined into one to avoid ambiguity.
+ -- Argh....
+ lhs <- anIntLit
+ maybeRhs <- optionMaybe (symbol "%" >> anIntLit)
+ case maybeRhs of
+ Nothing -> return $ Lint lhs
+ Just rhs -> return $ Lrational (lhs % rhs)
+
+anIntLit :: Parser Integer
+anIntLit = do
+ sign <- option 1 (symbol "-" >> return (-1))
+ n <- natural
+ return (sign * n)
+
+charLit :: Parser CoreLit
+charLit = charLiteral >>= (return . Lchar)
+ -- make sure this is right
+
+stringLit :: Parser CoreLit
+stringLit = stringLiteral >>= (return . Lstring)
+ -- make sure this is right
+
+coreAlts :: Parser [Alt]
+coreAlts = braces $ sepBy1 coreAlt (symbol ";")
+
+coreAlt :: Parser Alt
+coreAlt = conAlt <|> litAlt <|> defaultAlt
+
+conAlt :: Parser Alt
+conAlt = do
+ conName <- coreQualifiedCon
+ tBinds <- many (parens coreAtTbind)
+ whiteSpace -- necessary b/c otherwise we parse the next list as empty
+ vBinds <- many (parens lambdaBind)
+ whiteSpace
+ try (symbol "->")
+ rhs <- try coreFullExp
+ return $ Acon conName tBinds vBinds rhs
+
+litAlt :: Parser Alt
+litAlt = do
+ l <- parens coreLiteral
+ symbol "->"
+ rhs <- coreFullExp
+ return $ Alit l rhs
+
+defaultAlt :: Parser Alt
+defaultAlt = do
+ reserved "_"
+ symbol "->"
+ rhs <- coreFullExp
+ return $ Adefault rhs
+----------------
+extCore = P.makeTokenParser extCoreDef
+
+parens = P.parens extCore
+braces = P.braces extCore
+semiSep1 = P.semiSep1 extCore
+-- newlines are allowed anywhere
+whiteSpace = P.whiteSpace extCore <|> (newline >> return ())
+symbol = P.symbol extCore
+identifier = P.identifier extCore
+-- Keywords all begin with '%'
+reserved s = P.reserved extCore ('%':s)
+natural = P.natural extCore
+charLiteral = P.charLiteral extCore
+stringLiteral = P.stringLiteral extCore
+
+-- dodgy since Core doesn't really allow comments,
+-- but we'll pretend...
+extCoreDef = LanguageDef {
+ commentStart = "{-"
+ , commentEnd = "-}"
+ , commentLine = "--"
+ , nestedComments = True
+ , identStart = lower
+ , identLetter = lower <|> upper <|> digit <|> (char '\'')
+ , opStart = opLetter extCoreDef
+ , opLetter = oneOf ";=@:\\%_.*#?%"
+ , reservedNames = map ('%' :)
+ ["module", "data", "newtype", "rec",
+ "let", "in", "case", "of", "cast",
+ "note", "external", "forall"]
+ , reservedOpNames = [";", "=", "@", "::", "\\", "%_",
+ ".", "*", "#", "?"]
+ , caseSensitive = True
+ }
+
+-- Stuff to help with testing in ghci.
+pTest (Left a) = error (show a)
+pTest (Right t) = print t
+
+pTest1 :: Show a => CharParser () a -> String -> IO ()
+pTest1 pr s = do
+ let res = parse pr "" s
+ pTest res
+
+pt :: Show a => CharParser () a -> String -> IO ()
+pt pr s = do
+ x <- parseTest pr s
+ print x
+
+try_ = try
+many_ = many
+option_ = option
+many1_ = many1
+il = identLetter
+
+andThenSym a b = do
+ p <- a
+ symbol b
+ return p
{ Let $2 $4 }
| '%case' '(' ty ')' aexp '%of' vbind '{' alts1 '}'
{ Case $5 $7 $3 $9 }
- | '%cast' exp aty
+-- Note: ty, not aty! You can cast something to a forall type
+-- Though now we have shift/reduce conflicts like woah
+ | '%cast' exp ty
{ Cast $2 $3 }
| '%note' STRING exp
{ Note $2 $3 }
-- it sucks to have to repeat the Maybe-checking twice,
-- but otherwise we get reduce/reduce conflicts
+-- TODO: this is the ambiguity here. mname '.' name --
+-- but by maximal-munch, in GHC.Base.Bool the entire
+-- thing gets counted as the module name. What to do,
+-- besides z-encoding the dots in the hierarchy again?
+-- (Or using syntax other than a dot to separate the
+-- module name from the variable name...)
qname :: { (Mname,Id) }
: name { (Nothing, $1) }
| mname '.' name
prepExp (venv,tvenv) (Lam (Vb vb) e) = Lam (Vb vb) (prepExp (eextend venv vb,tvenv) e)
prepExp (venv,tvenv) (Lam (Tb tb) e) = Lam (Tb tb) (prepExp (venv,eextend tvenv tb) e)
prepExp env@(venv,tvenv) (Let (Nonrec(Vdef((Nothing,x),t,b))) e)
- | kindof tvenv t == Kunlifted && suspends b =
+ | kindof tvenv t `eqKind` Kunlifted && suspends b =
-- There are two places where we call the typechecker, one of them
-- here.
-- We need to know the type of the let body in order to construct
where g e (v,t) = Lam (Vb(v,t)) (App e (Var (unqual v)))
rewindApp env e [] = e
- rewindApp env@(venv,tvenv) e1 (Left e2:as) | kindof tvenv t == Kunlifted && suspends e2 =
+ rewindApp env@(venv,tvenv) e1 (Left e2:as) | kindof tvenv t `eqKind` Kunlifted && suspends e2 =
-- This is the other place where we call the typechecker.
Case (prepExp env' e2) (v,t) (typeOfExp env rhs) [Adefault rhs]
where rhs = (rewindApp env' (App e1 (Var (unqual v))) as)
instance Show Lit where
showsPrec d l = shows (plit l)
+instance Show CoreLit where
+ showsPrec d l = shows (pclit l)
indent = nest 2
(text "%module" <+> panmname mname)
$$ indent ((vcat (map ((<> char ';') . ptdef) tdefs))
$$ (vcat (map ((<> char ';') . pvdefg) vdefgs)))
+ <> (if ((not.null) tdefs) || ((not.null) vdefgs) then char '\n' else empty)
+ -- add final newline; sigh.
ptdef (Data qtcon tbinds cdefs) =
(text "%data" <+> pqname qtcon <+> (hsep (map ptbind tbinds)) <+> char '=')
$$ indent (braces ((vcat (punctuate (char ';') (map pcdef cdefs)))))
-ptdef (Newtype qtcon tbinds tyopt ) =
- text "%newtype" <+> pqname qtcon <+> (hsep (map ptbind tbinds)) <+>
- (case tyopt of
- Just ty -> char '=' <+> pty ty
- Nothing -> empty)
+ptdef (Newtype qtcon tbinds (coercion,k) tyopt) =
+ text "%newtype" <+> pqname qtcon <+> (hsep (map ptbind tbinds))
+ $$ indent (axiomclause $$ repclause)
+ where axiomclause = char '^' <+> parens (pqname coercion <+> text "::"
+ <+> pkind k)
+ repclause = case tyopt of
+ Just ty -> char '=' <+> pty ty
+ Nothing -> empty
pcdef (Constr qdcon tbinds tys) =
(pqname qdcon) <+> (sep [hsep (map pattbind tbinds),sep (map paty tys)])
-- be sure to print the '.' here so we don't print out
-- ".foo" for unqualified foo...
pmname Nothing = empty
-pmname (Just m) = panmname m <> char '.'
+-- Notice that we print the "^" here; this is so that
+-- "%module foo" doesn't get printed as "%module ^foo"
+pmname (Just m) = char '^' <> panmname m <> char '.'
panmname p@(pkgName, parents, name) =
let parentStrs = map pname parents in
pakind k = parens (pkind k)
pkind (Karrow k1 k2) = parens (pakind k1 <> text "->" <> pkind k2)
+pkind (Keq t1 t2) = parens (parens (pty t1) <+> text ":=:" <+> parens (pty t2))
pkind k = pakind k
paty (Tvar n) = pname n
pexp (Lam b e) = char '\\' <+> plamexp [b] e
pexp (Let vd e) = (text "%let" <+> pvdefg vd) $$ (text "%in" <+> pexp e)
-pexp (Case e vb t alts) = sep [text "%case" <+> pty t <+> paexp e,
+pexp (Case e vb t alts) = sep [text "%case" <+> paty t <+> paexp e,
text "%of" <+> pvbind vb]
$$ (indent (braces (vcat (punctuate (char ';') (map palt alts)))))
-pexp (Cast e t) = (text "%cast" <+> paty t) $$ pexp e
+pexp (Cast e t) = (text "%cast" <+> parens (pexp e)) $$ paty t
pexp (Note s e) = (text "%note" <+> pstring s) $$ pexp e
-pexp (External n t) = (text "%extcall" <+> pstring n) $$ paty t
+-- TODO: ccall shouldn't really be there
+pexp (External n t) = (text "%external ccall" <+> pstring n) $$ paty t
pexp e = pfexp e
(text "%_ ->")
$$ indent (pexp e)
-plit (Lint i t) = parens (integer i <> text "::" <> pty t)
-plit (Lrational r t) = parens (text (show (fromRat r)) <> text "::" <> pty t)
-plit (Lchar c t) = parens (text ("\'" ++ escape [c] ++ "\'") <> text "::" <> pty t)
-plit (Lstring s t) = parens (pstring s <> text "::" <> pty t)
+plit (Literal cl t) = parens (pclit cl <> text "::" <> pty t)
+
+pclit (Lint i) = integer i
+-- makes sure to print it out as n % d
+pclit (Lrational r) = text (show r)
+pclit (Lchar c) = text ("\'" ++ escape [c] ++ "\'")
+pclit (Lstring s) = pstring s
pstring s = doubleQuotes(text (escape s))
+escape :: String -> String
escape s = foldr f [] (map ord s)
where
- f cv rest | (cv < 0x20 || cv > 0x7e || cv == 0x22 || cv == 0x27 || cv == 0x5c) =
+ f cv rest
+ | cv > 0xFF = '\\':'x':hs ++ rest
+ | (cv < 0x20 || cv > 0x7e || cv == 0x22 || cv == 0x27 || cv == 0x5c) =
'\\':'x':h1:h0:rest
where (q1,r1) = quotRem cv 16
h1 = intToDigit q1
h0 = intToDigit r1
+ hs = dropWhile (=='0') $ reverse $ mkHex cv
+ mkHex 0 = ""
+ mkHex cv = intToDigit r : mkHex q
+ where (q,r) = quotRem cv 16
f cv rest = (chr cv):rest
-
In particular, typechecker and interpreter give a precise semantics.
-All can be built using, e.g.,
+To build, run "make".
-happy -o Parser.hs Parser.y
-ghc --make -package text -fglasgow-exts -o Driver Driver.hs
+To run the checker and interpreter (which currently aren't working anyway),
+you need to generate External Core for all the base, integer and ghc-prim
+libraries. This can be done by adding "-fext-core" to the GhcLibHcOpts in
+your build.mk file, then running "make" under libraries/.
+Then you need to edit Driver.hs and change "baseDir" to point to your GHC
+libraries directory.
-Most recently tested with GHC 6.8.1. I make no claims of portability. --tjc
+Most recently tested with GHC 6.8.2. I make no claims of portability. --tjc
projects / ghc-hetmet.git / commitdiff