Skip to content

Instantly share code, notes, and snippets.

Matthew Brecknell mbrcknl

View GitHub Profile
View hlist.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -Wall #-}
data HList f l where
HNil :: HList f '[]
View PHOAS.hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilyDependencies #-}
data Ty = IntTy | FunTy Ty Ty
View PHOAS.hs
{-# 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
View locale_experiment.thy
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"
View Scratch.thy
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"
View sf_p5_p6_equiv.v
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).
View phoas.v
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)
View SortingFunction.v
Require Import Sorted.
Require Import Permutation.
Definition isSortingFunction (A: Type) (R: A -> A -> Prop) (f: list A -> list A): Prop :=
forall (xs: list A), Permutation xs (f xs) /\ Sorted R (f xs).
Check (isSortingFunction: forall (A: Type), (A -> A -> Prop) -> (list A -> list A) -> Prop).
@mbrcknl
mbrcknl / phoas-de-bruijn.v
Created Oct 20, 2015
Mucking about with PHOAS and type-indexed de Bruijn representations
View phoas-de-bruijn.v
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)
@mbrcknl
mbrcknl / Norm.v
Created Sep 29, 2015
Extending saturated sets to product types, alternative version
View Norm.v
Fixpoint R (T:ty) (t:tm) {struct T} : Prop :=
has_type empty t T /\ halts t /\
match T with
| TBool => True
| TArrow T1 T2 => (forall s, R T1 s -> R T2 (tapp t s))
| TProd T1 T2 => exists t1, exists t2, t ==>* tpair t1 t2 /\ R T1 t1 /\ R T2 t2
end.
You can’t perform that action at this time.