jasigal

The trick

The following code implements a Bird-style traversal replaceMin which traverses a tree exactly once to produce a new tree of the same shape with the leaves replaced with the minimum of all leaf values in the original tree.

import System.IO (fixIO)

data Tree a = Leaf a | Branch (Tree a) (Tree a)

jasigal

module EffectsAreContainers where

open import Level
open import Data.Fin
open import Data.Unit
open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.Nat
open import Function

jasigal

pub module approx-recip

import smooth

fun approx-recip(iters : int, x : a) : <smooth<a>,div> a {
  var acc := c(1.0)
  var prev := c(1.0)
  repeat(iters) {
    prev := (prev *. (~.)(x -. c(1.0)))
    acc := (acc +. prev)

jasigal

module Main where

import           Data.Array.Accelerate             as A
import           Data.Array.Accelerate.LLVM.Native

g :: Scalar Double -> Scalar Double
g = (runN (A.map f :: Acc (Scalar Double) -> Acc (Scalar Double)))
  where
    f x = let y = recip x
              b = (-y) * y