Skip to content

Lean2Js.Renderable

Imports 3

That the compiler only builds modules the reader takes back #

That the module compileProgram builds is one the reader in Parse takes back.

Roundtrip proves parseModule (render m) = some m for every m its RenderableModule accepts. What that leaves open is whether the compiler ever builds a module outside it. It does not, and this file is the argument: every name the compiler writes went through validateIdent or starts with the reserved prefix, every operator it writes is one of a handful it spells itself, and the doc comment is built from names and type renderings, none of which contain a *.

No `*` reaches the doc comment #

A doc comment goes into /** */ unescaped, so Renderable asks it not to spell */. The doc is built from names and type renderings, and neither can contain a * at all, which is the stronger and much shorter thing to prove.

def

Lean2Js.Compile.noStar

(s : String) :

Equations

Lean2Js.Compile.noStar s = s.toList.all fun (x : Char) => x != '*'

Instances For

Used by

theorem

Lean2Js.Compile.noStar_append

[Core.Discriminators] {s t : String} (hs : noStar s = true) (ht : noStar t = true) :

noStar (s ++ t) = true

Used by

theorem

Lean2Js.Compile.noCommentClose_of_all_ne_star

[Core.Discriminators] (cs : List Char) :

(cs.all fun (x : Char) => x != '*') = true → Parse.noCommentClose cs = true

Used by

theorem

Lean2Js.Compile.noCommentClose_of_noStar

[Core.Discriminators] {s : String} (h : noStar s = true) :

Parse.noCommentClose s.toList = true

Used by

theorem

Lean2Js.Compile.ne_star_of_isIdentPart

[Core.Discriminators] {c : Char} (h : isIdentPart c = true) :

(c != '*') = true

Used by

theorem

Lean2Js.Compile.noStar_of_okName

[Core.Discriminators] {s : String} (h : okName s = true) :

noStar s = true

Used by

Type renderings carry no `*` #

A type renders as keywords, punctuation and the names of the types it mentions. wfTy has already found every one of those names in p.types, and validateType has already put every one of those through validateIdent, so the whole rendering is made of identifier characters and the separators between them.

The scope is empty wherever a declaration's types are checked, so Ty.var never survives to be rendered and a type parameter's name never has to be accounted for.

def

Lean2Js.Compile.TypeNamesOk

(p : Core.Program) :

Every type the program declares is named by an identifier.

Equations

Lean2Js.Compile.TypeNamesOk p = ∀ (t : Lean2Js.Core.TypeDef), t ∈ p.types → Lean2Js.okName t.name = true

Instances For

Used by

theorem

Lean2Js.Compile.typeNamesOk_of_validated

[Core.Discriminators] {p : Core.Program} (ts : List Core.TypeDef) :

ts.forM (validateType p) = Except.ok () → ∀ (t : Core.TypeDef), t ∈ ts → okName t.name = true

Used by

theorem

Lean2Js.Compile.okName_of_findType

[Core.Discriminators] {p : Core.Program} (hn : TypeNamesOk p) {n : String} {t : Core.TypeDef} (h : p.findType? n = some t) :

okName n = true

Used by

theorem

Lean2Js.Compile.noStar_render

[Core.Discriminators] {p : Core.Program} (hn : TypeNamesOk p) (ty : Core.Ty) :

wfTy p [] ty = Except.ok () → noStar ty.render = true

Used by

theorem

Lean2Js.Compile.noStar_renderArgs

[Core.Discriminators] {p : Core.Program} (hn : TypeNamesOk p) (tys : List Core.Ty) :

wfTyArgs p [] tys = Except.ok () → noStar (Core.Ty.renderArgs tys) = true

Used by

theorem

Lean2Js.Compile.noStar_renderParamsRest

[Core.Discriminators] {p : Core.Program} (hn : TypeNamesOk p) (tys : List Core.Ty) :

tys.forM (wfTy p []) = Except.ok () → noStar (Core.Ty.renderParamsRest tys) = true

Used by

theorem

Lean2Js.Compile.noStar_renderParams

