jozefg

module intrinsic where
open import Function using (_∘_; id)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Sum as S
open import Data.Bool as B
open import Data.Nat as N

jozefg

open Cmdliner

module type Config_t =
sig
  type opt_level = O1 | O2 | O3

  val int_of_opt : opt_level -> int

  type config =
    { line_width : int

jozefg

\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{pftools}

\@ifundefined{basedir}{%
\RequirePackage{locallabel}
}{%
\RequirePackage{\basedir locallabel}
}%

\RequirePackage{Tabbing}	% Avoid the standard tabbing environment. Its \< conflicts with the semantic package.

jozefg

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternGuards #-}
module Unification where
import           Control.Monad
import           Control.Monad.Gen
import           Control.Monad.Trans
import qualified Data.Map.Strict     as M
import           Data.Foldable
import           Data.Monoid

jozefg

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternGuards #-}
module Unification where
import           Control.Monad
import           Control.Monad.Gen
import           Control.Monad.Trans
import qualified Data.Map.Strict     as M
import           Data.Foldable
import           Data.List           (foldl')

jozefg

module Main where
import Criterion.Main

f1 :: [(Int, b)] -> [Int] -> Bool
f1 ps qs = all (\q -> all (\p -> fst p /= q) ps) qs

f2 :: [(Int, b)] -> [Int] -> Bool
f2 ps qs = all (flip all ps . flip ((/=) . fst)) qs

main :: IO ()

jozefg

module simple-bracket where
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

record PCA : Set₁ where
  constructor mk-pca
  field
    A   : Set
    _≈_ : A → A → Set

jozefg

module howe where
open import Data.Nat
open import Data.Vec
open import Data.List
open import Data.Product
import Data.Fin  as F
import Relation.Binary as B
open import Relation.Binary.PropositionalEquality hiding (subst)
open import Relation.Nullary

jozefg

.global _c0_main
.text
_c0_main:
	push %rbx
	subq $0, %rsp
	movl $5, %eax
	imull %eax, %eax
	push %rbp
	movl %eax, %ebp
	movl %eax, %edi

jozefg

{-# LANGUAGE FlexibleContexts, ConstraintKinds, RecordWildCards #-}
module RegAlloc where
import Control.Applicative
import Control.Monad
import Data.Set (Set)
import Data.Map (Map)
import Control.Monad.Writer.Strict
import Control.Monad.State.Strict
import qualified Data.Set as S
import qualified Data.Map as M