Skip to content

Instantly share code, notes, and snippets.

View tpsinnem's full-sized avatar

Timo Petteri Sinnemäki tpsinnem

14 followers · 4 following
View GitHub Profile
@tpsinnem
tpsinnem / MachineDabbling.hs
Last active October 13, 2015 14:31
{-# LANGUAGE Rank2Types #-}
module Data.Machine.Dabbling
( unfoldPlan
) where
import Data.Machine
import Data.Profunctor.Unsafe ((#.))
@tpsinnem
tpsinnem / gist:4564912f584316142f1e
Created June 2, 2014 13:09
Question about totality checking recursion on a predecessor function on a binary number representation.
%default total
-------------------------
-- General stuff first:
-------------------------
decProofType : {a:Type} -> Dec a -> Type
decProofType {a} (Yes _) = a
decProofType {a} (No _) = a -> _|_
@tpsinnem
tpsinnem / gist:11090327
Created April 19, 2014 16:58
A case that should be impossible gives an odd 'valid case' error.
----------------------
-- This is not recognized as a complete function, but produces a metavariable
-- instead. Fair enough, but...
----------------------
myFalseElimFail : _|_ -> a
----------------------
-- ... when trying to complete it with 'impossible', this weird error pops up:
-- Type checking ./bad-valids.idr
-- bad-valids.idr:14:18:myFalseElimFail' x is a valid case
@tpsinnem
tpsinnem / gist:10057490
Last active August 29, 2015 13:58
A successful attempt at making https://gist.github.com/esmooov/3185eba5d7d8784366fd work more conveniently with the default arg substitution patch https://github.com/tpsinnem/Idris-dev/tree/d5162a0fee5c925660b60a8644566f017dae831c
module Main
-- A fun experiment to try to implement vectors that would correspond to a fixed
-- size in underlying memory. Similar to the capacity of Go slices.
taken : Nat -> Nat -> Nat -> Nat
taken n max = (\v => if v+n > max then max + 8 else max)
-- data Fmv : (c : Nat) -> (m : Nat) -> (Nat -> Nat) -> Type -> Type where
-- fwv : (Vect c t) -> (m : Nat) -> Fmv c m (taken c m) t
@tpsinnem
tpsinnem / gist:10054033
Created April 7, 2014 21:00
A failed attempt at making https://gist.github.com/esmooov/3185eba5d7d8784366fd work more conveniently with the default arg substitution patch https://github.com/tpsinnem/Idris-dev/tree/d5162a0fee5c925660b60a8644566f017dae831c
module Main
||| A fun experiment to try to implement vectors that would correspond to a fixed
||| size in underlying memory. Similar to the capacity of Go slices.
taken : Nat -> Nat -> Nat -> Nat
taken n max = (\v => if v+n > max then max + 8 else max)
--data Fmv : (c : Nat) -> (m : Nat) -> (Nat -> Nat) -> Type -> Type where
-- fwv : (Vect c t) -> (m : Nat) -> Fmv c m (taken c m) t
@tpsinnem
tpsinnem / gist:9992007
Created April 5, 2014 13:32
Warnings and error in 'make test'
Warnings and error in 'make test' on commit aa392335ed70c4b05259e1c120b854e7865a9bb7
$ make test
cabal haddock --executables --hyperlink-source --html --hoogle --html-location="http://hackage.haskell.org/packages/archive/\$pkg/latest/doc/html" --haddock-options="--title Idris"
Running Haddock for idris-0.9.12...
Running hscolour for idris-0.9.12...
Preprocessing library idris-0.9.12...
Preprocessing executable 'idris' for idris-0.9.12...
Preprocessing library idris-0.9.12...
Warning: The documentation for the following packages are not installed. No
@tpsinnem
tpsinnem / gist:9987630
Created April 5, 2014 04:45
Another incredibly useful thing one can do given the default arg substitution patch
mutual
data Foo : Type where
foo : Foo
fooey : (fooa:Foo) -> { default (foox fooa) foob : Foo } -> Foo
foox : Foo -> Foo
foox (fooey fa) = fa
foox f = f
{-
@tpsinnem
tpsinnem / gist:9970467
Last active August 29, 2015 13:58
Syntax for Dec-based default arguments. Relies on a WIP compiler patch for substitution into default arguments: https://github.com/tpsinnem/Idris-dev/tree/default-arg-subst
%default total
--------------------------------------------------------------------------
-- First some generic stuff that will probably also be useful elsewhere:
--------------------------------------------------------------------------
DecProofType : {a:Type} -> Dec a -> Type
DecProofType {a} (Yes _) = a
DecProofType {a} (No _) = a -> _|_
@tpsinnem
tpsinnem / gist:9962238
Created April 3, 2014 20:27
Error during 'make test' on my default arguments WIP atop a somewhat revent github master -- don't know whether it's related to my code ATM or not.
[... snip ...]
0% ( 0 / 7) in 'Pkg.PParser'
60% ( 12 / 20) in 'Pkg.Package'
0% ( 0 / 9) in 'Idris.Transforms'
Warning: Idris.Colours: could not find link destinations for:
System.Console.ANSI.Common.Color
Warning: Idris.Core.TC: could not find link destinations for:
Control.Monad.Trans.Error.Error
Warning: Idris.Core.TT: could not find link destinations for:
Text.PrettyPrint.Annotated.Leijen.Doc Control.Monad.Trans.Error.Error Data.Text.Internal.Text Data.Vector.Unboxed.Base.Vector Util.Pretty.Pretty
@tpsinnem
tpsinnem / gist:9961593
Last active August 29, 2015 13:58
Substitution into default arguments, using a WIP compiler patch: https://github.com/tpsinnem/Idris-dev/tree/default-arg-subst . UPDATE: Now works in syntax rules as well: https://gist.github.com/tpsinnem/9970467
%default total
--------------------------------------------------------------------------
-- First some generic stuff that will probably also be useful elsewhere:
--------------------------------------------------------------------------
DecProofType : {a:Type} -> Dec a -> Type
DecProofType {a} (Yes _) = a
DecProofType {a} (No _) = a -> _|_