Lean.Compiler.ExternAttr

source

inductive Lean.ExternEntry :

Type

adhoc: Lean.Name → Lean.ExternEntry
inline: Lean.Name → String → Lean.ExternEntry
standard: Lean.Name → String → Lean.ExternEntry
foreign: Lean.Name → String → Lean.ExternEntry

source

structure Lean.ExternAttrData :

Type

arity? : Option Nat
entries : List Lean.ExternEntry

source

instance Lean.instInhabitedExternAttrData :

Inhabited Lean.ExternAttrData

Equations

Lean.instInhabitedExternAttrData = { default := { arity? := default, entries := default } }

source

@[extern lean_add_extern]

constant Lean.addExtern (env : Lean.Environment) (n : Lean.Name) :

ExceptT String Id Lean.Environment

source

constant Lean.externAttr :

Lean.ParametricAttribute Lean.ExternAttrData

source

def Lean.getExternAttrData (env : Lean.Environment) (n : Lean.Name) :

Option Lean.ExternAttrData

Equations

Lean.getExternAttrData env n = Lean.ParametricAttribute.getParam Lean.externAttr env n

source

def Lean.expandExternPatternAux (args : List String) :

Nat → String.Iterator → String → String

Equations

Lean.expandExternPatternAux args 0 x x = x
Lean.expandExternPatternAux args (Nat.succ i) x x = if ¬String.Iterator.hasNext x = true then x else let c := String.Iterator.curr x; if c ≠ Char.ofNat 35 then Lean.expandExternPatternAux args i (String.Iterator.next x) (String.push x c) else let it := String.Iterator.next x; let x := Lean.parseOptNum (String.Iterator.remainingBytes it) it 0; let j := x.2 - 1; Lean.expandExternPatternAux args i x.1 (x ++ List.getD args j "")

source

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

String

Equations

Lean.expandExternPattern pattern args = Lean.expandExternPatternAux args (String.length pattern) (String.mkIterator pattern) ""

source

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

String

Equations

Lean.mkSimpleFnCall fn args = fn ++ "(" ++ List.foldl (fun a a_1 => a ++ a_1) "" (List.intersperse ", " args) ++ ")"

source

def Lean.ExternEntry.backend :

Lean.ExternEntry → Lean.Name

Equations

Lean.ExternEntry.backend x = match x with | Lean.ExternEntry.adhoc n => n | Lean.ExternEntry.inline n x => n | Lean.ExternEntry.standard n x => n | Lean.ExternEntry.foreign n x => n

source

def Lean.getExternEntryForAux (backend : Lean.Name) :

List Lean.ExternEntry → Option Lean.ExternEntry

Equations

Lean.getExternEntryForAux backend [] = none
Lean.getExternEntryForAux backend (e :: es) = if (Lean.ExternEntry.backend e == `all) = true then some e else if (Lean.ExternEntry.backend e == backend) = true then some e else Lean.getExternEntryForAux backend es

source

def Lean.getExternEntryFor (d : Lean.ExternAttrData) (backend : Lean.Name) :

Option Lean.ExternEntry

Equations

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

source

def Lean.isExtern (env : Lean.Environment) (fn : Lean.Name) :

Bool

Equations

Lean.isExtern env fn = Option.isSome (Lean.getExternAttrData env fn)

source

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

Bool

Equations

Lean.isExternC env fn = match Lean.getExternAttrData env fn with | some { arity? := x_1, entries := [Lean.ExternEntry.standard (Lean.Name.str Lean.Name.anonymous "all" x_2) x] } => true | x => false

source

def Lean.getExternNameFor (env : Lean.Environment) (backend : Lean.Name) (fn : Lean.Name) :

Option String

Equations

Lean.getExternNameFor env backend fn = OptionM.run do let data ← Lean.getExternAttrData env fn let entry ← Lean.getExternEntryFor data backend match entry with | Lean.ExternEntry.standard x n => pure n | Lean.ExternEntry.foreign x n => pure n | x => failure

source

def Lean.getExternConstArityExport (env : Lean.Environment) (declName : Lean.Name) :

IO (Option Nat)

Equations

Lean.getExternConstArityExport env declName = do let r ← tryCatch (do let discr ← Lean.Core.CoreM.toIO (Lean.getExternConstArity declName) { options := { entries := [] }, currRecDepth := 0, maxRecDepth := 1000, ref := Lean.Syntax.missing, currNamespace := Lean.Name.anonymous, openDecls := [], initHeartbeats := 0, maxHeartbeats := Lean.Core.getMaxHeartbeats { entries := [] } } { env := env, nextMacroScope := Lean.firstFrontendMacroScope + 1, ngen := { namePrefix := `_uniq, idx := 1 }, traceState := { enabled := true, traces := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } } let x : Nat × Lean.Core.State := discr match x with | (arity, x) => pure (some arity)) fun ex => match ex with | IO.Error.userError msg => pure none | x => pure none pure r