mb64

(* Itty bitty SMT solver: DPLL(T) where T = equality *)
(*
# let x, y = 0, 1 (* integer variable IDs *) ;;
# let prob = SMT.new_problem 2 (* 2 for two variables *) ;;
# let b = SMT.new_bool prob;;  
# SMT.add_clause prob [b; SMT.eq prob x y];
  SMT.add_clause prob [SMT.not b];
  SMT.solve prob;;
- : SMT.response = SMT.SAT
# SMT.add_clause prob [SMT.not (SMT.eq prob x y)];

mb64

(* Typechecker for MLTT with a universe hierarchy *)
(* Build with: ocamlfind ocamlc -package angstrom,stdio -linkpkg mltt.ml -o mltt *)
type name = string

module AST = struct
  type tm =
    | Var of name
    | U of int
    | Pi of name * ty * ty
    | Annot of tm * ty

mb64

type name = string

module AST = struct
  type ty =
    | TFun of ty * ty
    | TNamed of string
    | TApp of ty * ty

  type exp =
    | Annot of exp * ty

mb64

-- Normalization by Evaluation for STLC, in Agda
--
-- Partially based on "NbE for CBPV and polarized lambda calculus" (Abel, 2019)

open import Function

infixr 5 _⇒_
infixl 4 _,_
infix 2 _⊃_

mb64

#!/bin/bash

# Source: https://taylor.fausak.me/2021/11/16/haskell-survey-results
wget https://taylor.fausak.me/static/pages/2021-state-of-haskell-survey-results.json.zip
unzip 2021-state-of-haskell-survey-results.json.zip

echo "Question: If you wanted to convince someone to use Haskell, what would you say?" > q1-convince.txt
echo "---" >> q1-convince.txt
jq -r 'map(.s9q0 | .[]?) | join("\n---\n")' < 2021-state-of-haskell-survey-results.json >> q1-convince.txt

mb64

(* Compile with:
  $ ocamlfind ocamlc -package angstrom,stdio -linkpkg tychk.ml -o tychk
Example use:
  $ ./tychk <<EOF
  > let f = (fun x -> x) : forall a. a -> a
  > in f f
  > EOF
  input : forall a. a -> a
*)

mb64

kind ty type.

type tunit  ty.
type tfun   ty -> ty -> ty.
type tall   (ty -> ty) -> ty.

kind tm type.

type unit   tm.
type app    tm -> tm -> tm.

mb64

{-# OPTIONS --guardedness --safe #-}

open import Data.Product
open import Function using (_$_)
open import Relation.Binary using (IsEquivalence)
open import Algebra
open import Relation.Binary.Definitions
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

open import Tactic.RingSolver using (solve-∀)

mb64

(** A small benchmark for heap implementations
 *
 * Task: (mutably) sort an array, using heap sort
 * Implementations:
 *  - BinaryHeap, a simple binary heap implemented with mutable array operations
 *  - PairingHeap, Okazaki's strict amortized pairing heap
 *  - SplayHeap, Okazaki's strict amortized splay heap
 *  - BinomialHeap, Okazaki's strict amortized binomial heap
 *  - LeftistHeap, Okazaki's strict rank-based leftist heap
 *

mb64

{-# LANGUAGE ImportQualifiedPost, BlockArguments #-}
module Main where

import Control.Applicative
import Control.Monad
import Control.Monad.RWS
import Data.Char
import Data.Foldable
import Data.List
import Data.Set qualified as Set