A Template Expander

Model a simple template engine as a tree of nodes
Use recursive inductive types to represent template syntax
Walk the tree with an explicit context to substitute variables
Handle loops and conditionals with functional recursion

Template engines like Jinja and Mustache fill in placeholders with data
We'll build a minimal engine that supports variables, loops, and conditionals

Template Values

-- Values that can appear in a template context
inductive TVal where
  | Str  : String → TVal
  | List : List (List (String × TVal)) → TVal
  deriving Repr

TVal is a sum type for values in the template context
TVal.Str s holds a plain string
TVal.List items holds a list of contexts, one per loop iteration
- Each inner list is itself a Context (a list of (name, value) pairs) for that iteration

Context

-- A context maps variable names to template values
abbrev Context := List (String × TVal)

A context is a list of (name, value) pairs
- Like a Python dict but implemented as an association list
abbrev creates a type alias without introducing a new wrapper type
- Context and List (String × TVal) are fully interchangeable
Each variable lookup scans the list linearly
- Small contexts: this is simple and fine
- Large contexts: a HashMap would be faster but isn't in the prelude (DEBT)

Template Nodes

-- Template abstract syntax tree nodes
inductive TNode where
  | TText : String → TNode                    -- literal text
  | TVar  : String → TNode                    -- {{ var }}
  | TLoop : String → TNode → TNode            -- {% for x in list %} body {% end %}
  | TIf   : String → TNode → TNode → TNode   -- {% if var %} then {% else %} else {% end %}
  | TSeq  : List TNode → TNode                -- sequence of nodes
  deriving Repr

TNode defines the abstract syntax tree of a template
Five constructors:
- TNode.TText s: literal text, output as-is
- TNode.TVar name: variable substitution {% raw %}{{ var }}{% endraw %}
- TNode.TLoop name body: loop over a list {% raw %}{% for x in items %}...{% end %}{% endraw %}
- TNode.TIf name thenNode elseNode: conditional
- TNode.TSeq nodes: a sequence of nodes in order
TNode is recursive: branches can contain more TNode trees

Variable Lookup

-- Look up a variable in the context
def ctxGet (ctx : Context) (name : String) : Option TVal :=
  (ctx.find? (·.1 == name)).map (·.2)

ctxGet searches the context for a variable by name
ctx.find? (·.1 == name) returns the first pair where the key matches
- .1 accesses the first element of the (String × TVal) tuple
.map (·.2) extracts the value from the found pair
Returns Option TVal: some if found, none if not
- Like Python's dict.get(name) but more explicit

Expanding Templates

-- Expand a template node to a string using the given context
def expand (ctx : Context) : TNode → String
  | TNode.TText s     => s
  | TNode.TVar name   =>
      match ctxGet ctx name with
      | some (TVal.Str s) => s
      | _                 => ""
  | TNode.TLoop listName body =>
      match ctxGet ctx listName with
      | some (TVal.List items) =>
          items.foldl (init := "") fun acc itemCtx =>
            acc ++ expand (itemCtx ++ ctx) body
      | _ => ""
  | TNode.TIf varName thenNode elseNode =>
      match ctxGet ctx varName with
      | some (TVal.Str s) => if s.isEmpty then expand ctx elseNode
                             else expand ctx thenNode
      | some (TVal.List l) => if l.isEmpty then expand ctx elseNode
                              else expand ctx thenNode
      | none => expand ctx elseNode
  | TNode.TSeq nodes  => nodes.foldl (init := "") fun acc n => acc ++ expand ctx n

expand is the heart of the engine: recursively walks the tree and builds output
Each node type has a different expansion rule:
- TText: output the string directly
- TVar: look up the variable; output its string value (or "" if not found)
- TLoop: for each item in the list variable, expand the body with that item's context pushed on top
- TIf: check the variable; a non-empty Str or non-empty List is truthy → then branch; empty or missing → else branch
- TSeq: expand all child nodes and concatenate results with ++
itemCtx ++ ctx in TLoop pushes the loop variable's context in front
- The inner variable shadows any outer variable with the same name
foldl is used for both loops and sequences
- Accumulator starts as "" and grows as each element expands

