Skip to content

Lean2Js.Exhaustive

Imports 2

A `match` the compiler accepted has an arm for every value of its scrutinee #

Maranget's usefulness test, read back as a statement about values: a match the compiler accepted as exhaustive has an arm for every value of the scrutinee's type.

The generated code takes its last arm without a test, so this is what says the reference semantics never reaches the end of the chain either — evalExpr returns noMatchingAlternative for no scrutinee the entry check let through.

def

Lean2Js.Exhaustive.Covers

(rows : List (List Core.Pat)) (vs : List Value) :

Some row of the matrix accepts the value vector.

Equations

Lean2Js.Exhaustive.Covers rows vs = ∃ (row : List Lean2Js.Core.Pat), row ∈ rows ∧ (Lean2Js.matchPats row vs).isSome = true

Instances For

Used by

def

Lean2Js.Exhaustive.ValuesTyped

(p : Core.Program) :

List Value → List Core.Ty → Prop

The columns type the values, pairwise.

Equations

Lean2Js.Exhaustive.ValuesTyped p [] [] = True
Lean2Js.Exhaustive.ValuesTyped p (v :: vs) (ty :: tys) = (Lean2Js.Value.hasTy p v ty = true ∧ Lean2Js.Exhaustive.ValuesTyped p vs tys)
Lean2Js.Exhaustive.ValuesTyped p x✝¹ x✝ = False

Instances For

Used by

Reading `matchPats` apart #

theorem

Lean2Js.Exhaustive.matchPats_nil_inv

[Core.Discriminators] {vs : List Value} (h : (matchPats [] vs).isSome = true) :

vs = []

Used by

theorem

Lean2Js.Exhaustive.matchPats_nil

[Core.Discriminators] :

(matchPats [] []).isSome = true

Used by

theorem

Lean2Js.Exhaustive.matchPats_cons_inv

[Core.Discriminators] {pat : Core.Pat} {pats : List Core.Pat} {vs : List Value} (h : (matchPats (pat :: pats) vs).isSome = true) :

