Skip to content

Lean2Js.Roundtrip

Imports 2

That the reader gives the printer's input back #

That the reader in Parse gives the printer's input back.

Js.Expr.render is not injective, so the statement is about the trees the compiler actually builds. Renderable names the three places two trees share a text — a callee that the reader dispatches on, a unary operator that is not ! or -, a name that is not an identifier — plus a doc comment that closes itself early.

The fuel is bounded by the length of the text being read, so the top level passes the text's own length and no fuel caveat survives.

What the reader needs of a tree #

def

Lean2Js.Parse.dispatchNames

:

The names parseNamed gives a meaning of their own. An identifier or a callee spelled one of these reads back as the form the reader has a constructor for.

Equations

Lean2Js.Parse.dispatchNames = ["true", "false", "new", "__ck", "__out", "__map", "__filter", "__find", "__all", "__any", "__reduce", "__sortBy", "__fold"]

Instances For

Used by

def

Lean2Js.Parse.okCallee

(s : String) :

Equations

Lean2Js.Parse.okCallee s = (Lean2Js.okName s && !Lean2Js.Parse.dispatchNames.contains s)

Instances For

Used by

def

Lean2Js.Parse.okOp

(s : String) :

Equations

Lean2Js.Parse.okOp s = match s.toList with | [] => false | c :: cs => (c :: cs).all Lean2Js.Parse.isOpChar

Instances For

Used by

def

Lean2Js.Parse.RenderableExpr

@[irreducible]

:

Js.Expr → Bool

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.num i) = true
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.bigLit i) = true
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.str s) = true
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.bool b) = true
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.ident name) = Lean2Js.Parse.okCallee name
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.unary op e) = ((op == "!" || op == "-") && Lean2Js.Parse.RenderableExpr e)
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.binary op lhs rhs) = (Lean2Js.Parse.okOp op && Lean2Js.Parse.RenderableExpr lhs && Lean2Js.Parse.RenderableExpr rhs)
Lean2Js.Parse.RenderableExpr (c.cond t e) = (Lean2Js.Parse.RenderableExpr c && Lean2Js.Parse.RenderableExpr t && Lean2Js.Parse.RenderableExpr e)
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.call callee args) = (Lean2Js.Parse.okCallee callee && Lean2Js.Parse.RenderableList args)
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.arrowCall params body args) = (params.all Lean2Js.okName && Lean2Js.Parse.RenderableExpr body && Lean2Js.Parse.RenderableList args)
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.objLit fields) = Lean2Js.Parse.RenderablePairs fields
Lean2Js.Parse.RenderableExpr (obj.member field) = (Lean2Js.Parse.RenderableExpr obj && Lean2Js.okName field)
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.arrayLit items) = Lean2Js.Parse.RenderableList items
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.dictLit entries) = Lean2Js.Parse.RenderablePairs entries
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.check d e) = Lean2Js.Parse.RenderableExpr e
Lean2Js.Parse.RenderableExpr (arr.mapJs binder body) = (Lean2Js.Parse.RenderableExpr arr && Lean2Js.okName binder && Lean2Js.Parse.RenderableExpr body)
Lean2Js.Parse.RenderableExpr (arr.filterJs binder body) = (Lean2Js.Parse.RenderableExpr arr && Lean2Js.okName binder && Lean2Js.Parse.RenderableExpr body)
Lean2Js.Parse.RenderableExpr (arr.sortByJs binder body) = (Lean2Js.Parse.RenderableExpr arr && Lean2Js.okName binder && Lean2Js.Parse.RenderableExpr body)
Lean2Js.Parse.RenderableExpr (arr.findJs binder body) = (Lean2Js.Parse.RenderableExpr arr && Lean2Js.okName binder && Lean2Js.Parse.RenderableExpr body)
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.quantJs op arr binder body) = (Lean2Js.Parse.RenderableExpr arr && Lean2Js.okName binder && Lean2Js.Parse.RenderableExpr body)
Lean2Js.Parse.RenderableExpr (Lean2Js.Js.Expr.out d e) = Lean2Js.Parse.RenderableExpr e
Lean2Js.Parse.RenderableExpr (scrut.foldJs key spec binder body) = (Lean2Js.Parse.RenderableExpr scrut && Lean2Js.okName binder && Lean2Js.Parse.RenderableExpr body)

Instances For

Used by

def

Lean2Js.Parse.RenderableList

@[irreducible]

:

List Js.Expr → Bool

Equations

Lean2Js.Parse.RenderableList [] = true
Lean2Js.Parse.RenderableList (e :: rest) = (Lean2Js.Parse.RenderableExpr e && Lean2Js.Parse.RenderableList rest)

Instances For

Used by

def

Lean2Js.Parse.RenderablePairs

@[irreducible]

:

List (String × Js.Expr) → Bool

Equations

Lean2Js.Parse.RenderablePairs [] = true
Lean2Js.Parse.RenderablePairs ((fst, v) :: rest) = (Lean2Js.Parse.RenderableExpr v && Lean2Js.Parse.RenderablePairs rest)

Instances For

Used by

The printer's equations #

Expr.render recurses on a measure, so its equations do not unfold on their own.

theorem

Lean2Js.Parse.render_num

(i : Int) :

(Js.Expr.num i).render = renderInt i

Used by

theorem

Lean2Js.Parse.render_bigLit

(i : Int) :

(Js.Expr.bigLit i).render = renderInt i ++ "n"

Used by

theorem

Lean2Js.Parse.render_str

(s : String) :

(Js.Expr.str s).render = "\"" ++ escapeString s ++ "\""

Used by

theorem

Lean2Js.Parse.render_bool

(b : Bool) :

(Js.Expr.bool b).render = if b = true then "true" else "false"

Used by

theorem

Lean2Js.Parse.render_ident

(name : String) :

(Js.Expr.ident name).render = name

Used by

theorem

Lean2Js.Parse.render_unary

(op : String) (e : Js.Expr) :

(Js.Expr.unary op e).render = "(" ++ op ++ e.render ++ ")"

Used by

theorem

Lean2Js.Parse.render_binary

(op : String) (l r : Js.Expr) :

(Js.Expr.binary op l r).render = "(" ++ l.render ++ " " ++ op ++ " " ++ r.render ++ ")"

Used by

theorem

Lean2Js.Parse.render_cond

(c t e : Js.Expr) :

(c.cond t e).render = "(" ++ c.render ++ " ? " ++ t.render ++ " : " ++ e.render ++ ")"

Used by

theorem

Lean2Js.Parse.render_call

(callee : String) (args : List Js.Expr) :

(Js.Expr.call callee args).render = callee ++ "(" ++ Js.Expr.renderList args ++ ")"

