← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Syntax/Parser/Layout.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, d5cf60f
  • Date: 2015-05-20 13:08:33 UTC
  • mfrom: (1.1.7)
  • Revision ID: package-import@ubuntu.com-20150520130833-cdcmhagwsouna237
Tags: 2.4.2.2-2
[d5cf60f] Depend on ${shlibs:Depends}, to get libc (& maybe other) deps

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Syntax/Parser/Layout.hs
39
39
--   context.
40
40
openBrace :: LexAction Token
41
41
openBrace = token $ \_ ->
42
 
    do  pushContext NoLayout
43
 
        i <- getParseInterval
44
 
        return (TokSymbol SymOpenBrace i)
 
42
    do  pushContext NoLayout
 
43
        i <- getParseInterval
 
44
        return (TokSymbol SymOpenBrace i)
45
45
 
46
46
 
47
47
{-| Executed upon lexing a close brace (@\'}\'@). Exits the current layout
51
51
-}
52
52
closeBrace :: LexAction Token
53
53
closeBrace = token $ \_ ->
54
 
    do  popContext
55
 
        i <- getParseInterval
56
 
        return (TokSymbol SymCloseBrace i)
 
54
    do  popContext
 
55
        i <- getParseInterval
 
56
        return (TokSymbol SymCloseBrace i)
57
57
 
58
58
 
59
59
{-| Executed for the first token in each line (see 'Agda.Syntax.Parser.Lexer.bol').
61
61
    If the token is
62
62
 
63
63
    - /to the left/ :
64
 
        Exit the current context and a return virtual close brace (stay in the
65
 
        'Agda.Syntax.Parser.Lexer.bol' state).
 
64
        Exit the current context and a return virtual close brace (stay in the
 
65
        'Agda.Syntax.Parser.Lexer.bol' state).
66
66
 
67
67
    - /same column/ :
68
 
        Exit the 'Agda.Syntax.Parser.Lexer.bol' state and return a virtual semi
69
 
        colon.
 
68
        Exit the 'Agda.Syntax.Parser.Lexer.bol' state and return a virtual semi
 
69
        colon.
70
70
 
71
71
    - /to the right/ :
72
 
        Exit the 'Agda.Syntax.Parser.Lexer.bol' state and continue lexing.
 
72
        Exit the 'Agda.Syntax.Parser.Lexer.bol' state and continue lexing.
73
73
 
74
74
    If the current block doesn't use layout (i.e. it was started by
75
75
    'openBrace') all positions are considered to be /to the right/.
76
76
-}
77
77
offsideRule :: LexAction Token
78
78
offsideRule inp _ _ =
79
 
    do  offs <- getOffside p
80
 
        case offs of
81
 
            LT  -> do   popContext
82
 
                        return (TokSymbol SymCloseVirtualBrace (Interval p p))
83
 
            EQ  -> do   popLexState
84
 
                        return (TokSymbol SymVirtualSemi (Interval p p))
85
 
            GT  -> do   popLexState
86
 
                        lexToken
 
79
    do  offs <- getOffside p
 
80
        case offs of
 
81
            LT  -> do   popContext
 
82
                        return (TokSymbol SymCloseVirtualBrace (Interval p p))
 
83
            EQ  -> do   popLexState
 
84
                        return (TokSymbol SymVirtualSemi (Interval p p))
 
85
            GT  -> do   popLexState
 
86
                        lexToken
87
87
    where
88
 
        p = lexPos inp
 
88
        p = lexPos inp
89
89
 
90
90
 
91
91
{-| This action is only executed from the 'Agda.Syntax.Parser.Lexer.empty_layout'
95
95
-}
96
96
emptyLayout :: LexAction Token
97
97
emptyLayout inp _ _ =
98
 
    do  popLexState
99
 
        pushLexState bol
100
 
        return (TokSymbol SymCloseVirtualBrace (Interval p p))
 
98
    do  popLexState
 
99
        pushLexState bol
 
100
        return (TokSymbol SymCloseVirtualBrace (Interval p p))
101
101
    where
102
 
        p = lexPos inp
 
102
        p = lexPos inp
103
103
 
104
104
 
105
105
{-| Start a new layout context. This is one of two ways to get out of the
125
125
-}
126
126
newLayoutContext :: LexAction Token
127
127
newLayoutContext inp _ _ =
128
 
    do  let offset = posCol p
129
 
        ctx <- topContext
130
 
        case ctx of
131
 
            Layout prevOffs | prevOffs >= offset ->
132
 
                do  pushLexState empty_layout
133
 
                    return (TokSymbol SymOpenVirtualBrace (Interval p p))
134
 
            _ ->
135
 
                do  pushContext (Layout offset)
136
 
                    return (TokSymbol SymOpenVirtualBrace (Interval p p))
 
128
    do  let offset = posCol p
 
129
        ctx <- topContext
 
130
        case ctx of
 
131
            Layout prevOffs | prevOffs >= offset ->
 
132
                do  pushLexState empty_layout
 
133
                    return (TokSymbol SymOpenVirtualBrace (Interval p p))
 
134
            _ ->
 
135
                do  pushContext (Layout offset)
 
136
                    return (TokSymbol SymOpenVirtualBrace (Interval p p))
137
137
    where
138
 
        p = lexPos inp
 
138
        p = lexPos inp
139
139
 
140
140
 
141
141
-- | Compute the relative position of a location to the
142
142
--   current layout context.
143
143
getOffside :: Position -> Parser Ordering
144
144
getOffside loc =
145
 
    do  ctx <- topContext
146
 
        return $ case ctx of
147
 
            Layout n    -> compare (posCol loc) n
148
 
            _           -> GT
 
145
    do  ctx <- topContext
 
146
        return $ case ctx of
 
147
            Layout n    -> compare (posCol loc) n
 
148
            _           -> GT