happy-match-modal.rzk

#lang rzk-1

-- Exercise standalone diagnostics independently of the safe-mode bundle.
#set-option "rstt-safe" = "off"

-- A modal match checks the scrutinee under its modality. Every constructor
-- argument is then bound under the composition of that modality and the
-- argument's own modality: Flat ∘ Id = Flat and Flat ∘ Op = Flat here.
#data ModalMatch := mm (plain : 2) (op :_op 2)

#define modal-match-flat
  (f :_b (i : 2) -> (j : 2) -> Unit)
  (x :_b ModalMatch)
  : _b Unit
  := match _b x
       (mm plain op => mod _b (f plain op))

-- The modal spelling also supports an explicit motive.
#define modal-match-flat-into
  (f :_b (i : 2) -> (j : 2) -> Unit)
  (x :_b ModalMatch)
  : _b Unit
  := match _b x into (\ (_ :_b ModalMatch) -> _b Unit)
       (mm plain op => mod _b (f plain op))

#data Tagged : Unit -> U := tagged : Tagged unit

#define modal-match-indexed-motive
  (x :_b Tagged unit)
  : _b Unit
  := match _b x into (\ (i :_b Unit) (_ :_b Tagged i) -> _b Unit)
       (tagged => mod _b unit)

-- Composition is ordered: Op · Op = Id, so an op field of a value matched
-- under Op becomes available in the plain context.
#data OpField := op-field (point :_op 2)

#define modal-match-op-op
  (f : (i : 2) -> Unit)
  (x :_op OpField)
  : Unit
  := match _op x
       (op-field point => f point)

#data Nat := zero | suc (pred : Nat)

#check ind-Nat
  : (C : Nat -> U)
  -> C zero
  -> ((pred : Nat) -> (ih : C pred) -> C (suc pred))
  -> (n : Nat)
  -> C n
#check rec-Nat
  : (C : U) -> C -> ((pred : Nat) -> C -> C) -> Nat -> C
#check ind-op-Nat
  : (C : (n :_op Nat) -> U)
  -> C zero
  -> ((pred :_op Nat) -> (ih : C pred) -> C (suc pred))
  -> (n :_op Nat)
  -> C n
#check rec-op-Nat
  : (C : U) -> C -> ((pred :_op Nat) -> C -> C) -> (n :_op Nat) -> C
#check ind-b-Nat
  : (C : (n :_b Nat) -> U)
  -> C zero
  -> ((pred :_b Nat) -> (ih : C pred) -> C (suc pred))
  -> (n :_b Nat)
  -> C n
#check rec-b-Nat
  : (C : U) -> C -> ((pred :_b Nat) -> C -> C) -> (n :_b Nat) -> C

#define modal-predecessor-generated
  (n :_b Nat)
  : _b Nat
  := rec-b-Nat (_b Nat) (mod _b zero)
       (\ pred _ -> mod _b pred) n

#define modal-match-recursive
  (x :_b Nat)
  : Unit
  := match _b x
       ( zero => unit
       | suc pred ih => ih)