anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2024-12-11 08:25:46 +03:00
Code Issues Projects Releases Wiki Activity

Remove NameId from Core (#1649)

Browse Source
This commit is contained in:
Łukasz Czajka 2022-12-08 10:50:14 +01:00 committed by GitHub
parent f5de5faaef
commit 468a980e66
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
25 changed files with 320 additions and 336 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/Juvix/Compiler/Asm/Pretty/Base.hs
View File

@ -7,6 +7,7 @@ where
import Data.Foldable
import Data.HashMap.Strict qualified as HashMap
import Data.List.NonEmpty qualified as NonEmpty
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Asm.Data.InfoTable
import Juvix.Compiler.Asm.Extra.Base
import Juvix.Compiler.Asm.Interpreter.Base

4
src/Juvix/Compiler/Asm/Translation/FromCore.hs
View File

@ -27,8 +27,8 @@ genCode infoTable fi =
)
(fi ^. Core.functionBody)
in FunctionInfo
{ _functionName = maybe "function" (^. nameText) (fi ^. Core.functionName),
_functionLocation = fmap (^. nameLoc) (fi ^. Core.functionName),
{ _functionName = fi ^. Core.functionName,
_functionLocation = fi ^. Core.functionLocation,
_functionSymbol = fi ^. Core.functionSymbol,
_functionArgsNum = fi ^. Core.functionArgsNum,
_functionType = convertType (fi ^. Core.functionArgsNum) (fi ^. Core.functionType),

20
src/Juvix/Compiler/Core/Data/InfoTable.hs
View File

@ -12,7 +12,7 @@ data InfoTable = InfoTable
_infoIdentifiers :: HashMap Symbol IdentifierInfo,
_infoInductives :: HashMap Symbol InductiveInfo,
_infoConstructors :: HashMap Tag ConstructorInfo,
_infoAxioms :: HashMap Name AxiomInfo,
_infoAxioms :: HashMap Text AxiomInfo,
_infoNextSymbol :: Word,
_infoNextTag :: Word
}
@ -37,7 +37,8 @@ data IdentKind
| IdentConstr Tag
data IdentifierInfo = IdentifierInfo
{ _identifierName :: Maybe Name,
{ _identifierName :: Text,
_identifierLocation :: Maybe Location,
_identifierSymbol :: Symbol,
_identifierType :: Type,
-- _identifierArgsNum will be used often enough to justify avoiding recomputation
@ -47,13 +48,15 @@ data IdentifierInfo = IdentifierInfo
}
data ArgumentInfo = ArgumentInfo
{ _argumentName :: Maybe Name,
{ _argumentName :: Text,
_argumentLocation :: Maybe Location,
_argumentType :: Type,
_argumentIsImplicit :: IsImplicit
}
data InductiveInfo = InductiveInfo
{ _inductiveName :: Name,
{ _inductiveName :: Text,
_inductiveLocation :: Maybe Location,
_inductiveSymbol :: Symbol,
_inductiveKind :: Type,
_inductiveConstructors :: [ConstructorInfo],
@ -62,7 +65,8 @@ data InductiveInfo = InductiveInfo
}
data ConstructorInfo = ConstructorInfo
{ _constructorName :: Name,
{ _constructorName :: Text,
_constructorLocation :: Maybe Location,
_constructorTag :: Tag,
_constructorType :: Type,
_constructorArgsNum :: Int,
@ -70,13 +74,15 @@ data ConstructorInfo = ConstructorInfo
}
data ParameterInfo = ParameterInfo
{ _paramName :: Name,
{ _paramName :: Text,
_paramLocation :: Maybe Location,
_paramKind :: Type,
_paramIsImplicit :: Bool
}
data AxiomInfo = AxiomInfo
{ _axiomName :: Name,
{ _axiomName :: Text,
_axiomLocation :: Maybe Location,
_axiomType :: Type
}

25
src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
View File

@ -8,9 +8,9 @@ import Juvix.Compiler.Core.Language
data InfoTableBuilder m a where
FreshSymbol :: InfoTableBuilder m Symbol
FreshTag :: InfoTableBuilder m Tag
RegisterIdent :: IdentifierInfo -> InfoTableBuilder m ()
RegisterConstructor :: ConstructorInfo -> InfoTableBuilder m ()
RegisterInductive :: InductiveInfo -> InfoTableBuilder m ()
RegisterIdent :: Text -> IdentifierInfo -> InfoTableBuilder m ()
RegisterConstructor :: Text -> ConstructorInfo -> InfoTableBuilder m ()
RegisterInductive :: Text -> InductiveInfo -> InfoTableBuilder m ()
RegisterIdentNode :: Symbol -> Node -> InfoTableBuilder m ()
RegisterMain :: Symbol -> InfoTableBuilder m ()
OverIdentArgsInfo :: Symbol -> ([ArgumentInfo] -> [ArgumentInfo]) -> InfoTableBuilder m ()
@ -19,8 +19,6 @@ data InfoTableBuilder m a where
makeSem ''InfoTableBuilder
type MkIdentIndex = Name -> Text
getConstructorInfo :: Member InfoTableBuilder r => Tag -> Sem r ConstructorInfo
getConstructorInfo tag = do
tab <- getInfoTable
@ -34,8 +32,8 @@ checkSymbolDefined sym = do
setIdentArgsInfo :: Member InfoTableBuilder r => Symbol -> [ArgumentInfo] -> Sem r ()
setIdentArgsInfo sym = overIdentArgsInfo sym . const
runInfoTableBuilder :: forall r a. MkIdentIndex -> InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
runInfoTableBuilder mkIdentIndex tab =
runInfoTableBuilder :: forall r a. InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
runInfoTableBuilder tab =
runState tab
. reinterpret interp
where
@ -49,16 +47,15 @@ runInfoTableBuilder mkIdentIndex tab =
s <- get
modify' (over infoNextTag (+ 1))
return (UserTag (s ^. infoNextTag))
RegisterIdent ii -> do
RegisterIdent idt ii -> do
modify' (over infoIdentifiers (HashMap.insert (ii ^. identifierSymbol) ii))
whenJust (ii ^? identifierName . _Just) $ \n ->
modify' (over identMap (HashMap.insert (mkIdentIndex n) (IdentFun (ii ^. identifierSymbol))))
RegisterConstructor ci -> do
modify' (over identMap (HashMap.insert idt (IdentFun (ii ^. identifierSymbol))))
RegisterConstructor idt ci -> do
modify' (over infoConstructors (HashMap.insert (ci ^. constructorTag) ci))
modify' (over identMap (HashMap.insert (mkIdentIndex (ci ^. constructorName)) (IdentConstr (ci ^. constructorTag))))
RegisterInductive ii -> do
modify' (over identMap (HashMap.insert idt (IdentConstr (ci ^. constructorTag))))
RegisterInductive idt ii -> do
modify' (over infoInductives (HashMap.insert (ii ^. inductiveSymbol) ii))
modify' (over identMap (HashMap.insert (mkIdentIndex (ii ^. inductiveName)) (IdentInd (ii ^. inductiveSymbol))))
modify' (over identMap (HashMap.insert idt (IdentInd (ii ^. inductiveSymbol))))
RegisterIdentNode sym node ->
modify' (over identContext (HashMap.insert sym node))
RegisterMain sym -> do

15
src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs
View File

@ -10,7 +10,8 @@ data InfoTable = InfoTable
}
data FunctionInfo = FunctionInfo
{ _functionName :: Maybe Name,
{ _functionName :: Text,
_functionLocation :: Maybe Location,
_functionSymbol :: Symbol,
-- _functionBody has `_functionArgsNum` free variables corresponding to the
-- function arguments
@ -23,25 +24,29 @@ data FunctionInfo = FunctionInfo
}
data ArgumentInfo = ArgumentInfo
{ _argumentName :: Maybe Name,
{ _argumentName :: Text,
_argumentLocation :: Maybe Location,
_argumentType :: Type
}
data InductiveInfo = InductiveInfo
{ _inductiveName :: Name,
{ _inductiveName :: Text,
_inductiveLocation :: Maybe Location,
_inductiveKind :: Type,
_inductiveConstructors :: [ConstructorInfo],
_inductiveParams :: [ParameterInfo]
}
data ConstructorInfo = ConstructorInfo
{ _constructorName :: Maybe Name,
{ _constructorName :: Text,
_constructorLocation :: Maybe Location,
_constructorTag :: Tag,
_constructorType :: Type
}
data ParameterInfo = ParameterInfo
{ _paramName :: Maybe Name,
{ _paramName :: Text,
_paramLocation :: Maybe Location,
_paramKind :: Type,
_paramIsImplicit :: Bool
}

12
src/Juvix/Compiler/Core/Extra.hs
View File

@ -20,8 +20,6 @@ import Juvix.Compiler.Core.Extra.Info
import Juvix.Compiler.Core.Extra.Recursors
import Juvix.Compiler.Core.Extra.Recursors.Fold.Named
import Juvix.Compiler.Core.Extra.Recursors.Map.Named
import Juvix.Compiler.Core.Info.NameInfo
import Juvix.Compiler.Core.Info.TypeInfo
import Juvix.Compiler.Core.Language
isClosed :: Node -> Bool
@ -190,15 +188,7 @@ argumentInfoFromBinder :: Binder -> ArgumentInfo
argumentInfoFromBinder i =
ArgumentInfo
{ _argumentName = i ^. binderName,
_argumentLocation = i ^. binderLocation,
_argumentType = i ^. binderType,
_argumentIsImplicit = Explicit
}
infoFromArgumentInfo :: ArgumentInfo -> Info
infoFromArgumentInfo arg =
setInfoType (arg ^. argumentType) $
setName
mempty
where
setName :: Info -> Info
setName i = maybe i (`setInfoName` i) (arg ^. argumentName)

11
src/Juvix/Compiler/Core/Extra/Base.hs
View File

@ -104,7 +104,7 @@ mkPi :: Info -> Binder -> Type -> Type
mkPi i bi b = NPi (Pi i bi b)
mkPi' :: Type -> Type -> Type
mkPi' = mkPi Info.empty . Binder Nothing
mkPi' = mkPi Info.empty . Binder "" Nothing
mkPis :: [Binder] -> Type -> Type
mkPis tys ty = foldr (mkPi mempty) ty tys
@ -301,7 +301,7 @@ data NodeDetails = NodeDetails
_nodeChildren :: [NodeChild],
-- | 'nodeReassemble' reassembles the node from the info, the subinfos and
-- the children (which should be in the same fixed order as in the
-- 'nodeSubinfos' and 'nodeChildren' component).
-- 'nodeSubinfos' and 'nodeChildren' components).
_nodeReassemble :: Info -> [Info] -> [NodeChild] -> Node
}
@ -465,12 +465,13 @@ destruct = \case
(values', tys') = second (map (^. childNode)) (splitAtExact numItems valuesTys')
items' =
nonEmpty'
[ LetItem (Binder name ty') (v' ^. childNode)
| (v', ty', name) <-
zip3Exact
[ LetItem (Binder name loc ty') (v' ^. childNode)
| (v', ty', name, loc) <-
zip4Exact
values'
tys'
(map (^. letItemBinder . binderName) (toList vs))
(map (^. letItemBinder . binderLocation) (toList vs))
]
in mkLetRec i' items' (b' ^. childNode)
}

5
src/Juvix/Compiler/Core/Extra/Info.hs
View File

@ -4,7 +4,6 @@ import Juvix.Compiler.Core.Extra.Base
import Juvix.Compiler.Core.Extra.Recursors
import Juvix.Compiler.Core.Info qualified as Info
import Juvix.Compiler.Core.Info.LocationInfo
import Juvix.Compiler.Core.Info.NameInfo
import Juvix.Compiler.Core.Language
mapInfo :: (Info -> Info) -> Node -> Node
@ -17,6 +16,4 @@ lookupLocation :: Node -> Maybe Location
lookupLocation node =
case Info.lookup kLocationInfo (getInfo node) of
Just li -> Just (li ^. infoLocation)
Nothing -> case Info.lookup kNameInfo (getInfo node) of
Just ni -> Just $ ni ^. (infoName . nameLoc)
Nothing -> Nothing
Nothing -> Nothing

9
src/Juvix/Compiler/Core/Extra/Stripped/Base.hs
View File

@ -9,13 +9,13 @@ mkVar :: VarInfo -> Index -> Node
mkVar i idx = NVar (Var i idx)
mkVar' :: Index -> Node
mkVar' = mkVar (VarInfo Nothing TyDynamic)
mkVar' = mkVar (VarInfo "" Nothing TyDynamic)
mkIdent :: IdentInfo -> Symbol -> Node
mkIdent i sym = NIdt (Ident i sym)
mkIdent' :: Symbol -> Node
mkIdent' = mkIdent (IdentInfo Nothing TyDynamic)
mkIdent' = mkIdent (IdentInfo "" Nothing TyDynamic)
mkConstant :: ConstantValue -> Node
mkConstant cv = NCst (Constant () cv)
@ -30,7 +30,7 @@ mkConstr :: ConstrInfo -> Tag -> [Node] -> Node
mkConstr i tag args = NCtr (Constr i tag args)
mkConstr' :: Symbol -> Tag -> [Node] -> Node
mkConstr' sym = mkConstr (ConstrInfo Nothing TyDynamic sym)
mkConstr' sym = mkConstr (ConstrInfo "" Nothing TyDynamic sym)
mkLet :: LetInfo -> Node -> Node -> Node
mkLet i v b = NLet (Let i item b)
@ -39,6 +39,7 @@ mkLet i v b = NLet (Let i item b)
binder =
Binder
{ _binderName = i ^. letInfoBinderName,
_binderLocation = i ^. letInfoBinderLocation,
_binderType = i ^. letInfoBinderType
}
item :: LetItem
@ -49,7 +50,7 @@ mkLet i v b = NLet (Let i item b)
}
mkLet' :: Node -> Node -> Node
mkLet' = mkLet (LetInfo Nothing TyDynamic)
mkLet' = mkLet (LetInfo "" Nothing TyDynamic)
mkCase :: CaseInfo -> Node -> [CaseBranch] -> Maybe Node -> Node
mkCase ci v bs def = NCase (Case ci v bs def)

10
src/Juvix/Compiler/Core/Info/LocationInfo.hs
View File

@ -1,5 +1,6 @@
module Juvix.Compiler.Core.Info.LocationInfo where
import Juvix.Compiler.Core.Info qualified as Info
import Juvix.Compiler.Core.Language.Base
newtype LocationInfo = LocationInfo {_infoLocation :: Location}
@ -10,3 +11,12 @@ kLocationInfo :: Key LocationInfo
kLocationInfo = Proxy
makeLenses ''LocationInfo
getInfoLocation :: Info -> Maybe Location
getInfoLocation i =
case Info.lookup kLocationInfo i of
Just LocationInfo {..} -> Just _infoLocation
Nothing -> Nothing
setInfoLocation :: Location -> Info -> Info
setInfoLocation = Info.insert . LocationInfo

10
src/Juvix/Compiler/Core/Info/NameInfo.hs
View File

@ -3,7 +3,7 @@ module Juvix.Compiler.Core.Info.NameInfo where
import Juvix.Compiler.Core.Info qualified as Info
import Juvix.Compiler.Core.Language.Base
newtype NameInfo = NameInfo {_infoName :: Name}
newtype NameInfo = NameInfo {_infoName :: Text}
instance IsInfo NameInfo
@ -12,11 +12,11 @@ kNameInfo = Proxy
makeLenses ''NameInfo
getInfoName :: Info -> Maybe Name
getInfoName :: Info -> Text
getInfoName i =
case Info.lookup kNameInfo i of
Just NameInfo {..} -> Just _infoName
Nothing -> Nothing
Just NameInfo {..} -> _infoName
Nothing -> "?"
setInfoName :: Name -> Info -> Info
setInfoName :: Text -> Info -> Info
setInfoName = Info.insert . NameInfo

3
src/Juvix/Compiler/Core/Language.hs
View File

@ -135,6 +135,7 @@ instance HasAtomicity Node where
emptyBinder :: Binder
emptyBinder =
Binder
{ _binderName = Nothing,
{ _binderName = "?",
_binderLocation = Nothing,
_binderType = NDyn (Dynamic mempty)
}

13
src/Juvix/Compiler/Core/Language/Base.hs
View File

@ -4,12 +4,10 @@ module Juvix.Compiler.Core.Language.Base
IsInfo,
module Juvix.Compiler.Core.Language.Builtins,
module Juvix.Prelude,
module Juvix.Compiler.Abstract.Data.Name,
module Juvix.Compiler.Core.Language.Base,
)
where
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Core.Info (Info, IsInfo, Key)
import Juvix.Compiler.Core.Language.Builtins
import Juvix.Prelude
@ -19,10 +17,13 @@ type Location = Interval
-- | Consecutive symbol IDs for reachable user functions.
type Symbol = Word
-- | Tag of a constructor, uniquely identifying it. Tag values are consecutive and
-- separate from symbol IDs. We might need fixed special tags in Core for common
-- "builtin" constructors, e.g., unit, nat, lists, pairs, so that the code
-- generator can treat them specially.
uniqueName :: Text -> Symbol -> Text
uniqueName txt sym = txt <> "_" <> show sym
-- | Tag of a constructor, uniquely identifying it. Tag values are consecutive
-- and separate from symbol IDs. We might need fixed special tags in Core for
-- common "builtin" constructors, e.g., unit, nat, so that the code generator
-- can treat them specially.
data Tag = BuiltinTag BuiltinDataTag | UserTag Word
deriving stock (Eq, Generic)

3
src/Juvix/Compiler/Core/Language/Nodes.hs
View File

@ -34,7 +34,8 @@ data ConstantValue
-- | Info about a single binder. Associated with Lambda and Pi.
data Binder' ty = Binder
{ _binderName :: Maybe Name,
{ _binderName :: Text,
_binderLocation :: Maybe Location,
_binderType :: ty
}

16
src/Juvix/Compiler/Core/Language/Stripped.hs
View File

@ -15,23 +15,27 @@ import Juvix.Compiler.Core.Language.Stripped.Type
{---------------------------------------------------------------------------------}
data VarInfo = VarInfo
{ _varInfoName :: Maybe Name,
{ _varInfoName :: Text,
_varInfoLocation :: Maybe Location,
_varInfoType :: Type -- TyDynamic if not available
}
data IdentInfo = IdentInfo
{ _identInfoName :: Maybe Name,
{ _identInfoName :: Text,
_identInfoLocation :: Maybe Location,
_identInfoType :: Type
}
data ConstrInfo = ConstrInfo
{ _constrInfoName :: Maybe Name,
{ _constrInfoName :: Text,
_constrInfoLocation :: Maybe Location,
_constrInfoType :: Type,
_constrInfoInductive :: Symbol
}
data LetInfo = LetInfo
{ _letInfoBinderName :: Maybe Name,
{ _letInfoBinderName :: Text,
_letInfoBinderLocation :: Maybe Location,
_letInfoBinderType :: Type
}
@ -40,9 +44,9 @@ newtype CaseInfo = CaseInfo
}
data CaseBranchInfo = CaseBranchInfo
{ _caseBranchInfoBinderNames :: [Maybe Name],
{ _caseBranchInfoBinderNames :: [Text],
_caseBranchInfoBinderTypes :: [Type],
_caseBranchInfoConstrName :: Maybe Name,
_caseBranchInfoConstrName :: Text,
_caseBranchInfoConstrType :: Type
}

3
src/Juvix/Compiler/Core/Language/Stripped/Type.hs
View File

@ -11,7 +11,8 @@ data Type
deriving stock (Eq)
data TypeApp = TypeApp
{ _typeAppName :: Maybe Name,
{ _typeAppName :: Text,
_typeAppLocation :: Maybe Location,
_typeAppSymbol :: Symbol,
_typeAppArgs :: [Type]
}

130
src/Juvix/Compiler/Core/Pretty/Base.hs
View File

@ -7,6 +7,7 @@ where
import Data.HashMap.Strict qualified as HashMap
import Data.Map.Strict qualified as Map
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Core.Data.BinderList as BL
import Juvix.Compiler.Core.Data.InfoTable
import Juvix.Compiler.Core.Data.Stripped.InfoTable qualified as Stripped
@ -30,14 +31,6 @@ class PrettyCode c where
runPrettyCode :: PrettyCode c => Options -> c -> Doc Ann
runPrettyCode opts = run . runReader opts . ppCode
instance PrettyCode NameId where
ppCode (NameId k) = return (pretty k)
instance PrettyCode Name where
ppCode n = do
showNameId <- asks (^. optShowNameIds)
return (prettyName showNameId n)
instance PrettyCode BuiltinOp where
ppCode = \case
OpIntAdd -> return primPlus
@ -71,22 +64,16 @@ instance PrettyCode Primitive where
PrimBool _ -> return $ annotate (AnnKind KNameInductive) (pretty ("bool" :: String))
PrimString -> return $ annotate (AnnKind KNameInductive) (pretty ("string" :: String))
ppCodeVar' :: Member (Reader Options) r => Maybe Name -> Var' i -> Sem r (Doc Ann)
ppCodeVar' name v =
case name of
Just nm -> do
showDeBruijn <- asks (^. optShowDeBruijnIndices)
n <- ppCode nm
if showDeBruijn
then return $ n <> kwDeBruijnVar <> pretty (v ^. varIndex)
else return n
Nothing -> return $ kwDeBruijnVar <> pretty (v ^. varIndex)
ppName :: NameKind -> Text -> Sem r (Doc Ann)
ppName kind name = return $ annotate (AnnKind kind) (pretty name)
ppCodeIdent' :: Member (Reader Options) r => Maybe Name -> Ident' i -> Sem r (Doc Ann)
ppCodeIdent' name idt =
case name of
Just nm -> ppCode nm
Nothing -> return $ kwUnnamedIdent <> pretty (idt ^. identSymbol)
ppCodeVar' :: Member (Reader Options) r => Text -> Var' i -> Sem r (Doc Ann)
ppCodeVar' name v = do
let name' = annotate (AnnKind KNameLocal) (pretty name)
showDeBruijn <- asks (^. optShowDeBruijnIndices)
if showDeBruijn || name == ""
then return $ name' <> kwDeBruijnVar <> pretty (v ^. varIndex)
else return name'
instance PrettyCode (Constant' i) where
ppCode = \case
@ -104,7 +91,7 @@ instance (PrettyCode a, HasAtomicity a) => PrettyCode (App' i a) where
instance PrettyCode Stripped.Fun where
ppCode = \case
Stripped.FunVar x -> ppCodeVar' (x ^. (varInfo . Stripped.varInfoName)) x
Stripped.FunIdent x -> ppCodeIdent' (x ^. (identInfo . Stripped.identInfoName)) x
Stripped.FunIdent x -> ppName KNameLocal (x ^. (identInfo . Stripped.identInfoName))
instance (PrettyCode f, PrettyCode a, HasAtomicity a) => PrettyCode (Apps' f i a) where
ppCode Apps {..} = do
@ -118,12 +105,12 @@ instance (PrettyCode a, HasAtomicity a) => PrettyCode (BuiltinApp' i a) where
op' <- ppCode _builtinAppOp
return $ foldl' (<+>) op' args'
ppCodeConstr' :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) => Maybe Name -> Constr' i a -> Sem r (Doc Ann)
ppCodeConstr' :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) => Text -> Constr' i a -> Sem r (Doc Ann)
ppCodeConstr' name c = do
args' <- mapM (ppRightExpression appFixity) (c ^. constrArgs)
n' <- case name of
Just nm -> ppCode nm
Nothing -> ppCode (c ^. constrTag)
n' <- case c ^. constrTag of
BuiltinTag tag -> ppCode tag
_ -> ppName KNameConstructor name
return $ foldl' (<+>) n' args'
instance (Pretty k, PrettyCode a) => PrettyCode (Map k a) where
@ -151,18 +138,16 @@ instance PrettyCode a => PrettyCode (BinderList a) where
return $ brackets (hsep $ punctuate "," m)
instance PrettyCode a => PrettyCode (Binder' a) where
ppCode (Binder mname ty) = do
name' <- case mname of
Nothing -> return "_"
Just n -> ppCode n
ppCode (Binder mname _ ty) = do
let name' = case mname of
"" -> "_"
_ -> mname
ty' <- ppCode ty
return (parens (name' <+> kwColon <+> ty'))
return (parens (pretty name' <+> kwColon <+> ty'))
ppCodeLet' :: (PrettyCode a, Member (Reader Options) r) => Maybe Name -> Maybe (Doc Ann) -> Let' i a ty -> Sem r (Doc Ann)
ppCodeLet' :: (PrettyCode a, Member (Reader Options) r) => Text -> Maybe (Doc Ann) -> Let' i a ty -> Sem r (Doc Ann)
ppCodeLet' name mty lt = do
n' <- case name of
Just nm -> ppCode nm
Nothing -> return kwQuestion
n' <- ppName KNameConstructor name
v' <- ppCode (lt ^. letItem . letItemValue)
b' <- ppCode (lt ^. letBody)
let tty = case mty of
@ -172,12 +157,11 @@ ppCodeLet' name mty lt = do
mempty
return $ kwLet <+> n' <> tty <+> kwAssign <+> v' <+> kwIn <> line <> b'
ppCodeCase' :: (PrettyCode a, Member (Reader Options) r) => [[Maybe Name]] -> [Maybe Name] -> Case' i bi a -> Sem r (Doc Ann)
ppCodeCase' :: (PrettyCode a, Member (Reader Options) r) => [[Text]] -> [Text] -> Case' i bi a -> Sem r (Doc Ann)
ppCodeCase' branchBinderNames branchTagNames Case {..} = do
let branchTags = map (^. caseBranchTag) _caseBranches
let branchBodies = map (^. caseBranchBody) _caseBranches
bns <- mapM (mapM (maybe (return kwQuestion) ppCode)) branchBinderNames
cns <- zipWithM (\tag -> maybe (ppCode tag) ppCode) branchTags branchTagNames
bns <- mapM (mapM (ppName KNameLocal)) branchBinderNames
cns <- mapM (ppName KNameConstructor) branchTagNames
v <- ppCode _caseValue
bs' <- sequence $ zipWith3Exact (\cn bn br -> ppCode br >>= \br' -> return $ foldl' (<+>) cn bn <+> kwAssign <+> br') cns bns branchBodies
bs'' <-
@ -194,9 +178,7 @@ instance PrettyCode PatternWildcard where
instance PrettyCode PatternBinder where
ppCode PatternBinder {..} = do
n <- case _patternBinder ^. binderName of
Just name -> ppCode name
Nothing -> return kwQuestion
n <- ppName KNameLocal (_patternBinder ^. binderName)
case _patternBinderPattern of
PatWildcard {} -> return n
_ -> do
@ -205,7 +187,7 @@ instance PrettyCode PatternBinder where
instance PrettyCode PatternConstr where
ppCode PatternConstr {..} = do
n <- maybe (ppCode _patternConstrTag) ppCode (getInfoName _patternConstrInfo)
n <- ppName KNameConstructor (getInfoName _patternConstrInfo)
args <- mapM (ppRightExpression appFixity) _patternConstrArgs
return $ foldl' (<+>) n args
@ -250,10 +232,7 @@ instance PrettyCode LetRec where
in kwLetRec <> nss <> line <> bss <> line <> kwIn <> line <> b'
where
getName :: Binder -> Sem r (Doc Ann)
getName i =
case i ^. binderName of
Just name -> ppCode name
Nothing -> return kwQuestion
getName i = ppName KNameLocal (i ^. binderName)
instance PrettyCode Node where
ppCode :: forall r. Member (Reader Options) r => Node -> Sem r (Doc Ann)
@ -263,7 +242,7 @@ instance PrettyCode Node where
in ppCodeVar' name x
NIdt x ->
let name = getInfoName (x ^. identInfo)
in ppCodeIdent' name x
in ppName KNameLocal name
NCst x -> ppCode x
NApp x -> ppCode x
NBlt x -> ppCode x
@ -272,15 +251,13 @@ instance PrettyCode Node where
in ppCodeConstr' name x
NLam (Lambda _ bi body) -> do
b <- ppCode body
lam <- case bi ^. binderName of
Just name -> do
n <- ppCode name
case bi ^. binderType of
NDyn {} -> return $ kwLambda <> n
ty -> do
tty <- ppCode ty
return $ kwLambda <> parens (n <+> kwColon <+> tty)
Nothing -> return $ kwLambda <> kwQuestion
lam <- do
n <- ppName KNameLocal (bi ^. binderName)
case bi ^. binderType of
NDyn {} -> return $ kwLambda <> n
ty -> do
tty <- ppCode ty
return $ kwLambda <> parens (n <+> kwColon <+> tty)
return (lam <+> b)
NLet x -> ppCode x
NRec l -> ppCode l
@ -299,24 +276,21 @@ instance PrettyCode Node where
NPi Pi {..} ->
let piType = _piBinder ^. binderType
in case _piBinder ^. binderName of
Just name -> do
n <- ppCode name
ty <- ppCode piType
b <- ppCode _piBody
return $ kwPi <+> n <+> kwColon <+> ty <> comma <+> b
Nothing -> do
"" -> do
ty <- ppLeftExpression funFixity piType
b <- ppRightExpression funFixity _piBody
return $ ty <+> kwArrow <+> b
name -> do
n <- ppName KNameLocal name
ty <- ppCode piType
b <- ppCode _piBody
return $ kwPi <+> n <+> kwColon <+> ty <> comma <+> b
NUniv Univ {..} ->
return $ kwType <+> pretty _univLevel
NPrim TypePrim {..} -> ppCode _typePrimPrimitive
NTyp TypeConstr {..} -> do
args' <- mapM (ppRightExpression appFixity) _typeConstrArgs
n' <-
case getInfoName _typeConstrInfo of
Just name -> ppCode name
Nothing -> return $ kwUnnamedIdent <> pretty _typeConstrSymbol
n' <- ppName KNameConstructor (getInfoName _typeConstrInfo)
return $ foldl' (<+>) n' args'
NDyn {} -> return kwDynamic
Closure env l@Lambda {} ->
@ -325,9 +299,7 @@ instance PrettyCode Node where
instance PrettyCode Stripped.TypeApp where
ppCode Stripped.TypeApp {..} = do
args' <- mapM (ppRightExpression appFixity) _typeAppArgs
n' <- case _typeAppName of
Just nm -> ppCode nm
Nothing -> return $ kwUnnamedIdent <> pretty _typeAppSymbol
n' <- ppName KNameLocal _typeAppName
return $ foldl' (<+>) n' args'
instance PrettyCode Stripped.TypeFun where
@ -350,7 +322,7 @@ instance PrettyCode Stripped.Node where
in ppCodeVar' name x
Stripped.NIdt x ->
let name = x ^. (identInfo . Stripped.identInfoName)
in ppCodeIdent' name x
in ppName KNameLocal name
Stripped.NCst x -> ppCode x
Stripped.NApp x -> ppCode x
Stripped.NBlt x -> ppCode x
@ -379,10 +351,10 @@ instance PrettyCode InfoTable where
where
ppDef :: Symbol -> Node -> Sem r (Doc Ann)
ppDef s n = do
let mname :: Maybe Name
mname = tbl ^? infoIdentifiers . at s . _Just . identifierName . _Just
mname' = over (_Just . namePretty) (\nm -> nm <> "!" <> prettyText s) mname
sym' <- maybe (return (pretty s)) ppCode mname'
let mname :: Text
mname = tbl ^. infoIdentifiers . at s . _Just . identifierName
mname' = (\nm -> nm <> "!" <> prettyText s) mname
sym' <- ppName KNameLocal mname'
body' <- ppCode n
return (kwDef <+> sym' <+> kwAssign <+> nest 2 body')
@ -398,8 +370,8 @@ instance PrettyCode Stripped.InfoTable where
return (vsep defs)
where
ppDef :: Symbol -> Stripped.FunctionInfo -> Sem r (Doc Ann)
ppDef s fi = do
sym' <- maybe (return (pretty s)) ppCode (fi ^. Stripped.functionName)
ppDef _ fi = do
sym' <- ppName KNameFunction (fi ^. Stripped.functionName)
body' <- ppCode (fi ^. Stripped.functionBody)
return (kwDef <+> sym' <+> kwAssign <+> body')

2
src/Juvix/Compiler/Core/Transformation/Base.hs
View File

@ -18,7 +18,7 @@ mapT f tab = tab {_identContext = HashMap.mapWithKey f (tab ^. identContext)}
mapT' :: (Symbol -> Node -> Sem (InfoTableBuilder ': r) Node) -> InfoTable -> Sem r InfoTable
mapT' f tab =
fmap fst $
runInfoTableBuilder (^. nameText) tab $
runInfoTableBuilder tab $
mapM_
(\(k, v) -> f k v >>= registerIdentNode k)
(HashMap.toList (tab ^. identContext))

10
src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
View File

@ -47,10 +47,13 @@ lambdaLiftNode aboveBl top =
argsInfo :: [ArgumentInfo]
argsInfo = map (argumentInfoFromBinder . snd) freevarsAssocs
f <- freshSymbol
let name = uniqueName "lambda" f
registerIdent
name
IdentifierInfo
{ _identifierSymbol = f,
_identifierName = Nothing,
_identifierName = name,
_identifierLocation = Nothing,
_identifierType = typeFromArgs argsInfo,
_identifierArgsNum = length allfreevars,
_identifierArgsInfo = argsInfo,
@ -103,11 +106,14 @@ lambdaLiftNode aboveBl top =
let topBody = captureFreeVars (map (first (^. varIndex)) recItemsFreeVars) b
argsInfo :: [ArgumentInfo]
argsInfo = map (argumentInfoFromBinder . snd) recItemsFreeVars
name = uniqueName (itemBinder ^. binderName) sym
registerIdentNode sym topBody
registerIdent
name
IdentifierInfo
{ _identifierSymbol = sym,
_identifierName = itemBinder ^. binderName,
_identifierName = name,
_identifierLocation = itemBinder ^. binderLocation,
_identifierType = typeFromArgs argsInfo,
_identifierArgsNum = length recItemsFreeVars,
_identifierArgsInfo = argsInfo,

1
src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
View File

@ -29,6 +29,7 @@ topEtaExpand info = run (mapT' go info)
toArgumentInfo pi =
ArgumentInfo
{ _argumentName = pi ^. piLhsBinder . binderName,
_argumentLocation = pi ^. piLhsBinder . binderLocation,
_argumentType = pi ^. piLhsBinder . binderType,
_argumentIsImplicit = Explicit
}

20
src/Juvix/Compiler/Core/Translation/Base.hs
View File

@ -1,20 +0,0 @@
module Juvix.Compiler.Core.Translation.Base where
import Juvix.Compiler.Core.Language
freshName ::
Member NameIdGen r =>
NameKind ->
Text ->
Interval ->
Sem r Name
freshName kind txt i = do
nid <- freshNameId
return $
Name
{ _nameText = txt,
_nameId = nid,
_nameKind = kind,
_namePretty = txt,
_nameLoc = i
}

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

@ -2,6 +2,7 @@ module Juvix.Compiler.Core.Translation.FromInternal where
import Data.HashMap.Strict qualified as HashMap
import Data.List.NonEmpty (fromList)
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Concrete.Data.Literal (LiteralLoc)
import Juvix.Compiler.Core.Data
import Juvix.Compiler.Core.Extra
@ -29,7 +30,7 @@ mkIdentIndex = show . (^. Internal.nameId . Internal.unNameId)
fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult
fromInternal i = do
(res, _) <- runInfoTableBuilder mkIdentIndex emptyInfoTable (runReader (i ^. InternalTyped.resultIdenTypes) f)
(res, _) <- runInfoTableBuilder emptyInfoTable (runReader (i ^. InternalTyped.resultIdenTypes) f)
return $
CoreResult
{ _coreResultTable = res,
@ -53,7 +54,6 @@ fromInternalExpression res exp = do
<$> runReader
(Internal.buildTable modules)
( runInfoTableBuilder
mkIdentIndex
(res ^. coreResultTable)
( runReader
(res ^. coreResultInternalTypedResult . InternalTyped.resultIdenTypes)
@ -115,14 +115,15 @@ goInductiveDef i = do
ctorInfos <- mapM (goConstructor sym) (i ^. Internal.inductiveConstructors)
let info =
InductiveInfo
{ _inductiveName = i ^. Internal.inductiveName,
{ _inductiveName = i ^. Internal.inductiveName . nameText,
_inductiveLocation = Just $ i ^. Internal.inductiveName . nameLoc,
_inductiveSymbol = sym,
_inductiveKind = mkDynamic',
_inductiveConstructors = ctorInfos,
_inductiveParams = [],
_inductivePositive = i ^. Internal.inductivePositive
}
registerInductive info
registerInductive (mkIdentIndex (i ^. Internal.inductiveName)) info
goConstructor ::
forall r.
@ -135,13 +136,14 @@ goConstructor sym ctor = do
ty <- ctorType
let info =
ConstructorInfo
{ _constructorName = ctor ^. Internal.inductiveConstructorName,
{ _constructorName = ctor ^. Internal.inductiveConstructorName . nameText,
_constructorLocation = Just $ ctor ^. Internal.inductiveConstructorName . nameLoc,
_constructorTag = tag,
_constructorType = ty,
_constructorArgsNum = length (ctor ^. Internal.inductiveConstructorParameters),
_constructorInductive = sym
}
registerConstructor info
registerConstructor (mkIdentIndex (ctor ^. Internal.inductiveConstructorName)) info
return info
where
mBuiltin :: Sem r (Maybe Internal.BuiltinConstructor)
@ -190,14 +192,15 @@ goFunctionDefIden (f, sym) = do
funTy <- runReader initIndexTable (goExpression (f ^. Internal.funDefType))
let info =
IdentifierInfo
{ _identifierName = Just (f ^. Internal.funDefName),
{ _identifierName = f ^. Internal.funDefName . nameText,
_identifierLocation = Just $ f ^. Internal.funDefName . nameLoc,
_identifierSymbol = sym,
_identifierType = funTy,
_identifierArgsNum = 0,
_identifierArgsInfo = [],
_identifierIsExported = False
}
registerIdent info
registerIdent (mkIdentIndex (f ^. Internal.funDefName)) info
when (f ^. Internal.funDefName . Internal.nameText == Str.main) (registerMain sym)
goFunctionDef ::
@ -277,14 +280,15 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
sym <- freshSymbol
let info =
InductiveInfo
{ _inductiveName = a ^. Internal.axiomName,
{ _inductiveName = a ^. Internal.axiomName . nameText,
_inductiveLocation = Just $ a ^. Internal.axiomName . nameLoc,
_inductiveSymbol = sym,
_inductiveKind = mkDynamic',
_inductiveConstructors = [],
_inductiveParams = [],
_inductivePositive = False
}
registerInductive info
registerInductive (mkIdentIndex (a ^. Internal.axiomName)) info
goAxiomDef ::
forall r.
@ -297,14 +301,15 @@ goAxiomDef a = case a ^. Internal.axiomBuiltin >>= builtinBody of
ty <- axiomType'
let info =
IdentifierInfo
{ _identifierName = Just (a ^. Internal.axiomName),
{ _identifierName = a ^. Internal.axiomName . nameText,
_identifierLocation = Just $ a ^. Internal.axiomName . nameLoc,
_identifierSymbol = sym,
_identifierType = ty,
_identifierArgsNum = 0,
_identifierArgsInfo = [],
_identifierIsExported = False
}
registerIdent info
registerIdent (mkIdentIndex (a ^. Internal.axiomName)) info
registerIdentNode sym body
Nothing -> return ()
where
@ -339,7 +344,7 @@ fromPattern ::
Sem r Pattern
fromPattern = \case
Internal.PatternWildcard {} -> return wildcard
Internal.PatternVariable n -> return $ PatBinder (PatternBinder (Binder (Just n) mkDynamic') wildcard)
Internal.PatternVariable n -> return $ PatBinder (PatternBinder (Binder (n ^. nameText) (Just (n ^. nameLoc)) mkDynamic') wildcard)
Internal.PatternConstructorApp c -> do
let n = c ^. Internal.constrAppConstructor
explicitPatterns =
@ -347,11 +352,10 @@ fromPattern = \case
<$> filter
isExplicit
(c ^. Internal.constrAppParameters)
args <- mapM fromPattern explicitPatterns
m <- getIdent identIndex
case m of
Just (IdentConstr tag) -> return $ PatConstr (PatternConstr (setInfoName n Info.empty) tag args)
Just (IdentConstr tag) -> return $ PatConstr (PatternConstr (setInfoLocation (n ^. nameLoc) (setInfoName (n ^. nameText) Info.empty)) tag args)
Just _ -> error ("internal to core: not a constructor " <> txt)
Nothing -> error ("internal to core: undeclared identifier: " <> txt)
where
@ -364,6 +368,19 @@ fromPattern = \case
wildcard :: Pattern
wildcard = PatWildcard (PatternWildcard Info.empty)
getPatternVars :: Internal.Pattern -> [Name]
getPatternVars = \case
Internal.PatternWildcard {} -> []
Internal.PatternVariable n -> [n]
Internal.PatternConstructorApp c ->
concatMap getPatternVars explicitPatterns
where
explicitPatterns =
(^. Internal.patternArgPattern)
<$> filter
isExplicit
(c ^. Internal.constrAppParameters)
goPatterns ::
forall r.
Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r =>
@ -374,15 +391,15 @@ goPatterns body ps = do
vars <- asks (^. indexTableVars)
varsNum <- asks (^. indexTableVarsNum)
pats <- patterns
let bs :: [Binder]
bs = concatMap getPatternBinders pats
let bs :: [Name]
bs = concatMap getPatternVars (reverse ps)
(vars', varsNum') =
foldl'
( \(vs, k) name ->
(HashMap.insert (name ^. nameId) k vs, k + 1)
)
(vars, varsNum)
(map (fromJust . (^. binderName)) bs)
bs
body' :: Sem r Node
body' =
local
@ -452,30 +469,30 @@ goExpression' = \case
Internal.IdenVar n -> do
k <- HashMap.lookupDefault impossible id_ <$> asks (^. indexTableVars)
varsNum <- asks (^. indexTableVarsNum)
return (mkVar (Info.singleton (NameInfo n)) (varsNum - k - 1))
return (mkVar (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) (varsNum - k - 1))
Internal.IdenFunction n -> do
m <- getIdent identIndex
return $ case m of
Just (IdentFun sym) -> mkIdent (Info.singleton (NameInfo n)) sym
Just (IdentFun sym) -> mkIdent (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) sym
Just _ -> error ("internal to core: not a function: " <> txt)
Nothing -> error ("internal to core: undeclared identifier: " <> txt)
Internal.IdenInductive n -> do
m <- getIdent identIndex
return $ case m of
Just (IdentInd sym) -> mkTypeConstr (Info.singleton (NameInfo n)) sym []
Just (IdentInd sym) -> mkTypeConstr (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) sym []
Just _ -> error ("internal to core: not an inductive: " <> txt)
Nothing -> error ("internal to core: undeclared identifier: " <> txt)
Internal.IdenConstructor n -> do
m <- getIdent identIndex
case m of
Just (IdentConstr tag) -> return (mkConstr (Info.singleton (NameInfo n)) tag [])
Just (IdentConstr tag) -> return (mkConstr (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) tag [])
Just _ -> error ("internal to core: not a constructor " <> txt)
Nothing -> error ("internal to core: undeclared identifier: " <> txt)
Internal.IdenAxiom n -> do
m <- getIdent identIndex
return $ case m of
Just (IdentFun sym) -> mkIdent (Info.singleton (NameInfo n)) sym
Just (IdentInd sym) -> mkTypeConstr (Info.singleton (NameInfo n)) sym []
Just (IdentFun sym) -> mkIdent (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) sym
Just (IdentInd sym) -> mkTypeConstr (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) sym []
Just _ -> error ("internal to core: not an axiom: " <> txt)
Nothing -> error ("internal to core: undeclared identifier: " <> txt)
where
@ -503,7 +520,7 @@ goFunction (params, returnTypeExpr) = foldr f (goExpression returnTypeExpr) para
where
f :: Internal.FunctionParameter -> Sem r Node -> Sem r Node
f param acc = do
paramBinder <- Binder (param ^. Internal.paramName) <$> goExpression (param ^. Internal.paramType)
paramBinder <- Binder (maybe "" (^. nameText) $ param ^. Internal.paramName) (fmap (^. nameLoc) $ param ^. Internal.paramName) <$> goExpression (param ^. Internal.paramType)
case param ^. Internal.paramName of
Nothing -> mkPi mempty paramBinder <$> acc
Just vn -> mkPi mempty paramBinder <$> localAddName vn acc

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

@ -1,6 +1,7 @@
module Juvix.Compiler.Core.Translation.FromInternal.Data.IndexTable where
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Core.Language
data IndexTable = IndexTable

260
src/Juvix/Compiler/Core/Translation/FromSource.hs
View File

@ -17,7 +17,6 @@ import Juvix.Compiler.Core.Info.LocationInfo as LocationInfo
import Juvix.Compiler.Core.Info.NameInfo as NameInfo
import Juvix.Compiler.Core.Language
import Juvix.Compiler.Core.Transformation.Eta
import Juvix.Compiler.Core.Translation.Base
import Juvix.Compiler.Core.Translation.FromSource.Lexer
import Juvix.Parser.Error
import Text.Megaparsec qualified as P
@ -26,14 +25,12 @@ parseText :: InfoTable -> Text -> Either ParserError (InfoTable, Maybe Node)
parseText = runParser ""
-- | Note: only new symbols and tags that are not in the InfoTable already will be
-- generated during parsing, but nameIds are generated starting from 0
-- regardless of the names already in the InfoTable
-- generated during parsing
runParser :: FilePath -> InfoTable -> Text -> Either ParserError (InfoTable, Maybe Node)
runParser fileName tab input =
case run $
runInfoTableBuilder (^. nameText) tab $
runNameIdGen $
P.runParserT parseToplevel fileName input of
runInfoTableBuilder tab $
P.runParserT parseToplevel fileName input of
(_, Left err) -> Left (ParserError err)
(tbl, Right r) -> Right (tbl, r)
@ -47,7 +44,6 @@ guardSymbolNotDefined sym err = do
when b err
createBuiltinConstr ::
Member NameIdGen r =>
Symbol ->
BuiltinDataTag ->
Text ->
@ -55,11 +51,11 @@ createBuiltinConstr ::
Interval ->
Sem r ConstructorInfo
createBuiltinConstr sym btag nameTxt ty i = do
name <- freshName KNameConstructor nameTxt i
let n = builtinConstrArgsNum btag
return $
ConstructorInfo
{ _constructorName = name,
{ _constructorName = nameTxt,
_constructorLocation = Just i,
_constructorTag = BuiltinTag btag,
_constructorType = ty,
_constructorArgsNum = n,
@ -67,7 +63,7 @@ createBuiltinConstr sym btag nameTxt ty i = do
}
declareInductiveBuiltins ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Text ->
[(BuiltinDataTag, Text, Type -> Type)] ->
ParsecS r ()
@ -77,11 +73,12 @@ declareInductiveBuiltins indName ctrs = do
sym <- lift freshSymbol
let ty = mkIdent' sym
constrs <- lift $ mapM (\(tag, name, fty) -> createBuiltinConstr sym tag name (fty ty) i) ctrs
ioname <- lift $ freshName KNameInductive indName i
lift $
registerInductive
indName
( InductiveInfo
{ _inductiveName = ioname,
{ _inductiveName = indName,
_inductiveLocation = Just i,
_inductiveSymbol = sym,
_inductiveKind = mkDynamic',
_inductiveConstructors = constrs,
@ -89,9 +86,9 @@ declareInductiveBuiltins indName ctrs = do
_inductiveParams = []
}
)
lift $ mapM_ registerConstructor constrs
lift $ mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) constrs
declareIOBuiltins :: Members '[InfoTableBuilder, NameIdGen] r => ParsecS r ()
declareIOBuiltins :: Member InfoTableBuilder r => ParsecS r ()
declareIOBuiltins =
declareInductiveBuiltins
"IO"
@ -101,7 +98,7 @@ declareIOBuiltins =
(TagReadLn, "readLn", id)
]
declareBoolBuiltins :: Members '[InfoTableBuilder, NameIdGen] r => ParsecS r ()
declareBoolBuiltins :: Member InfoTableBuilder r => ParsecS r ()
declareBoolBuiltins =
declareInductiveBuiltins
"bool"
@ -110,7 +107,7 @@ declareBoolBuiltins =
]
parseToplevel ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
ParsecS r (Maybe Node)
parseToplevel = do
declareIOBuiltins
@ -122,12 +119,12 @@ parseToplevel = do
return r
statement ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
ParsecS r ()
statement = statementDef <|> statementInductive
statementDef ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
ParsecS r ()
statementDef = do
kw kwDef
@ -150,22 +147,22 @@ statementDef = do
Nothing -> do
mty <- optional typeAnnotation
sym <- lift freshSymbol
name <- lift $ freshName KNameFunction txt i
let ty = fromMaybe mkDynamic' mty
info =
IdentifierInfo
{ _identifierName = Just name,
{ _identifierName = txt,
_identifierLocation = Just i,
_identifierSymbol = sym,
_identifierType = ty,
_identifierArgsNum = 0,
_identifierArgsInfo = [],
_identifierIsExported = False
}
lift $ registerIdent info
lift $ registerIdent txt info
void $ optional (parseDefinition sym ty)
parseDefinition ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Symbol ->
Type ->
ParsecS r ()
@ -186,12 +183,13 @@ parseDefinition sym ty = do
toArgumentInfo bi =
ArgumentInfo
{ _argumentName = bi ^. binderName,
_argumentLocation = bi ^. binderLocation,
_argumentType = bi ^. binderType,
_argumentIsImplicit = Explicit
}
statementInductive ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
ParsecS r ()
statementInductive = do
kw kwInductive
@ -202,22 +200,22 @@ statementInductive = do
parseFailure off ("duplicate identifier: " ++ fromText txt)
mty <- optional typeAnnotation
sym <- lift freshSymbol
name <- lift $ freshName KNameConstructor txt i
let ii =
InductiveInfo
{ _inductiveName = name,
{ _inductiveName = txt,
_inductiveLocation = Just i,
_inductiveSymbol = sym,
_inductiveKind = fromMaybe (mkUniv' 0) mty,
_inductiveConstructors = [],
_inductiveParams = [],
_inductivePositive = True
}
lift $ registerInductive ii
lift $ registerInductive txt ii
ctrs <- braces $ P.sepEndBy (constrDecl sym) (kw kwSemicolon)
lift $ registerInductive ii {_inductiveConstructors = ctrs}
lift $ registerInductive txt ii {_inductiveConstructors = ctrs}
constrDecl ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Symbol ->
ParsecS r ConstructorInfo
constrDecl symInd = do
@ -228,27 +226,27 @@ constrDecl symInd = do
parseFailure off ("duplicate identifier: " ++ fromText txt)
tag <- lift freshTag
ty <- typeAnnotation
name <- lift $ freshName KNameConstructor txt i
let ci =
ConstructorInfo
{ _constructorName = name,
{ _constructorName = txt,
_constructorLocation = Just i,
_constructorTag = tag,
_constructorArgsNum = length (typeArgs ty),
_constructorType = ty,
_constructorInductive = symInd
}
lift $ registerConstructor ci
lift $ registerConstructor txt ci
return ci
typeAnnotation ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
ParsecS r Type
typeAnnotation = do
kw kwColon
expression
expression ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
ParsecS r Node
expression = do
node <- expr 0 mempty
@ -256,7 +254,7 @@ expression = do
return $ etaExpandApps tab node
expr ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
-- | current de Bruijn index, i.e., the number of binders upwards
Index ->
-- | reverse de Bruijn indices (de Bruijn levels)
@ -265,21 +263,21 @@ expr ::
expr varsNum vars = typeExpr varsNum vars
bracedExpr ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
bracedExpr varsNum vars = braces (expr varsNum vars) <|> expr varsNum vars
typeExpr ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
typeExpr varsNum vars = ioExpr varsNum vars >>= typeExpr' varsNum vars
typeExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -289,7 +287,7 @@ typeExpr' varsNum vars node =
<|> return node
typeFunExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -300,14 +298,14 @@ typeFunExpr' varsNum vars l = do
return $ mkPi' l r
ioExpr ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
ioExpr varsNum vars = cmpExpr varsNum vars >>= ioExpr' varsNum vars
ioExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -318,7 +316,7 @@ ioExpr' varsNum vars node =
<|> return node
bindExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -329,7 +327,7 @@ bindExpr' varsNum vars node = do
ioExpr' varsNum vars (mkConstr Info.empty (BuiltinTag TagBind) [node, node'])
seqExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -337,22 +335,21 @@ seqExpr' ::
seqExpr' varsNum vars node = do
((), i) <- interval (kw kwSeq)
node' <- cmpExpr (varsNum + 1) vars
name <- lift $ freshName KNameLocal "_" i
ioExpr' varsNum vars $
mkConstr
Info.empty
(BuiltinTag TagBind)
[node, mkLambda mempty (Binder (Just name) mkDynamic') node']
[node, mkLambda mempty (Binder "_" (Just i) mkDynamic') node']
cmpExpr ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
cmpExpr varsNum vars = arithExpr varsNum vars >>= cmpExpr' varsNum vars
cmpExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -366,7 +363,7 @@ cmpExpr' varsNum vars node =
<|> return node
eqExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -377,7 +374,7 @@ eqExpr' varsNum vars node = do
return $ mkBuiltinApp' OpEq [node, node']
ltExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -388,7 +385,7 @@ ltExpr' varsNum vars node = do
return $ mkBuiltinApp' OpIntLt [node, node']
leExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -399,7 +396,7 @@ leExpr' varsNum vars node = do
return $ mkBuiltinApp' OpIntLe [node, node']
gtExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -410,7 +407,7 @@ gtExpr' varsNum vars node = do
return $ mkBuiltinApp' OpIntLt [node', node]
geExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -421,14 +418,14 @@ geExpr' varsNum vars node = do
return $ mkBuiltinApp' OpIntLe [node', node]
arithExpr ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
arithExpr varsNum vars = factorExpr varsNum vars >>= arithExpr' varsNum vars
arithExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -439,7 +436,7 @@ arithExpr' varsNum vars node =
<|> return node
plusExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -450,7 +447,7 @@ plusExpr' varsNum vars node = do
arithExpr' varsNum vars (mkBuiltinApp' OpIntAdd [node, node'])
minusExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -461,14 +458,14 @@ minusExpr' varsNum vars node = do
arithExpr' varsNum vars (mkBuiltinApp' OpIntSub [node, node'])
factorExpr ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
factorExpr varsNum vars = appExpr varsNum vars >>= factorExpr' varsNum vars
factorExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -480,7 +477,7 @@ factorExpr' varsNum vars node =
<|> return node
mulExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -491,7 +488,7 @@ mulExpr' varsNum vars node = do
factorExpr' varsNum vars (mkBuiltinApp' OpIntMul [node, node'])
divExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -502,7 +499,7 @@ divExpr' varsNum vars node = do
factorExpr' varsNum vars (mkBuiltinApp' OpIntDiv [node, node'])
modExpr' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
Node ->
@ -513,14 +510,14 @@ modExpr' varsNum vars node = do
factorExpr' varsNum vars (mkBuiltinApp' OpIntMod [node, node'])
appExpr ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
appExpr varsNum vars = builtinAppExpr varsNum vars <|> atoms varsNum vars
builtinAppExpr ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
@ -539,7 +536,7 @@ builtinAppExpr varsNum vars = do
return $ mkBuiltinApp' op args
atoms ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
@ -548,7 +545,7 @@ atoms varsNum vars = do
return $ mkApps' (head es) (NonEmpty.tail es)
atom ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
@ -587,48 +584,43 @@ exprUniverse = do
exprDynamic :: ParsecS r Type
exprDynamic = kw kwAny $> mkDynamic'
parseLocalName ::
forall r.
Members '[InfoTableBuilder, NameIdGen] r =>
ParsecS r Name
parseLocalName :: ParsecS r (Text, Location)
parseLocalName = parseWildcardName <|> parseIdentName
where
parseWildcardName :: ParsecS r Name
parseWildcardName :: ParsecS r (Text, Location)
parseWildcardName = do
((), i) <- interval (kw kwWildcard)
lift $ freshName KNameLocal "_" i
return ("_", i)
parseIdentName :: ParsecS r Name
parseIdentName = do
(txt, i) <- identifierL
lift $ freshName KNameLocal txt i
parseIdentName :: ParsecS r (Text, Location)
parseIdentName = identifierL
exprPi ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
exprPi varsNum vars = do
kw kwPi
name <- parseLocalName
(name, loc) <- parseLocalName
kw kwColon
ty <- expr varsNum vars
kw kwComma
let vars' = HashMap.insert (name ^. nameText) varsNum vars
bi = Binder (Just name) ty
let vars' = HashMap.insert name varsNum vars
bi = Binder name (Just loc) ty
body <- expr (varsNum + 1) vars'
return $ mkPi mempty bi body
exprLambda ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
exprLambda varsNum vars = do
lambda
(name, mty) <- lambdaName
let vars' = HashMap.insert (name ^. nameText) varsNum vars
bi = Binder (Just name) (fromMaybe mkDynamic' mty)
((name, loc), mty) <- lambdaName
let vars' = HashMap.insert name varsNum vars
bi = Binder name (Just loc) (fromMaybe mkDynamic' mty)
body <- bracedExpr (varsNum + 1) vars'
return $ mkLambda mempty bi body
where
@ -643,24 +635,24 @@ exprLambda varsNum vars = do
<|> (\n -> (n, Nothing)) <$> parseLocalName
exprLetrecOne ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
exprLetrecOne varsNum vars = do
kw kwLetRec
name <- parseLocalName
(name, loc) <- parseLocalName
kw kwAssign
let vars' = HashMap.insert (name ^. nameText) varsNum vars
let vars' = HashMap.insert name varsNum vars
value <- bracedExpr (varsNum + 1) vars'
kw kwIn
body <- bracedExpr (varsNum + 1) vars'
let item :: LetItem
item = LetItem (Binder (Just name) mkDynamic') value
item = LetItem (Binder name (Just loc) mkDynamic') value
return $ mkLetRec mempty (pure item) body
exprLetrecMany ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
@ -680,7 +672,7 @@ letrecNames = P.between (symbol "[") (symbol "]") (NonEmpty.some identifier)
letrecDefs ::
forall r.
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
NonEmpty Text ->
Index ->
HashMap Text Level ->
@ -693,43 +685,41 @@ letrecDefs names varsNum vars = forM names letrecItem
(txt, i) <- identifierL
when (n /= txt) $
parseFailure off "identifier name doesn't match letrec signature"
name <- lift $ freshName KNameLocal txt i
kw kwAssign
v <- bracedExpr varsNum vars
kw kwSemicolon
return $ LetItem (Binder (Just name) mkDynamic') v
return $ LetItem (Binder txt (Just i) mkDynamic') v
letrecDef ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r (Name, Node)
ParsecS r (Text, Location, Node)
letrecDef varsNum vars = do
(txt, i) <- identifierL
name <- lift $ freshName KNameLocal txt i
kw kwAssign
v <- bracedExpr varsNum vars
return (name, v)
return (txt, i, v)
exprLet ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
exprLet varsNum vars = do
kw kwLet
name <- parseLocalName
(name, loc) <- parseLocalName
mty <- optional (kw kwColon >> expr varsNum vars)
kw kwAssign
value <- bracedExpr varsNum vars
kw kwIn
let vars' = HashMap.insert (name ^. nameText) varsNum vars
binder = Binder (Just name) (fromMaybe mkDynamic' mty)
let vars' = HashMap.insert name varsNum vars
binder = Binder name (Just loc) (fromMaybe mkDynamic' mty)
body <- bracedExpr (varsNum + 1) vars'
return $ mkLet mempty binder value body
exprCase ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
@ -742,7 +732,7 @@ exprCase varsNum vars = do
<|> exprCase' off value varsNum vars
exprCase' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Int ->
Node ->
Index ->
@ -761,7 +751,7 @@ exprCase' off value varsNum vars = do
parseFailure off "multiple default branches"
caseBranchP ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r (Either CaseBranch Node)
@ -770,7 +760,7 @@ caseBranchP varsNum vars =
<|> (caseMatchingBranch varsNum vars <&> Left)
caseDefaultBranch ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
@ -780,7 +770,7 @@ caseDefaultBranch varsNum vars = do
bracedExpr varsNum vars
caseMatchingBranch ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r CaseBranch
@ -794,7 +784,7 @@ caseMatchingBranch varsNum vars = do
Just IdentInd {} ->
parseFailure off ("not a constructor: " ++ fromText txt)
Just (IdentConstr tag) -> do
ns :: [Name] <- P.many parseLocalName
ns :: [(Text, Location)] <- P.many parseLocalName
let bindersNum = length ns
ci <- lift $ getConstructorInfo tag
when
@ -804,20 +794,20 @@ caseMatchingBranch varsNum vars = do
let vars' =
fst $
foldl'
( \(vs, k) name ->
(HashMap.insert (name ^. nameText) k vs, k + 1)
( \(vs, k) (name, _) ->
(HashMap.insert name k vs, k + 1)
)
(vars, varsNum)
ns
br <- bracedExpr (varsNum + bindersNum) vars'
let info = setInfoName (ci ^. constructorName) mempty
binders = [Binder (Just name) mkDynamic' | name <- ns]
binders = [Binder name (Just loc) mkDynamic' | (name, loc) <- ns]
return $ CaseBranch info tag binders bindersNum br
Nothing ->
parseFailure off ("undeclared identifier: " ++ fromText txt)
exprIf ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
@ -831,7 +821,7 @@ exprIf varsNum vars = do
return $ mkIf Info.empty value br1 br2
exprMatch ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
@ -843,7 +833,7 @@ exprMatch varsNum vars = do
<|> exprMatch' values varsNum vars
exprMatch' ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
[Node] ->
Index ->
HashMap Text Level ->
@ -853,7 +843,7 @@ exprMatch' values varsNum vars = do
return $ mkMatch' (fromList values) bs
matchBranch ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Int ->
Index ->
HashMap Text Level ->
@ -869,15 +859,15 @@ matchBranch patsNum varsNum vars = do
(vars', varsNum') =
foldl'
( \(vs, k) name ->
(HashMap.insert (name ^. nameText) k vs, k + 1)
(HashMap.insert name k vs, k + 1)
)
(vars, varsNum)
(map (fromJust . (^. binderName)) pis)
(map (^. binderName) pis)
br <- bracedExpr varsNum' vars'
return $ MatchBranch Info.empty (fromList pats) br
branchPattern ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
ParsecS r Pattern
branchPattern =
wildcardPattern
@ -890,7 +880,7 @@ wildcardPattern = do
return $ PatWildcard (PatternWildcard Info.empty)
binderOrConstrPattern ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Bool ->
ParsecS r Pattern
binderOrConstrPattern parseArgs = do
@ -907,14 +897,13 @@ binderOrConstrPattern parseArgs = do
let info = setInfoName (ci ^. constructorName) Info.empty
return $ PatConstr (PatternConstr info tag ps)
_ -> do
n <- lift $ freshName KNameLocal txt i
mp <- optional binderPattern
let pat = fromMaybe (PatWildcard (PatternWildcard Info.empty)) mp
binder = Binder (Just n) mkDynamic'
binder = Binder txt (Just i) mkDynamic'
return $ PatBinder (PatternBinder binder pat)
binderPattern ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
ParsecS r Pattern
binderPattern = do
symbolAt
@ -923,7 +912,7 @@ binderPattern = do
<|> parens branchPattern
exprNamed ::
Members '[InfoTableBuilder, NameIdGen] r =>
Member InfoTableBuilder r =>
Index ->
HashMap Text Level ->
ParsecS r Node
@ -933,21 +922,18 @@ exprNamed varsNum vars = do
case txt of
"int" -> return mkTypeInteger'
"string" -> return mkTypeString'
_ -> case HashMap.lookup txt vars of
Just k -> do
name <- lift $ freshName KNameLocal txt i
return $ mkVar (Info.singleton (NameInfo name)) (varsNum - k - 1)
Nothing -> do
r <- lift (getIdent txt)
case r of
Just (IdentFun sym) -> do
name <- lift $ freshName KNameFunction txt i
return $ mkIdent (Info.singleton (NameInfo name)) sym
Just (IdentInd sym) -> do
name <- lift $ freshName KNameConstructor txt i
return $ mkTypeConstr (Info.singleton (NameInfo name)) sym []
Just (IdentConstr tag) -> do
name <- lift $ freshName KNameConstructor txt i
return $ mkConstr (Info.singleton (NameInfo name)) tag []
Nothing ->
parseFailure off ("undeclared identifier: " ++ fromText txt)
_ ->
case HashMap.lookup txt vars of
Just k -> do
return $ mkVar (Info.insert (LocationInfo i) (Info.singleton (NameInfo txt))) (varsNum - k - 1)
Nothing -> do
r <- lift (getIdent txt)
case r of
Just (IdentFun sym) -> do
return $ mkIdent (Info.insert (LocationInfo i) (Info.singleton (NameInfo txt))) sym
Just (IdentInd sym) -> do
return $ mkTypeConstr (Info.insert (LocationInfo i) (Info.singleton (NameInfo txt))) sym []
Just (IdentConstr tag) -> do
return $ mkConstr (Info.insert (LocationInfo i) (Info.singleton (NameInfo txt))) tag []
Nothing ->
parseFailure off ("undeclared identifier: " ++ fromText txt)

5
src/Juvix/Prelude/Base.hs
View File

@ -260,6 +260,11 @@ commonPrefix a b = reverse (go [] a b)
| x' == y' -> go (x' : ac) xs ys
_ -> ac
zip4Exact :: [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
zip4Exact [] [] [] [] = []
zip4Exact (x1 : t1) (x2 : t2) (x3 : t3) (x4 : t4) = (x1, x2, x3, x4) : zip4Exact t1 t2 t3 t4
zip4Exact _ _ _ _ = error "zip4Exact"
--------------------------------------------------------------------------------
-- NonEmpty
--------------------------------------------------------------------------------