Lean2Js.HelperProof

(c : String) :

ofRes (Except.error c) = Res.thrown c

Used by

theorem

Lean2Js.HelperSem.applyVal_ext

source

@[simp]

(ext : Ext) (f i : Nat) (args : List Val) :

applyVal ext (f + 1) (Val.ext i) args = ext i args

Applying a function the caller supplied. walk reduces this rather than applyVal itself, so that a call to a closure — which is what __has hands __all and __find — stays folded until a lemma about that closure is available.

Used by

theorem

Lean2Js.HelperSem.applyVal_lam

source

(ext : Ext) (f : Nat) (ps : List String) (body : Helper.Expr) (cenv : Env) (args : List Val) (h : ps.length = args.length) :

applyVal ext (f + 1) (Val.lam ps body cenv) args = evalExpr ext f (bindAll ps args ++ cenv) body

Used by

def

Lean2Js.HelperSem.tacticWalk

source

Lean.ParserDescr

Walks the evaluator down a concrete tree. Everything it unfolds is either the evaluator itself or a table the evaluator consults; nothing about a helper's meaning is in here.

Equations

Lean2Js.HelperSem.tacticWalk = Lean.ParserDescr.node `Lean2Js.HelperSem.tacticWalk 1024 (Lean.ParserDescr.nonReservedSymbol "walk" false)

Instances For

Used by

theorem

Lean2Js.HelperSem.callDef_expr

source

{ext : Ext} {f : Nat} {name : String} {args : List Val} {d : Helper.Def} {e : Helper.Expr} (hd : List.find? (fun (x : Helper.Def) => x.name == name) Helper.defs = some d) (hb : d.body = Helper.Body.expr e) (hn : d.params.length = args.length) :

callDef ext (f + 1) name args = evalExpr ext f (bindAll d.params args) e

Used by

theorem

Lean2Js.HelperSem.callDef_block

source

{ext : Ext} {f : Nat} {name : String} {args : List Val} {d : Helper.Def} {ss : List Helper.Stmt} (hd : List.find? (fun (x : Helper.Def) => x.name == name) Helper.defs = some d) (hb : d.body = Helper.Body.block ss) (hn : d.params.length = args.length) :

callDef ext (f + 1) name args = match evalStmts ext f (bindAll d.params args) ss with | Res.ok (Outcome.ret v) => Res.ok v | Res.ok v => Res.stuck | Res.thrown c => Res.thrown c | Res.stuck => Res.stuck

source

(ext : Ext) (a b : Int) (f : Nat) :

source

(ext : Ext) (x : String) (f : Nat) :

callDef ext (f + 5) "__chars" [Val.str x] = Res.ok (Val.arr (List.map (fun (c : Char) => Val.str c.toString) x.toList))

Used by

theorem

Lean2Js.HelperSem.calls_cp

source

(ext : Ext) (c : Char) (f : Nat) :

callDef ext (f + 5) "__cp" [Val.str c.toString] = Res.ok (Val.num ↑c.toNat)

Used by

theorem

Lean2Js.HelperSem.find_str

source

List.find? (fun (x : Helper.Def) => x.name == "__str") Helper.defs = some Helper.str

Used by

theorem

Lean2Js.HelperSem.calls_str

source

(ext : Ext) (a : Int) (f : Nat) (hlo : Js.Runtime.safeMin ≤ a) (hhi : a ≤ Js.Runtime.safeMax) :

callDef ext (f + 5) "__str" [Val.num a] = Res.ok (Val.str (toString a))

Used by

theorem

source

(ext : Ext) (v : Val) (f : Nat) :

callDef ext (f + 8) "__isObj" [v] = Res.ok (Val.bool (match v with | Val.obj fields => true | Val.dict entries => true | x => false))

source

(ext : Ext) (xs acc : List Val) (A B : Val) (f : Nat) :

evalFor ext (f + xs.length + 3) [("out", Val.arr acc), ("a", A), ("b", B)] "v" xs [Helper.Stmt.push "out" (Helper.Expr.var "v")] = Res.ok (Outcome.next [("out", Val.arr (acc ++ xs)), ("a", A), ("b", B)])

Used by

theorem

Lean2Js.HelperSem.calls_aconcat

source

(ext : Ext) (a b : List Val) (f : Nat) :

callDef ext (f + a.length + b.length + 8) "__aconcat" [Val.arr a, Val.arr b] = Res.ok (Val.arr (a ++ b))

Used by

theorem

Lean2Js.HelperSem.areverse_loop

source

(ext : Ext) (xs ys acc : List Val) (f : Nat) (h : ys.length ≤ xs.length) :

evalFor ext (f + ys.length + 4) [("i", Val.num ↑ys.length), ("out", Val.arr acc), ("xs", Val.arr xs)] "v" ys [Helper.Stmt.setVar "i" (Helper.Expr.bin "-" (Helper.Expr.var "i") (Helper.Expr.num 1)), Helper.Stmt.push "out" ((Helper.Expr.var "xs").index (Helper.Expr.var "i"))] = Res.ok (Outcome.next [("i", Val.num 0), ("out", Val.arr (acc ++ (List.take ys.length xs).reverse)), ("xs", Val.arr xs)])

The loop reads xs[i - 1] while iterating over xs itself, so the induction runs on a second list that only carries the count still to go, and ys.length ≤ xs.length is what keeps that index in range.

Used by

theorem

Lean2Js.HelperSem.calls_areverse

source

(ext : Ext) (xs : List Val) (f : Nat) :

callDef ext (f + xs.length + 9) "__areverse" [Val.arr xs] = Res.ok (Val.arr xs.reverse)

Used by

def

Lean2Js.HelperSem.isSpaceStr

source

(s : String) :

Bool

The four strings __ws accepts. __lead counts them off the front of an array of strings; that the array is one string per code point is what __chars supplies, and calls_trim is where the two meet.

Equations

Lean2Js.HelperSem.isSpaceStr s = (s == " " || s == "\t" || s == "\n" || s == "\x0d")

a ++ x.toString ++ String.ofList l = a ++ String.ofList (x :: l)

Used by

theorem

source

List.find? (fun (x : Helper.Def) => x.name == "__lower") Helper.defs = some Helper.lower

Used by

theorem

Lean2Js.HelperSem.lower_loop

source

(ext : Ext) (cs : List Char) (acc : String) (S : Val) (f : Nat) :

evalFor ext (f + cs.length + 6) [("out", Val.str acc), ("s", S)] "c" (List.map (fun (c : Char) => Val.str c.toString) cs) [Helper.Stmt.setVar "out" (Helper.Expr.bin "+" (Helper.Expr.var "out") (((Helper.Expr.bin ">=" (Helper.Expr.var "c") (Helper.Expr.str "A")).andAlso (Helper.Expr.bin "<=" (Helper.Expr.var "c") (Helper.Expr.str "Z"))).cond ((Helper.Expr.var "c").method "toLowerCase" []) (Helper.Expr.var "c")))] = Res.ok (Outcome.next [("out", Val.str (acc ++ String.ofList (List.map (fun (c : Char) => if (decide ('A' ≤ c) && decide (c ≤ 'Z')) = true then Char.ofNat (c.toNat + 32) else c) cs))), ("s", S)])

Used by

theorem

Lean2Js.HelperSem.calls_lower

source

(ext : Ext) (x : String) (f : Nat) :

source

List.find? (fun (x : Helper.Def) => x.name == "__startsAt") Helper.defs = some Helper.startsAt

Used by

theorem

Lean2Js.HelperSem.find_indexOf

source

List.find? (fun (x : Helper.Def) => x.name == "__indexOf") Helper.defs = some Helper.indexOf

Used by

theorem

Lean2Js.HelperSem.find_join

source

List.find? (fun (x : Helper.Def) => x.name == "__join") Helper.defs = some Helper.join

Used by

theorem

Lean2Js.HelperSem.calls_startsAt

source

(ext : Ext) (cs : List Char) (t : String) (f : Nat) :

callDef ext (f + 8) "__startsAt" [Val.arr (List.map (fun (c : Char) => Val.str c.toString) cs), Val.str t] = Res.ok (Val.bool (t.toList.isPrefixOf cs))

Used by

def

Lean2Js.HelperSem.scanSteps

source

(t : List Char) :

List Char → Nat

How far the loop in __indexOf walks: to the first position the needle sits at, or off the end.

Equations

Lean2Js.HelperSem.scanSteps t [] = 0
Lean2Js.HelperSem.scanSteps t (c :: rest) = if t.isPrefixOf (c :: rest) = true then 0 else Lean2Js.HelperSem.scanSteps t rest + 1

callDef ext (f + ss.length + 20) "__join" [Val.arr (List.map Val.str ss), Val.str sep] = Res.ok (Val.str (Js.Runtime.strJoin ss sep))

Used by

theorem

Lean2Js.HelperSem.find_rep

source

List.find? (fun (x : Helper.Def) => x.name == "__rep") Helper.defs = some Helper.rep

Used by

theorem

Lean2Js.HelperSem.find_repeat

source

List.find? (fun (x : Helper.Def) => x.name == "__repeat") Helper.defs = some Helper.repeat

Used by

theorem

Lean2Js.HelperSem.calls_rep

source

(ext : Ext) (s : String) (n : Int) (f : Nat) :

callDef ext (f + 4 * n.toNat + 16) "__rep" [Val.str s, Val.num n] = Res.ok (Val.str (Js.Runtime.strRepeatFrom s n.toNat))

Used by

theorem

Lean2Js.HelperSem.find_range

source

List.find? (fun (x : Helper.Def) => x.name == "__range") Helper.defs = some Helper.range

Used by

theorem

Lean2Js.HelperSem.range_loop

source

(ext : Ext) (xs acc : List Val) (N : Val) (f : Nat) :

evalFor ext (f + xs.length + 3) [("out", Val.arr acc), ("n", N)] "c" xs [Helper.Stmt.push "out" ((Helper.Expr.var "out").field "length")] = Res.ok (Outcome.next [("out", Val.arr (acc ++ List.map (fun (k : Nat) => Val.num (Int.ofNat k)) (List.range' acc.length xs.length))), ("n", N)])

The loop keeps no counter of its own: it pushes the length the array has reached, so the element it adds is the index it is at. That is why the induction runs on the accumulator as well as on what is left to walk, and why the numbers start where the accumulator ends rather than at zero.

Used by

theorem

Lean2Js.HelperSem.calls_range

source

(ext : Ext) (n : Int) (f : Nat) :

callDef ext (f + 5 * n.toNat + 30) "__range" [Val.num n] = Res.ok (Val.arr (List.map (fun (k : Nat) => Val.num (Int.ofNat k)) (List.range n.toNat)))

Used by

theorem

Lean2Js.HelperSem.calls_repeat

source

(ext : Ext) (s : String) (n : Int) (f : Nat) :

callDef ext (f + 4 * n.toNat + 45) "__repeat" [Val.str s, Val.num n] = if s.toList.length = 0 then Res.ok (Val.str "") else if Js.Runtime.safeMax < ↑s.toList.length * n then Res.thrown "int53Overflow" else Res.ok (Val.str (Js.Runtime.strRepeatFrom s n.toNat))

Used by

theorem

Lean2Js.HelperSem.strcmp_loop

source

(ext : Ext) (bs cs : List Char) (i : Nat) (X A B : Val) (f : Nat) :

evalFor ext (f + cs.length + 12) [("i", Val.num ↑i), ("y", Val.arr (List.map (fun (c : Char) => Val.str c.toString) bs)), ("x", X), ("a", A), ("b", B)] "c" (List.map (fun (c : Char) => Val.str c.toString) cs) [Helper.Stmt.ifThen (Helper.Expr.bin ">=" (Helper.Expr.var "i") ((Helper.Expr.var "y").field "length")) [Helper.Stmt.ret (Helper.Expr.num 1)], Helper.Stmt.const "d" (Helper.Expr.bin "-" (Helper.Expr.call "__cp" [Helper.Expr.var "c"]) (Helper.Expr.call "__cp" [(Helper.Expr.var "y").index (Helper.Expr.var "i")])), Helper.Stmt.ifThen (Helper.Expr.bin "!==" (Helper.Expr.var "d") (Helper.Expr.num 0)) [Helper.Stmt.ret ((Helper.Expr.bin "<" (Helper.Expr.var "d") (Helper.Expr.num 0)).cond (Helper.Expr.num (-1)) (Helper.Expr.num 1))], Helper.Stmt.setVar "i" (Helper.Expr.bin "+" (Helper.Expr.var "i") (Helper.Expr.num 1))] = if cs.isPrefixOf (List.drop i bs) = true then Res.ok (Outcome.next [("i", Val.num (↑i + ↑cs.length)), ("y", Val.arr (List.map (fun (c : Char) => Val.str c.toString) bs)), ("x", X), ("a", A), ("b", B)]) else Res.ok (Outcome.ret (Val.num (if compare cs (List.drop i bs) = Ordering.lt then -1 else 1)))

Used by

theorem

Lean2Js.HelperSem.find_strcmp

source

List.find? (fun (x : Helper.Def) => x.name == "__strcmp") Helper.defs = some Helper.strcmp

Used by

theorem

Lean2Js.HelperSem.calls_strcmp

source

(ext : Ext) (x y : String) (f : Nat) :

callDef ext (f + x.toList.length + 17) "__strcmp" [Val.str x, Val.str y] = Res.ok (Val.num (Js.Runtime.strcmp x y))

Used by

Deleting a key #

The loop is stated as the foldl it runs, with no hypothesis about the dictionary. That it agrees with dropping the key — JsSem's filter — needs the keys to be distinct, which is a fact about the values the generated code hands over rather than about this helper, so it is a separate lemma.

theorem

Lean2Js.HelperSem.find_ddelete

source

List.find? (fun (x : Helper.Def) => x.name == "__ddelete") Helper.defs = some Helper.ddelete

Used by

def

Lean2Js.HelperSem.dropStep

source

(es : List (String × Val)) (k : String) (a : List (String × Val)) (key : String) :

List (String × Val)

Equations

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

Instances For

Used by

theorem

Lean2Js.HelperSem.ddelete_loop

source

(ext : Ext) (es acc : List (String × Val)) (k : String) (ks : List String) (f : Nat) :

evalFor ext (f + ks.length + 6) [("out", Val.dict acc), ("d", Val.dict es), ("k", Val.str k)] "key" (List.map Val.str ks) [Helper.Stmt.ifThen (Helper.Expr.bin "!==" (Helper.Expr.var "key") (Helper.Expr.var "k")) [Helper.Stmt.setKey "out" (Helper.Expr.var "key") ((Helper.Expr.var "d").method "get" [Helper.Expr.var "key"])]] = Res.ok (Outcome.next [("out", Val.dict (List.foldl (dropStep es k) acc ks)), ("d", Val.dict es), ("k", Val.str k)])

Used by

theorem

Lean2Js.HelperSem.calls_ddelete

source

(ext : Ext) (es : List (String × Val)) (k : String) (f : Nat) :

callDef ext (f + es.length + 12) "__ddelete" [Val.dict es, Val.str k] = Res.ok (Val.dict (List.foldl (dropStep es k) [] (List.map (fun (x : String × Val) => x.fst) es)))

Used by

theorem

Lean2Js.HelperSem.ddelete_fold

source

(es : List (String × Val)) (k : String) (h : Js.keysDistinct (List.map (fun (x : String × Val) => x.fst) es) = true) :

List.foldl (dropStep es k) [] (List.map (fun (x : String × Val) => x.fst) es) = List.filter (fun (x : String × Val) => x.fst != k) es

Used by

theorem

Lean2Js.HelperSem.calls_ddelete_distinct

source

(ext : Ext) (es : List (String × Val)) (k : String) (f : Nat) (h : Js.keysDistinct (List.map (fun (x : String × Val) => x.fst) es) = true) :

callDef ext (f + es.length + 12) "__ddelete" [Val.dict es, Val.str k] = Res.ok (Val.dict (List.filter (fun (x : String × Val) => x.fst != k) es))

What JsSem.helper says, for the dictionaries a Map can actually hold.

Used by

Trimming #

__trim slices between two counts, where strTrim drops from both ends. The two agree, and the only place they could come apart is a string that is whitespace throughout: there the slice is empty because its bounds cross, not because the counts line up, so the proof splits that case off first.

theorem

Lean2Js.HelperSem.find_trim

source

List.find? (fun (x : Helper.Def) => x.name == "__trim") Helper.defs = some Helper.trim

Used by

theorem

Lean2Js.HelperSem.calls_lead_chars

source

(ext : Ext) (cs : List Char) (f : Nat) :

callDef ext (f + cs.length + 18) "__lead" [Val.arr (List.map (fun (c : Char) => Val.str c.toString) cs)] = Res.ok (Val.num ↑(List.takeWhile Js.Runtime.isSpace cs).length)

Used by

theorem

Lean2Js.HelperSem.calls_trim

source

(ext : Ext) (x : String) (f : Nat) :

callDef ext (f + x.toList.length + 26) "__trim" [Val.str x] = Res.ok (Val.str (Js.Runtime.strTrim x))

Used by

Traversals #

The callback is ext, so what these compute is stated as a walk of the list that calls it once per element and stops at the first thrown. That is the shape JsSem's evalMapJs and its siblings already have, which is what lets the two be put side by side.

theorem

Lean2Js.HelperSem.find_map

source

List.find? (fun (x : Helper.Def) => x.name == "__map") Helper.defs = some Helper.map

Used by

def

Lean2Js.HelperSem.extMap

source

(ext : Ext) (i : Nat) :

List Val → Res (List Val)

Equations

Lean2Js.HelperSem.extMap ext i [] = Lean2Js.HelperSem.Res.ok []
Lean2Js.HelperSem.extMap ext i (x_1 :: rest) = do let v ← ext i [x_1] let vs ← Lean2Js.HelperSem.extMap ext i rest Lean2Js.HelperSem.Res.ok (v :: vs)

Instances For

Used by

theorem

Lean2Js.HelperSem.map_loop

source

(ext : Ext) (i : Nat) (xs acc : List Val) (X : Val) (f : Nat) :

evalFor ext (f + xs.length + 4) [("out", Val.arr acc), ("xs", X), ("f", Val.ext i)] "v" xs [Helper.Stmt.push "out" ((Helper.Expr.var "f").apply [Helper.Expr.var "v"])] = (extMap ext i xs).bind fun (ys : List Val) => Res.ok (Outcome.next [("out", Val.arr (acc ++ ys)), ("xs", X), ("f", Val.ext i)])

Used by

theorem

Lean2Js.HelperSem.calls_map

source

(ext : Ext) (i : Nat) (xs : List Val) (f : Nat) :

callDef ext (f + xs.length + 9) "__map" [Val.arr xs, Val.ext i] = (extMap ext i xs).bind fun (ys : List Val) => Res.ok (Val.arr ys)

Used by

theorem

Lean2Js.HelperSem.find_filter

source

List.find? (fun (x : Helper.Def) => x.name == "__filter") Helper.defs = some Helper.filter

Used by

def

Lean2Js.HelperSem.extFilter

source

(ext : Ext) (i : Nat) :

List Val → Res (List Val)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.extFilter ext i [] = Lean2Js.HelperSem.Res.ok []

Instances For

Used by

theorem

Lean2Js.HelperSem.filter_loop

source

(ext : Ext) (i : Nat) (xs acc : List Val) (X : Val) (f : Nat) :

evalFor ext (f + xs.length + 5) [("out", Val.arr acc), ("xs", X), ("f", Val.ext i)] "v" xs [Helper.Stmt.ifThen ((Helper.Expr.var "f").apply [Helper.Expr.var "v"]) [Helper.Stmt.push "out" (Helper.Expr.var "v")]] = (extFilter ext i xs).bind fun (ys : List Val) => Res.ok (Outcome.next [("out", Val.arr (acc ++ ys)), ("xs", X), ("f", Val.ext i)])

Used by

theorem

Lean2Js.HelperSem.calls_filter

source

(ext : Ext) (i : Nat) (xs : List Val) (f : Nat) :

callDef ext (f + xs.length + 10) "__filter" [Val.arr xs, Val.ext i] = (extFilter ext i xs).bind fun (ys : List Val) => Res.ok (Val.arr ys)

Used by

theorem

Lean2Js.HelperSem.find_find

source

List.find? (fun (x : Helper.Def) => x.name == "__find") Helper.defs = some Helper.find

Used by

theorem

Lean2Js.HelperSem.find_all

source

List.find? (fun (x : Helper.Def) => x.name == "__all") Helper.defs = some Helper.all

Used by

theorem

Lean2Js.HelperSem.find_any

source

List.find? (fun (x : Helper.Def) => x.name == "__any") Helper.defs = some Helper.any

Used by

theorem

Lean2Js.HelperSem.find_reduce

source

List.find? (fun (x : Helper.Def) => x.name == "__reduce") Helper.defs = some Helper.reduce

Used by

Callbacks #

__all and __find take a function value. The generated code hands them a function it defined, and __has hands them a closure of its own; the loops below are stated for either, with the fuel a sum over the elements rather than a length, because a closure that recurses does not cost a constant.

def

Lean2Js.HelperSem.valAll

source

(P : Val → Res Val) :

List Val → Res Bool

The walk __all performs: the function value is applied to each element, and the first false stops it. An answer that is not a boolean is a shape the model declines to read.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.valAll P [] = Lean2Js.HelperSem.Res.ok true

Instances For

Used by

def

Lean2Js.HelperSem.valFind

source

(P : Val → Res Val) :

List Val → Res (Option Val)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.valFind P [] = Lean2Js.HelperSem.Res.ok none

Instances For

Used by

def

Lean2Js.HelperSem.sumCost

source

(cost : Val → Nat) :

List Val → Nat

One element's fuel, plus one for the step.

Equations

Lean2Js.HelperSem.sumCost cost [] = 0
Lean2Js.HelperSem.sumCost cost (x_1 :: rest) = cost x_1 + Lean2Js.HelperSem.sumCost cost rest + 1

Instances For

Used by

def

Lean2Js.HelperSem.Answers

source

(ext : Ext) (F : Val) (P : Val → Res Val) (cost : Val → Nat) (xs : List Val) :

Prop

What a loop needs of the function value it was handed: on the elements it will actually see, past its cost there, applying it answers P. An inequality rather than an offset, because the loop applies it with whatever fuel it has left; restricted to the list because the closure __has builds only answers for values smaller than the one it was called on.

Equations

Lean2Js.HelperSem.Answers ext F P cost xs = ∀ (v : Lean2Js.HelperSem.Val), v ∈ xs → ∀ (g : Nat), cost v < g → Lean2Js.HelperSem.applyVal ext g F [v] = P v

Instances For

Used by

def

Lean2Js.HelperSem.extAll

source

(ext : Ext) (i : Nat) :

List Val → Res Bool

Equations

Lean2Js.HelperSem.extAll ext i = Lean2Js.HelperSem.valAll fun (v : Lean2Js.HelperSem.Val) => ext i [v]

Instances For

Used by

def

Lean2Js.HelperSem.extFind

source

(ext : Ext) (i : Nat) :

List Val → Res (Option Val)

Equations

Lean2Js.HelperSem.extFind ext i = Lean2Js.HelperSem.valFind fun (v : Lean2Js.HelperSem.Val) => ext i [v]

callDef ext (f + xs.length + 8) "__all" [Val.arr xs, Val.ext i] = (extAll ext i xs).bind fun (r : Bool) => Res.ok (Val.bool r)

Used by

def

Lean2Js.HelperSem.extAny

source

(ext : Ext) (i : Nat) :

List Val → Res Bool

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.extAny ext i [] = Lean2Js.HelperSem.Res.ok false

Instances For

Used by

theorem

Lean2Js.HelperSem.any_loop

source

(ext : Ext) (i : Nat) (xs : List Val) (X : Val) (f : Nat) :

evalFor ext (f + xs.length + 6) [("xs", X), ("f", Val.ext i)] "v" xs [Helper.Stmt.ifThen ((Helper.Expr.var "f").apply [Helper.Expr.var "v"]) [Helper.Stmt.ret (Helper.Expr.bool true)]] = (extAny ext i xs).bind fun (r : Bool) => if r = true then Res.ok (Outcome.ret (Val.bool true)) else Res.ok (Outcome.next [("xs", X), ("f", Val.ext i)])

Used by

theorem

Lean2Js.HelperSem.calls_any

source

(ext : Ext) (i : Nat) (xs : List Val) (f : Nat) :

callDef ext (f + xs.length + 8) "__any" [Val.arr xs, Val.ext i] = (extAny ext i xs).bind fun (r : Bool) => Res.ok (Val.bool r)

Used by

def

Lean2Js.HelperSem.extReduce

source

(ext : Ext) (i : Nat) :

Val → List Val → Res Val

Equations

Lean2Js.HelperSem.extReduce ext i x✝ [] = Lean2Js.HelperSem.Res.ok x✝
Lean2Js.HelperSem.extReduce ext i x✝ (x_2 :: rest) = (ext i [x✝, x_2]).bind fun (r : Lean2Js.HelperSem.Val) => Lean2Js.HelperSem.extReduce ext i r rest

Instances For

Used by

theorem

Lean2Js.HelperSem.reduce_loop

source

(ext : Ext) (i : Nat) (xs : List Val) (a X I : Val) (f : Nat) :

evalFor ext (f + xs.length + 5) [("acc", a), ("xs", X), ("init", I), ("f", Val.ext i)] "v" xs [Helper.Stmt.setVar "acc" ((Helper.Expr.var "f").apply [Helper.Expr.var "acc", Helper.Expr.var "v"])] = (extReduce ext i a xs).bind fun (r : Val) => Res.ok (Outcome.next [("acc", r), ("xs", X), ("init", I), ("f", Val.ext i)])

Used by

theorem

Lean2Js.HelperSem.calls_reduce

source

(ext : Ext) (i : Nat) (xs : List Val) (a : Val) (f : Nat) :

callDef ext (f + xs.length + 8) "__reduce" [Val.arr xs, a, Val.ext i] = (extReduce ext i a xs).bind fun (r : Val) => Res.ok r

Used by

source

Val → Val → Bool

The order __keyle puts two keys in.

Equations

Lean2Js.HelperSem.valLe (Lean2Js.HelperSem.Val.num a) (Lean2Js.HelperSem.Val.num b) = decide (a ≤ b)
Lean2Js.HelperSem.valLe (Lean2Js.HelperSem.Val.str a) (Lean2Js.HelperSem.Val.str b) = (compare a.toList b.toList != Ordering.gt)
Lean2Js.HelperSem.valLe x✝¹ x✝ = false

Instances For

Used by

theorem

Lean2Js.HelperSem.compare_ne_gt

source

(a b : Int) :

(compare a b != Ordering.gt) = decide (a ≤ b)

Used by

theorem

Lean2Js.HelperSem.compare_strcmp

source

(x y : String) :

compare (Js.Runtime.strcmp x y) 0 = compare x.toList y.toList

Used by

theorem

Lean2Js.HelperSem.calls_keyle_num

source

(ext : Ext) (a b : Int) (f : Nat) :

callDef ext (f + 5) "__keyle" [Val.num a, Val.num b] = Res.ok (Val.bool (valLe (Val.num a) (Val.num b)))

Used by

theorem

Lean2Js.HelperSem.calls_keyle_str

source

(ext : Ext) (x y : String) (f : Nat) :

callDef ext (f + x.toList.length + 22) "__keyle" [Val.str x, Val.str y] = Res.ok (Val.bool (valLe (Val.str x) (Val.str y)))

Used by

def

Lean2Js.HelperSem.keyOf

source

Val → Val

The key a pair carries. __sortBy builds every pair, so the shape is always [key, element].

Equations

Lean2Js.HelperSem.keyOf (Lean2Js.HelperSem.Val.arr (k :: tail)) = k
Lean2Js.HelperSem.keyOf x✝ = Lean2Js.HelperSem.Val.undef

Instances For

Used by

def

Lean2Js.HelperSem.pairLe

source

(a b : Val) :

Bool

Equations

Lean2Js.HelperSem.pairLe a b = Lean2Js.HelperSem.valLe (Lean2Js.HelperSem.keyOf a) (Lean2Js.HelperSem.keyOf b)

Instances For

Used by

def

Lean2Js.HelperSem.Compares

source

(ext : Ext) (kcost : Nat) (vs : List Val) :

Prop

What __merge and __msort need of the pairs they are handed: past a cost of its own, __keyle answers valLe on any two of their keys.

Equations

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

Instances For

Used by

def

Lean2Js.HelperSem.mergeCost

source

(kcost : Nat) :

List Val → Nat

Equations

Lean2Js.HelperSem.mergeCost kcost [] = 3
Lean2Js.HelperSem.mergeCost kcost (x_1 :: rest) = Lean2Js.HelperSem.mergeCost kcost rest + kcost + 12

Instances For

Used by

def

Lean2Js.HelperSem.IsPair

source

(v : Val) :

Prop

Every value the sort moves is a pair __sortBy built.

Equations

Lean2Js.HelperSem.IsPair v = ∃ (k : Lean2Js.HelperSem.Val ), ∃ (e : Lean2Js.HelperSem.Val ), v = Lean2Js.HelperSem.Val.arr [k, e]

xs.length ≤ n → (∀ (v : Val), v ∈ xs → IsPair v) → Compares ext kcost xs → ∃ (c : Nat ), ∀ (f : Nat), callDef ext (f + c) "__msort" [Val.arr xs] = Res.ok (Val.arr (xs.mergeSort pairLe))

Used by

def

Lean2Js.HelperSem.elemOf

source

Val → Val

Equations

Lean2Js.HelperSem.elemOf (Lean2Js.HelperSem.Val.arr [head, e]) = e
Lean2Js.HelperSem.elemOf x✝ = Lean2Js.HelperSem.Val.undef

Instances For

Used by

def

Lean2Js.HelperSem.pairsOf

source

List Val → List Val → List Val

The pairs __sortBy builds: each key in front of the element it was worked out from.

Equations

Lean2Js.HelperSem.pairsOf (k :: ks) (x_2 :: xs) = Lean2Js.HelperSem.Val.arr [k, x_2] :: Lean2Js.HelperSem.pairsOf ks xs
Lean2Js.HelperSem.pairsOf x✝¹ x✝ = []

Equations

Lean2Js.HelperSem.isNumV (Lean2Js.HelperSem.Val.num i) = true
Lean2Js.HelperSem.isNumV x✝ = false

Instances For

Used by

def

Lean2Js.HelperSem.isStrV

source

Val → Bool

Equations

Lean2Js.HelperSem.isStrV (Lean2Js.HelperSem.Val.str s) = true
Lean2Js.HelperSem.isStrV x✝ = false

Instances For

Used by

def

Lean2Js.HelperSem.strLens

source

List Val → Nat

One cost for every comparison of one call, taken over all the keys at once: __strcmp walks the left string, and a bound that holds of each key separately is what the loop needs.

Equations

Lean2Js.HelperSem.strLens [] = 0
Lean2Js.HelperSem.strLens (Lean2Js.HelperSem.Val.str s :: rest) = s.toList.length + Lean2Js.HelperSem.strLens rest
Lean2Js.HelperSem.strLens (x_1 :: rest) = 0 + Lean2Js.HelperSem.strLens rest

List.map elemOf ((pairsOf ks xs).mergeSort pairLe) = List.map (fun (x : Val × Val) => x.snd) ((ks.zip xs).mergeSort fun (a b : Val × Val) => valLe a.fst b.fst)

What __sortBy answers, read in the shape the model of the generated code assumes: the pairs of key and element, ordered by key, with the elements read back out.

Used by

theorem

Lean2Js.HelperSem.valLe_ofJs

source

(a b : Js.JsValue) :

valLe (ofJs a) (ofJs b) = Js.keyLe a b

The order the helpers put two keys in is the order JsSem assumes. Stated for every pair of values rather than for the keys of one call: neither side orders anything but two numbers or two strings.

Used by

Structural equality #

__eq decides a notion of its own, stated below as eqVal, not JsValue.beq. Two divergences, both real and both about values the compiler can produce:

objects are walked key by key with Object.hasOwn, so {a:1,b:2} and {b:2,a:1} are equal here and unequal under beq, which compares the field lists in order;
functions never reach the structural path — typeof says "function", not "object" — so the helper answers false where beq compares the names.

Dictionaries, unlike objects, are compared positionally: the loop checks __dkeys(b)[i] against the key it is on. Both walks look their values up by key in both operands, so the recursion is on lookupV, which is not structurally smaller — hence the well-founded definitions, and the fuel a call needs is a function of the values rather than a constant.

theorem

Lean2Js.HelperSem.sizeOf_lookupV

source

(es : List (String × Val)) (k : String) :

sizeOf (lookupV es k) < sizeOf (Val.obj es)

Used by

theorem

Lean2Js.HelperSem.sizeOf_lookupV_pair

source

(es fs : List (String × Val)) (k : String) :

sizeOf (lookupV es k) + sizeOf (lookupV fs k) < 1 + sizeOf es + (1 + sizeOf fs)

Used by

def

Lean2Js.HelperSem.eqVal

source

@[irreducible]

Val → Val → Bool

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.eqVal (Lean2Js.HelperSem.Val.arr xs) (Lean2Js.HelperSem.Val.arr ys) = (xs.length == ys.length && Lean2Js.HelperSem.eqList xs ys)
Lean2Js.HelperSem.eqVal x✝¹ x✝ = Lean2Js.HelperSem.strictEq x✝¹ x✝

Instances For

Used by

def

Lean2Js.HelperSem.eqList

source

@[irreducible]

List Val → List Val → Bool

Equations

Lean2Js.HelperSem.eqList [] x✝ = true
Lean2Js.HelperSem.eqList (head :: tail) [] = false
Lean2Js.HelperSem.eqList (x_2 :: xs) (y :: ys) = (Lean2Js.HelperSem.eqVal x_2 y && Lean2Js.HelperSem.eqList xs ys)

Instances For

Used by

def

Lean2Js.HelperSem.eqKeys

source

@[irreducible]

(es fs : List (String × Val)) :

List String → List String → Bool

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.eqKeys es fs [] x✝ = true
Lean2Js.HelperSem.eqKeys es fs (head :: tail) [] = false

Instances For

Used by

def

Lean2Js.HelperSem.eqObj

source

@[irreducible]

(es fs : List (String × Val)) :

List String → Bool

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.eqObj es fs [] = true

Instances For

Used by

def

Lean2Js.HelperSem.eqFuel

source

@[irreducible]

Val → Val → Nat

Equations

Lean2Js.HelperSem.eqFuel (Lean2Js.HelperSem.Val.dict es) (Lean2Js.HelperSem.Val.dict fs) = Lean2Js.HelperSem.eqFuelKeys es fs (List.map (fun (x : String × Lean2Js.HelperSem.Val) => x.fst) es) + 32
Lean2Js.HelperSem.eqFuel (Lean2Js.HelperSem.Val.arr xs) (Lean2Js.HelperSem.Val.arr ys) = Lean2Js.HelperSem.eqFuelList xs ys + 32
Lean2Js.HelperSem.eqFuel (Lean2Js.HelperSem.Val.obj es) (Lean2Js.HelperSem.Val.obj fs) = Lean2Js.HelperSem.eqFuelKeys es fs (List.map (fun (x : String × Lean2Js.HelperSem.Val) => x.fst) es) + 32
Lean2Js.HelperSem.eqFuel x✝¹ x✝ = 16

Instances For

Used by

def

Lean2Js.HelperSem.eqFuelList

source

@[irreducible]

List Val → List Val → Nat

Equations

Lean2Js.HelperSem.eqFuelList [] x✝ = 0
Lean2Js.HelperSem.eqFuelList (head :: tail) [] = 0
Lean2Js.HelperSem.eqFuelList (x_2 :: xs) (y :: ys) = Lean2Js.HelperSem.eqFuel x_2 y + 8 + Lean2Js.HelperSem.eqFuelList xs ys

Instances For

Used by

def

Lean2Js.HelperSem.eqFuelKeys

source

@[irreducible]

(es fs : List (String × Val)) :

List String → Nat

Equations

Lean2Js.HelperSem.eqFuelKeys es fs [] = 0
Lean2Js.HelperSem.eqFuelKeys es fs (k :: ks) = Lean2Js.HelperSem.eqFuel (Lean2Js.HelperSem.lookupV es k) (Lean2Js.HelperSem.lookupV fs k) + 8 + Lean2Js.HelperSem.eqFuelKeys es fs ks

Instances For

Used by

theorem

Lean2Js.HelperSem.eq_dict_loop

source

(ext : Ext) (es fs : List (String × Val)) (KS : Val) (hsub : ∀ (k : String) (g : Nat), callDef ext (g + eqFuel (lookupV es k) (lookupV fs k)) "__eq" [lookupV es k, lookupV fs k] = Res.ok (Val.bool (eqVal (lookupV es k) (lookupV fs k)))) (ks pre ls : List String) (f : Nat) :

evalFor ext (f + eqFuelKeys es fs ks + 8) [("i", Val.num ↑pre.length), ("ls", Val.arr (List.map Val.str (pre ++ ls))), ("ks", KS), ("a", Val.dict es), ("b", Val.dict fs)] "key" (List.map Val.str ks) [Helper.Stmt.ifThen (Helper.Expr.bin "!==" ((Helper.Expr.var "ls").index (Helper.Expr.var "i")) (Helper.Expr.var "key")) [Helper.Stmt.ret (Helper.Expr.bool false)], Helper.Stmt.ifThen (Helper.Expr.call "__eq" [(Helper.Expr.var "a").method "get" [Helper.Expr.var "key"], (Helper.Expr.var "b").method "get" [Helper.Expr.var "key"]]).not [Helper.Stmt.ret (Helper.Expr.bool false)], Helper.Stmt.setVar "i" (Helper.Expr.bin "+" (Helper.Expr.var "i") (Helper.Expr.num 1))] = if eqKeys es fs ks ls = true then Res.ok (Outcome.next [("i", Val.num (↑pre.length + ↑ks.length)), ("ls", Val.arr (List.map Val.str (pre ++ ls))), ("ks", KS), ("a", Val.dict es), ("b", Val.dict fs)]) else Res.ok (Outcome.ret (Val.bool false))

Used by

theorem

Lean2Js.HelperSem.eq_arr_loop

source

(ext : Ext) (A : Val) (xs ys pre : List Val) (f : Nat) :

xs.length = ys.length → (∀ (x : Val), x ∈ xs → ∀ (y : Val), y ∈ ys → ∀ (g : Nat), callDef ext (g + eqFuel x y) "__eq" [x, y] = Res.ok (Val.bool (eqVal x y))) → evalFor ext (f + eqFuelList xs ys + 8) [("i", Val.num ↑pre.length), ("a", A), ("b", Val.arr (pre ++ ys))] "v" xs [Helper.Stmt.ifThen (Helper.Expr.call "__eq" [Helper.Expr.var "v", (Helper.Expr.var "b").index (Helper.Expr.var "i")]).not [Helper.Stmt.ret (Helper.Expr.bool false)], Helper.Stmt.setVar "i" (Helper.Expr.bin "+" (Helper.Expr.var "i") (Helper.Expr.num 1))] = if eqList xs ys = true then Res.ok (Outcome.next [("i", Val.num (↑pre.length + ↑xs.length)), ("a", A), ("b", Val.arr (pre ++ ys))]) else Res.ok (Outcome.ret (Val.bool false))

Used by

theorem

Lean2Js.HelperSem.eq_obj_loop

source

evalFor ext (f + eqFuelKeys es fs ks + 8) [("keys", KS), ("a", Val.obj es), ("b", Val.obj fs)] "key" (List.map Val.str ks) [Helper.Stmt.ifThen (Helper.Expr.prim "Object.hasOwn" [Helper.Expr.var "b", Helper.Expr.var "key"]).not [Helper.Stmt.ret (Helper.Expr.bool false)], Helper.Stmt.ifThen (Helper.Expr.call "__eq" [(Helper.Expr.var "a").index (Helper.Expr.var "key"), (Helper.Expr.var "b").index (Helper.Expr.var "key")]).not [Helper.Stmt.ret (Helper.Expr.bool false)]] = if eqObj es fs ks = true then Res.ok (Outcome.next [("keys", KS), ("a", Val.obj es), ("b", Val.obj fs)]) else Res.ok (Outcome.ret (Val.bool false))

Used by

theorem

Lean2Js.HelperSem.find_eq

source

List.find? (fun (x : Helper.Def) => x.name == "__eq") Helper.defs = some Helper.eq

Used by

theorem

Lean2Js.HelperSem.calls_eq

source

(ext : Ext) (a b : Val) (f : Nat) :

callDef ext (f + eqFuel a b) "__eq" [a, b] = Res.ok (Val.bool (eqVal a b))

Used by

theorem

Lean2Js.HelperSem.sizeOf_lookupV_lt

source

(es : List (String × Val)) (k : String) :

sizeOf (lookupV es k) < 1 + sizeOf es

Used by

Entry checks #

def

Lean2Js.HelperSem.tyVal

source

@[irreducible]

Js.TyDesc → Val

The value the descriptor the compiler renders denotes. Js.TyDesc.render writes the text; that the text reads back to this value is the parser's question, not this one.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.tyVal Lean2Js.Js.TyDesc.bool = Lean2Js.HelperSem.Val.arr [Lean2Js.HelperSem.Val.str "bool"]
Lean2Js.HelperSem.tyVal Lean2Js.Js.TyDesc.int53 = Lean2Js.HelperSem.Val.arr [Lean2Js.HelperSem.Val.str "int53"]
Lean2Js.HelperSem.tyVal Lean2Js.Js.TyDesc.uint32 = Lean2Js.HelperSem.Val.arr [Lean2Js.HelperSem.Val.str "uint32"]
Lean2Js.HelperSem.tyVal Lean2Js.Js.TyDesc.string = Lean2Js.HelperSem.Val.arr [Lean2Js.HelperSem.Val.str "string"]
Lean2Js.HelperSem.tyVal Lean2Js.Js.TyDesc.bigint = Lean2Js.HelperSem.Val.arr [Lean2Js.HelperSem.Val.str "bigint"]
Lean2Js.HelperSem.tyVal t.option = Lean2Js.HelperSem.Val.arr [Lean2Js.HelperSem.Val.str "option", Lean2Js.HelperSem.tyVal t]
Lean2Js.HelperSem.tyVal (ok.result err) = Lean2Js.HelperSem.Val.arr [Lean2Js.HelperSem.Val.str "result", Lean2Js.HelperSem.tyVal ok, Lean2Js.HelperSem.tyVal err]
Lean2Js.HelperSem.tyVal t.array = Lean2Js.HelperSem.Val.arr [Lean2Js.HelperSem.Val.str "array", Lean2Js.HelperSem.tyVal t]
Lean2Js.HelperSem.tyVal t.dict = Lean2Js.HelperSem.Val.arr [Lean2Js.HelperSem.Val.str "dict", Lean2Js.HelperSem.tyVal t]
Lean2Js.HelperSem.tyVal t.dictObj = Lean2Js.HelperSem.Val.arr [Lean2Js.HelperSem.Val.str "dictObj", Lean2Js.HelperSem.tyVal t]
Lean2Js.HelperSem.tyVal (Lean2Js.Js.TyDesc.ref up) = Lean2Js.HelperSem.Val.arr [Lean2Js.HelperSem.Val.str "ref", Lean2Js.HelperSem.Val.num ↑up]

Instances For

Used by

def

Lean2Js.HelperSem.tyValFields

source

@[irreducible]

List (String × Js.TyDesc) → List Val

Equations

Instances For

Used by

def

Lean2Js.HelperSem.tyValAlts

source

@[irreducible]

List (String × List (String × Js.TyDesc)) → List Val

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.tyValAlts [] = []

Instances For

Used by

def

Lean2Js.HelperSem.envVals

source

(env : Js.TyEnv) :

List Val

One entry per mu the walk is inside, nearest first, holding what that node bound.

Equations

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

Instances For

Used by

def

Lean2Js.HelperSem.envVal

source

(env : Js.TyEnv) :

Val

The array those entries reach the helpers as.

Equations

Lean2Js.HelperSem.envVal env = Lean2Js.HelperSem.Val.arr (Lean2Js.HelperSem.envVals env)

Instances For

Used by

theorem

Lean2Js.HelperSem.envVals_cons

source

(b : String × Js.TyAlts) (env : Js.TyEnv) :

envVals (b :: env) = Val.arr [Val.str b.fst, Val.arr (tyValAlts b.snd)] :: envVals env

Used by

theorem

Lean2Js.HelperSem.envVals_length

source

(env : Js.TyEnv) :

(envVals env).length = List.length env

Used by

theorem

Lean2Js.HelperSem.envVals_drop

source

(env : Js.TyEnv) (k : Nat) :

envVals (List.drop k env) = List.drop k (envVals env)

Used by

theorem

Lean2Js.HelperSem.envVals_getElem?

source

(env : Js.TyEnv) (k : Nat) :

(envVals env)[k]? = Option.map (fun (b : String × Js.TyAlts) => Val.arr [Val.str b.fst, Val.arr (tyValAlts b.snd)]) env[k]?

Used by

def

Lean2Js.HelperSem.hasV

source

@[irreducible]

(env : Js.TyEnv) :

Val → Js.TyDesc → Bool

What __has decides. An object's field is read by name, with lookupV, exactly as Js.checkTy reads it; has_checkTy below is where the two meet.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.hasV env (Lean2Js.HelperSem.Val.bool b) Lean2Js.Js.TyDesc.bool = true
Lean2Js.HelperSem.hasV env (Lean2Js.HelperSem.Val.num i) Lean2Js.Js.TyDesc.int53 = (decide (Lean2Js.Js.Runtime.safeMin ≤ i) && decide (i ≤ Lean2Js.Js.Runtime.safeMax))
Lean2Js.HelperSem.hasV env (Lean2Js.HelperSem.Val.num i) Lean2Js.Js.TyDesc.uint32 = (decide (0 ≤ i) && decide (i ≤ 4294967295))
Lean2Js.HelperSem.hasV env (Lean2Js.HelperSem.Val.str s) Lean2Js.Js.TyDesc.string = true
Lean2Js.HelperSem.hasV env (Lean2Js.HelperSem.Val.bigint i) Lean2Js.Js.TyDesc.bigint = true
Lean2Js.HelperSem.hasV env (Lean2Js.HelperSem.Val.arr xs) t.array = Lean2Js.HelperSem.hasList env xs t
Lean2Js.HelperSem.hasV env (Lean2Js.HelperSem.Val.dict es) t.dict = Lean2Js.HelperSem.hasEntries env es t
Lean2Js.HelperSem.hasV env (Lean2Js.HelperSem.Val.obj es) t.dictObj = Lean2Js.HelperSem.hasEntries env es t
Lean2Js.HelperSem.hasV env (Lean2Js.HelperSem.Val.dict es) t.dictObj = Lean2Js.HelperSem.hasEntries env es t
Lean2Js.HelperSem.hasV env x✝ (Lean2Js.Js.TyDesc.mu key alts) = Lean2Js.HelperSem.hasV ((key, alts) :: env) x✝ (Lean2Js.Js.TyDesc.ctors key alts)
Lean2Js.HelperSem.hasV env x✝ (Lean2Js.Js.TyDesc.ref up) = match env[up]? with | some b => Lean2Js.HelperSem.hasV (List.drop up env) x✝ (Lean2Js.Js.TyDesc.ctors b.fst b.snd) | none => false
Lean2Js.HelperSem.hasV env x✝¹ x✝ = false

Instances For

Used by

def

Lean2Js.HelperSem.hasList

source

@[irreducible]

(env : Js.TyEnv) :

List Val → Js.TyDesc → Bool

Equations

Lean2Js.HelperSem.hasList env [] x✝ = true
Lean2Js.HelperSem.hasList env (x_2 :: rest) x✝ = (Lean2Js.HelperSem.hasV env x_2 x✝ && Lean2Js.HelperSem.hasList env rest x✝)

Instances For

Used by

def

Lean2Js.HelperSem.hasEntries

source

@[irreducible]

(env : Js.TyEnv) :

List (String × Val) → Js.TyDesc → Bool

Equations

Lean2Js.HelperSem.hasEntries env [] x✝ = true
Lean2Js.HelperSem.hasEntries env ((fst, v) :: rest) x✝ = (Lean2Js.HelperSem.hasV env v x✝ && Lean2Js.HelperSem.hasEntries env rest x✝)

Instances For

Used by

def

Lean2Js.HelperSem.hasFields

source

@[irreducible]

(env : Js.TyEnv) (es : List (String × Val)) :

List (String × Js.TyDesc) → Bool

__hasFields asks the object for each declared field by name. A key the descriptor does not name is never looked at, which is how an object carrying more than the type declares still passes.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.hasFields env es [] = true

Instances For

Used by

def

Lean2Js.HelperSem.hasFuel

source

@[irreducible]

(env : Js.TyEnv) :

Val → Js.TyDesc → Nat

Enough fuel for __has, by the same recursion as hasV. A generous constant per level: the claims are stated for every larger amount, so an upper bound is all a proof needs.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.hasFuel env (Lean2Js.HelperSem.Val.arr xs) t.array = Lean2Js.HelperSem.hasFuelList env xs t + 66
Lean2Js.HelperSem.hasFuel env (Lean2Js.HelperSem.Val.dict es) t.dict = Lean2Js.HelperSem.hasFuelEntries env es t + 4 * es.length + 66
Lean2Js.HelperSem.hasFuel env (Lean2Js.HelperSem.Val.obj es) t.dictObj = Lean2Js.HelperSem.hasFuelEntries env es t + 66
Lean2Js.HelperSem.hasFuel env (Lean2Js.HelperSem.Val.dict es) t.dictObj = Lean2Js.HelperSem.hasFuelEntries env es t + 66
Lean2Js.HelperSem.hasFuel env (Lean2Js.HelperSem.Val.obj es) t.option = Lean2Js.HelperSem.hasFuelFields env es [("value", t)] + 66
Lean2Js.HelperSem.hasFuel env (Lean2Js.HelperSem.Val.obj es) (ok.result err) = Lean2Js.HelperSem.hasFuelFields env es [("value", ok)] + Lean2Js.HelperSem.hasFuelFields env es [("error", err)] + 66
Lean2Js.HelperSem.hasFuel env (Lean2Js.HelperSem.Val.obj es) (Lean2Js.Js.TyDesc.ctors key alts) = Lean2Js.HelperSem.hasFuelAlts env es alts + 5 * alts.length + 66
Lean2Js.HelperSem.hasFuel env x✝ (Lean2Js.Js.TyDesc.ctors key alts) = 5 * alts.length + 66
Lean2Js.HelperSem.hasFuel env x✝ (Lean2Js.Js.TyDesc.mu key alts) = Lean2Js.HelperSem.hasFuel ((key, alts) :: env) x✝ (Lean2Js.Js.TyDesc.ctors key alts) + 2 * List.length env + 200
Lean2Js.HelperSem.hasFuel env x✝¹ x✝ = 66

Instances For

Used by

def

Lean2Js.HelperSem.hasFuelList

source

@[irreducible]

(env : Js.TyEnv) :

List Val → Js.TyDesc → Nat

Equations

Lean2Js.HelperSem.hasFuelList env [] x✝ = 0
Lean2Js.HelperSem.hasFuelList env (x_2 :: rest) x✝ = Lean2Js.HelperSem.hasFuel env x_2 x✝ + Lean2Js.HelperSem.hasFuelList env rest x✝ + 8

Instances For

Used by

def

Lean2Js.HelperSem.hasFuelEntries

source

@[irreducible]

(env : Js.TyEnv) :

List (String × Val) → Js.TyDesc → Nat

Equations

Lean2Js.HelperSem.hasFuelEntries env [] x✝ = 0
Lean2Js.HelperSem.hasFuelEntries env ((fst, v) :: rest) x✝ = Lean2Js.HelperSem.hasFuel env v x✝ + Lean2Js.HelperSem.hasFuelEntries env rest x✝ + 8

Instances For

Used by

def

Lean2Js.HelperSem.hasFuelAlts

source

@[irreducible]

(env : Js.TyEnv) (es : List (String × Val)) :

List (String × List (String × Js.TyDesc)) → Nat

Equations

Lean2Js.HelperSem.hasFuelAlts env es [] = 0
Lean2Js.HelperSem.hasFuelAlts env es ((c, fields) :: rest) = Lean2Js.HelperSem.hasFuelFields env es fields + Lean2Js.HelperSem.hasFuelAlts env es rest + 8

Instances For

Used by

def

Lean2Js.HelperSem.hasFuelFields

source

@[irreducible]

(env : Js.TyEnv) (es : List (String × Val)) :

List (String × Js.TyDesc) → Nat

Equations

Lean2Js.HelperSem.hasFuelFields env es [] = 0
Lean2Js.HelperSem.hasFuelFields env es ((n, d) :: rest) = Lean2Js.HelperSem.hasFuel env (Lean2Js.HelperSem.lookupV es n) d + Lean2Js.HelperSem.hasFuelFields env es rest + 16

source

(fields : List (String × Js.TyDesc)) :

(tyValFields fields).length = fields.length

Used by

theorem

Lean2Js.HelperSem.getElem?_eq_head?_drop

source

{α : Type u_1} (l : List α) (m : Nat) :

l[m]? = (List.drop m l).head?

Used by

theorem

Lean2Js.HelperSem.hasFields_loop

source

{tenv : Js.TyEnv} (ext : Ext) (es : List (String × Val)) (F : Val) (hsub : ∀ (name : String) (d : Js.TyDesc) (g : Nat), callDef ext (g + hasFuel tenv (lookupV es name) d) "__has" [lookupV es name, tyVal d, envVal tenv] = Res.ok (Val.bool (hasV tenv (lookupV es name) d))) (fields : List (String × Js.TyDesc)) (f : Nat) :

evalFor ext (f + hasFuelFields tenv es fields + 8) [("x", Val.obj es), ("fields", F), ("e", envVal tenv)] "f" (tyValFields fields) [Helper.Stmt.ifThen (Helper.Expr.prim "Object.hasOwn" [Helper.Expr.var "x", (Helper.Expr.var "f").index (Helper.Expr.num 0)]).not [Helper.Stmt.ret (Helper.Expr.bool false)], Helper.Stmt.ifThen (Helper.Expr.call "__has" [(Helper.Expr.var "x").index ((Helper.Expr.var "f").index (Helper.Expr.num 0)), (Helper.Expr.var "f").index (Helper.Expr.num 1), Helper.Expr.var "e"]).not [Helper.Stmt.ret (Helper.Expr.bool false)]] = if hasFields tenv es fields = true then Res.ok (Outcome.next [("x", Val.obj es), ("fields", F), ("e", envVal tenv)]) else Res.ok (Outcome.ret (Val.bool false))

Used by

theorem

Lean2Js.HelperSem.calls_hasFields

source

{tenv : Js.TyEnv} (ext : Ext) (es : List (String × Val)) (hsub : ∀ (name : String) (d : Js.TyDesc) (g : Nat), callDef ext (g + hasFuel tenv (lookupV es name) d) "__has" [lookupV es name, tyVal d, envVal tenv] = Res.ok (Val.bool (hasV tenv (lookupV es name) d))) (fields : List (String × Js.TyDesc)) (f : Nat) :

source

Js.TyDesc → String

The head the compiler renders for a descriptor: what __has dispatches on.

Equations

Lean2Js.HelperSem.headName Lean2Js.Js.TyDesc.bool = "bool"
Lean2Js.HelperSem.headName Lean2Js.Js.TyDesc.int53 = "int53"
Lean2Js.HelperSem.headName Lean2Js.Js.TyDesc.uint32 = "uint32"
Lean2Js.HelperSem.headName Lean2Js.Js.TyDesc.string = "string"
Lean2Js.HelperSem.headName Lean2Js.Js.TyDesc.bigint = "bigint"
Lean2Js.HelperSem.headName t.array = "array"
Lean2Js.HelperSem.headName value.dict = "dict"
Lean2Js.HelperSem.headName value.dictObj = "dictObj"
Lean2Js.HelperSem.headName t.option = "option"
Lean2Js.HelperSem.headName (ok.result err) = "result"
Lean2Js.HelperSem.headName (Lean2Js.Js.TyDesc.ctors key alts) = "ctors"
Lean2Js.HelperSem.headName (Lean2Js.Js.TyDesc.mu key alts) = "mu"
Lean2Js.HelperSem.headName (Lean2Js.Js.TyDesc.ref up) = "ref"

Instances For

Used by

theorem

Lean2Js.HelperSem.has_head

source

{tenv : Js.TyEnv} (ext : Ext) (f : Nat) (v : Val) (t : Js.TyDesc) :

evalExpr ext (f + 3) [("x", v), ("t", tyVal t), ("e", envVal tenv)] ((Helper.Expr.var "t").index (Helper.Expr.num 0)) = Res.ok (Val.str (headName t))

Used by

theorem

Lean2Js.HelperSem.lookup_k

source

{tenv : Js.TyEnv} (t : Js.TyDesc) (v : Val) :

lookup [("k", Val.str (headName t)), ("x", v), ("t", tyVal t), ("e", envVal tenv)] "k" = some (Val.str (headName t))

Used by

theorem

Lean2Js.HelperSem.sumCost_hasFuelList

source

{tenv : Js.TyEnv} (te : Js.TyDesc) (xs : List Val) :

sumCost (fun (w : Val) => hasFuel tenv w te + 7) xs = hasFuelList tenv xs te

Used by

theorem

Lean2Js.HelperSem.valAll_hasList

source

{tenv : Js.TyEnv} (te : Js.TyDesc) (xs : List Val) :

valAll (fun (w : Val) => Res.ok (Val.bool (hasV tenv w te))) xs = Res.ok (hasList tenv xs te)

Used by

theorem

Lean2Js.HelperSem.answers_element

source

{tenv : Js.TyEnv} (ext : Ext) (n : Nat) (ih : ∀ (w : Val) (te : Js.TyDesc), sizeOf w < n → ∀ (g : Nat), callDef ext (g + hasFuel tenv w te) "__has" [w, tyVal te, envVal tenv] = Res.ok (Val.bool (hasV tenv w te))) (te : Js.TyDesc) (head : String) (x : Val) (xs : List Val) (hsz : ∀ (w : Val), w ∈ xs → sizeOf w < n) :

Answers ext (Val.lam ["y"] (Helper.Expr.call "__has" [Helper.Expr.var "y", (Helper.Expr.var "t").index (Helper.Expr.num 1), Helper.Expr.var "e"]) [("k", Val.str head), ("x", x), ("t", Val.arr [Val.str head, tyVal te]), ("e", envVal tenv)]) (fun (w : Val) => Res.ok (Val.bool (hasV tenv w te))) (fun (w : Val) => hasFuel tenv w te + 7) xs

The closure __has hands to __all: it asks __has about the element, at the descriptor sitting one along from the one it is checking. Its cost is not a constant — the call recurses — so the loop is given a cost per element rather than a length.

Used by

theorem

Lean2Js.HelperSem.hasEntries_eq

source

{tenv : Js.TyEnv} (te : Js.TyDesc) (es : List (String × Val)) :

hasEntries tenv es te = hasList tenv (List.map (fun (x : String × Val) => x.snd) es) te

Used by

theorem

Lean2Js.HelperSem.hasFuelEntries_eq

source

{tenv : Js.TyEnv} (te : Js.TyDesc) (es : List (String × Val)) :

hasFuelEntries tenv es te = hasFuelList tenv (List.map (fun (x : String × Val) => x.snd) es) te

Used by

theorem

Lean2Js.HelperSem.answers_keyString

source

Instances For

Used by

theorem

Lean2Js.HelperSem.tyValAlts_eq

source

(alts : List (String × List (String × Js.TyDesc))) :

tyValAlts alts = List.map altVal alts

Used by

def

Lean2Js.HelperSem.altMatch

source

(tag c : Val) :

Res Val

What the closure __has hands __find computes: the alternative's name against the object's tag.

Equations

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

Instances For

Used by

theorem

source

(ext : Ext) (x key tag tv ev : Val) (xs : List Val) (hkey : index tv (Val.num 1) = Res.ok key) (htag : index x key = Res.ok tag) :

Answers ext (Val.lam ["c"] (Helper.Expr.bin "===" ((Helper.Expr.var "c").index (Helper.Expr.num 0)) ((Helper.Expr.var "x").index ((Helper.Expr.var "t").index (Helper.Expr.num 1)))) [("k", Val.str "ctors"), ("x", x), ("t", tv), ("e", ev)]) (altMatch tag) (fun (x : Val) => 4) xs

Used by

theorem

source

List.find? (fun (x : Helper.Def) => x.name == "__norm") Helper.defs = some Helper.norm

Used by

theorem

Lean2Js.HelperSem.find_normFields

source

List.find? (fun (x : Helper.Def) => x.name == "__normFields") Helper.defs = some Helper.normFields

Used by

def

Lean2Js.HelperSem.normV

source

@[irreducible]

(tenv : Js.TyEnv) :

Val → Js.TyDesc → Val

What __norm builds. The tag keeps the slot the object handed it; the constructor's fields follow in the order the descriptor names them, and a name the object does not carry is dropped.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.normV tenv (Lean2Js.HelperSem.Val.arr xs) t.array = Lean2Js.HelperSem.Val.arr (Lean2Js.HelperSem.normVList tenv xs t)
Lean2Js.HelperSem.normV tenv (Lean2Js.HelperSem.Val.dict es) t.dict = Lean2Js.HelperSem.Val.dict (Lean2Js.HelperSem.normVEntries tenv es t)
Lean2Js.HelperSem.normV tenv (Lean2Js.HelperSem.Val.obj es) t.dictObj = Lean2Js.HelperSem.Val.dict (Lean2Js.HelperSem.mapSetAll [] (Lean2Js.HelperSem.normVEntries tenv es t))
Lean2Js.HelperSem.normV tenv (Lean2Js.HelperSem.Val.dict es) t.dictObj = Lean2Js.HelperSem.Val.dict (Lean2Js.HelperSem.normVEntries tenv es t)
Lean2Js.HelperSem.normV tenv x✝ (Lean2Js.Js.TyDesc.mu key alts) = Lean2Js.HelperSem.normV ((key, alts) :: tenv) x✝ (Lean2Js.Js.TyDesc.ctors key alts)
Lean2Js.HelperSem.normV tenv x✝ (Lean2Js.Js.TyDesc.ref up) = match tenv[up]? with | some b => Lean2Js.HelperSem.normV (List.drop up tenv) x✝ (Lean2Js.Js.TyDesc.ctors b.fst b.snd) | none => x✝
Lean2Js.HelperSem.normV tenv x✝¹ x✝ = x✝¹

Instances For

Used by

def

Lean2Js.HelperSem.normVList

source

@[irreducible]

(tenv : Js.TyEnv) :

List Val → Js.TyDesc → List Val

Equations

Lean2Js.HelperSem.normVList tenv [] x✝ = []
Lean2Js.HelperSem.normVList tenv (x_2 :: rest) x✝ = Lean2Js.HelperSem.normV tenv x_2 x✝ :: Lean2Js.HelperSem.normVList tenv rest x✝

Instances For

Used by

def

Lean2Js.HelperSem.normVEntries

source

@[irreducible]

(tenv : Js.TyEnv) :

List (String × Val) → Js.TyDesc → List (String × Val)

Equations

Lean2Js.HelperSem.normVEntries tenv [] x✝ = []
Lean2Js.HelperSem.normVEntries tenv ((fst, v) :: rest) x✝ = (fst, Lean2Js.HelperSem.normV tenv v x✝) :: Lean2Js.HelperSem.normVEntries tenv rest x✝

Instances For

Used by

def

Lean2Js.HelperSem.normVFields

source

@[irreducible]

(tenv : Js.TyEnv) (es : List (String × Val)) :

List (String × Js.TyDesc) → List (String × Val)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.normVFields tenv es [] = []

Instances For

Used by

def

Lean2Js.HelperSem.normFuel

source

@[irreducible]

(tenv : Js.TyEnv) :

Val → Js.TyDesc → Nat

Enough fuel for __norm, by the same recursion as normV and for the reason hasFuel is generous: the claims are stated for every larger amount.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.normFuel tenv (Lean2Js.HelperSem.Val.arr xs) t.array = Lean2Js.HelperSem.normFuelList tenv xs t + 4 * xs.length + 66
Lean2Js.HelperSem.normFuel tenv (Lean2Js.HelperSem.Val.dict es) t.dict = Lean2Js.HelperSem.normFuelEntries tenv es t + 8 * es.length + 66
Lean2Js.HelperSem.normFuel tenv (Lean2Js.HelperSem.Val.obj es) t.dictObj = Lean2Js.HelperSem.normFuelEntries tenv es t + 8 * es.length + 66
Lean2Js.HelperSem.normFuel tenv (Lean2Js.HelperSem.Val.dict es) t.dictObj = Lean2Js.HelperSem.normFuelEntries tenv es t + 8 * es.length + 66
Lean2Js.HelperSem.normFuel tenv (Lean2Js.HelperSem.Val.obj es) t.option = Lean2Js.HelperSem.normFuelFields tenv es [("value", t)] + 66
Lean2Js.HelperSem.normFuel tenv (Lean2Js.HelperSem.Val.obj es) (Lean2Js.Js.TyDesc.ctors key alts) = Lean2Js.HelperSem.normFuelAlts tenv es alts + 5 * alts.length + 66
Lean2Js.HelperSem.normFuel tenv x✝ (Lean2Js.Js.TyDesc.ctors key alts) = 5 * alts.length + 66
Lean2Js.HelperSem.normFuel tenv x✝ (Lean2Js.Js.TyDesc.mu key alts) = Lean2Js.HelperSem.normFuel ((key, alts) :: tenv) x✝ (Lean2Js.Js.TyDesc.ctors key alts) + 2 * List.length tenv + 200
Lean2Js.HelperSem.normFuel tenv x✝¹ x✝ = 66

Instances For

Used by

def

Lean2Js.HelperSem.normFuelList

source

@[irreducible]

(tenv : Js.TyEnv) :

List Val → Js.TyDesc → Nat

Equations

Lean2Js.HelperSem.normFuelList tenv [] x✝ = 0
Lean2Js.HelperSem.normFuelList tenv (x_2 :: rest) x✝ = Lean2Js.HelperSem.normFuel tenv x_2 x✝ + Lean2Js.HelperSem.normFuelList tenv rest x✝ + 8

Instances For

Used by

def

Lean2Js.HelperSem.normFuelEntries

source

@[irreducible]

(tenv : Js.TyEnv) :

List (String × Val) → Js.TyDesc → Nat

Equations

Lean2Js.HelperSem.normFuelEntries tenv [] x✝ = 0
Lean2Js.HelperSem.normFuelEntries tenv ((fst, v) :: rest) x✝ = Lean2Js.HelperSem.normFuel tenv v x✝ + Lean2Js.HelperSem.normFuelEntries tenv rest x✝ + 8

Instances For

Used by

def

Lean2Js.HelperSem.normFuelAlts

source

@[irreducible]

(tenv : Js.TyEnv) (es : List (String × Val)) :

List (String × List (String × Js.TyDesc)) → Nat

Equations

Lean2Js.HelperSem.normFuelAlts tenv es [] = 0
Lean2Js.HelperSem.normFuelAlts tenv es ((c, fields) :: rest) = Lean2Js.HelperSem.normFuelFields tenv es fields + Lean2Js.HelperSem.normFuelAlts tenv es rest + 8

Instances For

Used by

def

Lean2Js.HelperSem.normFuelFields

source

@[irreducible]

(tenv : Js.TyEnv) (es : List (String × Val)) :

List (String × Js.TyDesc) → Nat

Equations

Lean2Js.HelperSem.normFuelFields tenv es [] = 0
Lean2Js.HelperSem.normFuelFields tenv es ((n, d) :: rest) = Lean2Js.HelperSem.normFuel tenv (Lean2Js.HelperSem.lookupV es n) d + Lean2Js.HelperSem.normFuelFields tenv es rest + 16

Instances For

Used by

def

Lean2Js.HelperSem.normPairs

source

(tenv : Js.TyEnv) (es : List (String × Val)) :

List (String × Js.TyDesc) → List Val

The pairs __normFields pushes, in the order it pushes them.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.normPairs tenv es [] = []

Instances For

Used by

theorem

Lean2Js.HelperSem.fromPairs_normPairs

source

{tenv : Js.TyEnv} (es : List (String × Val)) {key : String} (fields : List (String × Js.TyDesc)) (acc : List (String × Val)) :

Js.namesOk key fields = true → (∀ (n : String), n ∈ List.map (fun (x : String × Js.TyDesc) => x.fst) fields → (acc.any fun (x : String × Val) => x.fst == n) = false) → fromPairs acc (normPairs tenv es fields) = some (acc ++ normVFields tenv es fields)

Object.fromEntries over what the loop pushed. It appends rather than replaces because the names are distinct and none of them is the tag the accumulator already carries.

Used by

theorem

Lean2Js.HelperSem.normFields_loop

source

{tenv : Js.TyEnv} (ext : Ext) (es : List (String × Val)) (K F : Val) (fields : List (String × Js.TyDesc)) (acc : List Val) (f : Nat) :

(∀ (name : String) (d : Js.TyDesc), (name, d) ∈ fields → ∀ (g : Nat), callDef ext (g + normFuel tenv (lookupV es name) d) "__norm" [lookupV es name, tyVal d, envVal tenv] = Res.ok (normV tenv (lookupV es name) d)) → evalFor ext (f + normFuelFields tenv es fields + 8) [("out", Val.arr acc), ("x", Val.obj es), ("key", K), ("fields", F), ("e", envVal tenv)] "f" (tyValFields fields) [Helper.Stmt.ifThen (Helper.Expr.prim "Object.hasOwn" [Helper.Expr.var "x", (Helper.Expr.var "f").index (Helper.Expr.num 0)]) [Helper.Stmt.push "out" (Helper.Expr.arrayLit [(Helper.Expr.var "f").index (Helper.Expr.num 0), Helper.Expr.call "__norm" [(Helper.Expr.var "x").index ((Helper.Expr.var "f").index (Helper.Expr.num 0)), (Helper.Expr.var "f").index (Helper.Expr.num 1), Helper.Expr.var "e"]])]] = Res.ok (Outcome.next [("out", Val.arr (acc ++ normPairs tenv es fields)), ("x", Val.obj es), ("key", K), ("fields", F), ("e", envVal tenv)])

Used by

theorem

Lean2Js.HelperSem.calls_normFields

source

{tenv : Js.TyEnv} (ext : Ext) (es : List (String × Val)) (key : String) (fields : List (String × Js.TyDesc)) (hsub : ∀ (name : String) (d : Js.TyDesc), (name, d) ∈ fields → ∀ (g : Nat), callDef ext (g + normFuel tenv (lookupV es name) d) "__norm" [lookupV es name, tyVal d, envVal tenv] = Res.ok (normV tenv (lookupV es name) d)) (hnames : Js.namesOk key fields = true) (f : Nat) :

callDef ext (f + normFuelFields tenv es fields + 16) "__normFields" [Val.obj es, Val.str key, Val.arr (tyValFields fields), envVal tenv] = Res.ok (Val.obj ((key, lookupV es key) :: normVFields tenv es fields))

Used by

theorem

Lean2Js.HelperSem.normArray_loop

source

{tenv : Js.TyEnv} (ext : Ext) (te : Js.TyDesc) (K : Val) (xs : List Val) (X : Val) (acc : List Val) (f : Nat) :

(∀ (y : Val), y ∈ xs → ∀ (g : Nat), callDef ext (g + normFuel tenv y te) "__norm" [y, tyVal te, envVal tenv] = Res.ok (normV tenv y te)) → evalFor ext (f + normFuelList tenv xs te + 8) [("out", Val.arr acc), ("k", K), ("x", X), ("t", Val.arr [Val.str "array", tyVal te]), ("e", envVal tenv)] "y" xs [Helper.Stmt.push "out" (Helper.Expr.call "__norm" [Helper.Expr.var "y", (Helper.Expr.var "t").index (Helper.Expr.num 1), Helper.Expr.var "e"])] = Res.ok (Outcome.next [("out", Val.arr (acc ++ normVList tenv xs te)), ("k", K), ("x", X), ("t", Val.arr [Val.str "array", tyVal te]), ("e", envVal tenv)])

Used by

def

Lean2Js.HelperSem.keysDistinctV

source

List String → Bool

What no Map can hold: the same key twice. Js.dictKeysDistinct says this of a JsValue; the source semantics needs it of the Val the helper is handed, because __norm rebuilds a dictionary by walking its keys.

Equations

Lean2Js.HelperSem.keysDistinctV [] = true
Lean2Js.HelperSem.keysDistinctV (k :: ks) = (!ks.contains k && Lean2Js.HelperSem.keysDistinctV ks)

Instances For

Used by

def

Lean2Js.HelperSem.mapsOk

source

@[irreducible]

Val → Bool

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.mapsOk (Lean2Js.HelperSem.Val.obj es) = Lean2Js.HelperSem.mapsOkFields es
Lean2Js.HelperSem.mapsOk (Lean2Js.HelperSem.Val.arr xs) = Lean2Js.HelperSem.mapsOkList xs
Lean2Js.HelperSem.mapsOk x✝ = true

Instances For

Used by

def

Lean2Js.HelperSem.mapsOkFields

source

@[irreducible]

List (String × Val) → Bool

Equations

Lean2Js.HelperSem.mapsOkFields [] = true
Lean2Js.HelperSem.mapsOkFields ((fst, v) :: rest) = (Lean2Js.HelperSem.mapsOk v && Lean2Js.HelperSem.mapsOkFields rest)

Instances For

Used by

def

Lean2Js.HelperSem.mapsOkList

source

@[irreducible]

List Val → Bool

Equations

Lean2Js.HelperSem.mapsOkList [] = true
Lean2Js.HelperSem.mapsOkList (x_1 :: rest) = (Lean2Js.HelperSem.mapsOk x_1 && Lean2Js.HelperSem.mapsOkList rest)

Instances For

Used by

def

Lean2Js.HelperSem.normSet

source

(tenv : Js.TyEnv) (es : List (String × Val)) (t : Js.TyDesc) :

List (String × Val) → List String → List (String × Val)

What the dictionary loop leaves in out: each key set, in the order __dkeys hands them over.

Equations

Lean2Js.HelperSem.normSet tenv es t x✝ [] = x✝
Lean2Js.HelperSem.normSet tenv es t x✝ (k :: ks) = Lean2Js.HelperSem.normSet tenv es t (Lean2Js.HelperSem.mapSet x✝ k (Lean2Js.HelperSem.normV tenv (Lean2Js.HelperSem.lookupV es k) t)) ks

Instances For

Used by

def

Lean2Js.HelperSem.normFuelKeys

source

(tenv : Js.TyEnv) (es : List (String × Val)) (t : Js.TyDesc) :

List String → Nat

Equations

Lean2Js.HelperSem.normFuelKeys tenv es t [] = 0
Lean2Js.HelperSem.normFuelKeys tenv es t (k :: ks) = Lean2Js.HelperSem.normFuel tenv (Lean2Js.HelperSem.lookupV es k) t + Lean2Js.HelperSem.normFuelKeys tenv es t ks + 12

{tenv : Js.TyEnv} (ext : Ext) (v : Val) (t : Js.TyDesc) (hd : Js.descOk (List.length tenv) t = true) (he : Js.envOk tenv = true) (hmo : mapsOk v = true) (hh : hasV tenv v t = true) (f : Nat) :

callDef ext (f + normFuel tenv v t) "__norm" [v, tyVal t, envVal tenv] = Res.ok (normV tenv v t)

What __norm builds, for every value the entry check accepts and every descriptor the compiler renders.

Used by

theorem

Lean2Js.HelperSem.envVal_nil

source

envVal [] = Val.arr []

Used by

theorem

Lean2Js.HelperSem.calls_ck

source

(ext : Ext) (v : Val) (t : Js.TyDesc) (hd : Js.descOk 0 t = true) (hmo : mapsOk v = true) (f : Nat) :

callDef ext (f + hasFuel [] v t + normFuel [] v t + 9) "__ck" [v, tyVal t] = if hasV [] v t = true then Res.ok (normV [] v t) else Res.thrown "typeError"

__ck is __has with a throw: what the check accepts comes back rebuilt in the shape the descriptor names, and what it refuses raises typeError. The environment it starts at is empty.

source

@[irreducible]

(tenv : Js.TyEnv) :

Val → Js.TyDesc → Val

What __out builds. The tag keeps the slot the object handed it; the constructor's fields follow in the order the descriptor names them, and a name the object does not carry is dropped.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.outV tenv (Lean2Js.HelperSem.Val.arr xs) t.array = Lean2Js.HelperSem.Val.arr (Lean2Js.HelperSem.outVList tenv xs t)
Lean2Js.HelperSem.outV tenv (Lean2Js.HelperSem.Val.dict es) t.dict = Lean2Js.HelperSem.Val.dict (Lean2Js.HelperSem.outVEntries tenv es t)
Lean2Js.HelperSem.outV tenv (Lean2Js.HelperSem.Val.dict es) t.dictObj = Lean2Js.HelperSem.Val.obj (Lean2Js.HelperSem.outVEntries tenv es t)
Lean2Js.HelperSem.outV tenv x✝ (Lean2Js.Js.TyDesc.mu key alts) = Lean2Js.HelperSem.outV ((key, alts) :: tenv) x✝ (Lean2Js.Js.TyDesc.ctors key alts)
Lean2Js.HelperSem.outV tenv x✝ (Lean2Js.Js.TyDesc.ref up) = match tenv[up]? with | some b => Lean2Js.HelperSem.outV (List.drop up tenv) x✝ (Lean2Js.Js.TyDesc.ctors b.fst b.snd) | none => x✝
Lean2Js.HelperSem.outV tenv x✝¹ x✝ = x✝¹

Instances For

Used by

def

Lean2Js.HelperSem.outVList

source

@[irreducible]

(tenv : Js.TyEnv) :

List Val → Js.TyDesc → List Val

Equations

Lean2Js.HelperSem.outVList tenv [] x✝ = []
Lean2Js.HelperSem.outVList tenv (x_2 :: rest) x✝ = Lean2Js.HelperSem.outV tenv x_2 x✝ :: Lean2Js.HelperSem.outVList tenv rest x✝

Instances For

Used by

def

Lean2Js.HelperSem.outVEntries

source

@[irreducible]

(tenv : Js.TyEnv) :

List (String × Val) → Js.TyDesc → List (String × Val)

Equations

Lean2Js.HelperSem.outVEntries tenv [] x✝ = []
Lean2Js.HelperSem.outVEntries tenv ((fst, v) :: rest) x✝ = (fst, Lean2Js.HelperSem.outV tenv v x✝) :: Lean2Js.HelperSem.outVEntries tenv rest x✝

Instances For

Used by

def

Lean2Js.HelperSem.outVFields

source

@[irreducible]

(tenv : Js.TyEnv) (es : List (String × Val)) :

List (String × Js.TyDesc) → List (String × Val)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.outVFields tenv es [] = []

Instances For

Used by

def

Lean2Js.HelperSem.outFuel

source

@[irreducible]

(tenv : Js.TyEnv) :

Val → Js.TyDesc → Nat

Enough fuel for __out, by the same recursion as outV and for the reason hasFuel is generous: the claims are stated for every larger amount.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.outFuel tenv (Lean2Js.HelperSem.Val.arr xs) t.array = Lean2Js.HelperSem.outFuelList tenv xs t + 4 * xs.length + 66
Lean2Js.HelperSem.outFuel tenv (Lean2Js.HelperSem.Val.dict es) t.dict = Lean2Js.HelperSem.outFuelEntries tenv es t + 8 * es.length + 66
Lean2Js.HelperSem.outFuel tenv (Lean2Js.HelperSem.Val.dict es) t.dictObj = Lean2Js.HelperSem.outFuelEntries tenv es t + 8 * es.length + 66
Lean2Js.HelperSem.outFuel tenv (Lean2Js.HelperSem.Val.obj es) t.option = Lean2Js.HelperSem.outFuelFields tenv es [("value", t)] + 66
Lean2Js.HelperSem.outFuel tenv (Lean2Js.HelperSem.Val.obj es) (Lean2Js.Js.TyDesc.ctors key alts) = Lean2Js.HelperSem.outFuelAlts tenv es alts + 5 * alts.length + 66
Lean2Js.HelperSem.outFuel tenv x✝ (Lean2Js.Js.TyDesc.ctors key alts) = 5 * alts.length + 66
Lean2Js.HelperSem.outFuel tenv x✝ (Lean2Js.Js.TyDesc.mu key alts) = Lean2Js.HelperSem.outFuel ((key, alts) :: tenv) x✝ (Lean2Js.Js.TyDesc.ctors key alts) + 2 * List.length tenv + 200
Lean2Js.HelperSem.outFuel tenv x✝¹ x✝ = 66

Instances For

Used by

def

Lean2Js.HelperSem.outFuelList

source

@[irreducible]

(tenv : Js.TyEnv) :

List Val → Js.TyDesc → Nat

Equations

Lean2Js.HelperSem.outFuelList tenv [] x✝ = 0
Lean2Js.HelperSem.outFuelList tenv (x_2 :: rest) x✝ = Lean2Js.HelperSem.outFuel tenv x_2 x✝ + Lean2Js.HelperSem.outFuelList tenv rest x✝ + 8

Instances For

Used by

def

Lean2Js.HelperSem.outFuelEntries

source

@[irreducible]

(tenv : Js.TyEnv) :

List (String × Val) → Js.TyDesc → Nat

Equations

Lean2Js.HelperSem.outFuelEntries tenv [] x✝ = 0
Lean2Js.HelperSem.outFuelEntries tenv ((fst, v) :: rest) x✝ = Lean2Js.HelperSem.outFuel tenv v x✝ + Lean2Js.HelperSem.outFuelEntries tenv rest x✝ + 8

Instances For

Used by

def

Lean2Js.HelperSem.outFuelAlts

source

@[irreducible]

(tenv : Js.TyEnv) (es : List (String × Val)) :

List (String × List (String × Js.TyDesc)) → Nat

Equations

Lean2Js.HelperSem.outFuelAlts tenv es [] = 0
Lean2Js.HelperSem.outFuelAlts tenv es ((c, fields) :: rest) = Lean2Js.HelperSem.outFuelFields tenv es fields + Lean2Js.HelperSem.outFuelAlts tenv es rest + 8

Instances For

Used by

def

Lean2Js.HelperSem.outFuelFields

source

@[irreducible]

(tenv : Js.TyEnv) (es : List (String × Val)) :

List (String × Js.TyDesc) → Nat

Equations

Lean2Js.HelperSem.outFuelFields tenv es [] = 0
Lean2Js.HelperSem.outFuelFields tenv es ((n, d) :: rest) = Lean2Js.HelperSem.outFuel tenv (Lean2Js.HelperSem.lookupV es n) d + Lean2Js.HelperSem.outFuelFields tenv es rest + 16

Instances For

Used by

def

Lean2Js.HelperSem.outPairs

source

(tenv : Js.TyEnv) (es : List (String × Val)) :

List (String × Js.TyDesc) → List Val

The pairs __outFields pushes, in the order it pushes them.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.outPairs tenv es [] = []

Instances For

Used by

theorem

Lean2Js.HelperSem.fromPairs_outPairs

source

{tenv : Js.TyEnv} (es : List (String × Val)) {key : String} (fields : List (String × Js.TyDesc)) (acc : List (String × Val)) :

Js.namesOk key fields = true → (∀ (n : String), n ∈ List.map (fun (x : String × Js.TyDesc) => x.fst) fields → (acc.any fun (x : String × Val) => x.fst == n) = false) → fromPairs acc (outPairs tenv es fields) = some (acc ++ outVFields tenv es fields)

Object.fromEntries over what the loop pushed. It appends rather than replaces because the names are distinct and none of them is the tag the accumulator already carries.

Used by

theorem

Lean2Js.HelperSem.outFields_loop

source

{tenv : Js.TyEnv} (ext : Ext) (es : List (String × Val)) (K F : Val) (fields : List (String × Js.TyDesc)) (acc : List Val) (f : Nat) :

(∀ (name : String) (d : Js.TyDesc), (name, d) ∈ fields → ∀ (g : Nat), callDef ext (g + outFuel tenv (lookupV es name) d) "__out" [lookupV es name, tyVal d, envVal tenv] = Res.ok (outV tenv (lookupV es name) d)) → evalFor ext (f + outFuelFields tenv es fields + 8) [("out", Val.arr acc), ("x", Val.obj es), ("key", K), ("fields", F), ("e", envVal tenv)] "f" (tyValFields fields) [Helper.Stmt.ifThen (Helper.Expr.prim "Object.hasOwn" [Helper.Expr.var "x", (Helper.Expr.var "f").index (Helper.Expr.num 0)]) [Helper.Stmt.push "out" (Helper.Expr.arrayLit [(Helper.Expr.var "f").index (Helper.Expr.num 0), Helper.Expr.call "__out" [(Helper.Expr.var "x").index ((Helper.Expr.var "f").index (Helper.Expr.num 0)), (Helper.Expr.var "f").index (Helper.Expr.num 1), Helper.Expr.var "e"]])]] = Res.ok (Outcome.next [("out", Val.arr (acc ++ outPairs tenv es fields)), ("x", Val.obj es), ("key", K), ("fields", F), ("e", envVal tenv)])

Used by

theorem

Lean2Js.HelperSem.calls_outFields

source

{tenv : Js.TyEnv} (ext : Ext) (es : List (String × Val)) (key : String) (fields : List (String × Js.TyDesc)) (hsub : ∀ (name : String) (d : Js.TyDesc), (name, d) ∈ fields → ∀ (g : Nat), callDef ext (g + outFuel tenv (lookupV es name) d) "__out" [lookupV es name, tyVal d, envVal tenv] = Res.ok (outV tenv (lookupV es name) d)) (hnames : Js.namesOk key fields = true) (f : Nat) :

callDef ext (f + outFuelFields tenv es fields + 16) "__outFields" [Val.obj es, Val.str key, Val.arr (tyValFields fields), envVal tenv] = Res.ok (Val.obj ((key, lookupV es key) :: outVFields tenv es fields))

Used by

theorem

Lean2Js.HelperSem.outArray_loop

source

{tenv : Js.TyEnv} (ext : Ext) (te : Js.TyDesc) (K : Val) (xs : List Val) (X : Val) (acc : List Val) (f : Nat) :

(∀ (y : Val), y ∈ xs → ∀ (g : Nat), callDef ext (g + outFuel tenv y te) "__out" [y, tyVal te, envVal tenv] = Res.ok (outV tenv y te)) → evalFor ext (f + outFuelList tenv xs te + 8) [("out", Val.arr acc), ("k", K), ("x", X), ("t", Val.arr [Val.str "array", tyVal te]), ("e", envVal tenv)] "y" xs [Helper.Stmt.push "out" (Helper.Expr.call "__out" [Helper.Expr.var "y", (Helper.Expr.var "t").index (Helper.Expr.num 1), Helper.Expr.var "e"])] = Res.ok (Outcome.next [("out", Val.arr (acc ++ outVList tenv xs te)), ("k", K), ("x", X), ("t", Val.arr [Val.str "array", tyVal te]), ("e", envVal tenv)])

Used by

def

Lean2Js.HelperSem.outSet

source

(tenv : Js.TyEnv) (es : List (String × Val)) (t : Js.TyDesc) :

List (String × Val) → List String → List (String × Val)

What the dictionary loop leaves in out: each key set, in the order __dkeys hands them over.

Equations

Lean2Js.HelperSem.outSet tenv es t x✝ [] = x✝
Lean2Js.HelperSem.outSet tenv es t x✝ (k :: ks) = Lean2Js.HelperSem.outSet tenv es t (Lean2Js.HelperSem.mapSet x✝ k (Lean2Js.HelperSem.outV tenv (Lean2Js.HelperSem.lookupV es k) t)) ks

Instances For

Used by

def

Lean2Js.HelperSem.outFuelKeys

source

(tenv : Js.TyEnv) (es : List (String × Val)) (t : Js.TyDesc) :

List String → Nat

Equations

Lean2Js.HelperSem.outFuelKeys tenv es t [] = 0
Lean2Js.HelperSem.outFuelKeys tenv es t (k :: ks) = Lean2Js.HelperSem.outFuel tenv (Lean2Js.HelperSem.lookupV es k) t + Lean2Js.HelperSem.outFuelKeys tenv es t ks + 12

Instances For

Used by

theorem

Lean2Js.HelperSem.outVEntries_keys

source

{tenv : Js.TyEnv} (es : List (String × Val)) (t : Js.TyDesc) :

List.map (fun (x : String × Val) => x.fst) (outVEntries tenv es t) = List.map (fun (x : String × Val) => x.fst) es

Used by

def

Lean2Js.HelperSem.outEntryPairs

source

(tenv : Js.TyEnv) (t : Js.TyDesc) :

List (String × Val) → List Val

The pairs __out pushes for a dictionary leaving as a plain object, in the order the Map's iterator hands them over.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.outEntryPairs tenv t [] = []

Instances For

Used by

theorem

Lean2Js.HelperSem.fromPairs_outEntryPairs

source

{tenv : Js.TyEnv} (t : Js.TyDesc) (es acc : List (String × Val)) :

keysDistinctV (List.map (fun (x : String × Val) => x.fst) es) = true → (∀ (k : String), k ∈ List.map (fun (x : String × Val) => x.fst) es → (acc.any fun (x : String × Val) => x.fst == k) = false) → fromPairs acc (outEntryPairs tenv t es) = some (acc ++ outVEntries tenv es t)

Object.fromEntries over what that loop pushed. It appends rather than replaces because a Map cannot have handed the same key over twice.

Used by

theorem

Lean2Js.HelperSem.outDictObj_loop

source

{tenv : Js.TyEnv} (ext : Ext) (te : Js.TyDesc) (K X : Val) (es : List (String × Val)) (acc : List Val) (f : Nat) :

(∀ (w : Val), w ∈ List.map (fun (x : String × Val) => x.snd) es → ∀ (g : Nat), callDef ext (g + outFuel tenv w te) "__out" [w, tyVal te, envVal tenv] = Res.ok (outV tenv w te)) → evalFor ext (f + outFuelEntries tenv es te + 8 * es.length + 8) [("out", Val.arr acc), ("k", K), ("x", X), ("t", Val.arr [Val.str "dictObj", tyVal te]), ("e", envVal tenv)] "en" (List.map (fun (e : String × Val) => Val.arr [Val.str e.fst, e.snd]) es) [Helper.Stmt.push "out" (Helper.Expr.arrayLit [(Helper.Expr.var "en").index (Helper.Expr.num 0), Helper.Expr.call "__out" [(Helper.Expr.var "en").index (Helper.Expr.num 1), (Helper.Expr.var "t").index (Helper.Expr.num 1), Helper.Expr.var "e"]])] = Res.ok (Outcome.next [("out", Val.arr (acc ++ outEntryPairs tenv te es)), ("k", K), ("x", X), ("t", Val.arr [Val.str "dictObj", tyVal te]), ("e", envVal tenv)])

The loop __out runs over a dictionary leaving as a plain object. It walks the entries the Map's iterator hands over and pushes each one, so the object is built in the order the dictionary held.

Used by

theorem

Lean2Js.HelperSem.outDict_loop

source

{tenv : Js.TyEnv} (ext : Ext) (te : Js.TyDesc) (es : List (String × Val)) (K : Val) (ks : List String) (acc : List (String × Val)) (f : Nat) :

(∀ (k : String), k ∈ ks → ∀ (g : Nat), callDef ext (g + outFuel tenv (lookupV es k) te) "__out" [lookupV es k, tyVal te, envVal tenv] = Res.ok (outV tenv (lookupV es k) te)) → evalFor ext (f + outFuelKeys tenv es te ks + 8) [("out", Val.dict acc), ("k", K), ("x", Val.dict es), ("t", Val.arr [Val.str "dict", tyVal te]), ("e", envVal tenv)] "key" (List.map Val.str ks) [Helper.Stmt.setKey "out" (Helper.Expr.var "key") (Helper.Expr.call "__out" [(Helper.Expr.var "x").method "get" [Helper.Expr.var "key"], (Helper.Expr.var "t").index (Helper.Expr.num 1), Helper.Expr.var "e"])] = Res.ok (Outcome.next [("out", Val.dict (outSet tenv es te acc ks)), ("k", K), ("x", Val.dict es), ("t", Val.arr [Val.str "dict", tyVal te]), ("e", envVal tenv)])

Used by

theorem

Lean2Js.HelperSem.outSet_split

source

source

Js.normTy tenv (Js.JsValue.obj fields) t.option = Js.JsValue.obj fields

Used by

theorem

Lean2Js.HelperSem.normTy_result_unmatched

source

Js.normTy tenv (Js.JsValue.obj fields) (ok.result err) = Js.JsValue.obj fields

Used by

theorem

Lean2Js.HelperSem.strictEq_str_lookupV_false

source

{fields : List (String × Js.JsValue)} {key : String} (h : ∀ (ctor : String), Js.lookupField fields key = some (Js.JsValue.str ctor) → False) (s : String) :

strictEq (Val.str s) (lookupV (ofJsFields fields) key) = false

Used by

theorem

Lean2Js.HelperSem.normTy_ctors_unmatched

source

Js.normTy tenv (Js.JsValue.obj fields) (Js.TyDesc.ctors key alts) = Js.JsValue.obj fields

Used by

theorem

Lean2Js.HelperSem.normV_ofJs

source

(tenv : Js.TyEnv) (x : Js.JsValue) (t : Js.TyDesc) :

theorem

Lean2Js.HelperSem.outTy_result_unmatched

source

Js.outTy tenv (Js.JsValue.obj fields) (ok.result err) = Js.JsValue.obj fields

Used by

theorem

__fold is the helper a fold in the subset compiles to. It walks a value from the leaves up and hands each node to the one callback the compiler passed, with each field that came round already replaced by what the callback answered for it — so the callback reads a node of the shape the type declares and dispatches on the tag, which is what a match does.

Nothing emits a call to it yet: the Core.Expr form and its compilation are the commit after this one. What is here is the helper and the statement that it computes what the model says, which is the expensive half and the one this repository requires before a helper may ship.

def

Lean2Js.HelperSem.specValFields

source

Js.FoldFields → List Val

Equations

Instances For

Used by

def

Lean2Js.HelperSem.specValEntries

source

Js.FoldSpec → List (String × Val)

The spec as the object __fold reads it: one entry per constructor, holding that constructor's fields in declared order. Written as a recursion rather than through List.map, and reached through an abbrev, so that the walk can see the obj constructor and step into the read.

Equations

Lean2Js.HelperSem.specValEntries [] = []
Lean2Js.HelperSem.specValEntries ((c, fs) :: rest) = (c, Lean2Js.HelperSem.Val.arr (Lean2Js.HelperSem.specValFields fs)) :: Lean2Js.HelperSem.specValEntries rest

Instances For

Used by

abbrev

Lean2Js.HelperSem.specVal

source

@[reducible, inline]

(spec : Js.FoldSpec) :

Val

Equations

Lean2Js.HelperSem.specVal spec = Lean2Js.HelperSem.Val.obj (Lean2Js.HelperSem.specValEntries spec)

Instances For

Used by

def

Lean2Js.HelperSem.foldV

source

@[irreducible]

(ext : Ext) (i : Nat) (key : String) (spec : Js.FoldSpec) :

Val → Res Val

What __fold computes: the callback's answer for the node, with each field that came round already replaced by the callback's answer for it.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.foldV ext i key spec x✝ = Lean2Js.HelperSem.Res.stuck

Instances For

Used by

def

Lean2Js.HelperSem.foldList

source

@[irreducible]

(ext : Ext) (i : Nat) (key : String) (spec : Js.FoldSpec) :

List Val → Res (List Val)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.foldList ext i key spec [] = Lean2Js.HelperSem.Res.ok []

Instances For

Used by

def

Lean2Js.HelperSem.foldListAt

source

@[irreducible]

(ext : Ext) (i : Nat) (key : String) (spec : Js.FoldSpec) :

Val → Res (List Val)

A field the spec says holds a list of the type coming round. A value that is not an array is one the entry check would not have let through, so the walk declines to answer for it rather than guessing.

Written apart from foldPairs so that the match is on a value and not on a proof: an arm matching on lookupV es n in place makes that arm depend on the equation, and nothing can then case on the field.

Equations

Lean2Js.HelperSem.foldListAt ext i key spec (Lean2Js.HelperSem.Val.arr xs) = Lean2Js.HelperSem.foldList ext i key spec xs
Lean2Js.HelperSem.foldListAt ext i key spec x✝ = Lean2Js.HelperSem.Res.stuck

Instances For

Used by

def

Lean2Js.HelperSem.foldPairs

source

@[irreducible]

(ext : Ext) (i : Nat) (key : String) (spec : Js.FoldSpec) (es : List (String × Val)) :

Js.FoldFields → Res (List (String × Val))

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.foldPairs ext i key spec es [] = Lean2Js.HelperSem.Res.ok []

Instances For

Used by

def

Lean2Js.HelperSem.foldFuel

source

@[irreducible]

(key : String) (spec : Js.FoldSpec) :

Val → Nat

Enough fuel for __fold, by the same recursion as foldV. A generous constant per level: the claim is stated for every larger amount, so an upper bound is all a proof needs.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.foldFuel key spec x✝ = 30

Instances For

Used by

def

Lean2Js.HelperSem.foldFuelList

source

@[irreducible]

(key : String) (spec : Js.FoldSpec) :

List Val → Nat

Equations

Lean2Js.HelperSem.foldFuelList key spec [] = 6
Lean2Js.HelperSem.foldFuelList key spec (x_1 :: rest) = Lean2Js.HelperSem.foldFuel key spec x_1 + Lean2Js.HelperSem.foldFuelList key spec rest + 22

Instances For

Used by

def

Lean2Js.HelperSem.foldFuelListAt

source

@[irreducible]

(key : String) (spec : Js.FoldSpec) :

Val → Nat

Equations

Lean2Js.HelperSem.foldFuelListAt key spec (Lean2Js.HelperSem.Val.arr xs) = Lean2Js.HelperSem.foldFuelList key spec xs + 6
Lean2Js.HelperSem.foldFuelListAt key spec x✝ = 6

Instances For

Used by

def

Lean2Js.HelperSem.foldFuelPairs

source

@[irreducible]

(key : String) (spec : Js.FoldSpec) (es : List (String × Val)) :

Js.FoldFields → Nat

Equations

One or more equations did not get rendered due to their size.
Lean2Js.HelperSem.foldFuelPairs key spec es [] = 6
Lean2Js.HelperSem.foldFuelPairs key spec es ((n, Lean2Js.Js.FoldKind.plain ) :: rest) = Lean2Js.HelperSem.foldFuelPairs key spec es rest + 30

Instances For

Used by

theorem

Lean2Js.HelperSem.find_fold

source

List.find? (fun (x : Helper.Def) => x.name == "__fold") Helper.defs = some Helper.fold

Used by

def

Lean2Js.HelperSem.pairVals

source

List (String × Val) → List Val

The pairs the loop pushes, as the array literals it pushes them as.

Equations

Lean2Js.HelperSem.pairVals [] = []
Lean2Js.HelperSem.pairVals ((fst, v) :: rest) = Lean2Js.HelperSem.Val.arr [Lean2Js.HelperSem.Val.str fst, v] :: Lean2Js.HelperSem.pairVals rest

Instances For

Used by

theorem

Lean2Js.HelperSem.foldList_loop

source

(ext : Ext) (i : Nat) (key : String) (spec : Js.FoldSpec) (G O X : Val) (xs acc : List Val) (f : Nat) :

(∀ (x : Val), x ∈ xs → ∀ (g : Nat), callDef ext (g + foldFuel key spec x) "__fold" [x, Val.str key, specVal spec, Val.ext i] = foldV ext i key spec x) → evalFor ext (f + foldFuelList key spec xs + 6) [("ys", Val.arr acc), ("g", G), ("out", O), ("x", X), ("key", Val.str key), ("spec", specVal spec), ("f", Val.ext i)] "c" xs [Helper.Stmt.push "ys" (Helper.Expr.call "__fold" [Helper.Expr.var "c", Helper.Expr.var "key", Helper.Expr.var "spec", Helper.Expr.var "f"])] = (foldList ext i key spec xs).bind fun (ys : List Val) => Res.ok (Outcome.next [("ys", Val.arr (acc ++ ys)), ("g", G), ("out", O), ("x", X), ("key", Val.str key), ("spec", specVal spec), ("f", Val.ext i)])

Used by

abbrev

Lean2Js.HelperSem.foldBody

source

@[reducible, inline]

List Helper.Stmt

The body of the loop __fold runs over a constructor's fields. Named so that the lemma below and the helper read the same text.

Equations

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

Instances For

Used by

theorem

source

(ext : Ext) (i : Nat) (key : String) (spec : Js.FoldSpec) (v : Val) (f : Nat) :

callDef ext (f + foldFuel key spec v) "__fold" [v, Val.str key, specVal spec, Val.ext i] = foldV ext i key spec v

__fold computes what foldV says, at every value and every callback. The value is walked from the leaves up and each node is handed to the callback once, so a callback that throws stops the walk where the helper stops it.

Used by