4.3. Pure Constructs🔗

open Iris.HeapLang

namespace HeapLangExamples

HeapLang has native support for integers and booleans. With these, we can do basic arithmetic and control flow. Note that values in HeapLang are prefixed by a #.

def arith : Exp := hl(#1 + #2 * #3)

The expected result of evaluating arith is 7.

def booleans : Exp := hl((#1 + #2 * #3 = #7) && #true || (#true = #false))

The expected result is #true.

-- TODO (upstream — iris-lean): use the unit literal here once the
-- `hl` DSL gains a sugared form for `Val.lit BaseLit.unit` (Rocq: `#()`).
def if_then_else : Exp := hl(if #true then #1 else #0)

In the Rocq version of this example, the consequent is the unit value #(); iris-lean does not yet have a sugared spelling for the unit literal, so we use an integer here instead.

HeapLang supports let expressions. Technically, let expressions are not native to HeapLang — they are sugar for application of a lambda to its argument. Note that variables in HeapLang are strings; in the Lean DSL, you write them as plain identifiers, and they elaborate to Exp.var "x".

def lets : Exp := hl(
  let a := #4;
  let b := #2;
  a + b)

HeapLang has native support for pairs, with tuples being notation for nested pairs.

def pairs : Exp := hl(
  let p := (#40, #1 + #1);
  fst(p) + snd(p))

def tuples : Exp := hl(
  let t1 := (#1, #2, #3, #4);
  let t2 := (((#1, #2), #3), #4);
  snd(fst(fst(t1))) = snd(fst(fst(t2))))

We can also do pattern matching using sums. A common use case of sums is the option construction.

def sums : Exp := hl(
  let r := injr(#1);
  match r with
  | injl(_) => #0
  | injr(n) => n + #1
  )

def option : Exp := hl(
  let r := some(#1);
  match r with
  | none() => #0
  | some(n) => n + #1
  )

Finally, we have lambda abstractions and recursive functions. As with let expressions, lambda abstractions are also a derived construct — they are recursive functions that do not recurse. In HeapLang, functions are first-class citizens, which gives support for higher-order functions.

def lambda : Exp :=
  hl(let add5 := (λ x, x + #5);
     let double := (λ x, x * #2);
     let compose := (λ f g, λ x, g (f x));
     compose add5 double #5)

def recursion : Exp :=
  hl(let fac := (rec f n := if n = #0 then #1 else n * f (n - #1));
     (fac #4, fac #5))