mb64

module DerivingEq

import Language.Reflection

%language ElabReflection

public export
countArgs : (ty : TTImp) -> Nat
countArgs (IPi _ _ ExplicitArg _ _ retTy) = 1 + countArgs retTy
countArgs (IPi _ _ _ _ _ retTy) = countArgs retTy

mb64

module Bidir

Ident : Type
Ident = String

mutual
  BaseCtx' : Type
  Ctx' : BaseCtx' -> Type
  CtxItem' : (b : BaseCtx') -> (c : Ctx' b) -> Type

mb64

{-# OPTIONS --cubical --safe #-}

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism using (Iso; isoToPath)

data N : Set where
  one : N
  _+_ : N → N → N
  assoc : (a b c : N) → (a + b) + c ≡ a + (b + c)

mb64

.PHONY: all bench

all: bench

bench: main_c main_asm
	@echo "Running the C version..."
	@bash -c 'time ./main_c'
	@echo
	@echo "Running the asm version..."
	@bash -c 'time ./main_asm'

mb64

/* A flat representation of
 * data Tree = Leaf Int | Node Tree Tree
 *
 * Either:
 *  - *ft is LEAF and a single int follows
 *  - *ft is NODE and two subtrees follow
 */
#define LEAF 0
#define NODE 1

mb64

f : {a : Type} -> a -> a
f {a=Int}    x = 2 * x
f {a=String} x = "twice " ++ x
f {a=_}      x = x

main : IO ()
main = do
  -- Ad-hoc polymorphism type 1: type-based overloading
  -- Also in: C++, Java
  printLn $ "hi " ++ "there" -- uses the ++ for String

mb64

umask 022

declare -x PAGER='less'
declare -x EDITOR='vim'
declare -x VISUAL="${EDITOR}"
declare -x FCEDIT="${EDITOR}"

declare -x LS_COLORS='no=01;37:fi=01;37:di=01;34:ln=01;36:pi=01;32:so=01;35:do=01;35:bd=01;33:cd=01;33:ex=01;31:mi=00;37:or=00;36:'

declare -x HISTCONTROL=ignoreboth:erasedups

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

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

{-# 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-∀)