diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean index 0868f508a9..30fe29d466 100644 --- a/src/Lean/Compiler/ExternAttr.lean +++ b/src/Lean/Compiler/ExternAttr.lean @@ -40,16 +40,14 @@ inductive ExternEntry where encoding: ```.arity? = 2, .entries = [standard `cpp "ioPrimPrintln"]``` -/ structure ExternAttrData where - arity? : Option Nat := none entries : List ExternEntry deriving Inhabited, BEq, Hashable -- def externEntry := leading_parser optional ident >> optional (nonReservedSymbol "inline ") >> strLit -- @[builtin_attr_parser] def extern := leading_parser nonReservedSymbol "extern " >> optional numLit >> many externEntry private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do - let arity? := if stx[1].isNone then none else some <| stx[1][0].isNatLit?.getD 0 let entriesStx := stx[2].getArgs - if entriesStx.size == 0 && arity? == none then + if entriesStx.size == 0 then return { entries := [ ExternEntry.adhoc `all ] } let mut entries := #[] for entryStx in entriesStx do @@ -61,7 +59,7 @@ private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do entries := entries.push <| ExternEntry.standard backend str else entries := entries.push <| ExternEntry.inline backend str - return { arity? := arity?, entries := entries.toList } + return { entries := entries.toList } -- Forward declaration @[extern "lean_add_extern"] @@ -142,24 +140,4 @@ def getExternNameFor (env : Environment) (backend : Name) (fn : Name) : Option S | ExternEntry.standard _ n => pure n | _ => failure -private def getExternConstArity (declName : Name) : CoreM Nat := do - let fromSignature : Unit → CoreM Nat := fun _ => do - let cinfo ← getConstInfo declName - let (arity, _) ← (Meta.forallTelescopeReducing cinfo.type fun xs _ => pure xs.size : MetaM Nat).run - return arity - let env ← getEnv - match getExternAttrData? env declName with - | none => fromSignature () - | some data => match data.arity? with - | some arity => return arity - | none => fromSignature () - -def getExternConstArityExport (env : Environment) (declName : Name) : IO (Option Nat) := do - try - let (arity, _) ← (getExternConstArity declName).toIO { fileName := "", fileMap := default } { env := env } - return some arity - catch - | IO.Error.userError _ => return none - | _ => return none - end Lean diff --git a/src/Lean/Compiler/IR/CompilerM.lean b/src/Lean/Compiler/IR/CompilerM.lean index 15afe91bc4..1cd6546b22 100644 --- a/src/Lean/Compiler/IR/CompilerM.lean +++ b/src/Lean/Compiler/IR/CompilerM.lean @@ -133,9 +133,9 @@ builtin_initialize declMapExt : SimplePersistentEnvExtension Decl DeclMap ← match d with | .fdecl f xs ty b info => if let some (.str _ s) := getExportNameFor? env f then - return .extern f xs ty { arity? := xs.size, entries := [.standard `all s] } + return .extern f xs ty { entries := [.standard `all s] } else - return .extern f xs ty { arity? := xs.size, entries := [.opaque f] } + return .extern f xs ty { entries := [.opaque f] } | d => some d else entries -- Written to on codegen environment branch but accessed from other elaboration branches when diff --git a/src/Lean/Compiler/LCNF/PhaseExt.lean b/src/Lean/Compiler/LCNF/PhaseExt.lean index 9ebec46309..0e6139fe92 100644 --- a/src/Lean/Compiler/LCNF/PhaseExt.lean +++ b/src/Lean/Compiler/LCNF/PhaseExt.lean @@ -114,7 +114,7 @@ def mkDeclExt (phase : Phase) (name : Name := by exact decl_name%) : IO DeclExt if isDeclTransparent env phase decl.name then some decl else - some { decl with value := .extern { arity? := decl.getArity, entries := [.opaque decl.name] } } + some { decl with value := .extern { entries := [.opaque decl.name] } } return entries statsFn := fun s => let numEntries := s.foldl (init := 0) (fun count _ _ => count + 1) diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..7ef6c4e789 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,5 +1,5 @@ #include "util/options.h" - +// please update stage0 namespace lean { options get_default_options() { options opts;