hirrolot

type cps_var =
  (* Taken from the lambda term during CPS conversion. *)
  | CLamVar of string
  (* Generated uniquely during CPS conversion. *)
  | CGenVar of int

type cps_term =
  | CFix of (cps_var * cps_var list * cps_term) list * cps_term
  | CAppl of cps_var * cps_var list
  | CRecord of cps_var list * binder

hirrolot

(* A variable identifier of the lambda language [term]. *)
type var = string [@@deriving eq]

(* The lambda language; direct style. *)
type term =
  | Var of var
  | Fix of (var * var list * term) list * term
  | Appl of term * term list
  | Record of term list
  | Select of term * int

gabriel-fallen

namespace ADTs

/-
  In the game we have two banks of a river: left and right,
  and four characters: a wolf, a goat, a cabbage, and a farmer.
  The farmer prevents abybody from eathing anything, otherweise
  the wolf eats the goat, or the goat eats the cabbage.
  The game starts with all the characters on the left bank and
  the goal is to move everyone to the right bank safe and sound.
  The farmer can carry a single other character at a time

AndrasKovacs

{-# language BlockArguments, LambdaCase, Strict, UnicodeSyntax #-}

{-|
Minimal dependent lambda caluclus with:
  - HOAS-only representation
  - Lossless printing
  - Bidirectional checking
  - Efficient evaluation & conversion checking

Inspired by https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196

hirrolot

type term =
  | Lam of (term -> term)
  | Pi of term * (term -> term)
  | Appl of term * term
  | Ann of term * term
  | FreeVar of int
  | Star
  | Box

let unfurl lvl f = f (FreeVar lvl)

hirrolot

type term = Lam of (term -> term) | Appl of term * term | FreeVar of int

let unfurl lvl f = f (FreeVar lvl)
let unfurl2 lvl (f, g) = (unfurl lvl f, unfurl lvl g)

let rec print lvl =
  let plunge f = print (lvl + 1) (unfurl lvl f) in
  function
  | Lam f -> "(λ" ^ plunge f ^ ")"
  | Appl (m, n) -> "(" ^ print lvl m ^ " " ^ print lvl n ^ ")"

hirrolot

module type Form = sig
  type ('env, 'a) meaning

  val vz : ('a * 'env, 'a) meaning
  val vs : ('env, 'a) meaning -> ('b * 'env, 'a) meaning
  val lam : ('a * 'env, 'b) meaning -> ('env, 'a -> 'b) meaning

  val appl :
    ('env, 'a -> 'b) meaning -> ('env, 'a) meaning -> ('env, 'b) meaning
end

hirrolot

module type Form = sig
  type 'a meaning

  val lam : ('a meaning -> 'b meaning) -> ('a -> 'b) meaning
  val appl : ('a -> 'b) meaning -> 'a meaning -> 'b meaning
end

(* Evaluate a given term. *)
module Eval = struct
  type 'a meaning = 'a

hirrolot

let lam f = f
let appl f x = f x

hirrolot

let rec eval = function
  | `Appl (m, n) -> (
      let n' = eval n in
      match eval m with `Lam f -> eval (f n') | m' -> `Appl (m', n'))
  | (`Lam _ | `Var _) as t -> t

let sprintf = Printf.sprintf

(* Print a given term using De Bruijn levels. *)
let rec pp lvl = function