mirror of
https://github.com/anoma/juvix.git
synced 2024-12-03 09:41:10 +03:00
Store source location of (almost) everything (#2174)
- Closes #2162 This pr improves formatting of source files with comments. The concrete ast now stores location information of almost all keywords. We do not store location information of parentheses. Comments will be pushed out of parentheses by the formatter. E.g. ``` ( -- comment f x) ``` will become ``` -- comment (f x) ``` This only occurs if the comment appears just after the `(`. So the following will be respected ``` (f --comment x) ``` --------- Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
This commit is contained in:
Jan Mas Rovira
GitHub
parent
216c1cd0e8
commit
b7b0e1039e
@ -23,9 +23,9 @@ full _ := fail "full";
|
||||
|
||||
diagonals : List (List Square) → List (List Square);
|
||||
diagonals ((a1 :: _ :: b1 :: nil)
|
||||
:: (_ :: c :: _ :: nil)
|
||||
:: (b2 :: _ :: a2 :: nil)
|
||||
:: nil) :=
|
||||
:: (_ :: c :: _ :: nil)
|
||||
:: (b2 :: _ :: a2 :: nil)
|
||||
:: nil) :=
|
||||
(a1 :: c :: a2 :: nil) :: (b1 :: c :: b2 :: nil) :: nil;
|
||||
diagonals _ := fail "diagonals";
|
||||
|
||||
|
||||
@ -261,7 +261,7 @@ toApplicationArg p =
|
||||
( ExpressionHole
|
||||
( Hole
|
||||
{ _holeId = error "hole with no id",
|
||||
_holeLoc = error "hole with no location"
|
||||
_holeKw = error "hole with no location"
|
||||
}
|
||||
)
|
||||
)
|
||||
@ -337,6 +337,6 @@ freshHole = do
|
||||
ExpressionHole
|
||||
( Hole
|
||||
{ _holeId = uid,
|
||||
_holeLoc = error "freshHole with no location"
|
||||
_holeKw = error "freshHole with no location"
|
||||
}
|
||||
)
|
||||
|
||||
@ -95,7 +95,7 @@ instance PrettyCode Application where
|
||||
return $ l' <+> r'
|
||||
|
||||
instance PrettyCode Universe where
|
||||
ppCode (Universe n _) = return $ kwType <+?> (pretty <$> n)
|
||||
ppCode Universe {..} = return $ kwType <+?> (pretty <$> _universeLevel)
|
||||
|
||||
instance PrettyCode PatternArg where
|
||||
ppCode (PatternArg i n p) = do
|
||||
|
||||
@ -529,18 +529,21 @@ goFunctionParameters ::
|
||||
(Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
|
||||
FunctionParameters 'Scoped ->
|
||||
Sem r (NonEmpty Abstract.FunctionParameter)
|
||||
goFunctionParameters (FunctionParameters {..}) = do
|
||||
goFunctionParameters FunctionParameters {..} = do
|
||||
_paramType' <- goExpression _paramType
|
||||
return $
|
||||
fmap
|
||||
( \param ->
|
||||
Abstract.FunctionParameter
|
||||
{ Abstract._paramType = _paramType',
|
||||
Abstract._paramImplicit = _paramImplicit,
|
||||
Abstract._paramName = goSymbol <$> param
|
||||
}
|
||||
)
|
||||
(fromMaybe (pure Nothing) (nonEmpty _paramNames))
|
||||
let mkParam param =
|
||||
Abstract.FunctionParameter
|
||||
{ Abstract._paramType = _paramType',
|
||||
Abstract._paramImplicit = _paramImplicit,
|
||||
Abstract._paramName = goSymbol <$> param
|
||||
}
|
||||
return . fromMaybe (pure (mkParam Nothing)) . nonEmpty $
|
||||
mkParam . goFunctionParameter <$> _paramNames
|
||||
where
|
||||
goFunctionParameter :: FunctionParameter 'Scoped -> Maybe (SymbolType 'Scoped)
|
||||
goFunctionParameter = \case
|
||||
FunctionParameterName n -> Just n
|
||||
FunctionParameterWildcard {} -> Nothing
|
||||
|
||||
goPatternApplication ::
|
||||
(Members '[Error ScoperError, InfoTableBuilder] r) =>
|
||||
|
||||
@ -7,14 +7,14 @@ where
|
||||
|
||||
import Juvix.Data.Keyword
|
||||
import Juvix.Data.Keyword.All
|
||||
( kwArg,
|
||||
( delimSemicolon,
|
||||
kwArg,
|
||||
kwColon,
|
||||
kwDollar,
|
||||
kwFalse,
|
||||
kwFun,
|
||||
kwInductive,
|
||||
kwRightArrow,
|
||||
kwSemicolon,
|
||||
kwStar,
|
||||
kwTmp,
|
||||
kwTrue,
|
||||
@ -28,10 +28,10 @@ allKeywordStrings = keywordsStrings allKeywords
|
||||
|
||||
allKeywords :: [Keyword]
|
||||
allKeywords =
|
||||
[ kwFun,
|
||||
[ delimSemicolon,
|
||||
kwFun,
|
||||
kwInductive,
|
||||
kwColon,
|
||||
kwSemicolon,
|
||||
kwStar,
|
||||
kwRightArrow,
|
||||
kwTrue,
|
||||
|
||||
@ -116,7 +116,7 @@ statementFunction = do
|
||||
_functionMaxTempStackHeight = -1
|
||||
}
|
||||
lift $ registerFunction fi0
|
||||
mcode <- (kw kwSemicolon $> Nothing) <|> optional (braces parseCode)
|
||||
mcode <- (kw delimSemicolon $> Nothing) <|> optional (braces parseCode)
|
||||
let fi = fi0 {_functionCode = fromMaybe [] mcode}
|
||||
case idt of
|
||||
Just (IdentFwd _) -> do
|
||||
@ -155,7 +155,7 @@ statementInductive = do
|
||||
_inductiveRepresentation = IndRepStandard
|
||||
}
|
||||
lift $ registerInductive ii
|
||||
ctrs <- braces $ P.sepEndBy (constrDecl sym) (kw kwSemicolon)
|
||||
ctrs <- braces $ P.sepEndBy (constrDecl sym) (kw delimSemicolon)
|
||||
lift $ registerInductive ii {_inductiveConstructors = map (^. constructorTag) ctrs}
|
||||
|
||||
functionArguments ::
|
||||
@ -252,7 +252,7 @@ typeNamed = do
|
||||
parseCode ::
|
||||
(Member InfoTableBuilder r) =>
|
||||
ParsecS r Code
|
||||
parseCode = P.sepEndBy command (kw kwSemicolon)
|
||||
parseCode = P.sepEndBy command (kw delimSemicolon)
|
||||
|
||||
command ::
|
||||
(Member InfoTableBuilder r) =>
|
||||
|
||||
@ -8,11 +8,15 @@ where
|
||||
import Juvix.Data.Keyword
|
||||
import Juvix.Data.Keyword.All
|
||||
( -- delimiters
|
||||
|
||||
delimBraceL,
|
||||
delimBraceR,
|
||||
delimJudocBlockEnd,
|
||||
delimJudocBlockStart,
|
||||
delimJudocExample,
|
||||
delimJudocStart,
|
||||
delimParenL,
|
||||
delimParenR,
|
||||
delimSemicolon,
|
||||
-- keywords
|
||||
kwAs,
|
||||
kwAssign,
|
||||
@ -42,7 +46,6 @@ import Juvix.Data.Keyword.All
|
||||
kwPostfix,
|
||||
kwPublic,
|
||||
kwRightArrow,
|
||||
kwSemicolon,
|
||||
kwSyntax,
|
||||
kwTerminating,
|
||||
kwType,
|
||||
@ -57,7 +60,8 @@ allKeywordStrings = keywordsStrings allKeywords
|
||||
|
||||
allKeywords :: [Keyword]
|
||||
allKeywords =
|
||||
[ kwAssign,
|
||||
[ delimSemicolon,
|
||||
kwAssign,
|
||||
kwAt,
|
||||
kwAxiom,
|
||||
kwCase,
|
||||
@ -75,7 +79,6 @@ allKeywords =
|
||||
kwPipe,
|
||||
kwPublic,
|
||||
kwRightArrow,
|
||||
kwSemicolon,
|
||||
kwSyntax,
|
||||
kwType,
|
||||
kwUsing,
|
||||
|
||||
@ -43,6 +43,8 @@ data Stage
|
||||
|
||||
$(genSingletons [''Stage])
|
||||
|
||||
type Delims = Irrelevant (Maybe (KeywordRef, KeywordRef))
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Parsing stages
|
||||
--------------------------------------------------------------------------------
|
||||
@ -64,7 +66,7 @@ type family IdentifierType s = res | res -> s where
|
||||
|
||||
type HoleType :: Stage -> GHC.Type
|
||||
type family HoleType s = res | res -> s where
|
||||
HoleType 'Parsed = Interval
|
||||
HoleType 'Parsed = KeywordRef
|
||||
HoleType 'Scoped = Hole
|
||||
|
||||
type PatternAtomIdenType :: Stage -> GHC.Type
|
||||
@ -242,8 +244,10 @@ instance HasLoc IteratorSyntaxDef where
|
||||
|
||||
data TypeSignature (s :: Stage) = TypeSignature
|
||||
{ _sigName :: FunctionName s,
|
||||
_sigColonKw :: Irrelevant KeywordRef,
|
||||
_sigType :: ExpressionType s,
|
||||
_sigDoc :: Maybe (Judoc s),
|
||||
_sigAssignKw :: Irrelevant (Maybe KeywordRef),
|
||||
_sigPragmas :: Maybe ParsedPragmas,
|
||||
_sigBuiltin :: Maybe (WithLoc BuiltinFunction),
|
||||
_sigBody :: Maybe (ExpressionType s),
|
||||
@ -261,10 +265,11 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Typ
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
data AxiomDef (s :: Stage) = AxiomDef
|
||||
{ _axiomKw :: KeywordRef,
|
||||
{ _axiomKw :: Irrelevant KeywordRef,
|
||||
_axiomDoc :: Maybe (Judoc s),
|
||||
_axiomPragmas :: Maybe ParsedPragmas,
|
||||
_axiomName :: SymbolType s,
|
||||
_axiomColonKw :: Irrelevant KeywordRef,
|
||||
_axiomBuiltin :: Maybe (WithLoc BuiltinAxiom),
|
||||
_axiomType :: ExpressionType s
|
||||
}
|
||||
@ -285,6 +290,7 @@ type InductiveName s = SymbolType s
|
||||
|
||||
data InductiveConstructorDef (s :: Stage) = InductiveConstructorDef
|
||||
{ _constructorPipe :: Irrelevant (Maybe KeywordRef),
|
||||
_constructorColonKw :: Irrelevant KeywordRef,
|
||||
_constructorName :: InductiveConstructorName s,
|
||||
_constructorDoc :: Maybe (Judoc s),
|
||||
_constructorPragmas :: Maybe ParsedPragmas,
|
||||
@ -309,7 +315,8 @@ deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (Induct
|
||||
deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (InductiveParameters s)
|
||||
|
||||
data InductiveDef (s :: Stage) = InductiveDef
|
||||
{ _inductiveKw :: KeywordRef,
|
||||
{ _inductiveKw :: Irrelevant KeywordRef,
|
||||
_inductiveAssignKw :: Irrelevant KeywordRef,
|
||||
_inductiveBuiltin :: Maybe (WithLoc BuiltinInductive),
|
||||
_inductiveDoc :: Maybe (Judoc s),
|
||||
_inductivePragmas :: Maybe ParsedPragmas,
|
||||
@ -417,6 +424,7 @@ type FunctionName s = SymbolType s
|
||||
|
||||
data FunctionClause (s :: Stage) = FunctionClause
|
||||
{ _clauseOwnerFunction :: FunctionName s,
|
||||
_clauseAssignKw :: Irrelevant KeywordRef,
|
||||
_clausePatterns :: [PatternType s],
|
||||
_clauseBody :: ExpressionType s
|
||||
}
|
||||
@ -505,8 +513,28 @@ deriving stock instance
|
||||
) =>
|
||||
Ord (Module s t)
|
||||
|
||||
newtype HidingItem (s :: Stage) = HidingItem
|
||||
{ _hidingSymbol :: SymbolType s
|
||||
}
|
||||
|
||||
deriving stock instance
|
||||
( Show (SymbolType s)
|
||||
) =>
|
||||
Show (HidingItem s)
|
||||
|
||||
deriving stock instance
|
||||
( Eq (SymbolType s)
|
||||
) =>
|
||||
Eq (HidingItem s)
|
||||
|
||||
deriving stock instance
|
||||
( Ord (SymbolType s)
|
||||
) =>
|
||||
Ord (HidingItem s)
|
||||
|
||||
data UsingItem (s :: Stage) = UsingItem
|
||||
{ _usingSymbol :: SymbolType s,
|
||||
_usingAsKw :: Irrelevant (Maybe KeywordRef),
|
||||
_usingAs :: Maybe (SymbolType s)
|
||||
}
|
||||
|
||||
@ -525,9 +553,51 @@ deriving stock instance
|
||||
) =>
|
||||
Ord (UsingItem s)
|
||||
|
||||
data UsingList (s :: Stage) = UsingList
|
||||
{ _usingKw :: Irrelevant KeywordRef,
|
||||
_usingBraces :: Irrelevant (KeywordRef, KeywordRef),
|
||||
_usingList :: NonEmpty (UsingItem s)
|
||||
}
|
||||
|
||||
deriving stock instance
|
||||
( Show (SymbolType s)
|
||||
) =>
|
||||
Show (UsingList s)
|
||||
|
||||
deriving stock instance
|
||||
( Eq (SymbolType s)
|
||||
) =>
|
||||
Eq (UsingList s)
|
||||
|
||||
deriving stock instance
|
||||
( Ord (SymbolType s)
|
||||
) =>
|
||||
Ord (UsingList s)
|
||||
|
||||
data HidingList (s :: Stage) = HidingList
|
||||
{ _hidingKw :: Irrelevant KeywordRef,
|
||||
_hidingBraces :: Irrelevant (KeywordRef, KeywordRef),
|
||||
_hidingList :: NonEmpty (HidingItem s)
|
||||
}
|
||||
|
||||
deriving stock instance
|
||||
( Show (SymbolType s)
|
||||
) =>
|
||||
Show (HidingList s)
|
||||
|
||||
deriving stock instance
|
||||
( Eq (SymbolType s)
|
||||
) =>
|
||||
Eq (HidingList s)
|
||||
|
||||
deriving stock instance
|
||||
( Ord (SymbolType s)
|
||||
) =>
|
||||
Ord (HidingList s)
|
||||
|
||||
data UsingHiding (s :: Stage)
|
||||
= Using (NonEmpty (UsingItem s))
|
||||
| Hiding (NonEmpty (SymbolType s))
|
||||
= Using (UsingList s)
|
||||
| Hiding (HidingList s)
|
||||
|
||||
deriving stock instance
|
||||
( Show (SymbolType s)
|
||||
@ -617,6 +687,7 @@ data OpenModule (s :: Stage) = OpenModule
|
||||
_openModuleImportKw :: Maybe KeywordRef,
|
||||
_openImportAsName :: Maybe (ModulePathType s 'ModuleTop),
|
||||
_openUsingHiding :: Maybe (UsingHiding s),
|
||||
_openPublicKw :: Irrelevant (Maybe KeywordRef),
|
||||
_openPublic :: PublicAnn
|
||||
}
|
||||
|
||||
@ -707,10 +778,27 @@ instance HasAtomicity (Lambda s) where
|
||||
--------------------------------------------------------------------------------
|
||||
-- Function expression
|
||||
--------------------------------------------------------------------------------
|
||||
data FunctionParameter (s :: Stage)
|
||||
= FunctionParameterName (SymbolType s)
|
||||
| FunctionParameterWildcard KeywordRef
|
||||
|
||||
deriving stock instance
|
||||
(Show (ExpressionType s), Show (SymbolType s)) =>
|
||||
Show (FunctionParameter s)
|
||||
|
||||
deriving stock instance
|
||||
(Eq (ExpressionType s), Eq (SymbolType s)) =>
|
||||
Eq (FunctionParameter s)
|
||||
|
||||
deriving stock instance
|
||||
(Ord (ExpressionType s), Ord (SymbolType s)) =>
|
||||
Ord (FunctionParameter s)
|
||||
|
||||
data FunctionParameters (s :: Stage) = FunctionParameters
|
||||
{ _paramNames :: [Maybe (SymbolType s)],
|
||||
{ _paramNames :: [FunctionParameter s],
|
||||
_paramImplicit :: IsImplicit,
|
||||
_paramDelims :: Delims,
|
||||
_paramColon :: Irrelevant (Maybe KeywordRef),
|
||||
_paramType :: ExpressionType s
|
||||
}
|
||||
|
||||
@ -743,11 +831,9 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Fun
|
||||
-- Lambda expression
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- Notes: An empty lambda, here called 'the impossible case', is a lambda
|
||||
-- expression with empty list of arguments and empty body.
|
||||
|
||||
data Lambda (s :: Stage) = Lambda
|
||||
{ _lambdaKw :: KeywordRef,
|
||||
_lambdaBraces :: Irrelevant (KeywordRef, KeywordRef),
|
||||
_lambdaClauses :: NonEmpty (LambdaClause s)
|
||||
}
|
||||
|
||||
@ -772,6 +858,7 @@ deriving stock instance
|
||||
data LambdaClause (s :: Stage) = LambdaClause
|
||||
{ _lambdaPipe :: Irrelevant (Maybe KeywordRef),
|
||||
_lambdaParameters :: NonEmpty (PatternType s),
|
||||
_lambdaAssignKw :: Irrelevant KeywordRef,
|
||||
_lambdaBody :: ExpressionType s
|
||||
}
|
||||
|
||||
@ -828,6 +915,7 @@ instance HasFixity PostfixApplication where
|
||||
|
||||
data Let (s :: Stage) = Let
|
||||
{ _letKw :: KeywordRef,
|
||||
_letInKw :: Irrelevant KeywordRef,
|
||||
_letClauses :: NonEmpty (LetClause s),
|
||||
_letExpression :: ExpressionType s
|
||||
}
|
||||
@ -891,7 +979,8 @@ deriving stock instance
|
||||
Ord (LetClause s)
|
||||
|
||||
data CaseBranch (s :: Stage) = CaseBranch
|
||||
{ _caseBranchPipe :: KeywordRef,
|
||||
{ _caseBranchPipe :: Irrelevant KeywordRef,
|
||||
_caseBranchAssignKw :: Irrelevant KeywordRef,
|
||||
_caseBranchPattern :: PatternParensType s,
|
||||
_caseBranchExpression :: ExpressionType s
|
||||
}
|
||||
@ -923,6 +1012,7 @@ deriving stock instance (Ord (ExpressionType s), Ord (PatternParensType s)) => O
|
||||
|
||||
data Initializer (s :: Stage) = Initializer
|
||||
{ _initializerPattern :: PatternParensType s,
|
||||
_initializerAssignKw :: Irrelevant KeywordRef,
|
||||
_initializerExpression :: ExpressionType s
|
||||
}
|
||||
|
||||
@ -950,6 +1040,7 @@ deriving stock instance
|
||||
|
||||
data Range (s :: Stage) = Range
|
||||
{ _rangePattern :: PatternParensType s,
|
||||
_rangeInKw :: Irrelevant KeywordRef,
|
||||
_rangeExpression :: ExpressionType s
|
||||
}
|
||||
|
||||
@ -1111,6 +1202,9 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Jud
|
||||
|
||||
makeLenses ''PatternArg
|
||||
makeLenses ''UsingItem
|
||||
makeLenses ''HidingItem
|
||||
makeLenses ''HidingList
|
||||
makeLenses ''UsingList
|
||||
makeLenses ''JudocLine
|
||||
makeLenses ''Example
|
||||
makeLenses ''Lambda
|
||||
@ -1264,7 +1358,10 @@ instance HasLoc (AxiomDef 'Scoped) where
|
||||
getLoc m = getLoc (m ^. axiomKw) <> getLoc (m ^. axiomType)
|
||||
|
||||
instance HasLoc (OpenModule 'Scoped) where
|
||||
getLoc m = getLoc (m ^. openModuleKw) <> getLoc (m ^. openModuleName)
|
||||
getLoc m =
|
||||
getLoc (m ^. openModuleKw)
|
||||
<> getLoc (m ^. openModuleName)
|
||||
<>? fmap getLoc (m ^. openPublicKw . unIrrelevant)
|
||||
|
||||
instance HasLoc (Statement 'Scoped) where
|
||||
getLoc :: Statement 'Scoped -> Interval
|
||||
@ -1288,13 +1385,23 @@ instance HasLoc PostfixApplication where
|
||||
getLoc (PostfixApplication l o) = getLoc l <> getLoc o
|
||||
|
||||
instance HasLoc (LambdaClause 'Scoped) where
|
||||
getLoc c = getLocSpan (c ^. lambdaParameters) <> getLoc (c ^. lambdaBody)
|
||||
getLoc c =
|
||||
fmap getLoc (c ^. lambdaPipe . unIrrelevant)
|
||||
?<> getLocSpan (c ^. lambdaParameters)
|
||||
<> getLoc (c ^. lambdaBody)
|
||||
|
||||
instance HasLoc (Lambda 'Scoped) where
|
||||
getLoc l = getLoc (l ^. lambdaKw) <> getLocSpan (l ^. lambdaClauses)
|
||||
getLoc l = getLoc (l ^. lambdaKw) <> getLoc (l ^. lambdaBraces . unIrrelevant . _2)
|
||||
|
||||
instance HasLoc (FunctionParameter 'Scoped) where
|
||||
getLoc = \case
|
||||
FunctionParameterName n -> getLoc n
|
||||
FunctionParameterWildcard w -> getLoc w
|
||||
|
||||
instance HasLoc (FunctionParameters 'Scoped) where
|
||||
getLoc p = (getLoc <$> join (listToMaybe (p ^. paramNames))) ?<> getLoc (p ^. paramType)
|
||||
getLoc p = case p ^. paramDelims . unIrrelevant of
|
||||
Nothing -> (getLoc <$> listToMaybe (p ^. paramNames)) ?<> getLoc (p ^. paramType)
|
||||
Just (l, r) -> getLoc l <> getLoc r
|
||||
|
||||
instance HasLoc (Function 'Scoped) where
|
||||
getLoc f = getLoc (f ^. funParameters) <> getLoc (f ^. funReturn)
|
||||
@ -1396,7 +1503,7 @@ instance HasLoc PatternScopedIden where
|
||||
instance HasLoc PatternBinding where
|
||||
getLoc (PatternBinding n p) = getLoc n <> getLoc p
|
||||
|
||||
instance (SingI s) => HasLoc (PatternAtom s) where
|
||||
instance SingI s => HasLoc (PatternAtom s) where
|
||||
getLoc = \case
|
||||
PatternAtomIden i -> getLocIden i
|
||||
PatternAtomWildcard w -> getLoc w
|
||||
|
||||
@ -16,3 +16,6 @@ ppOutDefault = Print.ppOutNoComments defaultOptions
|
||||
|
||||
ppOut :: (HasLoc c, CanonicalProjection a Options, PrettyPrint c) => a -> c -> AnsiText
|
||||
ppOut = Print.ppOutNoComments
|
||||
|
||||
ppTrace :: (HasLoc c, PrettyPrint c) => c -> Text
|
||||
ppTrace = toAnsiText True . ppOut traceOptions
|
||||
|
||||
@ -14,6 +14,13 @@ defaultOptions =
|
||||
_optInJudocBlock = False
|
||||
}
|
||||
|
||||
traceOptions :: Options
|
||||
traceOptions =
|
||||
Options
|
||||
{ _optShowNameIds = True,
|
||||
_optInJudocBlock = False
|
||||
}
|
||||
|
||||
makeLenses ''Options
|
||||
|
||||
fromGenericOptions :: GenericOptions -> Options
|
||||
|
||||
@ -9,6 +9,7 @@ import Data.List.NonEmpty.Extra qualified as NonEmpty
|
||||
import Juvix.Compiler.Concrete.Data.InfoTable
|
||||
import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
|
||||
import Juvix.Compiler.Concrete.Extra qualified as Concrete
|
||||
import Juvix.Compiler.Concrete.Keywords qualified as Kw
|
||||
import Juvix.Compiler.Concrete.Language
|
||||
import Juvix.Compiler.Concrete.Pretty.Options
|
||||
import Juvix.Data.Ape.Base
|
||||
@ -17,7 +18,6 @@ import Juvix.Data.CodeAnn (Ann, CodeAnn (..), ppStringLit)
|
||||
import Juvix.Data.CodeAnn qualified as C
|
||||
import Juvix.Data.Effect.ExactPrint
|
||||
import Juvix.Data.IteratorAttribs
|
||||
import Juvix.Data.Keyword.All
|
||||
import Juvix.Extra.Strings qualified as Str
|
||||
import Juvix.Prelude hiding ((<+>), (<+?>), (<?+>), (?<>))
|
||||
import Juvix.Prelude.Pretty (annotate, pretty)
|
||||
@ -97,9 +97,9 @@ ppImportType = case sing :: SStage s of
|
||||
SScoped -> ppCode
|
||||
|
||||
ppHoleType :: forall s. SingI s => PrettyPrinting (HoleType s)
|
||||
ppHoleType w = case sing :: SStage s of
|
||||
SParsed -> ppCode kwWildcard
|
||||
SScoped -> ppCode w
|
||||
ppHoleType = case sing :: SStage s of
|
||||
SParsed -> ppCode
|
||||
SScoped -> ppCode
|
||||
|
||||
ppPatternAtomIdenType :: forall s. SingI s => PrettyPrinting (PatternAtomIdenType s)
|
||||
ppPatternAtomIdenType = case sing :: SStage s of
|
||||
@ -136,12 +136,12 @@ instance PrettyPrint PatternBinding where
|
||||
ppCode PatternBinding {..} = do
|
||||
let n' = ppSymbolType _patternBindingName
|
||||
p' = ppCode _patternBindingPattern
|
||||
n' <> ppCode kwAt <> p'
|
||||
n' <> ppCode Kw.kwAt <> p'
|
||||
|
||||
instance SingI s => PrettyPrint (PatternAtom s) where
|
||||
ppCode = \case
|
||||
PatternAtomIden n -> ppPatternAtomIdenType n
|
||||
PatternAtomWildcard {} -> ppCode kwWildcard
|
||||
PatternAtomWildcard w -> ppCode w
|
||||
PatternAtomEmpty {} -> parens (return ())
|
||||
PatternAtomParens p -> parens (ppPatternParensType p)
|
||||
PatternAtomBraces p -> braces (ppPatternParensType p)
|
||||
@ -157,13 +157,13 @@ instance SingI s => PrettyPrint (Initializer s) where
|
||||
ppCode Initializer {..} = do
|
||||
let n = ppPatternParensType _initializerPattern
|
||||
e = ppExpressionType _initializerExpression
|
||||
n <+> ppCode kwAssign <+> e
|
||||
n <+> ppCode _initializerAssignKw <+> e
|
||||
|
||||
instance SingI s => PrettyPrint (Range s) where
|
||||
ppCode Range {..} = do
|
||||
let n = ppPatternParensType _rangePattern
|
||||
e = ppExpressionType _rangeExpression
|
||||
n <+> ppCode kwIn <+> e
|
||||
n <+> ppCode _rangeInKw <+> e
|
||||
|
||||
instance SingI s => PrettyPrint (Iterator s) where
|
||||
ppCode Iterator {..} = do
|
||||
@ -174,7 +174,7 @@ instance SingI s => PrettyPrint (Iterator s) where
|
||||
rngs' = parens . sepSemicolon <$> nonEmpty rngs
|
||||
b = ppExpressionType _iteratorBody
|
||||
parensIf _iteratorParens $
|
||||
hang (n <+?> is' <+?> rngs' <> oneLineOrNextNoIndent b)
|
||||
nest (n <+?> is' <+?> rngs' <> oneLineOrNextNoIndent b)
|
||||
|
||||
instance PrettyPrint S.AName where
|
||||
ppCode (S.AName n) = annotated (AnnKind (S.getNameKind n)) (noLoc (pretty (n ^. S.nameVerbatim)))
|
||||
@ -209,7 +209,7 @@ instance PrettyPrint PatternScopedIden where
|
||||
instance PrettyPrint Hole where
|
||||
ppCode h = do
|
||||
let uid = h ^. holeId
|
||||
withNameIdSuffix uid (ppCode kwWildcard)
|
||||
withNameIdSuffix uid (ppCode (h ^. holeKw))
|
||||
|
||||
withNameIdSuffix :: Members '[ExactPrint, Reader Options] r => S.NameId -> Sem r () -> Sem r ()
|
||||
withNameIdSuffix nid a = do
|
||||
@ -237,7 +237,7 @@ instance (SingI t, SingI s) => PrettyPrint (Module s t) where
|
||||
<> modulePragmas'
|
||||
<> ppCode _moduleKw
|
||||
<+> modulePath'
|
||||
<> ppCode kwSemicolon
|
||||
<> ppCode Kw.delimSemicolon
|
||||
<> line
|
||||
<> body'
|
||||
<> ending
|
||||
@ -321,7 +321,7 @@ instance SingI s => PrettyPrint (Import s) where
|
||||
ppQual :: Maybe (Sem r ())
|
||||
ppQual = case i ^. importAsName of
|
||||
Nothing -> Nothing
|
||||
Just as -> Just (ppCode kwAs <+> ppModulePathType as)
|
||||
Just as -> Just (ppCode Kw.kwAs <+> ppModulePathType as)
|
||||
|
||||
instance PrettyPrint SyntaxDef where
|
||||
ppCode = \case
|
||||
@ -340,22 +340,23 @@ instance SingI s => PrettyPrint (LambdaClause s) where
|
||||
ppCode LambdaClause {..} = do
|
||||
let lambdaParameters' = hsep (ppPatternAtom <$> _lambdaParameters)
|
||||
lambdaBody' = ppExpressionType _lambdaBody
|
||||
lambdaParameters' <+> ppCode kwAssign <> oneLineOrNext lambdaBody'
|
||||
lambdaPipe' = ppCode <$> _lambdaPipe ^. unIrrelevant
|
||||
lambdaPipe' <?+> lambdaParameters' <+> ppCode _lambdaAssignKw <> oneLineOrNext lambdaBody'
|
||||
|
||||
instance SingI s => PrettyPrint (Let s) where
|
||||
ppCode Let {..} = do
|
||||
let letClauses' = blockIndent (ppBlock _letClauses)
|
||||
letExpression' = ppExpressionType _letExpression
|
||||
ppCode kwLet <> letClauses' <> ppCode kwIn <+> letExpression'
|
||||
ppCode _letKw <> letClauses' <> ppCode _letInKw <+> letExpression'
|
||||
|
||||
instance SingI s => PrettyPrint (Case s) where
|
||||
ppCode Case {..} = do
|
||||
let exp' = ppExpressionType _caseExpression
|
||||
branches' = indent . vsepHard $ fmap ppCode _caseBranches
|
||||
parensIf _caseParens (ppCode kwCase <+> exp' <> hardline <> branches')
|
||||
parensIf _caseParens (ppCode _caseKw <+> exp' <> hardline <> branches')
|
||||
|
||||
instance PrettyPrint Universe where
|
||||
ppCode (Universe n _) = ppCode kwType <+?> (noLoc <$> (pretty <$> n))
|
||||
ppCode Universe {..} = ppCode _universeKw <+?> (noLoc <$> (pretty <$> _universeLevel))
|
||||
|
||||
apeHelper :: (IsApe a ApeLeaf, Members '[Reader Options, ExactPrint] r) => a -> Sem r ()
|
||||
apeHelper a = do
|
||||
@ -386,19 +387,21 @@ instance SingI s => PrettyPrint (FunctionParameters s) where
|
||||
case _paramNames of
|
||||
[] -> ppLeftExpression' funFixity _paramType
|
||||
_ -> do
|
||||
let paramNames' = map ppParam _paramNames
|
||||
let paramNames' = map ppCode _paramNames
|
||||
paramType' = ppExpressionType _paramType
|
||||
delimIf _paramImplicit True (hsep paramNames' <+> ppCode kwColon <+> paramType')
|
||||
delims' = over both ppCode <$> _paramDelims ^. unIrrelevant
|
||||
colon' = ppCode (fromJust (_paramColon ^. unIrrelevant))
|
||||
delimIf' delims' _paramImplicit True (hsep paramNames' <+> colon' <+> paramType')
|
||||
where
|
||||
ppParam :: Maybe (SymbolType s) -> Sem r ()
|
||||
ppParam = \case
|
||||
Just n -> annDef n (ppSymbolType n)
|
||||
Nothing -> ppCode kwWildcard
|
||||
|
||||
ppLeftExpression' = case sing :: SStage s of
|
||||
SParsed -> ppLeftExpression
|
||||
SScoped -> ppLeftExpression
|
||||
|
||||
instance SingI s => PrettyPrint (FunctionParameter s) where
|
||||
ppCode = \case
|
||||
FunctionParameterName n -> annDef n (ppSymbolType n)
|
||||
FunctionParameterWildcard w -> ppCode w
|
||||
|
||||
instance SingI s => PrettyPrint (Function s) where
|
||||
ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => Function s -> Sem r ()
|
||||
ppCode a = case sing :: SStage s of
|
||||
@ -445,7 +448,7 @@ instance SingI s => PrettyPrint (CaseBranch s) where
|
||||
ppCode CaseBranch {..} = do
|
||||
let pat' = ppPatternParensType _caseBranchPattern
|
||||
e' = ppExpressionType _caseBranchExpression
|
||||
ppCode kwPipe <+> pat' <+> ppCode kwAssign <> oneLineOrNext e'
|
||||
ppCode _caseBranchPipe <+> pat' <+> ppCode _caseBranchAssignKw <> oneLineOrNext e'
|
||||
|
||||
instance SingI s => PrettyPrint (LetClause s) where
|
||||
ppCode c = case c of
|
||||
@ -455,15 +458,13 @@ instance SingI s => PrettyPrint (LetClause s) where
|
||||
ppBlock :: (PrettyPrint a, Members '[Reader Options, ExactPrint] r, Traversable t) => t a -> Sem r ()
|
||||
ppBlock items = vsep (sepEndSemicolon (fmap ppCode items))
|
||||
|
||||
ppPipeBlock :: (PrettyPrint a, Members '[Reader Options, ExactPrint] r, Traversable t) => t a -> Sem r ()
|
||||
ppPipeBlock items = vsepHard (fmap ((ppCode kwPipe <+>) . ppCode) items)
|
||||
|
||||
instance SingI s => PrettyPrint (Lambda s) where
|
||||
ppCode Lambda {..} = do
|
||||
let lambdaKw' = ppCode _lambdaKw
|
||||
braces' = uncurry enclose (over both ppCode (_lambdaBraces ^. unIrrelevant))
|
||||
lambdaClauses' = case _lambdaClauses of
|
||||
s :| [] -> braces (ppCode s)
|
||||
_ -> bracesIndent (ppPipeBlock _lambdaClauses)
|
||||
s :| [] -> braces' (ppCode s)
|
||||
_ -> braces' (blockIndent (vsepHard (ppCode <$> _lambdaClauses)))
|
||||
lambdaKw' <+> lambdaClauses'
|
||||
|
||||
instance PrettyPrint Precedence where
|
||||
@ -531,12 +532,12 @@ ppJudocStart = do
|
||||
inBlock <- asks (^. optInJudocBlock)
|
||||
if
|
||||
| inBlock -> return Nothing
|
||||
| otherwise -> ppCode delimJudocStart $> Just ()
|
||||
| otherwise -> ppCode Kw.delimJudocStart $> Just ()
|
||||
|
||||
instance SingI s => PrettyPrint (Example s) where
|
||||
ppCode e =
|
||||
ppJudocStart
|
||||
<??+> ppCode delimJudocExample
|
||||
<??+> ppCode Kw.delimJudocExample
|
||||
<+> ppExpressionType (e ^. exampleExpression)
|
||||
<> semicolon
|
||||
|
||||
@ -574,7 +575,7 @@ instance SingI s => PrettyPrint (Judoc s) where
|
||||
groupSep = line <> extraLine
|
||||
extraLine :: Sem r ()
|
||||
extraLine = case (g, b) of
|
||||
(JudocGroupLines {}, JudocGroupLines {}) -> ppCode delimJudocStart <> line
|
||||
(JudocGroupLines {}, JudocGroupLines {}) -> ppCode Kw.delimJudocStart <> line
|
||||
_ -> return ()
|
||||
|
||||
instance SingI s => PrettyPrint (JudocBlockParagraph s) where
|
||||
@ -612,17 +613,17 @@ instance SingI s => PrettyPrint (AxiomDef s) where
|
||||
?<> builtin'
|
||||
?<> ppCode _axiomKw
|
||||
<+> axiomName'
|
||||
<+> colon
|
||||
<+> ppCode _axiomColonKw
|
||||
<+> ppExpressionType _axiomType
|
||||
|
||||
instance PrettyPrint BuiltinInductive where
|
||||
ppCode i = ppCode kwBuiltin <+> keyword (P.prettyText i)
|
||||
ppCode i = ppCode Kw.kwBuiltin <+> keywordText (P.prettyText i)
|
||||
|
||||
instance PrettyPrint BuiltinFunction where
|
||||
ppCode i = ppCode kwBuiltin <+> keyword (P.prettyText i)
|
||||
ppCode i = ppCode Kw.kwBuiltin <+> keywordText (P.prettyText i)
|
||||
|
||||
instance PrettyPrint BuiltinAxiom where
|
||||
ppCode i = ppCode kwBuiltin <+> keyword (P.prettyText i)
|
||||
ppCode i = ppCode Kw.kwBuiltin <+> keywordText (P.prettyText i)
|
||||
|
||||
instance SingI s => PrettyPrint (TypeSignature s) where
|
||||
ppCode :: forall r. Members '[ExactPrint, Reader Options] r => TypeSignature s -> Sem r ()
|
||||
@ -635,19 +636,22 @@ instance SingI s => PrettyPrint (TypeSignature s) where
|
||||
name' = annDef _sigName (ppSymbolType _sigName)
|
||||
body' = case _sigBody of
|
||||
Nothing -> Nothing
|
||||
Just body -> Just (ppCode kwAssign <> oneLineOrNext (ppExpressionType body))
|
||||
Just body -> Just (ppCode (fromJust <$> _sigAssignKw) <> oneLineOrNext (ppExpressionType body))
|
||||
doc'
|
||||
?<> pragmas'
|
||||
?<> builtin'
|
||||
?<> termin'
|
||||
?<> ( name'
|
||||
<+> colon
|
||||
<+> ppCode _sigColonKw
|
||||
<> oneLineOrNext
|
||||
( type'
|
||||
<+?> body'
|
||||
)
|
||||
)
|
||||
|
||||
instance PrettyPrint Wildcard where
|
||||
ppCode w = morpheme (getLoc w) C.kwWildcard
|
||||
|
||||
instance PrettyPrint Pattern where
|
||||
ppCode = \case
|
||||
PatternVariable v -> annDef v (ppCode v)
|
||||
@ -655,7 +659,7 @@ instance PrettyPrint Pattern where
|
||||
let l' = ppLeftExpression appFixity l
|
||||
r' = ppRightExpression appFixity r
|
||||
l' <+> r'
|
||||
PatternWildcard {} -> ppCode kwWildcard
|
||||
PatternWildcard w -> ppCode w
|
||||
PatternEmpty {} -> parens (return ())
|
||||
PatternConstructor constr -> ppCode constr
|
||||
PatternInfixApplication i -> apeHelper i
|
||||
@ -665,7 +669,7 @@ instance PrettyPrint PatternArg where
|
||||
ppCode PatternArg {..} = do
|
||||
let name' = ppCode <$> _patternArgName
|
||||
pat' = ppCode _patternArgPattern
|
||||
(name' <&> (<> ppCode kwAt))
|
||||
(name' <&> (<> ppCode Kw.kwAt))
|
||||
?<> delimIf _patternArgIsImplicit delimCond pat'
|
||||
where
|
||||
delimCond :: Bool
|
||||
@ -677,38 +681,34 @@ instance PrettyPrint Text where
|
||||
ppUnkindedSymbol :: Members '[Reader Options, ExactPrint] r => WithLoc Text -> Sem r ()
|
||||
ppUnkindedSymbol = region (annotate AnnUnkindedSym) . ppCode
|
||||
|
||||
ppAtom :: (HasAtomicity c, PrettyPrint c, Members '[ExactPrint, Reader Options] r) => c -> Sem r ()
|
||||
ppAtom c
|
||||
| isAtomic c = ppCode c
|
||||
| otherwise = parens (ppCode c)
|
||||
instance SingI s => PrettyPrint (HidingItem s) where
|
||||
ppCode = ppSymbolType . (^. hidingSymbol)
|
||||
|
||||
instance SingI s => PrettyPrint (HidingList s) where
|
||||
ppCode HidingList {..} = do
|
||||
let (openb, closeb) = _hidingBraces ^. unIrrelevant
|
||||
items' = sequenceWith (semicolon <> space) (ppCode <$> _hidingList)
|
||||
ppCode _hidingKw <+> ppCode openb <> items' <> ppCode closeb
|
||||
|
||||
instance SingI s => PrettyPrint (UsingList s) where
|
||||
ppCode UsingList {..} = do
|
||||
let (openb, closeb) = _usingBraces ^. unIrrelevant
|
||||
items' = sequenceWith (semicolon <> space) (ppCode <$> _usingList)
|
||||
ppCode _usingKw <+> ppCode openb <> items' <> ppCode closeb
|
||||
|
||||
instance SingI s => PrettyPrint (UsingHiding s) where
|
||||
ppCode :: forall r. Members '[ExactPrint, Reader Options] r => UsingHiding s -> Sem r ()
|
||||
ppCode uh = do
|
||||
let bracedList =
|
||||
encloseSep
|
||||
lbrace
|
||||
rbrace
|
||||
(semicolon <> space)
|
||||
ppItems
|
||||
kw' <+> bracedList
|
||||
where
|
||||
kw' :: Sem r ()
|
||||
kw' = case uh of
|
||||
Using {} -> ppCode kwUsing
|
||||
Hiding {} -> ppCode kwHiding
|
||||
ppItems :: NonEmpty (Sem r ())
|
||||
ppItems = case uh of
|
||||
Using s -> fmap ppCode s
|
||||
Hiding s -> fmap ppSymbolType s
|
||||
ppCode = \case
|
||||
Using u -> ppCode u
|
||||
Hiding h -> ppCode h
|
||||
|
||||
instance SingI s => PrettyPrint (UsingItem s) where
|
||||
ppCode :: forall r. Members '[ExactPrint, Reader Options] r => UsingItem s -> Sem r ()
|
||||
ppCode ui = do
|
||||
let kwAs' :: Sem r () = ppCode kwAs
|
||||
as' = (kwAs' <+>) . ppSymbolType <$> ui ^. usingAs
|
||||
let kwAs' :: Maybe (Sem r ()) = ppCode <$> ui ^. usingAsKw . unIrrelevant
|
||||
alias' = ppSymbolType <$> ui ^. usingAs
|
||||
sym' = ppSymbolType (ui ^. usingSymbol)
|
||||
sym' <+?> as'
|
||||
sym' <+?> kwAs' <+?> alias'
|
||||
|
||||
instance PrettyPrint ModuleRef where
|
||||
ppCode (ModuleRef' (_ :&: ModuleRef'' {..})) = ppCode _moduleRefName
|
||||
@ -720,10 +720,8 @@ instance SingI s => PrettyPrint (OpenModule s) where
|
||||
usingHiding' = ppCode <$> _openUsingHiding
|
||||
importkw' = ppCode <$> _openModuleImportKw
|
||||
openkw = ppCode _openModuleKw
|
||||
alias' = (ppCode kwAs <+>) . ppModulePathType <$> _openImportAsName
|
||||
public' = case _openPublic of
|
||||
Public -> Just (ppCode kwPublic)
|
||||
NoPublic -> Nothing
|
||||
alias' = (ppCode Kw.kwAs <+>) . ppModulePathType <$> _openImportAsName
|
||||
public' = ppCode <$> _openPublicKw ^. unIrrelevant
|
||||
case importkw' of
|
||||
Nothing -> do
|
||||
openkw
|
||||
@ -746,9 +744,11 @@ instance SingI s => PrettyPrint (FunctionClause s) where
|
||||
Nothing -> Nothing
|
||||
Just ne -> Just (hsep (ppPatternAtom <$> ne))
|
||||
clauseBody' = ppExpressionType _clauseBody
|
||||
clauseFun'
|
||||
<+?> clausePatterns'
|
||||
<+> ppCode kwAssign
|
||||
nest
|
||||
( clauseFun'
|
||||
<+?> clausePatterns'
|
||||
)
|
||||
<+> ppCode _clauseAssignKw
|
||||
<> oneLineOrNext clauseBody'
|
||||
|
||||
ppCodeAtom :: (HasAtomicity c, PrettyPrint c) => PrettyPrinting c
|
||||
@ -768,12 +768,12 @@ instance SingI s => PrettyPrint (InductiveParameters s) where
|
||||
ppCode InductiveParameters {..} = do
|
||||
let names' = fmap (\nm -> annDef nm (ppSymbolType nm)) _inductiveParametersNames
|
||||
ty' = ppExpressionType _inductiveParametersType
|
||||
parens (hsep names' <+> ppCode kwColon <+> ty')
|
||||
parens (hsep names' <+> ppCode Kw.kwColon <+> ty')
|
||||
|
||||
instance SingI s => PrettyPrint (NonEmpty (InductiveParameters s)) where
|
||||
ppCode = hsep . fmap ppCode
|
||||
|
||||
instance (PrettyPrint a) => PrettyPrint (Irrelevant a) where
|
||||
instance PrettyPrint a => PrettyPrint (Irrelevant a) where
|
||||
ppCode (Irrelevant a) = ppCode a
|
||||
|
||||
instance SingI s => PrettyPrint (InductiveConstructorDef s) where
|
||||
@ -783,13 +783,13 @@ instance SingI s => PrettyPrint (InductiveConstructorDef s) where
|
||||
constructorType' = ppExpressionType _constructorType
|
||||
doc' = ppCode <$> _constructorDoc
|
||||
pragmas' = ppCode <$> _constructorPragmas
|
||||
nest (pipeHelper <+> doc' ?<> pragmas' ?<> constructorName' <+> colon <+> constructorType')
|
||||
pipeHelper <+> nest (doc' ?<> pragmas' ?<> constructorName' <+> ppCode _constructorColonKw <+> constructorType')
|
||||
where
|
||||
-- we use this helper so that comments appear before the first optional pipe if the pipe was omitted
|
||||
pipeHelper :: Sem r ()
|
||||
pipeHelper = case _constructorPipe ^. unIrrelevant of
|
||||
Just p -> ppCode p
|
||||
Nothing -> ppCode kwPipe
|
||||
Nothing -> ppCode Kw.kwPipe
|
||||
|
||||
ppInductiveSignature :: SingI s => PrettyPrinting (InductiveDef s)
|
||||
ppInductiveSignature InductiveDef {..} = do
|
||||
@ -819,9 +819,9 @@ instance SingI s => PrettyPrint (InductiveDef s) where
|
||||
doc'
|
||||
?<> pragmas'
|
||||
?<> sig'
|
||||
<+> ppCode kwAssign
|
||||
<+> ppCode _inductiveAssignKw
|
||||
<> line
|
||||
<> (indent . align) constrs'
|
||||
<> indent constrs'
|
||||
where
|
||||
ppConstructorBlock :: NonEmpty (InductiveConstructorDef s) -> Sem r ()
|
||||
ppConstructorBlock cs = vsep (ppCode <$> cs)
|
||||
|
||||
@ -572,6 +572,7 @@ checkInductiveDef InductiveDef {..} = do
|
||||
_inductiveConstructors = inductiveConstructors',
|
||||
_inductiveBuiltin,
|
||||
_inductivePositive,
|
||||
_inductiveAssignKw,
|
||||
_inductiveKw
|
||||
}
|
||||
where
|
||||
@ -597,7 +598,8 @@ checkInductiveDef InductiveDef {..} = do
|
||||
_constructorType = constructorType',
|
||||
_constructorDoc = doc',
|
||||
_constructorPragmas = _constructorPragmas,
|
||||
_constructorPipe
|
||||
_constructorPipe,
|
||||
_constructorColonKw
|
||||
}
|
||||
|
||||
createExportsTable :: ExportInfo -> HashSet NameId
|
||||
@ -874,8 +876,8 @@ checkOpenModuleNoImport OpenModule {..}
|
||||
|
||||
let checkUsingHiding :: UsingHiding 'Parsed -> Sem r (UsingHiding 'Scoped)
|
||||
checkUsingHiding = \case
|
||||
Hiding h -> Hiding <$> mapM scopeSymbol h
|
||||
Using uh -> Using <$> mapM checkUsingItem uh
|
||||
Hiding h -> Hiding <$> checkHidingList h
|
||||
Using uh -> Using <$> checkUsingList uh
|
||||
where
|
||||
scopeSymbol :: Symbol -> Sem r S.Symbol
|
||||
scopeSymbol s = do
|
||||
@ -895,6 +897,29 @@ checkOpenModuleNoImport OpenModule {..}
|
||||
registerName (S.unqualifiedSymbol scopedSym)
|
||||
return scopedSym
|
||||
|
||||
checkHidingList :: HidingList 'Parsed -> Sem r (HidingList 'Scoped)
|
||||
checkHidingList l = do
|
||||
items' <- mapM checkHidingItem (l ^. hidingList)
|
||||
return
|
||||
HidingList
|
||||
{ _hidingKw = l ^. hidingKw,
|
||||
_hidingBraces = l ^. hidingBraces,
|
||||
_hidingList = items'
|
||||
}
|
||||
|
||||
checkUsingList :: UsingList 'Parsed -> Sem r (UsingList 'Scoped)
|
||||
checkUsingList l = do
|
||||
items' <- mapM checkUsingItem (l ^. usingList)
|
||||
return
|
||||
UsingList
|
||||
{ _usingKw = l ^. usingKw,
|
||||
_usingBraces = l ^. usingBraces,
|
||||
_usingList = items'
|
||||
}
|
||||
|
||||
checkHidingItem :: HidingItem 'Parsed -> Sem r (HidingItem 'Scoped)
|
||||
checkHidingItem h = HidingItem <$> scopeSymbol (h ^. hidingSymbol)
|
||||
|
||||
checkUsingItem :: UsingItem 'Parsed -> Sem r (UsingItem 'Scoped)
|
||||
checkUsingItem i = do
|
||||
scopedSym <- scopeSymbol (i ^. usingSymbol)
|
||||
@ -905,7 +930,8 @@ checkOpenModuleNoImport OpenModule {..}
|
||||
return
|
||||
UsingItem
|
||||
{ _usingSymbol = scopedSym,
|
||||
_usingAs = scopedAs
|
||||
_usingAs = scopedAs,
|
||||
_usingAsKw = i ^. usingAsKw
|
||||
}
|
||||
|
||||
usingHiding' <- mapM checkUsingHiding _openUsingHiding
|
||||
@ -953,13 +979,17 @@ checkOpenModuleNoImport OpenModule {..}
|
||||
mayAs' <- u ^. at (symbolEntryNameId e)
|
||||
return (fromMaybe sym mayAs', e)
|
||||
u :: HashMap NameId (Maybe Symbol)
|
||||
u = HashMap.fromList [(i ^. usingSymbol . S.nameId, i ^? usingAs . _Just . S.nameConcrete) | i <- toList l]
|
||||
u =
|
||||
HashMap.fromList
|
||||
[ (i ^. usingSymbol . S.nameId, i ^? usingAs . _Just . S.nameConcrete)
|
||||
| i <- toList (l ^. usingList)
|
||||
]
|
||||
Just (Hiding l) -> over exportSymbols (HashMap.filter (not . inHiding))
|
||||
where
|
||||
inHiding :: SymbolEntry -> Bool
|
||||
inHiding e = HashSet.member (symbolEntryNameId e) u
|
||||
u :: HashSet NameId
|
||||
u = HashSet.fromList (map (^. S.nameId) (toList l))
|
||||
u = HashSet.fromList (map (^. hidingSymbol . S.nameId) (toList (l ^. hidingList)))
|
||||
Nothing -> id
|
||||
|
||||
checkOpenModule ::
|
||||
@ -987,7 +1017,8 @@ checkFunctionClause clause@FunctionClause {..} = do
|
||||
@$> FunctionClause
|
||||
{ _clauseOwnerFunction = clauseOwnerFunction',
|
||||
_clausePatterns = clausePatterns',
|
||||
_clauseBody = clauseBody'
|
||||
_clauseBody = clauseBody',
|
||||
_clauseAssignKw
|
||||
}
|
||||
where
|
||||
fun = _clauseOwnerFunction
|
||||
@ -1023,10 +1054,12 @@ checkFunction f = do
|
||||
_paramType <- checkParseExpressionAtoms (f ^. funParameters . paramType)
|
||||
withLocalScope $ do
|
||||
_paramNames <- forM (f ^. funParameters . paramNames) $ \case
|
||||
Nothing -> return Nothing
|
||||
Just p -> Just <$> bindVariableSymbol p
|
||||
FunctionParameterWildcard w -> return (FunctionParameterWildcard w)
|
||||
FunctionParameterName p -> FunctionParameterName <$> bindVariableSymbol p
|
||||
_funReturn <- checkParseExpressionAtoms (f ^. funReturn)
|
||||
let _paramImplicit = f ^. funParameters . paramImplicit
|
||||
_paramColon = f ^. funParameters . paramColon
|
||||
_paramDelims = f ^. funParameters . paramDelims
|
||||
_funParameters = FunctionParameters {..}
|
||||
_funKw = f ^. funKw
|
||||
return Function {..}
|
||||
@ -1054,7 +1087,8 @@ checkLet Let {..} =
|
||||
Let
|
||||
{ _letClauses = letClauses',
|
||||
_letExpression = letExpression',
|
||||
_letKw
|
||||
_letKw,
|
||||
_letInKw
|
||||
}
|
||||
where
|
||||
checkLetClauses :: NonEmpty (LetClause 'Parsed) -> Sem r (NonEmpty (LetClause 'Scoped))
|
||||
@ -1101,7 +1135,14 @@ checkLambda ::
|
||||
(Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
|
||||
Lambda 'Parsed ->
|
||||
Sem r (Lambda 'Scoped)
|
||||
checkLambda Lambda {..} = Lambda _lambdaKw <$> mapM checkLambdaClause _lambdaClauses
|
||||
checkLambda Lambda {..} = do
|
||||
clauses' <- mapM checkLambdaClause _lambdaClauses
|
||||
return
|
||||
Lambda
|
||||
{ _lambdaClauses = clauses',
|
||||
_lambdaKw,
|
||||
_lambdaBraces
|
||||
}
|
||||
|
||||
checkLambdaClause ::
|
||||
(Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
|
||||
@ -1114,7 +1155,8 @@ checkLambdaClause LambdaClause {..} = withLocalScope $ do
|
||||
LambdaClause
|
||||
{ _lambdaParameters = lambdaParameters',
|
||||
_lambdaBody = lambdaBody',
|
||||
_lambdaPipe
|
||||
_lambdaPipe,
|
||||
_lambdaAssignKw
|
||||
}
|
||||
|
||||
scopedVar ::
|
||||
@ -1215,11 +1257,11 @@ checkPatternBinding ::
|
||||
PatternBinding ->
|
||||
Sem r PatternArg
|
||||
checkPatternBinding (PatternBinding n p) = do
|
||||
n' <- bindVariableSymbol n
|
||||
p' <- checkParsePatternAtom p
|
||||
n' <- bindVariableSymbol n
|
||||
if
|
||||
| isJust (p' ^. patternArgName) -> throw (ErrDoubleBinderPattern (DoubleBinderPattern n' p'))
|
||||
| otherwise -> return $ set patternArgName (Just n') p'
|
||||
| otherwise -> return (set patternArgName (Just n') p')
|
||||
|
||||
checkPatternAtoms ::
|
||||
(Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
|
||||
@ -1300,17 +1342,15 @@ checkIterator iter = do
|
||||
( ErrIteratorUndefined
|
||||
IteratorUndefined {_iteratorUndefinedIterator = iter}
|
||||
)
|
||||
let inipats = map (^. initializerPattern) (iter ^. iteratorInitializers)
|
||||
inivals = map (^. initializerExpression) (iter ^. iteratorInitializers)
|
||||
rngpats = map (^. rangePattern) (iter ^. iteratorRanges)
|
||||
rngvals = map (^. rangeExpression) (iter ^. iteratorRanges)
|
||||
inivals' <- mapM checkParseExpressionAtoms inivals
|
||||
rngvals' <- mapM checkParseExpressionAtoms rngvals
|
||||
inivals' <- mapM (checkParseExpressionAtoms . (^. initializerExpression)) (iter ^. iteratorInitializers)
|
||||
rngvals' <- mapM (checkParseExpressionAtoms . (^. rangeExpression)) (iter ^. iteratorRanges)
|
||||
let initAssignKws = iter ^.. iteratorInitializers . each . initializerAssignKw
|
||||
rangesInKws = iter ^.. iteratorRanges . each . rangeInKw
|
||||
withLocalScope $ do
|
||||
inipats' <- mapM checkParsePatternAtoms inipats
|
||||
rngpats' <- mapM checkParsePatternAtoms rngpats
|
||||
let _iteratorInitializers = zipWithExact Initializer inipats' inivals'
|
||||
_iteratorRanges = zipWithExact Range rngpats' rngvals'
|
||||
inipats' <- mapM (checkParsePatternAtoms . (^. initializerPattern)) (iter ^. iteratorInitializers)
|
||||
rngpats' <- mapM (checkParsePatternAtoms . (^. rangePattern)) (iter ^. iteratorRanges)
|
||||
let _iteratorInitializers = [Initializer p k v | ((p, k), v) <- zipExact (zipExact inipats' initAssignKws) inivals']
|
||||
_iteratorRanges = [Range p k v | ((p, k), v) <- zipExact (zipExact rngpats' rangesInKws) rngvals']
|
||||
_iteratorParens = iter ^. iteratorParens
|
||||
_iteratorBody <- checkParseExpressionAtoms (iter ^. iteratorBody)
|
||||
return Iterator {..}
|
||||
@ -1322,7 +1362,11 @@ checkInitializer ::
|
||||
checkInitializer ini = do
|
||||
_initializerPattern <- checkParsePatternAtoms (ini ^. initializerPattern)
|
||||
_initializerExpression <- checkParseExpressionAtoms (ini ^. initializerExpression)
|
||||
return Initializer {..}
|
||||
return
|
||||
Initializer
|
||||
{ _initializerAssignKw = ini ^. initializerAssignKw,
|
||||
..
|
||||
}
|
||||
|
||||
checkRange ::
|
||||
(Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
|
||||
@ -1331,7 +1375,11 @@ checkRange ::
|
||||
checkRange rng = do
|
||||
_rangePattern <- checkParsePatternAtoms (rng ^. rangePattern)
|
||||
_rangeExpression <- checkParseExpressionAtoms (rng ^. rangeExpression)
|
||||
return Range {..}
|
||||
return
|
||||
Range
|
||||
{ _rangeInKw = rng ^. rangeInKw,
|
||||
..
|
||||
}
|
||||
|
||||
checkHole ::
|
||||
(Members '[NameIdGen] r) =>
|
||||
@ -1342,7 +1390,7 @@ checkHole h = do
|
||||
return
|
||||
Hole
|
||||
{ _holeId = i,
|
||||
_holeLoc = h
|
||||
_holeKw = h
|
||||
}
|
||||
|
||||
checkParens ::
|
||||
@ -1527,6 +1575,8 @@ makeExpressionTable (ExpressionAtoms atoms _) = [appOpExplicit] : operators ++ [
|
||||
param =
|
||||
FunctionParameters
|
||||
{ _paramNames = [],
|
||||
_paramDelims = Irrelevant Nothing,
|
||||
_paramColon = Irrelevant Nothing,
|
||||
_paramImplicit = Explicit,
|
||||
_paramType = a
|
||||
}
|
||||
@ -1732,10 +1782,12 @@ makePatternTable (PatternAtoms latoms _) = [appOp] : operators
|
||||
)
|
||||
|
||||
explicitP :: Pattern -> PatternArg
|
||||
explicitP = PatternArg Explicit Nothing
|
||||
|
||||
implicitP :: Pattern -> PatternArg
|
||||
implicitP = PatternArg Implicit Nothing
|
||||
explicitP _patternArgPattern =
|
||||
PatternArg
|
||||
{ _patternArgIsImplicit = Explicit,
|
||||
_patternArgName = Nothing,
|
||||
_patternArgPattern
|
||||
}
|
||||
|
||||
parsePatternTerm ::
|
||||
forall r.
|
||||
|
||||
@ -232,14 +232,39 @@ mkTopModulePath l = TopModulePath (NonEmpty.init l) (NonEmpty.last l)
|
||||
usingItem :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (UsingItem 'Parsed)
|
||||
usingItem = do
|
||||
_usingSymbol <- symbol
|
||||
_usingAs <- optional (kw kwAs >> symbol)
|
||||
alias <- optional $ do
|
||||
k <- Irrelevant <$> kw kwAs
|
||||
(k,) <$> symbol
|
||||
let _usingAsKw = mapM fst alias
|
||||
_usingAs = snd <$> alias
|
||||
return UsingItem {..}
|
||||
|
||||
usingItems :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (NonEmpty (UsingItem 'Parsed))
|
||||
usingItems = braces (P.sepBy1 usingItem semicolon)
|
||||
hidingItem :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (HidingItem 'Parsed)
|
||||
hidingItem = HidingItem <$> symbol
|
||||
|
||||
symbolList :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (NonEmpty Symbol)
|
||||
symbolList = braces (P.sepBy1 symbol semicolon)
|
||||
phidingList :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (HidingList 'Parsed)
|
||||
phidingList = do
|
||||
_hidingKw <- Irrelevant <$> kw kwHiding
|
||||
l <- kw delimBraceL
|
||||
_hidingList <- P.sepBy1 hidingItem semicolon
|
||||
r <- kw delimBraceR
|
||||
return
|
||||
HidingList
|
||||
{ _hidingBraces = Irrelevant (l, r),
|
||||
..
|
||||
}
|
||||
|
||||
pusingList :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (UsingList 'Parsed)
|
||||
pusingList = do
|
||||
_usingKw <- Irrelevant <$> kw kwUsing
|
||||
l <- kw delimBraceL
|
||||
_usingList <- P.sepBy1 usingItem semicolon
|
||||
r <- kw delimBraceR
|
||||
return
|
||||
UsingList
|
||||
{ _usingBraces = Irrelevant (l, r),
|
||||
..
|
||||
}
|
||||
|
||||
topModulePath :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r TopModulePath
|
||||
topModulePath = mkTopModulePath <$> dottedSymbol
|
||||
@ -553,8 +578,8 @@ expressionAtom =
|
||||
<|> (AtomLet <$> letBlock)
|
||||
<|> (AtomFunArrow <$> kw kwRightArrow)
|
||||
<|> (AtomHole <$> hole)
|
||||
<|> parens (AtomParens <$> parseExpressionAtoms)
|
||||
<|> braces (AtomBraces <$> withLoc parseExpressionAtoms)
|
||||
<|> (AtomParens <$> parens parseExpressionAtoms)
|
||||
<|> (AtomBraces <$> withLoc (braces parseExpressionAtoms))
|
||||
|
||||
parseExpressionAtoms ::
|
||||
(Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) =>
|
||||
@ -572,26 +597,40 @@ iterator ::
|
||||
(Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) =>
|
||||
ParsecS r (Iterator 'Parsed)
|
||||
iterator = do
|
||||
(isInit, _iteratorName, pat) <- P.try $ do
|
||||
(isInit, keywordRef, _iteratorName, pat) <- P.try $ do
|
||||
n <- name
|
||||
lparen
|
||||
pat <- parsePatternAtoms
|
||||
b <- (kw kwAssign >> return True) <|> (kw kwIn >> return False)
|
||||
return (b, n, pat)
|
||||
(isInit, kwr) <-
|
||||
((True,) <$> kw kwAssign)
|
||||
<|> ((False,) <$> kw kwIn)
|
||||
return (isInit, Irrelevant kwr, n, pat)
|
||||
val <- parseExpressionAtoms
|
||||
_iteratorInitializers <-
|
||||
if
|
||||
| isInit -> do
|
||||
inis <- many (semicolon >> initializer)
|
||||
rparen
|
||||
return (Initializer pat val : inis)
|
||||
let ini =
|
||||
Initializer
|
||||
{ _initializerPattern = pat,
|
||||
_initializerAssignKw = keywordRef,
|
||||
_initializerExpression = val
|
||||
}
|
||||
return (ini : inis)
|
||||
| otherwise -> return []
|
||||
_iteratorRanges <-
|
||||
if
|
||||
| not isInit -> do
|
||||
rngs <- many (semicolon >> range)
|
||||
rparen
|
||||
return (Range pat val : rngs)
|
||||
let ran =
|
||||
Range
|
||||
{ _rangeExpression = val,
|
||||
_rangePattern = pat,
|
||||
_rangeInKw = keywordRef
|
||||
}
|
||||
return (ran : rngs)
|
||||
| otherwise -> fmap (maybe [] toList) $ optional $ do
|
||||
lparen
|
||||
rngs <- P.sepBy1 range semicolon
|
||||
@ -603,19 +642,19 @@ iterator = do
|
||||
where
|
||||
initializer :: ParsecS r (Initializer 'Parsed)
|
||||
initializer = do
|
||||
_initializerPattern <- P.try $ do
|
||||
(_initializerPattern, _initializerAssignKw) <- P.try $ do
|
||||
pat <- parsePatternAtoms
|
||||
kw kwAssign
|
||||
return pat
|
||||
r <- Irrelevant <$> kw kwAssign
|
||||
return (pat, r)
|
||||
_initializerExpression <- parseExpressionAtoms
|
||||
return Initializer {..}
|
||||
|
||||
range :: ParsecS r (Range 'Parsed)
|
||||
range = do
|
||||
_rangePattern <- P.try $ do
|
||||
(_rangePattern, _rangeInKw) <- P.try $ do
|
||||
pat <- parsePatternAtoms
|
||||
kw kwIn
|
||||
return pat
|
||||
r <- Irrelevant <$> kw kwIn
|
||||
return (pat, r)
|
||||
_rangeExpression <- parseExpressionAtoms
|
||||
return Range {..}
|
||||
|
||||
@ -624,7 +663,7 @@ iterator = do
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
hole :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (HoleType 'Parsed)
|
||||
hole = snd <$> interval (kw kwHole)
|
||||
hole = kw kwHole
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Literals
|
||||
@ -654,15 +693,15 @@ letBlock :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r)
|
||||
letBlock = do
|
||||
_letKw <- kw kwLet
|
||||
_letClauses <- P.sepEndBy1 letClause semicolon
|
||||
kw kwIn
|
||||
_letInKw <- Irrelevant <$> kw kwIn
|
||||
_letExpression <- parseExpressionAtoms
|
||||
return Let {..}
|
||||
|
||||
caseBranch :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (CaseBranch 'Parsed)
|
||||
caseBranch = do
|
||||
_caseBranchPipe <- kw kwPipe
|
||||
_caseBranchPipe <- Irrelevant <$> kw kwPipe
|
||||
_caseBranchPattern <- parsePatternAtoms
|
||||
kw kwAssign
|
||||
_caseBranchAssignKw <- Irrelevant <$> kw kwAssign
|
||||
_caseBranchExpression <- parseExpressionAtoms
|
||||
return CaseBranch {..}
|
||||
|
||||
@ -680,13 +719,14 @@ case_ = do
|
||||
|
||||
universe :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r Universe
|
||||
universe = do
|
||||
i <- snd <$> interval (kw kwType)
|
||||
uni <- optional decimal
|
||||
i <- kw kwType
|
||||
lvl :: Maybe (WithLoc Natural) <- fmap (uncurry (flip WithLoc)) <$> optional decimal
|
||||
return
|
||||
( case uni of
|
||||
Nothing -> Universe Nothing i
|
||||
Just (lvl, i') -> Universe (Just lvl) (i <> i')
|
||||
)
|
||||
Universe
|
||||
{ _universeLevel = (^. withLocParam) <$> lvl,
|
||||
_universeKw = i,
|
||||
_universeLevelLoc = getLoc <$> lvl
|
||||
}
|
||||
|
||||
peekJudoc :: (Member JudocStash r) => ParsecS r (Maybe (Judoc 'Parsed))
|
||||
peekJudoc = P.lift get
|
||||
@ -710,11 +750,15 @@ typeSignature ::
|
||||
Maybe (WithLoc BuiltinFunction) ->
|
||||
ParsecS r (TypeSignature 'Parsed)
|
||||
typeSignature _sigTerminating _sigName _sigBuiltin = P.label "<type signature>" $ do
|
||||
kw kwColon
|
||||
_sigColonKw <- Irrelevant <$> kw kwColon
|
||||
_sigType <- parseExpressionAtoms
|
||||
_sigDoc <- getJudoc
|
||||
_sigPragmas <- getPragmas
|
||||
_sigBody <- optional (kw kwAssign >> parseExpressionAtoms)
|
||||
body <- optional $ do
|
||||
k <- Irrelevant <$> kw kwAssign
|
||||
(k,) <$> parseExpressionAtoms
|
||||
let _sigBody = snd <$> body
|
||||
_sigAssignKw = mapM fst body
|
||||
return TypeSignature {..}
|
||||
|
||||
-- | Used to minimize the amount of required @P.try@s.
|
||||
@ -744,11 +788,11 @@ axiomDef ::
|
||||
Maybe (WithLoc BuiltinAxiom) ->
|
||||
ParsecS r (AxiomDef 'Parsed)
|
||||
axiomDef _axiomBuiltin = do
|
||||
_axiomKw <- kw kwAxiom
|
||||
_axiomKw <- Irrelevant <$> kw kwAxiom
|
||||
_axiomDoc <- getJudoc
|
||||
_axiomPragmas <- getPragmas
|
||||
_axiomName <- symbol
|
||||
kw kwColon
|
||||
_axiomColonKw <- Irrelevant <$> kw kwColon
|
||||
_axiomType <- parseExpressionAtoms
|
||||
return AxiomDef {..}
|
||||
|
||||
@ -756,31 +800,32 @@ axiomDef _axiomBuiltin = do
|
||||
-- Function expression
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
implicitOpen :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r IsImplicit
|
||||
implicitOpen :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (KeywordRef, IsImplicit)
|
||||
implicitOpen =
|
||||
lbrace $> Implicit
|
||||
<|> lparen $> Explicit
|
||||
(,Implicit) <$> kw delimBraceL
|
||||
<|> (,Explicit) <$> kw delimParenL
|
||||
|
||||
implicitClose :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => IsImplicit -> ParsecS r ()
|
||||
implicitClose :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => IsImplicit -> ParsecS r KeywordRef
|
||||
implicitClose = \case
|
||||
Implicit -> rbrace
|
||||
Explicit -> rparen
|
||||
Implicit -> kw delimBraceR
|
||||
Explicit -> kw delimParenR
|
||||
|
||||
functionParams :: forall r. (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (FunctionParameters 'Parsed)
|
||||
functionParams = do
|
||||
(_paramNames, _paramImplicit) <- P.try $ do
|
||||
impl <- implicitOpen
|
||||
(openDelim, _paramNames, _paramImplicit, _paramColon) <- P.try $ do
|
||||
(opn, impl) <- implicitOpen
|
||||
n <- some pName
|
||||
kw kwColon
|
||||
return (n, impl)
|
||||
c <- Irrelevant . Just <$> kw kwColon
|
||||
return (opn, n, impl, c)
|
||||
_paramType <- parseExpressionAtoms
|
||||
implicitClose _paramImplicit
|
||||
closeDelim <- implicitClose _paramImplicit
|
||||
let _paramDelims = Irrelevant (Just (openDelim, closeDelim))
|
||||
return FunctionParameters {..}
|
||||
where
|
||||
pName :: ParsecS r (Maybe Symbol)
|
||||
pName :: ParsecS r (FunctionParameter 'Parsed)
|
||||
pName =
|
||||
Just <$> symbol
|
||||
<|> Nothing <$ kw kwWildcard
|
||||
FunctionParameterName <$> symbol
|
||||
<|> FunctionParameterWildcard <$> kw kwWildcard
|
||||
|
||||
function :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Function 'Parsed)
|
||||
function = do
|
||||
@ -796,14 +841,17 @@ function = do
|
||||
lambdaClause :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (LambdaClause 'Parsed)
|
||||
lambdaClause _lambdaPipe = do
|
||||
_lambdaParameters <- P.some patternAtom
|
||||
kw kwAssign
|
||||
_lambdaAssignKw <- Irrelevant <$> kw kwAssign
|
||||
_lambdaBody <- parseExpressionAtoms
|
||||
return LambdaClause {..}
|
||||
|
||||
lambda :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Lambda 'Parsed)
|
||||
lambda = do
|
||||
_lambdaKw <- kw kwLambda
|
||||
_lambdaClauses <- braces (pipeSep1 lambdaClause)
|
||||
brl <- kw delimBraceL
|
||||
_lambdaClauses <- pipeSep1 lambdaClause
|
||||
brr <- kw delimBraceR
|
||||
let _lambdaBraces = Irrelevant (brl, brr)
|
||||
return Lambda {..}
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
@ -813,7 +861,7 @@ lambda = do
|
||||
inductiveDef :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => Maybe (WithLoc BuiltinInductive) -> ParsecS r (InductiveDef 'Parsed)
|
||||
inductiveDef _inductiveBuiltin = do
|
||||
_inductivePositive <- optional (kw kwPositive)
|
||||
_inductiveKw <- kw kwInductive
|
||||
_inductiveKw <- Irrelevant <$> kw kwInductive
|
||||
_inductiveDoc <- getJudoc
|
||||
_inductivePragmas <- getPragmas
|
||||
_inductiveName <- symbol P.<?> "<type name>"
|
||||
@ -823,7 +871,7 @@ inductiveDef _inductiveBuiltin = do
|
||||
_inductiveType <-
|
||||
optional (kw kwColon >> parseExpressionAtoms)
|
||||
P.<?> "<type annotation e.g. ': Type'>"
|
||||
kw kwAssign P.<?> "<assignment symbol ':='>"
|
||||
_inductiveAssignKw <- Irrelevant <$> kw kwAssign P.<?> "<assignment symbol ':='>"
|
||||
_inductiveConstructors <-
|
||||
pipeSep1 constructorDef
|
||||
P.<?> "<constructor definition>"
|
||||
@ -841,9 +889,8 @@ constructorDef _constructorPipe = do
|
||||
_constructorDoc <- optional stashJudoc >> getJudoc
|
||||
_constructorPragmas <- optional stashPragmas >> getPragmas
|
||||
_constructorName <- symbol P.<?> "<constructor name>"
|
||||
_constructorType <-
|
||||
kw kwColon >> parseExpressionAtoms
|
||||
P.<?> "<constructor type signature (:)>"
|
||||
_constructorColonKw <- Irrelevant <$> kw kwColon
|
||||
_constructorType <- parseExpressionAtoms P.<?> "<constructor type>"
|
||||
return InductiveConstructorDef {..}
|
||||
|
||||
wildcard :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r Wildcard
|
||||
@ -867,7 +914,7 @@ patternAtomNamed nested = do
|
||||
off <- P.getOffset
|
||||
n <- name
|
||||
case n of
|
||||
NameQualified _ -> return (PatternAtomIden n)
|
||||
NameQualified {} -> return (PatternAtomIden n)
|
||||
NameUnqualified s -> do
|
||||
checkWrongEq off s
|
||||
patternAtomAt s <|> return (PatternAtomIden n)
|
||||
@ -904,7 +951,7 @@ parsePatternAtomsNested = do
|
||||
functionClause :: forall r. (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => Symbol -> ParsecS r (FunctionClause 'Parsed)
|
||||
functionClause _clauseOwnerFunction = do
|
||||
_clausePatterns <- P.many patternAtom
|
||||
kw kwAssign
|
||||
_clauseAssignKw <- Irrelevant <$> kw kwAssign
|
||||
_clauseBody <- parseExpressionAtoms
|
||||
return FunctionClause {..}
|
||||
|
||||
@ -951,7 +998,8 @@ openModule = do
|
||||
whenJust _openModuleImportKw (const (P.lift (importedModule (moduleNameToTopModulePath _openModuleName))))
|
||||
_openParameters <- many atomicExpression
|
||||
_openUsingHiding <- optional usingOrHiding
|
||||
_openPublic <- maybe NoPublic (const Public) <$> optional (kw kwPublic)
|
||||
_openPublicKw <- Irrelevant <$> optional (kw kwPublic)
|
||||
let _openPublic = maybe NoPublic (const Public) (_openPublicKw ^. unIrrelevant)
|
||||
return
|
||||
OpenModule
|
||||
{ _openImportAsName = Nothing,
|
||||
@ -960,8 +1008,8 @@ openModule = do
|
||||
|
||||
usingOrHiding :: (Members '[Error ParserError, InfoTableBuilder, JudocStash, NameIdGen, PragmasStash] r) => ParsecS r (UsingHiding 'Parsed)
|
||||
usingOrHiding =
|
||||
(kw kwUsing >> Using <$> usingItems)
|
||||
<|> (kw kwHiding >> Hiding <$> symbolList)
|
||||
Using <$> pusingList
|
||||
<|> Hiding <$> phidingList
|
||||
|
||||
newOpenSyntax :: forall r. (Members '[Error ParserError, PathResolver, Files, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (OpenModule 'Parsed)
|
||||
newOpenSyntax = do
|
||||
@ -969,11 +1017,9 @@ newOpenSyntax = do
|
||||
_openModuleKw <- kw kwOpen
|
||||
_openParameters <- many atomicExpression
|
||||
_openUsingHiding <- optional usingOrHiding
|
||||
_openPublic <- maybe NoPublic (const Public) <$> optional (kw kwPublic)
|
||||
_openPublicKw <- Irrelevant <$> optional (kw kwPublic)
|
||||
let _openModuleName = topModulePathToName (im ^. importModule)
|
||||
_openModuleImportKw = Just (im ^. importKw)
|
||||
_openImportAsName = im ^. importAsName
|
||||
return
|
||||
OpenModule
|
||||
{ ..
|
||||
}
|
||||
_openPublic = maybe NoPublic (const Public) (_openPublicKw ^. unIrrelevant)
|
||||
return OpenModule {..}
|
||||
|
||||
@ -115,7 +115,6 @@ lparen = delim "("
|
||||
rparen :: (Members '[InfoTableBuilder] r) => ParsecS r ()
|
||||
rparen = delim ")"
|
||||
|
||||
-- TODO Consider using this instead of kw kwPipe
|
||||
pipe :: (Members '[InfoTableBuilder] r) => ParsecS r ()
|
||||
pipe = delim "|"
|
||||
|
||||
|
||||
@ -7,7 +7,8 @@ where
|
||||
|
||||
import Juvix.Data.Keyword
|
||||
import Juvix.Data.Keyword.All
|
||||
( kwAny,
|
||||
( delimSemicolon,
|
||||
kwAny,
|
||||
kwAssign,
|
||||
kwBind,
|
||||
kwBottom,
|
||||
@ -37,7 +38,6 @@ import Juvix.Data.Keyword.All
|
||||
kwPi,
|
||||
kwPlus,
|
||||
kwRightArrow,
|
||||
kwSemicolon,
|
||||
kwSeq,
|
||||
kwSeqq,
|
||||
kwShow,
|
||||
@ -56,32 +56,32 @@ allKeywordStrings = keywordsStrings allKeywords
|
||||
|
||||
allKeywords :: [Keyword]
|
||||
allKeywords =
|
||||
[ kwAssign,
|
||||
kwBuiltin,
|
||||
[ delimSemicolon,
|
||||
kwAssign,
|
||||
kwBottom,
|
||||
kwLet,
|
||||
kwLetRec,
|
||||
kwBuiltin,
|
||||
kwCase,
|
||||
kwColon,
|
||||
kwComma,
|
||||
kwDef,
|
||||
kwDiv,
|
||||
kwElse,
|
||||
kwEq,
|
||||
kwIf,
|
||||
kwIn,
|
||||
kwInductive,
|
||||
kwCase,
|
||||
kwOf,
|
||||
kwLet,
|
||||
kwLetRec,
|
||||
kwMatch,
|
||||
kwWith,
|
||||
kwIf,
|
||||
kwThen,
|
||||
kwElse,
|
||||
kwDef,
|
||||
kwRightArrow,
|
||||
kwColon,
|
||||
kwSemicolon,
|
||||
kwComma,
|
||||
kwWildcard,
|
||||
kwPlus,
|
||||
kwMinus,
|
||||
kwMul,
|
||||
kwDiv,
|
||||
kwMod,
|
||||
kwEq,
|
||||
kwMul,
|
||||
kwOf,
|
||||
kwPlus,
|
||||
kwRightArrow,
|
||||
kwThen,
|
||||
kwWildcard,
|
||||
kwWith,
|
||||
kwLt,
|
||||
kwLe,
|
||||
kwGt,
|
||||
|
||||
@ -79,7 +79,7 @@ parseToplevel = do
|
||||
lift declareBoolBuiltins
|
||||
lift declareNatBuiltins
|
||||
space
|
||||
P.endBy statement (kw kwSemicolon)
|
||||
P.endBy statement (kw delimSemicolon)
|
||||
r <- optional expression
|
||||
P.eof
|
||||
return r
|
||||
@ -206,7 +206,7 @@ statementInductive = do
|
||||
_inductivePragmas = mempty
|
||||
}
|
||||
lift $ registerInductive txt ii
|
||||
ctrs <- braces $ P.sepEndBy (constrDecl sym) (kw kwSemicolon)
|
||||
ctrs <- braces $ P.sepEndBy (constrDecl sym) (kw delimSemicolon)
|
||||
lift $ registerInductive txt ii {_inductiveConstructors = map (^. constructorTag) ctrs}
|
||||
|
||||
constrDecl ::
|
||||
@ -751,7 +751,7 @@ letrecDefs names varsNum0 vars0 varsNum vars = forM names letrecItem
|
||||
parseFailure off "identifier name doesn't match letrec signature"
|
||||
kw kwAssign
|
||||
v <- bracedExpr varsNum vars
|
||||
kw kwSemicolon
|
||||
kw delimSemicolon
|
||||
let ty = fromMaybe mkDynamic' mty
|
||||
return $ LetItem (Binder txt (Just i) ty) v
|
||||
|
||||
@ -804,7 +804,7 @@ exprCase' ::
|
||||
HashMap Text Level ->
|
||||
ParsecS r Node
|
||||
exprCase' off value varsNum vars = do
|
||||
bs <- P.sepEndBy (caseBranchP varsNum vars) (kw kwSemicolon)
|
||||
bs <- P.sepEndBy (caseBranchP varsNum vars) (kw delimSemicolon)
|
||||
let bss = map fromLeft' $ filter isLeft bs
|
||||
let def' = map fromRight' $ filter isRight bs
|
||||
case bss of
|
||||
@ -959,7 +959,7 @@ exprMatch' ::
|
||||
exprMatch' vals rty varsNum vars = do
|
||||
let values = map fst vals
|
||||
types = map snd vals
|
||||
bs <- P.sepEndBy (matchBranch (length values) varsNum vars) (kw kwSemicolon)
|
||||
bs <- P.sepEndBy (matchBranch (length values) varsNum vars) (kw delimSemicolon)
|
||||
return $ mkMatch' (fromList types) rty (fromList values) bs
|
||||
|
||||
matchBranch ::
|
||||
|
||||
@ -665,4 +665,4 @@ checkExpression hintArity expr = case expr of
|
||||
(ArityUnknown, p : ps) -> (p :) <$> go (succ idx) ArityUnknown ps
|
||||
|
||||
newHole :: (Member NameIdGen r) => Interval -> Sem r Hole
|
||||
newHole loc = (`Hole` loc) <$> freshNameId
|
||||
newHole loc = mkHole loc <$> freshNameId
|
||||
|
||||
@ -486,9 +486,7 @@ checkPattern = go
|
||||
return (Right (ind, zipExact params args))
|
||||
|
||||
freshHole :: (Members '[Inference, NameIdGen] r) => Interval -> Sem r Hole
|
||||
freshHole l = do
|
||||
uid <- freshNameId
|
||||
return (Hole uid l)
|
||||
freshHole l = mkHole l <$> freshNameId
|
||||
|
||||
inferExpression' ::
|
||||
forall r.
|
||||
|
||||
@ -7,6 +7,7 @@ where
|
||||
import Juvix.Data.CodeAnn qualified as C
|
||||
import Juvix.Data.Effect.ExactPrint.Base
|
||||
import Juvix.Data.IsImplicit
|
||||
import Juvix.Data.Keyword.All
|
||||
import Juvix.Prelude.Base hiding ((<+>))
|
||||
import Juvix.Prelude.Pretty qualified as P
|
||||
|
||||
@ -47,16 +48,18 @@ infixl 7 <+?>
|
||||
annotated :: Members '[ExactPrint] r => C.CodeAnn -> Sem r () -> Sem r ()
|
||||
annotated an = region (P.annotate an)
|
||||
|
||||
-- | Opening parenthesis is printed after comments
|
||||
parens :: Members '[ExactPrint] r => Sem r () -> Sem r ()
|
||||
parens = region C.parens
|
||||
parens = enclose (enqueue C.kwParenL) (noLoc C.kwParenR)
|
||||
|
||||
parensIf :: Members '[ExactPrint] r => Bool -> Sem r () -> Sem r ()
|
||||
parensIf b
|
||||
| b = parens
|
||||
| otherwise = id
|
||||
|
||||
-- | Opening brace is printed after comments
|
||||
braces :: Members '[ExactPrint] r => Sem r () -> Sem r ()
|
||||
braces = region C.braces
|
||||
braces = enclose (enqueue C.kwBraceL) (noLoc C.kwBraceR)
|
||||
|
||||
lineOrEmpty :: Members '[ExactPrint] r => Sem r ()
|
||||
lineOrEmpty = noLoc P.line'
|
||||
@ -82,15 +85,6 @@ line = noLoc P.line
|
||||
hardline :: Members '[ExactPrint] r => Sem r ()
|
||||
hardline = noLoc P.hardline
|
||||
|
||||
lbrace :: Members '[ExactPrint] r => Sem r ()
|
||||
lbrace = noLoc C.kwBraceL
|
||||
|
||||
rbrace :: Members '[ExactPrint] r => Sem r ()
|
||||
rbrace = noLoc C.kwBraceR
|
||||
|
||||
bracesIndent :: Members '[ExactPrint] r => Sem r () -> Sem r ()
|
||||
bracesIndent = braces . blockIndent
|
||||
|
||||
colon :: Members '[ExactPrint] r => Sem r ()
|
||||
colon = noLoc C.kwColon
|
||||
|
||||
@ -131,7 +125,7 @@ enclose :: Monad m => m () -> m () -> m () -> m ()
|
||||
enclose l r p = l >> p >> r
|
||||
|
||||
encloseSep :: (Monad m, Foldable f) => m () -> m () -> m () -> f (m ()) -> m ()
|
||||
encloseSep l r sep f = l >> sequenceWith sep f >> r
|
||||
encloseSep l r sep f = enclose l r (sequenceWith sep f)
|
||||
|
||||
oneLineOrNextNoIndent :: Members '[ExactPrint] r => Sem r () -> Sem r ()
|
||||
oneLineOrNextNoIndent = region P.oneLineOrNextNoIndent
|
||||
@ -142,14 +136,29 @@ oneLineOrNext = region P.oneLineOrNext
|
||||
paragraphs :: (Foldable l, Members '[ExactPrint] r) => l (Sem r ()) -> Sem r ()
|
||||
paragraphs = sequenceWith (line >> ensureEmptyLine)
|
||||
|
||||
keyword :: Members '[ExactPrint] r => Text -> Sem r ()
|
||||
keyword = annotated C.AnnKeyword . noLoc . P.pretty
|
||||
kw :: Members '[ExactPrint] r => Keyword -> Sem r ()
|
||||
kw = annotated C.AnnKeyword . noLoc . P.pretty
|
||||
|
||||
keywordText :: Members '[ExactPrint] r => Text -> Sem r ()
|
||||
keywordText = annotated C.AnnKeyword . noLoc . P.pretty
|
||||
|
||||
-- | The first argument contains the left and right delimiters, if any.
|
||||
-- If the second argument is True, then the delimiters *must* be given.
|
||||
delimIf' :: Maybe (Sem r (), Sem r ()) -> IsImplicit -> Bool -> Sem r () -> Sem r ()
|
||||
delimIf' d impl delim
|
||||
| delim || impl == Implicit = uncurry enclose (fromJust d)
|
||||
| otherwise = id
|
||||
|
||||
delimIf :: Members '[ExactPrint] r => IsImplicit -> Bool -> Sem r () -> Sem r ()
|
||||
delimIf Implicit _ = braces
|
||||
delimIf Explicit True = parens
|
||||
delimIf Explicit False = id
|
||||
|
||||
morpheme :: forall r. Members '[ExactPrint] r => Interval -> Doc C.CodeAnn -> Sem r ()
|
||||
morpheme loc doc = do
|
||||
void (printCommentsUntil loc)
|
||||
noLoc doc
|
||||
|
||||
morphemeM :: forall r. Members '[ExactPrint] r => Interval -> Sem r () -> Sem r ()
|
||||
morphemeM loc doc = do
|
||||
void (printCommentsUntil loc)
|
||||
|
||||
@ -13,7 +13,8 @@ import Prettyprinter qualified as P
|
||||
|
||||
data ExactPrint m a where
|
||||
NoLoc :: Doc Ann -> ExactPrint m ()
|
||||
Morpheme :: Interval -> Doc Ann -> ExactPrint m ()
|
||||
-- | Used to print parentheses after comments.
|
||||
Enqueue :: Doc Ann -> ExactPrint m ()
|
||||
PrintCommentsUntil :: Interval -> ExactPrint m (Maybe SpaceSpan)
|
||||
EnsureEmptyLine :: ExactPrint m ()
|
||||
Region :: (Doc Ann -> Doc Ann) -> m b -> ExactPrint m b
|
||||
@ -24,6 +25,8 @@ makeSem ''ExactPrint
|
||||
data Builder = Builder
|
||||
{ -- | comments sorted by starting location
|
||||
_builderComments :: [SpaceSpan],
|
||||
-- | New elements are put at the front
|
||||
_builderQueue :: [Doc Ann],
|
||||
_builderDoc :: Doc Ann,
|
||||
_builderEnsureEmptyLine :: Bool,
|
||||
_builderEnd :: FileLoc
|
||||
@ -39,6 +42,7 @@ runExactPrint cs = fmap (first (^. builderDoc)) . runState ini . re
|
||||
Builder
|
||||
{ _builderComments = fromMaybe [] (cs ^? _Just . fileCommentsSorted),
|
||||
_builderDoc = mempty,
|
||||
_builderQueue = mempty,
|
||||
_builderEnsureEmptyLine = False,
|
||||
_builderEnd = FileLoc 0 0 0
|
||||
}
|
||||
@ -54,10 +58,10 @@ re = reinterpretH h
|
||||
ExactPrint (Sem rInitial) x ->
|
||||
Tactical ExactPrint (Sem rInitial) (State Builder ': r) x
|
||||
h = \case
|
||||
NoLoc p -> append' p >>= pureT
|
||||
NoLoc p -> noLoc' p >>= pureT
|
||||
EnsureEmptyLine -> modify' (set builderEnsureEmptyLine True) >>= pureT
|
||||
Morpheme l p -> morpheme' l p >>= pureT
|
||||
End -> end' >>= pureT
|
||||
Enqueue d -> enqueue' d >>= pureT
|
||||
PrintCommentsUntil l -> printCommentsUntil' l >>= pureT
|
||||
Region f m -> do
|
||||
st0 :: Builder <- set builderDoc mempty <$> get
|
||||
@ -69,6 +73,7 @@ re = reinterpretH h
|
||||
{ _builderDoc = doc' <> f (st' ^. builderDoc),
|
||||
_builderComments = st' ^. builderComments,
|
||||
_builderEnd = st' ^. builderEnd,
|
||||
_builderQueue = st' ^. builderQueue,
|
||||
_builderEnsureEmptyLine = st' ^. builderEnsureEmptyLine
|
||||
}
|
||||
return fx
|
||||
@ -76,6 +81,14 @@ re = reinterpretH h
|
||||
evalExactPrint' :: Builder -> Sem (ExactPrint ': r) a -> Sem r (Builder, a)
|
||||
evalExactPrint' b = runState b . re
|
||||
|
||||
enqueue' :: forall r. Members '[State Builder] r => Doc Ann -> Sem r ()
|
||||
enqueue' d = modify (over builderQueue (d :))
|
||||
|
||||
noLoc' :: forall r. Members '[State Builder] r => Doc Ann -> Sem r ()
|
||||
noLoc' d = do
|
||||
popQueue
|
||||
append' d
|
||||
|
||||
append' :: forall r. Members '[State Builder] r => Doc Ann -> Sem r ()
|
||||
append' d = modify (over builderDoc (<> d))
|
||||
|
||||
@ -105,15 +118,22 @@ printComment c = do
|
||||
append' (annotate AnnComment (P.pretty c))
|
||||
hardline'
|
||||
|
||||
popQueue :: Members '[State Builder] r => Sem r ()
|
||||
popQueue = do
|
||||
q <- gets (^. builderQueue)
|
||||
modify' (set builderQueue mempty)
|
||||
append' (mconcat (reverse q))
|
||||
|
||||
printCommentsUntil' :: forall r. Members '[State Builder] r => Interval -> Sem r (Maybe SpaceSpan)
|
||||
printCommentsUntil' loc = do
|
||||
forceLine <- popEnsureLine
|
||||
g <- fmap sconcat . nonEmpty <$> whileJustM popSpaceSpan
|
||||
g :: Maybe SpaceSpan <- fmap sconcat . nonEmpty <$> whileJustM popSpaceSpan
|
||||
let noSpaceLines = fromMaybe True $ do
|
||||
g' <- (^. spaceSpan) <$> g
|
||||
return (not (any (has _SpaceLines) g'))
|
||||
when (forceLine && noSpaceLines) line'
|
||||
whenJust g printSpaceSpan
|
||||
popQueue
|
||||
return g
|
||||
where
|
||||
cmp :: SpaceSpan -> Bool
|
||||
@ -134,8 +154,3 @@ printCommentsUntil' loc = do
|
||||
modify' (set builderComments hs)
|
||||
return (Just h)
|
||||
_ -> return Nothing
|
||||
|
||||
morpheme' :: forall r. Members '[State Builder] r => Interval -> Doc Ann -> Sem r ()
|
||||
morpheme' loc doc = do
|
||||
void (printCommentsUntil' loc)
|
||||
append' doc
|
||||
|
||||
@ -94,7 +94,7 @@ atomParens associates argAtom opInf = case argAtom of
|
||||
opPrec :: Precedence
|
||||
opPrec = opInf ^. fixityPrecedence
|
||||
|
||||
isAtomic :: (HasAtomicity a) => a -> Bool
|
||||
isAtomic :: HasAtomicity a => a -> Bool
|
||||
isAtomic x = case atomicity x of
|
||||
Atom -> True
|
||||
_ -> False
|
||||
|
||||
@ -1,5 +1,7 @@
|
||||
module Juvix.Data.Hole where
|
||||
|
||||
import Juvix.Data.Keyword
|
||||
import Juvix.Data.Keyword.All (kwWildcard)
|
||||
import Juvix.Data.Loc
|
||||
import Juvix.Data.NameId
|
||||
import Juvix.Prelude.Base
|
||||
@ -7,10 +9,24 @@ import Prettyprinter
|
||||
|
||||
data Hole = Hole
|
||||
{ _holeId :: NameId,
|
||||
_holeLoc :: Interval
|
||||
_holeKw :: KeywordRef
|
||||
}
|
||||
deriving stock (Show, Data)
|
||||
|
||||
mkHole :: Interval -> NameId -> Hole
|
||||
mkHole loc uid =
|
||||
Hole
|
||||
{ _holeId = uid,
|
||||
_holeKw = r
|
||||
}
|
||||
where
|
||||
r =
|
||||
KeywordRef
|
||||
{ _keywordRefKeyword = kwWildcard,
|
||||
_keywordRefInterval = loc,
|
||||
_keywordRefUnicode = Ascii
|
||||
}
|
||||
|
||||
makeLenses ''Hole
|
||||
|
||||
instance Eq Hole where
|
||||
@ -23,7 +39,7 @@ instance Hashable Hole where
|
||||
hashWithSalt s = hashWithSalt s . (^. holeId)
|
||||
|
||||
instance HasLoc Hole where
|
||||
getLoc = (^. holeLoc)
|
||||
getLoc = getLoc . (^. holeKw)
|
||||
|
||||
instance Pretty Hole where
|
||||
pretty = const "_"
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
-- ignored when checking for equality/ordering
|
||||
module Juvix.Data.Irrelevant where
|
||||
|
||||
import Juvix.Data.Loc
|
||||
import Juvix.Prelude.Base
|
||||
import Juvix.Prelude.Pretty
|
||||
|
||||
@ -10,6 +11,9 @@ newtype Irrelevant a = Irrelevant
|
||||
}
|
||||
deriving stock (Show)
|
||||
|
||||
instance HasLoc a => HasLoc (Irrelevant a) where
|
||||
getLoc (Irrelevant a) = getLoc a
|
||||
|
||||
instance Eq (Irrelevant a) where
|
||||
_ == _ = True
|
||||
|
||||
@ -29,4 +33,7 @@ instance Applicative Irrelevant where
|
||||
(<*>) :: Irrelevant (a -> b) -> Irrelevant a -> Irrelevant b
|
||||
Irrelevant f <*> Irrelevant a = Irrelevant (f a)
|
||||
|
||||
instance Monad Irrelevant where
|
||||
(Irrelevant mx) >>= f = f mx
|
||||
|
||||
makeLenses ''Irrelevant
|
||||
|
||||
@ -82,9 +82,6 @@ kwPublic = asciiKw Str.public
|
||||
kwRightArrow :: Keyword
|
||||
kwRightArrow = unicodeKw Str.toAscii Str.toUnicode
|
||||
|
||||
kwSemicolon :: Keyword
|
||||
kwSemicolon = asciiKw Str.semicolon
|
||||
|
||||
kwSyntax :: Keyword
|
||||
kwSyntax = asciiKw Str.syntax
|
||||
|
||||
@ -229,6 +226,18 @@ kwDollar = asciiKw Str.dollar
|
||||
kwMutual :: Keyword
|
||||
kwMutual = asciiKw Str.mutual
|
||||
|
||||
delimBraceL :: Keyword
|
||||
delimBraceL = mkDelim Str.braceL
|
||||
|
||||
delimBraceR :: Keyword
|
||||
delimBraceR = mkDelim Str.braceR
|
||||
|
||||
delimParenL :: Keyword
|
||||
delimParenL = mkDelim Str.parenL
|
||||
|
||||
delimParenR :: Keyword
|
||||
delimParenR = mkDelim Str.parenR
|
||||
|
||||
delimJudocExample :: Keyword
|
||||
delimJudocExample = mkJudocDelim Str.judocExample
|
||||
|
||||
@ -240,3 +249,6 @@ delimJudocBlockStart = mkJudocDelim Str.judocBlockStart
|
||||
|
||||
delimJudocBlockEnd :: Keyword
|
||||
delimJudocBlockEnd = mkJudocDelim Str.judocBlockEnd
|
||||
|
||||
delimSemicolon :: Keyword
|
||||
delimSemicolon = mkDelim Str.semicolon
|
||||
|
||||
@ -1,12 +1,15 @@
|
||||
module Juvix.Data.Universe where
|
||||
|
||||
import Juvix.Data.Fixity
|
||||
import Juvix.Data.Keyword
|
||||
import Juvix.Data.Keyword.All (kwType)
|
||||
import Juvix.Data.Loc
|
||||
import Juvix.Prelude.Base
|
||||
|
||||
data Universe = Universe
|
||||
{ _universeLevel :: Maybe Natural,
|
||||
_universeLoc :: Interval
|
||||
_universeKw :: KeywordRef,
|
||||
_universeLevelLoc :: Maybe Interval
|
||||
}
|
||||
deriving stock (Show, Ord, Data)
|
||||
|
||||
@ -26,6 +29,19 @@ getUniverseLevel Universe {..} = fromMaybe defaultLevel _universeLevel
|
||||
instance Eq Universe where
|
||||
(==) = (==) `on` getUniverseLevel
|
||||
|
||||
mkUniverse :: Maybe Natural -> Interval -> Universe
|
||||
mkUniverse lvl loc =
|
||||
Universe
|
||||
{ _universeLevel = lvl,
|
||||
_universeLevelLoc = Nothing,
|
||||
_universeKw =
|
||||
KeywordRef
|
||||
{ _keywordRefInterval = loc,
|
||||
_keywordRefKeyword = kwType,
|
||||
_keywordRefUnicode = Ascii
|
||||
}
|
||||
}
|
||||
|
||||
defaultLevel :: Natural
|
||||
defaultLevel = 0
|
||||
|
||||
@ -36,7 +52,7 @@ makeLenses ''Universe
|
||||
makeLenses ''SmallUniverse
|
||||
|
||||
smallUniverse :: Interval -> Universe
|
||||
smallUniverse = Universe (Just smallLevel)
|
||||
smallUniverse = mkUniverse (Just smallLevel)
|
||||
|
||||
isSmallUniverse :: Universe -> Bool
|
||||
isSmallUniverse = (== smallLevel) . getUniverseLevel
|
||||
@ -53,7 +69,7 @@ instance HasAtomicity SmallUniverse where
|
||||
atomicity _ = Atom
|
||||
|
||||
instance HasLoc Universe where
|
||||
getLoc = (^. universeLoc)
|
||||
getLoc = getLoc . (^. universeKw)
|
||||
|
||||
instance HasLoc SmallUniverse where
|
||||
getLoc = (^. smallUniverseLoc)
|
||||
|
||||
@ -26,6 +26,18 @@ pragmasStart = "{-#"
|
||||
pragmasEnd :: (IsString s) => s
|
||||
pragmasEnd = "#-}"
|
||||
|
||||
braceL :: IsString s => s
|
||||
braceL = "{"
|
||||
|
||||
braceR :: IsString s => s
|
||||
braceR = "}"
|
||||
|
||||
parenL :: IsString s => s
|
||||
parenL = "("
|
||||
|
||||
parenR :: IsString s => s
|
||||
parenR = ")"
|
||||
|
||||
end :: (IsString s) => s
|
||||
end = "end"
|
||||
|
||||
|
||||
@ -140,7 +140,7 @@ import Data.Text qualified as Text
|
||||
import Data.Text.Encoding
|
||||
import Data.Text.IO
|
||||
import Data.Traversable
|
||||
import Data.Tuple.Extra
|
||||
import Data.Tuple.Extra hiding (both)
|
||||
import Data.Typeable hiding (TyCon)
|
||||
import Data.Void
|
||||
import Data.Word
|
||||
@ -152,7 +152,7 @@ import GHC.Num
|
||||
import GHC.Real
|
||||
import GHC.Stack.Types
|
||||
import Language.Haskell.TH.Syntax (Lift)
|
||||
import Lens.Micro.Platform hiding (both)
|
||||
import Lens.Micro.Platform
|
||||
import Path
|
||||
import Path.IO qualified as Path
|
||||
import Polysemy
|
||||
|
||||
@ -1,9 +1,20 @@
|
||||
module Format;
|
||||
{-- This is Judoc block comment --}
|
||||
module -- Declaring a top module of name:
|
||||
Format;
|
||||
|
||||
import -- Import a module of name:
|
||||
Stdlib.Prelude open -- Bring all names into scope but..
|
||||
hiding -- Hide some names
|
||||
{-- like this
|
||||
,; -- don't want , here
|
||||
-- Bool either
|
||||
Bool; true; false};
|
||||
|
||||
import Stdlib.Prelude open hiding {,};
|
||||
import Stdlib.Data.Nat.Ord open;
|
||||
|
||||
-- Lorem ipsum dolor sit amet, consectetur adipiscing elit
|
||||
terminating
|
||||
-- Comment between terminating and type sig
|
||||
go : Nat → Nat → Nat;
|
||||
go n s :=
|
||||
if
|
||||
@ -11,8 +22,10 @@ go n s :=
|
||||
(go (sub n 1) s)
|
||||
(go n (sub s n) + go (sub n 1) s);
|
||||
|
||||
module M;
|
||||
syntax infixr 4 ,;
|
||||
module {- local module -}
|
||||
M;
|
||||
syntax -- syntax in local modules
|
||||
infixr 4 ,;
|
||||
axiom , : String → String → String;
|
||||
end;
|
||||
|
||||
@ -141,11 +154,13 @@ idLambda := λ {x := x};
|
||||
f : Nat -> Nat;
|
||||
f :=
|
||||
\ {
|
||||
-- comment before lambda pipe
|
||||
| zero :=
|
||||
let
|
||||
foo : Nat := 1;
|
||||
in foo
|
||||
| _ := 1
|
||||
| _ -- comment before lambda :=
|
||||
:= 1
|
||||
};
|
||||
|
||||
module Patterns;
|
||||
@ -174,16 +189,54 @@ module Comments;
|
||||
|
||||
-- attached to nothing
|
||||
|
||||
axiom a3 : Type;
|
||||
axiom a3 -- comment before axiom :
|
||||
: Type;
|
||||
|
||||
num -- comment before type sig :
|
||||
:
|
||||
-- comment after type sig :
|
||||
Nat;
|
||||
num -- comment before clause :=
|
||||
:=
|
||||
-- comment after clause :=
|
||||
123;
|
||||
|
||||
-- attached to nothing
|
||||
-- attached to nothing 2
|
||||
|
||||
-- attached to nothing 3
|
||||
|
||||
axiom a4 : Type;
|
||||
axiom a4 : -- before open pi brace
|
||||
{-- after open pi brace
|
||||
a -- before pi :
|
||||
: Type}
|
||||
-> Type;
|
||||
|
||||
id2 : {A : Type} -> A -> Nat -> A;
|
||||
id2 -- before patternarg braces
|
||||
{A} a -- before open patternarg parens
|
||||
(suc b) :=
|
||||
idLambda
|
||||
-- before implicit app
|
||||
{-- inside implicit arg
|
||||
A}
|
||||
-- before closing implicit arg
|
||||
a;
|
||||
|
||||
type color : Type :=
|
||||
-- comment before pipe
|
||||
| black : color
|
||||
| white : color
|
||||
| red : color
|
||||
-- comment before pipe
|
||||
| blue : color;
|
||||
|
||||
axiom a5 : Type;
|
||||
|
||||
open Patterns -- before using
|
||||
using -- before brace
|
||||
{-- before first f
|
||||
f; f};
|
||||
end;
|
||||
|
||||
-- Comment at the end of a module
|
||||
|
||||
Loading…
Reference in New Issue
Block a user