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