SemVer.Basic - Types for Version Numbers

Semantic Versioning defines a grammar for versions and precedence rules for two version.

Basic.lean provides the types for the the left-hand side of a grammar rules in Backus–Naur Form Grammar for Valid SemVer Versions.

@[implicit_reducible]

instance String.Slice.instRepr_semVer : Repr Slice

String.Slice has no Repr but uses ToString instead. However, the default implementation does not provide the surrounding quotes (") and that's an own instance is provided that overrides the default.

Before defining an instance for Repr String.Slice:

#synth (Repr String.Slice) -- failed to synthesize Repr Slice
#synth (ToString String.Slice) -- instToString
#eval "abc" -- "abc"
#eval "abc".toSlice -- abc without surrounding quotes

After defining the own instance:

#synth (Repr String.Slice) -- instRepr_semVer
#eval "abc".toSlice -- "abc" with surrounding quotes

Equations

• String.Slice.instRepr_semVer = { reprPrec := fun (s : String.Slice) (x : Nat) => Std.Format.text s.toString.quote }

def String.Slice.getPrefixn (s : Slice) (n : Nat) : Slice

Returns the n preceding characters of s in underlying string as String.Slice. If there are less then n characters before s, all characters preceding s are returned.

def s : String.Slice := "red green blue".slice ⟨⟨4⟩, by decide⟩ ⟨⟨9⟩, by decide⟩ (by decide)

#eval s -- "green"
#eval s.getPrefixn 2 -- "d "
#eval s.getPrefixn 10 -- "red "

Equations

• s.getPrefixn n = s.str.slice (s.startInclusive.prevn n) s.startInclusive ⋯

def String.Slice.getPrefix (s : Slice) : Slice

Returns the full prefix of s (i.e. all characters before s) in the underlying string as String.Slice.

Equations

• s.getPrefix = s.str.slice s.str.startPos s.startInclusive ⋯

def String.Slice.getSuffixn (s : Slice) (n : Nat) : Slice

Returns the n succeeding characters of s in underlying string as String.Slice. If there are less then n characters after s, all characters following s are returned.

def s : String.Slice := "red green blue".slice ⟨⟨4⟩, by decide⟩ ⟨⟨9⟩, by decide⟩ (by decide)

#eval s -- "green"
#eval s.getSuffixn 2 -- " b"
#eval s.getSuffixn 10 -- " blue"

Equations

• s.getSuffixn n = s.str.slice s.endExclusive (s.endExclusive.nextn n) ⋯

def String.Slice.getSuffix (s : Slice) : Slice

Returns the full suffix of s (i.e. all characters after s) within the underlying string as String.Slice.

Equations

• s.getSuffix = s.str.slice s.endExclusive s.str.endPos ⋯

structure ParserError : Type

If parsing fails, a ParserError is returned. In that, message gives an explanation of the error and input optionally provides the section of the input string that could not be parsed and thus caused the error.

• message : String
• input : Option String.Slice

@[implicit_reducible]

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.

@[implicit_reducible]

instance instBEqParserError : BEq ParserError

Equations

• instBEqParserError = { beq := instBEqParserError.beq }

def instBEqParserError.beq : ParserError → ParserError → Bool

Equations

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

def ParserError.toString (e : ParserError) : String

Returns a formatted string that contains the error message some context if some slice is provided.

Equations

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

@[implicit_reducible]

instance ParserError.instToString : ToString ParserError

Equations

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

@[implicit_reducible]

instance ParserError.instInhabited : Inhabited ParserError

Defines a default with "unknown error" as message and no input.

Equations

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

inductive ParserResult (α : Type) : Type

Parsers return a ParserResult. If parsing was successful, some value of type α is included, which has by retrieved from the input. If the input was incorrect, ParserResult is wrapper of a ParserError.

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

@[implicit_reducible]

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.

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

@[implicit_reducible]

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

Equations

• instBEqParserResult = { beq := instBEqParserResult.beq }

@[implicit_reducible]

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

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

Equations

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

def ParserResult.toString {α : Type} [ToString α] (res : ParserResult α) : String

Equations

• (ParserResult.success a).toString = toString a
• (ParserResult.failure a).toString = toString a

@[implicit_reducible]

instance ParserResult.instToString {α : Type} [ToString α] : ToString (ParserResult α)

Equations

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

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

Returns true iff the ParserResult results from a successful parser call.

Equations

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

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

Converts a parser result of type ParserResult α into a value if type Option α that is none in case of failure and some result if parsing was successful.

Equations

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

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

Unwraps the value from a .successful parser result and panics if a ParserResult with 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 successful parser result into an term of IO α and throws an error, if a ParserResult with .failure is provided.

Equations

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

class Parser (α : Type) : Type

A Parser provides function parse that takes a String.Slice as input and returns a ParserResult.

• parse (s : String.Slice) : ParserResult α

class SplitMapParser (α : Type) [Parser α] (β : Type → Type) : Type

A SplitMapParser implements parse by splitting the provided String.Slice based on separator sep and mapping Parser α to each sub-slice.

• parse (s : String.Slice) (sep : Char) : ParserResult (β α)

def NonEmptyList (α : Type) : Type

Defines non-empty lists as subtype of List.

Equations

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

@[implicit_reducible]

instance NonEmptyList.instDecidableEq (α : Type) [DecidableEq α] : DecidableEq (NonEmptyList α)

Equations

• NonEmptyList.instDecidableEq α = Subtype.instDecidableEq

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

@[implicit_reducible]

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

Equations

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

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

Less-than-relation for non-empty lists, which is List.lt applied to the two lists (lexicographic ordering of lists with respect to an ordering on their elements).

Equations

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

@[implicit_reducible]

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-than for NonEmptyList.

Equations

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

@[implicit_reducible]

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

Equations

• NonEmptyList.instDecidableLTOfDecidableEq α = NonEmptyList.decLt

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) [Parser α] (s : String.Slice) (sep : Char) : ParserResult (NonEmptyList α)

