Documentation

Lean.Elab.Do

Equations
Instances For
    Instances For
      @[inline, reducible]
      Equations
      Instances For
        structure Lean.Elab.Term.Do.Alt (σ : Type) :

        A doMatch alternative. vars is the array of variables declared by patterns.

        Instances For
          Equations
          • Lean.Elab.Term.Do.instInhabitedAlt = { default := { ref := default, vars := default, patterns := default, rhs := default } }

          Auxiliary datastructure for representing a do code block, and compiling "reassignments" (e.g., x := x + 1). We convert Code into a Syntax term representing the:

          • do-block, or
          • the visitor argument for the forIn combinator.

          We say the following constructors are terminals:

          • break: for interrupting a for x in s
          • continue: for interrupting the current iteration of a for x in s
          • return e: for returning e as the result for the whole do computation block
          • action a: for executing action a as a terminal
          • ite: if-then-else
          • match: pattern matching
          • jmp a goto to a join-point

          We say the terminals break, continue, action, and return are "exit points"

          Note that, return e is not equivalent to action (pure e). Here is an example:

          def f (x : Nat) : IO Unit := do
          if x == 0 then
             return ()
          IO.println "hello"
          

          Executing #eval f 0 will not print "hello". Now, consider

          def g (x : Nat) : IO Unit := do
          if x == 0 then
             pure ()
          IO.println "hello"
          

          The if statement is essentially a noop, and "hello" is printed when we execute g 0.

          • decl represents all declaration-like doElems (e.g., let, have, let rec). The field stx is the actual doElem, vars is the array of variables declared by it, and cont is the next instruction in the do code block. vars is an array since we have declarations such as let (a, b) := s.

          • reassign is an reassignment-like doElem (e.g., x := x + 1).

          • joinpoint is a join point declaration: an auxiliary let-declaration used to represent the control-flow.

          • seq a k executes action a, ignores its result, and then executes k. We also store the do-elements dbg_trace and assert! as actions in a seq.

          A code block C is well-formed if

          • For every jmp ref j as in C, there is a joinpoint j ps b k and jmp ref j as is in k, and ps.size == as.size
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              A code block, and the collection of variables updated by it.

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

                  Return true if the give code contains an exit point that satisfies p

                  Equations
                  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
                            • 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

                                Create a new jointpoint for c, and jump to it with the variables rs

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

                                  Create a new joinpoint that takes rs and val as arguments. val must be syntax representing a pure value. The body of the joinpoint is created using mkJPBody yFresh, where yFresh is a fresh variable created by this method.

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

                                    Auxiliary operation for adding new variables to the collection of updated variables in a CodeBlock. When a new variable is not already in the collection, but is shadowed by some declaration in c, we create auxiliary join points to make sure we preserve the semantics of the code block. Example: suppose we have the code block print x; let x := 10; return x. And we want to extend it with the reassignment x := x + 1. We first use pullExitPoints to create

                                    let jp (x!1) :=  return x!1;
                                    print x;
                                    let x := 10;
                                    jmp jp x
                                    

                                    and then we add the reassignment

                                    x := x + 1
                                    let jp (x!1) := return x!1;
                                    print x;
                                    let x := 10;
                                    jmp jp x
                                    

                                    Note that we created a fresh variable x!1 to avoid accidental name capture. As another example, consider

                                    print x;
                                    let x := 10
                                    y := y + 1;
                                    return x;
                                    

                                    We transform it into

                                    let jp (y x!1) := return x!1;
                                    print x;
                                    let x := 10
                                    y := y + 1;
                                    jmp jp y x
                                    

                                    and then we add the reassignment as in the previous example. We need to include y in the jump, because each exit point is implicitly returning the set of update variables.

                                    We implement the method as follows. Let us be c.uvars, then 1- for each return _ y in c, we create a join point let j (us y!1) := return y!1 and replace the return _ y with jmp us y 2- for each break, we create a join point let j (us) := break and replace the break with jmp us. 3- Same as 2 for continue.

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

                                      Extend the set of updated variables. It assumes ws is a super set of c.uvars. We cannot simply update the field c.uvars, because c may have shadowed some variable in ws. See discussion at pullExitPoints.

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

                                        Given two code blocks c₁ and c₂, make sure they have the same set of updated variables. Let ws the union of the updated variables in c₁‵ and ‵c₂. We use extendUpdatedVars c₁ ws and extendUpdatedVars c₂ ws

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

                                          Extending code blocks with variable declarations: let x : t := v and let x : t ← v. We remove x from the collection of updated variables. Remark: stx is the syntax for the declaration (e.g., letDecl), and xs are the variables declared by it. It is an array because we have let-declarations that declare multiple variables. Example: let (x, y) := t

                                          Equations
                                          Instances For

                                            Extending code blocks with reassignments: x : t := v and x : t ← v. Remark: stx is the syntax for the declaration (e.g., letDecl), and xs are the variables declared by it. It is an array because we have let-declarations that declare multiple variables. Example: (x, y) ← t

                                            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
                                                  • 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

                                                      Return a code block that executes terminal and then k with the value produced by terminal. This method assumes terminal is a terminal

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Equations
                                                        Instances For
                                                          Equations
                                                          Instances For
                                                            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
                                                                  • 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
                                                                          Instances For

                                                                            Return some action if doElem is a doExpr <action>

                                                                            Equations
                                                                            Instances For

                                                                              The procedure ToTerm.run converts a CodeBlock into a Syntax term. We use this method to convert 1- The CodeBlock for a root do ... term into a Syntax term. This kind of CodeBlock never contains break nor continue. Moreover, the collection of updated variables is not packed into the result. Thus, we have two kinds of exit points - Code.action e which is converted into e - Code.return _ e which is converted into pure e

                                                                              We use Kind.regular for this case.

                                                                              2- The CodeBlock for b at for x in xs do b. In this case, we need to generate a Syntax term representing a function for the xs.forIn combinator.

                                                                              a) If b contain a Code.return _ a exit point. The generated Syntax term has type m (ForInStep (Option α × σ)), where a : α, and the σ is the type of the tuple of variables reassigned by b. We use Kind.forInWithReturn for this case

                                                                              b) If b does not contain a Code.return _ a exit point. Then, the generated Syntax term has type m (ForInStep σ). We use Kind.forIn for this case.

                                                                              3- The CodeBlock c for a do sequence nested in a monadic combinator (e.g., MonadExcept.tryCatch).

                                                                              The generated Syntax term for c must inform whether c "exited" using Code.action, Code.return, Code.break or Code.continue. We use the auxiliary types DoResults for storing this information. For example, the auxiliary type DoResultPBC α σ is used for a code block that exits with Code.action, and Code.break/Code.continue, α is the type of values produced by the exit action, and σ is the type of the tuple of reassigned variables. The type DoResult α β σ is usedf for code blocks that exit with Code.action, Code.return, and Code.break/Code.continue, β is the type of the returned values. We don't use DoResult α β σ for all cases because:

                                                                                a) The elaborator would not be able to infer all type parameters without extra annotations. For example,
                                                                                   if the code block does not contain `Code.return _ _`, the elaborator will not be able to infer `β`.
                                                                              
                                                                                b) We need to pattern match on the result produced by the combinator (e.g., `MonadExcept.tryCatch`),
                                                                                   but we don't want to consider "unreachable" cases.
                                                                              

                                                                              We do not distinguish between cases that contain break, but not continue, and vice versa.

                                                                              When listing all cases, we use a to indicate the code block contains Code.action _, r for Code.return _ _, and b/c for a code block that contains Code.break _ or Code.continue _.

                                                                              Here is the recipe for adding new combinators with nested dos. Example: suppose we want to support repeat doSeq. Assuming we have repeat : m α → m α 1- Convert doSeq into codeBlock : CodeBlock 2- Create term term using mkNestedTerm code m uvars a r bc where code is codeBlock.code, uvars is an array containing codeBlock.uvars, m is a Syntax representing the Monad, and a is true if code contains Code.action _, r is true if code contains Code.return _ _, bc is true if code contains Code.break _ or Code.continue _.

                                                                              Remark: for combinators such as repeat that take a single doSeq, all arguments, but m, are extracted from codeBlock. 3- Create the term repeat $term 4- and then, convert it into a doSeq using matchNestedTermResult ref (repeat $term) uvsar a r bc

                                                                              Helper method for annotating term with the raw syntax ref. We use this method to implement finer-grained term infos for do-blocks.

                                                                              We use withRef term to make sure the synthetic position for the with_annotate_term is equal to the one for term. This is important for producing error messages when there is a type mismatch. Consider the following example:

                                                                              opaque f : IO Nat
                                                                              
                                                                              def g : IO String := do
                                                                                f
                                                                              

                                                                              There is at type mismatch at f, but it is detected when elaborating the expanded term containing the with_annotate_term .. f. The current getRef when this annotate is invoked is not necessarily f. Actually, it is the whole do-block. By using withRef we ensure the synthetic position for the with_annotate_term .. is equal to term. Recall that synthetic positions are used when generating error messages.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                Equations
                                                                                Instances For
                                                                                  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
                                                                                            • 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
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      Equations
                                                                                                      Instances For

                                                                                                        Given

                                                                                                        generate Kind. See comment at the beginning of the ToTerm namespace.

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

                                                                                                          Given a term term produced by ToTerm.run, pattern match on its result. See comment at the beginning of the ToTerm namespace.

                                                                                                          The result is a sequence of doElem

                                                                                                          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
                                                                                                                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
                                                                                                                        • 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

                                                                                                                              Generate CodeBlock for doReturn which is of the form

                                                                                                                              "return " >> optional termParser
                                                                                                                              

                                                                                                                              doElems is only used for sanity checking.

                                                                                                                              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

                                                                                                                                    Generate CodeBlock for doLetArrow; doElems doLetArrow is of the form

                                                                                                                                    "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
                                                                                                                                    

                                                                                                                                    where

                                                                                                                                    def doIdDecl   := leading_parser ident >> optType >> leftArrow >> doElemParser
                                                                                                                                    def doPatDecl  := leading_parser termParser >> leftArrow >> doElemParser >> optional (" | " >> doSeq)
                                                                                                                                    

                                                                                                                                    Generate CodeBlock for doReassignArrow; doElems doReassignArrow is of the form

                                                                                                                                    (doIdDecl <|> doPatDecl)
                                                                                                                                    

                                                                                                                                    Generate CodeBlock for doIf; doElems doIf is of the form

                                                                                                                                    "if " >> optIdent >> termParser >> " then " >> doSeq
                                                                                                                                     >> many (group (try (group (" else " >> " if ")) >> optIdent >> termParser >> " then " >> doSeq))
                                                                                                                                     >> optional (" else " >> doSeq)
                                                                                                                                    

                                                                                                                                    Generate CodeBlock for doUnless; doElems doUnless is of the form

                                                                                                                                    "unless " >> termParser >> "do " >> doSeq
                                                                                                                                    

                                                                                                                                    Generate CodeBlock for doFor; doElems doFor is of the form

                                                                                                                                    def doForDecl := leading_parser termParser >> " in " >> withForbidden "do" termParser
                                                                                                                                    def doFor := leading_parser "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
                                                                                                                                    

                                                                                                                                    Generate CodeBlock for doTry; doElems

                                                                                                                                    def doTry := leading_parser "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
                                                                                                                                    def doCatch      := leading_parser "catch " >> binderIdent >> optional (":" >> termParser) >> darrow >> doSeq
                                                                                                                                    def doCatchMatch := leading_parser "catch " >> doMatchAlts
                                                                                                                                    def doFinally    := leading_parser "finally " >> doSeq
                                                                                                                                    
                                                                                                                                    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