generic.disp

// generic.disp: the cell-derived generics. One fold/recursor/traversal/functorial-map for
// every inductive, read straight off the cells with no per-type code: fold_value (the
// catamorphism), rec_value (the dependent recursor, via elim) with the kernel recursors
// nat_rec/bool_rec/ord_rec as its annotated instances, children (traversal), and
// fmap/bimap/fmap_n (positional maps over Param markers) with their record-side duals
// key_over/fmap_rec/bimap_rec.

// Hermetic (MODULES.md): prelude + raw earlier siblings; givens for forward types.
open use raw "../prelude.disp" {}
open use raw "cut.disp" {}
open use raw "engine.disp" {}
open use raw "cells.disp" {}
open use raw "base.disp" {}
open use raw "positive.disp" {}

open given { Type : Type }

// fold_value (the cell-derived catamorphism — the SHAPE FUNCTOR read straight off the cells). For an
// inj-tagged value `v = inj tag (a0,…)`: look up the variant's cell telescope, extract each arg by its
// stored accessor, RECURSE the fold at `rec` cells, apply the algebra case `alg.tag`. ONE generic fold for
// every inductive; the dependent recursor, fmap, and (once §13) cubical transport are this fold with other algebras.
// apply_all: saturate a curried case with the positional (folded) args.
let apply_all := fix ({self, fn, args} -> if (is_fork args) then (self (fn (pair_fst args)) (pair_snd args)) else fn)
// collect_args: walk the cell telescope, extracting each arg (`acc payload`) and folding it at rec cells
// via `fold alg raw`. GOTCHA: `fold`/`alg` are threaded SEPARATELY (never pre-formed as `fold alg` — that
// closed redex unfolds forever at compile time; `fold alg raw` forms only at the runtime rec site).
let collect_args := fix ({self, cells, payload, fold, alg} ->
  if (is_fork cells) then {
    let cell := pair_fst cells
    let raw := ((type_meta cell).acc) payload
    let x := if (is_self_rec cell) then (fold alg raw) else raw
    cons x (self ((pair_snd cells) t) payload fold alg)
  } else nil)
// fold_value_via view: first DECODE v via `view` (the from-iso for SHAPE-encoded Nat/List/Ord), then fold
// the inj-tagged form — so ONE fold covers inj-tagged AND shape-encoded. `fold_value_via` takes the view
// explicitly; `fold_value` below AUTO-READS it from the `functor` iso (iso_id's view = `Ok` passes through).
fold_value_via := {view} -> fix ({fold, T, alg, v} -> {
  let dec := (match (view v) { Ok tg => tg; Err _ => v })
  let cells := (match (lookup_arm (type_meta T).recognizer_params (pair_fst dec)) { Ok a => (pos_tele a); Err _ => t })
  apply_all (field alg (pair_fst dec)) (collect_args cells (pair_snd dec) (wait fold T) alg)
})
// fold_value: like fold_value_via but AUTO-READS the decode `view` from the type's iso (functor),
// so `fold_value T` works on shape-encoded (Nat/List/Ord) AND inj-tagged (iso_id view = Ok) alike.
fold_value := {T} -> fold_value_via (pair_fst (type_meta T).functor) T

// rec_value (the dependent RECURSOR derived from cells — one recursor for ANY inductive).
// Unlike fold_value, a recursor case gets the RAW args AND the IH per recursive position — the §4 case-type
// `Π args. (IH per rec) → P (c args)`. Routes through `elim`, so a NEUTRAL target becomes a stuck elimination
// at `motive self` (usable under a Pi binder). all_args = raw args; ih_args = elim-recursion at each rec cell.
// Decodes the target through the functor view first (like fold_value), so shape-encoded types
// (Nat/Bool/Ord/List) dispatch by variant tag too.
let all_args := fix ({self, cells, payload} ->
  if (is_fork cells) then (cons (((type_meta (pair_fst cells)).acc) payload) (self ((pair_snd cells) t) payload)) else nil)
let ih_args := fix ({self, cells, payload, rec} ->
  if (is_fork cells) then {
    let cell := pair_fst cells
    let rest := self ((pair_snd cells) t) payload rec
    if (is_self_rec cell) then (cons (rec (((type_meta cell).acc) payload)) rest) else rest
  } else nil)
