Encapp.AppGen

1,060 lines: the reflected app types, the Lean interpreter the JS runtime mirrors, the JSON emission, and the three platform emitters.

ReflApp

structure ReflApp (β : Type) where
  init     : Doc
  pages    : List (String × RView)     -- path → view
  handlers : List RHandler
  gates    : List (String × String) := []
  binding  : Option β := none
  deriving Inhabited

A fully reflected, codegen-ready app. β is the host binding type; ReflApp Unit expects nothing of its host.

See Routing and gates for pages and gates.

HostBinding

class HostBinding (β : Type) where
  toJson : β → String
 
instance : HostBinding Unit where
  toJson _ := "null"

Opaque by design. Encapp knows a binding can be serialized and nothing else — every protocol concept lives in the layer above. See Host bindings.

Payload

inductive Payload where
  | atom : Atom → Payload
  | row  : Row → Payload

RHandler and Eff

structure RHandler where
  tag  : String
  effs : List Eff

The Eff constructors are documented with their semantics in Effects. Summary:

Domain-free — setConst, setInput, setFromRow, setFromScalar, appendFromScalars, appendFromScalarsIfAbsent, appendFromRow, removeWhereField, lookupRoute

Messaging-shaped — pushDraft, pushInput, pushInputWith, setConvId, pushConvMessage, routeIfHex64

Domain-specific — likeRow

RView

The reflected view vocabulary, documented constructor by constructor in Views. Groups:

• minimal — text, scalar, rowField, input, button, list, col
• styled — raw, el, elAttr, img, styled, btn, click, rowSelect, inp, rowFieldOr
• lists — listWhere, listDistinct, listOrEmpty
• conditionals — cond, condEq, condField, condFieldEqScalar

The interpreter

def applyEff (payload : Payload) (d : Doc) : Eff → Doc
 
def reflStep (hs : List RHandler) (tag : String) (payload : Payload) (d : Doc) : Doc :=
  match hs.find? (fun h => h.tag == tag) with
  | some h => h.effs.foldl (fun d e => applyEff payload d e) d
  | none   => d
 
def reflRun (hs : List RHandler) (steps : List (String × Payload)) (init : Doc) : Doc

reflStep is the Lean spec; the emitted appCoreJs is its operational mirror. An unknown tag is a no-op rather than an error, which keeps the function total.

reflRun folds a step list — it is what Workflow.run uses, so the interpreter that runs the app is literally the interpreter that proves the test.

postRow

def postRow (d : Doc) : Row :=
  let id := short16 (asStr (d.getScalar "identity"))
  [ ("from", .str id), ("body", d.getScalar "draft"), ("media", .str id),
    ("trailing", .str "now"), ("outgoing", .bool true) ]

The row a "post" produces from the current draft. It is a framework-level definition with a chat shape baked in — see the generality boundary.

JSON emission

The runtimes

appCoreJs being one definition shared by both targets is what makes test/native-core-identity.mjs able to assert byte-identity.

The emitters

def AppGen.emit       [HostBinding β] (chrome : DocChrome) (a : ReflApp β) : String
def AppGen.emitNative [HostBinding β] (a : ReflApp β)
                      (baseText baseInput baseButton : String := "") : String
def AppGen.emitDesktopMain        (c : DesktopChrome) : String
def AppGen.emitDesktopPreload     : String
def AppGen.emitDesktopPackageJson (c : DesktopChrome) : String

Chrome is data in both places:

structure DocChrome where
  title : String
  head  : String := ""
  css   : String
 
structure DesktopChrome where
  name   : String
  title  : String
  width  : Nat := 390
  height : Nat := 844

One emitter serves every app; presentation is the app's own value rather than a per-app emitter function. DocChrome.light name is the default theme used by the examples.

See Web, Native and Desktop.