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

stedolan

type alloc_count = { mutable total: float }
let allocs = { total = 0. }

let[@inline never] count txt =
  let now = int_of_float (Gc.minor_words () -. allocs.total) in
  Printf.printf "%20s: %d\n" txt now;
  allocs.total <- Gc.minor_words ()

let v = Sys.opaque_identity (ref 42)

stedolan

module F () =
  struct
    let v01 = ref 42
    let v02 = ref 42
    let v03 = ref 42
    let v04 = ref 42
    let v05 = ref 42
    let v06 = ref 42
    let v07 = ref 42
    let v08 = ref 42

stedolan

(**************************************************************************)
(*                                                                        *)
(*                                 OCaml                                  *)
(*                                                                        *)
(*                       Pierre Chambart, OCamlPro                        *)
(*           Mark Shinwell and Leo White, Jane Street Europe              *)
(*                                                                        *)
(*   Copyright 2013--2016 OCamlPro SAS                                    *)
(*   Copyright 2014--2016 Jane Street Group LLC                           *)
(*                                                                        *)

stedolan

type bigstring = (char, Bigarray.int8_unsigned_elt, Bigarray.c_layout) Bigarray.Array1.t
let alloc_bigstring size = Bigarray.Array1.create Char Bigarray.c_layout size
external bigstring_refcount : bigstring -> int = "pinbuf_bigstring_refcount" [@@noalloc]

module Pinbuf (Size : sig val size : int end) : sig
  type t = private bigstring
  val alloc : unit -> t
  val release : t -> unit

  val count_buffers : unit -> int