let rec_dispatcher := {T} -> fix ({self, motive, cases, v} -> {
  let dec := match ((pair_fst (type_meta T).functor) v) { Ok tg => tg; Err _ => v }
  let cells := (match (lookup_arm (type_meta T).recognizer_params (pair_fst dec)) { Ok a => (pos_tele a); Err _ => t })
  apply_all (field cases (pair_fst dec)) (list_cat (all_args cells (pair_snd dec)) (ih_args cells (pair_snd dec) (elim self motive cases)))
})
rec_value := {T, motive, cases, target} -> elim (rec_dispatcher T) motive cases target

// The kernel recursors are rec_value at the kernel inductives: one-line instances carrying the
// honest dependent-recursor annotations (rec_value itself stays unannotated; its type depends
// on the target type's declaration, see derive_case_telescope).
nat_rec : {P : Nat -> Type} -> P zero -> ({n : Nat} -> P n -> P (succ n)) -> {n : Nat} -> P n := {motive, base, step, target} -> rec_value Nat motive { zero := base; succ := step } target
bool_rec : {P : Bool -> Type} -> P true -> P false -> {b : Bool} -> P b := {motive, ct, cf, target} -> rec_value Bool motive { true := ct; false := cf } target
ord_rec : {P : Ord -> Type} -> P zero_ord -> ({a : Ord} -> {b : Ord} -> P a -> P b -> P (omega_plus a b)) -> {o : Ord} -> P o := {motive, case_z, case_op, target} -> rec_value Ord motive { zero_ord := case_z; omega_plus := case_op } target

// case_value (the ONE-LEVEL case eliminator — match as polarized application). The same
// dispatch as rec_value (functor-view decode, arm lookup, raw args by accessor) with NO
// recursion — and CASE-SHAPED arms: an arm takes exactly its constructor's raw args
// (`succ := {k} -> k`), no phantom-IH binders. The concrete face applies raw args only;
// the NEUTRAL face pads each arm to recursor shape at runtime (pad_cases below) and
// routes through the SAME gated respond as rec_value — one gate, two eliminators, and
// the padding runs only on the lazy neutral branch. Use it where a branch needs the raw
// sub-structure without paying the recursor's eager IH (typed pred/is_zero drop
// O(n) -> O(1)); raw `match` stays the substrate cut for raw sums and dispatcher
// internals (it fails closed on a hyp — pinned in case_value.test.disp along with both
// of case_value's faces).
let case_dispatcher := {T, motive, cases, v} -> {
  let dec := match ((pair_fst (type_meta T).functor) v) { Ok tg => tg; Err _ => v }
  let cells := (match (lookup_arm (type_meta T).recognizer_params (pair_fst dec)) { Ok a => (pos_tele a); Err _ => t })
  apply_all (field cases (pair_fst dec)) (all_args cells (pair_snd dec))
}
// pad_cases: rebuild the case record over T's variant list (canonical order), each arm
// padded to recursor shape for the gate — consume the raw args, then absorb one ignored
// IH per Rec cell via `list_const` (fork(leaf, v): applied to the minted IH it answers v
// by the K rule, no triage, so the absorber certifies and keeps the certificate honest).
// A missing arm projects junk and the gate rejects (self-enforcing totality).
let absorb_recs := fix ({self, cells, v} ->
  if (is_fork cells) then {
    let rest := self ((pair_snd cells) t) v
    if (is_self_rec (pair_fst cells)) then (list_const rest) else rest
  } else v)
let pad_arm := fix ({self, cells, all, f} ->
  if (is_fork cells) then ({x} -> self ((pair_snd cells) t) all (f x)) else (absorb_recs all f))
let arm_names := fix ({self, vs} -> if (is_fork vs) then (cons (pair_fst (pair_fst vs)) (self (pair_snd vs))) else nil)
let pad_go := fix ({self, vs, cases} ->
  if (is_fork vs) then {
    let cells := pos_tele (pair_snd (pair_fst vs))
    cons (list_const (pad_arm cells cells (field cases (pair_fst (pair_fst vs))))) (self (pair_snd vs) cases)
  } else nil)
let pad_cases := {T, cases} -> make_record (arm_names ((type_meta T).recognizer_params)) (pad_go ((type_meta T).recognizer_params) cases)
case_value := {T, motive, cases, target} ->
  select_lazy
    ({_} -> target { motive := motive; cases := pad_cases T cases })
    ({_} -> case_dispatcher T motive cases target)
    (is_neutral target)