Parses the given string slice 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.mapParser {α : Type} [Parser α] (slices : List String.Slice) : ParserResult (List α)

Equations

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

@[implicit_reducible]

instance NonEmptyList.instSplitMapParser {α : Type} [Parser α] : SplitMapParser α NonEmptyList

Equations

• NonEmptyList.instSplitMapParser = { parse := NonEmptyList.parse α }

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 }

@[implicit_reducible]

instance instReprNonEmptyString : Repr NonEmptyString

Equations

• instReprNonEmptyString = { reprPrec := instReprNonEmptyString._aux_1 }

@[implicit_reducible]

instance instDecidableEqNonEmptyString : DecidableEq NonEmptyString

Equations

• instDecidableEqNonEmptyString = instDecidableEqNonEmptyString._aux_1

@[implicit_reducible]

instance instToStringNonEmptyString : ToString NonEmptyString

Equations

• instToStringNonEmptyString = { toString := instToStringNonEmptyString._aux_1 }

@[implicit_reducible]

instance instBEqNonEmptyString : BEq NonEmptyString

Equations

• instBEqNonEmptyString = { beq := instBEqNonEmptyString._aux_1 }

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

Less-than-relation for non-empty strings.

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

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

Equations

• a.decidableLT b = a.decLt b

def NonEmptyString.parse (s : String.Slice) : ParserResult NonEmptyString

Parses a given string slice and returns a result containing a non-empty string if possible and a result that wraps a ParserError otherwise.

Equations

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

@[implicit_reducible]

instance NonEmptyString.instParser : Parser NonEmptyString

Equations

• NonEmptyString.instParser = { parse := NonEmptyString.parse }

def Char.toDigit? : Char → Option Nat

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

This implementation is seemingly better suited for proofs compared to 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 not digits (for base ten).

Equations

• c.toDigit! = match c.toDigit? with | some n => n | none => panicWithPosWithDecl "SemVer.Basic" "Char.toDigit!" 404 13 (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 = nes.val.toList.all Char.isDigit'

def Digits : Type

Defines a subtype of NonEmptyString with the restriction that all characters must be digits (for 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 }

@[implicit_reducible]

instance instReprDigits : Repr Digits

Equations

• instReprDigits = { reprPrec := instReprDigits._aux_1 }

@[implicit_reducible]

instance instToStringDigits : ToString Digits

Equations

• instToStringDigits = { toString := instToStringDigits._aux_1 }

@[implicit_reducible]

instance instBEqDigits : BEq Digits

Equations

• instBEqDigits = { beq := instBEqDigits._aux_1 }

@[implicit_reducible]

instance instDecidableEqDigits : DecidableEq Digits

Equations

• instDecidableEqDigits = instDecidableEqDigits._aux_1

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 = String.foldl (fun (acc : Nat) (c : Char) => acc * 10 + c.toDigit!) 0 d.val.val

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

Less-than-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)

