fd3d42ae33
git-subtree-dir: golang-lean git-subtree-mainline:6487c7046fgit-subtree-split:f5f1701922
37 lines
1.1 KiB
Text
37 lines
1.1 KiB
Text
import GolangLean.Value
|
||
|
||
namespace GolangLean
|
||
|
||
/-! # Environment / heap.
|
||
|
||
Distinct from octive-lean's flat `Env`: Go has lexically-nested scopes,
|
||
addressable variables (so a `&x` produces a stable heap index), and a
|
||
package-level namespace. This is a placeholder shape; flesh out as needed. -/
|
||
|
||
abbrev Frame := List (String × Value)
|
||
|
||
structure Env where
|
||
frames : List Frame -- top of list = innermost scope
|
||
package : List (String × Value) -- package-level decls
|
||
heap : Array Value -- addressable cells (`&x` returns an index)
|
||
builtins : List (String × (Array Value → IO (Except String Value)))
|
||
deriving Inhabited
|
||
|
||
namespace Env
|
||
|
||
def empty : Env :=
|
||
{ frames := [[]], package := [], heap := #[], builtins := [] }
|
||
|
||
/-- Look up a name: innermost frame first, then package, then builtins (later). -/
|
||
def lookup (env : Env) (name : String) : Option Value :=
|
||
let rec go : List Frame → Option Value
|
||
| [] => env.package.lookup name
|
||
| f :: fs =>
|
||
match f.lookup name with
|
||
| some v => some v
|
||
| none => go fs
|
||
go env.frames
|
||
|
||
end Env
|
||
|
||
end GolangLean
|