Used by

theorem

Lean2Js.Parse.render_arrowCall

(ps : List String) (body : Js.Expr) (args : List Js.Expr) :

(Js.Expr.arrowCall ps body args).render = "((" ++ Js.renderNames ps ++ ") => (" ++ body.render ++ "))(" ++ Js.Expr.renderList args ++ ")"

Used by

theorem

Lean2Js.Parse.render_objLit

(fs : List (String × Js.Expr)) :

(Js.Expr.objLit fs).render = "{ " ++ Js.Expr.renderFields fs ++ " }"

Used by

theorem

Lean2Js.Parse.render_member

(obj : Js.Expr) (field : String) :

(obj.member field).render = "(" ++ obj.render ++ ")." ++ field

Used by

theorem

Lean2Js.Parse.render_arrayLit

(items : List Js.Expr) :

(Js.Expr.arrayLit items).render = "[" ++ Js.Expr.renderList items ++ "]"

Used by

theorem

Lean2Js.Parse.render_dictLit

(es : List (String × Js.Expr)) :

(Js.Expr.dictLit es).render = "new Map([" ++ Js.Expr.renderEntries es ++ "])"

Used by

theorem

Lean2Js.Parse.render_check

(d : Js.TyDesc) (e : Js.Expr) :

(Js.Expr.check d e).render = "__ck(" ++ e.render ++ ", " ++ d.render ++ ")"

Used by

theorem

Lean2Js.Parse.render_out

(d : Js.TyDesc) (e : Js.Expr) :

(Js.Expr.out d e).render = "__out(" ++ e.render ++ ", " ++ d.render ++ ", [])"

Used by

theorem

Lean2Js.Parse.render_mapJs

(arr : Js.Expr) (b : String) (body : Js.Expr) :

(arr.mapJs b body).render = "__map(" ++ arr.render ++ ", (" ++ b ++ ") => (" ++ body.render ++ "))"

Used by

theorem

Lean2Js.Parse.render_filterJs

(arr : Js.Expr) (b : String) (body : Js.Expr) :

(arr.filterJs b body).render = "__filter(" ++ arr.render ++ ", (" ++ b ++ ") => (" ++ body.render ++ "))"

Used by

theorem

Lean2Js.Parse.render_sortByJs

(arr : Js.Expr) (b : String) (body : Js.Expr) :

(arr.sortByJs b body).render = "__sortBy(" ++ arr.render ++ ", (" ++ b ++ ") => (" ++ body.render ++ "))"

Used by

theorem

Lean2Js.Parse.render_findJs

(arr : Js.Expr) (b : String) (body : Js.Expr) :

(arr.findJs b body).render = "__find(" ++ arr.render ++ ", (" ++ b ++ ") => (" ++ body.render ++ "))"

Used by

theorem

Lean2Js.Parse.render_quantJs

(op : Core.QuantOp) (arr : Js.Expr) (b : String) (body : Js.Expr) :

(Js.Expr.quantJs op arr b body).render = "__" ++ op.name ++ "(" ++ arr.render ++ ", (" ++ b ++ ") => (" ++ body.render ++ "))"

Used by

theorem

Lean2Js.Parse.render_reduceJs

(arr init : Js.Expr) (a e : String) (body : Js.Expr) :

(arr.reduceJs init a e body).render = "__reduce(" ++ arr.render ++ ", " ++ init.render ++ ", (" ++ a ++ ", " ++ e ++ ") => (" ++ body.render ++ "))"

Used by

theorem

Lean2Js.Parse.render_foldJs

(scrut : Js.Expr) (key : String) (spec : Js.FoldSpec) (b : String) (body : Js.Expr) :

(scrut.foldJs key spec b body).render = "__fold(" ++ scrut.render ++ ", \"" ++ escapeString key ++ "\", { " ++ Js.renderFoldSpec spec ++ " }, (" ++ b ++ ") => (" ++ body.render ++ "))"

Used by

Separators #

The reader is greedy over names and numerals, it turns a name into a call when a ( follows, and after a ) it looks for a ., so a rendering has to be followed by a character that does none of those.

def

Lean2Js.Parse.Sep

(cs : List Char) :

Equations

Lean2Js.Parse.Sep cs = ∀ (c : Char) (r : List Char), cs = c :: r → Lean2Js.isIdentPart c = false ∧ c ≠ '(' ∧ c ≠ '.'

Instances For

Used by

theorem

Lean2Js.Parse.Sep.nil

:

Used by

theorem

Lean2Js.Parse.Sep.cons

{c : Char} (h1 : isIdentPart c = false) (h2 : c ≠ '(') (h3 : c ≠ '.') (r : List Char) :

Sep (c :: r)

Used by

theorem

Lean2Js.Parse.Sep.toIdent

{cs : List Char} (h : Sep cs) :

notIdentFirst cs

Used by

theorem

Lean2Js.Parse.Sep.toDigit

{cs : List Char} (h : Sep cs) :

notDigitFirst cs

Used by

theorem

Lean2Js.Parse.digit_isIdentPart

{c : Char} (h : c.isDigit = true) :

isIdentPart c = true

Used by

theorem

Lean2Js.Parse.natDigits_all_identPart

(n : Nat) :

(natDigits n).all isIdentPart = true

Used by

Names #

theorem

Lean2Js.Parse.okName_ne_nil

{s : String} (h : okName s = true) :

s.toList ≠ []

Used by

theorem

Lean2Js.Parse.okName_all

{s : String} (h : okName s = true) :

s.toList.all isIdentPart = true

Used by

theorem

Lean2Js.Parse.okName_start

{s : String} (h : okName s = true) {c : Char} {cs : List Char} (hm : s.toList = c :: cs) :

isIdentStart c = true

Used by

theorem

Lean2Js.Parse.okCallee_name

{s : String} (h : okCallee s = true) :

okName s = true

Used by

theorem

Lean2Js.Parse.okCallee_not_dispatch

{s : String} (h : okCallee s = true) :

dispatchNames.contains s = false

Used by

Where an identifier list stops #

parseParen decides between an arrow call and the other parenthesised forms by reading ahead for ( names ) => (. What makes that decision sound is that the lookahead fails on every rendering: the identifier list stops at the first character a name cannot contain, and in a rendering that character is never the ) the arrow head wants.

theorem

Lean2Js.Parse.expect_arrow_ne

{c : Char} (h : c ≠ ')') (cs : List Char) :

expect [')', ' ', '=', '>', ' ', '('] (c :: cs) = none

Used by

structure

Lean2Js.Parse.AfterHead

(cs : List Char) :

