hermit-1.0.0.0: Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone
LanguageHaskell2010

HERMIT.ParserCore

Synopsis

Documentation

parseCore :: ReadBindings c => CoreString -> c -> HermitM CoreExpr Source

parseCoreExprT :: (ReadBindings c, HasHermitMEnv m, HasLemmas m, LiftCoreM m) => CoreString -> Transform c m a CoreExpr Source

Parse a CoreString to a CoreExpr, using the current context.

parse2BeforeT :: (ReadBindings c, HasHermitMEnv m, HasLemmas m, LiftCoreM m) => (CoreExpr -> CoreExpr -> Translate c m a b) -> CoreString -> CoreString -> Translate c m a b Source

parse3BeforeT :: (ReadBindings c, HasHermitMEnv m, HasLemmas m, LiftCoreM m) => (CoreExpr -> CoreExpr -> CoreExpr -> Translate c m a b) -> CoreString -> CoreString -> CoreString -> Translate c m a b Source

parse2beforeBiR :: (CoreExpr -> CoreExpr -> BiRewriteH a) -> CoreString -> CoreString -> BiRewriteH a Source

parse3beforeBiR :: (CoreExpr -> CoreExpr -> CoreExpr -> BiRewriteH a) -> CoreString -> CoreString -> CoreString -> BiRewriteH a Source

parse4beforeBiR :: (CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr -> BiRewriteH a) -> CoreString -> CoreString -> CoreString -> CoreString -> BiRewriteH a Source

parse5beforeBiR :: (CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr -> BiRewriteH a) -> CoreString -> CoreString -> CoreString -> CoreString -> CoreString -> BiRewriteH a Source

data Token Source

Constructors

Tforall 
Trec 
Tlet 
Tin 
Tcase 
Tof 
Tcast 
Tnote 
Texternal 
Tlocal 
Twild 
Toparen 
Tcparen 
Tobrace 
Tcbrace 
Thash 
Teq 
Tcolon 
Tcoloncolon 
Tcoloneqcolon 
Tstar 
Tarrow 
Tdoublearrow 
Tlambda 
Tat 
Tdot 
Tquestion 
Tsemicolon 
Tname String 
Tcname String 
Tinteger Integer 
Trational Float 
Tstring String 
Tchar Char 

Instances

parseError :: Monad m => [Token] -> m a Source

lexer :: String -> Either String [Token] Source