/- Copyright (c) 2025 Stefan Kusterer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. This file refers to version 2.0.0 of Semantic Versioning (https://semver.org) which is published under Creative Commons ― CC BY 3.0 license. -/ section ParserErrors /-- Contains an error message and the position at which the interpretation of the input string was not possible anymore. -/ structure ParserError where message : String position : Nat input: Option String := none deriving Repr, BEq namespace ParserError /-- Returns a formatted string that contains the error message and position. -/ def toString (e : ParserError) : String := match e.input with | some str => s!"error in position {e.position} of '{str}': {e.message}" | none => s!"error in position {e.position}: {e.message}" instance : ToString ParserError := ⟨toString⟩ /-- Defines a default with "unknown error" as message an implausible position for parser error. -/ instance : Inhabited ParserError := ⟨{message := "unknown error", position := 42}⟩ end ParserError end ParserErrors section ParserResults /-- Holds either the value of the given type, if parsing was successful or a parser error in case of failure. -/ inductive ParserResult (α : Type) where | success : α → ParserResult α | failure : ParserError → ParserResult α deriving Repr, BEq /-- Defines a default for `ParserResult α` based on the default of `ParserError`. -/ instance {α : Type} : Inhabited (ParserResult α) := ⟨.failure default⟩ namespace ParserResult /-- Returns `true` iff the `ParserResult` contains a value of type `α`. -/ def isSuccess {α : Type} (res : ParserResult α) : Bool := match res with | .success _ => true | .failure _ => false /-- Converts a parser result into an optional value. -/ def to? {α : Type} (res : ParserResult α) : Option α := match res with | .success s => s | .failure _ => none /-- Unwraps the value from a `.success` parser result and panics if a `.failure` is provided. -/ def to! {α : Type} [Inhabited α] (res : ParserResult α) : α := match res with | .success s => s | .failure e => panic s!"no parser result due to {e}" /-- Converts the value from a `.success` parser result into an term of `IO α` and throws an error, if a `.failure` is provided. -/ def toIO! {α : Type} (res : ParserResult α) : IO α := do match res with | .success s => return s | .failure e => throw (IO.userError e.toString) end ParserResult end ParserResults section NonEmptyLists /-- Defines non-empty lists as subtype of `List`. -/ def NonEmptyList (α : Type) : Type := {l: List α // !l.isEmpty} instance (α : Type) [DecidableEq α] : DecidableEq (NonEmptyList α) := Subtype.instDecidableEq namespace NonEmptyList /-- Less-then (`lt`) for non-empty lists. -/ def lt {α: Type} [LT α] (a b : NonEmptyList α) : Prop := a.val.lt b.val instance (α : Type) [LT α] : LT (NonEmptyList α) := ⟨lt⟩ /-- Decidable _less-then_ for `NonEmptyList`. -/ def decLt {α: Type} [DecidableEq α] [LT α] [DecidableLT α] (a b : NonEmptyList α) : Decidable (a < b) := List.decidableLT a.val b.val instance (α : Type) [DecidableEq α] [LT α] [DecidableLT α] : DecidableLT (NonEmptyList α) := decLt /-- Provides a representation for a non empty list so that `#eval` can be used. -/ def repr {α : Type} [Repr α] (a : NonEmptyList α) (n : Nat) : Std.Format := List.repr a.val n instance (α : Type) [Repr α] : Repr (NonEmptyList α) := ⟨repr⟩ /-- Renders a non-empty list as string with its elements separated by ".". For instance, ```lean #eval toDotSeparatedString (⟨[0, 1, 2, 3, 4], rfl⟩ : NonEmptyList Nat) ``` results in `"0.1.2.3.4"`. -/ def toDotSeparatedString {α : Type} [ToString α] (a : NonEmptyList α) : String := String.intercalate "." (a.val.map (fun a => ToString.toString a)) /-- Parses the given string and, if possible, returns a result containing a non-empty list of terms of type `α`. -/ def parse {α : Type} (str : String) (parseElement : String → ParserResult α) (sep : Char) : ParserResult (NonEmptyList α) := let rec helper (lstr : List String) (parseElement : String → ParserResult α) : ParserResult (List α) := match lstr with | str::tail => match parseElement str with | .success res => match helper tail parseElement with | .success lres => .success (res::lres) | .failure e => .failure { message := e.message, position := e.position + str.length + 1, -- 1 for sep } | .failure e => .failure e | [] => .success [] match helper (str.split (· == sep)) parseElement with | .success res => if h : !res.isEmpty then .success ⟨res, h⟩ else .failure default | .failure e => .failure { message := e.message, position := e.position, input := str } end NonEmptyList end NonEmptyLists section NonEmptyStrings /-- 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](https://semver.org/#spec-item-9). -/ def NonEmptyString : Type := { s : String // !s.isEmpty } deriving instance DecidableEq, BEq, ToString, Repr for NonEmptyString namespace NonEmptyString /-- Less-then (`lt`) for non-empty strings. -/ def lt (a b : NonEmptyString) : Prop := a.val < b.val instance : LT NonEmptyString := ⟨lt⟩ /-- `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) ``` -/ def decLt (a b : NonEmptyString) : Decidable (a < b) := String.decidableLT a.val b.val instance decidableLT (a b : NonEmptyString) : Decidable (a < b) := decLt a b /-- Parses a given string and returns a result containing a non-empty string if possible. -/ def parse (str : String) : ParserResult NonEmptyString := if h: !str.isEmpty then .success ⟨str, h⟩ else .failure { message := "string must not be empty", position := 0, input := str } end NonEmptyString end NonEmptyStrings section Digits namespace Char /-- 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. ```lean def toDigit? (c: Char) : Option Nat := if c.isDigit then some (c.toNat - '0'.toNat) else none ``` -/ def toDigit? : Char → Option Nat | '0' => some 0 | '1' => some 1 | '2' => some 2 | '3' => some 3 | '4' => some 4 | '5' => some 5 | '6' => some 6 | '7' => some 7 | '8' => some 8 | '9' => some 9 | _ => none /-- 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`. -/ def isDigit' (c : Char) : Bool := match c.toDigit? with | some _ => true | none => false /-- Returns the digit as natural number for a given character that is known to be one of '0', '1' ... '9' -/ def toDigit (c : Char) (h: c.isDigit') : Nat := match g: c.toDigit? with | some n => n | none => by unfold isDigit' at h; simp [g] at h /-- Converts a digit to a natural number and panics for characters that are no digits (for base ten). -/ def toDigit! (c : Char) : Nat := match c.toDigit? with | some n => n | none => panic! s!"'{c}' is not a digit!" end Char /-- 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 ```lean def NonEmptyString.hasOnlyDigits (nes: NonEmptyString) : Bool := nes.val.isNat ``` -/ def NonEmptyString.hasOnlyDigits (nes: NonEmptyString) : Bool := let rec helper : List Char → Bool | [] => true | c::cs => c.isDigit' && (helper cs) helper nes.val.data /-- Defines a subtype of `NonEmptyString` with the restriction that all characters must be digits of base ten. This is used for the definitions ```text ::= | ::= "0" | ::= "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ``` (see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions). -/ def Digits : Type := { nes : NonEmptyString // nes.hasOnlyDigits} deriving instance DecidableEq, BEq, ToString, Repr for Digits namespace Digits /-- Converts a non-empty string of digits to `Nat`. Also here, shorter implementations exists like ```lean def toNat (nes: NonEmptyString) : Nat := nes.val.toNat! ``` However, for direct use in proofs, this implementation appears as preferable. -/ def toNat (d : Digits) : Nat := let rec helper : List Char → Nat → Nat | [], acc => acc | c::cs, acc => helper cs (acc * 10 + c.toDigit!) helper d.val.val.data 0 /-- Less-then relation for digits, which is based on `Nat` (and not `String`) as defined in https://semver.org/ under 4.1: ```text 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: ```lean 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 ``` -/ def lt (a b : Digits) := a.toNat < b.toNat instance : LT Digits := ⟨lt⟩ /-- Decidable _less-then_ for `Digits`. -/ def decLt (a b : Digits) : Decidable (a < b) := if h: a.toNat < b.toNat then have g : lt a b := by unfold lt; exact h isTrue g else have g : ¬ lt a b := by unfold lt; exact h isFalse g instance decidableLT (a b : Digits) : Decidable (a < b) := decLt a b /-- Converts strings to `Digits` if possible - wrapped into a `ParserResult`. -/ def parse (str: String) : ParserResult Digits := if h1: !str.isEmpty then let nes : NonEmptyString := ⟨str, h1⟩ if h2 : nes.hasOnlyDigits then .success ⟨nes, h2⟩ else let pos := str.find (not ∘ Char.isDigit') .failure { message := "input string contains non-digit characters", position := pos.byteIdx, input := str } else .failure {message := "input string must not be empty", position := 0, input := str} end Digits end Digits section NumericIdentifiers /-- 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. -/ def Digits.hasNoLeadingZeros (d: Digits) : Bool := match d.val.val.data with | c::(_::_) => c != '0' | _ => true /-- 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 ```text ::= "0" | | ``` (see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions). -/ def NumIdent : Type := { d: Digits // d.hasNoLeadingZeros } deriving instance DecidableEq, BEq, ToString, Repr for NumIdent namespace NumIdent /-- Converts a numeric identifier to a natural number. -/ def toNat (n : NumIdent) : Nat := n.val.toNat /-- Less-then for numerical identifiers, which is based on their value as natural number and not as strings. -/ def lt (a b : NumIdent) : Prop := a.toNat < b.toNat instance : LT NumIdent := ⟨lt⟩ /-- Decidable _less-then_ for `NumIdent`. -/ def decLt (a b : NumIdent) : Decidable (a < b) := Digits.decLt a.val b.val instance decidableLT (a b : NumIdent) : Decidable (a < b) := decLt a b /-- Parses strings into `NumIdent` wrapped into a `ParserResult` if possible. -/ def parse (str : String) : ParserResult NumIdent := match Digits.parse str with | .success dig => let lz := dig.hasNoLeadingZeros match g : lz with | true => .success ⟨dig,g⟩ | false => .failure { message := "numeric identifiers must not have leading zeros", position := 0, input := str } | .failure e => .failure e end NumIdent end NumericIdentifiers section Identifiers /-- 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 ```text ::= | ::= | "-" ::= | ::= "0" | ::= "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ::= "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). -/ def Char.isAllowedForIdentifier (chr : Char) : Bool := chr.isAlphanum || chr == '-' /-- Checks if a `NonEmptyString` only contains characters that are allowed for identifiers. -/ def NonEmptyString.isAllowedAsIdentifier (s: NonEmptyString) : Bool := let rec helper : (List Char) → Bool | chr::tail => chr.isAllowedForIdentifier && helper tail | [] => true helper s.val.data /-- Defines the fundamental base type for the different kinds of identifiers. -/ def Ident : Type := { s: NonEmptyString // s.isAllowedAsIdentifier } deriving instance DecidableEq, BEq, ToString, Repr for Ident namespace Ident def lt (a b : Ident) : Prop := a.val < b.val instance : LT Ident := ⟨lt⟩ /-- Decidable _less-then_ for `Ident`. -/ def decLt (a b : Ident) : Decidable (a < b) := NonEmptyString.decLt a.val b.val instance decidableLT (a b : Ident) : Decidable (a < b) := decLt a b /-- Parses the given string and if it is not empty and contains only allowed characters, returns an `Ident` wrapped in a `ParserResult`. -/ def parse (str : String) : ParserResult Ident := match NonEmptyString.parse str with | .failure e => .failure e | .success nes => match g : nes.isAllowedAsIdentifier with | true => .success ⟨nes, g⟩ | false => let pos := str.find (not ∘ Char.isAllowedForIdentifier) .failure { message := "character is not in [0-9A-Za-z-]", position := pos.byteIdx, input := str } end Ident end Identifiers section AlphaNumericIdentifiers /-- 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 ```text ::= | | | ``` (see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions). -/ def Char.isAllowedAndNonDigit (chr: Char) : Bool := chr.isAlpha || chr = '-' /-- Returns `true` iff at least one character in the given identifier is not a digit. -/ def Ident.hasNonDigit (i: Ident) : Bool := let rec helper : (List Char) → Bool | chr::tail => if chr.isAllowedAndNonDigit then true else helper tail | [] => false helper i.val.val.data def AlphanumIdent : Type := { i : Ident // i.hasNonDigit } instance : DecidableEq AlphanumIdent := Subtype.instDecidableEq deriving instance BEq, ToString, Repr for AlphanumIdent namespace AlphanumIdent def lt (a b : AlphanumIdent) : Prop := a.val < b.val instance : LT AlphanumIdent := ⟨lt⟩ /-- Decidable _less-then_ for `AlphanumIdent`. -/ def decLt (a b : AlphanumIdent) : Decidable (a < b) := Ident.decLt a.val b.val instance decidableLT (a b : AlphanumIdent) : Decidable (a < b) := decLt a b /-- Parses the given string and if it is a valid alphanumeric identifier, returns it wrapped in a `ParserResult`. -/ def parse (str : String) : ParserResult AlphanumIdent := match Ident.parse str with | .success id => if g : id.hasNonDigit then .success ⟨id,g⟩ else let pos := str.find (not ∘ Char.isAllowedAndNonDigit) .failure { message := "alphanumeric identifier must contain a non-digit character", position := pos.byteIdx, input := str } | .failure e => .failure e end AlphanumIdent end AlphaNumericIdentifiers section BuildIdentifiers /-- Defines build-identifiers in accordance with ```text ::= | ``` (see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions). -/ inductive BuildIdent where | alphanumIdent (val : AlphanumIdent) : BuildIdent | digits (val : Digits) : BuildIdent deriving instance DecidableEq, BEq, Repr for BuildIdent namespace BuildIdent /-- Returns the string representation of a build identifier. -/ def toString : BuildIdent → String | alphanumIdent val => (ToString.toString val) | digits val => (ToString.toString val) instance : ToString BuildIdent := ⟨toString⟩ /-- Parses the given string and if it is a valid build identifier, returns it wrapped in a `ParserResult`. -/ def parse (str : String) : ParserResult BuildIdent := match AlphanumIdent.parse str with | .success ani => .success (alphanumIdent ani) | .failure e1 => match Digits.parse str with | .success dig => .success (digits dig) | .failure e2 => .failure { message := s!"neither alphanumeric identifier nor digits found because\n1. {e1.message}\n2. {e2.message}" position := Nat.max e1.position e2.position, input := str } end BuildIdent /-- Defines dot-separated build identifiers as non-empty lists of `BuildIdent`s in accordance with ```text ::= | "." ``` (see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions). -/ def DotSepBuildIdents : Type := NonEmptyList BuildIdent deriving instance DecidableEq, BEq, Repr for DotSepBuildIdents /-- Defines a default value for `DotSepBuildIdents` so that `to!` can be used on `ParserResult DotSepBuildIdents`. -/ instance : Inhabited DotSepBuildIdents := ⟨[(BuildIdent.digits (⟨⟨"0", rfl⟩, rfl⟩: Digits))], rfl⟩ namespace DotSepBuildIdents /-- Returns the string representation of dot-separated build identifiers. -/ def toString : DotSepBuildIdents → String := NonEmptyList.toDotSeparatedString instance : ToString DotSepBuildIdents := ⟨toString⟩ /-- Parses the given string and if it is a valid dot-separated build identifiers, retruns it wrapped in a `ParserResult`. -/ def parse (str : String) : ParserResult DotSepBuildIdents := NonEmptyList.parse str BuildIdent.parse '.' end DotSepBuildIdents end BuildIdentifiers section PreReleaseIdentifiers /-- Defines pre-release identifiers in accordance with ```text ::= | ``` (see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions). -/ inductive PreRelIdent where | alphanumIdent (val : AlphanumIdent) : PreRelIdent | numIdent (val : NumIdent) : PreRelIdent deriving instance DecidableEq, BEq, Repr for PreRelIdent namespace PreRelIdent /-- 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). -/ def lt (a b : PreRelIdent) : Prop := match a, b with | alphanumIdent _, numIdent _ => False | numIdent _, alphanumIdent _ => True | alphanumIdent s, alphanumIdent t | numIdent s, numIdent t => s < t instance : LT PreRelIdent := ⟨lt⟩ /-- Decidable _less-then_ for `PreRelIdent`. -/ def decLt (a b : PreRelIdent) : Decidable (a < b) := match ha: a, hb: b with | alphanumIdent s, alphanumIdent t | numIdent s, numIdent t => if h: s < t then isTrue h else isFalse h | alphanumIdent _, numIdent _ => have h : ¬ a.lt b := by unfold lt; simp [ha, hb] isFalse (by rw [ha, hb] at h; exact h) | numIdent _, alphanumIdent _ => have h : a.lt b := by unfold lt; simp [ha, hb] isTrue (by rw [ha, hb] at h; exact h) instance : DecidableLT PreRelIdent := decLt /-- Returns the string representation of a pre-release identifier. -/ def toString : PreRelIdent → String | alphanumIdent val => (ToString.toString val) | numIdent val => (ToString.toString val) instance : ToString PreRelIdent := ⟨toString⟩ /-- Parses the given string and if it is a valid pre-release identifier, returns it wrapped in a `ParserResult`. -/ def parse (str : String) : ParserResult PreRelIdent := match AlphanumIdent.parse str with | .success val => .success (alphanumIdent val) | .failure e1 => match NumIdent.parse str with | .success val => .success (numIdent val) | .failure e2 => .failure { message := s!"neither alphanumeric nor numeric identifier found because \n1. {e1.message}\n2. {e2.message}" position := Nat.max e1.position e2.position input := str } end PreRelIdent /-- Defines dot-separated pre-release identifiers in accordance with ```text ::= | "." ``` (see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions). -/ def DotSepPreRelIdents : Type := NonEmptyList PreRelIdent deriving instance DecidableEq, BEq, Repr for DotSepPreRelIdents instance : Inhabited DotSepPreRelIdents := ⟨[(PreRelIdent.numIdent ⟨⟨⟨"0", rfl⟩, rfl⟩, rfl⟩)], rfl⟩ namespace DotSepPreRelIdents /-- Provides a representation for dot-separated pre-release identifiers so that `#eval` can be used. -/ def repr (a : DotSepPreRelIdents) (n: Nat) : Std.Format := List.repr a.val n instance : Repr DotSepPreRelIdents := ⟨repr⟩ def lt (a b : DotSepPreRelIdents) : Prop := NonEmptyList.lt a b instance : LT DotSepPreRelIdents := ⟨lt⟩ /-- Decidable _less-then_ for `DotSepPreRelIdents`. -/ def decLt (a b : DotSepPreRelIdents) : Decidable (a < b) := NonEmptyList.decLt a b instance : DecidableLT DotSepPreRelIdents := decLt def toString : DotSepPreRelIdents → String := NonEmptyList.toDotSeparatedString instance : ToString DotSepPreRelIdents := ⟨toString⟩ /-- Parses the given string and if it is a valid dot-separated pre-release identifiers, returns it wrapped in a `ParserResult`. -/ def parse (str : String) : ParserResult DotSepPreRelIdents := NonEmptyList.parse str PreRelIdent.parse '.' end DotSepPreRelIdents end PreReleaseIdentifiers section VersionCores /-- Defines the version _core_ in accordance with ```text ::= "." "." ::= ::= ::= ``` (see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions). Version cores default to `1.0.0`. -/ structure VersionCore where major : Nat := 1 minor : Nat := 0 patch : Nat := 0 deriving DecidableEq, BEq, Repr, Inhabited namespace VersionCore /-- Returns the string representation of a version core. -/ def toString (a : VersionCore) : String := s!"{a.major}.{a.minor}.{a.patch}" instance : ToString VersionCore := ⟨toString⟩ /-- Returns the version core as list of three natural numbers. -/ def toList (v : VersionCore) : List Nat := [v.major, v.minor, v.patch] /-- Constructs a version core from a list of three natural numbers. -/ def fromList (l : List Nat) (h : l.length == 3) : VersionCore := match l with | [m,n,p] => {major := m, minor := n, patch := p} /-- Less-then for version cores. -/ def lt (v w : VersionCore) : Prop := v.toList < w.toList instance : LT VersionCore := ⟨lt⟩ /-- Decides if `<` holds true for two version cores. -/ def decLt (v w : VersionCore) : Decidable (v < w) := v.toList.decidableLT w.toList instance : DecidableLT VersionCore := decLt /-- Parses the given string and if it is a valid version core, returns it wrapped in a `ParserResult`. -/ def parse (str : String) : ParserResult VersionCore := match NonEmptyList.parse str NumIdent.parse '.' with | .success l => let nums := l.val.map NumIdent.toNat if h : nums.length == 3 then .success (fromList nums h) else .failure { message := "exactly three numbers - separated by '.' - must be provided, not one more, not one less", position := 0, input := str } | .failure e => .failure e end VersionCore end VersionCores section Versions /-- Defines a full semantic version in accordance with ```text ::= | "-" | "+" | "-" "+" ::= ::= ``` (see https://semver.org/#backusnaur-form-grammar-for-valid-semver-versions). -/ structure Version extends VersionCore where preRelease : Option DotSepPreRelIdents := none build : Option DotSepBuildIdents := none deriving DecidableEq, BEq, Repr, Inhabited namespace Version /-- Returns the string representation of a version. -/ def toString (a : Version) : String := match a.preRelease, a.build with | none, none => s!"{a.toVersionCore}" | some r, none => s!"{a.toVersionCore}-{r}" | none, some b => s!"{a.toVersionCore}+{b}" | some r, some b => s!"{a.toVersionCore}-{r}+{b}" instance : ToString Version := ⟨toString⟩ /-- Helper function for comparing the parts of versions outside the version core. -/ def ltPreRelease (a b : Version) : Bool := match a.preRelease, b.preRelease with | some _, none => true | some s, some t => (s.decLt t).decide | none, none | none, some _ => false /-- Less-then for versions in accordance with [section 11 of the SemVer specification](https://semver.org/#spec-item-11). -/ def lt (v w : Version) : Prop := (v.toVersionCore < w.toVersionCore) ∨ (v.toVersionCore = w.toVersionCore ∧ (v.ltPreRelease w = true)) instance : LT Version := ⟨lt⟩ /-- Decides if `<` holds true for two versions. -/ def decLt (v w : Version) : Decidable (v < w) := match v.toVersionCore.decLt w.toVersionCore with | isTrue h1 => have h2 : v.lt w := by unfold lt; simp [h1] isTrue h2 | isFalse h1 => if h2 : v.toVersionCore = w.toVersionCore then if h3: v.ltPreRelease w then have h4 : lt v w := by unfold lt; simp [h2, h3] isTrue h4 else have h4 : ¬ lt v w := by unfold lt; simp [h1]; simp[h2, h3] isFalse h4 else have h3 : ¬ lt v w := by unfold lt; simp [h1, h2] isFalse h3 instance : DecidableLT Version := decLt /-- Helper function that parses the version core and optional pre-release part of a version string. -/ def parseCorePreRel (str : String) : ParserResult (VersionCore × Option DotSepPreRelIdents) := match str.split (· == '-') with | [] => panic "internal error - split returns empty list" | core_str::tail => let pre_rel_str := String.intercalate "-" tail let core_res := VersionCore.parse core_str match core_res with | .failure e => .failure e | .success core => if pre_rel_str.isEmpty then .success (core, none) else match DotSepPreRelIdents.parse pre_rel_str with | .success pre_rel => .success (core, pre_rel) | .failure e => .failure { message := e.message, position := e.position + core_str.length + 1 input := str } /-- Parses the given string and if it is a valid version, returns it wrapped in a `ParserResult`. -/ def parse (str : String) : ParserResult Version := match str.split (· == '+') with | [] => panic "internal error - split returns empty list" | [core_pre_rel_str] => match parseCorePreRel core_pre_rel_str with | .failure e => .failure e | .success core_pre_rel_res => .success { toVersionCore := core_pre_rel_res.fst, preRelease := core_pre_rel_res.snd, build := none } | [core_pre_rel_str, build_str] => match parseCorePreRel core_pre_rel_str with | .failure e => .failure e | .success core_pre_rel_res => match DotSepBuildIdents.parse build_str with | .success build_res => .success { toVersionCore := core_pre_rel_res.fst, preRelease := core_pre_rel_res.snd, build := build_res } | .failure e => .failure { message := e.message, position := e.position + core_pre_rel_str.length + 1, input := str } | head1::(head2::_) => .failure { message := "versions cannot contain more than one plus-sign", position := head1.length + head2.length + 1, input := str } /-- Returns `true` if public API provided under this version is stable. -/ def isStable (v: Version) : Bool := match v with | { major := 0, minor := _, patch := _, preRelease := _, build := _ } | { major := _, minor := _, patch := _, preRelease := some _, build := _ } => false | _ => true /-- Returns a version that is the next major version based on the provided version. The returned version has no pre-release or build metadata. -/ def nextMajor (v : Version) : Version := {major := v.major + 1} /-- Returns a version that is the next minor version based on the provided version. The returned version has no pre-release or build metadata. -/ def nextMinor (v : Version) : Version := {major := v.major, minor := v.minor + 1} /-- Returns a version that is the next patch version based on the provided version. The returned version has no pre-release or build metadata. -/ def nextPatch (v : Version) : Version := {major := v.major, minor := v.minor, patch := v.patch + 1} /-- 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. -/ def subsequentPreRelease? (v : Version) (str : String) : Option Version := match parse s!"{v.toVersionCore}-{str}" with | .success w => if v < w then w else none | .failure _ => none /-- 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. -/ def setPreRelease? (v: Version) (str : String) : Option Version := match v with | { toVersionCore := c, preRelease := _ , build := _ } => (parse s!"{c}-{str}").to? /-- 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. -/ def setBuild? (v: Version) (str : String) : Option Version := match v with | { toVersionCore := c, preRelease := none, build := _ } => (parse s!"{c}+{str}").to? | { toVersionCore := c, preRelease := some p, build := _ } => (parse s!"{c}-{p}+{str}").to? /-- Helper function that checks if a character can be the start of a version in a string, given the previous character (if any). -/ def isPossibleStart (previous : Option Char) (current : Char) : Bool := match previous, current with | none, d => d.isDigit | some c, d => (!c.isDigit) && (d.isDigit) end Version /-- Helper function that checks if a character is valid in a version string. -/ def Char.isValidForVersion (c : Char ) : Bool := c.isAllowedForIdentifier || c == '.' || c == '+' def VersionCore.addPreRelease? (c : VersionCore) (suffix : String) : Option Version := (Version.parse s!"{c}-{suffix}").to? end Versions section Extraction /-- Helper that cuts off the prefix of a string that cannot be part of a version. -/ def cutOffPrefix (ch : Option Char) (str: String) : String := let rec helper : (Option Char) → (List Char) → (List Char) | _, [] => [] | c, d::t => if (Version.isPossibleStart c) d then d::t else helper d t String.mk ((helper ch) str.data) /-- Extracts all versions that are contained in a given string. -/ def extractVersions (str: String) : List Version := let rec helper : List String → List Version | [] => [] | text::tail => let withoutPrefix := cutOffPrefix none text match Version.parse withoutPrefix with | .success v => v::(helper tail) | .failure _ => helper tail helper (str.split (not ∘ Char.isValidForVersion)) end Extraction