notIdent(c : Char) (r : List Char) : cs = c :: r → isIdentPart c = false
notComma : expect [',', ' '] cs = none
notArrow : expect [')', ' ', '=', '>', ' ', '('] cs = none

Instances For

Used by

theorem

Lean2Js.Parse.AfterHead.close

(r : List Char) :

AfterHead (')' :: '.' :: r)

Used by

theorem

Lean2Js.Parse.AfterHead.cons

{c : Char} (h1 : isIdentPart c = false) (h2 : c ≠ ',') (h3 : c ≠ ')') (r : List Char) :

AfterHead (c :: r)

Used by

theorem

Lean2Js.Parse.parseIdentList_stuck

(f : Nat) {c : Char} (hc : isIdentPart c = false) (cs : List Char) :

parseIdentList (f + 1) (c :: cs) = some ([], c :: cs)

Used by

theorem

Lean2Js.Parse.parseIdentList_last

(f : Nat) (name : List Char) (hne : name ≠ []) (hall : name.all isIdentPart = true) (suffix : List Char) (hsuf : notIdentFirst suffix) (hcomma : expect [',', ' '] suffix = none) :

parseIdentList (f + 1) (name ++ suffix) = some ([String.ofList name], suffix)

Used by

theorem

Lean2Js.Parse.identList_head

{c : Char} (hc : isIdentPart c = false) (hne : c ≠ ')') (f : Nat) (tail : List Char) {ns : List String} {r : List Char} (h : parseIdentList (f + 1) (c :: tail) = some (ns, r)) :

expect [')', ' ', '=', '>', ' ', '('] r = none

The rendering opens with a character no name can contain, so the list is empty and the lookahead stops on that character.

Used by

theorem

Lean2Js.Parse.identList_name_head

(f : Nat) (name : List Char) (hne : name ≠ []) (hall : name.all isIdentPart = true) {c : Char} (hc : isIdentPart c = false) (hcm : c ≠ ',') (hcp : c ≠ ')') (tail : List Char) {ns : List String} {r : List Char} (h : parseIdentList (f + 1) (name ++ c :: tail) = some (ns, r)) :

expect [')', ' ', '=', '>', ' ', '('] r = none

The rendering opens with a name and then a character no name can contain.

Used by

theorem

Lean2Js.Parse.identList_name_all

(f : Nat) (name : List Char) (hne : name ≠ []) (hall : name.all isIdentPart = true) (suffix : List Char) (hs : AfterHead suffix) {ns : List String} {r : List Char} (h : parseIdentList (f + 1) (name ++ suffix) = some (ns, r)) :

expect [')', ' ', '=', '>', ' ', '('] r = none

The rendering is a name and nothing else, so the lookahead stops where the rendering ends.

Used by

The printer's output as characters #

Everything below reads the rendering one character at a time, so each printer branch is restated as the list it writes, with the literal chunks spelled out and the recursive parts left as they are.

theorem

Lean2Js.Parse.render_num_toList

(i : Int) :

(Js.Expr.num i).render.toList = (renderInt i).toList

Used by

theorem

Lean2Js.Parse.render_bigLit_toList

(i : Int) :

(Js.Expr.bigLit i).render.toList = (renderInt i).toList ++ ['n']

Used by

theorem

Lean2Js.Parse.render_str_toList

(s : String) :

(Js.Expr.str s).render.toList = '\"' :: ((escapeString s).toList ++ ['\"'])

Used by

theorem

Lean2Js.Parse.render_bool_true_toList

:

(Js.Expr.bool true).render.toList = ['t', 'r', 'u', 'e']

Used by

theorem

Lean2Js.Parse.render_bool_false_toList

:

(Js.Expr.bool false).render.toList = ['f', 'a', 'l', 's', 'e']

Used by

theorem

Lean2Js.Parse.render_ident_toList

(name : String) :

(Js.Expr.ident name).render.toList = name.toList

Used by

theorem

Lean2Js.Parse.render_unary_toList

(op : String) (e : Js.Expr) :

(Js.Expr.unary op e).render.toList = '(' :: (op.toList ++ (e.render.toList ++ [')']))

Used by

theorem

Lean2Js.Parse.render_binary_toList

(op : String) (l r : Js.Expr) :

(Js.Expr.binary op l r).render.toList = '(' :: (l.render.toList ++ ' ' :: (op.toList ++ ' ' :: (r.render.toList ++ [')'])))

Used by

theorem

Lean2Js.Parse.render_cond_toList

(c t e : Js.Expr) :

(c.cond t e).render.toList = '(' :: (c.render.toList ++ ' ' :: '?' :: ' ' :: (t.render.toList ++ ' ' :: ':' :: ' ' :: (e.render.toList ++ [')'])))

Used by

theorem

Lean2Js.Parse.render_call_toList

(callee : String) (args : List Js.Expr) :

(Js.Expr.call callee args).render.toList = callee.toList ++ '(' :: ((Js.Expr.renderList args).toList ++ [')'])

Used by

theorem

Lean2Js.Parse.render_arrowCall_toList

(ps : List String) (body : Js.Expr) (args : List Js.Expr) :

(Js.Expr.arrowCall ps body args).render.toList = '(' :: '(' :: ((Js.renderNames ps).toList ++ ')' :: ' ' :: '=' :: '>' :: ' ' :: '(' :: (body.render.toList ++ ')' :: ')' :: '(' :: ((Js.Expr.renderList args).toList ++ [')'])))

Used by

theorem

Lean2Js.Parse.render_objLit_toList

(fs : List (String × Js.Expr)) :

(Js.Expr.objLit fs).render.toList = '{' :: ' ' :: ((Js.Expr.renderFields fs).toList ++ [' ', '}'])

Used by

theorem

Lean2Js.Parse.render_member_toList

(obj : Js.Expr) (field : String) :

(obj.member field).render.toList = '(' :: (obj.render.toList ++ ')' :: '.' :: field.toList)

Used by

theorem

Lean2Js.Parse.render_arrayLit_toList

(items : List Js.Expr) :

(Js.Expr.arrayLit items).render.toList = '[' :: ((Js.Expr.renderList items).toList ++ [']'])

Used by

theorem

Lean2Js.Parse.render_dictLit_toList

(es : List (String × Js.Expr)) :

(Js.Expr.dictLit es).render.toList = 'n' :: 'e' :: 'w' :: ' ' :: 'M' :: 'a' :: 'p' :: '(' :: '[' :: ((Js.Expr.renderEntries es).toList ++ [']', ')'])

Used by

theorem

Lean2Js.Parse.render_check_toList

(d : Js.TyDesc) (e : Js.Expr) :

(Js.Expr.check d e).render.toList = '_' :: '_' :: 'c' :: 'k' :: '(' :: (e.render.toList ++ ',' :: ' ' :: (d.render.toList ++ [')']))

