einblicker

|- let rec sum = fun f -> fun n ->
     if n < 1 then 0 else f n + sum f (n - 1) in 
   sum (fun x -> x * x) 2
  evalto 5
    by E-LetRec {
      sum = ()[rec sum = fun f -> fun n ->
               if n < 1 then 0 else f n + sum f (n - 1)] |-
        ((sum (fun x -> x * x)) 2)
          evalto 5
            by E-App {

einblicker

|- let rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2) in
   fib 5
  evalto 5 by E-LetRec {
    fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |-
      fib 5
        evalto 5 by E-AppRec {

          fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |-
            fib
              evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)]

einblicker

|- let rec fact = fun n ->
   if n < 2 then 1 else n * fact (n - 1) in
   fact 3
  evalto 6 by E-LetRec {
    fact = ()[rec fact = fun n ->
              if n < 2 then 1 else n * fact (n - 1)] |-
      fact 3
        evalto 6 by E-AppRec {
          fact = ()[rec fact = fun n ->
                    if n < 2 then 1 else n * fact (n - 1)] |-

einblicker

|- let s = fun f -> fun g -> fun x -> f x (g x) in
   let k = fun x -> fun y -> x in
   s k k 7
  evalto 7 by E-Let {
    |- fun f -> fun g -> fun x -> f x (g x) evalto ()[fun f -> fun g -> fun x -> f x (g x)] by E-Fun {};
    
    s = ()[fun f -> fun g -> fun x -> f x (g x)] |-
    let k = fun x -> fun y -> x in
    s k k 7
    evalto 7 by E-Let {

einblicker

|- let compose = fun f -> fun g -> fun x -> f (g x) in 
   let p = fun x -> x * x in
   let q = fun x -> x + 4 in
   compose p q 4 
  evalto 64 by E-Let {
  |- fun f -> fun g -> fun x -> f (g x) evalto ()[fun f -> fun g -> fun x -> f (g x)] by E-Fun {};
  compose = ()[fun f -> fun g -> fun x -> f (g x)]
  |- let p = fun x -> x * x in
     let q = fun x -> x + 4 in
     compose p q 4 

einblicker

|- let twice = fun f -> fun x -> f (f x) in twice twice (fun x -> x * x) 2 evalto 65536 by E-Let {
  |- fun f -> fun x -> f (f x) evalto ()[fun f -> fun x -> f (f x)] by E-Fun {};
  twice = ()[fun f -> fun x -> f (f x)] |- ((twice twice) (fun x -> x * x)) 2 evalto 65536 by E-App {
    twice = ()[fun f -> fun x -> f (f x)] |- ((twice twice) (fun x -> x * x)) evalto
      (f = (f = (twice = ()[fun f -> fun x -> f (f x)])[fun x -> x * x])[fun x -> f (f x)])[fun x -> f (f x)] by E-App {
      twice = ()[fun f -> fun x -> f (f x)] |- (twice twice) evalto (f = ()[fun f -> fun x -> f (f x)])[fun x -> f (f x)] by E-App {
	twice = ()[fun f -> fun x -> f (f x)] |- twice evalto ()[fun f -> fun x -> f (f x)] by E-Var1 {};
	twice = ()[fun f -> fun x -> f (f x)] |- twice evalto ()[fun f -> fun x -> f (f x)] by E-Var1 {};
	f = ()[fun f -> fun x -> f (f x)] |- fun x -> f (f x) evalto (f = ()[fun f -> fun x -> f (f x)])[fun x -> f (f x)] by E-Fun {}
      };

einblicker

open System
open Microsoft.FSharp.Quotations
open Microsoft.FSharp.Quotations.ExprShape
open Microsoft.FSharp.Linq.QuotationEvaluation

module Util =
  let rnd = new Random()
  let (|Range|_|) min max x =
    if min <= x && x <= max then Some() else None

einblicker

module DepList =
    type Z = internal new() = {}

    [<Sealed>]
    type S<'nat when 'nat :> Z> = inherit Z private new() = {}

    [<Sealed>]
    type DepList<'a, 'length when 'length :> Z> =
        val internal _list: 'a list
        internal new(list: 'a list) = { _list = list }

einblicker

methodName = "append"

def makeType(i)
  acc = "Z"
  i.times{|e|
    acc = "S<" + acc + ">"
  }
  acc
end

einblicker

#ifndef STATIC_DISPATCHER_HPP_INCLUDED
#define STATIC_DISPATCHER_HPP_INCLUDED

#include <boost/mpl/list.hpp>
#include <boost/mpl/front.hpp>
#include <boost/mpl/pop_front.hpp>
#include <boost/mpl/index_of.hpp>
#include <boost/mpl/bool.hpp>
#include <boost/mpl/if.hpp>
#include <boost/mpl/replace.hpp>