anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2025-01-06 06:53:33 +03:00
Code Issues Projects Releases Wiki Activity

Translate function bodies to Isabelle/HOL (#2868)

Browse Source 
* Closes #2813 

Implements a translation from Juvix functions to Isabelle/HOL functions.
This extends the previous Juvix -> Isabelle translation which could
handle only type signatures.

Checklist
---------

- [x] Basic translation
- [x] Polymorphism
- [x] Arithmetic operators
- [x] Numeric literals
- [x] List literals
- [x] Comparison operators
- [x] Boolean operators
- [x] `if` translated to Isabelle `if`
- [x] `true` and `false` translated to Isabelle `True` and `False`
- [x] `zero` and `suc` translated to Isabelle `0` and `Suc`
- [x] `Maybe` translated to Isabelle `option`
- [x] Pairs translated to Isabelle tuples
- [x] Quote Isabelle identifier names (e.g. cannot begin with `_`)
- [x] Rename variables to avoid clashes (in Isabelle/HOL pattern
variables don't shadow function identifiers)
- [x] Common stdlib functions (`map`, `filter`, etc) translated to
corresponding Isabelle functions
- [x] Multiple assignments in a single `let`
- [x] CLI
- [x] Test
- The test is very fragile, similar to the markdown test. It just
compares the result of translation to Isabelle against a predefined
expected output file.

Limitations
-----------

The translation is not designed to be completely correct under all
circumstances. There are aspects of the Juvix language that cannot be
straightforwardly translated to Isabelle/HOL, and these are not planned
to ever be properly handled. There are other aspects that are difficult
but not impossible to translate, and these are left for future work.
Occasionally, the generated code may need manual adjustments to
type-check in Isabelle/HOL.

In particular:
* Higher-rank polymorphism or functions on types cannot be translated as
these features are not supported by Isabelle/HOL. Juvix programs using
these features will not be correctly translated (the generated output
may need manual adjustment).
* In cases where Juvix termination checking diverges from Isabelle/HOL
termination checking, providing a termination proof manually may be
necessary. Non-terminating Juvix functions cannot be automatically
translated and need to be manually modelled in Isabelle/HOL in a
different way (e.g. as relations).
* Comments (including judoc) are ignored. This is left for future work.
* Traits are not translated to Isabelle/HOL type classes / locales. This
is left for future work.
* Mutually recursive functions are not correctly translated. This is
left for future work.
* Record creation, update, field access and pattern matching are not
correctly translated. This is left for future work.
* Named patterns are not correctly translated. This is left for future
work.
* Side conditions in patterns are not supported. This is left for future
work.
* If a Juvix function in the translated module has the same name as some
function from the Isabelle/HOL standard library, there will be a name
clash in the generated code.

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
This commit is contained in:
Łukasz Czajka 2024-07-19 09:40:07 +02:00 committed by GitHub
parent 2793514325
commit 83837b9c5f
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
32 changed files with 1508 additions and 95 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
app/Commands/Isabelle/Options.hs
View File

@ -19,18 +19,18 @@ parseIsabelle = do
parseGenericOutputDir
( value "isabelle"
<> showDefault
<> help "Isabelle/HOL output directory."
<> help "Isabelle/HOL output directory"
<> action "directory"
)
_isabelleStdout <-
switch
( long "stdout"
<> help "Write the output to stdout instead of a file."
<> help "Write the output to stdout instead of a file"
)
_isabelleOnlyTypes <-
switch
( long "only-types"
<> help "Translate types only. Omit function signatures."
<> help "Translate types only"
)
_isabelleInputFile <- optional (parseInputFile FileExtJuvix)
pure IsabelleOptions {..}

4
app/TopCommand/Options.hs
View File

@ -201,14 +201,14 @@ commandIsabelle =
command "isabelle" $
info
(Isabelle <$> parseIsabelle)
(progDesc "Generate Isabelle/HOL types for a Juvix file")
(progDesc "Translate a Juvix file to Isabelle/HOL")
commandDev :: Mod CommandFields TopCommand
commandDev =
command "dev" $
info
(Dev <$> Dev.parseDevCommand)
(progDesc "Commands for the developers")
(progDesc "Commands for the Juvix compiler developers")
parseCompilerCommand :: Parser TopCommand
parseCompilerCommand =

2
include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix
View File

@ -7,8 +7,10 @@ trait
type Natural A :=
mkNatural {
syntax operator + additive;
{-# isabelle-operator: {name: "+", prec: 65, assoc: left} #-}
+ : A -> A -> A;
syntax operator * multiplicative;
{-# isabelle-operator: {name: "*", prec: 70, assoc: left} #-}
* : A -> A -> A;
builtin from-nat
fromNat : Nat -> A

2
juvix-stdlib

@ -1 +1 @@
Subproject commit 17f22fcec5d78be511ea59984aee3499da5f3342
Subproject commit 61bc0778e53f4e6e13d929072179a855ea9ad9d2

8
src/Juvix/Compiler/Backend/Isabelle/Extra.hs Normal file
View File

@ -0,0 +1,8 @@
module Juvix.Compiler.Backend.Isabelle.Extra where
import Juvix.Compiler.Backend.Isabelle.Language
mkApp :: Expression -> [Expression] -> Expression
mkApp fn = \case
[] -> fn
arg : args -> mkApp (ExprApp (Application fn arg)) args

212
src/Juvix/Compiler/Backend/Isabelle/Language.hs
View File

@ -5,17 +5,17 @@ module Juvix.Compiler.Backend.Isabelle.Language
)
where
import Juvix.Compiler.Internal.Data.Name
import Juvix.Prelude
import Juvix.Compiler.Internal.Data.Name hiding (letFixity)
import Juvix.Prelude hiding (Cons, letFixity)
data Type
= TyVar Var
= TyVar TypeVar
| TyFun FunType
| TyInd IndApp
deriving stock (Eq)
data Var = Var
{ _varName :: Name
data TypeVar = TypeVar
{ _typeVarName :: Name
}
deriving stock (Eq)
@ -31,6 +31,8 @@ data Inductive
| IndInt
| IndList
| IndString
| IndOption
| IndTuple
| IndUser Name
deriving stock (Eq)
@ -40,10 +42,108 @@ data IndApp = IndApp
}
deriving stock (Eq)
makeLenses ''Var
makeLenses ''TypeVar
makeLenses ''FunType
makeLenses ''IndApp
data Expression
= ExprIden Name
| ExprUndefined
| ExprLiteral Literal
| ExprApp Application
| ExprBinop Binop
| ExprTuple (Tuple Expression)
| ExprList (List Expression)
| ExprCons (Cons Expression)
| ExprLet Let
| ExprIf If
| ExprCase Case
| ExprLambda Lambda
data Literal
= LitNumeric Integer
| LitString Text
data Application = Application
{ _appLeft :: Expression,
_appRight :: Expression
}
data Binop = Binop
{ _binopOperator :: Name,
_binopLeft :: Expression,
_binopRight :: Expression,
_binopFixity :: Fixity
}
data Let = Let
{ _letClauses :: NonEmpty LetClause,
_letBody :: Expression
}
data LetClause = LetClause
{ _letClauseName :: Name,
_letClauseValue :: Expression
}
data If = If
{ _ifValue :: Expression,
_ifBranchTrue :: Expression,
_ifBranchFalse :: Expression
}
data Case = Case
{ _caseValue :: Expression,
_caseBranches :: NonEmpty CaseBranch
}
data CaseBranch = CaseBranch
{ _caseBranchPattern :: Pattern,
_caseBranchBody :: Expression
}
data Lambda = Lambda
{ _lambdaVar :: Name,
_lambdaType :: Maybe Type,
_lambdaBody :: Expression
}
data Pattern
= PatVar Name
| PatZero
| PatConstrApp ConstrApp
| PatTuple (Tuple Pattern)
| PatList (List Pattern)
| PatCons (Cons Pattern)
newtype Tuple a = Tuple
{ _tupleComponents :: NonEmpty a
}
newtype List a = List
{ _listElements :: [a]
}
data Cons a = Cons
{ _consHead :: a,
_consTail :: a
}
data ConstrApp = ConstrApp
{ _constrAppConstructor :: Name,
_constrAppArgs :: [Pattern]
}
makeLenses ''Application
makeLenses ''Let
makeLenses ''LetClause
makeLenses ''If
makeLenses ''Case
makeLenses ''CaseBranch
makeLenses ''Lambda
makeLenses ''ConstrApp
makeLenses ''Expression
data Statement
= StmtDefinition Definition
| StmtFunction Function
@ -53,12 +153,19 @@ data Statement
data Definition = Definition
{ _definitionName :: Name,
_definitionType :: Type
_definitionType :: Type,
_definitionBody :: Expression
}
data Function = Function
{ _functionName :: Name,
_functionType :: Type
_functionType :: Type,
_functionClauses :: NonEmpty Clause
}
data Clause = Clause
{ _clausePatterns :: NonEmpty Pattern,
_clauseBody :: Expression
}
data Synonym = Synonym
@ -68,7 +175,7 @@ data Synonym = Synonym
data Datatype = Datatype
{ _datatypeName :: Name,
_datatypeParams :: [Var],
_datatypeParams :: [TypeVar],
_datatypeConstructors :: [Constructor]
}
@ -79,7 +186,7 @@ data Constructor = Constructor
data Record = Record
{ _recordName :: Name,
_recordParams :: [Var],
_recordParams :: [TypeVar],
_recordFields :: [RecordField]
}
@ -95,6 +202,7 @@ makeLenses ''Datatype
makeLenses ''Constructor
makeLenses ''Record
makeLenses ''RecordField
makeLenses ''Tuple
data Theory = Theory
{ _theoryName :: Name,
@ -104,7 +212,63 @@ data Theory = Theory
makeLenses ''Theory
instance HasAtomicity Var where
caseFixity :: Fixity
caseFixity =
Fixity
{ _fixityPrecedence = PrecNat 0,
_fixityArity = OpBinary AssocLeft,
_fixityId = Nothing
}
lambdaFixity :: Fixity
lambdaFixity =
Fixity
{ _fixityPrecedence = PrecNat 0,
_fixityArity = OpUnary AssocPostfix,
_fixityId = Nothing
}
ifFixity :: Fixity
ifFixity =
Fixity
{ _fixityPrecedence = PrecNat 1,
_fixityArity = OpBinary AssocRight,
_fixityId = Nothing
}
letFixity :: Fixity
letFixity =
Fixity
{ _fixityPrecedence = PrecNat 2,
_fixityArity = OpBinary AssocRight,
_fixityId = Nothing
}
consFixity :: Fixity
consFixity =
Fixity
{ _fixityPrecedence = PrecNat 80,
_fixityArity = OpBinary AssocRight,
_fixityId = Nothing
}
andFixity :: Fixity
andFixity =
Fixity
{ _fixityPrecedence = PrecNat 35,
_fixityArity = OpBinary AssocRight,
_fixityId = Nothing
}
orFixity :: Fixity
orFixity =
Fixity
{ _fixityPrecedence = PrecNat 30,
_fixityArity = OpBinary AssocRight,
_fixityId = Nothing
}
instance HasAtomicity TypeVar where
atomicity _ = Atom
instance HasAtomicity Type where
@ -114,3 +278,29 @@ instance HasAtomicity Type where
TyInd IndApp {..}
| null _indAppParams -> Atom
| otherwise -> Aggregate appFixity
instance HasAtomicity Expression where
atomicity = \case
ExprIden {} -> Atom
ExprUndefined -> Atom
ExprLiteral {} -> Atom
ExprApp {} -> Aggregate appFixity
ExprBinop Binop {..} -> Aggregate _binopFixity
ExprTuple {} -> Atom
ExprList {} -> Atom
ExprCons {} -> Aggregate consFixity
ExprLet {} -> Aggregate letFixity
ExprIf {} -> Aggregate ifFixity
ExprCase {} -> Aggregate caseFixity
ExprLambda {} -> Aggregate lambdaFixity
instance HasAtomicity Pattern where
atomicity = \case
PatVar {} -> Atom
PatZero -> Atom
PatConstrApp ConstrApp {..}
| null _constrAppArgs -> Atom
| otherwise -> Aggregate appFixity
PatTuple {} -> Atom
PatList {} -> Atom
PatCons {} -> Aggregate consFixity

157
src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
View File

@ -1,5 +1,6 @@
module Juvix.Compiler.Backend.Isabelle.Pretty.Base where
import Data.Text qualified as Text
import Juvix.Compiler.Backend.Isabelle.Language
import Juvix.Compiler.Backend.Isabelle.Pretty.Keywords
import Juvix.Compiler.Backend.Isabelle.Pretty.Options
@ -19,6 +20,9 @@ ppCodeQuoted c
| atomicity c == Atom = ppCode c
| otherwise = dquotes <$> ppCode c
ppTopCode :: (HasAtomicity c, PrettyCode c, Member (Reader Options) r) => c -> Sem r (Doc Ann)
ppTopCode c = parensIf (not (isAtomic c)) <$> ppCode c
ppParams :: (HasAtomicity c, PrettyCode c, Member (Reader Options) r) => [c] -> Sem r (Maybe (Doc Ann))
ppParams = \case
[] -> return Nothing
@ -36,9 +40,9 @@ instance PrettyCode Type where
TyFun x -> ppCode x
TyInd x -> ppCode x
instance PrettyCode Var where
ppCode Var {..} =
(squote <>) <$> ppCode _varName
instance PrettyCode TypeVar where
ppCode TypeVar {..} =
(squote <>) <$> ppCode _typeVarName
instance PrettyCode FunType where
ppCode FunType {..} = do
@ -53,13 +57,128 @@ instance PrettyCode Inductive where
IndInt -> return $ primitive "int"
IndList -> return $ primitive "list"
IndString -> return $ primitive "string"
IndOption -> return $ primitive "option"
IndTuple -> return $ primitive "×"
IndUser name -> ppCode name
instance PrettyCode IndApp where
ppCode IndApp {..} = do
params <- ppParams _indAppParams
ind <- ppCode _indAppInductive
return $ params <?+> ind
ppCode IndApp {..}
| _indAppInductive == IndTuple = do
ps <- mapM ppCode _indAppParams
ind <- ppCode _indAppInductive
return $ hsep $ punctuate (space <> ind) ps
| otherwise = do
params <- ppParams _indAppParams
ind <- ppCode _indAppInductive
return $ params <?+> ind
instance PrettyCode Expression where
ppCode = \case
ExprIden x -> ppCode x
ExprUndefined -> return kwUndefined
ExprLiteral x -> ppCode x
ExprApp x -> ppCode x
ExprBinop x -> ppCode x
ExprTuple x -> ppCode x
ExprList x -> ppCode x
ExprCons x -> ppCode x
ExprLet x -> ppCode x
ExprIf x -> ppCode x
ExprCase x -> ppCode x
ExprLambda x -> ppCode x
instance PrettyCode Literal where
ppCode = \case
LitNumeric x -> return $ annotate AnnLiteralInteger (pretty x)
LitString x -> return $ annotate AnnLiteralString $ squotes $ squotes $ pretty x
instance PrettyCode Application where
ppCode Application {..} = do
l <- ppLeftExpression appFixity _appLeft
r <- ppRightExpression appFixity _appRight
return $ l <+> r
instance PrettyCode Binop where
ppCode Binop {..} = do
op <- ppCode _binopOperator
l <- ppLeftExpression _binopFixity _binopLeft
r <- ppRightExpression _binopFixity _binopRight
return $ l <+> op <+> r
instance PrettyCode LetClause where
ppCode LetClause {..} = do
name <- ppCode _letClauseName
val <- ppCode _letClauseValue
return $ name <+> "=" <+> align val
instance PrettyCode Let where
ppCode Let {..} = do
cls <- mapM ppCode _letClauses
body <- ppCode _letBody
return $ align $ kwLet <> blockIndent (vsep (punctuate semi (toList cls))) <> kwIn <+> body
instance PrettyCode If where
ppCode If {..} = do
val <- ppCode _ifValue
br1 <- ppCode _ifBranchTrue
br2 <- ppCode _ifBranchFalse
return $ align $ kwIf <> oneLineOrNextBlock val <> kwThen <> oneLineOrNextBlock br1 <> kwElse <> oneLineOrNext br2
instance PrettyCode Case where
ppCode Case {..} = do
val <- ppCode _caseValue
brs <- toList <$> mapM ppCode _caseBranches
let brs' = punctuate (space <> kwPipe) brs
return $ align $ kwCase <> oneLineOrNextBlock val <> kwOf <> hardline <> indent' (vsepHard brs')
instance PrettyCode CaseBranch where
ppCode CaseBranch {..} = do
pat <- ppTopCode _caseBranchPattern
body <- ppRightExpression caseFixity _caseBranchBody
return $ pat <+> arrow <> oneLineOrNext body
instance (PrettyCode a) => PrettyCode (Tuple a) where
ppCode Tuple {..} = do
elems <- mapM ppCode _tupleComponents
return $ parens $ hsep (punctuate comma (toList elems))
instance (PrettyCode a) => PrettyCode (List a) where
ppCode List {..} = do
elems <- mapM ppCode _listElements
return $ brackets $ hsep (punctuate comma (toList elems))
instance (PrettyCode a, HasAtomicity a) => PrettyCode (Cons a) where
ppCode Cons {..} = do
h <- ppLeftExpression consFixity _consHead
t <- ppRightExpression consFixity _consTail
return $ h <+> "#" <+> t
instance PrettyCode Pattern where
ppCode = \case
PatVar x -> ppCode x
PatZero -> return $ annotate AnnLiteralInteger (pretty (0 :: Int))
PatConstrApp x -> ppCode x
PatTuple x -> ppCode x
PatList x -> ppCode x
PatCons x -> ppCode x
instance PrettyCode ConstrApp where
ppCode ConstrApp {..} = do
args <- mapM ppCode _constrAppArgs
name <- ppCode _constrAppConstructor
if
| null args ->
return name
| otherwise ->
return $ name <+> hsep args
instance PrettyCode Lambda where
ppCode Lambda {..} = do
name <- ppCode _lambdaVar
mty <- maybe (return Nothing) (ppCode >=> return . Just) _lambdaType
body <- ppCode _lambdaBody
let ty = fmap (\t -> colon <> colon <+> t) mty
return $ kwLambda <+> name <+?> ty <+> dot <+> body
instance PrettyCode Statement where
ppCode = \case
@ -73,26 +192,35 @@ instance PrettyCode Definition where
ppCode Definition {..} = do
n <- ppCode _definitionName
ty <- ppCodeQuoted _definitionType
return $ kwDefinition <+> n <+> "::" <+> ty <+> kwWhere <> line <> dquotes (n <+> "=" <+> kwUndefined)
body <- ppCode _definitionBody
return $ kwDefinition <+> n <+> "::" <+> ty <+> kwWhere <> line <> indent' (dquotes (n <+> "=" <> oneLineOrNext body))
instance PrettyCode Function where
ppCode Function {..} = do
n <- ppCode _functionName
ty <- ppCodeQuoted _functionType
return $ kwFun <+> n <+> "::" <+> ty <+> kwWhere <> line <> dquotes (n <+> "_" <+> "=" <+> kwUndefined)
cls <- mapM ppCode _functionClauses
let cls' = punctuate (space <> kwPipe) $ map (dquotes . (n <+>)) (toList cls)
return $ kwFun <+> n <+> "::" <+> ty <+> kwWhere <> line <> indent' (vsep cls')
instance PrettyCode Clause where
ppCode Clause {..} = do
pats <- mapM ppTopCode _clausePatterns
body <- ppTopCode _clauseBody
return $ hsep pats <+> "=" <> oneLineOrNext body
instance PrettyCode Synonym where
ppCode Synonym {..} = do
n <- ppCode _synonymName
ty <- ppCodeQuoted _synonymType
return $ kwTypeSynonym <+> n <+> "=" <+> ty
return $ kwTypeSynonym <+> n <+> "=" <> oneLineOrNext ty
instance PrettyCode Datatype where
ppCode Datatype {..} = do
n <- ppCode _datatypeName
params <- ppParams _datatypeParams
ctrs <- mapM ppCode _datatypeConstructors
return $ kwDatatype <+> params <?+> n <> line <> indent' ("=" <+> vsep (punctuate "|" ctrs))
return $ kwDatatype <+> params <?+> n <> line <> indent' ("=" <+> align (vsep (punctuate (space <> kwPipe) ctrs)))
instance PrettyCode Constructor where
ppCode Constructor {..} = do
@ -113,16 +241,21 @@ instance PrettyCode RecordField where
ty <- ppCodeQuoted _recordFieldType
return $ n <+> "::" <+> ty
ppImports :: [Name] -> Sem r [Doc Ann]
ppImports ns =
return $ map (dquotes . pretty) $ filter (not . Text.isPrefixOf "Stdlib/") $ map (Text.replace "." "/" . (^. namePretty)) ns
instance PrettyCode Theory where
ppCode Theory {..} = do
n <- ppCode _theoryName
imports <- ppImports _theoryImports
stmts <- mapM ppCode _theoryStatements
return $
kwTheory
<+> n
<> line
<> kwImports
<+> "Main"
<+> align (vsep ("Main" : imports))
<> line
<> kwBegin
<> line

6
src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs
View File

@ -28,3 +28,9 @@ kwImports = keyword "imports"
kwBegin :: Doc Ann
kwBegin = keyword "begin"
kwThen :: Doc Ann
kwThen = keyword "then"
kwElse :: Doc Ann
kwElse = keyword "else"

777
src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
View File

@ -1,8 +1,11 @@
module Juvix.Compiler.Backend.Isabelle.Translation.FromTyped where
import Data.HashMap.Strict qualified as HashMap
import Data.HashSet qualified as HashSet
import Data.Text qualified as T
import Data.Text qualified as Text
import Juvix.Compiler.Backend.Isabelle.Data.Result
import Juvix.Compiler.Backend.Isabelle.Extra
import Juvix.Compiler.Backend.Isabelle.Language
import Juvix.Compiler.Internal.Data.InfoTable qualified as Internal
import Juvix.Compiler.Internal.Extra qualified as Internal
@ -13,6 +16,17 @@ import Juvix.Compiler.Store.Extra
import Juvix.Compiler.Store.Language
import Juvix.Extra.Paths qualified as P
newtype NameSet = NameSet
{ _nameSet :: HashSet Text
}
newtype NameMap = NameMap
{ _nameMap :: HashMap Name Name
}
makeLenses ''NameSet
makeLenses ''NameMap
fromInternal ::
forall r.
(Members '[Error JuvixError, Reader EntryPoint, Reader ModuleTable, NameIdGen] r) =>
@ -90,32 +104,15 @@ goModule onlyTypes infoTable Internal.Module {..} =
where
params = map goInductiveParameter _inductiveParameters
goInductiveParameter :: Internal.InductiveParameter -> Var
goInductiveParameter Internal.InductiveParameter {..} = Var _inductiveParamName
goInductiveParameter :: Internal.InductiveParameter -> TypeVar
goInductiveParameter Internal.InductiveParameter {..} = TypeVar _inductiveParamName
goRecordField :: Internal.FunctionParameter -> RecordField
goRecordField Internal.FunctionParameter {..} =
RecordField
{ _recordFieldName = fromMaybe defaultName _paramName,
{ _recordFieldName = fromMaybe (defaultName "_") _paramName,
_recordFieldType = goType _paramType
}
where
defaultName =
Name
{ _nameText = "_",
_nameId = defaultId,
_nameKind = KNameLocal,
_nameKindPretty = KNameLocal,
_namePretty = "",
_nameLoc = defaultLoc,
_nameFixity = Nothing
}
defaultLoc = singletonInterval $ mkInitialLoc P.noFile
defaultId =
NameId
{ _nameIdUid = 0,
_nameIdModuleId = defaultModuleId
}
goConstructorDef :: Internal.ConstructorDef -> Constructor
goConstructorDef Internal.ConstructorDef {..} =
@ -126,35 +123,78 @@ goModule onlyTypes infoTable Internal.Module {..} =
where
tyargs = map (goType . (^. Internal.paramType)) (fst $ Internal.unfoldFunType _inductiveConstructorType)
goDef :: Name -> Internal.Expression -> Maybe Internal.Expression -> Statement
goDef name ty body = case ty of
goDef :: Name -> Internal.Expression -> [Internal.ArgInfo] -> Maybe Internal.Expression -> Statement
goDef name ty argsInfo body = case ty of
Internal.ExpressionUniverse {} ->
StmtSynonym
Synonym
{ _synonymName = name,
{ _synonymName = name',
_synonymType = goType $ fromMaybe (error "unsupported axiomatic type") body
}
_
| argsNum == 0 ->
StmtDefinition
Definition
{ _definitionName = name,
_definitionType = goType ty
}
| otherwise ->
| isFunction argnames ty body ->
StmtFunction
Function
{ _functionName = name,
_functionType = goType ty
{ _functionName = name',
_functionType = goType ty,
_functionClauses = goBody argnames ty body
}
| otherwise ->
StmtDefinition
Definition
{ _definitionName = name',
_definitionType = goType ty,
_definitionBody = maybe ExprUndefined goExpression' body
}
where
argsNum = length $ fst $ Internal.unfoldFunType ty
argnames =
map (overNameText quote) $ filterTypeArgs 0 ty $ map (fromMaybe (defaultName "_") . (^. Internal.argInfoName)) argsInfo
name' = overNameText quote name
isFunction :: [Name] -> Internal.Expression -> Maybe Internal.Expression -> Bool
isFunction argnames ty = \case
Just (Internal.ExpressionLambda Internal.Lambda {..})
| not $ null $ filterTypeArgs 0 ty $ toList $ head _lambdaClauses ^. Internal.lambdaPatterns ->
True
_ -> not (null argnames)
goBody :: [Name] -> Internal.Expression -> Maybe Internal.Expression -> NonEmpty Clause
goBody argnames ty = \case
Nothing -> oneClause ExprUndefined
-- We assume here that all clauses have the same number of patterns
Just (Internal.ExpressionLambda Internal.Lambda {..})
| not $ null $ filterTypeArgs 0 ty $ toList $ head _lambdaClauses ^. Internal.lambdaPatterns ->
fmap goClause _lambdaClauses
| otherwise ->
oneClause (goExpression'' nset (NameMap mempty) (head _lambdaClauses ^. Internal.lambdaBody))
Just body -> oneClause (goExpression'' nset (NameMap mempty) body)
where
nset :: NameSet
nset = NameSet $ HashSet.fromList $ map (^. namePretty) argnames
oneClause :: Expression -> NonEmpty Clause
oneClause expr =
nonEmpty'
[ Clause
{ _clausePatterns = nonEmpty' $ map PatVar argnames,
_clauseBody = expr
}
]
goClause :: Internal.LambdaClause -> Clause
goClause Internal.LambdaClause {..} =
Clause
{ _clausePatterns = nonEmpty' pats,
_clauseBody = goExpression'' nset' nmap' _lambdaBody
}
where
(pats, nset', nmap') = goPatternArgs'' (filterTypeArgs 0 ty (toList _lambdaPatterns))
goFunctionDef :: Internal.FunctionDef -> Statement
goFunctionDef Internal.FunctionDef {..} = goDef _funDefName _funDefType (Just _funDefBody)
goFunctionDef Internal.FunctionDef {..} = goDef _funDefName _funDefType _funDefArgsInfo (Just _funDefBody)
goAxiomDef :: Internal.AxiomDef -> Statement
goAxiomDef Internal.AxiomDef {..} = goDef _axiomName _axiomType Nothing
goAxiomDef Internal.AxiomDef {..} = goDef _axiomName _axiomType [] Nothing
goType :: Internal.Expression -> Type
goType ty = case ty of
@ -182,6 +222,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
Just Internal.BuiltinNat -> IndNat
Just Internal.BuiltinInt -> IndInt
Just Internal.BuiltinList -> IndList
Just Internal.BuiltinMaybe -> IndOption
Just Internal.BuiltinPair -> IndTuple
_ -> IndUser name
Nothing -> case HashMap.lookup name (infoTable ^. Internal.infoAxioms) of
Just ai -> case ai ^. Internal.axiomInfoDef . Internal.axiomBuiltin of
@ -191,27 +233,674 @@ goModule onlyTypes infoTable Internal.Module {..} =
goTypeIden :: Internal.Iden -> Type
goTypeIden = \case
Internal.IdenFunction name -> mkIndType name []
Internal.IdenFunction name -> mkIndType (overNameText quote name) []
Internal.IdenConstructor name -> error ("unsupported type: constructor " <> Internal.ppTrace name)
Internal.IdenVar name -> TyVar $ Var name
Internal.IdenAxiom name -> mkIndType name []
Internal.IdenInductive name -> mkIndType name []
Internal.IdenVar name -> TyVar $ TypeVar (overNameText quote name)
Internal.IdenAxiom name -> mkIndType (overNameText quote name) []
Internal.IdenInductive name -> mkIndType (overNameText quote name) []
goTypeApp :: Internal.Application -> Type
goTypeApp app = mkIndType name params
where
(ind, args) = Internal.unfoldApplication app
params = map goType (toList args)
name = case ind of
name = overNameText quote $ case ind of
Internal.ExpressionIden (Internal.IdenFunction n) -> n
Internal.ExpressionIden (Internal.IdenAxiom n) -> n
Internal.ExpressionIden (Internal.IdenInductive n) -> n
_ -> error ("unsupported type: " <> Internal.ppTrace app)
goTypeFun :: Internal.Function -> Type
goTypeFun Internal.Function {..} = case lty of
Internal.ExpressionUniverse {} -> goType _functionRight
_ ->
TyFun $ FunType (goType lty) (goType _functionRight)
goTypeFun Internal.Function {..}
| Internal.isTypeConstructor lty = goType _functionRight
| otherwise =
TyFun $ FunType (goType lty) (goType _functionRight)
where
lty = _functionLeft ^. Internal.paramType
goConstrName :: Name -> Name
goConstrName name =
case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
Just ctrInfo ->
case ctrInfo ^. Internal.constructorInfoBuiltin of
Just Internal.BuiltinNatSuc ->
setNameText "Suc" name
Just Internal.BuiltinBoolTrue ->
setNameText "True" name
Just Internal.BuiltinBoolFalse ->
setNameText "False" name
Just Internal.BuiltinMaybeNothing ->
setNameText "None" name
Just Internal.BuiltinMaybeJust ->
setNameText "Some" name
_ -> overNameText quote name
Nothing -> overNameText quote name
goFunName :: Name -> Name
goFunName name =
case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of
Just funInfo ->
case funInfo ^. Internal.functionInfoPragmas . pragmasIsabelleFunction of
Just PragmaIsabelleFunction {..} -> setNameText _pragmaIsabelleFunctionName name
Nothing -> overNameText quote name
Nothing -> overNameText quote name
lookupName :: forall r. (Member (Reader NameMap) r) => Name -> Sem r Name
lookupName name = do
nmap <- asks (^. nameMap)
return $ fromMaybe name $ HashMap.lookup name nmap
localName :: forall a r. (Members '[Reader NameSet, Reader NameMap] r) => Name -> Name -> Sem r a -> Sem r a
localName v v' =
local (over nameSet (HashSet.insert (v' ^. namePretty)))
. local (over nameMap (HashMap.insert v v'))
localNames :: forall a r. (Members '[Reader NameSet, Reader NameMap] r) => [(Name, Name)] -> Sem r a -> Sem r a
localNames vs e = foldl' (flip (uncurry localName)) e vs
withLocalNames :: forall a r. (Members '[Reader NameSet, Reader NameMap] r) => NameSet -> NameMap -> Sem r a -> Sem r a
withLocalNames nset nmap =
local (const nset) . local (const nmap)
goExpression' :: Internal.Expression -> Expression
goExpression' = goExpression'' (NameSet mempty) (NameMap mempty)
goExpression'' :: NameSet -> NameMap -> Internal.Expression -> Expression
goExpression'' nset nmap e =
run $ runReader nset $ runReader nmap $ goExpression e
goExpression :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => Internal.Expression -> Sem r Expression
goExpression = \case
Internal.ExpressionIden x -> goIden x
Internal.ExpressionApplication x -> goApplication x
Internal.ExpressionFunction x -> goFunType x
Internal.ExpressionLiteral x -> goLiteral x
Internal.ExpressionHole x -> goHole x
Internal.ExpressionInstanceHole x -> goInstanceHole x
Internal.ExpressionLet x -> goLet x
Internal.ExpressionUniverse x -> goUniverse x
Internal.ExpressionSimpleLambda x -> goSimpleLambda x
Internal.ExpressionLambda x -> goLambda x
Internal.ExpressionCase x -> goCase x
where
goIden :: Internal.Iden -> Sem r Expression
goIden iden = case iden of
Internal.IdenFunction name -> do
name' <- lookupName name
return $ ExprIden (goFunName name')
Internal.IdenConstructor name ->
case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
Just ctrInfo ->
case ctrInfo ^. Internal.constructorInfoBuiltin of
Just Internal.BuiltinNatZero -> return $ ExprLiteral (LitNumeric 0)
_ -> return $ ExprIden (goConstrName name)
Nothing -> return $ ExprIden (goConstrName name)
Internal.IdenVar name -> do
name' <- lookupName name
return $ ExprIden name'
Internal.IdenAxiom name -> return $ ExprIden (overNameText quote name)
Internal.IdenInductive name -> return $ ExprIden (overNameText quote name)
goApplication :: Internal.Application -> Sem r Expression
goApplication app@Internal.Application {..}
| Just (pragmas, arg1, arg2) <- getIsabelleOperator app =
mkIsabelleOperator pragmas arg1 arg2
| Just x <- getLiteral app =
return $ ExprLiteral $ LitNumeric x
| Just xs <- getList app = do
xs' <- mapM goExpression xs
return $ ExprList (List xs')
| Just (arg1, arg2) <- getCons app = do
arg1' <- goExpression arg1
arg2' <- goExpression arg2
return $ ExprCons $ Cons arg1' arg2'
| Just (val, br1, br2) <- getIf app = do
val' <- goExpression val
br1' <- goExpression br1
br2' <- goExpression br2
return $ ExprIf $ If val' br1' br2'
| Just (op, fixity, arg1, arg2) <- getBoolOperator app = do
arg1' <- goExpression arg1
arg2' <- goExpression arg2
return $
ExprBinop
Binop
{ _binopOperator = op,
_binopLeft = arg1',
_binopRight = arg2',
_binopFixity = fixity
}
| Just (x, y) <- getPair app = do
x' <- goExpression x
y' <- goExpression y
return $ ExprTuple (Tuple (x' :| [y']))
| Just (fn, args) <- getIdentApp app = do
fn' <- goExpression fn
args' <- mapM goExpression args
return $ mkApp fn' args'
| otherwise = do
l <- goExpression _appLeft
r <- goExpression _appRight
return $ ExprApp (Application l r)
mkIsabelleOperator :: PragmaIsabelleOperator -> Internal.Expression -> Internal.Expression -> Sem r Expression
mkIsabelleOperator PragmaIsabelleOperator {..} arg1 arg2 = do
arg1' <- goExpression arg1
arg2' <- goExpression arg2
return $
ExprBinop
Binop
{ _binopOperator = defaultName _pragmaIsabelleOperatorName,
_binopLeft = arg1',
_binopRight = arg2',
_binopFixity =
Fixity
{ _fixityPrecedence = PrecNat (fromMaybe 0 _pragmaIsabelleOperatorPrec),
_fixityArity = OpBinary (fromMaybe AssocNone _pragmaIsabelleOperatorAssoc),
_fixityId = Nothing
}
}
getIsabelleOperator :: Internal.Application -> Maybe (PragmaIsabelleOperator, Internal.Expression, Internal.Expression)
getIsabelleOperator app = case fn of
Internal.ExpressionIden (Internal.IdenFunction name) ->
case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of
Just funInfo ->
case funInfo ^. Internal.functionInfoPragmas . pragmasIsabelleOperator of
Just pragma ->
case args of
Internal.ExpressionIden (Internal.IdenInductive tyname) :| [_, arg1, arg2] ->
case HashMap.lookup tyname (infoTable ^. Internal.infoInductives) of
Just Internal.InductiveInfo {..} ->
case _inductiveInfoBuiltin of
Just Internal.BuiltinNat -> Just (pragma, arg1, arg2)
Just Internal.BuiltinInt -> Just (pragma, arg1, arg2)
_ -> Nothing
Nothing -> Nothing
_ -> Nothing
Nothing -> Nothing
Nothing -> Nothing
_ -> Nothing
where
(fn, args) = Internal.unfoldApplication app
getLiteral :: Internal.Application -> Maybe Integer
getLiteral app = case fn of
Internal.ExpressionIden (Internal.IdenFunction name) ->
case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of
Just funInfo ->
case funInfo ^. Internal.functionInfoBuiltin of
Just Internal.BuiltinFromNat -> lit
Just Internal.BuiltinFromInt -> lit
_ -> Nothing
Nothing -> Nothing
_ -> Nothing
where
(fn, args) = Internal.unfoldApplication app
lit :: Maybe Integer
lit = case args of
_ :| [_, Internal.ExpressionLiteral l] ->
case l ^. Internal.withLocParam of
Internal.LitString {} -> Nothing
Internal.LitNumeric x -> Just x
Internal.LitInteger x -> Just x
Internal.LitNatural x -> Just x
_ -> Nothing
getList :: Internal.Application -> Maybe [Internal.Expression]
getList app = case fn of
Internal.ExpressionIden (Internal.IdenConstructor name) ->
case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
Just ctrInfo ->
case ctrInfo ^. Internal.constructorInfoBuiltin of
Just Internal.BuiltinListNil -> Just []
Just Internal.BuiltinListCons
| (_ :| [arg1, Internal.ExpressionApplication app2]) <- args,
Just lst <- getList app2 ->
Just (arg1 : lst)
_ -> Nothing
Nothing -> Nothing
_ -> Nothing
where
(fn, args) = Internal.unfoldApplication app
getCons :: Internal.Application -> Maybe (Internal.Expression, Internal.Expression)
getCons app = case fn of
Internal.ExpressionIden (Internal.IdenConstructor name) ->
case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
Just ctrInfo ->
case ctrInfo ^. Internal.constructorInfoBuiltin of
Just Internal.BuiltinListCons
| (_ :| [arg1, arg2]) <- args ->
Just (arg1, arg2)
_ -> Nothing
Nothing -> Nothing
_ -> Nothing
where
(fn, args) = Internal.unfoldApplication app
getIf :: Internal.Application -> Maybe (Internal.Expression, Internal.Expression, Internal.Expression)
getIf app = case fn of
Internal.ExpressionIden (Internal.IdenFunction name) ->
case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of
Just funInfo ->
case funInfo ^. Internal.functionInfoBuiltin of
Just Internal.BuiltinBoolIf
| (_ :| [val, br1, br2]) <- args ->
Just (val, br1, br2)
_ -> Nothing
Nothing -> Nothing
_ -> Nothing
where
(fn, args) = Internal.unfoldApplication app
getBoolOperator :: Internal.Application -> Maybe (Name, Fixity, Internal.Expression, Internal.Expression)
getBoolOperator app = case fn of
Internal.ExpressionIden (Internal.IdenFunction name) ->
case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of
Just funInfo ->
case funInfo ^. Internal.functionInfoBuiltin of
Just Internal.BuiltinBoolAnd
| (arg1 :| [arg2]) <- args ->
Just (defaultName "∧", andFixity, arg1, arg2)
Just Internal.BuiltinBoolOr
| (arg1 :| [arg2]) <- args ->
Just (defaultName "∨", orFixity, arg1, arg2)
_ -> Nothing
Nothing -> Nothing
_ -> Nothing
where
(fn, args) = Internal.unfoldApplication app
getPair :: Internal.Application -> Maybe (Internal.Expression, Internal.Expression)
getPair app = case fn of
Internal.ExpressionIden (Internal.IdenConstructor name) ->
case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
Just ctrInfo ->
case ctrInfo ^. Internal.constructorInfoBuiltin of
Just Internal.BuiltinPairConstr
| (_ :| [_, arg1, arg2]) <- args ->
Just (arg1, arg2)
_ -> Nothing
Nothing -> Nothing
_ -> Nothing
where
(fn, args) = Internal.unfoldApplication app
getIdentApp :: Internal.Application -> Maybe (Internal.Expression, [Internal.Expression])
getIdentApp app = case mty of
Just (ty, paramsNum) -> Just (fn, args')
where
args' = filterTypeArgs paramsNum ty (toList args)
Nothing -> Nothing
where
(fn, args) = Internal.unfoldApplication app
mty = case fn of
Internal.ExpressionIden (Internal.IdenFunction name) ->
case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of
Just funInfo -> Just (funInfo ^. Internal.functionInfoType, 0)
Nothing -> Nothing
Internal.ExpressionIden (Internal.IdenConstructor name) ->
case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
Just ctrInfo ->
Just
( ctrInfo ^. Internal.constructorInfoType,
length (ctrInfo ^. Internal.constructorInfoInductiveParameters)
)
Nothing -> Nothing
_ -> Nothing
goFunType :: Internal.Function -> Sem r Expression
goFunType _ = return ExprUndefined
goLiteral :: Internal.LiteralLoc -> Sem r Expression
goLiteral lit = return $ ExprLiteral $ case lit ^. withLocParam of
Internal.LitString s -> LitString s
Internal.LitNumeric n -> LitNumeric n
Internal.LitInteger n -> LitNumeric n
Internal.LitNatural n -> LitNumeric n
goHole :: Internal.Hole -> Sem r Expression
goHole _ = return ExprUndefined
goInstanceHole :: Internal.InstanceHole -> Sem r Expression
goInstanceHole _ = return ExprUndefined
-- TODO: binders
goLet :: Internal.Let -> Sem r Expression
goLet Internal.Let {..} = do
let fdefs = concatMap toFunDefs (toList _letClauses)
cls <- mapM goFunDef fdefs
let ns = zipExact (map (^. Internal.funDefName) fdefs) (map (^. letClauseName) cls)
expr <- localNames ns $ goExpression _letExpression
return $
ExprLet
Let
{ _letClauses = nonEmpty' cls,
_letBody = expr
}
where
toFunDefs :: Internal.LetClause -> [Internal.FunctionDef]
toFunDefs = \case
Internal.LetFunDef d -> [d]
Internal.LetMutualBlock Internal.MutualBlockLet {..} -> toList _mutualLet
goFunDef :: Internal.FunctionDef -> Sem r LetClause
goFunDef Internal.FunctionDef {..} = do
nset <- asks (^. nameSet)
let name' = overNameText (disambiguate nset) _funDefName
val <- localName _funDefName name' $ goExpression _funDefBody
return $
LetClause
{ _letClauseName = name',
_letClauseValue = val
}
goUniverse :: Internal.SmallUniverse -> Sem r Expression
goUniverse _ = return ExprUndefined
goSimpleLambda :: Internal.SimpleLambda -> Sem r Expression
goSimpleLambda Internal.SimpleLambda {..} = do
nset <- asks (^. nameSet)
let v = _slambdaBinder ^. Internal.sbinderVar
v' = overNameText (disambiguate nset) v
body <-
localName v v' $
goExpression _slambdaBody
return $
ExprLambda
Lambda
{ _lambdaVar = v',
_lambdaType = Just $ goType $ _slambdaBinder ^. Internal.sbinderType,
_lambdaBody = body
}
goLambda :: Internal.Lambda -> Sem r Expression
goLambda Internal.Lambda {..}
| npats == 0 = goExpression (head _lambdaClauses ^. Internal.lambdaBody)
| otherwise = goLams vars
where
npats =
case _lambdaType of
Just ty ->
length
. filterTypeArgs 0 ty
. toList
$ head _lambdaClauses ^. Internal.lambdaPatterns
Nothing ->
length
. filter ((/= Internal.Implicit) . (^. Internal.patternArgIsImplicit))
. toList
$ head _lambdaClauses ^. Internal.lambdaPatterns
vars = map (\i -> defaultName ("x" <> show i)) [0 .. npats - 1]
goLams :: [Name] -> Sem r Expression
goLams = \case
v : vs -> do
nset <- asks (^. nameSet)
let v' = overNameText (disambiguate nset) v
body <-
localName v v' $
goLams vs
return $
ExprLambda
Lambda
{ _lambdaType = Nothing,
_lambdaVar = v',
_lambdaBody = body
}
[] -> do
val <-
case vars of
[v] -> do
v' <- lookupName v
return $ ExprIden v'
_ -> do
vars' <- mapM lookupName vars
return $
ExprTuple
Tuple
{ _tupleComponents = nonEmpty' $ map ExprIden vars'
}
brs <- mapM goClause _lambdaClauses
return $
ExprCase
Case
{ _caseValue = val,
_caseBranches = brs
}
goClause :: Internal.LambdaClause -> Sem r CaseBranch
goClause Internal.LambdaClause {..} = do
(pat, nset, nmap) <- case _lambdaPatterns of
p :| [] -> goPatternArg' p
_ -> do
(pats, nset, nmap) <- goPatternArgs' (toList _lambdaPatterns)
let pat =
PatTuple
Tuple
{ _tupleComponents = nonEmpty' pats
}
return (pat, nset, nmap)
body <- withLocalNames nset nmap $ goExpression _lambdaBody
return $
CaseBranch
{ _caseBranchPattern = pat,
_caseBranchBody = body
}
goCase :: Internal.Case -> Sem r Expression
goCase Internal.Case {..} = do
val <- goExpression _caseExpression
brs <- mapM goCaseBranch _caseBranches
return $
ExprCase
Case
{ _caseValue = val,
_caseBranches = brs
}
goCaseBranch :: Internal.CaseBranch -> Sem r CaseBranch
goCaseBranch Internal.CaseBranch {..} = do
(pat, nset, nmap) <- goPatternArg' _caseBranchPattern
rhs <- withLocalNames nset nmap $ goCaseBranchRhs _caseBranchRhs
return $
CaseBranch
{ _caseBranchPattern = pat,
_caseBranchBody = rhs
}
goCaseBranchRhs :: Internal.CaseBranchRhs -> Sem r Expression
goCaseBranchRhs = \case
Internal.CaseBranchRhsExpression e -> goExpression e
Internal.CaseBranchRhsIf {} -> error "unsupported: side conditions"
goPatternArgs'' :: [Internal.PatternArg] -> ([Pattern], NameSet, NameMap)
goPatternArgs'' pats =
(pats', nset, nmap)
where
(nset, (nmap, pats')) = run $ runState (NameSet mempty) $ runState (NameMap mempty) $ goPatternArgs pats
goPatternArg' :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => Internal.PatternArg -> Sem r (Pattern, NameSet, NameMap)
goPatternArg' pat = do
nset <- ask @NameSet
nmap <- ask @NameMap
let (nmap', (nset', pat')) = run $ runState nmap $ runState nset $ goPatternArg pat
return (pat', nset', nmap')
goPatternArgs' :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => [Internal.PatternArg] -> Sem r ([Pattern], NameSet, NameMap)
goPatternArgs' pats = do
nset <- ask @NameSet
nmap <- ask @NameMap
let (nmap', (nset', pats')) = run $ runState nmap $ runState nset $ goPatternArgs pats
return (pats', nset', nmap')
goPatternArgs :: forall r. (Members '[State NameSet, State NameMap] r) => [Internal.PatternArg] -> Sem r [Pattern]
goPatternArgs = mapM goPatternArg
-- TODO: named patterns (`_patternArgName`) are not handled properly
goPatternArg :: forall r. (Members '[State NameSet, State NameMap] r) => Internal.PatternArg -> Sem r Pattern
goPatternArg Internal.PatternArg {..} =
goPattern _patternArgPattern
where
goPattern :: Internal.Pattern -> Sem r Pattern
goPattern = \case
Internal.PatternVariable name -> do
binders <- gets (^. nameSet)
let name' = overNameText (disambiguate binders) name
modify' (over nameSet (HashSet.insert (name' ^. namePretty)))
modify' (over nameMap (HashMap.insert name name'))
return $ PatVar name'
Internal.PatternConstructorApp x -> goPatternConstructorApp x
Internal.PatternWildcardConstructor {} -> impossible
goPatternConstructorApp :: Internal.ConstructorApp -> Sem r Pattern
goPatternConstructorApp Internal.ConstructorApp {..}
| Just lst <- getListPat _constrAppConstructor _constrAppParameters = do
pats <- goPatternArgs lst
return $ PatList (List pats)
| Just (x, y) <- getConsPat _constrAppConstructor _constrAppParameters = do
x' <- goPatternArg x
y' <- goPatternArg y
return $ PatCons (Cons x' y')
| Just (x, y) <- getPairPat _constrAppConstructor _constrAppParameters = do
x' <- goPatternArg x
y' <- goPatternArg y
return $ PatTuple (Tuple (x' :| [y']))
| Just p <- getNatPat _constrAppConstructor _constrAppParameters =
case p of
Left zero -> return zero
Right arg -> do
arg' <- goPatternArg arg
return (PatConstrApp (ConstrApp (goConstrName _constrAppConstructor) [arg']))
| otherwise = do
args <- mapM goPatternArg _constrAppParameters
return $
PatConstrApp
ConstrApp
{ _constrAppConstructor = goConstrName _constrAppConstructor,
_constrAppArgs = args
}
-- This function cannot be simply merged with `getList` because in patterns
-- the constructors don't get the type arguments.
getListPat :: Name -> [Internal.PatternArg] -> Maybe [Internal.PatternArg]
getListPat name args =
case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
Just funInfo ->
case funInfo ^. Internal.constructorInfoBuiltin of
Just Internal.BuiltinListNil -> Just []
Just Internal.BuiltinListCons
| [arg1, Internal.PatternArg {..}] <- args,
Internal.PatternConstructorApp Internal.ConstructorApp {..} <- _patternArgPattern,
Just lst <- getListPat _constrAppConstructor _constrAppParameters ->
Just (arg1 : lst)
_ -> Nothing
Nothing -> Nothing
getConsPat :: Name -> [Internal.PatternArg] -> Maybe (Internal.PatternArg, Internal.PatternArg)
getConsPat name args =
case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
Just funInfo ->
case funInfo ^. Internal.constructorInfoBuiltin of
Just Internal.BuiltinListCons
| [arg1, arg2] <- args ->
Just (arg1, arg2)
_ -> Nothing
Nothing -> Nothing
getNatPat :: Name -> [Internal.PatternArg] -> Maybe (Either Pattern Internal.PatternArg)
getNatPat name args =
case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
Just funInfo ->
case funInfo ^. Internal.constructorInfoBuiltin of
Just Internal.BuiltinNatZero
| null args ->
Just $ Left PatZero
Just Internal.BuiltinNatSuc
| [arg] <- args ->
Just $ Right arg
_ -> Nothing
Nothing -> Nothing
getPairPat :: Name -> [Internal.PatternArg] -> Maybe (Internal.PatternArg, Internal.PatternArg)
getPairPat name args =
case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
Just funInfo ->
case funInfo ^. Internal.constructorInfoBuiltin of
Just Internal.BuiltinPairConstr
| [arg1, arg2] <- args ->
Just (arg1, arg2)
_ -> Nothing
Nothing -> Nothing
defaultName :: Text -> Name
defaultName n =
Name
{ _nameText = n,
_nameId = defaultId,
_nameKind = KNameLocal,
_nameKindPretty = KNameLocal,
_namePretty = n,
_nameLoc = defaultLoc,
_nameFixity = Nothing
}
where
defaultLoc = singletonInterval $ mkInitialLoc P.noFile
defaultId =
NameId
{ _nameIdUid = 0,
_nameIdModuleId = defaultModuleId
}
setNameText :: Text -> Name -> Name
setNameText txt name =
set namePretty txt
. set nameText txt
$ name
overNameText :: (Text -> Text) -> Name -> Name
overNameText f name =
over namePretty f
. over nameText f
$ name
disambiguate :: HashSet Text -> Text -> Text
disambiguate binders = disambiguate' binders . quote
disambiguate' :: HashSet Text -> Text -> Text
disambiguate' binders name
| name == "?" || name == "" || name == "_" =
disambiguate' binders "X"
| HashSet.member name binders
|| HashSet.member name names =
disambiguate' binders (prime name)
| otherwise =
name
names :: HashSet Text
names =
HashSet.fromList $
map (^. Internal.functionInfoName . namePretty) (filter (not . (^. Internal.functionInfoIsLocal)) (HashMap.elems (infoTable ^. Internal.infoFunctions)))
++ map (^. Internal.constructorInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoConstructors))
++ map (^. Internal.inductiveInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoInductives))
++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms))
quote :: Text -> Text
quote txt = case Text.uncons txt of
Just (c, txt') | not (isLetter c) -> txt'
_ -> txt
filterTypeArgs :: Int -> Internal.Expression -> [a] -> [a]
filterTypeArgs paramsNum ty args =
map fst $
filter (not . snd) $
zip (drop paramsNum args) (argtys ++ repeat False)
where
argtys =
map Internal.isTypeConstructor
. map (^. Internal.paramType)
. fst
. Internal.unfoldFunType
$ ty

27
src/Juvix/Compiler/Builtins/Pair.hs Normal file
View File

@ -0,0 +1,27 @@
module Juvix.Compiler.Builtins.Pair where
import Juvix.Compiler.Builtins.Effect
import Juvix.Compiler.Internal.Extra
import Juvix.Compiler.Internal.Pretty
import Juvix.Prelude
registerPairDef :: (Member Builtins r) => InductiveDef -> Sem r ()
registerPairDef d = do
unless (isSmallUniverse' (d ^. inductiveType)) (error "Pair should be in the small universe")
registerBuiltin BuiltinPair (d ^. inductiveName)
case d ^. inductiveConstructors of
[c] -> registerPairConstr p1 p2 c
_ -> error "Pair should have exactly one constructor"
where
(p1, p2) = case d ^. inductiveParameters of
[v1, v2] -> (v1 ^. inductiveParamName, v2 ^. inductiveParamName)
_ -> error "Pair should have exactly two type parameters"
registerPairConstr :: (Member Builtins r) => VarName -> VarName -> ConstructorDef -> Sem r ()
registerPairConstr a b d@ConstructorDef {..} = do
let pr = _inductiveConstructorName
ty = _inductiveConstructorType
pair_ <- getBuiltinName (getLoc d) BuiltinPair
let prty = a --> b --> pair_ @@ a @@ b
unless (ty === prty) (error $ ", has the wrong type " <> ppTrace ty <> " | " <> ppTrace prty)
registerBuiltin BuiltinPairConstr pr

5
src/Juvix/Compiler/Concrete/Data/Builtins.hs
View File

@ -48,6 +48,7 @@ builtinConstructors = \case
BuiltinInt -> [BuiltinIntOfNat, BuiltinIntNegSuc]
BuiltinList -> [BuiltinListNil, BuiltinListCons]
BuiltinMaybe -> [BuiltinMaybeNothing, BuiltinMaybeJust]
BuiltinPair -> [BuiltinPairConstr]
BuiltinPoseidonState -> [BuiltinMkPoseidonState]
BuiltinEcPoint -> [BuiltinMkEcPoint]
@ -57,6 +58,7 @@ data BuiltinInductive
| BuiltinInt
| BuiltinList
| BuiltinMaybe
| BuiltinPair
| BuiltinPoseidonState
| BuiltinEcPoint
deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
@ -74,6 +76,7 @@ instance Pretty BuiltinInductive where
BuiltinInt -> Str.int_
BuiltinList -> Str.list
BuiltinMaybe -> Str.maybe_
BuiltinPair -> Str.pair
BuiltinPoseidonState -> Str.cairoPoseidonState
BuiltinEcPoint -> Str.cairoEcPoint
@ -89,6 +92,7 @@ instance Pretty BuiltinConstructor where
BuiltinListCons -> Str.cons
BuiltinMaybeNothing -> Str.nothing
BuiltinMaybeJust -> Str.just
BuiltinPairConstr -> Str.pair
BuiltinMkPoseidonState -> Str.cairoMkPoseidonState
BuiltinMkEcPoint -> Str.cairoMkEcPoint
@ -103,6 +107,7 @@ data BuiltinConstructor
| BuiltinListCons
| BuiltinMaybeNothing
| BuiltinMaybeJust
| BuiltinPairConstr
| BuiltinMkPoseidonState
| BuiltinMkEcPoint
deriving stock (Show, Eq, Ord, Generic, Data)

2
src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs
View File

@ -65,6 +65,8 @@ checkCairo md = do
isRecordOrList TypeConstr {..} = case ii ^. inductiveBuiltin of
Just (BuiltinTypeInductive BuiltinList) ->
all isArgType _typeConstrArgs
Just (BuiltinTypeInductive BuiltinPair) ->
all isArgType _typeConstrArgs
Just {} ->
False
Nothing ->

1
src/Juvix/Compiler/Core/Translation/FromInternal.hs
View File

@ -211,6 +211,7 @@ goConstructor sym ctor = do
Just Internal.BuiltinListCons -> freshTag
Just Internal.BuiltinMaybeNothing -> freshTag
Just Internal.BuiltinMaybeJust -> freshTag
Just Internal.BuiltinPairConstr -> freshTag
Just Internal.BuiltinMkPoseidonState -> freshTag
Just Internal.BuiltinMkEcPoint -> freshTag
Nothing -> freshTag

2
src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
View File

@ -64,6 +64,7 @@ fromCore fsize tab =
BuiltinMkEcPoint -> True
BuiltinMaybeNothing -> True
BuiltinMaybeJust -> True
BuiltinPairConstr -> True
BuiltinNatZero -> False
BuiltinNatSuc -> False
BuiltinBoolTrue -> False
@ -110,6 +111,7 @@ fromCore fsize tab =
BuiltinTypeInductive i -> case i of
BuiltinList -> True
BuiltinMaybe -> True
BuiltinPair -> True
BuiltinPoseidonState -> True
BuiltinEcPoint -> True
BuiltinNat -> False

13
src/Juvix/Compiler/Internal/Data/InfoTable.hs
View File

@ -30,8 +30,8 @@ import Juvix.Compiler.Store.Internal.Data.TypesTable
import Juvix.Compiler.Store.Internal.Language
import Juvix.Prelude
functionInfoFromFunctionDef :: FunctionDef -> FunctionInfo
functionInfoFromFunctionDef FunctionDef {..} =
functionInfoFromFunctionDef :: Bool -> FunctionDef -> FunctionInfo
functionInfoFromFunctionDef isLocal FunctionDef {..} =
FunctionInfo
{ _functionInfoName = _funDefName,
_functionInfoType = _funDefType,
@ -40,7 +40,8 @@ functionInfoFromFunctionDef FunctionDef {..} =
_functionInfoCoercion = _funDefCoercion,
_functionInfoInstance = _funDefInstance,
_functionInfoTerminating = _funDefTerminating,
_functionInfoPragmas = _funDefPragmas
_functionInfoPragmas = _funDefPragmas,
_functionInfoIsLocal = isLocal
}
inductiveInfoFromInductiveDef :: InductiveDef -> InductiveInfo
@ -62,7 +63,7 @@ extendWithReplExpression e =
infoFunctions
( HashMap.union
( HashMap.fromList
[ (f ^. funDefName, functionInfoFromFunctionDef f)
[ (f ^. funDefName, functionInfoFromFunctionDef True f)
| f <- letFunctionDefs e
]
)
@ -127,10 +128,10 @@ computeInternalModuleInfoTable m = InfoTable {..}
_infoFunctions :: HashMap Name FunctionInfo
_infoFunctions =
HashMap.fromList $
[ (f ^. funDefName, functionInfoFromFunctionDef f)
[ (f ^. funDefName, functionInfoFromFunctionDef False f)
| StatementFunction f <- mutuals
]
<> [ (f ^. funDefName, functionInfoFromFunctionDef f)
<> [ (f ^. funDefName, functionInfoFromFunctionDef True f)
| s <- ss,
f <- letFunctionDefs s
]

7
src/Juvix/Compiler/Internal/Extra/Base.hs
View File

@ -136,8 +136,6 @@ instance HasExpressions Case where
_caseExpressionType <- directExpressions f (l ^. caseExpressionType)
_caseExpressionWholeType <- directExpressions f (l ^. caseExpressionWholeType)
pure Case {..}
where
_caseParens = l ^. caseParens
instance HasExpressions MutualBlock where
directExpressions f (MutualBlock defs) =
@ -767,6 +765,11 @@ isSmallUniverse' = \case
ExpressionUniverse {} -> True
_ -> False
-- | This function does not take into account synonyms (won't work with e.g.
-- `Type' : Type := Type`).
isTypeConstructor :: Expression -> Bool
isTypeConstructor = isSmallUniverse' . snd . unfoldFunType
explicitPatternArg :: Pattern -> PatternArg
explicitPatternArg _patternArgPattern =
PatternArg

3
src/Juvix/Compiler/Internal/Extra/Clonable.hs
View File

@ -140,8 +140,7 @@ instance Clonable Case where
{ _caseExpression = e',
_caseExpressionType = ety',
_caseExpressionWholeType = wholetype',
_caseBranches = branches',
_caseParens
_caseBranches = branches'
}
instance Clonable Function where

1
src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
View File

@ -194,6 +194,7 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
addInductiveStartNode
BuiltinList -> return ()
BuiltinMaybe -> return ()
BuiltinPair -> return ()
BuiltinPoseidonState -> return ()
BuiltinEcPoint -> return ()

7
src/Juvix/Compiler/Internal/Language.hs
View File

@ -6,12 +6,14 @@ module Juvix.Compiler.Internal.Language
module Juvix.Data.Universe,
module Juvix.Data.Hole,
module Juvix.Compiler.Concrete.Data.Builtins,
module Juvix.Data.InstanceHole,
)
where
import Juvix.Compiler.Concrete.Data.Builtins
import Juvix.Compiler.Internal.Data.Name
import Juvix.Data.Hole
import Juvix.Data.InstanceHole
import Juvix.Data.IsImplicit
import Juvix.Data.Universe hiding (smallUniverse)
import Juvix.Data.WithLoc
@ -273,8 +275,7 @@ data Case = Case
_caseExpressionType :: Maybe Expression,
-- | The type of the whole case expression. The typechecker fills this field
_caseExpressionWholeType :: Maybe Expression,
_caseBranches :: NonEmpty CaseBranch,
_caseParens :: Bool
_caseBranches :: NonEmpty CaseBranch
}
deriving stock (Eq, Generic, Data)
@ -413,8 +414,6 @@ data ConstructorDef = ConstructorDef
}
deriving stock (Data)
-- | At the moment we only use the name when we have a default value, so
-- isNothing _argInfoDefault implies isNothing _argInfoName
data ArgInfo = ArgInfo
{ _argInfoDefault :: Maybe Expression,
_argInfoName :: Maybe Name

2
src/Juvix/Compiler/Internal/Pretty/Base.hs
View File

@ -120,7 +120,7 @@ instance PrettyCode Case where
ppCode Case {..} = do
exp <- ppCode _caseExpression
branches <- indent' . vsep <$> mapM ppCode _caseBranches
return $ parensIf _caseParens (kwCase <+> exp <> line <> branches)
return $ kwCase <+> exp <> line <> branches
instance PrettyCode Let where
ppCode l = do

5
src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
View File

@ -14,6 +14,7 @@ import Data.HashSet qualified as HashSet
import Data.IntMap.Strict qualified as IntMap
import Data.List.NonEmpty qualified as NonEmpty
import Juvix.Compiler.Builtins
import Juvix.Compiler.Builtins.Pair
import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
import Juvix.Compiler.Concrete.Extra qualified as Concrete
import Juvix.Compiler.Concrete.Gen qualified as Gen
@ -500,6 +501,7 @@ registerBuiltinInductive d = \case
BuiltinInt -> registerIntDef d
BuiltinList -> registerListDef d
BuiltinMaybe -> registerMaybeDef d
BuiltinPair -> registerPairDef d
BuiltinPoseidonState -> registerPoseidonStateDef d
BuiltinEcPoint -> registerEcPointDef d
@ -1084,8 +1086,7 @@ goCase :: forall r. (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Err
goCase c = do
_caseExpression <- goExpression (c ^. caseExpression)
_caseBranches <- mapM goBranch (c ^. caseBranches)
let _caseParens = False
_caseExpressionType :: Maybe Internal.Expression = Nothing
let _caseExpressionType :: Maybe Internal.Expression = Nothing
_caseExpressionWholeType :: Maybe Internal.Expression = Nothing
return Internal.Case {..}
where

1
src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
View File

@ -1024,7 +1024,6 @@ inferLeftAppExpression mhint e = case e of
funty :: Expression
funty = ExpressionFunction (mkFunction (typedCaseExpression ^. typedType) ty)
_caseBranches <- mapM goBranch (c ^. caseBranches)
let _caseParens = c ^. caseParens
return
TypedExpression
{ _typedType = ty,

3
src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs
View File

@ -26,7 +26,8 @@ data FunctionInfo = FunctionInfo
_functionInfoCoercion :: Bool,
_functionInfoBuiltin :: Maybe BuiltinFunction,
_functionInfoArgsInfo :: [ArgInfo],
_functionInfoPragmas :: Pragmas
_functionInfoPragmas :: Pragmas,
_functionInfoIsLocal :: Bool
}
deriving stock (Generic)

2
src/Juvix/Data/Fixity.hs
View File

@ -22,6 +22,8 @@ data BinaryAssoc
| AssocRight
deriving stock (Show, Eq, Ord, Data, Generic)
instance Hashable BinaryAssoc
data OperatorArity
= OpUnary UnaryAssoc
| OpBinary BinaryAssoc

62
src/Juvix/Data/Pragmas.hs
View File

@ -1,6 +1,7 @@
module Juvix.Data.Pragmas where
import Data.Aeson.BetterErrors qualified as Aeson
import Juvix.Data.Fixity
import Juvix.Data.Yaml
import Juvix.Extra.Serialize
import Juvix.Prelude.Base
@ -58,6 +59,18 @@ newtype PragmaEval = PragmaEval
}
deriving stock (Show, Eq, Ord, Data, Generic)
data PragmaIsabelleOperator = PragmaIsabelleOperator
{ _pragmaIsabelleOperatorName :: Text,
_pragmaIsabelleOperatorPrec :: Maybe Int,
_pragmaIsabelleOperatorAssoc :: Maybe BinaryAssoc
}
deriving stock (Show, Eq, Ord, Data, Generic)
newtype PragmaIsabelleFunction = PragmaIsabelleFunction
{ _pragmaIsabelleFunctionName :: Text
}
deriving stock (Show, Eq, Ord, Data, Generic)
data Pragmas = Pragmas
{ _pragmasInline :: Maybe PragmaInline,
_pragmasUnroll :: Maybe PragmaUnroll,
@ -67,7 +80,9 @@ data Pragmas = Pragmas
_pragmasSpecialise :: Maybe PragmaSpecialise,
_pragmasSpecialiseArgs :: Maybe PragmaSpecialiseArgs,
_pragmasSpecialiseBy :: Maybe PragmaSpecialiseBy,
_pragmasEval :: Maybe PragmaEval
_pragmasEval :: Maybe PragmaEval,
_pragmasIsabelleOperator :: Maybe PragmaIsabelleOperator,
_pragmasIsabelleFunction :: Maybe PragmaIsabelleFunction
}
deriving stock (Show, Eq, Ord, Data, Generic)
@ -78,6 +93,8 @@ makeLenses ''PragmaFormat
makeLenses ''PragmaSpecialiseArgs
makeLenses ''PragmaSpecialiseBy
makeLenses ''PragmaEval
makeLenses ''PragmaIsabelleOperator
makeLenses ''PragmaIsabelleFunction
makeLenses ''Pragmas
instance Hashable PragmaInline
@ -100,6 +117,10 @@ instance Hashable PragmaSpecialiseBy
instance Hashable PragmaEval
instance Hashable PragmaIsabelleOperator
instance Hashable PragmaIsabelleFunction
instance Hashable Pragmas
instance Serialize PragmaInline
@ -142,6 +163,14 @@ instance Serialize PragmaEval
instance NFData PragmaEval
instance Serialize PragmaIsabelleOperator
instance NFData PragmaIsabelleOperator
instance Serialize PragmaIsabelleFunction
instance NFData PragmaIsabelleFunction
instance Serialize Pragmas
instance NFData Pragmas
@ -170,6 +199,8 @@ instance FromJSON Pragmas where
specby' <- keyMay "specialize-by" parseSpecialiseBy
let _pragmasSpecialiseBy = specby <|> specby'
_pragmasEval <- keyMay "eval" parseEval
_pragmasIsabelleOperator <- keyMay "isabelle-operator" parseIsabelleOperator
_pragmasIsabelleFunction <- keyMay "isabelle-function" parseIsabelleFunction
return Pragmas {..}
parseInline :: Parse YamlError PragmaInline
@ -221,6 +252,27 @@ instance FromJSON Pragmas where
_pragmaEval <- asBool
return PragmaEval {..}
parseIsabelleOperator :: Parse YamlError PragmaIsabelleOperator
parseIsabelleOperator = do
_pragmaIsabelleOperatorName <- key "name" asText
_pragmaIsabelleOperatorPrec <- keyMay "prec" asIntegral
_pragmaIsabelleOperatorAssoc <- keyMay "assoc" parseAssoc
return PragmaIsabelleOperator {..}
parseAssoc :: Parse YamlError BinaryAssoc
parseAssoc = do
assoc <- asText
case assoc of
"left" -> return AssocLeft
"right" -> return AssocRight
"none" -> return AssocNone
_ -> throwCustomError "unknown associativity"
parseIsabelleFunction :: Parse YamlError PragmaIsabelleFunction
parseIsabelleFunction = do
_pragmaIsabelleFunctionName <- key "name" asText
return PragmaIsabelleFunction {..}
parseSpecialiseArg :: Parse YamlError PragmaSpecialiseArg
parseSpecialiseArg =
(SpecialiseArgNum <$> asIntegral)
@ -262,7 +314,9 @@ instance Semigroup Pragmas where
_pragmasEval = p2 ^. pragmasEval <|> p1 ^. pragmasEval,
_pragmasSpecialise = p2 ^. pragmasSpecialise <|> p1 ^. pragmasSpecialise,
_pragmasSpecialiseArgs = p2 ^. pragmasSpecialiseArgs <|> p1 ^. pragmasSpecialiseArgs,
_pragmasSpecialiseBy = p2 ^. pragmasSpecialiseBy <|> p1 ^. pragmasSpecialiseBy
_pragmasSpecialiseBy = p2 ^. pragmasSpecialiseBy <|> p1 ^. pragmasSpecialiseBy,
_pragmasIsabelleOperator = p2 ^. pragmasIsabelleOperator,
_pragmasIsabelleFunction = p2 ^. pragmasIsabelleFunction
}
instance Monoid Pragmas where
@ -276,7 +330,9 @@ instance Monoid Pragmas where
_pragmasSpecialise = Nothing,
_pragmasSpecialiseArgs = Nothing,
_pragmasSpecialiseBy = Nothing,
_pragmasEval = Nothing
_pragmasEval = Nothing,
_pragmasIsabelleOperator = Nothing,
_pragmasIsabelleFunction = Nothing
}
adjustPragmaInline :: Int -> PragmaInline -> PragmaInline

3
src/Juvix/Extra/Strings.hs
View File

@ -905,6 +905,9 @@ nothing = "nothing"
just :: (IsString s) => s
just = "just"
pair :: (IsString s) => s
pair = "pair"
unary :: (IsString s) => s
unary = "unary"

10
test/Isabelle.hs Normal file
View File

@ -0,0 +1,10 @@
module Isabelle
( allTests,
)
where
import Base
import Isabelle.Positive qualified as P
allTests :: TestTree
allTests = testGroup "Isabelle tests" [P.allTests]

54
test/Isabelle/Positive.hs Normal file
View File

@ -0,0 +1,54 @@
module Isabelle.Positive where
import Base
import Juvix.Compiler.Backend.Isabelle.Data.Result
import Juvix.Compiler.Backend.Isabelle.Pretty
data PosTest = PosTest
{ _name :: String,
_dir :: Path Abs Dir,
_file :: Path Abs File,
_expectedFile :: Path Abs File
}
makeLenses ''PosTest
root :: Path Abs Dir
root = relToProject $(mkRelDir "tests/positive/Isabelle")
posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
posTest _name rdir rfile efile =
let _dir = root <//> rdir
_file = _dir <//> rfile
_expectedFile = _dir <//> efile
in PosTest {..}
testDescr :: PosTest -> TestDescr
testDescr PosTest {..} =
TestDescr
{ _testName = _name,
_testRoot = _dir,
_testAssertion = Steps $ \step -> do
entryPoint <- testDefaultEntryPointIO _dir _file
step "Translate"
PipelineResult {..} <- snd <$> testRunIO entryPoint upToIsabelle
let thy = _pipelineResult ^. resultTheory
step "Checking against expected output file"
expFile :: Text <- readFile _expectedFile
assertEqDiffText "Compare to expected output" (ppPrint thy <> "\n") expFile
}
allTests :: TestTree
allTests =
testGroup
"Isabelle positive tests"
(map (mkTest . testDescr) tests)
tests :: [PosTest]
tests =
[ posTest
"Test Isabelle translation"
$(mkRelDir ".")
$(mkRelFile "Program.juvix")
$(mkRelFile "isabelle/Program.thy")
]

2
test/Main.hs
View File

@ -11,6 +11,7 @@ import Examples qualified
import Format qualified
import Formatter qualified
import Internal qualified
import Isabelle qualified
import Nockma qualified
import Package qualified
import Parsing qualified
@ -60,6 +61,7 @@ fastTests =
Formatter.allTests,
Package.allTests,
BackendMarkdown.allTests,
Isabelle.allTests,
Nockma.allTests
]

8
tests/positive/Isabelle/Package.juvix Normal file
View File

@ -0,0 +1,8 @@
module Package;
import PackageDescription.V2 open;
package : Package :=
defaultPackage@?{
name := "isabelle"
};

97
tests/positive/Isabelle/Program.juvix Normal file
View File

@ -0,0 +1,97 @@
module Program;
import Stdlib.Prelude open;
id0 : Nat -> Nat := id;
id1 : List Nat -> List Nat := id;
id2 {A : Type} : A -> A := id;
add_one : List Nat -> List Nat
| [] := []
| (x :: xs) := (x + 1) :: add_one xs;
sum : List Nat -> Nat
| [] := 0
| (x :: xs) := x + sum xs;
f (x y : Nat) : Nat -> Nat
| z := (z + 1) * x + y;
g (x y : Nat) : Bool :=
if
| x == y := false
| else := true;
inc (x : Nat) : Nat := suc x;
dec : Nat -> Nat
| zero := zero
| (suc x) := x;
dec' (x : Nat) : Nat :=
case x of zero := zero | suc y := y;
optmap {A} (f : A -> A) : Maybe A -> Maybe A
| nothing := nothing
| (just x) := just (f x);
pboth {A B A' B'} (f : A -> A') (g : B -> B') : Pair A B -> Pair A' B'
| (x, y) := (f x, g y);
bool_fun (x y z : Bool) : Bool := x && y || z;
bool_fun' (x y z : Bool) : Bool := (x && y) || z;
-- Queues
--- A type of Queues
type Queue (A : Type) := queue : List A -> List A -> Queue A;
qfst : {A : Type} → Queue A → List A
| (queue x _) := x;
qsnd : {A : Type} → Queue A → List A
| (queue _ x) := x;
pop_front {A} (q : Queue A) : Queue A :=
let
q' : Queue A := queue (tail (qfst q)) (qsnd q);
in case qfst q' of
| nil := queue (reverse (qsnd q')) nil
| _ := q';
push_back {A} (q : Queue A) (x : A) : Queue A :=
case qfst q of
| nil := queue (x :: nil) (qsnd q)
| q' := queue q' (x :: qsnd q);
is_empty {A} (q : Queue A) : Bool :=
case qfst q of
| nil :=
case qsnd q of {
| nil := true
| _ := false
}
| _ := false;
empty : {A : Type} → Queue A := queue nil nil;
-- Multiple let expressions
funkcja (n : Nat) : Nat :=
let
nat1 : Nat := 1;
nat2 : Nat := 2;
plusOne (n : Nat) : Nat := n + 1;
in plusOne n + nat1 + nat2;
type Either' A B := Left' A | Right' B;
-- Records
type R := mkR {
r1 : Nat;
r2 : Nat;
};

112
tests/positive/Isabelle/isabelle/Program.thy Normal file
View File

@ -0,0 +1,112 @@
theory Program
imports Main
begin
definition id0 :: "nat ⇒ nat" where
"id0 = id"
definition id1 :: "nat list ⇒ nat list" where
"id1 = id"
definition id2 :: "'A ⇒ 'A" where
"id2 = id"
fun add_one :: "nat list ⇒ nat list" where
"add_one [] = []" |
"add_one (x # xs) = ((x + 1) # add_one xs)"
fun sum :: "nat list ⇒ nat" where
"sum [] = 0" |
"sum (x # xs) = (x + sum xs)"
fun f :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"f x y z = ((z + 1) * x + y)"
fun g :: "nat ⇒ nat ⇒ bool" where
"g x y = (if x = y then False else True)"
fun inc :: "nat ⇒ nat" where
"inc x = (Suc x)"
fun dec :: "nat ⇒ nat" where
"dec 0 = 0" |
"dec (Suc x) = x"
fun dec' :: "nat ⇒ nat" where
"dec' x =
(case x of
0 ⇒ 0 |
(Suc y) ⇒ y)"
fun optmap :: "('A ⇒ 'A) ⇒ 'A option ⇒ 'A option" where
"optmap f' None = None" |
"optmap f' (Some x) = (Some (f' x))"
fun pboth :: "('A ⇒ 'A') ⇒ ('B ⇒ 'B') ⇒ 'A × 'B ⇒ 'A' × 'B'" where
"pboth f' g' (x, y) = (f' x, g' y)"
fun bool_fun :: "bool ⇒ bool ⇒ bool ⇒ bool" where
"bool_fun x y z = (x ∧ (y ∨ z))"
fun bool_fun' :: "bool ⇒ bool ⇒ bool ⇒ bool" where
"bool_fun' x y z = (x ∧ y ∨ z)"
datatype 'A Queue
= queue "'A list" "'A list"
fun qfst :: "'A Queue ⇒ 'A list" where
"qfst (queue x ω) = x"
fun qsnd :: "'A Queue ⇒ 'A list" where
"qsnd (queue ω x) = x"
fun pop_front :: "'A Queue ⇒ 'A Queue" where
"pop_front q =
(let
q' = queue (tl (qfst q)) (qsnd q)
in case qfst q' of
[] ⇒ queue (rev (qsnd q')) [] |
ω ⇒ q')"
fun push_back :: "'A Queue ⇒ 'A ⇒ 'A Queue" where
"push_back q x =
(case qfst q of
[] ⇒ queue [x] (qsnd q) |
q' ⇒ queue q' (x # qsnd q))"
fun is_empty :: "'A Queue ⇒ bool" where
"is_empty q =
(case qfst q of
[] ⇒
(case qsnd q of
[] ⇒ True |
ω ⇒ False) |
ω ⇒ False)"
definition empty :: "'A Queue" where
"empty = queue [] []"
fun funkcja :: "nat ⇒ nat" where
"funkcja n =
(let
nat1 = 1;
nat2 = 2;
plusOne = λ x0 . case x0 of
n' ⇒ n' + 1
in plusOne n + nat1 + nat2)"
datatype ('A, 'B) Either'
= Left' 'A |
Right' 'B
record R =
r1 :: nat
r2 :: nat
fun r1 :: "R ⇒ nat" where
"r1 (mkR a b) = a"
fun r2 :: "R ⇒ nat" where
"r2 (mkR a b) = b"
end