Used by

theorem

Lean2Js.Parse.render_out_toList

(d : Js.TyDesc) (e : Js.Expr) :

(Js.Expr.out d e).render.toList = '_' :: '_' :: 'o' :: 'u' :: 't' :: '(' :: (e.render.toList ++ ',' :: ' ' :: (d.render.toList ++ [',', ' ', '[', ']', ')']))

Used by

theorem

Lean2Js.Parse.render_mapJs_toList

(arr : Js.Expr) (b : String) (body : Js.Expr) :

(arr.mapJs b body).render.toList = '_' :: '_' :: 'm' :: 'a' :: 'p' :: '(' :: Lean2Js.Parse.lambdaTail✝ arr b body

Used by

theorem

Lean2Js.Parse.render_sortByJs_toList

(arr : Js.Expr) (b : String) (body : Js.Expr) :

(arr.sortByJs b body).render.toList = '_' :: '_' :: 's' :: 'o' :: 'r' :: 't' :: 'B' :: 'y' :: '(' :: Lean2Js.Parse.lambdaTail✝ arr b body

Used by

theorem

Lean2Js.Parse.render_filterJs_toList

(arr : Js.Expr) (b : String) (body : Js.Expr) :

(arr.filterJs b body).render.toList = '_' :: '_' :: 'f' :: 'i' :: 'l' :: 't' :: 'e' :: 'r' :: '(' :: Lean2Js.Parse.lambdaTail✝ arr b body

Used by

theorem

Lean2Js.Parse.render_findJs_toList

(arr : Js.Expr) (b : String) (body : Js.Expr) :

(arr.findJs b body).render.toList = '_' :: '_' :: 'f' :: 'i' :: 'n' :: 'd' :: '(' :: Lean2Js.Parse.lambdaTail✝ arr b body

Used by

theorem

Lean2Js.Parse.render_allJs_toList

(arr : Js.Expr) (b : String) (body : Js.Expr) :

(Js.Expr.quantJs Core.QuantOp.all arr b body).render.toList = '_' :: '_' :: 'a' :: 'l' :: 'l' :: '(' :: Lean2Js.Parse.lambdaTail✝ arr b body

Used by

theorem

Lean2Js.Parse.render_anyJs_toList

(arr : Js.Expr) (b : String) (body : Js.Expr) :

(Js.Expr.quantJs Core.QuantOp.any arr b body).render.toList = '_' :: '_' :: 'a' :: 'n' :: 'y' :: '(' :: Lean2Js.Parse.lambdaTail✝ arr b body

Used by

theorem

Lean2Js.Parse.render_reduceJs_toList

(arr init : Js.Expr) (a e : String) (body : Js.Expr) :

(arr.reduceJs init a e body).render.toList = '_' :: '_' :: 'r' :: 'e' :: 'd' :: 'u' :: 'c' :: 'e' :: '(' :: (arr.render.toList ++ ',' :: ' ' :: (init.render.toList ++ ',' :: ' ' :: '(' :: (a.toList ++ ',' :: ' ' :: (e.toList ++ ')' :: ' ' :: '=' :: '>' :: ' ' :: '(' :: (body.render.toList ++ [')', ')'])))))

Used by

theorem

Lean2Js.Parse.render_foldJs_toList

(scrut : Js.Expr) (key : String) (spec : Js.FoldSpec) (b : String) (body : Js.Expr) :

(scrut.foldJs key spec b body).render.toList = '_' :: '_' :: 'f' :: 'o' :: 'l' :: 'd' :: '(' :: (scrut.render.toList ++ ',' :: ' ' :: '\"' :: ((escapeString key).toList ++ '\"' :: ',' :: ' ' :: '{' :: ' ' :: ((Js.renderFoldSpec spec).toList ++ ' ' :: '}' :: ',' :: ' ' :: '(' :: (b.toList ++ ')' :: ' ' :: '=' :: '>' :: ' ' :: '(' :: (body.render.toList ++ [')', ')'])))))

Used by

theorem

Lean2Js.Parse.renderList_nil_toList

:

(Js.Expr.renderList []).toList = []

Used by

theorem

Lean2Js.Parse.renderList_one_toList

(e : Js.Expr) :

(Js.Expr.renderList [e]).toList = e.render.toList

Used by

theorem

Lean2Js.Parse.renderList_cons_toList

(e a : Js.Expr) (rest : List Js.Expr) :

(Js.Expr.renderList (e :: a :: rest)).toList = e.render.toList ++ ',' :: ' ' :: (Js.Expr.renderList (a :: rest)).toList

Used by

theorem

Lean2Js.Parse.renderFields_nil_toList

:

(Js.Expr.renderFields []).toList = []

Used by

theorem

Lean2Js.Parse.renderFields_one_toList

(k : String) (v : Js.Expr) :

(Js.Expr.renderFields [(k, v)]).toList = '\"' :: ((escapeString k).toList ++ '\"' :: ':' :: ' ' :: v.render.toList)

Used by

theorem

Lean2Js.Parse.renderFields_cons_toList

(k : String) (v : Js.Expr) (a : String × Js.Expr) (rest : List (String × Js.Expr)) :

(Js.Expr.renderFields ((k, v) :: a :: rest)).toList = '\"' :: ((escapeString k).toList ++ '\"' :: ':' :: ' ' :: (v.render.toList ++ ',' :: ' ' :: (Js.Expr.renderFields (a :: rest)).toList))

Used by

theorem

Lean2Js.Parse.renderEntries_nil_toList

:

(Js.Expr.renderEntries []).toList = []

Used by

theorem

Lean2Js.Parse.renderEntries_one_toList

(k : String) (v : Js.Expr) :

(Js.Expr.renderEntries [(k, v)]).toList = '[' :: '\"' :: ((escapeString k).toList ++ '\"' :: ',' :: ' ' :: (v.render.toList ++ [']']))

Used by

theorem

Lean2Js.Parse.renderEntries_cons_toList

(k : String) (v : Js.Expr) (a : String × Js.Expr) (rest : List (String × Js.Expr)) :

(Js.Expr.renderEntries ((k, v) :: a :: rest)).toList = '[' :: '\"' :: ((escapeString k).toList ++ '\"' :: ',' :: ' ' :: (v.render.toList ++ ']' :: ',' :: ' ' :: (Js.Expr.renderEntries (a :: rest)).toList))

Used by

The lookahead fails on every rendering but an arrow call #

theorem

Lean2Js.Parse.renderInt_ofNat_toList

(n : Nat) :

(renderInt (Int.ofNat n)).toList = natDigits n

Used by

theorem