Tests

-- Tests ----------------------------------------------------------------

-- Simple variable substitution: "Hello, {{ name }}!" with name="World"
def helloTmpl : TNode :=
  TNode.TSeq [TNode.TText "Hello, ", TNode.TVar "name", TNode.TText "!"]

#guard expand [("name", TVal.Str "World")] helloTmpl == "Hello, World!"

-- Loop: <ul>{% for item in items %}<li>{{ x }}</li>{% end %}</ul>
def listTmpl : TNode :=
  TNode.TSeq [
    TNode.TText "<ul>",
    TNode.TLoop "items"
      (TNode.TSeq [TNode.TText "<li>", TNode.TVar "x", TNode.TText "</li>"]),
    TNode.TText "</ul>"
  ]

def listCtx : Context := [
  ("items", TVal.List [[("x", TVal.Str "apples")], [("x", TVal.Str "bananas")]])
]

#guard expand listCtx listTmpl == "<ul><li>apples</li><li>bananas</li></ul>"

-- Conditional: {% if show %}visible{% else %}hidden{% end %}
def ifTmpl : TNode :=
  TNode.TIf "show" (TNode.TText "visible") (TNode.TText "hidden")

#guard expand [("show", TVal.Str "yes")] ifTmpl == "visible"
#guard expand [("show", TVal.Str "")]    ifTmpl == "hidden"
#guard expand []                         ifTmpl == "hidden"

-- Nested: variable inside conditional inside sequence
def nestedTmpl : TNode :=
  TNode.TSeq [
    TNode.TText "Status: ",
    TNode.TIf "active"
      (TNode.TSeq [TNode.TText "ON (", TNode.TVar "user", TNode.TText ")"])
      (TNode.TText "OFF")
  ]

#guard expand [("active", TVal.Str "1"), ("user", TVal.Str "admin")] nestedTmpl
        == "Status: ON (admin)"
#guard expand [("active", TVal.Str "")] nestedTmpl
        == "Status: OFF"

Four templates are tested with #guard
Variable substitution: "Hello, {{ name }}!" with name="World" → "Hello, World!"
Loop: <ul> with two list items → full HTML string
- Each loop iteration gets its own sub-context: [("x", "apples")], then [("x", "bananas")]
Conditional: "visible" when truthy, "hidden" when falsy or missing
Nested: variable inside conditional inside sequence
Notice the loop body uses x as the loop variable name
- The template defines {{ x }} in the body, and the data provides x in each item context

A Hello Template

-- Render a simple hello template
def helloTemplate : TNode :=
  TNode.TSeq [
    TNode.TText "<h1>Welcome, ",
    TNode.TVar "user",
    TNode.TText "!</h1>",
    TNode.TText "\n",
    TNode.TText "<p>You have ",
    TNode.TVar "count",
    TNode.TText " items.</p>"
  ]

def helloCtx : Context := [
  ("user", TVal.Str "Alice"),
  ("count", TVal.Str "3")
]

helloTemplate is a larger example: HTML with two variable substitutions
helloCtx provides values for both "user" and "count"
This template would render to:

<h1>Welcome, Alice!</h1>
<p>You have 3 items.</p>

A HashMap Context

-- A HashMap context: O(1) lookup keyed by variable name
abbrev HashCtx := HashMap String TVal

HashMap String TVal maps variable names directly to values
- Lookup is O(1) instead of O(n) scan down the association list
- From the Batteries library: import Batteries and open Std are required
ctx[name]? returns Option TVal — same return type as the list version
The change is entirely inside HashCtx and ctxGet: nothing else in the engine needs to know

-- O(1) lookup: index directly into the HashMap
def ctxGet (ctx : HashCtx) (name : String) : Option TVal :=
  ctx[name]?