[Core.Discriminators] {p : Core.Program} (hn : TypeNamesOk p) (tys : List Core.Ty) :

tys.forM (wfTy p []) = Except.ok () → noStar (Core.Ty.renderParams tys) = true

Used by

theorem

Lean2Js.Compile.noStar_render_of_wfParamTy

[Core.Discriminators] {p : Core.Program} (hn : TypeNamesOk p) (ty : Core.Ty) :

wfParamTy p ty = Except.ok () → noStar ty.render = true

Used by

theorem

Lean2Js.Compile.noStar_declSigRest

[Core.Discriminators] {p : Core.Program} (hn : TypeNamesOk p) (params : List Core.Param) :

(params.forM fun (param : Core.Param) => validateIdent "parameter" param.name) = Except.ok () → (params.forM fun (param : Core.Param) => wfParamTy p param.ty) = Except.ok () → noStar (declSigRest params) = true

Used by

theorem

Lean2Js.Compile.noStar_declSig

[Core.Discriminators] {p : Core.Program} (hn : TypeNamesOk p) (params : List Core.Param) :

(params.forM fun (param : Core.Param) => validateIdent "parameter" param.name) = Except.ok () → (params.forM fun (param : Core.Param) => wfParamTy p param.ty) = Except.ok () → noStar (declSig params) = true

Used by

Names the compiler writes #

Renderable asks a name to be an identifier, and a name in callee position to be none of the ten the reader gives a meaning of its own. A user's name went through validateIdent, which rejects both the __ prefix and the JavaScript keywords, and those two rejections between them cover all ten.

theorem

Lean2Js.Compile.okCallee_of_validateIdent

[Core.Discriminators] {kind name : String} {u : Unit} (h : validateIdent kind name = Except.ok u) :

Parse.okCallee name = true

Used by

theorem

Lean2Js.Compile.okCallee_bodyName

[Core.Discriminators] {name : String} (h : okName name = true) :

Parse.okCallee (bodyName name) = true

The name a declaration's body is compiled under is a callee the reader takes back: it is spelled as an identifier, and none of the names the reader gives a meaning of its own carries _ where the body prefix does.

Used by

What the compiler is holding while it builds an expression #

The names in scope and the names of the declarations are the only two places a compiled expression can pick a name up from that is not one the compiler spells itself. Both went through validateIdent.

def

Lean2Js.Compile.CtxOk

(ctx : Ctx) :

Equations

Lean2Js.Compile.CtxOk ctx = ∀ (x : String × Lean2Js.Core.Ty), x ∈ ctx → Lean2Js.Parse.okCallee x.fst = true

Instances For

Used by

def

Lean2Js.Compile.DeclNamesOk

(p : Core.Program) :

Equations

Lean2Js.Compile.DeclNamesOk p = ∀ (d : Lean2Js.Core.Decl), d ∈ p.decls → Lean2Js.Parse.okCallee d.name = true

Instances For

Used by

def

Lean2Js.Compile.FieldNamesOk

(p : Core.Program) :

Field names reach the generated code through .field and through the paths a pattern reads, so a match and a projection both need them to be identifiers.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Compile.ArmOk

(a : Arm) :

One lowered match arm the reader can take back: the tests it runs, the names it binds, the paths it reads them from and the body under them.

Equations

Lean2Js.Compile.ArmOk a = (Lean2Js.Parse.RenderableList a.tests && a.names.all Lean2Js.okName && Lean2Js.Parse.RenderableList a.paths && Lean2Js.Parse.RenderableExpr a.body)

Instances For

Used by

theorem

Lean2Js.Compile.renderableList_append

[Core.Discriminators] (xs ys : List Js.Expr) :

Parse.RenderableList xs = true → Parse.RenderableList ys = true → Parse.RenderableList (xs ++ ys) = true

Used by

theorem

Lean2Js.Compile.renderableList_nil

[Core.Discriminators] :

Parse.RenderableList [] = true

Used by

theorem

Lean2Js.Compile.renderablePairs_nil

[Core.Discriminators] :

Parse.RenderablePairs [] = true

