source.ml.ref

[@@@foo]

let (x [@foo]) : (unit[@foo]) = () [@foo] [@@foo]

type t = Foo of (t[@foo]) [@foo] [@@foo]

[@@@foo]

module M = struct
  type t = { l : (t[@foo]) [@foo] } [@@foo] [@@foo]

  [@@@foo]
end [@foo]
[@@foo]

module type S = sig
  include ((module type of M [@foo]) [@foo] with type t := M.t [@foo]) [@@foo]

  [@@@foo]
end [@foo]
[@@foo]

[@@@foo]

type 'a with_default =
  ?size:int (** default [42] *) -> ?resizable:bool (** default [true] *) -> 'a

type obj =
  < meth1 : int -> int  (** method 1 *)
  ; meth2 : unit -> float  (** method 2 *) >

type var = [ `Foo  (** foo *) | `Bar of int * string  (** bar *) ]

[%%foo
let x = 1 in
x]

let [%foo 2 + 1] : [%foo bar.baz] = [%foo "foo"]

[%%foo module M = [%bar]]

let [%foo let () = ()] : [%foo type t = t] = [%foo class c = object end]

[%%foo: 'a list]

let [%foo: [ `Foo ]] : [%foo: t -> t] = [%foo: < foo : t > ]

[%%foo? _]
[%%foo? Some y when y > 0]

let [%foo? Bar x | Baz x] : [%foo? #bar] = [%foo? { x }]

[%%foo: module M : [%baz]]

let [%foo: include S with type t = t] :
    [%foo:
      val x : t
      val y : t] =
  [%foo: type t = t]

let int_with_custom_modifier =
  1234567890_1234567890_1234567890_1234567890_1234567890z

let float_with_custom_modifier =
  1234567890_1234567890_1234567890_1234567890_1234567890.z

let int32 = 1234l
let int64 = 1234L
let nativeint = 1234n
let hex_without_modifier = 0x32f
let hex_with_modifier = 0x32g
let float_without_modifer = 1.2e3
let float_with_modifer = 1.2g
let%foo x = 42

let%foo _ = ()
and _ = ()

let%foo _ = ()

(* Expressions *)
let () =
  let%foo[@foo] x = 3 and[@foo] y = 4 in
  (let module%foo [@foo] M = M in
   ());
  (let open%foo [@foo] M in
   ());
  (fun%foo[@foo] x -> ());
  (function%foo[@foo] x -> ());
  (try%foo[@foo] () with _ -> ());
  if%foo[@foo] () then () else ();
  while%foo[@foo] () do () done;
  for%foo[@foo] x = () to () do
    ()
  done;
  assert%foo[@foo] true;
  lazy%foo[@foo] x;
  object%foo[@foo] end;
  begin%foo[@foo]
    3
  end;
  new%foo[@foo] x;

  match%foo[@foo] () with
  | [%foo?
      (* Pattern expressions *)
      ((lazy x) [@foo])] ->
      ()
  | [%foo? ((exception x) [@foo])] -> ()
  | effect x, k -> ()

(* Class expressions *)
class x =
  fun [@foo] x ->
  let[@foo] x = 3 in
  object
    inherit x [@@foo]
    val x = 3 [@@foo]
    val virtual x : t [@@foo]
    val! mutable x = 3 [@@foo]
    method x = 3 [@@foo]
    method virtual x : t [@@foo]
    method! private x = 3 [@@foo]
    initializer x [@@foo]
  end
  [@foo]

(* Class type expressions *)
class type t = object
  inherit t [@@foo]
  val x : t [@@foo]
  val mutable x : t [@@foo]
  method x : t [@@foo]
  method private x : t [@@foo]
  constraint t = t' [@@foo]
  [@@@abc]
  [%%id]
  [@@@aaa]
end[@foo]

(* Type expressions *)
type t = [%foo: ((module M)[@foo])]

(* Module expressions *)
module M = (functor [@foo] (M : S) -> (val x) [@foo] (struct end [@foo]))

(* Module type expression *)
module type S = functor [@foo] (M : S) -> (module type of M) [@foo] -> sig end
[@foo]

module type S = S -> S -> S
module type S = (S -> S) -> S
module type S = functor (M : S) -> S -> S
module type S = (functor (M : S) -> S) -> S
module type S = (S -> S) [@foo] -> S
module type S = (functor [@foo] (M : S) -> S) -> S

module type S = sig
  module rec A : (S with type t = t)
  and B : (S with type t = t)
end

(* Structure items *)
let%foo[@foo] x = 4
and[@foo] y = x

type%foo[@foo] t = int
and[@foo] t = int

type%foo [@foo] t += T
type t += A = M.A [@a]
type t += B = M.A [@b] | C = M.A [@c] [@@t]

class%foo [@foo] x = x

class type%foo [@foo] x = x

external%foo [@foo] x : _ = ""

exception%foo [@foo] X
exception A = M.A [@a]

module%foo [@foo] M = M

module%foo [@foo] rec M : S = M
and [@foo] M : S = M

module type%foo [@foo] S = S

include%foo [@foo] M
open%foo [@foo] M

(* Signature items *)
module type S = sig
  val%foo [@foo] x : t
  external%foo [@foo] x : t = ""

  type%foo[@foo] t = int
  and[@foo] t' = int

  type%foo [@foo] t += T

  exception%foo [@foo] X

  module%foo [@foo] M : S

  module%foo [@foo] rec M : S
  and [@foo] M : S

  module%foo [@foo] M = M

  module type%foo [@foo] S = S

  include%foo [@foo] M
  open%foo [@foo] M

  class%foo [@foo] x : t

  class type%foo [@foo] x = x
end

type t = ..
type t += A;;

[%extension_constructor A];;
([%extension_constructor A] : extension_constructor);;

module M = struct
  type extension_constructor = int
end

open M;;

([%extension_constructor A] : extension_constructor);;

(* By using two types we can have a recursive constraint *)
type 'a class_name = .. constraint 'a = < cast : 'a. 'a name -> 'a ; .. >

and 'a name =
  | Class : 'a class_name -> (< cast : 'a. 'a name -> 'a ; .. > as 'a) name

exception Bad_cast

class type castable = object
  method cast : 'a. 'a name -> 'a
end

(* Lets create a castable class with a name*)

class type foo_t = object
  inherit castable
  method foo : string
end

type 'a class_name += Foo : foo_t class_name

class foo : foo_t =
  object (self)
    method cast : type a. a name -> a =
      function Class Foo -> (self :> foo_t) | _ -> (raise Bad_cast : a)

    method foo = "foo"
  end

(* Now we can create a subclass of foo *)

class type bar_t = object
  inherit foo
  method bar : string
end

type 'a class_name += Bar : bar_t class_name

class bar : bar_t =
  object (self)
    inherit foo as super

    method cast : type a. a name -> a =
      function Class Bar -> (self :> bar_t) | other -> super#cast other

    method bar = "bar"
    [@@@id]
    [%%id]
  end

(* Now lets create a mutable list of castable objects *)

let clist : castable list ref = ref []
let push_castable (c : #castable) = clist := (c :> castable) :: !clist

let pop_castable () =
  match !clist with
  | c :: rest ->
      clist := rest;
      c
  | [] -> raise Not_found
;;

(* We can add foos and bars to this list, and retrieve them *)

push_castable (new foo);;
push_castable (new bar);;
push_castable (new foo);;

let c1 : castable = pop_castable ()
let c2 : castable = pop_castable ()
let c3 : castable = pop_castable ()

(* We can also downcast these values to foos and bars *)

let f1 : foo = c1#cast (Class Foo)

(* Ok *)
let f2 : foo = c2#cast (Class Foo)

(* Ok *)
let f3 : foo = c3#cast (Class Foo)

(* Ok *)

let b1 : bar = c1#cast (Class Bar)

(* Exception Bad_cast *)
let b2 : bar = c2#cast (Class Bar)

(* Ok *)
let b3 : bar = c3#cast (Class Bar)

(* Exception Bad_cast *)

type foo = ..
type foo += A | B of int

let is_a x = match x with A -> true | _ -> false

(* The type must be open to create extension *)

type foo
type foo += A of int (* Error type is not open *)

(* The type parameters must match *)

type 'a foo = ..
type ('a, 'b) foo += A of int (* Error: type parameter mismatch *)

(* In a signature the type does not have to be open *)

module type S = sig
  type foo
  type foo += A of float
end

(* But it must still be extensible *)

module type S = sig
  type foo = A of int
  type foo += B of float (* Error foo does not have an extensible type *)
end

(* Signatures can change the grouping of extensions *)

type foo = ..

module M = struct
  type foo += A of int | B of string
  type foo += C of int | D of float
end

module type S = sig
  type foo += B of string | C of int
  type foo += D of float
  type foo += A of int
end

module M_S : S = M

(* Extensions can be GADTs *)

type 'a foo = ..
type _ foo += A : int -> int foo | B : int foo

let get_num : type a. a foo -> a -> a option =
 fun f i1 -> match f with A i2 -> Some (i1 + i2) | _ -> None

(* Extensions must obey constraints *)

type 'a foo = .. constraint 'a = [> `Var ]
type 'a foo += A of 'a

let a = A 9 (* ERROR: Constraints not met *)

type 'a foo += B : int foo (* ERROR: Constraints not met *)

(* Signatures can make an extension private *)

type foo = ..

module M = struct
  type foo += A of int
end

let a1 = M.A 10

module type S = sig
  type foo += private A of int
end

module M_S : S = M

let is_s x = match x with M_S.A _ -> true | _ -> false
let a2 = M_S.A 20 (* ERROR: Cannot create a value using a private constructor *)

(* Extensions can be rebound *)

type foo = ..

module M = struct
  type foo += A1 of int
end

type foo += A2 = M.A1
type bar = ..
type bar += A3 = M.A1 (* Error: rebind wrong type *)

module M = struct
  type foo += private B1 of int
end

type foo += private B2 = M.B1
type foo += B3 = M.B1 (* Error: rebind private extension *)
type foo += C = Unknown (* Error: unbound extension *)

(* Extensions can be rebound even if type is closed *)

module M : sig
  type foo
  type foo += A1 of int
end = struct
  type foo = ..
  type foo += A1 of int
end

type M.foo += A2 = M.A1

(* Rebinding handles abbreviations *)

type 'a foo = ..
type 'a foo1 = 'a foo = ..
type 'a foo2 = 'a foo = ..
type 'a foo1 += A of int | B of 'a | C : int foo1
type 'a foo2 += D = A | E = B | F = C

(* Extensions must obey variances *)

type +'a foo = ..
type 'a foo += A of (int -> 'a)
type 'a foo += B of ('a -> int)
(* ERROR: Parameter variances are not satisfied *)

type _ foo += C : ('a -> int) -> 'a foo
(* ERROR: Parameter variances are not satisfied *)

type 'a bar = ..
type +'a bar += D of (int -> 'a) (* ERROR: type variances do not match *)

(* Exceptions are compatible with extensions *)

module M : sig
  type exn += Foo of int * float | Bar : 'a list -> exn
end = struct
  exception Bar : 'a list -> exn
  exception Foo of int * float
end

module M : sig
  exception Bar : 'a list -> exn
  exception Foo of int * float
end = struct
  type exn += Foo of int * float | Bar : 'a list -> exn
end

exception Foo of int * float
exception Bar : 'a list -> exn

module M : sig
  type exn += Foo of int * float | Bar : 'a list -> exn
end = struct
  exception Bar = Bar
  exception Foo = Foo
end

(* Test toplevel printing *)

type foo = ..
type foo += Foo of int * int option | Bar of int option

let x = (Foo (3, Some 4), Bar (Some 5)) (* Prints Foo and Bar successfully *)

type foo += Foo of string

let y = x (* Prints Bar but not Foo (which has been shadowed) *)

exception Foo of int * int option
exception Bar of int option

let x = (Foo (3, Some 4), Bar (Some 5)) (* Prints Foo and Bar successfully *)

type foo += Foo of string

let y = x (* Prints Bar and part of Foo (which has been shadowed) *)

(* Test Obj functions *)

type foo = ..
type foo += Foo | Bar of int

let extension_name e = Obj.extension_name (Obj.extension_constructor e)
let extension_id e = Obj.extension_id (Obj.extension_constructor e)
let n1 = extension_name Foo
let n2 = extension_name (Bar 1)
let t = extension_id (Bar 2) = extension_id (Bar 3) (* true *)
let f = extension_id (Bar 2) = extension_id Foo (* false *)
let is_foo x = extension_id Foo = extension_id x

type foo += Foo

let f = is_foo Foo
let _ = Obj.extension_constructor 7 (* Invald_arg *)

let _ =
  Obj.extension_constructor
    object
      method m = 3
    end
(* Invald_arg *)

(* Typed names *)

module Msg : sig
  type 'a tag
  type result = Result : 'a tag * 'a -> result

  val write : 'a tag -> 'a -> unit
  val read : unit -> result

  type 'a tag += Int : int tag

  module type Desc = sig
    type t

    val label : string
    val write : t -> string
    val read : string -> t
  end

  module Define (D : Desc) : sig
    type 'a tag += C : D.t tag
  end
