Documentation

Lean.Compiler.IR.EmitC

Equations
    Instances For
      Instances For
        @[reducible, inline]
        abbrev Lean.IR.EmitC.M (α : Type) :
        Equations
          Instances For
            Equations
              Instances For
                Equations
                  Instances For
                    Equations
                      Instances For
                        @[inline]
                        def Lean.IR.EmitC.emit {α : Type} [ToString α] (a : α) :
                        Equations
                          Instances For
                            @[inline]
                            def Lean.IR.EmitC.emitLn {α : Type} [ToString α] (a : α) :
                            Equations
                              Instances For
                                def Lean.IR.EmitC.emitLns {α : Type} [ToString α] (as : List α) :
                                Equations
                                  Instances For
                                    Equations
                                      Instances For
                                        Equations
                                          Instances For
                                            Equations
                                              Instances For
                                                Equations
                                                  Instances For
                                                    Equations
                                                      Instances For
                                                        Equations
                                                          Instances For
                                                            Equations
                                                              Instances For
                                                                Equations
                                                                  Instances For
                                                                    def Lean.IR.EmitC.emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) :
                                                                    Equations
                                                                      Instances For
                                                                        def Lean.IR.EmitC.emitFnDecl (decl : Decl) (isExternal : Bool) :
                                                                        Equations
                                                                          Instances For
                                                                            def Lean.IR.EmitC.emitExternDeclAux (decl : Decl) (cNameStr : String) :
                                                                            Equations
                                                                              Instances For
                                                                                Equations
                                                                                  Instances For
                                                                                    Equations
                                                                                      Instances For
                                                                                        Equations
                                                                                          Instances For
                                                                                            Equations
                                                                                              Instances For
                                                                                                Equations
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                      Instances For
                                                                                                        Equations
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                  Instances For
                                                                                                                    Equations
                                                                                                                      Instances For
                                                                                                                        def Lean.IR.EmitC.emitTag (x : VarId) (xType : IRType) :
                                                                                                                        Equations
                                                                                                                          Instances For
                                                                                                                            Equations
                                                                                                                              Instances For
                                                                                                                                def Lean.IR.EmitC.emitInc (x : VarId) (n : Nat) (checkRef : Bool) :
                                                                                                                                Equations
                                                                                                                                  Instances For
                                                                                                                                    def Lean.IR.EmitC.emitDec (x : VarId) (n : Nat) (checkRef : Bool) :
                                                                                                                                    Equations
                                                                                                                                      Instances For
                                                                                                                                        Equations
                                                                                                                                          Instances For
                                                                                                                                            Equations
                                                                                                                                              Instances For
                                                                                                                                                def Lean.IR.EmitC.emitSet (x : VarId) (i : Nat) (y : Arg) :
                                                                                                                                                Equations
                                                                                                                                                  Instances For
                                                                                                                                                    Equations
                                                                                                                                                      Instances For
                                                                                                                                                        def Lean.IR.EmitC.emitUSet (x : VarId) (n : Nat) (y : VarId) :
                                                                                                                                                        Equations
                                                                                                                                                          Instances For
                                                                                                                                                            def Lean.IR.EmitC.emitSSet (x : VarId) (n offset : Nat) (y : VarId) (t : IRType) :
                                                                                                                                                            Equations
                                                                                                                                                              Instances For
                                                                                                                                                                Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            def Lean.IR.EmitC.emitReset (z : VarId) (n : Nat) (x : VarId) :
                                                                                                                                                                                            Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                def Lean.IR.EmitC.emitReuse (z x : VarId) (c : CtorInfo) (updtHeader : Bool) (ys : Array Arg) :
                                                                                                                                                                                                Equations
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    def Lean.IR.EmitC.emitProj (z : VarId) (i : Nat) (x : VarId) :
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        def Lean.IR.EmitC.emitUProj (z : VarId) (i : Nat) (x : VarId) :
                                                                                                                                                                                                        Equations
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            def Lean.IR.EmitC.emitSProj (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) :
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                            def Lean.IR.EmitC.emitBox (z x : VarId) (xType : IRType) :
                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                    Given [p_0, ..., p_{n-1}], [y_0, ..., y_{n-1}], representing the assignments

                                                                                                                                                                                                                                                                                    p_0 := y_0,
                                                                                                                                                                                                                                                                                    ...
                                                                                                                                                                                                                                                                                    p_{n-1} := y_{n-1}
                                                                                                                                                                                                                                                                                    

                                                                                                                                                                                                                                                                                    Return true iff we have (i, j) where j > i, and y_j == p_i. That is, we have

                                                                                                                                                                                                                                                                                          p_i := y_i,
                                                                                                                                                                                                                                                                                          ...
                                                                                                                                                                                                                                                                                          p_j := p_i, -- p_i was overwritten above
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                            partial def Lean.IR.EmitC.emitIf (x : VarId) (xType : IRType) (tag : Nat) (t e : FnBody) :
                                                                                                                                                                                                                                                                                            partial def Lean.IR.EmitC.emitCase (x : VarId) (xType : IRType) (alts : Array Alt) :
                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                        @[export lean_ir_emit_c]
                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                          Instances For