∃ (v : Value ), ∃ (vs' : List Value), vs = v :: vs' ∧ (matchPat pat v).isSome = true ∧ (matchPats pats vs').isSome = true

Used by

theorem

Lean2Js.Exhaustive.matchPats_cons

[Core.Discriminators] {pat : Core.Pat} {pats : List Core.Pat} {v : Value} {vs : List Value} (hp : (matchPat pat v).isSome = true) (hr : (matchPats pats vs).isSome = true) :

(matchPats (pat :: pats) (v :: vs)).isSome = true

Used by

theorem

Lean2Js.Exhaustive.matchPats_length

[Core.Discriminators] {pats : List Core.Pat} {vs : List Value} :

(matchPats pats vs).isSome = true → pats.length = vs.length

Used by

theorem

Lean2Js.Exhaustive.matchPats_append

[Core.Discriminators] {as : List Core.Pat} {xs : List Value} {bs : List Core.Pat} {ys : List Value} :

(matchPats as xs).isSome = true → (matchPats bs ys).isSome = true → (matchPats (as ++ bs) (xs ++ ys)).isSome = true

Used by

theorem

Lean2Js.Exhaustive.matchPats_append_inv

[Core.Discriminators] {as : List Core.Pat} {xs : List Value} {bs : List Core.Pat} {ys : List Value} :

as.length = xs.length → (matchPats (as ++ bs) (xs ++ ys)).isSome = true → (matchPats as xs).isSome = true ∧ (matchPats bs ys).isSome = true

Used by

The head a value takes #

The matrix splits a column by the head of its values. A value of a type the signature enumerates carries exactly one of the heads, with the fields that head lists.

def

Lean2Js.Exhaustive.HeadOf

(h : Compile.Head) (v : Value) (fieldVs : List Value) :

The value a head stands for, and the fields it carries.

Equations

Lean2Js.Exhaustive.HeadOf (Lean2Js.Compile.Head.lit l) v fieldVs = ((Lean2Js.litValue l == v) = true ∧ fieldVs = [])
Lean2Js.Exhaustive.HeadOf (Lean2Js.Compile.Head.ctor name) (Lean2Js.Value.obj ctor fields) fieldVs = (name = ctor ∧ fieldVs = List.map (fun (x : String × Lean2Js.Value) => x.snd) fields)
Lean2Js.Exhaustive.HeadOf (Lean2Js.Compile.Head.ctor name) v fieldVs = False

Instances For

Used by

theorem

Lean2Js.Exhaustive.lit_beq_eq

[Core.Discriminators] {a b : Core.Lit} :

(a == b) = true → a = b

Used by

theorem

Lean2Js.Exhaustive.head_beq_eq

[Core.Discriminators] {a b : Compile.Head} :

(a == b) = true → a = b

Used by

theorem

Lean2Js.Exhaustive.litValue_beq_self

[Core.Discriminators] (l : Core.Lit) :

(litValue l == litValue l) = true

A literal's value equals itself. The matcher compares by Value.beq, and a literal pattern only ever faces the value the same literal builds.

Used by

Reading the matrix apart #

specialize and defaultRows are how the test splits a column. Both directions of the split have to be read back as statements about the values a row accepts.

theorem

Lean2Js.Exhaustive.covers_of_specialize

[Core.Discriminators] {hd : Compile.Head} {v : Value} {fieldVs restVs : List Value} {arity : Nat} (hv : HeadOf hd v fieldVs) (harity : arity = fieldVs.length) (rows : List (List Core.Pat)) (hcov : Covers (Compile.specialize hd arity rows) (fieldVs ++ restVs)) :

Covers rows (v :: restVs)

A row of the specialized matrix that accepts the head's fields, followed by the rest of the vector, comes from a row of the original that accepts the value itself.

Used by

theorem

Lean2Js.Exhaustive.covers_of_defaultRows

[Core.Discriminators] {v : Value} {restVs : List Value} (rows : List (List Core.Pat)) :

Covers (Compile.defaultRows rows) restVs → Covers rows (v :: restVs)

A row of the default matrix that accepts the rest of the vector comes from a row of the original whose head is a wildcard, which accepts any value in front of it.

Used by

The head a typed value takes #

theorem

Lean2Js.Exhaustive.valuesTyped_of_hasFieldTys

[Core.Discriminators] {p : Core.Program} {fields : List (String × Value)} {ftys : List (String × Core.Ty)} :

Value.hasFieldTys p fields ftys = true → ValuesTyped p (List.map (fun (x : String × Value) => x.snd) fields) (List.map (fun (x : String × Core.Ty) => x.snd) ftys)

Used by

theorem

Lean2Js.Exhaustive.head_of_hasTy

[Core.Discriminators] {p : Core.Program} {ty : Core.Ty} {v : Value} {heads : List (Compile.Head × List (String × Core.Ty))} (hsig : Compile.signature p.types ty = some heads) (hv : Value.hasTy p v ty = true) :

∃ (hd : Compile.Head ), ∃ (fields : List (String × Core.Ty)), ∃ (fieldVs : List Value), List.find? (fun (x : Compile.Head × List (String × Core.Ty)) => x.fst == hd) heads = some (hd, fields) ∧ HeadOf hd v fieldVs ∧ ValuesTyped p fieldVs (List.map (fun (x : String × Core.Ty) => x.snd) fields)

A value of a type the signature enumerates carries one of the heads it lists, with fields of the types that head names. This is what says a wildcard column with every head seen leaves nothing out.

Used by

Widths #

The matrix's rows are as wide as the query. Splitting a column keeps them lined up.

def

Lean2Js.Exhaustive.SameWidth

(rows : List (List Core.Pat)) (n : Nat) :

Equations

Lean2Js.Exhaustive.SameWidth rows n = ∀ (row : List Lean2Js.Core.Pat), row ∈ rows → row.length = n

Instances For

Used by

theorem

Lean2Js.Exhaustive.sameWidth_specialize

[Core.Discriminators] {hd : Compile.Head} {arity n : Nat} (hlit : ∀ (l : Core.Lit), hd = Compile.Head.lit l → arity = 0) (rows : List (List Core.Pat)) :

SameWidth rows (n + 1) → SameWidth (Compile.specialize hd arity rows) (arity + n)

Used by

theorem

Lean2Js.Exhaustive.sameWidth_defaultRows

[Core.Discriminators] {n : Nat} (rows : List (List Core.Pat)) :

SameWidth rows (n + 1) → SameWidth (Compile.defaultRows rows) n

Used by

theorem

Lean2Js.Exhaustive.valuesTyped_length

[Core.Discriminators] {p : Core.Program} {vs : List Value} {tys : List Core.Ty} :

ValuesTyped p vs tys → vs.length = tys.length

Used by

theorem

Lean2Js.Exhaustive.valuesTyped_append

[Core.Discriminators] {p : Core.Program} {as : List Value} {atys : List Core.Ty} {bs : List Value} {btys : List Core.Ty} :

ValuesTyped p as atys → ValuesTyped p bs btys → ValuesTyped p (as ++ bs) (atys ++ btys)

Used by

theorem

Lean2Js.Exhaustive.matchPats_replicate_wild

[Core.Discriminators] (vs : List Value) :

(matchPats (List.replicate vs.length Core.Pat.wild) vs).isSome = true

Used by

What the test settles #

theorem

Lean2Js.Exhaustive.headOf_obj_inv

[Core.Discriminators] {hd : Compile.Head} {ctor : String} {fields : List (String × Value)} {fieldVs : List Value} (h : HeadOf hd (Value.obj ctor fields) fieldVs) :

hd = Compile.Head.ctor ctor ∧ fieldVs = List.map (fun (x : String × Value) => x.snd) fields

A literal never stands for a constructor value.

Used by

theorem

Lean2Js.Exhaustive.head_fieldTys

[Core.Discriminators] {p : Core.Program} {ty : Core.Ty} {v : Value} {heads : List (Compile.Head × List (String × Core.Ty))} (hsig : Compile.signature p.types ty = some heads) (hv : Value.hasTy p v ty = true) :

∃ (hd : Compile.Head ), ∃ (fields : List (String × Core.Ty)), ∃ (fieldVs : List Value), List.find? (fun (x : Compile.Head × List (String × Core.Ty)) => x.fst == hd) heads = some (hd, fields) ∧ HeadOf hd v fieldVs ∧ ValuesTyped p fieldVs (Compile.fieldTysOf (some heads) hd)

The field types the signature gives a value's head, in the shape fieldTysOf reads them.

Used by

theorem

Lean2Js.Exhaustive.signature_isSome_of_obj

[Core.Discriminators] {p : Core.Program} {ty : Core.Ty} {ctor : String} {fields : List (String × Value)} (hv : Value.hasTy p (Value.obj ctor fields) ty = true) :

(Compile.signature p.types ty).isSome = true

Only a named type, an option or a result has a constructor value, and each of those has a signature. So a value the matcher took apart is one the matrix can split on.

Used by

theorem

Lean2Js.Exhaustive.covered_wildcard

[Core.Discriminators] (p : Core.Program) (budget : Nat) (ih : ∀ (rows : List (List Core.Pat)) (q : List Core.Pat) (tys : List Core.Ty) (vs : List Value), Compile.useful p.types budget rows q tys = false → SameWidth rows q.length → (matchPats q vs).isSome = true → ValuesTyped p vs tys → Covers rows vs) (rows : List (List Core.Pat)) (qs : List Core.Pat) (ty : Core.Ty) (tys : List Core.Ty) (v : Value) (vs' : List Value) (hu : (match Compile.signature p.types ty with | some heads => if (heads.all fun (x : Compile.Head × List (String × Core.Ty)) => (List.filterMap (fun (row : List Core.Pat) => match row with | pat :: tail => Compile.headOf pat | [] => none) rows).contains x.fst) = true then heads.any fun (x : Compile.Head × List (String × Core.Ty)) => Compile.useful p.types budget (Compile.specialize x.fst (List.map (fun (x : String × Core.Ty) => x.snd) x.snd).length rows) (List.replicate (List.map (fun (x : String × Core.Ty) => x.snd) x.snd).length Core.Pat.wild ++ qs) (List.map (fun (x : String × Core.Ty) => x.snd) x.snd ++ tys) else Compile.useful p.types budget (Compile.defaultRows rows) qs tys | none => Compile.useful p.types budget (Compile.defaultRows rows) qs tys) = false) (hw : SameWidth rows (qs.length + 1)) (hrest : (matchPats qs vs').isSome = true) (hvty : Value.hasTy p v ty = true) (hvs' : ValuesTyped p vs' tys) :

Covers rows (v :: vs')

The column a wildcard leaves open. Either the matrix has every head the type can take, and the value carries one of them, or it does not, and the rows that fall through cover the value. Both branches hand the rest of the vector to the induction hypothesis.

Used by

theorem

Lean2Js.Exhaustive.covered_of_useful_false

[Core.Discriminators] (p : Core.Program) (budget : Nat) (rows : List (List Core.Pat)) (q : List Core.Pat) (tys : List Core.Ty) (vs : List Value) :

Compile.useful p.types budget rows q tys = false → SameWidth rows q.length → (matchPats q vs).isSome = true → ValuesTyped p vs tys → Covers rows vs

If the usefulness test finds no value vector that q accepts and every row misses, then a vector the columns type and q accepts is accepted by some row.

match asks this of an all-wildcard q: the answer is that every value of the scrutinee's type is matched by an arm.

Used by

What a compiled `match` settles #

The generated arm chain takes its last arm without a test. That is sound because the compiler refused a match the usefulness test called useful — and by the theorem above, a match it accepted has an arm for every value the scrutinee's type can take. So the reference semantics never reaches the end of the chain either.

theorem

Lean2Js.Exhaustive.useful_false_of_compile

[Core.Discriminators] {p : Core.Program} {ctx : Compile.Ctx} {scrut : Core.Expr} {alts : List Core.Alt} {je : Js.Expr} {ty : Core.Ty} {jscrut : Js.Expr} {tscrut : Core.Ty} (hc : Compile.compileExpr p ctx (scrut.matchE alts) = Except.ok (je, ty)) (hcs : Compile.compileExpr p ctx scrut = Except.ok (jscrut, tscrut)) :

Compile.useful p.types (Compile.usefulBudget p.types [tscrut]) (List.map (fun (x : Core.Pat) => [x]) (List.map Core.Alt.pat alts)) [Core.Pat.wild ] [tscrut] = false

The exhaustiveness check a compiled match passed.

Used by

theorem

Lean2Js.Exhaustive.firstMatch_isSome_of_mem

[Core.Discriminators] {alts : List Core.Alt} {sv : Value} {alt : Core.Alt} (hmem : alt ∈ alts) (hpv : (matchPat alt.pat sv).isSome = true) :

(firstMatch alts sv).isSome = true

An arm whose pattern matches is reached, or an earlier one is.

Used by

theorem

Lean2Js.Exhaustive.firstMatch_isSome

[Core.Discriminators] {p : Core.Program} {ctx : Compile.Ctx} {scrut : Core.Expr} {alts : List Core.Alt} {je jscrut : Js.Expr} {ty tscrut : Core.Ty} {sv : Value} (hc : Compile.compileExpr p ctx (scrut.matchE alts) = Except.ok (je, ty)) (hcs : Compile.compileExpr p ctx scrut = Except.ok (jscrut, tscrut)) (hsv : Value.hasTy p sv tscrut = true) :

(firstMatch alts sv).isSome = true

An arm matches. The chain the generated code walks ends in an arm it takes without a test, and this is what says the reference semantics takes an arm too.

Used by

What a compiled fold settles #

A fold's alternatives are not matched against the value the fold was handed but against the rebuilt node, whose fields that came round carry the fold's answers. That node is a value of no type the language writes, so firstMatch_isSome does not reach it and the compiler does not check its alternatives with useful: it checks them with usefulFold, at foldHeads, which is the same test with the one column's signature handed over rather than read off the declared type.

Checking it at the declared type instead would not be conservative. Two types may declare constructors of the same name, so an alternative may name every constructor the declared type has, pass the test at that type, and still leave a rebuilt node no alternative matches.

theorem

Lean2Js.Exhaustive.covered_of_usefulFold_false

[Core.Discriminators] {p : Core.Program} {heads : List (Compile.Head × List (String × Core.Ty))} {rows : List (List Core.Pat)} {ctor : String} {fields : List (String × Value)} {fs : List (String × Core.Ty)} (hu : Compile.usefulFold p.types heads rows Core.Pat.wild = false) (hw : SameWidth rows 1) (hmem : (Compile.Head.ctor ctor, fs) ∈ heads) (hvs : ValuesTyped p (List.map (fun (x : String × Value) => x.snd) fields) (List.map (fun (x : String × Core.Ty) => x.snd) fs)) :

Covers rows [Value.obj ctor fields]

The rebuilt node a fold's alternatives are matched against is covered by one of them.

covered_of_useful_false's twin at one column. A twin rather than an instance: what types the node's fields is the head list, and no Ty names it.

Used by

theorem

Lean2Js.Exhaustive.usefulFold_false_of_compile

[Core.Discriminators] {p : Core.Program} {ctx : Compile.Ctx} {scrut : Core.Expr} {tn : String} {ta : List Core.Ty} {result : Core.Ty} {alts : List Core.Alt} {je : Js.Expr} {ty : Core.Ty} {t : Core.TypeDef} (hc : Compile.compileExpr p ctx (scrut.foldE tn ta result alts) = Except.ok (je, ty)) (ht : List.find? (fun (x : Core.TypeDef) => x.name == tn) p.types = some t) :

Compile.usefulFold p.types (Compile.foldHeads tn ta result t) (List.map (fun (x : Core.Pat) => [x]) (List.map Core.Alt.pat alts)) Core.Pat.wild = false

The exhaustiveness check a compiled fold passed.

Used by

theorem

Lean2Js.Exhaustive.foldFirstMatch_isSome

[Core.Discriminators] {p : Core.Program} {ctx : Compile.Ctx} {scrut : Core.Expr} {tn : String} {ta : List Core.Ty} {result : Core.Ty} {alts : List Core.Alt} {je : Js.Expr} {ty : Core.Ty} {t : Core.TypeDef} {c : Core.CtorDef} {ctor : String} {fields : List (String × Value)} (hc : Compile.compileExpr p ctx (scrut.foldE tn ta result alts) = Except.ok (je, ty)) (ht : List.find? (fun (x : Core.TypeDef) => x.name == tn) p.types = some t) (hcf : t.findAt? ta ctor = some c) (hvs : ValuesTyped p (List.map (fun (x : String × Value) => x.snd) fields) (List.map (fun (x : String × Core.Ty) => x.snd) (Compile.foldFieldTys tn ta result c.fields))) :

(firstMatch alts (Value.obj ctor fields)).isSome = true

An alternative of a fold matches the rebuilt node. The chain the generated code walks ends in an arm it takes without a test, and this is what says the reference semantics takes an arm too.

Used by