Documentation

Lean.Compiler.LCNF.Internalize

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.Internalize.InternalizeM (pu : Purity) (α : Type) :
Type
Instances For
    source
    @[implicit_reducible]
    instance Lean.Compiler.LCNF.Internalize.instMonadFVarSubstInternalizeMTrue {pu : Purity} :
    MonadFVarSubst (InternalizeM pu) pu 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
    @[implicit_reducible]
    instance Lean.Compiler.LCNF.Internalize.instMonadFVarSubstStateInternalizeM {pu : Purity} :
    MonadFVarSubstState (InternalizeM pu) pu
    source
    def Lean.Compiler.LCNF.Internalize.internalizeParam {pu : Purity} (p : Param pu) :
    InternalizeM pu (Param pu)
    Instances For
      source
      def Lean.Compiler.LCNF.Internalize.internalizeArg {pu : Purity} (arg : Arg pu) :
      InternalizeM pu (Arg pu)
      Instances For
        source
        def Lean.Compiler.LCNF.Internalize.internalizeArgs {pu : Purity} (args : Array (Arg pu)) :
        InternalizeM pu (Array (Arg pu))
        Instances For
          source
          def Lean.Compiler.LCNF.Internalize.internalizeLetDecl {pu : Purity} (decl : LetDecl pu) :
          InternalizeM pu (LetDecl pu)
          Instances For
            source
            partial def Lean.Compiler.LCNF.Internalize.internalizeFunDecl {pu : Purity} (decl : FunDecl pu) :
            InternalizeM pu (FunDecl pu)
            source
            partial def Lean.Compiler.LCNF.Internalize.internalizeCode {pu : Purity} (code : Code pu) :
            InternalizeM pu (Code pu)
            source
            def Lean.Compiler.LCNF.Internalize.internalizeCodeDecl {pu : Purity} (decl : CodeDecl pu) :
            InternalizeM pu (CodeDecl pu)
            Instances For
              source
              def Lean.Compiler.LCNF.Code.internalize {pu : Purity} (code : Code pu) (s : FVarSubst pu := ∅) :
              CompilerM (Code pu)

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

              Instances For
                source
                def Lean.Compiler.LCNF.Decl.internalize {pu : Purity} (decl : Decl pu) (s : FVarSubst pu := ∅) :
                CompilerM (Decl pu)
                Instances For
                  source
                  def Lean.Compiler.LCNF.cleanup {pu : Purity} (decl : Array (Decl pu)) :
                  CompilerM (Array (Decl pu))

                  Create a fresh local context and internalize the given decls.

                  Instances For
                    source
                    def Lean.Compiler.LCNF.normalizeFVarIds {pu : Purity} (decl : Decl pu) :
                    CoreM (Decl pu)
                    Instances For