Tools

-- Read n bytes of OS entropy and combine them into a single Nat
def randomBytes (n : USize) : IO Nat := do
  let bytes ← IO.getRandomBytes n
  return bytes.toList.foldl (fun acc b => acc * 256 + b.toNat) 0

-- Return a Nat sampled uniformly from [lo, hi] (both inclusive)
def randomInRange (lo hi : Nat) : IO Nat := do
  let raw ← randomBytes 4  -- 4 bytes = 32 bits of entropy
  return lo + raw % (hi - lo + 1)

-- Pure helper exposed for testing: maps a raw value to the range [lo, hi]
def mapToRange (lo hi raw : Nat) : Nat := lo + raw % (hi - lo + 1)

-- raw = 0 always maps to lo
#guard mapToRange 1 6 0 == 1
-- raw = hi - lo always maps to hi (the top is reachable)
#guard mapToRange 0 5 5 == 5
-- result is always at most hi
#guard mapToRange 0 9 999 ≤ 9
-- result is always at least lo
#guard mapToRange 3 7 0 ≥ 3

def main : IO Unit := do
  let roll ← randomInRange 1 6
  IO.println s!"dice roll: {roll}"
  let pick ← randomInRange 0 2
  IO.println s!"random colour: {(["red", "green", "blue"])[pick]!}"
  -- sample a few values to show the range
  let samples ← List.range 5 |>.mapM (fun _ => randomInRange 10 99)
  IO.println s!"five samples in [10, 99]: {samples}"

dice roll: 1
random colour: blue
five samples in [10, 99]: [96, 93, 40, 56, 71]

-- Construct a JSON object with named fields
def makePerson (name : String) (age : Nat) : Json :=
  Json.mkObj [("name", Json.str name), ("age", Json.num age)]

-- Construct a JSON array of numbers
def makeScores (xs : List Nat) : Json :=
  Json.arr (xs.map (Json.num ∘ JsonNumber.fromNat)).toArray

-- Extract a String field; return none if absent or the wrong type
def getStr (j : Json) (key : String) : Option String :=
  match j.getObjValAs? String key with
  | .ok s    => some s
  | .error _ => none

-- Extract a Nat field; return none if absent or the wrong type
def getNat (j : Json) (key : String) : Option Nat :=
  match j.getObjValAs? Nat key with
  | .ok n    => some n
  | .error _ => none

-- build: fields are accessible after construction
#guard
  let p := makePerson "Ada" 36
  getStr p "name" == some "Ada" && getNat p "age" == some 36

-- build: missing field returns none
#guard (getNat (makePerson "Euler" 76) "score").isNone

-- array: length matches the source list
#guard
  match makeScores [10, 20, 30] with
  | Json.arr vs => vs.size == 3
  | _           => false

-- parse: round-trip through a JSON string
#guard
  match Json.parse "{\"name\": \"Grace\", \"age\": 107}" with
  | .error _ => false
  | .ok v    => getStr v "name" == some "Grace" && getNat v "age" == some 107

-- parse: malformed input signals an error
#guard !(Json.parse "not json").isOk

def main : IO Unit := do
  -- Build and print
  let p := makePerson "Lean" 4
  IO.println s!"person: {p}"
  IO.println s!"scores: {makeScores [85, 92, 78]}"
  -- Parse a JSON string and extract fields
  match Json.parse "{\"name\": \"Turing\", \"age\": 41}" with
  | .error e => IO.println s!"parse error: {e}"
  | .ok v    =>
    let name := (getStr v "name").getD "?"
    let age  := (getNat v "age").getD  0
    IO.println s!"parsed: {name}, age {age}"

person: {"name": "Lean", "age": 4}
scores: [85, 92, 78]
parsed: Turing, age 41

