Documentation

Lean.Elab.Do.InferControlInfo

source
structure Lean.Elab.Do.ControlInfo :
Type

Represents information about what control effects a do block has.

The fields split by flavor:

  • breaks, continues, returnsEarly, and reassigns are syntactic: true/non-empty iff the corresponding construct appears anywhere in the source text of the block, independent of whether it is semantically reachable. Downstream elaborators must assume every such syntactic effect may occur, because the elaborator visits every doElem (only top-level return/break/continue short-circuit via elabAsSyntacticallyDeadCode).
  • numRegularExits is also syntactic: the number of times the block wires the enclosing continuation into its elaborated expression. withDuplicableCont reads it as a join-point duplication trigger (> 1).
  • noFallthrough = true asserts that the next doElem in the enclosing sequence is semantically irrelevant (control never falls through to it). noFallthrough = false makes no such assertion. The dead-code warning fires on the next element when this is true.

Invariant: numRegularExits = 0 → noFallthrough. The converse does not hold.

  • breaks : Bool

    The do block syntactically contains a break.

  • continues : Bool

    The do block syntactically contains a continue.

  • returnsEarly : Bool

    The do block syntactically contains an early return.

  • numRegularExits : Nat

    The number of times the block wires the enclosing continuation into its elaborated expression. Consumed by withDuplicableCont to decide whether to introduce a join point (> 1).

  • noFallthrough : Bool

    When true, asserts that the next doElem in the enclosing sequence is semantically irrelevant (control never falls through to it). false asserts nothing.

  • reassigns : NameSet

    The variables that are syntactically reassigned somewhere in the do block.

Instances For
    source
    @[implicit_reducible]
    instance Lean.Elab.Do.instInhabitedControlInfo :
    Inhabited ControlInfo
    Equations
    source
    def Lean.Elab.Do.ControlInfo.pure :
    ControlInfo
    Equations
    Instances For
      source
      def Lean.Elab.Do.ControlInfo.empty :
      ControlInfo

      The identity of ControlInfo.alternative: a ControlInfo describing a block with no branches at all (so no regular exits and the next element is trivially unreachable).

      Equations
      Instances For
        source
        def Lean.Elab.Do.ControlInfo.sequence (a b : ControlInfo) :
        ControlInfo
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Elab.Do.ControlInfo.alternative (a b : ControlInfo) :
          ControlInfo
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[implicit_reducible]
            instance Lean.Elab.Do.instToMessageDataControlInfo :
            ToMessageData ControlInfo
            Equations
            • One or more equations did not get rendered due to their size.
            source
            @[reducible, inline]
            abbrev Lean.Elab.Do.ControlInfoHandler :
            Type

            A handler for inferring ControlInfo from a doElem syntax. Register with @[doElem_control_info parserName].

            Equations
            Instances For
              source
              unsafe def Lean.Elab.Do.mkControlInfoElemAttributeUnsafe (ref : Name) :
              IO (KeyedDeclsAttribute ControlInfoHandler)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[implemented_by Lean.Elab.Do.mkControlInfoElemAttributeUnsafe]
                opaque Lean.Elab.Do.mkControlInfoElemAttribute (ref : Name) :
                IO (KeyedDeclsAttribute ControlInfoHandler)
                source
                opaque Lean.Elab.Do.controlInfoElemAttribute :
                KeyedDeclsAttribute ControlInfoHandler

                Registers a ControlInfo inference handler for the given doElem syntax node kind.

                A handler should have type ControlInfoHandler (i.e. TSyntax \doElem → TermElabM ControlInfo). For pure handlers, use fun stx => return ControlInfo.pure`.

                source
                partial def Lean.Elab.Do.InferControlInfo.ofElem (stx : TSyntax `doElem) :
                TermElabM ControlInfo
                source
                partial def Lean.Elab.Do.InferControlInfo.ofLetOrReassignArrow (reassignment : Bool) (decl : TSyntax [`Lean.Parser.Term.doIdDecl, `Lean.Parser.Term.doPatDecl]) :
                TermElabM ControlInfo
                source
                partial def Lean.Elab.Do.InferControlInfo.ofLetOrReassign (reassigned : Array Ident) (rhs? : Option (TSyntax `doElem)) (otherwise? body? : Option (TSyntax `Lean.Parser.Term.doSeqIndent)) :
                TermElabM ControlInfo
                source
                partial def Lean.Elab.Do.InferControlInfo.ofSeq (stx : TSyntax `Lean.Parser.Term.doSeq) :
                TermElabM ControlInfo
                source
                partial def Lean.Elab.Do.InferControlInfo.ofOptionSeq (stx? : Option (TSyntax `Lean.Parser.Term.doSeq)) :
                TermElabM ControlInfo
                source
                def Lean.Elab.Do.inferControlInfoSeq (doSeq : TSyntax `Lean.Parser.Term.doSeq) :
                TermElabM ControlInfo
                Equations
                Instances For
                  source
                  def Lean.Elab.Do.inferControlInfoElem (doElem : TSyntax `doElem) :
                  TermElabM ControlInfo
                  Equations
                  Instances For