@[implicit_reducible]

instance Digits.instLT : LT Digits

Equations

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

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

Decidable less-than for Digits.

Equations

• a.decLt b = if h : a.toNat < b.toNat then isTrue h else isFalse h

@[implicit_reducible]

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

Equations

• a.decidableLT b = a.decLt b

def Digits.parse (s : String.Slice) : ParserResult Digits

Converts a string slice into Digits if possible - wrapped into a ParserResult.

Equations

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

@[implicit_reducible]

instance Digits.instParser : Parser Digits

Equations

• Digits.instParser = { parse := Digits.parse }

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.toList 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 }

@[implicit_reducible]

instance instBEqNumIdent : BEq NumIdent

Equations

• instBEqNumIdent = { beq := instBEqNumIdent._aux_1 }

@[implicit_reducible]

instance instDecidableEqNumIdent : DecidableEq NumIdent

Equations

• instDecidableEqNumIdent = instDecidableEqNumIdent._aux_1

@[implicit_reducible]

instance instReprNumIdent : Repr NumIdent

Equations

• instReprNumIdent = { reprPrec := instReprNumIdent._aux_1 }

@[implicit_reducible]

instance instToStringNumIdent : ToString NumIdent

Equations

• instToStringNumIdent = { toString := instToStringNumIdent._aux_1 }

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-than-relation for numerical identifiers, which is based on their value as natural number and not as strings.

Equations

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

@[implicit_reducible]

instance NumIdent.instLT : LT NumIdent

Equations

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

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

Decidable less-than for NumIdent.

Equations

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

@[implicit_reducible]

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

Equations

• a.decidableLT b = a.decLt b

def NumIdent.parse (s : String.Slice) : ParserResult NumIdent

Parses string slices into NumIdent wrapped into a ParserResult if possible.

Equations

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

@[implicit_reducible]

instance NumIdent.instParser : Parser NumIdent

Equations

• NumIdent.instParser = { parse := NumIdent.parse }

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.

The shorter implementation

def NonEmptyString.isAllowedAsIdentifier (s: NonEmptyString) : Bool :=
  s.val.all Char.isAllowedForIdentifier

does not work for statements like

example : NonEmptyString.isAllowedAsIdentifier ⟨"12ab", by decide⟩ == true := by decide

with by decide as proof but requires seemingly a more sophisticated proof.

Equations

• s.isAllowedAsIdentifier = NonEmptyString.isAllowedAsIdentifier.checkCharacters s.val.toList

def NonEmptyString.isAllowedAsIdentifier.checkCharacters : List Char → Bool

Equations

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

def Ident : Type

Defines the base type for the different kinds of identifiers.

Equations

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

@[implicit_reducible]

instance instDecidableEqIdent : DecidableEq Ident

Equations

• instDecidableEqIdent = instDecidableEqIdent._aux_1

@[implicit_reducible]

instance instToStringIdent : ToString Ident

Equations

• instToStringIdent = { toString := instToStringIdent._aux_1 }

@[implicit_reducible]

instance instBEqIdent : BEq Ident

Equations

• instBEqIdent = { beq := instBEqIdent._aux_1 }

@[implicit_reducible]

instance instReprIdent : Repr Ident

Equations

• instReprIdent = { reprPrec := instReprIdent._aux_1 }

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

Defines the less-than-relation for Ident.

Equations

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

@[implicit_reducible]

instance Ident.instLT : LT Ident

Equations

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

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

Decidable less-than for Ident.

Equations

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

@[implicit_reducible]

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

Equations

• a.decidableLT b = a.decLt b

def Ident.parse (s : String.Slice) : ParserResult Ident

Parses the given string slice 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.

@[implicit_reducible]

instance Ident.instParser : Parser Ident

Equations

• Ident.instParser = { parse := Ident.parse }

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.

Again, there are shorter implementation such as

def Ident.hasNonDigit (i: Ident) : Bool :=
  i.val.val.any Char.isAllowedAndNonDigit

but they less convenient in proofs.

Equations

• i.hasNonDigit = Ident.hasNonDigit.checkCharacters i.val.val.toList

def Ident.hasNonDigit.checkCharacters : List Char → Bool

Equations

• Ident.hasNonDigit.checkCharacters (chr :: tail) = (chr.isAllowedAndNonDigit || Ident.hasNonDigit.checkCharacters tail)
• Ident.hasNonDigit.checkCharacters [] = false

