Documentation

Lean.Compiler.LCNF.Internalize

source
@[inline, reducible]
abbrev Lean.Compiler.LCNF.Internalize.InternalizeM (α : Type) :
Type
Instances For
    source
    instance Lean.Compiler.LCNF.Internalize.instMonadFVarSubstInternalizeMTrue :
    Lean.Compiler.LCNF.MonadFVarSubst Lean.Compiler.LCNF.Internalize.InternalizeM true

    The InternalizeM monad is a translator. It "translates" the free variables in the input expressions and Code, into new fresh free variables in the local context.

    source
    instance Lean.Compiler.LCNF.Internalize.instMonadFVarSubstStateInternalizeM :
    Lean.Compiler.LCNF.MonadFVarSubstState Lean.Compiler.LCNF.Internalize.InternalizeM
    source
    def Lean.Compiler.LCNF.Internalize.internalizeParam (p : Lean.Compiler.LCNF.Param) :
    Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.Param
    Instances For
      source
      def Lean.Compiler.LCNF.Internalize.internalizeLetDecl (decl : Lean.Compiler.LCNF.LetDecl) :
      Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.LetDecl
      Instances For
        source
        partial def Lean.Compiler.LCNF.Internalize.internalizeFunDecl (decl : Lean.Compiler.LCNF.FunDecl) :
        Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.FunDecl
        source
        partial def Lean.Compiler.LCNF.Internalize.internalizeCode (code : Lean.Compiler.LCNF.Code) :
        Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.Code
        source
        def Lean.Compiler.LCNF.Internalize.internalizeCodeDecl (decl : Lean.Compiler.LCNF.CodeDecl) :
        Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.CodeDecl
        Instances For
          source
          def Lean.Compiler.LCNF.Code.internalize (code : Lean.Compiler.LCNF.Code) (s : optParam Lean.Compiler.LCNF.FVarSubst ∅) :
          Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code

          Refresh free variables ids in code, and store their declarations in the local context.

          Instances For
            source
            def Lean.Compiler.LCNF.Decl.internalize (decl : Lean.Compiler.LCNF.Decl) (s : optParam Lean.Compiler.LCNF.FVarSubst ∅) :
            Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl
            Instances For
              source
              def Lean.Compiler.LCNF.Decl.internalize.go (decl : Lean.Compiler.LCNF.Decl) :
              Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.Decl
              Instances For
                source
                def Lean.Compiler.LCNF.cleanup (decl : Array Lean.Compiler.LCNF.Decl) :
                Lean.Compiler.LCNF.CompilerM (Array Lean.Compiler.LCNF.Decl)

                Create a fresh local context and internalize the given decls.

                Instances For
                  source
                  def Lean.Compiler.LCNF.normalizeFVarIds (decl : Lean.Compiler.LCNF.Decl) :
                  Lean.CoreM Lean.Compiler.LCNF.Decl
                  Instances For