pkgs/build-support/coq/extra-lib.nix

   1 { lib }:
   2
   3 let
   4   inherit (lib)
   5     all
   6     concatStringsSep
   7     findFirst
   8     flip
   9     getAttr
  10     head
  11     isFunction
  12     length
  13     recursiveUpdate
  14     splitVersion
  15     tail
  16     take
  17     versionAtLeast
  18     versionOlder
  19     zipListsWith
  20     ;
  21 in
  22 recursiveUpdate lib (rec {
  23
  24   versions =
  25     let
  26       truncate = n: v: concatStringsSep "." (take n (splitVersion v));
  27       opTruncate = op: v0: v: let n = length (splitVersion v0); in
  28          op (truncate n v) (truncate n v0);
  29     in rec {
  30
  31     /* Get string of the first n parts of a version string.
  32
  33        Example:
  34        - truncate 2 "1.2.3-stuff"
  35          => "1.2"
  36
  37        - truncate 4 "1.2.3-stuff"
  38          => "1.2.3.stuff"
  39     */
  40
  41     inherit truncate;
  42
  43     /* Get string of the first three parts (major, minor and patch)
  44        of a version string.
  45
  46        Example:
  47          majorMinorPatch "1.2.3-stuff"
  48          => "1.2.3"
  49     */
  50     majorMinorPatch = truncate 3;
  51
  52     /* Version comparison predicates,
  53       - isGe v0 v <-> v is greater or equal than v0   [*]
  54       - isLe v0 v <-> v is lesser  or equal than v0   [*]
  55       - isGt v0 v <-> v is strictly greater than v0   [*]
  56       - isLt v0 v <-> v is strictly lesser  than v0   [*]
  57       - isEq v0 v <-> v is equal to v0                [*]
  58       - range low high v <-> v is between low and high [**]
  59
  60     [*]  truncating v to the same number of digits as v0
  61     [**] truncating v to low for the lower bound and high for the upper bound
  62
  63       Examples:
  64       - isGe "8.10" "8.10.1"
  65         => true
  66       - isLe "8.10" "8.10.1"
  67         => true
  68       - isGt "8.10" "8.10.1"
  69         => false
  70       - isGt "8.10.0" "8.10.1"
  71         => true
  72       - isEq "8.10" "8.10.1"
  73         => true
  74       - range "8.10" "8.11" "8.11.1"
  75         => true
  76       - range "8.10" "8.11+" "8.11.0"
  77         => false
  78       - range "8.10" "8.11+" "8.11+beta1"
  79         => false
  80
  81     */
  82     isGe = opTruncate versionAtLeast;
  83     isGt = opTruncate (flip versionOlder);
  84     isLe = opTruncate (flip versionAtLeast);
  85     isLt = opTruncate versionOlder;
  86     isEq = opTruncate pred.equal;
  87     range = low: high: pred.inter (versions.isGe low) (versions.isLe high);
  88   };
  89
  90   /* Returns a list of list, splitting it using a predicate.
  91      This is analoguous to builtins.split sep list,
  92      with a predicate as a separator and a list instead of a string.
  93
  94     Type: splitList :: (a -> bool) -> [a] -> [[a]]
  95
  96     Example:
  97       splitList (x: x == "x") [ "y" "x" "z" "t" ]
  98       => [ [ "y" ] "x" [ "z" "t" ] ]
  99   */
 100   splitList = pred: l: # put in file lists
 101     let loop = (vv: v: l: if l == [] then vv ++ [v]
 102       else let hd = head l; tl = tail l; in
 103       if pred hd then loop (vv ++ [ v hd ]) [] tl else loop vv (v ++ [hd]) tl);
 104     in loop [] [] l;
 105
 106   pred = {
 107     /* Predicate intersection, union, and complement */
 108     inter = p: q: x: p x && q x;
 109     union = p: q: x: p x || q x;
 110     compl = p:    x: ! p x;
 111     true  = p: true;
 112     false = p: false;
 113
 114     /* predicate "being equal to y" */
 115     equal = y:    x: x == y;
 116   };
 117
 118   /* Emulate a "switch - case" construct,
 119    instead of relying on `if then else if ...` */
 120   /* Usage:
 121   ```nix
 122   switch-if [
 123     if-clause-1
 124     ..
 125     if-clause-k
 126   ] default-out
 127   ```
 128   where a if-clause has the form `{ cond = b; out = r; }`
 129   the first branch such as `b` is true */
 130
 131   switch-if = c: d: (findFirst (getAttr "cond") {} c).out or d;
 132
 133   /* Usage:
 134   ```nix
 135   switch x [
 136     simple-clause-1
 137     ..
 138     simple-clause-k
 139   ] default-out
 140   ```
 141   where a simple-clause has the form `{ case = p; out = r; }`
 142   the first branch such as `p x` is true
 143   or
 144   ```nix
 145   switch [ x1 .. xn ] [
 146     complex-clause-1
 147     ..
 148     complex-clause-k
 149   ] default-out
 150   ```
 151   where a complex-clause is either a simple-clause
 152   or has the form { cases = [ p1 .. pn ]; out = r; }
 153   in which case the first branch such as all `pi x` are true
 154
 155   if the variables p are not functions,
 156   they are converted to a equal p
 157   if out is missing the default-out is taken */
 158
 159   switch = var: clauses: default: with pred; let
 160       compare = f:  if isFunction f then f else equal f;
 161       combine = cl: var:
 162         if cl?case then compare cl.case var
 163         else all (equal true) (zipListsWith compare cl.cases var); in
 164     switch-if (map (cl: { cond = combine cl var; inherit (cl) out; }) clauses) default;
 165
 166   /* Override arguments to mkCoqDerivation for a Coq library.
 167
 168      This function allows you to easily override arguments to mkCoqDerivation,
 169      even when they are not exposed by the Coq library directly.
 170
 171      Type: overrideCoqDerivation :: AttrSet -> CoqLibraryDerivation -> CoqLibraryDerivation
 172
 173      Example:
 174
 175      ```nix
 176      coqPackages.lib.overrideCoqDerivation
 177        {
 178          defaultVersion = "9999";
 179          release."9999".hash = "sha256-fDoP11rtrIM7+OLdMisv2EF7n/IbGuwFxHiPtg3qCNM=";
 180        }
 181        coqPackages.QuickChick;
 182      ```
 183
 184      This example overrides the `defaultVersion` and `release` arguments that
 185      are passed to `mkCoqDerivation` in the QuickChick derivation.
 186
 187      Note that there is a difference between using `.override` on a Coq
 188      library vs this `overrideCoqDerivation` function. `.override` allows you
 189      to modify arguments to the derivation itself, for instance by passing
 190      different versions of dependencies:
 191
 192      ```nix
 193      coqPackages.QuickChick.override { ssreflect = my-cool-ssreflect; }
 194      ```
 195
 196      whereas `overrideCoqDerivation` allows you to override arguments to the
 197      call to `mkCoqDerivation` in the Coq library.
 198
 199      Note that all Coq libraries in Nixpkgs have a `version` argument for
 200      easily using a different version.  So if all you want to do is use a
 201      different version, and the derivation for the Coq library already has
 202      support for the version you want, you likely only need to update the
 203      `version` argument on the library derivation.  This is done with
 204      `.override`:
 205
 206      ```nix
 207      coqPackages.QuickChick.override { version = "1.4.0"; }
 208      ```
 209   */
 210   overrideCoqDerivation = f: drv: (drv.override (args: {
 211     mkCoqDerivation = drv_: (args.mkCoqDerivation drv_).override f;
 212   }));
 213 })