feat(library/init/lean/compiler/ir): add ExternEntry to Decl.extern constructor

library/init/lean/compiler/ir/basic.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.name init.lean.kvmap init.lean.format init.data.array
+import init.data.array
+import init.lean.name init.lean.extern
+import init.lean.kvmap init.lean.format
 /-
 Implements (extended) λPure and λRc proposed in the article
 "Counting Immutable Beans", Sebastian Ullrich and Leonardo de Moura.
@@ -338,24 +340,24 @@ bs.hmmap $ λ b, match b with
 
 inductive Decl
 | fdecl  (f : FunId) (xs : Array Param) (ty : IRType) (b : FnBody)
-| extern (f : FunId) (xs : Array Param) (ty : IRType)
+| extern (f : FunId) (xs : Array Param) (ty : IRType) (ext : ExternEntry)
 
 namespace Decl
 
 instance : Inhabited Decl :=
-⟨extern (default _) (default _) IRType.irrelevant⟩
+⟨fdecl (default _) (default _) IRType.irrelevant (default _)⟩
 
 def name : Decl → FunId
-| (Decl.fdecl f _ _ _) := f
-| (Decl.extern f _ _)  := f
+| (Decl.fdecl f _ _ _)  := f
+| (Decl.extern f _ _ _) := f
 
 def params : Decl → Array Param
-| (Decl.fdecl _ xs _ _) := xs
-| (Decl.extern _ xs _)  := xs
+| (Decl.fdecl _ xs _ _)  := xs
+| (Decl.extern _ xs _ _) := xs
 
 def resultType : Decl → IRType
-| (Decl.fdecl _ _ t _) := t
-| (Decl.extern _ _ t)  := t
+| (Decl.fdecl _ _ t _)  := t
+| (Decl.extern _ _ t _) := t
 
 end Decl
 

library/init/lean/compiler/ir/checker.lean

@@ -98,8 +98,8 @@ partial def checkFnBody : FnBody → M Unit
 | (FnBody.unreachable)      := pure ()
 
 def checkDecl : Decl → M Unit
-| (Decl.fdecl f xs t b) := withParams xs (checkFnBody b)
-| (Decl.extern f xs t)  := withParams xs (pure ())
+| (Decl.fdecl f xs t b)  := withParams xs (checkFnBody b)
+| (Decl.extern f xs t _) := withParams xs (pure ())
 
 end Checker
 

library/init/lean/compiler/ir/format.lean

@@ -92,8 +92,8 @@ instance fnBodyHasFormat : HasFormat FnBody := ⟨formatFnBody⟩
 instance fnBodyHasToString : HasToString FnBody := ⟨λ b, (format b).pretty⟩
 
 def formatDecl (indent : Nat := 2) : Decl → Format
-| (Decl.fdecl f xs ty b) := "def " ++ format f ++ formatArray xs ++ format " : " ++ format ty ++ " :=" ++ Format.nest indent (Format.line ++ formatFnBody indent b)
-| (Decl.extern f xs ty)  := "extern " ++ format f ++ formatArray xs ++ format " : " ++ format ty
+| (Decl.fdecl f xs ty b)  := "def " ++ format f ++ formatArray xs ++ format " : " ++ format ty ++ " :=" ++ Format.nest indent (Format.line ++ formatFnBody indent b)
+| (Decl.extern f xs ty _) := "extern " ++ format f ++ formatArray xs ++ format " : " ++ format ty
 
 instance declHasFormat : HasFormat Decl := ⟨formatDecl⟩
 

library/init/lean/compiler/ir/freevars.lean

@@ -73,8 +73,8 @@ partial def collectFnBody : FnBody → Collector
 | FnBody.unreachable        := skip
 
 partial def collectDecl : Decl → Collector
-| (Decl.fdecl _ xs _ b) := collectParams xs; collectFnBody b
-| (Decl.extern _ xs _)  := collectParams xs
+| (Decl.fdecl _ xs _ b)  := collectParams xs; collectFnBody b
+| (Decl.extern _ xs _ _) := collectParams xs
 
 end MaxIndex
 

library/init/lean/compiler/ir/normids.lean

@@ -31,8 +31,8 @@ partial def checkFnBody : FnBody → M Bool
 | b                       := if b.isTerminal then pure true else checkFnBody b.body
 
 partial def checkDecl : Decl → M Bool
-| (Decl.fdecl _ xs _ b) := checkParams xs <&&> checkFnBody b
-| (Decl.extern _ xs _)  := checkParams xs
+| (Decl.fdecl _ xs _ b)  := checkParams xs <&&> checkFnBody b
+| (Decl.extern _ xs _ _) := checkParams xs
 
 end UniqueIds