mirror of
https://github.com/anoma/juvix.git
synced 2025-01-04 13:42:04 +03:00
Add C code generation backend (#68)
* [cbackend] Adds an AST for C This should cover enough C to implement the microjuvix backend. * [cbackend] Add C serializer using language-c library We may decide to write our own serializer for the C AST but this demonstrates that the C AST is sufficient at least. * [cbackend] Declarations will always be typed * [cbackend] Add CPP support to AST * [cbackend] Rename some names for clarity * [cbackend] Add translation of InductiveDef to C * [cbackend] Add CLI for C backend * [cbackend] Add stdbool.h to file header * [cbackend] Allow Cpp and Verbatim code inline * [cbackend] Add a newline after printing C * [cbackend] Support foreign blocks * [cbackend] Add support for axioms * [cbackend] Remove code examples * [cbackend] wip FunctionDef including Expressions * [parser] Support esacping '}' inside a foreign block * [cbackend] Add support for patterns in functions * [cbackend] Add foreign C support to HelloWorld.mjuvix * hlint fixes * More hlint fixes not picked up by pre-commit * [cbackend] Remove CompileStatement from MonoJuvix * [cbackend] Add support for compile blocks * [cbackend] Move compileInfo extraction to MonoJuvixResult * [minihaskell] Fix compile block support * [chore] Remove ununsed isBackendSupported function * [chore] Remove unused imports * [cbackend] Use a Reader for pattern bindings * [cbackend] Fix compiler warnings * [cbackend] Add support for nested patterns * [cbackend] Use functions to instantiate argument names * [cbackend] Add non-exhaustive pattern error message * [cbackend] Adds test for c to WASM compile and execution * [cbackend] Add links to test dependencies in quickstart * [cbackend] Add test with inductive types and patterns * [cbackend] Fix indentation * [cbackend] Remove ExpressionTyped case https://github.com/heliaxdev/minijuvix/issues/79 * [lexer] Fix lexing of \ inside a foreign block * [cbackend] PR review fixes * [chore] Remove unused import * [cbackend] Rename CJuvix to MiniC * [cbackend] Rename MonoJuvixToC to MonoJuvixToMiniC * [cbackend] Add test for polymorphic function * [cbackend] Add module for string literals
This commit is contained in:
Paul Cadman
GitHub
parent
077e53cfb1
commit
60236e7b58
4
.github/workflows/ci.yml
vendored
4
.github/workflows/ci.yml
vendored
@ -103,6 +103,10 @@ jobs:
|
||||
uses: actions/checkout@v2
|
||||
with:
|
||||
path: main
|
||||
- name: Setup Emscripten
|
||||
uses: mymindstorm/setup-emsdk@v11
|
||||
- name: Setup Wasmer
|
||||
uses: wasmerio/setup-wasmer@v1
|
||||
- name: Test suite
|
||||
id: test
|
||||
run: |
|
||||
|
||||
4
Makefile
4
Makefile
@ -62,6 +62,10 @@ clean-full:
|
||||
test:
|
||||
stack test --fast --jobs $(THREADS)
|
||||
|
||||
.PHONY : test-skip-slow
|
||||
test-skip-slow:
|
||||
stack test --fast --jobs $(THREADS) --ta '-p "! /slow tests/"'
|
||||
|
||||
.PHONY : test-watch
|
||||
test-watch:
|
||||
stack test --fast --jobs $(THREADS) --file-watch
|
||||
|
||||
@ -53,7 +53,7 @@ If the installation succeeds, you must be able to run the =minijuvix=
|
||||
command from any location. To get the complete list of commands, please
|
||||
run =minijuvix --help=.
|
||||
|
||||
- To test everything works correctly, you can run the following command:
|
||||
- To test everything works correctly, you can run the following command. You will need to have [[https://emscripten.org][emscripten]] and [[https://wasmer.io][wasmer]] installed.
|
||||
|
||||
#+begin_src shell
|
||||
$ stack test
|
||||
|
||||
16
app/Commands/MiniC.hs
Normal file
16
app/Commands/MiniC.hs
Normal file
@ -0,0 +1,16 @@
|
||||
{-# LANGUAGE ApplicativeDo #-}
|
||||
|
||||
module Commands.MiniC where
|
||||
|
||||
import Commands.Extra
|
||||
import MiniJuvix.Prelude hiding (Doc)
|
||||
import Options.Applicative
|
||||
|
||||
newtype MiniCOptions = MiniCOptions
|
||||
{ _miniCInputFile :: FilePath
|
||||
}
|
||||
|
||||
parseMiniC :: Parser MiniCOptions
|
||||
parseMiniC = do
|
||||
_miniCInputFile <- parseInputFile
|
||||
pure MiniCOptions {..}
|
||||
20
app/Main.hs
20
app/Main.hs
@ -4,6 +4,7 @@ module Main (main) where
|
||||
|
||||
import Commands.Extra
|
||||
import Commands.MicroJuvix
|
||||
import Commands.MiniC
|
||||
import Commands.MiniHaskell
|
||||
import Commands.MonoJuvix
|
||||
import Commands.Termination as Termination
|
||||
@ -29,9 +30,9 @@ import MiniJuvix.Syntax.MicroJuvix.TypeChecker qualified as MicroTyped
|
||||
import MiniJuvix.Syntax.MiniHaskell.Pretty qualified as MiniHaskell
|
||||
import MiniJuvix.Syntax.MonoJuvix.Pretty qualified as Mono
|
||||
import MiniJuvix.Termination qualified as Termination
|
||||
import MiniJuvix.Termination.CallGraph qualified as Termination
|
||||
import MiniJuvix.Translation.AbstractToMicroJuvix qualified as Micro
|
||||
import MiniJuvix.Translation.MicroJuvixToMonoJuvix qualified as Mono
|
||||
import MiniJuvix.Translation.MonoJuvixToMiniC qualified as MiniC
|
||||
import MiniJuvix.Translation.MonoJuvixToMiniHaskell qualified as MiniHaskell
|
||||
import MiniJuvix.Translation.ScopedToAbstract qualified as Abstract
|
||||
import MiniJuvix.Utils.Version (runDisplayVersion)
|
||||
@ -52,6 +53,7 @@ data Command
|
||||
| Html HtmlOptions
|
||||
| Termination TerminationCommand
|
||||
| MiniHaskell MiniHaskellOptions
|
||||
| MiniC MiniCOptions
|
||||
| MicroJuvix MicroJuvixCommand
|
||||
| MonoJuvix MonoJuvixOptions
|
||||
| DisplayVersion
|
||||
@ -209,6 +211,7 @@ parseCommand =
|
||||
commandMonoJuvix,
|
||||
commandMicroJuvix,
|
||||
commandMiniHaskell,
|
||||
commandMiniC,
|
||||
commandHighlight
|
||||
]
|
||||
)
|
||||
@ -240,6 +243,15 @@ parseCommand =
|
||||
(MiniHaskell <$> parseMiniHaskell)
|
||||
(progDesc "Translate a MiniJuvix file to MiniHaskell")
|
||||
|
||||
commandMiniC :: Mod CommandFields Command
|
||||
commandMiniC = command "minic" minfo
|
||||
where
|
||||
minfo :: ParserInfo Command
|
||||
minfo =
|
||||
info
|
||||
(MiniC <$> parseMiniC)
|
||||
(progDesc "Translate a MiniJuvix file to MiniC")
|
||||
|
||||
commandHighlight :: Mod CommandFields Command
|
||||
commandHighlight = command "highlight" minfo
|
||||
where
|
||||
@ -349,6 +361,9 @@ instance HasEntryPoint MonoJuvixOptions where
|
||||
instance HasEntryPoint MiniHaskellOptions where
|
||||
getEntryPoint root = EntryPoint root . pure . _mhaskellInputFile
|
||||
|
||||
instance HasEntryPoint MiniCOptions where
|
||||
getEntryPoint root = EntryPoint root . pure . _miniCInputFile
|
||||
|
||||
instance HasEntryPoint CallsOptions where
|
||||
getEntryPoint root = EntryPoint root . pure . _callsInputFile
|
||||
|
||||
@ -433,6 +448,9 @@ runCLI cli = do
|
||||
MiniHaskell o -> do
|
||||
minihaskell <- head . (^. MiniHaskell.resultModules) <$> runIO (upToMiniHaskell (getEntryPoint root o))
|
||||
renderStdOutMini (MiniHaskell.ppOutDefault minihaskell)
|
||||
MiniC o -> do
|
||||
miniC <- (^. MiniC.resultCCode) <$> runIO (upToMiniC (getEntryPoint root o))
|
||||
putStrLn miniC
|
||||
Termination (Calls opts@CallsOptions {..}) -> do
|
||||
results <- runIO (upToAbstract (getEntryPoint root opts))
|
||||
let topModule = head (results ^. Abstract.resultModules)
|
||||
|
||||
@ -31,6 +31,7 @@ dependencies:
|
||||
- filepath == 1.4.*
|
||||
- gitrev == 1.3.*
|
||||
- hashable == 1.4.*
|
||||
- language-c == 0.9.*
|
||||
- megaparsec == 9.2.*
|
||||
- microlens-platform == 0.4.*
|
||||
- parser-combinators == 1.3.*
|
||||
@ -38,6 +39,7 @@ dependencies:
|
||||
- polysemy-plugin == 0.4.*
|
||||
- prettyprinter == 1.7.*
|
||||
- prettyprinter-ansi-terminal == 1.1.*
|
||||
- pretty == 1.1.*
|
||||
- process == 1.6.*
|
||||
- safe == 0.3.*
|
||||
- semirings == 0.6.*
|
||||
|
||||
@ -158,6 +158,9 @@ ghc = "ghc"
|
||||
agda :: IsString s => s
|
||||
agda = "agda"
|
||||
|
||||
cBackend :: IsString s => s
|
||||
cBackend = "c"
|
||||
|
||||
terminating :: IsString s => s
|
||||
terminating = "terminating"
|
||||
|
||||
|
||||
@ -18,6 +18,7 @@ import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as MicroJuvix
|
||||
import MiniJuvix.Syntax.MicroJuvix.TypeChecker qualified as MicroJuvix
|
||||
import MiniJuvix.Translation.AbstractToMicroJuvix qualified as MicroJuvix
|
||||
import MiniJuvix.Translation.MicroJuvixToMonoJuvix qualified as MonoJuvix
|
||||
import MiniJuvix.Translation.MonoJuvixToMiniC qualified as MiniC
|
||||
import MiniJuvix.Translation.MonoJuvixToMiniHaskell qualified as MiniHaskell
|
||||
import MiniJuvix.Translation.ScopedToAbstract qualified as Abstract
|
||||
|
||||
@ -75,6 +76,10 @@ upToMiniHaskell ::
|
||||
Members '[Files, NameIdGen, Error AJuvixError] r => EntryPoint -> Sem r MiniHaskell.MiniHaskellResult
|
||||
upToMiniHaskell = upToMonoJuvix >=> pipelineMiniHaskell
|
||||
|
||||
upToMiniC ::
|
||||
Members '[Files, NameIdGen, Error AJuvixError] r => EntryPoint -> Sem r MiniC.MiniCResult
|
||||
upToMiniC = upToMonoJuvix >=> pipelineMiniC
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
pipelineParser :: Members '[Files, Error AJuvixError] r => EntryPoint -> Sem r Parser.ParserResult
|
||||
@ -112,3 +117,9 @@ pipelineMiniHaskell ::
|
||||
MonoJuvix.MonoJuvixResult ->
|
||||
Sem r MiniHaskell.MiniHaskellResult
|
||||
pipelineMiniHaskell = mapError (toAJuvixError @Text) . MiniHaskell.entryMiniHaskell
|
||||
|
||||
pipelineMiniC ::
|
||||
Members '[Files, Error AJuvixError] r =>
|
||||
MonoJuvix.MonoJuvixResult ->
|
||||
Sem r MiniC.MiniCResult
|
||||
pipelineMiniC = mapError (toAJuvixError @Text) . MiniC.entryMiniC
|
||||
|
||||
@ -2,7 +2,7 @@ module MiniJuvix.Syntax.Backends where
|
||||
|
||||
import MiniJuvix.Prelude
|
||||
|
||||
data Backend = BackendGhc | BackendAgda
|
||||
data Backend = BackendGhc | BackendAgda | BackendC
|
||||
deriving stock (Show, Eq, Ord, Generic)
|
||||
|
||||
instance Hashable Backend
|
||||
@ -16,7 +16,3 @@ data BackendItem = BackendItem
|
||||
instance Hashable BackendItem
|
||||
|
||||
makeLenses ''BackendItem
|
||||
|
||||
isBackendSupported :: Backend -> Bool
|
||||
isBackendSupported BackendGhc = True
|
||||
isBackendSupported BackendAgda = False
|
||||
|
||||
@ -46,10 +46,9 @@ integer = do
|
||||
Nothing -> return nat
|
||||
_ -> return (-nat)
|
||||
|
||||
-- | TODO allow escaping { inside the string using \{
|
||||
bracedString :: MonadParsec e Text m => m Text
|
||||
bracedString :: forall e m. MonadParsec e Text m => m Text
|
||||
bracedString =
|
||||
Text.strip . unIndent . pack <$> (char '{' >> manyTill anySingle (char '}'))
|
||||
Text.strip . unIndent . pack <$> (char '{' >> manyTill (P.try escaped <|> anySingle) (char '}'))
|
||||
where
|
||||
unIndent :: Text -> Text
|
||||
unIndent t = Text.unlines (Text.drop (fromMaybe 0 (indentIdx t)) <$> Text.lines t)
|
||||
@ -57,6 +56,10 @@ bracedString =
|
||||
indentIdx = minimumMay . mapMaybe firstNonBlankChar . Text.lines
|
||||
firstNonBlankChar :: Text -> Maybe Int
|
||||
firstNonBlankChar = Text.findIndex (not . isSpace)
|
||||
escaped :: m Char
|
||||
escaped = do
|
||||
void (char '\\')
|
||||
char '}'
|
||||
|
||||
string :: MonadParsec e Text m => m Text
|
||||
string = pack <$> (char '"' >> manyTill L.charLiteral (char '"'))
|
||||
@ -274,3 +277,6 @@ ghc = keyword Str.ghc
|
||||
|
||||
agda :: Member InfoTableBuilder r => ParsecS r ()
|
||||
agda = keyword Str.agda
|
||||
|
||||
cBackend :: Member InfoTableBuilder r => ParsecS r ()
|
||||
cBackend = keyword Str.cBackend
|
||||
|
||||
@ -143,6 +143,7 @@ backend :: Member InfoTableBuilder r => ParsecS r Backend
|
||||
backend =
|
||||
ghc $> BackendGhc
|
||||
<|> agda $> BackendAgda
|
||||
<|> cBackend $> BackendC
|
||||
|
||||
foreignBlock :: Member InfoTableBuilder r => ParsecS r ForeignBlock
|
||||
foreignBlock = do
|
||||
|
||||
@ -6,6 +6,7 @@ module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
|
||||
where
|
||||
|
||||
import Data.List.NonEmpty.Extra qualified as NonEmpty
|
||||
import Data.Text qualified as T
|
||||
import MiniJuvix.Internal.Strings qualified as Str
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Concrete.Language
|
||||
@ -64,6 +65,9 @@ kwGhc = keyword Str.ghc
|
||||
kwAgda :: Doc Ann
|
||||
kwAgda = keyword Str.agda
|
||||
|
||||
kwC :: Doc Ann
|
||||
kwC = keyword Str.cBackend
|
||||
|
||||
kwWhere :: Doc Ann
|
||||
kwWhere = keyword Str.where_
|
||||
|
||||
@ -285,6 +289,7 @@ instance PrettyCode Backend where
|
||||
ppCode = \case
|
||||
BackendGhc -> return kwGhc
|
||||
BackendAgda -> return kwAgda
|
||||
BackendC -> return kwC
|
||||
|
||||
instance SingI s => PrettyCode (Compile s) where
|
||||
ppCode Compile {..} = do
|
||||
@ -297,9 +302,12 @@ instance PrettyCode ForeignBlock where
|
||||
_foreignBackend' <- ppCode _foreignBackend
|
||||
return $
|
||||
kwForeign <+> _foreignBackend' <+> lbrace <> line
|
||||
<> pretty _foreignCode
|
||||
<> pretty (escape _foreignCode)
|
||||
<> line
|
||||
<> rbrace
|
||||
where
|
||||
escape :: Text -> Text
|
||||
escape = T.replace "}" "\\}"
|
||||
|
||||
instance PrettyCode BackendItem where
|
||||
ppCode BackendItem {..} = do
|
||||
|
||||
@ -99,6 +99,9 @@ kwCompile = keyword Str.compile
|
||||
kwAgda :: Doc Ann
|
||||
kwAgda = keyword Str.agda
|
||||
|
||||
kwC :: Doc Ann
|
||||
kwC = keyword Str.cBackend
|
||||
|
||||
kwGhc :: Doc Ann
|
||||
kwGhc = keyword Str.ghc
|
||||
|
||||
@ -245,6 +248,7 @@ instance PrettyCode Backend where
|
||||
ppCode = \case
|
||||
BackendGhc -> return kwGhc
|
||||
BackendAgda -> return kwAgda
|
||||
BackendC -> return kwC
|
||||
|
||||
instance PrettyCode ForeignBlock where
|
||||
ppCode ForeignBlock {..} = do
|
||||
|
||||
262
src/MiniJuvix/Syntax/MiniC/Language.hs
Normal file
262
src/MiniJuvix/Syntax/MiniC/Language.hs
Normal file
@ -0,0 +1,262 @@
|
||||
module MiniJuvix.Syntax.MiniC.Language where
|
||||
|
||||
import MiniJuvix.Prelude hiding (Enum)
|
||||
|
||||
newtype CCodeUnit = CCodeUnit
|
||||
{ _ccodeCode :: [CCode]
|
||||
}
|
||||
|
||||
data CCode
|
||||
= ExternalDecl Declaration
|
||||
| ExternalFunc Function
|
||||
| ExternalMacro Cpp
|
||||
| Verbatim Text
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Prepreocessor Directives
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data Cpp
|
||||
= CppIncludeFile Text
|
||||
| CppIncludeSystem Text
|
||||
| CppDefine Define
|
||||
|
||||
data Define = Define
|
||||
{ _defineName :: Text,
|
||||
_defineBody :: Text
|
||||
}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Declaration
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data Declaration = Declaration
|
||||
{ _declType :: DeclType,
|
||||
_declIsPtr :: Bool,
|
||||
_declName :: Maybe Text,
|
||||
_declInitializer :: Maybe Initializer
|
||||
}
|
||||
|
||||
data Initializer
|
||||
= ExprInitializer Expression
|
||||
| DesignatorInitializer [DesigInit]
|
||||
|
||||
data DesigInit = DesigInit
|
||||
{ _desigDesignator :: Text,
|
||||
_desigInitializer :: Initializer
|
||||
}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Function
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data Function = Function
|
||||
{ _funcReturnType :: DeclType,
|
||||
_funcIsPtr :: Bool,
|
||||
_funcQualifier :: Qualifier,
|
||||
_funcName :: Text,
|
||||
_funcArgs :: [Declaration],
|
||||
_funcBody :: [BodyItem]
|
||||
}
|
||||
|
||||
data BodyItem
|
||||
= BodyStatement Statement
|
||||
| BodyDecl Declaration
|
||||
|
||||
data Qualifier
|
||||
= StaticInline
|
||||
| None
|
||||
deriving stock (Eq)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Types
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data DeclType
|
||||
= DeclTypeDefType Text
|
||||
| DeclStructUnion StructUnion
|
||||
| DeclTypeDef DeclType
|
||||
| DeclEnum Enum
|
||||
| BoolType
|
||||
|
||||
data StructUnion = StructUnion
|
||||
{ _structUnionTag :: StructUnionTag,
|
||||
_structUnionName :: Maybe Text,
|
||||
_structMembers :: Maybe [Declaration]
|
||||
}
|
||||
|
||||
data StructUnionTag
|
||||
= StructTag
|
||||
| UnionTag
|
||||
|
||||
data Enum = Enum
|
||||
{ _enumName :: Maybe Text,
|
||||
_enumMembers :: Maybe [Text]
|
||||
}
|
||||
|
||||
data CDeclType = CDeclType
|
||||
{ _typeDeclType :: DeclType,
|
||||
_typeIsPtr :: Bool
|
||||
}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Expressions
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data Expression
|
||||
= ExpressionAssign Assign
|
||||
| ExpressionCast Cast
|
||||
| ExpressionCall Call
|
||||
| ExpressionLiteral Literal
|
||||
| ExpressionVar Text
|
||||
| ExpressionBinary Binary
|
||||
| ExpressionUnary Unary
|
||||
| ExpressionMember MemberAccess
|
||||
|
||||
data Assign = Assign
|
||||
{ _assignLeft :: Expression,
|
||||
_assignRight :: Expression
|
||||
}
|
||||
|
||||
data Cast = Cast
|
||||
{ _castDecl :: Declaration,
|
||||
_castExpression :: Expression
|
||||
}
|
||||
|
||||
data Call = Call
|
||||
{ _callCallee :: Expression,
|
||||
_callArgs :: [Expression]
|
||||
}
|
||||
|
||||
data Literal
|
||||
= LiteralInt Integer
|
||||
| LiteralChar Char
|
||||
| LiteralString Text
|
||||
|
||||
data BinaryOp
|
||||
= Eq
|
||||
| Neq
|
||||
| And
|
||||
| Or
|
||||
|
||||
data Binary = Binary
|
||||
{ _binaryOp :: BinaryOp,
|
||||
_binaryLeft :: Expression,
|
||||
_binaryRight :: Expression
|
||||
}
|
||||
|
||||
data UnaryOp
|
||||
= Address
|
||||
| Indirection
|
||||
| Negation
|
||||
|
||||
data Unary = Unary
|
||||
{ _unaryOp :: UnaryOp,
|
||||
_unarySubject :: Expression
|
||||
}
|
||||
|
||||
data MemberAccessOp
|
||||
= Object
|
||||
| Pointer
|
||||
deriving stock (Eq)
|
||||
|
||||
data MemberAccess = MemberAccess
|
||||
{ _memberSubject :: Expression,
|
||||
_memberField :: Text,
|
||||
_memberOp :: MemberAccessOp
|
||||
}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Statements
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data Statement
|
||||
= StatementReturn (Maybe Expression)
|
||||
| StatementIf If
|
||||
| StatementExpr Expression
|
||||
| StatementCompound [Statement]
|
||||
|
||||
data If = If
|
||||
{ _ifCondition :: Expression,
|
||||
_ifThen :: Statement,
|
||||
_ifElse :: Maybe Statement
|
||||
}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Constructions
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
functionCall :: Expression -> [Expression] -> Expression
|
||||
functionCall fExpr args =
|
||||
ExpressionCall
|
||||
( Call
|
||||
{ _callCallee = fExpr,
|
||||
_callArgs = args
|
||||
}
|
||||
)
|
||||
|
||||
ptrType :: DeclType -> Text -> Declaration
|
||||
ptrType typ n =
|
||||
Declaration
|
||||
{ _declType = typ,
|
||||
_declIsPtr = True,
|
||||
_declName = Just n,
|
||||
_declInitializer = Nothing
|
||||
}
|
||||
|
||||
typeDefType :: Text -> Text -> Declaration
|
||||
typeDefType typName declName =
|
||||
Declaration
|
||||
{ _declType = DeclTypeDefType typName,
|
||||
_declIsPtr = False,
|
||||
_declName = Just declName,
|
||||
_declInitializer = Nothing
|
||||
}
|
||||
|
||||
equals :: Expression -> Expression -> Expression
|
||||
equals e1 e2 =
|
||||
ExpressionBinary
|
||||
( Binary
|
||||
{ _binaryOp = Eq,
|
||||
_binaryLeft = e1,
|
||||
_binaryRight = e2
|
||||
}
|
||||
)
|
||||
|
||||
memberAccess :: MemberAccessOp -> Expression -> Text -> Expression
|
||||
memberAccess op e fieldName =
|
||||
ExpressionMember
|
||||
( MemberAccess
|
||||
{ _memberSubject = e,
|
||||
_memberField = fieldName,
|
||||
_memberOp = op
|
||||
}
|
||||
)
|
||||
|
||||
staticInlineFunc :: DeclType -> Bool -> Text -> [Declaration] -> [BodyItem] -> Function
|
||||
staticInlineFunc t isPtr name args body =
|
||||
Function
|
||||
{ _funcReturnType = t,
|
||||
_funcIsPtr = isPtr,
|
||||
_funcQualifier = StaticInline,
|
||||
_funcName = name,
|
||||
_funcArgs = args,
|
||||
_funcBody = body
|
||||
}
|
||||
|
||||
typeDefWrap :: Text -> DeclType -> Declaration
|
||||
typeDefWrap typeDefName typ =
|
||||
Declaration
|
||||
{ _declType = DeclTypeDef typ,
|
||||
_declIsPtr = False,
|
||||
_declName = Just typeDefName,
|
||||
_declInitializer = Nothing
|
||||
}
|
||||
|
||||
returnStatement :: Expression -> BodyItem
|
||||
returnStatement e =
|
||||
BodyStatement (StatementReturn (Just e))
|
||||
|
||||
makeLenses ''CCodeUnit
|
||||
makeLenses ''Declaration
|
||||
makeLenses ''CDeclType
|
||||
153
src/MiniJuvix/Syntax/MiniC/Serialization.hs
Normal file
153
src/MiniJuvix/Syntax/MiniC/Serialization.hs
Normal file
@ -0,0 +1,153 @@
|
||||
module MiniJuvix.Syntax.MiniC.Serialization where
|
||||
|
||||
import Language.C qualified as C
|
||||
import Language.C.Data.Ident qualified as C
|
||||
import Language.C.Pretty qualified as P
|
||||
import Language.C.Syntax
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.MiniC.Language
|
||||
import Text.PrettyPrint.HughesPJ qualified as HP
|
||||
|
||||
encAngles :: HP.Doc -> HP.Doc
|
||||
encAngles p = HP.char '<' HP.<> p HP.<> HP.char '>'
|
||||
|
||||
prettyText :: Text -> HP.Doc
|
||||
prettyText = HP.text . unpack
|
||||
|
||||
prettyCpp :: Cpp -> HP.Doc
|
||||
prettyCpp = \case
|
||||
CppIncludeFile i -> "#include" HP.<+> HP.doubleQuotes (prettyText i)
|
||||
CppIncludeSystem i -> "#include" HP.<+> encAngles (prettyText i)
|
||||
CppDefine Define {..} -> "#define" HP.<+> (prettyText _defineName HP.<+> prettyText _defineBody)
|
||||
|
||||
prettyCCode :: CCode -> HP.Doc
|
||||
prettyCCode = \case
|
||||
ExternalDecl decl -> P.pretty (CDeclExt (mkCDecl decl))
|
||||
ExternalFunc fun -> P.pretty (CFDefExt (mkCFunDef fun))
|
||||
ExternalMacro m -> prettyCpp m
|
||||
Verbatim t -> prettyText t
|
||||
|
||||
serialize :: CCodeUnit -> Text
|
||||
serialize = show . codeUnitDoc
|
||||
where
|
||||
codeUnitDoc :: CCodeUnit -> HP.Doc
|
||||
codeUnitDoc c = HP.vcat (map prettyCCode (c ^. ccodeCode))
|
||||
|
||||
mkCDecl :: Declaration -> CDecl
|
||||
mkCDecl Declaration {..} =
|
||||
CDecl
|
||||
(mkDeclSpecifier _declType)
|
||||
[(Just declrName, initializer, Nothing)]
|
||||
C.undefNode
|
||||
where
|
||||
declrName :: CDeclr
|
||||
declrName = CDeclr (mkIdent <$> _declName) ptrDeclr Nothing [] C.undefNode
|
||||
ptrDeclr :: [CDerivedDeclarator C.NodeInfo]
|
||||
ptrDeclr = [CPtrDeclr [] C.undefNode | _declIsPtr]
|
||||
initializer :: Maybe CInit
|
||||
initializer = mkCInit <$> _declInitializer
|
||||
|
||||
mkCInit :: Initializer -> CInit
|
||||
mkCInit = \case
|
||||
ExprInitializer e -> CInitExpr (mkCExpr e) C.undefNode
|
||||
DesignatorInitializer ds -> CInitList (f <$> ds) C.undefNode
|
||||
where
|
||||
f :: DesigInit -> ([CDesignator], CInit)
|
||||
f DesigInit {..} = ([CMemberDesig (mkIdent _desigDesignator) C.undefNode], mkCInit _desigInitializer)
|
||||
|
||||
mkCFunDef :: Function -> CFunDef
|
||||
mkCFunDef Function {..} =
|
||||
CFunDef declSpec declr [] statement C.undefNode
|
||||
where
|
||||
declr :: CDeclr
|
||||
declr = CDeclr (Just (mkIdent _funcName)) derivedDeclr Nothing [] C.undefNode
|
||||
declSpec :: [CDeclSpec]
|
||||
declSpec = qualifier <> mkDeclSpecifier _funcReturnType
|
||||
qualifier :: [CDeclSpec]
|
||||
qualifier = if _funcQualifier == StaticInline then [CStorageSpec (CStatic C.undefNode), CFunSpec (CInlineQual C.undefNode)] else []
|
||||
derivedDeclr :: [CDerivedDeclr]
|
||||
derivedDeclr = funDerDeclr <> ptrDeclr
|
||||
ptrDeclr :: [CDerivedDeclr]
|
||||
ptrDeclr = [CPtrDeclr [] C.undefNode | _funcIsPtr]
|
||||
funDerDeclr :: [CDerivedDeclr]
|
||||
funDerDeclr = [CFunDeclr (Right (funArgs, False)) [] C.undefNode]
|
||||
funArgs :: [CDecl]
|
||||
funArgs = mkCDecl <$> _funcArgs
|
||||
statement :: CStat
|
||||
statement = CCompound [] block C.undefNode
|
||||
block :: [CBlockItem]
|
||||
block = mkBlockItem <$> _funcBody
|
||||
|
||||
mkBlockItem :: BodyItem -> CBlockItem
|
||||
mkBlockItem = \case
|
||||
BodyStatement s -> CBlockStmt (mkCStat s)
|
||||
BodyDecl d -> CBlockDecl (mkCDecl d)
|
||||
|
||||
mkCExpr :: Expression -> CExpr
|
||||
mkCExpr = \case
|
||||
ExpressionAssign Assign {..} -> CAssign CAssignOp (mkCExpr _assignLeft) (mkCExpr _assignRight) C.undefNode
|
||||
ExpressionCast Cast {..} -> CCast (mkCDecl _castDecl) (mkCExpr _castExpression) C.undefNode
|
||||
ExpressionCall Call {..} -> CCall (mkCExpr _callCallee) (mkCExpr <$> _callArgs) C.undefNode
|
||||
ExpressionLiteral l -> case l of
|
||||
LiteralInt i -> CConst (CIntConst (cInteger i) C.undefNode)
|
||||
LiteralChar c -> CConst (CCharConst (cChar c) C.undefNode)
|
||||
LiteralString s -> CConst (CStrConst (cString (unpack s)) C.undefNode)
|
||||
ExpressionVar n -> CVar (mkIdent n) C.undefNode
|
||||
ExpressionBinary Binary {..} ->
|
||||
CBinary (mkBinaryOp _binaryOp) (mkCExpr _binaryLeft) (mkCExpr _binaryRight) C.undefNode
|
||||
ExpressionUnary Unary {..} ->
|
||||
CUnary (mkUnaryOp _unaryOp) (mkCExpr _unarySubject) C.undefNode
|
||||
ExpressionMember MemberAccess {..} ->
|
||||
CMember (mkCExpr _memberSubject) (mkIdent _memberField) (_memberOp == Pointer) C.undefNode
|
||||
|
||||
mkCStat :: Statement -> CStat
|
||||
mkCStat = \case
|
||||
StatementReturn me -> CReturn (mkCExpr <$> me) C.undefNode
|
||||
StatementIf If {..} ->
|
||||
CIf (mkCExpr _ifCondition) (mkCStat _ifThen) (mkCStat <$> _ifElse) C.undefNode
|
||||
StatementExpr e -> CExpr (Just (mkCExpr e)) C.undefNode
|
||||
StatementCompound ss -> CCompound [] (CBlockStmt . mkCStat <$> ss) C.undefNode
|
||||
|
||||
mkBinaryOp :: BinaryOp -> CBinaryOp
|
||||
mkBinaryOp = \case
|
||||
Eq -> CEqOp
|
||||
Neq -> CNeqOp
|
||||
And -> CLndOp
|
||||
Or -> CLorOp
|
||||
|
||||
mkUnaryOp :: UnaryOp -> CUnaryOp
|
||||
mkUnaryOp = \case
|
||||
Address -> CAdrOp
|
||||
Indirection -> CIndOp
|
||||
Negation -> CNegOp
|
||||
|
||||
mkDeclSpecifier :: DeclType -> [CDeclSpec]
|
||||
mkDeclSpecifier = \case
|
||||
DeclTypeDefType typeDefName -> mkTypeDefTypeSpec typeDefName
|
||||
DeclTypeDef typ -> CStorageSpec (CTypedef C.undefNode) : mkDeclSpecifier typ
|
||||
DeclStructUnion StructUnion {..} -> mkStructUnionTypeSpec _structUnionTag _structUnionName _structMembers
|
||||
DeclEnum Enum {..} -> mkEnumSpec _enumName _enumMembers
|
||||
BoolType -> [CTypeSpec (CBoolType C.undefNode)]
|
||||
|
||||
mkEnumSpec :: Maybe Text -> Maybe [Text] -> [CDeclSpec]
|
||||
mkEnumSpec name members = [CTypeSpec (CEnumType enum C.undefNode)]
|
||||
where
|
||||
enum :: CEnum
|
||||
enum = CEnum (mkIdent <$> name) (fmap (map (\m -> (mkIdent m, Nothing))) members) [] C.undefNode
|
||||
|
||||
mkTypeDefTypeSpec :: Text -> [CDeclSpec]
|
||||
mkTypeDefTypeSpec name = [CTypeSpec (CTypeDef (mkIdent name) C.undefNode)]
|
||||
|
||||
mkStructUnionTypeSpec :: StructUnionTag -> Maybe Text -> Maybe [Declaration] -> [CDeclSpec]
|
||||
mkStructUnionTypeSpec tag name members = [CTypeSpec (CSUType struct C.undefNode)]
|
||||
where
|
||||
struct :: CStructUnion
|
||||
struct = CStruct cStructTag (mkIdent <$> name) memberDecls [] C.undefNode
|
||||
memberDecls :: Maybe [CDecl]
|
||||
memberDecls = fmap (map mkCDecl) members
|
||||
cStructTag = case tag of
|
||||
StructTag -> CStructTag
|
||||
UnionTag -> CUnionTag
|
||||
|
||||
mkIdent :: Text -> C.Ident
|
||||
mkIdent t = C.Ident (unpack t) 0 C.undefNode
|
||||
@ -2,7 +2,6 @@ module MiniJuvix.Syntax.MonoJuvix.InfoTable where
|
||||
|
||||
import Data.HashMap.Strict qualified as HashMap
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Backends
|
||||
import MiniJuvix.Syntax.MonoJuvix.Language
|
||||
|
||||
data ConstructorInfo = ConstructorInfo
|
||||
@ -18,15 +17,10 @@ newtype AxiomInfo = AxiomInfo
|
||||
{ _axiomInfoType :: Type
|
||||
}
|
||||
|
||||
newtype CompileInfo = CompileInfo
|
||||
{ _compileInfoBackendItems :: [BackendItem]
|
||||
}
|
||||
|
||||
data InfoTable = InfoTable
|
||||
{ _infoConstructors :: HashMap Name ConstructorInfo,
|
||||
_infoAxioms :: HashMap Name AxiomInfo,
|
||||
_infoFunctions :: HashMap Name FunctionInfo,
|
||||
_infoCompilationRules :: HashMap Name CompileInfo
|
||||
_infoFunctions :: HashMap Name FunctionInfo
|
||||
}
|
||||
|
||||
-- TODO temporary function.
|
||||
@ -54,16 +48,9 @@ buildTable m = InfoTable {..}
|
||||
[ (d ^. axiomName, AxiomInfo (d ^. axiomType))
|
||||
| StatementAxiom d <- ss
|
||||
]
|
||||
_infoCompilationRules :: HashMap Name CompileInfo
|
||||
_infoCompilationRules =
|
||||
HashMap.fromList
|
||||
[ (d ^. compileName, CompileInfo (d ^. compileBackendItems))
|
||||
| StatementCompile d <- ss
|
||||
]
|
||||
ss = m ^. (moduleBody . moduleStatements)
|
||||
|
||||
makeLenses ''InfoTable
|
||||
makeLenses ''FunctionInfo
|
||||
makeLenses ''ConstructorInfo
|
||||
makeLenses ''AxiomInfo
|
||||
makeLenses ''CompileInfo
|
||||
|
||||
@ -6,7 +6,6 @@ module MiniJuvix.Syntax.MonoJuvix.Language
|
||||
where
|
||||
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Backends
|
||||
import MiniJuvix.Syntax.Concrete.Language qualified as C
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..))
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
|
||||
@ -63,14 +62,8 @@ data Statement
|
||||
= StatementInductive InductiveDef
|
||||
| StatementFunction FunctionDef
|
||||
| StatementForeign ForeignBlock
|
||||
| StatementCompile Compile
|
||||
| StatementAxiom AxiomDef
|
||||
|
||||
data Compile = Compile
|
||||
{ _compileName :: Name,
|
||||
_compileBackendItems :: [BackendItem]
|
||||
}
|
||||
|
||||
data AxiomDef = AxiomDef
|
||||
{ _axiomName :: AxiomName,
|
||||
_axiomType :: Type
|
||||
@ -159,7 +152,6 @@ makeLenses ''ModuleBody
|
||||
makeLenses ''Application
|
||||
makeLenses ''InductiveConstructorDef
|
||||
makeLenses ''ConstructorApp
|
||||
makeLenses ''Compile
|
||||
|
||||
instance HasAtomicity Application where
|
||||
atomicity = const (Aggregate appFixity)
|
||||
|
||||
@ -4,14 +4,35 @@ module MiniJuvix.Syntax.MonoJuvix.MonoJuvixResult
|
||||
)
|
||||
where
|
||||
|
||||
import Data.HashMap.Strict qualified as HashMap
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Abstract.AbstractResult qualified as A
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.InfoTable qualified as S
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
|
||||
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult qualified as Micro
|
||||
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as Micro
|
||||
import MiniJuvix.Syntax.MonoJuvix.InfoTable
|
||||
import MiniJuvix.Syntax.MonoJuvix.Language
|
||||
|
||||
type CompileInfoTable = HashMap S.NameId S.CompileInfo
|
||||
|
||||
data MonoJuvixResult = MonoJuvixResult
|
||||
{ _resultMicroTyped :: Micro.MicroJuvixTypedResult,
|
||||
_resultModules :: NonEmpty Module
|
||||
}
|
||||
|
||||
makeLenses ''MonoJuvixResult
|
||||
|
||||
compileInfoTable :: MonoJuvixResult -> CompileInfoTable
|
||||
compileInfoTable r =
|
||||
HashMap.mapKeys
|
||||
(^. S.nameId)
|
||||
( r
|
||||
^. resultMicroTyped
|
||||
. Micro.resultMicroJuvixResult
|
||||
. Micro.resultAbstract
|
||||
. A.resultScoper
|
||||
. Scoper.resultScoperTable
|
||||
. S.infoCompilationRules
|
||||
)
|
||||
|
||||
@ -79,6 +79,9 @@ kwCompile = keyword Str.compile
|
||||
kwAgda :: Doc Ann
|
||||
kwAgda = keyword Str.agda
|
||||
|
||||
kwC :: Doc Ann
|
||||
kwC = keyword Str.cBackend
|
||||
|
||||
kwGhc :: Doc Ann
|
||||
kwGhc = keyword Str.ghc
|
||||
|
||||
@ -197,6 +200,7 @@ instance PrettyCode Backend where
|
||||
ppCode = \case
|
||||
BackendGhc -> return kwGhc
|
||||
BackendAgda -> return kwAgda
|
||||
BackendC -> return kwC
|
||||
|
||||
instance PrettyCode ForeignBlock where
|
||||
ppCode ForeignBlock {..} = do
|
||||
@ -207,12 +211,6 @@ instance PrettyCode ForeignBlock where
|
||||
<> line
|
||||
<> rbrace
|
||||
|
||||
instance PrettyCode Compile where
|
||||
ppCode Compile {..} = do
|
||||
compileName' <- ppCode _compileName
|
||||
compileBackendItems' <- ppBlock _compileBackendItems
|
||||
return $ kwCompile <+> compileName' <+> compileBackendItems'
|
||||
|
||||
instance PrettyCode AxiomDef where
|
||||
ppCode AxiomDef {..} = do
|
||||
axiomName' <- ppCode _axiomName
|
||||
@ -225,7 +223,6 @@ instance PrettyCode Statement where
|
||||
StatementFunction f -> ppCode f
|
||||
StatementInductive f -> ppCode f
|
||||
StatementAxiom f -> ppCode f
|
||||
StatementCompile f -> ppCode f
|
||||
|
||||
instance PrettyCode ModuleBody where
|
||||
ppCode m = do
|
||||
|
||||
695
src/MiniJuvix/Translation/MonoJuvixToMiniC.hs
Normal file
695
src/MiniJuvix/Translation/MonoJuvixToMiniC.hs
Normal file
@ -0,0 +1,695 @@
|
||||
module MiniJuvix.Translation.MonoJuvixToMiniC where
|
||||
|
||||
import Data.HashMap.Strict qualified as HashMap
|
||||
import Data.Text qualified as T
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Backends
|
||||
import MiniJuvix.Syntax.Concrete.Language qualified as C
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.InfoTable qualified as S
|
||||
import MiniJuvix.Syntax.ForeignBlock
|
||||
import MiniJuvix.Syntax.MiniC.Language
|
||||
import MiniJuvix.Syntax.MiniC.Serialization
|
||||
import MiniJuvix.Syntax.MonoJuvix.Language qualified as Mono
|
||||
import MiniJuvix.Syntax.NameId
|
||||
import MiniJuvix.Translation.MicroJuvixToMonoJuvix qualified as Mono
|
||||
import MiniJuvix.Translation.MonoJuvixToMiniC.Strings
|
||||
|
||||
newtype MiniCResult = MiniCResult
|
||||
{ _resultCCode :: Text
|
||||
}
|
||||
|
||||
makeLenses ''MiniCResult
|
||||
|
||||
entryMiniC ::
|
||||
Mono.MonoJuvixResult ->
|
||||
Sem r MiniCResult
|
||||
entryMiniC i = return (MiniCResult (serialize cunitResult))
|
||||
where
|
||||
compileInfo :: Mono.CompileInfoTable
|
||||
compileInfo = Mono.compileInfoTable i
|
||||
cunitResult :: CCodeUnit
|
||||
cunitResult =
|
||||
CCodeUnit
|
||||
{ _ccodeCode = cheader <> cmodules
|
||||
}
|
||||
cheader :: [CCode]
|
||||
cheader =
|
||||
map
|
||||
ExternalMacro
|
||||
[ CppIncludeSystem stdlib,
|
||||
CppIncludeSystem stdbool,
|
||||
CppIncludeSystem stdio
|
||||
]
|
||||
cmodules :: [CCode]
|
||||
cmodules = toList (i ^. Mono.resultModules) >>= (run . runReader compileInfo . goModule)
|
||||
|
||||
type Err = Text
|
||||
|
||||
unsupported :: Err -> a
|
||||
unsupported msg = error (msg <> " Mono to C: not yet supported")
|
||||
|
||||
goModule ::
|
||||
Member (Reader Mono.CompileInfoTable) r =>
|
||||
Mono.Module ->
|
||||
Sem r [CCode]
|
||||
goModule Mono.Module {..} = goModuleBody _moduleBody
|
||||
|
||||
goModuleBody ::
|
||||
Member (Reader Mono.CompileInfoTable) r =>
|
||||
Mono.ModuleBody ->
|
||||
Sem r [CCode]
|
||||
goModuleBody Mono.ModuleBody {..} =
|
||||
concatMapM goStatement _moduleStatements
|
||||
|
||||
goStatement ::
|
||||
Member (Reader Mono.CompileInfoTable) r =>
|
||||
Mono.Statement ->
|
||||
Sem r [CCode]
|
||||
goStatement = \case
|
||||
Mono.StatementInductive d -> return (goInductiveDef d)
|
||||
Mono.StatementFunction d -> return (goFunctionDef d)
|
||||
Mono.StatementForeign d -> return (goForeign d)
|
||||
Mono.StatementAxiom d -> goAxiom d
|
||||
|
||||
type CTypeName = Text
|
||||
|
||||
asStruct :: Text -> Text
|
||||
asStruct n = n <> "_s"
|
||||
|
||||
asTypeDef :: Text -> Text
|
||||
asTypeDef n = n <> "_t"
|
||||
|
||||
asTag :: Text -> Text
|
||||
asTag n = n <> "_tag"
|
||||
|
||||
asNew :: Text -> Text
|
||||
asNew n = "new_" <> n
|
||||
|
||||
asCast :: Text -> Text
|
||||
asCast n = "as_" <> n
|
||||
|
||||
asIs :: Text -> Text
|
||||
asIs n = "is_" <> n
|
||||
|
||||
asFunArg :: Text -> Text
|
||||
asFunArg n = "fa" <> n
|
||||
|
||||
asCtorArg :: Text -> Text
|
||||
asCtorArg n = "ca" <> n
|
||||
|
||||
mkArgs :: (Text -> Text) -> [Text]
|
||||
mkArgs f = map (f . show) [0 :: Integer ..]
|
||||
|
||||
funArgs :: [Text]
|
||||
funArgs = mkArgs asFunArg
|
||||
|
||||
ctorArgs :: [Text]
|
||||
ctorArgs = mkArgs asCtorArg
|
||||
|
||||
mkName :: Mono.Name -> Text
|
||||
mkName n =
|
||||
adaptFirstLetter lexeme <> nameTextSuffix
|
||||
where
|
||||
lexeme
|
||||
| T.null lexeme' = "v"
|
||||
| otherwise = lexeme'
|
||||
where
|
||||
lexeme' = T.filter isValidChar (n ^. Mono.nameText)
|
||||
isValidChar :: Char -> Bool
|
||||
isValidChar c = isLetter c && isAscii c
|
||||
adaptFirstLetter :: Text -> Text
|
||||
adaptFirstLetter t = case T.uncons t of
|
||||
Nothing -> impossible
|
||||
Just (h, r) -> T.cons (capitalize h) r
|
||||
where
|
||||
capitalize :: Char -> Char
|
||||
capitalize
|
||||
| capital = toUpper
|
||||
| otherwise = toLower
|
||||
capital = case n ^. Mono.nameKind of
|
||||
Mono.KNameConstructor -> True
|
||||
Mono.KNameInductive -> True
|
||||
Mono.KNameTopModule -> True
|
||||
Mono.KNameLocalModule -> True
|
||||
_ -> False
|
||||
nameTextSuffix :: Text
|
||||
nameTextSuffix = case n ^. Mono.nameKind of
|
||||
Mono.KNameTopModule -> mempty
|
||||
Mono.KNameFunction ->
|
||||
if n ^. Mono.nameText == main then mempty else idSuffix
|
||||
_ -> idSuffix
|
||||
idSuffix :: Text
|
||||
idSuffix = "_" <> show (n ^. Mono.nameId . unNameId)
|
||||
|
||||
goFunctionDef :: Mono.FunctionDef -> [CCode]
|
||||
goFunctionDef Mono.FunctionDef {..} =
|
||||
[ ExternalFunc
|
||||
( Function
|
||||
{ _funcReturnType = funReturnType ^. typeDeclType,
|
||||
_funcIsPtr = funReturnType ^. typeIsPtr,
|
||||
_funcQualifier = None,
|
||||
_funcName = mkName _funDefName,
|
||||
_funcArgs = namedArgs asFunArg funArgTypes,
|
||||
_funcBody = maybeToList (BodyStatement <$> mkBody (goFunctionClause <$> toList _funDefClauses))
|
||||
}
|
||||
)
|
||||
]
|
||||
where
|
||||
mkBody :: [(Maybe Expression, Statement)] -> Maybe Statement
|
||||
mkBody cs = do
|
||||
let lastBranch = const fallback . head <$> nonEmpty cs
|
||||
foldr mkIf lastBranch cs
|
||||
mkIf :: (Maybe Expression, Statement) -> Maybe Statement -> Maybe Statement
|
||||
mkIf (mcondition, thenBranch) elseBranch = case mcondition of
|
||||
Nothing -> Just thenBranch
|
||||
Just condition ->
|
||||
Just
|
||||
( StatementIf
|
||||
( If
|
||||
{ _ifCondition = condition,
|
||||
_ifThen = thenBranch,
|
||||
_ifElse = elseBranch
|
||||
}
|
||||
)
|
||||
)
|
||||
funArgTypes :: [CDeclType]
|
||||
funArgTypes = fst funType
|
||||
funReturnType :: CDeclType
|
||||
funReturnType = snd funType
|
||||
funType :: ([CDeclType], CDeclType)
|
||||
funType = unfoldFunType _funDefType
|
||||
unfoldFunType :: Mono.Type -> ([CDeclType], CDeclType)
|
||||
unfoldFunType = \case
|
||||
Mono.TypeFunction (Mono.Function l r) ->
|
||||
first (goType l :) (unfoldFunType r)
|
||||
t -> ([], goType t)
|
||||
fallback :: Statement
|
||||
fallback =
|
||||
StatementCompound
|
||||
[ StatementExpr
|
||||
( functionCall
|
||||
(ExpressionVar fprintf)
|
||||
[ ExpressionVar stderr_,
|
||||
ExpressionLiteral (LiteralString "Error: Pattern match(es) are non-exhaustive in %s\n"),
|
||||
ExpressionLiteral (LiteralString (_funDefName ^. Mono.nameText))
|
||||
]
|
||||
),
|
||||
StatementExpr
|
||||
( functionCall
|
||||
(ExpressionVar exit)
|
||||
[ ExpressionVar exitFailure_
|
||||
]
|
||||
)
|
||||
]
|
||||
|
||||
type PatternBindings = HashMap Text Expression
|
||||
|
||||
goFunctionClause :: Mono.FunctionClause -> (Maybe Expression, Statement)
|
||||
goFunctionClause Mono.FunctionClause {..} = (clauseCondition, returnStmt)
|
||||
where
|
||||
conditions :: [Expression]
|
||||
conditions = do
|
||||
(p, arg) <- zip _clausePatterns funArgs
|
||||
patternCondition (ExpressionVar arg) p
|
||||
|
||||
patternCondition :: Expression -> Mono.Pattern -> [Expression]
|
||||
patternCondition arg = \case
|
||||
Mono.PatternConstructorApp Mono.ConstructorApp {..} ->
|
||||
isCtor : subConditions
|
||||
where
|
||||
ctorName :: Text
|
||||
ctorName = mkName _constrAppConstructor
|
||||
isCtor :: Expression
|
||||
isCtor = functionCall (ExpressionVar (asIs ctorName)) [arg]
|
||||
asCtor :: Expression
|
||||
asCtor = functionCall (ExpressionVar (asCast ctorName)) [arg]
|
||||
subConditions :: [Expression]
|
||||
subConditions = do
|
||||
let subArgs = map (memberAccess Object asCtor) ctorArgs
|
||||
(p, subArg) <- zip _constrAppParameters subArgs
|
||||
patternCondition subArg p
|
||||
Mono.PatternVariable {} -> []
|
||||
Mono.PatternWildcard {} -> []
|
||||
|
||||
clauseCondition :: Maybe Expression
|
||||
clauseCondition = fmap (foldr1 f) (nonEmpty conditions)
|
||||
where
|
||||
f :: Expression -> Expression -> Expression
|
||||
f e1 e2 =
|
||||
ExpressionBinary
|
||||
( Binary
|
||||
{ _binaryOp = And,
|
||||
_binaryLeft = e1,
|
||||
_binaryRight = e2
|
||||
}
|
||||
)
|
||||
patternBindings :: PatternBindings
|
||||
patternBindings = HashMap.fromList patternVars
|
||||
patternVars :: [(Text, Expression)]
|
||||
patternVars = do
|
||||
(p, arg) <- zipWith (curry (second ExpressionVar)) _clausePatterns funArgs
|
||||
case p of
|
||||
Mono.PatternVariable v -> [(v ^. Mono.nameText, arg)]
|
||||
Mono.PatternConstructorApp Mono.ConstructorApp {..} ->
|
||||
goConstructorApp arg _constrAppConstructor _constrAppParameters
|
||||
Mono.PatternWildcard {} -> []
|
||||
returnStmt :: Statement
|
||||
returnStmt = StatementReturn (Just (run (runReader patternBindings (goExpression False _clauseBody))))
|
||||
|
||||
goConstructorApp :: Expression -> Mono.Name -> [Mono.Pattern] -> [(Text, Expression)]
|
||||
goConstructorApp arg n ps = do
|
||||
(p, field) <- zip ps ctorArgs
|
||||
let ctorField = memberAccess Object asConstructor field
|
||||
case p of
|
||||
Mono.PatternVariable v -> [(v ^. Mono.nameText, ctorField)]
|
||||
Mono.PatternConstructorApp Mono.ConstructorApp {..} ->
|
||||
goConstructorApp ctorField _constrAppConstructor _constrAppParameters
|
||||
Mono.PatternWildcard {} -> []
|
||||
where
|
||||
asConstructor :: Expression
|
||||
asConstructor = functionCall (ExpressionVar (asCast (mkName n))) [arg]
|
||||
|
||||
goExpression :: Member (Reader PatternBindings) r => Bool -> Mono.Expression -> Sem r Expression
|
||||
goExpression fromApplication = \case
|
||||
Mono.ExpressionIden i -> goIden fromApplication i
|
||||
Mono.ExpressionApplication a -> goApplication a
|
||||
Mono.ExpressionLiteral l -> return (ExpressionLiteral (goLiteral l))
|
||||
|
||||
goIden :: Member (Reader PatternBindings) r => Bool -> Mono.Iden -> Sem r Expression
|
||||
goIden fromApplication = \case
|
||||
Mono.IdenFunction n
|
||||
| fromApplication -> return e
|
||||
| otherwise -> return (functionCall e [])
|
||||
where
|
||||
e :: Expression
|
||||
e = ExpressionVar (mkName n)
|
||||
Mono.IdenConstructor n
|
||||
| fromApplication -> return newCtor
|
||||
| otherwise -> return (functionCall newCtor [])
|
||||
where
|
||||
newCtor :: Expression
|
||||
newCtor = ExpressionVar (asNew (mkName n))
|
||||
Mono.IdenVar n -> HashMap.lookupDefault impossible (n ^. Mono.nameText) <$> ask
|
||||
Mono.IdenAxiom n -> return (ExpressionVar (mkName n))
|
||||
|
||||
goApplication :: forall r. Member (Reader PatternBindings) r => Mono.Application -> Sem r Expression
|
||||
goApplication a = do
|
||||
(fName, fArgs) <- f
|
||||
return (functionCall fName (reverse fArgs))
|
||||
where
|
||||
f :: Sem r (Expression, [Expression])
|
||||
f = unfoldApp a
|
||||
unfoldApp :: Mono.Application -> Sem r (Expression, [Expression])
|
||||
unfoldApp Mono.Application {..} = case _appLeft of
|
||||
Mono.ExpressionApplication x -> do
|
||||
fName <- goExpression False _appRight
|
||||
uf <- unfoldApp x
|
||||
return (second (fName :) uf)
|
||||
_ -> do
|
||||
fName <- goExpression True _appLeft
|
||||
fArg <- goExpression False _appRight
|
||||
return (fName, [fArg])
|
||||
|
||||
goLiteral :: C.LiteralLoc -> Literal
|
||||
goLiteral C.LiteralLoc {..} = case _literalLocLiteral of
|
||||
C.LitString s -> LiteralString s
|
||||
C.LitInteger i -> LiteralInt i
|
||||
|
||||
goAxiom ::
|
||||
Member (Reader Mono.CompileInfoTable) r =>
|
||||
Mono.AxiomDef ->
|
||||
Sem r [CCode]
|
||||
goAxiom a = do
|
||||
backends <- lookupBackends (axiomName ^. Mono.nameId)
|
||||
case firstJust getCode backends of
|
||||
Nothing -> error ("C backend does not support this axiom:" <> show (axiomName ^. Mono.nameText))
|
||||
Just defineBody ->
|
||||
return
|
||||
[ ExternalMacro
|
||||
( CppDefine
|
||||
( Define
|
||||
{ _defineName = defineName,
|
||||
_defineBody = defineBody
|
||||
}
|
||||
)
|
||||
)
|
||||
]
|
||||
where
|
||||
axiomName :: Mono.Name
|
||||
axiomName = a ^. Mono.axiomName
|
||||
defineName :: Text
|
||||
defineName = mkName axiomName
|
||||
getCode :: BackendItem -> Maybe Text
|
||||
getCode b =
|
||||
guard (BackendC == b ^. backendItemBackend)
|
||||
$> b ^. backendItemCode
|
||||
lookupBackends ::
|
||||
Member (Reader Mono.CompileInfoTable) r =>
|
||||
NameId ->
|
||||
Sem r [BackendItem]
|
||||
lookupBackends f = (^. S.compileInfoBackendItems) . HashMap.lookupDefault impossible f <$> ask
|
||||
|
||||
goForeign :: ForeignBlock -> [CCode]
|
||||
goForeign b = case b ^. foreignBackend of
|
||||
BackendC -> [Verbatim (b ^. foreignCode)]
|
||||
_ -> []
|
||||
|
||||
mkInductiveName :: Mono.InductiveDef -> Text
|
||||
mkInductiveName i = mkName (i ^. Mono.inductiveName)
|
||||
|
||||
mkInductiveConstructorNames :: Mono.InductiveDef -> [Text]
|
||||
mkInductiveConstructorNames i = mkName . view Mono.constructorName <$> i ^. Mono.inductiveConstructors
|
||||
|
||||
goInductiveDef :: Mono.InductiveDef -> [CCode]
|
||||
goInductiveDef i =
|
||||
[ ExternalDecl structTypeDef,
|
||||
ExternalDecl tagsType
|
||||
]
|
||||
<> (i ^. Mono.inductiveConstructors >>= goInductiveConstructorDef)
|
||||
<> [ExternalDecl inductiveDecl]
|
||||
<> (i ^. Mono.inductiveConstructors >>= goInductiveConstructorNew i)
|
||||
<> (ExternalFunc . isFunction <$> constructorNames)
|
||||
<> (ExternalFunc . asFunction <$> constructorNames)
|
||||
where
|
||||
baseName :: Text
|
||||
baseName = mkName (i ^. Mono.inductiveName)
|
||||
|
||||
constructorNames :: [Text]
|
||||
constructorNames = mkInductiveConstructorNames i
|
||||
|
||||
structTypeDef :: Declaration
|
||||
structTypeDef =
|
||||
typeDefWrap
|
||||
(asTypeDef baseName)
|
||||
( DeclStructUnion
|
||||
( StructUnion
|
||||
{ _structUnionTag = StructTag,
|
||||
_structUnionName = Just (asStruct baseName),
|
||||
_structMembers = Nothing
|
||||
}
|
||||
)
|
||||
)
|
||||
|
||||
tagsType :: Declaration
|
||||
tagsType =
|
||||
typeDefWrap
|
||||
(asTag baseName)
|
||||
( DeclEnum
|
||||
( Enum
|
||||
{ _enumName = Nothing,
|
||||
_enumMembers = Just (asTag <$> constructorNames)
|
||||
}
|
||||
)
|
||||
)
|
||||
|
||||
inductiveDecl :: Declaration
|
||||
inductiveDecl =
|
||||
Declaration
|
||||
{ _declType = inductiveStruct,
|
||||
_declIsPtr = False,
|
||||
_declName = Nothing,
|
||||
_declInitializer = Nothing
|
||||
}
|
||||
|
||||
inductiveStruct :: DeclType
|
||||
inductiveStruct =
|
||||
DeclStructUnion
|
||||
( StructUnion
|
||||
{ _structUnionTag = StructTag,
|
||||
_structUnionName = Just (asStruct baseName),
|
||||
_structMembers =
|
||||
Just
|
||||
[ typeDefType (asTag baseName) tag,
|
||||
Declaration
|
||||
{ _declType = unionMembers,
|
||||
_declIsPtr = False,
|
||||
_declName = Just data_,
|
||||
_declInitializer = Nothing
|
||||
}
|
||||
]
|
||||
}
|
||||
)
|
||||
|
||||
unionMembers :: DeclType
|
||||
unionMembers =
|
||||
DeclStructUnion
|
||||
( StructUnion
|
||||
{ _structUnionTag = UnionTag,
|
||||
_structUnionName = Nothing,
|
||||
_structMembers = Just (map (\ctorName -> typeDefType (asTypeDef ctorName) ctorName) constructorNames)
|
||||
}
|
||||
)
|
||||
|
||||
isFunction :: Text -> Function
|
||||
isFunction ctorName =
|
||||
Function
|
||||
{ _funcReturnType = BoolType,
|
||||
_funcIsPtr = False,
|
||||
_funcQualifier = StaticInline,
|
||||
_funcName = asIs ctorName,
|
||||
_funcArgs = [ptrType (DeclTypeDefType (asTypeDef baseName)) funcArg],
|
||||
_funcBody =
|
||||
[ returnStatement
|
||||
( equals
|
||||
(memberAccess Pointer (ExpressionVar funcArg) tag)
|
||||
(ExpressionVar (asTag ctorName))
|
||||
)
|
||||
]
|
||||
}
|
||||
where
|
||||
funcArg :: Text
|
||||
funcArg = "a"
|
||||
|
||||
asFunction :: Text -> Function
|
||||
asFunction ctorName =
|
||||
Function
|
||||
{ _funcReturnType = DeclTypeDefType (asTypeDef ctorName),
|
||||
_funcIsPtr = False,
|
||||
_funcQualifier = StaticInline,
|
||||
_funcName = asCast ctorName,
|
||||
_funcArgs = [ptrType (DeclTypeDefType (asTypeDef baseName)) funcArg],
|
||||
_funcBody =
|
||||
[ returnStatement
|
||||
(memberAccess Object (memberAccess Pointer (ExpressionVar funcArg) data_) ctorName)
|
||||
]
|
||||
}
|
||||
where
|
||||
funcArg :: Text
|
||||
funcArg = "a"
|
||||
|
||||
goInductiveConstructorNew ::
|
||||
Mono.InductiveDef ->
|
||||
Mono.InductiveConstructorDef ->
|
||||
[CCode]
|
||||
goInductiveConstructorNew i ctor =
|
||||
[ExternalFunc ctorNewFun]
|
||||
where
|
||||
ctorNewFun :: Function
|
||||
ctorNewFun = if null ctorParams then ctorNewNullary else ctorNewNary
|
||||
|
||||
baseName :: Text
|
||||
baseName = mkName (ctor ^. Mono.constructorName)
|
||||
|
||||
inductiveName :: Text
|
||||
inductiveName = mkInductiveName i
|
||||
|
||||
ctorParams :: [Mono.Type]
|
||||
ctorParams = ctor ^. Mono.constructorParameters
|
||||
|
||||
ctorNewNullary :: Function
|
||||
ctorNewNullary =
|
||||
commonFunctionDeclr
|
||||
[]
|
||||
[ BodyDecl allocInductive,
|
||||
BodyDecl (commonInitDecl (dataInit true_)),
|
||||
BodyStatement assignPtr,
|
||||
returnStatement (ExpressionVar tmpPtrName)
|
||||
]
|
||||
|
||||
ctorNewNary :: Function
|
||||
ctorNewNary =
|
||||
commonFunctionDeclr
|
||||
ctorDecls
|
||||
[ BodyDecl allocInductive,
|
||||
BodyDecl ctorStructInit,
|
||||
BodyDecl (commonInitDecl (dataInit tmpCtorStructName)),
|
||||
BodyStatement assignPtr,
|
||||
returnStatement (ExpressionVar tmpPtrName)
|
||||
]
|
||||
where
|
||||
ctorDecls :: [Declaration]
|
||||
ctorDecls = inductiveCtorArgs ctor
|
||||
|
||||
ctorInit :: [DesigInit]
|
||||
-- TODO: _declName is never Nothing by construction, fix the types
|
||||
ctorInit = map (f . fromJust . _declName) ctorDecls
|
||||
|
||||
f :: Text -> DesigInit
|
||||
f fieldName =
|
||||
DesigInit
|
||||
{ _desigDesignator = fieldName,
|
||||
_desigInitializer = ExprInitializer (ExpressionVar fieldName)
|
||||
}
|
||||
|
||||
ctorStructInit :: Declaration
|
||||
ctorStructInit =
|
||||
Declaration
|
||||
{ _declType = DeclTypeDefType (asTypeDef baseName),
|
||||
_declIsPtr = False,
|
||||
_declName = Just tmpCtorStructName,
|
||||
_declInitializer = Just (DesignatorInitializer ctorInit)
|
||||
}
|
||||
|
||||
commonFunctionDeclr :: [Declaration] -> [BodyItem] -> Function
|
||||
commonFunctionDeclr args body =
|
||||
Function
|
||||
{ _funcReturnType = DeclTypeDefType (asTypeDef inductiveName),
|
||||
_funcIsPtr = True,
|
||||
_funcQualifier = StaticInline,
|
||||
_funcName = asNew baseName,
|
||||
_funcArgs = args,
|
||||
_funcBody = body
|
||||
}
|
||||
|
||||
commonInitDecl :: Initializer -> Declaration
|
||||
commonInitDecl di =
|
||||
( Declaration
|
||||
{ _declType = DeclTypeDefType (asTypeDef inductiveName),
|
||||
_declIsPtr = False,
|
||||
_declName = Just tmpStructName,
|
||||
_declInitializer =
|
||||
Just
|
||||
( DesignatorInitializer
|
||||
[ DesigInit
|
||||
{ _desigDesignator = tag,
|
||||
_desigInitializer = ExprInitializer (ExpressionVar (asTag baseName))
|
||||
},
|
||||
DesigInit
|
||||
{ _desigDesignator = data_,
|
||||
_desigInitializer = di
|
||||
}
|
||||
]
|
||||
)
|
||||
}
|
||||
)
|
||||
|
||||
tmpPtrName :: Text
|
||||
tmpPtrName = "n"
|
||||
|
||||
tmpStructName :: Text
|
||||
tmpStructName = "m"
|
||||
|
||||
tmpCtorStructName :: Text
|
||||
tmpCtorStructName = "s"
|
||||
|
||||
allocInductive :: Declaration
|
||||
allocInductive =
|
||||
( Declaration
|
||||
{ _declType = DeclTypeDefType (asTypeDef inductiveName),
|
||||
_declIsPtr = True,
|
||||
_declName = Just tmpPtrName,
|
||||
_declInitializer = Just (ExprInitializer (mallocSizeOf (asTypeDef inductiveName)))
|
||||
}
|
||||
)
|
||||
|
||||
dataInit :: Text -> Initializer
|
||||
dataInit varName =
|
||||
DesignatorInitializer
|
||||
[ DesigInit
|
||||
{ _desigDesignator = baseName,
|
||||
_desigInitializer = ExprInitializer (ExpressionVar varName)
|
||||
}
|
||||
]
|
||||
|
||||
assignPtr :: Statement
|
||||
assignPtr =
|
||||
StatementExpr
|
||||
( ExpressionAssign
|
||||
( Assign
|
||||
{ _assignLeft =
|
||||
ExpressionUnary
|
||||
( Unary
|
||||
{ _unaryOp = Indirection,
|
||||
_unarySubject = ExpressionVar tmpPtrName
|
||||
}
|
||||
),
|
||||
_assignRight = ExpressionVar tmpStructName
|
||||
}
|
||||
)
|
||||
)
|
||||
|
||||
namedArgs :: (Text -> Text) -> [CDeclType] -> [Declaration]
|
||||
namedArgs prefix = zipWith goTypeDecl argLabels
|
||||
where
|
||||
argLabels :: [Text]
|
||||
argLabels = prefix . show <$> [0 :: Integer ..]
|
||||
|
||||
inductiveCtorArgs :: Mono.InductiveConstructorDef -> [Declaration]
|
||||
inductiveCtorArgs ctor = namedArgs asCtorArg (goType <$> ctorParams)
|
||||
where
|
||||
ctorParams :: [Mono.Type]
|
||||
ctorParams = ctor ^. Mono.constructorParameters
|
||||
|
||||
goInductiveConstructorDef ::
|
||||
Mono.InductiveConstructorDef ->
|
||||
[CCode]
|
||||
goInductiveConstructorDef ctor =
|
||||
[ExternalDecl ctorDecl]
|
||||
where
|
||||
ctorDecl :: Declaration
|
||||
ctorDecl = if null ctorParams then ctorBool else ctorStruct
|
||||
|
||||
baseName :: Text
|
||||
baseName = mkName (ctor ^. Mono.constructorName)
|
||||
|
||||
ctorParams :: [Mono.Type]
|
||||
ctorParams = ctor ^. Mono.constructorParameters
|
||||
|
||||
ctorBool :: Declaration
|
||||
ctorBool = typeDefWrap (asTypeDef baseName) BoolType
|
||||
|
||||
ctorStruct :: Declaration
|
||||
ctorStruct = typeDefWrap (asTypeDef baseName) struct
|
||||
|
||||
struct :: DeclType
|
||||
struct =
|
||||
DeclStructUnion
|
||||
( StructUnion
|
||||
{ _structUnionTag = StructTag,
|
||||
_structUnionName = Just (asStruct baseName),
|
||||
_structMembers = Just (inductiveCtorArgs ctor)
|
||||
}
|
||||
)
|
||||
|
||||
goType :: Mono.Type -> CDeclType
|
||||
goType = \case
|
||||
Mono.TypeIden ti -> getMonoType ti
|
||||
Mono.TypeFunction {} -> unsupported "TypeFunction"
|
||||
Mono.TypeUniverse {} -> unsupported "TypeUniverse"
|
||||
Mono.TypeAny {} -> unsupported "TypeAny"
|
||||
where
|
||||
getMonoType :: Mono.TypeIden -> CDeclType
|
||||
getMonoType = \case
|
||||
Mono.TypeIdenInductive mn ->
|
||||
CDeclType
|
||||
{ _typeDeclType = DeclTypeDefType (asTypeDef (mkName mn)),
|
||||
_typeIsPtr = True
|
||||
}
|
||||
Mono.TypeIdenAxiom mn ->
|
||||
CDeclType
|
||||
{ _typeDeclType = DeclTypeDefType (mkName mn),
|
||||
_typeIsPtr = False
|
||||
}
|
||||
|
||||
goTypeDecl :: Text -> CDeclType -> Declaration
|
||||
goTypeDecl n CDeclType {..} =
|
||||
Declaration
|
||||
{ _declType = _typeDeclType,
|
||||
_declIsPtr = _typeIsPtr,
|
||||
_declName = Just n,
|
||||
_declInitializer = Nothing
|
||||
}
|
||||
|
||||
mallocSizeOf :: Text -> Expression
|
||||
mallocSizeOf typeName =
|
||||
functionCall (ExpressionVar malloc) [functionCall (ExpressionVar sizeof) [ExpressionVar typeName]]
|
||||
42
src/MiniJuvix/Translation/MonoJuvixToMiniC/Strings.hs
Normal file
42
src/MiniJuvix/Translation/MonoJuvixToMiniC/Strings.hs
Normal file
@ -0,0 +1,42 @@
|
||||
module MiniJuvix.Translation.MonoJuvixToMiniC.Strings where
|
||||
|
||||
import MiniJuvix.Prelude
|
||||
|
||||
stdlib :: IsString s => s
|
||||
stdlib = "stdlib.h"
|
||||
|
||||
stdbool :: IsString s => s
|
||||
stdbool = "stdbool.h"
|
||||
|
||||
stdio :: IsString s => s
|
||||
stdio = "stdio.h"
|
||||
|
||||
main :: IsString s => s
|
||||
main = "main"
|
||||
|
||||
fprintf :: IsString s => s
|
||||
fprintf = "fprintf"
|
||||
|
||||
stderr_ :: IsString s => s
|
||||
stderr_ = "stderr"
|
||||
|
||||
exit :: IsString s => s
|
||||
exit = "exit"
|
||||
|
||||
exitFailure_ :: IsString s => s
|
||||
exitFailure_ = "EXIT_FAILURE"
|
||||
|
||||
malloc :: IsString s => s
|
||||
malloc = "malloc"
|
||||
|
||||
sizeof :: IsString s => s
|
||||
sizeof = "sizeof"
|
||||
|
||||
true_ :: IsString s => s
|
||||
true_ = "true"
|
||||
|
||||
tag :: IsString s => s
|
||||
tag = "tag"
|
||||
|
||||
data_ :: IsString s => s
|
||||
data_ = "data"
|
||||
@ -4,19 +4,18 @@ module MiniJuvix.Translation.MonoJuvixToMiniHaskell
|
||||
)
|
||||
where
|
||||
|
||||
import Data.HashMap.Strict qualified as HashMap
|
||||
import Data.Text qualified as Text
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Backends
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.InfoTable qualified as S
|
||||
import MiniJuvix.Syntax.ForeignBlock
|
||||
import MiniJuvix.Syntax.MiniHaskell.Language
|
||||
import MiniJuvix.Syntax.MiniHaskell.MiniHaskellResult
|
||||
import MiniJuvix.Syntax.MonoJuvix.InfoTable qualified as Mono
|
||||
import MiniJuvix.Syntax.MonoJuvix.Language qualified as Mono
|
||||
import MiniJuvix.Syntax.MonoJuvix.MonoJuvixResult qualified as Mono
|
||||
import Prettyprinter
|
||||
|
||||
-- import Base (Members)
|
||||
|
||||
entryMiniHaskell ::
|
||||
Member (Error Err) r =>
|
||||
Mono.MonoJuvixResult ->
|
||||
@ -26,18 +25,14 @@ entryMiniHaskell i = do
|
||||
return MiniHaskellResult {..}
|
||||
where
|
||||
_resultMonoJuvix = i
|
||||
goModule' m = runReader table (goModule m)
|
||||
goModule' m = runReader compileTable (goModule m)
|
||||
where
|
||||
table = Mono.buildTable m
|
||||
|
||||
translateModule :: Mono.Module -> Either Err Module
|
||||
translateModule m = run (runError (runReader table (goModule m)))
|
||||
where
|
||||
table = Mono.buildTable m
|
||||
compileTable :: Mono.CompileInfoTable
|
||||
compileTable = Mono.compileInfoTable i
|
||||
|
||||
type Err = Text
|
||||
|
||||
goModule :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.Module -> Sem r Module
|
||||
goModule :: Members '[Error Err, Reader Mono.CompileInfoTable] r => Mono.Module -> Sem r Module
|
||||
goModule Mono.Module {..} = do
|
||||
_moduleBody' <- goModuleBody _moduleBody
|
||||
return
|
||||
@ -50,13 +45,13 @@ unsupported :: Text -> a
|
||||
unsupported msg = error $ msg <> " not yet supported"
|
||||
|
||||
goModuleBody ::
|
||||
Members '[Error Err, Reader Mono.InfoTable] r =>
|
||||
Members '[Error Err, Reader Mono.CompileInfoTable] r =>
|
||||
Mono.ModuleBody ->
|
||||
Sem r ModuleBody
|
||||
goModuleBody Mono.ModuleBody {..} =
|
||||
ModuleBody <$> mapMaybeM goStatement _moduleStatements
|
||||
|
||||
goStatement :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.Statement -> Sem r (Maybe Statement)
|
||||
goStatement :: Members '[Error Err, Reader Mono.CompileInfoTable] r => Mono.Statement -> Sem r (Maybe Statement)
|
||||
goStatement = \case
|
||||
Mono.StatementInductive d -> Just . StatementInductive <$> goInductive d
|
||||
Mono.StatementFunction d -> Just . StatementFunction <$> goFunctionDef d
|
||||
@ -68,44 +63,32 @@ goForeign b = case b ^. foreignBackend of
|
||||
BackendGhc -> Just (StatementVerbatim (b ^. foreignCode))
|
||||
_ -> Nothing
|
||||
|
||||
lookupCompile ::
|
||||
Members '[Error Err, Reader Mono.InfoTable] r =>
|
||||
Mono.Name ->
|
||||
Sem r Mono.CompileInfo
|
||||
lookupCompile name =
|
||||
fromMaybe impossible . (^. Mono.infoCompilationRules . at name) <$> ask
|
||||
|
||||
lookupAxiom ::
|
||||
Members '[Error Err, Reader Mono.InfoTable] r =>
|
||||
Mono.Name ->
|
||||
Sem r Mono.AxiomInfo
|
||||
lookupAxiom n =
|
||||
fromMaybe impossible . (^. Mono.infoAxioms . at n) <$> ask
|
||||
|
||||
goIden :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.Iden -> Sem r Expression
|
||||
goIden :: Members '[Error Err, Reader Mono.CompileInfoTable] r => Mono.Iden -> Sem r Expression
|
||||
goIden = \case
|
||||
Mono.IdenFunction fun -> return (goName' fun)
|
||||
Mono.IdenConstructor c -> return (goName' c)
|
||||
Mono.IdenVar v -> return (goName' v)
|
||||
Mono.IdenAxiom a -> undefined
|
||||
Mono.IdenAxiom a -> ExpressionVerbatim <$> goAxiomIden a
|
||||
|
||||
throwErr :: Member (Error Err) r => Text -> Sem r a
|
||||
throwErr = throw
|
||||
|
||||
goCompile ::
|
||||
Members '[Error Err, Reader Mono.InfoTable] r =>
|
||||
Mono.Name ->
|
||||
Sem r Text
|
||||
goCompile name = do
|
||||
backends <- (^. Mono.compileInfoBackendItems) <$> lookupCompile name
|
||||
goAxiomIden :: Members '[Error Err, Reader Mono.CompileInfoTable] r => Mono.Name -> Sem r Text
|
||||
goAxiomIden n = do
|
||||
backends <- lookupBackends (n ^. Mono.nameId)
|
||||
case firstJust getCode backends of
|
||||
Nothing -> throwErr ("ghc does not support this primitive:" <> show (pretty name))
|
||||
Nothing -> throwErr ("ghc does not support this primitive:" <> show (pretty n))
|
||||
Just t -> return t
|
||||
where
|
||||
getCode :: BackendItem -> Maybe Text
|
||||
getCode b =
|
||||
guard (BackendGhc == b ^. backendItemBackend)
|
||||
$> b ^. backendItemCode
|
||||
lookupBackends ::
|
||||
Member (Reader Mono.CompileInfoTable) r =>
|
||||
NameId ->
|
||||
Sem r [BackendItem]
|
||||
lookupBackends f = (^. S.compileInfoBackendItems) . HashMap.lookupDefault impossible f <$> ask
|
||||
|
||||
goName' :: Mono.Name -> Expression
|
||||
goName' = ExpressionIden . goName
|
||||
@ -154,7 +137,7 @@ goNameText n =
|
||||
haskellMainName :: Text
|
||||
haskellMainName = "main"
|
||||
|
||||
goFunctionDef :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.FunctionDef -> Sem r FunctionDef
|
||||
goFunctionDef :: Members '[Error Err, Reader Mono.CompileInfoTable] r => Mono.FunctionDef -> Sem r FunctionDef
|
||||
goFunctionDef Mono.FunctionDef {..} = do
|
||||
_funDefType' <- goType _funDefType
|
||||
_funDefClauses' <- mapM goFunctionClause _funDefClauses
|
||||
@ -179,7 +162,7 @@ goConstructorApp c =
|
||||
}
|
||||
|
||||
goExpression ::
|
||||
Members '[Error Err, Reader Mono.InfoTable] r =>
|
||||
Members '[Error Err, Reader Mono.CompileInfoTable] r =>
|
||||
Mono.Expression ->
|
||||
Sem r Expression
|
||||
goExpression = \case
|
||||
@ -188,7 +171,7 @@ goExpression = \case
|
||||
Mono.ExpressionLiteral l -> return (ExpressionLiteral l)
|
||||
|
||||
goApplication ::
|
||||
Members '[Error Err, Reader Mono.InfoTable] r =>
|
||||
Members '[Error Err, Reader Mono.CompileInfoTable] r =>
|
||||
Mono.Application ->
|
||||
Sem r Application
|
||||
goApplication Mono.Application {..} = do
|
||||
@ -201,7 +184,7 @@ goApplication Mono.Application {..} = do
|
||||
}
|
||||
|
||||
goFunctionClause ::
|
||||
Members '[Error Err, Reader Mono.InfoTable] r =>
|
||||
Members '[Error Err, Reader Mono.CompileInfoTable] r =>
|
||||
Mono.FunctionClause ->
|
||||
Sem r FunctionClause
|
||||
goFunctionClause Mono.FunctionClause {..} = do
|
||||
@ -214,7 +197,7 @@ goFunctionClause Mono.FunctionClause {..} = do
|
||||
}
|
||||
|
||||
goInductive ::
|
||||
Members '[Error Err, Reader Mono.InfoTable] r =>
|
||||
Members '[Error Err, Reader Mono.CompileInfoTable] r =>
|
||||
Mono.InductiveDef ->
|
||||
Sem r InductiveDef
|
||||
goInductive Mono.InductiveDef {..} = do
|
||||
@ -226,7 +209,7 @@ goInductive Mono.InductiveDef {..} = do
|
||||
}
|
||||
|
||||
goConstructorDef ::
|
||||
Members '[Error Err, Reader Mono.InfoTable] r =>
|
||||
Members '[Error Err, Reader Mono.CompileInfoTable] r =>
|
||||
Mono.InductiveConstructorDef ->
|
||||
Sem r InductiveConstructorDef
|
||||
goConstructorDef Mono.InductiveConstructorDef {..} = do
|
||||
@ -237,7 +220,7 @@ goConstructorDef Mono.InductiveConstructorDef {..} = do
|
||||
_constructorParameters = _constructorParameters'
|
||||
}
|
||||
|
||||
goFunction :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.Function -> Sem r Function
|
||||
goFunction :: Members '[Error Err, Reader Mono.CompileInfoTable] r => Mono.Function -> Sem r Function
|
||||
goFunction Mono.Function {..} = do
|
||||
_funLeft' <- goType _funLeft
|
||||
_funRight' <- goType _funRight
|
||||
@ -247,12 +230,12 @@ goFunction Mono.Function {..} = do
|
||||
_funRight = _funRight'
|
||||
}
|
||||
|
||||
goTypeIden :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.TypeIden -> Sem r Type
|
||||
goTypeIden :: Members '[Error Err, Reader Mono.CompileInfoTable] r => Mono.TypeIden -> Sem r Type
|
||||
goTypeIden = \case
|
||||
Mono.TypeIdenInductive n -> return (TypeIden (TypeIdenInductive (goName n)))
|
||||
Mono.TypeIdenAxiom _ -> undefined -- TypeVerbatim <$> goAxiomIden n
|
||||
Mono.TypeIdenAxiom n -> TypeVerbatim <$> goAxiomIden n
|
||||
|
||||
goType :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.Type -> Sem r Type
|
||||
goType :: Members '[Error Err, Reader Mono.CompileInfoTable] r => Mono.Type -> Sem r Type
|
||||
goType = \case
|
||||
Mono.TypeIden t -> goTypeIden t
|
||||
Mono.TypeFunction f -> TypeFunction <$> goFunction f
|
||||
|
||||
7
test/BackendC.hs
Normal file
7
test/BackendC.hs
Normal file
@ -0,0 +1,7 @@
|
||||
module BackendC where
|
||||
|
||||
import BackendC.Positive qualified as P
|
||||
import Base
|
||||
|
||||
allTests :: TestTree
|
||||
allTests = testGroup "Backend C tests" [P.allTests]
|
||||
66
test/BackendC/Positive.hs
Normal file
66
test/BackendC/Positive.hs
Normal file
@ -0,0 +1,66 @@
|
||||
module BackendC.Positive where
|
||||
|
||||
import Base
|
||||
import Data.Text.IO qualified as TIO
|
||||
import MiniJuvix.Pipeline
|
||||
import MiniJuvix.Translation.MonoJuvixToMiniC as MiniC
|
||||
import System.IO.Extra (withTempDir)
|
||||
import System.Process qualified as P
|
||||
|
||||
data PosTest = PosTest
|
||||
{ _name :: String,
|
||||
_relDir :: FilePath
|
||||
}
|
||||
|
||||
makeLenses ''PosTest
|
||||
|
||||
root :: FilePath
|
||||
root = "tests/positive/MiniC"
|
||||
|
||||
mainFile :: FilePath
|
||||
mainFile = "Input.mjuvix"
|
||||
|
||||
testDescr :: PosTest -> TestDescr
|
||||
testDescr PosTest {..} =
|
||||
let tRoot = root </> _relDir
|
||||
in TestDescr
|
||||
{ _testName = _name,
|
||||
_testRoot = tRoot,
|
||||
_testAssertion = Steps $ \step -> do
|
||||
step "Check emscripten and wasmer are on path"
|
||||
assertCmdExists "emcc"
|
||||
assertCmdExists "wasmer"
|
||||
|
||||
step "C Generation"
|
||||
let entryPoint = EntryPoint "." (return "Input.mjuvix")
|
||||
p :: MiniC.MiniCResult <- runIO (upToMiniC entryPoint)
|
||||
|
||||
actual <-
|
||||
withTempDir
|
||||
( \dirPath -> do
|
||||
let cOutputFile = dirPath </> "out.c"
|
||||
wasmOutputFile = dirPath </> "out.wasm"
|
||||
TIO.writeFile cOutputFile (p ^. MiniC.resultCCode)
|
||||
step "WASM generation"
|
||||
P.callProcess "emcc" ["-o", wasmOutputFile, cOutputFile]
|
||||
step "WASM execution"
|
||||
pack <$> P.readProcess "wasmer" [wasmOutputFile] ""
|
||||
)
|
||||
|
||||
expected <- TIO.readFile "expected.golden"
|
||||
step "Compare expected and actual program output"
|
||||
assertEqDiff "check: WASM output = expected.golden" actual expected
|
||||
}
|
||||
|
||||
allTests :: TestTree
|
||||
allTests =
|
||||
testGroup
|
||||
"Backend C positive tests"
|
||||
(map (mkTest . testDescr) tests)
|
||||
|
||||
tests :: [PosTest]
|
||||
tests =
|
||||
[ PosTest "HelloWorld" "HelloWorld",
|
||||
PosTest "Inductive types and pattern matching" "Nat",
|
||||
PosTest "Polymorphic types" "Polymorphism"
|
||||
]
|
||||
17
test/Base.hs
17
test/Base.hs
@ -6,9 +6,12 @@ module Base
|
||||
)
|
||||
where
|
||||
|
||||
import Data.Algorithm.Diff
|
||||
import Data.Algorithm.DiffOutput
|
||||
import MiniJuvix.Prelude
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
import Text.Show.Pretty hiding (Html)
|
||||
|
||||
data AssertionDescr
|
||||
= Single Assertion
|
||||
@ -27,3 +30,17 @@ mkTest :: TestDescr -> TestTree
|
||||
mkTest TestDescr {..} = case _testAssertion of
|
||||
Single assertion -> testCase _testName $ withCurrentDirectory _testRoot assertion
|
||||
Steps steps -> testCaseSteps _testName (withCurrentDirectory _testRoot . steps)
|
||||
|
||||
assertEqDiff :: (Eq a, Show a) => String -> a -> a -> Assertion
|
||||
assertEqDiff msg a b
|
||||
| a == b = return ()
|
||||
| otherwise = do
|
||||
putStrLn (pack $ ppDiff (getGroupedDiff pa pb))
|
||||
putStrLn "End diff"
|
||||
fail msg
|
||||
where
|
||||
pa = lines $ ppShow a
|
||||
pb = lines $ ppShow b
|
||||
|
||||
assertCmdExists :: FilePath -> Assertion
|
||||
assertCmdExists cmd = assertBool ("Command: " <> cmd <> " is not present on $PATH") . isJust =<< findExecutable cmd
|
||||
|
||||
16
test/Main.hs
16
test/Main.hs
@ -1,18 +1,26 @@
|
||||
module Main (main) where
|
||||
|
||||
import BackendC qualified
|
||||
import Base
|
||||
import MonoJuvix qualified
|
||||
import Scope qualified
|
||||
import TypeCheck qualified
|
||||
|
||||
allTests :: TestTree
|
||||
allTests =
|
||||
slowTests :: TestTree
|
||||
slowTests =
|
||||
testGroup
|
||||
"MiniJuvix tests"
|
||||
"MiniJuvix slow tests"
|
||||
[BackendC.allTests]
|
||||
|
||||
fastTests :: TestTree
|
||||
fastTests =
|
||||
testGroup
|
||||
"MiniJuvix fast tests"
|
||||
[ Scope.allTests,
|
||||
TypeCheck.allTests,
|
||||
MonoJuvix.allTests
|
||||
]
|
||||
|
||||
main :: IO ()
|
||||
main = defaultMain allTests
|
||||
main = do
|
||||
defaultMain (testGroup "MiniJuvix tests" [fastTests, slowTests])
|
||||
|
||||
@ -1,8 +1,6 @@
|
||||
module Scope.Positive where
|
||||
|
||||
import Base
|
||||
import Data.Algorithm.Diff
|
||||
import Data.Algorithm.DiffOutput
|
||||
import Data.HashMap.Strict qualified as HashMap
|
||||
import MiniJuvix.Internal.NameIdGen
|
||||
import MiniJuvix.Pipeline
|
||||
@ -10,7 +8,6 @@ import MiniJuvix.Syntax.Concrete.Parser qualified as Parser
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Text qualified as M
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Utils
|
||||
import Text.Show.Pretty hiding (Html)
|
||||
|
||||
data PosTest = PosTest
|
||||
{ _name :: String,
|
||||
@ -76,17 +73,6 @@ testDescr PosTest {..} =
|
||||
assertEqDiff "check: parse . pretty . parse = parse" pmodules parsedPrettyModules
|
||||
}
|
||||
|
||||
assertEqDiff :: (Eq a, Show a) => String -> a -> a -> Assertion
|
||||
assertEqDiff msg a b
|
||||
| a == b = return ()
|
||||
| otherwise = do
|
||||
putStrLn (pack $ ppDiff (getGroupedDiff pa pb))
|
||||
putStrLn "End diff"
|
||||
fail msg
|
||||
where
|
||||
pa = lines $ ppShow a
|
||||
pb = lines $ ppShow b
|
||||
|
||||
allTests :: TestTree
|
||||
allTests =
|
||||
testGroup
|
||||
|
||||
1
tests/.gitattributes
vendored
Normal file
1
tests/.gitattributes
vendored
Normal file
@ -0,0 +1 @@
|
||||
*.golden -text
|
||||
@ -24,4 +24,14 @@ foreign ghc {
|
||||
import Foo.Baz
|
||||
};
|
||||
|
||||
foreign ghc {
|
||||
data Foo = Foo { _unFoo :: Int \} -- \\ test
|
||||
};
|
||||
|
||||
foreign ghc {
|
||||
data Foo = Foo {
|
||||
_unFoo :: Int
|
||||
\}
|
||||
};
|
||||
|
||||
end;
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
module HelloWorld;
|
||||
|
||||
-- the foreign keyword has two arguments:
|
||||
-- 1. The name of the backend. Only ghc is available now.
|
||||
-- 1. The name of the backend.
|
||||
-- 2. A string. For ease of use, the string is given between braces
|
||||
-- and can have multiple lines. Space at the beginning and at the end is ignored.
|
||||
-- The given code is inlined verbatim when compiling to the given backend.
|
||||
@ -9,26 +9,37 @@ module HelloWorld;
|
||||
foreign ghc {
|
||||
|
||||
import Data.Text
|
||||
import Data.Text.IO
|
||||
|
||||
};
|
||||
|
||||
foreign c {
|
||||
|
||||
#include <stdio.h>
|
||||
|
||||
};
|
||||
|
||||
axiom Action : Type;
|
||||
|
||||
compile Action {
|
||||
ghc ↦ "IO ()";
|
||||
c ↦ "int";
|
||||
};
|
||||
|
||||
axiom String : Type;
|
||||
axiom putStr : String -> Action;
|
||||
|
||||
-- the compile keyword has three arguments:
|
||||
-- 1. The name of the MiniJuvix Axiom.
|
||||
-- 2. The name of the backend.
|
||||
-- 3. The thing we should inline when compiling this
|
||||
-- axiom to the given backend.
|
||||
compile String {
|
||||
ghc ↦ "[Char]";
|
||||
c ↦ "char*";
|
||||
};
|
||||
|
||||
axiom putStrLn : String -> Action;
|
||||
|
||||
-- main : Action;
|
||||
-- main := putStr "hello world";
|
||||
compile putStrLn {
|
||||
ghc ↦ "putStrLn";
|
||||
c ↦ "puts";
|
||||
};
|
||||
|
||||
main : Action;
|
||||
main := putStrLn "hello world";
|
||||
|
||||
end;
|
||||
|
||||
29
tests/positive/MiniC/HelloWorld/Input.mjuvix
Normal file
29
tests/positive/MiniC/HelloWorld/Input.mjuvix
Normal file
@ -0,0 +1,29 @@
|
||||
module Input;
|
||||
|
||||
foreign c {
|
||||
#include <stdio.h>
|
||||
};
|
||||
|
||||
axiom String : Type;
|
||||
|
||||
compile String {
|
||||
c ↦ "char*";
|
||||
};
|
||||
|
||||
axiom Action : Type;
|
||||
|
||||
compile Action {
|
||||
c ↦ "int";
|
||||
};
|
||||
|
||||
axiom put-str-ln : String → Action;
|
||||
|
||||
compile put-str-ln {
|
||||
ghc ↦ "putStrLn";
|
||||
c ↦ "puts";
|
||||
};
|
||||
|
||||
main : Action;
|
||||
main ≔ put-str-ln "hello world!";
|
||||
|
||||
end;
|
||||
1
tests/positive/MiniC/HelloWorld/expected.golden
Normal file
1
tests/positive/MiniC/HelloWorld/expected.golden
Normal file
@ -0,0 +1 @@
|
||||
hello world!
|
||||
185
tests/positive/MiniC/Nat/Input.mjuvix
Normal file
185
tests/positive/MiniC/Nat/Input.mjuvix
Normal file
@ -0,0 +1,185 @@
|
||||
module Input;
|
||||
|
||||
foreign c {
|
||||
#include <stdio.h>
|
||||
};
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Booleans
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
inductive Bool {
|
||||
true : Bool;
|
||||
false : Bool;
|
||||
};
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Strings
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
axiom String : Type;
|
||||
|
||||
compile String {
|
||||
ghc ↦ "[Char]";
|
||||
c ↦ "char*";
|
||||
};
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- IO
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
axiom Action : Type;
|
||||
|
||||
compile Action {
|
||||
ghc ↦ "IO ()";
|
||||
c ↦ "int";
|
||||
};
|
||||
|
||||
foreign c {
|
||||
int sequence(int a, int b) {
|
||||
return a + b;
|
||||
\}
|
||||
|
||||
int putStr(char* s) {
|
||||
return fputs(s, stdout);
|
||||
\}
|
||||
};
|
||||
|
||||
infixl 1 >>;
|
||||
axiom >> : Action → Action → Action;
|
||||
|
||||
compile >> {
|
||||
ghc ↦ "(>>)";
|
||||
c ↦ "sequence";
|
||||
};
|
||||
|
||||
axiom put-str : String → Action;
|
||||
|
||||
compile put-str {
|
||||
ghc ↦ "putStr";
|
||||
c ↦ "putStr";
|
||||
};
|
||||
|
||||
axiom put-str-ln : String → Action;
|
||||
|
||||
compile put-str-ln {
|
||||
ghc ↦ "putStrLn";
|
||||
c ↦ "puts";
|
||||
};
|
||||
|
||||
bool-to-str : Bool → String;
|
||||
bool-to-str true ≔ "True";
|
||||
bool-to-str false ≔ "False";
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Integers
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
axiom Int : Type;
|
||||
|
||||
compile Int {
|
||||
ghc ↦ "Int";
|
||||
c ↦ "int";
|
||||
};
|
||||
|
||||
foreign c {
|
||||
int plus(int l, int r) {
|
||||
return l + r;
|
||||
\}
|
||||
|
||||
char* intToStr(int i) {
|
||||
int length = snprintf(NULL, 0, "%d", i);
|
||||
char* str = malloc(length + 1);
|
||||
snprintf(str, length + 1, "%d", i);
|
||||
return str;
|
||||
\}
|
||||
};
|
||||
|
||||
infixl 6 +int;
|
||||
axiom +int : Int -> Int -> Int;
|
||||
|
||||
compile +int {
|
||||
ghc ↦ "(+)";
|
||||
c ↦ "plus";
|
||||
};
|
||||
|
||||
axiom to-str : Int → String;
|
||||
|
||||
compile to-str {
|
||||
ghc ↦ "show";
|
||||
c ↦ "intToStr";
|
||||
};
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Natural Numbers
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
inductive Nat {
|
||||
zero : Nat;
|
||||
suc : Nat → Nat
|
||||
};
|
||||
|
||||
infixl 6 +;
|
||||
+ : Nat → Nat → Nat;
|
||||
+ zero n ≔ n;
|
||||
+ (suc m) n ≔ suc (m + n);
|
||||
|
||||
is-even : Nat → Bool;
|
||||
is-even zero ≔ true;
|
||||
is-even (suc (suc n)) ≔ is-even n;
|
||||
is-even _ ≔ false;
|
||||
|
||||
infix 4 ==Nat;
|
||||
==Nat : Nat → Nat → Bool;
|
||||
==Nat zero zero ≔ true;
|
||||
==Nat (suc n) (suc m) ≔ n ==Nat m;
|
||||
==Nat _ _ ≔ false;
|
||||
|
||||
to-int : Nat → Int;
|
||||
to-int zero ≔ 0;
|
||||
to-int (suc n) ≔ 1 +int (to-int n);
|
||||
|
||||
nat-to-str : Nat → String;
|
||||
nat-to-str n ≔ to-str (to-int n);
|
||||
|
||||
one : Nat;
|
||||
one ≔ suc zero;
|
||||
|
||||
two : Nat;
|
||||
two ≔ suc one;
|
||||
|
||||
three : Nat;
|
||||
three ≔ suc two;
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Main
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
three-plus-suc-one : Action;
|
||||
three-plus-suc-one ≔ (put-str "3 + (1 + 1) = ")
|
||||
>> put-str-ln (nat-to-str (three + (suc one)));
|
||||
|
||||
three-eq-suc-two : Action;
|
||||
three-eq-suc-two ≔ (put-str "3 == 1 + 2 : ")
|
||||
>> put-str-ln (bool-to-str (three ==Nat (one + two)));
|
||||
|
||||
three-neq-two : Action;
|
||||
three-neq-two ≔ (put-str "3 == 2 : ")
|
||||
>> put-str-ln (bool-to-str (three ==Nat two));
|
||||
|
||||
three-is-not-even : Action;
|
||||
three-is-not-even ≔ (put-str "is-even 3 : ")
|
||||
>> put-str-ln (bool-to-str (is-even three));
|
||||
|
||||
four-is-even : Action;
|
||||
four-is-even ≔ (put-str "is-even 4 : ")
|
||||
>> put-str-ln (bool-to-str (is-even (suc three)));
|
||||
|
||||
main : Action;
|
||||
main ≔ three-plus-suc-one
|
||||
>> three-eq-suc-two
|
||||
>> three-neq-two
|
||||
>> three-is-not-even
|
||||
>> four-is-even
|
||||
|
||||
end;
|
||||
5
tests/positive/MiniC/Nat/expected.golden
Normal file
5
tests/positive/MiniC/Nat/expected.golden
Normal file
@ -0,0 +1,5 @@
|
||||
3 + (1 + 1) = 5
|
||||
3 == 1 + 2 : True
|
||||
3 == 2 : False
|
||||
is-even 3 : False
|
||||
is-even 4 : True
|
||||
97
tests/positive/MiniC/Polymorphism/Input.mjuvix
Normal file
97
tests/positive/MiniC/Polymorphism/Input.mjuvix
Normal file
@ -0,0 +1,97 @@
|
||||
module Input;
|
||||
|
||||
foreign c {
|
||||
#include <stdio.h>
|
||||
};
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Booleans
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
inductive Bool {
|
||||
true : Bool;
|
||||
false : Bool;
|
||||
};
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Strings
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
axiom String : Type;
|
||||
|
||||
compile String {
|
||||
ghc ↦ "[Char]";
|
||||
c ↦ "char*";
|
||||
};
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- IO
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
axiom Action : Type;
|
||||
|
||||
compile Action {
|
||||
ghc ↦ "IO ()";
|
||||
c ↦ "int";
|
||||
};
|
||||
|
||||
foreign c {
|
||||
int sequence(int a, int b) {
|
||||
return a + b;
|
||||
\}
|
||||
|
||||
int putStr(char* s) {
|
||||
return fputs(s, stdout);
|
||||
\}
|
||||
};
|
||||
|
||||
infixl 1 >>;
|
||||
axiom >> : Action → Action → Action;
|
||||
|
||||
compile >> {
|
||||
ghc ↦ "(>>)";
|
||||
c ↦ "sequence";
|
||||
};
|
||||
|
||||
axiom put-str : String → Action;
|
||||
|
||||
compile put-str {
|
||||
ghc ↦ "putStr";
|
||||
c ↦ "putStr";
|
||||
};
|
||||
|
||||
axiom put-str-ln : String → Action;
|
||||
|
||||
compile put-str-ln {
|
||||
ghc ↦ "putStrLn";
|
||||
c ↦ "puts";
|
||||
};
|
||||
|
||||
bool-to-str : Bool → String;
|
||||
bool-to-str true ≔ "True";
|
||||
bool-to-str false ≔ "False";
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Pair
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
inductive Pair (A : Type) (B : Type) {
|
||||
mkPair : A → B → Pair A B;
|
||||
};
|
||||
|
||||
fst : (A : Type) → (B : Type) → Pair A B → A;
|
||||
fst _ _ (mkPair a b) ≔ a;
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Main
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
fst-of-pair : Action;
|
||||
fst-of-pair ≔ (put-str "fst (True, False) = ")
|
||||
>> put-str-ln (bool-to-str (fst Bool Bool (mkPair Bool Bool true false)));
|
||||
|
||||
main : Action;
|
||||
main ≔ fst-of-pair;
|
||||
|
||||
end;
|
||||
1
tests/positive/MiniC/Polymorphism/expected.golden
Normal file
1
tests/positive/MiniC/Polymorphism/expected.golden
Normal file
@ -0,0 +1 @@
|
||||
fst (True, False) = True
|
||||
Loading…
Reference in New Issue
Block a user