diff --git a/src/Core/FC.idr b/src/Core/FC.idr index b6ff6f6b73..72c5c30399 100644 --- a/src/Core/FC.idr +++ b/src/Core/FC.idr @@ -97,6 +97,10 @@ mapFC f (MkFCVal fc val) = MkFCVal fc (f val) distribFC : WithFC (List a) -> List (WithFC a) distribFC x = map (MkFCVal x.fc) x.val +%inline export +traverseFCMaybe : (a -> Maybe b) -> WithFC a -> Maybe (WithFC b) +traverseFCMaybe f (MkFCVal fc val) = MkFCVal fc <$> f val + ||| An interface to extract the location of some data public export interface HasFC ty where diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index db46b7c4b1..4ef02cc60c 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -383,7 +383,7 @@ mutual cls <- traverse (map snd . desugarClause ps True) cls pure $ ICase fc opts scr scrty cls desugarB side ps (PLocal fc xs scope) - = let ps' = definedIn xs ++ ps in + = let ps' = definedIn (map val xs) ++ ps in pure $ ILocal fc (concat !(traverse (desugarDecl ps') xs)) !(desugar side ps' scope) desugarB side ps (PApp pfc (PUpdate fc fs) rec) @@ -1079,13 +1079,13 @@ mutual {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> List Name -> PDecl -> Core (List ImpDecl) - desugarDecl ps (PClaim (MkFCVal fc (MkPClaim rig vis fnopts ty))) + desugarDecl ps (MkFCVal fc $ PClaim (MkPClaim rig vis fnopts ty)) = do opts <- traverse (desugarFnOpt ps) fnopts types <- desugarType ps ty pure $ flip (map {f = List, b = ImpDecl}) types $ \ty' => IClaim (MkFCVal fc $ MkIClaimData rig vis opts ty') - desugarDecl ps (PDef (MkFCVal fc clauses)) + desugarDecl ps (MkFCVal fc $ PDef clauses) -- The clauses won't necessarily all be from the same function, so split -- after desugaring, by function name, using collectDefs from RawImp = do ncs <- traverse (desugarClause ps False) clauses @@ -1100,10 +1100,10 @@ mutual toIDef nm (ImpossibleClause fc lhs) = pure $ IDef fc nm [ImpossibleClause fc lhs] - desugarDecl ps (PData fc doc vis mbtot ddecl) + desugarDecl ps (MkFCVal fc $ PData doc vis mbtot ddecl) = pure [IData fc vis mbtot !(desugarData ps doc ddecl)] - desugarDecl ps (PParameters fc params pds) + desugarDecl ps (MkFCVal fc $ PParameters params pds) = do params' <- getArgs params let paramList = forget params' @@ -1132,7 +1132,7 @@ mutual let allbinders = map (\nn => (nn.val, rig, i', tm')) n pure allbinders) params - desugarDecl ps (PUsing fc uimpls uds) + desugarDecl ps (MkFCVal fc $ PUsing uimpls uds) = do syn <- get Syn let oldu = usingImpl syn uimpls' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm) @@ -1142,7 +1142,7 @@ mutual uds' <- traverse (desugarDecl ps) uds update Syn { usingImpl := oldu } pure (concat uds') - desugarDecl ps (PInterface fc vis cons_in tn doc params det conname body) + desugarDecl ps (MkFCVal fc $ PInterface vis cons_in tn doc params det conname body) = do addDocString tn doc let paramNames = concatMap (map val . forget . names) params @@ -1156,7 +1156,7 @@ mutual params let _ = the (List (WithFC Name, RigCount, RawImp)) params' -- Look for bindable names in all the constraints and parameters - let mnames = map dropNS (definedIn body) + let mnames = map dropNS (definedIn (map val body)) bnames <- ifThenElse (not !isUnboundImplicits) (pure []) $ map concat $ for (map Builtin.snd cons' ++ map (snd . snd) params') @@ -1187,7 +1187,7 @@ mutual expandConstraint (Nothing, p) = map (\x => (Nothing, x)) (pairToCons p) - desugarDecl ps (PImplementation fc vis fnopts pass is cons tn params impln nusing body) + desugarDecl ps (MkFCVal fc $ PImplementation vis fnopts pass is cons tn params impln nusing body) = do opts <- traverse (desugarFnOpt ps) fnopts is' <- for is $ \ (fc, c, n, pi, tm) => do tm' <- desugar AnyExpr ps tm @@ -1226,8 +1226,8 @@ mutual isNamed Nothing = False isNamed (Just _) = True - desugarDecl ps (PRecord fc doc vis mbtot (MkPRecordLater tn params)) - = desugarDecl ps (PData fc doc vis mbtot (MkPLater fc tn (mkRecType params))) + desugarDecl ps (MkFCVal fc $ PRecord doc vis mbtot (MkPRecordLater tn params)) + = desugarDecl ps (MkFCVal fc $ PData doc vis mbtot (MkPLater fc tn (mkRecType params))) where mkRecType : List PBinder -> PTerm mkRecType [] = PType fc @@ -1235,7 +1235,7 @@ mutual = PPi fc c p (Just n.val) t (mkRecType ts) mkRecType (MkPBinder p (MkBasicMultiBinder c (n ::: x :: xs) t) :: ts) = PPi fc c p (Just n.val) t (mkRecType (MkPBinder p (MkBasicMultiBinder c (x ::: xs) t) :: ts)) - desugarDecl ps (PRecord fc doc vis mbtot (MkPRecord tn params opts conname_in fields)) + desugarDecl ps (MkFCVal fc $ PRecord doc vis mbtot (MkPRecord tn params opts conname_in fields)) = do addDocString tn doc params' <- concat <$> traverse (\ (MkPBinder info (MkBasicMultiBinder rig names tm)) => do tm' <- desugar AnyExpr ps tm @@ -1278,7 +1278,7 @@ mutual NS ns (DN str (MN ("__mk" ++ str) 0)) mkConName n = DN (show n) (MN ("__mk" ++ show n) 0) - desugarDecl ps fx@(PFixity $ MkFCVal fc (MkPFixityData vis binding fix prec opNames)) + desugarDecl ps fx@(MkFCVal fc $ PFixity (MkPFixityData vis binding fix prec opNames)) = flip (Core.traverseList1_ {b = Unit}) opNames (\opName : OpStr => do unless (checkValidFixity binding fix prec) (throw $ GenericMsgSol fc @@ -1309,14 +1309,14 @@ mutual addName updatedNS (MkFixityInfo fc (collapseDefault vis) binding fix prec) }) >> pure [] - desugarDecl ps d@(PFail fc mmsg ds) + desugarDecl ps d@(MkFCVal fc $ PFail mmsg ds) = do -- save the state: the content of a failing block should be discarded ust <- get UST md <- get MD opts <- get ROpts syn <- get Syn defs <- branch - log "desugar.failing" 20 $ "Desugaring the block:\n" ++ show d + log "desugar.failing" 20 $ "Desugaring the block:\n" ++ show d.val -- See whether the desugaring phase fails and return -- * Right ds if the desugaring succeeded -- the error will have to come later in the pipeline @@ -1351,22 +1351,22 @@ mutual Right ds => [IFail fc mmsg ds] <$ log "desugar.failing" 20 "Success" Left Nothing => [] <$ log "desugar.failing" 20 "Correctly failed" Left (Just err) => throw err - desugarDecl ps (PMutual (MkFCVal fc ds)) + desugarDecl ps (MkFCVal fc $ PMutual ds) = do let (tys, defs) = splitMutual ds mds' <- traverse (desugarDecl ps) (tys ++ defs) pure (concat mds') - desugarDecl ps (PNamespace fc ns decls) + desugarDecl ps (MkFCVal fc $ PNamespace ns decls) = withExtendedNS ns $ do ds <- traverse (desugarDecl ps) decls pure [INamespace fc ns (concat ds)] - desugarDecl ps (PTransform fc n lhs rhs) + desugarDecl ps (MkFCVal fc $ PTransform n lhs rhs) = do (bound, blhs) <- bindNames False !(desugar LHS ps lhs) rhs' <- desugar AnyExpr (bound ++ ps) rhs pure [ITransform fc (UN $ Basic n) blhs rhs'] - desugarDecl ps (PRunElabDecl fc tm) + desugarDecl ps (MkFCVal fc $ PRunElabDecl tm) = do tm' <- desugar AnyExpr ps tm pure [IRunElabDecl fc tm'] - desugarDecl ps (PDirective $ MkFCVal fc d) + desugarDecl ps (MkFCVal fc $ PDirective d) = case d of Hide (HideName n) => pure [IPragma fc [] (\nest, env => hide fc n)] Hide (HideFixity fx n) => pure [IPragma fc [] (\_, _ => removeFixity fc fx n)] @@ -1411,7 +1411,7 @@ mutual update Ctxt { options->foreignImpl $= (map (n',) calls ++) } )] - desugarDecl ps (PBuiltin fc type name) = pure [IBuiltin fc type name] + desugarDecl ps (MkFCVal fc $ PBuiltin type name) = pure [IBuiltin fc type name] export desugarDo : {auto s : Ref Syn SyntaxInfo} -> diff --git a/src/Idris/Desugar/Mutual.idr b/src/Idris/Desugar/Mutual.idr index 63c73e31e7..bfca852448 100644 --- a/src/Idris/Desugar/Mutual.idr +++ b/src/Idris/Desugar/Mutual.idr @@ -13,19 +13,19 @@ import Data.List1 -- records (just the generated type constructor) -- implementation headers (i.e. note their existence, but not the bodies) -- Everything else on the second pass -getDecl : Pass -> PDecl -> Maybe PDecl -getDecl p (PImplementation fc vis opts _ is cons n ps iname nusing ds) - = Just (PImplementation fc vis opts p is cons n ps iname nusing ds) - -getDecl p (PNamespace fc ns ds) - = Just (PNamespace fc ns (assert_total $ mapMaybe (getDecl p) ds)) - -getDecl AsType d@(PClaim _) = Just d -getDecl AsType (PData fc doc vis mbtot (MkPData dfc tyn (Just tyc) _ _)) - = Just (PData fc doc vis mbtot (MkPLater dfc tyn tyc)) -getDecl AsType d@(PInterface _ _ _ _ _ _ _ _ _) = Just d -getDecl AsType (PRecord fc doc vis mbtot (MkPRecord n ps _ _ _)) - = Just (PData fc doc vis mbtot (MkPLater fc n (mkRecType ps))) +getDecl : Pass -> PDecl-> Maybe PDecl +getDecl p (MkFCVal fc $ PImplementation vis opts _ is cons n ps iname nusing ds) + = Just (MkFCVal fc $ PImplementation vis opts p is cons n ps iname nusing ds) + +getDecl p (MkFCVal fc $ PNamespace ns ds) + = Just (MkFCVal fc $ PNamespace ns (assert_total $ mapMaybe (getDecl p) ds)) + +getDecl AsType d@(MkFCVal _ $ PClaim _) = Just d +getDecl AsType (MkFCVal fc $ PData doc vis mbtot (MkPData dfc tyn (Just tyc) _ _)) + = Just (MkFCVal fc $ PData doc vis mbtot (MkPLater dfc tyn tyc)) +getDecl AsType d@(MkFCVal _ $ PInterface _ _ _ _ _ _ _ _) = Just d +getDecl AsType (MkFCVal fc $ PRecord doc vis mbtot (MkPRecord n ps _ _ _)) + = Just (MkFCVal fc $ PData doc vis mbtot (MkPLater fc n (mkRecType ps))) where mkRecType : List PBinder -> PTerm mkRecType [] = PType fc @@ -34,22 +34,22 @@ getDecl AsType (PRecord fc doc vis mbtot (MkPRecord n ps _ _ _)) mkRecType (MkPBinder p (MkBasicMultiBinder c (n ::: x :: xs) t) :: ts) = PPi fc c p (Just n.val) t (assert_total $ mkRecType (MkPBinder p (MkBasicMultiBinder c (x ::: xs) t) :: ts)) -getDecl AsType d@(PFixity _ ) = Just d -getDecl AsType d@(PDirective _) = Just d +getDecl AsType d@(MkFCVal _ $ PFixity _ ) = Just d +getDecl AsType d@(MkFCVal _ $ PDirective _) = Just d getDecl AsType d = Nothing -getDecl AsDef (PClaim _) = Nothing -getDecl AsDef d@(PData _ _ _ _ (MkPLater _ _ _)) = Just d -getDecl AsDef (PInterface _ _ _ _ _ _ _ _ _) = Nothing -getDecl AsDef d@(PRecord _ _ _ _ (MkPRecordLater _ _)) = Just d -getDecl AsDef (PFixity _ ) = Nothing -getDecl AsDef (PDirective _) = Nothing +getDecl AsDef (MkFCVal _ $ PClaim _) = Nothing +getDecl AsDef d@(MkFCVal _ $ PData _ _ _ (MkPLater _ _ _)) = Just d +getDecl AsDef (MkFCVal _ $ PInterface _ _ _ _ _ _ _ _) = Nothing +getDecl AsDef d@(MkFCVal _ $ PRecord _ _ _ (MkPRecordLater _ _)) = Just d +getDecl AsDef (MkFCVal _ $ PFixity _ ) = Nothing +getDecl AsDef (MkFCVal _ $ PDirective _) = Nothing getDecl AsDef d = Just d -getDecl p (PParameters fc ps pds) - = Just (PParameters fc ps (assert_total $ mapMaybe (getDecl p) pds)) -getDecl p (PUsing fc ps pds) - = Just (PUsing fc ps (assert_total $ mapMaybe (getDecl p) pds)) +getDecl p (MkFCVal fc $ PParameters ps pds) + = Just (MkFCVal fc $ PParameters ps (assert_total $ mapMaybe (getDecl p) pds)) +getDecl p (MkFCVal fc $ PUsing ps pds) + = Just (MkFCVal fc $ PUsing ps (assert_total $ mapMaybe (getDecl p) pds)) getDecl Single d = Just d diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index d1471ba07b..350905698b 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1402,14 +1402,12 @@ dataVisOpt fname <|> do { tot <- totalityOpt fname ; vis <- visibility fname ; pure (vis, Just tot) } <|> pure (defaulted, Nothing) -dataDecl : OriginDesc -> IndentInfo -> Rule PDecl -dataDecl fname indents - = do b <- bounds (do doc <- optDocumentation fname - (vis,mbTot) <- dataVisOpt fname - dat <- dataDeclBody fname indents - pure (doc, vis, mbTot, dat)) - (doc, vis, mbTot, dat) <- pure b.val - pure (PData (boundToFC fname b) doc vis mbTot dat) +dataDecl : (fname : OriginDesc) => (indents : IndentInfo) => Rule PDeclNoFC +dataDecl + = do doc <- optDocumentation fname + (vis,mbTot) <- dataVisOpt fname + dat <- dataDeclBody fname indents + pure (PData doc vis mbTot dat) stripBraces : String -> String stripBraces str = pack (drop '{' (reverse (drop '}' (reverse (unpack str))))) @@ -1438,8 +1436,8 @@ logLevel fname pure (Just (mkLogLevel' topic (fromInteger lvl))) <|> fail "expected a log level" -directive : OriginDesc -> IndentInfo -> Rule Directive -directive fname indents +directive : (fname : OriginDesc) => (indents : IndentInfo) => Rule Directive +directive = do decoratedPragma fname "hide" n <- (fixityNS <|> (HideName <$> name)) atEnd indents @@ -1567,85 +1565,77 @@ namespaceHead fname = do decoratedKeyword fname "namespace" decorate fname Namespace $ mustWork namespaceId -namespaceDecl : OriginDesc -> IndentInfo -> Rule PDecl -namespaceDecl fname indents - = do b <- bounds (do doc <- optDocumentation fname - col <- column - ns <- namespaceHead fname - ds <- blockAfter col (topDecl fname) - pure (doc, ns, ds)) - (doc, ns, ds) <- pure b.val - pure (PNamespace (boundToFC fname b) ns (collectDefs ds)) - -transformDecl : OriginDesc -> IndentInfo -> Rule PDecl -transformDecl fname indents - = do b <- bounds (do decoratedPragma fname "transform" - n <- simpleStr - lhs <- expr plhs fname indents - decoratedSymbol fname "=" - rhs <- expr pnowith fname indents - pure (n, lhs, rhs)) - (n, lhs, rhs) <- pure b.val - pure (PTransform (boundToFC fname b) n lhs rhs) - -runElabDecl : OriginDesc -> IndentInfo -> Rule PDecl -runElabDecl fname indents - = do tm <- bounds $ do - decoratedPragma fname "runElab" - expr pnowith fname indents - pure (PRunElabDecl (boundToFC fname tm) tm.val) - -failDecls : OriginDesc -> IndentInfo -> Rule PDecl -failDecls fname indents - = do msgds <- bounds $ do - col <- column - decoratedKeyword fname "failing" - commit - msg <- optional (decorate fname Data simpleStr) - (msg,) <$> nonEmptyBlockAfter col (topDecl fname) - pure $ - let (msg, ds) = msgds.val - fc = boundToFC fname msgds - in PFail fc msg (collectDefs (forget ds)) - -mutualDecls : OriginDesc -> IndentInfo -> Rule PDecl -mutualDecls fname indents - = do ds <- bounds $ do - col <- column - decoratedKeyword fname "mutual" - commit - nonEmptyBlockAfter col (topDecl fname) - pure (PMutual (mapFC forget ds.withFC)) - -usingDecls : OriginDesc -> IndentInfo -> Rule PDecl -usingDecls fname indents - = do b <- bounds $ do - col <- column - decoratedKeyword fname "using" - commit - decoratedSymbol fname "(" - us <- sepBy (decoratedSymbol fname ",") - (do n <- optional $ do - x <- unqualifiedName - decoratedSymbol fname ":" - pure (UN $ Basic x) - ty <- typeExpr pdef fname indents - pure (n, ty)) - decoratedSymbol fname ")" - ds <- nonEmptyBlockAfter col (topDecl fname) - pure (us, ds) - (us, ds) <- pure b.val - pure (PUsing (boundToFC fname b) us (collectDefs (forget ds))) - -builtinDecl : OriginDesc -> IndentInfo -> Rule PDecl -builtinDecl fname indents - = do b <- bounds (do decoratedPragma fname "builtin" - commit - t <- builtinType - n <- name - pure (t, n)) - (t, n) <- pure b.val - pure $ PBuiltin (boundToFC fname b) t n +parameters {auto fname : OriginDesc} {auto indents : IndentInfo} + namespaceDecl : Rule PDeclNoFC + namespaceDecl + = do doc <- optDocumentation fname -- documentation is not recoded??? + col <- column + ns <- namespaceHead fname + ds <- blockAfter col (topDecl fname) + pure (PNamespace ns (collectDefs ds)) + + transformDecl : Rule PDeclNoFC + transformDecl + = do decoratedPragma fname "transform" + n <- simpleStr + lhs <- expr plhs fname indents + decoratedSymbol fname "=" + rhs <- expr pnowith fname indents + pure (PTransform n lhs rhs) + + runElabDecl : Rule PDeclNoFC + runElabDecl + = do + decoratedPragma fname "runElab" + tm <- expr pnowith fname indents + pure (PRunElabDecl tm) + + ||| failDecls := 'failing' simpleStr? nonEmptyBlock + failDecls : Rule PDeclNoFC + failDecls + = do + col <- column + decoratedKeyword fname "failing" + commit + msg <- optional (decorate fname Data simpleStr) + ds <- nonEmptyBlockAfter col (topDecl fname) + pure $ PFail msg (collectDefs $ forget ds) + + ||| mutualDecls := 'mutual' nonEmptyBlock + mutualDecls : Rule PDeclNoFC + mutualDecls + = do + col <- column + decoratedKeyword fname "mutual" + commit + ds <- nonEmptyBlockAfter col (topDecl fname) + pure (PMutual (forget ds)) + + usingDecls : Rule PDeclNoFC + usingDecls + = do col <- column + decoratedKeyword fname "using" + commit + decoratedSymbol fname "(" + us <- sepBy (decoratedSymbol fname ",") + (do n <- optional $ do + x <- unqualifiedName + decoratedSymbol fname ":" + pure (UN $ Basic x) + ty <- typeExpr pdef fname indents + pure (n, ty)) + decoratedSymbol fname ")" + ds <- nonEmptyBlockAfter col (topDecl fname) + pure (PUsing us (collectDefs (forget ds))) + + ||| builtinDecl := 'builtin' builtinType name + builtinDecl : Rule PDeclNoFC + builtinDecl + = do decoratedPragma fname "builtin" + commit + t <- builtinType + n <- name + pure $ PBuiltin t n visOpt : OriginDesc -> Rule (Either Visibility PFnOpt) visOpt fname @@ -1723,70 +1713,8 @@ implBinds fname indents namedImpl = concatMap (map adjust) <$> go where pure (ns :: more) <|> pure [] -ifaceParam : OriginDesc -> IndentInfo -> Rule BasicMultiBinder -ifaceParam fname indents - = parens fname basicMultiBinder - <|> do n <- fcBounds (decorate fname Bound name) - pure (MkBasicMultiBinder erased (singleton n) (PInfer n.fc)) - -ifaceDecl : OriginDesc -> IndentInfo -> Rule PDecl -ifaceDecl fname indents - = do b <- bounds (do doc <- optDocumentation fname - vis <- visibility fname - col <- column - decoratedKeyword fname "interface" - commit - cons <- constraints fname indents - n <- decorate fname Typ name - params <- many (ifaceParam fname indents) - det <- option [] $ decoratedSymbol fname "|" *> sepBy (decoratedSymbol fname ",") (decorate fname Bound name) - decoratedKeyword fname "where" - dc <- optional (recordConstructor fname) - body <- blockAfter col (topDecl fname) - pure (\fc : FC => PInterface fc - vis cons n doc params det dc (collectDefs body))) - pure (b.val (boundToFC fname b)) - -implDecl : OriginDesc -> IndentInfo -> Rule PDecl -implDecl fname indents - = do b <- bounds (do doc <- optDocumentation fname - visOpts <- many (visOpt fname) - vis <- getVisibility Nothing visOpts - let opts = mapMaybe getRight visOpts - col <- column - option () (decoratedKeyword fname "implementation") - iname <- optional $ decoratedSymbol fname "[" - *> decorate fname Function name - <* decoratedSymbol fname "]" - impls <- implBinds fname indents (isJust iname) - cons <- constraints fname indents - n <- decorate fname Typ name - params <- many (continue indents *> simpleExpr fname indents) - nusing <- option [] $ decoratedKeyword fname "using" - *> forget <$> some (decorate fname Function name) - body <- optional $ decoratedKeyword fname "where" *> blockAfter col (topDecl fname) - pure $ \fc : FC => - (PImplementation fc vis opts Single impls cons n params iname nusing - (map collectDefs body))) - atEnd indents - pure (b.val (boundToFC fname b)) - -localClaim : OriginDesc -> IndentInfo -> Rule (WithFC PClaimData) -localClaim fname indents - = do bs <- bounds (do - doc <- optDocumentation fname - visOpts <- many (visOpt fname) - vis <- getVisibility Nothing visOpts - let opts = mapMaybe getRight visOpts - rig <- multiplicity fname - cls <- tyDecls (decorate fname Function name) - doc fname indents - pure $ MkPClaim rig vis opts cls - ) - pure bs.withFC - -fieldDecl : OriginDesc -> IndentInfo -> Rule PField -fieldDecl fname indents +fieldDecl : (fname : OriginDesc) => IndentInfo -> Rule PField +fieldDecl indents = do doc <- optDocumentation fname decoratedSymbol fname "{" commit @@ -1813,112 +1741,172 @@ fieldDecl fname indents pure (MkRecordField doc rig p (forget ns) ty)) pure b.withFC --- A Single binder with multiple names -typedArg : (fname : OriginDesc) => (indents : IndentInfo) => Rule PBinder -typedArg - = do params <- parens fname $ pibindListName fname indents - pure $ MkPBinder Explicit params - <|> do decoratedSymbol fname "{" - commit - info <- - (pure AutoImplicit <* decoratedKeyword fname "auto" - <|> (decoratedKeyword fname "default" *> DefImplicit <$> simpleExpr fname indents) - <|> pure Implicit) - params <- pibindListName fname indents - decoratedSymbol fname "}" - pure $ MkPBinder info params - -recordParam : OriginDesc -> IndentInfo -> Rule (PBinder) -recordParam fname indents - = typedArg - <|> do n <- fcBounds (decoratedSimpleBinderUName fname) - pure (MkFullBinder Explicit top n $ PInfer n.fc) - --- A record without a where is a forward declaration -recordBody : OriginDesc -> IndentInfo -> - String -> WithDefault Visibility Private -> - Maybe TotalReq -> - Int -> - Name -> - List PBinder -> - EmptyRule (FC -> PDecl) -recordBody fname indents doc vis mbtot col n params - = do atEndIndent indents - pure (\fc : FC => PRecord fc doc vis mbtot (MkPRecordLater n params)) - <|> do mustWork $ decoratedKeyword fname "where" - opts <- dataOpts fname - dcflds <- blockWithOptHeaderAfter col - (\ idt => recordConstructor fname <* atEnd idt) - (fieldDecl fname) - pure (\fc : FC => PRecord fc doc vis mbtot - (MkPRecord n params opts (fst dcflds) (snd dcflds))) - -recordDecl : OriginDesc -> IndentInfo -> Rule PDecl -recordDecl fname indents - = do b <- bounds (do doc <- optDocumentation fname - (vis,mbtot) <- dataVisOpt fname - col <- column - decoratedKeyword fname "record" - n <- mustWork (decoratedDataTypeName fname) - paramss <- many (continue indents >> recordParam fname indents) - recordBody fname indents doc vis mbtot col n paramss) - pure (b.val (boundToFC fname b)) - -||| Parameter blocks -||| BNF: -||| paramDecls := 'parameters' (oldParamDecls | newParamDecls) indentBlockDefs -paramDecls : OriginDesc -> IndentInfo -> Rule PDecl -paramDecls fname indents = do - startCol <- column - b1 <- bounds (decoratedKeyword fname "parameters") - commit - args <- bounds (Right <$> newParamDecls <|> Left <$> oldParamDecls) - commit - declarations <- bounds $ nonEmptyBlockAfter startCol (topDecl fname) - mergedBounds <- pure $ b1 `mergeBounds` (args `mergeBounds` declarations) - pure (PParameters (boundToFC fname mergedBounds) args.val - (collectDefs (forget declarations.val))) +parameters {auto fname : OriginDesc} {auto indents : IndentInfo} + + ifaceParam : Rule BasicMultiBinder + ifaceParam + = parens fname basicMultiBinder + <|> do n <- fcBounds (decorate fname Bound name) + pure (MkBasicMultiBinder erased (singleton n) (PInfer n.fc)) + + ifaceDecl : Rule PDeclNoFC + ifaceDecl + = do doc <- optDocumentation fname + vis <- visibility fname + col <- column + decoratedKeyword fname "interface" + commit + cons <- constraints fname indents + n <- decorate fname Typ name + params <- many ifaceParam + det <- option [] $ decoratedSymbol fname "|" *> sepBy (decoratedSymbol fname ",") (decorate fname Bound name) + decoratedKeyword fname "where" + dc <- optional (recordConstructor fname) + body <- blockAfter col (topDecl fname) + pure (PInterface + vis cons n doc params det dc (collectDefs body)) + + implDecl : Rule PDeclNoFC + implDecl + = do doc <- optDocumentation fname + visOpts <- many (visOpt fname) + vis <- getVisibility Nothing visOpts + let opts = mapMaybe getRight visOpts + col <- column + option () (decoratedKeyword fname "implementation") + iname <- optional $ decoratedSymbol fname "[" + *> decorate fname Function name + <* decoratedSymbol fname "]" + impls <- implBinds fname indents (isJust iname) + cons <- constraints fname indents + n <- decorate fname Typ name + params <- many (continue indents *> simpleExpr fname indents) + nusing <- option [] $ decoratedKeyword fname "using" + *> forget <$> some (decorate fname Function name) + body <- optional $ decoratedKeyword fname "where" *> blockAfter col (topDecl fname) + atEnd indents + pure $ + PImplementation vis opts Single impls cons n params iname nusing + (map collectDefs body) + + localClaim : Rule PClaimData + localClaim + = do doc <- optDocumentation fname + visOpts <- many (visOpt fname) + vis <- getVisibility Nothing visOpts + let opts = mapMaybe getRight visOpts + rig <- multiplicity fname + cls <- tyDecls (decorate fname Function name) + doc fname indents + pure $ MkPClaim rig vis opts cls + + + -- A Single binder with multiple names + typedArg : Rule PBinder + typedArg + = do params <- parens fname $ pibindListName fname indents + pure $ MkPBinder Explicit params + <|> do decoratedSymbol fname "{" + commit + info <- + (pure AutoImplicit <* decoratedKeyword fname "auto" + <|> (decoratedKeyword fname "default" *> DefImplicit <$> simpleExpr fname indents) + <|> pure Implicit) + params <- pibindListName fname indents + decoratedSymbol fname "}" + pure $ MkPBinder info params + + recordParam : Rule (PBinder) + recordParam + = typedArg + <|> do n <- fcBounds (decoratedSimpleBinderUName fname) + pure (MkFullBinder Explicit top n $ PInfer n.fc) + + -- A record without a where is a forward declaration + recordBody : String -> WithDefault Visibility Private -> + Maybe TotalReq -> + Int -> + Name -> + List PBinder -> + EmptyRule PDeclNoFC + recordBody doc vis mbtot col n params + = do atEndIndent indents + pure (PRecord doc vis mbtot (MkPRecordLater n params)) + <|> do mustWork $ decoratedKeyword fname "where" + opts <- dataOpts fname + dcflds <- blockWithOptHeaderAfter col + (\ idt => recordConstructor fname <* atEnd idt) + fieldDecl + pure (PRecord doc vis mbtot + (MkPRecord n params opts (fst dcflds) (snd dcflds))) + + recordDecl : Rule PDeclNoFC + recordDecl + = do doc <- optDocumentation fname + (vis,mbtot) <- dataVisOpt fname + col <- column + decoratedKeyword fname "record" + n <- mustWork (decoratedDataTypeName fname) + paramss <- many (continue indents >> recordParam) + recordBody doc vis mbtot col n paramss + + ||| Parameter blocks + ||| BNF: + ||| paramDecls := 'parameters' (oldParamDecls | newParamDecls) indentBlockDefs + paramDecls : Rule PDeclNoFC + paramDecls = do + startCol <- column + b1 <- decoratedKeyword fname "parameters" + commit + args <- Right <$> newParamDecls <|> Left <$> oldParamDecls + commit + declarations <- nonEmptyBlockAfter startCol (topDecl fname) + pure (PParameters args + (collectDefs (forget declarations))) - where - oldParamDecls : Rule (List1 PlainBinder) - oldParamDecls - = parens fname $ sepBy1 (decoratedSymbol fname ",") plainBinder - - newParamDecls : Rule (List1 PBinder) - newParamDecls = some typedArg - - --- topLevelClaim is for claims appearing at the top-level of the file --- localClaim is for claims appearing in nested positions, like `let` or `record` in the future -topLevelClaim : OriginDesc -> IndentInfo -> Rule PDecl -topLevelClaim o i = PClaim <$> localClaim o i - -definition : OriginDesc -> IndentInfo -> Rule PDecl -definition fname indents - = do nd <- bounds (clause 0 Nothing fname indents) - pure (PDef $ MkFCVal (boundToFC fname nd) [nd.val]) - -operatorBindingKeyword : OriginDesc -> EmptyRule BindingModifier -operatorBindingKeyword fname - = (decoratedKeyword fname "autobind" >> pure Autobind) - <|> (decoratedKeyword fname "typebind" >> pure Typebind) - <|> pure NotBinding - -fixDecl : OriginDesc -> IndentInfo -> Rule PDecl -fixDecl fname indents - = do vis <- exportVisibility fname - binding <- operatorBindingKeyword fname - b <- bounds (do fixity <- decorate fname Keyword $ fix - commit - prec <- decorate fname Keyword $ intLit - ops <- sepBy1 (decoratedSymbol fname ",") iOperator - pure (MkPFixityData vis binding fixity (fromInteger prec) ops) - ) - pure (PFixity b.withFC) - -directiveDecl : OriginDesc -> IndentInfo -> Rule PDecl -directiveDecl fname indents - = PDirective . (.withFC) <$> bounds (directive fname indents) + where + oldParamDecls : Rule (List1 PlainBinder) + oldParamDecls + = parens fname $ sepBy1 (decoratedSymbol fname ",") plainBinder + + newParamDecls : Rule (List1 PBinder) + newParamDecls = some typedArg + + + -- topLevelClaim is for claims appearing at the top-level of the file + -- localClaim is for claims appearing in nested positions, like `let` or `record` in the future + topLevelClaim : Rule PDeclNoFC + topLevelClaim = PClaim <$> localClaim + + definition : Rule PDeclNoFC + definition + = do nd <- clause 0 Nothing fname indents + pure (PDef (singleton nd)) + + operatorBindingKeyword : EmptyRule BindingModifier + operatorBindingKeyword + = (decoratedKeyword fname "autobind" >> pure Autobind) + <|> (decoratedKeyword fname "typebind" >> pure Typebind) + <|> pure NotBinding + + fixDecl : Rule PDecl + fixDecl + = do vis <- exportVisibility fname + binding <- operatorBindingKeyword + b <- fcBounds (do fixity <- decorate fname Keyword $ fix + commit + prec <- decorate fname Keyword $ intLit + ops <- sepBy1 (decoratedSymbol fname ",") iOperator + pure (MkPFixityData vis binding fixity (fromInteger prec) ops) + ) + pure (mapFC PFixity b) + +cgDirectiveDecl : Rule PDeclNoFC +cgDirectiveDecl + = (>>=) {c1 = True, c2 = False} cgDirective $ \dir => + let (cg1, cg2) = span isAlphaNum dir + in the (EmptyRule PDeclNoFC) $ pure $ + PDirective (CGAction cg1 (stripBraces (trim cg2))) -- Declared at the top -- topDecl : OriginDesc -> IndentInfo -> Rule (List PDecl) @@ -1927,29 +1915,23 @@ topDecl fname indents -- i.e. the claim "String : Type" is a parse error, but the underlying reason may not be clear to new users. = do id <- anyReservedIdent the (Rule PDecl) $ fatalLoc id.bounds "Cannot begin a declaration with a reserved identifier" - <|> dataDecl fname indents - <|> topLevelClaim fname indents - <|> directiveDecl fname indents - <|> implDecl fname indents - <|> definition fname indents - <|> fixDecl fname indents - <|> ifaceDecl fname indents - <|> recordDecl fname indents - <|> namespaceDecl fname indents - <|> failDecls fname indents - <|> mutualDecls fname indents - <|> paramDecls fname indents - <|> usingDecls fname indents - <|> builtinDecl fname indents - <|> runElabDecl fname indents - <|> transformDecl fname indents - <|> do dstr <- bounds (terminal "Expected CG directive" - (\case - CGDirective d => Just d - _ => Nothing)) - pure (let cgrest = span isAlphaNum dstr.val in - PDirective $ MkFCVal (boundToFC fname dstr) - (CGAction (fst cgrest) (stripBraces (trim (snd cgrest))))) + <|> fcBounds dataDecl + <|> fcBounds topLevelClaim + <|> fcBounds (PDirective <$> directive) + <|> fcBounds implDecl + <|> fcBounds definition + <|> fixDecl + <|> fcBounds ifaceDecl + <|> fcBounds recordDecl + <|> fcBounds namespaceDecl + <|> fcBounds failDecls + <|> fcBounds mutualDecls + <|> fcBounds paramDecls + <|> fcBounds usingDecls + <|> fcBounds builtinDecl + <|> fcBounds runElabDecl + <|> fcBounds transformDecl + <|> fcBounds cgDirectiveDecl -- If the user tried to begin a declaration with any other keyword, then show a more informative error. <|> do kw <- bounds anyKeyword the (Rule PDecl) $ fatalLoc kw.bounds "Keyword '\{kw.val}' is not a valid start to a declaration" @@ -1963,7 +1945,7 @@ topDecl fname indents -- Declared at the top. -- collectDefs : List PDecl -> List PDecl collectDefs [] = [] -collectDefs (PDef (MkFCVal annot cs) :: ds) +collectDefs (MkFCVal annot (PDef cs) :: ds) = let (csWithFC, rest) = spanBy isPDef ds cs' = cs ++ concat (map val csWithFC) annot' = foldr @@ -1971,11 +1953,11 @@ collectDefs (PDef (MkFCVal annot cs) :: ds) annot (map fc csWithFC) in - PDef (MkFCVal annot' cs') :: assert_total (collectDefs rest) -collectDefs (PNamespace annot ns nds :: ds) - = PNamespace annot ns (collectDefs nds) :: collectDefs ds -collectDefs (PMutual nds :: ds) - = PMutual (mapFC collectDefs nds) :: collectDefs ds + MkFCVal annot' (PDef cs') :: assert_total (collectDefs rest) +collectDefs (MkFCVal annot (PNamespace ns nds) :: ds) + = MkFCVal annot (PNamespace ns (collectDefs nds)) :: collectDefs ds +collectDefs (MkFCVal fc (PMutual nds) :: ds) + = MkFCVal fc (PMutual (collectDefs nds)) :: collectDefs ds collectDefs (d :: ds) = d :: collectDefs ds diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index 66968e1980..0a29db951d 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -79,10 +79,10 @@ processDecl : {auto c : Ref Ctxt Defs} -> -- Special cases to avoid treating these big blocks as units -- This should give us better error recovery (the whole block won't fail -- as soon as one of the definitions fails) -processDecl (PNamespace fc ns ps) +processDecl (MkFCVal fc $ PNamespace ns ps) = withExtendedNS ns $ processDecls ps -processDecl (PMutual ps) - = let (tys, defs) = splitMutual ps.val in +processDecl (MkFCVal _ $ PMutual ps) + = let (tys, defs) = splitMutual ps in processDecls (tys ++ defs) processDecl decl diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index e4af8cba00..406f2f588a 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -529,14 +529,14 @@ mutual ImpDecl' KindedName -> Core (Maybe (PDecl' KindedName)) toPDecl (IClaim (MkFCVal fc $ MkIClaimData rig vis opts ty)) = do opts' <- traverse toPFnOpt opts - pure (Just (PClaim (MkFCVal fc $ MkPClaim rig vis opts' !(toPTypeDecl ty)))) + pure (Just (MkFCVal fc $ PClaim (MkPClaim rig vis opts' !(toPTypeDecl ty)))) toPDecl (IData fc vis mbtot d) - = pure (Just (PData fc "" vis mbtot !(toPData d))) + = pure (Just (MkFCVal fc $ PData "" vis mbtot !(toPData d))) toPDecl (IDef fc n cs) - = pure (Just (PDef $ MkFCVal fc !(traverse toPClause cs))) + = pure (Just (MkFCVal fc $ PDef !(traverse toPClause cs))) toPDecl (IParameters fc ps ds) = do ds' <- traverse toPDecl ds - pure (Just (PParameters fc + pure (Just (MkFCVal fc $ PParameters (Right !(traverseList1 (\(n, rig, info, tpe) => do info' <- traverse (toPTerm startPrec) info tpe' <- toPTerm startPrec tpe @@ -546,7 +546,7 @@ mutual (catMaybes ds'))) toPDecl (IRecord fc _ vis mbtot r) = do (n, ps, opts, con, fs) <- toPRecord r - pure (Just (PRecord fc "" vis mbtot (MkPRecord n (map toBinder ps) opts con fs))) + pure (Just (MkFCVal fc $ PRecord "" vis mbtot (MkPRecord n (map toBinder ps) opts con fs))) where toBinder : (Name, ZeroOneOmega, PiInfo (PTerm' KindedName), PTerm' KindedName) -> PBinder' KindedName toBinder (n, rig, info, ty) @@ -556,19 +556,19 @@ mutual toPDecl (IFail fc msg ds) = do ds' <- traverse toPDecl ds - pure (Just (PFail fc msg (catMaybes ds'))) + pure (Just (MkFCVal fc $ PFail msg (catMaybes ds'))) toPDecl (INamespace fc ns ds) = do ds' <- traverse toPDecl ds - pure (Just (PNamespace fc ns (catMaybes ds'))) + pure (Just (MkFCVal fc $ PNamespace ns (catMaybes ds'))) toPDecl (ITransform fc n lhs rhs) - = pure (Just (PTransform fc (show n) + = pure (Just (MkFCVal fc $ PTransform (show n) !(toPTerm startPrec lhs) !(toPTerm startPrec rhs))) toPDecl (IRunElabDecl fc tm) - = pure (Just (PRunElabDecl fc !(toPTerm startPrec tm))) + = pure (Just (MkFCVal fc $ PRunElabDecl !(toPTerm startPrec tm))) toPDecl (IPragma _ _ _) = pure Nothing toPDecl (ILog _) = pure Nothing - toPDecl (IBuiltin fc type name) = pure $ Just $ PBuiltin fc type name + toPDecl (IBuiltin fc type name) = pure $ Just $ MkFCVal fc $ PBuiltin type name export cleanPTerm : {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 968aa0f9ab..f7385e2131 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -574,19 +574,17 @@ mutual PDecl = PDecl' Name public export - data PDecl' : Type -> Type where - PClaim : WithFC (PClaimData' nm) -> PDecl' nm - PDef : WithFC (List (PClause' nm)) -> PDecl' nm - PData : FC -> (doc : String) -> WithDefault Visibility Private -> - Maybe TotalReq -> PDataDecl' nm -> PDecl' nm - PParameters : FC -> - Either (List1 (PlainBinder' nm)) + data PDeclNoFC' : Type -> Type where + PClaim : PClaimData' nm -> PDeclNoFC' nm + PDef : List (PClause' nm) -> PDeclNoFC' nm + PData : (doc : String) -> WithDefault Visibility Private -> + Maybe TotalReq -> PDataDecl' nm -> PDeclNoFC' nm + PParameters : Either (List1 (PlainBinder' nm)) (List1 (PBinder' nm)) -> - List (PDecl' nm) -> PDecl' nm - PUsing : FC -> List (Maybe Name, PTerm' nm) -> - List (PDecl' nm) -> PDecl' nm - PInterface : FC -> - WithDefault Visibility Private -> + List (PDecl' nm) -> PDeclNoFC' nm + PUsing : List (Maybe Name, PTerm' nm) -> + List (PDecl' nm) -> PDeclNoFC' nm + PInterface : WithDefault Visibility Private -> (constraints : List (Maybe Name, PTerm' nm)) -> Name -> (doc : String) -> @@ -594,9 +592,8 @@ mutual (det : List Name) -> (conName : Maybe (String, Name)) -> List (PDecl' nm) -> - PDecl' nm - PImplementation : FC -> - Visibility -> List PFnOpt -> Pass -> + PDeclNoFC' nm + PImplementation : Visibility -> List PFnOpt -> Pass -> (implicits : List (FC, RigCount, Name, PiInfo (PTerm' nm), PTerm' nm)) -> (constraints : List (Maybe Name, PTerm' nm)) -> Name -> @@ -604,50 +601,38 @@ mutual (implName : Maybe Name) -> (nusing : List Name) -> Maybe (List (PDecl' nm)) -> - PDecl' nm - PRecord : FC -> - (doc : String) -> + PDeclNoFC' nm + PRecord : (doc : String) -> WithDefault Visibility Private -> Maybe TotalReq -> PRecordDecl' nm -> - PDecl' nm + PDeclNoFC' nm -- TODO: PPostulate -- TODO: POpen (for opening named interfaces) ||| PFail is a failing block. The string must appear as a ||| substring of the error message raised when checking the block. - PFail : FC -> Maybe String -> List (PDecl' nm) -> PDecl' nm + PFail : Maybe String -> List (PDecl' nm) -> PDeclNoFC' nm - PMutual : WithFC (List (PDecl' nm)) -> PDecl' nm - PFixity : WithFC PFixityData -> PDecl' nm - PNamespace : FC -> Namespace -> List (PDecl' nm) -> PDecl' nm - PTransform : FC -> String -> PTerm' nm -> PTerm' nm -> PDecl' nm - PRunElabDecl : FC -> PTerm' nm -> PDecl' nm - PDirective : WithFC Directive -> PDecl' nm - PBuiltin : FC -> BuiltinType -> Name -> PDecl' nm + PMutual : List (PDecl' nm) -> PDeclNoFC' nm + PFixity : PFixityData -> PDeclNoFC' nm + PNamespace : Namespace -> List (PDecl' nm) -> PDeclNoFC' nm + PTransform : String -> PTerm' nm -> PTerm' nm -> PDeclNoFC' nm + PRunElabDecl : PTerm' nm -> PDeclNoFC' nm + PDirective : Directive -> PDeclNoFC' nm + PBuiltin : BuiltinType -> Name -> PDeclNoFC' nm + + public export + PDeclNoFC : Type + PDeclNoFC = PDeclNoFC' Name + + public export + PDecl' : Type -> Type + PDecl' x = WithFC (PDeclNoFC' x) export getPDeclLoc : PDecl' nm -> FC - getPDeclLoc (PClaim c) = c.fc - getPDeclLoc (PDef c) = c.fc - getPDeclLoc (PData fc _ _ _ _) = fc - getPDeclLoc (PParameters fc _ _) = fc - getPDeclLoc (PUsing fc _ _) = fc - getPDeclLoc (PInterface fc _ _ _ _ _ _ _ _) = fc - getPDeclLoc (PImplementation fc _ _ _ _ _ _ _ _ _ _) = fc - getPDeclLoc (PRecord fc _ _ _ _) = fc - getPDeclLoc (PMutual x) = x.fc - getPDeclLoc (PFail fc _ _) = fc - getPDeclLoc (PFixity pf) = pf.fc - getPDeclLoc (PNamespace fc _ _) = fc - getPDeclLoc (PTransform fc _ _ _) = fc - getPDeclLoc (PRunElabDecl fc _) = fc - getPDeclLoc (PDirective d) = d.fc - getPDeclLoc (PBuiltin fc _ _) = fc - -export -HasFC (PDecl' nm) where - (.getFC) = getPDeclLoc + getPDeclLoc x = x.fc export isStrInterp : PStr -> Maybe FC @@ -661,7 +646,7 @@ isStrLiteral (StrLiteral fc str) = Just (fc, str) export isPDef : PDecl -> Maybe (WithFC (List PClause)) -isPDef (PDef cs) = Just cs +isPDef (MkFCVal fc (PDef cs)) = Just (MkFCVal fc cs) isPDef _ = Nothing @@ -670,13 +655,13 @@ definedInData (MkPData _ n _ _ cons) = n :: concatMap (.nameList) cons definedInData (MkPLater _ n _) = [n] export -definedIn : List PDecl -> List Name +definedIn : List PDeclNoFC -> List Name definedIn [] = [] -definedIn (PClaim claim :: ds) = claim.val.type.nameList ++ definedIn ds -definedIn (PData _ _ _ _ d :: ds) = definedInData d ++ definedIn ds -definedIn (PParameters _ _ pds :: ds) = definedIn pds ++ definedIn ds -definedIn (PUsing _ _ pds :: ds) = definedIn pds ++ definedIn ds -definedIn (PNamespace _ _ ns :: ds) = definedIn ns ++ definedIn ds +definedIn (PClaim claim :: ds) = claim.type.nameList ++ definedIn ds +definedIn (PData _ _ _ d :: ds) = definedInData d ++ definedIn ds +definedIn (PParameters _ pds :: ds) = definedIn (map val pds) ++ definedIn ds +definedIn (PUsing _ pds :: ds) = definedIn (map val pds) ++ definedIn ds +definedIn (PNamespace _ ns :: ds) = definedIn (map val ns) ++ definedIn ds definedIn (_ :: ds) = definedIn ds public export @@ -1255,16 +1240,16 @@ Show PClaimData where -- TODO: finish writing this instance export covering -Show PDecl where - show (PClaim pclaim) = show pclaim.val - show (PDef cls) = unlines (show <$> cls.val) +Show PDeclNoFC where + show (PClaim pclaim) = show pclaim + show (PDef cls) = unlines (show <$> cls) show (PData{}) = "PData" show (PParameters{}) = "PParameters" show (PUsing{}) = "PUsing" show (PInterface{}) = "PInterface" show (PImplementation{}) = "PImplementation" show (PRecord{}) = "PRecord" - show (PFail _ mstr ds) = unlines (unwords ("failing" :: maybe [] (pure . show) mstr) :: (show <$> ds)) + show (PFail mstr ds) = unlines (unwords ("failing" :: maybe [] (pure . show) mstr) :: (show . val <$> ds)) show (PMutual{}) = "PMutual" show (PFixity{}) = "PFixity" show (PNamespace{}) = "PNamespace" diff --git a/src/Idris/Syntax/Traversals.idr b/src/Idris/Syntax/Traversals.idr index f37067ac03..f67657aa5b 100644 --- a/src/Idris/Syntax/Traversals.idr +++ b/src/Idris/Syntax/Traversals.idr @@ -46,7 +46,7 @@ mapPTermM f = goPTerm where <*> goPClauses xs >>= f goPTerm (PLocal fc xs scope) = - PLocal fc <$> goPDecls xs + PLocal fc <$> traverse (traverseFC goPDecl) xs <*> goPTerm scope >>= f goPTerm (PUpdate fc xs) = @@ -85,7 +85,7 @@ mapPTermM f = goPTerm where >>= f goPTerm t@(PQuoteName _ _) = f t goPTerm (PQuoteDecl fc x) = - PQuoteDecl fc <$> traverse goPDecl x + PQuoteDecl fc <$> goPDecls x >>= f goPTerm (PUnquote fc x) = PUnquote fc <$> goPTerm x @@ -268,49 +268,49 @@ mapPTermM f = goPTerm where -- goParamArgs : - goPDecl : PDecl' nm -> Core (PDecl' nm) + goPDecl : PDeclNoFC' nm -> Core (PDeclNoFC' nm) goPDecl (PClaim claim) = - PClaim <$> traverseFC goPClaim claim - goPDecl (PDef cls) = PDef <$> traverseFC goPClauses cls - goPDecl (PData fc doc v mbt d) = PData fc doc v mbt <$> goPDataDecl d - goPDecl (PParameters fc nts ps) = - PParameters fc <$> either (\x => Left <$> traverseList1 goPlainBinder x) - (\x => Right <$> traverseList1 goPBinder x) nts -- go4TupledPTerms nts - <*> goPDecls ps - goPDecl (PUsing fc mnts ps) = - PUsing fc <$> goPairedPTerms mnts - <*> goPDecls ps - goPDecl (PInterface fc v mnts n doc nrts ns mn ps) = - PInterface fc v <$> goPairedPTerms mnts - <*> pure n - <*> pure doc - <*> traverse goBasicMultiBinder nrts - <*> pure ns - <*> pure mn - <*> goPDecls ps - goPDecl (PImplementation fc v opts p is cs n ts mn ns mps) = - PImplementation fc v opts p <$> goImplicits is - <*> goPairedPTerms cs - <*> pure n - <*> goPTerms ts - <*> pure mn - <*> pure ns - <*> goMPDecls mps - goPDecl (PRecord fc doc v tot (MkPRecord n nts opts mn fs)) = - pure $ PRecord fc doc v tot !(MkPRecord n <$> traverse goPBinder nts - <*> pure opts - <*> pure mn - <*> goPFields fs) - goPDecl (PRecord fc doc v tot (MkPRecordLater n nts)) = - pure $ PRecord fc doc v tot (MkPRecordLater n !(traverse goPBinder nts)) - goPDecl (PFail fc msg ps) = PFail fc msg <$> goPDecls ps - goPDecl (PMutual ps) = PMutual <$> traverseFC goPDecls ps + PClaim <$> goPClaim claim + goPDecl (PDef cls) = PDef <$> goPClauses cls + goPDecl (PData doc v mbt d) = PData doc v mbt <$> goPDataDecl d + goPDecl (PParameters nts ps) = + PParameters <$> either (\x => Left <$> traverseList1 goPlainBinder x) + (\x => Right <$> traverseList1 goPBinder x) nts -- go4TupledPTerms nts + <*> goPDecls ps + goPDecl (PUsing mnts ps) = + PUsing <$> goPairedPTerms mnts + <*> goPDecls ps + goPDecl (PInterface v mnts n doc nrts ns mn ps) = + PInterface v <$> goPairedPTerms mnts + <*> pure n + <*> pure doc + <*> traverse goBasicMultiBinder nrts + <*> pure ns + <*> pure mn + <*> goPDecls ps + goPDecl (PImplementation v opts p is cs n ts mn ns mps) = + PImplementation v opts p <$> goImplicits is + <*> goPairedPTerms cs + <*> pure n + <*> goPTerms ts + <*> pure mn + <*> pure ns + <*> goMPDecls mps + goPDecl (PRecord doc v tot (MkPRecord n nts opts mn fs)) = + pure $ PRecord doc v tot !(MkPRecord n <$> traverse goPBinder nts + <*> pure opts + <*> pure mn + <*> goPFields fs) + goPDecl (PRecord doc v tot (MkPRecordLater n nts)) = + pure $ PRecord doc v tot (MkPRecordLater n !(traverse goPBinder nts)) + goPDecl (PFail msg ps) = PFail msg <$> goPDecls ps + goPDecl (PMutual ps) = PMutual <$> goPDecls ps goPDecl (PFixity p) = pure (PFixity p) - goPDecl (PNamespace fc strs ps) = PNamespace fc strs <$> goPDecls ps - goPDecl (PTransform fc n a b) = PTransform fc n <$> goPTerm a <*> goPTerm b - goPDecl (PRunElabDecl fc a) = PRunElabDecl fc <$> goPTerm a + goPDecl (PNamespace strs ps) = PNamespace strs <$> goPDecls ps + goPDecl (PTransform n a b) = PTransform n <$> goPTerm a <*> goPTerm b + goPDecl (PRunElabDecl a) = PRunElabDecl <$> goPTerm a goPDecl (PDirective d) = pure (PDirective d) - goPDecl p@(PBuiltin _ _ _) = pure p + goPDecl p@(PBuiltin _ _) = pure p goPTypeDecl : PTypeDeclData' nm -> Core (PTypeDeclData' nm) @@ -403,7 +403,7 @@ mapPTermM f = goPTerm where goPDecls : List (PDecl' nm) -> Core (List (PDecl' nm)) goPDecls [] = pure [] - goPDecls (d :: ds) = (::) <$> goPDecl d <*> goPDecls ds + goPDecls (MkFCVal fc d :: ds) = (::) <$> (MkFCVal fc <$> goPDecl d) <*> goPDecls ds goPFieldUpdates : List (PFieldUpdate' nm) -> Core (List (PFieldUpdate' nm)) goPFieldUpdates [] = pure [] @@ -442,7 +442,7 @@ mapPTerm f = goPTerm where goPTerm (PCase fc opts x xs) = f $ PCase fc (goPFnOpt <$> opts) (goPTerm x) (goPClause <$> xs) goPTerm (PLocal fc xs scope) - = f $ PLocal fc (goPDecl <$> xs) (goPTerm scope) + = f $ PLocal fc (map (mapFC goPDecl) xs) (goPTerm scope) goPTerm (PUpdate fc xs) = f $ PUpdate fc (goPFieldUpdate <$> xs) goPTerm (PApp fc x y) @@ -465,7 +465,7 @@ mapPTerm f = goPTerm where = f $ PQuote fc $ goPTerm x goPTerm t@(PQuoteName _ _) = f t goPTerm (PQuoteDecl fc x) - = f $ PQuoteDecl fc (goPDecl <$> x) + = f $ PQuoteDecl fc (map (mapFC goPDecl) x) goPTerm (PUnquote fc x) = f $ PUnquote fc $ goPTerm x goPTerm (PRunElab fc x) @@ -544,7 +544,7 @@ mapPTerm f = goPTerm where = DoLet fc lhsFC n c (goPTerm t) (goPTerm scope) goPDo (DoLetPat fc pat t scope cls) = DoLetPat fc (goPTerm pat) (goPTerm t) (goPTerm scope) (goPClause <$> cls) - goPDo (DoLetLocal fc decls) = DoLetLocal fc $ goPDecl <$> decls + goPDo (DoLetLocal fc decls) = DoLetLocal fc $ map (mapFC goPDecl) decls goPDo (DoRewrite fc t) = DoRewrite fc $ goPTerm t goPWithProblem : PWithProblem' nm -> PWithProblem' nm @@ -552,7 +552,7 @@ mapPTerm f = goPTerm where goPClause : PClause' nm -> PClause' nm goPClause (MkPatClause fc lhs rhs wh) - = MkPatClause fc (goPTerm lhs) (goPTerm rhs) (goPDecl <$> wh) + = MkPatClause fc (goPTerm lhs) (goPTerm rhs) (map (mapFC goPDecl) wh) goPClause (MkWithClause fc lhs wps flags cls) = MkWithClause fc (goPTerm lhs) (goPWithProblem <$> wps) flags (goPClause <$> cls) goPClause (MkImpossible fc lhs) = MkImpossible fc $ goPTerm lhs @@ -567,33 +567,33 @@ mapPTerm f = goPTerm where goPBinderScope (MkPBinderScope binder scope) = MkPBinderScope (goPBinder binder) (goPTerm scope) - goPDecl : PDecl' nm -> PDecl' nm + goPDecl : PDeclNoFC' nm -> PDeclNoFC' nm goPDecl (PClaim claim) - = PClaim $ mapFC goPClaim claim - goPDecl (PDef cls) = PDef $ mapFC (map goPClause) cls - goPDecl (PData fc doc v mbt d) = PData fc doc v mbt $ goPDataDecl d - goPDecl (PParameters fc nts ps) - = PParameters fc (bimap (map goPlainBinder) (map goPBinder) nts) (goPDecl <$> ps) - goPDecl (PUsing fc mnts ps) - = PUsing fc (goPairedPTerms mnts) (goPDecl <$> ps) - goPDecl (PInterface fc v mnts n doc nrts ns mn ps) - = PInterface fc v (goPairedPTerms mnts) n doc (goBasicMultiBinder <$> nrts) ns mn (goPDecl <$> ps) - goPDecl (PImplementation fc v opts p is cs n ts mn ns mps) - = PImplementation fc v opts p (goImplicits is) (goPairedPTerms cs) - n (goPTerm <$> ts) mn ns (map (goPDecl <$>) mps) - goPDecl (PRecord fc doc v tot (MkPRecord n nts opts mn fs)) - = PRecord fc doc v tot + = PClaim $ goPClaim claim + goPDecl (PDef cls) = PDef $ (map goPClause) cls + goPDecl (PData doc v mbt d) = PData doc v mbt $ goPDataDecl d + goPDecl (PParameters nts ps) + = PParameters (bimap (map goPlainBinder) (map goPBinder) nts) (mapFC goPDecl <$> ps) + goPDecl (PUsing mnts ps) + = PUsing (goPairedPTerms mnts) (mapFC goPDecl <$> ps) + goPDecl (PInterface v mnts n doc nrts ns mn ps) + = PInterface v (goPairedPTerms mnts) n doc (goBasicMultiBinder <$> nrts) ns mn (mapFC goPDecl <$> ps) + goPDecl (PImplementation v opts p is cs n ts mn ns mps) + = PImplementation v opts p (goImplicits is) (goPairedPTerms cs) + n (goPTerm <$> ts) mn ns (map (mapFC goPDecl <$>) mps) + goPDecl (PRecord doc v tot (MkPRecord n nts opts mn fs)) + = PRecord doc v tot (MkPRecord n (map goPBinder nts) opts mn (map (mapFC goRecordField) fs)) - goPDecl (PRecord fc doc v tot (MkPRecordLater n nts)) - = PRecord fc doc v tot (MkPRecordLater n (goPBinder <$> nts )) - goPDecl (PFail fc msg ps) = PFail fc msg $ goPDecl <$> ps - goPDecl (PMutual ps) = PMutual $ mapFC (map goPDecl) ps + goPDecl (PRecord doc v tot (MkPRecordLater n nts)) + = PRecord doc v tot (MkPRecordLater n (goPBinder <$> nts )) + goPDecl (PFail msg ps) = PFail msg $ mapFC goPDecl <$> ps + goPDecl (PMutual ps) = PMutual $ map (mapFC goPDecl) ps goPDecl (PFixity p) = PFixity p - goPDecl (PNamespace fc strs ps) = PNamespace fc strs $ goPDecl <$> ps - goPDecl (PTransform fc n a b) = PTransform fc n (goPTerm a) (goPTerm b) - goPDecl (PRunElabDecl fc a) = PRunElabDecl fc $ goPTerm a + goPDecl (PNamespace strs ps) = PNamespace strs $ mapFC goPDecl <$> ps + goPDecl (PTransform n a b) = PTransform n (goPTerm a) (goPTerm b) + goPDecl (PRunElabDecl a) = PRunElabDecl $ goPTerm a goPDecl (PDirective d) = PDirective d - goPDecl p@(PBuiltin _ _ _) = p + goPDecl p@(PBuiltin _ _) = p goPBinder : PBinder' nm -> PBinder' nm goPBinder (MkPBinder info bind) = MkPBinder (goPiInfo info) (goBasicMultiBinder bind) diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr index 20ef8e9f11..5e34b41e24 100644 --- a/src/Parser/Rule/Source.idr +++ b/src/Parser/Rule/Source.idr @@ -263,6 +263,14 @@ pragma n = Pragma s => guard (s == n) _ => Nothing +export +cgDirective : Rule String +cgDirective = + terminal "Expected CG directive" $ + \case + CGDirective d => Just d + _ => Nothing + export builtinType : Rule BuiltinType builtinType =