| ?- set_prolog_flag(occurs_check,true). | |
| lookup([(X,A)|_],X,A). | |
| lookup([(Y,_)|T],X,A) :- \+ X = Y, lookup(T,X,A). | |
| /* Rules from the STLC lecture */ | |
| pred(D,DD) :- D >= 0, DD is D - 1. | |
| type(_,u,unit,D) :- pred(D,_). |
| From ocaml/opam2 | |
| RUN sudo apt update | |
| RUN sudo apt install -y m4 perl libgmp-dev pkg-config | |
| RUN opam remote add upstream https://opam.ocaml.org && \ | |
| opam update && opam upgrade | |
| RUN git clone https://github.com/mirage/irmin | |
| WORKDIR irmin | |
| RUN opam pin add -k git -n irmin . && \ | |
| opam pin add -k git -n irmin-unix . && \ | |
| opam pin add -k git -n irmin-fs . && \ |
This document contains instructions for the artefact evaluation. The draft paper is available at kcsrk.info/papers/pldi18-memory.pdf.
The main evaluation in the paper is the overhead of compiling our proposed memory model to relaxed architectures such as ARM and POWER (Fig 7 on page 10).
| (* Reverse-mode algorithmic differentiation using effect handlers. | |
| Adapted from https://twitter.com/tiarkrompf/status/963314799521222656. | |
| See https://openreview.net/forum?id=SJxJtYkPG for more information. *) | |
| module F = struct | |
| type t = { v : float; mutable d : float } | |
| let mk v = {v; d = 0.0} | |
| effect Plus : t * t -> t |
| (* GC stress/performance test. | |
| Uses only core GC features - no finalisers, weak references, etc. *) | |
| type work = F : (int -> 'a) * ('a -> int) -> work | |
| type bintree = Leaf of int | Branch of bintree * bintree | |
| let tree = | |
| let rec mktree = function | |
| | 0 -> Leaf 1 | |
| | n -> Branch (mktree (n-1), mktree (n-1)) in |
| (* Requires: OCaml 4.03.0+ *) | |
| (* Usage: `ocaml eff.ml` *) | |
| (** Identifiers *) | |
| module Ident = struct | |
| type t = string | |
| let id = ref 0 | |
| let create base = |
| /***********************************************************************/ | |
| /* */ | |
| /* OCaml */ | |
| /* */ | |
| /* Xavier Leroy and Damien Doligez, INRIA Rocquencourt */ | |
| /* */ | |
| /* Copyright 2009 Institut National de Recherche en Informatique et */ | |
| /* en Automatique. All rights reserved. This file is distributed */ | |
| /* under the terms of the GNU Library General Public License, with */ | |
| /* the special exception on linking described in file ../../LICENSE. */ |
| module type Handler = sig | |
| type effect = .. | |
| type 'a t | |
| type cont | |
| val return : 'a -> 'a t | |
| val (>>=) : 'a t -> ('a -> 'b t) -> 'b t | |
| val run : unit t -> unit | |
| val handle : 'a t -> (effect -> cont -> unit t) -> unit t | |
| val continue : cont -> unit t |
| ## Docker file for OCaml with GDB support | |
| # | |
| # Build | |
| # ----- | |
| # $ mkdir monda-docker | |
| # $ cp <this_file> monda-docker/ | |
| # $ docker build --force-rm=true -t monda . | |
| # ..takes a while.. | |
| # | |
| # Run |
| ## Docker file for OCaml with GDB support | |
| # | |
| # Build | |
| # ----- | |
| # $ mkdir monda-docker | |
| # $ cp <this_file> monda-docker/ | |
| # $ docker build --force-rm=true -t monda . | |
| # ..takes a while.. | |
| # | |
| # Run |
