source
inductive Lean.ExternEntry :
Type

- adhoc (backend : Name) : ExternEntry
- inline (backend : Name) (pattern : String) : ExternEntry
- standard (backend : Name) (fn : String) : ExternEntry
- opaque (fn : Name) : ExternEntry

  Call to a Lean function without exported IR.

Instances For

source
def Lean.instBEqExternEntry.beq :
ExternEntry → ExternEntry → Bool
Equations

- Lean.instBEqExternEntry.beq (Lean.ExternEntry.adhoc a) (Lean.ExternEntry.adhoc b) = (a == b)
- Lean.instBEqExternEntry.beq (Lean.ExternEntry.inline a a_1) (Lean.ExternEntry.inline b b_1) = (a == b && a_1 == b_1)
- Lean.instBEqExternEntry.beq (Lean.ExternEntry.standard a a_1) (Lean.ExternEntry.standard b b_1) = (a == b && a_1 == b_1)
- Lean.instBEqExternEntry.beq (Lean.ExternEntry.opaque a) (Lean.ExternEntry.opaque b) = (a == b)
- Lean.instBEqExternEntry.beq x✝¹ x✝ = false

Instances For

source
instance Lean.instBEqExternEntry :
BEq ExternEntry
Equations

- Lean.instBEqExternEntry = { beq := Lean.instBEqExternEntry.beq }

source
def Lean.instHashableExternEntry.hash :
ExternEntry → UInt64
Equations

- Lean.instHashableExternEntry.hash (Lean.ExternEntry.adhoc a) = mixHash 0 (hash a)
- Lean.instHashableExternEntry.hash (Lean.ExternEntry.inline a a_1) = mixHash (mixHash 1 (hash a)) (hash a_1)
- Lean.instHashableExternEntry.hash (Lean.ExternEntry.standard a a_1) = mixHash (mixHash 2 (hash a)) (hash a_1)
- Lean.instHashableExternEntry.hash (Lean.ExternEntry.opaque a) = mixHash 3 (hash a)

Instances For

source
instance Lean.instHashableExternEntry :
Hashable ExternEntry
Equations

- Lean.instHashableExternEntry = { hash := Lean.instHashableExternEntry.hash }

source
structure Lean.ExternAttrData :
Type

- `@[extern]` encoding: `.entries = [adhoc `all]`
- `@[extern "level_hash"]` encoding: `.entries = [standard `all "levelHash"]`
- `@[extern cpp "lean::string_size" llvm "lean_str_size"]` encoding: `.entries = [standard `cpp "lean::string_size", standard `llvm "leanStrSize"]`
- `@[extern cpp inline "#1 + #2"]` encoding: `.entries = [inline `cpp "#1 + #2"]`
- `@[extern cpp "foo" llvm adhoc]` encoding: `.entries = [standard `cpp "foo", adhoc `llvm]`

- entries : List ExternEntry

Instances For

source
def Lean.instInhabitedExternAttrData.default :
ExternAttrData
Equations

- Lean.instInhabitedExternAttrData.default = { entries := default }

Instances For

source
instance Lean.instInhabitedExternAttrData :
Inhabited ExternAttrData
Equations

- Lean.instInhabitedExternAttrData = { default := Lean.instInhabitedExternAttrData.default }

source
def Lean.instBEqExternAttrData.beq :
ExternAttrData → ExternAttrData → Bool
Equations

- Lean.instBEqExternAttrData.beq { entries := a } { entries := b } = (a == b)
- Lean.instBEqExternAttrData.beq x✝¹ x✝ = false

Instances For

source
instance Lean.instBEqExternAttrData :
BEq ExternAttrData
Equations

- Lean.instBEqExternAttrData = { beq := Lean.instBEqExternAttrData.beq }

source
instance Lean.instHashableExternAttrData :
Hashable ExternAttrData
Equations

- Lean.instHashableExternAttrData = { hash := Lean.instHashableExternAttrData.hash }

source
def Lean.instHashableExternAttrData.hash :
ExternAttrData → UInt64
Equations

- Lean.instHashableExternAttrData.hash { entries := a } = mixHash 0 (hash a)

Instances For

source
@[extern lean_add_extern]
opaque Lean.addExtern (declName : Name) (externAttrData : ExternAttrData) :
CoreM Unit
source
opaque Lean.externAttr :
ParametricAttribute ExternAttrData
source
def Lean.getExternAttrData? (env : Environment) (n : Name) :
Option ExternAttrData
Equations

- Lean.getExternAttrData? env n = Lean.externAttr.getParam? env n

Instances For

source
def Lean.expandExternPatternAux (args : List String) :
Nat → String.Iterator → String → String
Equations

- One or more equations did not get rendered due to their size.
- Lean.expandExternPatternAux args 0 x✝¹ x✝ = x✝

Instances For

source
def Lean.expandExternPattern (pattern : String) (args : List String) :
String
Equations

- Lean.expandExternPattern pattern args = Lean.expandExternPatternAux args pattern.length pattern.mkIterator ""

Instances For

source
def Lean.mkSimpleFnCall (fn : String) (args : List String) :
String
Equations

- Lean.mkSimpleFnCall fn args = fn ++ "(" ++ List.foldl (fun (x1 x2 : String) => x1 ++ x2) "" (List.intersperse ", " args) ++ ")"

Instances For

source
def Lean.ExternEntry.backend :
ExternEntry → Name
Equations

- (Lean.ExternEntry.adhoc a).backend = a
- (Lean.ExternEntry.inline a a_1).backend = a
- (Lean.ExternEntry.standard a a_1).backend = a
- (Lean.ExternEntry.opaque a).backend = `all

Instances For

source
def Lean.getExternEntryForAux (backend : Name) (entries : List ExternEntry) :
Option ExternEntry
Equations

- Lean.getExternEntryForAux backend entries = List.find? (fun (e : Lean.ExternEntry) => e.backend == `all || e.backend == backend) entries

Instances For

source
def Lean.getExternEntryFor (d : ExternAttrData) (backend : Name) :
Option ExternEntry
Equations

- Lean.getExternEntryFor d backend = Lean.getExternEntryForAux backend d.entries

Instances For

source
def Lean.isExtern (env : Environment) (fn : Name) :
Bool
Equations

- Lean.isExtern env fn = (Lean.getExternAttrData? env fn).isSome

Instances For

source
def Lean.isExternC (env : Environment) (fn : Name) :
Bool

We say a Lean function marked as `[extern "<c_fn_name>"]` is for all backends, and it is implemented using `extern "C"`. Thus, there is no name mangling.

Equations

- Lean.isExternC env fn = match Lean.getExternAttrData? env fn with | some { entries := [Lean.ExternEntry.standard `all fn] } => true | x => false

Instances For

source
def Lean.getExternNameFor (env : Environment) (backend fn : Name) :
Option String
Equations

- One or more equations did not get rendered due to their size.

Instances For