Documentation

Lean.Parser.Types

@[reducible, inline]
Equations
Instances For
    @[reducible, inline]
    Equations
    Instances For
      def Lean.Parser.getNext (input : String) (pos : String.Pos) :

      Return character after position pos

      Equations
      Instances For

        Maximal (and function application) precedence. In the standard lean language, no parser has precedence higher than maxPrec.

        Note that nothing prevents users from using a higher precedence, but we strongly discourage them from doing it.

        Equations
        Instances For
          Equations
          Instances For
            Equations
            Instances For
              Equations
              Instances For
                @[reducible, inline]
                Equations
                Instances For

                  Input string and related data. Recall that the FileMap is a helper structure for mapping String.Pos in the input string to line/column information.

                  Instances For
                    Equations

                    Input context derived from elaboration of previous commands.

                    Instances For

                      Parser context parts that can be updated without invalidating the parser cache.

                      Instances For

                        Parser context updateable in adaptUncacheableContextFn.

                        Instances For

                          Opaque parser context updateable using adaptCacheableContextFn and adaptUncacheableContextFn.

                            Instances For
                              Instances For
                                Equations
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Instances For
                                      Instances For
                                        Instances For
                                          Equations
                                          Instances For

                                            A syntax array with an inaccessible prefix, used for sound caching.

                                            Instances For
                                              Equations
                                              • stack.toSubarray = stack.raw.toSubarray stack.drop
                                              Instances For
                                                Equations
                                                • stack.size = stack.raw.size - stack.drop
                                                Instances For
                                                  Equations
                                                  • stack.isEmpty = (stack.size == 0)
                                                  Instances For
                                                    Equations
                                                    • stack.shrink n = { raw := stack.raw.shrink (stack.drop + n), drop := stack.drop }
                                                    Instances For
                                                      Equations
                                                      • stack.push a = { raw := stack.raw.push a, drop := stack.drop }
                                                      Instances For
                                                        Equations
                                                        • stack.pop = if stack.size > 0 then { raw := stack.raw.pop, drop := stack.drop } else stack
                                                        Instances For
                                                          Equations
                                                          • stack.back = if stack.size > 0 then stack.raw.back else panicWithPosWithDecl "Lean.Parser.Types" "Lean.Parser.SyntaxStack.back" 175 4 "SyntaxStack.back: element is inaccessible"
                                                          Instances For
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              Equations
                                                              • stack.extract start stop = stack.raw.extract (stack.drop + start) (stack.drop + stop)
                                                              Instances For
                                                                Instances For
                                                                  @[inline]
                                                                  Equations
                                                                  • s.hasError = (s.errorMsg != none)
                                                                  Instances For
                                                                    Equations
                                                                    • s.stackSize = s.stxStack.size
                                                                    Instances For
                                                                      Equations
                                                                      • s.restore iniStackSz iniPos = { stxStack := s.stxStack.shrink iniStackSz, lhsPrec := s.lhsPrec, pos := iniPos, cache := s.cache, errorMsg := none, recoveredErrors := s.recoveredErrors }
                                                                      Instances For
                                                                        Equations
                                                                        • s.setPos pos = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := pos, cache := s.cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }
                                                                        Instances For
                                                                          Equations
                                                                          • s.setCache cache = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := s.pos, cache := cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }
                                                                          Instances For
                                                                            Equations
                                                                            • s.pushSyntax n = { stxStack := s.stxStack.push n, lhsPrec := s.lhsPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }
                                                                            Instances For
                                                                              Equations
                                                                              • s.popSyntax = { stxStack := s.stxStack.pop, lhsPrec := s.lhsPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }
                                                                              Instances For
                                                                                Equations
                                                                                • s.shrinkStack iniStackSz = { stxStack := s.stxStack.shrink iniStackSz, lhsPrec := s.lhsPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }
                                                                                Instances For
                                                                                  Equations
                                                                                  • s.next input pos = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := input.next pos, cache := s.cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }
                                                                                  Instances For
                                                                                    Equations
                                                                                    • s.next' input pos h = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := input.next' pos h, cache := s.cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }
                                                                                    Instances For
                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          Equations
                                                                                          Instances For
                                                                                            @[inline]
                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              Equations
                                                                                              Instances For
                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  Equations
                                                                                                  • s.mkEOIError expected = s.mkUnexpectedError "unexpected end of input" expected
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      Equations
                                                                                                      • s.mkErrorAt msg pos initStackSz? = s.mkErrorsAt [msg] pos initStackSz?
                                                                                                      Instances For

                                                                                                        Reports given 'expected' messages at range of top stack element (assumed to be a single token). Replaces the element with missing and resets position to the token position. iniPos can be specified to avoid this position lookup but still must be identical to the token position.

                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For

                                                                                                          Reports given 'expected' message at range of top stack element (assumed to be a single token). Replaces the element with missing and resets position to the token position. iniPos can be specified to avoid this position lookup but still must be identical to the token position.

                                                                                                          Equations
                                                                                                          • s.mkUnexpectedTokenError msg iniPos = s.mkUnexpectedTokenErrors [msg] iniPos
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                            • s.mkUnexpectedErrorAt msg pos = (s.setPos pos).mkUnexpectedError msg
                                                                                                            Instances For
                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For
                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  Instances For
                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    Instances For
                                                                                                                      Equations
                                                                                                                      Equations
                                                                                                                      @[reducible, inline]
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[inline]

                                                                                                                        Create a simple parser combinator that inherits the info of the nested parser.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          Equations
                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                          Instances For

                                                                                                                            Run p with a fresh cache, restore outer cache afterwards. p may access the entire syntax stack.

                                                                                                                            Equations
                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                            Instances For

                                                                                                                              Run p with a fresh cache, restore outer cache afterwards. p may access the entire syntax stack.

                                                                                                                              Equations
                                                                                                                              Instances For

                                                                                                                                Run p under the given context transformation with a fresh cache (see also withResetCacheFn).

                                                                                                                                Equations
                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                Instances For

                                                                                                                                  Run p and record result in parser cache for any further invocation with this parserName, parser context, and parser state. p cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history. As this excludes trailing parsers from being cached, we also reset lhsPrec, which is not read but set by leading parsers, to 0 in order to increase cache hits. Finally, errorMsg is also reset to none as a leading parser should not be called in the first place if there was an error.

                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For

                                                                                                                                    Run p and record result in parser cache for any further invocation with this parserName, parser context, and parser state. p cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history. As this excludes trailing parsers from being cached, we also reset lhsPrec, which is not read but set by leading parsers, to 0 in order to increase cache hits. Finally, errorMsg is also reset to none as a leading parser should not be called in the first place if there was an error.

                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      Equations
                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                      Instances For