This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
➜ ~ ~/.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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
____ __ _ | |
/ _/___/ /____(_)____ | |
/ // __ / ___/ / ___/ 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[] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mkPersist sqlSettings [persistLowerCase| | |
Person | |
name String | |
age Int | |
deriving Show | |
|] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
$ ../../.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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
$ 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 |
NewerOlder