Documentation

Lean.Compiler.LCNF.Simp.DiscrM

source
inductive Lean.Compiler.LCNF.Simp.CtorInfo :
Type
Instances For
    source
    def Lean.Compiler.LCNF.Simp.CtorInfo.getName :
    CtorInfo → Name
    Equations
    Instances For
      source
      def Lean.Compiler.LCNF.Simp.CtorInfo.getNumParams :
      CtorInfo → Nat
      Equations
      Instances For
        source
        def Lean.Compiler.LCNF.Simp.CtorInfo.getNumFields :
        CtorInfo → Nat
        Equations
        Instances For
          source
          structure Lean.Compiler.LCNF.Simp.DiscrM.Context :
          Type
          • discrCtorMap : FVarIdMap CtorInfo

            A mapping from discriminant to constructor application it is equal to in the current context.

          • ctorDiscrMap : PersistentExprMap FVarId

            A mapping from constructor application to discriminant it is equal to in the current context.

          Instances For
            source
            @[reducible, inline]
            abbrev Lean.Compiler.LCNF.Simp.DiscrM (α : Type) :
            Type

            Helper monad for tracking mappings from discriminant to constructor applications and back. The combinator withDiscrCtor should be used when visiting cases alternatives.

            Equations
            Instances For
              source
              def Lean.Compiler.LCNF.Simp.findCtor? (fvarId : FVarId) :
              DiscrM (Option CtorInfo)

              If fvarId is a constructor application, returns constructor information. Remark: we use the map discrCtorMap. Remark: We use this method when simplifying projections and cases-constructor.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Lean.Compiler.LCNF.Simp.findCtorName? (fvarId : FVarId) :
                DiscrM (Option Name)
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Lean.Compiler.LCNF.Simp.getIndInfo? (type : Expr) (ind : Name) :
                  CoreM (Option (List Level × Array Arg))

                  If type is an application of the inductive type ind, return its universe levels and parameters.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[inline]
                    def Lean.Compiler.LCNF.Simp.withDiscrCtorImp {α : Type} (discr : FVarId) (ctorName : Name) (ctorFields : Array Param) (x : DiscrM α) :
                    DiscrM α

                    Execute x with the information that discr = ctorName ctorFields. We use this information to simplify nested cases on the same discriminant.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[inline]
                      def Lean.Compiler.LCNF.Simp.withDiscrCtor {m : Type → Type u_1} {α : Type} [MonadFunctorT DiscrM m] (discr : FVarId) (ctorName : Name) (ctorFields : Array Param) :
                      m α → m α

                      Execute x with the information that discr = ctorName ctorFields. We use this information to simplify nested cases on the same discriminant.

                      Equations
                      Instances For
                        source
                        def Lean.Compiler.LCNF.Simp.simpCtorDiscrCore? (e : Expr) :
                        DiscrM (Option FVarId)
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For