japesinator

➜  ~ ~/.local/bin/manticore --verbose heap0
2017-03-13 15:15:42,372: [10700] MAIN:INFO: [+] Loading challenge ['heap0']
2017-03-13 15:15:42,372: [10700] MODEL:DEBUG: Opening file descriptors (0,1,2)
2017-03-13 15:15:42,375: [10700] MODEL:DEBUG: Loading heap0 as a i386 elf
2017-03-13 15:15:42,378: [10700] MODEL:DEBUG: Loading elf offset: 00000000 addr:56555000 56556000 r x
2017-03-13 15:15:42,378: [10700] MODEL:DEBUG: Loading elf offset: 00000000 addr:56556000 56558000 rw 
2017-03-13 15:15:42,379: [10700] MODEL:DEBUG: Zeroing main elf fractional pages. From 56557008 to 56558000.
2017-03-13 15:15:42,379: [10700] MODEL:DEBUG: Main elf bss:56557008
2017-03-13 15:15:42,379: [10700] MODEL:DEBUG: Main elf brk 56558000:
2017-03-13 15:15:42,446: [10700] MODEL:DEBUG: Loading interpreter offset: 00000000 addr:bffbd000 bffdf000 r x

japesinator

{-# LANGUAGE Rank2Types #-}

class Numbery a where
  floating    :: a -> Float
  add         :: a -> a -> a
  mul         :: a -> a -> a

sigma :: Numbery a => [a] -> a
sigma = foldr1 add

japesinator

{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

class Profunctor p where
  dimap :: (s -> a) -> (b -> t) -> p a b -> p s t

type Iso s t a b = forall p. Profunctor p => p a b -> p s t

iso :: (s -> a) -> (b -> t) -> Iso s t a b

japesinator

     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.18-
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Type checking ./test.idr
Elaborating type decl Main.forwards[]

japesinator

class Profunctor (p : Type -> Type -> Type) where

  dimap : (a -> b) -> (c -> d) -> p b c -> p a d
  dimap f g = lmap f . rmap g

  lmap : (a -> b) -> p b c -> p a c
  lmap = flip dimap id

  rmap : (a -> b) -> p c a -> p c b
  rmap = dimap id

japesinator

mkPersist sqlSettings [persistLowerCase|
Person
    name String
    age Int
    deriving Show
|]

japesinator

Lens Theory Independent Study Writeup
=====================================

JP Smith
-------

(Note: This file compiles as both markdown and idris, and the below is just boilerplate to allow that)

> import Control.Arrow
> import Control.Category

japesinator

module Main

import Data.Profunctor
import Data.Profunctor.Lens

-- This is an unpleasant helper function because type inference is Hard
myLens : Lensing p => Simple (Lens {p}) (String, String) String
myLens = _1

-- hello : String

japesinator

$ ../../.cabal-sandbox/bin/idris --nocolour --quiet interactive005.idr < input
3 : Nat
Hello, World
main : IO ()
    This is a docstring

Main.main is Total
Hello, World
Prelude.Basics.id : a -> a
Prelude.Basics.id : {a : Type} -> (__pi_arg : a) -> a

japesinator

$ make test
[...]
Ran interactive005...FAILURE
13a14,15
>        IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
>        PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE
make: *** [interactive005.test] Error 1

$ cd test/interactive005
$ diff <(./run) expected