Lean2Js.Value

Imports 2

The values `eval` returns, and the traps that line the semantics up with JS #

The values eval returns, and the traps that have to be taken to line the semantics up with JS.

Where Lean and JS split on the answer, both sides fail rather than one being bent toward the other. Division by zero is the archetype: Lean's / 0 = 0 and JS's Infinity are both "right", so trapping is the only way to make them agree.

def

Lean2Js.int53Max

source

Int

JS's Number.MAX_SAFE_INTEGER.

Equations

Lean2Js.int53Max = 9007199254740991

Instances For

Used by

def

Lean2Js.int53Min

source

Int

JS's Number.MIN_SAFE_INTEGER.

Equations

Lean2Js.int53Min = -9007199254740991

Instances For

Used by

inductive

Lean2Js.Value

source

Type

A value with a constructor becomes a tagged object on the JS side too. Option is not specialised to T | null because the moment one is nested, none and some none stop being distinguishable.

bool : Value
int53 : Value
uint32 : Value
str : Value
bigint : Value
obj : Value
arr : Value
dict : Value
fn : Value

Instances For

Used by

instance

Lean2Js.instReprValue

source

@[instance_reducible]

Repr Value

Equations

Lean2Js.instReprValue = { reprPrec := Lean2Js.instReprValue.repr }

Used by

partial def

Lean2Js.instReprValue.repr

source

Value → Nat → Std.Format

Used by

instance

Lean2Js.instInhabitedValue

source

@[instance_reducible]

Inhabited Value

Equations

Lean2Js.instInhabitedValue = { default := Lean2Js.instInhabitedValue.default }

Used by

def

Lean2Js.lookupFieldV

source

(fields : List (String × Value)) (k : String) :

Option Value

A constructor value's field by name. Everything that walks a value asks for a key rather than for a position, because the field order a value carries is the declaration's and not the caller's.

Equations

Lean2Js.lookupFieldV fields k = Option.map (fun (x : String × Lean2Js.Value) => x.snd) (List.find? (fun (x : String × Lean2Js.Value) => x.fst == k) fields)

Instances For

Used by

theorem

Lean2Js.sizeOf_lookupFieldV

source

(fields : List (String × Value)) (k : String) {v : Value} (h : lookupFieldV fields k = some v) :

sizeOf v < sizeOf fields

Used by

inductive

Lean2Js.Err

source

Type

divByZero : Err
int53Overflow : Err
outOfFuel : Err
indexOutOfBounds : Err
noMatchingAlternative : Err
typeError : Err
unknownVar : Err
unknownFn : Err
arity : Err

Instances For

Used by

instance

Lean2Js.instReprErr

source

@[instance_reducible]

Repr Err

Equations

Lean2Js.instReprErr = { reprPrec := Lean2Js.instReprErr.repr }

Used by

def

Lean2Js.instReprErr.repr

source

Err → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
Lean2Js.instReprErr.repr Lean2Js.Err.divByZero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean2Js.Err.divByZero")).group prec✝
Lean2Js.instReprErr.repr Lean2Js.Err.int53Overflow prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean2Js.Err.int53Overflow")).group prec✝
Lean2Js.instReprErr.repr Lean2Js.Err.outOfFuel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean2Js.Err.outOfFuel")).group prec✝
Lean2Js.instReprErr.repr Lean2Js.Err.indexOutOfBounds prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean2Js.Err.indexOutOfBounds")).group prec✝

Instances For

Used by

def

Lean2Js.instBEqErr.beq

source

Err → Err → Bool

Equations

Instances For

Used by

instance

Lean2Js.instBEqErr

source

@[instance_reducible]

BEq Err

Equations

Lean2Js.instBEqErr = { beq := Lean2Js.instBEqErr.beq }

Used by

instance

Lean2Js.instInhabitedErr

source

@[instance_reducible]

Inhabited Err

Equations

Lean2Js.instInhabitedErr = { default := Lean2Js.instInhabitedErr.default }

Used by

def

Lean2Js.Err.code

source

Err → String

Equations