ctx[name]? is HashMap's subscript operator — equivalent to HashMap.getElem? ctx name
- Like Python's ctx.get(name) on a dict

What Stays the Same

-- Same template AST as the association-list version — unchanged
inductive TNode where
  | TText : String → TNode
  | TVar  : String → TNode
  | TLoop : String → TNode → TNode
  | TIf   : String → TNode → TNode → TNode
  | TSeq  : List TNode → TNode
  deriving Repr

TNode is unchanged — it describes template syntax, not how context is stored
expand is also unchanged in structure: it calls ctxGet and recurses on nodes

-- expand is structurally identical to the list version;
-- only the Context type and ctxGet implementation differ
def expand (ctx : HashCtx) : TNode → String
  | TNode.TText s     => s
  | TNode.TVar name   =>
      match ctxGet ctx name with
      | some (TVal.Str s) => s
      | _                 => ""
  | TNode.TLoop listName body =>
      match ctxGet ctx listName with
      | some (TVal.List items) =>
          items.foldl (init := "") fun acc itemCtx =>
            -- merge loop-iteration variables on top of outer context
            let inner := itemCtx.foldl (fun m (k, v) => m.insert k v) ctx
            acc ++ expand inner body
      | _ => ""
  | TNode.TIf varName thenNode elseNode =>
      match ctxGet ctx varName with
      | some (TVal.Str s)  => if s.isEmpty then expand ctx elseNode
                              else expand ctx thenNode
      | some (TVal.List l) => if l.isEmpty then expand ctx elseNode
                              else expand ctx thenNode
      | none => expand ctx elseNode
  | TNode.TSeq nodes  => nodes.foldl (init := "") fun acc n => acc ++ expand ctx n

The only difference in expand is the loop case: merging an item's context into the HashMap
- itemCtx.foldl (fun m (k, v) => m.insert k v) ctx inserts the loop variables on top
- Instead of itemCtx ++ ctx (list prepend), we fold-insert into the parent map
Every other branch is structurally identical to the association-list version
This is encapsulation in practice: TNode and the core of expand are stable; only the context implementation changed

Running the HashMap Version

-- The same tests pass with the new context type
def helloTmpl : TNode :=
  TNode.TSeq [TNode.TText "Hello, ", TNode.TVar "name", TNode.TText "!"]

#guard expand (HashMap.ofList [("name", TVal.Str "World")]) helloTmpl == "Hello, World!"

def listTmpl : TNode :=
  TNode.TSeq [
    TNode.TText "<ul>",
    TNode.TLoop "items"
      (TNode.TSeq [TNode.TText "<li>", TNode.TVar "x", TNode.TText "</li>"]),
    TNode.TText "</ul>"
  ]

#guard expand
    (HashMap.ofList [("items", TVal.List
      [[("x", TVal.Str "apples")], [("x", TVal.Str "bananas")]])])
    listTmpl
  == "<ul><li>apples</li><li>bananas</li></ul>"

#guard expand (HashMap.ofList [("show", TVal.Str "yes")])
    (TNode.TIf "show" (TNode.TText "visible") (TNode.TText "hidden"))
  == "visible"

#guard expand ({} : HashCtx)
    (TNode.TIf "show" (TNode.TText "visible") (TNode.TText "hidden"))
  == "hidden"

def main : IO Unit := do
  let ctx : HashCtx := HashMap.ofList [
    ("user",  TVal.Str "Alice"),
    ("count", TVal.Str "3")
  ]
  let tmpl : TNode :=
    TNode.TSeq [
      TNode.TText "<h1>Welcome, ", TNode.TVar "user", TNode.TText "!</h1>\n",
      TNode.TText "<p>You have ", TNode.TVar "count", TNode.TText " items.</p>"
    ]
  IO.println (expand ctx tmpl)
  IO.println "Done."

The same tests pass with no changes to the test inputs or expected outputs
HashMap.ofList [...] builds a context from a list of pairs — like Python's dict([...])
In a real project, TVal, TNode, and expand would live in a shared module (see build) and both the association-list and HashMap versions would import from it