Lean2Js.Parse.renderInt_negSucc_toList

(n : Nat) :

(renderInt (Int.negSucc n)).toList = '-' :: natDigits (n + 1)

Used by

theorem

Lean2Js.Parse.parseIdentList_render

(e : Js.Expr) (he : RenderableExpr e = true) (f : Nat) (suffix : List Char) (hs : AfterHead suffix) {ns : List String} {r : List Char} (h : parseIdentList (f + 1) (e.render.toList ++ suffix) = some (ns, r)) :

expect [')', ' ', '=', '>', ' ', '('] r = none

Used by

theorem

Lean2Js.Parse.arrowHead_ne

(f : Nat) {c : Char} (hc : c ≠ '(') (cs : List Char) :

parseArrowHead f (c :: cs) = none

Used by

theorem

Lean2Js.Parse.arrowHead_stuck

(f : Nat) (inner : List Char) (hstuck : ∀ (ns : List String) (r : List Char), parseIdentList (f + 1) inner = some (ns, r) → expect [')', ' ', '=', '>', ' ', '('] r = none) :

parseArrowHead (f + 1) ('(' :: inner) = none

Used by

theorem

Lean2Js.Parse.arrowHead_head

(f : Nat) {c : Char} (hc : isIdentPart c = false) (hne : c ≠ ')') (inner : List Char) :

parseArrowHead (f + 1) ('(' :: c :: inner) = none

Used by

theorem

Lean2Js.Parse.parseArrowHead_render

(e : Js.Expr) (he : RenderableExpr e = true) (f : Nat) (suffix : List Char) (hs : AfterHead suffix) :

parseArrowHead (f + 1) (e.render.toList ++ suffix) = none

The lookahead that picks an arrow call fails on every other parenthesised form: member closes with )., and binary and cond put a space where the arrow wants ).

Used by

Reaching the reader's branches #

The reader picks its branch on one character, so each case first has to say which character the rendering opens with.

theorem

Lean2Js.Parse.identStart_not_digit

{c : Char} (h : isIdentStart c = true) :

c.isDigit = false

Used by

theorem

Lean2Js.Parse.head_digit_of_natDigits

{n : Nat} {d : Char} {ds : List Char} (hn : natDigits n = d :: ds) :

d.isDigit = true

Used by

theorem

Lean2Js.Parse.render_head

(e : Js.Expr) (he : RenderableExpr e = true) :

∃ (c : Char ), ∃ (cs : List Char), e.render.toList = c :: cs ∧ (isIdentStart c = true ∨ c.isDigit = true ∨ c = '-' ∨ c = '\"' ∨ c = '(' ∨ c = '[' ∨ c = '{')

Used by

theorem

Lean2Js.Parse.render_head_ne

(e : Js.Expr) (he : RenderableExpr e = true) {c : Char} {cs : List Char} (h : e.render.toList = c :: cs) :

c ≠ ')' ∧ c ≠ ']' ∧ c ≠ ' ' ∧ c ≠ '!'

No rendering opens with a character that closes a list, so a reader looking for the end of one never mistakes an element for it.

Used by

theorem

Lean2Js.Parse.parseExpr_numHead

(f : Nat) {c : Char} (hc : (c == '-' || c.isDigit) = true) (cs : List Char) :

parseExpr (f + 1) (c :: cs) = parseNumeral (c :: cs)

Used by

theorem

Lean2Js.Parse.parseExpr_int

(f : Nat) (i : Int) (cs : List Char) :

parseExpr (f + 1) ((renderInt i).toList ++ cs) = parseNumeral ((renderInt i).toList ++ cs)

Used by

theorem

Lean2Js.Parse.parseExpr_start

(f : Nat) {c : Char} (hs : isIdentStart c = true) (cs : List Char) :

parseExpr (f + 1) (c :: cs) = match parseIdent (c :: cs) with | none => none | some (name, r) => parseNamed f name r

Used by

theorem

Lean2Js.Parse.parseNumeral_num

(i : Int) (rest : List Char) (hrest : Sep rest) :

parseNumeral ((renderInt i).toList ++ rest) = some (Js.Expr.num i, rest)

Used by

theorem

Lean2Js.Parse.parseNumeral_bigLit

(i : Int) (rest : List Char) :

parseNumeral ((renderInt i).toList ++ 'n' :: rest) = some (Js.Expr.bigLit i, rest)

Used by

theorem

Lean2Js.Parse.parseNamed_other

(f : Nat) (name : String) (h : dispatchNames.contains name = false) (cs : List Char) :

parseNamed (f + 1) name cs = match expect ['('] cs with | none => some (Js.Expr.ident name, cs) | some cs => do let __x ← parseExprList f ')' cs match __x with | (args, cs) => do let cs ← expect [')'] cs pure (Js.Expr.call name args, cs)

Used by

theorem

Lean2Js.Parse.render_head_num

(e : Js.Expr) (he : RenderableExpr e = true) {c : Char} {cs : List Char} (h : e.render.toList = c :: cs) (hc : c.isDigit = true ∨ c = '-') :

(∃ (i : Int ), e = Js.Expr.num i) ∨ ∃ (i : Int ), e = Js.Expr.bigLit i

