iitalics

(* type level naturals *)

type zero = |
type 'n suc = |

type _ nat =
  | Z : zero nat
  | S : 'n nat -> 'n suc nat

(* length indexed lists *)

iitalics

const fn str_trim_ascii_whitespace(s: &str) -> &str {
    let mut bs = s.as_bytes();

    while let Some((hd, tl)) = bs.split_first() {
        if hd.is_ascii_whitespace() {
            bs = tl;
        } else {
            break;
        }
    }

iitalics

#!/usr/bin/env bash

# ~/.local/libexec/discord-update.bash

which tar >/dev/null 2>/dev/null || (echo "missing command: 'tar'"; exit 1)
which wget >/dev/null 2>/dev/null || (echo "missing command: 'wget'"; exit 1)
which curl >/dev/null 2>/dev/null || (echo "missing command: 'curl'"; exit 1)
which jq >/dev/null 2>/dev/null || (echo "missing command: 'jq'"; exit 1)

if [[ "$EUID" == 0 ]]; then

iitalics

type 'a susp = ('a, unit) Effect.Shallow.continuation

type context =
  | Top
  | Sub of {
      mutable n : int;
      sus : unit susp;
      sup : context;
    }

iitalics

open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_; _^_)
open import Data.Product using (_×_; _,_)
open import Function.Base using (_$_; _∘_)
open import Function.Definitions using (Injective)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; trans; sym; cong; refl; subst)

------------------------------------------------------------------------------------------
-- The "crush" function maps a pair of ℕ's to a single ℕ via prime factors 2 and 3.
------------------------------------------------------------------------------------------

iitalics

async fn communicate(
    mut child: tokio::process::Child,
    input: String
) -> std::io::Result<std::process::Output> {
    use tokio::io::{AsyncReadExt, AsyncWriteExt};
    let mut stdin = child.stdin.take().expect("No stdin on child process");
    let mut stdout = child.stdout.take().expect("No stdout on child process");
    let mut stderr = child.stderr.take().expect("No stderr on child process");

    let write_stdin_fut = async {

iitalics

let label = "iitalics"
let time_limit = 5.
let threads = 1
let tags = "algorithm=base,faithful=yes,bits=1"

let report iters time =
  Printf.printf "%s;%d;%f;%d;%s\n"
    label iters time threads tags

(* optionally runs afterwards to check solution against a reference *)

iitalics

(* 0. recursive impl **************************************************)

let sum l =
  let rec sum = function
    | x :: xs -> sum xs + x
    | [] -> 0
  in
  sum l

(* 1. continuation passing style **************************************)

iitalics

module Data = struct
  type color = I | J | L | O | S | T | Z
  type cell = NoCell | Garbage | CI | CJ | CL | CO | CS | CT | CZ
  let cell_of_color (co: color): cell = Obj.magic (2 + Obj.magic co)
  let char_of_cell (cl: cell): char = ".GIJLOSTZ".[Obj.magic cl]
  let char_of_color co = char_of_cell (cell_of_color co)
end

module type Matrix_S = sig
  type t

iitalics

/* input: (some strict language with haskell-like syntax)
    a ++ b = case a of
      []      -> b
      x :: a' -> x :: (a' ++ b)
 */

// -- direct compilation to C -->

list* append(list* a, list* b) {
  switch (a->tag) {