-- Fetch the body of a plain-HTTP URL using Lean's native HTTP library.
-- Returns none if the URL is malformed, DNS lookup fails,
-- or the TCP connection is refused.  HTTPS is not supported.
def fetchUrl (url : String) : IO (Option String) := do
  try
    -- parse the URL and extract host and port
    let some uri := URI.parse? url | return none
    let some auth := uri.authority | return none
    let host := toString auth.host
    let port : UInt16 := match auth.port with
      | .value p => p
      | _        => URI.Scheme.defaultPort uri.scheme
    -- resolve hostname to one or more IP addresses
    let addrs ← (DNS.getAddrInfo host "http").block
    let some ip := addrs[0]? | return none
    let sockAddr : SocketAddress := match ip with
      | .v4 a => .v4 { addr := a, port := port }
      | .v6 a => .v6 { addr := a, port := port }
    -- build the request target (path + query string)
    let pathStr :=
      let p := toString uri.path
      let q := toString uri.query
      if p.isEmpty then "/" ++ q else p ++ q
    let target := RequestTarget.originForm! pathStr
    let reqHead := (Request.get target
      |>.header! "Host"       host
      |>.header! "Connection" "close").line
    -- connect, send the request, and read the full response
    let client ← TCP.Socket.Client.mk
    (client.connect sockAddr).block
    (client.send (Encode.encode (v := .v11) .empty reqHead).toByteArray).block
    let mut raw : ByteArray := .empty
    let mut done := false
    while !done do
      match ← (client.recv? 4096).block with
      | none       => done := true
      | some chunk => raw := raw ++ chunk
    (client.shutdown).block
    -- strip response headers; body follows the first blank line
    let response := String.fromUTF8? raw |>.getD ""
    return match response.splitOn "\r\n\r\n" with
    | _ :: rest => some (String.intercalate "\r\n\r\n" rest)
    | []        => none
  catch _ =>
    return none

def main (args : List String) : IO Unit := do
  let url := args.headD "http://httpbin.org/get"
  IO.println s!"fetching: {url}"
  match ← fetchUrl url with
  | none      => IO.println "request failed"
  | some body =>
    IO.println s!"status: ok ({body.length} bytes)"
    match Json.parse body with
    | .error e => IO.println s!"JSON parse error: {e}"
    | .ok v    =>
      match v with
      | Json.obj m =>
        for (k, val) in m.toList do
          IO.println s!"  {k}: {val}"
      | _ => IO.println s!"body: {body}"

fetching: http://httpbin.org/get
status: ok (199 bytes)
  args: {}
  headers: {"X-Amzn-Trace-Id": "Root=1-6a199ea5-6764aa4b4ed01b5409c9bc65",
 "Host": "httpbin.org"}
  origin: "142.188.27.125"
  url: "http://httpbin.org/get"

-- Read an environment variable, falling back to a default when unset
def getEnvOr (key default : String) : IO String :=
  return (← IO.getEnv key) |>.getD default

-- Parse one "KEY=VALUE" line; skip blank lines and # comments
def parseLine (line : String) : Option (String × String) :=
  let t := line.trimAscii.toString
  if t.isEmpty || t.startsWith "#" then none
  else
    match t.splitOn "=" with
    | [] | [_] => none
    | k :: rest =>
      let key := k.trimAscii.toString
      -- rejoin with "=" in case the value itself contains "="
      let val := (String.intercalate "=" rest).trimAscii.toString
      if key.isEmpty then none else some (key, val)

-- Parse a .env-style file into a list of (key, value) pairs
def parseEnvFile (text : String) : List (String × String) :=
  text.splitOn "\n" |>.filterMap parseLine

-- blank lines and comments are skipped
#guard parseLine ""        == none
#guard parseLine "# note"  == none

-- a simple KEY=VALUE line is parsed correctly
#guard parseLine "HOST=localhost" == some ("HOST", "localhost")

-- values may contain "=" (only the first "=" is the separator)
#guard parseLine "URL=http://x.com/a=b" == some ("URL", "http://x.com/a=b")

-- a multi-line file with blanks and a comment
#guard
  parseEnvFile "HOST=localhost\nPORT=5432\n# comment\n\nUSER=admin" ==
  [("HOST", "localhost"), ("PORT", "5432"), ("USER", "admin")]

def main : IO Unit := do
  -- Read individual environment variables
  let home ← getEnvOr "HOME" "(not set)"
  let user ← getEnvOr "USER" "(not set)"
  IO.println s!"HOME: {home}"
  IO.println s!"USER: {user}"
  -- Parse a .env-style config embedded as a string
  let config := "DB_HOST=localhost\nDB_PORT=5432\n# database name\nDB_NAME=myapp"
  IO.println "parsed config:"
  for (k, v) in parseEnvFile config do
    IO.println s!"  {k} = {v}"

HOME: /Users/gvwilson
USER: gvwilson
parsed config:
  DB_HOST = localhost
  DB_PORT = 5432
  DB_NAME = myapp