structure ParserError : Type

Contains an error message and the position at which the interpretation of the input string was not possible anymore.

• message : String
• position : Nat
• input : Option String

instance instReprParserError : Repr ParserError

Equations

• instReprParserError = { reprPrec := instReprParserError.repr }

def instReprParserError.repr : ParserError → Nat → Std.Format

Equations

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

instance instBEqParserError : BEq ParserError

Equations

• instBEqParserError = { beq := instBEqParserError.beq }

def instBEqParserError.beq : ParserError → ParserError → Bool

Equations

• instBEqParserError.beq { message := a, position := a_1, input := a_2 } { message := b, position := b_1, input := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• instBEqParserError.beq x✝¹ x✝ = false

def ParserError.toString (e : ParserError) : String

Returns a formatted string that contains the error message and position.

Equations

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

instance ParserError.instToString : ToString ParserError

Equations

• ParserError.instToString = { toString := ParserError.toString }

instance ParserError.instInhabited : Inhabited ParserError

Defines a default with "unknown error" as message an implausible position for parser error.

Equations

• ParserError.instInhabited = { default := { message := "unknown error", position := 42 } }

inductive ParserResult (α : Type) : Type

Holds either the value of the given type, if parsing was successful or a parser error in case of failure.

• success {α : Type} : α → ParserResult α
• failure {α : Type} : ParserError → ParserResult α

instance instReprParserResult {α✝ : Type} [Repr α✝] : Repr (ParserResult α✝)

Equations

• instReprParserResult = { reprPrec := instReprParserResult.repr }

def instReprParserResult.repr {α✝ : Type} [Repr α✝] : ParserResult α✝ → Nat → Std.Format

Equations

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

instance instBEqParserResult {α✝ : Type} [BEq α✝] : BEq (ParserResult α✝)

Equations

• instBEqParserResult = { beq := instBEqParserResult.beq }

def instBEqParserResult.beq {α✝ : Type} [BEq α✝] : ParserResult α✝ → ParserResult α✝ → Bool

Equations

• instBEqParserResult.beq (ParserResult.success a) (ParserResult.success b) = (a == b)
• instBEqParserResult.beq (ParserResult.failure a) (ParserResult.failure b) = (a == b)
• instBEqParserResult.beq x✝¹ x✝ = false

instance instInhabitedParserResult {α : Type} : Inhabited (ParserResult α)

Defines a default for ParserResult α based on the default of ParserError.

Equations

• instInhabitedParserResult = { default := ParserResult.failure default }

def ParserResult.isSuccess {α : Type} (res : ParserResult α) : Bool

Returns true iff the ParserResult contains a value of type α.

Equations

• (ParserResult.success a).isSuccess = true
• (ParserResult.failure a).isSuccess = false

def ParserResult.to? {α : Type} (res : ParserResult α) : Option α

Converts a parser result into an optional value.

Equations

• (ParserResult.success a).to? = some a
• (ParserResult.failure a).to? = none

def ParserResult.to! {α : Type} [Inhabited α] (res : ParserResult α) : α

Unwraps the value from a .success parser result and panics if a .failure is provided.

Equations

• (ParserResult.success a).to! = a
• (ParserResult.failure a).to! = panic (toString "no parser result due to " ++ toString a)

def ParserResult.toIO! {α : Type} (res : ParserResult α) : IO α

Converts the value from a .success parser result into an term of IO α and throws an error, if a .failure is provided.

Equations

• (ParserResult.success a).toIO! = pure a
• (ParserResult.failure a).toIO! = throw (IO.userError a.toString)

def NonEmptyList (α : Type) : Type

Defines non-empty lists as subtype of List.

Equations

• NonEmptyList α = { l : List α // (!l.isEmpty) = true }

instance instDecidableEqNonEmptyList (α : Type) [DecidableEq α] : DecidableEq (NonEmptyList α)

Equations

• instDecidableEqNonEmptyList α = Subtype.instDecidableEq

def NonEmptyList.lt {α : Type} [LT α] (a b : NonEmptyList α) : Prop

Less-then (lt) for non-empty lists.

Equations

• a.lt b = a.val.lt b.val

instance NonEmptyList.instLT (α : Type) [LT α] : LT (NonEmptyList α)

Equations

• NonEmptyList.instLT α = { lt := NonEmptyList.lt }

def NonEmptyList.decLt {α : Type} [DecidableEq α] [LT α] [DecidableLT α] (a b : NonEmptyList α) : Decidable (a < b)

Decidable less-then for NonEmptyList.

Equations

• a.decLt b = a.val.decidableLT b.val

instance NonEmptyList.instDecidableLTOfDecidableEq (α : Type) [DecidableEq α] [LT α] [DecidableLT α] : DecidableLT (NonEmptyList α)

Equations

• NonEmptyList.instDecidableLTOfDecidableEq α = NonEmptyList.decLt

def NonEmptyList.repr {α : Type} [Repr α] (a : NonEmptyList α) (n : Nat) : Std.Format

Provides a representation for a non empty list so that #eval can be used.

Equations

• a.repr n = a.val.repr n

instance NonEmptyList.instRepr (α : Type) [Repr α] : Repr (NonEmptyList α)

Equations

• NonEmptyList.instRepr α = { reprPrec := NonEmptyList.repr }

def NonEmptyList.toDotSeparatedString {α : Type} [ToString α] (a : NonEmptyList α) : String

Renders a non-empty list as string with its elements separated by ".".

For instance,

#eval toDotSeparatedString (⟨[0, 1, 2, 3, 4], rfl⟩ : NonEmptyList Nat)

results in "0.1.2.3.4".

Equations

• a.toDotSeparatedString = ".".intercalate (List.map (fun (a : α) => toString a) a.val)

def NonEmptyList.parse {α : Type} (str : String) (parseElement : String → ParserResult α) (sep : Char) : ParserResult (NonEmptyList α)

Parses the given string and, if possible, returns a result containing a non-empty list of terms of type α.

Equations

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

def NonEmptyList.parse.helper {α : Type} (lstr : List String) (parseElement : String → ParserResult α) : ParserResult (List α)

Equations

• One or more equations did not get rendered due to their size.
• NonEmptyList.parse.helper [] parseElement = ParserResult.success []

def NonEmptyString : Type

Defines non-empty strings as subtype of String.

They ensure that the requirement "Identifiers MUST NOT be empty." fulfilled that is stated as item #9 in semver.org.

Equations

• NonEmptyString = { s : String // (!s.isEmpty) = true }

instance instBEqNonEmptyString : BEq NonEmptyString

Equations

• instBEqNonEmptyString = Subtype.instBEq

instance instReprNonEmptyString : Repr NonEmptyString

Equations

• instReprNonEmptyString = instReprSubtype

instance instToStringNonEmptyString : ToString NonEmptyString

Equations

• instToStringNonEmptyString = instToStringSubtype

instance instDecidableEqNonEmptyString : DecidableEq NonEmptyString

Equations

• instDecidableEqNonEmptyString a b = a.instDecidableEq b

def NonEmptyString.lt (a b : NonEmptyString) : Prop

Less-then (lt) for non-empty strings.

Equations

• a.lt b = (a.val < b.val)

instance NonEmptyString.instLT : LT NonEmptyString

Equations

• NonEmptyString.instLT = { lt := NonEmptyString.lt }

def NonEmptyString.decLt (a b : NonEmptyString) : Decidable (a < b)

decLt is the decidable <-relation for non-empty strings, which allows for comparing two non-empty strings as in

#eval decLt (⟨"abc", rfl⟩ : NonEmptyString) (⟨"bcd", rfl⟩ : NonEmptyString)

Equations

• a.decLt b = a.val.decidableLT b.val

instance NonEmptyString.decidableLT (a b : NonEmptyString) : Decidable (a < b)

Equations

• a.decidableLT b = a.decLt b

def NonEmptyString.parse (str : String) : ParserResult NonEmptyString

Parses a given string and returns a result containing a non-empty string if possible.

Equations

• NonEmptyString.parse str = if h : (!str.isEmpty) = true then ParserResult.success ⟨str, h⟩ else ParserResult.failure { message := "string must not be empty", position := 0, input := some str }

def Char.toDigit? : Char → Option Nat

Converts a character representing a digit for base ten to the natural number corresponding to this digit - for other characters none is returned.

This implementation is seemingly better suited for proofs compared than e.g.

def toDigit? (c: Char) : Option Nat :=
  if c.isDigit then
    some (c.toNat - '0'.toNat)
  else
    none

Equations

• '0'.toDigit? = some 0
• '1'.toDigit? = some 1
• '2'.toDigit? = some 2
• '3'.toDigit? = some 3
• '4'.toDigit? = some 4
• '5'.toDigit? = some 5
• '6'.toDigit? = some 6
• '7'.toDigit? = some 7
• '8'.toDigit? = some 8
• '9'.toDigit? = some 9
• x✝.toDigit? = none

def Char.isDigit' (c : Char) : Bool

Is an alternative implementation to the standard function Char.isDigit that is based on Char.toDigit?.

This implementation appears to be better suited for proofs than Char.isDigit.

Equations

• c.isDigit' = match c.toDigit? with | some val => true | none => false

def Char.toDigit (c : Char) (h : c.isDigit' = true) : Nat

Returns the digit as natural number for a given character that is known to be one of '0', '1' ... '9'

Equations

• c.toDigit h = match g : c.toDigit? with | some n => n | none => ⋯.elim

def Char.toDigit! (c : Char) : Nat

Converts a digit to a natural number and panics for characters that are no digits (for base ten).

Equations

• c.toDigit! = match c.toDigit? with | some n => n | none => panicWithPosWithDecl "SemVer.Basic" "Char.toDigit!" 290 14 (toString "'" ++ toString c ++ toString "' is not a digit!")

def NonEmptyString.hasOnlyDigits (nes : NonEmptyString) : Bool

Returns true if the NonEmptyString that is provided as input only contains digits (for base ten). It is based on Char.isDigit', so that it easier to work with it in proofs.

Hence it is used here instead of shorter implementations like

def NonEmptyString.hasOnlyDigits (nes: NonEmptyString) : Bool := nes.val.isNat

Equations

• nes.hasOnlyDigits = NonEmptyString.hasOnlyDigits.helper nes.val.data

def NonEmptyString.hasOnlyDigits.helper : List Char → Bool

Equations

• NonEmptyString.hasOnlyDigits.helper [] = true
• NonEmptyString.hasOnlyDigits.helper (c :: cs) = (c.isDigit' && NonEmptyString.hasOnlyDigits.helper cs)

def Digits : Type

Defines a subtype of NonEmptyString with the restriction that all characters must be digits of base ten.

This is used for the definitions

  <digits> ::= <digit>
            | <digit> <digits>

  <digit> ::= "0"
            | <positive digit>

  <positive digit> ::= "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"

(see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions).

Equations

• Digits = { nes : NonEmptyString // nes.hasOnlyDigits = true }

instance instReprDigits : Repr Digits

Equations

• instReprDigits = instReprSubtype

instance instBEqDigits : BEq Digits

Equations

• instBEqDigits = Subtype.instBEq

instance instToStringDigits : ToString Digits

Equations

• instToStringDigits = instToStringSubtype

instance instDecidableEqDigits : DecidableEq Digits

Equations

• instDecidableEqDigits a b = a.instDecidableEq b

def Digits.toNat (d : Digits) : Nat

Converts a non-empty string of digits to Nat.

Also here, shorter implementations exists like

def toNat (nes: NonEmptyString) : Nat := nes.val.toNat!

However, for direct use in proofs, this implementation appears as preferable.

Equations

• d.toNat = Digits.toNat.helper d.val.val.data 0

def Digits.toNat.helper : List Char → Nat → Nat

Equations

• Digits.toNat.helper [] x✝ = x✝
• Digits.toNat.helper (c :: cs) x✝ = Digits.toNat.helper cs (x✝ * 10 + c.toDigit!)

def Digits.lt (a b : Digits) : Prop

Less-then relation for digits, which is based on Nat (and not String) as defined in https://semver.org/ under 4.1:

Identifiers consisting of only digits are compared numerically.

This means that the canonical injection fun (a : Digits) => a.val is not a strictly increasing function as the following example shows:

def a : NonEmptyString := ⟨"23", rfl⟩
def b : NonEmptyString := ⟨"123", rfl⟩
#eval b < a -- true

def a' : Digits := ⟨a, rfl⟩
def b' : Digits := ⟨b, rfl⟩
#eval a' < b' -- true

Equations

• a.lt b = (a.toNat < b.toNat)

instance Digits.instLT : LT Digits

Equations

• Digits.instLT = { lt := Digits.lt }

def Digits.decLt (a b : Digits) : Decidable (a < b)

Decidable less-then for Digits.

Equations

• a.decLt b = if h : a.toNat < b.toNat then have g := ⋯; isTrue g else have g := ⋯; isFalse g

instance Digits.decidableLT (a b : Digits) : Decidable (a < b)

Equations

• a.decidableLT b = a.decLt b

def Digits.parse (str : String) : ParserResult Digits

Converts strings to Digits if possible - wrapped into a ParserResult.

Equations

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

def Digits.hasNoLeadingZeros (d : Digits) : Bool

Detects if a given term of type Digits has a leading zero.

https://semver.org/ forbids leading zeros for both, numbers in the version core and numeric identifiers.

Equations

• d.hasNoLeadingZeros = match d.val.val.data with | c :: head :: tail => c != '0' | x => true

def NumIdent : Type

Numeric identifiers are sequences of digits without leading zeros.

Examples: Strings "1234" and "0" are valid numeric identifiers while "01" is not.

This is used for the definition

  <numeric identifier> ::= "0"
                        | <positive digit>
                        | <positive digit> <digits>

(see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions).

Equations

• NumIdent = { d : Digits // d.hasNoLeadingZeros = true }

instance instReprNumIdent : Repr NumIdent

Equations

• instReprNumIdent = instReprSubtype

instance instBEqNumIdent : BEq NumIdent

Equations

• instBEqNumIdent = Subtype.instBEq

instance instToStringNumIdent : ToString NumIdent

Equations

• instToStringNumIdent = instToStringSubtype

instance instDecidableEqNumIdent : DecidableEq NumIdent

Equations

• instDecidableEqNumIdent a b = a.instDecidableEq b

def NumIdent.toNat (n : NumIdent) : Nat

Converts a numeric identifier to a natural number.

Equations

• n.toNat = n.val.toNat

def NumIdent.lt (a b : NumIdent) : Prop

Less-then for numerical identifiers, which is based on their value as natural number and not as strings.

Equations

• a.lt b = (a.toNat < b.toNat)

instance NumIdent.instLT : LT NumIdent

Equations

• NumIdent.instLT = { lt := NumIdent.lt }

def NumIdent.decLt (a b : NumIdent) : Decidable (a < b)

Decidable less-then for NumIdent.

Equations

• a.decLt b = a.val.decLt b.val

instance NumIdent.decidableLT (a b : NumIdent) : Decidable (a < b)

Equations

• a.decidableLT b = a.decLt b

def NumIdent.parse (str : String) : ParserResult NumIdent

Parses strings into NumIdent wrapped into a ParserResult if possible.

Equations

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

def Char.isAllowedForIdentifier (chr : Char) : Bool

Checks if a character is allowed for identifiers, i.e. it is either an letter (upper or lowercase), a digit (for base 10) or '-'.

This is used for the definition

  <identifier character> ::= <digit>
                          | <non-digit>
  <non-digit> ::= <letter>
              | "-"

  <digits> ::= <digit>
            | <digit> <digits>

  <digit> ::= "0"
            | <positive digit>

  <positive digit> ::= "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"

  <letter> ::= "A" | "B" | "C" | "D" | "E" | "F" | "G" | "H" | "I" | "J"
             | "K" | "L" | "M" | "N" | "O" | "P" | "Q" | "R" | "S" | "T"
             | "U" | "V" | "W" | "X" | "Y" | "Z" | "a" | "b" | "c" | "d"
             | "e" | "f" | "g" | "h" | "i" | "j" | "k" | "l" | "m" | "n"
             | "o" | "p" | "q" | "r" | "s" | "t" | "u" | "v" | "w" | "x"
             | "y" | "z"

(see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions).

Equations

• chr.isAllowedForIdentifier = (chr.isAlphanum || chr == '-')

def NonEmptyString.isAllowedAsIdentifier (s : NonEmptyString) : Bool

Checks if a NonEmptyString only contains characters that are allowed for identifiers.

Equations

• s.isAllowedAsIdentifier = NonEmptyString.isAllowedAsIdentifier.helper s.val.data

def NonEmptyString.isAllowedAsIdentifier.helper : List Char → Bool

Equations

• NonEmptyString.isAllowedAsIdentifier.helper (chr :: tail) = (chr.isAllowedForIdentifier && NonEmptyString.isAllowedAsIdentifier.helper tail)
• NonEmptyString.isAllowedAsIdentifier.helper [] = true

def Ident : Type

Defines the fundamental base type for the different kinds of identifiers.

Equations

• Ident = { s : NonEmptyString // s.isAllowedAsIdentifier = true }

instance instReprIdent : Repr Ident

Equations

• instReprIdent = instReprSubtype

instance instBEqIdent : BEq Ident

Equations

• instBEqIdent = Subtype.instBEq

instance instDecidableEqIdent : DecidableEq Ident

Equations

• instDecidableEqIdent a b = a.instDecidableEq b

instance instToStringIdent : ToString Ident

Equations

• instToStringIdent = instToStringSubtype

def Ident.lt (a b : Ident) : Prop

Equations

• a.lt b = (a.val < b.val)

instance Ident.instLT : LT Ident

Equations

• Ident.instLT = { lt := Ident.lt }

def Ident.decLt (a b : Ident) : Decidable (a < b)

Decidable less-then for Ident.

Equations

• a.decLt b = a.val.decLt b.val

instance Ident.decidableLT (a b : Ident) : Decidable (a < b)

Equations

• a.decidableLT b = a.decLt b

def Ident.parse (str : String) : ParserResult Ident

Parses the given string and if it is not empty and contains only allowed characters, returns an Ident wrapped in a ParserResult.

Equations

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

def Char.isAllowedAndNonDigit (chr : Char) : Bool

Returns true iff the character is allowed for identifiers but is not a digit, i.e. is in [A-Za-z\-].

This is used for

  <alphanumeric identifier> ::= <non-digit>
                              | <non-digit> <identifier characters>
                              | <identifier characters> <non-digit>
                              | <identifier characters> <non-digit> <identifier characters>

(see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions).

Equations

• chr.isAllowedAndNonDigit = (chr.isAlpha || decide (chr = '-'))

def Ident.hasNonDigit (i : Ident) : Bool

Returns true iff at least one character in the given identifier is not a digit.

Equations

• i.hasNonDigit = Ident.hasNonDigit.helper i.val.val.data

def Ident.hasNonDigit.helper : List Char → Bool

Equations

• Ident.hasNonDigit.helper (chr :: tail) = if chr.isAllowedAndNonDigit = true then true else Ident.hasNonDigit.helper tail
• Ident.hasNonDigit.helper [] = false

def AlphanumIdent : Type

Equations

• AlphanumIdent = { i : Ident // i.hasNonDigit = true }

instance instDecidableEqAlphanumIdent : DecidableEq AlphanumIdent

Equations

• instDecidableEqAlphanumIdent = Subtype.instDecidableEq

instance instReprAlphanumIdent : Repr AlphanumIdent

Equations

• instReprAlphanumIdent = instReprSubtype

instance instToStringAlphanumIdent : ToString AlphanumIdent

Equations

• instToStringAlphanumIdent = instToStringSubtype

instance instBEqAlphanumIdent : BEq AlphanumIdent

Equations

• instBEqAlphanumIdent = Subtype.instBEq

def AlphanumIdent.lt (a b : AlphanumIdent) : Prop

Equations

• a.lt b = (a.val < b.val)

instance AlphanumIdent.instLT : LT AlphanumIdent

Equations

• AlphanumIdent.instLT = { lt := AlphanumIdent.lt }

def AlphanumIdent.decLt (a b : AlphanumIdent) : Decidable (a < b)

Decidable less-then for AlphanumIdent.

Equations

• a.decLt b = a.val.decLt b.val

instance AlphanumIdent.decidableLT (a b : AlphanumIdent) : Decidable (a < b)

Equations

• a.decidableLT b = a.decLt b

def AlphanumIdent.parse (str : String) : ParserResult AlphanumIdent

Parses the given string and if it is a valid alphanumeric identifier, returns it wrapped in a ParserResult.

Equations

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

inductive BuildIdent : Type

Defines build-identifiers in accordance with

  <build identifier> ::= <alphanumeric identifier>
                      | <digits>

(see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions).

• alphanumIdent (val : AlphanumIdent) : BuildIdent
• digits (val : Digits) : BuildIdent

instance instDecidableEqBuildIdent : DecidableEq BuildIdent

Equations

• instDecidableEqBuildIdent = instDecidableEqBuildIdent.decEq

def instDecidableEqBuildIdent.decEq (x✝ x✝¹ : BuildIdent) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqBuildIdent.decEq (BuildIdent.alphanumIdent a) (BuildIdent.alphanumIdent b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqBuildIdent.decEq (BuildIdent.alphanumIdent val) (BuildIdent.digits val_1) = isFalse ⋯
• instDecidableEqBuildIdent.decEq (BuildIdent.digits val) (BuildIdent.alphanumIdent val_1) = isFalse ⋯
• instDecidableEqBuildIdent.decEq (BuildIdent.digits a) (BuildIdent.digits b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance instBEqBuildIdent : BEq BuildIdent

Equations

• instBEqBuildIdent = { beq := instBEqBuildIdent.beq }

def instBEqBuildIdent.beq : BuildIdent → BuildIdent → Bool

Equations

• instBEqBuildIdent.beq (BuildIdent.alphanumIdent a) (BuildIdent.alphanumIdent b) = (a == b)
• instBEqBuildIdent.beq (BuildIdent.digits a) (BuildIdent.digits b) = (a == b)
• instBEqBuildIdent.beq x✝¹ x✝ = false

def instReprBuildIdent.repr : BuildIdent → Nat → Std.Format

Equations

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

instance instReprBuildIdent : Repr BuildIdent

Equations

• instReprBuildIdent = { reprPrec := instReprBuildIdent.repr }

def BuildIdent.toString : BuildIdent → String

Returns the string representation of a build identifier.

Equations

• (BuildIdent.alphanumIdent a).toString = toString a
• (BuildIdent.digits a).toString = toString a

instance BuildIdent.instToString : ToString BuildIdent

Equations

• BuildIdent.instToString = { toString := BuildIdent.toString }

def BuildIdent.parse (str : String) : ParserResult BuildIdent

Parses the given string and if it is a valid build identifier, returns it wrapped in a ParserResult.

Equations

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

def DotSepBuildIdents : Type

Defines dot-separated build identifiers as non-empty lists of BuildIdents in accordance with

  <dot-separated build identifiers> ::= <build identifier>
                                    | <build identifier> "." <dot-separated build identifiers>

(see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions).

Equations

• DotSepBuildIdents = NonEmptyList BuildIdent

instance instDecidableEqDotSepBuildIdents : DecidableEq DotSepBuildIdents

Equations

• instDecidableEqDotSepBuildIdents a b = instDecidableEqNonEmptyList BuildIdent a b

instance instBEqDotSepBuildIdents : BEq DotSepBuildIdents

Equations

• instBEqDotSepBuildIdents = instBEqOfDecidableEq

instance instReprDotSepBuildIdents : Repr DotSepBuildIdents

Equations

• instReprDotSepBuildIdents = NonEmptyList.instRepr BuildIdent

instance instInhabitedDotSepBuildIdents : Inhabited DotSepBuildIdents

Defines a default value for DotSepBuildIdents so that to! can be used on ParserResult DotSepBuildIdents.

Equations

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

def DotSepBuildIdents.toString : DotSepBuildIdents → String

Returns the string representation of dot-separated build identifiers.

Equations

• DotSepBuildIdents.toString = NonEmptyList.toDotSeparatedString

instance DotSepBuildIdents.instToString : ToString DotSepBuildIdents

Equations

• DotSepBuildIdents.instToString = { toString := DotSepBuildIdents.toString }

def DotSepBuildIdents.parse (str : String) : ParserResult DotSepBuildIdents

Parses the given string and if it is a valid dot-separated build identifiers, retruns it wrapped in a ParserResult.

Equations

• DotSepBuildIdents.parse str = NonEmptyList.parse str BuildIdent.parse '.'

inductive PreRelIdent : Type

Defines pre-release identifiers in accordance with

  <pre-release identifier> ::= <alphanumeric identifier>
                            | <numeric identifier>

(see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions).

• alphanumIdent (val : AlphanumIdent) : PreRelIdent
• numIdent (val : NumIdent) : PreRelIdent

instance instDecidableEqPreRelIdent : DecidableEq PreRelIdent

Equations

• instDecidableEqPreRelIdent = instDecidableEqPreRelIdent.decEq

def instDecidableEqPreRelIdent.decEq (x✝ x✝¹ : PreRelIdent) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqPreRelIdent.decEq (PreRelIdent.alphanumIdent a) (PreRelIdent.alphanumIdent b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqPreRelIdent.decEq (PreRelIdent.alphanumIdent val) (PreRelIdent.numIdent val_1) = isFalse ⋯
• instDecidableEqPreRelIdent.decEq (PreRelIdent.numIdent val) (PreRelIdent.alphanumIdent val_1) = isFalse ⋯
• instDecidableEqPreRelIdent.decEq (PreRelIdent.numIdent a) (PreRelIdent.numIdent b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance instBEqPreRelIdent : BEq PreRelIdent

Equations

• instBEqPreRelIdent = { beq := instBEqPreRelIdent.beq }

def instBEqPreRelIdent.beq : PreRelIdent → PreRelIdent → Bool

Equations

• instBEqPreRelIdent.beq (PreRelIdent.alphanumIdent a) (PreRelIdent.alphanumIdent b) = (a == b)
• instBEqPreRelIdent.beq (PreRelIdent.numIdent a) (PreRelIdent.numIdent b) = (a == b)
• instBEqPreRelIdent.beq x✝¹ x✝ = false

instance instReprPreRelIdent : Repr PreRelIdent

Equations

• instReprPreRelIdent = { reprPrec := instReprPreRelIdent.repr }

def instReprPreRelIdent.repr : PreRelIdent → Nat → Std.Format

Equations

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

def PreRelIdent.lt (a b : PreRelIdent) : Prop

Less-then for pre-release identifiers. Numeric identifiers always have lower precedence than alphanumeric (non-numeric) identifiers (see https://semver.org/, section 11.4.3).

Equations

• (PreRelIdent.alphanumIdent val).lt (PreRelIdent.numIdent val_1) = False
• (PreRelIdent.numIdent val).lt (PreRelIdent.alphanumIdent val_1) = True
• (PreRelIdent.alphanumIdent s).lt (PreRelIdent.alphanumIdent t) = (s < t)
• (PreRelIdent.numIdent s).lt (PreRelIdent.numIdent t) = (s < t)

instance PreRelIdent.instLT : LT PreRelIdent

Equations

• PreRelIdent.instLT = { lt := PreRelIdent.lt }

def PreRelIdent.decLt (a b : PreRelIdent) : Decidable (a < b)

Decidable less-then for PreRelIdent.

Equations

• (PreRelIdent.alphanumIdent s).decLt (PreRelIdent.alphanumIdent t) = if h : s < t then isTrue h else isFalse h
• (PreRelIdent.numIdent s).decLt (PreRelIdent.numIdent t) = if h : s < t then isTrue h else isFalse h
• (PreRelIdent.alphanumIdent val).decLt (PreRelIdent.numIdent val_1) = isFalse ⋯
• (PreRelIdent.numIdent val).decLt (PreRelIdent.alphanumIdent val_1) = isTrue ⋯

instance PreRelIdent.instDecidableLT : DecidableLT PreRelIdent

Equations

• PreRelIdent.instDecidableLT = PreRelIdent.decLt

def PreRelIdent.toString : PreRelIdent → String

Returns the string representation of a pre-release identifier.

Equations

• (PreRelIdent.alphanumIdent a).toString = toString a
• (PreRelIdent.numIdent a).toString = toString a

instance PreRelIdent.instToString : ToString PreRelIdent

Equations

• PreRelIdent.instToString = { toString := PreRelIdent.toString }

def PreRelIdent.parse (str : String) : ParserResult PreRelIdent

Parses the given string and if it is a valid pre-release identifier, returns it wrapped in a ParserResult.

Equations

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

def DotSepPreRelIdents : Type

Defines dot-separated pre-release identifiers in accordance with

  <dot-separated pre-release identifiers> ::= <pre-release identifier>
                                        | <pre-release identifier> "." <dot-separated pre-release identifiers>

(see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions).

Equations

• DotSepPreRelIdents = NonEmptyList PreRelIdent

instance instReprDotSepPreRelIdents : Repr DotSepPreRelIdents

Equations

• instReprDotSepPreRelIdents = NonEmptyList.instRepr PreRelIdent

instance instDecidableEqDotSepPreRelIdents : DecidableEq DotSepPreRelIdents

Equations

• instDecidableEqDotSepPreRelIdents a b = instDecidableEqNonEmptyList PreRelIdent a b

instance instBEqDotSepPreRelIdents : BEq DotSepPreRelIdents

Equations

• instBEqDotSepPreRelIdents = instBEqOfDecidableEq

instance instInhabitedDotSepPreRelIdents : Inhabited DotSepPreRelIdents

Equations

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

def DotSepPreRelIdents.repr (a : DotSepPreRelIdents) (n : Nat) : Std.Format

Provides a representation for dot-separated pre-release identifiers so that #eval can be used.

Equations

• a.repr n = a.val.repr n

instance DotSepPreRelIdents.instRepr : Repr DotSepPreRelIdents

Equations

• DotSepPreRelIdents.instRepr = { reprPrec := DotSepPreRelIdents.repr }

def DotSepPreRelIdents.lt (a b : DotSepPreRelIdents) : Prop

Equations

• a.lt b = NonEmptyList.lt a b

instance DotSepPreRelIdents.instLT : LT DotSepPreRelIdents

Equations

• DotSepPreRelIdents.instLT = { lt := DotSepPreRelIdents.lt }

def DotSepPreRelIdents.decLt (a b : DotSepPreRelIdents) : Decidable (a < b)

Decidable less-then for DotSepPreRelIdents.

Equations

• a.decLt b = NonEmptyList.decLt a b

instance DotSepPreRelIdents.instDecidableLT : DecidableLT DotSepPreRelIdents

Equations

• DotSepPreRelIdents.instDecidableLT = DotSepPreRelIdents.decLt

def DotSepPreRelIdents.toString : DotSepPreRelIdents → String

Equations

• DotSepPreRelIdents.toString = NonEmptyList.toDotSeparatedString

instance DotSepPreRelIdents.instToString : ToString DotSepPreRelIdents

Equations

• DotSepPreRelIdents.instToString = { toString := DotSepPreRelIdents.toString }

def DotSepPreRelIdents.parse (str : String) : ParserResult DotSepPreRelIdents

Parses the given string and if it is a valid dot-separated pre-release identifiers, returns it wrapped in a ParserResult.

Equations

• DotSepPreRelIdents.parse str = NonEmptyList.parse str PreRelIdent.parse '.'

structure VersionCore : Type

Defines the version core in accordance with

  <version core> ::= <major> "." <minor> "." <patch>
  <major> ::= <numeric identifier>
  <minor> ::= <numeric identifier>
  <patch> ::= <numeric identifier>

(see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions).

Version cores default to 1.0.0.

• major : Nat
• minor : Nat
• patch : Nat

instance instDecidableEqVersionCore : DecidableEq VersionCore

Equations

• instDecidableEqVersionCore = instDecidableEqVersionCore.decEq

def instDecidableEqVersionCore.decEq (x✝ x✝¹ : VersionCore) : Decidable (x✝ = x✝¹)

Equations

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

def instBEqVersionCore.beq : VersionCore → VersionCore → Bool

Equations

• instBEqVersionCore.beq { major := a, minor := a_1, patch := a_2 } { major := b, minor := b_1, patch := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• instBEqVersionCore.beq x✝¹ x✝ = false

instance instBEqVersionCore : BEq VersionCore

Equations

• instBEqVersionCore = { beq := instBEqVersionCore.beq }

instance instReprVersionCore : Repr VersionCore

Equations

• instReprVersionCore = { reprPrec := instReprVersionCore.repr }

def instReprVersionCore.repr : VersionCore → Nat → Std.Format

Equations

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

def instInhabitedVersionCore.default : VersionCore

Equations

• instInhabitedVersionCore.default = { major := default, minor := default, patch := default }

instance instInhabitedVersionCore : Inhabited VersionCore

Equations

• instInhabitedVersionCore = { default := instInhabitedVersionCore.default }

def VersionCore.toString (a : VersionCore) : String

Returns the string representation of a version core.

Equations

• a.toString = toString a.major ++ toString "." ++ toString a.minor ++ toString "." ++ toString a.patch

instance VersionCore.instToString : ToString VersionCore

Equations

• VersionCore.instToString = { toString := VersionCore.toString }

def VersionCore.toList (v : VersionCore) : List Nat

Returns the version core as list of three natural numbers.

Equations

• v.toList = [v.major, v.minor, v.patch]

def VersionCore.fromList (l : List Nat) (h : (l.length == 3) = true) : VersionCore

Constructs a version core from a list of three natural numbers.

Equations

• VersionCore.fromList [m, n, p] h_2 = { major := m, minor := n, patch := p }

def VersionCore.lt (v w : VersionCore) : Prop

Less-then for version cores.

Equations

• v.lt w = (v.toList < w.toList)

instance VersionCore.instLT : LT VersionCore

Equations

• VersionCore.instLT = { lt := VersionCore.lt }

def VersionCore.decLt (v w : VersionCore) : Decidable (v < w)

Decides if < holds true for two version cores.

Equations

• v.decLt w = v.toList.decidableLT w.toList

instance VersionCore.instDecidableLT : DecidableLT VersionCore

Equations

• VersionCore.instDecidableLT = VersionCore.decLt

def VersionCore.parse (str : String) : ParserResult VersionCore

Parses the given string and if it is a valid version core, returns it wrapped in a ParserResult.

Equations

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

structure Versionextends VersionCore : Type

Defines a full semantic version in accordance with

  <version> ::= <version core>
              | <version core> "-" <pre-release>
              | <version core> "+" <build>
              | <version core> "-" <pre-release> "+" <build>
  <pre-release> ::= <dot-separated pre-release identifiers>
  <build> ::= <dot-separated build identifiers>

(see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions).

• major : Nat
• minor : Nat
• patch : Nat
• preRelease : Option DotSepPreRelIdents
• build : Option DotSepBuildIdents

def instDecidableEqVersion.decEq (x✝ x✝¹ : Version) : Decidable (x✝ = x✝¹)

Equations

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

instance instDecidableEqVersion : DecidableEq Version

Equations

• instDecidableEqVersion = instDecidableEqVersion.decEq

instance instBEqVersion : BEq Version

Equations

• instBEqVersion = { beq := instBEqVersion.beq }

def instBEqVersion.beq : Version → Version → Bool

Equations

• instBEqVersion.beq { toVersionCore := a, preRelease := a_1, build := a_2 } { toVersionCore := b, preRelease := b_1, build := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• instBEqVersion.beq x✝¹ x✝ = false

def instReprVersion.repr : Version → Nat → Std.Format

Equations

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

instance instReprVersion : Repr Version

Equations

• instReprVersion = { reprPrec := instReprVersion.repr }

def instInhabitedVersion.default : Version

Equations

• instInhabitedVersion.default = { toVersionCore := default, preRelease := default, build := default }

instance instInhabitedVersion : Inhabited Version

Equations

• instInhabitedVersion = { default := instInhabitedVersion.default }

def Version.toString (a : Version) : String

Returns the string representation of a version.

Equations

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

instance Version.instToString : ToString Version

Equations

• Version.instToString = { toString := Version.toString }

def Version.ltPreRelease (a b : Version) : Bool

Helper function for comparing the parts of versions outside the version core.

Equations

• a.ltPreRelease b = match a.preRelease, b.preRelease with | some val, none => true | some s, some t => decide (s < t) | none, none => false | none, some val => false

def Version.lt (v w : Version) : Prop

Less-then for versions in accordance with section 11 of the SemVer specification.

Equations

• v.lt w = (v.toVersionCore < w.toVersionCore ∨ v.toVersionCore = w.toVersionCore ∧ v.ltPreRelease w = true)

instance Version.instLT : LT Version

Equations

• Version.instLT = { lt := Version.lt }

def Version.decLt (v w : Version) : Decidable (v < w)

Decides if < holds true for two versions.

Equations

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

instance Version.instDecidableLT : DecidableLT Version

Equations

• Version.instDecidableLT = Version.decLt

def Version.parseCorePreRel (str : String) : ParserResult (VersionCore × Option DotSepPreRelIdents)

Helper function that parses the version core and optional pre-release part of a version string.

Equations

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

def Version.parse (str : String) : ParserResult Version

Parses the given string and if it is a valid version, returns it wrapped in a ParserResult.

Equations

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

def Version.isStable (v : Version) : Bool

Returns true if public API provided under this version is stable.

Equations

• { major := 0, minor := minor, patch := patch, preRelease := preRelease, build := build }.isStable = false
• { major := major, minor := minor, patch := patch, preRelease := some val, build := build }.isStable = false
• v.isStable = true

def Version.nextMajor (v : Version) : Version

Returns a version that is the next major version based on the provided version. The returned version has no pre-release or build metadata.

Equations

• v.nextMajor = { major := v.major + 1 }

def Version.nextMinor (v : Version) : Version

Returns a version that is the next minor version based on the provided version. The returned version has no pre-release or build metadata.

Equations

• v.nextMinor = { major := v.major, minor := v.minor + 1 }

def Version.nextPatch (v : Version) : Version

Returns a version that is the next patch version based on the provided version. The returned version has no pre-release or build metadata.

Equations

• v.nextPatch = { major := v.major, minor := v.minor, patch := v.patch + 1 }

def Version.subsequentPreRelease? (v : Version) (str : String) : Option Version

Returns a version that is the subsequent pre-release version based on the provided version and pre-release string.

If the resulting version is not greater than the provided version, or if the pre-release string is invalid, none is returned.

Equations

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

def Version.setPreRelease? (v : Version) (str : String) : Option Version

Returns a version that is the same as the provided version but with the pre-release part set to the provided string.

If the resulting version is not greater than the provided version, or if the pre-release string is invalid, none is returned.

Equations

• { toVersionCore := c, preRelease := preRelease, build := build }.setPreRelease? str = (Version.parse (toString c ++ toString "-" ++ toString str)).to?

def Version.setBuild? (v : Version) (str : String) : Option Version

Returns a version that is the same as the provided version but with the build part set to the provided string.

If the given string is not valid as build metadata, none is returned.

Equations

• { toVersionCore := c, build := build }.setBuild? str = (Version.parse (toString c ++ toString "+" ++ toString str)).to?
• { toVersionCore := c, preRelease := some p, build := build }.setBuild? str = (Version.parse (toString c ++ toString "-" ++ toString p ++ toString "+" ++ toString str)).to?

def Version.isPossibleStart (previous : Option Char) (current : Char) : Bool

Helper function that checks if a character can be the start of a version in a string, given the previous character (if any).

Equations

• Version.isPossibleStart none current = current.isDigit
• Version.isPossibleStart (some c) current = (!c.isDigit && current.isDigit)

def Char.isValidForVersion (c : Char) : Bool

Helper function that checks if a character is valid in a version string.

Equations

• c.isValidForVersion = (c.isAllowedForIdentifier || c == '.' || c == '+')

def VersionCore.addPreRelease? (c : VersionCore) (suffix : String) : Option Version

Equations

• c.addPreRelease? suffix = (Version.parse (toString c ++ toString "-" ++ toString suffix)).to?

def cutOffPrefix (ch : Option Char) (str : String) : String

Helper that cuts off the prefix of a string that cannot be part of a version.

Equations

• cutOffPrefix ch str = { data := cutOffPrefix.helper ch str.data }

def cutOffPrefix.helper : Option Char → List Char → List Char

Equations

• cutOffPrefix.helper x✝ [] = []
• cutOffPrefix.helper x✝ (d :: t) = if Version.isPossibleStart x✝ d = true then d :: t else cutOffPrefix.helper (some d) t

def extractVersions (str : String) : List Version

Extracts all versions that are contained in a given string.

Equations

• extractVersions str = extractVersions.helper (str.split (not ∘ Char.isValidForVersion))

def extractVersions.helper : List String → List Version

Equations

• One or more equations did not get rendered due to their size.
• extractVersions.helper [] = []