Used by

theorem

Lean2Js.Compile.renderableList_of_all

[Core.Discriminators] (es : List Js.Expr) :

es.all Parse.RenderableExpr = true → Parse.RenderableList es = true

Used by

theorem

Lean2Js.Compile.renderablePairs_zip

[Core.Discriminators] (ns : List String) (es : List Js.Expr) :

Parse.RenderableList es = true → Parse.RenderablePairs (ns.zip es) = true

Used by

theorem

Lean2Js.Compile.renderable_objOf

[Core.Discriminators] (ctor : String) (fields : List (String × Js.Expr)) (h : Parse.RenderablePairs fields = true) :

Parse.RenderableExpr (objOf ctor fields) = true

Used by

The lowered `match` #

chain conjoins an arm's tests with && and nests the arms into conditionals, and apply wraps an arm's body in an arrow when it binds anything. Both build only shapes the reader has.

theorem

Lean2Js.Compile.renderable_foldl_and

[Core.Discriminators] (ts : List Js.Expr) (t : Js.Expr) :

Parse.RenderableExpr t = true → Parse.RenderableList ts = true → Parse.RenderableExpr (List.foldl (Js.Expr.binary "&&") t ts) = true

Used by

theorem

Lean2Js.Compile.renderable_apply

[Core.Discriminators] {a : Arm} (h : ArmOk a = true) :

Parse.RenderableExpr (compileExpr.apply a) = true

Used by

theorem

Lean2Js.Compile.renderable_chain

[Core.Discriminators] (arms : List Arm) :

arms.all ArmOk = true → Parse.RenderableExpr (compileExpr.chain arms) = true

Used by

Patterns #

A pattern lowers to tests over paths into the scrutinee. The paths are built by reading fields, so the field names a signature reports have to be identifiers; the declared ones went through validateType and the built-in ones are value and error.

theorem

Lean2Js.Compile.okName_of_signature

[Core.Discriminators] {p : Core.Program} (hf : FieldNamesOk p) (ty : Core.Ty) (heads : List (Head × List (String × Core.Ty))) :

signature p.types ty = some heads → ∀ (hd : Head × List (String × Core.Ty)), hd ∈ heads → ∀ (f : String × Core.Ty), f ∈ hd.snd → okName f.fst = true

Used by

def

Lean2Js.Compile.BindsOk

(binds : List (String × Js.Expr × Core.Ty)) :

What a pattern's bindings have to be for the arm built from them to be readable back: a name the reader can read, bound to a path it can read.

Equations

Lean2Js.Compile.BindsOk binds = binds.all fun (b : String × Lean2Js.Js.Expr × Lean2Js.Core.Ty) => Lean2Js.Parse.okCallee b.fst && Lean2Js.Parse.RenderableExpr b.snd.fst

Instances For

Used by

theorem

Lean2Js.Compile.renderable_litJs

[Core.Discriminators] {ty : Core.Ty} {l : Core.Lit} {j : Js.Expr} (h : litJs ty l = Except.ok j) :

Parse.RenderableExpr j = true

Used by

theorem

Lean2Js.Compile.renderable_patParts

[Core.Discriminators] {p : Core.Program} (hfn : FieldNamesOk p) :

(∀ (ty : Core.Ty) (path : Js.Expr) (pat : Core.Pat), Parse.RenderableExpr path = true → ∀ (tests : List Js.Expr) (binds : List (String × Js.Expr × Core.Ty)), patParts p.types ty path pat = Except.ok (tests, binds) → Parse.RenderableList tests = true ∧ BindsOk binds = true) ∧ ∀ (tys : List Core.Ty) (paths : List Js.Expr) (pats : List Core.Pat), paths.all Parse.RenderableExpr = true → ∀ (tests : List Js.Expr) (binds : List (String × Js.Expr × Core.Ty)), patPartsList p.types tys paths pats = Except.ok (tests, binds) → Parse.RenderableList tests = true ∧ BindsOk binds = true

Used by

Building readable expressions #

