Guest0x0

type type_name = string
type var = string

type term =
  | Atom of { type_name : type_name }
  | Var of var
  | Lam of var * term
  | App of term * term

Guest0x0

type op = Add | Sub

type expr =
  | Lit of int
  | Op  of expr * op * expr

type result =
  | Val of int
  | Term of expr

Guest0x0

module type Reduction_Theory = sig
  type term
  type value
  type redex

  val v2t : value -> term
  val contract : redex -> term option

  (* an elementary context is a single frame of elemetary context,

Guest0x0

type op = Add | Sub

type expr =
  | Lit of int
  | Op  of expr * op * expr

type result =
  | Val of int
  | Term of expr
  | Stuck

Guest0x0

(* HAMT v.s. AVL benchmark.

   test for their usage as string map.

   usage:
   > ocamlopt HAMT.ml -o <executable-name>
   > <executable-name> (avl|hamt) (random|ordered) <key-length>

   time data of the form:
     <tree-size> <add-time> <find-time>

Guest0x0

(* 这是我（预期，亦或是已经）在 ∞-type càfe summer school 上做的 talk，

     "从零教你手把手实现一个 MLTT 类型检查器"

   的内容稿。本 talk 计划以现场边讲解边手写代码的方式实现，
   所以虽然这份内容稿会尽量尝试还原 talk 的思路和逻辑，
   它的内容可能会与实际的 talk 有出入，建议有条件的人直接去听 talk 本身 *)

(* 本次 talk 将会使用 OCaml 来实现一个 MLTT 类型检查器。
   你可能不会写 OCaml，但这没有关系。本次 talk 只会使用以下的功能：

Guest0x0

(* a minimal pattern-matching compiler *)

(* use integer as variable for easy generation *)
type var = int

type typename = string
type constructor = string


type typ =

Guest0x0

module Src = struct
    type expr =
        | Int of int
        | Var of string
        | Op  of string * expr * expr
        | Let of string * expr * expr
        | If  of expr * expr * expr
end

Guest0x0

module Src = struct
    type expr =
        | Int of int
        | Var of string
        | Op  of string * expr * expr
        | Let of string * expr * expr
        | If  of expr * expr * expr
end