Safe Haskell	Safe
Language	Haskell2010

Embedder.Atmo.ToIsabelle

Synopsis

rewireUserMods :: [Text]
embedModule :: MonadError AstError m => FilePath -> Module -> m (Maybe Theory)
embedFreeProgram :: MonadError AstError m => FilePath -> FreeProgram -> m Theory
tFreeProgram :: MonadError AstError m => FreeProgram -> m ([Decl], Graph, [Tree Vertex])
tModule :: MonadError AstError m => Module -> m ([Decl], Graph, [Tree Vertex])
tDeclaration :: MonadError AstError m => Declaration -> m Decl
tTypeSynonym :: Monad m => TypeSynonym -> m Decl
tDefn :: MonadError AstError m => Defn -> m Decl
tFunBinding :: MonadError AstError m => FunBinding -> m ([Pttrn], Term)
tFun :: MonadError AstError m => Defn -> m (Text, TypSig, [([Pttrn], Term)])
tRDefns :: MonadError AstError m => [Defn] -> m Decl
tDataDefn :: Monad m => DataDefn -> m Decl
tRecDefn :: Monad m => RecDefn -> m Decl
tDataCon :: Monad m => DataCon -> m DatatypeConstructor
tType :: Ty -> Typ
tTypeSig :: Ty -> TypSig
tPoly :: Monad m => Poly -> m ([TName], Typ)
tPolySig :: Monad m => Poly -> m ([TName], TypSig)
flattenTyTuple :: Ty -> Ty
flattenTy :: Ty -> (Ty, [Ty])
tExp :: Monad m => Exp -> m Term
tPat :: Pat -> Pttrn
tPatBind :: Monad m => PatBind -> m (Pttrn, Term)
flattenCase :: Exp -> (Exp, [(Pat, Exp)])
tCase :: Monad m => (Pat, Exp) -> m (Pttrn, Term)
tGlobal :: Text -> Text
tLocal :: Text -> Text
getBaseName :: Text -> Text
filterName :: Text -> Text
isReWire :: Show a => a -> Bool

Documentation

rewireUserMods :: [Text] Source #

The rewire-user library modules, by theory name. Their Isabelle semantics is the hand-written session (targets/isabelle/thys, imported as ReWire.Atmo), so embedding them would emit theories nothing imports. Matched against the theory name rather than the output path, which -o overrides.

embedModule :: MonadError AstError m => FilePath -> Module -> m (Maybe Theory) Source #

embedFreeProgram :: MonadError AstError m => FilePath -> FreeProgram -> m Theory Source #

tFreeProgram :: MonadError AstError m => FreeProgram -> m ([Decl], Graph, [Tree Vertex]) Source #

tModule :: MonadError AstError m => Module -> m ([Decl], Graph, [Tree Vertex]) Source #

tDeclaration :: MonadError AstError m => Declaration -> m Decl Source #

tTypeSynonym :: Monad m => TypeSynonym -> m Decl Source #

tDefn :: MonadError AstError m => Defn -> m Decl Source #

tFunBinding :: MonadError AstError m => FunBinding -> m ([Pttrn], Term) Source #

tFun :: MonadError AstError m => Defn -> m (Text, TypSig, [([Pttrn], Term)]) Source #

tRDefns :: MonadError AstError m => [Defn] -> m Decl Source #

tDataDefn :: Monad m => DataDefn -> m Decl Source #

tRecDefn :: Monad m => RecDefn -> m Decl Source #