From 05f59b0b4f8d63cf8d94526742002c6822e0ee8d Mon Sep 17 00:00:00 2001 From: Jules Aguillon Date: Thu, 5 Sep 2024 15:34:28 +0200 Subject: [PATCH] tests: Add source-conventional.ml.ref --- test/passing/dune.inc | 18 + test/passing/tests/source-conventional.ml.err | 6 + .../passing/tests/source-conventional.ml.opts | 1 + test/passing/tests/source-conventional.ml.ref | 8701 +++++++++++++++++ 4 files changed, 8726 insertions(+) create mode 100644 test/passing/tests/source-conventional.ml.err create mode 100644 test/passing/tests/source-conventional.ml.opts create mode 100644 test/passing/tests/source-conventional.ml.ref diff --git a/test/passing/dune.inc b/test/passing/dune.inc index 9a1f00a0cc..bb963092e2 100644 --- a/test/passing/dune.inc +++ b/test/passing/dune.inc @@ -5020,6 +5020,24 @@ (package ocamlformat) (action (diff tests/skip.ml.err skip.ml.stderr))) +(rule + (deps tests/.ocamlformat ) + (package ocamlformat) + (action + (with-stdout-to source-conventional.ml.stdout + (with-stderr-to source-conventional.ml.stderr + (run %{bin:ocamlformat} --margin-check --profile=default --max-iters=3 %{dep:tests/source.ml}))))) + +(rule + (alias runtest) + (package ocamlformat) + (action (diff tests/source-conventional.ml.ref source-conventional.ml.stdout))) + +(rule + (alias runtest) + (package ocamlformat) + (action (diff tests/source-conventional.ml.err source-conventional.ml.stderr))) + (rule (deps tests/.ocamlformat ) (package ocamlformat) diff --git a/test/passing/tests/source-conventional.ml.err b/test/passing/tests/source-conventional.ml.err new file mode 100644 index 0000000000..4dc692a474 --- /dev/null +++ b/test/passing/tests/source-conventional.ml.err @@ -0,0 +1,6 @@ +Warning: tests/source.ml:927 exceeds the margin +Warning: tests/source.ml:1002 exceeds the margin +Warning: tests/source.ml:1225 exceeds the margin +Warning: tests/source.ml:1342 exceeds the margin +Warning: tests/source.ml:6617 exceeds the margin +Warning: tests/source.ml:7075 exceeds the margin diff --git a/test/passing/tests/source-conventional.ml.opts b/test/passing/tests/source-conventional.ml.opts new file mode 100644 index 0000000000..bfae9aa9ca --- /dev/null +++ b/test/passing/tests/source-conventional.ml.opts @@ -0,0 +1 @@ +--profile=default --max-iters=3 diff --git a/test/passing/tests/source-conventional.ml.ref b/test/passing/tests/source-conventional.ml.ref new file mode 100644 index 0000000000..e0885dd89d --- /dev/null +++ b/test/passing/tests/source-conventional.ml.ref @@ -0,0 +1,8701 @@ +[@@@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 + [%foo + (let module M = M in + ()) + [@foo]]; + [%foo + (let open M in + ()) [@foo]]; + [%foo fun [@foo] x -> ()]; + [%foo function[@foo] x -> ()]; + [%foo try[@foo] () with _ -> ()]; + if%foo [@foo] () then () else (); + [%foo + while () do + () + done + [@foo]]; + [%foo + for x = () to () do + () + done + [@foo]]; + [%foo assert true [@foo]]; + [%foo lazy x [@foo]]; + [%foo object end [@foo]]; + [%foo + begin [@foo] + 3 + end]; + [%foo new x [@foo]]; + + [%foo + match[@foo] () with + | [%foo? + (* Pattern expressions *) + ((lazy x) + [@foo])] -> + () + | [%foo? ((exception x) [@foo])] -> ()] + +(* 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) + -> functor + (_ : (module type of M) [@foo]) + -> sig end [@foo] + +module type S = functor (_ : S) (_ : S) -> S +module type S = functor (_ : functor (_ : S) -> S) -> S +module type S = functor (M : S) (_ : S) -> S +module type S = functor (_ : functor (M : S) -> S) -> S +module type S = functor (_ : functor [@foo] (_ : S) -> S) -> S +module type S = functor (_ : 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 + +class%foo [@foo] x = x + +class type%foo [@foo] x = x + +external%foo [@foo] x : _ = "" + +exception%foo [@foo] X + +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 retrive 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 = string_of_int; 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 string_of_int 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 -> string_of_int (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 + (string_of_int + (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 = *) + +(** 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 = *) + +(** 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 = *) + +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 -> ( + match eq_sel sel sel' with + | None -> get_case sel rem + | Some Eq -> (name, None)) + | (name, TCarg (sel', ty)) :: rem -> ( + match eq_sel sel sel' with + | None -> get_case sel rem + | Some Eq -> (name, Some ty)) + | [] -> 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) -> ( + 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) + | _ -> 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) : + ((noarg -> a * a vlist -> unit, c) ty_sel * c -> a vlist) -> + function + | Thd, Noarg -> `Nil + | Ttl Thd, v -> `Cons v) + (* 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' -> ( + match sameNat a' b' with Some Eq -> Some Eq | None -> None) + | _ -> 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 + 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) + else + 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)) + +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 + match r with + | Leaf -> ( + match bal with Same -> Ddecr (Eq, l) | More -> Ddecr (Eq, l)) + | Node _ -> ( + 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)) + else if y < x then + match del y l with + | Dsame l -> Dsame (Node (bal, l, x, r)) + | Ddecr (Eq, l) -> ( + 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)) + else + match del y r with + | Dsame r -> Dsame (Node (bal, l, x, r)) + | Ddecr (Eq, r) -> ( + 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))) + +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) -> ( + match rep_equal a1 b1 with + | None -> None + | Some Eq -> ( + match rep_equal a2 b2 with None -> None | Some Eq -> Some Eq)) + | Rfun (a1, a2), Rfun (b1, b2) -> ( + match rep_equal a1 b1 with + | None -> None + | Some Eq -> ( + match rep_equal a2 b2 with None -> None | Some Eq -> Some Eq)) + | _ -> 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) -> ( + 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)) + | 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) -> ( + 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) -> ( + match compare a xt with + | Inl s -> Cerror s + | Inr Eq -> Cok (App (f', x'), b)) + | _ -> Cerror "Non fun in Ap"))) + | Ab (s, t, body) -> ( + 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))) + | 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 -> ( + match subst body (Bind (x, v, Id)) with + | Ex term -> ( match mode term with Pexp -> Inl term | Pval -> Inr term)) + | 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, _ -> ( + match onestep e1 with + | Inl e -> Inl (App (e, e2)) + | Inr v -> Inl (App (v, e2))) + | Pval, Pexp -> ( + match onestep e2 with + | Inl e -> Inl (App (e1, e)) + | Inr v -> Inl (App (e1, v))) + | 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 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 = +|}] + +let test_foo () = + for i = 0 to 100_000_000 do + Foo.x := !Foo.x + done + +[%%expect {| +val test_foo : unit -> unit = +|}] + +let test_bar () = + for i = 0 to 100_000_000 do + Bar.x := !Bar.x + done + +[%%expect {| +val test_bar : unit -> unit = +|}] + +(* 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 to omit the signature in (val ...) expressions. + + 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 -> string_of_int (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 ^ string_of_int (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 ^ string_of_int (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 ^ string_of_int (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 t -> (array_of_sexp _of_a) t + +let _ = t_of_sexp + +let sexp_of_t : 'a. ('a -> sexp) -> 'a t -> sexp = + fun _of_a 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 _of_perms 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 _of_perms 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 t -> t__of_sexp t + + let _ = t_of_sexp + + let sexp_of_t : 'perms. ('perms -> sexp) -> 'perms t -> sexp = + fun _of_perms 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 = Pervasives.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 : M.S with type a = a) -> X.v + + method a : 'a. 'a M.s -> 'a = + fun (type a) (module X : 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 : M'.S with type a = a) -> X.v + + method a : 'a. 'a M'.s -> 'a = + fun (type a) (module X : 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 (string_of_int 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 + +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 + 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) + + 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 = {} + + method sub pos len = + {} + + 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; + {} + 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) : M2.t -> x + +(* 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 = ) *) +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 -> Pervasives.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 + 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 + +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 + +(* exemple 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 -> + 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} + | b, s, ba1, ba2, ba3, bg -> + 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 + +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 = *) + +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') : t' -> assert false +let foo : 't. 't = fun (type t) : t -> assert false +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 + +class 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] };; +fun contents -> { contents = contents [@foo]; 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 = |;; + +M.(Some x) [@foo] + +[@@@foo:] + +let x = (A B).a +let x = A (B).a + +let formula_base x = + let open Formula.Infix in + (Expr.typeof x) #== (Lit (Type IntType)) + #&& (x #<= (Expr.int 4)) + #&& ((Expr.int 0) #< x) + +let _ = call ~f:(fun pair : (a * b) -> pair);; + +f + (fun _ -> function + | true -> + let () = () in + () + | false -> ()) + () +;; + +f + (fun _ -> function + | true -> + let () = () in + () + (* comment *) + | false -> ()) + () + +let xxxxxx = + let%map (* _____________________________ + __________ *) () = + yyyyyyyy + in + { zzzzzzzzzzzzz } + +let _ = fun (x : int as 'a) : (int as 'a) -> x + +let eradicate_meta_class_is_nullsafe = + register ~id:"ERADICATE_META_CLASS_IS_NULLSAFE" + ~hum:"Class is marked @Nullsafe and has 0 issues" + (* Should be enabled for special integrations *) + ~enabled:false Info Eradicate (* TODO *) + ~user_documentation:"" + +let eradicate_meta_class_is_nullsafe = + register + ~id:"ERADICATE_META_CLASS_IS_NULLSAFE" + (* Should be enabled for special integrations *) + ~hum:"Class is marked @Nullsafe and has 0 issues" + (* Should be enabled for special integrations *) + ~enabled:false Info + +let () = match () with _ -> ( fun _ : _ -> match () with _ -> ()) | _ -> ()