Skip to content

Lean2Js.Vectors

Imports 4

The inputs of the differential test and the values `eval` must return #

Builds the inputs of the differential test and the values eval is expected to return. What agreement means, and the file both checkers read, are in Lean2Js/Agree.lean: saying what the generated code must hand back needs the encoding, and the encoding is that module's subject.

Traps are encoded as expected values too. Division by zero and Int53 overflow are the central design decision for lining JS and Lean up, so "that it throws" is itself the behaviour we want to check.

def

Lean2Js.bmpMax

:

The last character of the BMP. JS's .length counts UTF-16 units, so past here it splits from Lean.

Equations

Lean2Js.bmpMax = String.singleton (Char.ofNat 65535)

Instances For

Used by

def

Lean2Js.astral

:

A character outside the BMP. In JS it becomes a surrogate pair, two units long.

Equations

Lean2Js.astral = String.singleton (Char.ofNat 65536)

Instances For

Used by

def

Lean2Js.dictKeyPool

:

The keys a generated dictionary uses. They are drawn from the strings a String parameter is offered, so a lookup in one of these dictionaries can actually hit.

Equations

Lean2Js.dictKeyPool = ["a", "b", "ab"]

Instances For

Used by

def

Lean2Js.namedDepth

(p : Core.Program) :

How many declared types deep a generated value goes. A type that names itself has no finite set of values, so the generator stops expanding one this far down and the constructors that reach it drop out — which for a well-founded inductive leaves the ones that do not, and those are its base cases.

Deep enough that no type which does not name itself is cut short: tyDescBudget bounds the expansion of such a type by the number of declared types, and nothing here goes further than the descriptor does.

Equations

Lean2Js.namedDepth p = p.types.length + 1

Instances For

Used by

partial def

Lean2Js.edgeCases

(p : Core.Program) (depth width : Nat) :

Core.Ty → List Value

Always steps just inside and just outside the boundary. Overflow and rounding break nowhere else.

Used by

inductive

Lean2Js.ArgShape

:

How an argument is written on the JS side. encodeValue puts the key the constructor's name is carried under first and the declared fields in declared order, but the .d.ts names no order and tolerates keys the type does not declare, so both of those readings need vectors of their own. Neither is a Value: the perturbation rides alongside the argument and is applied to its encoding.

asObject is not a perturbation of the encoding but a second encoding: the argument read through the type it was declared at, so a dictionary the type says crosses as a plain object is written as one. It cannot be a perturbation, because whether a dictionary crosses as an object is the declared type's to say — turning every Map into an object would be refused at a Dict parameter.

canonical : ArgShape
reversed : ArgShape
extraKey : ArgShape
asObject : ArgShape

Instances For

Used by

def

Lean2Js.instBEqArgShape.beq

:

ArgShape → ArgShape → Bool

Equations

Lean2Js.instBEqArgShape.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

Used by

instance

Lean2Js.instBEqArgShape

@[instance_reducible]

:

Equations

Lean2Js.instBEqArgShape = { beq := Lean2Js.instBEqArgShape.beq }

Used by

def

Lean2Js.instReprArgShape.repr

:

ArgShape → Nat → Std.Format

Equations

Lean2Js.instReprArgShape.repr Lean2Js.ArgShape.canonical prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean2Js.ArgShape.canonical")).group prec✝
Lean2Js.instReprArgShape.repr Lean2Js.ArgShape.reversed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean2Js.ArgShape.reversed")).group prec✝
Lean2Js.instReprArgShape.repr Lean2Js.ArgShape.extraKey prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean2Js.ArgShape.extraKey")).group prec✝
Lean2Js.instReprArgShape.repr Lean2Js.ArgShape.asObject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean2Js.ArgShape.asObject")).group prec✝

Instances For

Used by

instance

Lean2Js.instReprArgShape

@[instance_reducible]

:

Equations

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

Used by

instance

Lean2Js.instInhabitedArgShape

@[instance_reducible]

:

Inhabited ArgShape

Equations

Lean2Js.instInhabitedArgShape = { default := Lean2Js.instInhabitedArgShape.default }

Used by

def

Lean2Js.ArgShape.render

:

ArgShape → String

Equations

Lean2Js.ArgShape.canonical.render = "canonical"
Lean2Js.ArgShape.reversed.render = "reversed"
Lean2Js.ArgShape.extraKey.render = "extraKey"
Lean2Js.ArgShape.asObject.render = "asObject"

Instances For

Used by

def

Lean2Js.extraKeyName

:

The key ArgShape.extraKey adds. It is not an identifier, so no program can declare a field by that name and the key is undeclared whatever the program is.

Equations

Lean2Js.extraKeyName = "not a field"

Instances For

Used by

structure

Lean2Js.TestVector

:

fn : String
args : List Value
argTys : List Core.Ty
The types the parameters were declared at, in order. How an argument is written can depend on its type — a dictionary at a Dict.Obj parameter crosses as a plain object — so the types travel with the vector rather than being looked up by name again at each reader.
expected : Except Err Value
ret : Core.Ty
The declaration's return type. The entry hands its result back through it, so it is what decides whether a dictionary comes back as a Map or as a plain object, and both checkers read it rather than assuming the encoding a Value has on its own.
shapes : List ArgShape

Instances For

Used by

def

Lean2Js.TestVector.shapeAt

(v : TestVector) (i : Nat) :

Equations

v.shapeAt i = v.shapes.getD i Lean2Js.ArgShape.canonical

Instances For

Used by

def

Lean2Js.TestVector.writtenArgs

(v : TestVector) :

List (ArgShape × Core.Ty × Value)

Each argument with the type it was declared at and the way this vector says to write it. Pairing the three lists once here is what keeps a reader from having to default a type it could not find.

Equations

v.writtenArgs = List.map (fun (x : (Lean2Js.Value × Lean2Js.Core.Ty) × Nat) => match x with | ((a, ty), i) => (v.shapeAt i, ty, a)) (v.args.zip v.argTys).zipIdx

Instances For

Used by

partial def

Lean2Js.Value.toJson

[Core.Discriminators] :

The key a constructor's name is carried under travels with the vector: the script on Node builds the argument the way the generated code expects it, and that is the type's own key rather than a fixed one.

Used by

def

Lean2Js.vectorsFor

(p : Core.Program) (d : Core.Decl) (edgeLimit randomCount : Nat) (seed : UInt64) :

List TestVector

Equations

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

Instances For

Used by

def

Lean2Js.allTestVectors

(p : Core.Program) (edgeLimit randomCount : Nat) :

List TestVector

Equations

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

Instances For

Used by