Running the Program

-- Entry point: render a template and print the result
-- Run with: lean --run template/code.lean
def main : IO Unit := do
  let output := expand helloCtx helloTemplate
  IO.println output
  IO.println "Done."

main renders helloTemplate and prints the result
IO.println output displays the rendered HTML
Compile and type-check with:
- lake env lean template/code.lean
Run interactively with:
- lean --run template/code.lean
The output is plain text — adding file I/O is left as an exercise (see io)

Exercises

Fix: Variable Not Found

-- ctxGet returns Option TVal, but this code treats it as a String. Fix it.
abbrev Context := List (String × TVal)

inductive TVal where | Str (s : String) | List (items : List Context)

def ctxGet (ctx : Context) (name : String) : Option TVal :=
  (ctx.find? (·.1 == name)).map (·.2)

def getGreeting (ctx : Context) : String :=
  let val := ctxGet ctx "user"
  s!"Hello, {val}!"

#guard getGreeting [("user", TVal.Str "Alice")] == "Hello, Alice!"
#guard getGreeting [] == "Hello, unknown!"

hint

ctxGet ctx "user" returns Option TVal, but the code tries to use it directly as a string
Add a match expression to handle some (TVal.Str s) and _ (not found)
Return "unknown" when the variable is missing

Fix: Loop Skips Items

-- The loop only processes the first item instead of all. Fix it.
abbrev Context := List (String × TVal)

inductive TVal where | Str (s : String) | List (items : List Context)

inductive TNode where
  | TText (s : String) | TVar (name : String)
  | TLoop (name : String) (body : TNode) | TSeq (nodes : List TNode)

def ctxGet (ctx : Context) (name : String) : Option TVal :=
  (ctx.find? (·.1 == name)).map (·.2)

def expand (ctx : Context) : TNode → String
  | TNode.TText s => s
  | TNode.TVar name =>
      match ctxGet ctx name with
      | some (TVal.Str s) => s
      | _ => ""
  | TNode.TLoop listName body =>
      match ctxGet ctx listName with
      | some (TVal.List items) =>
          match items.head? with
          | some itemCtx => expand (itemCtx ++ ctx) body
          | none => ""
      | _ => ""
  | TNode.TSeq nodes => nodes.foldl (init := "") fun acc n => acc ++ expand ctx n

def body : TNode := TNode.TSeq [TNode.TText "- ", TNode.TVar "x"]
def tmpl : TNode := TNode.TLoop "items" body
def ctx : Context := [("items", TVal.List [[("x", TVal.Str "a")], [("x", TVal.Str "b")]])]

#guard expand ctx tmpl == "- a- b"

hint

The loop only processes the first item in the list instead of all of them
items.head? returns only the first element (or none for empty)
Replace with items.foldl over all items, like the working expand function

Fix: Empty String Is Truthy

-- An empty string "" should be falsy, but this treats it as truthy. Fix it.
abbrev Context := List (String × TVal)

inductive TVal where | Str (s : String) | List (items : List Context)

inductive TNode where
  | TText (s : String) | TIf (name : String) (t e : TNode)

def ctxGet (ctx : Context) (name : String) : Option TVal :=
  (ctx.find? (·.1 == name)).map (·.2)

def expand (ctx : Context) : TNode → String
  | TNode.TText s => s
  | TNode.TIf varName thenNode elseNode =>
      match ctxGet ctx varName with
      | some (TVal.Str s) => expand ctx thenNode
      | _ => expand ctx elseNode

def tmpl : TNode := TNode.TIf "flag" (TNode.TText "ON") (TNode.TText "OFF")

#guard expand [("flag", TVal.Str "yes")] tmpl == "ON"
#guard expand [("flag", TVal.Str "")]    tmpl == "OFF"
#guard expand []                          tmpl == "OFF"

hint