Lean2Js.Err.divByZero.code = "divByZero"
Lean2Js.Err.int53Overflow.code = "int53Overflow"
Lean2Js.Err.outOfFuel.code = "outOfFuel"
Lean2Js.Err.indexOutOfBounds.code = "indexOutOfBounds"
Lean2Js.Err.noMatchingAlternative.code = "noMatchingAlternative"
(Lean2Js.Err.typeError a).code = "typeError"
(Lean2Js.Err.unknownVar a).code = "unknownVar"
(Lean2Js.Err.unknownFn a).code = "unknownFn"
(Lean2Js.Err.arity a).code = "arity"

Instances For

Used by

def

Lean2Js.Value.beq

source

@[irreducible]

Value → Value → Bool

Structural equality. JS's === compares references, so the generated code calls a helper following the same rules.

Equations

(Lean2Js.Value.bool a).beq (Lean2Js.Value.bool b) = (a == b)
(Lean2Js.Value.int53 a).beq (Lean2Js.Value.int53 b) = (a == b)
(Lean2Js.Value.uint32 a).beq (Lean2Js.Value.uint32 b) = (a == b)
(Lean2Js.Value.str a).beq (Lean2Js.Value.str b) = (a == b)
(Lean2Js.Value.bigint a).beq (Lean2Js.Value.bigint b) = (a == b)
(Lean2Js.Value.obj ca fa).beq (Lean2Js.Value.obj cb fb) = (ca == cb && Lean2Js.Value.beqFields fa fb)
(Lean2Js.Value.arr xs).beq (Lean2Js.Value.arr ys) = Lean2Js.Value.beqList xs ys
(Lean2Js.Value.dict a).beq (Lean2Js.Value.dict b) = Lean2Js.Value.beqFields a b
(Lean2Js.Value.fn a).beq (Lean2Js.Value.fn b) = (a == b)
x✝¹.beq x✝ = false

Instances For

Used by

def

Lean2Js.Value.beqFields

source

@[irreducible]

List (String × Value) → List (String × Value) → Bool

Equations

Lean2Js.Value.beqFields [] [] = true
Lean2Js.Value.beqFields ((ka, va) :: as) ((kb, vb) :: bs) = (ka == kb && va.beq vb && Lean2Js.Value.beqFields as bs)
Lean2Js.Value.beqFields x✝¹ x✝ = false

Instances For

Used by

def

Lean2Js.Value.beqList

source

@[irreducible]

List Value → List Value → Bool

Equations

Lean2Js.Value.beqList [] [] = true
Lean2Js.Value.beqList (a :: as) (b :: bs) = (a.beq b && Lean2Js.Value.beqList as bs)
Lean2Js.Value.beqList x✝¹ x✝ = false

Instances For

Used by

instance

Lean2Js.instBEqValue

source

@[instance_reducible]

BEq Value

Equations

Lean2Js.instBEqValue = { beq := Lean2Js.Value.beq }

Used by

theorem

Lean2Js.Value.beq_def

source

(a b : Value) :

(a == b) = a.beq b

Where a proof about matching a pattern literal starts: matchPat compares with ==, and what reduces on a literal is Value.beq.

Used by

Value.beq is structural equality, and the two halves of saying so are what lets a claim about == on an author's own type be settled by comparing encodings.

theorem

Lean2Js.Value.beq_refl

source

(v : Value) :

v.beq v = true

Used by

theorem

Lean2Js.Value.beqFields_refl

source

(fs : List (String × Value)) :

beqFields fs fs = true

Used by

theorem

Lean2Js.Value.beqList_refl

source

(xs : List Value) :

beqList xs xs = true

Used by

theorem

Lean2Js.Value.eq_of_beq

source

{a b : Value} :

a.beq b = true → a = b

Used by

theorem

Lean2Js.Value.eq_of_beqFields

source

{as bs : List (String × Value)} :

beqFields as bs = true → as = bs

Used by

theorem

Lean2Js.Value.eq_of_beqList

source

{as bs : List Value} :

beqList as bs = true → as = bs

Used by

def

Lean2Js.keysDistinct

source

List String → Bool

A JS Map cannot hold one key twice, so a dictionary that does has no value on the other side of the boundary and is rejected there.

Equations

Lean2Js.keysDistinct [] = true
Lean2Js.keysDistinct (k :: rest) = (!rest.contains k && Lean2Js.keysDistinct rest)

Instances For

Used by

def

Lean2Js.entrySet

source

(acc : List (String × Value)) (k : String) (v : Value) :

List (String × Value)