One lemma per shape the compiler builds, so that the case analysis over compileExpr reads as the shape it emits rather than as an unfolding of RenderableExpr.

theorem

Lean2Js.Compile.renderableList_cons

[Core.Discriminators] {e : Js.Expr} {es : List Js.Expr} (he : Parse.RenderableExpr e = true) (hes : Parse.RenderableList es = true) :

Parse.RenderableList (e :: es) = true

Used by

theorem

Lean2Js.Compile.renderable_num

[Core.Discriminators] (i : Int) :

Parse.RenderableExpr (Js.Expr.num i) = true

Used by

theorem

Lean2Js.Compile.renderable_bigLit

[Core.Discriminators] (i : Int) :

Parse.RenderableExpr (Js.Expr.bigLit i) = true

Used by

theorem

Lean2Js.Compile.renderable_str

[Core.Discriminators] (s : String) :

Parse.RenderableExpr (Js.Expr.str s) = true

Used by

theorem

Lean2Js.Compile.renderable_bool

[Core.Discriminators] (b : Bool) :

Parse.RenderableExpr (Js.Expr.bool b) = true

Used by

theorem

Lean2Js.Compile.renderable_ident

[Core.Discriminators] {n : String} (h : Parse.okCallee n = true) :

Parse.RenderableExpr (Js.Expr.ident n) = true

Used by

theorem

Lean2Js.Compile.renderable_unary

[Core.Discriminators] {op : String} {e : Js.Expr} (ho : (op == "!" || op == "-") = true) (he : Parse.RenderableExpr e = true) :

Parse.RenderableExpr (Js.Expr.unary op e) = true

Used by

theorem

Lean2Js.Compile.renderable_binary

[Core.Discriminators] {op : String} {l r : Js.Expr} (ho : Parse.okOp op = true) (hl : Parse.RenderableExpr l = true) (hr : Parse.RenderableExpr r = true) :

Parse.RenderableExpr (Js.Expr.binary op l r) = true

Used by

theorem

Lean2Js.Compile.renderable_cond

[Core.Discriminators] {c t e : Js.Expr} (hc : Parse.RenderableExpr c = true) (ht : Parse.RenderableExpr t = true) (he : Parse.RenderableExpr e = true) :

Parse.RenderableExpr (c.cond t e) = true

Used by

theorem

Lean2Js.Compile.renderable_call

[Core.Discriminators] {c : String} {as : List Js.Expr} (hc : Parse.okCallee c = true) (ha : Parse.RenderableList as = true) :

Parse.RenderableExpr (Js.Expr.call c as) = true

Used by

theorem

Lean2Js.Compile.renderable_arrowCall

[Core.Discriminators] {ps : List String} {body : Js.Expr} {as : List Js.Expr} (hp : ps.all okName = true) (hb : Parse.RenderableExpr body = true) (ha : Parse.RenderableList as = true) :

Parse.RenderableExpr (Js.Expr.arrowCall ps body as) = true

Used by

theorem

Lean2Js.Compile.renderable_member

[Core.Discriminators] {o : Js.Expr} {f : String} (ho : Parse.RenderableExpr o = true) (hf : okName f = true) :

Parse.RenderableExpr (o.member f) = true

Used by

theorem

Lean2Js.Compile.renderable_arrayLit

[Core.Discriminators] {es : List Js.Expr} (h : Parse.RenderableList es = true) :

Parse.RenderableExpr (Js.Expr.arrayLit es) = true

Used by

theorem

Lean2Js.Compile.renderable_dictLit

[Core.Discriminators] {es : List (String × Js.Expr)} (h : Parse.RenderablePairs es = true) :

Parse.RenderableExpr (Js.Expr.dictLit es) = true

Used by

theorem

Lean2Js.Compile.renderable_mapJs

[Core.Discriminators] {arr : Js.Expr} {b : String} {body : Js.Expr} (ha : Parse.RenderableExpr arr = true) (hb : okName b = true) (hy : Parse.RenderableExpr body = true) :

Parse.RenderableExpr (arr.mapJs b body) = true

Used by

theorem