An empty string "" should be treated as falsy (like Python)
The function currently treats every some value as truthy
Add a check: if s.isEmpty then ... else ...

Fix: Sequence Concatenation Order

-- reverse.foldl produces backward output. Fix it.
abbrev Context := List (String × TVal)

inductive TVal where | Str (s : String) | List (items : List Context)

inductive TNode where
  | TText (s : String) | TSeq (nodes : List TNode)

def expand (ctx : Context) : TNode → String
  | TNode.TText s => s
  | TNode.TSeq nodes => nodes.reverse.foldl (init := "") fun acc n => acc ++ expand ctx n

def tmpl : TNode :=
  TNode.TSeq [TNode.TText "A", TNode.TText "B", TNode.TText "C"]

#guard expand [] tmpl == "ABC"

hint

nodes.reverse.foldl reverses the list before folding, producing backward output
Remove .reverse to keep the original left-to-right order

Fix: Context Shadowing

-- Loop context should shadow outer context, but this puts outer first. Fix it.
abbrev Context := List (String × TVal)

inductive TVal where | Str (s : String) | List (items : List Context)

inductive TNode where
  | TText (s : String) | TVar (name : String)
  | TLoop (name : String) (body : TNode) | TSeq (nodes : List TNode)

def ctxGet (ctx : Context) (name : String) : Option TVal :=
  (ctx.find? (·.1 == name)).map (·.2)

def expand (ctx : Context) : TNode → String
  | TNode.TText s => s
  | TNode.TVar name =>
      match ctxGet ctx name with
      | some (TVal.Str s) => s
      | _ => ""
  | TNode.TLoop listName body =>
      match ctxGet ctx listName with
      | some (TVal.List items) =>
          items.foldl (init := "") fun acc itemCtx =>
            acc ++ expand (ctx ++ itemCtx) body
      | _ => ""
  | TNode.TSeq nodes => nodes.foldl (init := "") fun acc n => acc ++ expand ctx n

def tmpl : TNode :=
  TNode.TSeq [
    TNode.TText "outer: ",
    TNode.TVar "x",
    TNode.TText " | ",
    TNode.TLoop "items" (TNode.TVar "x")
  ]

-- Outer x is "outer", inner x is "a". The loop should print "a", not "outer".
def ctx : Context := [("x", TVal.Str "outer"), ("items", TVal.List [[("x", TVal.Str "a")]])]

#guard expand ctx tmpl == "outer: outer | a"

hint

In the loop body, the inner context should shadow outer variables
The code uses ctx ++ itemCtx which puts the outer context first
Swap to itemCtx ++ ctx so the loop variable takes precedence

Fix: Wrong Type in Lookup

-- ctxGet returns Option TVal, not Option String. Fix the type mismatch.
abbrev Context := List (String × TVal)

inductive TVal where | Str (s : String) | List (items : List Context)

def ctxGet (ctx : Context) (name : String) : Option TVal :=
  (ctx.find? (·.1 == name)).map (·.2)

def lookupString (ctx : Context) (name : String) : String :=
  match ctxGet ctx name with
  | some s => s
  | none => ""

#guard lookupString [("x", TVal.Str "hello")] "x" == "hello"
#guard lookupString [] "x" == ""

hint

ctxGet returns Option TVal, but the code tries to treat it as Option String
TVal is not String — you need to pattern-match and extract the TVal.Str s value
Add match and return "" when the variable has a different type or is missing

Write: Greeting Template

-- Build a TNode tree for the template "Hello, {{ name }}!" and test it
inductive TVal where
  | Str (s : String)
  | List (items : List (List (String × TVal)))

abbrev Context := List (String × TVal)

inductive TNode where
  | TText (s : String) | TVar (name : String) | TSeq (nodes : List TNode)

def ctxGet (ctx : Context) (name : String) : Option TVal :=
  (ctx.find? (·.1 == name)).map (·.2)

