brendanzab

use std::hash::Hash;

pub trait Key {
  type T: Hash + Eq;
}

pub trait Map<K : Key> {
  type T<V>;

  fn new<V>() -> Self::T<V>;

brendanzab

(** Fractal binary trees

    L-systems are a really wonderful model of plant growth, showing how a set of
    simple grammar rules can result in incredibly life-like and complicated
    organic forms.

    They do however seem a little… stuck in the 80s? In L-systems the state of a
    plant is modelled as a list of instructions, where the branching structure
    emerges from an imperative interpretation of “push” and “pop” symbols. For
    example an L-system that describes a fractal binary tree looks like this:

brendanzab

(*
  T ::=
    | Bool
    | T -> T

  t ::=
    | x
    | \(x : T). t
    | t t

brendanzab

// Syntax

pub enum Expr {
  Int(i32),
  Neg(Box<Expr>),
  Add(Box<Expr>, Box<Expr>),
  Mul(Box<Expr>, Box<Expr>),
}

// Semantics

brendanzab

(** Phrase generator based on an example from the Grammatical Framework tutorial.

  - {{:https://okmij.org/ftp/gengo/NASSLLI10/}
    Lambda: the ultimate syntax-semantics interface}
  - {{:https://www.grammaticalframework.org/doc/tutorial/gf-tutorial.html#toc16}
    Grammatical Framework Tutorial: Lesson 2}

  Todo:

  - generate languages (orthographies, vacabularies, grammars)

brendanzab

(** An elaborator for a simply typed lambda calculus with mutable metavars.

    This implementation is based on Arad Arbel’s gist:
    https://gist.github.com/aradarbel10/837aa65d2f06ac6710c6fbe479909b4c
*)

module Core = struct

  (** {1 Types} *)

brendanzab

//! Bidirectional type checker for a simple functional language

use std::rc::Rc;

#[derive(Clone, PartialEq, Eq)]
enum Type {
    Bool,
    Int,
    Fun(Rc<Type>, Rc<Type>),
}

brendanzab

module IndexedMonad = struct

  module type S = sig

    type ('i, 'a) t

    val pure : 'a -> (_, 'a) t
    val bind : ('i, 'a) t -> ('a -> ('i, 'b) t) -> ('i, 'b) t

  end

brendanzab

(** {0 An implementation of a small dependently typed language}

    This is an implementation simple dependently typed language where types are
    first-class and where the output types of functions may depend on the inputs
    supplied to them.

    Type checking is is implemented in terms of an {i elaborator}, which checks
    and tanslates a user-friendly {i surface language} into a simpler and more
    explicit {i core language} that is more closely connected to type theory.
    Because we need to simplify types during elaboration we also implement an

brendanzab

(** {0 Elaboration with Record Patching and Singleton Types}

    This is a small implementation of a dependently typed language with
    dependent record types, with some additional features intended to make it
    more convenient to use records as first-class modules. It was originally
    ported from {{: https://gist.github.com/mb64/04315edd1a8b1b2c2e5bd38071ff66b5}
    a gist by mb64}.

    The type system is implemented in terms of an ‘elaborator’, which type
    checks and tanslates a user-friendly surface language into a simpler and