Lean2Js.Compile.renderable_filterJs

[Core.Discriminators] {arr : Js.Expr} {b : String} {body : Js.Expr} (ha : Parse.RenderableExpr arr = true) (hb : okName b = true) (hy : Parse.RenderableExpr body = true) :

Parse.RenderableExpr (arr.filterJs b body) = true

Used by

theorem

Lean2Js.Compile.renderable_sortByJs

[Core.Discriminators] {arr : Js.Expr} {b : String} {body : Js.Expr} (ha : Parse.RenderableExpr arr = true) (hb : okName b = true) (hy : Parse.RenderableExpr body = true) :

Parse.RenderableExpr (arr.sortByJs b body) = true

Used by

theorem

Lean2Js.Compile.renderable_findJs

[Core.Discriminators] {arr : Js.Expr} {b : String} {body : Js.Expr} (ha : Parse.RenderableExpr arr = true) (hb : okName b = true) (hy : Parse.RenderableExpr body = true) :

Parse.RenderableExpr (arr.findJs b body) = true

Used by

theorem

Lean2Js.Compile.renderable_quantJs

[Core.Discriminators] {op : Core.QuantOp} {arr : Js.Expr} {b : String} {body : Js.Expr} (ha : Parse.RenderableExpr arr = true) (hb : okName b = true) (hy : Parse.RenderableExpr body = true) :

Parse.RenderableExpr (Js.Expr.quantJs op arr b body) = true

Used by

theorem

Lean2Js.Compile.renderable_reduceJs

[Core.Discriminators] {arr init : Js.Expr} {a e : String} {body : Js.Expr} (ha : Parse.RenderableExpr arr = true) (hi : Parse.RenderableExpr init = true) (hac : okName a = true) (he : okName e = true) (hy : Parse.RenderableExpr body = true) :

Parse.RenderableExpr (arr.reduceJs init a e body) = true

Used by

theorem

Lean2Js.Compile.renderable_check

[Core.Discriminators] {d : Js.TyDesc} {e : Js.Expr} (he : Parse.RenderableExpr e = true) :

Parse.RenderableExpr (Js.Expr.check d e) = true

Used by

theorem

Lean2Js.Compile.renderable_out

[Core.Discriminators] {d : Js.TyDesc} {e : Js.Expr} (he : Parse.RenderableExpr e = true) :

Parse.RenderableExpr (Js.Expr.out d e) = true

Used by

theorem

Lean2Js.Compile.renderable_foldJs

[Core.Discriminators] {scrut : Js.Expr} {key : String} {spec : Js.FoldSpec} {b : String} {body : Js.Expr} (hs : Parse.RenderableExpr scrut = true) (hb : okName b = true) (hy : Parse.RenderableExpr body = true) :

Parse.RenderableExpr (scrut.foldJs key spec b body) = true

A fold's call is readable back where its scrutinee and its arm chain are. The key it indexes by and the spec it hands __fold are read off the declared type rather than written by an author, and the reader takes both back from the text without a name of its own.

Used by

theorem

Lean2Js.Compile.renderable_retWalk

[Core.Discriminators] {d : Js.TyDesc} {e : Js.Expr} (he : Parse.RenderableExpr e = true) :

Parse.RenderableExpr (retWalk d e) = true

The entry's walk out is renderable either way: where it emits nothing the expression is the call itself, and where it emits the walk it is the call inside one more form.

Used by

theorem

Lean2Js.Compile.okCallee_of_ctx

[Core.Discriminators] {ctx : Ctx} {name : String} {ty : Core.Ty} (hctx : CtxOk ctx) (h : Option.map (fun (x : String × Core.Ty) => x.snd) (List.find? (fun (x : String × Core.Ty) => x.fst == name) ctx) = some ty) :

Parse.okCallee name = true

Used by

theorem

Lean2Js.Compile.okCallee_of_decl

[Core.Discriminators] {p : Core.Program} {name : String} {d : Core.Decl} (hp : DeclNamesOk p) (h : p.find? name = some d) :

Parse.okCallee name = true

Used by

