Skip to content

Instantly share code, notes, and snippets.

View emilaxelsson's full-sized avatar

Emil Axelsson emilaxelsson

View GitHub Profile
@emilaxelsson
emilaxelsson / gist:5028556
Last active December 14, 2015 04:29
Liveness analysis and variable reuse for a list of assignments. Assumptions: All variables have the same type and size.
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TypeOperators #-}
import Control.Monad.State
import Data.Foldable (Foldable)
import qualified Data.Foldable as Fold
import Data.Map (Map)
import qualified Data.Map as Map
@emilaxelsson
emilaxelsson / gist:5170284
Last active December 15, 2015 00:08
Virtual tuples in Feldspar

Proposal for feldspar-language and feldspar-compiler.

Background

Tuples are currently compiled to structs whenever they are forced by a Syntax-overloaded function, such as condition or forLoop. In most cases, we would like to avoid the struct and just have the members as separate variables.

Consider the example

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
import Data.Type.Equality
import GHC.TypeLits
@emilaxelsson
emilaxelsson / Binding.hs
Last active August 29, 2015 14:01
Implementation of evaluation without dynamic type casting in Syntactic
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
@emilaxelsson
emilaxelsson / FeldsparBound.lhs
Last active August 29, 2015 14:13
Trying out the Bound library
> [UPDATE, 2015-02-23: The post has been slightly updated based on comments by Edward Kmett.]
In trying to understand the [Bound library](http://hackage.haskell.org/package/bound), and in particular, its limitations (if any) in terms of expressiveness and efficiency. I will here try to implement a small subset of the [Feldspar](http://hackage.haskell.org/package/feldspar-language) EDSL using Bound.
DISCLAIMER: Statements in this text may very well reflect my misunderstandings rather than actual truths about Bound.
Note that I'm assuming basic familiarity with Bound. If you're not familiar with the library, see [its documentation](http://hackage.haskell.org/package/bound/docs/Bound.html).
I would be happy to receive feedback and hints for how to improve the code.
@emilaxelsson
emilaxelsson / StrictTermination.lhs
Last active October 26, 2015 09:57
Strictness can fix non-termination!
<!--
\begin{code}
module Loop where
\end{code}
-->
(This post is literate Haskell, [available here](https://gist.github.com/emilaxelsson/26658849e39918883ffe).)
I've always thought that strictness annotations can only turn terminating programs into non-terminating ones. Turns out that this isn't always the case. As always, `unsafePerformIO` changes things.
<!--
\begin{code}
module SudokuSAT where
\end{code}
-->
(This post is literate Haskell, [available here](https://gist.github.com/emilaxelsson/e15a3b72eef7468e5edf).)
Inspired by an [old(-ish) Galois post](https://galois.com/blog/2009/03/solving-sudoku-using-cryptol/) about using its SAT back end to solve sudokus, here is a similar sudoku solver written in Haskell using Koen Claessen's [SAT+ library](https://github.com/koengit/satplus).
(This post is literate Haskell, [available here](https://gist.github.com/emilaxelsson/81d2774f0c96750378bf).)
This post will show a trick for making it easier to work with terms representated as fixed-points of functors in Haskell. It is assumed that the reader is familiar with this representation.
First some extensions:
\begin{code}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
@emilaxelsson
emilaxelsson / CompleteMatching.hs
Last active January 20, 2017 19:28
Compilation as a Typed EDSL-to-EDSL Transformation
s{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
-- A version of the code from <http://fun-discoveries.blogspot.se/2016/03/compilation-as-typed-edsl-to-edsl.html>
-- which avoids incomplete matching on `Val` and `Ref`.
@emilaxelsson
emilaxelsson / tgmath_test.c
Created April 19, 2016 15:04
Test of tgmath.h
// This file demonstrates that if `tgmath.h` is included, it doesn't matter if
// `math.h` is also included and which order the include statements appear.
#include <stdio.h>
#include <tgmath.h>
#include <math.h>
int main() {
printf("%.20f\n", sinf((float) 5.0));
printf("%.20f\n", sin((double) 5.0));