jroesch

  trace = TracePoint.new(:call, :b_call, :c_call) do |tp|
    p [tp.lineno, tp.defined_class, tp.method_id, tp.event]
  end

  trace.enable

  puts "Hello, TracePoint!"

puts [1,2,3].length

jroesch

data UnAuthErr = MkErr deriving (Eq, Show)
data Req = MkReq deriving (Eq, Show)
data Credentials = MkCredentials deriving (Eq, Show)

data Auth a = Error a
            | Request Req a
            | Auth Credentials a
            deriving (Eq, Show)

instance Functor Auth where

jroesch

import java.nio._
import charset._
import scala.reflect.macros.blackbox.Context
import scala.language.experimental.macros

/* A set of example encodings */
sealed trait Encoding {
  val encodingName: String
}

jroesch

use std::io::BufferedReader;
use std::io::File;

pub struct Data {
  content: Box<Iterator<String>>
}

impl Iterator<String> for Data {
  fn next(&mut self) -> Option<String> {
    self.content.next()

jroesch

-- Program analysis and types are just views of the same problem. I encode my possible analysis here in the types and rely on the
-- type checker to ensure the correctness of my implementation instead of leaving it to pen and paper proof.
-- In this case we encode a langauge that is ideally correct by construction and then prove that translation of such a language
-- into ISA's is possible each indexed by the same time (which must be statically known, i.e reflected into the type). 
-- If we can prove equvalence between our higher level language to the ISA's and equivalence to the ISA then we have the desired
-- analysis, it only requires that you encode the cost model in the constructors of the ISAs

-- We simply use Nat's for the time being.
Time : Type
Time = Nat

jroesch

class A
  def m
    puts "A"
  end
end

module C
  def m
    puts "C"
  end

jroesch

cannot load such file -- iconv
/Users/jroesch/.rbenv/versions/2.1.2/lib/ruby/gems/2.1.0/bundler/gems/rails-45f3010d6d7a/activesupport/lib/active_support/dependencies.rb:251:in `require'
/Users/jroesch/.rbenv/versions/2.1.2/lib/ruby/gems/2.1.0/bundler/gems/rails-45f3010d6d7a/activesupport/lib/active_support/dependencies.rb:251:in `block in require'
/Users/jroesch/.rbenv/versions/2.1.2/lib/ruby/gems/2.1.0/bundler/gems/rails-45f3010d6d7a/activesupport/lib/active_support/dependencies.rb:236:in `load_dependency'
/Users/jroesch/.rbenv/versions/2.1.2/lib/ruby/gems/2.1.0/bundler/gems/rails-45f3010d6d7a/activesupport/lib/active_support/dependencies.rb:251:in `require'
/Users/jroesch/Invoca/web/config/initializers/action_mailer_utils.rb:1:in `<top (required)>'
/Users/jroesch/.rbenv/versions/2.1.2/lib/ruby/gems/2.1.0/bundler/gems/rails-45f3010d6d7a/activesupport/lib/active_support/dependencies.rb:245:in `load'
/Users/jroesch/.rbenv/versions/2.1.2/lib/ruby/gems/2.1.0/bundler/gems/rails-45f3010d6d7a/activesupport/lib/acti

jroesch

 cc -dynamic -bundle -undefined suppress -flat_namespace -o ../../.ext/i686-darwin13.2.0/gdbm.bundle gdbm.o -L. -L../.. -L. -L/Users/jroesch/.rbenv/versions/ree-1     .8.7-2012.02/lib     -lgdbm  -L/opt/local/lib -ldl -lobjc

jroesch

Type checking ./Parallax/ByteString/Core.idr
./Parallax/ByteString/Core.idr:32:56:When elaborating right hand side of Parallax.ByteString.Core.case block in case block in case block in case block in case block in case block in peekBits8:
When elaborating argument val to constructor Delay:
        INTERNAL ERROR: Not a guess ? {letty185} : Type 0. let succ' : {letty185} = ?defer Parallax.ByteString.Core.here : (t : Type h15) -> Type j15 -> Parallax.ByteString.Buffer.Buffer -> Parallax.ByteString.Buffer.Buffer -> Prelude.Nat.Nat -> Parallax.Types.Pos -> Parallax.Types.More -> Parallax.Types.More -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bit

jroesch

using (x : Type, P : x -> Type)
    data HList : (P : x -> Type) -> List x -> Type where
        Nil : HList P []
        (::) : {head : x} -> {tail : List x} -> P head -> HList P tail -> HList P (head :: tail)

head : {h : ty} -> {t : List ty} -> {P : ty -> Type} -> HList P (h :: t) -> P h
head (h :: _) = h

tail : {h : ty} -> {t : List ty} -> {P : ty -> Type} -> HList P (h :: t) -> HList P t
tail (_ :: t) = t