theorem

Lean2Js.Compile.okName_of_okCallee

[Core.Discriminators] {s : String} (h : Parse.okCallee s = true) :

okName s = true

Used by

theorem

Lean2Js.Compile.ctxOk_cons

[Core.Discriminators] {ctx : Ctx} {n : String} {ty : Core.Ty} (hn : Parse.okCallee n = true) (h : CtxOk ctx) :

CtxOk ((n, ty) :: ctx)

Used by

theorem

Lean2Js.Compile.ctxOk_append

[Core.Discriminators] {ctx : Ctx} {binds : List (String × Js.Expr × Core.Ty)} (hb : BindsOk binds = true) (h : CtxOk ctx) :

CtxOk (List.map (fun (b : String × Js.Expr × Core.Ty) => (b.fst, b.snd.snd)) binds ++ ctx)

Used by

theorem

Lean2Js.Compile.okCallee_of_decl_name

[Core.Discriminators] {p : Core.Program} {name : String} {d : Core.Decl} (hp : DeclNamesOk p) (h : p.find? name = some d) :

Parse.okCallee d.name = true

Used by

theorem

Lean2Js.Compile.renderable_numericHelper

[Core.Discriminators] {ty : Core.Ty} {op : Core.BinOp} {a b j : Js.Expr} (ha : Parse.RenderableExpr a = true) (hb : Parse.RenderableExpr b = true) (h : numericHelper ty op a b = some j) :

Parse.RenderableExpr j = true

Used by

theorem

Lean2Js.Compile.okOp_of_orderSymbol

[Core.Discriminators] {op : Core.BinOp} {sym : String} (h : orderSymbol op = some sym) :

Parse.okOp sym = true

Used by

theorem

Lean2Js.Compile.okCallee_strUnHelper

[Core.Discriminators] (op : Core.StrUnOp) :

Parse.okCallee (strUnHelper op) = true

Used by

theorem

Lean2Js.Compile.okCallee_strBinHelper

[Core.Discriminators] (op : Core.StrBinOp) :

Parse.okCallee (strBinHelper op) = true

Used by

theorem

Lean2Js.Compile.okName_of_ctorsAt

[Core.Discriminators] {p : Core.Program} (hfn : FieldNamesOk p) {n : String} {t : Core.TypeDef} (ht : p.findType? n = some t) {args : List Core.Ty} {c : Core.CtorDef} (hc : c ∈ t.ctorsAt args) {f : Core.Field} (hf : f ∈ c.fields) :

okName f.name = true

Used by

theorem

Lean2Js.Compile.okName_of_proj

[Core.Discriminators] {p : Core.Program} (hfn : FieldNamesOk p) {n : String} {args : List Core.Ty} {t : Core.TypeDef} {c : Core.CtorDef} {f : Core.Field} {field : String} (hft : p.findType? n = some t) (hc : t.ctorsAt args = [c]) (hf : List.find? (fun (x : Core.Field) => x.name == field) c.fields = some f) :

okName field = true

The name a field read writes after the dot is the name of a field the type declares, and validateType has already put that through validateIdent.

Used by

theorem

Lean2Js.Compile.renderablePairs_cons

[Core.Discriminators] {k : String} {v : Js.Expr} {rest : List (String × Js.Expr)} (hv : Parse.RenderableExpr v = true) (hr : Parse.RenderablePairs rest = true) :

Parse.RenderablePairs ((k, v) :: rest) = true

Used by

theorem

Lean2Js.Compile.renderable_foldPatParts

[Core.Discriminators] {p : Core.Program} (hfn : FieldNamesOk p) {typeName : String} {tyArgs : List Core.Ty} {result : Core.Ty} {path : Js.Expr} {pat : Core.Pat} (hpath : Parse.RenderableExpr path = true) (tests : List Js.Expr) (binds : List (String × Js.Expr × Core.Ty)) :

foldPatParts p.types typeName tyArgs result path pat = Except.ok (tests, binds) → Parse.RenderableList tests = true ∧ BindsOk binds = true

