lib: etc

lib/default.nix

@@ -15,11 +15,15 @@ let
     trivial = callLibs ./trivial.nix;
     fixedPoints = callLibs ./fixed-points.nix;
 
+    # control flow
+    switchs = callLibs ./switchs.nix;
+
     # datatypes
     attrsets = callLibs ./attrsets.nix;
     lists = callLibs ./lists.nix;
     strings = callLibs ./strings.nix;
     stringsWithDeps = callLibs ./strings-with-deps.nix;
+    preds = callLibs ./preds.nix;
 
     # packaging
     customisation = callLibs ./customisation.nix;
@@ -71,6 +75,7 @@ let
       toHexString toBaseDigits;
     inherit (self.fixedPoints) fix fix' converge extends composeExtensions
       composeManyExtensions makeExtensible makeExtensibleWithCustomName;
+    inherit (self.switchs) switch-if switch;
     inherit (self.attrsets) attrByPath hasAttrByPath setAttrByPath
       getAttrFromPath attrVals attrValues getAttrs catAttrs filterAttrs
       filterAttrsRecursive foldAttrs collect nameValuePair mapAttrs
@@ -81,7 +86,7 @@ let
       getLib getDev getMan chooseDevOutputs zipWithNames zip
       recurseIntoAttrs dontRecurseIntoAttrs cartesianProductOfSets;
     inherit (self.lists) singleton forEach foldr fold foldl foldl' imap0 imap1
-      concatMap flatten remove findSingle findFirst any all count
+      concatMap flatten remove findSingle findFirst splitList any all count
       optional optionals toList range partition zipListsWith zipLists
       reverseList listDfs toposort sort naturalSort compareLists take
       drop sublist last init crossLists unique intersectLists

lib/lists.nix

@@ -200,6 +200,46 @@ rec {
     let found = filter pred list;
     in if found == [] then default else head found;
 
+  /* Takes a predicate and a list as input and
+     returns a list of lists, separated by elements that match the predicate.
+
+     This is analoguous to `builtins.split separator string`,
+     with a predicate instead of a separator
+     and a list instead of a string.
+
+     Type: splitList :: (a -> bool) -> [a] -> [ (a | [a]) ]
+
+     The returned list always has the form `[ [...] sep [...] ... sep [...] ]`
+     i.e. begins with a list, alternates with separators and ends with a list,
+     so that the following is true for `res = splitList pred l`:
+     - `res` has length `2 * k + 1`,
+       where `k` is the number of elements of `l` that
+       match `pred`. (ie `splitList pred l`)
+     - `elemAt res (2 * n)` is always a list,
+       which contains no element matching `pred`.
+     - `elemAt res (2 * n + 1)` is always a single element that matches `pred`.
+
+     Ie, for all `pred` and `l`, let `k = length (filter pred l)`, we have:
+     - `length (splitList pred l) = 2 * k + 1`,
+     - `isList (elemAt (splitList pred l) (2 * n))`, for all `n <= k`,
+     - `pred (elemAt (splitList pred l) (2 * n + 1))`, for all `n < k`,
+     - `flatten (map (pick (splitList pred l)) (range 0 (2 * k))) == l`, where
+       `pick = r: n: (if mod n 2 == 1 then singleton else id) (elemAt r n)`
+
+     Examples:
+     - splitList (x: x == "x") [ "y" "x" "z" "t" ]
+       => [ [ "y" ] "x" [ "z" "t" ] ]
+     - splitList (x: false) l == [ l ]
+     - splitList (x: x < 2) [ 2 1 3 4 0 1 3 1 ]
+       => [ [ 2 ] 1 [ 3 4 ] 0 [ ] 1 [ 3 ] 1 [ ] ]
+
+  */
+  splitList = pred: l:
+    let loop = (vv: v: l: if l == [] then vv ++ [v]
+      else let hd = head l; tl = tail l; in
+      if pred hd then loop (vv ++ [ v hd ]) [] tl else loop vv (v ++ [hd]) tl);
+    in loop [] [] l;
+
   /* Return true if function `pred` returns true for at least one
      element of `list`.
 

lib/preds.nix

@@ -0,0 +1,17 @@
+{ lib }:
+with lib; {
+  /* Constant predicates: true and false */
+  true  = p: true;
+  false = p: false;
+
+  /* Predicate intersection, union, complement,
+     difference and implication */
+  inter = p: q: x: p x && q x;
+  union = p: q: x: p x || q x;
+  compl = p:    x: ! p x;
+  diff  = p: q: preds.inter p (preds.compl q);
+  impl  = p: q: x: p x -> q x;
+
+  /* predicate "being equal to x" */
+  equal = x: y: y == x;
+}

