mbrcknl

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
 
{-# OPTIONS_GHC -Wall #-}
 
data HList f l where
  HNil :: HList f '[]

mbrcknl

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilyDependencies #-}

data Ty = IntTy | FunTy Ty Ty

mbrcknl

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}

data Ty = IntTy | FunTy Ty Ty

data Term :: (Ty -> *) -> Ty -> * where
  Lit :: Int -> Term var IntTy

mbrcknl

theory locale_experiment
imports Main
begin

section \<open>Algebraic formulation of a semilattice\<close>

locale semigroup =
  fixes ap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes assoc: "\<And>x y z. ap x (ap y z) = ap (ap x y) z"

mbrcknl

-- Matthew Brecknell @mbrcknl
-- BFPG.org, March-April 2015

-- With thanks to Conor McBride (@pigworker) for his lecture series:
-- https://www.youtube.com/playlist?list=PL44F162A8B8CB7C87
-- from which I learned most of what I know about Agda, and
-- from which I stole several ideas for this talk.

open import Agda.Primitive using (_⊔_)

mbrcknl

theory Scratch imports Main begin

locale Magma =
  fixes m :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"

locale SemiGroup = Magma +
  assumes assoc: "\<And>x y z. m (m x y) z = m x (m y z)"

locale Commutative = Magma +
  assumes comm: "\<And>x y. m x y = m y x"

mbrcknl

Definition p5 : com :=
  WHILE (BNot (BEq (AId X) (ANum 1))) DO
    HAVOC X
  END.

Definition p6 : com :=
  X ::= ANum 1.

Lemma p5_may_terminate: forall s, p5 / s || update s X 1.
  intro s; destruct (eq_nat_dec (s X) 1).

mbrcknl

import Data.Set.Monad as SM
import Debug.Trace as DT

(<+>) = liftM . plus
plus x y = DT.trace "." (x + y)

l = SM.fromList [0,1]

-- Intuitively expect 28 additions, but we actually get 60!
test = Set Int

mbrcknl

# ...

if [ -f ~/.gpg-agent-info ]; then
  . ~/.gpg-agent-info
  export GPG_AGENT_INFO
fi

# ...

mbrcknl

Require Import List.

Inductive type : Type :=
| base : type
| arr  : type -> type -> type.

Infix "==>" := arr (right associativity, at level 52).

Inductive elem {A: Type} (x: A): list A -> Type :=
| here  : forall xs, elem x (x :: xs)