packages feed

futhark 0.26.2 → 0.26.3

raw patch · 51 files changed

+2073/−458 lines, 51 files

Files

CHANGELOG.md view
@@ -5,6 +5,26 @@ The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/) and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html). +## [0.26.3]++### Added++* `futhark test` now suppports property-based testing (like QuickCheck). Work by+  Matin Nafar and Simon August Mørk.++### Fixed++* `futhark bench`: entry points that consumed their input produced misleading+  profiling information. (#2464)++* Sometimes arrays returned from entry points would be unnecessarily copied if+  the compiler could not be sure statically that they were in row-major layout.++* The type checker would fail to reject entry points that accepted lifted+  abstract types. (#2467)++* An issue in the interpreter's handling of local opens.+ ## [0.26.2]  ### Added
docs/js-api.rst view
@@ -9,7 +9,7 @@ those wrappers.  The exact generated files and the top-level JavaScript interface differ-somewhat between the WASM-style backends and the WebGPU backend, so the+somewhat between the WASM backend and the WebGPU backend, so the relevant differences are described below.  First a warning: **the JavaScript API is experimental**.  It may@@ -40,16 +40,33 @@  The exact file set is backend-dependent and may change over time. -The module exports a function, ``newFutharkContext``, which is a factory-function that returns a Promise producing a ``FutharkContext``-instance (see below).  A simple usage example:+The generated JavaScript wrapper exposes a ``FutharkModule`` class,+which is the preferred top-level interface for using a compiled Futhark+program from JavaScript.  The module is initialised with the generated+backend runtime module. +The initialisation pattern is the same for the WASM-style backend and+the WebGPU backend. The only difference is how ``Module`` is made available.+For the WASM-style backend, the generated ``.mjs`` file exports it as the+default export, so it is imported together with ``FutharkModule``:+ .. code-block:: javascript -   import { newFutharkContext } from './futlib.mjs';-   var fc;-   newFutharkContext().then(x => fc = x);+   import Module, { FutharkModule } from './futlib.mjs'; +   const module = await Module();++   const fut = new FutharkModule();+   await fut.init(module);++For the WebGPU backend, the generated runtime module is usually loaded+before the application code, for example:++.. code-block:: html++   <script src="futlib.js"></script>+   <script src="main.js"></script>+ General concerns ---------------- @@ -61,50 +78,45 @@ Top-level wrapper objects ------------------------- -The top-level JavaScript interface differs between backends.--WASM wrapper-~~~~~~~~~~~~--The WASM backend exports a ``newFutharkContext()`` factory function that-asynchronously constructs a ``FutharkContext``.--.. js:function:: newFutharkContext()--   Asynchronously create a new ``FutharkContext`` object.+The preferred top-level JavaScript interface is ``FutharkModule``.  A+``FutharkModule`` object represents an instance of a compiled Futhark+program. It owns the underlying Futhark context and is used to construct+arrays, call entry points, and free resources. -.. js:class:: FutharkContext()+.. js:class:: FutharkModule()     A bookkeeping class representing an instance of a compiled Futhark    program. -.. js:function:: FutharkContext.free()+.. js:function:: FutharkModule.init(module) -   Frees all memory created by the ``FutharkContext`` object.  It is an-   error to use a ``FutharkArray`` or ``FutharkOpaque`` after the-   ``FutharkContext`` on which they were defined has been freed.+   Asynchronously initialise the ``FutharkModule`` object. -WebGPU wrapper-~~~~~~~~~~~~~~+   For the WASM-style backend, the ``module`` argument is optional. If+   omitted, the generated wrapper loads the WebAssembly module itself. -The WebGPU backend generates a ``FutharkModule`` wrapper class.  This-wrapper is initialised with the generated backend runtime module.+   For the WebGPU backend, ``module`` must be the generated backend+   runtime module. -.. js:class:: FutharkModule()+.. js:function:: FutharkModule.free() -   A bookkeeping class representing an instance of a compiled Futhark-   program.+   Frees the Futhark context and configuration associated with the+   module. It is an error to use a ``FutharkArray`` or ``FutharkOpaque``+   after the ``FutharkModule`` on which it was created has been freed. -.. js:function:: FutharkModule.init(module)+.. js:attribute:: FutharkModule.entry -   Asynchronously initialise the ``FutharkModule`` object with the-   generated backend runtime module.+   Object containing the generated entry point functions. For example,+   an entry point named ``main`` is available as ``fut.entry.main``. -.. js:function:: FutharkModule.free()+.. js:attribute:: FutharkModule.types -   Frees the Futhark context and configuration associated with the-   module.+   Object containing generated type information and array constructor+   objects for the array types used by the program. +The backends also provides utility methods for synchronisation,+cache management, and profiling.+ .. js:function:: FutharkModule.context_sync()     Wait for pending backend work associated with the context to finish.@@ -125,6 +137,25 @@     Resume profiling. +WASM compatibility interface+~~~~~~~~~~~~~~~~~~~~~~~~~~~~++The WASM-style backend also keep the older ``FutharkContext`` interface+for backwards compatibility.++.. js:function:: newFutharkContext()++   Asynchronously create a new ``FutharkContext`` object.++.. js:class:: FutharkContext()++   Backwards-compatible wrapper class for WASM-style backend.+   ``FutharkContext`` supports the same main interface as+   ``FutharkModule``, including ``entry``, ``types``, array constructors,+   and ``free``.++New code should prefer ``FutharkModule``.+ Values ------ @@ -138,34 +169,11 @@ FutharkArray ------------ -The exact ``FutharkArray`` API differs slightly between backends.--WASM wrapper-~~~~~~~~~~~~--.. js:function:: FutharkArray.toArray()--   Returns a nested JavaScript array.--.. js:function:: FutharkArray.toTypedArray()--   Returns a flat typed array of the underlying data.+Arrays are represented by ``FutharkArray`` objects.  The common array API is+shared by the WASM backend and the WebGPU backend.  .. js:function:: FutharkArray.shape() -   Returns the shape of the ``FutharkArray`` as an array of ``BigInt`` values.--.. js:function:: FutharkArray.free()--   Frees the memory used by the ``FutharkArray``.--WebGPU wrapper-~~~~~~~~~~~~~~--The WebGPU backend generates per-type subclasses of ``FutharkArray``.--.. js:function:: FutharkArray.get_shape()-    Returns the shape of the array as a ``BigInt64Array``.  .. js:function:: FutharkArray.values()@@ -176,32 +184,41 @@     Frees the memory used by the ``FutharkArray``. -Array construction also differs a bit between backends.+The WASM backend also provides a few older convenience methods. -For the WASM wrapper, ``FutharkContext`` contains constructor methods for-each array type that appears in an entry point.  For example, for the-type ``[]i32``:+.. js:function:: FutharkArray.toArray() -.. js:function:: FutharkContext.new_i32_1d_from_jsarray(jsarray)+   Returns a nested JavaScript array. -   Creates and returns a one-dimensional ``i32`` ``FutharkArray``-   representing the JavaScript array ``jsarray``.+.. js:function:: FutharkArray.toTypedArray() -.. js:function:: FutharkContext.new_i32_1d(array, dim0)+   Returns a flat typed array of the underlying data. -   Creates and returns a one-dimensional ``i32`` ``FutharkArray``-   representing the typed array ``array``, with shape ``dim0``.+.. js:function:: FutharkArray.shape() -For the WebGPU wrapper, each generated array type is represented by its-own generated class, available through the ``FutharkModule`` object.+   Returns the shape of the ``FutharkArray`` as an array of ``BigInt`` values. +Array construction+~~~~~~~~~~~~~~~~~~++Each array type used by an entry point is exposed through a generated+constructor object.  For example, for the type ``[]i32``:+ .. js:function:: fut.i32_1d.from_data(data, dim0)     Creates and returns a one-dimensional ``i32`` ``FutharkArray`` from    a JavaScript ``Array`` or the corresponding typed array, with the    given shape. +For the WASM backend, the generated constructor object also+provides a convenience method for nested JavaScript arrays. +.. js:function:: fut.i32_1d.from_jsarray(jsarray)++   Creates and returns a one-dimensional ``i32`` ``FutharkArray`` from+   a JavaScript array.  For higher-dimensional arrays, the JavaScript+   array is expected to be nested according to the array rank.+ FutharkOpaque ------------- @@ -219,11 +236,18 @@ Entry Points ------------ -Each entry point in the compiled futhark program for the WASM wrapper has an entry point method on-the ``FutharkContext``, and for the WebGPU wrapper, each entry point is exposed through the ``entry`` field of the ``FutharkModule`` object:+Each entry point in the compiled Futhark program is exposed through the+``entry`` field of the top-level wrapper object. For example, an entry+point named ``main`` can be called as: -.. js:function:: FutharkContext.<entry_point_name>(in1, ..., inN)+.. code-block:: javascript -  The entry point function taking the N arguments of the Futhark entry point-  function, and returns the result. For the WASM wrapper, if the result is a tuple the return value-  is an array. For the WebGPU wrapper, if there are multiple outputs, the return value is an array of outputs in order.+   const res = await fut.entry.main(in1, ..., inN);++.. js:function:: fut.entry.<entry_point_name>(in1, ..., inN)++   The entry point function takes the JavaScript representations of the+   Futhark entry point arguments and returns the result.++   If the entry point has multiple outputs, the return value is an array+   containing the outputs in order.
docs/man/futhark-bench.rst view
@@ -14,13 +14,13 @@ DESCRIPTION =========== -This tool is the recommended way to benchmark Futhark programs.-Programs are compiled using the specified backend (``c`` by default),-then run a number of times for each test case, and the arithmetic mean-runtime and 95% confidence interval printed on standard output.  Refer-to :ref:`futhark-test(1)` for information on how to format test data.-A program will be ignored if it contains no data sets - it will not-even be compiled.+This tool is the recommended way to benchmark Futhark programs. Programs are+compiled using the specified backend (``c`` by default), then run a number of+times for each test case, and the arithmetic mean runtime and 95% confidence+interval printed on standard output. Refer to :ref:`futhark-test(1)` for+information on how to format test data. A program will be ignored if it contains+no data sets - it will not even be compiled. Property-based tests are ignored+when benchmarking.  If compilation of a program fails, then ``futhark bench`` will abort immediately.  If execution of a test set fails, an error message will
docs/man/futhark-test.rst view
@@ -28,12 +28,11 @@   ==   cases... -The ``description`` is an arbitrary (and possibly multiline)-human-readable explanation of the test program.  It is separated from-the test cases by a line containing just ``==``.  Any comment starting-at the beginning of the line, and containing a line consisting of just-``==``, will be considered a test block.  The format of a test case is-as follows::+The ``description`` is an arbitrary (and possibly multiline) human-readable+explanation of the test program. It is separated from the test cases by a line+containing just ``==``. Any comment starting at the beginning of the line, and+containing a line consisting of just ``==``, will be considered a test block.+The format of a unit test case is as follows::    [tags { tags... }]   [entry: names...]@@ -136,6 +135,49 @@ element. If no suffix is provided, integer arrays have element type ``i32`` and decimal arrays have type ``f64``. +PROPERTY-BASED TESTING+----------------------++Apart from containing input/output tests as described above, a test block may+also have the following form::++  property: names...++In this case, the names indicate *properties*. A property is an entry point+with this type::++  t -> bool++for some ``t``, which has been given a ``#[prop]`` pragma. To test a property,+``futhark test`` will randomly generate values of type ``t``, called+*candidates*, looking for a candidate that makes the property return ``false``,+called a *counterexample*. When a counterexample has been found, ``futhark+test`` will try to shrink it and finally report the smallest counterexample that+it was able construct.++The ``#[prop]`` attribute supports various optional arguments that grant more+control over the testing process. They are passed as arguments, e.g.,+``#[prop(gen(foo),shrink(bar))]``. The following are supported:++* ``gen(f)``, where ``f`` is an entry point function with this type::++    (size: i64) -> (seed: u64) -> t++  Instead of automatically generating candidates for the property, ``futhark+  test`` will invoke ``f`` with a size and a randomly generated seed. This can+  be used to generate more complicated types.++* ``shrink(f)``, where ``f`` is an entry point function with this type::++    t -> u64 -> t++  When shrinking a counterexample, ``futhark test`` will call ``f`` with the+  candidate so far along with a random number, which is then expected to return+  a smaller value.++* ``size(N)``, where ``N`` is an integer. This sets the size of generated candidates+  (or the size argument passed to generators).+ OPTIONS ======= @@ -186,6 +228,11 @@   Run ``structure`` tests. These are not run by default. When this   option is passed, no other testing is done. +--seed=INT++  Set random seed used to generate values for property-based tests. If unset, a+  seed is randomly generated.+ --futhark=program    The program used to perform operations (eg. compilation).  Defaults@@ -278,8 +325,16 @@   -- random input { [100]i32 [100]i32 } auto output   -- random input { [1000]i32 [1000]i32 } auto output -  let main xs ys = i32.product (map2 (*) xs ys)+  entry main xs ys = i32.product (map2 (*) xs ys) +The following tests that reverse is an involution::++  -- ==+  -- property: reverse_involution++  #[prop]+  entry reverse_involution (xs: []i32) =+    and (map2 (==) (reverse (reverse xs)) xs)  SEE ALSO ========
futhark.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name:           futhark-version:        0.26.2+version:        0.26.3 synopsis:       An optimising compiler for a functional, array-oriented language.  description:    Futhark is a small programming language designed to be compiled to@@ -320,7 +320,6 @@       Futhark.Optimise.BlkRegTiling       Futhark.Optimise.CSE       Futhark.Optimise.DoubleBuffer-      Futhark.Optimise.EntryPointMem       Futhark.Optimise.Fusion       Futhark.Optimise.Fusion.Composing       Futhark.Optimise.Fusion.GraphRep@@ -394,6 +393,7 @@       Futhark.Profile.SourceRange       Futhark.Script       Futhark.Test+      Futhark.Test.Property       Futhark.Test.Spec       Futhark.Test.Values       Futhark.Tools
rts/c/cache.h view
@@ -67,8 +67,8 @@   if (fseek(f, 0, SEEK_END) != 0) {     goto error;   }-  int64_t f_size = (int64_t)ftell(f);-  if (fseek(f, CACHE_HEADER_SIZE, SEEK_SET) != 0) {+  int64_t f_size = (int64_t)ftello(f);+  if (fseeko(f, CACHE_HEADER_SIZE, SEEK_SET) != 0) {     goto error;   } 
rts/c/server.h view
@@ -1624,7 +1624,7 @@   // (which doesn't care if there's extra at the end), then we compute   // how much space the the object actually takes in serialised form   // and rewind the file to that position.  The only downside is more IO.-  size_t start = ftell(f);+  size_t start = (size_t)ftello(f);   size_t size;   char *bytes = fslurp_file(f, &size);   void *obj = aux->restore(ctx, bytes);@@ -1633,10 +1633,10 @@     *(void**)p = obj;     size_t obj_size;     (void)aux->store(ctx, obj, NULL, &obj_size);-    fseek(f, start+obj_size, SEEK_SET);+    fseeko(f, start+obj_size, SEEK_SET);     return 0;   } else {-    fseek(f, start, SEEK_SET);+    fseeko(f, start, SEEK_SET);     return 1;   } }
rts/c/util.h view
@@ -60,10 +60,10 @@ // Read the rest of an open file into a NUL-terminated string; returns // NULL on error. static void* fslurp_file(FILE *f, size_t *size) {-  long start = ftell(f);-  fseek(f, 0, SEEK_END);-  long src_size = ftell(f)-start;-  fseek(f, start, SEEK_SET);+  off_t start = ftello(f);+  fseeko(f, 0, SEEK_END);+  off_t src_size = ftello(f)-start;+  fseeko(f, start, SEEK_SET);   unsigned char *s = (unsigned char*) malloc((size_t)src_size + 1);   if (fread(s, 1, (size_t)src_size, f) != (size_t)src_size) {     free(s);
rts/javascript/wrapperclasses.js view
@@ -32,9 +32,13 @@   shape() {     this.validCheck();     var s = this.fshape(this.ctx.ctx, this.ptr) >> 3;-    return Array.from(this.ctx.wasm.HEAP64.subarray(s, s + this.dim));+    return this.ctx.wasm.HEAP64.subarray(s, s + this.dim);   } +  // get_shape() {+  //   return BigInt64Array.from(this.shape());+  // }+   toTypedArray(dims = this.shape()) {     this.validCheck();     console.assert(dims.length === this.dim, "dim=%s,dims=%s", this.dim, dims.toString());@@ -56,6 +60,10 @@         return Array.from(Array(d0), (x,i) => nest(offs + i * d1, ds.slice(1)));       }     })(0, dims);+  }++  async values() {+    return this.toTypedArray();   } } 
src/Futhark/Analysis/LastUse.hs view
@@ -301,6 +301,10 @@   let free_in_e = freeIn se <> freeIn sp   (used_nms', lu_vars) <- lastUsedInNames used_nms free_in_e   pure (M.empty, lu_vars, used_nms')+lastUseMemOp _ (EnsureDirect v) used_nms = do+  let free_in_e = freeIn v+  (used_nms', lu_vars) <- lastUsedInNames used_nms free_in_e+  pure (M.empty, lu_vars, used_nms') lastUseMemOp onInner (Inner op) used_nms = onInner op used_nms  lastUseSegOp ::@@ -399,6 +403,10 @@ lastUseSeqOp :: Op (Aliases SeqMem) -> Names -> LastUseM SeqMem (LUTabFun, Names, Names) lastUseSeqOp (Alloc se sp) used_nms = do   let free_in_e = freeIn se <> freeIn sp+  (used_nms', lu_vars) <- lastUsedInNames used_nms free_in_e+  pure (mempty, lu_vars, used_nms')+lastUseSeqOp (EnsureDirect v) used_nms = do+  let free_in_e = freeIn v   (used_nms', lu_vars) <- lastUsedInNames used_nms free_in_e   pure (mempty, lu_vars, used_nms') lastUseSeqOp (Inner NoOp) used_nms = do
src/Futhark/Analysis/MemAlias.hs view
@@ -85,6 +85,9 @@   MemAliasesM (inner rep) MemAliases analyzeStm m (Let (Pat [PatElem vname _]) _ (Op (Alloc _ _))) =   pure $ m <> singleton vname mempty+analyzeStm m (Let (Pat (PatElem mem_name _ : _)) _ (Op (EnsureDirect _))) =+  pure $ m <> singleton mem_name mempty+analyzeStm m (Let _ _ (Op (EnsureDirect _))) = pure m analyzeStm m (Let _ _ (Op (Inner inner))) = do   on_inner <- asks onInner   on_inner m inner
src/Futhark/Bench.hs view
@@ -325,9 +325,11 @@         | otherwise =             Nothing +      maybeReload =+        when (any inputConsumed input_types) reloadInput+       doRun = do         call_lines <- cmdEither (cmdCall server entry out ins)-        when (any inputConsumed input_types) reloadInput         case mapMaybe runtime call_lines of           [call_runtime] -> pure (RunResult call_runtime, call_lines)           [] -> throwError "Could not find runtime in output."@@ -337,9 +339,9 @@     -- First one uncounted warmup run.     void $ cmdEither $ cmdCall server entry out ins -    ys <- runMinimum (freeOut *> doRun) opts 0 0 mempty+    ys <- runMinimum (freeOut *> doRun <* maybeReload) opts 0 0 mempty -    xs <- runConvergence (freeOut *> doRun) opts ys+    xs <- runConvergence (freeOut *> doRun <* maybeReload) opts ys      -- Possibly a profiled run at the end.     profile_log <-@@ -347,6 +349,8 @@         then pure Nothing         else do           cmdMaybe . liftIO $ cmdUnpauseProfiling server+          -- No need to reload the input here, and it would indeed be misleading+          -- in the profiling results.           profile_log <- freeOut *> doRun           cmdMaybe . liftIO $ cmdPauseProfiling server           pure $ Just profile_log
src/Futhark/CLI/Autotune.hs view
@@ -130,7 +130,7 @@    truns <-     case testAction spec of-      RunCases ios _ _ | not $ null ios -> do+      RunCases ios _ _ _ | not $ null ios -> do         when (optVerbose opts > 1) $           putStrLn $             unwords ("Entry points:" : map (T.unpack . iosEntryPoint) ios)
src/Futhark/CLI/Bench.hs view
@@ -186,7 +186,7 @@ compileBenchmark opts (program, program_spec) = do   spec <- maybe (pure program_spec) testSpecFromFileOrDie $ optTestSpec opts   case testAction spec of-    RunCases cases _ _+    RunCases cases _ _ _       | null $           optExcludeCase opts             `intersect` (testTags spec <> testTags program_spec),
src/Futhark/CLI/Dataset.hs view
@@ -5,18 +5,19 @@ module Futhark.CLI.Dataset (main) where  import Control.Monad-import Control.Monad.ST import Data.Binary qualified as Bin import Data.ByteString.Lazy.Char8 qualified as BS import Data.Text qualified as T import Data.Text.IO qualified as T-import Data.Vector.Generic (freeze)-import Data.Vector.Storable qualified as SVec-import Data.Vector.Storable.Mutable qualified as USVec import Data.Word import Futhark.Data qualified as V import Futhark.Data.Reader (readValues)-import Futhark.Util (convFloat)+import Futhark.Test.Values+  ( RandomConfiguration (..),+    Range,+    initialRandomConfiguration,+    randomValue,+  ) import Futhark.Util.Options import Language.Futhark.Parser import Language.Futhark.Pretty ()@@ -29,8 +30,6 @@   ) import System.Exit import System.IO-import System.Random (mkStdGen, uniformR)-import System.Random.Stateful (UniformRange (..))  -- | Run @futhark dataset@. main :: String -> [String] -> IO ()@@ -209,23 +208,6 @@ toValueType (TEVar v _) =   Left $ "Unknown type " <> prettyText v --- | Closed interval, as in @System.Random@.-type Range a = (a, a)--data RandomConfiguration = RandomConfiguration-  { i8Range :: Range Int8,-    i16Range :: Range Int16,-    i32Range :: Range Int32,-    i64Range :: Range Int64,-    u8Range :: Range Word8,-    u16Range :: Range Word16,-    u32Range :: Range Word32,-    u64Range :: Range Word64,-    f16Range :: Range Half,-    f32Range :: Range Float,-    f64Range :: Range Double-  }- -- The following lines provide evidence about how Haskells record -- system sucks. seti8Range :: Range Int8 -> RandomConfiguration -> RandomConfiguration@@ -260,67 +242,3 @@  setf64Range :: Range Double -> RandomConfiguration -> RandomConfiguration setf64Range bounds config = config {f64Range = bounds}--initialRandomConfiguration :: RandomConfiguration-initialRandomConfiguration =-  RandomConfiguration-    (minBound, maxBound)-    (minBound, maxBound)-    (minBound, maxBound)-    (minBound, maxBound)-    (minBound, maxBound)-    (minBound, maxBound)-    (minBound, maxBound)-    (minBound, maxBound)-    (0.0, 1.0)-    (0.0, 1.0)-    (0.0, 1.0)--randomValue :: RandomConfiguration -> V.ValueType -> Word64 -> V.Value-randomValue conf (V.ValueType ds t) seed =-  case t of-    V.I8 -> gen i8Range V.I8Value-    V.I16 -> gen i16Range V.I16Value-    V.I32 -> gen i32Range V.I32Value-    V.I64 -> gen i64Range V.I64Value-    V.U8 -> gen u8Range V.U8Value-    V.U16 -> gen u16Range V.U16Value-    V.U32 -> gen u32Range V.U32Value-    V.U64 -> gen u64Range V.U64Value-    V.F16 -> gen f16Range V.F16Value-    V.F32 -> gen f32Range V.F32Value-    V.F64 -> gen f64Range V.F64Value-    V.Bool -> gen (const (False, True)) V.BoolValue-  where-    gen range final = randomVector (range conf) final ds seed--randomVector ::-  (SVec.Storable v, UniformRange v) =>-  Range v ->-  (SVec.Vector Int -> SVec.Vector v -> V.Value) ->-  [Int] ->-  Word64 ->-  V.Value-randomVector range final ds seed = runST $ do-  -- Use some nice impure computation where we can preallocate a-  -- vector of the desired size, populate it via the random number-  -- generator, and then finally reutrn a frozen binary vector.-  arr <- USVec.new n-  let fill g i-        | i < n = do-            let (v, g') = uniformR range g-            USVec.write arr i v-            g' `seq` fill g' $! i + 1-        | otherwise =-            pure ()-  fill (mkStdGen $ fromIntegral seed) 0-  final (SVec.fromList ds) . SVec.convert <$> freeze arr-  where-    n = product ds---- XXX: The following instance is an orphan.  Maybe it could be--- avoided with some newtype trickery or refactoring, but it's so--- convenient this way.-instance UniformRange Half where-  uniformRM (a, b) g =-    (convFloat :: Float -> Half) <$> uniformRM (convFloat a, convFloat b) g
src/Futhark/CLI/Dev.hs view
@@ -675,6 +675,11 @@       "Ignore 'unsafe'.",     Option       []+      ["strip-provenance"]+      (NoArg $ Right $ changeFutharkConfig $ \opts -> opts {futharkStripProvenance = True})+      "Strip provenance (location information).",+    Option+      []       ["entry-points"]       ( ReqArg           ( \arg -> Right $
src/Futhark/CLI/Misc.hs view
@@ -84,7 +84,7 @@      testSpecRuns = testActionRuns . testAction     testActionRuns CompileTimeFailure {} = []-    testActionRuns (RunCases ios _ _) = concatMap iosTestRuns ios+    testActionRuns (RunCases ios _ _ _) = concatMap iosTestRuns ios  -- | @futhark check-syntax@ mainCheckSyntax :: String -> [String] -> IO ()
src/Futhark/CLI/Test.hs view
@@ -14,16 +14,19 @@ import Control.Monad.Trans.Class (lift) import Data.ByteString qualified as SBS import Data.ByteString.Lazy qualified as LBS+import Data.IORef import Data.List (delete, partition) import Data.Map.Strict qualified as M+import Data.Maybe (mapMaybe) import Data.Text qualified as T import Data.Text.Encoding qualified as T import Data.Text.IO qualified as T import Data.Time.Clock.System (SystemTime (..), getSystemTime)+import Data.Word (Word64) import Futhark.Analysis.Metrics.Type import Futhark.Server import Futhark.Test-import Futhark.Util (atMostChars, fancyTerminal, showText)+import Futhark.Util (atMostChars, fancyTerminal, randomSeed, showText) import Futhark.Util.Options import Futhark.Util.Pretty (annotate, bgColor, bold, hardline, pretty, putDoc, vsep) import Futhark.Util.Table@@ -92,8 +95,8 @@ timeout :: Int timeout = 5 * 60 * 1000000 -withProgramServer :: FilePath -> FilePath -> [String] -> (Server -> IO [TestResult]) -> TestM ()-withProgramServer program runner extra_options f = do+withProgramServer :: FilePath -> FilePath -> [String] -> IORef PBTPhase -> (Server -> IO [TestResult]) -> TestM ()+withProgramServer program runner extra_options phaseRef f = do   -- Explicitly prefixing the current directory is necessary for   -- readProcessWithExitCode to find the binary when binOutputf has   -- no path component.@@ -112,7 +115,24 @@       race (threadDelay timeout) (f server) >>= \case         Left _ -> do           abortServer server-          fail $ "test timeout after " <> show timeout <> " microseconds"+          st <- readIORef phaseRef+          fail . T.unpack $+            "test timeout after " <> showText timeout <> " microseconds" <> case activeTest st of+              Nothing -> mempty+              Just activeTestName -> do+                -- use annotate to make the phase name stand out in the error message, since it is the most likely place to find out what went wrong+                let phaseInfo = maybe mempty (" during phase " <>) (phase st)+                    shrinkInfo = maybe mempty (" while shrinking with " <>) (shrinkWith st)+                    sizeInfo = maybe mempty ((" at size=" <>) . showText) (phaseSize st)+                    seedInfo = maybe mempty ((" and seed=" <>) . showText) (phaseSeed st)+                    tacticInfo = maybe mempty ((" with tactic=" <>) . showText) (phaseRandom st)+                ". Was evaluating property:\n"+                  <> activeTestName+                  <> phaseInfo+                  <> shrinkInfo+                  <> sizeInfo+                  <> seedInfo+                  <> tacticInfo         Right r -> pure r  data TestMode@@ -134,7 +154,8 @@   { _testCaseMode :: TestMode,     testCaseProgram :: FilePath,     testCaseTest :: ProgramTest,-    _testCasePrograms :: ProgConfig+    _testCasePrograms :: ProgConfig,+    pbtConfig :: PBTConfig   }   deriving (Show) @@ -252,7 +273,7 @@    in accErrors_ $ map runInterpretedCase run_cases  runTestCase :: TestCase -> TestM ()-runTestCase (TestCase mode program testcase progs) = do+runTestCase (TestCase mode program testcase progs pbtConfig) = do   futhark <- liftIO $ maybe getExecutablePath pure $ configFuthark progs   let checkctx =         mconcat@@ -289,11 +310,22 @@               ExitSuccess -> pure ()               ExitFailure 127 -> throwError $ progNotFound $ T.pack futhark               ExitFailure _ -> throwError $ T.decodeUtf8 err-    RunCases ios structures warnings -> do+    RunCases ios structures warnings properties -> do       -- Compile up-front and reuse same executable for several entry points.       let backend = configBackend progs           extra_compiler_options = configExtraCompilerOptions progs +      phaseRef <-+        liftIO . newIORef $+          PBTPhase+            { activeTest = Nothing,+              phase = Nothing,+              shrinkWith = Nothing,+              phaseSize = Nothing,+              phaseSeed = Nothing,+              phaseRandom = Nothing+            }+       when (mode `elem` [Compiled, Interpreted]) $         context "Generating reference outputs" $           -- We probably get the concurrency at the test program level,@@ -316,10 +348,29 @@                     ++ configExtraOptions progs                 runner = configRunner progs             context "Running compiled program" $-              withProgramServer program runner extra_options $ \server -> do+              withProgramServer program runner extra_options phaseRef $ \server -> do                 let run = runCompiledEntry (FutharkExe futhark) server program-                concat <$> mapM run ios+                liftIO (extractPropSpecs server (map propertyEntryPoint properties)) >>= \case+                  Left err -> pure [Failure [err]]+                  Right propSpecs -> liftIO $ do+                    normal_test_result <- concat <$> mapM run ios +                    let verifiedProps = selectRequestedPropSpecs properties propSpecs+                    pbt_resultE <- runPBT pbtConfig server verifiedProps phaseRef program++                    let allResults = flip map pbt_resultE $ \case+                          Left err -> Failure [err]+                          Right (Just e) -> Failure [e]+                          Right Nothing -> Success++                    let hasFailures = any (\case Failure _ -> True; _ -> False) allResults++                    when hasFailures $+                      liftIO $+                        propToFile program allResults++                    pure $ normal_test_result ++ allResults+       when (mode == Interpreted) $         context "Interpreting" $           accErrors_ $@@ -464,7 +515,7 @@  makeTestCase :: TestConfig -> TestMode -> (FilePath, ProgramTest) -> TestCase makeTestCase config mode (file, spec) =-  excludeCases config $ TestCase mode file spec $ configPrograms config+  excludeCases config $ TestCase mode file spec (configPrograms config) (configPBTConfig config)  data ReportMsg   = TestStarted TestCase@@ -489,8 +540,8 @@   where     onTest (ProgramTest desc tags action) =       ProgramTest desc tags $ onAction action-    onAction (RunCases ios stest wtest) =-      RunCases (map onIOs $ filter relevantEntry ios) stest wtest+    onAction (RunCases ios stest wtest properties) =+      RunCases (map onIOs $ filter relevantEntry ios) stest wtest properties     onAction action = action     onIOs (InputOutputs entry runs) =       InputOutputs entry $ filter (not . any excluded . runTags) runs@@ -569,6 +620,7 @@   all_tests <-     map (makeTestCase config mode)       <$> testSpecsFromPathsOrDie paths+  -- putStrLn $ "Test cases are: " ++ show (map testCaseProgram all_tests)   testmvar <- newEmptyMVar   reportmvar <- newEmptyMVar   concurrency <- maybe getNumCapabilities pure $ configConcurrency config@@ -591,11 +643,11 @@       numTestCases tc =         case testAction $ testCaseTest tc of           CompileTimeFailure _ -> 1-          RunCases ios sts wts ->+          RunCases ios sts wts pbts ->             length (concatMap iosTestRuns ios)               + length sts               + length wts-+              + length pbts       getResults ts         | null (testStatusRemain ts) = report ts >> pure ts         | otherwise = do@@ -639,7 +691,6 @@                             testStatusRunFail ts'                               + min (numTestCases test) (length s)                         }-   when fancy spaceTable    ts <-@@ -659,7 +710,12 @@   -- Removes "Now testing" output.   if fancy     then cursorUpLine 1 >> clearLine-    else putStrLn $ show (testStatusPass ts) <> "/" <> show (testStatusTotal ts) <> " passed."+    else+      putStrLn $+        show (testStatusPass ts)+          <> "/"+          <> show (testStatusTotal ts)+          <> " passed."    unless (null excluded) . putStrLn $     show (length excluded) ++ " program(s) excluded."@@ -678,7 +734,8 @@     configExclude :: [T.Text],     configLineOutput :: Bool,     configConcurrency :: Maybe Int,-    configEntryPoint :: Maybe String+    configEntryPoint :: Maybe String,+    configPBTConfig :: PBTConfig   }  defaultConfig :: TestConfig@@ -698,7 +755,14 @@           },       configLineOutput = False,       configConcurrency = Nothing,-      configEntryPoint = Nothing+      configEntryPoint = Nothing,+      configPBTConfig =+        PBTConfig+          { configNumTests = 100,+            configMaxSize = 50,+            configSeed = randomSeed,+            configShrinkTries = 5+          }     }  data ProgConfig = ProgConfig@@ -716,6 +780,9 @@ changeProgConfig :: (ProgConfig -> ProgConfig) -> TestConfig -> TestConfig changeProgConfig f config = config {configPrograms = f $ configPrograms config} +changePBTConfig :: (PBTConfig -> PBTConfig) -> TestConfig -> TestConfig+changePBTConfig f config = config {configPBTConfig = f $ configPBTConfig config}+ setBackend :: FilePath -> ProgConfig -> ProgConfig setBackend backend config =   config {configBackend = backend}@@ -854,7 +921,72 @@           )           "NAME"       )-      "Only run entry points with this name."+      "Only run entry points with this name.",+    Option+      "n"+      ["num-tests"]+      ( ReqArg+          ( \n ->+              case reads n of+                [(n', "")]+                  | n' >= 0 ->+                      Right $ changePBTConfig $ \pbt -> pbt {configNumTests = n'}+                _ ->+                  Left . optionsError $ "'" ++ n ++ "' is not a non-negative integer."+          )+          "NUM"+      )+      $ "Number of tests to run per property (default: "+        <> show (configNumTests . configPBTConfig $ defaultConfig)+        <> ").",+    Option+      "m"+      ["max-size"]+      ( ReqArg+          ( \n ->+              case reads n of+                [(n', "")]+                  | n' >= 0 ->+                      Right $ changePBTConfig $ \pbt -> pbt {configMaxSize = n'}+                _ ->+                  Left . optionsError $ "'" ++ n ++ "' is not a non-negative integer."+          )+          "NUM"+      )+      $ "Maximum size parameter to use for generators (default: "+        <> show (configMaxSize . configPBTConfig $ defaultConfig)+        <> ").",+    Option+      []+      ["seed"]+      ( ReqArg+          ( \n ->+              case (reads n :: [(Word64, String)]) of+                [(n', "")] ->+                  Right $ changePBTConfig $ \pbt -> pbt {configSeed = n'}+                _ ->+                  Left . optionsError $ "'" ++ n ++ "' is not a valid integer."+          )+          "NUM"+      )+      "Set seed for all tests to use for generators.",+    Option+      []+      ["num-tries"]+      ( ReqArg+          ( \n ->+              case reads n of+                [(n', "")]+                  | n' >= 0 ->+                      Right $ changePBTConfig $ \pbt -> pbt {configShrinkTries = n'}+                _ ->+                  Left . optionsError $ "'" ++ n ++ "' is not a non-negative integer."+          )+          "NUM"+      )+      $ "The number of tries the shrinker will perform before giving up (default: "+        <> show (configShrinkTries . configPBTConfig $ defaultConfig)+        <> ")."   ]  excludeBackend :: TestConfig -> TestConfig@@ -865,9 +997,35 @@           : configExclude config     } +selectRequestedPropSpecs :: [PropertyCase] -> [PropSpec] -> [PropSpec]+selectRequestedPropSpecs properties specs =+  mapMaybe lookupSpec properties+  where+    lookupSpec (PropertyCase name) =+      firstMatching name specs++    firstMatching _ [] =+      Nothing+    firstMatching name (spec : rest)+      | psProp spec == name = Just spec+      | otherwise = firstMatching name rest++-- Save to file helper functions+propToFile :: FilePath -> [TestResult] -> IO ()+propToFile testFile results = do+  let fileName = dropExtension testFile <> ".prop_result"+      textResults = T.unlines $ concatMap resultLines results+  withFile fileName WriteMode $ \h ->+    T.hPutStr h textResults+  where+    resultLines :: TestResult -> [T.Text]+    resultLines Success = []+    resultLines (Failure msgs) = msgs+ -- | Run @futhark test@. main :: String -> [String] -> IO ()-main = mainWithOptions defaultConfig commandLineOptions "options... programs..." $ \progs config ->-  case progs of-    [] -> Nothing-    _ -> Just $ runTests (excludeBackend config) progs+main =+  mainWithOptions defaultConfig commandLineOptions "options... programs..." $ \progs config ->+    case progs of+      [] -> Nothing+      _ -> Just $ runTests (excludeBackend config) progs
src/Futhark/CodeGen/Backends/GenericC.hs view
@@ -314,6 +314,7 @@ #ifndef _GNU_SOURCE // Avoid possible double-definition warning. #define _GNU_SOURCE #endif+#define _FILE_OFFSET_BITS 64 |]  -- We may generate variables that are never used (e.g. for
src/Futhark/CodeGen/Backends/GenericWASM.hs view
@@ -132,7 +132,12 @@          "_futhark_context_config_free",          "_futhark_context_new",          "_futhark_context_free",-         "_futhark_context_get_error"+         "_futhark_context_get_error",+         "_futhark_context_sync",+         "_futhark_context_clear_caches",+         "_futhark_context_report",+         "_futhark_context_pause_profiling",+         "_futhark_context_unpause_profiling"        ]   where     -- Include array types from both entry points and record fields.@@ -153,23 +158,28 @@       classFutharkContext entryPoints opaqueTypes     ] +-- Make FutharkModule the generated primary class, but keeps FutharkContext around for backwards compatibility. classFutharkContext :: [JSEntryPoint] -> [(String, JSOpaqueType)] -> T.Text classFutharkContext entryPoints opaqueTypes =   T.unlines-    [ "class FutharkContext {",-      constructor entryPoints opaqueTypes,+    [ "class FutharkModule {",+      moduleConstructor,+      moduleInitFromWasm entryPoints opaqueTypes,+      moduleInit,       getFreeFun,       getEntryPointsFun,       getTypesFun,       getErrorFun,+      getUtilityFuns,       T.unlines $ map toFutharkArray arrays,       T.unlines $ concatMap (generateProjectMethods . snd) opaqueTypes,       T.unlines $ map jsWrapEntryPoint entryPoints,       "}",+      classFutharkContextCompat,       [text|-      async function newFutharkContext() {+      async function newFutharkContext(num_threads) {         var wasm = await loadWASM();-        return new FutharkContext(wasm);+        return new FutharkContext(wasm, num_threads);       }       |]     ]@@ -180,32 +190,90 @@     entryPointTypes = concatMap (\jse -> parameters jse ++ [ret jse]) entryPoints     recordFieldTypes = [jsrfType rf | (_, JSOpaqueRecord fields) <- opaqueTypes, rf <- fields] -constructor :: [JSEntryPoint] -> [(String, JSOpaqueType)] -> T.Text-constructor jses opaqueTypes =+moduleConstructor :: T.Text+moduleConstructor =   [text|-  constructor(wasm, num_threads) {+  constructor() {+    this.wasm = undefined;+    this.cfg = undefined;+    this.ctx = undefined;+    this.entry_points = {};+    this.types = {};+    this.entry = {};+  }+  |]++moduleInitFromWasm :: [JSEntryPoint] -> [(String, JSOpaqueType)] -> T.Text+moduleInitFromWasm jses opaqueTypes =+  [text|+  _init_from_wasm(wasm, num_threads) {     this.wasm = wasm;     this.cfg = this.wasm._futhark_context_config_new();     if (num_threads) this.wasm._futhark_context_config_set_num_threads(this.cfg, num_threads);     this.ctx = this.wasm._futhark_context_new(this.cfg);+     this.entry_points = {       ${entries}     };     this.types = {       ${type_entries}     };+    this.entry = {};+    ${entry_aliases}+    ${array_aliases}+    ${array_type_aliases}   }   |]   where     entries = T.intercalate "," $ map dicEntry jses     type_entries = T.intercalate "," $ map dicTypeEntry opaqueTypes+    entry_aliases = T.unlines $ map entryAlias jses+    array_aliases = T.unlines $ map arrayAlias arrays+    array_type_aliases = T.unlines $ map arrayTypeAlias arrays +    arrays = nubOrd $ filter isArray (entryPointTypes ++ recordFieldTypes)+    entryPointTypes = concatMap (\jse -> parameters jse ++ [ret jse]) jses+    recordFieldTypes = [jsrfType rf | (_, JSOpaqueRecord fields) <- opaqueTypes, rf <- fields]++moduleInit :: T.Text+moduleInit =+  [text|+  async init(wasm, num_threads) {+    if (wasm === undefined) {+      throw new Error("FutharkModule.init() requires the generated backend runtime module");+    }++    this._init_from_wasm(wasm, num_threads);+  }+  |]++classFutharkContextCompat :: T.Text+classFutharkContextCompat =+  [text|+  class FutharkContext extends FutharkModule {+    constructor(wasm, num_threads) {+      super();++      if (wasm !== undefined) {+        this._init_from_wasm(wasm, num_threads);+      }+    }+  }+  |]+ getFreeFun :: T.Text getFreeFun =   [text|   free() {-    this.wasm._futhark_context_free(this.ctx);-    this.wasm._futhark_context_config_free(this.cfg);+    if (this.ctx !== undefined) {+      this.wasm._futhark_context_free(this.ctx);+      this.ctx = undefined;+    }++    if (this.cfg !== undefined) {+      this.wasm._futhark_context_config_free(this.cfg);+      this.cfg = undefined;+    }   }   |] @@ -237,6 +305,65 @@   }   |] +getUtilityFuns :: T.Text+getUtilityFuns =+  [text|+  async context_sync() {+    return this.wasm._futhark_context_sync(this.ctx);+  }++  async clear_caches() {+    return this.wasm._futhark_context_clear_caches(this.ctx);+  }++  async report() {+    var ptr = this.wasm._futhark_context_report(this.ctx);+    var len = this.wasm.HEAP8.subarray(ptr).indexOf(0);+    var bytes = this.wasm.HEAPU8.subarray(ptr, ptr + len);+    var str = new TextDecoder().decode(bytes);+    this.wasm._free(ptr);+    return str;+  }++  async pause_profiling() {+    return this.wasm._futhark_context_pause_profiling(this.ctx);+  }++  async unpause_profiling() {+    return this.wasm._futhark_context_unpause_profiling(this.ctx);+  }+  |]++entryAlias :: JSEntryPoint -> T.Text+entryAlias jse =+  [text|this.entry["${ename}"] = this.${fname}.bind(this);|]+  where+    fname = GC.escapeName $ T.pack $ name jse+    ename = T.pack $ name jse++arrayAlias :: String -> T.Text+arrayAlias typ =+  [text|+  this.${signature} = {+    from_data: (data, ${dims}) => this.new_${signature}(data, ${dims}),+    from_jsarray: (data) => this.new_${signature}_from_jsarray(data)+  };+  |]+  where+    d = dim typ+    ftype = baseType typ+    signature = T.pack $ ftype ++ "_" ++ show d ++ "d"+    dims = T.pack $ intercalate ", " ["d" ++ show i | i <- [0 .. d - 1]]++arrayTypeAlias :: String -> T.Text+arrayTypeAlias typ =+  [text|this.types["${typ_text}"] = this.${signature};|]+  where+    d = dim typ+    ftype = baseType typ+    signature = T.pack $ ftype ++ "_" ++ show d ++ "d"+    typ_text = T.pack typ+ dicEntry :: JSEntryPoint -> T.Text dicEntry jse =   [text|@@ -476,4 +603,4 @@  -- | The names exported by the generated module. libraryExports :: T.Text-libraryExports = "export {newFutharkContext, FutharkContext, FutharkArray, FutharkOpaque};"+libraryExports = "export {newFutharkContext, FutharkContext, FutharkModule, FutharkArray, FutharkOpaque};"
src/Futhark/CodeGen/ImpGen.hs view
@@ -59,6 +59,7 @@     tvVar,     ToExp (..),     compileAlloc,+    compileEnsureDirect,     everythingVolatile,     compileBody,     compileBody',@@ -1741,6 +1742,32 @@     Just allocator' -> allocator' (patElemName mem) e' compileAlloc pat _ _ =   error $ "compileAlloc: Invalid pattern: " ++ prettyString pat++-- | Compile an 'EnsureDirect' operation. The pattern must contain+-- two elements: a memory block and an array. If the input array is+-- already row-major with zero offset, no copy is made. Otherwise,+-- memory is allocated and the array is copied into it.+compileEnsureDirect ::+  (Mem rep inner) => Pat (LetDec rep) -> VName -> ImpM rep r op ()+compileEnsureDirect (Pat [mem_pe, _]) src = do+  src_entry <- lookupArray src+  let src_loc@(MemLoc src_mem src_shape src_lmad) = entryArrayLoc src_entry+      pt = entryArrayElemType src_entry+      row_major_lmad = LMAD.iota 0 (map pe64 src_shape)+      is_row_major = LMAD.dynamicEqualsLMAD src_lmad row_major_lmad+  src_space <- entryMemSpace <$> lookupMemory src_mem+  let dest_mem = patElemName mem_pe+      dest_loc = MemLoc dest_mem src_shape row_major_lmad+  sIf+    is_row_major+    (emit $ Imp.SetMem dest_mem src_mem src_space)+    ( do+        let size = Imp.bytes $ primByteSize pt * product (map pe64 src_shape)+        sAlloc_ dest_mem size src_space+        lmadCopy pt dest_loc src_loc+    )+compileEnsureDirect pat _ =+  error $ "compileEnsureDirect: Invalid pattern: " ++ prettyString pat  -- | The number of bytes needed to represent the array in a -- straightforward contiguous format, as an t'Int64' expression.
src/Futhark/CodeGen/ImpGen/GPU.hs view
@@ -115,6 +115,8 @@   CallKernelGen () opCompiler dest (Alloc e space) =   compileAlloc dest e space+opCompiler dest (EnsureDirect v) =+  compileEnsureDirect dest v opCompiler (Pat [pe]) (Inner (SizeOp (GetSize key size_class))) = do   fname <- askFunction   let key' = keyWithEntryPoint fname key
src/Futhark/CodeGen/ImpGen/Multicore.hs view
@@ -23,6 +23,7 @@  opCompiler :: OpCompiler MCMem HostEnv Imp.Multicore opCompiler dest (Alloc e space) = compileAlloc dest e space+opCompiler dest (EnsureDirect v) = compileEnsureDirect dest v opCompiler dest (Inner op) = compileMCOp dest op  parallelCopy :: CopyCompiler MCMem HostEnv Imp.Multicore
src/Futhark/CodeGen/ImpGen/Sequential.hs view
@@ -19,4 +19,6 @@     ops = ImpGen.defaultOperations opCompiler     opCompiler dest (Alloc e space) =       ImpGen.compileAlloc dest e space+    opCompiler dest (EnsureDirect v) =+      ImpGen.compileEnsureDirect dest v     opCompiler _ (Inner NoOp) = pure ()
src/Futhark/Compiler/Config.hs view
@@ -41,7 +41,9 @@     -- | Additional functions that should be exposed as entry points.     futharkEntryPoints :: [Name],     -- | If false, disable type-checking-    futharkTypeCheck :: Bool+    futharkTypeCheck :: Bool,+    -- | If true, strip provenance from program.+    futharkStripProvenance :: Bool   }  -- | The default compiler configuration.@@ -53,5 +55,6 @@       futharkWerror = False,       futharkSafe = False,       futharkEntryPoints = [],-      futharkTypeCheck = True+      futharkTypeCheck = True,+      futharkStripProvenance = False     }
src/Futhark/IR/GPUMem.hs view
@@ -52,6 +52,7 @@         TC.TypeM GPUMem ()       typeCheckMemoryOp _ (Alloc size _) =         TC.require (Prim int64) size+      typeCheckMemoryOp _ (EnsureDirect _) = pure ()       typeCheckMemoryOp lvl (Inner op) =         typeCheckHostOp (typeCheckMemoryOp . Just) lvl (const $ pure ()) op   checkFParamDec = checkMemInfo
src/Futhark/IR/MCMem.hs view
@@ -43,6 +43,7 @@     where       typeCheckMemoryOp (Alloc size _) =         TC.require (Prim int64) size+      typeCheckMemoryOp (EnsureDirect _) = pure ()       typeCheckMemoryOp (Inner op) =         typeCheckMCOp (const $ pure ()) op   checkFParamDec = checkMemInfo
src/Futhark/IR/Mem.hs view
@@ -184,6 +184,12 @@ data MemOp (inner :: Data.Kind.Type -> Data.Kind.Type) (rep :: Data.Kind.Type)   = -- | Allocate a memory block.     Alloc SubExp Space+  | -- | If the given array has a direct index function (as 'LMAD.isDirect'),+    -- returns the array unchanged. Otherwise, make a copy of the array. The+    -- choice is made dynamically, and the goal is to handle cases where we must+    -- return something that is direct (mostly entry point return types), but we+    -- cannot statically be sure of the layout of some array.+    EnsureDirect VName   | Inner (inner rep)   deriving (Eq, Ord, Show) @@ -193,59 +199,79 @@   OpStmsTraverser m (inner rep) rep ->   OpStmsTraverser m (MemOp inner rep) rep traverseMemOpStms _ _ op@Alloc {} = pure op+traverseMemOpStms _ _ op@EnsureDirect {} = pure op traverseMemOpStms onInner f (Inner inner) = Inner <$> onInner f inner  instance (RephraseOp inner) => RephraseOp (MemOp inner) where   rephraseInOp _ (Alloc e space) = pure (Alloc e space)+  rephraseInOp _ (EnsureDirect v) = pure (EnsureDirect v)   rephraseInOp r (Inner x) = Inner <$> rephraseInOp r x  instance (FreeIn (inner rep)) => FreeIn (MemOp inner rep) where   freeIn' (Alloc size _) = freeIn' size+  freeIn' (EnsureDirect v) = freeIn' v   freeIn' (Inner k) = freeIn' k  instance (TypedOp inner) => TypedOp (MemOp inner) where   opType (Alloc _ space) = pure [Mem space]+  opType (EnsureDirect v) = f <$> lookupType v+    where+      f (Array pt shape _) =+        [Mem DefaultSpace, Array pt (fmap Free shape) NoUniqueness]+      f _ = error $ "EnsureDirect applied to non-array: " ++ show v   opType (Inner k) = opType k  instance (AliasedOp inner) => AliasedOp (MemOp inner) where   opAliases Alloc {} = [mempty]+  -- XXX - why not mem aliases for EnsureDirect?+  opAliases (EnsureDirect v) = [mempty, oneName v]   opAliases (Inner k) = opAliases k    consumedInOp Alloc {} = mempty+  consumedInOp EnsureDirect {} = mempty   consumedInOp (Inner k) = consumedInOp k  instance (CanBeAliased inner) => CanBeAliased (MemOp inner) where   addOpAliases _ (Alloc se space) = Alloc se space+  addOpAliases _ (EnsureDirect v) = EnsureDirect v   addOpAliases aliases (Inner k) = Inner $ addOpAliases aliases k  instance (Rename (inner rep)) => Rename (MemOp inner rep) where   rename (Alloc size space) = Alloc <$> rename size <*> pure space+  rename (EnsureDirect v) = EnsureDirect <$> rename v   rename (Inner k) = Inner <$> rename k  instance (Substitute (inner rep)) => Substitute (MemOp inner rep) where   substituteNames subst (Alloc size space) = Alloc (substituteNames subst size) space+  substituteNames subst (EnsureDirect v) = EnsureDirect (substituteNames subst v)   substituteNames subst (Inner k) = Inner $ substituteNames subst k  instance (PP.Pretty (inner rep)) => PP.Pretty (MemOp inner rep) where   pretty (Alloc e DefaultSpace) = "alloc" <> PP.apply [PP.pretty e]   pretty (Alloc e s) = "alloc" <> PP.apply [PP.pretty e, PP.pretty s]+  pretty (EnsureDirect v) = "ensure_direct" <> PP.apply [PP.pretty v]   pretty (Inner k) = PP.pretty k  instance (OpMetrics (inner rep)) => OpMetrics (MemOp inner rep) where   opMetrics Alloc {} = seen "Alloc"+  opMetrics EnsureDirect {} = seen "EnsureDirect"   opMetrics (Inner k) = opMetrics k  instance (IsOp inner) => IsOp (MemOp inner) where   safeOp (Alloc (Constant (IntValue (Int64Value k))) _) = k >= 0   safeOp Alloc {} = False+  safeOp EnsureDirect {} = True   safeOp (Inner k) = safeOp k   cheapOp (Inner k) = cheapOp k   cheapOp Alloc {} = True+  cheapOp EnsureDirect {} = False   opDependencies (Alloc _ e) = [freeIn e]+  opDependencies (EnsureDirect v) = [mempty, freeIn v]   opDependencies (Inner op) = opDependencies op  instance (CanBeWise inner) => CanBeWise (MemOp inner) where   addOpWisdom (Alloc size space) = Alloc size space+  addOpWisdom (EnsureDirect v) = EnsureDirect v   addOpWisdom (Inner k) = Inner $ addOpWisdom k  instance (ST.IndexOp (inner rep)) => ST.IndexOp (MemOp inner rep) where@@ -1159,6 +1185,18 @@  instance (OpReturns inner) => OpReturns (MemOp inner) where   opReturns (Alloc _ space) = pure [MemMem space]+  opReturns (EnsureDirect v) = do+    space <- lookupMemSpace . fst =<< lookupArraySummary v+    summary <- lookupMemInfo v+    case summary of+      MemArray et shape _ _ ->+        pure+          [ MemMem space,+            MemArray et (fmap Free shape) NoUniqueness . Just $+              ReturnsNewBlock space 0 . LMAD.iota 0 $+                fmap (fmap Free . pe64) (shapeDims shape)+          ]+      _ -> error "EnsureDirect applied to non-array"   opReturns (Inner op) = opReturns op  instance OpReturns NoOp where
src/Futhark/IR/Mem/Simplify.hs view
@@ -13,6 +13,7 @@ import Futhark.Analysis.UsageTable qualified as UT import Futhark.Construct import Futhark.IR.Mem+import Futhark.IR.Mem.LMAD qualified as LMAD import Futhark.IR.Prop.Aliases (AliasedOp) import Futhark.Optimise.Simplify qualified as Simplify import Futhark.Optimise.Simplify.Engine qualified as Engine@@ -112,6 +113,18 @@       Simplify $ attributing attrs $ letBind pat $ Op op decertifySafeAlloc _ _ _ _ = Skip +-- If we know by now that this array is direct, then there is no need for+-- EnsureDirect and we just remove it.+knownDirect :: (SimplifyMemory rep inner) => TopDownRuleOp (Wise rep)+knownDirect _ (Pat [PatElem mem' _, PatElem v' _]) _ (EnsureDirect v) = Simplify $ do+  ~(MemArray _ _ _ (ArrayIn mem v_lmad)) <- lookupMemInfo v+  if LMAD.isDirect v_lmad+    then do+      letBindNames [mem'] $ BasicOp $ SubExp $ Var mem+      letBindNames [v'] $ BasicOp $ SubExp $ Var v+    else cannotSimplify+knownDirect _ _ _ _ = Skip+ -- -- copy(reshape(manifest(v0),s)) can be rewritten to just reshape(manifest(v0),s). --@@ -141,6 +154,7 @@   standardRules     <> ruleBook       [ RuleOp decertifySafeAlloc,-        RuleBasicOp copyManifest+        RuleBasicOp copyManifest,+        RuleOp knownDirect       ]       []
src/Futhark/IR/Parse.hs view
@@ -1132,6 +1132,8 @@     [ keyword "alloc"         *> parens           (Alloc <$> pSubExp <*> choice [pComma *> pSpace, pure DefaultSpace]),+      keyword "ensure_direct"+        *> parens (EnsureDirect <$> pVName),       Inner <$> pInner     ] 
src/Futhark/IR/SeqMem.hs view
@@ -37,6 +37,7 @@  instance TC.Checkable SeqMem where   checkOp (Alloc size _) = TC.require (Prim int64) size+  checkOp (EnsureDirect _) = pure ()   checkOp (Inner NoOp) = pure ()   checkFParamDec = checkMemInfo   checkLParamDec = checkMemInfo
src/Futhark/Internalise.hs view
@@ -85,7 +85,11 @@   maybeLog "Defunctionalising"   prog_decs5 <- Defunctionalise.transformProg prog_decs4   maybeLog "Converting to core IR"-  Exps.transformProg (futharkSafe config) (visibleTypes prog) prog_decs5+  Exps.transformProg+    (futharkSafe config)+    (futharkStripProvenance config)+    (visibleTypes prog)+    prog_decs5   where     verbose = fst (futharkVerbose config) > NotVerbose     maybeLog s
src/Futhark/Internalise/Exps.hs view
@@ -31,10 +31,17 @@  -- | Convert a program in source Futhark to a program in the Futhark -- core language.-transformProg :: (MonadFreshNames m) => Bool -> VisibleTypes -> [E.ValBind] -> m (I.Prog SOACS)-transformProg always_safe types vbinds = do+transformProg ::+  (MonadFreshNames m) =>+  Bool ->+  Bool ->+  VisibleTypes ->+  [E.ValBind] ->+  m (I.Prog SOACS)+transformProg always_safe strip_provenance types vbinds = do   (opaques, consts, funs) <--    runInternaliseM always_safe (internaliseValBinds types vbinds)+    runInternaliseM always_safe strip_provenance $+      internaliseValBinds types vbinds   I.renameProg $ I.Prog opaques consts funs  internaliseValBinds :: VisibleTypes -> [E.ValBind] -> InternaliseM ()
src/Futhark/Internalise/Monad.hs view
@@ -51,7 +51,8 @@     envDoBoundsChecks :: Bool,     envSafe :: Bool,     envAttrs :: Attrs,-    envLoc :: Loc+    envLoc :: Loc,+    envStripProvenance :: Bool   }  data InternaliseState = InternaliseState@@ -102,9 +103,10 @@ runInternaliseM ::   (MonadFreshNames m) =>   Bool ->+  Bool ->   InternaliseM () ->   m (OpaqueTypes, Stms SOACS, [FunDef SOACS])-runInternaliseM safe (InternaliseM m) =+runInternaliseM safe strip (InternaliseM m) =   modifyNameSource $ \src ->     let ((_, consts), s) =           runState (runReaderT (runBuilderT m mempty) newEnv) (newState src)@@ -118,7 +120,8 @@           envDoBoundsChecks = True,           envSafe = safe,           envAttrs = mempty,-          envLoc = mempty+          envLoc = mempty,+          envStripProvenance = strip         }     newState src =       InternaliseState@@ -220,9 +223,11 @@ -- | Attach the provided location to all statements produced during execution of -- this action. locating :: (Located a) => a -> InternaliseM b -> InternaliseM b-locating a-  | loc == mempty || isBuiltinLoc loc = id-  | otherwise = censorStms $ fmap onStm+locating a m+  | loc == mempty || isBuiltinLoc loc = m+  | otherwise = do+      strip <- asks envStripProvenance+      if strip then m else censorStms (fmap onStm) m   where     loc = locOf a     onStm (Let pat aux e) = Let pat (aux {stmAuxLoc = Provenance mempty loc}) e
src/Futhark/Optimise/ArrayShortCircuiting/ArrayCoalescing.hs view
@@ -274,6 +274,7 @@   BotUpEnv ->   ShortCircuitM GPUMem BotUpEnv shortCircuitGPUMem _ _ _ (Alloc _ _) _ bu_env = pure bu_env+shortCircuitGPUMem _ _ _ (EnsureDirect _) _ bu_env = pure bu_env shortCircuitGPUMem lutab pat certs (Inner (GPU.SegOp op)) td_env bu_env =   shortCircuitSegOp isSegThread lutab pat certs op td_env bu_env shortCircuitGPUMem lutab pat certs (Inner (GPU.GPUBody _ body)) td_env bu_env = do@@ -308,6 +309,7 @@   BotUpEnv ->   ShortCircuitM MCMem BotUpEnv shortCircuitMCMem _ _ _ (Alloc _ _) _ bu_env = pure bu_env+shortCircuitMCMem _ _ _ (EnsureDirect _) _ bu_env = pure bu_env shortCircuitMCMem _ _ _ (Inner (MC.OtherOp NoOp)) _ bu_env = pure bu_env shortCircuitMCMem lutab pat certs (Inner (MC.ParOp (Just par_op) op)) td_env bu_env =   shortCircuitSegOp (const True) lutab pat certs par_op td_env bu_env@@ -1738,6 +1740,7 @@ computeScalarTableMemOp ::   ComputeScalarTable rep (inner (Aliases rep)) -> ComputeScalarTable rep (MemOp inner (Aliases rep)) computeScalarTableMemOp _ _ (Alloc _ _) = pure mempty+computeScalarTableMemOp _ _ (EnsureDirect _) = pure mempty computeScalarTableMemOp onInner scope_table (Inner op) = onInner scope_table op  computeScalarTableSegOp ::
src/Futhark/Optimise/CSE.hs view
@@ -324,6 +324,7 @@  instance (CSEInOp (op rep)) => CSEInOp (Memory.MemOp op rep) where   cseInOp o@Memory.Alloc {} = pure o+  cseInOp o@Memory.EnsureDirect {} = pure o   cseInOp (Memory.Inner k) = Memory.Inner <$> subCSE (cseInOp k)  instance
− src/Futhark/Optimise/EntryPointMem.hs
@@ -1,76 +0,0 @@-{-# LANGUAGE TypeFamilies #-}---- | We require that entry points return arrays with zero offset in--- row-major order.  "Futhark.Pass.ExplicitAllocations" is--- conservative and inserts copies to ensure this is the case.  After--- simplification, it may turn out that those copies are redundant.--- This pass removes them.  It's a pretty simple pass, as it only has--- to look at the top level of entry points.-module Futhark.Optimise.EntryPointMem-  ( entryPointMemGPU,-    entryPointMemMC,-    entryPointMemSeq,-  )-where--import Data.List (find)-import Data.Map.Strict qualified as M-import Futhark.IR.GPUMem (GPUMem)-import Futhark.IR.MCMem (MCMem)-import Futhark.IR.Mem-import Futhark.IR.SeqMem (SeqMem)-import Futhark.Pass-import Futhark.Pass.ExplicitAllocations.GPU ()-import Futhark.Transform.Substitute--type Table rep = M.Map VName (Stm rep)--mkTable :: Stms rep -> Table rep-mkTable = foldMap f-  where-    f stm = M.fromList $ map (,stm) (patNames (stmPat stm))--varInfo :: (Mem rep inner) => VName -> Table rep -> Maybe (LetDecMem, Exp rep)-varInfo v table = do-  Let pat _ e <- M.lookup v table-  PatElem _ info <- find ((== v) . patElemName) (patElems pat)-  Just (letDecMem info, e)--optimiseFun :: (Mem rep inner) => Table rep -> FunDef rep -> FunDef rep-optimiseFun consts_table fd =-  fd {funDefBody = onBody $ funDefBody fd}-  where-    table = consts_table <> mkTable (bodyStms (funDefBody fd))-    mkSubst (Var v0)-      | Just (MemArray _ _ _ (ArrayIn mem0 lmad0), BasicOp (Manifest v1 _)) <--          varInfo v0 table,-        Just (MemArray _ _ _ (ArrayIn mem1 lmad1), _) <--          varInfo v1 table,-        lmad0 == lmad1 =-          M.fromList [(mem0, mem1), (v0, v1)]-    mkSubst _ = mempty-    onBody (Body dec stms res) =-      let substs = mconcat $ map (mkSubst . resSubExp) res-       in Body dec stms $ substituteNames substs res--entryPointMem :: (Mem rep inner) => Pass rep rep-entryPointMem =-  Pass-    { passName = "Entry point memory optimisation",-      passDescription = "Remove redundant copies of entry point results.",-      passFunction = intraproceduralTransformationWithConsts pure onFun-    }-  where-    onFun consts fd = pure $ optimiseFun (mkTable consts) fd---- | The pass for GPU representation.-entryPointMemGPU :: Pass GPUMem GPUMem-entryPointMemGPU = entryPointMem---- | The pass for MC representation.-entryPointMemMC :: Pass MCMem MCMem-entryPointMemMC = entryPointMem---- | The pass for Seq representation.-entryPointMemSeq :: Pass SeqMem SeqMem-entryPointMemSeq = entryPointMem
src/Futhark/Optimise/InliningDeadFun.hs view
@@ -331,7 +331,13 @@         onLambda lam =           lam {lambdaBody = onBody for_assert $ lambdaBody lam}     onStm (Let pat aux e) =-      Let pat (traceLocs p aux) $ onExp e+      Let pat aux' $ onExp e+      where+        -- To cut down on clutter, we only propagate attributes to certain+        -- expressions.+        aux' = traceLocs p $ case e of+          BasicOp Manifest {} -> aux {stmAuxAttrs = attrs <> stmAuxAttrs aux}+          _ -> aux      onExp =       mapExp
src/Futhark/Pass/ExpandAllocations.hs view
@@ -896,6 +896,7 @@       Pat <$> mapM (rephrasePatElem (Right . unMem)) pes      unAllocOp Alloc {} = Left "unAllocOp: unhandled Alloc"+    unAllocOp EnsureDirect {} = Left "unAllocOp: unhandled EnsureDirect"     unAllocOp (Inner OtherOp {}) = Left "unAllocOp: unhandled OtherOp"     unAllocOp (Inner GPUBody {}) = Left "unAllocOp: unhandled GPUBody"     unAllocOp (Inner (SizeOp op)) = pure $ SizeOp op
src/Futhark/Pass/ExplicitAllocations.hs view
@@ -182,7 +182,7 @@ repairExpression (BasicOp (Reshape v shape)) = do   v_mem <- fst <$> lookupArraySummary v   space <- lookupMemSpace v_mem-  v' <- snd <$> ensureDirectArray (Just space) v+  v' <- snd <$> allocLinearArray space (baseName v) v   pure $ BasicOp $ Reshape v' shape repairExpression e =   error $ "repairExpression:\n" <> prettyString e@@ -513,7 +513,14 @@   default_space <- askDefaultSpace   if LMAD.isDirect lmad && maybe True (== mem_space) space_ok     then pure (mem, v)-    else needCopy (fromMaybe default_space space_ok)+    else+      if maybe True (== mem_space) space_ok+        then do+          mem' <- newVName $ baseName mem <> "_direct"+          v' <- newVName $ baseName v <> "_v"+          letBindNames [mem', v'] $ Op $ EnsureDirect v+          pure (mem', v')+        else needCopy (fromMaybe default_space space_ok)   where     needCopy space =       -- We need to do a new allocation, copy 'v', and make a new@@ -1080,6 +1087,8 @@   Engine.SimpleM rep (MemOp inner (Engine.Wise rep), Stms (Engine.Wise rep)) simplifyMemOp _ (Alloc size space) =   (,) <$> (Alloc <$> Engine.simplify size <*> pure space) <*> pure mempty+simplifyMemOp _ (EnsureDirect v) =+  (,) <$> (EnsureDirect <$> Engine.simplify v) <*> pure mempty simplifyMemOp onInner (Inner k) = do   (k', hoisted) <- onInner k   pure (Inner k', hoisted)@@ -1123,6 +1132,8 @@     opUsage (Alloc (Var size) _) =       UT.sizeUsage size     opUsage (Alloc _ _) =+      mempty+    opUsage (EnsureDirect _) =       mempty     opUsage (Inner inner) =       innerUsage inner
src/Futhark/Passes.hs view
@@ -22,7 +22,6 @@ import Futhark.Optimise.ArrayShortCircuiting qualified as ArrayShortCircuiting import Futhark.Optimise.CSE import Futhark.Optimise.DoubleBuffer-import Futhark.Optimise.EntryPointMem import Futhark.Optimise.Fusion import Futhark.Optimise.GenRedOpt import Futhark.Optimise.HistAccs@@ -130,7 +129,6 @@     >>> passes       [ performCSE False,         simplifySeqMem,-        entryPointMemSeq,         simplifySeqMem,         LiftAllocations.liftAllocationsSeqMem,         simplifySeqMem,@@ -152,7 +150,6 @@       [ simplifyGPUMem,         performCSE False,         simplifyGPUMem,-        entryPointMemGPU,         doubleBufferGPU,         simplifyGPUMem,         performCSE False,@@ -197,7 +194,6 @@       [ simplifyMCMem,         performCSE False,         simplifyMCMem,-        entryPointMemMC,         doubleBufferMC,         simplifyMCMem,         performCSE False,
src/Futhark/Test.hs view
@@ -2,7 +2,8 @@ -- program is an ordinary Futhark program where an initial comment -- block specifies input- and output-sets. module Futhark.Test-  ( module Futhark.Test.Spec,+  ( module Futhark.Test.Property,+    module Futhark.Test.Spec,     valuesFromByteString,     FutharkExe (..),     getValues,@@ -45,6 +46,7 @@ import Futhark.Script qualified as Script import Futhark.Server import Futhark.Server.Values+import Futhark.Test.Property import Futhark.Test.Spec import Futhark.Test.Values qualified as V import Futhark.Util (ensureCacheDirectory, isEnvVarAtLeast, pmapIO, showText)
+ src/Futhark/Test/Property.hs view
@@ -0,0 +1,1048 @@+{-# LANGUAGE LambdaCase #-}++module Futhark.Test.Property+  ( runPBT,+    PBTConfig (..),+    PBTPhase (..),+    PropSpec (..),+    PBTOutput,+    PBTFailure,+    extractPropSpecs,+  )+where++import Control.Exception+import Control.Monad+import Control.Monad.IO.Class (MonadIO, liftIO)+import Control.Monad.Trans.Except+import Data.Either (fromRight, partitionEithers)+import Data.IORef+import Data.Int+import Data.List qualified as L+import Data.Maybe (catMaybes, fromMaybe, mapMaybe)+import Data.Text qualified as T+import Data.Word (Word64)+import Futhark.Data+import Futhark.Server+import Futhark.Server.Values qualified as FSV+import Futhark.Test.Values+  ( RandomConfiguration (..),+    initialRandomConfiguration,+    randomValue,+  )+import Futhark.Util (showText)+import System.FilePath (dropExtension)+import System.Random (StdGen, mkStdGen, random)+import System.Random.Stateful (IOGenM (..), applyIOGen, newIOGenM)++-- | Configuration for property-based testing.+-- Includes parameters for test case generation, shrinking, and random seed management.+data PBTConfig = PBTConfig+  { -- | Number of test cases to run for each property.+    configNumTests :: Int32,+    -- | Maximum size argument to pass to generators and shrinkers (unless+    -- overridden by PropSpec).+    configMaxSize :: Int64,+    -- | Seed to use for the random number generator (can be overridden by PropSpec).+    configSeed :: Word64,+    -- | Number of shrinking attempts to make on userdefined shrinker before+    -- giving up and reporting the current candidate as the final+    -- counterexample.+    configShrinkTries :: Int+  }+  deriving (Show, Eq)++-- | Specification for a property to be tested, including the property entry point and+-- optional generator and shrinker entry points, as well as an optional size parameter.+data PropSpec = PropSpec+  { -- | The property entry point to test.+    psProp :: T.Text,+    -- | Optional generator entry point to use instead of the default+    -- auto-generator.+    psGen :: Maybe T.Text,+    -- | Optional shrinker entry point to use instead of the default+    -- auto-shrinker.+    psShrink :: Maybe T.Text,+    -- | Optional size argument to pass to the generator and shrinker phases+    -- (overrides 'configMaxSize').+    psSize :: Maybe Int64+  }+  deriving (Show, Eq)++-- | Information about the current phase of property-based testing,+-- used for logging and debugging.+data PBTPhase = PBTPhase+  { -- | Property being tested (same for generator and shrinker phases).+    activeTest :: Maybe EntryName,+    -- | Current entrypoint being called (property, generator, or shrinker).+    phase :: Maybe EntryName,+    -- | Property or generator (only for auto).+    shrinkWith :: Maybe EntryName,+    -- | Size argument for generator and shrinker phases.+    phaseSize :: Maybe Int64,+    -- | Seed argument for generator and shrinker phases.+    phaseSeed :: Maybe Word64,+    -- | Random value argument for shrinker phase (used for user-defined+    -- shrinker, otherwise 'Nothing').+    phaseRandom :: Maybe Word64+  }+  deriving (Show, Eq)++-- | Output of a property-based test run, which is either a failure with+-- an error message or a success.+type PBTOutput = Maybe T.Text++-- | Failure in property-based testing, represented as an error message.+-- For example a division by zero runtime error.+type PBTFailure = T.Text++-- | The Haskell-level random number generator that we use for generating seeds+-- passed to generators.+type PBTGen = IOGenM StdGen++genWord64 :: (MonadIO m) => PBTGen -> m Word64+genWord64 = applyIOGen random++-- | For unexcpected critical errors+unexpectedFailure :: (MonadFail m) => T.Text -> m a+unexpectedFailure msg =+  fail $+    "Unexpected critical error: "+      <> T.unpack msg+      <> "\nProbably a bug please report as issue on the GitHub repository."++lookupArgText :: T.Text -> [T.Text] -> Maybe T.Text+lookupArgText name = lookupArgWith name Just++lookupArgRead :: (Read a) => T.Text -> [T.Text] -> Maybe a+lookupArgRead name = lookupArgWith name readMaybeText++lookupArgWith :: T.Text -> (T.Text -> Maybe a) -> [T.Text] -> Maybe a+lookupArgWith name f = msum . map (stripCall name >=> f)++stripCall :: T.Text -> T.Text -> Maybe T.Text+stripCall name t =+  let s = T.strip t+   in if s == name+        then Just ""+        else T.stripSuffix ")" <=< T.stripPrefix (name <> "(") $ s++readMaybeText :: (Read a) => T.Text -> Maybe a+readMaybeText t =+  case reads (T.unpack t) of+    [(x, "")] -> Just x+    _ -> Nothing++parsePropSpec :: T.Text -> T.Text -> Maybe PropSpec+parsePropSpec entry attr = do+  argsText <- stripCall "prop" attr+  let args = map T.strip $ T.splitOn "," argsText+  pure+    PropSpec+      { psProp = entry,+        psGen = lookupArgText "gen" args,+        psShrink = lookupArgText "shrink" args,+        psSize = fromInteger <$> lookupArgRead "size" args+      }++getPropAttrs :: T.Text -> [T.Text] -> [PropSpec]+getPropAttrs entry = mapMaybe $ parsePropSpec entry++getInputTypes :: Server -> EntryName -> IO [TypeName]+getInputTypes srv entry =+  fmap (map inputType) $+    cmdErrorHandlerE ("Failed to get input types for " <> entry <> ": ") $+      cmdInputs srv entry++getOutputType :: Server -> EntryName -> IO TypeName+getOutputType s entry =+  fmap outputType $+    cmdErrorHandlerE ("Failed to get output types for " <> entry <> ": ") $+      cmdOutput s entry++validateGenTypes :: Server -> EntryName -> Maybe EntryName -> IO (Maybe PBTFailure)+validateGenTypes _srv _prop_name Nothing = pure Nothing+validateGenTypes srv prop_name (Just gen_name) = fmap (either Just (const Nothing)) . runExceptT $ do+  gen_ins <- liftIO $ getInputTypes srv gen_name+  gen_out <- liftIO $ getOutputType srv gen_name++  -- check expected output type for generator matches property input type+  test_ty <-+    liftIO (getSingleInputType srv prop_name) >>= \case+      Left err -> throwE $ showText err+      Right ty -> pure ty++  let actual_tys = gen_ins ++ [gen_out]+      expected_tys = ["i64", "u64", test_ty]++  unless (actual_tys == expected_tys) $+    throwE $+      ("Generator \"" <> gen_name <> "\" for property \"" <> prop_name <> "\" has invalid type.\n")+        <> ("Expected: " <> T.intercalate " -> " expected_tys <> "\n")+        <> ("Actual:   " <> T.intercalate " -> " actual_tys)++validateShrinkTypes :: Server -> EntryName -> EntryName -> IO (Maybe PBTFailure)+validateShrinkTypes srv propName shrinkName = fmap (either Just (const Nothing)) . runExceptT $ do+  propTy <-+    liftIO (getSingleInputType srv propName) >>= \case+      Left err -> throwE $ showText err+      Right ty -> pure ty++  shrinkIns <- liftIO $ getInputTypes srv shrinkName++  -- validate input+  case shrinkIns of+    [xTy, randTy] -> do+      let errors =+            [ "Property " <> propName <> " expects " <> propTy <> " but shrinker " <> shrinkName <> " takes " <> xTy+            | xTy /= propTy+            ]+              <> [ "Shrinker " <> shrinkName <> " takes random value " <> randTy <> " but expected u64"+                 | randTy /= "u64"+                 ]++      unless (null errors) $+        throwE $+          "Shrinker Mismatch:\n" <> T.intercalate "\n---\n" errors+    tys ->+      throwE $+        "Shrinker input arity mismatch.\n shrinker "+          <> shrinkName+          <> " inputs: "+          <> showText tys+          <> "\nExpected exactly 2 inputs: ("+          <> propTy+          <> ", u64)."++  -- validate output+  shrinkOut <- liftIO $ getOutputType srv shrinkName+  let isMatch = propTy == shrinkOut++  unless isMatch $+    throwE $+      "Shrinker output mismatch.\nProperty "+        <> propName+        <> " expects: "+        <> propTy+        <> "\nShrinker "+        <> shrinkName+        <> " returns: "+        <> showText shrinkOut+        <> "\nExpected shrinker output to equal the property input type."++validatePropTypes :: Server -> EntryName -> IO (Maybe PBTFailure)+validatePropTypes srv propName = fmap (either Just (const Nothing)) . runExceptT $ do+  ins <- liftIO $ getInputTypes srv propName+  case ins of+    [_] -> pure ()+    [] -> throwE $ "Property " <> propName <> " has no inputs: expected 1."+    _ -> throwE $ "Property " <> propName <> " has " <> showText (length ins) <> " inputs; expected 1."++  out <- liftIO $ getOutputType srv propName+  case out of+    "bool" -> pure ()+    ty -> throwE $ "Property " <> propName <> " output must be bool, got: " <> ty++validateOneSpec :: Server -> [EntryName] -> PropSpec -> ExceptT PBTFailure IO ()+validateOneSpec srv eps spec = do+  let prop = psProp spec++  unless (prop `elem` eps) $+    throwE $+      "Property entry point not found: " <> prop++  liftIO (validatePropTypes srv prop) >>= maybe (pure ()) throwE++  genName <- case psGen spec of+    Nothing ->+      pure Nothing+    Just g+      | g `notElem` eps ->+          throwE $ "Generator is not a server entry point: " <> g+    Just g ->+      pure $ Just g++  liftIO (validateGenTypes srv prop genName) >>= maybe (pure ()) throwE++  case psShrink spec of+    Nothing -> pure ()+    Just sh -> do+      unless (sh `elem` eps) $+        throwE $+          "Shrinker is not a server entry point: " <> sh+      liftIO (validateShrinkTypes srv prop sh) >>= maybe (pure ()) throwE++-- | Extract property specifications from the server by looking for entry+-- points with #[prop(...)] attributes, comparing with the declared list of properties.+extractPropSpecs :: Server -> [EntryName] -> IO (Either PBTFailure [PropSpec])+extractPropSpecs srv properties = do+  eps <- either (error . show) pure <=< liftIO $ cmdEntryPoints srv+  checks <- mapM (runExceptT . getOne eps) eps+  let missing = do+        f <- properties+        guard $ f `L.notElem` eps+        pure $ Left $ "Declared as property, but is not an entry point: \"" <> f <> "\"."+  case partitionEithers $ checks ++ missing of+    ([], specs) -> pure $ Right $ catMaybes specs+    (errors, _) -> pure $ Left $ T.intercalate "\n" errors+  where+    getOne eps entry = do+      attrs <-+        either (unexpectedFailure . showText) pure <=< liftIO $+          cmdAttributes srv entry+      let specs = getPropAttrs entry attrs+          is_prop = entry `elem` properties+      case specs of+        [spec] | is_prop -> do+          validateOneSpec srv eps spec+          pure $ Just spec+        []+          | is_prop ->+              throwE $+                "Entry point \""+                  <> entry+                  <> "\" declared as property, but has no #[prop(...)] attribute."+          | otherwise ->+              pure Nothing+        _+          | is_prop ->+              throwE $+                "Entry point \""+                  <> entry+                  <> "\" has more than one #[prop(...)] attribute."+          | otherwise ->+              throwE $+                "Entry point \""+                  <> entry+                  <> "\" not declared as property, but has #[prop(...)] attribute."++-- | Generate a candidate automatically.+automaticGenerator :: Server -> EntryName -> TypeName -> Int64 -> PBTGen -> IO (Maybe PBTFailure)+automaticGenerator srv candidate genTy size rng = do+  kRes <- cmdErrorHandlerE "automaticGenerator cmdKind failed: " $ cmdKind srv genTy+  case kRes of+    Record -> do+      resFields <- cmdFields srv genTy+      case resFields of+        Right fields -> do+          let fieldVarNames = [candidate <> "_$compositeVal" <> fieldName fld | fld <- fields]++          results <- forM (zip fieldVarNames fields) $ \(fVarName, fld) ->+            automaticGenerator srv fVarName (fieldType fld) size rng++          case sequence results of+            Just err -> pure $ Just $ T.unlines err+            Nothing -> do+              freeVars srv [candidate]+              cmdErrorHandlerM ("Failed to pack record " <> candidate <> ": ") $+                cmdNew srv candidate genTy fieldVarNames++              freeVars srv fieldVarNames+              pure Nothing+        Left err -> pure $ Just $ showText err+    Array -> do+      (dimCount, baseTy) <- getArrayDimsAndBase srv genTy+      baseKind <- cmdErrorHandlerE "automaticGenerator base cmdKind failed: " $ cmdKind srv baseTy+      case baseKind of+        Record -> do+          resFields <- cmdFields srv baseTy+          case resFields of+            Right fields -> do+              let fieldVarNames = [candidate <> "_$compositeArr_" <> fieldName fld | fld <- fields]++              results <- forM (zip fieldVarNames fields) $ \(fVarName, fld) -> do+                (innerDimCount, innerBaseTy) <- getArrayDimsAndBase srv (fieldType fld)+                let totalDimCount = dimCount + innerDimCount+                    fArrTy = T.replicate totalDimCount "[]" <> innerBaseTy+                automaticGenerator srv fVarName fArrTy size rng++              case sequence results of+                Just err -> pure $ Just $ T.unlines err+                Nothing -> do+                  freeVars srv [candidate]+                  cmdErrorHandlerM ("Failed to zip array of records " <> candidate <> ": ") $+                    cmdZip srv candidate genTy fieldVarNames++                  freeVars srv fieldVarNames+                  pure Nothing+            Left err -> pure $ Just $ showText err+        _ -> do+          let shapeList = replicate dimCount size+          seed <- genWord64 rng+          case makeFutPrimitiveValue baseTy shapeList seed of+            Right val -> do+              freeVars srv [candidate]+              putRes <- FSV.putValue srv candidate val+              case putRes of+                Nothing -> pure Nothing+                Just err -> pure $ Just $ showText err+            Left err -> pure $ Just err+    _ -> do+      seed <- genWord64 rng+      case makeFutPrimitiveValue genTy [] seed of+        Right val -> do+          freeVars srv [candidate]+          putRes <- FSV.putValue srv candidate val+          case putRes of+            Nothing -> pure Nothing+            Just err -> pure $ Just $ showText err+        Left _ -> do+          let genName = "gen_" <> genTy+              szVar = candidate <> "_$size"+              sdVar = candidate <> "_$seed"++          putVal srv szVar size+          putVal srv sdVar seed++          callFreeIns srv genName candidate [szVar, sdVar]++-- | Recursively unwrap arrays using the Futhark server to handle type aliases dynamically.+getArrayDimsAndBase :: Server -> TypeName -> IO (Int, TypeName)+getArrayDimsAndBase srv t+  | "[]" `T.isPrefixOf` t = do+      (d, base) <- getArrayDimsAndBase srv (T.drop 2 t)+      pure (d + 1, base)+  | otherwise = do+      kRes <- cmdKind srv t+      case kRes of+        Right Array -> do+          etRes <- cmdElemtype srv t+          case etRes of+            Right et -> do+              (d, base) <- getArrayDimsAndBase srv et+              pure (d + 1, base)+            Left _ -> pure (0, t) -- Fallback if server fails to resolve elemtype+        _ -> pure (0, t)++makeFutPrimitiveValue :: TypeName -> [Int64] -> Word64 -> Either PBTFailure Value+makeFutPrimitiveValue ty shape seed =+  case ty of+    "i8" -> Right $ randomValue cfg (ValueType shape' I8) seed+    "i16" -> Right $ randomValue cfg (ValueType shape' I16) seed+    "i32" -> Right $ randomValue cfg (ValueType shape' I32) seed+    "i64" -> Right $ randomValue cfg (ValueType shape' I64) seed+    "u8" -> Right $ randomValue cfg (ValueType shape' U8) seed+    "u16" -> Right $ randomValue cfg (ValueType shape' U16) seed+    "u32" -> Right $ randomValue cfg (ValueType shape' U32) seed+    "u64" -> Right $ randomValue cfg (ValueType shape' U64) seed+    "f16" -> Right $ randomValue cfg (ValueType shape' F16) seed+    "f32" -> Right $ randomValue cfg (ValueType shape' F32) seed+    "f64" -> Right $ randomValue cfg (ValueType shape' F64) seed+    "bool" -> Right $ randomValue cfg (ValueType shape' Bool) seed+    _ -> Left ("Automatic generation not implemented for: " <> ty)+  where+    shape' = map fromIntegral shape+    cfg = initialRandomConfiguration {f32Range = (-1, 1)}++runOne :: PropSpec -> PBTConfig -> Server -> IORef PBTPhase -> FilePath -> IO (Either PBTFailure PBTOutput)+runOne s config srv entryNameRef program = runExceptT $ do+  rng <- newIOGenM $ mkStdGen $ fromIntegral $ configSeed config+  let loop i+        | i >= numTests = pure Nothing+        | otherwise = check (i + 1)+      check i = do+        seed <- genWord64 rng+        let runUpdate ph =+              liftIO $+                updatePhase+                  (Just propName)+                  (Just ph)+                  Nothing+                  (Just size)+                  Nothing+                  Nothing+                  entryNameRef++        generatorCandidateM <- liftIO $ generatorPhase seed+        maybe (pure ()) throwE generatorCandidateM++        runUpdate propName++        okE <-+          liftIO $ withCallKeepIns srv propName serverOk [serverIn] $ getVal srv+        ok <- case okE of+          Right b -> pure b+          Left err -> do+            liftIO $+              cmdErrorHandlerM "cmdStore failed to store when property crashed" $+                cmdStore srv propertyFileName [serverIn]+            valuePPrint <- liftIO pPrintPhase+            throwE $+              "Property "+                <> propName+                <> " failed with candidate="+                <> valuePPrint+                <> " with error: "+                <> err+        if ok+          then loop i+          else do+            let failmsg =+                  "PBT FAIL: "+                    <> propName+                    <> " size="+                    <> showText size+                    <> " seed="+                    <> showText (configSeed config)+                    <> " after "+                    <> showText i+                    <> " tests\n"++            shrinkRes <- case psShrink s of+              Nothing ->+                liftIO $+                  autoShrinkLoop+                    srv+                    propName+                    genName+                    serverIn+                    size+                    seed+                    serverSize+                    serverSeed+                    entryNameRef+              Just sh -> do+                userShrinkRes <-+                  liftIO $+                    shrinkLoop+                      srv+                      propName+                      serverIn+                      sh+                      rng+                      (configShrinkTries config)+                      entryNameRef++                case userShrinkRes of+                  Right Nothing ->+                    pure (Right Nothing)+                  Right (Just err) -> do+                    autoRes <-+                      liftIO $+                        autoShrinkLoop+                          srv+                          propName+                          genName+                          serverIn+                          size+                          seed+                          serverSize+                          serverSeed+                          entryNameRef++                    pure $+                      Right $+                        Just $+                          "User shrinker failed: "+                            <> err+                            <> "\nAttempted auto-shrinker fallback."+                            <> formatAutoShrinkResult autoRes+                  Left err -> do+                    autoRes <-+                      liftIO $+                        autoShrinkLoop+                          srv+                          propName+                          genName+                          serverIn+                          size+                          seed+                          serverSize+                          serverSeed+                          entryNameRef++                    pure $+                      Right $+                        Just $+                          "User shrinker failed: "+                            <> err+                            <> "\nAttempted auto-shrinker fallback."+                            <> formatAutoShrinkResult autoRes++            case shrinkRes of+              Left err -> do+                runUpdate "prettyPrint"+                counterLog <- liftIO pPrintPhase+                liftIO $ cmdErrorHandlerM "cmdStore failed to store when shrinker crashed" $ cmdStore srv propertyFileName [serverIn]+                pure $+                  Just $+                    failmsg+                      <> "Shrinking failed: "+                      <> err+                      <> "\nCounterexample: "+                      <> counterLog+              Right (Just note) -> do+                runUpdate "prettyPrint"+                counterLog <- liftIO pPrintPhase+                pure $+                  Just $+                    failmsg+                      <> "Shrinking note: "+                      <> note+                      <> "\nCounterexample: "+                      <> counterLog+              Right Nothing -> do+                runUpdate "prettyPrint"+                counterLog <- liftIO pPrintPhase+                liftIO $+                  cmdErrorHandlerM "cmdStore failed to store shrinker result" $+                    cmdStore srv propertyFileName [serverIn]+                pure $ Just $ failmsg <> "Counterexample: " <> counterLog+  loop 0+  where+    propName = psProp s+    genName = psGen s+    size = fromMaybe (configMaxSize config) (psSize s)+    numTests = configNumTests config+    serverSize = "runPBT_size"+    serverSeed = "runPBT_seed"+    serverIn = "runPBT_input"+    serverOk = "runPBT_ok"+    propertyFileName =+      dropExtension program <> "_" <> T.unpack propName <> ".counterexample"++    generatorPhase seed = do+      let runUpdate ph =+            liftIO $+              updatePhase+                (Just propName)+                (Just ph)+                Nothing+                (Just size)+                (Just seed)+                Nothing+                entryNameRef+      case genName of+        Nothing -> fmap (either Just (const Nothing)) . runExceptT $ do+          liftIO $ freeVars srv [serverIn]+          propType <-+            liftIO (getSingleInputType srv propName) >>= \case+              Left err -> throwE $ showText err+              Right ty -> pure ty++          rng <- newIOGenM $ mkStdGen $ fromIntegral seed+          errM <- liftIO $ automaticGenerator srv serverIn propType size rng+          maybe (pure ()) (throwE . ("Automatic generator failed: " <>)) errM+        Just gn -> fmap (either Just (const Nothing)) . runExceptT $ do+          runUpdate "User Generator"+          liftIO $ putVal srv serverSize size+          liftIO $ putVal srv serverSeed seed++          let genOut = outName gn++          ExceptT $ withFreedVars srv [genOut] $ runExceptT $ do+            liftIO (callFreeIns srv gn genOut [serverSize, serverSeed]) >>= \case+              Nothing -> pure ()+              Just err -> do+                liftIO $ putVal srv serverSize size >> putVal srv serverSeed seed+                liftIO $+                  cmdErrorHandlerM "cmdStore failed to store generator error: " $+                    cmdStore srv propertyFileName [serverSize, serverSeed]+                liftIO $ freeVars srv [serverSize, serverSeed]+                throwE $+                  "User Generator "+                    <> gn+                    <> " failed with size="+                    <> showText size+                    <> " and seed="+                    <> showText seed+                    <> " with error: "+                    <> err++            liftIO $ renameVar srv serverIn genOut++    pPrintPhase = do+      inputTypes <- getInputTypes srv propName+      case inputTypes of+        [] -> pure "Could not retrieve input type for counterexample."+        ty0 : _ -> prettyVar srv serverIn ty0++formatAutoShrinkResult :: Either PBTFailure PBTOutput -> T.Text+formatAutoShrinkResult autoRes =+  case autoRes of+    Right Nothing ->+      "\nAuto-shrinker fallback completed."+    Right (Just msg) ->+      "\nAuto-shrinker fallback completed with note: " <> msg+    Left autoErr ->+      "\nAuto-shrinker fallback also failed: " <> autoErr++updatePhase ::+  Maybe EntryName ->+  Maybe EntryName ->+  Maybe EntryName ->+  Maybe Int64 ->+  Maybe Word64 ->+  Maybe Word64 ->+  IORef PBTPhase ->+  IO ()+updatePhase propName phase activeTest size seed rand phaseRef =+  writeIORef phaseRef $+    PBTPhase+      { activeTest = propName,+        phase = phase,+        shrinkWith = activeTest,+        phaseSize = size,+        phaseSeed = seed,+        phaseRandom = rand+      }++-- Given a known counterexample (generated with provided size and seed), here we+-- try to find a smaller counterexample by decreasing the size (but using the+-- same seed) until the generated value stops being a counterexample.+--+-- XXX: currently the automatic generator does not reuse the seed, but creates a+-- new PBTGen from it.+autoShrinkLoop ::+  Server ->+  EntryName ->+  Maybe EntryName ->+  VarName ->+  Int64 ->+  Word64 ->+  VarName ->+  VarName ->+  IORef PBTPhase ->+  IO (Either PBTFailure PBTOutput)+autoShrinkLoop srv propName genName vCounterExample size seed serverSize serverSeed phaseRef = runExceptT $ do+  let loop i+        | i <= 1 = pure Nothing+        | otherwise = do+            let newSize = i - 1++            errM <- liftIO $ generatorPhase newSize+            maybe (pure ()) (throwE . ("Auto-shrinker generator failed: " <>)) errM++            liftIO $ autoShrinkUpdatePhase (Right $ Just propName)++            ok <-+              either (throwE . ("Property " <>)) pure <=< liftIO $+                withCallKeepIns srv propName vOk [vCandidate] $+                  getVal srv++            liftIO $ autoShrinkUpdatePhase (Left Nothing)++            case ok of+              True -> do+                liftIO $ freeVars srv [vCandidate]+                loop newSize+              False -> do+                liftIO $+                  freeOnException srv [vCounterExample] $+                    renameVar srv vCounterExample vCandidate+                loop newSize+  loop size+  where+    vCandidate = "auto_shrink_candidate"+    vOk = "auto_shrink_ok"+    autoShrinkUpdatePhase active =+      liftIO $+        updatePhase+          (Just propName)+          (Just "autoShrinkLoop")+          (fromRight (Just "Automatic generator") active)+          (Just size)+          (Just seed)+          Nothing+          phaseRef+    generatorPhase size' = do+      fmap (either Just (const Nothing)) . runExceptT $+        case genName of+          Nothing -> do+            propertyType <- do+              liftIO (getSingleInputType srv propName) >>= \case+                Left err -> throwE $ showText err+                Right ty -> pure ty+            liftIO $ freeVars srv [serverSize, serverSeed]+            runExceptT $ do+              rng <- newIOGenM $ mkStdGen $ fromIntegral seed+              errM <- liftIO $ automaticGenerator srv vCandidate propertyType size' rng+              maybe (pure ()) (throwE . ("Automatic generator failed: " <>)) errM+          Just gn -> do+            liftIO $ putVal srv serverSize size' >> putVal srv serverSeed seed+            runExceptT $ do+              errM <- liftIO $ callFreeIns srv gn vCandidate [serverSize, serverSeed]+              maybe (pure ()) (\err -> throwE $ "User Generator " <> gn <> " failed: " <> err) errM++data Step+  = -- | Property still failed with the new candidate+    AcceptedShrink+  | -- | Property passed with the new candidate+    NotAcceptedShrink+  | -- | Shrinker error (including property failure in shrinker)+    ErrorInShrink T.Text+  deriving (Eq, Show)++shrinkLoop :: Server -> EntryName -> VarName -> EntryName -> PBTGen -> Int -> IORef PBTPhase -> IO (Either PBTFailure PBTOutput)+shrinkLoop srv propName counterExample shrinkName rng numTries phaseRef = runExceptT $ do+  -- 1. Setup Phase+  oldRef <- liftIO $ readIORef phaseRef+  let size = fromMaybe 0 (phaseSize oldRef)+      shrinkUpdatePhase activeTest =+        liftIO $+          updatePhase+            (Just propName)+            (Just shrinkName)+            activeTest+            (Just size)+            Nothing+            Nothing+            phaseRef++  shrinkUpdatePhase Nothing++  let loop (acc :: Int) (totalCounter :: Int)+        | acc >= numTries = pure Nothing+        | otherwise = do+            random_value <- genWord64 rng+            stepResultE <- liftIO $ oneStep size random_value+            stepResult <-+              either+                ( \err ->+                    throwE $+                      "Error in shrinker "+                        <> shrinkName+                        <> " with random="+                        <> showText random_value+                        <> ": "+                        <> err+                )+                pure+                stepResultE++            case stepResult of+              AcceptedShrink ->+                loop 0 (totalCounter + 1) -- Reset trials on success+              NotAcceptedShrink ->+                loop (acc + 1) (totalCounter + 1) -- Increment trials+              ErrorInShrink err ->+                throwE $ "Error in shrinker: " <> err+  loop 0 0+  where+    oneStep size (val :: Word64) = do+      let vCandidate = "shrink_candidate"+          vOk = "shrink_ok"+          vRandomValue = "shrink_random"++      let shrinkUpdatePhase activeTest randomNum =+            updatePhase+              (Just propName)+              (Just shrinkName)+              activeTest+              (Just size)+              Nothing+              randomNum+              phaseRef++      freeVars srv [vRandomValue]+      putVal srv vRandomValue val++      shrinkUpdatePhase Nothing $ Just val++      withFreedVar srv vCandidate $ runExceptT $ do+        errE <- liftIO $ callKeepIns srv shrinkName vCandidate [counterExample, vRandomValue]+        liftIO $ freeVars srv [vRandomValue]+        maybe (pure ()) (throwE . ((shrinkName <> " has ") <>)) errE++        liftIO $ shrinkUpdatePhase Nothing $ Just $ fromIntegral val++        ok <-+          either (throwE . ("Property " <>)) pure <=< liftIO $+            withCallKeepIns srv propName vOk [vCandidate] $+              getVal srv++        liftIO $ shrinkUpdatePhase Nothing $ Just $ fromIntegral val++        case ok of+          True -> pure NotAcceptedShrink+          False -> do+            liftIO $ renameVar srv counterExample vCandidate+            pure AcceptedShrink++-- | Name of out-variable for this entry point.+outName :: EntryName -> VarName+outName = (<> "_out")++putVal :: (PutValue1 a) => Server -> T.Text -> a -> IO ()+putVal s name x = do+  let v = putValue1 x+  cmdErrorHandlerM ("putValue failed for " <> name <> ": ") $ FSV.putValue s name v++freeVars :: Server -> [VarName] -> IO ()+freeVars s vs = do+  mFail <- cmdFree s vs+  case mFail of+    Nothing -> pure ()+    Just err+      | any (T.isPrefixOf "Unknown variable:") (failureMsg err) -> pure ()+      | otherwise ->+          unexpectedFailure $+            "cmdFree failed for "+              <> showText vs+              <> ": "+              <> showText (failureMsg err)++callFreeIns :: Server -> EntryName -> VarName -> [VarName] -> IO (Maybe PBTFailure)+callFreeIns s entry out ins = do+  freeVars s [out]+  r <- cmdCall s entry out ins+  freeVars s ins+  either (pure . handleRuntimeError entry) (const $ pure Nothing) r++isRuntimeError :: CmdFailure -> Bool+isRuntimeError failure = any ("runtime: " `T.isPrefixOf`) (failureLog failure)++handleRuntimeError :: EntryName -> CmdFailure -> Maybe PBTFailure+handleRuntimeError entry err+  | isRuntimeError err = Just $ "Runtime error: " <> showText (failureMsg err)+  | otherwise =+      unexpectedFailure $+        "Fatal Error on "+          <> entry+          <> ": "+          <> showText (failureMsg err)++callKeepIns :: Server -> EntryName -> VarName -> [VarName] -> IO (Maybe PBTFailure)+callKeepIns s entry out ins = do+  freeVars s [out]+  r <- cmdCall s entry out ins+  either (pure . handleRuntimeError entry) (const $ pure Nothing) r++freeOnException :: Server -> [VarName] -> IO a -> IO a+freeOnException srv vs action =+  action `onException` freeVars srv vs++withCallKeepIns :: Server -> EntryName -> VarName -> [VarName] -> (VarName -> IO a) -> IO (Either PBTFailure a)+withCallKeepIns srv entry out ins k = do+  errM <- callKeepIns srv entry out ins+  maybe+    (Right <$> (k out `finally` freeVars srv [out]))+    (pure . Left . ((entry <> " has ") <>))+    errM++withFreedVars :: Server -> [VarName] -> IO a -> IO a+withFreedVars srv vs action =+  action `finally` freeVars srv vs++-- | Bracket a single temporary var name.+withFreedVar :: Server -> VarName -> IO a -> IO a+withFreedVar srv v = withFreedVars srv [v]++renameVar :: Server -> VarName -> VarName -> IO ()+renameVar srv new old = do+  freeVars srv [new]+  cmdErrorHandlerM "cmdRename failed: " $ cmdRename srv old new++cmdErrorHandlerM :: T.Text -> IO (Maybe CmdFailure) -> IO ()+cmdErrorHandlerM msg action = action >>= maybe (pure ()) (unexpectedFailure . format)+  where+    format err = msg <> showText err++cmdErrorHandlerE :: T.Text -> IO (Either CmdFailure a) -> IO a+cmdErrorHandlerE msg action = action >>= either (unexpectedFailure . format) pure+  where+    format err = msg <> showText err++getVal :: (GetValue a) => Server -> VarName -> IO a+getVal srv name = do+  v <- getDataVal srv name+  case getValue v of+    Just b -> pure b+    Nothing ->+      unexpectedFailure $+        "Expected "+          <> name+          <> " to decode, got: "+          <> valueText v++getDataVal :: Server -> VarName -> IO Value+getDataVal s name = do+  r <- FSV.getValue s name+  case r of+    Left msg ->+      unexpectedFailure $+        "getValue failed for "+          <> name+          <> ": "+          <> msg+    Right v -> pure v++prettyVar :: Server -> VarName -> TypeName -> IO T.Text+prettyVar srv v ty = do+  kRes <- cmdErrorHandlerE "cmdKind failed: " $ cmdKind srv ty+  case kRes of+    Record -> do+      fieldsRes <- cmdFields srv ty+      case fieldsRes of+        Right fieldLines -> do+          let fnames = map fieldName fieldLines+              ftypes = map fieldType fieldLines+              isTuple = all (\(n, i :: Int) -> n == showText i) (zip fnames [0 ..])++          rendered <- forM (zip fnames ftypes) $ \(fname, fty) -> do+            let tmp = v <> "_proj_" <> fname+            sField <- withFreedVar srv tmp $ do+              cmdErrorHandlerM "project failed: " $ cmdProject srv tmp v fname+              prettyVar srv tmp fty+            pure $ if isTuple then sField else fname <> " = " <> sField++          pure $+            if isTuple+              then "(" <> T.intercalate ", " rendered <> ")"+              else "{" <> T.intercalate ", " rendered <> "}"+        Left _ -> pure "<error: record fields missing>"+    Array -> do+      valRes <- FSV.getValue srv v+      case valRes of+        Right val -> pure (valueText val)+        Left _ -> do+          dims <- cmdErrorHandlerE "cmdShape failed: " $ cmdShape srv v+          baseTy <- getBaseType ty+          buildNested v baseTy dims []+    _ -> fallbackValue+  where+    fallbackValue = do+      valRes <- FSV.getValue srv v+      case valRes of+        Right val -> pure (valueText val)+        Left _ -> pure ("<opaque:" <> ty <> ">")++    getBaseType :: TypeName -> IO TypeName+    getBaseType t = do+      k <- cmdErrorHandlerE "cmdKind failed: " $ cmdKind srv t+      case k of+        Array -> do+          et <- cmdErrorHandlerE "cmdElemtype failed: " $ cmdElemtype srv t+          getBaseType et+        _ -> pure t++    buildNested :: VarName -> TypeName -> [Int] -> [Int] -> IO T.Text+    buildNested varName baseType dims currentPath =+      case dims of+        [] -> do+          let pathStr = T.intercalate "_" (map showText currentPath)+              tmpElem = varName <> "_elem_" <> pathStr++          withFreedVar srv tmpElem $ do+            cmdErrorHandlerM "index failed: " $ cmdIndex srv tmpElem varName currentPath+            prettyVar srv tmpElem baseType+        (d : restDims) -> do+          elements <- forM [0 .. d - 1] $ \idx -> do+            buildNested varName baseType restDims (currentPath ++ [idx])++          pure $ "[" <> T.intercalate ", " elements <> "]"++getSingleInputType :: Server -> EntryName -> IO (Either PBTFailure TypeName)+getSingleInputType srv ep = do+  tys <- getInputTypes srv ep+  case tys of+    [ty] -> pure $ Right ty+    [] -> pure $ Left $ T.pack $ "Entrypoint " <> T.unpack ep <> " has no inputs (expected 1)."+    _ -> pure $ Left $ T.pack $ "Entrypoint " <> T.unpack ep <> " has >1 input (expected 1): " <> show tys++-- | Run a list of property specifications, returning a list of results.+-- Each result is either a failure with an error message or a success.+runPBT :: PBTConfig -> Server -> [PropSpec] -> IORef PBTPhase -> FilePath -> IO [Either PBTFailure PBTOutput]+runPBT config srv specs entryNameRef program =+  forM specs $ \spec ->+    runOne spec config srv entryNameRef program
src/Futhark/Test/Spec.hs view
@@ -13,6 +13,7 @@     TestAction (..),     ExpectedError (..),     InputOutputs (..),+    PropertyCase (..),     TestRun (..),     ExpectedResult (..),     Success (..),@@ -26,6 +27,7 @@ import Control.Exception (catch) import Control.Monad import Data.Char+import Data.Either (partitionEithers) import Data.Functor import Data.List qualified as L import Data.Map.Strict qualified as M@@ -62,7 +64,7 @@ -- | How to test a program. data TestAction   = CompileTimeFailure ExpectedError-  | RunCases [InputOutputs] [StructureTest] [WarningTest]+  | RunCases [InputOutputs] [StructureTest] [WarningTest] [PropertyCase]   deriving (Show)  -- | Input and output pairs for some entry point(s).@@ -72,6 +74,10 @@   }   deriving (Show) +newtype PropertyCase = PropertyCase+  {propertyEntryPoint :: T.Text}+  deriving (Show)+ -- | The error expected for a negative test. data ExpectedError   = AnyError@@ -217,12 +223,33 @@ parseAction sep =   choice     [ CompileTimeFailure <$> (lexstr' "error:" *> parseExpectedError sep),+      try parseAsProperty,+      parseAsRunCase+    ]+  where+    parseAsProperty = do+      props <- parseProperty sep+      pure $ RunCases [] [] [] props++    parseAsRunCase =       RunCases         <$> parseInputOutputs sep         <*> many (parseExpectedStructure sep)         <*> many (parseWarning sep)-    ]+        <*> pure [] +parseProperty :: Parser () -> Parser [PropertyCase]+parseProperty sep = do+  entryss <- some (parseEntryPointsProp sep)+  pure $ map PropertyCase (concat entryss)++parseEntryPointsProp :: Parser () -> Parser [T.Text]+parseEntryPointsProp sep =+  lexeme' "property:" *> some entry <* sep+  where+    constituent c = not (isSpace c)+    entry = lexeme' $ takeWhile1P Nothing constituent+ parseInputOutputs :: Parser () -> Parser [InputOutputs] parseInputOutputs sep = do   entrys <- parseEntryPoints sep@@ -382,9 +409,19 @@     optional ("--" *> sep *> testSpec sep) <* pEndOfTestBlock <* many pNonTestLine   case maybe_spec of     Just spec-      | RunCases old_cases structures warnings <- testAction spec -> do-          cases <- many $ pInputOutputs <* many pNonTestLine-          pure spec {testAction = RunCases (old_cases ++ concat cases) structures warnings}+      | RunCases old_cases structures warnings old_properties <- testAction spec -> do+          let pAnyBlock = (Left <$> pInputOutputs) <|> (Right <$> pPropertyCases)+          restBlocks <- many (pAnyBlock <* many pNonTestLine)+          let (restCases, restProperties) = partitionEithers restBlocks+          pure+            spec+              { testAction =+                  RunCases+                    (old_cases ++ concat restCases)+                    structures+                    warnings+                    (old_properties ++ concat restProperties)+              }       | otherwise ->           many pNonTestLine             *> notFollowedBy "-- =="@@ -396,20 +433,23 @@     sep = void $ hspace *> optional (try $ eol *> "--" *> sep)      noTest =-      ProgramTest mempty mempty (RunCases mempty mempty mempty)+      ProgramTest mempty mempty (RunCases mempty mempty mempty mempty)      pEndOfTestBlock =       (void eol <|> eof) *> notFollowedBy "--"     pNonTestLine =       void $ notFollowedBy "-- ==" *> restOfLine     pInputOutputs =-      "--" *> sep *> parseDescription sep *> parseInputOutputs sep <* pEndOfTestBlock+      try $+        "--" *> sep *> parseDescription sep *> parseInputOutputs sep <* pEndOfTestBlock+    pPropertyCases =+      "--" *> sep *> parseDescription sep *> parseProperty sep <* pEndOfTestBlock  validate :: FilePath -> ProgramTest -> Either String ProgramTest validate path pt = do   case testAction pt of     CompileTimeFailure {} -> pure pt-    RunCases ios _ _ -> do+    RunCases ios _ _ _ -> do       mapM_ (noDups . map runDescription . iosTestRuns) ios       Right pt   where
src/Futhark/Test/Values.hs view
@@ -11,16 +11,30 @@     CompoundValue,     mkCompound,     unCompound,++    -- * Random value generation+    Range,+    RandomConfiguration (..),+    initialRandomConfiguration,+    randomValue,   ) where +import Control.Monad.ST+import Data.Int import Data.Map qualified as M import Data.Text qualified as T import Data.Traversable+import Data.Vector.Storable qualified as SVec+import Data.Vector.Storable.Mutable qualified as USVec+import Data.Word import Futhark.Data import Futhark.Data.Compare import Futhark.Data.Reader-import Futhark.Util.Pretty+import Futhark.Util (convFloat)+import Futhark.Util.Pretty (Pretty (..), braces, commasep, equals, parens)+import Numeric.Half+import System.Random.Stateful (UniformRange (..), mkStdGen, uniformR)  instance Pretty Value where   pretty = pretty . valueText@@ -70,3 +84,84 @@ -- supported by raw values.  You cannot parse or read these in -- standard ways, and they cannot be elements of arrays. type CompoundValue = Compound Value++randomVector ::+  (SVec.Storable v, UniformRange v) =>+  Range v ->+  (SVec.Vector Int -> SVec.Vector v -> Value) ->+  [Int] ->+  Word64 ->+  Value+randomVector range final ds seed = runST $ do+  -- Use some nice impure computation where we can preallocate a+  -- vector of the desired size, populate it via the random number+  -- generator, and then finally reutrn a frozen binary vector.+  arr <- USVec.new n+  let fill g i+        | i < n = do+            let (v, g') = uniformR range g+            USVec.write arr i v+            g' `seq` fill g' $! i + 1+        | otherwise =+            pure ()+  fill (mkStdGen $ fromIntegral seed) 0+  final (SVec.fromList ds) . SVec.convert <$> SVec.freeze arr+  where+    n = product ds++-- XXX: The following instance is an orphan.  Maybe it could be+-- avoided with some newtype trickery or refactoring, but it's so+-- convenient this way.+instance UniformRange Half where+  uniformRM (a, b) g =+    (convFloat :: Float -> Half) <$> uniformRM (convFloat a, convFloat b) g++-- | Closed interval, as in @System.Random@.+type Range a = (a, a)++data RandomConfiguration = RandomConfiguration+  { i8Range :: Range Int8,+    i16Range :: Range Int16,+    i32Range :: Range Int32,+    i64Range :: Range Int64,+    u8Range :: Range Word8,+    u16Range :: Range Word16,+    u32Range :: Range Word32,+    u64Range :: Range Word64,+    f16Range :: Range Half,+    f32Range :: Range Float,+    f64Range :: Range Double+  }++initialRandomConfiguration :: RandomConfiguration+initialRandomConfiguration =+  RandomConfiguration+    (minBound, maxBound)+    (minBound, maxBound)+    (minBound, maxBound)+    (minBound, maxBound)+    (minBound, maxBound)+    (minBound, maxBound)+    (minBound, maxBound)+    (minBound, maxBound)+    (0.0, 1.0)+    (0.0, 1.0)+    (0.0, 1.0)++randomValue :: RandomConfiguration -> ValueType -> Word64 -> Value+randomValue conf (ValueType ds t) seed =+  case t of+    I8 -> gen i8Range I8Value+    I16 -> gen i16Range I16Value+    I32 -> gen i32Range I32Value+    I64 -> gen i64Range I64Value+    U8 -> gen u8Range U8Value+    U16 -> gen u16Range U16Value+    U32 -> gen u32Range U32Value+    U64 -> gen u64Range U64Value+    F16 -> gen f16Range F16Value+    F32 -> gen f32Range F32Value+    F64 -> gen f64Range F64Value+    Bool -> gen (const (False, True)) BoolValue+  where+    gen range final = randomVector (range conf) final ds seed
src/Futhark/Util.hs view
@@ -31,6 +31,7 @@     showText,     unixEnvironment,     isEnvVarAtLeast,+    randomSeed,     startupTime,     fancyTerminal,     hFancyTerminal,@@ -81,6 +82,7 @@ import Data.Text.IO qualified as T import Data.Time.Clock (UTCTime, getCurrentTime) import Data.Tuple (swap)+import Data.Word (Word64) import Debug.Trace import Numeric import System.Directory (createDirectoryIfMissing, listDirectory)@@ -94,6 +96,7 @@ import System.IO.Error (isAlreadyInUseError, isDoesNotExistError) import System.IO.Unsafe import System.Process.ByteString+import System.Random (randomIO) import Text.Read (readMaybe)  -- | Like @nub@, but without the quadratic runtime.@@ -249,6 +252,13 @@   case readMaybe =<< lookup s unixEnvironment of     Just y -> y >= x     _ -> False++{-# NOINLINE randomSeed #-}++-- | A random number generated at startup. Can be used to produce different+-- behaviour whenever the program is run.+randomSeed :: Word64+randomSeed = unsafePerformIO randomIO  {-# NOINLINE startupTime #-} 
src/Language/Futhark/Interpreter.hs view
@@ -985,11 +985,9 @@ eval env (Hole (Info t) loc) =   bad loc env $ "Hole of type: " <> prettyTextOneLine t eval env (Parens e _) = eval env e-eval env (QualParens (qv, _) e loc) = do-  m <- evalModuleVar env qv-  case m of-    ModuleFun {} -> error $ "Local open of module function at " ++ locStr loc-    Module m' -> eval (m' <> env) e+eval env (QualParens _ e _) =+  -- Already handled by the names added by the type checker.+  eval env e eval env (TupLit vs _) = toTuple <$> mapM (eval env) vs eval env (RecordLit fields _) =   ValueRecord . M.fromList <$> mapM evalField fields
src/Language/Futhark/Prop.hs view
@@ -54,6 +54,7 @@     orderZero,     unfoldFunType,     foldFunType,+    typeQualVars,     typeVars,     isAccType, @@ -553,20 +554,24 @@       [] -> retDims (unInfo (valBindRetType vb))       _ -> [] --- | The type names mentioned in a type.-typeVars :: TypeBase dim as -> S.Set VName-typeVars t =+-- | The qualified type names mentioned in a type.+typeQualVars :: TypeBase dim as -> [QualName VName]+typeQualVars t =   case t of     Scalar Prim {} -> mempty     Scalar (TypeVar _ tn targs) ->-      mconcat $ S.singleton (qualLeaf tn) : map typeArgFree targs-    Scalar (Arrow _ _ _ t1 (RetType _ t2)) -> typeVars t1 <> typeVars t2-    Scalar (Record fields) -> foldMap typeVars fields-    Scalar (Sum cs) -> mconcat $ (foldMap . fmap) typeVars cs-    Array _ _ rt -> typeVars $ Scalar rt+      tn : concatMap typeArgFree targs+    Scalar (Arrow _ _ _ t1 (RetType _ t2)) -> typeQualVars t1 <> typeQualVars t2+    Scalar (Record fields) -> foldMap typeQualVars fields+    Scalar (Sum cs) -> mconcat $ (foldMap . fmap) typeQualVars cs+    Array _ _ rt -> typeQualVars $ Scalar rt   where-    typeArgFree (TypeArgType ta) = typeVars ta+    typeArgFree (TypeArgType ta) = typeQualVars ta     typeArgFree TypeArgDim {} = mempty++-- | The type names mentioned in a type.+typeVars :: TypeBase dim as -> S.Set VName+typeVars = S.fromList . map qualLeaf . typeQualVars  -- | @orderZero t@ is 'True' if the argument type has order 0, i.e., it is not -- a function type, does not contain a function type as a subcomponent, and may
src/Language/Futhark/TypeChecker.hs view
@@ -37,6 +37,9 @@ import Language.Futhark.TypeChecker.Types import Prelude hiding (abs, mod) +importTable :: Imports -> ImportTable+importTable = M.map (\f -> (fileAbs f, fileEnv f)) . M.fromList+ --- The main checker  -- | Type check a program containing no type information, yielding@@ -53,7 +56,7 @@ checkProg files src name prog =   runTypeM initialEnv files' name src $ checkProgM prog   where-    files' = M.map fileEnv $ M.fromList files+    files' = importTable files  -- | Type check a single expression containing no type information, -- yielding either a type error or the same expression annotated with@@ -75,7 +78,7 @@       src       (checkOneExp =<< resolveExp e)   where-    files' = M.map fileEnv $ M.fromList files+    files' = importTable files  -- | Type check a single declaration containing no type information, -- yielding either a type error or the same declaration annotated with@@ -91,12 +94,12 @@ checkDec files src env name d =   second (fmap massage) $     runTypeM env files' name src $ do-      (_, env', d') <- checkOneDec d+      (env', d') <- checkOneDec d       pure (env' <> env, d')   where     massage ((env', d'), src') =       (env', d', src')-    files' = M.map fileEnv $ M.fromList files+    files' = importTable files  -- | Type check a single module expression containing no type information, -- yielding either a type error or the same expression annotated with@@ -109,11 +112,10 @@   ModExpBase NoInfo Name ->   (Warnings, Either TypeError (MTy, ModExpBase Info VName)) checkModExp files src env me =-  second (fmap fst) . runTypeM env files' (mkInitialImport "") src $ do-    (_abs, mty, me') <- checkOneModExp me-    pure (mty, me')+  second (fmap fst) . runTypeM env files' (mkInitialImport "") src $+    checkOneModExp me   where-    files' = M.map fileEnv $ M.fromList files+    files' = importTable files  -- | An initial environment for the type checker, containing -- intrinsics and such.@@ -150,7 +152,7 @@ checkProgM :: UncheckedProg -> TypeM FileModule checkProgM (Prog doc decs) = do   checkForDuplicateDecs decs-  (abs, env, decs', full_env) <- checkDecs decs+  ((env, decs', full_env), abs) <- collectTySet $ checkDecs decs   pure (FileModule abs env (Prog doc decs') full_env)  dupDefinitionError ::@@ -283,7 +285,7 @@         TypeSpec l name' ps' doc loc : specs'       ) checkSpecs (ModSpec name sig doc loc : specs) = do-  (_sig_abs, mty, sig') <- checkModTypeExp sig+  (mty, sig') <- checkModTypeExp sig   bindSpaced1 Term name loc $ \name' -> do     usedName name'     let senv =@@ -298,13 +300,13 @@         ModSpec name' sig' doc loc : specs'       ) checkSpecs (IncludeSpec e loc : specs) = do-  (e_abs, env_abs, e_env, e') <- checkModTypeExpToEnv e+  (env_abs, e_env, e') <- checkModTypeExpToEnv e    mapM_ warnIfShadowing $ M.keys env_abs    (abstypes, env, specs') <- localEnv e_env $ checkSpecs specs   pure-    ( e_abs <> env_abs <> abstypes,+    ( env_abs <> abstypes,       env <> e_env,       IncludeSpec e' loc : specs'     )@@ -315,28 +317,28 @@     warnAbout qn =       warn loc $ "Inclusion shadows type" <+> dquotes (pretty qn) <> "." -checkModTypeExp :: ModTypeExpBase NoInfo Name -> TypeM (TySet, MTy, ModTypeExpBase Info VName)+checkModTypeExp :: ModTypeExpBase NoInfo Name -> TypeM (MTy, ModTypeExpBase Info VName) checkModTypeExp (ModTypeParens e loc) = do-  (abs, mty, e') <- checkModTypeExp e-  pure (abs, mty, ModTypeParens e' loc)+  (mty, e') <- checkModTypeExp e+  pure (mty, ModTypeParens e' loc) checkModTypeExp (ModTypeVar name NoInfo loc) = do   (name', mty) <- lookupMTy loc name   (mty', substs) <- newNamesForMTy mty-  pure (mtyAbs mty', mty', ModTypeVar name' (Info substs) loc)+  pure (mty', ModTypeVar name' (Info substs) loc) checkModTypeExp (ModTypeSpecs specs loc) = do   checkForDuplicateSpecs specs-  (abstypes, env, specs') <- checkSpecs specs-  pure (abstypes, MTy abstypes $ ModEnv env, ModTypeSpecs specs' loc)+  (abs, env, specs') <- checkSpecs specs+  pure (MTy abs $ ModEnv env, ModTypeSpecs specs' loc) checkModTypeExp (ModTypeWith s (TypeRef tname ps te trloc) loc) = do-  (abs, s_abs, s_env, s') <- checkModTypeExpToEnv s+  (s_abs, s_env, s') <- checkModTypeExpToEnv s   resolveTypeParams ps $ \ps' -> do     (ext, te', te_t, _) <- bindingTypeParams ps' $ checkTypeDecl te     (tname', s_abs', s_env') <-       refineEnv loc s_abs s_env tname ps' $ RetType ext te_t-    pure (abs, MTy s_abs' $ ModEnv s_env', ModTypeWith s' (TypeRef tname' ps' te' trloc) loc)+    pure (MTy s_abs' $ ModEnv s_env', ModTypeWith s' (TypeRef tname' ps' te' trloc) loc) checkModTypeExp (ModTypeArrow maybe_pname e1 e2 loc) = do-  (e1_abs, MTy s_abs e1_mod, e1') <- checkModTypeExp e1-  (maybe_pname', (e2_abs, e2_mod, e2')) <-+  (MTy s_abs e1_mod, e1') <- checkModTypeExp e1+  (maybe_pname', (e2_mod, e2')) <-     case maybe_pname of       Just pname -> bindSpaced1 Term pname loc $ \pname' ->         localEnv (mempty {envModTable = M.singleton pname' e1_mod}) $@@ -344,29 +346,28 @@       Nothing ->         (Nothing,) <$> checkModTypeExp e2   pure-    ( e1_abs <> e2_abs,-      MTy mempty $ ModFun $ FunModType s_abs e1_mod e2_mod,+    ( MTy mempty $ ModFun $ FunModType s_abs e1_mod e2_mod,       ModTypeArrow maybe_pname' e1' e2' loc     )  checkModTypeExpToEnv ::   ModTypeExpBase NoInfo Name ->-  TypeM (TySet, TySet, Env, ModTypeExpBase Info VName)+  TypeM (TySet, Env, ModTypeExpBase Info VName) checkModTypeExpToEnv e = do-  (abs, MTy mod_abs mod, e') <- checkModTypeExp e+  (MTy mod_abs mod, e') <- checkModTypeExp e   case mod of-    ModEnv env -> pure (abs, mod_abs, env, e')+    ModEnv env -> pure (mod_abs, env, e')     ModFun {} -> unappliedFunctor $ srclocOf e -checkModTypeBind :: ModTypeBindBase NoInfo Name -> TypeM (TySet, Env, ModTypeBindBase Info VName)+checkModTypeBind :: ModTypeBindBase NoInfo Name -> TypeM (Env, ModTypeBindBase Info VName) checkModTypeBind (ModTypeBind name e doc loc) = do-  (abs, env, e') <- checkModTypeExp e+  (mty, e') <- checkModTypeExp e+  addTySet $ mtyAbs mty   bindSpaced1 Signature name loc $ \name' -> do     usedName name'     pure-      ( abs,-        mempty-          { envModTypeTable = M.singleton name' env,+      ( mempty+          { envModTypeTable = M.singleton name' mty,             envNameMap = M.singleton (Signature, name) (qualName name')           },         ModTypeBind name' e' doc loc@@ -374,16 +375,15 @@  checkOneModExp ::   ModExpBase NoInfo Name ->-  TypeM (TySet, MTy, ModExpBase Info VName)+  TypeM (MTy, ModExpBase Info VName) checkOneModExp (ModParens e loc) = do-  (abs, mty, e') <- checkOneModExp e-  pure (abs, mty, ModParens e' loc)+  (mty, e') <- checkOneModExp e+  pure (mty, ModParens e' loc) checkOneModExp (ModDecs decs loc) = do   checkForDuplicateDecs decs-  (abstypes, env, decs', _) <- checkDecs decs+  ((env, decs', _), abstypes) <- collectTySet $ checkDecs decs   pure-    ( abstypes,-      MTy abstypes $ ModEnv env,+    ( MTy abstypes $ ModEnv env,       ModDecs decs' loc     ) checkOneModExp (ModVar v loc) = do@@ -393,47 +393,46 @@         && isIntrinsic (qualLeaf v')     )     $ typeError loc mempty "The 'intrinsics' module may not be used in module expressions."-  pure (mempty, MTy mempty env, ModVar v' loc)+  pure (MTy mempty env, ModVar v' loc) checkOneModExp (ModImport name NoInfo loc) = do   (name', env) <- lookupImport loc name   pure-    ( mempty,-      MTy mempty $ ModEnv env,+    ( MTy mempty $ ModEnv env,       ModImport name (Info name') loc     ) checkOneModExp (ModApply f e NoInfo NoInfo loc) = do-  (f_abs, f_mty, f') <- checkOneModExp f+  (f_mty, f') <- checkOneModExp f   case mtyMod f_mty of     ModFun functor -> do-      (e_abs, e_mty, e') <- checkOneModExp e+      (e_mty, e') <- checkOneModExp e       (mty, psubsts, rsubsts) <- applyFunctor (locOf loc) functor e_mty       pure-        ( mtyAbs mty <> f_abs <> e_abs,-          mty,+        ( mty,           ModApply f' e' (Info psubsts) (Info rsubsts) loc         )     _ ->       typeError loc mempty "Cannot apply non-parametric module." checkOneModExp (ModAscript me se NoInfo loc) = do-  (me_abs, me_mod, me') <- checkOneModExp me-  (se_abs, se_mty, se') <- checkModTypeExp se+  (me_mod, me') <- checkOneModExp me+  (se_mty, se') <- checkModTypeExp se+  addTySet $ mtyAbs se_mty   match_subst <- badOnLeft $ matchMTys me_mod se_mty (locOf loc)-  pure (se_abs <> me_abs, se_mty, ModAscript me' se' (Info match_subst) loc)+  pure (se_mty, ModAscript me' se' (Info match_subst) loc) checkOneModExp (ModLambda param maybe_fsig_e body_e loc) =   withModParam param $ \param' param_abs param_mod -> do-    (abs, maybe_fsig_e', body_e', mty) <-+    (maybe_fsig_e', body_e', mty) <-       checkModBody (fst <$> maybe_fsig_e) body_e loc     pure-      ( abs,-        MTy mempty $ ModFun $ FunModType param_abs param_mod mty,+      ( MTy mempty $ ModFun $ FunModType param_abs param_mod mty,         ModLambda param' maybe_fsig_e' body_e' loc       ) -checkOneModExpToEnv :: ModExpBase NoInfo Name -> TypeM (TySet, Env, ModExpBase Info VName)+checkOneModExpToEnv :: ModExpBase NoInfo Name -> TypeM (Env, ModExpBase Info VName) checkOneModExpToEnv e = do-  (e_abs, MTy abs mod, e') <- checkOneModExp e+  (MTy abs mod, e') <- checkOneModExp e+  addTySet abs   case mod of-    ModEnv env -> pure (e_abs <> abs, env, e')+    ModEnv env -> pure (env, e')     ModFun {} -> unappliedFunctor $ srclocOf e  withModParam ::@@ -441,7 +440,7 @@   (ModParamBase Info VName -> TySet -> Mod -> TypeM a) ->   TypeM a withModParam (ModParam pname psig_e NoInfo loc) m = do-  (_abs, MTy p_abs p_mod, psig_e') <- checkModTypeExp psig_e+  (MTy p_abs p_mod, psig_e') <- checkModTypeExp psig_e   bindSpaced1 Term pname loc $ \pname' -> do     let in_body_env = mempty {envModTable = M.singleton pname' p_mod}     localEnv in_body_env $@@ -461,54 +460,50 @@   ModExpBase NoInfo Name ->   SrcLoc ->   TypeM-    ( TySet,-      Maybe (ModTypeExp, Info (M.Map VName VName)),+    ( Maybe (ModTypeExp, Info (M.Map VName VName)),       ModExp,       MTy     ) checkModBody maybe_fsig_e body_e loc = enteringModule $ do-  (body_e_abs, body_mty, body_e') <- checkOneModExp body_e+  (body_mty, body_e') <- checkOneModExp body_e   case maybe_fsig_e of     Nothing ->       pure-        ( mtyAbs body_mty <> body_e_abs,-          Nothing,+        ( Nothing,           body_e',           body_mty         )     Just fsig_e -> do-      (fsig_abs, fsig_mty, fsig_e') <- checkModTypeExp fsig_e+      (fsig_mty, fsig_e') <- checkModTypeExp fsig_e+      addTySet $ mtyAbs fsig_mty       fsig_subst <- badOnLeft $ matchMTys body_mty fsig_mty (locOf loc)       pure-        ( fsig_abs <> body_e_abs,-          Just (fsig_e', Info fsig_subst),+        ( Just (fsig_e', Info fsig_subst),           body_e',           fsig_mty         ) -checkModBind :: ModBindBase NoInfo Name -> TypeM (TySet, Env, ModBindBase Info VName)+checkModBind :: ModBindBase NoInfo Name -> TypeM (Env, ModBindBase Info VName) checkModBind (ModBind name [] maybe_fsig_e e doc loc) = do-  (e_abs, maybe_fsig_e', e', mty) <- checkModBody (fst <$> maybe_fsig_e) e loc+  (maybe_fsig_e', e', mty) <- checkModBody (fst <$> maybe_fsig_e) e loc   bindSpaced1 Term name loc $ \name' -> do     usedName name'     pure-      ( e_abs,-        mempty+      ( mempty           { envModTable = M.singleton name' $ mtyMod mty,             envNameMap = M.singleton (Term, name) $ qualName name'           },         ModBind name' [] maybe_fsig_e' e' doc loc       ) checkModBind (ModBind name (p : ps) maybe_fsig_e body_e doc loc) = do-  (abs, params', maybe_fsig_e', body_e', funsig) <-+  (params', maybe_fsig_e', body_e', funsig) <-     withModParam p $ \p' p_abs p_mod ->       withModParams ps $ \params_stuff -> do         let (ps', ps_abs, ps_mod) = unzip3 params_stuff-        (abs, maybe_fsig_e', body_e', mty) <- checkModBody (fst <$> maybe_fsig_e) body_e loc+        (maybe_fsig_e', body_e', mty) <- checkModBody (fst <$> maybe_fsig_e) body_e loc         let addParam (x, y) mty' = MTy mempty $ ModFun $ FunModType x y mty'         pure-          ( abs,-            p' : ps',+          ( p' : ps',             maybe_fsig_e',             body_e',             FunModType p_abs p_mod $ foldr addParam mty $ zip ps_abs ps_mod@@ -516,8 +511,7 @@   bindSpaced1 Term name loc $ \name' -> do     usedName name'     pure-      ( abs,-        mempty+      ( mempty           { envModTable =               M.singleton name' $ ModFun funsig,             envNameMap =@@ -633,6 +627,14 @@     onRetType te t =       ([], EntryType t te) +-- | Check that a type is non-functional, looking up the liftedness of abstract+-- types in the environment. This works because entry points cannot be polymorphic, so any remaining type names must be abstract.+orderZeroM :: TypeBase dim u -> TypeM Bool+orderZeroM t = do+  (orderZero t &&) . and <$> mapM isUnlifted (typeQualVars t)+  where+    isUnlifted qv = (< Lifted) <$> lookupAbsTy qv+ checkEntryPoint ::   SrcLoc ->   [TypeParam] ->@@ -645,12 +647,6 @@         withIndexLink           "polymorphic-entry"           "Entry point functions may not be polymorphic."-  | not (all orderZero param_ts)-      || not (orderZero rettype') =-      typeError loc mempty $-        withIndexLink-          "higher-order-entry"-          "Entry point functions may not be higher-order."   | sizes_only_in_ret <-       S.fromList (map typeParamName tparams)         `S.intersection` fvVars (freeInType rettype')@@ -666,8 +662,14 @@         "Entry point size parameter "           <> pretty p           <> " only used non-constructively."-  | otherwise =-      pure ()+  | otherwise = do+      param_ts_order_zero <- mapM orderZeroM param_ts+      ret_order_zero <- orderZeroM rettype'+      when (not (and param_ts_order_zero) || not ret_order_zero) $+        typeError loc mempty $+          withIndexLink+            "higher-order-entry"+            "Entry point functions may not be higher-order."   where     (RetType _ rettype_t) = rettype     (rettype_params, rettype') = unfoldFunType rettype_t@@ -704,39 +706,38 @@       vb'     ) -checkOneDec :: DecBase NoInfo Name -> TypeM (TySet, Env, DecBase Info VName)+checkOneDec :: DecBase NoInfo Name -> TypeM (Env, DecBase Info VName) checkOneDec (ModDec struct) = do-  (abs, modenv, struct') <- checkModBind struct-  pure (abs, modenv, ModDec struct')+  (modenv, struct') <- checkModBind struct+  pure (modenv, ModDec struct') checkOneDec (ModTypeDec sig) = do-  (abs, sigenv, sig') <- checkModTypeBind sig-  pure (abs, sigenv, ModTypeDec sig')+  (sigenv, sig') <- checkModTypeBind sig+  pure (sigenv, ModTypeDec sig') checkOneDec (TypeDec tdec) = do   (tenv, tdec') <- checkTypeBind tdec-  pure (mempty, tenv, TypeDec tdec')+  pure (tenv, TypeDec tdec') checkOneDec (OpenDec x loc) = do-  (x_abs, x_env, x') <- checkOneModExpToEnv x-  pure (x_abs, x_env, OpenDec x' loc)+  (x_env, x') <- checkOneModExpToEnv x+  pure (x_env, OpenDec x' loc) checkOneDec (LocalDec d loc) = do-  (abstypes, env, d') <- checkOneDec d-  pure (abstypes, env, LocalDec d' loc)+  (env, d') <- checkOneDec d+  pure (env, LocalDec d' loc) checkOneDec (ImportDec name NoInfo loc) = do   (name', env) <- lookupImport loc name   when (isBuiltin name) $     typeError loc mempty $       pretty name <+> "may not be explicitly imported."-  pure (mempty, env, ImportDec name (Info name') loc)+  pure (env, ImportDec name (Info name') loc) checkOneDec (ValDec vb) = do   (env, vb') <- checkValBind vb-  pure (mempty, env, ValDec vb')+  pure (env, ValDec vb') -checkDecs :: [DecBase NoInfo Name] -> TypeM (TySet, Env, [DecBase Info VName], Env)+checkDecs :: [DecBase NoInfo Name] -> TypeM (Env, [DecBase Info VName], Env) checkDecs (d : ds) = do-  (d_abstypes, d_env, d') <- checkOneDec d-  (ds_abstypes, ds_env, ds', full_env) <- localEnv d_env $ checkDecs ds+  (d_env, d') <- checkOneDec d+  (ds_env, ds', full_env) <- localEnv d_env $ checkDecs ds   pure-    ( d_abstypes <> ds_abstypes,-      case d' of+    ( case d' of         LocalDec {} -> ds_env         ImportDec {} -> ds_env         _ -> ds_env <> d_env,@@ -745,4 +746,4 @@     ) checkDecs [] = do   full_env <- askEnv-  pure (mempty, mempty, [], full_env)+  pure (mempty, [], full_env)
src/Language/Futhark/TypeChecker/Modules.hs view
@@ -89,8 +89,9 @@     pure (v, v')   let substs = M.fromList pairs       rev_substs = M.fromList $ map (uncurry $ flip (,)) pairs--  pure (substituteInMTy substs orig_mty, rev_substs)+      new_mty = substituteInMTy substs orig_mty+  addTySet $ mtyAbs new_mty+  pure (new_mty, rev_substs)   where     substituteInMTy :: M.Map VName VName -> MTy -> MTy     substituteInMTy substs (MTy mty_abs mty_mod) =
src/Language/Futhark/TypeChecker/Monad.hs view
@@ -14,6 +14,7 @@     lookupMTy,     lookupImport,     lookupMod,+    lookupAbsTy,     localEnv,     TypeError (..),     prettyTypeError,@@ -26,6 +27,8 @@     aNote,     MonadTypeChecker (..),     TypeState (stateNameSource),+    addTySet,+    collectTySet,     usedName,     checkName,     checkAttr,@@ -76,7 +79,7 @@ import Language.Futhark.Traversals import Language.Futhark.Warnings import Paths_futhark qualified-import Prelude hiding (mapM, mod)+import Prelude hiding (abs, mapM, mod)  newtype Note = Note (Doc ()) @@ -159,7 +162,7 @@  -- | A mapping from import import names to 'Env's.  This is used to -- resolve @import@ declarations.-type ImportTable = M.Map ImportName Env+type ImportTable = M.Map ImportName (TySet, Env)  data Context = Context   { contextEnv :: Env,@@ -175,6 +178,8 @@     stateWarnings :: Warnings,     -- | Which names have been used.     stateUsed :: S.Set VName,+    -- | Known abstract type names.+    stateTySet :: TySet,     stateCounter :: Int   } @@ -216,7 +221,7 @@   (Warnings, Either TypeError (a, VNameSource)) runTypeM env imports fpath src (TypeM m) = do   let ctx = Context env imports fpath True-      s = TypeState src mempty mempty 0+      s = TypeState src mempty mempty mempty 0   case runExcept $ runStateT (runReaderT m ctx) s of     Left (ws, e) -> (ws, Left e)     Right (x, s') -> (stateWarnings s', Right (x, stateNameSource s'))@@ -246,6 +251,33 @@   where     explode = unknownVariable Signature qn loc +-- | Add set of abstract types.+addTySet :: TySet -> TypeM ()+addTySet tys = modify $ \s -> s {stateTySet = tys <> stateTySet s}++-- | Run type checking command while accumulating (and returning) all new+-- abstract types, then reset to known abstract types afterwards.+collectTySet :: TypeM a -> TypeM (a, TySet)+collectTySet m = do+  old <- gets stateTySet+  x <- m+  new <- gets stateTySet+  modify $ \s -> s {stateTySet = old}+  pure (x, new `M.difference` old)++-- | Look up the liftedness of an abstract type.+lookupAbsTy :: QualName VName -> TypeM Liftedness+lookupAbsTy v = do+  abs <- gets stateTySet+  case M.lookup v abs of+    Just l -> pure l+    Nothing ->+      error $+        unlines+          [ "lookupAbsTy: " <> prettyString v,+            "known: " <> show abs+          ]+ -- | Look up an import. lookupImport :: SrcLoc -> FilePath -> TypeM (ImportName, Env) lookupImport loc file = do@@ -259,7 +291,9 @@           <+> dquotes (pretty (includeToText canonical_import))           </> "Known:"           <+> commasep (map (pretty . includeToText) (M.keys imports))-    Just scope -> pure (canonical_import, scope)+    Just (abs, scope) -> do+      addTySet abs+      pure (canonical_import, scope)  -- | Evaluate a 'TypeM' computation within an extended (/not/ -- replaced) environment.