Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Lysxia / msets.v
Created Jul 10, 2021
Minimal example of instantiating MSetAVL
View msets.v
From Coq Require Import MSets.
Import Orders.
Inductive t : Type :=
| A : t
| B : t -> t
.
Module OrderedTAlt <: OrderedTypeAlt.
@Lysxia
Lysxia / MyPlugin.hs
Last active Jun 20, 2021
Source plugin skeleton
View MyPlugin.hs
-- GHC 9+
import GHC.Plugins hiding (Type)
import GHC.Hs
plugin :: Plugin
plugin = defaultPlugin
{ parsedResultAction = \_ _ m -> pure (transform m)
}
transform :: HsParsedModule -> HsParsedModule
@Lysxia
Lysxia / testeq.hs
Created May 29, 2021
Generic implementation of TestEquality
View testeq.hs
{-# LANGUAGE KindSignatures, DataKinds, TemplateHaskell, GADTs, TypeFamilies, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, QuantifiedConstraints, ConstraintKinds, PolyKinds, TypeApplications, ScopedTypeVariables #-}
import Data.Kind (Type)
import Data.Type.Equality
import Data.Maybe (isJust, isNothing)
import Generics.Kind hiding ((:~:))
import Generics.Kind.TH
-- * Example
View eval_subst.v
Set Implicit Arguments.
(* Source *)
Inductive exp :=
| CONST : nat -> exp
| IFV : exp -> exp -> exp -> exp
| ADD : exp -> exp -> exp.
Definition ifnat {R} (n : nat) (x1 x2 : R) : R :=
match n with
View better_N.v
From Coq Require Import NArith.
Fixpoint add (x y : positive) {struct x} : positive :=
match x with
| (p~1)%positive =>
match y with
| (q~1)%positive => ((Pos.succ (add p q))~0)%positive (* Only change *)
| (q~0)%positive => ((add p q)~1)%positive
| 1%positive => ((Pos.succ p)~0)%positive
end
View NN.v
From Coq Require Import NArith.
Lemma lem1 p : (Pos.succ p) = (p + 1)%positive.
Proof.
induction p; cbn; auto.
Qed.
Lemma lem2 p p0 :
(Pos.succ (p + p0)) = (p + Pos.succ p0)%positive /\ Pos.add_carry p p0 = (p + Pos.succ p0)%positive.
Proof.
@Lysxia
Lysxia / twist.v
Last active Mar 10, 2021
Non-uniqueness of pure without parametricity: a twisted applicative functor https://stackoverflow.com/questions/66555516/uniqueness-of-pure
View twist.v
Set Implicit Arguments.
Set Maximal Implicit Insertion.
(** A non-parametric extension of System F. *)
(** Typecase, and flip all booleans *)
Axiom twist : forall a : Type, a -> a.
Axiom twist_fun : forall a b, @twist (a -> b) = fun f x => twist (f (twist x)).
Axiom twist_bool : @twist bool = negb. (* Not the identity *)
(* [twist = id] for all other types *)
View w.hs
{-# LANGUAGE DeriveGeneric #-}
import Control.Applicative
import Test.QuickCheck
import GHC.Generics
data FirstChoice a = FirstChoice a [a]
deriving (Eq, Show, Generic)
instance Functor FirstChoice where
fmap f (FirstChoice x xs) = FirstChoice (f x) (fmap f xs)
View generic-free-monad.hs
{- Derive Monad for a type like @Pipe@, which is isomorphic to a @Free@ monad
@
data Pipe i o a
= Input (i -> Pipe i o a)
| Output o (Pipe i o a)
| Return a
deriving Generic
@
View freemonoid.v
(* The free monoid functor ([list]) is a monad *)
Set Implicit Arguments.
Set Contextual Implicit.
Set Maximal Implicit Insertion.
From Coq Require Import
List
Setoid
Morphisms.