Only a numeral is written starting with a digit or a minus sign, which is what lets parseParen decide by the character after ( whether a numeral reader should take the sign.

Used by

theorem

Lean2Js.Parse.descSize_le

(d : Js.TyDesc) :

descSize d ≤ d.render.toList.length

The descriptor reader's budget, read off the text it is handed rather than off the descriptor.

Used by

theorem

Lean2Js.Parse.foldFieldsSize_le

(fs : Js.FoldFields) :

foldFieldsSize fs ≤ (Js.renderFoldFields fs).toList.length + 1

The spec reader's budget, read off the text the same way the descriptor's is.

Used by

theorem

Lean2Js.Parse.specSize_le

(spec : Js.FoldSpec) :

specSize spec ≤ (Js.renderFoldSpec spec).toList.length + 1

Used by

theorem

Lean2Js.Parse.parseInt_neg_ofNat

(n : Nat) (rest : List Char) (hrest : notDigitFirst rest) :

parseInt ('-' :: (natDigits n ++ rest)) = some (-↑n, rest)

Used by

theorem

Lean2Js.Parse.parseExprList_step

(f : Nat) (close : Char) {c : Char} (hne : (c == close) = false) (cs : List Char) :

parseExprList (f + 1) close (c :: cs) = do let __x ← parseExpr f (c :: cs) match __x with | (e, r) => match expect [',', ' '] r with | none => pure ([e], r) | some r => do let __x ← parseExprList f close r match __x with | (es, r) => pure (e :: es, r)

Used by

Name lists and operators #

theorem

Lean2Js.Parse.renderNames_nil_toList

:

(Js.renderNames []).toList = []

Used by

theorem

Lean2Js.Parse.renderNames_one_toList

(n : String) :

(Js.renderNames [n]).toList = n.toList

Used by

theorem

Lean2Js.Parse.renderNames_cons_toList

(n a : String) (rest : List String) :

(Js.renderNames (n :: a :: rest)).toList = n.toList ++ ',' :: ' ' :: (Js.renderNames (a :: rest)).toList

Used by

theorem

Lean2Js.Parse.parseIdent_none

{cs : List Char} (h : notIdentFirst cs) :

parseIdent cs = none

Used by

theorem

Lean2Js.Parse.parseIdentList_names

(ps : List String) (hps : ps.all okName = true) (f : Nat) (hf : ps.length < f) (rest : List Char) (hrest : notIdentFirst rest) (hcomma : expect [',', ' '] rest = none) :

parseIdentList f ((Js.renderNames ps).toList ++ rest) = some (ps, rest)

Used by

theorem

Lean2Js.Parse.renderNames_length

(ps : List String) (hps : ps.all okName = true) :

ps.length ≤ (Js.renderNames ps).toList.length

Used by

theorem

Lean2Js.Parse.okOp_ne_nil

{s : String} (h : okOp s = true) :

s.toList ≠ []

Used by

theorem

Lean2Js.Parse.okOp_all

{s : String} (h : okOp s = true) :

s.toList.all isOpChar = true

Used by

theorem

Lean2Js.Parse.okOp_head

{s : String} (h : okOp s = true) {c : Char} {cs : List Char} (hm : s.toList = c :: cs) :

isOpChar c = true

Used by

theorem

Lean2Js.Parse.parseOpChars_append

(ds : List Char) (hds : ds.all isOpChar = true) (rest : List Char) (hrest : ∀ (c : Char) (r : List Char), rest = c :: r → isOpChar c = false) :

parseOpChars (ds ++ rest) = (ds, rest)

Used by

theorem

Lean2Js.Parse.parseOp_append

(op : String) (hop : okOp op = true) (rest : List Char) (hrest : ∀ (c : Char) (r : List Char), rest = c :: r → isOpChar c = false) :

parseOp (op.toList ++ rest) = some (op, rest)

Used by

theorem

Lean2Js.Parse.exists_cons_of_ne_nil

{α : Type u_1} {l : List α} (h : l ≠ []) :

∃ (a : α), ∃ (as : List α), l = a :: as

Used by

theorem

Lean2Js.Parse.parseExpr_name

(f : Nat) (name : String) (hn : okName name = true) (rest : List Char) (hrest : notIdentFirst rest) :

parseExpr (f + 1) (name.toList ++ rest) = parseNamed f name rest

Used by

theorem

Lean2Js.Parse.expect_open_none

{rest : List Char} (hrest : Sep rest) :

expect ['('] rest = none

Used by

Reaching the parenthesised branches #

theorem

Lean2Js.Parse.parseParen_bang

(g : Nat) (r : List Char) :

parseParen (g + 1 + 1) ('!' :: r) = do let __x ← parseExpr (g + 1) r match __x with | (e, r) => do let r ← expect [')'] r pure (Js.Expr.unary "!" e, r)

Used by

theorem

Lean2Js.Parse.parseParen_minusDigit

(g : Nat) {d : Char} (hd : d.isDigit = true) (r : List Char) :

parseParen (g + 1 + 1) ('-' :: d :: r) = do let __x ← parseNumeral ('-' :: d :: r) match __x with | (e, r') => parseAfterHead (g + 1) e r'

Used by

theorem

Lean2Js.Parse.parseParen_minusOther

(g : Nat) {d : Char} (hd : d.isDigit = false) (r : List Char) :

parseParen (g + 1 + 1) ('-' :: d :: r) = do let __x ← parseExpr (g + 1) (d :: r) match __x with | (e, r) => do let r ← expect [')'] r pure (Js.Expr.unary "-" e, r)

Used by

theorem

Lean2Js.Parse.parseParen_fallback

(g : Nat) {c : Char} (h1 : c ≠ '!') (h2 : c ≠ '-') (cs : List Char) (harrow : parseArrowHead (g + 1) (c :: cs) = none) :

parseParen (g + 1 + 1) (c :: cs) = do let __x ← parseExpr (g + 1) (c :: cs) match __x with | (e, r) => parseAfterHead (g + 1) e r

Used by

theorem

Lean2Js.Parse.parseAfterHead_member

(g : Nat) (e : Js.Expr) (field : String) (hfield : okName field = true) (rest : List Char) (hrest : notIdentFirst rest) :

parseAfterHead (g + 1) e (')' :: '.' :: (field.toList ++ rest)) = some (e.member field, rest)

Used by

theorem

Lean2Js.Parse.parseAfterHead_negate

(g : Nat) (e : Js.Expr) {c : Char} (hc : c ≠ '.') (rest : List Char) :

parseAfterHead (g + 1) e (')' :: c :: rest) = Option.map (fun (e : Js.Expr) => (Js.Expr.unary "-" e, c :: rest)) (negateNumeral e)

Used by

theorem

Lean2Js.Parse.parseAfterHead_negate_nil

(g : Nat) (e : Js.Expr) :

parseAfterHead (g + 1) e [')'] = Option.map (fun (e : Js.Expr) => (Js.Expr.unary "-" e, [])) (negateNumeral e)

Used by

theorem

Lean2Js.Parse.parseAfterHead_neg

(g : Nat) (e : Js.Expr) (rest : List Char) (hrest : Sep rest) :

parseAfterHead (g + 1) e (')' :: rest) = Option.map (fun (e : Js.Expr) => (Js.Expr.unary "-" e, rest)) (negateNumeral e)

Used by

theorem

Lean2Js.Parse.parseAfterHead_binary

(g : Nat) (e : Js.Expr) {c : Char} (hc : c ≠ '?') (cs : List Char) :

parseAfterHead (g + 1) e (' ' :: c :: cs) = do let __x ← parseOp (c :: cs) match __x with | (op, r) => do let r ← expect [' '] r let __x ← parseExpr g r match __x with | (rhs, r) => do let r ← expect [')'] r pure (Js.Expr.binary op e rhs, r)

Used by

The roundtrip on expressions #

Each case reads back exactly what the matching printer branch wrote. The fuel is bounded by the length of the text, which every recursive call shortens by at least the delimiters around it.

theorem

Lean2Js.Parse.parseExpr_append

(e : Js.Expr) (he : RenderableExpr e = true) (f : Nat) (hf : e.render.toList.length < f) (rest : List Char) (hrest : Sep rest) :

parseExpr f (e.render.toList ++ rest) = some (e, rest)

Used by

theorem

Lean2Js.Parse.parseParen_head

(h : Js.Expr) (hh : RenderableExpr h = true) (f : Nat) (hf : h.render.toList.length < f) (tail : List Char) (hsep : Sep tail) (hafter : AfterHead tail) :

parseParen (f + 1) (h.render.toList ++ tail) = parseAfterHead f h tail

Used by

theorem

Lean2Js.Parse.parseLambdaCall_append

(arr : Js.Expr) (b : String) (body : Js.Expr) (harr : RenderableExpr arr = true) (hb : okName b = true) (hbody : RenderableExpr body = true) (k : Nat) (hk1 : arr.render.toList.length < k) (hk2 : body.render.toList.length < k) (rest : List Char) (hrest : Sep rest) :

parseLambdaCall (k + 1) ('(' :: (arr.render.toList ++ ',' :: ' ' :: '(' :: (b.toList ++ ')' :: ' ' :: '=' :: '>' :: ' ' :: '(' :: (body.render.toList ++ ')' :: ')' :: rest)))) = some (arr, b, body, rest)

Used by

theorem

Lean2Js.Parse.parseExprList_append

(es : List Js.Expr) (hes : RenderableList es = true) (f : Nat) (hf : (Js.Expr.renderList es).toList.length + 1 < f) (close : Char) (hclose : close = ')' ∨ close = ']') (rest : List Char) :

parseExprList f close ((Js.Expr.renderList es).toList ++ close :: rest) = some (es, close :: rest)

Used by

theorem

Lean2Js.Parse.parseObjFields_append

(fs : List (String × Js.Expr)) (hfs : RenderablePairs fs = true) (f : Nat) (hf : (Js.Expr.renderFields fs).toList.length + 1 < f) (rest : List Char) :

parseObjFields f ((Js.Expr.renderFields fs).toList ++ ' ' :: '}' :: rest) = some (fs, ' ' :: '}' :: rest)

Used by

theorem

Lean2Js.Parse.parseEntries_append

(es : List (String × Js.Expr)) (hes : RenderablePairs es = true) (f : Nat) (hf : (Js.Expr.renderEntries es).toList.length + 1 < f) (rest : List Char) :

parseEntries f ((Js.Expr.renderEntries es).toList ++ ']' :: rest) = some (es, ']' :: rest)

Used by

Statements, functions and the module #

def

Lean2Js.Parse.RenderableStmt

:

Js.Stmt → Bool

Equations

Lean2Js.Parse.RenderableStmt (Lean2Js.Js.Stmt.const name val) = (Lean2Js.okName name && Lean2Js.Parse.RenderableExpr val)
Lean2Js.Parse.RenderableStmt (Lean2Js.Js.Stmt.ret e) = Lean2Js.Parse.RenderableExpr e

Instances For

Used by

def

Lean2Js.Parse.noCommentClose

:

List Char → Bool

A doc comment goes into /** */ unescaped, so it must not close the comment itself.

Equations

Lean2Js.Parse.noCommentClose [] = true
Lean2Js.Parse.noCommentClose [head] = true
Lean2Js.Parse.noCommentClose [head, head_1] = true
Lean2Js.Parse.noCommentClose [head, head_1, head_2] = true
Lean2Js.Parse.noCommentClose (a :: b :: c :: d :: rest) = (!(' ' == a && '*' == b && '/' == c && '\n' == d) && Lean2Js.Parse.noCommentClose (b :: c :: d :: rest))

Instances For

Used by

def

Lean2Js.Parse.RenderableFunc

(fn : Js.Func) :

Equations

Lean2Js.Parse.RenderableFunc fn = (Lean2Js.okName fn.name && fn.params.all Lean2Js.okName && fn.body.all Lean2Js.Parse.RenderableStmt && Lean2Js.Parse.noCommentClose fn.doc.toList)

Instances For

Used by

def

Lean2Js.Parse.RenderableModule

(m : Js.Module) :

Equations

Lean2Js.Parse.RenderableModule m = m.funcs.all Lean2Js.Parse.RenderableFunc

Instances For

Used by

theorem

Lean2Js.Parse.render_const_toList

(name : String) (val : Js.Expr) :

(Js.Stmt.const name val).render.toList = ' ' :: ' ' :: 'c' :: 'o' :: 'n' :: 's' :: 't' :: ' ' :: (name.toList ++ ' ' :: '=' :: ' ' :: (val.render.toList ++ [';']))

Used by

theorem

Lean2Js.Parse.render_ret_toList

(e : Js.Expr) :

(Js.Stmt.ret e).render.toList = ' ' :: ' ' :: 'r' :: 'e' :: 't' :: 'u' :: 'r' :: 'n' :: ' ' :: (e.render.toList ++ [';'])

Used by

theorem

Lean2Js.Parse.render_stmt_head

(st : Js.Stmt) :

∃ (x : List Char), st.render.toList = ' ' :: ' ' :: x

Used by

theorem

Lean2Js.Parse.stmtAll_nil_toList

:

(Js.Stmt.renderAll []).toList = []

Used by

theorem

Lean2Js.Parse.stmtAll_one_toList

(st : Js.Stmt) :

(Js.Stmt.renderAll [st]).toList = st.render.toList

Used by

theorem

Lean2Js.Parse.stmtAll_cons_toList

(st a : Js.Stmt) (rest : List Js.Stmt) :

(Js.Stmt.renderAll (st :: a :: rest)).toList = st.render.toList ++ '\n' :: (Js.Stmt.renderAll (a :: rest)).toList

Used by

theorem

Lean2Js.Parse.funcAll_nil_toList

:

(Js.Func.renderAll []).toList = []

Used by

theorem

Lean2Js.Parse.funcAll_cons_toList

(fn : Js.Func) (rest : List Js.Func) :

(Js.Func.renderAll (fn :: rest)).toList = fn.render.toList ++ '\n' :: '\n' :: (Js.Func.renderAll rest).toList

Used by

theorem

Lean2Js.Parse.render_func_toList

(fn : Js.Func) :

fn.render.toList = (if fn.doc.isEmpty = true then [] else '/' :: '*' :: '*' :: ' ' :: (fn.doc.toList ++ [' ', '*', '/', '\n'])) ++ ((if fn.exported = true then ['e', 'x', 'p', 'o', 'r', 't', ' '] else []) ++ 'f' :: 'u' :: 'n' :: 'c' :: 't' :: 'i' :: 'o' :: 'n' :: ' ' :: (fn.name.toList ++ '(' :: ((Js.renderNames fn.params).toList ++ ')' :: ' ' :: '{' :: '\n' :: ((Js.Stmt.renderAll fn.body).toList ++ ['\n', '}']))))

Used by

theorem

Lean2Js.Parse.render_func_split

(fn : Js.Func) (rest : List Char) :

fn.render.toList ++ rest = (if fn.doc.isEmpty = true then [] else '/' :: '*' :: '*' :: ' ' :: (fn.doc.toList ++ [' ', '*', '/', '\n'])) ++ ((if fn.exported = true then ['e', 'x', 'p', 'o', 'r', 't', ' '] else []) ++ 'f' :: 'u' :: 'n' :: 'c' :: 't' :: 'i' :: 'o' :: 'n' :: ' ' :: (fn.name.toList ++ '(' :: ((Js.renderNames fn.params).toList ++ ')' :: ' ' :: '{' :: '\n' :: ((Js.Stmt.renderAll fn.body).toList ++ '\n' :: '}' :: rest))))

Used by

theorem

Lean2Js.Parse.render_func_length

(fn : Js.Func) :

(Js.renderNames fn.params).toList.length + (Js.Stmt.renderAll fn.body).toList.length + 13 ≤ fn.render.toList.length

Used by

Reading a doc comment back #

theorem

Lean2Js.Parse.takeUntil_close

(rest : List Char) :

takeUntil [' ', '*', '/', '\n'] ([' ', '*', '/', '\n'] ++ rest) = some ([], [' ', '*', '/', '\n'] ++ rest)

Used by

theorem

Lean2Js.Parse.noCommentClose_tail

{a : Char} {d : List Char} (h : noCommentClose (a :: d) = true) :

noCommentClose d = true

Used by

theorem

Lean2Js.Parse.takeUntil_doc

(d : List Char) (h : noCommentClose d = true) (rest : List Char) :

takeUntil [' ', '*', '/', '\n'] (d ++ ([' ', '*', '/', '\n'] ++ rest)) = some (d, [' ', '*', '/', '\n'] ++ rest)

Used by

theorem

Lean2Js.Parse.expect_docOpen

(Y : List Char) :

expect ['/', '*', '*', ' '] ('/' :: '*' :: '*' :: ' ' :: Y) = some Y

Used by

theorem

Lean2Js.Parse.expect_docClose

(Y : List Char) :

expect [' ', '*', '/', '\n'] (' ' :: '*' :: '/' :: '\n' :: Y) = some Y

Used by

theorem

Lean2Js.Parse.takeUntil_doc'

(d : List Char) (h : noCommentClose d = true) (rest : List Char) :

takeUntil [' ', '*', '/', '\n'] (d ++ ' ' :: '*' :: '/' :: '\n' :: rest) = some (d, ' ' :: '*' :: '/' :: '\n' :: rest)

The shape a doc comment takes inside a rendering, where the closing marker is spelled out.

Used by

The roundtrip on statements, functions and the module #

theorem

Lean2Js.Parse.parseStmt_append

(st : Js.Stmt) (hst : RenderableStmt st = true) (f : Nat) (hf : st.render.toList.length < f) (rest : List Char) :

parseStmt f (st.render.toList ++ rest) = some (st, rest)

Used by

theorem

Lean2Js.Parse.stmtAll_head

(ss : List Js.Stmt) (h : ss ≠ []) :

∃ (z : List Char), (Js.Stmt.renderAll ss).toList = ' ' :: ' ' :: z

Used by

theorem

Lean2Js.Parse.parseStmts_step

(f : Nat) (cs x : List Char) (h : cs = ' ' :: ' ' :: x) :

parseStmts (f + 1) cs = do let __x ← parseStmt f cs match __x with | (st, r) => match r with | '\n' :: '}' :: tail => pure ([st], r) | '\n' :: r' => do let __x ← parseStmts f r' match __x with | (ss, r') => pure (st :: ss, r') | x => none

Used by

theorem

Lean2Js.Parse.parseStmts_append

(ss : List Js.Stmt) (hss : ss.all RenderableStmt = true) (f : Nat) (hf : (Js.Stmt.renderAll ss).toList.length + 1 < f) (rest : List Char) :

parseStmts f ((Js.Stmt.renderAll ss).toList ++ '\n' :: '}' :: rest) = some (ss, '\n' :: '}' :: rest)

Used by

theorem

Lean2Js.Parse.parseFunc_append

(fn : Js.Func) (hfn : RenderableFunc fn = true) (f : Nat) (hf : fn.render.toList.length + 1 < f) (rest : List Char) :

parseFunc f (fn.render.toList ++ rest) = some (fn, rest)

Used by

theorem

Lean2Js.Parse.parseFuncs_step

(f : Nat) (cs : List Char) (c : Char) (x : List Char) (h : cs = c :: x) :

parseFuncs (f + 1) cs = do let __x ← parseFunc f cs match __x with | (fn, r) => do let r ← expect ['\n', '\n'] r let __x ← parseFuncs f r match __x with | (fs, r) => pure (fn :: fs, r)

Used by

theorem

Lean2Js.Parse.expect_self

(l : List Char) :

expect l l = some []

Used by

theorem

Lean2Js.Parse.render_func_head

(fn : Js.Func) :

∃ (c : Char ), ∃ (x : List Char), fn.render.toList = c :: x

Used by

theorem

Lean2Js.Parse.parseFuncs_append

(fs : List Js.Func) (hfs : fs.all RenderableFunc = true) (f : Nat) (hf : (Js.Func.renderAll fs).toList.length + 1 < f) :

parseFuncs f (Js.Func.renderAll fs).toList = some (fs, [])

Used by

theorem

Lean2Js.Parse.parseModule_of

(P : List Char) (hP : 1 < P.length) (fs : List Js.Func) (hfs : fs.all RenderableFunc = true) :

(do let r ← expect P (P ++ (Js.Func.renderAll fs).toList) let __x ← parseFuncs (P ++ (Js.Func.renderAll fs).toList).length r match __x with | (fs', r) => if r.isEmpty = true then some { funcs := fs' } else none) = some { funcs := fs }

The prelude is a long literal, so it is kept opaque here: nothing about the roundtrip depends on what it says, only on its being the same text on both sides and on its leaving the reader more fuel than the functions after it need.

Used by

theorem

Lean2Js.Parse.preamble_length

:

1 < Js.preamble.toList.length

The prelude opens with a comment, so it leaves the reader more fuel than the functions after it need.

Used by

theorem

Lean2Js.Parse.parseModule_render

(m : Js.Module) (hm : RenderableModule m = true) :

parseModule m.render.toList = some m

The file the compiler writes reads back as the module it was compiled from.

Used by