// children (generic TRAVERSAL): the immediate recursive sub-values of `v`, read off the cells (the
// `is_rec_cell` positions, not folded) — raw material for size/depth over ANY inductive, no per-type code.
let rec_children := fix ({self, cells, payload} ->
  if (is_fork cells) then {
    let cell := pair_fst cells
    let rest := self ((pair_snd cells) t) payload
    if (is_self_rec cell) then (cons (((type_meta cell).acc) payload) rest) else rest
  } else nil)
children := {T, v} -> rec_children (match (lookup_arm (type_meta T).recognizer_params (pair_fst v)) { Ok a => (pos_tele a); Err _ => t }) (pair_snd v)

// ── fmap / fmap_n — the cell-derived functorial map (CELL_OPTICS §3).
// `walk_map` (sibling of `tele_walk`) walks an inj-tagged value's argspec and REBUILDS via the optic's `over`
// (`slot_over`, position-wise): maps a `Param i` arg with `fns i`, recurses at a `Rec` arg, leaves the
// rest. `fmap`/`bimap` are 1-/2-param specializations; `fmap_n` view-decodes shape-encoded types via the
// `functor` iso (List/Nat/Ord work too). Deferred: nested `RecUnder F` (F≠Id, needs F's map).
let slot_over := fix ({self, depth, is_last, f, p} ->
  if (tree_eq depth zero)
    then (if is_last then (f p) else (pair (f (pair_fst p)) (pair_snd p)))
    else (pair (pair_fst p) (self (nat_pred depth) is_last f (pair_snd p))))
let walk_map_args := fix ({self, nm, fns, argspec, payload, depth} ->
  if (is_fork argspec) then {
    let marker := pair_fst argspec
    let is_last := is_leaf (pair_snd argspec)
    let trans := (if (is_param_marker marker) then (fns (pair_snd marker)) else (if (and (is_recunder_marker marker) (tree_eq (pair_snd marker) Id)) then (nm fns) else Id))
    self nm fns (pair_snd argspec) (slot_over depth is_last trans payload) (succ depth)
  } else payload)
// fmap_n: map a value via the type's iso (functor) — decode (view) -> map the inj form (slot_over,
// recursing at Rec cells) -> re-encode. Identity iso = plain inj map; a real iso makes the SAME `fmap`
// work on shape values. `fmap_step` splits out the map+encode so the match arm ends in the arm-bound `tg`.
let fmap_step := {self, T, fns, encode, tg} ->
  encode (inj (pair_fst tg) (walk_map_args (wait self T) fns (match (lookup_arm (type_meta T).recognizer_params (pair_fst tg)) { Ok a => a; Err _ => t }) (pair_snd tg) zero))
fmap_n := fix ({self, T, fns, v} -> {
  let iso := (type_meta T).functor
  match ((pair_fst iso) v) {
    Ok tg => (fmap_step self T fns (pair_snd iso) tg)
    Err _ => v
  }
})
fmap  := {T, f, v}    -> fmap_n T ({i} -> f) v
bimap := {T, f, g, v} -> fmap_n T ({i} -> if (tree_eq i zero) then f else g) v

// key.over (CELL_OPTICS, the NAMED side): `key name = slot (index_of names name)` — the §2.6 cut run
// BACKWARD, so `fmap`/`bimap` work over records (compose key.overs) by the same engine as positional slot.over.
key_over := {name, f, record} -> { // rebuild the §2.6 record with field `name` mapped (stored values are list_const-wrapped)
  let np := type_meta record
  make_record (pair_fst np) (list_update (list_index_of (pair_fst np) name) ({w} -> list_const (f (w t))) (pair_snd np))
}
// walk_map over a record: map each `Param i` field via key.over (compose). fmap_rec/bimap_rec derive.
let walk_map_fields := fix ({self, fns, fields, record} ->
  if (is_fork fields) then {
    let arm := pair_fst fields
    let record2 := if (is_param_marker (pair_snd arm)) then (key_over (pair_fst arm) (fns (pair_snd (pair_snd arm))) record) else record
    self fns (pair_snd fields) record2
  } else record)
fmap_rec  := {T, fns, r}    -> walk_map_fields fns (type_meta T).recognizer_params r
bimap_rec := {T, f, g, r}   -> fmap_rec T ({i} -> if (tree_eq i zero) then f else g) r