einblicker

(require :arnesi)
(require :cl-match)
(require :split-sequence)
(import '(arnesi:queue arnesi:enqueue arnesi:dequeue split-sequence:split-sequence))
(use-package :cl-match)
(arnesi:enable-sharp-l)

(defvar *maze-str*
"**************************
*S* *                    *

einblicker

(require :cl-lex)
(require :yacc)
(require :arnesi)
(use-package :cl-lex)
(use-package :yacc)
(arnesi:enable-sharp-l)

(defun str->sym (str) 
  (values (intern (string-upcase str))))

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>

einblicker

methodName = "append"

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

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

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

|- 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

|- 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 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 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)] |-