def AlphanumIdent : Type

AlphanumIdent is the type for alphanumeric identifiers.

Equations

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

@[implicit_reducible]

instance instDecidableEqAlphanumIdent : DecidableEq AlphanumIdent

Equations

• instDecidableEqAlphanumIdent = Subtype.instDecidableEq

@[implicit_reducible]

instance instBEqAlphanumIdent : BEq AlphanumIdent

Equations

• instBEqAlphanumIdent = { beq := instBEqAlphanumIdent._aux_1 }

@[implicit_reducible]

instance instToStringAlphanumIdent : ToString AlphanumIdent

Equations

• instToStringAlphanumIdent = { toString := instToStringAlphanumIdent._aux_1 }

@[implicit_reducible]

instance instReprAlphanumIdent : Repr AlphanumIdent

Equations

• instReprAlphanumIdent = { reprPrec := instReprAlphanumIdent._aux_1 }

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

Defines the less-than-relation for AlphanumIdent.

Equations

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

@[implicit_reducible]

instance AlphanumIdent.instLT : LT AlphanumIdent

Equations

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

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

Decidable less-than for AlphanumIdent.

Equations

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

@[implicit_reducible]

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

Equations

• a.decidableLT b = a.decLt b

def AlphanumIdent.parse (s : String.Slice) : ParserResult AlphanumIdent

Parses the given string slice 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

@[implicit_reducible]

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 ⋯

@[implicit_reducible]

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.

@[implicit_reducible]

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

@[implicit_reducible]

instance BuildIdent.instToString : ToString BuildIdent

Equations

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

def BuildIdent.parse (s : String.Slice) : ParserResult BuildIdent

Parses the given string slice 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.

@[implicit_reducible]

instance BuildIdent.instParser : Parser BuildIdent

Equations

• BuildIdent.instParser = { parse := BuildIdent.parse }

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

@[implicit_reducible]

instance instReprDotSepBuildIdents : Repr DotSepBuildIdents

Equations

• instReprDotSepBuildIdents = { reprPrec := instReprDotSepBuildIdents._aux_1 }

@[implicit_reducible]

instance instDecidableEqDotSepBuildIdents : DecidableEq DotSepBuildIdents

Equations

• instDecidableEqDotSepBuildIdents = instDecidableEqDotSepBuildIdents._aux_1

@[implicit_reducible]

instance instBEqDotSepBuildIdents : BEq DotSepBuildIdents

Equations

• instBEqDotSepBuildIdents = { beq := instBEqDotSepBuildIdents._aux_1 }

@[implicit_reducible]

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 a string representation of dot-separated build identifiers.

Equations

• DotSepBuildIdents.toString = NonEmptyList.toDotSeparatedString

@[implicit_reducible]

instance DotSepBuildIdents.instToString : ToString DotSepBuildIdents

Equations

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

def DotSepBuildIdents.parse (s : String.Slice) : ParserResult DotSepBuildIdents

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

Equations

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

@[implicit_reducible]

instance DotSepBuildIdents.instParser : Parser DotSepBuildIdents

Equations

• DotSepBuildIdents.instParser = { parse := DotSepBuildIdents.parse }

inductive PreRelIdent : Type

Defines the type for 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

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 ⋯

@[implicit_reducible]

instance instDecidableEqPreRelIdent : DecidableEq PreRelIdent

Equations

• instDecidableEqPreRelIdent = instDecidableEqPreRelIdent.decEq

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

@[implicit_reducible]

instance instBEqPreRelIdent : BEq PreRelIdent

Equations

• instBEqPreRelIdent = { beq := instBEqPreRelIdent.beq }

@[implicit_reducible]

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-than-relation 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)

@[implicit_reducible]

instance PreRelIdent.instLT : LT PreRelIdent

Equations

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

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

Decidable less-than 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 ⋯

@[implicit_reducible]

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

@[implicit_reducible]

instance PreRelIdent.instToString : ToString PreRelIdent

Equations

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

def PreRelIdent.parse (s : String.Slice) : ParserResult PreRelIdent

Parses the given string slice 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.

@[implicit_reducible]

instance PreRelIdent.instParser : Parser PreRelIdent

Equations

• PreRelIdent.instParser = { parse := PreRelIdent.parse }

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

@[implicit_reducible]

instance instDecidableEqDotSepPreRelIdents : DecidableEq DotSepPreRelIdents

Equations

• instDecidableEqDotSepPreRelIdents = instDecidableEqDotSepPreRelIdents._aux_1