def expand (ctx : Context) : TNode → String
  | TNode.TText s => s
  | TNode.TVar name =>
      match ctxGet ctx name with
      | some (TVal.Str s) => s
      | _ => ""
  | TNode.TSeq nodes => nodes.foldl (init := "") fun acc n => acc ++ expand ctx n

def greetingTmpl : TNode :=
  TNode.TSeq []

#guard expand [("name", TVal.Str "World")] greetingTmpl == "Hello, World!"

hint

Build a TNode.TSeq with TNode.TText "Hello, ", TNode.TVar "name", and TNode.TText "!"
If name is missing, expand already returns "" for missing variables
The #guard expects "Hello, World!" with name="World"

Write: List Items

-- Build a template that renders a bulleted list from a "items" list
inductive TVal where
  | Str (s : String)
  | List (items : List (List (String × TVal)))

abbrev Context := List (String × TVal)

inductive TNode where
  | TText (s : String) | TVar (name : String)
  | TLoop (name : String) (body : TNode) | TSeq (nodes : List TNode)

def ctxGet (ctx : Context) (name : String) : Option TVal :=
  (ctx.find? (·.1 == name)).map (·.2)

def expand (ctx : Context) : TNode → String
  | TNode.TText s => s
  | TNode.TVar name =>
      match ctxGet ctx name with
      | some (TVal.Str s) => s
      | _ => ""
  | TNode.TLoop listName body =>
      match ctxGet ctx listName with
      | some (TVal.List items) =>
          items.foldl (init := "") fun acc itemCtx =>
            acc ++ expand (itemCtx ++ ctx) body
      | _ => ""
  | TNode.TSeq nodes => nodes.foldl (init := "") fun acc n => acc ++ expand ctx n

def listItemsTmpl : TNode :=
  TNode.TLoop "items" (TNode.TSeq [])

def ctx : Context := [
  ("items", TVal.List [
    [("item", TVal.Str "apples")],
    [("item", TVal.Str "bananas")]
  ])
]

#guard expand ctx listItemsTmpl == "* apples* bananas"

hint

Use TNode.TLoop with list name "items" and a body that wraps TNode.TVar "item" in "* " prefix
The body should be TNode.TSeq [TNode.TText "* ", TNode.TVar "item"]
Use TVal.List with each item being [("item", TVal.Str "...")]

Write: HTML Page

-- Build a template that renders a full HTML page with a title
inductive TVal where
  | Str (s : String)
  | List (items : List (List (String × TVal)))

abbrev Context := List (String × TVal)

inductive TNode where
  | TText (s : String) | TVar (name : String) | TSeq (nodes : List TNode)

def ctxGet (ctx : Context) (name : String) : Option TVal :=
  (ctx.find? (·.1 == name)).map (·.2)

def expand (ctx : Context) : TNode → String
  | TNode.TText s => s
  | TNode.TVar name =>
      match ctxGet ctx name with
      | some (TVal.Str s) => s
      | _ => ""
  | TNode.TSeq nodes => nodes.foldl (init := "") fun acc n => acc ++ expand ctx n

def htmlPageTmpl : TNode :=
  TNode.TSeq []

#guard expand [("title", TVal.Str "My Site")] htmlPageTmpl == "<html><body><h1>My Site</h1></body></html>"

hint

Build a full <html><body>...</body></html> structure using TNode.TSeq
Include a TNode.TVar "title" inside <h1> tags
The #guard checks for <html><body><h1>My Site</h1></body></html>

Write: Show/Hide Section

-- Use TIf to show or hide a section based on "show_section"
inductive TVal where
  | Str (s : String)
  | List (items : List (List (String × TVal)))

abbrev Context := List (String × TVal)

inductive TNode where
  | TText (s : String) | TIf (name : String) (t e : TNode)

def ctxGet (ctx : Context) (name : String) : Option TVal :=
  (ctx.find? (·.1 == name)).map (·.2)

def expand (ctx : Context) : TNode → String
  | TNode.TText s => s
  | TNode.TIf varName thenNode elseNode =>
      match ctxGet ctx varName with
      | some (TVal.Str s) => if s.isEmpty then expand ctx elseNode
                             else expand ctx thenNode
      | _ => expand ctx elseNode

