Layout

cryptol.cabal

@@ -81,6 +81,8 @@ library
 
   Exposed-modules:     Cryptol.Parser,
                        Cryptol.Parser.Lexer,
+                       Cryptol.Parser.Token,
+                       Cryptol.Parser.Layout,
                        Cryptol.Parser.AST,
                        Cryptol.Parser.Position,
                        Cryptol.Parser.Names,

src/Cryptol/Parser.y

@@ -35,6 +35,7 @@ import           Control.Monad(liftM2,msum)
 import Cryptol.Parser.AST
 import Cryptol.Parser.Position
 import Cryptol.Parser.LexerUtils hiding (mkIdent)
+import Cryptol.Parser.Token
 import Cryptol.Parser.ParserUtils
 import Cryptol.Parser.Unlit(PreProc(..), guessPreProc)
 import Cryptol.Utils.Ident(paramInstModName)

src/Cryptol/Parser/Layout.hs

@@ -0,0 +1,237 @@
+{-# Language BlockArguments #-}
+{-# Language OverloadedStrings #-}
+module Cryptol.Parser.Layout where
+
+import Cryptol.Utils.Panic(panic)
+import Cryptol.Parser.Position
+import Cryptol.Parser.Token
+
+{-
+
+We assume the existence of an explicit EOF token at the end of the input.  This token is *less* indented
+than all other tokens (i.e., it is at column 0)
+
+Explicit Layout Blocks
+
+  * The symbols `(`, `{`, and `[` start an explicit layout block.
+  * While in an explicit layout block we pass through tokens, except:
+      - We may start new implicit or explicit layout blocks
+      - A `,` terminates any *nested* layout blocks
+      - We terminate the current layout block if we encounter the matching
+        closing symbol `)`, `}`, `]`
+
+Implicit Layout Blocks
+
+  * The keywords `where`, `private`, and `parameter` start an implicit
+    layout block.
+  * The layout block starts at the column of the *following* token and we
+    insert "virtual start block" between the current and the following tokens.
+  * While in an implicit layout block:
+    - We may start new implicit or explicit layout blocks
+    - We insert a "virtual separator" before tokens starting at the same
+      column as the layout block, EXCEPT:
+        * we do not insert a separator if the previous token was a
+          "documentation comment"
+        * we do not insert a separator before the first token in the block
+
+    - The implicit layout block is ended by:
+          * a token than is less indented that the block, or
+          * `)`, `}`, `]`, or 
+          * ',' but only if there is an outer paren block
+          block's column.
+    - When an implicit layout block ends, we insert a "virtual end block"
+      token just before the token that caused the block to end.
+
+Examples:
+
+f = x where x = 0x1         -- end implicit layout by layout
+g = 0x3                     -- (`g` is less indented than `x`)
+
+f (x where x = 2)           -- end implicit layout by `)`
+
+[ x where x = 2, 3 ]        -- end implicit layout by `,`
+
+module A where              -- two implicit layout blocks with the
+private                     -- *same* indentation (`where` and `private`)
+x = 0x2
+-}
+
+
+layout :: Bool -> [Located Token] -> [Located Token]
+layout isMod ts0
+
+  -- Star an implicit layout block at the top of the module
+  | let t         = head ts0
+        rng       = srcRange t
+        blockCol  = max 1 (col (from rng)) -- see startImplicitBlock
+  , isMod && tokenType (thing t) /= KW KW_module =
+    virt rng VCurlyL : go [ Virtual blockCol ] blockCol True ts0
+
+  | otherwise =
+    go [] 0 False ts0
+
+  where
+
+  {- State parameters for `go`:
+
+       stack:
+          The stack of implicit and explicit blocks
+
+       lastVirt:
+          The indentation of the outer most implicit block, or 0 if none.
+          This can be computed from the stack but we cache
+          it here as we need to check it on each token.
+
+       noVirtSep:
+          Do not emit a virtual separator even if token matches block alignment.
+          This is enabled at the beginning of a block, or after a doc string,
+          or if we just emitted a separtor, but have not yet consumed the
+          next token.
+
+       tokens:
+          remaining tokens to process
+  -}
+
+  go stack lastVirt noVirtSep tokens
+
+    -- End implicit layout due to indentation.  If the outermost block
+    -- is a lyout block we just end it.   If the outermost block is an
+    -- explicit layout block we report a lexical error.
+    | col curLoc < lastVirt =
+      endImplictBlock
+
+    -- End implicit layout block due to a symbol
+    | Just (Virtual {}) <- curBlock, endsLayout curTokTy =
+      endImplictBlock
+
+    -- End implicit layout block due to a comma
+    | Just (Virtual {}) <- curBlock
+    , Sym Comma <- curTokTy
+    , not (null [ () | Explicit _ <- popStack ]) =
+      endImplictBlock
+
+    -- Insert a virtual separator
+    | Just (Virtual {}) <- curBlock
+    , col curLoc == lastVirt && not noVirtSep =
+      virt curRange VSemi : go stack lastVirt True tokens
+
+    -- Start a new implicit layout. Advances token position.
+    | startsLayout curTokTy = startImplicitBlock
+
+    -- Start a paren block.  Advances token position
+    | Just close <- startsParenBlock curTokTy =
+      curTok : go (Explicit close : stack) lastVirt False advanceTokens
+
+    -- End a paren block. Advances token position
+    | Just (Explicit close) <- curBlock, close == curTokTy =
+      curTok : go popStack lastVirt False advanceTokens
+
+    -- Disable virtual separator after doc string. Advances token position
+    | White DocStr <- curTokTy =
+      curTok : go stack lastVirt True advanceTokens
+
+    -- Check to see if we are done.  Note that if we got here, implicit layout
+    -- blocks should have already been closed, as `EOF` is less indented than
+    -- all other tokens
+    | EOF <- curTokTy =
+      [curTok]
+
+    -- Any other token, just emit.  Advances token position
+    | otherwise =
+      curTok : go stack lastVirt False advanceTokens
+
+    where
+    curTok : advanceTokens = tokens
+    curTokTy               = tokenType (thing curTok)
+    curRange               = srcRange curTok
+    curLoc                 = from curRange
+
+    (curBlock,popStack) =
+      case stack of
+        a : b -> (Just a,b)
+        []    -> (Nothing, panic "layout" ["pop empty stack"])
+
+
+    startImplicitBlock =
+      let nextRng  = srcRange (head advanceTokens)
+          nextLoc  = from nextRng
+          blockCol = max 1 (col nextLoc)
+          -- the `max` ensuraes that indentation is always at least 1,
+          -- in case we are starting a block at the very end of the input
+
+      in curTok
+       : virt nextRng VCurlyL
+       : go (Virtual blockCol : stack) blockCol True advanceTokens
+
+
+    endImplictBlock =
+      case curBlock of
+        Just (Virtual {}) ->
+           virt curRange VCurlyR
+           : go popStack newVirt False tokens
+          where newVirt = case [ n | Virtual n <- popStack ] of
+                            n : _ -> n
+                            _     -> 0
+
+        Just (Explicit c) ->
+          errTok curRange (InvalidIndentation c) : advanceTokens
+
+        Nothing -> panic "layout" ["endImplictBlock with empty stack"]
+
+
+--------------------------------------------------------------------------------
+
+data Block =
+    Virtual Int     -- ^ Virtual layout block
+  | Explicit TokenT -- ^ An explicit layout block, expecting this ending token.
+    deriving (Show)
+
+-- | These tokens start an implicit layout block
+startsLayout :: TokenT -> Bool
+startsLayout ty =
+  case ty of
+    KW KW_where       -> True
+    KW KW_private     -> True
+    KW KW_parameter   -> True
+    _                 -> False
+
+-- | These tokens end an implicit layout block
+endsLayout :: TokenT -> Bool
+endsLayout ty =
+  case ty of
+    Sym BracketR -> True
+    Sym ParenR   -> True
+    Sym CurlyR   -> True
+    _            -> False
+
+-- | These tokens start an explicit "paren" layout block.
+-- If so, the result contains the corresponding closing paren.
+startsParenBlock :: TokenT -> Maybe TokenT
+startsParenBlock ty =
+  case ty of
+    Sym BracketL -> Just (Sym BracketR)
+    Sym ParenL   -> Just (Sym ParenR)
+    Sym CurlyL   -> Just (Sym CurlyR)
+    _            -> Nothing
+
+
+--------------------------------------------------------------------------------
+
+-- | Make a virtual token of the given type
+virt :: Range -> TokenV -> Located Token
+virt rng x = Located { srcRange = rng { to = from rng }, thing = t }
+  where
+  t = Token (Virt x)
+      case x of
+        VCurlyL -> "beginning of layout block"
+        VCurlyR -> "end of layout block"
+        VSemi   -> "layout block separator"
+
+errTok :: Range -> TokenErr -> Located Token
+errTok rng x = Located { srcRange = rng { to = from rng }, thing = t }
+  where
+  t = Token { tokenType = Err x, tokenText = "" }
+
+
+
+

src/Cryptol/Parser/Lexer.x

@@ -18,10 +18,13 @@ module Cryptol.Parser.Lexer
   , Located(..)
   , Config(..)
   , defaultConfig
+  , dbgLex
   ) where
 
 import Cryptol.Parser.Position
+import Cryptol.Parser.Token
 import Cryptol.Parser.LexerUtils
+import qualified Cryptol.Parser.Layout as L
 import Cryptol.Parser.Unlit(unLit)
 import Data.Text (Text)
 import qualified Data.Text as Text
@@ -195,7 +198,7 @@ stateToInt (InChar {})    = char
 -- This stream is fed to the parser.
 lexer :: Config -> Text -> ([Located Token], Position)
 lexer cfg cs = ( case cfgLayout cfg of
-                   Layout   -> layout cfg lexemes
+                   Layout   -> L.layout (cfgModuleScope cfg) lexemes
                    NoLayout -> lexemes
                , finalPos
                )
@@ -253,5 +256,10 @@ primLexer cfg cs = run inp Normal
             (rest,pos)  = run i' $! s'
         in (mtok ++ rest, pos)
 
+dbgLex file =
+  do txt <- readFile file
+     let (ts,_) = lexer defaultConfig (Text.pack txt)
+     mapM_ (print . thing) ts
+
 -- vim: ft=haskell
 }