@[implicit_reducible]

instance instBEqDotSepPreRelIdents : BEq DotSepPreRelIdents

Equations

• instBEqDotSepPreRelIdents = { beq := instBEqDotSepPreRelIdents._aux_1 }

@[implicit_reducible]

instance instReprDotSepPreRelIdents : Repr DotSepPreRelIdents

Equations

• instReprDotSepPreRelIdents = { reprPrec := instReprDotSepPreRelIdents._aux_1 }

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance DotSepPreRelIdents.instLT : LT DotSepPreRelIdents

Equations

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

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

Decidable less-than-relation for DotSepPreRelIdents.

Equations

• a.decLt b = NonEmptyList.decLt a b

@[implicit_reducible]

instance DotSepPreRelIdents.instDecidableLT : DecidableLT DotSepPreRelIdents

Equations

• DotSepPreRelIdents.instDecidableLT = DotSepPreRelIdents.decLt

def DotSepPreRelIdents.toString : DotSepPreRelIdents → String

Equations

• DotSepPreRelIdents.toString = NonEmptyList.toDotSeparatedString

@[implicit_reducible]

instance DotSepPreRelIdents.instToString : ToString DotSepPreRelIdents

Equations

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

def DotSepPreRelIdents.parse (s : String.Slice) : ParserResult DotSepPreRelIdents

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

Equations

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

@[implicit_reducible]

instance DotSepPreRelIdents.instParser : Parser DotSepPreRelIdents

Equations

• DotSepPreRelIdents.instParser = { parse := DotSepPreRelIdents.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

@[implicit_reducible]

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

@[implicit_reducible]

instance instBEqVersionCore : BEq VersionCore

Equations

• instBEqVersionCore = { beq := instBEqVersionCore.beq }

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

Equations

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

@[implicit_reducible]

instance instReprVersionCore : Repr VersionCore

Equations

• instReprVersionCore = { reprPrec := instReprVersionCore.repr }

@[implicit_reducible]

instance instInhabitedVersionCore : Inhabited VersionCore

Equations

• instInhabitedVersionCore = { default := instInhabitedVersionCore.default }

def instInhabitedVersionCore.default : VersionCore

Equations

• instInhabitedVersionCore.default = { major := default, minor := default, patch := 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

@[implicit_reducible]

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-than-relation for version cores.

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance VersionCore.instDecidableLT : DecidableLT VersionCore

Equations

• VersionCore.instDecidableLT = VersionCore.decLt

def VersionCore.parse (s : String.Slice) : 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.

@[implicit_reducible]

instance VersionCore.instParser : Parser VersionCore

Equations

• VersionCore.instParser = { parse := VersionCore.parse }

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

@[implicit_reducible]

instance instDecidableEqVersion : DecidableEq Version

Equations

• instDecidableEqVersion = instDecidableEqVersion.decEq

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

Equations

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

@[implicit_reducible]

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.

@[implicit_reducible]

instance instReprVersion : Repr Version

Equations

• instReprVersion = { reprPrec := instReprVersion.repr }

@[implicit_reducible]

instance instInhabitedVersion : Inhabited Version

Equations

• instInhabitedVersion = { default := instInhabitedVersion.default }

def instInhabitedVersion.default : Version

Equations

• instInhabitedVersion.default = { toVersionCore := default, preRelease := default, build := 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.

@[implicit_reducible]

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-than-relation 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)

@[implicit_reducible]

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.

@[implicit_reducible]

instance Version.instDecidableLT : DecidableLT Version

Equations

• Version.instDecidableLT = Version.decLt

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

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

Equations

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

def Version.parse (s : String.Slice) : ParserResult Version

Parses the given string slice 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.

@[implicit_reducible]

instance Version.instParser : Parser Version

Equations

• Version.instParser = { parse := Version.parse }

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).toSlice).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).toSlice).to?
• { toVersionCore := c, preRelease := some p, build := build }.setBuild? str = (Version.parse (toString c ++ toString "-" ++ toString p ++ toString "+" ++ toString str).toSlice).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).toSlice).to?

def cutOffPrefix (s : String.Slice) : String.Slice

Equations

• cutOffPrefix s = s.dropWhile fun (c : Char) => !c.isDigit'

def extractVersions (str : String) : List Version

Extracts all versions that are contained in a given string.

Equations

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

def extractVersions.mapParser : List String.Slice → List Version

Equations

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