Documentation

Lean.Compiler.LCNF.Internalize

source
structure Lean.Compiler.LCNF.Internalize.Context :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Lean.Compiler.LCNF.Internalize.InternalizeM (pu : Purity) (α : Type) :
    Type
    Instances For
      source
      @[inline]
      def Lean.Compiler.LCNF.Internalize.InternalizeM.run {pu : Purity} {α : Type} (x : InternalizeM pu α) (state : FVarSubst pu) (ctx : Context := { }) :
      CompilerM (α × FVarSubst pu)
      Instances For
        source
        @[inline]
        def Lean.Compiler.LCNF.Internalize.InternalizeM.run' {pu : Purity} {α : Type} (x : InternalizeM pu α) (state : FVarSubst pu) (ctx : Context := { }) :
        CompilerM α
        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 := ∅) (uniqueIdents : Bool := false) :
                    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 := ∅) (uniqueIdents : Bool := false) :
                      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