def showHideTmpl : TNode :=
  TNode.TIf "show_section" (TNode.TText "Section content") (TNode.TText "")

#guard expand [("show_section", TVal.Str "yes")] showHideTmpl == "Section content"
#guard expand [("show_section", TVal.Str "")]    showHideTmpl == ""
#guard expand []                                  showHideTmpl == ""

hint

Use TNode.TIf to conditionally render the section
Check the "show_section" variable
When true, render "Section content"; when false, render ""

Write: Repeat N Times

-- Build a template that repeats a word N times using a loop
inductive TVal where
  | Str (s : String)
  | List (items : List (List (String × TVal)))

abbrev Context := List (String × TVal)

inductive TNode where
  | TText (s : String) | TVar (name : String)
  | TLoop (name : String) (body : TNode) | TSeq (nodes : List TNode)

def ctxGet (ctx : Context) (name : String) : Option TVal :=
  (ctx.find? (·.1 == name)).map (·.2)

def expand (ctx : Context) : TNode → String
  | TNode.TText s => s
  | TNode.TVar name =>
      match ctxGet ctx name with
      | some (TVal.Str s) => s
      | _ => ""
  | TNode.TLoop listName body =>
      match ctxGet ctx listName with
      | some (TVal.List items) =>
          items.foldl (init := "") fun acc itemCtx =>
            acc ++ expand (itemCtx ++ ctx) body
      | _ => ""
  | TNode.TSeq nodes => nodes.foldl (init := "") fun acc n => acc ++ expand ctx n

def repeatTmpl : TNode :=
  TNode.TLoop "times" (TNode.TVar "word")

def ctx : Context := [
  ("times", TVal.List (List.replicate 3 [("word", TVal.Str "go")]))
]

#guard expand ctx repeatTmpl == "gogogo"

hint

Create a context with a list of n identical items
Use List.replicate n ctx to create n copies of the same context
The loop body just references TNode.TVar "word"

Write: Join With Separator

-- Build a template that joins items with ", " but no trailing separator
inductive TVal where
  | Str (s : String)
  | List (items : List (List (String × TVal)))

abbrev Context := List (String × TVal)

inductive TNode where
  | TText (s : String) | TVar (name : String)
  | TLoop (name : String) (body : TNode) | TSeq (nodes : List TNode)

def ctxGet (ctx : Context) (name : String) : Option TVal :=
  (ctx.find? (·.1 == name)).map (·.2)

def expand (ctx : Context) : TNode → String
  | TNode.TText s => s
  | TNode.TVar name =>
      match ctxGet ctx name with
      | some (TVal.Str s) => s
      | _ => ""
  | TNode.TLoop listName body =>
      match ctxGet ctx listName with
      | some (TVal.List items) =>
          items.foldl (init := "") fun acc itemCtx =>
            acc ++ expand (itemCtx ++ ctx) body
      | _ => ""
  | TNode.TSeq nodes => nodes.foldl (init := "") fun acc n => acc ++ expand ctx n

def joinTmpl : TNode :=
  TNode.TLoop "items" (TNode.TSeq [
    TNode.TVar "x",
    TNode.TText ", "
  ])

def ctx : Context := [
  ("items", TVal.List [
    [("x", TVal.Str "a")],
    [("x", TVal.Str "b")],
    [("x", TVal.Str "c")]
  ])
]

def renderWithJoin (ctx : Context) (tmpl : TNode) : String :=
  let raw := expand ctx tmpl
  if raw.isEmpty then raw else raw.dropRight 2

#guard renderWithJoin ctx joinTmpl == "a, b, c"

hint

Expand the loop body to produce item ++ ", " for each item
Handle the trailing separator: either check if it's the last item, or trim after
String.dropRight 2 can remove the trailing ", " after expansion
Or use items.foldl directly with index awareness