lib/switchs.nix

@@ -0,0 +1,75 @@
+{ lib }:
+with lib; {
+  /* Emulate a "switch - case" construct,
+   instead of relying on `if then else if ...` */
+
+  /* Usage:
+       ```nix
+       switch-if [
+         if-clause-1
+         ..
+         if-clause-k
+       ] default-out
+       ```
+       where a if-clause has the form `{ cond = b; out = r; }`
+       the first branch such as `b` is true
+
+     Example:
+       ```nix
+       let alphanum = n: switch-if [
+           { cond = n == 0; out = "zero"; }
+           { cond = n == 1; out = "one";  }
+         ] "I do not count beyond one"; in
+       [ (alphanum 0) (alphanum 1) (alphanum 42) ]
+       ```
+      => `[ "zero" "one" "I do not count beyond one" ]`
+
+  */
+  switch-if = c: d: (findFirst (getAttr "cond") {} c).out or d;
+
+  /* Usage:
+       ```nix
+       switch x [
+         simple-clause-1
+         ..
+         simple-clause-k
+       ] default-out
+       ```
+       where a simple-clause has the form `{ case = p; out = r; }`
+       the first branch such as `p x` is true
+       or
+       ```nix
+       switch [ x1 .. xn ] [
+         complex-clause-1
+         ..
+         complex-clause-k
+       ] default-out
+       ```
+       where a complex-clause is either a simple-clause
+       or has the form { cases = [ p1 .. pn ]; out = r; }
+       in which case the first branch such as all `pi xi` are true
+
+       if the variables p are not functions,
+       they are converted to a `equal p`
+       if `out` is missing then `default-out` is taken
+
+     Example:
+       ```nix
+       let test = v1: v2: with versions; switch [ v1 v2 ] [
+           { cases = [ (x: x * 2 < 4) 8 ]; out = "small, 8"; }
+           { case  = [ 42 42 ]; }          # no `out` means `default-out`
+           { case  = l: fold add 0 l > 42; out = "sum over 42"; }
+           { case  = [ 0 1 ];              out = "zero, one"; }
+         ] "weird"; in
+       [ (test 1 8) (test 40 3) (test 0 1) (test 42 42) (test 1 0)]
+       ```
+      => `[ "small, 8" "sum over 42" "zero, one" "weird" "weird" ]`
+  */
+  switch = var: clauses: default: with preds; let
+      compare = f:  if isFunction f then f else equal f;
+      combine = cl: var:
+        if cl?case then compare cl.case var
+        else all (equal true) (zipListsWith compare cl.cases var); in
+    switch-if (map (cl: { cond = combine cl var;
+                          out = cl.out or default; }) clauses) default;
+}

lib/versions.nix

@@ -1,13 +1,29 @@
 /* Version string functions. */
 { lib }:
 
