Sorts

Ground monomorphic types. They name the sort of a value in the denotational semantics (Strata.DL.Lambda.Denote.LExprDenote) and the element types of collection literals (LConst.mapConst, LConst.sequenceConst). Their properties, and their decidable equality, are in Strata.DL.Lambda.LSortProps.

inductive Lambda.LSort : Type

A sort is a ground monomorphic type — an LMonoTy with no free type variables. We use a separate type rather than LMonoTy to avoid carrying around proofs that a type has no type variables.

• tcons (name : String) (args : List LSort) : LSort

  A named type constructor applied to sort arguments.

• bitvec (size : Nat) : LSort

  A bit vector sort of the given size.

partial def Lambda.instReprLSort.repr : LSort → Nat → Std.Format

@[instance_reducible]

instance Lambda.instReprLSort : Repr LSort

Equations

• Lambda.instReprLSort = { reprPrec := Lambda.instReprLSort.repr }

partial def Lambda.instHashableLSort.hash : LSort → UInt64

@[instance_reducible]

instance Lambda.instHashableLSort : Hashable LSort

Equations

• Lambda.instHashableLSort = { hash := Lambda.instHashableLSort.hash }

@[reducible, inline]

abbrev Lambda.LSort.bool : LSort

The Boolean sort.

Equations

• Lambda.LSort.bool = Lambda.LSort.tcons "bool" []

@[reducible, inline]

abbrev Lambda.LSort.int : LSort

The integer sort.

Equations

• Lambda.LSort.int = Lambda.LSort.tcons "int" []

@[reducible, inline]

abbrev Lambda.LSort.real : LSort

The real sort.

Equations

• Lambda.LSort.real = Lambda.LSort.tcons "real" []

@[reducible, inline]

abbrev Lambda.LSort.string : LSort

The string sort.

Equations

• Lambda.LSort.string = Lambda.LSort.tcons "string" []

@[reducible, inline]

abbrev Lambda.LSort.map (k v : LSort) : LSort

The sort Map k v of the total maps from k to v.

Equations

• k.map v = Lambda.LSort.tcons "Map" [k, v]

@[reducible, inline]

abbrev Lambda.LSort.seq (a : LSort) : LSort

The sort Sequence a of the finite sequences of a.

Equations

• a.seq = Lambda.LSort.tcons "Sequence" [a]

def Lambda.LSort_eqb (s1 s2 : LSort) : Bool

Boolean equality of sorts, structurally.

Equations

• Lambda.LSort_eqb (Lambda.LSort.tcons n1 a1) (Lambda.LSort.tcons n2 a2) = (n1 == n2 && Lambda.LSort_eqb.LSort_eqb_list✝ a1 a2)
• Lambda.LSort_eqb (Lambda.LSort.bitvec s1_2) (Lambda.LSort.bitvec s2_2) = (s1_2 == s2_2)
• Lambda.LSort_eqb s1 s2 = false

@[irreducible]

def Lambda.LSort.rec' (P : LSort → Sort u) (htcons : (name : String) → (args : List LSort) → ((x : LSort) → x ∈ args → P x) → P (tcons name args)) (hbitvec : (n : Nat) → P (bitvec n)) (s : LSort) : P s

Recursion on sorts with the hypothesis on the arguments of a constructor stated by list membership.

Equations

• Lambda.LSort.rec' P htcons hbitvec (Lambda.LSort.tcons a a_1) = htcons a a_1 fun (x : Lambda.LSort) (x_1 : x ∈ a_1) => Lambda.LSort.rec' P htcons hbitvec x
• Lambda.LSort.rec' P htcons hbitvec (Lambda.LSort.bitvec a) = hbitvec a

def Lambda.LSort.toMonoTy : LSort → LMonoTy

The monomorphic type (without type variables) naming a sort.

Equations

• (Lambda.LSort.tcons name args).toMonoTy = Lambda.LMonoTy.tcons name (Lambda.LSort.toMonoTy.map args)
• (Lambda.LSort.bitvec n).toMonoTy = Lambda.LMonoTy.bitvec n

def Lambda.LSort.toMonoTy.map : List LSort → List LMonoTy

Equations

• Lambda.LSort.toMonoTy.map [] = []
• Lambda.LSort.toMonoTy.map (s :: ss) = s.toMonoTy :: Lambda.LSort.toMonoTy.map ss

def Lambda.LSort.hasMap : LSort → Bool

Whether a sort mentions the Map type constructor anywhere. Two well-typed constants of a sort without Map are equal exactly when they denote the same value; map literals are not canonical (two different literals can denote the same map, e.g. when the key sort is finite), so for them only syntactic equality is known to imply semantic equality.

Equations

• (Lambda.LSort.tcons name args).hasMap = (name == "Map" || Lambda.LSort.hasMap.hasMapList args)
• (Lambda.LSort.bitvec n).hasMap = false

def Lambda.LSort.hasMap.hasMapList : List LSort → Bool

Equations

• Lambda.LSort.hasMap.hasMapList [] = false
• Lambda.LSort.hasMap.hasMapList (s :: ss) = (s.hasMap || Lambda.LSort.hasMap.hasMapList ss)

def Lambda.LMonoTy.toSort? : LMonoTy → Option LSort

The sort a monomorphic type names, if it has no type variables.

Equations

• (Lambda.LMonoTy.ftvar name).toSort? = none
• (Lambda.LMonoTy.bitvec n).toSort? = some (Lambda.LSort.bitvec n)
• (Lambda.LMonoTy.tcons name args).toSort? = Option.map (Lambda.LSort.tcons name) (Lambda.LMonoTy.toSort?.toSortList? args)

def Lambda.LMonoTy.toSort?.toSortList? : List LMonoTy → Option (List LSort)

Equations

• Lambda.LMonoTy.toSort?.toSortList? [] = some []
• Lambda.LMonoTy.toSort?.toSortList? (t :: ts) = match t.toSort?, Lambda.LMonoTy.toSort?.toSortList? ts with | some s, some ss => some (s :: ss) | x, x_1 => none