Skip to content

Lean2Js.Enc

Imports 2

Where an ordinary Lean type sits inside `Value` #

eval answers with a Value, so a certificate about an author's def has to say which Value the def's result is. Enc is that correspondence: one instance per type an author may write, carrying the subset type it lands in, the encoding, and the decoding that shows the encoding does not fold two terms into one.

The entry check is not a law of the class. toValue is total and the boundary is not — Enc Int encodes every Int, including the ones past Int53 that Decl.decl_refuses turns away. So hasTy holds only of the values accepts admits, and accepts is what an author sees as a hypothesis on their shipped theorem. A type whose encoding cannot reach outside its subset type carries accepts _ _ := True and the hypothesis disappears.

Value.bigint and Value.dict are instanced in Lean2Js/Prelude.lean rather than here: both need a Lean type that is not already spoken for, since Int encodes to Int53 and List (String × α) would be an array. Value.fn gets none at all — it names a declaration, and no Lean function value knows which declaration it is.

class

Lean2Js.Enc

(α : Type) :

How a Lean type is carried across the boundary.

ty : Core.Ty
toValue : α → Value
ofValue : Value → Option α
ofValue_toValue(a : α) : ofValue (toValue a) = some a
accepts : Core.Program → α → Prop
What the boundary asks of the program and the value before toValue a may cross.
toValue_hasTy{p : Core.Program} {a : α} : accepts p a → Value.hasTy p (toValue a) (ty α) = true

Instances

Used by

The scalars #

instance

Lean2Js.Enc.instBool

@[instance_reducible]

:

Equations

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

Used by

theorem

Lean2Js.Enc.ty_bool

@[simp]

:

ty Bool = Core.Ty.bool

Used by

theorem

Lean2Js.Enc.toValue_bool

@[simp]

(b : Bool) :

toValue b = Value.bool b

Used by

instance

Lean2Js.Enc.instInt

@[instance_reducible]

:

Equations

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

Used by

theorem

Lean2Js.Enc.ty_int

@[simp]

:

ty Int = Core.Ty.int53

Used by

theorem

Lean2Js.Enc.toValue_int

@[simp]

(i : Int) :

toValue i = Value.int53 i

Used by

instance

Lean2Js.Enc.instUInt32

@[instance_reducible]

:

Equations

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

Used by

theorem

Lean2Js.Enc.ty_uint32

@[simp]

:

ty UInt32 = Core.Ty.uint32

Used by

theorem

Lean2Js.Enc.toValue_uint32

@[simp]

(n : UInt32) :

toValue n = Value.uint32 n

Used by

instance

Lean2Js.Enc.instString

@[instance_reducible]

:

Equations

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

Used by

theorem

Lean2Js.Enc.ty_string

@[simp]

:

ty String = Core.Ty.string

Used by

theorem

Lean2Js.Enc.toValue_str

@[simp]

(s : String) :

toValue s = Value.str s

Used by

theorem

Lean2Js.Enc.toValue_inj

{α : Type} [Enc α] {a b : α} (h : toValue a = toValue b) :

a = b

No two terms share an encoding. ofValue recovers the term, so a type's Enc already says this; what it takes to use it is naming the step.

Used by

class

Lean2Js.Enc.EncBEq

(α : Type) [Enc α] [BEq α] :

The types the subset compares for equality. eval compares encodings and the author writes == on their own type, so the two agree exactly when the encoding neither folds two terms together nor splits one apart. It is a class of its own rather than a law of Enc because a type with no BEq has nothing to state.

beq_toValue(a b : α) : (toValue a == toValue b) = (a == b)

Instances

Used by

instance

Lean2Js.Enc.instEncBEqOfLawfulBEq

{α : Type} [Enc α] [BEq α] [LawfulBEq α] :

Injectivity is one half; the other is that both ==s decide equality rather than something coarser. An author's own type reaches this by deriving DecidableEq, which is where its LawfulBEq comes from.

Used by

The shapes built out of another type #

instance

Lean2Js.Enc.instOption

@[instance_reducible]

{α : Type} [Enc α] :

Enc (Option α)

Equations

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

Used by

The subset type is normalised the way the scalars are, because a declaration's parameter carries it as this projection. The encoding is not: nothing in the subset's own forms needs it rewritten, and what does is a match on one, whose arm has to reach the tag the pattern tests.

theorem

Lean2Js.Enc.ty_option

@[simp]

{α : Type} [Enc α] :

ty (Option α) = (ty α).option

Used by

theorem

Lean2Js.Enc.toValue_none

{α : Type} [Enc α] :

toValue none = Value.obj "none" []

Used by

theorem

Lean2Js.Enc.toValue_some

{α : Type} [Enc α] (a : α) :

toValue (some a) = Value.obj "some" [("value", toValue a)]

Used by

instance

Lean2Js.Enc.instExcept

@[instance_reducible]

{ε α : Type} [Enc ε] [Enc α] :

Enc (Except ε α)

Equations

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

Used by

theorem

Lean2Js.Enc.ty_except

@[simp]

{ε α : Type} [Enc ε] [Enc α] :

ty (Except ε α) = (ty α).result (ty ε)

Used by

theorem

Lean2Js.Enc.toValue_ok

{ε α : Type} [Enc ε] [Enc α] (a : α) :

toValue (Except.ok a) = Value.obj "ok" [("value", toValue a)]

Used by

theorem

Lean2Js.Enc.toValue_error

{ε α : Type} [Enc ε] [Enc α] (e : ε) :

toValue (Except.error e) = Value.obj "error" [("error", toValue e)]

Used by

theorem

Lean2Js.Enc.hasFieldTys_cons_of

(p : Core.Program) (key : String) (v : Value) (ty : Core.Ty) (rest : List (String × Value)) (tys : List (String × Core.Ty)) (hv : Value.hasTy p v ty = true) (hrest : Value.hasFieldTys p rest tys = true) :

Value.hasFieldTys p ((key, v) :: rest) ((key, ty) :: tys) = true

One field of an object, checked against one field of the declared type. The value and its type are taken as they are rather than through Enc, which is what a field whose type is the one being declared needs: that type has no instance yet where its own encoding is being written.

Used by

theorem

Lean2Js.Enc.hasFieldTys_toValue

(p : Core.Program) (key : String) {α : Type} [Enc α] (x : α) (rest : List (String × Value)) (tys : List (String × Core.Ty)) (hx : accepts p x) (hrest : Value.hasFieldTys p rest tys = true) :

Value.hasFieldTys p ((key, toValue x) :: rest) ((key, ty α) :: tys) = true

One field of a constructor, for the instance a deriving Enc writes: the entry check on an object is the checks on its fields, and each field's is its own Enc's.

Used by

instance

Lean2Js.Enc.instList

@[instance_reducible]

{α : Type} [Enc α] :

Equations

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

Used by

theorem

Lean2Js.Enc.ty_list

@[simp]

{α : Type} [Enc α] :

ty (List α) = (ty α).array

Used by

theorem

Lean2Js.Enc.toValue_list

@[simp]

{α : Type} [Enc α] (xs : List α) :

toValue xs = Value.arr (List.map toValue xs)

Used by