end = struct
  type 'a tag = ..
  type ktag = T : 'a tag -> ktag

  type 'a kind = {
    tag : 'a tag;
    label : string;
    write : 'a -> string;
    read : string -> 'a;
  }

  type rkind = K : 'a kind -> rkind
  type wkind = { f : 'a. 'a tag -> 'a kind }

  let readTbl : (string, rkind) Hashtbl.t = Hashtbl.create 13
  let writeTbl : (ktag, wkind) Hashtbl.t = Hashtbl.create 13
  let read_raw () : string * string = raise (Failure "Not implemented")

  type result = Result : 'a tag * 'a -> result

  let read () =
    let label, content = read_raw () in
    let (K k) = Hashtbl.find readTbl label in
    let body = k.read content in
    Result (k.tag, body)

  let write_raw (label : string) (content : string) =
    raise (Failure "Not implemented")

  let write (tag : 'a tag) (body : 'a) =
    let { f } = Hashtbl.find writeTbl (T tag) in
    let k = f tag in
    let content = k.write body in
    write_raw k.label content

  (* Add int kind *)

  type 'a tag += Int : int tag

  let ik =
    { tag = Int; label = "int"; write = Int.to_string; read = int_of_string }

  let () = Hashtbl.add readTbl "int" (K ik)

  let () =
    let f (type t) (i : t tag) : t kind =
      match i with Int -> ik | _ -> assert false
    in
    Hashtbl.add writeTbl (T Int) { f }

  (* Support user defined kinds *)

  module type Desc = sig
    type t

    val label : string
    val write : t -> string
    val read : string -> t
  end

  module Define (D : Desc) = struct
    type 'a tag += C : D.t tag

    let k = { tag = C; label = D.label; write = D.write; read = D.read }
    let () = Hashtbl.add readTbl D.label (K k)

    let () =
      let f (type t) (c : t tag) : t kind =
        match c with C -> k | _ -> assert false
      in
      Hashtbl.add writeTbl (T C) { f }
  end
end

let write_int i = Msg.write Msg.Int i

module StrM = Msg.Define (struct
  type t = string

  let label = "string"
  let read s = s
  let write s = s
end)

type 'a Msg.tag += String = StrM.C

let write_string s = Msg.write String s

let read_one () =
  let (Msg.Result (tag, body)) = Msg.read () in
  match tag with
  | Msg.Int -> print_int body
  | String -> print_string body
  | _ -> print_string "Unknown"

(* Example of algorithm parametrized with modules *)

let sort (type s) set l =
  let module Set = (val set : Set.S with type elt = s) in
  Set.elements (List.fold_right Set.add l Set.empty)

let make_set (type s) cmp =
  let module S = Set.Make (struct
    type t = s

    let compare = cmp
  end) in
  (module S : Set.S with type elt = s)

let both l =
  List.map
    (fun set -> sort set l)
    [ make_set compare; make_set (fun x y -> compare y x) ]

let () =
  print_endline
    (String.concat "  "
       (List.map (String.concat "/") (both [ "abc"; "xyz"; "def" ])))

(* Hiding the internal representation *)

module type S = sig
  type t

  val to_string : t -> string
  val apply : t -> t
  val x : t
end

let create (type s) to_string apply x =
  let module M = struct
    type t = s

    let to_string = to_string
    let apply = apply
    let x = x
  end in
  (module M : S with type t = s)

let forget (type s) x =
  let module M = (val x : S with type t = s) in
  (module M : S)

let print x =
  let module M = (val x : S) in
  print_endline (M.to_string M.x)

let apply x =
  let module M = (val x : S) in
  let module N = struct
    include M

    let x = apply x
  end in
  (module N : S)

let () =
  let int = forget (create Int.to_string succ 0) in
  let str = forget (create (fun s -> s) (fun s -> s ^ s) "X") in
  List.iter print (List.map apply [ int; apply int; apply (apply str) ])

(* Existential types + type equality witnesses -> pseudo GADT *)

module TypEq : sig
  type ('a, 'b) t

  val apply : ('a, 'b) t -> 'a -> 'b
  val refl : ('a, 'a) t
  val sym : ('a, 'b) t -> ('b, 'a) t
end = struct
  type ('a, 'b) t = unit

  let apply _ = Obj.magic
  let refl = ()
  let sym () = ()
end

module rec Typ : sig
  module type PAIR = sig
    type t
    type t1
    type t2

    val eq : (t, t1 * t2) TypEq.t
    val t1 : t1 Typ.typ
    val t2 : t2 Typ.typ
  end

  type 'a typ =
    | Int of ('a, int) TypEq.t
    | String of ('a, string) TypEq.t
    | Pair of (module PAIR with type t = 'a)
end = struct
  module type PAIR = sig
    type t
    type t1
    type t2

    val eq : (t, t1 * t2) TypEq.t
    val t1 : t1 Typ.typ
    val t2 : t2 Typ.typ
  end

  type 'a typ =
    | Int of ('a, int) TypEq.t
    | String of ('a, string) TypEq.t
    | Pair of (module PAIR with type t = 'a)
end

open Typ

let int = Int TypEq.refl
let str = String TypEq.refl

let pair (type s1) (type s2) t1 t2 =
  let module P = struct
    type t = s1 * s2
    type t1 = s1
    type t2 = s2

    let eq = TypEq.refl
    let t1 = t1
    let t2 = t2
  end in
  let pair = (module P : PAIR with type t = s1 * s2) in
  Pair pair

module rec Print : sig
  val to_string : 'a Typ.typ -> 'a -> string
end = struct
  let to_string (type s) t x =
    match t with
    | Int eq -> Int.to_string (TypEq.apply eq x)
    | String eq -> Printf.sprintf "%S" (TypEq.apply eq x)
    | Pair p ->
        let module P = (val p : PAIR with type t = s) in
        let x1, x2 = TypEq.apply P.eq x in
        Printf.sprintf "(%s,%s)" (Print.to_string P.t1 x1)
          (Print.to_string P.t2 x2)
end

let () =
  print_endline (Print.to_string int 10);
  print_endline (Print.to_string (pair int (pair str int)) (123, ("A", 456)))

(* #6262: first-class modules and module type aliases *)

module type S1 = sig end
module type S2 = S1

let _f (x : (module S1)) : (module S2) = x

module X = struct
  module type S
end

module Y = struct
  include X
end

let _f (x : (module X.S)) : (module Y.S) = x

(* PR#6194, main example *)
module type S3 = sig
  val x : bool
end

let f = function
  | Some (module M : S3) when M.x -> 1
  | ((Some _) [@foooo]) -> 2
  | None -> 3
;;

print_endline
  (Int.to_string
     (f
        (Some
           (module struct
             let x = false
           end))))
;;

type 'a ty = Int : int ty | Bool : bool ty

let fbool (type t) (x : t) (tag : t ty) = match tag with Bool -> x

(* val fbool : 'a -> 'a ty -> 'a = <fun> *)
(* * OK: the return value is x of type t **)

let fint (type t) (x : t) (tag : t ty) = match tag with Int -> x > 0

(* val fint : 'a -> 'a ty -> bool = <fun> *)
(* * OK: the return value is x > 0 of type bool;
This has used the equation t = bool, not visible in the return type **)

let f (type t) (x : t) (tag : t ty) = match tag with Int -> x > 0 | Bool -> x
(* val f : 'a -> 'a ty -> bool = <fun> *)

let g (type t) (x : t) (tag : t ty) = match tag with Bool -> x | Int -> x > 0
(* Error: This expression has type bool but an expression was expected of type
t = int *)

let id x = x

let idb1 =
  (fun id ->
    let _ = id true in
    id)
    id

let idb2 : bool -> bool = id
let idb3 (_ : bool) = false

let g (type t) (x : t) (tag : t ty) =
  match tag with Bool -> idb3 x | Int -> x > 0

let g (type t) (x : t) (tag : t ty) =
  match tag with Bool -> idb2 x | Int -> x > 0
(* Encoding generics using GADTs *)
(* (c) Alain Frisch / Lexifi *)
(* cf. http://www.lexifi.com/blog/dynamic-types *)

(* Basic tag *)

type 'a ty =
  | Int : int ty
  | String : string ty
  | List : 'a ty -> 'a list ty
  | Pair : ('a ty * 'b ty) -> ('a * 'b) ty

(* Tagging data *)

type variant =
  | VInt of int
  | VString of string
  | VList of variant list
  | VPair of variant * variant

let rec variantize : type t. t ty -> t -> variant =
 fun ty x ->
  (* type t is abstract here *)
  match ty with
  | Int -> VInt x (* in this branch: t = int *)
  | String -> VString x (* t = string *)
  | List ty1 ->
      VList (List.map (variantize ty1) x) (* t = 'a list for some 'a *)
  | Pair (ty1, ty2) -> VPair (variantize ty1 (fst x), variantize ty2 (snd x))
(* t = ('a, 'b) for some 'a and 'b *)

exception VariantMismatch

let rec devariantize : type t. t ty -> variant -> t =
 fun ty v ->
  match (ty, v) with
  | Int, VInt x -> x
  | String, VString x -> x
  | List ty1, VList vl -> List.map (devariantize ty1) vl
  | Pair (ty1, ty2), VPair (x1, x2) -> (devariantize ty1 x1, devariantize ty2 x2)
  | _ -> raise VariantMismatch

(* Handling records *)

type 'a ty =
  | Int : int ty
  | String : string ty
  | List : 'a ty -> 'a list ty
  | Pair : ('a ty * 'b ty) -> ('a * 'b) ty
  | Record : 'a record -> 'a ty

and 'a record = { path : string; fields : 'a field_ list }
and 'a field_ = Field : ('a, 'b) field -> 'a field_
and ('a, 'b) field = { label : string; field_type : 'b ty; get : 'a -> 'b }

(* Again *)

type variant =
  | VInt of int
  | VString of string
  | VList of variant list
  | VPair of variant * variant
  | VRecord of (string * variant) list

let rec variantize : type t. t ty -> t -> variant =
 fun ty x ->
  (* type t is abstract here *)
  match ty with
  | Int -> VInt x (* in this branch: t = int *)
  | String -> VString x (* t = string *)
  | List ty1 ->
      VList (List.map (variantize ty1) x) (* t = 'a list for some 'a *)
  | Pair (ty1, ty2) ->
      VPair (variantize ty1 (fst x), variantize ty2 (snd x))
      (* t = ('a, 'b) for some 'a and 'b *)
  | Record { fields } ->
      VRecord
        (List.map
           (fun (Field { field_type; label; get }) ->
             (label, variantize field_type (get x)))
           fields)

(* Extraction *)

type 'a ty =
  | Int : int ty
  | String : string ty
  | List : 'a ty -> 'a list ty
  | Pair : ('a ty * 'b ty) -> ('a * 'b) ty
  | Record : ('a, 'builder) record -> 'a ty

and ('a, 'builder) record = {
  path : string;
  fields : ('a, 'builder) field list;
  create_builder : unit -> 'builder;
  of_builder : 'builder -> 'a;
}

and ('a, 'builder) field =
  | Field : ('a, 'builder, 'b) field_ -> ('a, 'builder) field

and ('a, 'builder, 'b) field_ = {
  label : string;
  field_type : 'b ty;
  get : 'a -> 'b;
  set : 'builder -> 'b -> unit;
}

let rec devariantize : type t. t ty -> variant -> t =
 fun ty v ->
  match (ty, v) with
  | Int, VInt x -> x
  | String, VString x -> x
  | List ty1, VList vl -> List.map (devariantize ty1) vl
  | Pair (ty1, ty2), VPair (x1, x2) -> (devariantize ty1 x1, devariantize ty2 x2)
  | Record { fields; create_builder; of_builder }, VRecord fl ->
      if List.length fields <> List.length fl then raise VariantMismatch;
      let builder = create_builder () in
      List.iter2
        (fun (Field { label; field_type; set }) (lab, v) ->
          if label <> lab then raise VariantMismatch;
          set builder (devariantize field_type v))
        fields fl;
      of_builder builder
  | _ -> raise VariantMismatch

type my_record = { a : int; b : string list }

let my_record =
  let fields =
    [
      Field
        {
          label = "a";
          field_type = Int;
          get = (fun { a } -> a);
          set = (fun (r, _) x -> r := Some x);
        };
      Field
        {
          label = "b";
          field_type = List String;
          get = (fun { b } -> b);
          set = (fun (_, r) x -> r := Some x);
        };
    ]
  in
  let create_builder () = (ref None, ref None) in
  let of_builder (a, b) =
    match (!a, !b) with
    | Some a, Some b -> { a; b }
    | _ -> failwith "Some fields are missing in record of type my_record"
  in
  Record { path = "My_module.my_record"; fields; create_builder; of_builder }

(* Extension to recursive types and polymorphic variants *)
(* by Jacques Garrigue *)

type noarg = Noarg

type (_, _) ty =
  | Int : (int, _) ty
  | String : (string, _) ty
  | List : ('a, 'e) ty -> ('a list, 'e) ty
  | Option : ('a, 'e) ty -> ('a option, 'e) ty
  | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty
  (* Support for type variables and recursive types *)
  | Var : ('a, 'a -> 'e) ty
  | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty
  | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty
  (* Change the representation of a type *)
  | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty
  (* Sum types (both normal sums and polymorphic variants) *)
  | Sum : ('a, 'e, 'b) ty_sum -> ('a, 'e) ty

and ('a, 'e, 'b) ty_sum = {
  sum_proj : 'a -> string * 'e ty_dyn option;
  sum_cases : (string * ('e, 'b) ty_case) list;
  sum_inj : 'c. ('b, 'c) ty_sel * 'c -> 'a;
}

and 'e ty_dyn =
  (* dynamic type *)
  | Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn

and (_, _) ty_sel =
  (* selector from a list of types *)
  | Thd : ('a -> 'b, 'a) ty_sel
  | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel

and (_, _) ty_case =
  (* type a sum case *)
  | TCarg : ('b, 'a) ty_sel * ('a, 'e) ty -> ('e, 'b) ty_case
  | TCnoarg : ('b, noarg) ty_sel -> ('e, 'b) ty_case

type _ ty_env =
  (* type variable substitution *)
  | Enil : unit ty_env
  | Econs : ('a, 'e) ty * 'e ty_env -> ('a -> 'e) ty_env

(* Comparing selectors *)
type (_, _) eq = Eq : ('a, 'a) eq

let rec eq_sel : type a b c. (a, b) ty_sel -> (a, c) ty_sel -> (b, c) eq option
    =
 fun s1 s2 ->
  match (s1, s2) with
  | Thd, Thd -> Some Eq
  | Ttl s1, Ttl s2 -> (
      match eq_sel s1 s2 with None -> None | Some Eq -> Some Eq)
  | _ -> None

(* Auxiliary function to get the type of a case from its selector *)
let rec get_case : type a b e.
    (b, a) ty_sel -> (string * (e, b) ty_case) list -> string * (a, e) ty option
    =
 fun sel cases ->
  match cases with
  | (name, TCnoarg sel') :: rem ->
      begin match eq_sel sel sel' with
      | None -> get_case sel rem
      | Some Eq -> (name, None)
      end
  | (name, TCarg (sel', ty)) :: rem ->
      begin match eq_sel sel sel' with
      | None -> get_case sel rem
      | Some Eq -> (name, Some ty)
      end
  | [] -> raise Not_found

(* Untyped representation of values *)
type variant =
  | VInt of int
  | VString of string
  | VList of variant list
  | VOption of variant option
  | VPair of variant * variant
  | VConv of string * variant
  | VSum of string * variant option

let may_map f = function Some x -> Some (f x) | None -> None

let rec variantize : type a e. e ty_env -> (a, e) ty -> a -> variant =
 fun e ty v ->
  match ty with
  | Int -> VInt v
  | String -> VString v
  | List t -> VList (List.map (variantize e t) v)
  | Option t -> VOption (may_map (variantize e t) v)
  | Pair (t1, t2) -> VPair (variantize e t1 (fst v), variantize e t2 (snd v))
  | Rec t -> variantize (Econs (ty, e)) t v
  | Pop t -> ( match e with Econs (_, e') -> variantize e' t v)
  | Var -> ( match e with Econs (t, e') -> variantize e' t v)
  | Conv (s, proj, inj, t) -> VConv (s, variantize e t (proj v))
  | Sum ops ->
      let tag, arg = ops.sum_proj v in
      VSum (tag, may_map (function Tdyn (ty, arg) -> variantize e ty arg) arg)

let rec devariantize : type t e. e ty_env -> (t, e) ty -> variant -> t =
 fun e ty v ->
  match (ty, v) with
  | Int, VInt x -> x
  | String, VString x -> x
  | List ty1, VList vl -> List.map (devariantize e ty1) vl
  | Pair (ty1, ty2), VPair (x1, x2) ->
      (devariantize e ty1 x1, devariantize e ty2 x2)
  | Rec t, _ -> devariantize (Econs (ty, e)) t v
  | Pop t, _ -> ( match e with Econs (_, e') -> devariantize e' t v)
  | Var, _ -> ( match e with Econs (t, e') -> devariantize e' t v)
  | Conv (s, proj, inj, t), VConv (s', v) when s = s' ->
      inj (devariantize e t v)
  | Sum ops, VSum (tag, a) ->
      begin try
        match (List.assoc tag ops.sum_cases, a) with
        | TCarg (sel, t), Some a -> ops.sum_inj (sel, devariantize e t a)
        | TCnoarg sel, None -> ops.sum_inj (sel, Noarg)
        | _ -> raise VariantMismatch
      with Not_found -> raise VariantMismatch
      end
  | _ -> raise VariantMismatch

(* First attempt: represent 1-constructor variants using Conv *)
let wrap_A t = Conv ("`A", (fun (`A x) -> x), (fun x -> `A x), t)
let ty a = Rec (wrap_A (Option (Pair (a, Var))))
let v = variantize Enil (ty Int)
let x = v (`A (Some (1, `A (Some (2, `A None)))))

(* Can also use it to decompose a tuple *)

let triple t1 t2 t3 =
  Conv
    ( "Triple",
      (fun (a, b, c) -> (a, (b, c))),
      (fun (a, (b, c)) -> (a, b, c)),
      Pair (t1, Pair (t2, t3)) )

let v = variantize Enil (triple String Int Int) ("A", 2, 3)

(* Second attempt: introduce a real sum construct *)
let ty_abc =
  (* Could also use [get_case] for proj, but direct definition is shorter *)
  let proj = function
    | `A n -> ("A", Some (Tdyn (Int, n)))
    | `B s -> ("B", Some (Tdyn (String, s)))
    | `C -> ("C", None)
  (* Define inj in advance to be able to write the type annotation easily *)
  and inj : type c.
      (int -> string -> noarg -> unit, c) ty_sel * c ->
      [ `A of int | `B of string | `C ] = function
    | Thd, v -> `A v
    | Ttl Thd, v -> `B v
    | Ttl (Ttl Thd), Noarg -> `C
  in
  (* Coherence of sum_inj and sum_cases is checked by the typing *)
  Sum
    {
      sum_proj = proj;
      sum_inj = inj;
      sum_cases =
        [
          ("A", TCarg (Thd, Int));
          ("B", TCarg (Ttl Thd, String));
          ("C", TCnoarg (Ttl (Ttl Thd)));
        ];
    }

let v = variantize Enil ty_abc (`A 3)
let a = devariantize Enil ty_abc v

(* And an example with recursion... *)
type 'a vlist = [ `Nil | `Cons of 'a * 'a vlist ]

let ty_list : type a e. (a, e) ty -> (a vlist, e) ty =
 fun t ->
  let tcons = Pair (Pop t, Var) in
  Rec
    (Sum
       {
         sum_proj =
           (function
           | `Nil -> ("Nil", None)
           | `Cons p -> ("Cons", Some (Tdyn (tcons, p))));
         sum_cases = [ ("Nil", TCnoarg Thd); ("Cons", TCarg (Ttl Thd, tcons)) ];
         sum_inj =
           (fun (type c) ->
             (function Thd, Noarg -> `Nil | Ttl Thd, v -> `Cons v
               : (noarg -> a * a vlist -> unit, c) ty_sel * c -> a vlist))
           (* One can also write the type annotation directly *);
       })

let v = variantize Enil (ty_list Int) (`Cons (1, `Cons (2, `Nil)))

(* Simpler but weaker approach *)

type (_, _) ty =
  | Int : (int, _) ty
  | String : (string, _) ty
  | List : ('a, 'e) ty -> ('a list, 'e) ty
  | Option : ('a, 'e) ty -> ('a option, 'e) ty
  | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty
  | Var : ('a, 'a -> 'e) ty
  | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty
  | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty
  | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty
  | Sum :
      ('a -> string * 'e ty_dyn option) * (string * 'e ty_dyn option -> 'a)
      -> ('a, 'e) ty

and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn

let ty_abc : ([ `A of int | `B of string | `C ], 'e) ty =
  (* Could also use [get_case] for proj, but direct definition is shorter *)
  Sum
    ( (function
      | `A n -> ("A", Some (Tdyn (Int, n)))
      | `B s -> ("B", Some (Tdyn (String, s)))
      | `C -> ("C", None)),
      function
      | "A", Some (Tdyn (Int, n)) -> `A n
      | "B", Some (Tdyn (String, s)) -> `B s
      | "C", None -> `C
      | _ -> invalid_arg "ty_abc" )

(* Breaks: no way to pattern-match on a full recursive type *)
let ty_list : type a e. (a, e) ty -> (a vlist, e) ty =
 fun t ->
  let targ = Pair (Pop t, Var) in
  Rec
    (Sum
       ( (function
         | `Nil -> ("Nil", None)
         | `Cons p -> ("Cons", Some (Tdyn (targ, p)))),
         function
         | "Nil", None -> `Nil
         | "Cons", Some (Tdyn (Pair (_, Var), (p : a * a vlist))) -> `Cons p ))

(* Define Sum using object instead of record for first-class polymorphism *)

type (_, _) ty =
  | Int : (int, _) ty
  | String : (string, _) ty
  | List : ('a, 'e) ty -> ('a list, 'e) ty
  | Option : ('a, 'e) ty -> ('a option, 'e) ty
  | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty
  | Var : ('a, 'a -> 'e) ty
  | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty
  | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty
  | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty
  | Sum :
      < proj : 'a -> string * 'e ty_dyn option
      ; cases : (string * ('e, 'b) ty_case) list
      ; inj : 'c. ('b, 'c) ty_sel * 'c -> 'a >
      -> ('a, 'e) ty

and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn

and (_, _) ty_sel =
  | Thd : ('a -> 'b, 'a) ty_sel
  | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel

and (_, _) ty_case =
  | TCarg : ('b, 'a) ty_sel * ('a, 'e) ty -> ('e, 'b) ty_case
  | TCnoarg : ('b, noarg) ty_sel -> ('e, 'b) ty_case

let ty_abc : (([ `A of int | `B of string | `C ] as 'a), 'e) ty =
  Sum
    object
      method proj =
        function
        | `A n -> ("A", Some (Tdyn (Int, n)))
        | `B s -> ("B", Some (Tdyn (String, s)))
        | `C -> ("C", None)

      method cases =
        [
          ("A", TCarg (Thd, Int));
          ("B", TCarg (Ttl Thd, String));
          ("C", TCnoarg (Ttl (Ttl Thd)));
        ]

      method inj : type c.
          (int -> string -> noarg -> unit, c) ty_sel * c ->
          [ `A of int | `B of string | `C ] =
        function
        | Thd, v -> `A v
        | Ttl Thd, v -> `B v
        | Ttl (Ttl Thd), Noarg -> `C
    end

type 'a vlist = [ `Nil | `Cons of 'a * 'a vlist ]

let ty_list : type a e. (a, e) ty -> (a vlist, e) ty =
 fun t ->
  let tcons = Pair (Pop t, Var) in
  Rec
    (Sum
       object
         method proj =
           function
           | `Nil -> ("Nil", None)
           | `Cons p -> ("Cons", Some (Tdyn (tcons, p)))

         method cases =
           [ ("Nil", TCnoarg Thd); ("Cons", TCarg (Ttl Thd, tcons)) ]

         method inj : type c.
             (noarg -> a * a vlist -> unit, c) ty_sel * c -> a vlist =
           function Thd, Noarg -> `Nil | Ttl Thd, v -> `Cons v
       end)

(*
type (_,_) ty_assoc =
  | Anil : (unit,'e) ty_assoc
  | Acons : string * ('a,'e) ty * ('b,'e) ty_assoc -> ('a -> 'b, 'e) ty_assoc

and (_,_) ty_pvar =
  | Pnil : ('a,'e) ty_pvar
  | Pconst : 't * ('b,'e) ty_pvar -> ('t -> 'b, 'e) ty_pvar
  | Parg : 't * ('a,'e) ty * ('b,'e) ty_pvar -> ('t * 'a -> 'b, 'e) ty_pvar
*)
(*
   An attempt at encoding omega examples from the 2nd Central European
   Functional Programming School:
     Generic Programming in Omega, by Tim Sheard and Nathan Linger
          http://web.cecs.pdx.edu/~sheard/
*)

(* Basic types *)

type ('a, 'b) sum = Inl of 'a | Inr of 'b
type zero = Zero
type 'a succ = Succ of 'a
type _ nat = NZ : zero nat | NS : 'a nat -> 'a succ nat

(* 2: A simple example *)

type (_, _) seq =
  | Snil : ('a, zero) seq
  | Scons : 'a * ('a, 'n) seq -> ('a, 'n succ) seq

let l1 = Scons (3, Scons (5, Snil))

(* We do not have type level functions, so we need to use witnesses. *)
(* We copy here the definitions from section 3.9 *)
(* Note the addition of the ['a nat] argument to PlusZ, since we do not
   have kinds *)
type (_, _, _) plus =
  | PlusZ : 'a nat -> (zero, 'a, 'a) plus
  | PlusS : ('a, 'b, 'c) plus -> ('a succ, 'b, 'c succ) plus

let rec length : type a n. (a, n) seq -> n nat = function
  | Snil -> NZ
  | Scons (_, s) -> NS (length s)

(* app returns the catenated lists with a witness proving that
   the size is the sum of its two inputs *)
type (_, _, _) app =
  | App : ('a, 'p) seq * ('n, 'm, 'p) plus -> ('a, 'n, 'm) app

let rec app : type a n m. (a, n) seq -> (a, m) seq -> (a, n, m) app =
 fun xs ys ->
  match xs with
  | Snil -> App (ys, PlusZ (length ys))
  | Scons (x, xs') ->
      let (App (xs'', pl)) = app xs' ys in
      App (Scons (x, xs''), PlusS pl)

(* 3.1 Feature: kinds *)

(* We do not have kinds, but we can encode them as predicates *)

type tp = TP
type nd = ND
type ('a, 'b) fk = FK

type _ shape =
  | Tp : tp shape
  | Nd : nd shape
  | Fk : 'a shape * 'b shape -> ('a, 'b) fk shape

type tt = TT
type ff = FF
type _ boolean = BT : tt boolean | BF : ff boolean

(* 3.3 Feature : GADTs *)

type (_, _) path =
  | Pnone : 'a -> (tp, 'a) path
  | Phere : (nd, 'a) path
  | Pleft : ('x, 'a) path -> (('x, 'y) fk, 'a) path
  | Pright : ('y, 'a) path -> (('x, 'y) fk, 'a) path

type (_, _) tree =
  | Ttip : (tp, 'a) tree
  | Tnode : 'a -> (nd, 'a) tree
  | Tfork : ('x, 'a) tree * ('y, 'a) tree -> (('x, 'y) fk, 'a) tree

let tree1 = Tfork (Tfork (Ttip, Tnode 4), Tfork (Tnode 4, Tnode 3))

let rec find : type sh.
    ('a -> 'a -> bool) -> 'a -> (sh, 'a) tree -> (sh, 'a) path list =
 fun eq n t ->
  match t with
  | Ttip -> []
  | Tnode m -> if eq n m then [ Phere ] else []
  | Tfork (x, y) ->
      List.map (fun x -> Pleft x) (find eq n x)
      @ List.map (fun x -> Pright x) (find eq n y)

let rec extract : type sh. (sh, 'a) path -> (sh, 'a) tree -> 'a =
 fun p t ->
  match (p, t) with
  | Pnone x, Ttip -> x
  | Phere, Tnode y -> y
  | Pleft p, Tfork (l, _) -> extract p l
  | Pright p, Tfork (_, r) -> extract p r

(* 3.4 Pattern : Witness *)

type (_, _) le =
  | LeZ : 'a nat -> (zero, 'a) le
  | LeS : ('n, 'm) le -> ('n succ, 'm succ) le

type _ even = EvenZ : zero even | EvenSS : 'n even -> 'n succ succ even
type one = zero succ
type two = one succ
type three = two succ
type four = three succ

let even0 : zero even = EvenZ
let even2 : two even = EvenSS EvenZ
let even4 : four even = EvenSS (EvenSS EvenZ)
let p1 : (two, one, three) plus = PlusS (PlusS (PlusZ (NS NZ)))

let rec summandLessThanSum : type a b c. (a, b, c) plus -> (a, c) le =
 fun p ->
  match p with PlusZ n -> LeZ n | PlusS p' -> LeS (summandLessThanSum p')

(* 3.8 Pattern: Leibniz Equality *)

type (_, _) equal = Eq : ('a, 'a) equal

let convert : type a b. (a, b) equal -> a -> b = fun Eq x -> x

let rec sameNat : type a b. a nat -> b nat -> (a, b) equal option =
 fun a b ->
  match (a, b) with
  | NZ, NZ -> Some Eq
  | NS a', NS b' ->
      begin match sameNat a' b' with Some Eq -> Some Eq | None -> None
      end
  | _ -> None

(* Extra: associativity of addition *)

let rec plus_func : type a b m n.
    (a, b, m) plus -> (a, b, n) plus -> (m, n) equal =
 fun p1 p2 ->
  match (p1, p2) with
  | PlusZ _, PlusZ _ -> Eq
  | PlusS p1', PlusS p2' ->
      let Eq = plus_func p1' p2' in
      Eq

let rec plus_assoc : type a b c ab bc m n.
    (a, b, ab) plus ->
    (ab, c, m) plus ->
    (b, c, bc) plus ->
    (a, bc, n) plus ->
    (m, n) equal =
 fun p1 p2 p3 p4 ->
  match (p1, p4) with
  | PlusZ b, PlusZ bc ->
      let Eq = plus_func p2 p3 in
      Eq
  | PlusS p1', PlusS p4' ->
      let (PlusS p2') = p2 in
      let Eq = plus_assoc p1' p2' p3 p4' in
      Eq

(* 3.9 Computing Programs and Properties Simultaneously *)

(* Plus and app1 are moved to section 2 *)

let smaller : type a b. (a succ, b succ) le -> (a, b) le = function LeS x -> x

type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff

(*
let rec diff : type a b. (a,b) le -> a nat -> b nat -> (a,b) diff =
  fun le a b ->
  match a, b, le with
  | NZ, m, _ -> Diff (m, PlusZ m)
  | NS x, NZ, _ -> assert false
  | NS x, NS y, q ->
      match diff (smaller q) x y with Diff (m, p) -> Diff (m, PlusS p)
;;
*)

let rec diff : type a b. (a, b) le -> a nat -> b nat -> (a, b) diff =
 fun le a b ->
  match (le, a, b) with
  | LeZ _, _, m -> Diff (m, PlusZ m)
  | LeS q, NS x, NS y -> (
      match diff q x y with Diff (m, p) -> Diff (m, PlusS p))

let rec diff : type a b. (a, b) le -> a nat -> b nat -> (a, b) diff =
 fun le a b ->
  match (a, b, le) with
  (* warning *)
  | NZ, m, LeZ _ -> Diff (m, PlusZ m)
  | NS x, NS y, LeS q -> (
      match diff q x y with Diff (m, p) -> Diff (m, PlusS p))
  | _ -> .

let rec diff : type a b. (a, b) le -> b nat -> (a, b) diff =
 fun le b ->
  match (b, le) with
  | m, LeZ _ -> Diff (m, PlusZ m)
  | NS y, LeS q -> ( match diff q y with Diff (m, p) -> Diff (m, PlusS p))

type (_, _) filter = Filter : ('m, 'n) le * ('a, 'm) seq -> ('a, 'n) filter

let rec leS' : type m n. (m, n) le -> (m, n succ) le = function
  | LeZ n -> LeZ (NS n)
  | LeS le -> LeS (leS' le)

let rec filter : type a n. (a -> bool) -> (a, n) seq -> (a, n) filter =
 fun f s ->
  match s with
  | Snil -> Filter (LeZ NZ, Snil)
  | Scons (a, l) -> (
      match filter f l with
      | Filter (le, l') ->
          if f a then Filter (LeS le, Scons (a, l')) else Filter (leS' le, l'))

(* 4.1 AVL trees *)

type (_, _, _) balance =
  | Less : ('h, 'h succ, 'h succ) balance
  | Same : ('h, 'h, 'h) balance
  | More : ('h succ, 'h, 'h succ) balance

type _ avl =
  | Leaf : zero avl
  | Node : ('hL, 'hR, 'hMax) balance * 'hL avl * int * 'hR avl -> 'hMax succ avl

type avl' = Avl : 'h avl -> avl'

let empty = Avl Leaf

let rec elem : type h. int -> h avl -> bool =
 fun x t ->
  match t with
  | Leaf -> false
  | Node (_, l, y, r) -> x = y || if x < y then elem x l else elem x r

let rec rotr : type n.
    n succ succ avl ->
    int ->
    n avl ->
    (n succ succ avl, n succ succ succ avl) sum =
 fun tL y tR ->
  match tL with
  | Node (Same, a, x, b) -> Inr (Node (Less, a, x, Node (More, b, y, tR)))
  | Node (More, a, x, b) -> Inl (Node (Same, a, x, Node (Same, b, y, tR)))
  | Node (Less, a, x, Node (Same, b, z, c)) ->
      Inl (Node (Same, Node (Same, a, x, b), z, Node (Same, c, y, tR)))
  | Node (Less, a, x, Node (Less, b, z, c)) ->
      Inl (Node (Same, Node (More, a, x, b), z, Node (Same, c, y, tR)))
  | Node (Less, a, x, Node (More, b, z, c)) ->
      Inl (Node (Same, Node (Same, a, x, b), z, Node (Less, c, y, tR)))

let rec rotl : type n.
    n avl ->
    int ->
    n succ succ avl ->
    (n succ succ avl, n succ succ succ avl) sum =
 fun tL u tR ->
  match tR with
  | Node (Same, a, x, b) -> Inr (Node (More, Node (Less, tL, u, a), x, b))
  | Node (Less, a, x, b) -> Inl (Node (Same, Node (Same, tL, u, a), x, b))
  | Node (More, Node (Same, a, x, b), y, c) ->
      Inl (Node (Same, Node (Same, tL, u, a), x, Node (Same, b, y, c)))
  | Node (More, Node (Less, a, x, b), y, c) ->
      Inl (Node (Same, Node (More, tL, u, a), x, Node (Same, b, y, c)))
  | Node (More, Node (More, a, x, b), y, c) ->
      Inl (Node (Same, Node (Same, tL, u, a), x, Node (Less, b, y, c)))

let rec ins : type n. int -> n avl -> (n avl, n succ avl) sum =
 fun x t ->
  match t with
  | Leaf -> Inr (Node (Same, Leaf, x, Leaf))
  | Node (bal, a, y, b) ->
      if x = y then Inl t
      else if x < y then
        begin match ins x a with
        | Inl a -> Inl (Node (bal, a, y, b))
        | Inr a -> (
            match bal with
            | Less -> Inl (Node (Same, a, y, b))
            | Same -> Inr (Node (More, a, y, b))
            | More -> rotr a y b)
        end
      else
        begin match ins x b with
        | Inl b -> Inl (Node (bal, a, y, b) : n avl)
        | Inr b -> (
            match bal with
            | More -> Inl (Node (Same, a, y, b) : n avl)
            | Same -> Inr (Node (Less, a, y, b) : n succ avl)
            | Less -> rotl a y b)
        end

let insert x (Avl t) = match ins x t with Inl t -> Avl t | Inr t -> Avl t

let rec del_min : type n. n succ avl -> int * (n avl, n succ avl) sum = function
  | Node (Less, Leaf, x, r) -> (x, Inl r)
  | Node (Same, Leaf, x, r) -> (x, Inl r)
  | Node (bal, (Node _ as l), x, r) -> (
      match del_min l with
      | y, Inr l -> (y, Inr (Node (bal, l, x, r)))
      | y, Inl l ->
          ( y,
            match bal with
            | Same -> Inr (Node (Less, l, x, r))
            | More -> Inl (Node (Same, l, x, r))
            | Less -> rotl l x r ))

type _ avl_del =
  | Dsame : 'n avl -> 'n avl_del
  | Ddecr : ('m succ, 'n) equal * 'm avl -> 'n avl_del

let rec del : type n. int -> n avl -> n avl_del =
 fun y t ->
  match t with
  | Leaf -> Dsame Leaf
  | Node (bal, l, x, r) ->
      if x = y then
        begin match r with
        | Leaf ->
            begin match bal with Same -> Ddecr (Eq, l) | More -> Ddecr (Eq, l)
            end
        | Node _ ->
            begin match (bal, del_min r) with
            | _, (z, Inr r) -> Dsame (Node (bal, l, z, r))
            | Same, (z, Inl r) -> Dsame (Node (More, l, z, r))
            | Less, (z, Inl r) -> Ddecr (Eq, Node (Same, l, z, r))
            | More, (z, Inl r) -> (
                match rotr l z r with
                | Inl t -> Ddecr (Eq, t)
                | Inr t -> Dsame t)
            end
        end
      else if y < x then
        begin match del y l with
        | Dsame l -> Dsame (Node (bal, l, x, r))
        | Ddecr (Eq, l) ->
            begin match bal with
            | Same -> Dsame (Node (Less, l, x, r))
            | More -> Ddecr (Eq, Node (Same, l, x, r))
            | Less -> (
                match rotl l x r with
                | Inl t -> Ddecr (Eq, t)
                | Inr t -> Dsame t)
            end
        end
      else
        begin match del y r with
        | Dsame r -> Dsame (Node (bal, l, x, r))
        | Ddecr (Eq, r) ->
            begin match bal with
            | Same -> Dsame (Node (More, l, x, r))
            | Less -> Ddecr (Eq, Node (Same, l, x, r))
            | More -> (
                match rotr l x r with
                | Inl t -> Ddecr (Eq, t)
                | Inr t -> Dsame t)
            end
        end

let delete x (Avl t) =
  match del x t with Dsame t -> Avl t | Ddecr (_, t) -> Avl t

(* Exercise 22: Red-black trees *)

type red = RED
type black = BLACK

type (_, _) sub_tree =
  | Bleaf : (black, zero) sub_tree
  | Rnode :
      (black, 'n) sub_tree * int * (black, 'n) sub_tree
      -> (red, 'n) sub_tree
  | Bnode :
      ('cL, 'n) sub_tree * int * ('cR, 'n) sub_tree
      -> (black, 'n succ) sub_tree

type rb_tree = Root : (black, 'n) sub_tree -> rb_tree
type dir = LeftD | RightD

type (_, _) ctxt =
  | CNil : (black, 'n) ctxt
  | CRed : int * dir * (black, 'n) sub_tree * (red, 'n) ctxt -> (black, 'n) ctxt
  | CBlk :
      int * dir * ('c1, 'n) sub_tree * (black, 'n succ) ctxt
      -> ('c, 'n) ctxt

let blacken = function Rnode (l, e, r) -> Bnode (l, e, r)

type _ crep = Red : red crep | Black : black crep

let color : type c n. (c, n) sub_tree -> c crep = function
  | Bleaf -> Black
  | Rnode _ -> Red
  | Bnode _ -> Black

let rec fill : type c n. (c, n) ctxt -> (c, n) sub_tree -> rb_tree =
 fun ct t ->
  match ct with
  | CNil -> Root t
  | CRed (e, LeftD, uncle, c) -> fill c (Rnode (uncle, e, t))
  | CRed (e, RightD, uncle, c) -> fill c (Rnode (t, e, uncle))
  | CBlk (e, LeftD, uncle, c) -> fill c (Bnode (uncle, e, t))
  | CBlk (e, RightD, uncle, c) -> fill c (Bnode (t, e, uncle))

let recolor d1 pE sib d2 gE uncle t =
  match (d1, d2) with
  | LeftD, RightD -> Rnode (Bnode (sib, pE, t), gE, uncle)
  | RightD, RightD -> Rnode (Bnode (t, pE, sib), gE, uncle)
  | LeftD, LeftD -> Rnode (uncle, gE, Bnode (sib, pE, t))
  | RightD, LeftD -> Rnode (uncle, gE, Bnode (t, pE, sib))

let rotate d1 pE sib d2 gE uncle (Rnode (x, e, y)) =
  match (d1, d2) with
  | RightD, RightD -> Bnode (Rnode (x, e, y), pE, Rnode (sib, gE, uncle))
  | LeftD, RightD -> Bnode (Rnode (sib, pE, x), e, Rnode (y, gE, uncle))
  | LeftD, LeftD -> Bnode (Rnode (uncle, gE, sib), pE, Rnode (x, e, y))
  | RightD, LeftD -> Bnode (Rnode (uncle, gE, x), e, Rnode (y, pE, sib))

let rec repair : type c n. (red, n) sub_tree -> (c, n) ctxt -> rb_tree =
 fun t ct ->
  match ct with
  | CNil -> Root (blacken t)
  | CBlk (e, LeftD, sib, c) -> fill c (Bnode (sib, e, t))
  | CBlk (e, RightD, sib, c) -> fill c (Bnode (t, e, sib))
  | CRed (e, dir, sib, CBlk (e', dir', uncle, ct)) -> (
      match color uncle with
      | Red -> repair (recolor dir e sib dir' e' (blacken uncle) t) ct
      | Black -> fill ct (rotate dir e sib dir' e' uncle t))

let rec ins : type c n. int -> (c, n) sub_tree -> (c, n) ctxt -> rb_tree =
 fun e t ct ->
  match t with
  | Rnode (l, e', r) ->
      if e < e' then ins e l (CRed (e', RightD, r, ct))
      else ins e r (CRed (e', LeftD, l, ct))
  | Bnode (l, e', r) ->
      if e < e' then ins e l (CBlk (e', RightD, r, ct))
      else ins e r (CBlk (e', LeftD, l, ct))
  | Bleaf -> repair (Rnode (Bleaf, e, Bleaf)) ct

let insert e (Root t) = ins e t CNil

(* 5.7 typed object languages using GADTs *)

type _ term =
  | Const : int -> int term
  | Add : (int * int -> int) term
  | LT : (int * int -> bool) term
  | Ap : ('a -> 'b) term * 'a term -> 'b term
  | Pair : 'a term * 'b term -> ('a * 'b) term

let ex1 = Ap (Add, Pair (Const 3, Const 5))
let ex2 = Pair (ex1, Const 1)

let rec eval_term : type a. a term -> a = function
  | Const x -> x
  | Add -> fun (x, y) -> x + y
  | LT -> fun (x, y) -> x < y
  | Ap (f, x) -> eval_term f (eval_term x)
  | Pair (x, y) -> (eval_term x, eval_term y)

type _ rep =
  | Rint : int rep
  | Rbool : bool rep
  | Rpair : 'a rep * 'b rep -> ('a * 'b) rep
  | Rfun : 'a rep * 'b rep -> ('a -> 'b) rep

type (_, _) equal = Eq : ('a, 'a) equal

let rec rep_equal : type a b. a rep -> b rep -> (a, b) equal option =
 fun ra rb ->
  match (ra, rb) with
  | Rint, Rint -> Some Eq
  | Rbool, Rbool -> Some Eq
  | Rpair (a1, a2), Rpair (b1, b2) ->
      begin match rep_equal a1 b1 with
      | None -> None
      | Some Eq -> (
          match rep_equal a2 b2 with None -> None | Some Eq -> Some Eq)
      end
  | Rfun (a1, a2), Rfun (b1, b2) ->
      begin match rep_equal a1 b1 with
      | None -> None
      | Some Eq -> (
          match rep_equal a2 b2 with None -> None | Some Eq -> Some Eq)
      end
  | _ -> None

type assoc = Assoc : string * 'a rep * 'a -> assoc

let rec assoc : type a. string -> a rep -> assoc list -> a =
 fun x r -> function
  | [] -> raise Not_found
  | Assoc (x', r', v) :: env ->
      if x = x' then
        match rep_equal r r' with
        | None -> failwith ("Wrong type for " ^ x)
        | Some Eq -> v
      else assoc x r env

type _ term =
  | Var : string * 'a rep -> 'a term
  | Abs : string * 'a rep * 'b term -> ('a -> 'b) term
  | Const : int -> int term
  | Add : (int * int -> int) term
  | LT : (int * int -> bool) term
  | Ap : ('a -> 'b) term * 'a term -> 'b term
  | Pair : 'a term * 'b term -> ('a * 'b) term

let rec eval_term : type a. assoc list -> a term -> a =
 fun env -> function
  | Var (x, r) -> assoc x r env
  | Abs (x, r, e) -> fun v -> eval_term (Assoc (x, r, v) :: env) e
  | Const x -> x
  | Add -> fun (x, y) -> x + y
  | LT -> fun (x, y) -> x < y
  | Ap (f, x) -> eval_term env f (eval_term env x)
  | Pair (x, y) -> (eval_term env x, eval_term env y)

let ex3 = Abs ("x", Rint, Ap (Add, Pair (Var ("x", Rint), Var ("x", Rint))))
let ex4 = Ap (ex3, Const 3)
let v4 = eval_term [] ex4

(* 5.9/5.10 Language with binding *)

type rnil = RNIL
type ('a, 'b, 'c) rcons = RCons of 'a * 'b * 'c

type _ is_row =
  | Rnil : rnil is_row
  | Rcons : 'c is_row -> ('a, 'b, 'c) rcons is_row

type (_, _) lam =
  | Const : int -> ('e, int) lam
  | Var : 'a -> (('a, 't, 'e) rcons, 't) lam
  | Shift : ('e, 't) lam -> (('a, 'q, 'e) rcons, 't) lam
  | Abs : 'a * (('a, 's, 'e) rcons, 't) lam -> ('e, 's -> 't) lam
  | App : ('e, 's -> 't) lam * ('e, 's) lam -> ('e, 't) lam

type x = X
type y = Y

let ex1 = App (Var X, Shift (Var Y))
let ex2 = Abs (X, Abs (Y, App (Shift (Var X), Var Y)))

type _ env =
  | Enil : rnil env
  | Econs : 'a * 't * 'e env -> ('a, 't, 'e) rcons env

let rec eval_lam : type e t. e env -> (e, t) lam -> t =
 fun env m ->
  match (env, m) with
  | _, Const n -> n
  | Econs (_, v, r), Var _ -> v
  | Econs (_, _, r), Shift e -> eval_lam r e
  | _, Abs (n, body) -> fun x -> eval_lam (Econs (n, x, env)) body
  | _, App (f, x) -> eval_lam env f (eval_lam env x)

type add = Add
type suc = Suc

let env0 = Econs (Zero, 0, Econs (Suc, succ, Econs (Add, ( + ), Enil)))
let _0 : (_, int) lam = Var Zero
let suc x = App (Shift (Var Suc : (_, int -> int) lam), x)
let _1 = suc _0
let _2 = suc _1
let _3 = suc _2
let add = Shift (Shift (Var Add : (_, int -> int -> int) lam))
let double = Abs (X, App (App (Shift add, Var X), Var X))
let ex3 = App (double, _3)
let v3 = eval_lam env0 ex3

(* 5.13: Constructing typing derivations at runtime *)

(* Modified slightly to use the language of 5.10, since this is more fun.
   Of course this works also with the language of 5.12. *)

type _ rep = I : int rep | Ar : 'a rep * 'b rep -> ('a -> 'b) rep

let rec compare : type a b. a rep -> b rep -> (string, (a, b) equal) sum =
 fun a b ->
  match (a, b) with
  | I, I -> Inr Eq
  | Ar (x, y), Ar (s, t) ->
      begin match compare x s with
      | Inl _ as e -> e
      | Inr Eq -> ( match compare y t with Inl _ as e -> e | Inr Eq as e -> e)
      end
  | I, Ar _ -> Inl "I <> Ar _"
  | Ar _, I -> Inl "Ar _ <> I"

type term =
  | C of int
  | Ab : string * 'a rep * term -> term
  | Ap of term * term
  | V of string

type _ ctx =
  | Cnil : rnil ctx
  | Ccons : 't * string * 'x rep * 'e ctx -> ('t, 'x, 'e) rcons ctx

type _ checked = Cerror of string | Cok : ('e, 't) lam * 't rep -> 'e checked

let rec lookup : type e. string -> e ctx -> e checked =
 fun name ctx ->
  match ctx with
  | Cnil -> Cerror ("Name not found: " ^ name)
  | Ccons (l, s, t, rs) -> (
      if s = name then Cok (Var l, t)
      else
        match lookup name rs with
        | Cerror m -> Cerror m
        | Cok (v, t) -> Cok (Shift v, t))

let rec tc : type n e. n nat -> e ctx -> term -> e checked =
 fun n ctx t ->
  match t with
  | V s -> lookup s ctx
  | Ap (f, x) ->
      begin match tc n ctx f with
      | Cerror _ as e -> e
      | Cok (f', ft) -> (
          match tc n ctx x with
          | Cerror _ as e -> e
          | Cok (x', xt) -> (
              match ft with
              | Ar (a, b) ->
                  begin match compare a xt with
                  | Inl s -> Cerror s
                  | Inr Eq -> Cok (App (f', x'), b)
                  end
              | _ -> Cerror "Non fun in Ap"))
      end
  | Ab (s, t, body) ->
      begin match tc (NS n) (Ccons (n, s, t, ctx)) body with
      | Cerror _ as e -> e
      | Cok (body', et) -> Cok (Abs (n, body'), Ar (t, et))
      end
  | C m -> Cok (Const m, I)

let ctx0 =
  Ccons
    ( Zero,
      "0",
      I,
      Ccons (Suc, "S", Ar (I, I), Ccons (Add, "+", Ar (I, Ar (I, I)), Cnil)) )

let ex1 = Ab ("x", I, Ap (Ap (V "+", V "x"), V "x"))
let c1 = tc NZ ctx0 ex1
let ex2 = Ap (ex1, C 3)
let c2 = tc NZ ctx0 ex2

let eval_checked env = function
  | Cerror s -> failwith s
  | Cok (e, I) -> (eval_lam env e : int)
  | Cok _ -> failwith "Can only evaluate expressions of type I"

let v2 = eval_checked env0 c2

(* 5.12 Soundness *)

type pexp = PEXP
type pval = PVAL
type _ mode = Pexp : pexp mode | Pval : pval mode
type ('a, 'b) tarr = TARR
type tint = TINT

type (_, _) rel =
  | IntR : (tint, int) rel
  | IntTo : ('b, 's) rel -> ((tint, 'b) tarr, int -> 's) rel

type (_, _, _) lam =
  | Const : ('a, 'b) rel * 'b -> (pval, 'env, 'a) lam
  | Var : 'a -> (pval, ('a, 't, 'e) rcons, 't) lam
  | Shift : ('m, 'e, 't) lam -> ('m, ('a, 'q, 'e) rcons, 't) lam
  | Lam : 'a * ('m, ('a, 's, 'e) rcons, 't) lam -> (pval, 'e, ('s, 't) tarr) lam
  | App : ('m1, 'e, ('s, 't) tarr) lam * ('m2, 'e, 's) lam -> (pexp, 'e, 't) lam

let ex1 = App (Lam (X, Var X), Const (IntR, 3))

let rec mode : type m e t. (m, e, t) lam -> m mode = function
  | Lam (v, body) -> Pval
  | Var v -> Pval
  | Const (r, v) -> Pval
  | Shift e -> mode e
  | App _ -> Pexp

type (_, _) sub =
  | Id : ('r, 'r) sub
  | Bind :
      't * ('m, 'r2, 'x) lam * ('r, 'r2) sub
      -> (('t, 'x, 'r) rcons, 'r2) sub
  | Push : ('r1, 'r2) sub -> (('a, 'b, 'r1) rcons, ('a, 'b, 'r2) rcons) sub

type (_, _) lam' = Ex : ('m, 's, 't) lam -> ('s, 't) lam'

let rec subst : type m1 r t s. (m1, r, t) lam -> (r, s) sub -> (s, t) lam' =
 fun t s ->
  match (t, s) with
  | _, Id -> Ex t
  | Const (r, c), sub -> Ex (Const (r, c))
  | Var v, Bind (x, e, r) -> Ex e
  | Var v, Push sub -> Ex (Var v)
  | Shift e, Bind (_, _, r) -> subst e r
  | Shift e, Push sub -> ( match subst e sub with Ex a -> Ex (Shift a))
  | App (f, x), sub -> (
      match (subst f sub, subst x sub) with Ex g, Ex y -> Ex (App (g, y)))
  | Lam (v, x), sub -> (
      match subst x (Push sub) with Ex body -> Ex (Lam (v, body)))

type closed = rnil
type 'a rlam = ((pexp, closed, 'a) lam, (pval, closed, 'a) lam) sum

let rec rule : type a b.
    (pval, closed, (a, b) tarr) lam -> (pval, closed, a) lam -> b rlam =
 fun v1 v2 ->
  match (v1, v2) with
  | Lam (x, body), v ->
      begin match subst body (Bind (x, v, Id)) with
      | Ex term -> ( match mode term with Pexp -> Inl term | Pval -> Inr term)
      end
  | Const (IntTo b, f), Const (IntR, x) -> Inr (Const (b, f x))

let rec onestep : type m t. (m, closed, t) lam -> t rlam = function
  | Lam (v, body) -> Inr (Lam (v, body))
  | Const (r, v) -> Inr (Const (r, v))
  | App (e1, e2) -> (
      match (mode e1, mode e2) with
      | Pexp, _ ->
          begin match onestep e1 with
          | Inl e -> Inl (App (e, e2))
          | Inr v -> Inl (App (v, e2))
          end
      | Pval, Pexp ->
          begin match onestep e2 with
          | Inl e -> Inl (App (e1, e))
          | Inr v -> Inl (App (e1, v))
          end
      | Pval, Pval -> rule e1 e2)

type ('env, 'a) var =
  | Zero : ('a * 'env, 'a) var
  | Succ : ('env, 'a) var -> ('b * 'env, 'a) var

type ('env, 'a) typ =
  | Tint : ('env, int) typ
  | Tbool : ('env, bool) typ
  | Tvar : ('env, 'a) var -> ('env, 'a) typ

let f : type env a. (env, a) typ -> (env, a) typ -> int =
 fun ta tb ->
  match (ta, tb) with
  | Tint, Tint -> 0
  | Tbool, Tbool -> 1
  | Tvar var, tb -> 2
  | _ -> . (* error *)

(* let x = f Tint (Tvar Zero) ;; *)
type inkind = [ `Link | `Nonlink ]

type _ inline_t =
  | Text : string -> [< inkind > `Nonlink ] inline_t
  | Bold : 'a inline_t list -> 'a inline_t
  | Link : string -> [< inkind > `Link ] inline_t
  | Mref : string * [ `Nonlink ] inline_t list -> [< inkind > `Link ] inline_t

let uppercase seq =
  let rec process : type a. a inline_t -> a inline_t = function
    | Text txt -> Text (String.uppercase_ascii txt)
    | Bold xs -> Bold (List.map process xs)
    | Link lnk -> Link lnk
    | Mref (lnk, xs) -> Mref (lnk, List.map process xs)
  in
  List.map process seq

type ast_t =
  | Ast_Text of string
  | Ast_Bold of ast_t list
  | Ast_Link of string
  | Ast_Mref of string * ast_t list

let inlineseq_from_astseq seq =
  let rec process_nonlink = function
    | Ast_Text txt -> Text txt
    | Ast_Bold xs -> Bold (List.map process_nonlink xs)
    | _ -> assert false
  in
  let rec process_any = function
    | Ast_Text txt -> Text txt
    | Ast_Bold xs -> Bold (List.map process_any xs)
    | Ast_Link lnk -> Link lnk
    | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs)
  in
  List.map process_any seq

(* OK *)
type _ linkp = Nonlink : [ `Nonlink ] linkp | Maylink : inkind linkp

let inlineseq_from_astseq seq =
  let rec process : type a. a linkp -> ast_t -> a inline_t =
   fun allow_link ast ->
    match (allow_link, ast) with
    | Maylink, Ast_Text txt -> Text txt
    | Nonlink, Ast_Text txt -> Text txt
    | x, Ast_Bold xs -> Bold (List.map (process x) xs)
    | Maylink, Ast_Link lnk -> Link lnk
    | Nonlink, Ast_Link _ -> assert false
    | Maylink, Ast_Mref (lnk, xs) -> Mref (lnk, List.map (process Nonlink) xs)
    | Nonlink, Ast_Mref _ -> assert false
  in
  List.map (process Maylink) seq

(* Bad *)
type _ linkp2 = Kind : 'a linkp -> ([< inkind ] as 'a) linkp2

let inlineseq_from_astseq seq =
  let rec process : type a. a linkp2 -> ast_t -> a inline_t =
   fun allow_link ast ->
    match (allow_link, ast) with
    | Kind _, Ast_Text txt -> Text txt
    | x, Ast_Bold xs -> Bold (List.map (process x) xs)
    | Kind Maylink, Ast_Link lnk -> Link lnk
    | Kind Nonlink, Ast_Link _ -> assert false
    | Kind Maylink, Ast_Mref (lnk, xs) ->
        Mref (lnk, List.map (process (Kind Nonlink)) xs)
    | Kind Nonlink, Ast_Mref _ -> assert false
  in
  List.map (process (Kind Maylink)) seq

module Add (T : sig
  type two
end) =
struct
  type _ t = One : [ `One ] t | Two : T.two t

  let add (type a) : a t * a t -> string = function
    | One, One -> "two"
    | Two, Two -> "four"
end

module B : sig
  type (_, _) t = Eq : ('a, 'a) t

  val f : 'a -> 'b -> ('a, 'b) t
end = struct
  type (_, _) t = Eq : ('a, 'a) t

  let f t1 t2 = Obj.magic Eq
end

let of_type : type a. a -> a = fun x -> match B.f x 4 with Eq -> 5

type _ constant = Int : int -> int constant | Bool : bool -> bool constant

type (_, _, _) binop =
  | Eq : ('a, 'a, bool) binop
  | Leq : ('a, 'a, bool) binop
  | Add : (int, int, int) binop

let eval (type a) (type b) (type c) (bop : (a, b, c) binop) (x : a constant)
    (y : b constant) : c constant =
  match (bop, x, y) with
  | Eq, Bool x, Bool y -> Bool (if x then y else not y)
  | Leq, Int x, Int y -> Bool (x <= y)
  | Leq, Bool x, Bool y -> Bool (x <= y)
  | Add, Int x, Int y -> Int (x + y)

let _ = eval Eq (Int 2) (Int 3)

type tag = [ `TagA | `TagB | `TagC ]

type 'a poly =
  | AandBTags : [< `TagA of int | `TagB ] poly
  | ATag : [< `TagA of int ] poly
(* constraint 'a = [< `TagA of int | `TagB] *)

let intA = function `TagA i -> i
let intB = function `TagB -> 4
let intAorB = function `TagA i -> i | `TagB -> 4

type _ wrapPoly =
  | WrapPoly : 'a poly -> ([< `TagA of int | `TagB ] as 'a) wrapPoly

let example6 : type a. a wrapPoly -> a -> int =
 fun w ->
  match w with
  | WrapPoly ATag -> intA
  | WrapPoly _ -> intA (* This should not be allowed *)

let _ = example6 (WrapPoly AandBTags) `TagB (* This causes a seg fault *)

module F (S : sig
  type 'a t
end) =
struct
  type _ ab = A : int S.t ab | B : float S.t ab

  let f : int S.t ab -> float S.t ab -> string =
   fun (l : int S.t ab) (r : float S.t ab) ->
    match (l, r) with A, B -> "f A B"
end

module F (S : sig
  type 'a t
end) =
struct
  type a = int * int
  type b = int -> int
  type _ ab = A : a S.t ab | B : b S.t ab

  let f : a S.t ab -> b S.t ab -> string =
   fun l r -> match (l, r) with A, B -> "f A B"
end

type (_, _) t = Any : ('a, 'b) t | Eq : ('a, 'a) t

module M : sig
  type s = private [> `A ]

  val eq : (s, [ `A | `B ]) t
end = struct
  type s = [ `A | `B ]

  let eq = Eq
end

let f : (M.s, [ `A | `B ]) t -> string = function Any -> "Any"
let () = print_endline (f M.eq)

module N : sig
  type s = private < a : int ; .. >

  val eq : (s, < a : int ; b : bool >) t
end = struct
  type s = < a : int ; b : bool >

  let eq = Eq
end

let f : (N.s, < a : int ; b : bool >) t -> string = function Any -> "Any"

type (_, _) comp = Eq : ('a, 'a) comp | Diff : ('a, 'b) comp

module U = struct
  type t = T
end

module M : sig
  type t = T

  val comp : (U.t, t) comp
end = struct
  include U

  let comp = Eq
end
;;

match M.comp with Diff -> false;;

module U = struct
  type t = { x : int }
end

module M : sig
  type t = { x : int }

  val comp : (U.t, t) comp
end = struct
  include U

  let comp = Eq
end
;;

match M.comp with Diff -> false;;

type 'a t = T of 'a
type 'a s = S of 'a
type (_, _) eq = Refl : ('a, 'a) eq

let f : (int s, int t) eq -> unit = function Refl -> ()

module M (S : sig
  type 'a t = T of 'a
  type 'a s = T of 'a
end) =
struct
  let f : ('a S.s, 'a S.t) eq -> unit = function Refl -> ()
end

type _ nat = Zero : [ `Zero ] nat | Succ : 'a nat -> [ `Succ of 'a ] nat
type 'a pre_nat = [ `Zero | `Succ of 'a ]

type aux =
  | Aux :
      [ `Succ of [< [< [< [ `Zero ] pre_nat ] pre_nat ] pre_nat ] ] nat
      -> aux

let f (Aux x) =
  match x with
  | Succ Zero -> "1"
  | Succ (Succ Zero) -> "2"
  | Succ (Succ (Succ Zero)) -> "3"
  | Succ (Succ (Succ (Succ Zero))) -> "4"
  | _ -> . (* error *)

type _ t = C : ((('a -> 'o) -> 'o) -> ('b -> 'o) -> 'o) t

let f : type a o. ((a -> o) -> o) t -> (a -> o) -> o = fun C k -> k (fun x -> x)

type (_, _) t = A : ('a, 'a) t | B : string -> ('a, 'b) t

module M (A : sig
  module type T
end) (B : sig
  module type T
end) =
struct
  let f : ((module A.T), (module B.T)) t -> string = function B s -> s
end

module A = struct
  module type T = sig end
end

module N = M (A) (A)

let x = N.f A

type 'a visit_action
type insert
type 'a local_visit_action

type ('a, 'result, 'visit_action) context =
  | Local : ('a, ('a * insert as 'result), 'a local_visit_action) context
  | Global : ('a, 'a, 'a visit_action) context

let vexpr (type visit_action) :
    (_, _, visit_action) context -> _ -> visit_action = function
  | Local -> fun _ -> raise Exit
  | Global -> fun _ -> raise Exit

let vexpr (type visit_action) :
    ('a, 'result, visit_action) context -> 'a -> visit_action = function
  | Local -> fun _ -> raise Exit
  | Global -> fun _ -> raise Exit

let vexpr (type result) (type visit_action) :
    (unit, result, visit_action) context -> unit -> visit_action = function
  | Local -> fun _ -> raise Exit
  | Global -> fun _ -> raise Exit

module A = struct
  type nil = Cstr
end

open A

type _ s = Nil : nil s | Cons : 't s -> ('h -> 't) s

type ('stack, 'typ) var =
  | Head : (('typ -> _) s, 'typ) var
  | Tail : ('tail s, 'typ) var -> ((_ -> 'tail) s, 'typ) var

type _ lst = CNil : nil lst | CCons : 'h * 't lst -> ('h -> 't) lst

let rec get_var : type stk ret. (stk s, ret) var -> stk lst -> ret =
 fun n s ->
  match (n, s) with
  | Head, CCons (h, _) -> h
  | Tail n', CCons (_, t) -> get_var n' t

type 'a t = [< `Foo | `Bar ] as 'a
type 'a s = [< `Foo | `Bar | `Baz > `Bar ] as 'a

type 'a first = First : 'a second -> ('b t as 'a) first
and 'a second = Second : ('b s as 'a) second

type aux = Aux : 'a t second * ('a -> int) -> aux

let it : 'a. ([< `Bar | `Foo > `Bar ] as 'a) = `Bar
let g (Aux (Second, f)) = f it

type (_, _) eqp = Y : ('a, 'a) eqp | N : string -> ('a, 'b) eqp

let f : ('a list, 'a) eqp -> unit = function N s -> print_string s

module rec A : sig
  type t = B.t list
end = struct
  type t = B.t list
end

and B : sig
  type t

  val eq : (B.t list, t) eqp
end = struct
  type t = A.t

  let eq = Y
end
;;

f B.eq;;

type (_, _) t =
  | Nil : ('tl, 'tl) t
  | Cons : 'a * ('b, 'tl) t -> ('a * 'b, 'tl) t

let get1 (Cons (x, _) : (_ * 'a, 'a) t) = x

(* warn, cf PR#6993 *)

let get1' = function (Cons (x, _) : (_ * 'a, 'a) t) -> x | Nil -> assert false

(* ok *)
type _ t =
  | Int : int -> int t
  | String : string -> string t
  | Same : 'l t -> 'l t

let rec f = function Int x -> x | Same s -> f s

type 'a tt = 'a t =
  | Int : int -> int tt
  | String : string -> string tt
  | Same : 'l1 t -> 'l2 tt

type _ t = I : int t

let f (type a) (x : a t) =
  let module M = struct
    let (I : a t) = x (* fail because of toplevel let *)
    let x = (I : a t)
  end in
  ()

(* extra example by Stephen Dolan, using recursive modules *)
(* Should not be allowed! *)
type (_, _) eq = Refl : ('a, 'a) eq

let bad (type a) =
  let module N = struct
    module rec M : sig
      val e : (int, a) eq
    end = struct
      let (Refl : (int, a) eq) = M.e (* must fail for soundness *)
      let e : (int, a) eq = Refl
    end
  end in
  N.M.e

type +'a n = private int
type nil = private Nil_type

type (_, _) elt =
  | Elt_fine : 'nat n -> ('l, 'nat * 'l) elt
  | Elt : 'nat n -> ('l, 'nat -> 'l) elt

type _ t = Nil : nil t | Cons : ('x, 'fx) elt * 'x t -> 'fx t

let undetected : ('a -> 'b -> nil) t -> 'a n -> 'b n -> unit =
 fun sh i j ->
  let (Cons (Elt dim, _)) = sh in
  ()

type _ t = T : int t

(* Should raise Not_found *)
let _ = match (raise Not_found : float t) with _ -> .

type (_, _) eq = Eq : ('a, 'a) eq | Neq : int -> ('a, 'b) eq
type 'a t

let f (type a) (Neq n : (a, a t) eq) = n

(* warn! *)

module F (T : sig
  type _ t
end) =
struct
  let f (type a) (Neq n : (a, a T.t) eq) = n (* warn! *)
end

(* First-Order Unification by Structural Recursion *)
(* Conor McBride, JFP 13(6) *)
(* http://strictlypositive.org/publications.html *)

(* This is a translation of the code part to ocaml *)
(* Of course, we do not prove other properties, not even termination *)

(* 2.2 Inductive Families *)

type zero = Zero
type _ succ = Succ
type _ nat = NZ : zero nat | NS : 'a nat -> 'a succ nat
type _ fin = FZ : 'a succ fin | FS : 'a fin -> 'a succ fin

(* We cannot define
     val empty : zero fin -> 'a
   because we cannot write an empty pattern matching.
   This might be useful to have *)

(* In place, prove that the parameter is 'a succ *)
type _ is_succ = IS : 'a succ is_succ

let fin_succ : type n. n fin -> n is_succ = function FZ -> IS | FS _ -> IS

(* 3 First-Order Terms, Renaming and Substitution *)

type 'a term = Var of 'a fin | Leaf | Fork of 'a term * 'a term

let var x = Var x
let lift r : 'm fin -> 'n term = fun x -> Var (r x)

let rec pre_subst f = function
  | Var x -> f x
  | Leaf -> Leaf
  | Fork (t1, t2) -> Fork (pre_subst f t1, pre_subst f t2)

let comp_subst f g (x : 'a fin) = pre_subst f (g x)
(*  val comp_subst :
    ('b fin -> 'c term) -> ('a fin -> 'b term) -> 'a fin -> 'c term *)

(* 4 The Occur-Check, through thick and thin *)

let rec thin : type n. n succ fin -> n fin -> n succ fin =
 fun x y ->
  match (x, y) with
  | FZ, y -> FS y
  | FS x, FZ -> FZ
  | FS x, FS y -> FS (thin x y)

let bind t f = match t with None -> None | Some x -> f x
(* val bind : 'a option -> ('a -> 'b option) -> 'b option *)

let rec thick : type n. n succ fin -> n succ fin -> n fin option =
 fun x y ->
  match (x, y) with
  | FZ, FZ -> None
  | FZ, FS y -> Some y
  | FS x, FZ ->
      let IS = fin_succ x in
      Some FZ
  | FS x, FS y ->
      let IS = fin_succ x in
      bind (thick x y) (fun x -> Some (FS x))

let rec check : type n. n succ fin -> n succ term -> n term option =
 fun x t ->
  match t with
  | Var y -> bind (thick x y) (fun x -> Some (Var x))
  | Leaf -> Some Leaf
  | Fork (t1, t2) ->
      bind (check x t1) (fun t1 ->
          bind (check x t2) (fun t2 -> Some (Fork (t1, t2))))

let subst_var x t' y = match thick x y with None -> t' | Some y' -> Var y'
(* val subst_var : 'a succ fin -> 'a term -> 'a succ fin -> 'a term *)

let subst x t' = pre_subst (subst_var x t')
(* val subst : 'a succ fin -> 'a term -> 'a succ term -> 'a term *)

(* 5 A Refinement of Substitution *)

type (_, _) alist =
  | Anil : ('n, 'n) alist
  | Asnoc : ('m, 'n) alist * 'm term * 'm succ fin -> ('m succ, 'n) alist

let rec sub : type m n. (m, n) alist -> m fin -> n term = function
  | Anil -> var
  | Asnoc (s, t, x) -> comp_subst (sub s) (subst_var x t)

let rec append : type m n l. (m, n) alist -> (l, m) alist -> (l, n) alist =
 fun r s ->
  match s with Anil -> r | Asnoc (s, t, x) -> Asnoc (append r s, t, x)

type _ ealist = EAlist : ('a, 'b) alist -> 'a ealist

let asnoc a t' x = EAlist (Asnoc (a, t', x))

(* Extra work: we need sub to work on ealist too, for examples *)
let rec weaken_fin : type n. n fin -> n succ fin = function
  | FZ -> FZ
  | FS x -> FS (weaken_fin x)

let weaken_term t = pre_subst (fun x -> Var (weaken_fin x)) t

let rec weaken_alist : type m n. (m, n) alist -> (m succ, n succ) alist =
  function
  | Anil -> Anil
  | Asnoc (s, t, x) -> Asnoc (weaken_alist s, weaken_term t, weaken_fin x)

let rec sub' : type m. m ealist -> m fin -> m term = function
  | EAlist Anil -> var
  | EAlist (Asnoc (s, t, x)) ->
      comp_subst
        (sub' (EAlist (weaken_alist s)))
        (fun t' -> weaken_term (subst_var x t t'))

let subst' d = pre_subst (sub' d)
(*  val subst' : 'a ealist -> 'a term -> 'a term *)

(* 6 First-Order Unification *)

let flex_flex x y =
  match thick x y with Some y' -> asnoc Anil (Var y') x | None -> EAlist Anil
(* val flex_flex : 'a succ fin -> 'a succ fin -> 'a succ ealist *)

let flex_rigid x t = bind (check x t) (fun t' -> Some (asnoc Anil t' x))
(* val flex_rigid : 'a succ fin -> 'a succ term -> 'a succ ealist option *)

let rec amgu : type m. m term -> m term -> m ealist -> m ealist option =
 fun s t acc ->
  match (s, t, acc) with
  | Leaf, Leaf, _ -> Some acc
  | Leaf, Fork _, _ -> None
  | Fork _, Leaf, _ -> None
  | Fork (s1, s2), Fork (t1, t2), _ -> bind (amgu s1 t1 acc) (amgu s2 t2)
  | Var x, Var y, EAlist Anil ->
      let IS = fin_succ x in
      Some (flex_flex x y)
  | Var x, t, EAlist Anil ->
      let IS = fin_succ x in
      flex_rigid x t
  | t, Var x, EAlist Anil ->
      let IS = fin_succ x in
      flex_rigid x t
  | s, t, EAlist (Asnoc (d, r, z)) ->
      bind
        (amgu (subst z r s) (subst z r t) (EAlist d))
        (fun (EAlist d) -> Some (asnoc d r z))

let mgu s t = amgu s t (EAlist Anil)
(* val mgu : 'a term -> 'a term -> 'a ealist option *)

let s = Fork (Var FZ, Fork (Var (FS (FS FZ)), Leaf))
let t = Fork (Var (FS FZ), Var (FS FZ))
let d = match mgu s t with Some x -> x | None -> failwith "mgu"
let s' = subst' d s
let t' = subst' d t

(* Injectivity *)

type (_, _) eq = Refl : ('a, 'a) eq

let magic : 'a 'b. 'a -> 'b =
 fun (type a b) (x : a) ->
  let module M =
    (functor
      (T : sig
         type 'a t
       end)
      ->
      struct
        let f (Refl : (a T.t, b T.t) eq) = (x :> b)
      end)
      (struct
        type 'a t = unit
      end)
  in
  M.f Refl

(* Variance and subtyping *)

type (_, +_) eq = Refl : ('a, 'a) eq

let magic : 'a 'b. 'a -> 'b =
 fun (type a) (type b) (x : a) ->
  let bad_proof (type a) =
    (Refl : (< m : a >, < m : a >) eq :> (< m : a >, < >) eq)
  in
  let downcast : type a. (a, < >) eq -> < > -> a =
   fun (type a) (Refl : (a, < >) eq) (s : < >) -> (s :> a)
  in
  (downcast bad_proof
     (object
        method m = x
      end
       :> < >))
    #m

(* Record patterns *)

type _ t = IntLit : int t | BoolLit : bool t

let check : type s. s t * s -> bool = function
  | BoolLit, false -> false
  | IntLit, 6 -> false

type ('a, 'b) pair = { fst : 'a; snd : 'b }

let check : type s. (s t, s) pair -> bool = function
  | { fst = BoolLit; snd = false } -> false
  | { fst = IntLit; snd = 6 } -> false

module type S = sig
  type t [@@immediate]
end

module F (M : S) : S = M

[%%expect
{|
module type S = sig type t [@@immediate] end
module F : functor (M : S) -> S
|}]

(* VALID DECLARATIONS *)

module A = struct
  (* Abstract types can be immediate *)
  type t [@@immediate]

  (* [@@immediate] tag here is unnecessary but valid since t has it *)
  type s = t [@@immediate]

  (* Again, valid alias even without tag *)
  type r = s

  (* Mutually recursive declarations work as well *)
  type p = q [@@immediate]
  and q = int
end

[%%expect
{|
module A :
  sig
    type t [@@immediate]
    type s = t [@@immediate]
    type r = s
    type p = q [@@immediate]
    and q = int
  end
|}]

(* Valid using with constraints *)
module type X = sig
  type t
end

module Y = struct
  type t = int
end

module Z : sig
  type t [@@immediate]
end = (Y : X with type t = int)

[%%expect
{|
module type X = sig type t end
module Y : sig type t = int end
module Z : sig type t [@@immediate] end
|}]

(* Valid using an explicit signature *)
module M_valid : S = struct
  type t = int
end

module FM_valid = F (struct
  type t = int
end)

[%%expect {|
module M_valid : S
module FM_valid : S
|}]

(* Practical usage over modules *)
module Foo : sig
  type t

  val x : t ref
end = struct
  type t = int

  let x = ref 0
end

[%%expect {|
module Foo : sig type t val x : t ref end
|}]

module Bar : sig
  type t [@@immediate]

  val x : t ref
end = struct
  type t = int

  let x = ref 0
end

[%%expect {|
module Bar : sig type t [@@immediate] val x : t ref end
|}]

let test f =
  let start = Sys.time () in
  f ();
  Sys.time () -. start

[%%expect {|
val test : (unit -> 'a) -> float = <fun>
|}]

let test_foo () =
  for i = 0 to 100_000_000 do
    Foo.x := !Foo.x
  done

[%%expect {|
val test_foo : unit -> unit = <fun>
|}]

let test_bar () =
  for i = 0 to 100_000_000 do
    Bar.x := !Bar.x
  done

[%%expect {|
val test_bar : unit -> unit = <fun>
|}]

(* Uncomment these to test. Should see substantial speedup!
let () = Printf.printf "No @@immediate: %fs\n" (test test_foo)
let () = Printf.printf "With @@immediate: %fs\n" (test test_bar) *)

(* INVALID DECLARATIONS *)

(* Cannot directly declare a non-immediate type as immediate *)
module B = struct
  type t = string [@@immediate]
end

[%%expect
{|
Line _, characters 2-31:
Error: Types marked with the immediate attribute must be
       non-pointer types like int or bool
|}]

(* Not guaranteed that t is immediate, so this is an invalid declaration *)
module C = struct
  type t
  type s = t [@@immediate]
end

[%%expect
{|
Line _, characters 2-26:
Error: Types marked with the immediate attribute must be
       non-pointer types like int or bool
|}]

(* Can't ascribe to an immediate type signature with a non-immediate type *)
module D : sig
  type t [@@immediate]
end = struct
  type t = string
end

[%%expect
{|
Line _, characters 42-70:
Error: Signature mismatch:
       Modules do not match:
         sig type t = string end
       is not included in
         sig type t [@@immediate] end
       Type declarations do not match:
         type t = string
       is not included in
         type t [@@immediate]
       the first is not an immediate type.
|}]

(* Same as above but with explicit signature *)
module M_invalid : S = struct
  type t = string
end

module FM_invalid = F (struct
  type t = string
end)

[%%expect
{|
Line _, characters 23-49:
Error: Signature mismatch:
       Modules do not match: sig type t = string end is not included in S
       Type declarations do not match:
         type t = string
       is not included in
         type t [@@immediate]
       the first is not an immediate type.
|}]

(* Can't use a non-immediate type even if mutually recursive *)
module E = struct
  type t = s [@@immediate]
  and s = string
end

[%%expect
{|
Line _, characters 2-26:
Error: Types marked with the immediate attribute must be
       non-pointer types like int or bool
|}]

(*
   Implicit unpack allows the signature in (val ...) expressions to be omitted.

   It also adds (module M : S) and (module M) patterns, relying on
   implicit (val ...) for the implementation. Such patterns can only
   be used in function definition, match clauses, and let ... in.

   New: implicit pack is also supported, and you only need to be able
   to infer the the module type path from the context.
 *)
(* ocaml -principal *)

(* Use a module pattern *)
let sort (type s) (module Set : Set.S with type elt = s) l =
  Set.elements (List.fold_right Set.add l Set.empty)

(* No real improvement here? *)
let make_set (type s) cmp : (module Set.S with type elt = s) =
  (module Set.Make (struct
    type t = s

    let compare = cmp
  end))

(* No type annotation here *)
let sort_cmp (type s) cmp =
  sort
    (module Set.Make (struct
      type t = s

      let compare = cmp
    end))

module type S = sig
  type t

  val x : t
end

let f (module M : S with type t = int) = M.x
let f (module M : S with type t = 'a) = M.x

(* Error *)
let f (type a) (module M : S with type t = a) = M.x;;

f
  (module struct
    type t = int

    let x = 1
  end)
;;

type 'a s = { s : (module S with type t = 'a) };;

{
  s =
    (module struct
      type t = int

      let x = 1
    end);
}
;;

let f { s = (module M) } = M.x

(* Error *)
let f (type a) ({ s = (module M) } : a s) = M.x

type s = { s : (module S with type t = int) }

let f { s = (module M) } = M.x
let f { s = (module M) } { s = (module N) } = M.x + N.x

module type S = sig
  val x : int
end

let f (module M : S) y (module N : S) = M.x + y + N.x

let m =
  (module struct
    let x = 3
  end)

(* Error *)
let m =
  (module struct
    let x = 3
  end : S)
;;

f m 1 m;;

f m 1
  (module struct
    let x = 2
  end)
;;

let (module M) = m in
M.x
;;

let (module M) = m

(* Error: only allowed in [let .. in] *)
class c =
  let (module M) = m in
  object end

(* Error again *)
module M = (val m)

module type S' = sig
  val f : int -> int
end
;;

(* Even works with recursion, but must be fully explicit *)
let rec (module M : S') =
  (module struct
    let f n = if n <= 0 then 1 else n * M.f (n - 1)
  end : S')
in
M.f 3
;;

(* Subtyping *)

module type S = sig
  type t
  type u

  val x : t * u
end

let f (l : (module S with type t = int and type u = bool) list) =
  (l :> (module S with type u = bool) list)

(* GADTs from the manual *)
(* the only modification is in to_string *)

module TypEq : sig
  type ('a, 'b) t

  val apply : ('a, 'b) t -> 'a -> 'b
  val refl : ('a, 'a) t
  val sym : ('a, 'b) t -> ('b, 'a) t
end = struct
  type ('a, 'b) t = ('a -> 'b) * ('b -> 'a)

  let refl = ((fun x -> x), fun x -> x)
  let apply (f, _) x = f x
  let sym (f, g) = (g, f)
end

module rec Typ : sig
  module type PAIR = sig
    type t
    and t1
    and t2

    val eq : (t, t1 * t2) TypEq.t
    val t1 : t1 Typ.typ
    val t2 : t2 Typ.typ
  end

  type 'a typ =
    | Int of ('a, int) TypEq.t
    | String of ('a, string) TypEq.t
    | Pair of (module PAIR with type t = 'a)
end =
  Typ

let int = Typ.Int TypEq.refl
let str = Typ.String TypEq.refl

let pair (type s1) (type s2) t1 t2 =
  let module P = struct
    type t = s1 * s2
    type t1 = s1
    type t2 = s2

    let eq = TypEq.refl
    let t1 = t1
    let t2 = t2
  end in
  Typ.Pair (module P)

open Typ

let rec to_string : 'a. 'a Typ.typ -> 'a -> string =
 fun (type s) t x ->
  match (t : s typ) with
  | Int eq -> Int.to_string (TypEq.apply eq x)
  | String eq -> Printf.sprintf "%S" (TypEq.apply eq x)
  | Pair (module P) ->
      let x1, x2 = TypEq.apply P.eq x in
      Printf.sprintf "(%s,%s)" (to_string P.t1 x1) (to_string P.t2 x2)

(* Wrapping maps *)
module type MapT = sig
  include Map.S

  type data
  type map

  val of_t : data t -> map
  val to_t : map -> data t
end

type ('k, 'd, 'm) map =
  (module MapT with type key = 'k and type data = 'd and type map = 'm)

let add (type k) (type d) (type m) (m : (k, d, m) map) x y s =
  let module M =
    (val m : MapT with type key = k and type data = d and type map = m)
  in
  M.of_t (M.add x y (M.to_t s))

module SSMap = struct
  include Map.Make (String)

  type data = string
  type map = data t

  let of_t x = x
  let to_t x = x
end

let ssmap =
  (module SSMap : MapT
    with type key = string
     and type data = string
     and type map = SSMap.map)

let ssmap =
  (module struct
    include SSMap
  end : MapT
    with type key = string
     and type data = string
     and type map = SSMap.map)

let ssmap =
  (let module S = struct
     include SSMap
   end in
   (module S)
    : (module MapT
         with type key = string
          and type data = string
          and type map = SSMap.map))

let ssmap =
  (module SSMap : MapT with type key = _ and type data = _ and type map = _)

let ssmap : (_, _, _) map = (module SSMap);;

add ssmap;;

open StdLabels
open MoreLabels

(* Use maps for substitutions and sets for free variables *)

module Subst = Map.Make (struct
  type t = string

  let compare = compare
end)

module Names = Set.Make (struct
  type t = string

  let compare = compare
end)

(* Variables are common to lambda and expr *)

type var = [ `Var of string ]

let subst_var ~subst : var -> _ = function
  | `Var s as x -> ( try Subst.find s subst with Not_found -> x)

let free_var : var -> _ = function `Var s -> Names.singleton s

(* The lambda language: free variables, substitutions, and evaluation *)

type 'a lambda = [ `Var of string | `Abs of string * 'a | `App of 'a * 'a ]

let free_lambda ~free_rec : _ lambda -> _ = function
  | #var as x -> free_var x
  | `Abs (s, t) -> Names.remove s (free_rec t)
  | `App (t1, t2) -> Names.union (free_rec t1) (free_rec t2)

let map_lambda ~map_rec : _ lambda -> _ = function
  | #var as x -> x
  | `Abs (s, t) as l ->
      let t' = map_rec t in
      if t == t' then l else `Abs (s, t')
  | `App (t1, t2) as l ->
      let t'1 = map_rec t1 and t'2 = map_rec t2 in
      if t'1 == t1 && t'2 == t2 then l else `App (t'1, t'2)

let next_id =
  let current = ref 3 in
  fun () ->
    incr current;
    !current

let subst_lambda ~subst_rec ~free ~subst : _ lambda -> _ = function
  | #var as x -> subst_var ~subst x
  | `Abs (s, t) as l ->
      let used = free t in
      let used_expr =
        Subst.fold subst ~init:[] ~f:(fun ~key ~data acc ->
            if Names.mem s used then data :: acc else acc)
      in
      if List.exists used_expr ~f:(fun t -> Names.mem s (free t)) then
        let name = s ^ Int.to_string (next_id ()) in
        `Abs
          (name, subst_rec ~subst:(Subst.add ~key:s ~data:(`Var name) subst) t)
      else map_lambda ~map_rec:(subst_rec ~subst:(Subst.remove s subst)) l
  | `App _ as l -> map_lambda ~map_rec:(subst_rec ~subst) l

let eval_lambda ~eval_rec ~subst l =
  match map_lambda ~map_rec:eval_rec l with
  | `App (`Abs (s, t1), t2) ->
      eval_rec (subst ~subst:(Subst.add ~key:s ~data:t2 Subst.empty) t1)
  | t -> t

(* Specialized versions to use on lambda *)

let rec free1 x = free_lambda ~free_rec:free1 x
let rec subst1 ~subst = subst_lambda ~subst_rec:subst1 ~free:free1 ~subst
let rec eval1 x = eval_lambda ~eval_rec:eval1 ~subst:subst1 x

(* The expr language of arithmetic expressions *)

type 'a expr =
  [ `Var of string
  | `Num of int
  | `Add of 'a * 'a
  | `Neg of 'a
  | `Mult of 'a * 'a ]

let free_expr ~free_rec : _ expr -> _ = function
  | #var as x -> free_var x
  | `Num _ -> Names.empty
  | `Add (x, y) -> Names.union (free_rec x) (free_rec y)
  | `Neg x -> free_rec x
  | `Mult (x, y) -> Names.union (free_rec x) (free_rec y)

(* Here map_expr helps a lot *)
let map_expr ~map_rec : _ expr -> _ = function
  | #var as x -> x
  | `Num _ as x -> x
  | `Add (x, y) as e ->
      let x' = map_rec x and y' = map_rec y in
      if x == x' && y == y' then e else `Add (x', y')
  | `Neg x as e ->
      let x' = map_rec x in
      if x == x' then e else `Neg x'
  | `Mult (x, y) as e ->
      let x' = map_rec x and y' = map_rec y in
      if x == x' && y == y' then e else `Mult (x', y')

let subst_expr ~subst_rec ~subst : _ expr -> _ = function
  | #var as x -> subst_var ~subst x
  | #expr as e -> map_expr ~map_rec:(subst_rec ~subst) e

let eval_expr ~eval_rec e =
  match map_expr ~map_rec:eval_rec e with
  | `Add (`Num m, `Num n) -> `Num (m + n)
  | `Neg (`Num n) -> `Num (-n)
  | `Mult (`Num m, `Num n) -> `Num (m * n)
  | #expr as e -> e

(* Specialized versions *)

let rec free2 x = free_expr ~free_rec:free2 x
let rec subst2 ~subst = subst_expr ~subst_rec:subst2 ~subst
let rec eval2 x = eval_expr ~eval_rec:eval2 x

(* The lexpr language, reunion of lambda and expr *)

type lexpr =
  [ `Var of string
  | `Abs of string * lexpr
  | `App of lexpr * lexpr
  | `Num of int
  | `Add of lexpr * lexpr
  | `Neg of lexpr
  | `Mult of lexpr * lexpr ]

let rec free : lexpr -> _ = function
  | #lambda as x -> free_lambda ~free_rec:free x
  | #expr as x -> free_expr ~free_rec:free x

let rec subst ~subst:s : lexpr -> _ = function
  | #lambda as x -> subst_lambda ~subst_rec:subst ~subst:s ~free x
  | #expr as x -> subst_expr ~subst_rec:subst ~subst:s x

let rec eval : lexpr -> _ = function
  | #lambda as x -> eval_lambda ~eval_rec:eval ~subst x
  | #expr as x -> eval_expr ~eval_rec:eval x

let rec print = function
  | `Var id -> print_string id
  | `Abs (id, l) ->
      print_string (" " ^ id ^ " . ");
      print l
  | `App (l1, l2) ->
      print l1;
      print_string " ";
      print l2
  | `Num x -> print_int x
  | `Add (e1, e2) ->
      print e1;
      print_string " + ";
      print e2
  | `Neg e ->
      print_string "-";
      print e
  | `Mult (e1, e2) ->
      print e1;
      print_string " * ";
      print e2

let () =
  let e1 = eval1 (`App (`Abs ("x", `Var "x"), `Var "y")) in
  let e2 = eval2 (`Add (`Mult (`Num 3, `Neg (`Num 2)), `Var "x")) in
  let e3 =
    eval (`Add (`App (`Abs ("x", `Mult (`Var "x", `Var "x")), `Num 2), `Num 5))
  in
  print e1;
  print_newline ();
  print e2;
  print_newline ();
  print e3;
  print_newline ()
(* Full fledge version, using objects to structure code *)

open StdLabels
open MoreLabels

(* Use maps for substitutions and sets for free variables *)

module Subst = Map.Make (struct
  type t = string

  let compare = compare
end)

module Names = Set.Make (struct
  type t = string

  let compare = compare
end)

(* To build recursive objects *)

let lazy_fix make =
  let rec obj () = make (lazy (obj ()) : _ Lazy.t) in
  obj ()

let ( !! ) = Lazy.force

(* The basic operations *)

class type ['a, 'b] ops = object
  method free : x:'b -> ?y:'c -> Names.t
  method subst : sub:'a Subst.t -> 'b -> 'a
  method eval : 'b -> 'a
end

(* Variables are common to lambda and expr *)

type var = [ `Var of string ]

class ['a] var_ops =
  object (self : ('a, var) #ops)
    constraint 'a = [> var ]
    method subst ~sub (`Var s as x) = try Subst.find s sub with Not_found -> x
    method free (`Var s) = Names.singleton s
    method eval (#var as v) = v
  end

(* The lambda language: free variables, substitutions, and evaluation *)

type 'a lambda = [ `Var of string | `Abs of string * 'a | `App of 'a * 'a ]

let next_id =
  let current = ref 3 in
  fun () ->
    incr current;
    !current

class ['a] lambda_ops (ops : ('a, 'a) #ops Lazy.t) =
  let var : 'a var_ops = new var_ops
  and free = lazy !!ops#free
  and subst = lazy !!ops#subst
  and eval = lazy !!ops#eval in
  object (self : ('a, 'a lambda) #ops)
    constraint 'a = [> 'a lambda ]

    method free =
      function
      | #var as x -> var#free x
      | `Abs (s, t) -> Names.remove s (!!free t)
      | `App (t1, t2) -> Names.union (!!free t1) (!!free t2)

    method map ~f =
      function
      | #var as x -> x
      | `Abs (s, t) as l ->
          let t' = f t in
          if t == t' then l else `Abs (s, t')
      | `App (t1, t2) as l ->
          let t'1 = f t1 and t'2 = f t2 in
          if t'1 == t1 && t'2 == t2 then l else `App (t'1, t'2)

    method subst ~sub =
      function
      | #var as x -> var#subst ~sub x
      | `Abs (s, t) as l ->
          let used = !!free t in
          let used_expr =
            Subst.fold sub ~init:[] ~f:(fun ~key ~data acc ->
                if Names.mem s used then data :: acc else acc)
          in
          if List.exists used_expr ~f:(fun t -> Names.mem s (!!free t)) then
            let name = s ^ Int.to_string (next_id ()) in
            `Abs (name, !!subst ~sub:(Subst.add ~key:s ~data:(`Var name) sub) t)
          else self#map ~f:(!!subst ~sub:(Subst.remove s sub)) l
      | `App _ as l -> self#map ~f:(!!subst ~sub) l

    method eval l =
      match self#map ~f:!!eval l with
      | `App (`Abs (s, t1), t2) ->
          !!eval (!!subst ~sub:(Subst.add ~key:s ~data:t2 Subst.empty) t1)
      | t -> t
  end

(* Operations specialized to lambda *)

let lambda = lazy_fix (new lambda_ops)

(* The expr language of arithmetic expressions *)

type 'a expr =
  [ `Var of string
  | `Num of int
  | `Add of 'a * 'a
  | `Neg of 'a
  | `Mult of 'a * 'a ]

class ['a] expr_ops (ops : ('a, 'a) #ops Lazy.t) =
  let var : 'a var_ops = new var_ops
  and free = lazy !!ops#free
  and subst = lazy !!ops#subst
  and eval = lazy !!ops#eval in
  object (self : ('a, 'a expr) #ops)
    constraint 'a = [> 'a expr ]

    method free =
      function
      | #var as x -> var#free x
      | `Num _ -> Names.empty
      | `Add (x, y) -> Names.union (!!free x) (!!free y)
      | `Neg x -> !!free x
      | `Mult (x, y) -> Names.union (!!free x) (!!free y)

    method map ~f =
      function
      | #var as x -> x
      | `Num _ as x -> x
      | `Add (x, y) as e ->
          let x' = f x and y' = f y in
          if x == x' && y == y' then e else `Add (x', y')
      | `Neg x as e ->
          let x' = f x in
          if x == x' then e else `Neg x'
      | `Mult (x, y) as e ->
          let x' = f x and y' = f y in
          if x == x' && y == y' then e else `Mult (x', y')

    method subst ~sub =
      function
      | #var as x -> var#subst ~sub x
      | #expr as e -> self#map ~f:(!!subst ~sub) e

    method eval (#expr as e) =
      match self#map ~f:!!eval e with
      | `Add (`Num m, `Num n) -> `Num (m + n)
      | `Neg (`Num n) -> `Num (-n)
      | `Mult (`Num m, `Num n) -> `Num (m * n)
      | e -> e
  end

(* Specialized versions *)

let expr = lazy_fix (new expr_ops)

(* The lexpr language, reunion of lambda and expr *)

type 'a lexpr = [ 'a lambda | 'a expr ]

class ['a] lexpr_ops (ops : ('a, 'a) #ops Lazy.t) =
  let lambda = new lambda_ops ops in
  let expr = new expr_ops ops in
  object (self : ('a, 'a lexpr) #ops)
    constraint 'a = [> 'a lexpr ]

    method free =
      function #lambda as x -> lambda#free x | #expr as x -> expr#free x

    method subst ~sub =
      function
      | #lambda as x -> lambda#subst ~sub x
      | #expr as x -> expr#subst ~sub x

    method eval =
      function #lambda as x -> lambda#eval x | #expr as x -> expr#eval x
  end

let lexpr = lazy_fix (new lexpr_ops)

let rec print = function
  | `Var id -> print_string id
  | `Abs (id, l) ->
      print_string (" " ^ id ^ " . ");
      print l
  | `App (l1, l2) ->
      print l1;
      print_string " ";
      print l2
  | `Num x -> print_int x
  | `Add (e1, e2) ->
      print e1;
      print_string " + ";
      print e2
  | `Neg e ->
      print_string "-";
      print e
  | `Mult (e1, e2) ->
      print e1;
      print_string " * ";
      print e2

let () =
  let e1 = lambda#eval (`App (`Abs ("x", `Var "x"), `Var "y")) in
  let e2 = expr#eval (`Add (`Mult (`Num 3, `Neg (`Num 2)), `Var "x")) in
  let e3 =
    lexpr#eval
      (`Add (`App (`Abs ("x", `Mult (`Var "x", `Var "x")), `Num 2), `Num 5))
  in
  print e1;
  print_newline ();
  print e2;
  print_newline ();
  print e3;
  print_newline ()
(* Full fledge version, using objects to structure code *)

open StdLabels
open MoreLabels

(* Use maps for substitutions and sets for free variables *)

module Subst = Map.Make (struct
  type t = string

  let compare = compare
end)

module Names = Set.Make (struct
  type t = string

  let compare = compare
end)

(* To build recursive objects *)

let lazy_fix make =
  let rec obj () = make (lazy (obj ()) : _ Lazy.t) in
  obj ()

let ( !! ) = Lazy.force

(* The basic operations *)

class type ['a, 'b] ops = object
  method free : 'b -> Names.t
  method subst : sub:'a Subst.t -> 'b -> 'a
  method eval : 'b -> 'a
end

(* Variables are common to lambda and expr *)

type var = [ `Var of string ]

let var =
  object (self : ([> var ], var) #ops)
    method subst ~sub (`Var s as x) = try Subst.find s sub with Not_found -> x
    method free (`Var s) = Names.singleton s
    method eval (#var as v) = v
  end

(* The lambda language: free variables, substitutions, and evaluation *)

type 'a lambda = [ `Var of string | `Abs of string * 'a | `App of 'a * 'a ]

let next_id =
  let current = ref 3 in
  fun () ->
    incr current;
    !current

let lambda_ops (ops : ('a, 'a) #ops Lazy.t) =
  let free = lazy !!ops#free
  and subst = lazy !!ops#subst
  and eval = lazy !!ops#eval in
  object (self : ([> 'a lambda ], 'a lambda) #ops)
    method free =
      function
      | #var as x -> var#free x
      | `Abs (s, t) -> Names.remove s (!!free t)
      | `App (t1, t2) -> Names.union (!!free t1) (!!free t2)

    method private map ~f =
      function
      | #var as x -> x
      | `Abs (s, t) as l ->
          let t' = f t in
          if t == t' then l else `Abs (s, t')
      | `App (t1, t2) as l ->
          let t'1 = f t1 and t'2 = f t2 in
          if t'1 == t1 && t'2 == t2 then l else `App (t'1, t'2)

    method subst ~sub =
      function
      | #var as x -> var#subst ~sub x
      | `Abs (s, t) as l ->
          let used = !!free t in
          let used_expr =
            Subst.fold sub ~init:[] ~f:(fun ~key ~data acc ->
                if Names.mem s used then data :: acc else acc)
          in
          if List.exists used_expr ~f:(fun t -> Names.mem s (!!free t)) then
            let name = s ^ Int.to_string (next_id ()) in
            `Abs (name, !!subst ~sub:(Subst.add ~key:s ~data:(`Var name) sub) t)
          else self#map ~f:(!!subst ~sub:(Subst.remove s sub)) l
      | `App _ as l -> self#map ~f:(!!subst ~sub) l

    method eval l =
      match self#map ~f:!!eval l with
      | `App (`Abs (s, t1), t2) ->
          !!eval (!!subst ~sub:(Subst.add ~key:s ~data:t2 Subst.empty) t1)
      | t -> t
  end

(* Operations specialized to lambda *)

let lambda = lazy_fix lambda_ops

(* The expr language of arithmetic expressions *)

type 'a expr =
  [ `Var of string
  | `Num of int
  | `Add of 'a * 'a
  | `Neg of 'a
  | `Mult of 'a * 'a ]

let expr_ops (ops : ('a, 'a) #ops Lazy.t) =
  let free = lazy !!ops#free
  and subst = lazy !!ops#subst
  and eval = lazy !!ops#eval in
  object (self : ([> 'a expr ], 'a expr) #ops)
    method free =
      function
      | #var as x -> var#free x
      | `Num _ -> Names.empty
      | `Add (x, y) -> Names.union (!!free x) (!!free y)
      | `Neg x -> !!free x
      | `Mult (x, y) -> Names.union (!!free x) (!!free y)

    method private map ~f =
      function
      | #var as x -> x
      | `Num _ as x -> x
      | `Add (x, y) as e ->
          let x' = f x and y' = f y in
          if x == x' && y == y' then e else `Add (x', y')
      | `Neg x as e ->
          let x' = f x in
          if x == x' then e else `Neg x'
      | `Mult (x, y) as e ->
          let x' = f x and y' = f y in
          if x == x' && y == y' then e else `Mult (x', y')

    method subst ~sub =
      function
      | #var as x -> var#subst ~sub x
      | #expr as e -> self#map ~f:(!!subst ~sub) e

    method eval (#expr as e) =
      match self#map ~f:!!eval e with
      | `Add (`Num m, `Num n) -> `Num (m + n)
      | `Neg (`Num n) -> `Num (-n)
      | `Mult (`Num m, `Num n) -> `Num (m * n)
      | e -> e
  end

(* Specialized versions *)

let expr = lazy_fix expr_ops

(* The lexpr language, reunion of lambda and expr *)

type 'a lexpr = [ 'a lambda | 'a expr ]

let lexpr_ops (ops : ('a, 'a) #ops Lazy.t) =
  let lambda = lambda_ops ops in
  let expr = expr_ops ops in
  object (self : ([> 'a lexpr ], 'a lexpr) #ops)
    method free =
      function #lambda as x -> lambda#free x | #expr as x -> expr#free x

    method subst ~sub =
      function
      | #lambda as x -> lambda#subst ~sub x
      | #expr as x -> expr#subst ~sub x

    method eval =
      function #lambda as x -> lambda#eval x | #expr as x -> expr#eval x
  end

let lexpr = lazy_fix lexpr_ops

let rec print = function
  | `Var id -> print_string id
  | `Abs (id, l) ->
      print_string (" " ^ id ^ " . ");
      print l
  | `App (l1, l2) ->
      print l1;
      print_string " ";
      print l2
  | `Num x -> print_int x
  | `Add (e1, e2) ->
      print e1;
      print_string " + ";
      print e2
  | `Neg e ->
      print_string "-";
      print e
  | `Mult (e1, e2) ->
      print e1;
      print_string " * ";
      print e2

let () =
  let e1 = lambda#eval (`App (`Abs ("x", `Var "x"), `Var "y")) in
  let e2 = expr#eval (`Add (`Mult (`Num 3, `Neg (`Num 2)), `Var "x")) in
  let e3 =
    lexpr#eval
      (`Add (`App (`Abs ("x", `Mult (`Var "x", `Var "x")), `Num 2), `Num 5))
  in
  print e1;
  print_newline ();
  print e2;
  print_newline ();
  print e3;
  print_newline ()

type sexp = A of string | L of sexp list
type 'a t = 'a array

let _ = fun (_ : 'a t) -> ()
let array_of_sexp _ _ = [||]
let sexp_of_array _ _ = A "foo"
let sexp_of_int _ = A "42"
let int_of_sexp _ = 42

let t_of_sexp : 'a. (sexp -> 'a) -> sexp -> 'a t =
  let _tp_loc = "core_array.ml.t" in
  fun _of_a -> fun t -> (array_of_sexp _of_a) t

let _ = t_of_sexp

let sexp_of_t : 'a. ('a -> sexp) -> 'a t -> sexp =
 fun _of_a -> fun v -> (sexp_of_array _of_a) v

let _ = sexp_of_t

module T = struct
  module Int = struct
    type t_ = int array

    let _ = fun (_ : t_) -> ()

    let t__of_sexp : sexp -> t_ =
      let _tp_loc = "core_array.ml.T.Int.t_" in
      fun t -> (array_of_sexp int_of_sexp) t

    let _ = t__of_sexp
    let sexp_of_t_ : t_ -> sexp = fun v -> (sexp_of_array sexp_of_int) v
    let _ = sexp_of_t_
  end
end

module type Permissioned = sig
  type ('a, -'perms) t
end

module Permissioned : sig
  type ('a, -'perms) t

  include sig
    val t_of_sexp : (sexp -> 'a) -> (sexp -> 'perms) -> sexp -> ('a, 'perms) t
    val sexp_of_t : ('a -> sexp) -> ('perms -> sexp) -> ('a, 'perms) t -> sexp
  end

  module Int : sig
    type nonrec -'perms t = (int, 'perms) t

    include sig
      val t_of_sexp : (sexp -> 'perms) -> sexp -> 'perms t
      val sexp_of_t : ('perms -> sexp) -> 'perms t -> sexp
    end
  end
end = struct
  type ('a, -'perms) t = 'a array

  let _ = fun (_ : ('a, 'perms) t) -> ()

  let t_of_sexp :
      'a 'perms. (sexp -> 'a) -> (sexp -> 'perms) -> sexp -> ('a, 'perms) t =
    let _tp_loc = "core_array.ml.Permissioned.t" in
    fun _of_a -> fun _of_perms -> fun t -> (array_of_sexp _of_a) t

  let _ = t_of_sexp

  let sexp_of_t :
      'a 'perms. ('a -> sexp) -> ('perms -> sexp) -> ('a, 'perms) t -> sexp =
   fun _of_a -> fun _of_perms -> fun v -> (sexp_of_array _of_a) v

  let _ = sexp_of_t

  module Int = struct
    include T.Int

    type -'perms t = t_

    let _ = fun (_ : 'perms t) -> ()

    let t_of_sexp : 'perms. (sexp -> 'perms) -> sexp -> 'perms t =
      let _tp_loc = "core_array.ml.Permissioned.Int.t" in
      fun _of_perms -> fun t -> t__of_sexp t

    let _ = t_of_sexp

    let sexp_of_t : 'perms. ('perms -> sexp) -> 'perms t -> sexp =
     fun _of_perms -> fun v -> sexp_of_t_ v

    let _ = sexp_of_t
  end
end

type 'a foo = { x : 'a; y : int }

let r = { { x = 0; y = 0 } with x = 0 }
let r' : string foo = r

external foo : int = "%ignore"

let _ = foo ()

type 'a t = [ `A of 'a t t ] as 'a

(* fails *)

type 'a t = [ `A of 'a t t ]

(* fails *)

type 'a t = [ `A of 'a t t ] constraint 'a = 'a t
type 'a t = [ `A of 'a t ] constraint 'a = 'a t
type 'a t = [ `A of 'a ] as 'a

type 'a v = [ `A of u v ] constraint 'a = t
and t = u
and u = t

(* fails *)

type 'a t = 'a

let f (x : 'a t as 'a) = ()

(* fails *)

let f (x : 'a t) (y : 'a) = x = y

(* PR#6505 *)
module type PR6505 = sig
  type 'o is_an_object = < .. > as 'o
  and 'o abs constraint 'o = 'o is_an_object

  val abs : 'o is_an_object -> 'o abs
  val unabs : 'o abs -> 'o
end

(* fails *)
(* PR#5835 *)
let f ~x = x + 1;;

f ?x:0;;

(* PR#6352 *)
let foo (f : unit -> unit) = ()
let g ?x () = ();;

foo
  (();
   g)
;;

(* PR#5748 *)
foo (fun ?opt () -> ());;

(* fails *)
(* PR#5907 *)

type 'a t = 'a

let f (g : 'a list -> 'a t -> 'a) s = g s s
let f (g : 'a * 'b -> 'a t -> 'a) s = g s s

type ab = [ `A | `B ]

let f (x : [ `A ]) = match x with #ab -> 1

let f x =
  ignore (match x with #ab -> 1);
  ignore (x : [ `A ])

let f x =
  ignore (match x with `A | `B -> 1);
  ignore (x : [ `A ])

let f (x : [< `A | `B ]) = match x with `A | `B | `C -> 0

(* warn *)
let f (x : [ `A | `B ]) = match x with `A | `B | `C -> 0

(* fail *)

(* PR#6787 *)
let revapply x f = f x

let f x (g : [< `Foo ]) =
  let y = (`Bar x, g) in
  revapply y (fun (`Bar i, _) -> i)

(* f : 'a -> [< `Foo ] -> 'a *)

let rec x =
  [| x |];
  1.

let rec x =
  let u = [| y |] in
  10.

and y = 1.

type 'a t
type a

let f : < .. > t -> unit = fun _ -> ()
let g : [< `b ] t -> unit = fun _ -> ()
let h : [> `b ] t -> unit = fun _ -> ()
let _ = fun (x : a t) -> f x
let _ = fun (x : a t) -> g x
let _ = fun (x : a t) -> h x

(* PR#7012 *)

type t = [ 'A_name | `Hi ]

let f (x : 'id_arg) = x
let f (x : 'Id_arg) = x

(* undefined labels *)
type t = { x : int; y : int };;

{ x = 3; z = 2 };;
fun { x = 3; z = 2 } -> ();;

(* mixed labels *)
{ x = 3; contents = 2 };;

(* private types *)
type u = private { mutable u : int };;

{ u = 3 };;
fun x -> x.u <- 3;;

(* Punning and abbreviations *)
module M = struct
  type t = { x : int; y : int }
end

let f { M.x; y } = x + y
let r = { M.x = 1; y = 2 }
let z = f r

(* messages *)
type foo = { mutable y : int }

let f (r : int) = r.y <- 3

(* bugs *)
type foo = { y : int; z : int }
type bar = { x : int }

let f (r : bar) = ({ r with z = 3 } : foo)

type foo = { x : int }

let r : foo = { ZZZ.x = 2 };;

(ZZZ.X : int option);;

(* PR#5865 *)
let f (x : Complex.t) = x.Complex.z

(* PR#6394 *)

module rec X : sig
  type t = int * bool
end = struct
  type t = A | B

  let f = function A | B -> 0
end

(* PR#6768 *)

type _ prod = Prod : ('a * 'y) prod

let f : type t. t prod -> _ = function
  | Prod ->
      let module M = struct
        type d = d * d
      end in
      ()

let (a : M.a) = 2
let (b : M.b) = 2
let _ = A.a = B.b

module Std = struct
  module Hash = Hashtbl
end

open Std
module Hash1 : module type of Hash = Hash

module Hash2 : sig
  include module type of Hash
end =
  Hash

let f1 (x : (_, _) Hash1.t) = (x : (_, _) Hashtbl.t)
let f2 (x : (_, _) Hash2.t) = (x : (_, _) Hashtbl.t)

(* Another case, not using include *)

module Std2 = struct
  module M = struct
    type t
  end
end

module Std' = Std2
module M' : module type of Std'.M = Std2.M

let f3 (x : M'.t) = (x : Std2.M.t)

(* original report required Core_kernel:
module type S = sig
open Core_kernel.Std

module Hashtbl1 : module type of Hashtbl
module Hashtbl2 : sig
  include (module type of Hashtbl)
end

module Coverage : Core_kernel.Std.Hashable

type types = unit constraint 'a Coverage.Table.t = (Coverage.t, 'a) Hashtbl1.t
type doesnt_type = unit
  constraint 'a Coverage.Table.t = (Coverage.t, 'a) Hashtbl2.t
end
*)
module type INCLUDING = sig
  include module type of List
  include module type of ListLabels
end

module Including_typed : INCLUDING = struct
  include List
  include ListLabels
end

module X = struct
  module type SIG = sig
    type t = int

    val x : t
  end

  module F (Y : SIG) : SIG = struct
    type t = Y.t

    let x = Y.x
  end
end

module DUMMY = struct
  type t = int

  let x = 2
end

let x = (3 : X.F(DUMMY).t)

module X2 = struct
  module type SIG = sig
    type t = int

    val x : t
  end

  module F (Y : SIG) (Z : SIG) = struct
    type t = Y.t

    let x = Y.x

    type t' = Z.t

    let x' = Z.x
  end
end

let x = (3 : X2.F(DUMMY)(DUMMY).t)
let x = (3 : X2.F(DUMMY)(DUMMY).t')

module F (M : sig
  type 'a t
  type 'a u = string

  val f : unit -> _ u t
end) =
struct
  let t = M.f ()
end

type 't a = [ `A ]
type 't wrap = 't constraint 't = [> 't wrap a ]
type t = t a wrap

module T = struct
  let foo : 't wrap -> 't wrap -> unit = fun _ _ -> ()
  let bar : 'a a wrap as 'a = `A
end

module Good : sig
  val bar : t
  val foo : t -> t -> unit
end =
  T

module Bad : sig
  val foo : t -> t -> unit
  val bar : t
end =
  T

module M : sig
  module type T

  module F (X : T) : sig end
end = struct
  module type T = sig end

  module F (X : T) = struct end
end

module type T = M.T

module F : functor (X : T) -> sig end = M.F

module type S = sig
  type t = { a : int; b : int }
end

let f (module M : S with type t = int) = { M.a = 0 }
let flag = ref false

module F
    (S : sig
      module type T
    end)
    (A : S.T)
    (B : S.T) =
struct
  module X = (val if !flag then (module A) else (module B) : S.T)
end

(* If the above were accepted, one could break soundness *)
module type S = sig
  type t

  val x : t
end

module Float = struct
  type t = float

  let x = 0.0
end

module Int = struct
  type t = int

  let x = 0
end

module M = F (struct
  module type T = S
end)

let () = flag := false

module M1 = M (Float) (Int)

let () = flag := true

module M2 = M (Float) (Int)

let _ = [| M2.X.x; M1.X.x |]

module type PR6513 = sig
  module type S = sig
    type u
  end

  module type T = sig
    type 'a wrap
    type uri
  end

  module Make : functor (Html5 : T with type 'a wrap = 'a) ->
    S with type u = < foo : Html5.uri >
end

(* Requires -package tyxml
module type PR6513_orig = sig
module type S =
sig
        type t
        type u
end

module Make: functor (Html5: Html5_sigs.T
                             with type 'a Xml.wrap = 'a and
                             type 'a wrap = 'a and
                             type 'a list_wrap = 'a list)
                     -> S with type t = Html5_types.div Html5.elt and
                               type u = < foo: Html5.uri >
end
*)
module type S = sig
  include Set.S

  module E : sig
    val x : int
  end
end

module Make (O : Set.OrderedType) : S with type elt = O.t = struct
  include Set.Make (O)

  module E = struct
    let x = 1
  end
end

module rec A : Set.OrderedType = struct
  type t = int

  let compare = Stdlib.compare
end

and B : S = struct
  module C = Make (A)
  include C
end

module type S = sig
  module type T

  module X : T
end

module F (X : S) = X.X

module M = struct
  module type T = sig
    type t
  end

  module X = struct
    type t = int
  end
end

type t = F(M).t

module Common0 = struct
  type msg = Msg

  let handle_msg = ref (function _ -> failwith "Unable to handle message")

  let extend_handle f =
    let old = !handle_msg in
    handle_msg := f old

  let q : _ Queue.t = Queue.create ()
  let add msg = Queue.add msg q
  let handle_queue_messages () = Queue.iter !handle_msg q
end

let q' : Common0.msg Queue.t = Common0.q

module Common = struct
  type msg = ..

  let handle_msg = ref (function _ -> failwith "Unable to handle message")

  let extend_handle f =
    let old = !handle_msg in
    handle_msg := f old

  let q : _ Queue.t = Queue.create ()
  let add msg = Queue.add msg q
  let handle_queue_messages () = Queue.iter !handle_msg q
end

module M1 = struct
  type Common.msg += Reload of string | Alert of string

  let handle fallback = function
    | Reload s -> print_endline ("Reload " ^ s)
    | Alert s -> print_endline ("Alert " ^ s)
    | x -> fallback x

  let () = Common.extend_handle handle
  let () = Common.add (Reload "config.file")
  let () = Common.add (Alert "Initialisation done")
end

let should_reject =
  let table = Hashtbl.create 1 in
  fun x y -> Hashtbl.add table x y

type 'a t = 'a option

let is_some = function None -> false | Some _ -> true
let should_accept ?x () = is_some x

include struct
  let foo `Test = ()
  let wrap f `Test = f
  let bar = wrap ()
end

let f () =
  let module S = String in
  let module N = Map.Make (S) in
  N.add "sum" 41 N.empty

module X = struct
  module Y = struct
    module type S = sig
      type t
    end
  end
end

(* open X  (* works! *) *)
module Y = X.Y

type 'a arg_t = 'at constraint 'a = (module Y.S with type t = 'at)
type t = (module X.Y.S with type t = unit)

let f (x : t arg_t) = ()
let () = f ()

module type S = sig
  type a
  type b
end

module Foo
    (Bar : S with type a = private [> `A ])
    (Baz : S with type b = private < b : Bar.b ; .. >) =
struct end

module A = struct
  module type A_S = sig end

  type t = (module A_S)
end

module type S = sig
  type t
end

let f (type a) (module X : S with type t = a) = ()
let _ = f (module A) (* ok *)

module A_annotated_alias : S with type t = (module A.A_S) = A

let _ = f (module A_annotated_alias) (* ok *)
let _ = f (module A_annotated_alias : S with type t = (module A.A_S)) (* ok *)

module A_alias = A

module A_alias_expanded = struct
  include A_alias
end

let _ = f (module A_alias_expanded : S with type t = (module A.A_S)) (* ok *)
let _ = f (module A_alias_expanded) (* ok *)
let _ = f (module A_alias : S with type t = (module A.A_S)) (* doesn't type *)
let _ = f (module A_alias) (* doesn't type either *)

module Foo (Bar : sig
  type a = private [> `A ]
end) (Baz : module type of struct
  include Bar
end) =
struct end

module Bazoinks = struct
  type a = [ `A ]
end

module Bug = Foo (Bazoinks) (Bazoinks)
(* PR#6992, reported by Stephen Dolan *)

type (_, _) eq = Eq : ('a, 'a) eq

let cast : type a b. (a, b) eq -> a -> b = fun Eq x -> x

module Fix (F : sig
  type 'a f
end) =
struct
  type 'a fix = ('a, 'a F.f) eq

  let uniq (type a) (type b) (Eq : a fix) (Eq : b fix) : (a, b) eq = Eq
end

(* This would allow:
module FixId = Fix (struct type 'a f = 'a end)
 let bad : (int, string) eq = FixId.uniq Eq Eq
 let _ = Printf.printf "Oh dear: %s" (cast bad 42)
*)
module M = struct
  module type S = sig
    type a

    val v : a
  end

  type 'a s = (module S with type a = 'a)
end

module B = struct
  class type a = object
    method a : 'a. 'a M.s -> 'a
  end
end

module M' = M
module B' = B

class b : B.a =
  object
    method a : 'a. 'a M.s -> 'a =
      fun (type a) ((module X) : (module M.S with type a = a)) -> X.v
  end

class b' : B.a =
  object
    method a : 'a. 'a M'.s -> 'a =
      fun (type a) ((module X) : (module M'.S with type a = a)) -> X.v
  end

module type FOO = sig
  type t
end

module type BAR = sig
  (* Works: module rec A : (sig include FOO with type t = < b:B.t > end) *)
  module rec A : (FOO with type t = < b : B.t >)
  and B : FOO
end

module A = struct
  module type S

  module S = struct end
end

module F (_ : sig end) = struct
  module type S

  module S = A.S
end

module M = struct end
module N = M
module G (X : F(N).S) : A.S = X

module F (_ : sig end) = struct
  module type S
end

module M = struct end
module N = M
module G (X : F(N).S) : F(M).S = X

module M : sig
  type make_dec

  val add_dec : make_dec -> unit
end = struct
  type u

  module Fast : sig
    type 'd t

    val create : unit -> 'd t

    module type S = sig
      module Data : sig
        type t
      end

      val key : Data.t t
    end

    module Register (D : S) : sig end

    val attach : 'd t -> 'd -> unit
  end = struct
    type 'd t = unit

    let create () = ()

    module type S = sig
      module Data : sig
        type t
      end

      val key : Data.t t
    end

    module Register (D : S) = struct end

    let attach _ _ = ()
  end

  type make_dec

  module Dem = struct
    module Data = struct
      type t = make_dec
    end

    let key = Fast.create ()
  end

  module EDem = Fast.Register (Dem)

  let add_dec dec = Fast.attach Dem.key dec
end

(* simpler version *)

module Simple = struct
  type 'a t

  module type S = sig
    module Data : sig
      type t
    end

    val key : Data.t t
  end

  module Register (D : S) = struct
    let key = D.key
  end

  module M = struct
    module Data = struct
      type t = int
    end

    let key : _ t = Obj.magic ()
  end
end

module EM = Simple.Register (Simple.M);;

Simple.M.key;;

module Simple2 = struct
  type 'a t

  module type S = sig
    module Data : sig
      type t
    end

    val key : Data.t t
  end

  module M = struct
    module Data = struct
      type t = int
    end

    let key : _ t = Obj.magic ()
  end

  module Register (D : S) = struct
    let key = D.key
  end

  module EM = Simple.Register (Simple.M)

  let k : M.Data.t t = M.key
end

module rec M : sig
  external f : int -> int = "%identity"
end = struct
  external f : int -> int = "%identity"
end
(* with module *)

module type S = sig
  type t
  and s = t
end

module type S' = S with type t := int

module type S = sig
  module rec M : sig end
  and N : sig end
end

module type S' = S with module M := String

(* with module type *)
(*
module type S = sig module type T module F(X:T) : T end;;
module type T0 = sig type t end;;
module type S1 = S with module type T = T0;;
module type S2 = S with module type T := T0;;
module type S3 = S with module type T := sig type t = int end;;
module H = struct
  include (Hashtbl : module type of Hashtbl with
           type statistics := Hashtbl.statistics
           and module type S := Hashtbl.S
           and module Make := Hashtbl.Make
           and module MakeSeeded := Hashtbl.MakeSeeded
           and module type SeededS := Hashtbl.SeededS
           and module type HashedType := Hashtbl.HashedType
           and module type SeededHashedType := Hashtbl.SeededHashedType)
end;;
*)

(* A subtle problem appearing with -principal *)
type -'a t

class type c = object
  method m : [ `A ] t
end

module M : sig
  val v : (#c as 'a) -> 'a
end = struct
  let v x =
    ignore (x :> c);
    x
end

(* PR#4838 *)

let id =
  let module M = struct end in
  fun x -> x

(* PR#4511 *)

let ko =
  let module M = struct end in
  fun _ -> ()

(* PR#5993 *)

module M : sig
  type -'a t = private int
end = struct
  type +'a t = private int
end

(* PR#6005 *)

module type A = sig
  type t = X of int
end

type u = X of bool

module type B = A with type t = u

(* fail *)

(* PR#5815 *)
(* ---> duplicated exception name is now an error *)

module type S = sig
  exception Foo of int
  exception Foo of bool
end

(* PR#6410 *)

module F (X : sig end) = struct
  let x = 3
end
;;

F.x;;

(* fail *)
module C = Char;;

C.chr 66;;

module C' : module type of Char = C;;

C'.chr 66;;

module C3 = struct
  include Char
end
;;

C3.chr 66;;

let f x =
  let module M = struct
    module L = List
  end in
  M.L.length x

let g x =
  let module L = List in
  L.length (L.map succ x)

module F (X : sig end) = Char
module C4 = F (struct end);;

C4.chr 66;;

module G (X : sig end) = struct
  module M = X
end

(* does not alias X *)
module M = G (struct end)

module M' = struct
  module N = struct
    let x = 1
  end

  module N' = N
end
;;

M'.N'.x;;

module M'' : sig
  module N' : sig
    val x : int
  end
end =
  M'
;;

M''.N'.x;;

module M2 = struct
  include M'
end

module M3 : sig
  module N' : sig
    val x : int
  end
end = struct
  include M'
end
;;

M3.N'.x;;

module M3' : sig
  module N' : sig
    val x : int
  end
end =
  M2
;;

M3'.N'.x;;

module M4 : sig
  module N' : sig
    val x : int
  end
end = struct
  module N = struct
    let x = 1
  end

  module N' = N
end
;;

M4.N'.x;;

module F (X : sig end) = struct
  module N = struct
    let x = 1
  end

  module N' = N
end

module G : functor (X : sig end) -> sig
  module N' : sig
    val x : int
  end
end =
  F

module M5 = G (struct end);;

M5.N'.x;;

module M = struct
  module D = struct
    let y = 3
  end

  module N = struct
    let x = 1
  end

  module N' = N
end

module M1 : sig
  module N : sig
    val x : int
  end

  module N' = N
end =
  M
;;

M1.N'.x;;

module M2 : sig
  module N' : sig
    val x : int
  end
end = (
  M :
    sig
      module N : sig
        val x : int
      end

      module N' = N
    end)
;;

M2.N'.x;;

open M;;

N'.x;;

module M = struct
  module C = Char
  module C' = C
end

module M1 : sig
  module C : sig
    val escaped : char -> string
  end

  module C' = C
end =
  M
;;

(* sound, but should probably fail *)
M1.C'.escaped 'A';;

module M2 : sig
  module C' : sig
    val chr : int -> char
  end
end = (
  M :
    sig
      module C : sig
        val chr : int -> char
      end

      module C' = C
    end)
;;

M2.C'.chr 66;;
StdLabels.List.map;;

module Q = Queue

exception QE = Q.Empty;;

try Q.pop (Q.create ()) with QE -> "Ok";;

module type Complex = module type of Complex with type t = Complex.t

module M : sig
  module C : Complex
end = struct
  module C = Complex
end

module C = Complex;;

C.one.Complex.re;;

include C

module F (X : sig
  module C = Char
end) =
struct
  module C = X.C
end

(* Applicative functors *)
module S = String
module StringSet = Set.Make (String)
module SSet = Set.Make (S)

let f (x : StringSet.t) = (x : SSet.t)

(* Also using include (cf. Leo's mail 2013-11-16) *)
module F (M : sig end) : sig
  type t
end = struct
  type t = int
end

module T = struct
  module M = struct end
  include F (M)
end

include T

let f (x : t) : T.t = x

(* PR#4049 *)
(* This works thanks to abbreviations *)
module A = struct
  module B = struct
    type t

    let compare x y = 0
  end

  module S = Set.Make (B)

  let empty = S.empty
end

module A1 = A;;

A1.empty = A.empty;;

(* PR#3476 *)
(* Does not work yet *)
module FF (X : sig end) = struct
  type t
end

module M = struct
  module X = struct end
  module Y = FF (X) (* XXX *)

  type t = Y.t
end

module F (Y : sig
  type t
end) (M : sig
  type t = Y.t
end) =
struct end

module G = F (M.Y)

(*module N = G (M);;
module N = F (M.Y) (M);;*)

(* PR#6307 *)

module A1 = struct end
module A2 = struct end

module L1 = struct
  module X = A1
end

module L2 = struct
  module X = A2
end

module F (L : module type of L1) = struct end
module F1 = F (L1)

(* ok *)
module F2 = F (L2)

(* should succeed too *)

(* Counter example: why we need to be careful with PR#6307 *)
module Int = struct
  type t = int

  let compare = compare
end

module SInt = Set.Make (Int)

type (_, _) eq = Eq : ('a, 'a) eq
type wrap = W of (SInt.t, SInt.t) eq

module M = struct
  module I = Int

  type wrap' = wrap = W of (Set.Make(Int).t, Set.Make(I).t) eq
end

module type S = module type of M

(* keep alias *)

module Int2 = struct
  type t = int

  let compare x y = compare y x
end

module type S' = sig
  module I = Int2
  include S with module I := I
end

(* fail *)

(* (* if the above succeeded, one could break invariants *)
module rec M2 : S' = M2;; (* should succeed! (but this is bad) *)

let M2.W eq = W Eq;;

let s = List.fold_right SInt.add [1;2;3] SInt.empty;;
module SInt2 = Set.Make(Int2);;
let conv : type a b. (a,b) eq -> a -> b = fun Eq x -> x;;
let s' : SInt2.t = conv eq s;;
SInt2.elements s';;
SInt2.mem 2 s';; (* invariants are broken *)
*)

(* Check behavior with submodules *)
module M = struct
  module N = struct
    module I = Int
  end

  module P = struct
    module I = N.I
  end

  module Q = struct
    type wrap' = wrap = W of (Set.Make(Int).t, Set.Make(P.I).t) eq
  end
end

module type S = module type of M

module M = struct
  module N = struct
    module I = Int
  end

  module P = struct
    module I = N.I
  end

  module Q = struct
    type wrap' = wrap = W of (Set.Make(Int).t, Set.Make(N.I).t) eq
  end
end

module type S = module type of M

(* PR#6365 *)
module type S = sig
  module M : sig
    type t

    val x : t
  end
end

module H = struct
  type t = A

  let x = A
end

module H' = H

module type S' = S with module M = H'

(* shouldn't introduce an alias *)

(* PR#6376 *)
module type Alias = sig
  module N : sig end
  module M = N
end

module F (X : sig end) = struct
  type t
end

module type A = Alias with module N := F(List)

module rec Bad : A = Bad

(* Shinwell 2014-04-23 *)
module B = struct
  module R = struct
    type t = string
  end

  module O = R
end

module K = struct
  module E = B
  module N = E.O
end

let x : K.N.t = "foo"

(* PR#6465 *)

module M = struct
  type t = A

  module B = struct
    type u = B
  end
end

module P : sig
  type t = M.t = A

  module B = M.B
end =
  M

(* should be ok *)
module P : sig
  type t = M.t = A

  module B = M.B
end = struct
  include M
end

module type S = sig
  module M : sig
    module P : sig end
  end

  module Q = M
end

module type S = sig
  module M : sig
    module N : sig end
    module P : sig end
  end

  module Q : sig
    module N = M.N
    module P = M.P
  end
end

module R = struct
  module M = struct
    module N = struct end
    module P = struct end
  end

  module Q = M
end

module R' : S = R

(* should be ok *)

(* PR#6578 *)

module M = struct
  let f x = x
end

module rec R : sig
  module M : sig
    val f : 'a -> 'a
  end
end = struct
  module M = M
end
;;

R.M.f 3;;

module rec R : sig
  module M = M
end = struct
  module M = M
end
;;

R.M.f 3;;

open A

let f = L.map S.capitalize
let () = L.iter print_endline (f [ "jacques"; "garrigue" ])

module C : sig
  module L : module type of List
end = struct
  include A
end

(* The following introduces a (useless) dependency on A:
module C : sig module L : module type of List end = A
*)

include D'

(*
let () =
  print_endline (Int.to_string D'.M.y)
*)
open A

let f = L.map S.capitalize
let () = L.iter print_endline (f [ "jacques"; "garrigue" ])

module C : sig
  module L : module type of List
end = struct
  include A
end

(* The following introduces a (useless) dependency on A:
module C : sig module L : module type of List end = A
*)

(* No dependency on D *)
let x = 3

module M = struct
  let y = 5
end

module type S = sig
  type u
  type t
end

module type S' = sig
  type t = int
  type u = bool
end

(* ok to convert between structurally equal signatures, and parameters
   are inferred *)
let f (x : (module S with type t = 'a and type u = 'b)) = (x : (module S'))
let g x = (x : (module S with type t = 'a and type u = 'b) :> (module S'))

(* with subtyping it is also ok to forget some types *)
module type S2 = sig
  type u
  type t
  type w
end

let g2 x = (x : (module S2 with type t = 'a and type u = 'b) :> (module S'))
let h x = (x : (module S2 with type t = 'a) :> (module S with type t = 'a))
let f2 (x : (module S2 with type t = 'a and type u = 'b)) = (x : (module S'))

(* fail *)
let k (x : (module S2 with type t = 'a)) = (x : (module S with type t = 'a))

(* fail *)

(* but you cannot forget values (no physical coercions) *)
module type S3 = sig
  type u
  type t

  val x : int
end

let g3 x = (x : (module S3 with type t = 'a and type u = 'b) :> (module S'))

(* fail *)
(* Using generative functors *)

(* Without type *)
module type S = sig
  val x : int
end

let v =
  (module struct
    let x = 3
  end : S)

module F () = (val v)

(* ok *)
module G (X : sig end) : S = F ()

(* ok *)
module H (X : sig end) = (val v)

(* ok *)

(* With type *)
module type S = sig
  type t

  val x : t
end

let v =
  (module struct
    type t = int

    let x = 3
  end : S)

module F () = (val v)

(* ok *)
module G (X : sig end) : S = F ()

(* fail *)
module H () = F ()

(* ok *)

(* Alias *)
module U = struct end
module M = F (struct end)

(* ok *)
module M = F (U)

(* fail *)

(* Cannot coerce between applicative and generative *)
module F1 (X : sig end) = struct end
module F2 : functor () -> sig end = F1

(* fail *)
module F3 () = struct end
module F4 : functor (X : sig end) -> sig end = F3

(* fail *)

(* tests for shortened functor notation () *)
module X (X : sig end) (Y : sig end) = functor (Z : sig end) -> struct end
module Y = functor (X : sig end) (Y : sig end) (Z : sig end) -> struct end
module Z = functor (_ : sig end) (_ : sig end) (_ : sig end) -> struct end

module GZ : functor (X : sig end) () (Z : sig end) -> sig end =
functor (X : sig end) () (Z : sig end) -> struct end

module F (X : sig end) = struct
  type t = int
end

module F (_ : sig end) = struct
  type t = int
end

type t = F(Does_not_exist).t
type expr = [ `Abs of string * expr | `App of expr * expr ]

class type exp = object
  method eval : (string, exp) Hashtbl.t -> expr
end

class app e1 e2 : exp =
  object
    val l = e1
    val r = e2

    method eval env =
      match l with
      | `Abs (var, body) ->
          Hashtbl.add env var r;
          body
      | _ -> `App (l, r)
  end

class virtual ['subject, 'event] observer =
  object
    method virtual notify : 'subject -> 'event -> unit
  end

class ['event] subject =
  object (self : 'subject)
    val mutable observers = ([] : ('subject, 'event) observer list)
    method add_observer obs = observers <- obs :: observers

    method notify_observers (e : 'event) =
      List.iter (fun x -> x#notify self e) observers
  end

type id = int

class entity (id : id) =
  object
    val ent_destroy_subject = new subject
    method destroy_subject : id subject = ent_destroy_subject
    method entity_id = id
  end

class ['entity] entity_container =
  object (self)
    inherit ['entity, id] observer as observer
    method add_entity (e : 'entity) = e#destroy_subject#add_observer self
    method notify _ id = ()
  end

let f (x : entity entity_container) = ()

(*
class world =
  object
    val entity_container : entity entity_container = new entity_container

    method add_entity (s : entity) =
      entity_container#add_entity (s :> entity)

  end
*)
(* Two v's in the same class *)
class c v =
  object
    initializer print_endline v
    val v = 42
  end
;;

new c "42";;

(* Two hidden v's in the same class! *)
class c (v : int) =
  object
    method v0 = v

    inherit
      (fun v ->
         object
           method v : string = v
         end)
        "42"
  end
;;

(new c 42)#v0;;

class virtual ['a] c =
  object (s : 'a)
    method virtual m : 'b
  end

let o =
  object (s : 'a)
    inherit ['a] c
    method m = 42
  end

module M : sig
  class x : int -> object
    method m : int
  end
end = struct
  class x _ =
    object
      method m = 42
    end
end

module M : sig
  class c : 'a -> object
    val x : 'b
  end
end = struct
  class c x =
    object
      val x = x
    end
end

class c (x : int) =
  object
    inherit M.c x
    method x : bool = x
  end

let r = (new c 2)#x

(* test.ml *)
class alfa =
  object (_ : 'self)
    method x : 'a. ('a, out_channel, unit) format -> 'a = Printf.printf
  end

class bravo a =
  object
    val y = (a :> alfa)
    initializer y#x "bravo initialized"
  end

class charlie a =
  object
    inherit bravo a
    initializer y#x "charlie initialized"
  end

(* The module begins *)
exception Out_of_range

class type ['a] cursor = object
  method get : 'a
  method incr : unit -> unit
  method is_last : bool
end

class type ['a] storage = object ('self)
  method first : 'a cursor
  method len : int
  method nth : int -> 'a cursor
  method copy : 'self
  method sub : int -> int -> 'self
  method concat : 'a storage -> 'self
  method fold : 'b. ('a -> int -> 'b -> 'b) -> 'b -> 'b
  method iter : ('a -> unit) -> unit
end

class virtual ['a, 'cursor] storage_base =
  object (self : 'self)
    constraint 'cursor = 'a #cursor
    method virtual first : 'cursor
    method virtual len : int
    method virtual copy : 'self
    method virtual sub : int -> int -> 'self
    method virtual concat : 'a storage -> 'self

    method fold : 'b. ('a -> int -> 'b -> 'b) -> 'b -> 'b =
      fun f a0 ->
        let cur = self#first in
        let rec loop count a =
          if count >= self#len then a
          else
            let a' = f cur#get count a in
            cur#incr ();
            loop (count + 1) a'
        in
        loop 0 a0

    method iter proc =
      let p = self#first in
      for i = 0 to self#len - 2 do
        proc p#get;
        p#incr ()
      done;
      if self#len > 0 then proc p#get else ()
  end

class type ['a] obj_input_channel = object
  method get : unit -> 'a
  method close : unit -> unit
end

class type ['a] obj_output_channel = object
  method put : 'a -> unit
  method flush : unit -> unit
  method close : unit -> unit
end

module UChar = struct
  type t = int

  let highest_bit = 1 lsl 30
  let lower_bits = highest_bit - 1
  let char_of c = try Char.chr c with Invalid_argument _ -> raise Out_of_range
  let of_char = Char.code
  let code c = if c lsr 30 = 0 then c else raise Out_of_range
  let chr n = if n >= 0 && n lsr 31 = 0 then n else raise Out_of_range
  let uint_code c = c
  let chr_of_uint n = n
end

type uchar = UChar.t

let int_of_uchar u = UChar.uint_code u
let uchar_of_int n = UChar.chr_of_uint n

class type ucursor = [uchar] cursor
class type ustorage = [uchar] storage

class virtual ['ucursor] ustorage_base = [uchar, 'ucursor] storage_base

module UText = struct
  (* the internal representation is UCS4 with big endian*)
  (* The most significant digit appears first. *)
  let get_buf s i =
    let n = Char.code s.[i] in
    let n = (n lsl 8) lor Char.code s.[i + 1] in
    let n = (n lsl 8) lor Char.code s.[i + 2] in
    let n = (n lsl 8) lor Char.code s.[i + 3] in
    UChar.chr_of_uint n

  let set_buf s i u =
    let n = UChar.uint_code u in
    begin
      s.![i] <- Char.chr (n lsr 24);
      s.![i + 1] <- Char.chr ((n lsr 16) lor 0xff);
      s.![i + 2] <- Char.chr ((n lsr 8) lor 0xff);
      s.![i + 3] <- Char.chr (n lor 0xff)
    end

  let init_buf buf pos init =
    if init#len = 0 then ()
    else
      let cur = init#first in
      for i = 0 to init#len - 2 do
        set_buf buf (pos + (i lsl 2)) cur#get;
        cur#incr ()
      done;
      set_buf buf (pos + ((init#len - 1) lsl 2)) cur#get

  let make_buf init =
    let s = String.create (init#len lsl 2) in
    init_buf s 0 init;
    s

  class text_raw buf =
    object (self : 'self)
      inherit [cursor] ustorage_base
      val contents = buf
      method first = new cursor (self :> text_raw) 0
      method len = String.length contents / 4
      method get i = get_buf contents (4 * i)
      method nth i = new cursor (self :> text_raw) i
      method copy = {<contents = String.copy contents>}

      method sub pos len =
        {<contents = String.sub contents (pos * 4) (len * 4)>}

      method concat (text : ustorage) =
        let buf = String.create (String.length contents + (4 * text#len)) in
        String.blit contents 0 buf 0 (String.length contents);
        init_buf buf (String.length contents) text;
        {<contents = buf>}
    end

  and cursor text i =
    object
      val contents = text
      val mutable pos = i
      method get = contents#get pos
      method incr () = pos <- pos + 1
      method is_last = pos + 1 >= contents#len
    end

  class string_raw buf =
    object
      inherit text_raw buf
      method set i u = set_buf contents (4 * i) u
    end

  class text init = text_raw (make_buf init)
  class string init = string_raw (make_buf init)

  let of_string s =
    let buf = String.make (4 * String.length s) '\000' in
    for i = 0 to String.length s - 1 do
      buf.![4 * i] <- s.[i]
    done;
    new text_raw buf

  let make len u =
    let s = String.create (4 * len) in
    for i = 0 to len - 1 do
      set_buf s (4 * i) u
    done;
    new string_raw s

  let create len = make len (UChar.chr 0)
  let copy s = s#copy
  let sub s start len = s#sub start len

  let fill s start len u =
    for i = start to start + len - 1 do
      s#set i u
    done

  let blit src srcoff dst dstoff len =
    for i = 0 to len - 1 do
      let u = src#get (srcoff + i) in
      dst#set (dstoff + i) u
    done

  let concat s1 s2 = s1#concat (s2 (* : #ustorage *) :> uchar storage)
  let iter proc s = s#iter proc
end

class type foo_t = object
  method foo : string
end

type 'a name = Foo : foo_t name | Int : int name

class foo =
  object (self)
    method foo = "foo"
    method cast = function Foo -> (self :> < foo : string >)
  end

class foo : foo_t =
  object (self)
    method foo = "foo"

    method cast : type a. a name -> a =
      function Foo -> (self :> foo_t) | _ -> raise Exit
  end

class type c = object end

module type S = sig
  class c : c
end

class virtual name = object end

and func (args_ty, ret_ty) =
  object (self)
    inherit name
    val mutable memo_args = None

    method arguments =
      match memo_args with
      | Some xs -> xs
      | None ->
          let args = List.map (fun ty -> new argument (self, ty)) args_ty in
          memo_args <- Some args;
          args
  end

and argument (func, ty) =
  object
    inherit name
  end

let f (x : #M.foo) = 0

class type ['e] t = object ('s)
  method update : 'e -> 's
end

module type S = sig
  class base : 'e -> ['e] t
end

type 'par t = 'par

module M : sig
  val x : < m : 'a. 'a >
end = struct
  let x : < m : 'a. 'a t > = Obj.magic ()
end

let ident v = v

class alias =
  object
    method alias : 'a. 'a t -> 'a = ident
  end

module Classdef = struct
  class virtual ['a, 'b, 'c] cl0 =
    object
      constraint 'c = < m : 'a -> 'b -> int ; .. >
    end

  class virtual ['a, 'b] cl1 =
    object
      method virtual raise_trouble : int -> 'a
      method virtual m : 'a -> 'b -> int
    end

  class virtual ['a, 'b] cl2 =
    object
      method virtual as_cl0 : ('a, 'b, ('a, 'b) cl1) cl0
    end
end

type refer1 = < poly : 'a 'b 'c. (('b, 'c) #Classdef.cl2 as 'a) >
type refer2 = < poly : 'a 'b 'c. (('b, 'c) #Classdef.cl2 as 'a) >

(* Actually this should succeed ... *)
let f (x : refer1) = (x : refer2)

module Classdef = struct
  class virtual ['a, 'b, 'c] cl0 =
    object
      constraint 'c = < m : 'a -> 'b -> int ; .. >
    end

  class virtual ['a, 'b] cl1 =
    object
      method virtual raise_trouble : int -> 'a
      method virtual m : 'a -> 'b -> int
    end

  class virtual ['a, 'b] cl2 =
    object
      method virtual as_cl0 : ('a, 'b, ('a, 'b) cl1) cl0
    end
end

module M : sig
  type refer = { poly : 'a 'b 'c. (('b, 'c) #Classdef.cl2 as 'a) }
end = struct
  type refer = { poly : 'a 'b 'c. (('b, 'c) #Classdef.cl2 as 'a) }
end
(*
  ocamlc -c pr3918a.mli pr3918b.mli
  rm -f pr3918a.cmi
  ocamlc -c pr3918c.ml
*)

open Pr3918b

let f x = (x : 'a vlist :> 'b vlist)
let f (x : 'a vlist) = (x : 'b vlist)

module type Poly = sig
  type 'a t = 'a constraint 'a = [> ]
end

module Combine (A : Poly) (B : Poly) = struct
  type ('a, 'b) t = 'a A.t constraint 'a = 'b B.t
end

module C =
  Combine
    (struct
      type 'a t = 'a constraint 'a = [> ]
    end)
    (struct
      type 'a t = 'a constraint 'a = [> ]
    end)

module type Priv = sig
  type t = private int
end

module Make (Unit : sig end) : Priv = struct
  type t = int
end

module A = Make (struct end)

module type Priv' = sig
  type t = private [> `A ]
end

module Make' (Unit : sig end) : Priv' = struct
  type t = [ `A ]
end

module A' = Make' (struct end)
(* PR5057 *)

module TT = struct
  module IntSet = Set.Make (struct
    type t = int

    let compare = compare
  end)
end

let () =
  let f flag =
    let module T = TT in
    let _ = match flag with `A -> 0 | `B r -> r in
    let _ = match flag with `A -> T.IntSet.mem | `B r -> r in
    ()
  in
  f `A
(* This one should fail *)

let f flag =
  let module T = Set.Make (struct
    type t = int

    let compare = compare
  end) in
  let _ = match flag with `A -> 0 | `B r -> r in
  let _ = match flag with `A -> T.mem | `B r -> r in
  ()

module type S = sig
  type +'a t

  val foo : [ `A ] t -> unit
  val bar : [< `A | `B ] t -> unit
end

module Make (T : S) = struct
  let f x =
    T.foo x;
    T.bar x;
    (x :> [ `A | `C ] T.t)
end

type 'a termpc =
  [ `And of 'a * 'a | `Or of 'a * 'a | `Not of 'a | `Atom of string ]

type 'a termk = [ `Dia of 'a | `Box of 'a | 'a termpc ]

module type T = sig
  type term

  val map : (term -> term) -> term -> term
  val nnf : term -> term
  val nnf_not : term -> term
end

module Fpc (X : T with type term = private [> 'a termpc ] as 'a) = struct
  type term = X.term termpc

  let nnf = function
    | `Not (`Atom _) as x -> x
    | `Not x -> X.nnf_not x
    | x -> X.map X.nnf x

  let map f : term -> X.term = function
    | `Not x -> `Not (f x)
    | `And (x, y) -> `And (f x, f y)
    | `Or (x, y) -> `Or (f x, f y)
    | `Atom _ as x -> x

  let nnf_not : term -> _ = function
    | `Not x -> X.nnf x
    | `And (x, y) -> `Or (X.nnf_not x, X.nnf_not y)
    | `Or (x, y) -> `And (X.nnf_not x, X.nnf_not y)
    | `Atom _ as x -> `Not x
end

module Fk (X : T with type term = private [> 'a termk ] as 'a) = struct
  type term = X.term termk

  module Pc = Fpc (X)

  let map f : term -> _ = function
    | `Dia x -> `Dia (f x)
    | `Box x -> `Box (f x)
    | #termpc as x -> Pc.map f x

  let nnf = Pc.nnf

  let nnf_not : term -> _ = function
    | `Dia x -> `Box (X.nnf_not x)
    | `Box x -> `Dia (X.nnf_not x)
    | #termpc as x -> Pc.nnf_not x
end

type untyped
type -'a typed = private untyped

type -'typing wrapped = private sexp
and +'a t = 'a typed wrapped
and sexp = private untyped wrapped

class type ['a] s3 = object
  val underlying : 'a t
end

class ['a] s3object r : ['a] s3 =
  object
    val underlying = r
  end

module M (T : sig
  type t
end) =
struct
  type t = private { t : T.t }
end

module P = struct
  module T = struct
    type t
  end

  module R = M (T)
end

module Foobar : sig
  type t = private int
end = struct
  type t = int
end

module F0 : sig
  type t = private int
end =
  Foobar

let f (x : F0.t) = (x : Foobar.t)

(* fails *)

module F = Foobar

let f (x : F.t) = (x : Foobar.t)

module M = struct
  type t = < m : int >
end

module M1 : sig
  type t = private < m : int ; .. >
end =
  M

module M2 : sig
  type t = private < m : int ; .. >
end =
  M1
;;

fun (x : M1.t) -> (x : M2.t);;

(* fails *)

module M3 : sig
  type t = private M1.t
end =
  M1
;;

fun x -> (x : M3.t :> M1.t);;
fun x -> (x : M3.t :> M.t);;

module M4 : sig
  type t = private M3.t
end =
  M2

(* fails *)
module M4 : sig
  type t = private M3.t
end =
  M

(* fails *)
module M4 : sig
  type t = private M3.t
end =
  M1

(* might be ok *)
module M5 : sig
  type t = private M1.t
end =
  M3

module M6 : sig
  type t = private < n : int ; .. >
end =
  M1

(* fails *)

module Bar : sig
  type t = private Foobar.t

  val f : int -> t
end = struct
  type t = int

  let f (x : int) = (x : t)
end

(* must fail *)

module M : sig
  type t = private T of int

  val mk : int -> t
end = struct
  type t = T of int

  let mk x = T x
end

module M1 : sig
  type t = M.t

  val mk : int -> t
end = struct
  type t = M.t

  let mk = M.mk
end

module M2 : sig
  type t = M.t

  val mk : int -> t
end = struct
  include M
end

module M3 : sig
  type t = M.t

  val mk : int -> t
end =
  M

module M4 : sig
  type t = M.t = T of int

  val mk : int -> t
end =
  M

(* Error: The variant or record definition does not match that of type M.t *)

module M5 : sig
  type t = M.t = private T of int

  val mk : int -> t
end =
  M

module M6 : sig
  type t = private T of int

  val mk : int -> t
end =
  M

module M' : sig
  type t_priv = private T of int
  type t = t_priv

  val mk : int -> t
end = struct
  type t_priv = T of int
  type t = t_priv

  let mk x = T x
end

module M3' : sig
  type t = M'.t

  val mk : int -> t
end =
  M'

module M : sig
  type 'a t = private T of 'a
end = struct
  type 'a t = T of 'a
end

module M1 : sig
  type 'a t = 'a M.t = private T of 'a
end = struct
  type 'a t = 'a M.t = private T of 'a
end

(* PR#6090 *)
module Test = struct
  type t = private A
end

module Test2 : module type of Test with type t = Test.t = Test

let f (x : Test.t) = (x : Test2.t)
let f Test2.A = ()
let a = Test2.A

(* fail *)
(* The following should fail from a semantical point of view,
   but allow it for backward compatibility *)
module Test2 : module type of Test with type t = private Test.t = Test

(* PR#6331 *)
type t = private < x : int ; .. > as 'a
type t = private (< x : int ; .. > as 'a) as 'a
type t = private < x : int > as 'a
type t = private (< x : int > as 'a) as 'b
type 'a t = private < x : int ; .. > as 'a
type 'a t = private 'a constraint 'a = < x : int ; .. >

(* Bad (t = t) *)
module rec A : sig
  type t = A.t
end = struct
  type t = A.t
end

(* Bad (t = t) *)
module rec A : sig
  type t = B.t
end = struct
  type t = B.t
end

and B : sig
  type t = A.t
end = struct
  type t = A.t
end

(* OK (t = int) *)
module rec A : sig
  type t = B.t
end = struct
  type t = B.t
end

and B : sig
  type t = int
end = struct
  type t = int
end

(* Bad (t = int * t) *)
module rec A : sig
  type t = int * A.t
end = struct
  type t = int * A.t
end

(* Bad (t = t -> int) *)
module rec A : sig
  type t = B.t -> int
end = struct
  type t = B.t -> int
end

and B : sig
  type t = A.t
end = struct
  type t = A.t
end

(* OK (t = <m:t>) *)
module rec A : sig
  type t = < m : B.t >
end = struct
  type t = < m : B.t >
end

and B : sig
  type t = A.t
end = struct
  type t = A.t
end

(* Bad (not regular) *)
module rec A : sig
  type 'a t = < m : 'a list A.t >
end = struct
  type 'a t = < m : 'a list A.t >
end

(* Bad (not regular) *)
module rec A : sig
  type 'a t = < m : 'a list B.t ; n : 'a array B.t >
end = struct
  type 'a t = < m : 'a list B.t ; n : 'a array B.t >
end

and B : sig
  type 'a t = 'a A.t
end = struct
  type 'a t = 'a A.t
end

(* Bad (not regular) *)
module rec A : sig
  type 'a t = 'a B.t
end = struct
  type 'a t = 'a B.t
end

and B : sig
  type 'a t = < m : 'a list A.t ; n : 'a array A.t >
end = struct
  type 'a t = < m : 'a list A.t ; n : 'a array A.t >
end

(* OK *)
module rec A : sig
  type 'a t = 'a array B.t * 'a list B.t
end = struct
  type 'a t = 'a array B.t * 'a list B.t
end

and B : sig
  type 'a t = < m : 'a B.t >
end = struct
  type 'a t = < m : 'a B.t >
end

(* Bad (not regular) *)
module rec A : sig
  type 'a t = 'a list B.t
end = struct
  type 'a t = 'a list B.t
end

and B : sig
  type 'a t = < m : 'a array B.t >
end = struct
  type 'a t = < m : 'a array B.t >
end

(* Bad (not regular) *)
module rec M : sig
  class ['a] c : 'a -> object
    method map : ('a -> 'b) -> 'b M.c
  end
end = struct
  class ['a] c (x : 'a) =
    object
      method map : 'b. ('a -> 'b) -> 'b M.c = fun f -> new M.c (f x)
    end
end

(* OK *)
class type ['node] extension = object
  method node : 'node
end

and ['ext] node = object
  constraint 'ext = ('ext node #extension[@id])
end

class x =
  object
    method node : x node = assert false
  end

type t = x node

(* Bad - PR 4261 *)

module PR_4261 = struct
  module type S = sig
    type t
  end

  module type T = sig
    module D : S

    type t = D.t
  end

  module rec U : (T with module D = U') = U
  and U' : (S with type t = U'.t) = U
end

(* Bad - PR 4512 *)
module type S' = sig
  type t = int
end

module rec M : (S' with type t = M.t) = struct
  type t = M.t
end

(* PR#4450 *)

module PR_4450_1 = struct
  module type MyT = sig
    type 'a t = Succ of 'a t
  end

  module MyMap (X : MyT) = X
  module rec MyList : MyT = MyMap (MyList)
end

module PR_4450_2 = struct
  module type MyT = sig
    type 'a wrap = My of 'a t
    and 'a t = private < map : 'b. ('a -> 'b) -> 'b wrap ; .. >

    val create : 'a list -> 'a t
  end

  module MyMap (X : MyT) = struct
    include X

    class ['a] c l =
      object (self)
        method map : 'b. ('a -> 'b) -> 'b wrap =
          fun f -> My (create (List.map f l))
      end
  end

  module rec MyList : sig
    type 'a wrap = My of 'a t
    and 'a t = < map : 'b. ('a -> 'b) -> 'b wrap >

    val create : 'a list -> 'a t
  end = struct
    include MyMap (MyList)

    let create l = new c l
  end
end

(* A synthetic example of bootstrapped data structure
   (suggested by J-C Filliatre) *)

module type ORD = sig
  type t

  val compare : t -> t -> int
end

module type SET = sig
  type elt
  type t

  val iter : (elt -> unit) -> t -> unit
end

type 'a tree = E | N of 'a tree * 'a * 'a tree

module Bootstrap2
    (MakeDiet : functor
      (X : ORD)
      -> SET with type t = X.t tree and type elt = X.t) :
  SET with type elt = int = struct
  type elt = int

  module rec Elt : sig
    type t = I of int * int | D of int * Diet.t * int

    val compare : t -> t -> int
    val iter : (int -> unit) -> t -> unit
  end = struct
    type t = I of int * int | D of int * Diet.t * int

    let compare x1 x2 = 0

    let rec iter f = function
      | I (l, r) ->
          for i = l to r do
            f i
          done
      | D (_, d, _) -> Diet.iter (iter f) d
  end

  and Diet : (SET with type t = Elt.t tree and type elt = Elt.t) = MakeDiet (Elt)

  type t = Diet.t

  let iter f = Diet.iter (Elt.iter f)
end
(* PR 4470: simplified from OMake's sources *)

module rec DirElt : sig
  type t = DirRoot | DirSub of DirHash.t
end = struct
  type t = DirRoot | DirSub of DirHash.t
end

and DirCompare : sig
  type t = DirElt.t
end = struct
  type t = DirElt.t
end

and DirHash : sig
  type t = DirElt.t list
end = struct
  type t = DirCompare.t list
end
(* PR 4758, PR 4266 *)

module PR_4758 = struct
  module type S = sig end

  module type Mod = sig
    module Other : S
  end

  module rec A : S = struct end

  and C : sig
    include Mod with module Other = A
  end = struct
    module Other = A
  end

  module C' = C (* check that we can take an alias *)

  module F (X : sig end) = struct
    type t
  end

  let f (x : F(C).t) = (x : F(C').t)
end

(* PR 4557 *)
module PR_4557 = struct
  module F (X : Set.OrderedType) = struct
    module rec Mod : sig
      module XSet : sig
        type elt = X.t
        type t = Set.Make(X).t
      end

      module XMap : sig
        type key = X.t
        type 'a t = 'a Map.Make(X).t
      end

      type elt = X.t
      type t = XSet.t XMap.t

      val compare : t -> t -> int
    end = struct
      module XSet = Set.Make (X)
      module XMap = Map.Make (X)

      type elt = X.t
      type t = XSet.t XMap.t

      let compare = fun x y -> 0
    end

    and ModSet : (Set.S with type elt = Mod.t) = Set.Make (Mod)
  end
end

module F (X : Set.OrderedType) = struct
  module rec Mod : sig
    module XSet : sig
      type elt = X.t
      type t = Set.Make(X).t
    end

    module XMap : sig
      type key = X.t
      type 'a t = 'a Map.Make(X).t
    end

    type elt = X.t
    type t = XSet.t XMap.t

    val compare : t -> t -> int
  end = struct
    module XSet = Set.Make (X)
    module XMap = Map.Make (X)

    type elt = X.t
    type t = XSet.t XMap.t

    let compare = fun x y -> 0
  end

  and ModSet : (Set.S with type elt = Mod.t) = Set.Make (Mod)
end
(* Tests for recursive modules *)

let test number result expected =
  if result = expected then Printf.printf "Test %d passed.\n" number
  else Printf.printf "Test %d FAILED.\n" number;
  flush stdout

(* Tree of sets *)

module rec A : sig
  type t = Leaf of int | Node of ASet.t

  val compare : t -> t -> int
end = struct
  type t = Leaf of int | Node of ASet.t

  let compare x y =
    match (x, y) with
    | Leaf i, Leaf j -> Stdlib.compare i j
    | Leaf i, Node t -> -1
    | Node s, Leaf j -> 1
    | Node s, Node t -> ASet.compare s t
end

and ASet : (Set.S with type elt = A.t) = Set.Make (A)

let _ =
  let x = A.Node (ASet.add (A.Leaf 3) (ASet.singleton (A.Leaf 2))) in
  let y = A.Node (ASet.add (A.Leaf 1) (ASet.singleton x)) in
  test 10 (A.compare x x) 0;
  test 11 (A.compare x (A.Leaf 3)) 1;
  test 12 (A.compare (A.Leaf 0) x) (-1);
  test 13 (A.compare y y) 0;
  test 14 (A.compare x y) 1

(* Simple value recursion *)

module rec Fib : sig
  val f : int -> int
end = struct
  let f x = if x < 2 then 1 else Fib.f (x - 1) + Fib.f (x - 2)
end

let _ = test 20 (Fib.f 10) 89

(* Update function by infix *)

module rec Fib2 : sig
  val f : int -> int
end = struct
  let rec g x = Fib2.f (x - 1) + Fib2.f (x - 2)
  and f x = if x < 2 then 1 else g x
end

let _ = test 21 (Fib2.f 10) 89

(* Early application *)

let _ =
  let res =
    try
      let module A = struct
        module rec Bad : sig
          val f : int -> int
        end = struct
          let f =
            let y = Bad.f 5 in
            fun x -> x + y
        end
      end in
      false
    with Undefined_recursive_module _ -> true
  in
  test 30 res true

(* Early strict evaluation *)

(*
module rec Cyclic
  : sig val x : int end
  = struct let x = Cyclic.x + 1 end
;;
*)

(* Reordering of evaluation based on dependencies *)

module rec After : sig
  val x : int
end = struct
  let x = Before.x + 1
end

and Before : sig
  val x : int
end = struct
  let x = 3
end

let _ = test 40 After.x 4

(* Type identity between A.t and t within A's definition *)

module rec Strengthen : sig
  type t

  val f : t -> t
end = struct
  type t = A | B

  let _ = (A : Strengthen.t)
  let f x = if true then A else Strengthen.f B
end

module rec Strengthen2 : sig
  type t

  val f : t -> t

  module M : sig
    type u
  end

  module R : sig
    type v
  end
end = struct
  type t = A | B

  let _ = (A : Strengthen2.t)
  let f x = if true then A else Strengthen2.f B

  module M = struct
    type u = C

    let _ = (C : Strengthen2.M.u)
  end

  module rec R : sig
    type v = Strengthen2.R.v
  end = struct
    type v = D

    let _ = (D : R.v)
    let _ = (D : Strengthen2.R.v)
  end
end

(* Polymorphic recursion *)

module rec PolyRec : sig
  type 'a t = Leaf of 'a | Node of 'a list t * 'a list t

  val depth : 'a t -> int
end = struct
  type 'a t = Leaf of 'a | Node of 'a list t * 'a list t

  let x = (PolyRec.Leaf 1 : int t)

  let depth = function
    | Leaf x -> 0
    | Node (l, r) -> 1 + max (PolyRec.depth l) (PolyRec.depth r)
end

(* Wrong LHS signatures (PR#4336) *)

(*
module type ASig = sig type a val a:a val print:a -> unit end
module type BSig = sig type b val b:b val print:b -> unit end

module A = struct type a = int let a = 0 let print = print_int end
module B = struct type b = float let b = 0.0 let print = print_float end

module MakeA (Empty:sig end) : ASig = A
module MakeB (Empty:sig end) : BSig = B

module
   rec NewA : ASig = MakeA (struct end)
   and NewB : BSig with type b = NewA.a = MakeB (struct end);;

*)

(* Expressions and bindings *)

module StringSet = Set.Make (String)

module rec Expr : sig
  type t =
    | Var of string
    | Const of int
    | Add of t * t
    | Binding of Binding.t * t

  val make_let : string -> t -> t -> t
  val fv : t -> StringSet.t
  val simpl : t -> t
end = struct
  type t =
    | Var of string
    | Const of int
    | Add of t * t
    | Binding of Binding.t * t

  let make_let id e1 e2 = Binding ([ (id, e1) ], e2)

  let rec fv = function
    | Var s -> StringSet.singleton s
    | Const n -> StringSet.empty
    | Add (t1, t2) -> StringSet.union (fv t1) (fv t2)
    | Binding (b, t) ->
        StringSet.union (Binding.fv b) (StringSet.diff (fv t) (Binding.bv b))

  let rec simpl = function
    | Var s -> Var s
    | Const n -> Const n
    | Add (Const i, Const j) -> Const (i + j)
    | Add (Const 0, t) -> simpl t
    | Add (t, Const 0) -> simpl t
    | Add (t1, t2) -> Add (simpl t1, simpl t2)
    | Binding (b, t) -> Binding (Binding.simpl b, simpl t)
end

and Binding : sig
  type t = (string * Expr.t) list

  val fv : t -> StringSet.t
  val bv : t -> StringSet.t
  val simpl : t -> t
end = struct
  type t = (string * Expr.t) list

  let fv b =
    List.fold_left
      (fun v (id, e) -> StringSet.union v (Expr.fv e))
      StringSet.empty b

  let bv b =
    List.fold_left (fun v (id, e) -> StringSet.add id v) StringSet.empty b

  let simpl b = List.map (fun (id, e) -> (id, Expr.simpl e)) b
end

let _ =
  let e =
    Expr.make_let "x" (Expr.Add (Expr.Var "y", Expr.Const 0)) (Expr.Var "x")
  in
  let e' = Expr.make_let "x" (Expr.Var "y") (Expr.Var "x") in
  test 50 (StringSet.elements (Expr.fv e)) [ "y" ];
  test 51 (Expr.simpl e) e'

(* Okasaki's bootstrapping *)

module type ORDERED = sig
  type t

  val eq : t -> t -> bool
  val lt : t -> t -> bool
  val leq : t -> t -> bool
end

module type HEAP = sig
  module Elem : ORDERED

  type heap

  val empty : heap
  val isEmpty : heap -> bool
  val insert : Elem.t -> heap -> heap
  val merge : heap -> heap -> heap
  val findMin : heap -> Elem.t
  val deleteMin : heap -> heap
end

module Bootstrap
    (MakeH : functor (Element : ORDERED) -> HEAP with module Elem = Element)
    (Element : ORDERED) : HEAP with module Elem = Element = struct
  module Elem = Element

  module rec BE : sig
    type t = E | H of Elem.t * PrimH.heap

    val eq : t -> t -> bool
    val lt : t -> t -> bool
    val leq : t -> t -> bool
  end = struct
    type t = E | H of Elem.t * PrimH.heap

    let leq t1 t2 =
      match (t1, t2) with
      | H (x, _), H (y, _) -> Elem.leq x y
      | H _, E -> false
      | E, H _ -> true
      | E, E -> true

    let eq t1 t2 =
      match (t1, t2) with
      | H (x, _), H (y, _) -> Elem.eq x y
      | H _, E -> false
      | E, H _ -> false
      | E, E -> true

    let lt t1 t2 =
      match (t1, t2) with
      | H (x, _), H (y, _) -> Elem.lt x y
      | H _, E -> false
      | E, H _ -> true
      | E, E -> false
  end

  and PrimH : (HEAP with type Elem.t = BE.t) = MakeH (BE)

  type heap = BE.t

  let empty = BE.E
  let isEmpty = function BE.E -> true | _ -> false

  let rec merge x y =
    match (x, y) with
    | BE.E, _ -> y
    | _, BE.E -> x
    | (BE.H (e1, p1) as h1), (BE.H (e2, p2) as h2) ->
        if Elem.leq e1 e2 then BE.H (e1, PrimH.insert h2 p1)
        else BE.H (e2, PrimH.insert h1 p2)

  let insert x h = merge (BE.H (x, PrimH.empty)) h
  let findMin = function BE.E -> raise Not_found | BE.H (x, _) -> x

  let deleteMin = function
    | BE.E -> raise Not_found
    | BE.H (x, p) ->
        if PrimH.isEmpty p then BE.E
        else
          begin match PrimH.findMin p with
          | BE.H (y, p1) ->
              let p2 = PrimH.deleteMin p in
              BE.H (y, PrimH.merge p1 p2)
          | BE.E -> assert false
          end
end

module LeftistHeap (Element : ORDERED) : HEAP with module Elem = Element =
struct
  module Elem = Element

  type heap = E | T of int * Elem.t * heap * heap

  let rank = function E -> 0 | T (r, _, _, _) -> r

  let make x a b =
    if rank a >= rank b then T (rank b + 1, x, a, b) else T (rank a + 1, x, b, a)

  let empty = E
  let isEmpty = function E -> true | _ -> false

  let rec merge h1 h2 =
    match (h1, h2) with
    | _, E -> h1
    | E, _ -> h2
    | T (_, x1, a1, b1), T (_, x2, a2, b2) ->
        if Elem.leq x1 x2 then make x1 a1 (merge b1 h2)
        else make x2 a2 (merge h1 b2)

  let insert x h = merge (T (1, x, E, E)) h
  let findMin = function E -> raise Not_found | T (_, x, _, _) -> x
  let deleteMin = function E -> raise Not_found | T (_, x, a, b) -> merge a b
end

module Ints = struct
  type t = int

  let eq = ( = )
  let lt = ( < )
  let leq = ( <= )
end

module C = Bootstrap (LeftistHeap) (Ints)

let _ =
  let h = List.fold_right C.insert [ 6; 4; 8; 7; 3; 1 ] C.empty in
  test 60 (C.findMin h) 1;
  test 61 (C.findMin (C.deleteMin h)) 3;
  test 62 (C.findMin (C.deleteMin (C.deleteMin h))) 4

(* Classes *)

module rec Class1 : sig
  class c : object
    method m : int -> int
  end
end = struct
  class c =
    object
      method m x = if x <= 0 then x else (new Class2.d)#m x
    end
end

and Class2 : sig
  class d : object
    method m : int -> int
  end
end = struct
  class d =
    object (self)
      inherit Class1.c as super
      method m (x : int) = super#m 0
    end
end

let _ = test 70 ((new Class1.c)#m 7) 0

let _ =
  try
    let module A = struct
      module rec BadClass1 : sig
        class c : object
          method m : int
        end
      end = struct
        class c =
          object
            method m = 123
          end
      end

      and BadClass2 : sig
        val x : int
      end = struct
        let x = (new BadClass1.c)#m
      end
    end in
    test 71 true false
  with Undefined_recursive_module _ -> test 71 true true

(* Coercions *)

module rec Coerce1 : sig
  val g : int -> int
  val f : int -> int
end = struct
  module A : sig
    val f : int -> int
  end =
    Coerce1

  let g x = x
  let f x = if x <= 0 then 1 else A.f (x - 1) * x
end

let _ = test 80 (Coerce1.f 10) 3628800

module CoerceF (S : sig end) = struct
  let f1 () = 1
  let f2 () = 2
  let f3 () = 3
  let f4 () = 4
  let f5 () = 5
end

module rec Coerce2 : sig
  val f1 : unit -> int
end =
  CoerceF (Coerce3)

and Coerce3 : sig end = struct end

let _ = test 81 (Coerce2.f1 ()) 1

module Coerce4 (A : sig
  val f : int -> int
end) =
struct
  let x = 0
  let at a = A.f a
end

module rec Coerce5 : sig
  val blabla : int -> int
  val f : int -> int
end = struct
  let blabla x = 0
  let f x = 5
end

and Coerce6 : sig
  val at : int -> int
end =
  Coerce4 (Coerce5)

let _ = test 82 (Coerce6.at 100) 5

(* Miscellaneous bug reports *)

module rec F : sig
  type t = X of int | Y of int

  val f : t -> bool
end = struct
  type t = X of int | Y of int

  let f = function X _ -> false | _ -> true
end

let _ =
  test 100 (F.f (F.X 1)) false;
  test 101 (F.f (F.Y 2)) true

(* PR#4316 *)
module G (S : sig
  val x : int Lazy.t
end) =
struct
  include S
end

module M1 = struct
  let x = lazy 3
end

let _ = Lazy.force M1.x

module rec M2 : sig
  val x : int Lazy.t
end =
  G (M1)

let _ = test 102 (Lazy.force M2.x) 3
let _ = Gc.full_major () (* will shortcut forwarding in M1.x *)

module rec M3 : sig
  val x : int Lazy.t
end =
  G (M1)

let _ = test 103 (Lazy.force M3.x) 3

(** Pure type-checking tests: see recmod/*.ml *)
type t = A of { x : int; mutable y : int }

let f (A r) = r

(* -> escape *)
let f (A r) = r.x

(* ok *)
let f x = A { x; y = x }

(* ok *)
let f (A r) = A { r with y = r.x + 1 }

(* ok *)
let f () = A { a = 1 }

(* customized error message *)
let f () = A { x = 1; y = 3 }

(* ok *)

type _ t = A : { x : 'a; y : 'b } -> 'a t

let f (A { x; y }) = A { x; y = () }

(* ok *)
let f (A ({ x; y } as r)) = A { x = r.x; y = r.y }

(* ok *)

module M = struct
  type 'a t = A of { x : 'a } | B : { u : 'b } -> unit t

  exception Foo of { x : int }
end

module N : sig
  type 'b t = 'b M.t = A of { x : 'b } | B : { u : 'bla } -> unit t

  exception Foo of { x : int }
end = struct
  type 'b t = 'b M.t = A of { x : 'b } | B : { u : 'z } -> unit t

  exception Foo = M.Foo
end

module type S = sig
  exception A of { x : int }
end

module F (X : sig
  val x : (module S)
end) =
struct
  module A = (val X.x)
end

(* -> this expression creates fresh types (not really!) *)

module type S = sig
  exception A of { x : int }
  exception A of { x : string }
end

module M = struct
  exception A of { x : int }
  exception A of { x : string }
end

module M1 = struct
  exception A of { x : int }
end

module M = struct
  include M1
  include M1
end

module type S1 = sig
  exception A of { x : int }
end

module type S = sig
  include S1
  include S1
end

module M = struct
  exception A = M1.A
end

module X1 = struct
  type t = ..
end

module X2 = struct
  type t = ..
end

module Z = struct
  type X1.t += A of { x : int }
  type X2.t += A of { x : int }
end

(* PR#6716 *)

type _ c = C : [ `A ] c
type t = T : { x : [< `A ] c } -> t

let f (T { x = C }) = ()

module M : sig
  type 'a t

  type u = u t
  and v = v t

  val f : int -> u
  val g : v -> bool
end = struct
  type 'a t = 'a

  type u = int
  and v = bool

  let f x = x
  let g x = x
end

let h (x : int) : bool = M.g (M.f x)

type _ t = C : ((('a -> 'o) -> 'o) -> ('b -> 'o) -> 'o) t

let f : type a o. ((a -> o) -> o) t -> (a -> o) -> o = fun C k -> k (fun x -> x)

module type T = sig
  type 'a t
end

module Fix (T : T) = struct
  type r = 'r T.t as 'r
end

type _ t = X of string | Y : bytes t

let y : string t = Y
let f : string A.t -> unit = function A.X s -> print_endline s
let () = f A.y

module rec A : sig
  type t
end = struct
  type t = { a : unit; b : unit }

  let _ = { a = () }
end

type t = [ `A | `B ]
type 'a u = t

let a : [< int u ] = `A

type 'a s = 'a

let b : [< t s ] = `B

module Core = struct
  module Int = struct
    module T = struct
      type t = int

      let compare = compare
      let ( + ) x y = x + y
    end

    include T
    module Map = Map.Make (T)
  end

  module Std = struct
    module Int = Int
  end
end

open Core.Std

let x = Int.Map.empty
let y = x + x

(* Avoid ambiguity *)

module M = struct
  type t = A
  type u = C
end

module N = struct
  type t = B
end

open M
open N;;

A;;
B;;
C;;

include M
open M;;

C;;

module L = struct
  type v = V
end

open L;;

V;;

module L = struct
  type v = V
end

open L;;

V;;

type t1 = A

module M1 = struct
  type u = v
  and v = t1
end

module N1 = struct
  type u = v
  and v = M1.v
end

type t1 = B

module N2 = struct
  type u = v
  and v = M1.v
end

(* PR#6566 *)
module type PR6566 = sig
  type t = string
end

module PR6566 = struct
  type t = int
end

module PR6566' : PR6566 = PR6566

module A = struct
  module B = struct
    type t = T
  end
end

module M2 = struct
  type u = A.B.t
  type foo = int
  type v = A.B.t
end

(* Adapted from: An Expressive Language of Signatures
   by Norman Ramsey, Kathleen Fisher and Paul Govereau *)

module type VALUE = sig
  type value (* a Lua value *)
  type state (* the state of a Lua interpreter *)
  type usert (* a user-defined value *)
end

module type CORE0 = sig
  module V : VALUE

  val setglobal : V.state -> string -> V.value -> unit
  (* five more functions common to core and evaluator *)
end

module type CORE = sig
  include CORE0

  val apply : V.value -> V.state -> V.value list -> V.value
  (* apply function f in state s to list of args *)
end

module type AST = sig
  module Value : VALUE

  type chunk
  type program

  val get_value : chunk -> Value.value
end

module type EVALUATOR = sig
  module Value : VALUE
  module Ast : AST with module Value := Value

  type state = Value.state
  type value = Value.value

  exception Error of string

  val compile : Ast.program -> string

  include CORE0 with module V := Value
end

module type PARSER = sig
  type chunk

  val parse : string -> chunk
end

module type INTERP = sig
  include EVALUATOR
  module Parser : PARSER with type chunk = Ast.chunk

  val dostring : state -> string -> value list
  val mk : unit -> state
end

module type USERTYPE = sig
  type t

  val eq : t -> t -> bool
  val to_string : t -> string
end

module type TYPEVIEW = sig
  type combined
  type t

  val map : (combined -> t) * (t -> combined)
end

module type COMBINED_COMMON = sig
  module T : sig
    type t
  end

  module TV1 : TYPEVIEW with type combined := T.t
  module TV2 : TYPEVIEW with type combined := T.t
end

module type COMBINED_TYPE = sig
  module T : USERTYPE
  include COMBINED_COMMON with module T := T
end

module type BARECODE = sig
  type state

  val init : state -> unit
end

module USERCODE (X : TYPEVIEW) = struct
  module type F = functor (C : CORE with type V.usert = X.combined) ->
    BARECODE with type state := C.V.state
end

module Weapon = struct
  type t
end

module type WEAPON_LIB = sig
  type t = Weapon.t

  module T : USERTYPE with type t = t
  module Make : functor (TV : TYPEVIEW with type t = t) -> USERCODE(TV).F
end

module type X = functor (X : CORE) -> BARECODE
module type X = functor (_ : CORE) -> BARECODE

module M = struct
  type t = int * (< m : 'a > as 'a)
end

module type S = sig
  module M : sig
    type t
  end
end
with module M = M

module type Printable = sig
  type t

  val print : Format.formatter -> t -> unit
end

module type Comparable = sig
  type t

  val compare : t -> t -> int
end

module type PrintableComparable = sig
  include Printable
  include Comparable with type t = t
end

(* Fails *)
module type PrintableComparable = sig
  type t

  include Printable with type t := t
  include Comparable with type t := t
end

module type PrintableComparable = sig
  include Printable
  include Comparable with type t := t
end

module type ComparableInt = Comparable with type t := int

module type S = sig
  type t

  val f : t -> t
end

module type S' = S with type t := int

module type S = sig
  type 'a t

  val map : ('a -> 'b) -> 'a t -> 'b t
end

module type S1 = S with type 'a t := 'a list

module type S2 = sig
  type 'a dict = (string * 'a) list

  include S with type 'a t := 'a dict
end

module type S = sig
  module T : sig
    type exp
    type arg
  end

  val f : T.exp -> T.arg
end

module M = struct
  type exp = string
  type arg = int
end

module type S' = S with module T := M

module type S = sig
  type 'a t
end
with type 'a t := unit

(* Fails *)
let property (type t) () =
  let module M = struct
    exception E of t
  end in
  ((fun x -> M.E x), function M.E x -> Some x | _ -> None)

let () =
  let int_inj, int_proj = property () in
  let string_inj, string_proj = property () in

  let i = int_inj 3 in
  let s = string_inj "abc" in

  Printf.printf "%B\n%!" (int_proj i = None);
  Printf.printf "%B\n%!" (int_proj s = None);
  Printf.printf "%B\n%!" (string_proj i = None);
  Printf.printf "%B\n%!" (string_proj s = None)

let sort_uniq (type s) cmp l =
  let module S = Set.Make (struct
    type t = s

    let compare = cmp
  end) in
  S.elements (List.fold_right S.add l S.empty)

let () =
  print_endline (String.concat "," (sort_uniq compare [ "abc"; "xyz"; "abc" ]))

let f x (type a) (y : a) = x = y

(* Fails *)
class ['a] c =
  object (self)
    method m : 'a -> 'a = fun x -> x
    method n : 'a -> 'a = fun (type g) (x : g) -> self#m x
  end

(* Fails *)

external a : (int[@untagged]) -> unit = "a" "a_nat"
external b : (int32[@unboxed]) -> unit = "b" "b_nat"
external c : (int64[@unboxed]) -> unit = "c" "c_nat"
external d : (nativeint[@unboxed]) -> unit = "d" "d_nat"
external e : (float[@unboxed]) -> unit = "e" "e_nat"

type t = private int

external f : (t[@untagged]) -> unit = "f" "f_nat"

module M : sig
  external a : int -> (int[@untagged]) = "a" "a_nat"
  external b : (int[@untagged]) -> int = "b" "b_nat"
end = struct
  external a : int -> (int[@untagged]) = "a" "a_nat"
  external b : (int[@untagged]) -> int = "b" "b_nat"
end

module Global_attributes = struct
  [@@@ocaml.warning "-3"]

  external a : float -> float = "a" "noalloc" "a_nat" "float"
  external b : float -> float = "b" "noalloc" "b_nat"
  external c : float -> float = "c" "c_nat" "float"
  external d : float -> float = "d" "noalloc"
  external e : float -> float = "e"

  (* Should output a warning: no native implementation provided *)
  external f : (int32[@unboxed]) -> (int32[@unboxed]) = "f" "noalloc"
  external g : int32 -> int32 = "g" "g_nat" [@@unboxed] [@@noalloc]
  external h : (int[@untagged]) -> (int[@untagged]) = "h" "h_nat" "noalloc"
  external i : int -> int = "i" "i_nat" [@@untagged] [@@noalloc]
end

module Old_style_warning = struct
  [@@@ocaml.warning "+3"]

  external a : float -> float = "a" "noalloc" "a_nat" "float"
  external b : float -> float = "b" "noalloc" "b_nat"
  external c : float -> float = "c" "c_nat" "float"
  external d : float -> float = "d" "noalloc"
  external e : float -> float = "c" "float"
end

(* Bad: attributes not reported in the interface *)

module Bad1 : sig
  external f : int -> int = "f" "f_nat"
end = struct
  external f : int -> (int[@untagged]) = "f" "f_nat"
end

module Bad2 : sig
  external f : int -> int = "a" "a_nat"
end = struct
  external f : (int[@untagged]) -> int = "f" "f_nat"
end

module Bad3 : sig
  external f : float -> float = "f" "f_nat"
end = struct
  external f : float -> (float[@unboxed]) = "f" "f_nat"
end

module Bad4 : sig
  external f : float -> float = "a" "a_nat"
end = struct
  external f : (float[@unboxed]) -> float = "f" "f_nat"
end

(* Bad: attributes in the interface but not in the implementation *)

module Bad5 : sig
  external f : int -> (int[@untagged]) = "f" "f_nat"
end = struct
  external f : int -> int = "f" "f_nat"
end

module Bad6 : sig
  external f : (int[@untagged]) -> int = "f" "f_nat"
end = struct
  external f : int -> int = "a" "a_nat"
end

module Bad7 : sig
  external f : float -> (float[@unboxed]) = "f" "f_nat"
end = struct
  external f : float -> float = "f" "f_nat"
end

module Bad8 : sig
  external f : (float[@unboxed]) -> float = "f" "f_nat"
end = struct
  external f : float -> float = "a" "a_nat"
end

(* Bad: unboxed or untagged with the wrong type *)

external g : (float[@untagged]) -> float = "g" "g_nat"
external h : (int[@unboxed]) -> float = "h" "h_nat"

(* Bad: unboxing the function type *)
external i : (int -> float[@unboxed]) = "i" "i_nat"

(* Bad: unboxing a "deep" sub-type. *)
external j : int -> (float[@unboxed]) * float = "j" "j_nat"

(* This should be rejected, but it is quite complicated to do
   in the current state of things *)

external k : int -> (float[@unboxd]) = "k" "k_nat"

(* Bad: old style annotations + new style attributes *)

external l : float -> float = "l" "l_nat" "float" [@@unboxed]
external m : (float[@unboxed]) -> float = "m" "m_nat" "float"
external n : float -> float = "n" "noalloc" [@@noalloc]

(* Warnings: unboxed / untagged without any native implementation *)
external o : (float[@unboxed]) -> float = "o"
external p : float -> (float[@unboxed]) = "p"
external q : (int[@untagged]) -> float = "q"
external r : int -> (int[@untagged]) = "r"
external s : int -> int = "s" [@@untagged]
external t : float -> float = "t" [@@unboxed]

let _ = ignore ( + )
let _ = raise Exit 3;;

(* comment 9644 of PR#6000 *)

fun b -> if b then format_of_string "x" else "y";;
fun b -> if b then "x" else format_of_string "y";;
fun b : (_, _, _) format -> if b then "x" else "y";;

(* PR#7135 *)

module PR7135 = struct
  module M : sig
    type t = private int
  end = struct
    type t = int
  end

  include M

  let lift2 (f : int -> int -> int) (x : t) (y : t) = f (x :> int) (y :> int)
end

(* example of non-ground coercion *)

module Test1 = struct
  type t = private int

  let f x =
    let y = if true then x else (x : t) in
    (y :> int)
end

(* Warn about all relevant cases when possible *)
let f = function None, None -> 1 | Some _, Some _ -> 2

(* Exhaustiveness check is very slow *)
type _ t = A : int t | B : bool t | C : char t | D : float t
type (_, _, _, _) u = U : (int, int, int, int) u
type v = E | F | G

let f : type a b c d e f g.
    a t
    * b t
    * c t
    * d t
    * e t
    * f t
    * g t
    * v
    * (a, b, c, d) u
    * (e, f, g, g) u ->
    int = function
  | A, A, A, A, A, A, A, _, U, U -> 1
  | _, _, _, _, _, _, _, G, _, _ -> 1
(*| _ -> _ *)

(* Unused cases *)
let f (x : int t) = match x with A -> 1 | _ -> 2

(* warn *)
let f (x : unit t option) = match x with None -> 1 | _ -> 2

(* warn? *)
let f (x : unit t option) = match x with None -> 1 | Some _ -> 2

(* warn *)
let f (x : int t option) = match x with None -> 1 | _ -> 2
let f (x : int t option) = match x with None -> 1

(* warn *)

(* Example with record, type, single case *)

type 'a box = Box of 'a
type 'a pair = { left : 'a; right : 'a }

let f : (int t box pair * bool) option -> unit = function None -> ()
let f : (string t box pair * bool) option -> unit = function None -> ()

(* Examples from ML2015 paper *)

type _ t = Int : int t | Bool : bool t

let f : type a. a t -> a = function Int -> 1 | Bool -> true
let g : int t -> int = function Int -> 1

let h : type a. a t -> a t -> bool =
 fun x y -> match (x, y) with Int, Int -> true | Bool, Bool -> true

type (_, _) cmp = Eq : ('a, 'a) cmp | Any : ('a, 'b) cmp

module A : sig
  type a
  type b

  val eq : (a, b) cmp
end = struct
  type a
  type b = a

  let eq = Eq
end

let f : (A.a, A.b) cmp -> unit = function Any -> ()
let deep : char t option -> char = function None -> 'c'

type zero = Zero
type _ succ = Succ

type (_, _, _) plus =
  | Plus0 : (zero, 'a, 'a) plus
  | PlusS : ('a, 'b, 'c) plus -> ('a succ, 'b, 'c succ) plus

let trivial : (zero succ, zero, zero) plus option -> bool = function
  | None -> false

let easy : (zero, zero succ, zero) plus option -> bool = function
  | None -> false

let harder : (zero succ, zero succ, zero succ) plus option -> bool = function
  | None -> false

let harder : (zero succ, zero succ, zero succ) plus option -> bool = function
  | None -> false
  | Some (PlusS _) -> .

let inv_zero : type a b c d. (a, b, c) plus -> (c, d, zero) plus -> bool =
 fun p1 p2 -> match (p1, p2) with Plus0, Plus0 -> true

(* Empty match *)

type _ t = Int : int t

let f (x : bool t) = match x with _ -> .

(* ok *)

(* trefis in PR#6437 *)

let f () = match None with _ -> .

(* error *)
let g () = match None with _ -> () | exception _ -> .

(* error *)
let h () = match None with _ -> . | exception _ -> .

(* error *)
let f x = match x with _ -> () | None -> .

(* do not warn *)

(* #7059, all clauses guarded *)

let f x y = match 1 with 1 when x = y -> 1

open CamlinternalOO

type _ choice = Left : label choice | Right : tag choice

let f : label choice -> bool = function Left -> true

(* warn *)
exception A

type a = A;;

A;;
raise A;;
fun (A : a) -> ();;
function Not_found -> 1 | A -> 2 | _ -> 3;;
try raise A with A -> 2;;

module TypEq = struct
  type (_, _) t = Eq : ('a, 'a) t
end

module type T = sig
  type _ is_t = Is : ('a, 'b) TypEq.t -> 'a is_t

  val is_t : unit -> unit is_t option
end

module Make (M : T) = struct
  let _ = match M.is_t () with None -> 0 | Some _ -> 0
  let f () = match M.is_t () with None -> 0
end

module Make2 (M : T) = struct
  type t = T of unit M.is_t

  let g : t -> int = function _ -> .
end

type t = A : t

module X1 : sig end = struct
  let _f ~x (* x unused argument *) = function
    | A ->
        let x = () in
        x
end

module X2 : sig end = struct
  let x = 42 (* unused value *)

  let _f = function
    | A ->
        let x = () in
        x
end

module X3 : sig end = struct
  module O = struct
    let x = 42 (* unused *)
  end

  open O (* unused open *)

  let _f = function
    | A ->
        let x = () in
        x
end

(* Use type information *)
module M1 = struct
  type t = { x : int; y : int }
  type u = { x : bool; y : bool }
end

module OK = struct
  open M1

  let f1 (r : t) = r.x (* ok *)

  let f2 r =
    ignore (r : t);
    r.x (* non principal *)

  let f3 (r : t) = match r with { x; y } -> y + y (* ok *)
end

module F1 = struct
  open M1

  let f r = match r with { x; y } -> y + y
end

(* fails *)

module F2 = struct
  open M1

  let f r =
    ignore (r : t);
    match r with { x; y } -> y + y
end

(* fails for -principal *)

(* Use type information with modules*)
module M = struct
  type t = { x : int }
  type u = { x : bool }
end

let f (r : M.t) = r.M.x

(* ok *)
let f (r : M.t) = r.x

(* warning *)
let f ({ x } : M.t) = x

(* warning *)

module M = struct
  type t = { x : int; y : int }
end

module N = struct
  type u = { x : bool; y : bool }
end

module OK = struct
  open M
  open N

  let f (r : M.t) = r.x
end

module M = struct
  type t = { x : int }

  module N = struct
    type s = t = { x : int }
  end

  type u = { x : bool }
end

module OK = struct
  open M.N

  let f (r : M.t) = r.x
end

(* Use field information *)
module M = struct
  type u = { x : bool; y : int; z : char }
  type t = { x : int; y : bool }
end

module OK = struct
  open M

  let f { x; z } = (x, z)
end

(* ok *)
module F3 = struct
  open M

  let r = { x = true; z = 'z' }
end

(* fail for missing label *)

module OK = struct
  type u = { x : int; y : bool }
  type t = { x : bool; y : int; z : char }

  let r = { x = 3; y = true }
end

(* ok *)

(* Corner cases *)

module F4 = struct
  type foo = { x : int; y : int }
  type bar = { x : int }

  let b : bar = { x = 3; y = 4 }
end

(* fail but don't warn *)

module M = struct
  type foo = { x : int; y : int }
end

module N = struct
  type bar = { x : int; y : int }
end

let r = { M.x = 3; N.y = 4 }

(* error: different definitions *)

module MN = struct
  include M
  include N
end

module NM = struct
  include N
  include M
end

let r = { MN.x = 3; NM.y = 4 }

(* error: type would change with order *)

(* Lpw25 *)

module M = struct
  type foo = { x : int; y : int }
  type bar = { x : int; y : int; z : int }
end

module F5 = struct
  open M

  let f r =
    ignore (r : foo);
    { r with x = 2; z = 3 }
end

module M = struct
  include M

  type other = { a : int; b : int }
end

module F6 = struct
  open M

  let f r =
    ignore (r : foo);
    { r with x = 3; a = 4 }
end

module F7 = struct
  open M

  let r = { x = 1; y = 2 }
  let r : other = { x = 1; y = 2 }
end

module A = struct
  type t = { x : int }
end

module B = struct
  type t = { x : int }
end

let f (r : B.t) = r.A.x

(* fail *)

(* Spellchecking *)

module F8 = struct
  type t = { x : int; yyy : int }

  let a : t = { x = 1; yyz = 2 }
end

(* PR#6004 *)

type t = A
type s = A

class f (_ : t) = object end
class g = f A

(* ok *)

class f (_ : 'a) (_ : 'a) = object end
class g = f (A : t) A

(* warn with -principal *)

(* PR#5980 *)

module Shadow1 = struct
  type t = { x : int }

  module M = struct
    type s = { x : string }
  end

  open M (* this open is unused, it isn't reported as shadowing 'x' *)

  let y : t = { x = 0 }
end

module Shadow2 = struct
  type t = { x : int }

  module M = struct
    type s = { x : string }
  end

  open M (* this open shadows label 'x' *)

  let y = { x = "" }
end

(* PR#6235 *)

module P6235 = struct
  type t = { loc : string }
  type v = { loc : string; x : int }
  type u = [ `Key of t ]

  let f (u : u) = match u with `Key { loc } -> loc
end

(* Remove interaction between branches *)

module P6235' = struct
  type t = { loc : string }
  type v = { loc : string; x : int }
  type u = [ `Key of t ]

  let f = function (_ : u) when false -> "" | `Key { loc } -> loc
end

module Unused : sig end = struct
  type unused = int
end

module Unused_nonrec : sig end = struct
  type nonrec used = int
  type nonrec unused = used
end

module Unused_rec : sig end = struct
  type unused = A of unused
end

module Unused_exception : sig end = struct
  exception Nobody_uses_me
end

module Unused_extension_constructor : sig
  type t = ..
end = struct
  type t = ..
  type t += Nobody_uses_me
end

module Unused_exception_outside_patterns : sig
  val falsity : exn -> bool
end = struct
  exception Nobody_constructs_me

  let falsity = function Nobody_constructs_me -> true | _ -> false
end

module Unused_extension_outside_patterns : sig
  type t = ..

  val falsity : t -> bool
end = struct
  type t = ..
  type t += Nobody_constructs_me

  let falsity = function Nobody_constructs_me -> true | _ -> false
end

module Unused_private_exception : sig
  type exn += private Private_exn
end = struct
  exception Private_exn
end

module Unused_private_extension : sig
  type t = ..
  type t += private Private_ext
end = struct
  type t = ..
  type t += Private_ext
end
;;

for i = 10 downto 0 do
  ()
done
;;

type t = < foo : int [@foo] >

let _ = [%foo: < foo : t > ]

type foo += private A of int

let f : 'a 'b 'c. < .. > = assert false

let () =
  let module M = (functor (T : sig end) -> struct end) (struct end) in
  ()

class c =
  object
    inherit (fun () -> object end [@wee] : object end) ()
  end

let f = function (x [@wee]) -> ()
let f = function '1' .. '9' | '1' .. '8' -> () | 'a' .. 'z' -> ()

let f = function
  | [| x1; x2 |] -> ()
  | [||] -> ()
  | ([| x |] [@foo]) -> ()
  | _ -> ()

let g = function
  | { l = x } -> ()
  | ({ l1 = x; l2 = y } [@foo]) -> ()
  | { l1 = x; l2 = y; _ } -> ()

let h = fun ?l:(p = 1) ?y:u ?(x = 3) -> 2

let _ = function
  | a, s, ba1, ba2, ba3, bg -> begin
      ignore
        (Array.get x 1 + Array.get [||] 0 + Array.get [| 1 |] 1
        + Array.get [| 1; 2 |] 2);
      ignore [ String.get s 1; String.get "" 2; String.get "123" 3 ];
      ignore (ba1.{0} + ba2.{1, 2} + ba3.{3, 4, 5}) ignore bg.{1, 2, 3, 4}
    end
  | b, s, ba1, ba2, ba3, bg -> begin
      y.(0) <- 1;
      s.![1] <- 'c';
      ba1.{1} <- 2;
      ba2.{1, 2} <- 3;
      ba3.{1, 2, 3} <- 4;
      bg.{1, 2, 3, 4, 5} <- 0
    end

let f (type t) () =
  let exception F of t in
  ();
  let exception G of t in
  ();
  let exception E of t in
  ( (fun x -> E x),
    function E _ -> print_endline "OK" | _ -> print_endline "KO" )

let inj1, proj1 = f ()
let inj2, proj2 = f ()
let () = proj1 (inj1 42)
let () = proj1 (inj2 42)
let _ = ~-1

class id = [%exp]
(* checkpoint *)

(* Subtyping is "syntactic" *)
let _ = fun (x : < x : int >) y z -> ((y :> 'a), (x :> 'a), (z :> 'a))

(* - : (< x : int > as 'a) -> 'a -> 'a * 'a = <fun> *)

class ['a] c () =
  object
    method f = (new c () : int c)
  end

and ['a] d () =
  object
    inherit ['a] c ()
  end

(* PR#7329 Pattern open *)
let _ =
  let module M = struct
    type t = { x : int }
  end in
  let f M.(x) = () in
  let g M.{ x } = () in
  let h = function M.[] | M.[ a ] | M.(a :: q) -> () in
  let i = function M.[||] | M.[| x |] -> true | _ -> false in
  ()

class ['a] c () =
  object
    constraint 'a = < .. > -> unit
    method m = (fun x -> () : 'a)
  end

let f : type a'. a' = assert false
let foo : type a' b'. a' -> b' = fun a -> assert false
let foo : type t'. t' = fun (type t') -> (assert false : t')
let foo : 't. 't = fun (type t) -> (assert false : t)
let foo : type a' b' c' t. a' -> b' -> c' -> t = fun a b c -> assert false

let f x =
  x.contents <-
    (print_string "coucou";
     x.contents)

let ( ~$ ) x = Some x
let g x = ~$(x.contents)
let ( ~$ ) x y = (x, y)
let g x y = ~$(x.contents) y.contents

(* PR#7506: attributes on list tail *)

let tail1 = [ 1; 2 ] [@hello]
let tail2 = 0 :: ([ 1; 2 ] [@hello])
let tail3 = 0 :: ([] [@hello])
let f ~l:(l [@foo]) = l
let test x y = (( + ) [@foo]) x y
let test x = (( ~- ) [@foo]) x
let test contents = { contents = contents [@foo] }

class type t = object (_[@foo]) end

let test f x = f ~x:(x [@foo])
let f = function (`A | `B) [@bar] | `C -> ()
let f = function _ :: ((_ :: _) [@foo]) -> () | _ -> ();;

function { contents = (contents [@foo]) } -> ();;
fun contents -> { contents = contents [@foo] };;

();
(();
 ())
[@foo]
;;

(* https://github.com/LexiFi/gen_js_api/issues/61 *)

let () = foo##.bar := ()

(* "let open" in classes and class types *)

class c =
  let open M in
  object
    method f : t = x
  end

class type ct =
  let open M in
object
  method f : t
end

(* M.(::) notation *)
module Exotic_list = struct
  module Inner = struct
    type ('a, 'b) t = [] | ( :: ) of 'a * 'b * ('a, 'b) t
  end

  let (Inner.( :: ) (x, y, Inner.[])) = Inner.( :: ) (1, "one", Inner.[])
end

(** Extended index operators *)
module Indexop = struct
  module Def = struct
    let ( .%[] ) = Hashtbl.find
    let ( .%[]<- ) = Hashtbl.add
    let ( .%() ) = Hashtbl.find
    let ( .%()<- ) = Hashtbl.add
    let ( .%{} ) = Hashtbl.find
    let ( .%{}<- ) = Hashtbl.add
  end
  ;;

  let h = Hashtbl.create 17 in
  h.Def.%["one"] <- 1;
  h.Def.%("two") <- 2;
  h.Def.%{"three"} <- 3
  ;;

  let x, y, z = Def.(h.%["one"], h.%("two"), h.%{"three"})
end

type t = |

(* GPR#2034 *)

let x = `Foo
let x = `(* wait for it *) Bar

type (+'a, -' a', ' a'b', 'ab', 'abcd', 'x (* ! *)) t =
  'a * ' a' * ' a'b' * 'ab' * 'abcd' * 'x (* !! *) as ' a'

(* #2190 *)

let f = function (lazy (A foo)) -> foo
let () = f (fun (type t) -> x)

(* #9778 *)

type t = unit

let rec equal : 'a. ('a -> 'a -> bool) -> 'a t -> 'a t -> bool =
 (fun poly_a (_ : unit) (_ : unit) -> true) [@ocaml.warning "-A"]
[@@ocaml.warning "-39"]

(* Issue #9548, PR #9591 *)

type u = [ `A ]
type v = [ u | `B ]

let f = fun (x : [ | u ]) -> x

(* Issue #9999 *)
let test = function (`A | `B) as x -> ignore x
let test = function (`A as x) | (`B as x) -> ignore x
let test = function ((`A as x) | (`B as x)) as z -> ignore (z, x)
let test = function ((`A as x) | (`B as x)) as z -> ignore (z, x)
let test = function `A | `B | `C -> ()
let test = function `A | `B | `C -> ()
let test = function `A | `B | `C -> ()
let test = function ((`A | `B) as x) | `C -> ()

(* Let-punning *)
module M = struct
  let ( let* ) x f = f x
  let ( and* ) a b = (a, b)

  let x = 1
  and y = 2
  and z = 3

  let p =
    let* x and* y and* z in
    (x, y, z)

  let q =
    let%foo x and y and z in
    (x, y, z)
end

(* No surrounding parentheses for immediate objects *)
let x =
  object
    method f = 1
  end

let x =
  object
    method f = 1
  end
    #f

let x =
  Some
    object
      method f = 1
    end

let x =
  Some
    object
      method f = 1
    end
      #f
;;

let f x y z = x in
f
  object
    method f = 1
  end
  object
    method f = 1
  end
    #f
  object end
;;

(* Punning of labelled function argument with type constraint *)
let g y =
  let f ~y = y + 1 in
  f ~(y : int)

let goober a = match a with C (type a b) y -> y

(** With constraints *)

module type s = sig
  type ('a, 'b) t
end
with type (-!'a, !+'b) t = 'b -> 'a list

module type s = sig
  type ('a, 'b) t
end
with type (!-'a, +!'b) t := 'b -> 'a list

module type s = sig
  type ('a, 'b) t
end
with type ('a, 'b) t := 'b -> 'a list

(* Coercion in value constraint *)

let x : [ `A ] :> [> `A | `B ] = `A
let x :> [> `A | `B ] = `A

(* Raw identifiers *)

module type A = sig
  type ('\#let, '\#a) \#virtual = '\#let * '\#a as '\#mutable

  val foo : '\#let '\#a. '\#a -> '\#let -> unit

  type \#foo = { \#let : int }
end

module M = struct
  let ((\#let, \#foo) as \#val) = (\#mutable, \#baz)
  let _ = fun (type \#let) (type \#foo) -> 1
  let f g ~\#let ?\#and ?(\#for = \#and) () = g ~\#let ?\#and ()

  class \#let =
    object
      inherit \#val \#let as \#mutable
    end
end

let x = new M.\#begin
let f = fun x (type \#begin) (type \#end) -> 1
let f : type \#if. \#if -> \#if = fun x -> x

(* check pretty-printing of local module open in core_type *)
type t = String.(t)

(* Utf8 identifier *)
let là = function ça -> ça