stedolan

(* An implementation of (part of) the lazy data structure of:

      First-Order Laziness
      Anton Lorenzen, Daan Leijen, Wouter Swierstra, Sam Lindley
      ICFP 2025

   Requires OCaml 5.2+ / OxCaml *)

module type LazyS = sig
  type _ repr

stedolan

let enable_hugepages () =
  let ch = open_in "/proc/self/maps" in
  let module Syscall = struct
    external madvise : (int64[@unboxed]) -> (int64[@unboxed]) -> (int[@untagged]) -> (int[@untagged]) =
      "unimplemented" "madvise"
  end in
  try
    while true do
      Scanf.sscanf (input_line ch) "%Lx-%Lx %s %Lx %x:%x %Ld %s"
        (fun start_addr end_addr perms offset devmaj devmin inode path ->

stedolan

Generating good code for bitfields

Here's a definition of the packed 16-bit RGB565 pixel format as a C struct:

typedef struct { unsigned r : 5, g : 6, b : 5; } pixel;

and a couple of functions that operate on it:

stedolan

let table = Array.init 10_000 (fun _ -> Bytes.make 1_000 'a')

let writes =
  Option.map bool_of_string (Sys.getenv_opt "WRITES")
  |> Option.value ~default:false

let[@inline never] f () =
  List.init (Array.length table) (fun i ->
    let buf = table.(i) in
    if writes then table.(i) <- buf;

stedolan

{-# LANGUAGE GADTs #-}
-- nontermination without any recursion, even in types
-- possible because of impredicativity + injectivity
-- based on https://gist.github.com/leodemoura/0c88341bb585bf9a72e6
-- see also https://github.com/idris-lang/Idris-dev/issues/3687

data False

data I (f :: * -> *) where

stedolan

let promotion_rate = 50
let collection_rate = 30
let ballast_mb = 100
let iters_m = 50

let rand =
  let counter = ref 43928071 in
  fun () ->
    let n = !counter in
    counter := n * 454339144066433781 + 1;

stedolan

module GenericTrees where
open import Agda.Builtin.String
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Primitive

variable l : Level

-- Products and sums

stedolan

while :; do clear; curl -skL https://bar.emf.camp/api/on-tap.json | jq -r 'keys[] as $k | ("--", ("\($k):"), (.[$k][] | "\(.manufacturer) \(.name) (\(.abv)%)@\(.price)\(if .remaining_pct|tonumber<5 then " (running out)" else "" end)"))' | column -t -s '@'; sleep 10; done

stedolan

-- Is this a bug in Agda?
-- Try repro with latest agda sometime

module VarBug where

open import Agda.Builtin.Equality
open import Agda.Primitive

data Unit : Set where
  tt : Unit

stedolan

type n = Z | S of n

let rec gen_locals (local_ n) depth _ = local_
  if depth = 0
  then
    S n
  else
    let s = S n in
    let m = gen_locals s (depth - 1) (ref 42) in
    let _ = gen_locals m (depth - 1) (ref 42) in