-rec {
+with lib;
+let
+  truncate = n: v: concatStringsSep "." (take n (splitVersion v));
+  opTruncate = op: v0: v: let n = length (splitVersion v0); in
+     op (truncate n v) (truncate n v0);
+in rec {
 
   /* Break a version string into its component parts.
 
      Example:
        splitVersion "1.2.3"
        => ["1" "2" "3"]
+
+     Remark: the builtins version of `splitVersion` -- which is
+     considered first -- has a behaviour which is different from
+     `(lib.splitString ".")`. For example, it also recognizes `-` and
+     transitions between numbers and other strings as delimiters.
+     This behaviour is hence inconsistent between versions of nix and
+     should not be relied upon.
+
+     Example (discouraged):
+       splitVersion "1-2a+3"
+       => [ "1" "2" "a+" "3" ]
   */
   splitVersion = builtins.splitVersion or (lib.splitString ".");
 
@@ -35,15 +51,106 @@ rec {
   */
   patch = v: builtins.elemAt (splitVersion v) 2;
 
+  /* Get string of the first n parts of a version string.
+
+    Example:
+    - truncate 2 "1.2.3-stuff"
+      => "1.2"
+    - truncate 4 "1.2.3-stuff"
+      => "1.2.3.stuff"
+  */
+
+  inherit truncate;
+
   /* Get string of the first two parts (major and minor)
      of a version string.
 
      Example:
        majorMinor "1.2.3"
        => "1.2"
   */
-  majorMinor = v:
-    builtins.concatStringsSep "."
-    (lib.take 2 (splitVersion v));
+  majorMinor = truncate 2;
+
+  /* Get string of the first three parts (major, minor and patch)
+     of a version string.
+
+    Example:
+      majorMinorPatch "1.2.3-stuff"
+      => "1.2.3"
+  */
+  majorMinorPatch = truncate 3;
+
+  /* Version comparison predicates,
+    - isGe v0 v <-> v is greater or equal than v0   [*]
+    - isLe v0 v <-> v is lesser  or equal than v0   [*]
+    - isGt v0 v <-> v is strictly greater than v0   [*]
+    - isLt v0 v <-> v is strictly lesser  than v0   [*]
+    - isEq v0 v <-> v is equal to v0                [*]
+    - range low high v <-> v is between low and high [**]
+
+    [*]  truncating v to the same number of digits as v0
+    [**] truncating v to low for the lower bound and high for the upper bound
+
+    Difference with `versionAtLeast` and `versionOlder`:
+    - `versionAtLeast` and `versionOlder` implement order relations on
+      version numbers, which are total assuming the only separator
+      which is used is `.`.
+
+    - `isGe`, `isLe`, `isLt`, and `isEq` are not order relations, they
+    are not antisymmetric (e.g. both `isLe "1.1" "1.1.2"` and `isLe
+    "1.1.2" "1.1"` are true).
+    `(isLe x) y` reads «`y` is a version which is lesser or equal to `x`».
+    Contrarily to `versionAtLeast`, it uses the first argument to
+    determine the length to truncate so that `isLe "1.1" "1.1.2"` is
+    true while `versionAtLeast "1.1" "1.1.2"` is false.
+
+    The main motivation is to be able to combine and read them nicely
+    with high order function such as:
+    - `filter`, e.g. the result of
+      ```
+      filter (versionAtLeast "1.0")
+             [ "1.3.1" "1.0.0" "1.0" "0.9.0" "1.0.2" ]
+      ```
+      is `[ "1.0" "0.9.0"]`.
+      In comparison
+      ```
+      filter (isLe "1.0")
+             [ "1.3.1" "1.0.0" "1.0" "0.9.0" "1.0.2" ]`
+      ```
+      returns `[ "1.0.0" "1.0" "0.9.0" "1.0.2" ]`, which can be read
+      naturally in English as «we keep versions that are lesser or
+      equal to "1.0"» and the outcome matches the expectations that
+      "1.0.0" and "1.0.2" belong to the family of "1.0" versions.
+        If you wanted to filter more precisely you should give the
+      patch version of the first argument of `isLe` instead (as in
+      `isLe "1.0.0"`, and if you wanted to exclude all "1.0", then you
+      should use `isLt "1.0"`.
+    - `switch` as in:
+      pkgs/development/coq-modules/mathcomp/default.nix#L21-L22
+
+    Examples:
+    - isGe "8.10" "8.10.1"
+      => true
+    - isLe "8.10" "8.10.1"
+      => true
+    - isGt "8.10" "8.10.1"
+      => false
+    - isGt "8.10.0" "8.10.1"
+      => true
+    - isEq "8.10" "8.10.1"
+      => true
+    - range "8.10" "8.11" "8.11.1"
+      => true
+    - range "8.10" "8.11+" "8.11.0"
+      => false
+    - range "8.10" "8.11+" "8.11+beta1"
+      => false
+  */
+  isGe = opTruncate versionAtLeast;
+  isGt = opTruncate (flip versionOlder);
+  isLe = opTruncate (flip versionAtLeast);
+  isLt = opTruncate versionOlder;
+  isEq = opTruncate preds.equal;
+  range = low: high: preds.inter (versions.isGe low) (versions.isLe high);
 
 }

pkgs/applications/science/logic/coq/default.nix

@@ -13,8 +13,6 @@
 , csdp ? null
 , version, coq-version ? null,
 }@args:
-let lib' = lib; in
-let lib = import ../../../../build-support/coq/extra-lib.nix {lib = lib';}; in
 with builtins; with lib;
 let
   release = {

pkgs/build-support/coq/default.nix

@@ -1,5 +1,4 @@
 { lib, stdenv, coqPackages, coq, fetchzip }@args:
-let lib = import ./extra-lib.nix {inherit (args) lib;}; in
 with builtins; with lib;
 let
   isGitHubDomain = d: match "^github.*" d != null;
@@ -74,7 +73,7 @@ stdenv.mkDerivation (removeAttrs ({
 
   meta = ({ platforms = coq.meta.platforms; } //
     (switch domain [{
-        case = pred.union isGitHubDomain isGitLabDomain;
+        case = preds.union isGitHubDomain isGitLabDomain;
         out = { homepage = "https://${domain}/${owner}/${repo}"; };
       }] {}) //
     optionalAttrs (fetched.broken or false) { coqFilter = true; broken = true; }) //