basic.mz

(* This is just a sample file. Try changing menhir to menhir --trace in the
 * Makefile to see the tokens being accepted and/or rejected. *)
data t a =
  | Foo
  | Bar {
    baz: a;
  }

and tree a =
  | Leaf
  | Node {
      datum: a;
      left: tree a;
      right: tree a
    }

and ty = DummyType

and typechecker =
  TC { typechecker: [a] (consumes t: tree a) -> (ty | t @ tree ty) }

and list a =
  | Cons { head: a; tail: list a }
  | Nil

and listops =
  ListOps {
    length0: [a] (x: list a) -> int;
    length1: [a] (consumes xs: list a) -> (result: int | xs @ list a); (* more explicit form *)
    length2: [a] (consumes xs: unknown | consumes xs @ list a) ->
                (result: int | xs @ list a); (* even more explicit form *)
    find: [key, a] (* duplicable a => *) (list (key, a), (key, key) -> bool, key) -> a;
    concat: [a] (consumes l1: list a, consumes l2: list a) -> (l3: list a)
  }

val x = ()

data mutable foo a b c =
  Foo {
    bar: a;
    baz: baz b c a;
  }

and baz a b c =
  Baz {
    foo: foo a b c;
  }

and v α = V {
  foo: u α;
}

and u α = U {
  bar: α;
  baz: v α;
}

(* The example discussed on the board. Takes three rounds to get to the
 * fixpoint. *)
and t1 a b = T1 {
  foo: t2 a b;
}

and t2 a b = T2 {
  bar: t1 (a, b) b;
  baz: a;
}

(* Only b and d should be constrained. *)
and odd a b c d = S { foo: b; bar: d }

(* [list_of_refs] should be affine *)
and mutable ref a = Ref { contents: a }
and list_refs a = L { list: list (ref a) }

(* and not_well_kinded container a = N { contents: container a; } *)

and should_be_dup a = D {
  foo: Nil;
  bar: a;
  foo2: Cons { head: a; tail: list a };
}

and should_be_aff a = A {
  foo: Cons { head: ref a; tail: list (ref a) };
}

and mutable noparams = NoParams
and aff = Whatever { whatever: noparams; }