A fold's alternative reads the paths a match's reads. Only the types its binders carry move — a field that came round is bound to the answer for it — and a type is not something the reader sees.

Used by

Every expression the compiler builds #

The recursion is compileExpr's own: the names it picks up come from the scope and from the declarations, the operators and callees it writes it spells itself, and everything else is one of its subexpressions.

theorem

Lean2Js.Compile.renderable_compiled

[Core.Discriminators] {p : Core.Program} (hp : DeclNamesOk p) (hfn : FieldNamesOk p) :

(∀ (ctx : Ctx) (e : Core.Expr), CtxOk ctx → ∀ (j : Js.Expr) (t : Core.Ty), compileExpr p ctx e = Except.ok (j, t) → Parse.RenderableExpr j = true) ∧ (∀ (ctx : Ctx) (entries : List (String × Core.Expr)), CtxOk ctx → ∀ (js : List (Js.Expr × Core.Ty)), compileValues p ctx entries = Except.ok js → Parse.RenderableList (List.map (fun (x : Js.Expr × Core.Ty) => x.fst) js) = true) ∧ (∀ (ctx : Ctx) (typeName : String) (tyArgs : List Core.Ty) (result : Core.Ty) (alts : List Core.Alt), CtxOk ctx → ∀ (arms : List Arm), compileFoldAlts p ctx typeName tyArgs result alts = Except.ok arms → arms.all ArmOk = true) ∧ (∀ (ctx : Ctx) (ty : Core.Ty) (alts : List Core.Alt), CtxOk ctx → ∀ (arms : List Arm), compileAlts p ctx ty alts = Except.ok arms → arms.all ArmOk = true) ∧ ∀ (ctx : Ctx) (es : List Core.Expr), CtxOk ctx → ∀ (js : List (Js.Expr × Core.Ty)), compileArgs p ctx es = Except.ok js → Parse.RenderableList (List.map (fun (x : Js.Expr × Core.Ty) => x.fst) js) = true

Used by

The statements a declaration's body becomes #

The entry's consts bind the declared names to the raw __p0, __p1, … it was called with, and the body's are the lets lined up at its head. Both are names the reader takes back: the declared ones went through validateIdent and the raw ones are the compiler's own.

theorem

Lean2Js.Compile.isDigit_digitChar

[Core.Discriminators] (d : Nat) :

d < 10 → d.digitChar.isDigit = true

Used by

theorem

Lean2Js.Compile.toDigitsCore_all_digit

[Core.Discriminators] (fuel n : Nat) (ds : List Char) :

ds.all Char.isDigit = true → (Nat.toDigitsCore 10 fuel n ds).all Char.isDigit = true

Used by

theorem

Lean2Js.Compile.repr_all_digit

[Core.Discriminators] (n : Nat) :

(toString n).toList.all Char.isDigit = true

Nat.repr is a wall to a proof that wants to read its characters back, but not to one that only wants to know they are digits.

Used by

theorem

Lean2Js.Compile.okCallee_rawParam

[Core.Discriminators] (i : Nat) :

Parse.okCallee (rawParam i) = true

Used by

theorem

Lean2Js.Compile.rawParams_all_okName

[Core.Discriminators] (i : Nat) (params : List Core.Param) :

(rawParams i params).all okName = true

Used by

theorem

Lean2Js.Compile.ctxOk_of_params

[Core.Discriminators] (params : List Core.Param) :

(params.forM fun (param : Core.Param) => validateIdent "parameter" param.name) = Except.ok () → CtxOk (List.map (fun (param : Core.Param) => (param.name, param.ty)) params)

Used by

theorem

Lean2Js.Compile.renderable_compileFinish

[Core.Discriminators] {p : Core.Program} (hp : DeclNamesOk p) (hfn : FieldNamesOk p) {ctx : Ctx} {e : Core.Expr} {acc stmts : List Js.Stmt} {ty : Core.Ty} (hctx : CtxOk ctx) (hacc : acc.all Parse.RenderableStmt = true) (h : compileFinish p ctx e acc = Except.ok (stmts, ty)) :

