einblicker

open FSharpx.Continuation

//from http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.3425
type DelimitedCont<'A,'B>() =
  let metaCont = ref Unchecked.defaultof<'A -> Cont<'A, 'B>>

  member private this.Abort (thunk:Cont<'A,'B>):Cont<'A,'B> =
    cont {
      let! v = thunk
      return! !metaCont v  

einblicker

module ToyTypeInfer

type Var = string

type Expr =
  | ENum of int
  | EBool of bool
  | EVar of Var
  | EPlus of Expr * Expr
  | EIf of Expr * Expr * Expr

einblicker

|- let rec apply = fun l -> fun x ->
      match l with [] -> x | f :: l -> apply l (f x) in
    apply ((fun x -> x * x) :: (fun y -> y + 3) :: []) 4 
   evalto 19
by E-LetRec {
  apply = ()[rec apply = fun l -> fun x ->
             match l with [] -> x | f :: l -> apply l (f x)] |-
    apply ((fun x -> x * x) :: (fun y -> y + 3) :: []) 4
      evalto 19
        by E-App {

einblicker

|- let rec apply = fun l -> fun x ->
   match l with [] -> x | f :: l -> f (apply l x) in
    apply ((fun x -> x * x) :: (fun y -> y + 3) :: []) 4 
   evalto 49
by E-LetRec {
  apply = ()[rec apply = fun l -> fun x ->
             match l with [] -> x | f :: l -> f (apply l x)] |-
    (apply ((fun x -> x * x) :: (fun y -> y + 3) :: [])) 4
      evalto 49
        by E-App {

einblicker

|- let rec length = fun l -> match l with [] -> 0 | x :: y -> 1 + length y in
    length ((1 :: 2 :: []) :: (3 :: 4 :: 5 :: []) :: []) evalto 2
by E-LetRec {
  length = ()[rec length = fun l -> match l with [] -> 0 | x :: y -> 1 + length y] |-
    length ((1 :: 2 :: []) :: (3 :: 4 :: 5 :: []) :: []) evalto 2
      by E-AppRec {
        length = ()[rec length = fun l -> match l with [] -> 0 | x :: y -> 1 + length y] |-
          length evalto ()[rec length = fun l -> match l with [] -> 0 | x :: y -> 1 + length y]
            by E-Var {};

einblicker

|- let rec length = fun l -> match l with [] -> 0 | x :: y -> 1 + length y in
    length (1 :: 2 :: 3 :: []) evalto 3
by E-LetRec {
  length = ()[rec length = fun l -> match l with [] -> 0 | x :: y -> 1 + length y] |-
    length (1 :: 2 :: 3 :: []) evalto 3
      by E-AppRec {
        length = ()[rec length = fun l -> match l with [] -> 0 | x :: y -> 1 + length y] |-
          length evalto ()[rec length = fun l -> match l with [] -> 0 | x :: y -> 1 + length y]
            by E-Var {};

einblicker

|- let rec f = fun x -> if x < 1 then [] else x :: f (x - 1) in
   f 3 evalto 3 :: 2 :: 1 :: []
    by E-LetRec {
      f = ()[rec f = fun x -> if x < 1 then [] else x :: f (x - 1)] |-
        f 3 evalto 3 :: 2 :: 1 :: []
          by E-AppRec {
            f = ()[rec f = fun x -> if x < 1 then [] else x :: f (x - 1)] |-
              f evalto ()[rec f = fun x -> if x < 1 then [] else x :: f (x - 1)]
                by E-Var {};

einblicker

|- let f = fun x -> match x with [] -> 0 | a :: b -> a in
    f (4::[]) + f [] + f (1 :: 2 :: 3 :: [])
evalto 5 by E-Let {
  |- fun x -> match x with [] -> 0 | a :: b -> a
    evalto ()[fun x -> match x with [] -> 0 | a :: b -> a]
      by E-Fun {};
  f = ()[fun x -> match x with [] -> 0 | a :: b -> a] |-
    ((f (4::[])) + (f [])) + (f (1 :: 2 :: 3 :: []))
      evalto 5 by E-Plus {
        

einblicker

|- let rec . = fun . -> 
     if #1 < 2 then 1 else #1 * #2 (#1 - 1) in #1 3
evalto 6 by E-LetRec {
  ()[rec . = fun . -> 
     if #1 < 2 then 1 else #1 * #2 (#1 - 1)] |- #1 3 evalto 6 by E-AppRec {
       ()[rec . = fun . -> 
          if #1 < 2 then 1 else #1 * #2 (#1 - 1)] |- #1
         evalto ()[rec . = fun . -> 
                   if #1 < 2 then 1 else #1 * #2 (#1 - 1)] by E-Var {};
       ()[rec . = fun . -> 

einblicker

|- let fact = fun self -> fun n ->
     if n < 2 then 1 else n * self self (n - 1) in
   fact fact 3
  evalto 6
    by E-Let {
      |- fun self -> fun n ->
        if n < 2 then 1 else n * self self (n - 1)
          evalto ()[fun self -> fun n ->
                    if n < 2 then 1 else n * self self (n - 1)]
            by E-Fun {};