What a Map filled from these entries holds, said on the side of the model's values. It mirrors Js.Runtime.mapSetAll across encodeValue, which is what the entry check needs when a dictionary reached it as a plain object: the object's entries are set into a Map one at a time, and this is the list that Map is left holding.

Equations

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

Instances For

Used by

def

Lean2Js.entrySetAll

source

List (String × Value) → List (String × Value) → List (String × Value)

Equations

Lean2Js.entrySetAll x✝ [] = x✝
Lean2Js.entrySetAll x✝ ((k, v) :: rest) = Lean2Js.entrySetAll (Lean2Js.entrySet x✝ k v) rest

Instances For

Used by

def

Lean2Js.Value.hasTy

source

@[irreducible]

(p : Core.Program) :

Value → Core.Ty → Bool

Checks that a value matches its declared type. This is what pins the public API boundary down by type.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Value.hasTy p (Lean2Js.Value.bool b) Lean2Js.Core.Ty.bool = true
Lean2Js.Value.hasTy p (Lean2Js.Value.int53 i) Lean2Js.Core.Ty.int53 = (decide (Lean2Js.int53Min ≤ i) && decide (i ≤ Lean2Js.int53Max))
Lean2Js.Value.hasTy p (Lean2Js.Value.uint32 n) Lean2Js.Core.Ty.uint32 = true
Lean2Js.Value.hasTy p (Lean2Js.Value.str s) Lean2Js.Core.Ty.string = true
Lean2Js.Value.hasTy p (Lean2Js.Value.bigint i) Lean2Js.Core.Ty.bigint = true
Lean2Js.Value.hasTy p (Lean2Js.Value.obj "none" fields) elem.option = fields.isEmpty
Lean2Js.Value.hasTy p (Lean2Js.Value.obj "some" fields) elem.option = Lean2Js.Value.hasFieldTys p fields [("value", elem)]
Lean2Js.Value.hasTy p (Lean2Js.Value.obj ctor fields) elem.option = false
Lean2Js.Value.hasTy p (Lean2Js.Value.obj "ok" fields) (ok.result err) = Lean2Js.Value.hasFieldTys p fields [("value", ok)]
Lean2Js.Value.hasTy p (Lean2Js.Value.obj "error" fields) (ok.result err) = Lean2Js.Value.hasFieldTys p fields [("error", err)]
Lean2Js.Value.hasTy p (Lean2Js.Value.obj ctor fields) (ok.result err) = false
Lean2Js.Value.hasTy p (Lean2Js.Value.arr xs) elem.array = Lean2Js.Value.hasElemTy p xs elem
Lean2Js.Value.hasTy p (Lean2Js.Value.dict entries) elem.dict = (Lean2Js.keysDistinct (List.map (fun (x : String × Lean2Js.Value) => x.fst) entries) && Lean2Js.Value.hasEntryTys p entries elem)
Lean2Js.Value.hasTy p x✝¹ x✝ = false

Instances For

Used by

def

Lean2Js.Value.hasFieldTys

source

@[irreducible]

(p : Core.Program) :

List (String × Value) → List (String × Core.Ty) → Bool

Equations

Lean2Js.Value.hasFieldTys p [] [] = true
Lean2Js.Value.hasFieldTys p ((key, value) :: rest) ((name, ty) :: tys) = (key == name && Lean2Js.Value.hasTy p value ty && Lean2Js.Value.hasFieldTys p rest tys)
Lean2Js.Value.hasFieldTys p x✝¹ x✝ = false

Instances For

Used by

def

Lean2Js.Value.hasElemTy

source

@[irreducible]

(p : Core.Program) :

List Value → Core.Ty → Bool

Equations

Lean2Js.Value.hasElemTy p [] x✝ = true
Lean2Js.Value.hasElemTy p (x_2 :: rest) x✝ = (Lean2Js.Value.hasTy p x_2 x✝ && Lean2Js.Value.hasElemTy p rest x✝)

Instances For

Used by

def

Lean2Js.Value.hasEntryTys

source

@[irreducible]

(p : Core.Program) :

List (String × Value) → Core.Ty → Bool

Equations

Lean2Js.Value.hasEntryTys p [] x✝ = true
Lean2Js.Value.hasEntryTys p ((fst, v) :: rest) x✝ = (Lean2Js.Value.hasTy p v x✝ && Lean2Js.Value.hasEntryTys p rest x✝)

