lovely-error

{-# OPTIONS --type-in-type #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Agda.Builtin.List

data Void : Set where

lovely-error

pub fn main() !void {

    const AbstractedObject = Opaque(&.{
        .{"f1", fn (*anyopaque) u1},
        .{"f2", fn (*anyopaque, u8, u8, u8, u8) L},
        .{"ferry", fn (*anyopaque)error{boo}!void},
    });

    var a = std.heap.ArenaAllocator.init(std.heap.page_allocator);
    var T = K {};

lovely-error

const std = @import("std");

pub const @"1KiB of bytes": comptime_int = 1024;
pub const @"1MiB of bytes": comptime_int = 1024 * 1024;
pub const @"1GiB of bytes": comptime_int = 1 << 30;
pub const @"Byte amount fitting within 48 bit address space": comptime_int = (1 << 48) - 1;

pub fn Ptr(comptime Pointee: type, comptime is_mutable: bool) type {
    const Ty = if (is_mutable) *Pointee else *const Pointee;
    return struct {

lovely-error

-- basically this in wolfram alpha terms
-- 2*(Integrate[sin\(40)x\(41),{x,0,Divide[pi,4]}]+Integrate[sin\(40)x\(41),{x,Divide[pi,4],Divide[pi,2]}])

-- https://www.desmos.com/calculator/1fokxfyphz
-- https://www.wolframalpha.com/input?i2d=true&i=Integrate%5Bsin%5C%2840%29x%5C%2841%29%2C%7Bx%2C0%2Cpi%7D%5D
-- https://www.wolframalpha.com/input?i2d=true&i=2*%5C%2840%29Integrate%5Bsin%5C%2840%29x%5C%2841%29%2C%7Bx%2C0%2CDivide%5Bpi%2C4%5D%7D%5D%2BIntegrate%5Bsin%5C%2840%29x%5C%2841%29%2C%7Bx%2CDivide%5Bpi%2C4%5D%2CDivide%5Bpi%2C2%5D%7D%5D%5C%2841%29

import Text.Printf (printf)

lovely-error

// this kernel writes a value only if invoaction index is even *_*

// when _flag is true, the store adress gets computed to be beyound (1 << 48) byte location .
// apparently stores beyound valid adress space on gpu... just become noops!

#define store_if_true(Ty, addr, val, flag) \
    *((__global Ty*)(((unsigned long)addr) + (((unsigned long)(flag == 0)) * ((1LU << 48) - ((unsigned long)addr))))) = val;

__kernel void kern(__global unsigned int* buffer) {

lovely-error

1. Create this file sudo touch /etc/apt/sources.list.d/rocm.list
2. put this line in there deb [arch=amd64] https://repo.radeon.com/rocm/apt/3.5.1/ xenial main
3. sudo apt update
4. install ocl sudo apt install rocm-opencl3.5.0
5. this script doesnt write icd path to /etc/OpenCL/vendors/ so that's on us
6. touch /etc/OpenCL/vendors/amdocl64.icd
7. echo "/opt/rocm-3.5.1/opencl/lib/libamdocl64.so" > /etc/OpenCL/vendors/amdocl64.icd
8. done. run clinfo. thing should work at this point

lovely-error

// for given number N, this function finds another number K such that
// (N * K) mod 2^64 = 1
fn mult_mod_inv(n: u64) -> u64 {
    assert!(n & 1 == 1, "Doesnt work for even numbers");
    assert!(n != 0, "Equation 0 mod N == 1 does not have a solution");
    let mut k = 1u64;
    let mut i = 1u64;
    for _ in 0 .. 64 {
        i <<= 1;
        let c = k.wrapping_mul(n);

lovely-error

{-# OPTIONS --type-in-type #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool

data Prod (L R : Set) : Set where
  pair : L -> R -> Prod L R

data Unit : Set where
  pt : Unit

lovely-error

def wmap : Type _ -> Type _ -> Type _ := 
  fun A B => @Subtype (Prod (A -> B) (B -> A)) fun ⟨ f , h ⟩ => ∀ i, h (f i) = i


def p1 : (w:wmap A B) -> let ⟨ ⟨ _ , h ⟩ , _ ⟩ := w; ∀ a:A , @Subtype B fun b => h b = a := by
  intro w
  let ⟨ ⟨ f , h ⟩ , p ⟩ := w
  simp at p
  simp
  intro a

lovely-error

example {x:Rat} : 3 * x / 0.2 = (2 + 1/2) / (3 + 1/3) -> x = 1/20 := by
  let is1 : (0.2:Rat) = 1/5 := by rfl
  rw [is1]
  let is2 : 3 * x / (1/5) = 3 * x * 5 := by
    simp_all only [one_div, div_inv_eq_mul]
  rw [is2]
  let is3 : 3 * x * 5 = 15 * x := by
    calc
      3 * x * 5 = 3 * 5 * x := mul_right_comm 3 x 5
      3 * 5 * _ = 15 * x := by