Brendan Zabarauskas brendanzab

## eval_lc_secd_deconstruction.ml
(** Interpreters based on the SECD machine from “A Rational Deconstruction of Landin's SECD Machine”

    - Olivier Danvy. 2003. A Rational Deconstruction of Landin’s SECD Machine.
      BRICS Report Series 33 (October 2003). https://doi.org/10.7146/brics.v10i33.21801
*)

module Source = struct

  type ident = string

## eval_stlc.pol
use "../std/data/bool.pol"
use "../std/data/nat.pol"

data Ty {
    FunTy(a b: Ty),
    NatTy,
    BoolTy,
}

data Ctx {

## set.pol
data Bool { T, F }

data Nat { Z, S(n: Nat) }

def (n1: Nat).eq(n2: Nat): Bool {
    Z => n2.match {
        Z => T,
        S(_) => F,
    },
    S(n1) => n2.match {

## intuitionistic.elf
%% Intuitionistic type theory in Twelf by Brendan Zabarauskas
%%
%% Inspired by the examples found in “An Equational Logical Framework
%% for Type Theories” https://arxiv.org/abs/2106.01484

tp : type.
el : tp -> type.

%% Equality

## isorecursion_vs_equirecursion.ml
module type Isorecursive = sig

  type t
  type 'a layer

  val roll : t layer -> t
  val unroll : t -> t layer

end

## option_shapes.ml
module Option = struct

  type 'a shape = [
    | `Some of 'a
    | `None
  ]

  module type S = sig

    type 'a t

## ast_folds.ml
module Expr = struct

  module Layer = struct

    type 'a t =
      | Mul of 'a * 'a
      | Add of 'a * 'a
      | Int of int

    let map (f : 'a -> 'b) (layer : 'a t) : 'b t =

## eval_stmts_cps.ml
(** An evaluator for an imperative language with loop, break, and continue in
    continuation passing style. *)

type expr =
  | Var of string
  | Let of string * expr * expr
  | Seq of expr * expr

  | Unit

## lambda_nbe.ml
type index = int
type level = int


type expr =
  | Var of index
  | Let of string * expr * expr
  | Fun_lit of string * expr
  | Fun_app of expr * expr

## set_objects.ml
(** Set examples in OCaml from {{:https://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf}
    “On Understanding Data Abstraction, Revisited”} by William R. Cook
*)

(** ADT-style set implementations.

    See Section 2 of the paper.
*)
module Abstract_data_types = struct
	(** Interpreters based on the SECD machine from “A Rational Deconstruction of Landin's SECD Machine”

	- Olivier Danvy. 2003. A Rational Deconstruction of Landin’s SECD Machine.
	BRICS Report Series 33 (October 2003). https://doi.org/10.7146/brics.v10i33.21801
	*)

	module Source = struct

	type ident = string
	use "../std/data/bool.pol"
	use "../std/data/nat.pol"

	data Ty {
	FunTy(a b: Ty),
	NatTy,
	BoolTy,
	}

	data Ctx {
	data Bool { T, F }

	data Nat { Z, S(n: Nat) }

	def (n1: Nat).eq(n2: Nat): Bool {
	Z => n2.match {
	Z => T,
	S(_) => F,
	},
	S(n1) => n2.match {
	%% Intuitionistic type theory in Twelf by Brendan Zabarauskas
	%%
	%% Inspired by the examples found in “An Equational Logical Framework
	%% for Type Theories” https://arxiv.org/abs/2106.01484

	tp : type.
	el : tp -> type.

	%% Equality
	module type Isorecursive = sig

	type t
	type 'a layer

	val roll : t layer -> t
	val unroll : t -> t layer

	end
	module Option = struct

	type 'a shape = [
	\| `Some of 'a
	\| `None
	]

	module type S = sig

	type 'a t
	module Expr = struct

	module Layer = struct

	type 'a t =
	\| Mul of 'a * 'a
	\| Add of 'a * 'a
	\| Int of int

	let map (f : 'a -> 'b) (layer : 'a t) : 'b t =
	(** An evaluator for an imperative language with loop, break, and continue in
	continuation passing style. *)

	type expr =
	\| Var of string
	\| Let of string * expr * expr
	\| Seq of expr * expr

	\| Unit
	type index = int
	type level = int


	type expr =
	\| Var of index
	\| Let of string * expr * expr
	\| Fun_lit of string * expr
	\| Fun_app of expr * expr
	(** Set examples in OCaml from {{:https://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf}
	“On Understanding Data Abstraction, Revisited”} by William R. Cook
	*)

	(** ADT-style set implementations.

	See Section 2 of the paper.
	*)
	module Abstract_data_types = struct