Mr-Andersen

{-# OPTIONS --overlapping-instances #-}

module Pointer where

open import Prelude

-- Allowes retrieving data by valid pointer
data Heap : Set
private variable h : Heap

Mr-Andersen

-- Works (no `List` at all) ------------------------------------------------------
data Layers2 : Nat -> Type -> Type where
    Leaf2 : t -> Layers2 lvl t
    Node2 : Layers2 (S lvl) t -> Layers2 (S lvl) t -> Layers2 lvl t

total
mapLayers2 : (a -> b) -> Layers2 lvl a -> Layers2 lvl b
mapLayers2 f (Leaf2 x)          = Leaf2 (f x)
mapLayers2 f (Node2 left right) = Node2 (mapLayers2 f left) (mapLayers2 f right)

Mr-Andersen

typedef struct {
    float mass;
    float rx;
    float ry;
    float vx;
    float vy;
} Particle_t;

__kernel void time_to_collision(
    __global Particle_t parts[PART_NUM],

Mr-Andersen

#include <iostream>


// get_type<i, Ts...>::type -> Ts[i] (Compile error of i >= length(Ts))
template<size_t i, typename T, typename... Ts>
struct get_type {
    typedef typename get_type<i - 1, Ts...>::type type;
};

template<typename T, typename... Ts>