stmts.all Parse.RenderableStmt = true

Used by

theorem

Lean2Js.Compile.renderable_compileBody

[Core.Discriminators] {p : Core.Program} (hp : DeclNamesOk p) (hfn : FieldNamesOk p) (ctx : Ctx) (e : Core.Expr) (acc stmts : List Js.Stmt) (ty : Core.Ty) :

CtxOk ctx → acc.all Parse.RenderableStmt = true → compileBody p ctx e acc = Except.ok (stmts, ty) → stmts.all Parse.RenderableStmt = true

Used by

theorem

Lean2Js.Compile.renderable_paramChecks

[Core.Discriminators] {p : Core.Program} (i : Nat) (params : List Core.Param) (checks : List Js.Stmt) :

(params.forM fun (param : Core.Param) => validateIdent "parameter" param.name) = Except.ok () → paramChecks p i params = Except.ok checks → checks.all Parse.RenderableStmt = true

Used by

The declaration and the program #

theorem

Lean2Js.Compile.fieldNamesOk_of_validated

[Core.Discriminators] {p : Core.Program} (ts : List Core.TypeDef) (h : ts.forM (validateType p) = Except.ok ()) (t : Core.TypeDef) :

t ∈ ts → ∀ (c : Core.CtorDef), c ∈ t.ctors → ∀ (f : Core.Field), f ∈ c.fields → okName f.name = true

Used by

theorem

Lean2Js.Compile.renderable_paramIdents

[Core.Discriminators] (params : List Core.Param) :

(params.forM fun (param : Core.Param) => validateIdent "parameter" param.name) = Except.ok () → Parse.RenderableList (paramIdents params) = true

Used by

theorem

Lean2Js.Compile.paramNames_all_okName

[Core.Discriminators] (params : List Core.Param) :

(params.forM fun (param : Core.Param) => validateIdent "parameter" param.name) = Except.ok () → (List.map (fun (x : Core.Param) => x.name) params).all okName = true

Used by

theorem

Lean2Js.Compile.renderableFunc_of_compileDecl

[Core.Discriminators] {p : Core.Program} (hp : DeclNamesOk p) (hfn : FieldNamesOk p) (hn : TypeNamesOk p) {d : Core.Decl} {fns : Js.Func × Js.Func} (h : compileDecl p d = Except.ok fns) :

Parse.RenderableFunc fns.fst = true ∧ Parse.RenderableFunc fns.snd = true

Used by

theorem

Lean2Js.Compile.declNames_of_compileDecls

[Core.Discriminators] {p : Core.Program} (i : Nat) (ds : List Core.Decl) (fs : List Js.Func) :

compileDecls p i ds = Except.ok fs → ∀ (d : Core.Decl), d ∈ ds → Parse.okCallee d.name = true

Used by

theorem

Lean2Js.Compile.renderable_compileDecls

[Core.Discriminators] {p : Core.Program} (hp : DeclNamesOk p) (hfn : FieldNamesOk p) (hn : TypeNamesOk p) (i : Nat) (ds : List Core.Decl) (fs : List Js.Func) :

compileDecls p i ds = Except.ok fs → fs.all Parse.RenderableFunc = true

Used by

theorem

Lean2Js.Compile.renderableModule_of_compileProgram

[Core.Discriminators] {p : Core.Program} {m : Js.Module} (h : compileProgram p = Except.ok m) :

Parse.RenderableModule m = true

Nothing the compiler builds falls outside what the reader takes back. Renderable names the trees render does not separate, and this says the compiler never writes one: the names it emits are the ones validateIdent accepted or the ones it spells itself, and its operators and callees are a fixed handful that the reader does not dispatch on.

Used by

theorem

Lean2Js.Compile.parseModule_render_of_compileProgram

[Core.Discriminators] {p : Core.Program} {m : Js.Module} (h : compileProgram p = Except.ok m) :

Parse.parseModule m.render.toList = some m

The file the compiler writes reads back as the module it was compiled from. No side condition is left: the roundtrip holds of everything compileProgram produces.

Used by