Instances For

Used by

Reading the entry check #

The check a public function runs on its arguments is stated over Value.hasTy, which is defined by well-founded recursion and so does not reduce on its own. One lemma per shape lets a proof about a declaration discharge the check without unfolding the type machinery by hand.

theorem

Lean2Js.hasTy_bool

source

(p : Core.Program) (b : Bool) :

Value.hasTy p (Value.bool b) Core.Ty.bool = true

Used by

theorem

Lean2Js.hasTy_uint32

source

(p : Core.Program) (n : UInt32) :

Value.hasTy p (Value.uint32 n) Core.Ty.uint32 = true

Used by

theorem

Lean2Js.hasTy_str

source

(p : Core.Program) (s : String) :

Value.hasTy p (Value.str s) Core.Ty.string = true

Used by

theorem

Lean2Js.hasTy_bigint

source

(p : Core.Program) (i : Int) :

Value.hasTy p (Value.bigint i) Core.Ty.bigint = true

Used by

theorem

Lean2Js.hasTy_int53

source

(p : Core.Program) (i : Int) :

Value.hasTy p (Value.int53 i) Core.Ty.int53 = (decide (int53Min ≤ i) && decide (i ≤ int53Max))

Used by

theorem

Lean2Js.hasTy_named

source

(p : Core.Program) (ctor : String) (fields : List (String × Value)) (n : String) (args : List Core.Ty) (t : Core.TypeDef) (c : Core.CtorDef) (ht : p.findType? n = some t) (hc : t.findAt? args ctor = some c) :

Value.hasTy p (Value.obj ctor fields) (Core.Ty.named n args) = Value.hasFieldTys p fields (List.map (fun (f : Core.Field) => (f.name, f.ty)) c.fields)

Used by

theorem

Lean2Js.hasTy_none

source

(p : Core.Program) (elem : Core.Ty) :

Value.hasTy p (Value.obj "none" []) elem.option = true

Used by

theorem

Lean2Js.hasTy_some

source

(p : Core.Program) (fields : List (String × Value)) (elem : Core.Ty) :

Value.hasTy p (Value.obj "some" fields) elem.option = Value.hasFieldTys p fields [("value", elem)]

Used by

theorem

Lean2Js.hasTy_ok

source

(p : Core.Program) (fields : List (String × Value)) (ok err : Core.Ty) :

Value.hasTy p (Value.obj "ok" fields) (ok.result err) = Value.hasFieldTys p fields [("value", ok)]

Used by

theorem

Lean2Js.hasTy_error

source

(p : Core.Program) (fields : List (String × Value)) (ok err : Core.Ty) :

Value.hasTy p (Value.obj "error" fields) (ok.result err) = Value.hasFieldTys p fields [("error", err)]

Used by

theorem

Lean2Js.hasTy_array

source

(p : Core.Program) (xs : List Value) (elem : Core.Ty) :

Value.hasTy p (Value.arr xs) elem.array = Value.hasElemTy p xs elem

Used by

theorem

Lean2Js.hasTy_dict

source

(p : Core.Program) (entries : List (String × Value)) (elem : Core.Ty) :

Value.hasTy p (Value.dict entries) elem.dict = (keysDistinct (List.map (fun (x : String × Value) => x.fst) entries) && Value.hasEntryTys p entries elem)

Used by

theorem

Lean2Js.hasTy_dictObj

source

(p : Core.Program) (entries : List (String × Value)) (elem : Core.Ty) :

Value.hasTy p (Value.dict entries) elem.dictObj = (keysDistinct (List.map (fun (x : String × Value) => x.fst) entries) && Value.hasEntryTys p entries elem)

A dictionary declared to cross as a plain object is the same value as one that crosses as a Map: the constructor moves the boundary's shape, not the model's.

Used by

theorem

Lean2Js.hasTy_dictObj_eq_dict

source

(p : Core.Program) (v : Value) (elem : Core.Ty) :

Value.hasTy p v elem.dictObj = Value.hasTy p v elem.dict

The two spellings of a dictionary ask a value for exactly the same thing. This is what lets one operation read a receiver at either of them: what the constructor decides is the shape the boundary writes, and inside the module there is one predicate, not two.

Used by

theorem