1[@@@foo] 2 3let (x[@foo]) : unit [@foo] = ()[@foo] 4 [@@foo] 5 6type t = 7 | Foo of (t[@foo]) [@foo] 8[@@foo] 9 10[@@@foo] 11 12 13module M = struct 14 type t = { 15 l : (t [@foo]) [@foo] 16 } 17 [@@foo] 18 [@@foo] 19 20 [@@@foo] 21end[@foo] 22[@@foo] 23 24module type S = sig 25 26 include (module type of (M[@foo]))[@foo] with type t := M.t[@foo] 27 [@@foo] 28 29 [@@@foo] 30 31end[@foo] 32[@@foo] 33 34[@@@foo] 35type 'a with_default 36 = ?size:int (** default [42] *) 37 -> ?resizable:bool (** default [true] *) 38 -> 'a 39 40type obj = < 41 meth1 : int -> int; 42 (** method 1 *) 43 44 meth2: unit -> float (** method 2 *); 45> 46 47type var = [ 48 | `Foo (** foo *) 49 | `Bar of int * string (** bar *) 50] 51 52[%%foo let x = 1 in x] 53let [%foo 2+1] : [%foo bar.baz] = [%foo "foo"] 54 55[%%foo module M = [%bar] ] 56let [%foo let () = () ] : [%foo type t = t ] = [%foo class c = object end] 57 58[%%foo: 'a list] 59let [%foo: [`Foo] ] : [%foo: t -> t ] = [%foo: < foo : t > ] 60 61[%%foo? _ ] 62[%%foo? Some y when y > 0] 63let [%foo? (Bar x | Baz x) ] : [%foo? #bar ] = [%foo? { x }] 64 65[%%foo: module M : [%baz]] 66let [%foo: include S with type t = t ] 67 : [%foo: val x : t val y : t] 68 = [%foo: type t = t ] 69let int_with_custom_modifier = 70 1234567890_1234567890_1234567890_1234567890_1234567890z 71let float_with_custom_modifier = 72 1234567890_1234567890_1234567890_1234567890_1234567890.z 73 74let int32 = 1234l 75let int64 = 1234L 76let nativeint = 1234n 77 78let hex_without_modifier = 0x32f 79let hex_with_modifier = 0x32g 80 81let float_without_modifer = 1.2e3 82let float_with_modifer = 1.2g 83let%foo x = 42 84let%foo _ = () and _ = () 85let%foo _ = () 86 87(* Expressions *) 88let () = 89 let%foo[@foo] x = 3 90 and[@foo] y = 4 in 91 (let module%foo[@foo] M = M in ()) ; 92 (let open%foo[@foo] M in ()) ; 93 (fun%foo[@foo] x -> ()) ; 94 (function%foo[@foo] x -> ()) ; 95 (try%foo[@foo] () with _ -> ()) ; 96 (if%foo[@foo] () then () else ()) ; 97 while%foo[@foo] () do () done ; 98 for%foo[@foo] x = () to () do () done ; 99 assert%foo[@foo] true ; 100 lazy%foo[@foo] x ; 101 object%foo[@foo] end ; 102 begin%foo[@foo] 3 end ; 103 new%foo[@foo] x ; 104 105 match%foo[@foo] () with 106 (* Pattern expressions *) 107 | lazy%foo[@foo] x -> () 108 | exception%foo[@foo] x -> () 109 110(* Class expressions *) 111class x = 112 fun[@foo] x -> 113 let[@foo] x = 3 in 114 object[@foo] 115 inherit[@foo] x 116 val[@foo] x = 3 117 val[@foo] virtual x : t 118 val![@foo] mutable x = 3 119 method[@foo] x = 3 120 method[@foo] virtual x : t 121 method![@foo] private x = 3 122 initializer[@foo] x 123 end 124 125(* Class type expressions *) 126class type t = 127 object[@foo] 128 inherit[@foo] t 129 val[@foo] x : t 130 val[@foo] mutable x : t 131 method[@foo] x : t 132 method[@foo] private x : t 133 constraint[@foo] t = t' 134 [@@@abc] 135 [%%id] 136 [@@@aaa] 137 end 138 139(* Type expressions *) 140type t = 141 (module%foo[@foo] M) 142 143(* Module expressions *) 144module M = 145 functor[@foo] (M : S) -> 146 (val[@foo] x) 147 (struct[@foo] end) 148 149(* Module type expression *) 150module type S = 151 functor[@foo] (M:S) -> 152 (module type of[@foo] M) -> 153 (sig[@foo] end) 154 155(* Structure items *) 156let%foo[@foo] x = 4 157and[@foo] y = x 158 159type%foo[@foo] t = int 160and[@foo] t = int 161type%foo[@foo] t += T 162 163class%foo[@foo] x = x 164class type%foo[@foo] x = x 165external%foo[@foo] x : _ = "" 166exception%foo[@foo] X 167 168module%foo[@foo] M = M 169module%foo[@foo] rec M : S = M 170and[@foo] M : S = M 171module type%foo[@foo] S = S 172 173include%foo[@foo] M 174open%foo[@foo] M 175 176(* Signature items *) 177module type S = sig 178 val%foo[@foo] x : t 179 external%foo[@foo] x : t = "" 180 181 type%foo[@foo] t = int 182 and[@foo] t' = int 183 type%foo[@foo] t += T 184 185 exception%foo[@foo] X 186 187 module%foo[@foo] M : S 188 module%foo[@foo] rec M : S 189 and[@foo] M : S 190 module%foo[@foo] M = M 191 192 module type%foo[@foo] S = S 193 194 include%foo[@foo] M 195 open%foo[@foo] M 196 197 class%foo[@foo] x : t 198 class type%foo[@foo] x = x 199 200end 201 202type t = ..;; 203type t += A;; 204 205[%extension_constructor A];; 206([%extension_constructor A] : extension_constructor);; 207 208module M = struct 209 type extension_constructor = int 210end;; 211 212open M;; 213 214([%extension_constructor A] : extension_constructor);; 215 216(* By using two types we can have a recursive constraint *) 217type 'a class_name = .. constraint 'a = < cast: 'a. 'a name -> 'a; ..> 218and 'a name = 219 Class : 'a class_name -> (< cast: 'a. 'a name -> 'a; ..> as 'a) name 220;; 221 222exception Bad_cast 223;; 224 225class type castable = 226object 227 method cast: 'a.'a name -> 'a 228end 229;; 230 231(* Lets create a castable class with a name*) 232 233class type foo_t = 234object 235 inherit castable 236 method foo: string 237end 238;; 239 240type 'a class_name += Foo: foo_t class_name 241;; 242 243class foo: foo_t = 244object(self) 245 method cast: type a. a name -> a = 246 function 247 Class Foo -> (self :> foo_t) 248 | _ -> ((raise Bad_cast) : a) 249 method foo = "foo" 250end 251;; 252 253(* Now we can create a subclass of foo *) 254 255class type bar_t = 256object 257 inherit foo 258 method bar: string 259end 260;; 261 262type 'a class_name += Bar: bar_t class_name 263;; 264 265class bar: bar_t = 266object(self) 267 inherit foo as super 268 method cast: type a. a name -> a = 269 function 270 Class Bar -> (self :> bar_t) 271 | other -> super#cast other 272 method bar = "bar" 273 [@@@id] 274 [%%id] 275end 276;; 277 278(* Now lets create a mutable list of castable objects *) 279 280let clist :castable list ref = ref [] 281;; 282 283let push_castable (c: #castable) = 284 clist := (c :> castable) :: !clist 285;; 286 287let pop_castable () = 288 match !clist with 289 c :: rest -> 290 clist := rest; 291 c 292 | [] -> raise Not_found 293;; 294 295(* We can add foos and bars to this list, and retrive them *) 296 297push_castable (new foo);; 298push_castable (new bar);; 299push_castable (new foo);; 300 301let c1: castable = pop_castable ();; 302let c2: castable = pop_castable ();; 303let c3: castable = pop_castable ();; 304 305(* We can also downcast these values to foos and bars *) 306 307let f1: foo = c1#cast (Class Foo);; (* Ok *) 308let f2: foo = c2#cast (Class Foo);; (* Ok *) 309let f3: foo = c3#cast (Class Foo);; (* Ok *) 310 311let b1: bar = c1#cast (Class Bar);; (* Exception Bad_cast *) 312let b2: bar = c2#cast (Class Bar);; (* Ok *) 313let b3: bar = c3#cast (Class Bar);; (* Exception Bad_cast *) 314 315type foo = .. 316;; 317 318type foo += 319 A 320 | B of int 321;; 322 323let is_a x = 324 match x with 325 A -> true 326 | _ -> false 327;; 328 329(* The type must be open to create extension *) 330 331type foo 332;; 333 334type foo += A of int (* Error type is not open *) 335;; 336 337(* The type parameters must match *) 338 339type 'a foo = .. 340;; 341 342type ('a, 'b) foo += A of int (* Error: type parameter mismatch *) 343;; 344 345(* In a signature the type does not have to be open *) 346 347module type S = 348sig 349 type foo 350 type foo += A of float 351end 352;; 353 354(* But it must still be extensible *) 355 356module type S = 357sig 358 type foo = A of int 359 type foo += B of float (* Error foo does not have an extensible type *) 360end 361;; 362 363(* Signatures can change the grouping of extensions *) 364 365type foo = .. 366;; 367 368module M = struct 369 type foo += 370 A of int 371 | B of string 372 373 type foo += 374 C of int 375 | D of float 376end 377;; 378 379module type S = sig 380 type foo += 381 B of string 382 | C of int 383 384 type foo += D of float 385 386 type foo += A of int 387end 388;; 389 390module M_S = (M : S) 391;; 392 393(* Extensions can be GADTs *) 394 395type 'a foo = .. 396;; 397 398type _ foo += 399 A : int -> int foo 400 | B : int foo 401;; 402 403let get_num : type a. a foo -> a -> a option = fun f i1 -> 404 match f with 405 A i2 -> Some (i1 + i2) 406 | _ -> None 407;; 408 409(* Extensions must obey constraints *) 410 411type 'a foo = .. constraint 'a = [> `Var ] 412;; 413 414type 'a foo += A of 'a 415;; 416 417let a = A 9 (* ERROR: Constraints not met *) 418;; 419 420type 'a foo += B : int foo (* ERROR: Constraints not met *) 421;; 422 423(* Signatures can make an extension private *) 424 425type foo = .. 426;; 427 428module M = struct type foo += A of int end 429;; 430 431let a1 = M.A 10 432;; 433 434module type S = sig type foo += private A of int end 435;; 436 437module M_S = (M : S) 438;; 439 440let is_s x = 441 match x with 442 M_S.A _ -> true 443 | _ -> false 444;; 445 446let a2 = M_S.A 20 (* ERROR: Cannot create a value using a private constructor *) 447;; 448 449(* Extensions can be rebound *) 450 451type foo = .. 452;; 453 454module M = struct type foo += A1 of int end 455;; 456 457type foo += A2 = M.A1 458;; 459 460type bar = .. 461;; 462 463type bar += A3 = M.A1 (* Error: rebind wrong type *) 464;; 465 466module M = struct type foo += private B1 of int end 467;; 468 469type foo += private B2 = M.B1 470;; 471 472type foo += B3 = M.B1 (* Error: rebind private extension *) 473;; 474 475type foo += C = Unknown (* Error: unbound extension *) 476;; 477 478(* Extensions can be rebound even if type is closed *) 479 480module M : sig type foo type foo += A1 of int end 481 = struct type foo = .. type foo += A1 of int end 482 483type M.foo += A2 = M.A1 484 485(* Rebinding handles abbreviations *) 486 487type 'a foo = .. 488;; 489 490type 'a foo1 = 'a foo = .. 491;; 492 493type 'a foo2 = 'a foo = .. 494;; 495 496type 'a foo1 += 497 A of int 498 | B of 'a 499 | C : int foo1 500;; 501 502type 'a foo2 += 503 D = A 504 | E = B 505 | F = C 506;; 507 508(* Extensions must obey variances *) 509 510type +'a foo = .. 511;; 512 513type 'a foo += A of (int -> 'a) 514;; 515 516type 'a foo += B of ('a -> int) 517 (* ERROR: Parameter variances are not satisfied *) 518;; 519 520type _ foo += C : ('a -> int) -> 'a foo 521 (* ERROR: Parameter variances are not satisfied *) 522;; 523 524type 'a bar = .. 525;; 526 527type +'a bar += D of (int -> 'a) (* ERROR: type variances do not match *) 528;; 529 530(* Exceptions are compatible with extensions *) 531 532module M : sig 533 type exn += 534 Foo of int * float 535 | Bar : 'a list -> exn 536end = struct 537 exception Bar : 'a list -> exn 538 exception Foo of int * float 539end 540;; 541 542module M : sig 543 exception Bar : 'a list -> exn 544 exception Foo of int * float 545end = struct 546 type exn += 547 Foo of int * float 548 | Bar : 'a list -> exn 549end 550;; 551 552exception Foo of int * float 553;; 554 555exception Bar : 'a list -> exn 556;; 557 558module M : sig 559 type exn += 560 Foo of int * float 561 | Bar : 'a list -> exn 562end = struct 563 exception Bar = Bar 564 exception Foo = Foo 565end 566;; 567 568(* Test toplevel printing *) 569 570type foo = .. 571;; 572 573type foo += 574 Foo of int * int option 575 | Bar of int option 576;; 577 578let x = Foo(3, Some 4), Bar(Some 5) (* Prints Foo and Bar successfully *) 579;; 580 581type foo += Foo of string 582;; 583 584let y = x (* Prints Bar but not Foo (which has been shadowed) *) 585;; 586 587exception Foo of int * int option 588;; 589 590exception Bar of int option 591;; 592 593let x = Foo(3, Some 4), Bar(Some 5) (* Prints Foo and Bar successfully *) 594;; 595 596type foo += Foo of string 597;; 598 599let y = x (* Prints Bar and part of Foo (which has been shadowed) *) 600;; 601 602(* Test Obj functions *) 603 604type foo = .. 605;; 606 607type foo += 608 Foo 609 | Bar of int 610;; 611 612let extension_name e = Obj.extension_name (Obj.extension_constructor e);; 613let extension_id e = Obj.extension_id (Obj.extension_constructor e);; 614 615let n1 = extension_name Foo 616;; 617 618let n2 = extension_name (Bar 1) 619;; 620 621let t = (extension_id (Bar 2)) = (extension_id (Bar 3)) (* true *) 622;; 623 624let f = (extension_id (Bar 2)) = (extension_id Foo) (* false *) 625;; 626 627let is_foo x = (extension_id Foo) = (extension_id x) 628 629type foo += Foo 630;; 631 632let f = is_foo Foo 633;; 634 635let _ = Obj.extension_constructor 7 (* Invald_arg *) 636;; 637 638let _ = Obj.extension_constructor (object method m = 3 end) (* Invald_arg *) 639;; 640(* Typed names *) 641 642module Msg : sig 643 644 type 'a tag 645 646 type result = Result : 'a tag * 'a -> result 647 648 val write : 'a tag -> 'a -> unit 649 650 val read : unit -> result 651 652 type 'a tag += Int : int tag 653 654 module type Desc = sig 655 type t 656 val label : string 657 val write : t -> string 658 val read : string -> t 659 end 660 661 module Define (D : Desc) : sig 662 type 'a tag += C : D.t tag 663 end 664 665end = struct 666 667 type 'a tag = .. 668 669 type ktag = T : 'a tag -> ktag 670 671 type 'a kind = 672 { tag : 'a tag; 673 label : string; 674 write : 'a -> string; 675 read : string -> 'a; } 676 677 type rkind = K : 'a kind -> rkind 678 679 type wkind = { f : 'a . 'a tag -> 'a kind } 680 681 let readTbl : (string, rkind) Hashtbl.t = Hashtbl.create 13 682 683 let writeTbl : (ktag, wkind) Hashtbl.t = Hashtbl.create 13 684 685 let read_raw () : string * string = raise (Failure "Not implemented") 686 687 type result = Result : 'a tag * 'a -> result 688 689 let read () = 690 let label, content = read_raw () in 691 let K k = Hashtbl.find readTbl label in 692 let body = k.read content in 693 Result(k.tag, body) 694 695 let write_raw (label : string) (content : string) = 696 raise (Failure "Not implemented") 697 698 let write (tag : 'a tag) (body : 'a) = 699 let {f} = Hashtbl.find writeTbl (T tag) in 700 let k = f tag in 701 let content = k.write body in 702 write_raw k.label content 703 704 (* Add int kind *) 705 706 type 'a tag += Int : int tag 707 708 let ik = 709 { tag = Int; 710 label = "int"; 711 write = string_of_int; 712 read = int_of_string } 713 714 let () = Hashtbl.add readTbl "int" (K ik) 715 716 let () = 717 let f (type t) (i : t tag) : t kind = 718 match i with 719 Int -> ik 720 | _ -> assert false 721 in 722 Hashtbl.add writeTbl (T Int) {f} 723 724 (* Support user defined kinds *) 725 726 module type Desc = sig 727 type t 728 val label : string 729 val write : t -> string 730 val read : string -> t 731 end 732 733 module Define (D : Desc) = struct 734 type 'a tag += C : D.t tag 735 let k = 736 { tag = C; 737 label = D.label; 738 write = D.write; 739 read = D.read } 740 let () = Hashtbl.add readTbl D.label (K k) 741 let () = 742 let f (type t) (c : t tag) : t kind = 743 match c with 744 C -> k 745 | _ -> assert false 746 in 747 Hashtbl.add writeTbl (T C) {f} 748 end 749 750end;; 751 752let write_int i = Msg.write Msg.Int i;; 753 754module StrM = Msg.Define(struct 755 type t = string 756 let label = "string" 757 let read s = s 758 let write s = s 759end);; 760 761type 'a Msg.tag += String = StrM.C;; 762 763let write_string s = Msg.write String s;; 764 765let read_one () = 766 let Msg.Result(tag, body) = Msg.read () in 767 match tag with 768 Msg.Int -> print_int body 769 | String -> print_string body 770 | _ -> print_string "Unknown";; 771(* Example of algorithm parametrized with modules *) 772 773let sort (type s) set l = 774 let module Set = (val set : Set.S with type elt = s) in 775 Set.elements (List.fold_right Set.add l Set.empty) 776 777let make_set (type s) cmp = 778 let module S = Set.Make(struct 779 type t = s 780 let compare = cmp 781 end) in 782 (module S : Set.S with type elt = s) 783 784let both l = 785 List.map 786 (fun set -> sort set l) 787 [ make_set compare; make_set (fun x y -> compare y x) ] 788 789let () = 790 print_endline (String.concat " " (List.map (String.concat "/") 791 (both ["abc";"xyz";"def"]))) 792 793 794(* Hiding the internal representation *) 795 796module type S = sig 797 type t 798 val to_string: t -> string 799 val apply: t -> t 800 val x: t 801end 802 803let create (type s) to_string apply x = 804 let module M = struct 805 type t = s 806 let to_string = to_string 807 let apply = apply 808 let x = x 809 end in 810 (module M : S with type t = s) 811 812let forget (type s) x = 813 let module M = (val x : S with type t = s) in 814 (module M : S) 815 816let print x = 817 let module M = (val x : S) in 818 print_endline (M.to_string M.x) 819 820let apply x = 821 let module M = (val x : S) in 822 let module N = struct 823 include M 824 let x = apply x 825 end in 826 (module N : S) 827 828let () = 829 let int = forget (create string_of_int succ 0) in 830 let str = forget (create (fun s -> s) (fun s -> s ^ s) "X") in 831 List.iter print (List.map apply [int; apply int; apply (apply str)]) 832 833 834(* Existential types + type equality witnesses -> pseudo GADT *) 835 836module TypEq : sig 837 type ('a, 'b) t 838 val apply: ('a, 'b) t -> 'a -> 'b 839 val refl: ('a, 'a) t 840 val sym: ('a, 'b) t -> ('b, 'a) t 841end = struct 842 type ('a, 'b) t = unit 843 let apply _ = Obj.magic 844 let refl = () 845 let sym () = () 846end 847 848 849module rec Typ : sig 850 module type PAIR = sig 851 type t 852 type t1 853 type t2 854 val eq: (t, t1 * t2) TypEq.t 855 val t1: t1 Typ.typ 856 val t2: t2 Typ.typ 857 end 858 859 type 'a typ = 860 | Int of ('a, int) TypEq.t 861 | String of ('a, string) TypEq.t 862 | Pair of (module PAIR with type t = 'a) 863end = struct 864 module type PAIR = sig 865 type t 866 type t1 867 type t2 868 val eq: (t, t1 * t2) TypEq.t 869 val t1: t1 Typ.typ 870 val t2: t2 Typ.typ 871 end 872 873 type 'a typ = 874 | Int of ('a, int) TypEq.t 875 | String of ('a, string) TypEq.t 876 | Pair of (module PAIR with type t = 'a) 877end 878 879open Typ 880 881let int = Int TypEq.refl 882 883let str = String TypEq.refl 884 885let pair (type s1) (type s2) t1 t2 = 886 let module P = struct 887 type t = s1 * s2 888 type t1 = s1 889 type t2 = s2 890 let eq = TypEq.refl 891 let t1 = t1 892 let t2 = t2 893 end in 894 let pair = (module P : PAIR with type t = s1 * s2) in 895 Pair pair 896 897module rec Print : sig 898 val to_string: 'a Typ.typ -> 'a -> string 899end = struct 900 let to_string (type s) t x = 901 match t with 902 | Int eq -> string_of_int (TypEq.apply eq x) 903 | String eq -> Printf.sprintf "%S" (TypEq.apply eq x) 904 | Pair p -> 905 let module P = (val p : PAIR with type t = s) in 906 let (x1, x2) = TypEq.apply P.eq x in 907 Printf.sprintf "(%s,%s)" (Print.to_string P.t1 x1) 908 (Print.to_string P.t2 x2) 909end 910 911let () = 912 print_endline (Print.to_string int 10); 913 print_endline (Print.to_string (pair int (pair str int)) (123, ("A", 456))) 914 915 916(* #6262: first-class modules and module type aliases *) 917 918module type S1 = sig end 919module type S2 = S1 920 921let _f (x : (module S1)) : (module S2) = x 922 923module X = struct 924 module type S 925end 926module Y = struct include X end 927 928let _f (x : (module X.S)) : (module Y.S) = x 929 930(* PR#6194, main example *) 931module type S3 = sig val x : bool end;; 932let f = function 933 | Some (module M : S3) when M.x ->1 934 | Some _ [@foooo]-> 2 935 | None -> 3 936;; 937print_endline (string_of_int (f (Some (module struct let x = false end))));; 938type 'a ty = 939 | Int : int ty 940 | Bool : bool ty 941 942let fbool (type t) (x : t) (tag : t ty) = 943 match tag with 944 | Bool -> x 945;; 946(* val fbool : 'a -> 'a ty -> 'a = <fun> *) 947(** OK: the return value is x of type t **) 948 949let fint (type t) (x : t) (tag : t ty) = 950 match tag with 951 | Int -> x > 0 952;; 953(* val fint : 'a -> 'a ty -> bool = <fun> *) 954(** OK: the return value is x > 0 of type bool; 955This has used the equation t = bool, not visible in the return type **) 956 957let f (type t) (x : t) (tag : t ty) = 958 match tag with 959 | Int -> x > 0 960 | Bool -> x 961(* val f : 'a -> 'a ty -> bool = <fun> *) 962 963 964let g (type t) (x : t) (tag : t ty) = 965 match tag with 966 | Bool -> x 967 | Int -> x > 0 968(* Error: This expression has type bool but an expression was expected of type 969t = int *) 970 971let id x = x;; 972let idb1 = (fun id -> let _ = id true in id) id;; 973let idb2 : bool -> bool = id;; 974let idb3 ( _ : bool ) = false;; 975 976let g (type t) (x : t) (tag : t ty) = 977 match tag with 978 | Bool -> idb3 x 979 | Int -> x > 0 980 981let g (type t) (x : t) (tag : t ty) = 982 match tag with 983 | Bool -> idb2 x 984 | Int -> x > 0 985(* Encoding generics using GADTs *) 986(* (c) Alain Frisch / Lexifi *) 987(* cf. http://www.lexifi.com/blog/dynamic-types *) 988 989(* Basic tag *) 990 991type 'a ty = 992 | Int: int ty 993 | String: string ty 994 | List: 'a ty -> 'a list ty 995 | Pair: ('a ty * 'b ty) -> ('a * 'b) ty 996;; 997 998(* Tagging data *) 999 1000type variant = 1001 | VInt of int 1002 | VString of string 1003 | VList of variant list 1004 | VPair of variant * variant 1005 1006let rec variantize: type t. t ty -> t -> variant = 1007 fun ty x -> 1008 (* type t is abstract here *) 1009 match ty with 1010 | Int -> VInt x (* in this branch: t = int *) 1011 | String -> VString x (* t = string *) 1012 | List ty1 -> 1013 VList (List.map (variantize ty1) x) 1014 (* t = 'a list for some 'a *) 1015 | Pair (ty1, ty2) -> 1016 VPair (variantize ty1 (fst x), variantize ty2 (snd x)) 1017 (* t = ('a, 'b) for some 'a and 'b *) 1018 1019exception VariantMismatch 1020 1021let rec devariantize: type t. t ty -> variant -> t = 1022 fun ty v -> 1023 match ty, v with 1024 | Int, VInt x -> x 1025 | String, VString x -> x 1026 | List ty1, VList vl -> 1027 List.map (devariantize ty1) vl 1028 | Pair (ty1, ty2), VPair (x1, x2) -> 1029 (devariantize ty1 x1, devariantize ty2 x2) 1030 | _ -> raise VariantMismatch 1031;; 1032 1033(* Handling records *) 1034 1035type 'a ty = 1036 | Int: int ty 1037 | String: string ty 1038 | List: 'a ty -> 'a list ty 1039 | Pair: ('a ty * 'b ty) -> ('a * 'b) ty 1040 | Record: 'a record -> 'a ty 1041 1042and 'a record = 1043 { 1044 path: string; 1045 fields: 'a field_ list; 1046 } 1047 1048and 'a field_ = 1049 | Field: ('a, 'b) field -> 'a field_ 1050 1051and ('a, 'b) field = 1052 { 1053 label: string; 1054 field_type: 'b ty; 1055 get: ('a -> 'b); 1056 } 1057;; 1058 1059(* Again *) 1060 1061type variant = 1062 | VInt of int 1063 | VString of string 1064 | VList of variant list 1065 | VPair of variant * variant 1066 | VRecord of (string * variant) list 1067 1068let rec variantize: type t. t ty -> t -> variant = 1069 fun ty x -> 1070 (* type t is abstract here *) 1071 match ty with 1072 | Int -> VInt x (* in this branch: t = int *) 1073 | String -> VString x (* t = string *) 1074 | List ty1 -> 1075 VList (List.map (variantize ty1) x) 1076 (* t = 'a list for some 'a *) 1077 | Pair (ty1, ty2) -> 1078 VPair (variantize ty1 (fst x), variantize ty2 (snd x)) 1079 (* t = ('a, 'b) for some 'a and 'b *) 1080 | Record {fields} -> 1081 VRecord 1082 (List.map (fun (Field{field_type; label; get}) -> 1083 (label, variantize field_type (get x))) fields) 1084;; 1085 1086(* Extraction *) 1087 1088type 'a ty = 1089 | Int: int ty 1090 | String: string ty 1091 | List: 'a ty -> 'a list ty 1092 | Pair: ('a ty * 'b ty) -> ('a * 'b) ty 1093 | Record: ('a, 'builder) record -> 'a ty 1094 1095and ('a, 'builder) record = 1096 { 1097 path: string; 1098 fields: ('a, 'builder) field list; 1099 create_builder: (unit -> 'builder); 1100 of_builder: ('builder -> 'a); 1101 } 1102 1103and ('a, 'builder) field = 1104 | Field: ('a, 'builder, 'b) field_ -> ('a, 'builder) field 1105 1106and ('a, 'builder, 'b) field_ = 1107 { 1108 label: string; 1109 field_type: 'b ty; 1110 get: ('a -> 'b); 1111 set: ('builder -> 'b -> unit); 1112 } 1113 1114let rec devariantize: type t. t ty -> variant -> t = 1115 fun ty v -> 1116 match ty, v with 1117 | Int, VInt x -> x 1118 | String, VString x -> x 1119 | List ty1, VList vl -> 1120 List.map (devariantize ty1) vl 1121 | Pair (ty1, ty2), VPair (x1, x2) -> 1122 (devariantize ty1 x1, devariantize ty2 x2) 1123 | Record {fields; create_builder; of_builder}, VRecord fl -> 1124 if List.length fields <> List.length fl then raise VariantMismatch; 1125 let builder = create_builder () in 1126 List.iter2 1127 (fun (Field {label; field_type; set}) (lab, v) -> 1128 if label <> lab then raise VariantMismatch; 1129 set builder (devariantize field_type v) 1130 ) 1131 fields fl; 1132 of_builder builder 1133 | _ -> raise VariantMismatch 1134;; 1135 1136type my_record = 1137 { 1138 a: int; 1139 b: string list; 1140 } 1141 1142let my_record = 1143 let fields = 1144 [ 1145 Field {label = "a"; field_type = Int; 1146 get = (fun {a} -> a); 1147 set = (fun (r, _) x -> r := Some x)}; 1148 Field {label = "b"; field_type = List String; 1149 get = (fun {b} -> b); 1150 set = (fun (_, r) x -> r := Some x)}; 1151 ] 1152 in 1153 let create_builder () = (ref None, ref None) in 1154 let of_builder (a, b) = 1155 match !a, !b with 1156 | Some a, Some b -> {a; b} 1157 | _ -> failwith "Some fields are missing in record of type my_record" 1158 in 1159 Record {path = "My_module.my_record"; fields; create_builder; of_builder} 1160;; 1161 1162(* Extension to recursive types and polymorphic variants *) 1163(* by Jacques Garrigue *) 1164 1165type noarg = Noarg 1166 1167type (_,_) ty = 1168 | Int: (int,_) ty 1169 | String: (string,_) ty 1170 | List: ('a,'e) ty -> ('a list, 'e) ty 1171 | Option: ('a,'e) ty -> ('a option, 'e) ty 1172 | Pair: (('a,'e) ty * ('b,'e) ty) -> ('a * 'b,'e) ty 1173 (* Support for type variables and recursive types *) 1174 | Var: ('a, 'a -> 'e) ty 1175 | Rec: ('a, 'a -> 'e) ty -> ('a,'e) ty 1176 | Pop: ('a, 'e) ty -> ('a, 'b -> 'e) ty 1177 (* Change the representation of a type *) 1178 | Conv: string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty 1179 (* Sum types (both normal sums and polymorphic variants) *) 1180 | Sum: ('a, 'e, 'b) ty_sum -> ('a, 'e) ty 1181 1182and ('a, 'e, 'b) ty_sum = 1183 { sum_proj: 'a -> string * 'e ty_dyn option; 1184 sum_cases: (string * ('e,'b) ty_case) list; 1185 sum_inj: 'c. ('b,'c) ty_sel * 'c -> 'a; } 1186 1187and 'e ty_dyn = (* dynamic type *) 1188 | Tdyn : ('a,'e) ty * 'a -> 'e ty_dyn 1189 1190and (_,_) ty_sel = (* selector from a list of types *) 1191 | Thd : ('a -> 'b, 'a) ty_sel 1192 | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel 1193 1194and (_,_) ty_case = (* type a sum case *) 1195 | TCarg : ('b,'a) ty_sel * ('a,'e) ty -> ('e,'b) ty_case 1196 | TCnoarg : ('b,noarg) ty_sel -> ('e,'b) ty_case 1197;; 1198 1199type _ ty_env = (* type variable substitution *) 1200 | Enil : unit ty_env 1201 | Econs : ('a,'e) ty * 'e ty_env -> ('a -> 'e) ty_env 1202;; 1203 1204(* Comparing selectors *) 1205type (_,_) eq = Eq: ('a,'a) eq 1206 1207let rec eq_sel : type a b c. (a,b) ty_sel -> (a,c) ty_sel -> (b,c) eq option = 1208 fun s1 s2 -> 1209 match s1, s2 with 1210 | Thd, Thd -> Some Eq 1211 | Ttl s1, Ttl s2 -> 1212 (match eq_sel s1 s2 with None -> None | Some Eq -> Some Eq) 1213 | _ -> None 1214 1215(* Auxiliary function to get the type of a case from its selector *) 1216let rec get_case : type a b e. 1217 (b, a) ty_sel -> (string * (e,b) ty_case) list -> string * (a, e) ty option = 1218 fun sel cases -> 1219 match cases with 1220 | (name, TCnoarg sel') :: rem -> 1221 begin match eq_sel sel sel' with 1222 | None -> get_case sel rem 1223 | Some Eq -> name, None 1224 end 1225 | (name, TCarg (sel', ty)) :: rem -> 1226 begin match eq_sel sel sel' with 1227 | None -> get_case sel rem 1228 | Some Eq -> name, Some ty 1229 end 1230 | [] -> raise Not_found 1231;; 1232 1233(* Untyped representation of values *) 1234type variant = 1235 | VInt of int 1236 | VString of string 1237 | VList of variant list 1238 | VOption of variant option 1239 | VPair of variant * variant 1240 | VConv of string * variant 1241 | VSum of string * variant option 1242 1243let may_map f = function Some x -> Some (f x) | None -> None 1244 1245let rec variantize : type a e. e ty_env -> (a,e) ty -> a -> variant = 1246 fun e ty v -> 1247 match ty with 1248 | Int -> VInt v 1249 | String -> VString v 1250 | List t -> VList (List.map (variantize e t) v) 1251 | Option t -> VOption (may_map (variantize e t) v) 1252 | Pair (t1, t2) -> VPair (variantize e t1 (fst v), variantize e t2 (snd v)) 1253 | Rec t -> variantize (Econs (ty, e)) t v 1254 | Pop t -> (match e with Econs (_, e') -> variantize e' t v) 1255 | Var -> (match e with Econs (t, e') -> variantize e' t v) 1256 | Conv (s, proj, inj, t) -> VConv (s, variantize e t (proj v)) 1257 | Sum ops -> 1258 let tag, arg = ops.sum_proj v in 1259 VSum (tag, may_map (function Tdyn (ty,arg) -> variantize e ty arg) arg) 1260;; 1261 1262let rec devariantize : type t e. e ty_env -> (t, e) ty -> variant -> t = 1263 fun e ty v -> 1264 match ty, v with 1265 | Int, VInt x -> x 1266 | String, VString x -> x 1267 | List ty1, VList vl -> 1268 List.map (devariantize e ty1) vl 1269 | Pair (ty1, ty2), VPair (x1, x2) -> 1270 (devariantize e ty1 x1, devariantize e ty2 x2) 1271 | Rec t, _ -> devariantize (Econs (ty, e)) t v 1272 | Pop t, _ -> (match e with Econs (_, e') -> devariantize e' t v) 1273 | Var, _ -> (match e with Econs (t, e') -> devariantize e' t v) 1274 | Conv (s, proj, inj, t), VConv (s', v) when s = s' -> 1275 inj (devariantize e t v) 1276 | Sum ops, VSum (tag, a) -> 1277 begin try match List.assoc tag ops.sum_cases, a with 1278 | TCarg (sel, t), Some a -> ops.sum_inj (sel, devariantize e t a) 1279 | TCnoarg sel, None -> ops.sum_inj (sel, Noarg) 1280 | _ -> raise VariantMismatch 1281 with Not_found -> raise VariantMismatch 1282 end 1283 | _ -> raise VariantMismatch 1284;; 1285 1286(* First attempt: represent 1-constructor variants using Conv *) 1287let wrap_A t = Conv ("`A", (fun (`A x) -> x), (fun x -> `A x), t);; 1288 1289let ty a = Rec (wrap_A (Option (Pair (a, Var)))) ;; 1290let v = variantize Enil (ty Int);; 1291let x = v (`A (Some (1, `A (Some (2, `A None))))) ;; 1292 1293(* Can also use it to decompose a tuple *) 1294 1295let triple t1 t2 t3 = 1296 Conv ("Triple", (fun (a,b,c) -> (a,(b,c))), 1297 (fun (a,(b,c)) -> (a,b,c)), Pair (t1, Pair (t2, t3))) 1298 1299let v = variantize Enil (triple String Int Int) ("A", 2, 3) ;; 1300 1301(* Second attempt: introduce a real sum construct *) 1302let ty_abc = 1303 (* Could also use [get_case] for proj, but direct definition is shorter *) 1304 let proj = function 1305 `A n -> "A", Some (Tdyn (Int, n)) 1306 | `B s -> "B", Some (Tdyn (String, s)) 1307 | `C -> "C", None 1308 (* Define inj in advance to be able to write the type annotation easily *) 1309 and inj : type c. (int -> string -> noarg -> unit, c) ty_sel * c -> 1310 [`A of int | `B of string | `C] = function 1311 Thd, v -> `A v 1312 | Ttl Thd, v -> `B v 1313 | Ttl (Ttl Thd), Noarg -> `C 1314 in 1315 (* Coherence of sum_inj and sum_cases is checked by the typing *) 1316 Sum { sum_proj = proj; sum_inj = inj; sum_cases = 1317 [ "A", TCarg (Thd, Int); "B", TCarg (Ttl Thd, String); 1318 "C", TCnoarg (Ttl (Ttl Thd)) ] } 1319;; 1320 1321let v = variantize Enil ty_abc (`A 3) 1322let a = devariantize Enil ty_abc v 1323 1324(* And an example with recursion... *) 1325type 'a vlist = [`Nil | `Cons of 'a * 'a vlist] 1326 1327let ty_list : type a e. (a, e) ty -> (a vlist, e) ty = fun t -> 1328 let tcons = Pair (Pop t, Var) in 1329 Rec (Sum { 1330 sum_proj = (function 1331 `Nil -> "Nil", None 1332 | `Cons p -> "Cons", Some (Tdyn (tcons, p))); 1333 sum_cases = ["Nil", TCnoarg Thd; "Cons", TCarg (Ttl Thd, tcons)]; 1334 sum_inj = fun (type c) -> 1335 (function 1336 | Thd, Noarg -> `Nil 1337 | Ttl Thd, v -> `Cons v 1338 : (noarg -> a * a vlist -> unit, c) ty_sel * c -> a vlist) 1339 (* One can also write the type annotation directly *) 1340 }) 1341 1342let v = variantize Enil (ty_list Int) (`Cons (1, `Cons (2, `Nil))) ;; 1343 1344 1345(* Simpler but weaker approach *) 1346 1347type (_,_) ty = 1348 | Int: (int,_) ty 1349 | String: (string,_) ty 1350 | List: ('a,'e) ty -> ('a list, 'e) ty 1351 | Option: ('a,'e) ty -> ('a option, 'e) ty 1352 | Pair: (('a,'e) ty * ('b,'e) ty) -> ('a * 'b,'e) ty 1353 | Var: ('a, 'a -> 'e) ty 1354 | Rec: ('a, 'a -> 'e) ty -> ('a,'e) ty 1355 | Pop: ('a, 'e) ty -> ('a, 'b -> 'e) ty 1356 | Conv: string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty 1357 | Sum: ('a -> string * 'e ty_dyn option) * (string * 'e ty_dyn option -> 'a) 1358 -> ('a, 'e) ty 1359and 'e ty_dyn = 1360 | Tdyn : ('a,'e) ty * 'a -> 'e ty_dyn 1361 1362let ty_abc : ([`A of int | `B of string | `C],'e) ty = 1363 (* Could also use [get_case] for proj, but direct definition is shorter *) 1364 Sum ( 1365 (function 1366 `A n -> "A", Some (Tdyn (Int, n)) 1367 | `B s -> "B", Some (Tdyn (String, s)) 1368 | `C -> "C", None), 1369 (function 1370 "A", Some (Tdyn (Int, n)) -> `A n 1371 | "B", Some (Tdyn (String, s)) -> `B s 1372 | "C", None -> `C 1373 | _ -> invalid_arg "ty_abc")) 1374;; 1375 1376(* Breaks: no way to pattern-match on a full recursive type *) 1377let ty_list : type a e. (a,e) ty -> (a vlist,e) ty = fun t -> 1378 let targ = Pair (Pop t, Var) in 1379 Rec (Sum ( 1380 (function `Nil -> "Nil", None 1381 | `Cons p -> "Cons", Some (Tdyn (targ, p))), 1382 (function "Nil", None -> `Nil 1383 | "Cons", Some (Tdyn (Pair (_, Var), (p : a * a vlist))) -> `Cons p))) 1384;; 1385 1386(* Define Sum using object instead of record for first-class polymorphism *) 1387 1388type (_,_) ty = 1389 | Int: (int,_) ty 1390 | String: (string,_) ty 1391 | List: ('a,'e) ty -> ('a list, 'e) ty 1392 | Option: ('a,'e) ty -> ('a option, 'e) ty 1393 | Pair: (('a,'e) ty * ('b,'e) ty) -> ('a * 'b,'e) ty 1394 | Var: ('a, 'a -> 'e) ty 1395 | Rec: ('a, 'a -> 'e) ty -> ('a,'e) ty 1396 | Pop: ('a, 'e) ty -> ('a, 'b -> 'e) ty 1397 | Conv: string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty 1398 | Sum: < proj: 'a -> string * 'e ty_dyn option; 1399 cases: (string * ('e,'b) ty_case) list; 1400 inj: 'c. ('b,'c) ty_sel * 'c -> 'a > 1401 -> ('a, 'e) ty 1402 1403and 'e ty_dyn = 1404 | Tdyn : ('a,'e) ty * 'a -> 'e ty_dyn 1405 1406and (_,_) ty_sel = 1407 | Thd : ('a -> 'b, 'a) ty_sel 1408 | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel 1409 1410and (_,_) ty_case = 1411 | TCarg : ('b,'a) ty_sel * ('a,'e) ty -> ('e,'b) ty_case 1412 | TCnoarg : ('b,noarg) ty_sel -> ('e,'b) ty_case 1413;; 1414 1415let ty_abc : ([`A of int | `B of string | `C] as 'a, 'e) ty = 1416 Sum (object 1417 method proj = function 1418 `A n -> "A", Some (Tdyn (Int, n)) 1419 | `B s -> "B", Some (Tdyn (String, s)) 1420 | `C -> "C", None 1421 method cases = 1422 [ "A", TCarg (Thd, Int); "B", TCarg (Ttl Thd, String); 1423 "C", TCnoarg (Ttl (Ttl Thd)) ]; 1424 method inj : type c. 1425 (int -> string -> noarg -> unit, c) ty_sel * c -> 1426 [`A of int | `B of string | `C] = 1427 function 1428 Thd, v -> `A v 1429 | Ttl Thd, v -> `B v 1430 | Ttl (Ttl Thd), Noarg -> `C 1431 end) 1432 1433type 'a vlist = [`Nil | `Cons of 'a * 'a vlist] 1434 1435let ty_list : type a e. (a, e) ty -> (a vlist, e) ty = fun t -> 1436 let tcons = Pair (Pop t, Var) in 1437 Rec (Sum (object 1438 method proj = function 1439 `Nil -> "Nil", None 1440 | `Cons p -> "Cons", Some (Tdyn (tcons, p)) 1441 method cases = ["Nil", TCnoarg Thd; "Cons", TCarg (Ttl Thd, tcons)] 1442 method inj : type c.(noarg -> a * a vlist -> unit, c) ty_sel * c -> a vlist 1443 = function 1444 | Thd, Noarg -> `Nil 1445 | Ttl Thd, v -> `Cons v 1446 end)) 1447;; 1448 1449(* 1450type (_,_) ty_assoc = 1451 | Anil : (unit,'e) ty_assoc 1452 | Acons : string * ('a,'e) ty * ('b,'e) ty_assoc -> ('a -> 'b, 'e) ty_assoc 1453 1454and (_,_) ty_pvar = 1455 | Pnil : ('a,'e) ty_pvar 1456 | Pconst : 't * ('b,'e) ty_pvar -> ('t -> 'b, 'e) ty_pvar 1457 | Parg : 't * ('a,'e) ty * ('b,'e) ty_pvar -> ('t * 'a -> 'b, 'e) ty_pvar 1458*) 1459(* 1460 An attempt at encoding omega examples from the 2nd Central European 1461 Functional Programming School: 1462 Generic Programming in Omega, by Tim Sheard and Nathan Linger 1463 http://web.cecs.pdx.edu/~sheard/ 1464*) 1465 1466(* Basic types *) 1467 1468type ('a,'b) sum = Inl of 'a | Inr of 'b 1469 1470type zero = Zero 1471type 'a succ = Succ of 'a 1472type _ nat = 1473 | NZ : zero nat 1474 | NS : 'a nat -> 'a succ nat 1475;; 1476 1477(* 2: A simple example *) 1478 1479type (_,_) seq = 1480 | Snil : ('a,zero) seq 1481 | Scons : 'a * ('a,'n) seq -> ('a, 'n succ) seq 1482;; 1483 1484let l1 = Scons (3, Scons (5, Snil)) ;; 1485 1486(* We do not have type level functions, so we need to use witnesses. *) 1487(* We copy here the definitions from section 3.9 *) 1488(* Note the addition of the ['a nat] argument to PlusZ, since we do not 1489 have kinds *) 1490type (_,_,_) plus = 1491 | PlusZ : 'a nat -> (zero, 'a, 'a) plus 1492 | PlusS : ('a,'b,'c) plus -> ('a succ, 'b, 'c succ) plus 1493;; 1494 1495let rec length : type a n. (a,n) seq -> n nat = function 1496 | Snil -> NZ 1497 | Scons (_, s) -> NS (length s) 1498;; 1499 1500(* app returns the catenated lists with a witness proving that 1501 the size is the sum of its two inputs *) 1502type (_,_,_) app = App : ('a,'p) seq * ('n,'m,'p) plus -> ('a,'n,'m) app 1503 1504let rec app : type a n m. (a,n) seq -> (a,m) seq -> (a,n,m) app = 1505 fun xs ys -> 1506 match xs with 1507 | Snil -> App (ys, PlusZ (length ys)) 1508 | Scons (x, xs') -> 1509 let App (xs'', pl) = app xs' ys in 1510 App (Scons (x, xs''), PlusS pl) 1511;; 1512 1513(* 3.1 Feature: kinds *) 1514 1515(* We do not have kinds, but we can encode them as predicates *) 1516 1517type tp = TP 1518type nd = ND 1519type ('a,'b) fk = FK 1520type _ shape = 1521 | Tp : tp shape 1522 | Nd : nd shape 1523 | Fk : 'a shape * 'b shape -> ('a,'b) fk shape 1524;; 1525type tt = TT 1526type ff = FF 1527type _ boolean = 1528 | BT : tt boolean 1529 | BF : ff boolean 1530;; 1531 1532(* 3.3 Feature : GADTs *) 1533 1534type (_,_) path = 1535 | Pnone : 'a -> (tp,'a) path 1536 | Phere : (nd,'a) path 1537 | Pleft : ('x,'a) path -> (('x,'y) fk, 'a) path 1538 | Pright : ('y,'a) path -> (('x,'y) fk, 'a) path 1539;; 1540type (_,_) tree = 1541 | Ttip : (tp,'a) tree 1542 | Tnode : 'a -> (nd,'a) tree 1543 | Tfork : ('x,'a) tree * ('y,'a) tree -> (('x,'y)fk, 'a) tree 1544;; 1545let tree1 = Tfork (Tfork (Ttip, Tnode 4), Tfork (Tnode 4, Tnode 3)) 1546;; 1547let rec find : type sh. 1548 ('a -> 'a -> bool) -> 'a -> (sh,'a) tree -> (sh,'a) path list 1549 = fun eq n t -> 1550 match t with 1551 | Ttip -> [] 1552 | Tnode m -> 1553 if eq n m then [Phere] else [] 1554 | Tfork (x, y) -> 1555 List.map (fun x -> Pleft x) (find eq n x) @ 1556 List.map (fun x -> Pright x) (find eq n y) 1557;; 1558let rec extract : type sh. (sh,'a) path -> (sh,'a) tree -> 'a = fun p t -> 1559 match (p, t) with 1560 | Pnone x, Ttip -> x 1561 | Phere, Tnode y -> y 1562 | Pleft p, Tfork(l,_) -> extract p l 1563 | Pright p, Tfork(_,r) -> extract p r 1564;; 1565 1566(* 3.4 Pattern : Witness *) 1567 1568type (_,_) le = 1569 | LeZ : 'a nat -> (zero, 'a) le 1570 | LeS : ('n, 'm) le -> ('n succ, 'm succ) le 1571;; 1572type _ even = 1573 | EvenZ : zero even 1574 | EvenSS : 'n even -> 'n succ succ even 1575;; 1576type one = zero succ 1577type two = one succ 1578type three = two succ 1579type four = three succ 1580;; 1581let even0 : zero even = EvenZ 1582let even2 : two even = EvenSS EvenZ 1583let even4 : four even = EvenSS (EvenSS EvenZ) 1584;; 1585let p1 : (two, one, three) plus = PlusS (PlusS (PlusZ (NS NZ))) 1586;; 1587let rec summandLessThanSum : type a b c. (a,b,c) plus -> (a,c) le = fun p -> 1588 match p with 1589 | PlusZ n -> LeZ n 1590 | PlusS p' -> LeS (summandLessThanSum p') 1591;; 1592 1593(* 3.8 Pattern: Leibniz Equality *) 1594 1595type (_,_) equal = Eq : ('a,'a) equal 1596 1597let convert : type a b. (a,b) equal -> a -> b = fun Eq x -> x 1598 1599let rec sameNat : type a b. a nat -> b nat -> (a,b) equal option = fun a b -> 1600 match a, b with 1601 | NZ, NZ -> Some Eq 1602 | NS a', NS b' -> 1603 begin match sameNat a' b' with 1604 | Some Eq -> Some Eq 1605 | None -> None 1606 end 1607 | _ -> None 1608;; 1609 1610(* Extra: associativity of addition *) 1611 1612let rec plus_func : type a b m n. 1613 (a,b,m) plus -> (a,b,n) plus -> (m,n) equal = 1614 fun p1 p2 -> 1615 match p1, p2 with 1616 | PlusZ _, PlusZ _ -> Eq 1617 | PlusS p1', PlusS p2' -> 1618 let Eq = plus_func p1' p2' in Eq 1619 1620let rec plus_assoc : type a b c ab bc m n. 1621 (a,b,ab) plus -> (ab,c,m) plus -> 1622 (b,c,bc) plus -> (a,bc,n) plus -> (m,n) equal = fun p1 p2 p3 p4 -> 1623 match p1, p4 with 1624 | PlusZ b, PlusZ bc -> 1625 let Eq = plus_func p2 p3 in Eq 1626 | PlusS p1', PlusS p4' -> 1627 let PlusS p2' = p2 in 1628 let Eq = plus_assoc p1' p2' p3 p4' in Eq 1629;; 1630 1631(* 3.9 Computing Programs and Properties Simultaneously *) 1632 1633(* Plus and app1 are moved to section 2 *) 1634 1635let smaller : type a b. (a succ, b succ) le -> (a,b) le = 1636 function LeS x -> x ;; 1637 1638type (_,_) diff = Diff : 'c nat * ('a,'c,'b) plus -> ('a,'b) diff ;; 1639 1640(* 1641let rec diff : type a b. (a,b) le -> a nat -> b nat -> (a,b) diff = 1642 fun le a b -> 1643 match a, b, le with 1644 | NZ, m, _ -> Diff (m, PlusZ m) 1645 | NS x, NZ, _ -> assert false 1646 | NS x, NS y, q -> 1647 match diff (smaller q) x y with Diff (m, p) -> Diff (m, PlusS p) 1648;; 1649*) 1650 1651let rec diff : type a b. (a,b) le -> a nat -> b nat -> (a,b) diff = 1652 fun le a b -> 1653 match le, a, b with 1654 | LeZ _, _, m -> Diff (m, PlusZ m) 1655 | LeS q, NS x, NS y -> 1656 match diff q x y with Diff (m, p) -> Diff (m, PlusS p) 1657;; 1658 1659let rec diff : type a b. (a,b) le -> a nat -> b nat -> (a,b) diff = 1660 fun le a b -> 1661 match a, b,le with (* warning *) 1662 | NZ, m, LeZ _ -> Diff (m, PlusZ m) 1663 | NS x, NS y, LeS q -> 1664 (match diff q x y with Diff (m, p) -> Diff (m, PlusS p)) 1665 | _ -> . 1666;; 1667 1668let rec diff : type a b. (a,b) le -> b nat -> (a,b) diff = 1669 fun le b -> 1670 match b,le with 1671 | m, LeZ _ -> Diff (m, PlusZ m) 1672 | NS y, LeS q -> 1673 match diff q y with Diff (m, p) -> Diff (m, PlusS p) 1674;; 1675 1676type (_,_) filter = Filter : ('m,'n) le * ('a,'m) seq -> ('a,'n) filter 1677 1678let rec leS' : type m n. (m,n) le -> (m,n succ) le = function 1679 | LeZ n -> LeZ (NS n) 1680 | LeS le -> LeS (leS' le) 1681;; 1682 1683let rec filter : type a n. (a -> bool) -> (a,n) seq -> (a,n) filter = 1684 fun f s -> 1685 match s with 1686 | Snil -> Filter (LeZ NZ, Snil) 1687 | Scons (a,l) -> 1688 match filter f l with Filter (le, l') -> 1689 if f a then Filter (LeS le, Scons (a, l')) 1690 else Filter (leS' le, l') 1691;; 1692 1693(* 4.1 AVL trees *) 1694 1695type (_,_,_) balance = 1696 | Less : ('h, 'h succ, 'h succ) balance 1697 | Same : ('h, 'h, 'h) balance 1698 | More : ('h succ, 'h, 'h succ) balance 1699 1700type _ avl = 1701 | Leaf : zero avl 1702 | Node : 1703 ('hL, 'hR, 'hMax) balance * 'hL avl * int * 'hR avl -> 'hMax succ avl 1704 1705type avl' = Avl : 'h avl -> avl' 1706;; 1707 1708let empty = Avl Leaf 1709 1710let rec elem : type h. int -> h avl -> bool = fun x t -> 1711 match t with 1712 | Leaf -> false 1713 | Node (_, l, y, r) -> 1714 x = y || if x < y then elem x l else elem x r 1715;; 1716 1717let rec rotr : type n. (n succ succ) avl -> int -> n avl -> 1718 ((n succ succ) avl, (n succ succ succ) avl) sum = 1719 fun tL y tR -> 1720 match tL with 1721 | Node (Same, a, x, b) -> Inr (Node (Less, a, x, Node (More, b, y, tR))) 1722 | Node (More, a, x, b) -> Inl (Node (Same, a, x, Node (Same, b, y, tR))) 1723 | Node (Less, a, x, Node (Same, b, z, c)) -> 1724 Inl (Node (Same, Node (Same, a, x, b), z, Node (Same, c, y, tR))) 1725 | Node (Less, a, x, Node (Less, b, z, c)) -> 1726 Inl (Node (Same, Node (More, a, x, b), z, Node (Same, c, y, tR))) 1727 | Node (Less, a, x, Node (More, b, z, c)) -> 1728 Inl (Node (Same, Node (Same, a, x, b), z, Node (Less, c, y, tR))) 1729;; 1730let rec rotl : type n. n avl -> int -> (n succ succ) avl -> 1731 ((n succ succ) avl, (n succ succ succ) avl) sum = 1732 fun tL u tR -> 1733 match tR with 1734 | Node (Same, a, x, b) -> Inr (Node (More, Node (Less, tL, u, a), x, b)) 1735 | Node (Less, a, x, b) -> Inl (Node (Same, Node (Same, tL, u, a), x, b)) 1736 | Node (More, Node (Same, a, x, b), y, c) -> 1737 Inl (Node (Same, Node (Same, tL, u, a), x, Node (Same, b, y, c))) 1738 | Node (More, Node (Less, a, x, b), y, c) -> 1739 Inl (Node (Same, Node (More, tL, u, a), x, Node (Same, b, y, c))) 1740 | Node (More, Node (More, a, x, b), y, c) -> 1741 Inl (Node (Same, Node (Same, tL, u, a), x, Node (Less, b, y, c))) 1742;; 1743let rec ins : type n. int -> n avl -> (n avl, (n succ) avl) sum = 1744 fun x t -> 1745 match t with 1746 | Leaf -> Inr (Node (Same, Leaf, x, Leaf)) 1747 | Node (bal, a, y, b) -> 1748 if x = y then Inl t else 1749 if x < y then begin 1750 match ins x a with 1751 | Inl a -> Inl (Node (bal, a, y, b)) 1752 | Inr a -> 1753 match bal with 1754 | Less -> Inl (Node (Same, a, y, b)) 1755 | Same -> Inr (Node (More, a, y, b)) 1756 | More -> rotr a y b 1757 end else begin 1758 match ins x b with 1759 | Inl b -> Inl (Node (bal, a, y, b) : n avl) 1760 | Inr b -> 1761 match bal with 1762 | More -> Inl (Node (Same, a, y, b) : n avl) 1763 | Same -> Inr (Node (Less, a, y, b) : n succ avl) 1764 | Less -> rotl a y b 1765 end 1766;; 1767 1768let insert x (Avl t) = 1769 match ins x t with 1770 | Inl t -> Avl t 1771 | Inr t -> Avl t 1772;; 1773 1774let rec del_min : type n. (n succ) avl -> int * (n avl, (n succ) avl) sum = 1775 function 1776 | Node (Less, Leaf, x, r) -> (x, Inl r) 1777 | Node (Same, Leaf, x, r) -> (x, Inl r) 1778 | Node (bal, (Node _ as l) , x, r) -> 1779 match del_min l with 1780 | y, Inr l -> (y, Inr (Node (bal, l, x, r))) 1781 | y, Inl l -> 1782 (y, match bal with 1783 | Same -> Inr (Node (Less, l, x, r)) 1784 | More -> Inl (Node (Same, l, x, r)) 1785 | Less -> rotl l x r) 1786 1787type _ avl_del = 1788 | Dsame : 'n avl -> 'n avl_del 1789 | Ddecr : ('m succ, 'n) equal * 'm avl -> 'n avl_del 1790 1791let rec del : type n. int -> n avl -> n avl_del = fun y t -> 1792 match t with 1793 | Leaf -> Dsame Leaf 1794 | Node (bal, l, x, r) -> 1795 if x = y then begin 1796 match r with 1797 | Leaf -> 1798 begin match bal with 1799 | Same -> Ddecr (Eq, l) 1800 | More -> Ddecr (Eq, l) 1801 end 1802 | Node _ -> 1803 begin match bal, del_min r with 1804 | _, (z, Inr r) -> Dsame (Node (bal, l, z, r)) 1805 | Same, (z, Inl r) -> Dsame (Node (More, l, z, r)) 1806 | Less, (z, Inl r) -> Ddecr (Eq, Node (Same, l, z, r)) 1807 | More, (z, Inl r) -> 1808 match rotr l z r with 1809 | Inl t -> Ddecr (Eq, t) 1810 | Inr t -> Dsame t 1811 end 1812 end else if y < x then begin 1813 match del y l with 1814 | Dsame l -> Dsame (Node (bal, l, x, r)) 1815 | Ddecr(Eq,l) -> 1816 begin match bal with 1817 | Same -> Dsame (Node (Less, l, x, r)) 1818 | More -> Ddecr (Eq, Node (Same, l, x, r)) 1819 | Less -> 1820 match rotl l x r with 1821 | Inl t -> Ddecr (Eq, t) 1822 | Inr t -> Dsame t 1823 end 1824 end else begin 1825 match del y r with 1826 | Dsame r -> Dsame (Node (bal, l, x, r)) 1827 | Ddecr(Eq,r) -> 1828 begin match bal with 1829 | Same -> Dsame (Node (More, l, x, r)) 1830 | Less -> Ddecr (Eq, Node (Same, l, x, r)) 1831 | More -> 1832 match rotr l x r with 1833 | Inl t -> Ddecr (Eq, t) 1834 | Inr t -> Dsame t 1835 end 1836 end 1837;; 1838 1839let delete x (Avl t) = 1840 match del x t with 1841 | Dsame t -> Avl t 1842 | Ddecr (_, t) -> Avl t 1843;; 1844 1845 1846(* Exercise 22: Red-black trees *) 1847 1848type red = RED 1849type black = BLACK 1850type (_,_) sub_tree = 1851 | Bleaf : (black, zero) sub_tree 1852 | Rnode : 1853 (black, 'n) sub_tree * int * (black, 'n) sub_tree -> (red, 'n) sub_tree 1854 | Bnode : 1855 ('cL, 'n) sub_tree * int * ('cR, 'n) sub_tree -> (black, 'n succ) sub_tree 1856 1857type rb_tree = Root : (black, 'n) sub_tree -> rb_tree 1858;; 1859 1860type dir = LeftD | RightD 1861 1862type (_,_) ctxt = 1863 | CNil : (black,'n) ctxt 1864 | CRed : int * dir * (black,'n) sub_tree * (red,'n) ctxt -> (black,'n) ctxt 1865 | CBlk : int * dir * ('c1,'n) sub_tree * (black, 'n succ) ctxt -> ('c,'n) ctxt 1866;; 1867 1868let blacken = function 1869 Rnode (l, e, r) -> Bnode (l, e, r) 1870 1871type _ crep = 1872 | Red : red crep 1873 | Black : black crep 1874 1875let color : type c n. (c,n) sub_tree -> c crep = function 1876 | Bleaf -> Black 1877 | Rnode _ -> Red 1878 | Bnode _ -> Black 1879;; 1880 1881let rec fill : type c n. (c,n) ctxt -> (c,n) sub_tree -> rb_tree = 1882 fun ct t -> 1883 match ct with 1884 | CNil -> Root t 1885 | CRed (e, LeftD, uncle, c) -> fill c (Rnode (uncle, e, t)) 1886 | CRed (e, RightD, uncle, c) -> fill c (Rnode (t, e, uncle)) 1887 | CBlk (e, LeftD, uncle, c) -> fill c (Bnode (uncle, e, t)) 1888 | CBlk (e, RightD, uncle, c) -> fill c (Bnode (t, e, uncle)) 1889;; 1890let recolor d1 pE sib d2 gE uncle t = 1891 match d1, d2 with 1892 | LeftD, RightD -> Rnode (Bnode (sib, pE, t), gE, uncle) 1893 | RightD, RightD -> Rnode (Bnode (t, pE, sib), gE, uncle) 1894 | LeftD, LeftD -> Rnode (uncle, gE, Bnode (sib, pE, t)) 1895 | RightD, LeftD -> Rnode (uncle, gE, Bnode (t, pE, sib)) 1896;; 1897let rotate d1 pE sib d2 gE uncle (Rnode (x, e, y)) = 1898 match d1, d2 with 1899 | RightD, RightD -> Bnode (Rnode (x,e,y), pE, Rnode (sib, gE, uncle)) 1900 | LeftD, RightD -> Bnode (Rnode (sib, pE, x), e, Rnode (y, gE, uncle)) 1901 | LeftD, LeftD -> Bnode (Rnode (uncle, gE, sib), pE, Rnode (x,e,y)) 1902 | RightD, LeftD -> Bnode (Rnode (uncle, gE, x), e, Rnode (y, pE, sib)) 1903;; 1904let rec repair : type c n. (red,n) sub_tree -> (c,n) ctxt -> rb_tree = 1905 fun t ct -> 1906 match ct with 1907 | CNil -> Root (blacken t) 1908 | CBlk (e, LeftD, sib, c) -> fill c (Bnode (sib, e, t)) 1909 | CBlk (e, RightD, sib, c) -> fill c (Bnode (t, e, sib)) 1910 | CRed (e, dir, sib, CBlk (e', dir', uncle, ct)) -> 1911 match color uncle with 1912 | Red -> repair (recolor dir e sib dir' e' (blacken uncle) t) ct 1913 | Black -> fill ct (rotate dir e sib dir' e' uncle t) 1914;; 1915let rec ins : type c n. int -> (c,n) sub_tree -> (c,n) ctxt -> rb_tree = 1916 fun e t ct -> 1917 match t with 1918 | Rnode (l, e', r) -> 1919 if e < e' then ins e l (CRed (e', RightD, r, ct)) 1920 else ins e r (CRed (e', LeftD, l, ct)) 1921 | Bnode (l, e', r) -> 1922 if e < e' then ins e l (CBlk (e', RightD, r, ct)) 1923 else ins e r (CBlk (e', LeftD, l, ct)) 1924 | Bleaf -> repair (Rnode (Bleaf, e, Bleaf)) ct 1925;; 1926let insert e (Root t) = ins e t CNil 1927;; 1928 1929(* 5.7 typed object languages using GADTs *) 1930 1931type _ term = 1932 | Const : int -> int term 1933 | Add : (int * int -> int) term 1934 | LT : (int * int -> bool) term 1935 | Ap : ('a -> 'b) term * 'a term -> 'b term 1936 | Pair : 'a term * 'b term -> ('a * 'b) term 1937 1938let ex1 = Ap (Add, Pair (Const 3, Const 5)) 1939let ex2 = Pair (ex1, Const 1) 1940 1941let rec eval_term : type a. a term -> a = function 1942 | Const x -> x 1943 | Add -> fun (x,y) -> x+y 1944 | LT -> fun (x,y) -> x<y 1945 | Ap(f,x) -> eval_term f (eval_term x) 1946 | Pair(x,y) -> (eval_term x, eval_term y) 1947 1948type _ rep = 1949 | Rint : int rep 1950 | Rbool : bool rep 1951 | Rpair : 'a rep * 'b rep -> ('a * 'b) rep 1952 | Rfun : 'a rep * 'b rep -> ('a -> 'b) rep 1953 1954type (_,_) equal = Eq : ('a,'a) equal 1955 1956let rec rep_equal : type a b. a rep -> b rep -> (a, b) equal option = 1957 fun ra rb -> 1958 match ra, rb with 1959 | Rint, Rint -> Some Eq 1960 | Rbool, Rbool -> Some Eq 1961 | Rpair (a1, a2), Rpair (b1, b2) -> 1962 begin match rep_equal a1 b1 with 1963 | None -> None 1964 | Some Eq -> match rep_equal a2 b2 with 1965 | None -> None 1966 | Some Eq -> Some Eq 1967 end 1968 | Rfun (a1, a2), Rfun (b1, b2) -> 1969 begin match rep_equal a1 b1 with 1970 | None -> None 1971 | Some Eq -> match rep_equal a2 b2 with 1972 | None -> None 1973 | Some Eq -> Some Eq 1974 end 1975 | _ -> None 1976;; 1977 1978type assoc = Assoc : string * 'a rep * 'a -> assoc 1979 1980let rec assoc : type a. string -> a rep -> assoc list -> a = 1981 fun x r -> function 1982 | [] -> raise Not_found 1983 | Assoc (x', r', v) :: env -> 1984 if x = x' then 1985 match rep_equal r r' with 1986 | None -> failwith ("Wrong type for " ^ x) 1987 | Some Eq -> v 1988 else assoc x r env 1989 1990type _ term = 1991 | Var : string * 'a rep -> 'a term 1992 | Abs : string * 'a rep * 'b term -> ('a -> 'b) term 1993 | Const : int -> int term 1994 | Add : (int * int -> int) term 1995 | LT : (int * int -> bool) term 1996 | Ap : ('a -> 'b) term * 'a term -> 'b term 1997 | Pair : 'a term * 'b term -> ('a * 'b) term 1998 1999let rec eval_term : type a. assoc list -> a term -> a = 2000 fun env -> function 2001 | Var (x, r) -> assoc x r env 2002 | Abs (x, r, e) -> fun v -> eval_term (Assoc (x, r, v) :: env) e 2003 | Const x -> x 2004 | Add -> fun (x,y) -> x+y 2005 | LT -> fun (x,y) -> x<y 2006 | Ap(f,x) -> eval_term env f (eval_term env x) 2007 | Pair(x,y) -> (eval_term env x, eval_term env y) 2008;; 2009 2010let ex3 = Abs ("x", Rint, Ap (Add, Pair (Var("x",Rint), Var("x",Rint)))) 2011let ex4 = Ap (ex3, Const 3) 2012 2013let v4 = eval_term [] ex4 2014;; 2015 2016(* 5.9/5.10 Language with binding *) 2017 2018type rnil = RNIL 2019type ('a,'b,'c) rcons = RCons of 'a * 'b * 'c 2020 2021type _ is_row = 2022 | Rnil : rnil is_row 2023 | Rcons : 'c is_row -> ('a,'b,'c) rcons is_row 2024 2025type (_,_) lam = 2026 | Const : int -> ('e, int) lam 2027 | Var : 'a -> (('a,'t,'e) rcons, 't) lam 2028 | Shift : ('e,'t) lam -> (('a,'q,'e) rcons, 't) lam 2029 | Abs : 'a * (('a,'s,'e) rcons, 't) lam -> ('e, 's -> 't) lam 2030 | App : ('e, 's -> 't) lam * ('e, 's) lam -> ('e, 't) lam 2031 2032type x = X 2033type y = Y 2034 2035let ex1 = App (Var X, Shift (Var Y)) 2036let ex2 = Abs (X, Abs (Y, App (Shift (Var X), Var Y))) 2037;; 2038 2039type _ env = 2040 | Enil : rnil env 2041 | Econs : 'a * 't * 'e env -> ('a, 't, 'e) rcons env 2042 2043let rec eval_lam : type e t. e env -> (e, t) lam -> t = 2044 fun env m -> 2045 match env, m with 2046 | _, Const n -> n 2047 | Econs (_, v, r), Var _ -> v 2048 | Econs (_, _, r), Shift e -> eval_lam r e 2049 | _, Abs (n, body) -> fun x -> eval_lam (Econs (n, x, env)) body 2050 | _, App (f, x) -> eval_lam env f (eval_lam env x) 2051;; 2052 2053type add = Add 2054type suc = Suc 2055 2056let env0 = Econs (Zero, 0, Econs (Suc, succ, Econs (Add, (+), Enil))) 2057 2058let _0 : (_, int) lam = Var Zero 2059let suc x = App (Shift (Var Suc : (_, int -> int) lam), x) 2060let _1 = suc _0 2061let _2 = suc _1 2062let _3 = suc _2 2063let add = Shift (Shift (Var Add : (_, int -> int -> int) lam)) 2064 2065let double = Abs (X, App (App (Shift add, Var X), Var X)) 2066let ex3 = App (double, _3) 2067;; 2068 2069let v3 = eval_lam env0 ex3 2070;; 2071 2072(* 5.13: Constructing typing derivations at runtime *) 2073 2074(* Modified slightly to use the language of 5.10, since this is more fun. 2075 Of course this works also with the language of 5.12. *) 2076 2077type _ rep = 2078 | I : int rep 2079 | Ar : 'a rep * 'b rep -> ('a -> 'b) rep 2080 2081let rec compare : type a b. a rep -> b rep -> (string, (a,b) equal) sum = 2082 fun a b -> 2083 match a, b with 2084 | I, I -> Inr Eq 2085 | Ar(x,y), Ar(s,t) -> 2086 begin match compare x s with 2087 | Inl _ as e -> e 2088 | Inr Eq -> match compare y t with 2089 | Inl _ as e -> e 2090 | Inr Eq as e -> e 2091 end 2092 | I, Ar _ -> Inl "I <> Ar _" 2093 | Ar _, I -> Inl "Ar _ <> I" 2094;; 2095 2096type term = 2097 | C of int 2098 | Ab : string * 'a rep * term -> term 2099 | Ap of term * term 2100 | V of string 2101 2102type _ ctx = 2103 | Cnil : rnil ctx 2104 | Ccons : 't * string * 'x rep * 'e ctx -> ('t,'x,'e) rcons ctx 2105;; 2106 2107type _ checked = 2108 | Cerror of string 2109 | Cok : ('e,'t) lam * 't rep -> 'e checked 2110 2111let rec lookup : type e. string -> e ctx -> e checked = 2112 fun name ctx -> 2113 match ctx with 2114 | Cnil -> Cerror ("Name not found: " ^ name) 2115 | Ccons (l,s,t,rs) -> 2116 if s = name then Cok (Var l,t) else 2117 match lookup name rs with 2118 | Cerror m -> Cerror m 2119 | Cok (v, t) -> Cok (Shift v, t) 2120;; 2121 2122let rec tc : type n e. n nat -> e ctx -> term -> e checked = 2123 fun n ctx t -> 2124 match t with 2125 | V s -> lookup s ctx 2126 | Ap(f,x) -> 2127 begin match tc n ctx f with 2128 | Cerror _ as e -> e 2129 | Cok (f', ft) -> match tc n ctx x with 2130 | Cerror _ as e -> e 2131 | Cok (x', xt) -> 2132 match ft with 2133 | Ar (a, b) -> 2134 begin match compare a xt with 2135 | Inl s -> Cerror s 2136 | Inr Eq -> Cok (App (f',x'), b) 2137 end 2138 | _ -> Cerror "Non fun in Ap" 2139 end 2140 | Ab(s,t,body) -> 2141 begin match tc (NS n) (Ccons (n, s, t, ctx)) body with 2142 | Cerror _ as e -> e 2143 | Cok (body', et) -> Cok (Abs (n, body'), Ar (t, et)) 2144 end 2145 | C m -> Cok (Const m, I) 2146;; 2147 2148let ctx0 = 2149 Ccons (Zero, "0", I, 2150 Ccons (Suc, "S", Ar(I,I), 2151 Ccons (Add, "+", Ar(I,Ar(I,I)), Cnil))) 2152 2153let ex1 = Ab ("x", I, Ap(Ap(V"+",V"x"),V"x"));; 2154let c1 = tc NZ ctx0 ex1;; 2155let ex2 = Ap (ex1, C 3);; 2156let c2 = tc NZ ctx0 ex2;; 2157 2158let eval_checked env = function 2159 | Cerror s -> failwith s 2160 | Cok (e, I) -> (eval_lam env e : int) 2161 | Cok _ -> failwith "Can only evaluate expressions of type I" 2162;; 2163 2164let v2 = eval_checked env0 c2 ;; 2165 2166(* 5.12 Soundness *) 2167 2168type pexp = PEXP 2169type pval = PVAL 2170type _ mode = 2171 | Pexp : pexp mode 2172 | Pval : pval mode 2173 2174type ('a,'b) tarr = TARR 2175type tint = TINT 2176 2177type (_,_) rel = 2178 | IntR : (tint, int) rel 2179 | IntTo : ('b, 's) rel -> ((tint, 'b) tarr, int -> 's) rel 2180 2181type (_,_,_) lam = 2182 | Const : ('a,'b) rel * 'b -> (pval, 'env, 'a) lam 2183 | Var : 'a -> (pval, ('a,'t,'e) rcons, 't) lam 2184 | Shift : ('m,'e,'t) lam -> ('m, ('a,'q,'e) rcons, 't) lam 2185 | Lam : 'a * ('m, ('a,'s,'e) rcons, 't) lam -> (pval, 'e, ('s,'t) tarr) lam 2186 | App : ('m1, 'e, ('s,'t) tarr) lam * ('m2, 'e, 's) lam -> (pexp, 'e, 't) lam 2187;; 2188 2189let ex1 = App (Lam (X, Var X), Const (IntR, 3)) 2190 2191let rec mode : type m e t. (m,e,t) lam -> m mode = function 2192 | Lam (v, body) -> Pval 2193 | Var v -> Pval 2194 | Const (r, v) -> Pval 2195 | Shift e -> mode e 2196 | App _ -> Pexp 2197;; 2198 2199type (_,_) sub = 2200 | Id : ('r,'r) sub 2201 | Bind : 't * ('m,'r2,'x) lam * ('r,'r2) sub -> (('t,'x,'r) rcons, 'r2) sub 2202 | Push : ('r1,'r2) sub -> (('a,'b,'r1) rcons, ('a,'b,'r2) rcons) sub 2203 2204type (_,_) lam' = Ex : ('m, 's, 't) lam -> ('s,'t) lam' 2205;; 2206 2207let rec subst : type m1 r t s. (m1,r,t) lam -> (r,s) sub -> (s,t) lam' = 2208 fun t s -> 2209 match t, s with 2210 | _, Id -> Ex t 2211 | Const(r,c), sub -> Ex (Const (r,c)) 2212 | Var v, Bind (x, e, r) -> Ex e 2213 | Var v, Push sub -> Ex (Var v) 2214 | Shift e, Bind (_, _, r) -> subst e r 2215 | Shift e, Push sub -> 2216 (match subst e sub with Ex a -> Ex (Shift a)) 2217 | App(f,x), sub -> 2218 (match subst f sub, subst x sub with Ex g, Ex y -> Ex (App (g,y))) 2219 | Lam(v,x), sub -> 2220 (match subst x (Push sub) with Ex body -> Ex (Lam (v, body))) 2221;; 2222 2223type closed = rnil 2224 2225type 'a rlam = ((pexp,closed,'a) lam, (pval,closed,'a) lam) sum ;; 2226 2227let rec rule : type a b. 2228 (pval, closed, (a,b) tarr) lam -> (pval, closed, a) lam -> b rlam = 2229 fun v1 v2 -> 2230 match v1, v2 with 2231 | Lam(x,body), v -> 2232 begin 2233 match subst body (Bind (x, v, Id)) with Ex term -> 2234 match mode term with 2235 | Pexp -> Inl term 2236 | Pval -> Inr term 2237 end 2238 | Const (IntTo b, f), Const (IntR, x) -> 2239 Inr (Const (b, f x)) 2240;; 2241let rec onestep : type m t. (m,closed,t) lam -> t rlam = function 2242 | Lam (v, body) -> Inr (Lam (v, body)) 2243 | Const (r, v) -> Inr (Const (r, v)) 2244 | App (e1, e2) -> 2245 match mode e1, mode e2 with 2246 | Pexp, _-> 2247 begin match onestep e1 with 2248 | Inl e -> Inl(App(e,e2)) 2249 | Inr v -> Inl(App(v,e2)) 2250 end 2251 | Pval, Pexp -> 2252 begin match onestep e2 with 2253 | Inl e -> Inl(App(e1,e)) 2254 | Inr v -> Inl(App(e1,v)) 2255 end 2256 | Pval, Pval -> rule e1 e2 2257;; 2258type ('env, 'a) var = 2259 | Zero : ('a * 'env, 'a) var 2260 | Succ : ('env, 'a) var -> ('b * 'env, 'a) var 2261;; 2262type ('env, 'a) typ = 2263 | Tint : ('env, int) typ 2264 | Tbool : ('env, bool) typ 2265 | Tvar : ('env, 'a) var -> ('env, 'a) typ 2266;; 2267let f : type env a. (env, a) typ -> (env, a) typ -> int = fun ta tb -> 2268 match ta, tb with 2269 | Tint, Tint -> 0 2270 | Tbool, Tbool -> 1 2271 | Tvar var, tb -> 2 2272 | _ -> . (* error *) 2273;; 2274(* let x = f Tint (Tvar Zero) ;; *) 2275type inkind = [ `Link | `Nonlink ] 2276 2277type _ inline_t = 2278 | Text: string -> [< inkind > `Nonlink ] inline_t 2279 | Bold: 'a inline_t list -> 'a inline_t 2280 | Link: string -> [< inkind > `Link ] inline_t 2281 | Mref: string * [ `Nonlink ] inline_t list -> [< inkind > `Link ] inline_t 2282;; 2283 2284let uppercase seq = 2285 let rec process: type a. a inline_t -> a inline_t = function 2286 | Text txt -> Text (String.uppercase_ascii txt) 2287 | Bold xs -> Bold (List.map process xs) 2288 | Link lnk -> Link lnk 2289 | Mref (lnk, xs) -> Mref (lnk, List.map process xs) 2290 in List.map process seq 2291;; 2292 2293type ast_t = 2294 | Ast_Text of string 2295 | Ast_Bold of ast_t list 2296 | Ast_Link of string 2297 | Ast_Mref of string * ast_t list 2298;; 2299 2300let inlineseq_from_astseq seq = 2301 let rec process_nonlink = function 2302 | Ast_Text txt -> Text txt 2303 | Ast_Bold xs -> Bold (List.map process_nonlink xs) 2304 | _ -> assert false in 2305 let rec process_any = function 2306 | Ast_Text txt -> Text txt 2307 | Ast_Bold xs -> Bold (List.map process_any xs) 2308 | Ast_Link lnk -> Link lnk 2309 | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs) 2310 in List.map process_any seq 2311;; 2312 2313(* OK *) 2314type _ linkp = 2315 | Nonlink : [ `Nonlink ] linkp 2316 | Maylink : inkind linkp 2317;; 2318let inlineseq_from_astseq seq = 2319 let rec process : type a. a linkp -> ast_t -> a inline_t = 2320 fun allow_link ast -> 2321 match (allow_link, ast) with 2322 | (Maylink, Ast_Text txt) -> Text txt 2323 | (Nonlink, Ast_Text txt) -> Text txt 2324 | (x, Ast_Bold xs) -> Bold (List.map (process x) xs) 2325 | (Maylink, Ast_Link lnk) -> Link lnk 2326 | (Nonlink, Ast_Link _) -> assert false 2327 | (Maylink, Ast_Mref (lnk, xs)) -> 2328 Mref (lnk, List.map (process Nonlink) xs) 2329 | (Nonlink, Ast_Mref _) -> assert false 2330 in List.map (process Maylink) seq 2331;; 2332 2333(* Bad *) 2334type _ linkp2 = Kind : 'a linkp -> ([< inkind ] as 'a) linkp2 2335;; 2336let inlineseq_from_astseq seq = 2337let rec process : type a. a linkp2 -> ast_t -> a inline_t = 2338 fun allow_link ast -> 2339 match (allow_link, ast) with 2340 | (Kind _, Ast_Text txt) -> Text txt 2341 | (x, Ast_Bold xs) -> Bold (List.map (process x) xs) 2342 | (Kind Maylink, Ast_Link lnk) -> Link lnk 2343 | (Kind Nonlink, Ast_Link _) -> assert false 2344 | (Kind Maylink, Ast_Mref (lnk, xs)) -> 2345 Mref (lnk, List.map (process (Kind Nonlink)) xs) 2346 | (Kind Nonlink, Ast_Mref _) -> assert false 2347 in List.map (process (Kind Maylink)) seq 2348;; 2349module Add (T : sig type two end) = 2350struct 2351 type _ t = 2352 | One : [`One] t 2353 | Two : T.two t 2354 2355 let add (type a) : a t * a t -> string = function 2356 | One, One -> "two" 2357 | Two, Two -> "four" 2358end;; 2359module B : sig 2360 type (_, _) t = Eq: ('a, 'a) t 2361 val f: 'a -> 'b -> ('a, 'b) t 2362end 2363= 2364struct 2365 type (_, _) t = Eq: ('a, 'a) t 2366 let f t1 t2 = Obj.magic Eq 2367end;; 2368 2369let of_type: type a. a -> a = fun x -> 2370 match B.f x 4 with 2371 | Eq -> 5 2372;; 2373type _ constant = 2374 | Int: int -> int constant 2375 | Bool: bool -> bool constant 2376 2377type (_, _, _) binop = 2378 | Eq: ('a, 'a, bool) binop 2379 | Leq: ('a, 'a, bool) binop 2380 | Add: (int, int, int) binop 2381 2382let eval (type a) (type b) (type c) (bop:(a,b,c) binop) (x:a constant) 2383 (y:b constant) : c constant = 2384 match bop, x, y with 2385 | Eq, Bool x, Bool y -> Bool (if x then y else not y) 2386 | Leq, Int x, Int y -> Bool (x <= y) 2387 | Leq, Bool x, Bool y -> Bool (x <= y) 2388 | Add, Int x, Int y -> Int (x + y) 2389 2390let _ = eval Eq (Int 2) (Int 3) 2391type tag = [`TagA | `TagB | `TagC];; 2392 2393type 'a poly = 2394 AandBTags : [< `TagA of int | `TagB ] poly 2395 | ATag : [< `TagA of int] poly 2396(* constraint 'a = [< `TagA of int | `TagB] *) 2397;; 2398 2399let intA = function `TagA i -> i 2400let intB = function `TagB -> 4 2401;; 2402 2403let intAorB = function 2404 `TagA i -> i 2405 | `TagB -> 4 2406;; 2407 2408type _ wrapPoly = 2409 WrapPoly : 'a poly -> ([< `TagA of int | `TagB] as 'a) wrapPoly 2410;; 2411 2412let example6 : type a. a wrapPoly -> (a -> int) = 2413 fun w -> 2414 match w with 2415 | WrapPoly ATag -> intA 2416 | WrapPoly _ -> intA (* This should not be allowed *) 2417;; 2418 2419let _ = example6 (WrapPoly AandBTags) `TagB (* This causes a seg fault *) 2420;; 2421module F(S : sig type 'a t end) = struct 2422 type _ ab = 2423 A : int S.t ab 2424 | B : float S.t ab 2425 2426 let f : int S.t ab -> float S.t ab -> string = 2427 fun (l : int S.t ab) (r : float S.t ab) -> match l, r with 2428 | A, B -> "f A B" 2429end;; 2430 2431module F(S : sig type 'a t end) = struct 2432 type a = int * int 2433 type b = int -> int 2434 2435 type _ ab = 2436 A : a S.t ab 2437 | B : b S.t ab 2438 2439 let f : a S.t ab -> b S.t ab -> string = 2440 fun l r -> match l, r with 2441 | A, B -> "f A B" 2442end;; 2443type (_, _) t = 2444 Any : ('a, 'b) t 2445 | Eq : ('a, 'a) t 2446;; 2447 2448module M : 2449sig 2450 type s = private [> `A] 2451 val eq : (s, [`A | `B]) t 2452end = 2453struct 2454 type s = [`A | `B] 2455 let eq = Eq 2456end;; 2457 2458let f : (M.s, [`A | `B]) t -> string = function 2459 | Any -> "Any" 2460;; 2461 2462let () = print_endline (f M.eq) ;; 2463 2464module N : 2465sig 2466 type s = private < a : int; .. > 2467 val eq : (s, <a : int; b : bool>) t 2468end = 2469struct 2470 type s = <a : int; b : bool> 2471 let eq = Eq 2472end 2473;; 2474 2475let f : (N.s, <a : int; b : bool>) t -> string = function 2476 | Any -> "Any" 2477;; 2478type (_, _) comp = 2479 | Eq : ('a, 'a) comp 2480 | Diff : ('a, 'b) comp 2481;; 2482 2483module U = struct type t = T end;; 2484 2485module M : sig 2486 type t = T 2487 val comp : (U.t, t) comp 2488end = struct 2489 include U 2490 let comp = Eq 2491end;; 2492 2493match M.comp with | Diff -> false;; 2494 2495module U = struct type t = {x : int} end;; 2496 2497module M : sig 2498 type t = {x : int} 2499 val comp : (U.t, t) comp 2500end = struct 2501 include U 2502 let comp = Eq 2503end;; 2504 2505match M.comp with | Diff -> false;; 2506type 'a t = T of 'a 2507type 'a s = S of 'a 2508 2509type (_, _) eq = Refl : ('a, 'a) eq;; 2510 2511let f : (int s, int t) eq -> unit = function Refl -> ();; 2512 2513module M (S : sig type 'a t = T of 'a type 'a s = T of 'a end) = 2514struct let f : ('a S.s, 'a S.t) eq -> unit = function Refl -> () end;; 2515type _ nat = 2516 Zero : [`Zero] nat 2517 | Succ : 'a nat -> [`Succ of 'a] nat;; 2518type 'a pre_nat = [`Zero | `Succ of 'a];; 2519type aux = 2520 | Aux : [`Succ of [<[<[<[`Zero] pre_nat] pre_nat] pre_nat]] nat -> aux;; 2521 2522let f (Aux x) = 2523 match x with 2524 | Succ Zero -> "1" 2525 | Succ (Succ Zero) -> "2" 2526 | Succ (Succ (Succ Zero)) -> "3" 2527 | Succ (Succ (Succ (Succ Zero))) -> "4" 2528 | _ -> . (* error *) 2529;; 2530type _ t = C : ((('a -> 'o) -> 'o) -> ('b -> 'o) -> 'o) t 2531let f : type a o. ((a -> o) -> o) t -> (a -> o) -> o = 2532 fun C k -> k (fun x -> x);; 2533type (_, _) t = 2534 A : ('a, 'a) t 2535| B : string -> ('a, 'b) t 2536;; 2537 2538module M (A : sig module type T end) (B : sig module type T end) = 2539struct 2540 let f : ((module A.T), (module B.T)) t -> string = function 2541 | B s -> s 2542end;; 2543 2544module A = struct module type T = sig end end;; 2545 2546module N = M(A)(A);; 2547 2548let x = N.f A;; 2549type 'a visit_action 2550 2551type insert 2552 2553type 'a local_visit_action 2554 2555type ('a, 'result, 'visit_action) context = 2556 | Local : ('a, ('a * insert) as 'result, 'a local_visit_action) context 2557 | Global : ('a, 'a, 'a visit_action) context 2558;; 2559 2560let vexpr (type visit_action) 2561 : (_, _, visit_action) context -> _ -> visit_action = 2562 function 2563 | Local -> fun _ -> raise Exit 2564 | Global -> fun _ -> raise Exit 2565;; 2566 2567let vexpr (type visit_action) 2568 : ('a, 'result, visit_action) context -> 'a -> visit_action = 2569 function 2570 | Local -> fun _ -> raise Exit 2571 | Global -> fun _ -> raise Exit 2572;; 2573 2574let vexpr (type result) (type visit_action) 2575 : (unit, result, visit_action) context -> unit -> visit_action = 2576 function 2577 | Local -> fun _ -> raise Exit 2578 | Global -> fun _ -> raise Exit 2579;; 2580module A = struct 2581 type nil = Cstr 2582 end 2583open A 2584;; 2585 2586type _ s = 2587 | Nil : nil s 2588 | Cons : 't s -> ('h -> 't) s 2589 2590type ('stack, 'typ) var = 2591 | Head : (('typ -> _) s, 'typ) var 2592 | Tail : ('tail s, 'typ) var -> ((_ -> 'tail) s, 'typ) var 2593 2594type _ lst = 2595 | CNil : nil lst 2596 | CCons : 'h * ('t lst) -> ('h -> 't) lst 2597;; 2598 2599let rec get_var : type stk ret. (stk s, ret) var -> stk lst -> ret = fun n s -> 2600 match n, s with 2601 | Head, CCons (h, _) -> h 2602 | Tail n', CCons (_, t) -> get_var n' t 2603;; 2604type 'a t = [< `Foo | `Bar] as 'a;; 2605type 'a s = [< `Foo | `Bar | `Baz > `Bar] as 'a;; 2606 2607type 'a first = First : 'a second -> ('b t as 'a) first 2608and 'a second = Second : ('b s as 'a) second;; 2609 2610type aux = Aux : 'a t second * ('a -> int) -> aux;; 2611 2612let it : 'a. [< `Bar | `Foo > `Bar ] as 'a = `Bar;; 2613 2614let g (Aux(Second, f)) = f it;; 2615type (_, _) eqp = Y : ('a, 'a) eqp | N : string -> ('a, 'b) eqp 2616let f : ('a list, 'a) eqp -> unit = function N s -> print_string s;; 2617 2618module rec A : sig type t = B.t list end = 2619 struct type t = B.t list end 2620and B : sig type t val eq : (B.t list, t) eqp end = 2621 struct 2622 type t = A.t 2623 let eq = Y 2624 end;; 2625 2626f B.eq;; 2627type (_, _) t = 2628 | Nil : ('tl, 'tl) t 2629 | Cons : 'a * ('b, 'tl) t -> ('a * 'b, 'tl) t;; 2630 2631let get1 (Cons (x, _) : (_ * 'a, 'a) t) = x ;; (* warn, cf PR#6993 *) 2632 2633let get1' = function 2634 | (Cons (x, _) : (_ * 'a, 'a) t) -> x 2635 | Nil -> assert false ;; (* ok *) 2636type _ t = 2637 Int : int -> int t | String : string -> string t | Same : 'l t -> 'l t;; 2638let rec f = function Int x -> x | Same s -> f s;; 2639type 'a tt = 'a t = 2640 Int : int -> int tt | String : string -> string tt | Same : 'l1 t -> 'l2 tt;; 2641type _ t = I : int t;; 2642 2643let f (type a) (x : a t) = 2644 let module M = struct 2645 let (I : a t) = x (* fail because of toplevel let *) 2646 let x = (I : a t) 2647 end in 2648 () ;; 2649 2650(* extra example by Stephen Dolan, using recursive modules *) 2651(* Should not be allowed! *) 2652type (_,_) eq = Refl : ('a, 'a) eq;; 2653 2654let bad (type a) = 2655 let module N = struct 2656 module rec M : sig 2657 val e : (int, a) eq 2658 end = struct 2659 let (Refl : (int, a) eq) = M.e (* must fail for soundness *) 2660 let e : (int, a) eq = Refl 2661 end 2662 end in N.M.e 2663;; 2664type +'a n = private int 2665type nil = private Nil_type 2666type (_,_) elt = 2667 | Elt_fine: 'nat n -> ('l,'nat * 'l) elt 2668 | Elt: 'nat n -> ('l,'nat -> 'l) elt 2669type _ t = Nil : nil t | Cons : ('x, 'fx) elt * 'x t -> 'fx t;; 2670 2671let undetected: ('a -> 'b -> nil) t -> 'a n -> 'b n -> unit = fun sh i j -> 2672 let Cons(Elt dim, _) = sh in () 2673;; 2674type _ t = T : int t;; 2675 2676(* Should raise Not_found *) 2677let _ = match (raise Not_found : float t) with _ -> .;; 2678type (_, _) eq = Eq : ('a, 'a) eq | Neq : int -> ('a, 'b) eq;; 2679type 'a t;; 2680let f (type a) (Neq n : (a, a t) eq) = n;; (* warn! *) 2681 2682module F (T : sig type _ t end) = struct 2683 let f (type a) (Neq n : (a, a T.t) eq) = n (* warn! *) 2684end;; 2685(* First-Order Unification by Structural Recursion *) 2686(* Conor McBride, JFP 13(6) *) 2687(* http://strictlypositive.org/publications.html *) 2688 2689(* This is a translation of the code part to ocaml *) 2690(* Of course, we do not prove other properties, not even termination *) 2691 2692(* 2.2 Inductive Families *) 2693 2694type zero = Zero 2695type _ succ = Succ 2696type _ nat = 2697 | NZ : zero nat 2698 | NS : 'a nat -> 'a succ nat 2699 2700type _ fin = 2701 | FZ : 'a succ fin 2702 | FS : 'a fin -> 'a succ fin 2703 2704(* We cannot define 2705 val empty : zero fin -> 'a 2706 because we cannot write an empty pattern matching. 2707 This might be useful to have *) 2708 2709(* In place, prove that the parameter is 'a succ *) 2710type _ is_succ = IS : 'a succ is_succ 2711 2712let fin_succ : type n. n fin -> n is_succ = function 2713 | FZ -> IS 2714 | FS _ -> IS 2715;; 2716 2717(* 3 First-Order Terms, Renaming and Substitution *) 2718 2719type 'a term = 2720 | Var of 'a fin 2721 | Leaf 2722 | Fork of 'a term * 'a term 2723 2724let var x = Var x 2725 2726let lift r : 'm fin -> 'n term = fun x -> Var (r x) 2727 2728let rec pre_subst f = function 2729 | Var x -> f x 2730 | Leaf -> Leaf 2731 | Fork (t1, t2) -> Fork (pre_subst f t1, pre_subst f t2) 2732 2733let comp_subst f g (x : 'a fin) = pre_subst f (g x) 2734(* val comp_subst : 2735 ('b fin -> 'c term) -> ('a fin -> 'b term) -> 'a fin -> 'c term *) 2736;; 2737 2738(* 4 The Occur-Check, through thick and thin *) 2739 2740let rec thin : type n. n succ fin -> n fin -> n succ fin = 2741 fun x y -> match x, y with 2742 | FZ, y -> FS y 2743 | FS x, FZ -> FZ 2744 | FS x, FS y -> FS (thin x y) 2745 2746let bind t f = 2747 match t with 2748 | None -> None 2749 | Some x -> f x 2750(* val bind : 'a option -> ('a -> 'b option) -> 'b option *) 2751 2752let rec thick : type n. n succ fin -> n succ fin -> n fin option = 2753 fun x y -> match x, y with 2754 | FZ, FZ -> None 2755 | FZ, FS y -> Some y 2756 | FS x, FZ -> let IS = fin_succ x in Some FZ 2757 | FS x, FS y -> 2758 let IS = fin_succ x in bind (thick x y) (fun x -> Some (FS x)) 2759 2760let rec check : type n. n succ fin -> n succ term -> n term option = 2761 fun x t -> match t with 2762 | Var y -> bind (thick x y) (fun x -> Some (Var x)) 2763 | Leaf -> Some Leaf 2764 | Fork (t1, t2) -> 2765 bind (check x t1) (fun t1 -> 2766 bind (check x t2) (fun t2 -> Some (Fork (t1, t2)))) 2767 2768let subst_var x t' y = 2769 match thick x y with 2770 | None -> t' 2771 | Some y' -> Var y' 2772(* val subst_var : 'a succ fin -> 'a term -> 'a succ fin -> 'a term *) 2773 2774let subst x t' = pre_subst (subst_var x t') 2775(* val subst : 'a succ fin -> 'a term -> 'a succ term -> 'a term *) 2776;; 2777 2778(* 5 A Refinement of Substitution *) 2779 2780type (_,_) alist = 2781 | Anil : ('n,'n) alist 2782 | Asnoc : ('m,'n) alist * 'm term * 'm succ fin -> ('m succ, 'n) alist 2783 2784let rec sub : type m n. (m,n) alist -> m fin -> n term = function 2785 | Anil -> var 2786 | Asnoc (s, t, x) -> comp_subst (sub s) (subst_var x t) 2787 2788let rec append : type m n l. (m,n) alist -> (l,m) alist -> (l,n) alist = 2789 fun r s -> match s with 2790 | Anil -> r 2791 | Asnoc (s, t, x) -> Asnoc (append r s, t, x) 2792 2793type _ ealist = EAlist : ('a,'b) alist -> 'a ealist 2794 2795let asnoc a t' x = EAlist (Asnoc (a, t', x)) 2796 2797(* Extra work: we need sub to work on ealist too, for examples *) 2798let rec weaken_fin : type n. n fin -> n succ fin = function 2799 | FZ -> FZ 2800 | FS x -> FS (weaken_fin x) 2801 2802let weaken_term t = pre_subst (fun x -> Var (weaken_fin x)) t 2803 2804let rec weaken_alist : type m n. (m, n) alist -> (m succ, n succ) alist = 2805 function 2806 | Anil -> Anil 2807 | Asnoc (s, t, x) -> Asnoc (weaken_alist s, weaken_term t, weaken_fin x) 2808 2809let rec sub' : type m. m ealist -> m fin -> m term = function 2810 | EAlist Anil -> var 2811 | EAlist (Asnoc (s, t, x)) -> 2812 comp_subst (sub' (EAlist (weaken_alist s))) 2813 (fun t' -> weaken_term (subst_var x t t')) 2814 2815let subst' d = pre_subst (sub' d) 2816(* val subst' : 'a ealist -> 'a term -> 'a term *) 2817;; 2818 2819(* 6 First-Order Unification *) 2820 2821let flex_flex x y = 2822 match thick x y with 2823 | Some y' -> asnoc Anil (Var y') x 2824 | None -> EAlist Anil 2825(* val flex_flex : 'a succ fin -> 'a succ fin -> 'a succ ealist *) 2826 2827let flex_rigid x t = 2828 bind (check x t) (fun t' -> Some (asnoc Anil t' x)) 2829(* val flex_rigid : 'a succ fin -> 'a succ term -> 'a succ ealist option *) 2830 2831let rec amgu : type m. m term -> m term -> m ealist -> m ealist option = 2832 fun s t acc -> match s, t, acc with 2833 | Leaf, Leaf, _ -> Some acc 2834 | Leaf, Fork _, _ -> None 2835 | Fork _, Leaf, _ -> None 2836 | Fork (s1, s2), Fork (t1, t2), _ -> 2837 bind (amgu s1 t1 acc) (amgu s2 t2) 2838 | Var x, Var y, EAlist Anil -> let IS = fin_succ x in Some (flex_flex x y) 2839 | Var x, t, EAlist Anil -> let IS = fin_succ x in flex_rigid x t 2840 | t, Var x, EAlist Anil -> let IS = fin_succ x in flex_rigid x t 2841 | s, t, EAlist(Asnoc(d,r,z)) -> 2842 bind (amgu (subst z r s) (subst z r t) (EAlist d)) 2843 (fun (EAlist d) -> Some (asnoc d r z)) 2844 2845let mgu s t = amgu s t (EAlist Anil) 2846(* val mgu : 'a term -> 'a term -> 'a ealist option *) 2847;; 2848 2849let s = Fork (Var FZ, Fork (Var (FS (FS FZ)), Leaf)) 2850let t = Fork (Var (FS FZ), Var (FS FZ)) 2851let d = match mgu s t with Some x -> x | None -> failwith "mgu" 2852let s' = subst' d s 2853let t' = subst' d t 2854;; 2855(* Injectivity *) 2856 2857type (_, _) eq = Refl : ('a, 'a) eq 2858 2859let magic : 'a 'b. 'a -> 'b = 2860 fun (type a b) (x : a) -> 2861 let module M = 2862 (functor (T : sig type 'a t end) -> 2863 struct 2864 let f (Refl : (a T.t, b T.t) eq) = (x :> b) 2865 end) 2866 (struct type 'a t = unit end) 2867 in M.f Refl 2868;; 2869 2870(* Variance and subtyping *) 2871 2872type (_, +_) eq = Refl : ('a, 'a) eq 2873 2874let magic : 'a 'b. 'a -> 'b = 2875 fun (type a) (type b) (x : a) -> 2876 let bad_proof (type a) = 2877 (Refl : (< m : a>, <m : a>) eq :> (<m : a>, < >) eq) in 2878 let downcast : type a. (a, < >) eq -> < > -> a = 2879 fun (type a) (Refl : (a, < >) eq) (s : < >) -> (s :> a) in 2880 (downcast bad_proof ((object method m = x end) :> < >)) # m 2881;; 2882 2883(* Record patterns *) 2884 2885type _ t = 2886 | IntLit : int t 2887 | BoolLit : bool t 2888 2889let check : type s . s t * s -> bool = function 2890 | BoolLit, false -> false 2891 | IntLit , 6 -> false 2892;; 2893 2894type ('a, 'b) pair = { fst : 'a; snd : 'b } 2895 2896let check : type s . (s t, s) pair -> bool = function 2897 | {fst = BoolLit; snd = false} -> false 2898 | {fst = IntLit ; snd = 6} -> false 2899;; 2900module type S = sig type t [@@immediate] end;; 2901module F (M : S) : S = M;; 2902[%%expect{| 2903module type S = sig type t [@@immediate] end 2904module F : functor (M : S) -> S 2905|}];; 2906 2907(* VALID DECLARATIONS *) 2908 2909module A = struct 2910 (* Abstract types can be immediate *) 2911 type t [@@immediate] 2912 2913 (* [@@immediate] tag here is unnecessary but valid since t has it *) 2914 type s = t [@@immediate] 2915 2916 (* Again, valid alias even without tag *) 2917 type r = s 2918 2919 (* Mutually recursive declarations work as well *) 2920 type p = q [@@immediate] 2921 and q = int 2922end;; 2923[%%expect{| 2924module A : 2925 sig 2926 type t [@@immediate] 2927 type s = t [@@immediate] 2928 type r = s 2929 type p = q [@@immediate] 2930 and q = int 2931 end 2932|}];; 2933 2934(* Valid using with constraints *) 2935module type X = sig type t end;; 2936module Y = struct type t = int end;; 2937module Z = ((Y : X with type t = int) : sig type t [@@immediate] end);; 2938[%%expect{| 2939module type X = sig type t end 2940module Y : sig type t = int end 2941module Z : sig type t [@@immediate] end 2942|}];; 2943 2944(* Valid using an explicit signature *) 2945module M_valid : S = struct type t = int end;; 2946module FM_valid = F (struct type t = int end);; 2947[%%expect{| 2948module M_valid : S 2949module FM_valid : S 2950|}];; 2951 2952(* Practical usage over modules *) 2953module Foo : sig type t val x : t ref end = struct 2954 type t = int 2955 let x = ref 0 2956end;; 2957[%%expect{| 2958module Foo : sig type t val x : t ref end 2959|}];; 2960 2961module Bar : sig type t [@@immediate] val x : t ref end = struct 2962 type t = int 2963 let x = ref 0 2964end;; 2965[%%expect{| 2966module Bar : sig type t [@@immediate] val x : t ref end 2967|}];; 2968 2969let test f = 2970 let start = Sys.time() in f (); 2971 (Sys.time() -. start);; 2972[%%expect{| 2973val test : (unit -> 'a) -> float = <fun> 2974|}];; 2975 2976let test_foo () = 2977 for i = 0 to 100_000_000 do 2978 Foo.x := !Foo.x 2979 done;; 2980[%%expect{| 2981val test_foo : unit -> unit = <fun> 2982|}];; 2983 2984let test_bar () = 2985 for i = 0 to 100_000_000 do 2986 Bar.x := !Bar.x 2987 done;; 2988[%%expect{| 2989val test_bar : unit -> unit = <fun> 2990|}];; 2991 2992(* Uncomment these to test. Should see substantial speedup! 2993let () = Printf.printf "No @@immediate: %fs\n" (test test_foo) 2994let () = Printf.printf "With @@immediate: %fs\n" (test test_bar) *) 2995 2996 2997(* INVALID DECLARATIONS *) 2998 2999(* Cannot directly declare a non-immediate type as immediate *) 3000module B = struct 3001 type t = string [@@immediate] 3002end;; 3003[%%expect{| 3004Line _, characters 2-31: 3005Error: Types marked with the immediate attribute must be 3006 non-pointer types like int or bool 3007|}];; 3008 3009(* Not guaranteed that t is immediate, so this is an invalid declaration *) 3010module C = struct 3011 type t 3012 type s = t [@@immediate] 3013end;; 3014[%%expect{| 3015Line _, characters 2-26: 3016Error: Types marked with the immediate attribute must be 3017 non-pointer types like int or bool 3018|}];; 3019 3020(* Can't ascribe to an immediate type signature with a non-immediate type *) 3021module D : sig type t [@@immediate] end = struct 3022 type t = string 3023end;; 3024[%%expect{| 3025Line _, characters 42-70: 3026Error: Signature mismatch: 3027 Modules do not match: 3028 sig type t = string end 3029 is not included in 3030 sig type t [@@immediate] end 3031 Type declarations do not match: 3032 type t = string 3033 is not included in 3034 type t [@@immediate] 3035 the first is not an immediate type. 3036|}];; 3037 3038(* Same as above but with explicit signature *) 3039module M_invalid : S = struct type t = string end;; 3040module FM_invalid = F (struct type t = string end);; 3041[%%expect{| 3042Line _, characters 23-49: 3043Error: Signature mismatch: 3044 Modules do not match: sig type t = string end is not included in S 3045 Type declarations do not match: 3046 type t = string 3047 is not included in 3048 type t [@@immediate] 3049 the first is not an immediate type. 3050|}];; 3051 3052(* Can't use a non-immediate type even if mutually recursive *) 3053module E = struct 3054 type t = s [@@immediate] 3055 and s = string 3056end;; 3057[%%expect{| 3058Line _, characters 2-26: 3059Error: Types marked with the immediate attribute must be 3060 non-pointer types like int or bool 3061|}];; 3062(* 3063 Implicit unpack allows to omit the signature in (val ...) expressions. 3064 3065 It also adds (module M : S) and (module M) patterns, relying on 3066 implicit (val ...) for the implementation. Such patterns can only 3067 be used in function definition, match clauses, and let ... in. 3068 3069 New: implicit pack is also supported, and you only need to be able 3070 to infer the the module type path from the context. 3071 *) 3072(* ocaml -principal *) 3073 3074(* Use a module pattern *) 3075let sort (type s) (module Set : Set.S with type elt = s) l = 3076 Set.elements (List.fold_right Set.add l Set.empty) 3077 3078(* No real improvement here? *) 3079let make_set (type s) cmp : (module Set.S with type elt = s) = 3080 (module Set.Make (struct type t = s let compare = cmp end)) 3081 3082(* No type annotation here *) 3083let sort_cmp (type s) cmp = 3084 sort (module Set.Make (struct type t = s let compare = cmp end)) 3085 3086module type S = sig type t val x : t end;; 3087let f (module M : S with type t = int) = M.x;; 3088let f (module M : S with type t = 'a) = M.x;; (* Error *) 3089let f (type a) (module M : S with type t = a) = M.x;; 3090f (module struct type t = int let x = 1 end);; 3091 3092type 'a s = {s: (module S with type t = 'a)};; 3093{s=(module struct type t = int let x = 1 end)};; 3094let f {s=(module M)} = M.x;; (* Error *) 3095let f (type a) ({s=(module M)} : a s) = M.x;; 3096 3097type s = {s: (module S with type t = int)};; 3098let f {s=(module M)} = M.x;; 3099let f {s=(module M)} {s=(module N)} = M.x + N.x;; 3100 3101module type S = sig val x : int end;; 3102let f (module M : S) y (module N : S) = M.x + y + N.x;; 3103let m = (module struct let x = 3 end);; (* Error *) 3104let m = (module struct let x = 3 end : S);; 3105f m 1 m;; 3106f m 1 (module struct let x = 2 end);; 3107 3108let (module M) = m in M.x;; 3109let (module M) = m;; (* Error: only allowed in [let .. in] *) 3110class c = let (module M) = m in object end;; (* Error again *) 3111module M = (val m);; 3112 3113module type S' = sig val f : int -> int end;; 3114(* Even works with recursion, but must be fully explicit *) 3115let rec (module M : S') = 3116 (module struct let f n = if n <= 0 then 1 else n * M.f (n-1) end : S') 3117in M.f 3;; 3118 3119(* Subtyping *) 3120 3121module type S = sig type t type u val x : t * u end 3122let f (l : (module S with type t = int and type u = bool) list) = 3123 (l :> (module S with type u = bool) list) 3124 3125(* GADTs from the manual *) 3126(* the only modification is in to_string *) 3127 3128module TypEq : sig 3129 type ('a, 'b) t 3130 val apply: ('a, 'b) t -> 'a -> 'b 3131 val refl: ('a, 'a) t 3132 val sym: ('a, 'b) t -> ('b, 'a) t 3133end = struct 3134 type ('a, 'b) t = ('a -> 'b) * ('b -> 'a) 3135 let refl = (fun x -> x), (fun x -> x) 3136 let apply (f, _) x = f x 3137 let sym (f, g) = (g, f) 3138end 3139 3140module rec Typ : sig 3141 module type PAIR = sig 3142 type t and t1 and t2 3143 val eq: (t, t1 * t2) TypEq.t 3144 val t1: t1 Typ.typ 3145 val t2: t2 Typ.typ 3146 end 3147 3148 type 'a typ = 3149 | Int of ('a, int) TypEq.t 3150 | String of ('a, string) TypEq.t 3151 | Pair of (module PAIR with type t = 'a) 3152end = Typ 3153 3154let int = Typ.Int TypEq.refl 3155 3156let str = Typ.String TypEq.refl 3157 3158let pair (type s1) (type s2) t1 t2 = 3159 let module P = struct 3160 type t = s1 * s2 3161 type t1 = s1 3162 type t2 = s2 3163 let eq = TypEq.refl 3164 let t1 = t1 3165 let t2 = t2 3166 end in 3167 Typ.Pair (module P) 3168 3169open Typ 3170let rec to_string: 'a. 'a Typ.typ -> 'a -> string = 3171 fun (type s) t x -> 3172 match (t : s typ) with 3173 | Int eq -> string_of_int (TypEq.apply eq x) 3174 | String eq -> Printf.sprintf "%S" (TypEq.apply eq x) 3175 | Pair (module P) -> 3176 let (x1, x2) = TypEq.apply P.eq x in 3177 Printf.sprintf "(%s,%s)" (to_string P.t1 x1) (to_string P.t2 x2) 3178 3179(* Wrapping maps *) 3180module type MapT = sig 3181 include Map.S 3182 type data 3183 type map 3184 val of_t : data t -> map 3185 val to_t : map -> data t 3186end 3187 3188type ('k,'d,'m) map = 3189 (module MapT with type key = 'k and type data = 'd and type map = 'm) 3190 3191let add (type k) (type d) (type m) (m:(k,d,m) map) x y s = 3192 let module M = 3193 (val m:MapT with type key = k and type data = d and type map = m) in 3194 M.of_t (M.add x y (M.to_t s)) 3195 3196module SSMap = struct 3197 include Map.Make(String) 3198 type data = string 3199 type map = data t 3200 let of_t x = x 3201 let to_t x = x 3202end 3203 3204let ssmap = 3205 (module SSMap: 3206 MapT with type key = string and type data = string and type map = SSMap.map) 3207;; 3208 3209let ssmap = 3210 (module struct include SSMap end : 3211 MapT with type key = string and type data = string and type map = SSMap.map) 3212;; 3213 3214let ssmap = 3215 (let module S = struct include SSMap end in (module S) : 3216 (module 3217 MapT with type key = string and type data = string and type map = SSMap.map)) 3218;; 3219 3220let ssmap = 3221 (module SSMap: MapT with type key = _ and type data = _ and type map = _) 3222;; 3223 3224let ssmap : (_,_,_) map = (module SSMap);; 3225 3226add ssmap;; 3227open StdLabels 3228open MoreLabels 3229 3230(* Use maps for substitutions and sets for free variables *) 3231 3232module Subst = Map.Make(struct type t = string let compare = compare end) 3233module Names = Set.Make(struct type t = string let compare = compare end) 3234 3235 3236(* Variables are common to lambda and expr *) 3237 3238type var = [`Var of string] 3239 3240let subst_var ~subst : var -> _ = 3241 function `Var s as x -> 3242 try Subst.find s subst 3243 with Not_found -> x 3244 3245let free_var : var -> _ = function `Var s -> Names.singleton s 3246 3247 3248(* The lambda language: free variables, substitutions, and evaluation *) 3249 3250type 'a lambda = [`Var of string | `Abs of string * 'a | `App of 'a * 'a] 3251 3252let free_lambda ~free_rec : _ lambda -> _ = function 3253 #var as x -> free_var x 3254 | `Abs (s, t) -> Names.remove s (free_rec t) 3255 | `App (t1, t2) -> Names.union (free_rec t1) (free_rec t2) 3256 3257let map_lambda ~map_rec : _ lambda -> _ = function 3258 #var as x -> x 3259 | `Abs (s, t) as l -> 3260 let t' = map_rec t in 3261 if t == t' then l else `Abs(s, t') 3262 | `App (t1, t2) as l -> 3263 let t'1 = map_rec t1 and t'2 = map_rec t2 in 3264 if t'1 == t1 && t'2 == t2 then l else `App (t'1, t'2) 3265 3266let next_id = 3267 let current = ref 3 in 3268 fun () -> incr current; !current 3269 3270let subst_lambda ~subst_rec ~free ~subst : _ lambda -> _ = function 3271 #var as x -> subst_var ~subst x 3272 | `Abs(s, t) as l -> 3273 let used = free t in 3274 let used_expr = 3275 Subst.fold subst ~init:[] 3276 ~f:(fun ~key ~data acc -> 3277 if Names.mem s used then data::acc else acc) in 3278 if List.exists used_expr ~f:(fun t -> Names.mem s (free t)) then 3279 let name = s ^ string_of_int (next_id ()) in 3280 `Abs(name, 3281 subst_rec ~subst:(Subst.add ~key:s ~data:(`Var name) subst) t) 3282 else 3283 map_lambda ~map_rec:(subst_rec ~subst:(Subst.remove s subst)) l 3284 | `App _ as l -> 3285 map_lambda ~map_rec:(subst_rec ~subst) l 3286 3287let eval_lambda ~eval_rec ~subst l = 3288 match map_lambda ~map_rec:eval_rec l with 3289 `App(`Abs(s,t1), t2) -> 3290 eval_rec (subst ~subst:(Subst.add ~key:s ~data:t2 Subst.empty) t1) 3291 | t -> t 3292 3293(* Specialized versions to use on lambda *) 3294 3295let rec free1 x = free_lambda ~free_rec:free1 x 3296let rec subst1 ~subst = subst_lambda ~subst_rec:subst1 ~free:free1 ~subst 3297let rec eval1 x = eval_lambda ~eval_rec:eval1 ~subst:subst1 x 3298 3299 3300(* The expr language of arithmetic expressions *) 3301 3302type 'a expr = 3303 [`Var of string | `Num of int | `Add of 'a * 'a 3304 | `Neg of 'a | `Mult of 'a * 'a] 3305 3306let free_expr ~free_rec : _ expr -> _ = function 3307 #var as x -> free_var x 3308 | `Num _ -> Names.empty 3309 | `Add(x, y) -> Names.union (free_rec x) (free_rec y) 3310 | `Neg x -> free_rec x 3311 | `Mult(x, y) -> Names.union (free_rec x) (free_rec y) 3312 3313(* Here map_expr helps a lot *) 3314let map_expr ~map_rec : _ expr -> _ = function 3315 #var as x -> x 3316 | `Num _ as x -> x 3317 | `Add(x, y) as e -> 3318 let x' = map_rec x and y' = map_rec y in 3319 if x == x' && y == y' then e 3320 else `Add(x', y') 3321 | `Neg x as e -> 3322 let x' = map_rec x in 3323 if x == x' then e else `Neg x' 3324 | `Mult(x, y) as e -> 3325 let x' = map_rec x and y' = map_rec y in 3326 if x == x' && y == y' then e 3327 else `Mult(x', y') 3328 3329let subst_expr ~subst_rec ~subst : _ expr -> _ = function 3330 #var as x -> subst_var ~subst x 3331 | #expr as e -> map_expr ~map_rec:(subst_rec ~subst) e 3332 3333let eval_expr ~eval_rec e = 3334 match map_expr ~map_rec:eval_rec e with 3335 `Add(`Num m, `Num n) -> `Num (m+n) 3336 | `Neg(`Num n) -> `Num (-n) 3337 | `Mult(`Num m, `Num n) -> `Num (m*n) 3338 | #expr as e -> e 3339 3340(* Specialized versions *) 3341 3342let rec free2 x = free_expr ~free_rec:free2 x 3343let rec subst2 ~subst = subst_expr ~subst_rec:subst2 ~subst 3344let rec eval2 x = eval_expr ~eval_rec:eval2 x 3345 3346 3347(* The lexpr language, reunion of lambda and expr *) 3348 3349type lexpr = 3350 [ `Var of string | `Abs of string * lexpr | `App of lexpr * lexpr 3351 | `Num of int | `Add of lexpr * lexpr | `Neg of lexpr 3352 | `Mult of lexpr * lexpr ] 3353 3354let rec free : lexpr -> _ = function 3355 #lambda as x -> free_lambda ~free_rec:free x 3356 | #expr as x -> free_expr ~free_rec:free x 3357 3358let rec subst ~subst:s : lexpr -> _ = function 3359 #lambda as x -> subst_lambda ~subst_rec:subst ~subst:s ~free x 3360 | #expr as x -> subst_expr ~subst_rec:subst ~subst:s x 3361 3362let rec eval : lexpr -> _ = function 3363 #lambda as x -> eval_lambda ~eval_rec:eval ~subst x 3364 | #expr as x -> eval_expr ~eval_rec:eval x 3365 3366let rec print = function 3367 | `Var id -> print_string id 3368 | `Abs (id, l) -> print_string ("\ " ^ id ^ " . "); print l 3369 | `App (l1, l2) -> print l1; print_string " "; print l2 3370 | `Num x -> print_int x 3371 | `Add (e1, e2) -> print e1; print_string " + "; print e2 3372 | `Neg e -> print_string "-"; print e 3373 | `Mult (e1, e2) -> print e1; print_string " * "; print e2 3374 3375let () = 3376 let e1 = eval1 (`App(`Abs("x",`Var"x"), `Var"y")) in 3377 let e2 = eval2 (`Add(`Mult(`Num 3,`Neg(`Num 2)), `Var"x")) in 3378 let e3 = eval (`Add(`App(`Abs("x",`Mult(`Var"x",`Var"x")),`Num 2), `Num 5)) in 3379 print e1; print_newline (); 3380 print e2; print_newline (); 3381 print e3; print_newline () 3382(* Full fledge version, using objects to structure code *) 3383 3384open StdLabels 3385open MoreLabels 3386 3387(* Use maps for substitutions and sets for free variables *) 3388 3389module Subst = Map.Make(struct type t = string let compare = compare end) 3390module Names = Set.Make(struct type t = string let compare = compare end) 3391 3392(* To build recursive objects *) 3393 3394let lazy_fix make = 3395 let rec obj () = make (lazy (obj ()) : _ Lazy.t) in 3396 obj () 3397 3398let (!!) = Lazy.force 3399 3400(* The basic operations *) 3401 3402class type ['a, 'b] ops = 3403 object 3404 method free : x:'b -> ?y:'c -> Names.t 3405 method subst : sub:'a Subst.t -> 'b -> 'a 3406 method eval : 'b -> 'a 3407 end 3408 3409(* Variables are common to lambda and expr *) 3410 3411type var = [`Var of string] 3412 3413class ['a] var_ops = object (self : ('a, var) #ops) 3414 constraint 'a = [> var] 3415 method subst ~sub (`Var s as x) = 3416 try Subst.find s sub with Not_found -> x 3417 method free (`Var s) = 3418 Names.singleton s 3419 method eval (#var as v) = v 3420end 3421 3422(* The lambda language: free variables, substitutions, and evaluation *) 3423 3424type 'a lambda = [`Var of string | `Abs of string * 'a | `App of 'a * 'a] 3425 3426let next_id = 3427 let current = ref 3 in 3428 fun () -> incr current; !current 3429 3430class ['a] lambda_ops (ops : ('a,'a) #ops Lazy.t) = 3431 let var : 'a var_ops = new var_ops 3432 and free = lazy !!ops#free 3433 and subst = lazy !!ops#subst 3434 and eval = lazy !!ops#eval in 3435 object (self : ('a, 'a lambda) #ops) 3436 constraint 'a = [> 'a lambda] 3437 method free = function 3438 #var as x -> var#free x 3439 | `Abs (s, t) -> Names.remove s (!!free t) 3440 | `App (t1, t2) -> Names.union (!!free t1) (!!free t2) 3441 3442 method map ~f = function 3443 #var as x -> x 3444 | `Abs (s, t) as l -> 3445 let t' = f t in 3446 if t == t' then l else `Abs(s, t') 3447 | `App (t1, t2) as l -> 3448 let t'1 = f t1 and t'2 = f t2 in 3449 if t'1 == t1 && t'2 == t2 then l else `App (t'1, t'2) 3450 3451 method subst ~sub = function 3452 #var as x -> var#subst ~sub x 3453 | `Abs(s, t) as l -> 3454 let used = !!free t in 3455 let used_expr = 3456 Subst.fold sub ~init:[] 3457 ~f:(fun ~key ~data acc -> 3458 if Names.mem s used then data::acc else acc) in 3459 if List.exists used_expr ~f:(fun t -> Names.mem s (!!free t)) then 3460 let name = s ^ string_of_int (next_id ()) in 3461 `Abs(name, 3462 !!subst ~sub:(Subst.add ~key:s ~data:(`Var name) sub) t) 3463 else 3464 self#map ~f:(!!subst ~sub:(Subst.remove s sub)) l 3465 | `App _ as l -> 3466 self#map ~f:(!!subst ~sub) l 3467 3468 method eval l = 3469 match self#map ~f:!!eval l with 3470 `App(`Abs(s,t1), t2) -> 3471 !!eval (!!subst ~sub:(Subst.add ~key:s ~data:t2 Subst.empty) t1) 3472 | t -> t 3473end 3474 3475(* Operations specialized to lambda *) 3476 3477let lambda = lazy_fix (new lambda_ops) 3478 3479(* The expr language of arithmetic expressions *) 3480 3481type 'a expr = 3482 [ `Var of string | `Num of int | `Add of 'a * 'a 3483 | `Neg of 'a | `Mult of 'a * 'a] 3484 3485class ['a] expr_ops (ops : ('a,'a) #ops Lazy.t) = 3486 let var : 'a var_ops = new var_ops 3487 and free = lazy !!ops#free 3488 and subst = lazy !!ops#subst 3489 and eval = lazy !!ops#eval in 3490 object (self : ('a, 'a expr) #ops) 3491 constraint 'a = [> 'a expr] 3492 method free = function 3493 #var as x -> var#free x 3494 | `Num _ -> Names.empty 3495 | `Add(x, y) -> Names.union (!!free x) (!!free y) 3496 | `Neg x -> !!free x 3497 | `Mult(x, y) -> Names.union (!!free x) (!!free y) 3498 3499 method map ~f = function 3500 #var as x -> x 3501 | `Num _ as x -> x 3502 | `Add(x, y) as e -> 3503 let x' = f x and y' = f y in 3504 if x == x' && y == y' then e 3505 else `Add(x', y') 3506 | `Neg x as e -> 3507 let x' = f x in 3508 if x == x' then e else `Neg x' 3509 | `Mult(x, y) as e -> 3510 let x' = f x and y' = f y in 3511 if x == x' && y == y' then e 3512 else `Mult(x', y') 3513 3514 method subst ~sub = function 3515 #var as x -> var#subst ~sub x 3516 | #expr as e -> self#map ~f:(!!subst ~sub) e 3517 3518 method eval (#expr as e) = 3519 match self#map ~f:!!eval e with 3520 `Add(`Num m, `Num n) -> `Num (m+n) 3521 | `Neg(`Num n) -> `Num (-n) 3522 | `Mult(`Num m, `Num n) -> `Num (m*n) 3523 | e -> e 3524 end 3525 3526(* Specialized versions *) 3527 3528let expr = lazy_fix (new expr_ops) 3529 3530(* The lexpr language, reunion of lambda and expr *) 3531 3532type 'a lexpr = [ 'a lambda | 'a expr ] 3533 3534class ['a] lexpr_ops (ops : ('a,'a) #ops Lazy.t) = 3535 let lambda = new lambda_ops ops in 3536 let expr = new expr_ops ops in 3537 object (self : ('a, 'a lexpr) #ops) 3538 constraint 'a = [> 'a lexpr] 3539 method free = function 3540 #lambda as x -> lambda#free x 3541 | #expr as x -> expr#free x 3542 3543 method subst ~sub = function 3544 #lambda as x -> lambda#subst ~sub x 3545 | #expr as x -> expr#subst ~sub x 3546 3547 method eval = function 3548 #lambda as x -> lambda#eval x 3549 | #expr as x -> expr#eval x 3550end 3551 3552let lexpr = lazy_fix (new lexpr_ops) 3553 3554let rec print = function 3555 | `Var id -> print_string id 3556 | `Abs (id, l) -> print_string ("\ " ^ id ^ " . "); print l 3557 | `App (l1, l2) -> print l1; print_string " "; print l2 3558 | `Num x -> print_int x 3559 | `Add (e1, e2) -> print e1; print_string " + "; print e2 3560 | `Neg e -> print_string "-"; print e 3561 | `Mult (e1, e2) -> print e1; print_string " * "; print e2 3562 3563let () = 3564 let e1 = lambda#eval (`App(`Abs("x",`Var"x"), `Var"y")) in 3565 let e2 = expr#eval (`Add(`Mult(`Num 3,`Neg(`Num 2)), `Var"x")) in 3566 let e3 = 3567 lexpr#eval (`Add(`App(`Abs("x",`Mult(`Var"x",`Var"x")),`Num 2), `Num 5)) 3568 in 3569 print e1; print_newline (); 3570 print e2; print_newline (); 3571 print e3; print_newline () 3572(* Full fledge version, using objects to structure code *) 3573 3574open StdLabels 3575open MoreLabels 3576 3577(* Use maps for substitutions and sets for free variables *) 3578 3579module Subst = Map.Make(struct type t = string let compare = compare end) 3580module Names = Set.Make(struct type t = string let compare = compare end) 3581 3582(* To build recursive objects *) 3583 3584let lazy_fix make = 3585 let rec obj () = make (lazy (obj ()) : _ Lazy.t) in 3586 obj () 3587 3588let (!!) = Lazy.force 3589 3590(* The basic operations *) 3591 3592class type ['a, 'b] ops = 3593 object 3594 method free : 'b -> Names.t 3595 method subst : sub:'a Subst.t -> 'b -> 'a 3596 method eval : 'b -> 'a 3597 end 3598 3599(* Variables are common to lambda and expr *) 3600 3601type var = [`Var of string] 3602 3603let var = object (self : ([>var], var) #ops) 3604 method subst ~sub (`Var s as x) = 3605 try Subst.find s sub with Not_found -> x 3606 method free (`Var s) = 3607 Names.singleton s 3608 method eval (#var as v) = v 3609end 3610 3611(* The lambda language: free variables, substitutions, and evaluation *) 3612 3613type 'a lambda = [`Var of string | `Abs of string * 'a | `App of 'a * 'a] 3614 3615let next_id = 3616 let current = ref 3 in 3617 fun () -> incr current; !current 3618 3619let lambda_ops (ops : ('a,'a) #ops Lazy.t) = 3620 let free = lazy !!ops#free 3621 and subst = lazy !!ops#subst 3622 and eval = lazy !!ops#eval in 3623 object (self : ([> 'a lambda], 'a lambda) #ops) 3624 method free = function 3625 #var as x -> var#free x 3626 | `Abs (s, t) -> Names.remove s (!!free t) 3627 | `App (t1, t2) -> Names.union (!!free t1) (!!free t2) 3628 3629 method private map ~f = function 3630 #var as x -> x 3631 | `Abs (s, t) as l -> 3632 let t' = f t in 3633 if t == t' then l else `Abs(s, t') 3634 | `App (t1, t2) as l -> 3635 let t'1 = f t1 and t'2 = f t2 in 3636 if t'1 == t1 && t'2 == t2 then l else `App (t'1, t'2) 3637 3638 method subst ~sub = function 3639 #var as x -> var#subst ~sub x 3640 | `Abs(s, t) as l -> 3641 let used = !!free t in 3642 let used_expr = 3643 Subst.fold sub ~init:[] 3644 ~f:(fun ~key ~data acc -> 3645 if Names.mem s used then data::acc else acc) in 3646 if List.exists used_expr ~f:(fun t -> Names.mem s (!!free t)) then 3647 let name = s ^ string_of_int (next_id ()) in 3648 `Abs(name, 3649 !!subst ~sub:(Subst.add ~key:s ~data:(`Var name) sub) t) 3650 else 3651 self#map ~f:(!!subst ~sub:(Subst.remove s sub)) l 3652 | `App _ as l -> 3653 self#map ~f:(!!subst ~sub) l 3654 3655 method eval l = 3656 match self#map ~f:!!eval l with 3657 `App(`Abs(s,t1), t2) -> 3658 !!eval (!!subst ~sub:(Subst.add ~key:s ~data:t2 Subst.empty) t1) 3659 | t -> t 3660end 3661 3662(* Operations specialized to lambda *) 3663 3664let lambda = lazy_fix lambda_ops 3665 3666(* The expr language of arithmetic expressions *) 3667 3668type 'a expr = 3669 [ `Var of string | `Num of int | `Add of 'a * 'a 3670 | `Neg of 'a | `Mult of 'a * 'a] 3671 3672let expr_ops (ops : ('a,'a) #ops Lazy.t) = 3673 let free = lazy !!ops#free 3674 and subst = lazy !!ops#subst 3675 and eval = lazy !!ops#eval in 3676 object (self : ([> 'a expr], 'a expr) #ops) 3677 method free = function 3678 #var as x -> var#free x 3679 | `Num _ -> Names.empty 3680 | `Add(x, y) -> Names.union (!!free x) (!!free y) 3681 | `Neg x -> !!free x 3682 | `Mult(x, y) -> Names.union (!!free x) (!!free y) 3683 3684 method private map ~f = function 3685 #var as x -> x 3686 | `Num _ as x -> x 3687 | `Add(x, y) as e -> 3688 let x' = f x and y' = f y in 3689 if x == x' && y == y' then e 3690 else `Add(x', y') 3691 | `Neg x as e -> 3692 let x' = f x in 3693 if x == x' then e else `Neg x' 3694 | `Mult(x, y) as e -> 3695 let x' = f x and y' = f y in 3696 if x == x' && y == y' then e 3697 else `Mult(x', y') 3698 3699 method subst ~sub = function 3700 #var as x -> var#subst ~sub x 3701 | #expr as e -> self#map ~f:(!!subst ~sub) e 3702 3703 method eval (#expr as e) = 3704 match self#map ~f:!!eval e with 3705 `Add(`Num m, `Num n) -> `Num (m+n) 3706 | `Neg(`Num n) -> `Num (-n) 3707 | `Mult(`Num m, `Num n) -> `Num (m*n) 3708 | e -> e 3709 end 3710 3711(* Specialized versions *) 3712 3713let expr = lazy_fix expr_ops 3714 3715(* The lexpr language, reunion of lambda and expr *) 3716 3717type 'a lexpr = [ 'a lambda | 'a expr ] 3718 3719let lexpr_ops (ops : ('a,'a) #ops Lazy.t) = 3720 let lambda = lambda_ops ops in 3721 let expr = expr_ops ops in 3722 object (self : ([> 'a lexpr], 'a lexpr) #ops) 3723 method free = function 3724 #lambda as x -> lambda#free x 3725 | #expr as x -> expr#free x 3726 3727 method subst ~sub = function 3728 #lambda as x -> lambda#subst ~sub x 3729 | #expr as x -> expr#subst ~sub x 3730 3731 method eval = function 3732 #lambda as x -> lambda#eval x 3733 | #expr as x -> expr#eval x 3734end 3735 3736let lexpr = lazy_fix lexpr_ops 3737 3738let rec print = function 3739 | `Var id -> print_string id 3740 | `Abs (id, l) -> print_string ("\ " ^ id ^ " . "); print l 3741 | `App (l1, l2) -> print l1; print_string " "; print l2 3742 | `Num x -> print_int x 3743 | `Add (e1, e2) -> print e1; print_string " + "; print e2 3744 | `Neg e -> print_string "-"; print e 3745 | `Mult (e1, e2) -> print e1; print_string " * "; print e2 3746 3747let () = 3748 let e1 = lambda#eval (`App(`Abs("x",`Var"x"), `Var"y")) in 3749 let e2 = expr#eval (`Add(`Mult(`Num 3,`Neg(`Num 2)), `Var"x")) in 3750 let e3 = 3751 lexpr#eval (`Add(`App(`Abs("x",`Mult(`Var"x",`Var"x")),`Num 2), `Num 5)) 3752 in 3753 print e1; print_newline (); 3754 print e2; print_newline (); 3755 print e3; print_newline () 3756type sexp = A of string | L of sexp list 3757type 'a t = 'a array 3758let _ = fun (_ : 'a t) -> () 3759 3760let array_of_sexp _ _ = [| |] 3761let sexp_of_array _ _ = A "foo" 3762let sexp_of_int _ = A "42" 3763let int_of_sexp _ = 42 3764 3765let t_of_sexp : 'a . (sexp -> 'a) -> sexp -> 'a t= 3766 let _tp_loc = "core_array.ml.t" in 3767 fun _of_a -> fun t -> (array_of_sexp _of_a) t 3768let _ = t_of_sexp 3769let sexp_of_t : 'a . ('a -> sexp) -> 'a t -> sexp= 3770 fun _of_a -> fun v -> (sexp_of_array _of_a) v 3771let _ = sexp_of_t 3772module T = 3773 struct 3774 module Int = 3775 struct 3776 type t_ = int array 3777 let _ = fun (_ : t_) -> () 3778 3779 let t__of_sexp: sexp -> t_ = 3780 let _tp_loc = "core_array.ml.T.Int.t_" in 3781 fun t -> (array_of_sexp int_of_sexp) t 3782 let _ = t__of_sexp 3783 let sexp_of_t_: t_ -> sexp = 3784 fun v -> (sexp_of_array sexp_of_int) v 3785 let _ = sexp_of_t_ 3786 end 3787 end 3788module type Permissioned = 3789 sig 3790 type ('a,-'perms) t 3791 end 3792module Permissioned : 3793 sig 3794 type ('a,-'perms) t 3795 include 3796 sig 3797 val t_of_sexp : 3798 (sexp -> 'a) -> 3799 (sexp -> 'perms) -> sexp -> ('a,'perms) t 3800 val sexp_of_t : 3801 ('a -> sexp) -> 3802 ('perms -> sexp) -> ('a,'perms) t -> sexp 3803 end 3804 module Int : 3805 sig 3806 type nonrec -'perms t = (int,'perms) t 3807 include 3808 sig 3809 val t_of_sexp : 3810 (sexp -> 'perms) -> sexp -> 'perms t 3811 val sexp_of_t : 3812 ('perms -> sexp) -> 'perms t -> sexp 3813 end 3814 end 3815 end = 3816 struct 3817 type ('a,-'perms) t = 'a array 3818 let _ = fun (_ : ('a,'perms) t) -> () 3819 3820 let t_of_sexp : 3821 'a 'perms . 3822 (sexp -> 'a) -> 3823 (sexp -> 'perms) -> sexp -> ('a,'perms) t= 3824 let _tp_loc = "core_array.ml.Permissioned.t" in 3825 fun _of_a -> fun _of_perms -> fun t -> (array_of_sexp _of_a) t 3826 let _ = t_of_sexp 3827 let sexp_of_t : 3828 'a 'perms . 3829 ('a -> sexp) -> 3830 ('perms -> sexp) -> ('a,'perms) t -> sexp= 3831 fun _of_a -> fun _of_perms -> fun v -> (sexp_of_array _of_a) v 3832 let _ = sexp_of_t 3833 module Int = 3834 struct 3835 include T.Int 3836 type -'perms t = t_ 3837 let _ = fun (_ : 'perms t) -> () 3838 3839 let t_of_sexp : 3840 'perms . (sexp -> 'perms) -> sexp -> 'perms t= 3841 let _tp_loc = "core_array.ml.Permissioned.Int.t" in 3842 fun _of_perms -> fun t -> t__of_sexp t 3843 let _ = t_of_sexp 3844 let sexp_of_t : 3845 'perms . ('perms -> sexp) -> 'perms t -> sexp= 3846 fun _of_perms -> fun v -> sexp_of_t_ v 3847 let _ = sexp_of_t 3848 end 3849 end 3850type 'a foo = {x: 'a; y: int} 3851let r = {{x = 0; y = 0} with x = 0} 3852let r' : string foo = r 3853external foo : int = "%ignore";; 3854let _ = foo ();; 3855type 'a t = [`A of 'a t t] as 'a;; (* fails *) 3856 3857type 'a t = [`A of 'a t t];; (* fails *) 3858 3859type 'a t = [`A of 'a t t] constraint 'a = 'a t;; 3860 3861type 'a t = [`A of 'a t] constraint 'a = 'a t;; 3862 3863type 'a t = [`A of 'a] as 'a;; 3864 3865type 'a v = [`A of u v] constraint 'a = t and t = u and u = t;; (* fails *) 3866 3867type 'a t = 'a;; 3868let f (x : 'a t as 'a) = ();; (* fails *) 3869 3870let f (x : 'a t) (y : 'a) = x = y;; 3871 3872(* PR#6505 *) 3873module type PR6505 = sig 3874 type 'o is_an_object = < .. > as 'o 3875 and 'o abs constraint 'o = 'o is_an_object 3876 val abs : 'o is_an_object -> 'o abs 3877 val unabs : 'o abs -> 'o 3878end;; (* fails *) 3879(* PR#5835 *) 3880let f ~x = x + 1;; 3881f ?x:0;; 3882 3883(* PR#6352 *) 3884let foo (f : unit -> unit) = ();; 3885let g ?x () = ();; 3886foo ((); g);; 3887 3888(* PR#5748 *) 3889foo (fun ?opt () -> ()) ;; (* fails *) 3890(* PR#5907 *) 3891 3892type 'a t = 'a;; 3893let f (g : 'a list -> 'a t -> 'a) s = g s s;; 3894let f (g : 'a * 'b -> 'a t -> 'a) s = g s s;; 3895type ab = [ `A | `B ];; 3896let f (x : [`A]) = match x with #ab -> 1;; 3897let f x = ignore (match x with #ab -> 1); ignore (x : [`A]);; 3898let f x = ignore (match x with `A|`B -> 1); ignore (x : [`A]);; 3899 3900let f (x : [< `A | `B]) = match x with `A | `B | `C -> 0;; (* warn *) 3901let f (x : [`A | `B]) = match x with `A | `B | `C -> 0;; (* fail *) 3902 3903(* PR#6787 *) 3904let revapply x f = f x;; 3905 3906let f x (g : [< `Foo]) = 3907 let y = `Bar x, g in 3908 revapply y (fun ((`Bar i), _) -> i);; 3909(* f : 'a -> [< `Foo ] -> 'a *) 3910 3911let rec x = [| x |]; 1.;; 3912 3913let rec x = let u = [|y|] in 10. and y = 1.;; 3914type 'a t 3915type a 3916 3917let f : < .. > t -> unit = fun _ -> ();; 3918 3919let g : [< `b] t -> unit = fun _ -> ();; 3920 3921let h : [> `b] t -> unit = fun _ -> ();; 3922 3923let _ = fun (x : a t) -> f x;; 3924 3925let _ = fun (x : a t) -> g x;; 3926 3927let _ = fun (x : a t) -> h x;; 3928(* PR#7012 *) 3929 3930type t = [ 'A_name | `Hi ];; 3931 3932let f (x:'id_arg) = x;; 3933 3934let f (x:'Id_arg) = x;; 3935(* undefined labels *) 3936type t = {x:int;y:int};; 3937{x=3;z=2};; 3938fun {x=3;z=2} -> ();; 3939 3940(* mixed labels *) 3941{x=3; contents=2};; 3942 3943(* private types *) 3944type u = private {mutable u:int};; 3945{u=3};; 3946fun x -> x.u <- 3;; 3947 3948(* Punning and abbreviations *) 3949module M = struct 3950 type t = {x: int; y: int} 3951end;; 3952 3953let f {M.x; y} = x+y;; 3954let r = {M.x=1; y=2};; 3955let z = f r;; 3956 3957(* messages *) 3958type foo = { mutable y:int };; 3959let f (r: int) = r.y <- 3;; 3960 3961(* bugs *) 3962type foo = { y: int; z: int };; 3963type bar = { x: int };; 3964let f (r: bar) = ({ r with z = 3 } : foo) 3965 3966type foo = { x: int };; 3967let r : foo = { ZZZ.x = 2 };; 3968 3969(ZZZ.X : int option);; 3970 3971(* PR#5865 *) 3972let f (x : Complex.t) = x.Complex.z;; 3973(* PR#6394 *) 3974 3975module rec X : sig 3976 type t = int * bool 3977end = struct 3978 type t = A | B 3979 let f = function A | B -> 0 3980end;; 3981(* PR#6768 *) 3982 3983type _ prod = Prod : ('a * 'y) prod;; 3984 3985let f : type t. t prod -> _ = function Prod -> 3986 let module M = 3987 struct 3988 type d = d * d 3989 end 3990 in () 3991;; 3992let (a : M.a) = 2 3993let (b : M.b) = 2 3994let _ = A.a = B.b 3995module Std = struct module Hash = Hashtbl end;; 3996 3997open Std;; 3998module Hash1 : module type of Hash = Hash;; 3999module Hash2 : sig include (module type of Hash) end = Hash;; 4000let f1 (x : (_,_) Hash1.t) = (x : (_,_) Hashtbl.t);; 4001let f2 (x : (_,_) Hash2.t) = (x : (_,_) Hashtbl.t);; 4002 4003(* Another case, not using include *) 4004 4005module Std2 = struct module M = struct type t end end;; 4006module Std' = Std2;; 4007module M' : module type of Std'.M = Std2.M;; 4008let f3 (x : M'.t) = (x : Std2.M.t);; 4009 4010(* original report required Core_kernel: 4011module type S = sig 4012open Core_kernel.Std 4013 4014module Hashtbl1 : module type of Hashtbl 4015module Hashtbl2 : sig 4016 include (module type of Hashtbl) 4017end 4018 4019module Coverage : Core_kernel.Std.Hashable 4020 4021type types = unit constraint 'a Coverage.Table.t = (Coverage.t, 'a) Hashtbl1.t 4022type doesnt_type = unit 4023 constraint 'a Coverage.Table.t = (Coverage.t, 'a) Hashtbl2.t 4024end 4025*) 4026module type INCLUDING = sig 4027 include module type of List 4028 include module type of ListLabels 4029end 4030 4031module Including_typed: INCLUDING = struct 4032 include List 4033 include ListLabels 4034end 4035module X=struct 4036 module type SIG=sig type t=int val x:t end 4037 module F(Y:SIG) : SIG = struct type t=Y.t let x=Y.x end 4038end;; 4039module DUMMY=struct type t=int let x=2 end;; 4040let x = (3 : X.F(DUMMY).t);; 4041 4042module X2=struct 4043 module type SIG=sig type t=int val x:t end 4044 module F(Y:SIG)(Z:SIG) = struct 4045 type t=Y.t 4046 let x=Y.x 4047 type t'=Z.t 4048 let x'=Z.x 4049 end 4050end;; 4051let x = (3 : X2.F(DUMMY)(DUMMY).t);; 4052let x = (3 : X2.F(DUMMY)(DUMMY).t');; 4053module F (M : sig 4054 type 'a t 4055 type 'a u = string 4056 val f : unit -> _ u t 4057 end) = struct 4058 let t = M.f () 4059 end 4060type 't a = [ `A ] 4061type 't wrap = 't constraint 't = [> 't wrap a ] 4062type t = t a wrap 4063 4064module T = struct 4065 let foo : 't wrap -> 't wrap -> unit = fun _ _ -> () 4066 let bar : ('a a wrap as 'a) = `A 4067end 4068 4069module Good : sig 4070 val bar: t 4071 val foo: t -> t -> unit 4072end = T 4073 4074module Bad : sig 4075 val foo: t -> t -> unit 4076 val bar: t 4077end = T 4078module M : sig 4079 module type T 4080 module F (X : T) : sig end 4081end = struct 4082 module type T = sig end 4083 module F (X : T) = struct end 4084end 4085 4086module type T = M.T 4087 4088module F : functor (X : T) -> sig end = M.F 4089module type S = sig type t = { a : int; b : int; } end;; 4090let f (module M : S with type t = int) = { M.a = 0 };; 4091let flag = ref false 4092module F(S : sig module type T end) (A : S.T) (B : S.T) = 4093struct 4094 module X = (val if !flag then (module A) else (module B) : S.T) 4095end 4096 4097(* If the above were accepted, one could break soundness *) 4098module type S = sig type t val x : t end 4099module Float = struct type t = float let x = 0.0 end 4100module Int = struct type t = int let x = 0 end 4101 4102module M = F(struct module type T = S end) 4103 4104let () = flag := false 4105module M1 = M(Float)(Int) 4106 4107let () = flag := true 4108module M2 = M(Float)(Int) 4109 4110let _ = [| M2.X.x; M1.X.x |] 4111module type PR6513 = sig 4112module type S = sig type u end 4113 4114module type T = sig 4115 type 'a wrap 4116 type uri 4117end 4118 4119module Make: functor (Html5 : T with type 'a wrap = 'a) -> 4120 S with type u = < foo : Html5.uri > 4121end 4122 4123(* Requires -package tyxml 4124module type PR6513_orig = sig 4125module type S = 4126sig 4127 type t 4128 type u 4129end 4130 4131module Make: functor (Html5: Html5_sigs.T 4132 with type 'a Xml.wrap = 'a and 4133 type 'a wrap = 'a and 4134 type 'a list_wrap = 'a list) 4135 -> S with type t = Html5_types.div Html5.elt and 4136 type u = < foo: Html5.uri > 4137end 4138*) 4139module type S = sig 4140 include Set.S 4141 module E : sig val x : int end 4142end 4143 4144module Make(O : Set.OrderedType) : S with type elt = O.t = 4145 struct 4146 include Set.Make(O) 4147 module E = struct let x = 1 end 4148 end 4149 4150module rec A : Set.OrderedType = struct 4151 type t = int 4152 let compare = Pervasives.compare 4153end 4154and B : S = struct 4155 module C = Make(A) 4156 include C 4157end 4158module type S = sig 4159 module type T 4160 module X : T 4161end 4162 4163module F (X : S) = X.X 4164 4165module M = struct 4166 module type T = sig type t end 4167 module X = struct type t = int end 4168end 4169 4170type t = F(M).t 4171module Common0 = 4172 struct 4173 type msg = Msg 4174 4175 let handle_msg = ref (function _ -> failwith "Unable to handle message") 4176 let extend_handle f = 4177 let old = !handle_msg in 4178 handle_msg := f old 4179 4180 let q : _ Queue.t = Queue.create () 4181 let add msg = Queue.add msg q 4182 let handle_queue_messages () = Queue.iter !handle_msg q 4183 end 4184 4185let q' : Common0.msg Queue.t = Common0.q 4186 4187module Common = 4188 struct 4189 type msg = .. 4190 4191 let handle_msg = ref (function _ -> failwith "Unable to handle message") 4192 let extend_handle f = 4193 let old = !handle_msg in 4194 handle_msg := f old 4195 4196 let q : _ Queue.t = Queue.create () 4197 let add msg = Queue.add msg q 4198 let handle_queue_messages () = Queue.iter !handle_msg q 4199 end 4200 4201module M1 = 4202 struct 4203 type Common.msg += Reload of string | Alert of string 4204 4205 let handle fallback = function 4206 Reload s -> print_endline ("Reload "^s) 4207 | Alert s -> print_endline ("Alert "^s) 4208 | x -> fallback x 4209 4210 let () = Common.extend_handle handle 4211 let () = Common.add (Reload "config.file") 4212 let () = Common.add (Alert "Initialisation done") 4213 end 4214let should_reject = 4215 let table = Hashtbl.create 1 in 4216 fun x y -> Hashtbl.add table x y 4217type 'a t = 'a option 4218let is_some = function 4219 | None -> false 4220 | Some _ -> true 4221 4222let should_accept ?x () = is_some x 4223include struct 4224 let foo `Test = () 4225 let wrap f `Test = f 4226 let bar = wrap () 4227end 4228let f () = 4229 let module S = String in 4230 let module N = Map.Make(S) in 4231 N.add "sum" 41 N.empty;; 4232module X = struct module Y = struct module type S = sig type t end end end 4233 4234(* open X (* works! *) *) 4235module Y = X.Y 4236 4237type 'a arg_t = 'at constraint 'a = (module Y.S with type t = 'at) 4238type t = (module X.Y.S with type t = unit) 4239 4240let f (x : t arg_t) = () 4241 4242let () = f () 4243module type S = 4244sig 4245 type a 4246 type b 4247end 4248module Foo 4249 (Bar : S with type a = private [> `A]) 4250 (Baz : S with type b = private < b : Bar.b ; .. >) = 4251struct 4252end 4253module A = struct 4254 module type A_S = sig 4255 end 4256 4257 type t = (module A_S) 4258end 4259 4260module type S = sig type t end 4261 4262let f (type a) (module X : S with type t = a) = () 4263 4264let _ = f (module A) (* ok *) 4265 4266module A_annotated_alias : S with type t = (module A.A_S) = A 4267 4268let _ = f (module A_annotated_alias) (* ok *) 4269let _ = f (module A_annotated_alias : S with type t = (module A.A_S)) (* ok *) 4270 4271module A_alias = A 4272module A_alias_expanded = struct include A_alias end 4273 4274let _ = f (module A_alias_expanded : S with type t = (module A.A_S)) (* ok *) 4275let _ = f (module A_alias_expanded) (* ok *) 4276 4277let _ = f (module A_alias : S with type t = (module A.A_S)) (* doesn't type *) 4278let _ = f (module A_alias) (* doesn't type either *) 4279module Foo 4280 (Bar : sig type a = private [> `A ] end) 4281 (Baz : module type of struct include Bar end) = 4282struct 4283end 4284module Bazoinks = struct type a = [ `A ] end 4285module Bug = Foo(Bazoinks)(Bazoinks) 4286(* PR#6992, reported by Stephen Dolan *) 4287 4288type (_, _) eq = Eq : ('a, 'a) eq 4289let cast : type a b . (a, b) eq -> a -> b = fun Eq x -> x 4290 4291module Fix (F : sig type 'a f end) = struct 4292 type 'a fix = ('a, 'a F.f) eq 4293 let uniq (type a) (type b) (Eq : a fix) (Eq : b fix) : (a, b) eq = Eq 4294end 4295 4296(* This would allow: 4297module FixId = Fix (struct type 'a f = 'a end) 4298 let bad : (int, string) eq = FixId.uniq Eq Eq 4299 let _ = Printf.printf "Oh dear: %s" (cast bad 42) 4300*) 4301module M = struct 4302 module type S = sig type a val v : a end 4303 type 'a s = (module S with type a = 'a) 4304end 4305 4306module B = struct 4307 class type a = object method a : 'a. 'a M.s -> 'a end 4308end 4309 4310module M' = M 4311module B' = B 4312 4313class b : B.a = object 4314 method a : 'a. 'a M.s -> 'a = fun (type a) ((module X) : (module M.S with type 4315a = a)) -> X.v 4316end 4317 4318class b' : B.a = object 4319 method a : 'a. 'a M'.s -> 'a = fun (type a) ((module X) : (module M'.S with 4320type a = a)) -> X.v 4321end 4322module type FOO = sig type t end 4323module type BAR = 4324sig 4325 (* Works: module rec A : (sig include FOO with type t = < b:B.t > end) *) 4326 module rec A : (FOO with type t = < b:B.t >) 4327 and B : FOO 4328end 4329module A = struct module type S module S = struct end end 4330module F (_ : sig end) = struct module type S module S = A.S end 4331module M = struct end 4332module N = M 4333module G (X : F(N).S) : A.S = X 4334module F (_ : sig end) = struct module type S end 4335module M = struct end 4336module N = M 4337module G (X : F(N).S) : F(M).S = X 4338module M : sig 4339 type make_dec 4340 val add_dec: make_dec -> unit 4341end = struct 4342 type u 4343 4344 module Fast: sig 4345 type 'd t 4346 val create: unit -> 'd t 4347 module type S = sig 4348 module Data: sig type t end 4349 val key: Data.t t 4350 end 4351 module Register (D:S): sig end 4352 val attach: 'd t -> 'd -> unit 4353 end = struct 4354 type 'd t = unit 4355 let create () = () 4356 module type S = sig 4357 module Data: sig type t end 4358 val key: Data.t t 4359 end 4360 module Register (D:S) = struct end 4361 let attach _ _ = () 4362 end 4363 4364 type make_dec 4365 4366 module Dem = struct 4367 module Data = struct 4368 type t = make_dec 4369 end 4370 let key = Fast.create () 4371 end 4372 4373 module EDem = Fast.Register(Dem) 4374 4375 let add_dec dec = 4376 Fast.attach Dem.key dec 4377end 4378 4379(* simpler version *) 4380 4381module Simple = struct 4382 type 'a t 4383 module type S = sig 4384 module Data: sig type t end 4385 val key: Data.t t 4386 end 4387 module Register (D:S) = struct let key = D.key end 4388 module M = struct 4389 module Data = struct type t = int end 4390 let key : _ t = Obj.magic () 4391 end 4392end;; 4393module EM = Simple.Register(Simple.M);; 4394Simple.M.key;; 4395 4396module Simple2 = struct 4397 type 'a t 4398 module type S = sig 4399 module Data: sig type t end 4400 val key: Data.t t 4401 end 4402 module M = struct 4403 module Data = struct type t = int end 4404 let key : _ t = Obj.magic () 4405 end 4406 module Register (D:S) = struct let key = D.key end 4407 module EM = Simple.Register(Simple.M) 4408 let k : M.Data.t t = M.key 4409end;; 4410module rec M 4411 : sig external f : int -> int = "%identity" end 4412 = struct external f : int -> int = "%identity" end 4413(* with module *) 4414 4415module type S = sig type t and s = t end;; 4416module type S' = S with type t := int;; 4417 4418module type S = sig module rec M : sig end and N : sig end end;; 4419module type S' = S with module M := String;; 4420 4421(* with module type *) 4422(* 4423module type S = sig module type T module F(X:T) : T end;; 4424module type T0 = sig type t end;; 4425module type S1 = S with module type T = T0;; 4426module type S2 = S with module type T := T0;; 4427module type S3 = S with module type T := sig type t = int end;; 4428module H = struct 4429 include (Hashtbl : module type of Hashtbl with 4430 type statistics := Hashtbl.statistics 4431 and module type S := Hashtbl.S 4432 and module Make := Hashtbl.Make 4433 and module MakeSeeded := Hashtbl.MakeSeeded 4434 and module type SeededS := Hashtbl.SeededS 4435 and module type HashedType := Hashtbl.HashedType 4436 and module type SeededHashedType := Hashtbl.SeededHashedType) 4437end;; 4438*) 4439 4440(* A subtle problem appearing with -principal *) 4441type -'a t 4442class type c = object method m : [ `A ] t end;; 4443module M : sig val v : (#c as 'a) -> 'a end = 4444 struct let v x = ignore (x :> c); x end;; 4445 4446(* PR#4838 *) 4447 4448let id = let module M = struct end in fun x -> x;; 4449 4450(* PR#4511 *) 4451 4452let ko = let module M = struct end in fun _ -> ();; 4453 4454(* PR#5993 *) 4455 4456module M : sig type -'a t = private int end = 4457 struct type +'a t = private int end 4458;; 4459 4460(* PR#6005 *) 4461 4462module type A = sig type t = X of int end;; 4463type u = X of bool;; 4464module type B = A with type t = u;; (* fail *) 4465 4466(* PR#5815 *) 4467(* ---> duplicated exception name is now an error *) 4468 4469module type S = sig exception Foo of int exception Foo of bool end;; 4470 4471(* PR#6410 *) 4472 4473module F(X : sig end) = struct let x = 3 end;; 4474F.x;; (* fail *) 4475module C = Char;; 4476C.chr 66;; 4477 4478module C' : module type of Char = C;; 4479C'.chr 66;; 4480 4481module C3 = struct include Char end;; 4482C3.chr 66;; 4483 4484let f x = let module M = struct module L = List end in M.L.length x;; 4485let g x = let module L = List in L.length (L.map succ x);; 4486 4487module F(X:sig end) = Char;; 4488module C4 = F(struct end);; 4489C4.chr 66;; 4490 4491module G(X:sig end) = struct module M = X end;; (* does not alias X *) 4492module M = G(struct end);; 4493 4494module M' = struct 4495 module N = struct let x = 1 end 4496 module N' = N 4497end;; 4498M'.N'.x;; 4499 4500module M'' : sig module N' : sig val x : int end end = M';; 4501M''.N'.x;; 4502module M2 = struct include M' end;; 4503module M3 : sig module N' : sig val x : int end end = struct include M' end;; 4504M3.N'.x;; 4505module M3' : sig module N' : sig val x : int end end = M2;; 4506M3'.N'.x;; 4507 4508module M4 : sig module N' : sig val x : int end end = struct 4509 module N = struct let x = 1 end 4510 module N' = N 4511end;; 4512M4.N'.x;; 4513 4514module F(X:sig end) = struct 4515 module N = struct let x = 1 end 4516 module N' = N 4517end;; 4518module G : functor(X:sig end) -> sig module N' : sig val x : int end end = F;; 4519module M5 = G(struct end);; 4520M5.N'.x;; 4521 4522module M = struct 4523 module D = struct let y = 3 end 4524 module N = struct let x = 1 end 4525 module N' = N 4526end;; 4527 4528module M1 : sig module N : sig val x : int end module N' = N end = M;; 4529M1.N'.x;; 4530module M2 : sig module N' : sig val x : int end end = 4531 (M : sig module N : sig val x : int end module N' = N end);; 4532M2.N'.x;; 4533 4534open M;; 4535N'.x;; 4536 4537module M = struct 4538 module C = Char 4539 module C' = C 4540end;; 4541module M1 4542 : sig module C : sig val escaped : char -> string end module C' = C end 4543 = M;; (* sound, but should probably fail *) 4544M1.C'.escaped 'A';; 4545module M2 : sig module C' : sig val chr : int -> char end end = 4546 (M : sig module C : sig val chr : int -> char end module C' = C end);; 4547M2.C'.chr 66;; 4548 4549StdLabels.List.map;; 4550 4551module Q = Queue;; 4552exception QE = Q.Empty;; 4553try Q.pop (Q.create ()) with QE -> "Ok";; 4554 4555module type Complex = module type of Complex with type t = Complex.t;; 4556module M : sig module C : Complex end = struct module C = Complex end;; 4557 4558module C = Complex;; 4559C.one.Complex.re;; 4560include C;; 4561 4562module F(X:sig module C = Char end) = struct module C = X.C end;; 4563 4564(* Applicative functors *) 4565module S = String 4566module StringSet = Set.Make(String) 4567module SSet = Set.Make(S);; 4568let f (x : StringSet.t) = (x : SSet.t);; 4569 4570(* Also using include (cf. Leo's mail 2013-11-16) *) 4571module F (M : sig end) : sig type t end = struct type t = int end 4572module T = struct 4573 module M = struct end 4574 include F(M) 4575end;; 4576include T;; 4577let f (x : t) : T.t = x ;; 4578 4579(* PR#4049 *) 4580(* This works thanks to abbreviations *) 4581module A = struct 4582 module B = struct type t let compare x y = 0 end 4583 module S = Set.Make(B) 4584 let empty = S.empty 4585end 4586module A1 = A;; 4587A1.empty = A.empty;; 4588 4589(* PR#3476 *) 4590(* Does not work yet *) 4591module FF(X : sig end) = struct type t end 4592module M = struct 4593 module X = struct end 4594 module Y = FF (X) (* XXX *) 4595 type t = Y.t 4596end 4597module F (Y : sig type t end) (M : sig type t = Y.t end) = struct end;; 4598 4599module G = F (M.Y);; 4600(*module N = G (M);; 4601module N = F (M.Y) (M);;*) 4602 4603(* PR#6307 *) 4604 4605module A1 = struct end 4606module A2 = struct end 4607module L1 = struct module X = A1 end 4608module L2 = struct module X = A2 end;; 4609 4610module F (L : (module type of L1)) = struct end;; 4611 4612module F1 = F(L1);; (* ok *) 4613module F2 = F(L2);; (* should succeed too *) 4614 4615(* Counter example: why we need to be careful with PR#6307 *) 4616module Int = struct type t = int let compare = compare end 4617module SInt = Set.Make(Int) 4618type (_,_) eq = Eq : ('a,'a) eq 4619type wrap = W of (SInt.t, SInt.t) eq 4620 4621module M = struct 4622 module I = Int 4623 type wrap' = wrap = W of (Set.Make(Int).t, Set.Make(I).t) eq 4624end;; 4625module type S = module type of M;; (* keep alias *) 4626 4627module Int2 = struct type t = int let compare x y = compare y x end;; 4628module type S' = sig 4629 module I = Int2 4630 include S with module I := I 4631end;; (* fail *) 4632 4633(* (* if the above succeeded, one could break invariants *) 4634module rec M2 : S' = M2;; (* should succeed! (but this is bad) *) 4635 4636let M2.W eq = W Eq;; 4637 4638let s = List.fold_right SInt.add [1;2;3] SInt.empty;; 4639module SInt2 = Set.Make(Int2);; 4640let conv : type a b. (a,b) eq -> a -> b = fun Eq x -> x;; 4641let s' : SInt2.t = conv eq s;; 4642SInt2.elements s';; 4643SInt2.mem 2 s';; (* invariants are broken *) 4644*) 4645 4646(* Check behavior with submodules *) 4647module M = struct 4648 module N = struct module I = Int end 4649 module P = struct module I = N.I end 4650 module Q = struct 4651 type wrap' = wrap = W of (Set.Make(Int).t, Set.Make(P.I).t) eq 4652 end 4653end;; 4654module type S = module type of M ;; 4655 4656module M = struct 4657 module N = struct module I = Int end 4658 module P = struct module I = N.I end 4659 module Q = struct 4660 type wrap' = wrap = W of (Set.Make(Int).t, Set.Make(N.I).t) eq 4661 end 4662end;; 4663module type S = module type of M ;; 4664 4665(* PR#6365 *) 4666module type S = sig module M : sig type t val x : t end end;; 4667module H = struct type t = A let x = A end;; 4668module H' = H;; 4669module type S' = S with module M = H';; (* shouldn't introduce an alias *) 4670 4671(* PR#6376 *) 4672module type Alias = sig module N : sig end module M = N end;; 4673module F (X : sig end) = struct type t end;; 4674module type A = Alias with module N := F(List);; 4675module rec Bad : A = Bad;; 4676 4677(* Shinwell 2014-04-23 *) 4678module B = struct 4679 module R = struct 4680 type t = string 4681 end 4682 4683 module O = R 4684end 4685 4686module K = struct 4687 module E = B 4688 module N = E.O 4689end;; 4690 4691let x : K.N.t = "foo";; 4692 4693(* PR#6465 *) 4694 4695module M = struct type t = A module B = struct type u = B end end;; 4696module P : sig type t = M.t = A module B = M.B end = M;; (* should be ok *) 4697module P : sig type t = M.t = A module B = M.B end = struct include M end;; 4698 4699module type S = sig 4700 module M : sig module P : sig end end 4701 module Q = M 4702end;; 4703module type S = sig 4704 module M : sig module N : sig end module P : sig end end 4705 module Q : sig module N = M.N module P = M.P end 4706end;; 4707module R = struct 4708 module M = struct module N = struct end module P = struct end end 4709 module Q = M 4710end;; 4711module R' : S = R;; (* should be ok *) 4712 4713(* PR#6578 *) 4714 4715module M = struct let f x = x end 4716module rec R : sig module M : sig val f : 'a -> 'a end end = 4717 struct module M = M end;; 4718R.M.f 3;; 4719module rec R : sig module M = M end = struct module M = M end;; 4720R.M.f 3;; 4721open A 4722let f = 4723 L.map S.capitalize 4724 4725let () = 4726 L.iter print_endline (f ["jacques"; "garrigue"]) 4727 4728module C : sig module L : module type of List end = struct include A end 4729 4730(* The following introduces a (useless) dependency on A: 4731module C : sig module L : module type of List end = A 4732*) 4733 4734include D' 4735(* 4736let () = 4737 print_endline (string_of_int D'.M.y) 4738*) 4739open A 4740let f = 4741 L.map S.capitalize 4742 4743let () = 4744 L.iter print_endline (f ["jacques"; "garrigue"]) 4745 4746module C : sig module L : module type of List end = struct include A end 4747 4748(* The following introduces a (useless) dependency on A: 4749module C : sig module L : module type of List end = A 4750*) 4751 4752(* No dependency on D *) 4753let x = 3 4754module M = struct let y = 5 end 4755module type S = sig type u type t end;; 4756module type S' = sig type t = int type u = bool end;; 4757 4758(* ok to convert between structurally equal signatures, and parameters 4759 are inferred *) 4760let f (x : (module S with type t = 'a and type u = 'b)) = (x : (module S'));; 4761let g x = (x : (module S with type t = 'a and type u = 'b) :> (module S'));; 4762 4763(* with subtyping it is also ok to forget some types *) 4764module type S2 = sig type u type t type w end;; 4765let g2 x = (x : (module S2 with type t = 'a and type u = 'b) :> (module S'));; 4766let h x = (x : (module S2 with type t = 'a) :> (module S with type t = 'a));; 4767let f2 (x : (module S2 with type t = 'a and type u = 'b)) = 4768 (x : (module S'));; (* fail *) 4769let k (x : (module S2 with type t = 'a)) = 4770 (x : (module S with type t = 'a));; (* fail *) 4771 4772(* but you cannot forget values (no physical coercions) *) 4773module type S3 = sig type u type t val x : int end;; 4774let g3 x = 4775 (x : (module S3 with type t = 'a and type u = 'b) :> (module S'));; (* fail *) 4776(* Using generative functors *) 4777 4778(* Without type *) 4779module type S = sig val x : int end;; 4780let v = (module struct let x = 3 end : S);; 4781module F() = (val v);; (* ok *) 4782module G (X : sig end) : S = F ();; (* ok *) 4783module H (X : sig end) = (val v);; (* ok *) 4784 4785(* With type *) 4786module type S = sig type t val x : t end;; 4787let v = (module struct type t = int let x = 3 end : S);; 4788module F() = (val v);; (* ok *) 4789module G (X : sig end) : S = F ();; (* fail *) 4790module H() = F();; (* ok *) 4791 4792(* Alias *) 4793module U = struct end;; 4794module M = F(struct end);; (* ok *) 4795module M = F(U);; (* fail *) 4796 4797(* Cannot coerce between applicative and generative *) 4798module F1 (X : sig end) = struct end;; 4799module F2 : functor () -> sig end = F1;; (* fail *) 4800module F3 () = struct end;; 4801module F4 : functor (X : sig end) -> sig end = F3;; (* fail *) 4802 4803(* tests for shortened functor notation () *) 4804module X (X: sig end) (Y: sig end) = functor (Z: sig end) -> struct end;; 4805module Y = functor (X: sig end) (Y:sig end) -> functor (Z: sig end) -> 4806 struct end;; 4807module Z = functor (_: sig end) (_:sig end) (_: sig end) -> struct end;; 4808module GZ : functor (X: sig end) () (Z: sig end) -> sig end 4809 = functor (X: sig end) () (Z: sig end) -> struct end;; 4810module F (X : sig end) = struct type t = int end;; 4811type t = F(Does_not_exist).t;; 4812type expr = 4813 [ `Abs of string * expr 4814 | `App of expr * expr 4815 ] 4816 4817class type exp = 4818object 4819 method eval : (string, exp) Hashtbl.t -> expr 4820end;; 4821 4822class app e1 e2 : exp = 4823object 4824 val l = e1 4825 val r = e2 4826 method eval env = 4827 match l with 4828 | `Abs(var,body) -> 4829 Hashtbl.add env var r; 4830 body 4831 | _ -> `App(l,r); 4832end 4833 4834class virtual ['subject, 'event] observer = 4835 object 4836 method virtual notify : 'subject -> 'event -> unit 4837 end 4838 4839class ['event] subject = 4840 object (self : 'subject) 4841 val mutable observers = ([]: (('subject, 'event) observer) list) 4842 method add_observer obs = observers <- (obs :: observers) 4843 method notify_observers (e : 'event) = 4844 List.iter (fun x -> x#notify self e) observers 4845 end 4846 4847type id = int 4848 4849class entity (id : id) = 4850 object 4851 val ent_destroy_subject = new subject 4852 method destroy_subject : (id) subject = ent_destroy_subject 4853 4854 method entity_id = id 4855 end 4856 4857class ['entity] entity_container = 4858 object (self) 4859 inherit ['entity, id] observer as observer 4860 4861 method add_entity (e : 'entity) = 4862 e#destroy_subject#add_observer (self) 4863 4864 method notify _ id = () 4865 end 4866 4867let f (x : entity entity_container) = () 4868 4869(* 4870class world = 4871 object 4872 val entity_container : entity entity_container = new entity_container 4873 4874 method add_entity (s : entity) = 4875 entity_container#add_entity (s :> entity) 4876 4877 end 4878*) 4879(* Two v's in the same class *) 4880class c v = object initializer print_endline v val v = 42 end;; 4881new c "42";; 4882 4883(* Two hidden v's in the same class! *) 4884class c (v : int) = 4885 object 4886 method v0 = v 4887 inherit ((fun v -> object method v : string = v end) "42") 4888 end;; 4889(new c 42)#v0;; 4890class virtual ['a] c = 4891object (s : 'a) 4892 method virtual m : 'b 4893end 4894 4895let o = 4896 object (s :'a) 4897 inherit ['a] c 4898 method m = 42 4899 end 4900module M : 4901 sig 4902 class x : int -> object method m : int end 4903 end 4904= 4905struct 4906 class x _ = object 4907 method m = 42 4908 end 4909end;; 4910module M : sig class c : 'a -> object val x : 'b end end = 4911 struct class c x = object val x = x end end 4912 4913class c (x : int) = object inherit M.c x method x : bool = x end 4914 4915let r = (new c 2)#x;; 4916(* test.ml *) 4917class alfa = object(_:'self) 4918 method x: 'a. ('a, out_channel, unit) format -> 'a = Printf.printf 4919end 4920 4921class bravo a = object 4922 val y = (a :> alfa) 4923 initializer y#x "bravo initialized" 4924end 4925 4926class charlie a = object 4927 inherit bravo a 4928 initializer y#x "charlie initialized" 4929end 4930(* The module begins *) 4931exception Out_of_range 4932 4933class type ['a] cursor = 4934 object 4935 method get : 'a 4936 method incr : unit -> unit 4937 method is_last : bool 4938 end 4939 4940class type ['a] storage = 4941 object ('self) 4942 method first : 'a cursor 4943 method len : int 4944 method nth : int -> 'a cursor 4945 method copy : 'self 4946 method sub : int -> int -> 'self 4947 method concat : 'a storage -> 'self 4948 method fold : 'b. ('a -> int -> 'b -> 'b) -> 'b -> 'b 4949 method iter : ('a -> unit) -> unit 4950 end 4951 4952class virtual ['a, 'cursor] storage_base = 4953 object (self : 'self) 4954 constraint 'cursor = 'a #cursor 4955 method virtual first : 'cursor 4956 method virtual len : int 4957 method virtual copy : 'self 4958 method virtual sub : int -> int -> 'self 4959 method virtual concat : 'a storage -> 'self 4960 method fold : 'b. ('a -> int -> 'b -> 'b) -> 'b -> 'b = fun f a0 -> 4961 let cur = self#first in 4962 let rec loop count a = 4963 if count >= self#len then a else 4964 let a' = f cur#get count a in 4965 cur#incr (); loop (count + 1) a' 4966 in 4967 loop 0 a0 4968 method iter proc = 4969 let p = self#first in 4970 for i = 0 to self#len - 2 do proc p#get; p#incr () done; 4971 if self#len > 0 then proc p#get else () 4972 end 4973 4974class type ['a] obj_input_channel = 4975 object 4976 method get : unit -> 'a 4977 method close : unit -> unit 4978 end 4979 4980class type ['a] obj_output_channel = 4981 object 4982 method put : 'a -> unit 4983 method flush : unit -> unit 4984 method close : unit -> unit 4985 end 4986 4987module UChar = 4988struct 4989 4990 type t = int 4991 4992 let highest_bit = 1 lsl 30 4993 let lower_bits = highest_bit - 1 4994 4995 let char_of c = 4996 try Char.chr c with Invalid_argument _ -> raise Out_of_range 4997 4998 let of_char = Char.code 4999 5000 let code c = 5001 if c lsr 30 = 0 5002 then c 5003 else raise Out_of_range 5004 5005 let chr n = 5006 if n >= 0 && (n lsr 31 = 0) then n else raise Out_of_range 5007 5008 let uint_code c = c 5009 let chr_of_uint n = n 5010 5011end 5012 5013type uchar = UChar.t 5014 5015let int_of_uchar u = UChar.uint_code u 5016let uchar_of_int n = UChar.chr_of_uint n 5017 5018class type ucursor = [uchar] cursor 5019 5020class type ustorage = [uchar] storage 5021 5022class virtual ['ucursor] ustorage_base = [uchar, 'ucursor] storage_base 5023 5024module UText = 5025struct 5026 5027(* the internal representation is UCS4 with big endian*) 5028(* The most significant digit appears first. *) 5029let get_buf s i = 5030 let n = Char.code s.[i] in 5031 let n = (n lsl 8) lor (Char.code s.[i + 1]) in 5032 let n = (n lsl 8) lor (Char.code s.[i + 2]) in 5033 let n = (n lsl 8) lor (Char.code s.[i + 3]) in 5034 UChar.chr_of_uint n 5035 5036let set_buf s i u = 5037 let n = UChar.uint_code u in 5038 begin 5039 s.[i] <- Char.chr (n lsr 24); 5040 s.[i + 1] <- Char.chr (n lsr 16 lor 0xff); 5041 s.[i + 2] <- Char.chr (n lsr 8 lor 0xff); 5042 s.[i + 3] <- Char.chr (n lor 0xff); 5043 end 5044 5045let init_buf buf pos init = 5046 if init#len = 0 then () else 5047 let cur = init#first in 5048 for i = 0 to init#len - 2 do 5049 set_buf buf (pos + i lsl 2) (cur#get); cur#incr () 5050 done; 5051 set_buf buf (pos + (init#len - 1) lsl 2) (cur#get) 5052 5053let make_buf init = 5054 let s = String.create (init#len lsl 2) in 5055 init_buf s 0 init; s 5056 5057class text_raw buf = 5058 object (self : 'self) 5059 inherit [cursor] ustorage_base 5060 val contents = buf 5061 method first = new cursor (self :> text_raw) 0 5062 method len = (String.length contents) / 4 5063 method get i = get_buf contents (4 * i) 5064 method nth i = new cursor (self :> text_raw) i 5065 method copy = {< contents = String.copy contents >} 5066 method sub pos len = 5067 {< contents = String.sub contents (pos * 4) (len * 4) >} 5068 method concat (text : ustorage) = 5069 let buf = String.create (String.length contents + 4 * text#len) in 5070 String.blit contents 0 buf 0 (String.length contents); 5071 init_buf buf (String.length contents) text; 5072 {< contents = buf >} 5073 end 5074and cursor text i = 5075 object 5076 val contents = text 5077 val mutable pos = i 5078 method get = contents#get pos 5079 method incr () = pos <- pos + 1 5080 method is_last = (pos + 1 >= contents#len) 5081 end 5082 5083class string_raw buf = 5084 object 5085 inherit text_raw buf 5086 method set i u = set_buf contents (4 * i) u 5087 end 5088 5089class text init = text_raw (make_buf init) 5090class string init = string_raw (make_buf init) 5091 5092let of_string s = 5093 let buf = String.make (4 * String.length s) '\000' in 5094 for i = 0 to String.length s - 1 do 5095 buf.[4 * i] <- s.[i] 5096 done; 5097 new text_raw buf 5098 5099let make len u = 5100 let s = String.create (4 * len) in 5101 for i = 0 to len - 1 do set_buf s (4 * i) u done; 5102 new string_raw s 5103 5104let create len = make len (UChar.chr 0) 5105 5106let copy s = s#copy 5107 5108let sub s start len = s#sub start len 5109 5110let fill s start len u = 5111 for i = start to start + len - 1 do s#set i u done 5112 5113let blit src srcoff dst dstoff len = 5114 for i = 0 to len - 1 do 5115 let u = src#get (srcoff + i) in 5116 dst#set (dstoff + i) u 5117 done 5118 5119let concat s1 s2 = s1#concat (s2 (* : #ustorage *) :> uchar storage) 5120 5121let iter proc s = s#iter proc 5122end 5123class type foo_t = 5124 object 5125 method foo: string 5126 end 5127 5128type 'a name = 5129 Foo: foo_t name 5130 | Int: int name 5131;; 5132 5133class foo = 5134 object(self) 5135 method foo = "foo" 5136 method cast = 5137 function 5138 Foo -> (self :> <foo : string>) 5139 end 5140;; 5141 5142class foo: foo_t = 5143 object(self) 5144 method foo = "foo" 5145 method cast: type a. a name -> a = 5146 function 5147 Foo -> (self :> foo_t) 5148 | _ -> raise Exit 5149 end 5150;; 5151class type c = object end;; 5152module type S = sig class c: c end;; 5153class virtual name = 5154object 5155end 5156 5157and func (args_ty, ret_ty) = 5158object(self) 5159 inherit name 5160 5161 val mutable memo_args = None 5162 5163 method arguments = 5164 match memo_args with 5165 | Some xs -> xs 5166 | None -> 5167 let args = List.map (fun ty -> new argument(self, ty)) args_ty in 5168 memo_args <- Some args; args 5169end 5170 5171and argument (func, ty) = 5172object 5173 inherit name 5174end 5175;; 5176let f (x: #M.foo) = 0;; 5177class type ['e] t = object('s) 5178 method update : 'e -> 's 5179end;; 5180 5181module type S = sig 5182 class base : 'e -> ['e] t 5183end;; 5184type 'par t = 'par 5185module M : sig val x : <m : 'a. 'a> end = 5186 struct let x : <m : 'a. 'a t> = Obj.magic () end 5187 5188let ident v = v 5189class alias = object method alias : 'a . 'a t -> 'a = ident end 5190module Classdef = struct 5191 class virtual ['a, 'b, 'c] cl0 = 5192 object 5193 constraint 'c = < m : 'a -> 'b -> int; .. > 5194 end 5195 5196 class virtual ['a, 'b] cl1 = 5197 object 5198 method virtual raise_trouble : int -> 'a 5199 method virtual m : 'a -> 'b -> int 5200 end 5201 5202 class virtual ['a, 'b] cl2 = 5203 object 5204 method virtual as_cl0 : ('a, 'b, ('a, 'b) cl1) cl0 5205 end 5206end 5207 5208type refer1 = < poly : 'a 'b 'c . (('b, 'c) #Classdef.cl2 as 'a) > 5209type refer2 = < poly : 'a 'b 'c . (('b, 'c) #Classdef.cl2 as 'a) > 5210 5211(* Actually this should succeed ... *) 5212let f (x : refer1) = (x : refer2) 5213module Classdef = struct 5214 class virtual ['a, 'b, 'c] cl0 = 5215 object 5216 constraint 'c = < m : 'a -> 'b -> int; .. > 5217 end 5218 5219 class virtual ['a, 'b] cl1 = 5220 object 5221 method virtual raise_trouble : int -> 'a 5222 method virtual m : 'a -> 'b -> int 5223 end 5224 5225 class virtual ['a, 'b] cl2 = 5226 object 5227 method virtual as_cl0 : ('a, 'b, ('a, 'b) cl1) cl0 5228 end 5229end 5230 5231module M : sig 5232 type refer = { poly : 'a 'b 'c . (('b, 'c) #Classdef.cl2 as 'a) } 5233end = struct 5234 type refer = { poly : 'a 'b 'c . (('b, 'c) #Classdef.cl2 as 'a) } 5235end 5236(* 5237 ocamlc -c pr3918a.mli pr3918b.mli 5238 rm -f pr3918a.cmi 5239 ocamlc -c pr3918c.ml 5240*) 5241 5242open Pr3918b 5243 5244let f x = (x : 'a vlist :> 'b vlist) 5245let f (x : 'a vlist) = (x : 'b vlist) 5246module type Poly = sig 5247 type 'a t = 'a constraint 'a = [> ] 5248end 5249 5250module Combine (A : Poly) (B : Poly) = struct 5251 type ('a, 'b) t = 'a A.t constraint 'a = 'b B.t 5252end 5253 5254module C = Combine 5255 (struct type 'a t = 'a constraint 'a = [> ] end) 5256 (struct type 'a t = 'a constraint 'a = [> ] end) 5257module type Priv = sig 5258 type t = private int 5259end 5260 5261module Make (Unit:sig end): Priv = struct type t = int end 5262 5263module A = Make (struct end) 5264 5265module type Priv' = sig 5266 type t = private [> `A] 5267end 5268 5269module Make' (Unit:sig end): Priv' = struct type t = [`A] end 5270 5271module A' = Make' (struct end) 5272(* PR5057 *) 5273 5274module TT = struct 5275 module IntSet = Set.Make(struct type t = int let compare = compare end) 5276end 5277 5278let () = 5279 let f flag = 5280 let module T = TT in 5281 let _ = match flag with `A -> 0 | `B r -> r in 5282 let _ = match flag with `A -> T.IntSet.mem | `B r -> r in 5283 () 5284 in 5285 f `A 5286(* This one should fail *) 5287 5288let f flag = 5289 let module T = Set.Make(struct type t = int let compare = compare end) in 5290 let _ = match flag with `A -> 0 | `B r -> r in 5291 let _ = match flag with `A -> T.mem | `B r -> r in 5292 () 5293module type S = sig 5294 type +'a t 5295 5296 val foo : [`A] t -> unit 5297 val bar : [< `A | `B] t -> unit 5298end 5299 5300module Make(T : S) = struct 5301 let f x = 5302 T.foo x; 5303 T.bar x; 5304 (x :> [`A | `C] T.t) 5305end 5306type 'a termpc = 5307 [`And of 'a * 'a 5308 |`Or of 'a * 'a 5309 |`Not of 'a 5310 |`Atom of string 5311 ] 5312 5313type 'a termk = 5314 [`Dia of 'a 5315 |`Box of 'a 5316 |'a termpc 5317 ] 5318 5319module type T = sig 5320 type term 5321 val map : (term -> term) -> term -> term 5322 val nnf : term -> term 5323 val nnf_not : term -> term 5324end 5325 5326module Fpc(X : T with type term = private [> 'a termpc] as 'a) = 5327 struct 5328 type term = X.term termpc 5329 let nnf = function 5330 |`Not(`Atom _) as x -> x 5331 |`Not x -> X.nnf_not x 5332 | x -> X.map X.nnf x 5333 let map f : term -> X.term = function 5334 |`Not x -> `Not (f x) 5335 |`And(x,y) -> `And (f x, f y) 5336 |`Or (x,y) -> `Or (f x, f y) 5337 |`Atom _ as x -> x 5338 let nnf_not : term -> _ = function 5339 |`Not x -> X.nnf x 5340 |`And(x,y) -> `Or (X.nnf_not x, X.nnf_not y) 5341 |`Or (x,y) -> `And (X.nnf_not x, X.nnf_not y) 5342 |`Atom _ as x -> `Not x 5343 end 5344 5345module Fk(X : T with type term = private [> 'a termk] as 'a) = 5346 struct 5347 type term = X.term termk 5348 module Pc = Fpc(X) 5349 let map f : term -> _ = function 5350 |`Dia x -> `Dia (f x) 5351 |`Box x -> `Box (f x) 5352 |#termpc as x -> Pc.map f x 5353 let nnf = Pc.nnf 5354 let nnf_not : term -> _ = function 5355 |`Dia x -> `Box (X.nnf_not x) 5356 |`Box x -> `Dia (X.nnf_not x) 5357 |#termpc as x -> Pc.nnf_not x 5358 end 5359type untyped;; 5360type -'a typed = private untyped;; 5361type -'typing wrapped = private sexp 5362and +'a t = 'a typed wrapped 5363and sexp = private untyped wrapped;; 5364class type ['a] s3 = object 5365 val underlying : 'a t 5366end;; 5367class ['a] s3object r : ['a] s3 = object 5368 val underlying = r 5369end;; 5370module M (T:sig type t end) 5371 = struct type t = private { t : T.t } end 5372module P 5373 = struct 5374 module T = struct type t end 5375 module R = M(T) 5376 end 5377module Foobar : sig 5378 type t = private int 5379end = struct 5380 type t = int 5381end;; 5382 5383module F0 : sig type t = private int end = Foobar;; 5384 5385let f (x : F0.t) = (x : Foobar.t);; (* fails *) 5386 5387module F = Foobar;; 5388 5389let f (x : F.t) = (x : Foobar.t);; 5390 5391module M = struct type t = <m:int> end;; 5392module M1 : sig type t = private <m:int; ..> end = M;; 5393module M2 : sig type t = private <m:int; ..> end = M1;; 5394fun (x : M1.t) -> (x : M2.t);; (* fails *) 5395 5396module M3 : sig type t = private M1.t end = M1;; 5397fun x -> (x : M3.t :> M1.t);; 5398fun x -> (x : M3.t :> M.t);; 5399module M4 : sig type t = private M3.t end = M2;; (* fails *) 5400module M4 : sig type t = private M3.t end = M;; (* fails *) 5401module M4 : sig type t = private M3.t end = M1;; (* might be ok *) 5402module M5 : sig type t = private M1.t end = M3;; 5403module M6 : sig type t = private < n:int; .. > end = M1;; (* fails *) 5404 5405module Bar : sig type t = private Foobar.t val f : int -> t end = 5406 struct type t = int let f (x : int) = (x : t) end;; (* must fail *) 5407 5408module M : sig 5409 type t = private T of int 5410 val mk : int -> t 5411end = struct 5412 type t = T of int 5413 let mk x = T(x) 5414end;; 5415 5416module M1 : sig 5417 type t = M.t 5418 val mk : int -> t 5419end = struct 5420 type t = M.t 5421 let mk = M.mk 5422end;; 5423 5424module M2 : sig 5425 type t = M.t 5426 val mk : int -> t 5427end = struct 5428 include M 5429end;; 5430 5431module M3 : sig 5432 type t = M.t 5433 val mk : int -> t 5434end = M;; 5435 5436module M4 : sig 5437 type t = M.t = T of int 5438 val mk : int -> t 5439 end = M;; 5440(* Error: The variant or record definition does not match that of type M.t *) 5441 5442module M5 : sig 5443 type t = M.t = private T of int 5444 val mk : int -> t 5445end = M;; 5446 5447module M6 : sig 5448 type t = private T of int 5449 val mk : int -> t 5450end = M;; 5451 5452module M' : sig 5453 type t_priv = private T of int 5454 type t = t_priv 5455 val mk : int -> t 5456end = struct 5457 type t_priv = T of int 5458 type t = t_priv 5459 let mk x = T(x) 5460end;; 5461 5462module M3' : sig 5463 type t = M'.t 5464 val mk : int -> t 5465end = M';; 5466 5467module M : sig type 'a t = private T of 'a end = 5468 struct type 'a t = T of 'a end;; 5469 5470module M1 : sig type 'a t = 'a M.t = private T of 'a end = 5471 struct type 'a t = 'a M.t = private T of 'a end;; 5472 5473(* PR#6090 *) 5474module Test = struct type t = private A end 5475module Test2 : module type of Test with type t = Test.t = Test;; 5476let f (x : Test.t) = (x : Test2.t);; 5477let f Test2.A = ();; 5478let a = Test2.A;; (* fail *) 5479(* The following should fail from a semantical point of view, 5480 but allow it for backward compatibility *) 5481module Test2 : module type of Test with type t = private Test.t = Test;; 5482 5483(* PR#6331 *) 5484type t = private < x : int; .. > as 'a;; 5485type t = private (< x : int; .. > as 'a) as 'a;; 5486type t = private < x : int > as 'a;; 5487type t = private (< x : int > as 'a) as 'b;; 5488type 'a t = private < x : int; .. > as 'a;; 5489type 'a t = private 'a constraint 'a = < x : int; .. >;; 5490(* Bad (t = t) *) 5491module rec A : sig type t = A.t end = struct type t = A.t end;; 5492(* Bad (t = t) *) 5493module rec A : sig type t = B.t end = struct type t = B.t end 5494 and B : sig type t = A.t end = struct type t = A.t end;; 5495(* OK (t = int) *) 5496module rec A : sig type t = B.t end = struct type t = B.t end 5497 and B : sig type t = int end = struct type t = int end;; 5498(* Bad (t = int * t) *) 5499module rec A : sig type t = int * A.t end = struct type t = int * A.t end;; 5500(* Bad (t = t -> int) *) 5501module rec A : sig type t = B.t -> int end = struct type t = B.t -> int end 5502 and B : sig type t = A.t end = struct type t = A.t end;; 5503(* OK (t = <m:t>) *) 5504module rec A : sig type t = <m:B.t> end = struct type t = <m:B.t> end 5505 and B : sig type t = A.t end = struct type t = A.t end;; 5506(* Bad (not regular) *) 5507module rec A : sig type 'a t = <m: 'a list A.t> end 5508 = struct type 'a t = <m: 'a list A.t> end;; 5509(* Bad (not regular) *) 5510module rec A : sig type 'a t = <m: 'a list B.t; n: 'a array B.t> end 5511 = struct type 'a t = <m: 'a list B.t; n: 'a array B.t> end 5512 and B : sig type 'a t = 'a A.t end = struct type 'a t = 'a A.t end;; 5513(* Bad (not regular) *) 5514module rec A : sig type 'a t = 'a B.t end 5515 = struct type 'a t = 'a B.t end 5516 and B : sig type 'a t = <m: 'a list A.t; n: 'a array A.t> end 5517 = struct type 'a t = <m: 'a list A.t; n: 'a array A.t> end;; 5518(* OK *) 5519module rec A : sig type 'a t = 'a array B.t * 'a list B.t end 5520 = struct type 'a t = 'a array B.t * 'a list B.t end 5521 and B : sig type 'a t = <m: 'a B.t> end 5522 = struct type 'a t = <m: 'a B.t> end;; 5523(* Bad (not regular) *) 5524module rec A : sig type 'a t = 'a list B.t end 5525 = struct type 'a t = 'a list B.t end 5526 and B : sig type 'a t = <m: 'a array B.t> end 5527 = struct type 'a t = <m: 'a array B.t> end;; 5528(* Bad (not regular) *) 5529module rec M : 5530 sig 5531 class ['a] c : 'a -> object 5532 method map : ('a -> 'b) -> 'b M.c 5533 end 5534 end 5535 = struct 5536 class ['a] c (x : 'a) = object 5537 method map : 'b. ('a -> 'b) -> 'b M.c 5538 = fun f -> new M.c (f x) 5539 end 5540 end;; 5541(* OK *) 5542class type [ 'node ] extension = object method node : 'node end 5543and [ 'ext ] node = object constraint 'ext = 'ext node #extension [@id] end 5544class x = object method node : x node = assert false end 5545type t = x node;; 5546(* Bad - PR 4261 *) 5547 5548module PR_4261 = struct 5549 module type S = 5550 sig 5551 type t 5552 end 5553 5554 module type T = 5555 sig 5556 module D : S 5557 type t = D.t 5558 end 5559 5560 module rec U : T with module D = U' = U 5561 and U' : S with type t = U'.t = U 5562end;; 5563(* Bad - PR 4512 *) 5564module type S' = sig type t = int end 5565module rec M : S' with type t = M.t = struct type t = M.t end;; 5566(* PR#4450 *) 5567 5568module PR_4450_1 = struct 5569 module type MyT = sig type 'a t = Succ of 'a t end 5570 module MyMap(X : MyT) = X 5571 module rec MyList : MyT = MyMap(MyList) 5572end;; 5573 5574module PR_4450_2 = struct 5575 module type MyT = sig 5576 type 'a wrap = My of 'a t 5577 and 'a t = private < map : 'b. ('a -> 'b) ->'b wrap; .. > 5578 val create : 'a list -> 'a t 5579 end 5580 module MyMap(X : MyT) = struct 5581 include X 5582 class ['a] c l = object (self) 5583 method map : 'b. ('a -> 'b) -> 'b wrap = 5584 fun f -> My (create (List.map f l)) 5585 end 5586 end 5587 module rec MyList : sig 5588 type 'a wrap = My of 'a t 5589 and 'a t = < map : 'b. ('a -> 'b) ->'b wrap > 5590 val create : 'a list -> 'a t 5591 end = struct 5592 include MyMap(MyList) 5593 let create l = new c l 5594 end 5595end;; 5596(* A synthetic example of bootstrapped data structure 5597 (suggested by J-C Filliatre) *) 5598 5599module type ORD = sig 5600 type t 5601 val compare : t -> t -> int 5602end 5603 5604module type SET = sig 5605 type elt 5606 type t 5607 val iter : (elt -> unit) -> t -> unit 5608end 5609 5610type 'a tree = E | N of 'a tree * 'a * 'a tree 5611 5612module Bootstrap2 5613 (MakeDiet : functor (X: ORD) -> SET with type t = X.t tree and type elt = X.t) 5614 : SET with type elt = int = 5615struct 5616 5617 type elt = int 5618 5619 module rec Elt : sig 5620 type t = I of int * int | D of int * Diet.t * int 5621 val compare : t -> t -> int 5622 val iter : (int -> unit) -> t -> unit 5623 end = 5624 struct 5625 type t = I of int * int | D of int * Diet.t * int 5626 let compare x1 x2 = 0 5627 let rec iter f = function 5628 | I (l, r) -> for i = l to r do f i done 5629 | D (_, d, _) -> Diet.iter (iter f) d 5630 end 5631 5632 and Diet : SET with type t = Elt.t tree and type elt = Elt.t = MakeDiet(Elt) 5633 5634 type t = Diet.t 5635 let iter f = Diet.iter (Elt.iter f) 5636end 5637(* PR 4470: simplified from OMake's sources *) 5638 5639module rec DirElt 5640 : sig 5641 type t = DirRoot | DirSub of DirHash.t 5642 end 5643 = struct 5644 type t = DirRoot | DirSub of DirHash.t 5645 end 5646 5647and DirCompare 5648 : sig 5649 type t = DirElt.t 5650 end 5651 = struct 5652 type t = DirElt.t 5653 end 5654 5655and DirHash 5656 : sig 5657 type t = DirElt.t list 5658 end 5659 = struct 5660 type t = DirCompare.t list 5661 end 5662(* PR 4758, PR 4266 *) 5663 5664module PR_4758 = struct 5665 module type S = sig end 5666 module type Mod = sig 5667 module Other : S 5668 end 5669 module rec A : S = struct end 5670 and C : sig include Mod with module Other = A end = struct 5671 module Other = A 5672 end 5673 module C' = C (* check that we can take an alias *) 5674 module F(X:sig end) = struct type t end 5675 let f (x : F(C).t) = (x : F(C').t) 5676end 5677(* PR 4557 *) 5678module PR_4557 = struct 5679 module F ( X : Set.OrderedType ) = struct 5680 module rec Mod : sig 5681 module XSet : 5682 sig 5683 type elt = X.t 5684 type t = Set.Make( X ).t 5685 end 5686 module XMap : 5687 sig 5688 type key = X.t 5689 type 'a t = 'a Map.Make(X).t 5690 end 5691 type elt = X.t 5692 type t = XSet.t XMap.t 5693 val compare: t -> t -> int 5694 end 5695 = 5696 struct 5697 module XSet = Set.Make( X ) 5698 module XMap = Map.Make( X ) 5699 5700 type elt = X.t 5701 type t = XSet.t XMap.t 5702 let compare = (fun x y -> 0) 5703 end 5704 and ModSet : Set.S with type elt = Mod.t = Set.Make( Mod ) 5705 end 5706end 5707module F ( X : Set.OrderedType ) = struct 5708 module rec Mod : sig 5709 module XSet : 5710 sig 5711 type elt = X.t 5712 type t = Set.Make( X ).t 5713 end 5714 module XMap : 5715 sig 5716 type key = X.t 5717 type 'a t = 'a Map.Make(X).t 5718 end 5719 type elt = X.t 5720 type t = XSet.t XMap.t 5721 val compare: t -> t -> int 5722 end 5723 = 5724 struct 5725 module XSet = Set.Make( X ) 5726 module XMap = Map.Make( X ) 5727 5728 type elt = X.t 5729 type t = XSet.t XMap.t 5730 let compare = (fun x y -> 0) 5731 end 5732 and ModSet : Set.S with type elt = Mod.t = Set.Make( Mod ) 5733end 5734(* Tests for recursive modules *) 5735 5736let test number result expected = 5737 if result = expected 5738 then Printf.printf "Test %d passed.\n" number 5739 else Printf.printf "Test %d FAILED.\n" number; 5740 flush stdout 5741 5742(* Tree of sets *) 5743 5744module rec A 5745 : sig 5746 type t = Leaf of int | Node of ASet.t 5747 val compare: t -> t -> int 5748 end 5749 = struct 5750 type t = Leaf of int | Node of ASet.t 5751 let compare x y = 5752 match (x,y) with 5753 (Leaf i, Leaf j) -> Pervasives.compare i j 5754 | (Leaf i, Node t) -> -1 5755 | (Node s, Leaf j) -> 1 5756 | (Node s, Node t) -> ASet.compare s t 5757 end 5758 5759and ASet : Set.S with type elt = A.t = Set.Make(A) 5760;; 5761 5762let _ = 5763 let x = A.Node (ASet.add (A.Leaf 3) (ASet.singleton (A.Leaf 2))) in 5764 let y = A.Node (ASet.add (A.Leaf 1) (ASet.singleton x)) in 5765 test 10 (A.compare x x) 0; 5766 test 11 (A.compare x (A.Leaf 3)) 1; 5767 test 12 (A.compare (A.Leaf 0) x) (-1); 5768 test 13 (A.compare y y) 0; 5769 test 14 (A.compare x y) 1 5770;; 5771 5772(* Simple value recursion *) 5773 5774module rec Fib 5775 : sig val f : int -> int end 5776 = struct let f x = if x < 2 then 1 else Fib.f(x-1) + Fib.f(x-2) end 5777;; 5778 5779let _ = 5780 test 20 (Fib.f 10) 89 5781;; 5782 5783(* Update function by infix *) 5784 5785module rec Fib2 5786 : sig val f : int -> int end 5787 = struct let rec g x = Fib2.f(x-1) + Fib2.f(x-2) 5788 and f x = if x < 2 then 1 else g x 5789 end 5790;; 5791 5792let _ = 5793 test 21 (Fib2.f 10) 89 5794;; 5795 5796(* Early application *) 5797 5798let _ = 5799 let res = 5800 try 5801 let module A = 5802 struct 5803 module rec Bad 5804 : sig val f : int -> int end 5805 = struct let f = let y = Bad.f 5 in fun x -> x+y end 5806 end in 5807 false 5808 with Undefined_recursive_module _ -> 5809 true in 5810 test 30 res true 5811;; 5812 5813(* Early strict evaluation *) 5814 5815(* 5816module rec Cyclic 5817 : sig val x : int end 5818 = struct let x = Cyclic.x + 1 end 5819;; 5820*) 5821 5822(* Reordering of evaluation based on dependencies *) 5823 5824module rec After 5825 : sig val x : int end 5826 = struct let x = Before.x + 1 end 5827and Before 5828 : sig val x : int end 5829 = struct let x = 3 end 5830;; 5831 5832let _ = 5833 test 40 After.x 4 5834;; 5835 5836(* Type identity between A.t and t within A's definition *) 5837 5838module rec Strengthen 5839 : sig type t val f : t -> t end 5840 = struct 5841 type t = A | B 5842 let _ = (A : Strengthen.t) 5843 let f x = if true then A else Strengthen.f B 5844 end 5845;; 5846 5847module rec Strengthen2 5848 : sig type t 5849 val f : t -> t 5850 module M : sig type u end 5851 module R : sig type v end 5852 end 5853 = struct 5854 type t = A | B 5855 let _ = (A : Strengthen2.t) 5856 let f x = if true then A else Strengthen2.f B 5857 module M = 5858 struct 5859 type u = C 5860 let _ = (C: Strengthen2.M.u) 5861 end 5862 module rec R : sig type v = Strengthen2.R.v end = 5863 struct 5864 type v = D 5865 let _ = (D : R.v) 5866 let _ = (D : Strengthen2.R.v) 5867 end 5868 end 5869;; 5870 5871(* Polymorphic recursion *) 5872 5873module rec PolyRec 5874 : sig 5875 type 'a t = Leaf of 'a | Node of 'a list t * 'a list t 5876 val depth: 'a t -> int 5877 end 5878 = struct 5879 type 'a t = Leaf of 'a | Node of 'a list t * 'a list t 5880 let x = (PolyRec.Leaf 1 : int t) 5881 let depth = function 5882 Leaf x -> 0 5883 | Node(l,r) -> 1 + max (PolyRec.depth l) (PolyRec.depth r) 5884 end 5885;; 5886 5887(* Wrong LHS signatures (PR#4336) *) 5888 5889(* 5890module type ASig = sig type a val a:a val print:a -> unit end 5891module type BSig = sig type b val b:b val print:b -> unit end 5892 5893module A = struct type a = int let a = 0 let print = print_int end 5894module B = struct type b = float let b = 0.0 let print = print_float end 5895 5896module MakeA (Empty:sig end) : ASig = A 5897module MakeB (Empty:sig end) : BSig = B 5898 5899module 5900 rec NewA : ASig = MakeA (struct end) 5901 and NewB : BSig with type b = NewA.a = MakeB (struct end);; 5902 5903*) 5904 5905(* Expressions and bindings *) 5906 5907module StringSet = Set.Make(String);; 5908 5909module rec Expr 5910 : sig 5911 type t = 5912 Var of string 5913 | Const of int 5914 | Add of t * t 5915 | Binding of Binding.t * t 5916 val make_let: string -> t -> t -> t 5917 val fv: t -> StringSet.t 5918 val simpl: t -> t 5919 end 5920 = struct 5921 type t = 5922 Var of string 5923 | Const of int 5924 | Add of t * t 5925 | Binding of Binding.t * t 5926 let make_let id e1 e2 = Binding([id, e1], e2) 5927 let rec fv = function 5928 Var s -> StringSet.singleton s 5929 | Const n -> StringSet.empty 5930 | Add(t1,t2) -> StringSet.union (fv t1) (fv t2) 5931 | Binding(b,t) -> 5932 StringSet.union (Binding.fv b) 5933 (StringSet.diff (fv t) (Binding.bv b)) 5934 let rec simpl = function 5935 Var s -> Var s 5936 | Const n -> Const n 5937 | Add(Const i, Const j) -> Const (i+j) 5938 | Add(Const 0, t) -> simpl t 5939 | Add(t, Const 0) -> simpl t 5940 | Add(t1,t2) -> Add(simpl t1, simpl t2) 5941 | Binding(b, t) -> Binding(Binding.simpl b, simpl t) 5942 end 5943 5944and Binding 5945 : sig 5946 type t = (string * Expr.t) list 5947 val fv: t -> StringSet.t 5948 val bv: t -> StringSet.t 5949 val simpl: t -> t 5950 end 5951 = struct 5952 type t = (string * Expr.t) list 5953 let fv b = 5954 List.fold_left (fun v (id,e) -> StringSet.union v (Expr.fv e)) 5955 StringSet.empty b 5956 let bv b = 5957 List.fold_left (fun v (id,e) -> StringSet.add id v) 5958 StringSet.empty b 5959 let simpl b = 5960 List.map (fun (id,e) -> (id, Expr.simpl e)) b 5961 end 5962;; 5963 5964let _ = 5965 let e = Expr.make_let "x" (Expr.Add (Expr.Var "y", Expr.Const 0)) 5966 (Expr.Var "x") in 5967 let e' = Expr.make_let "x" (Expr.Var "y") (Expr.Var "x") in 5968 test 50 (StringSet.elements (Expr.fv e)) ["y"]; 5969 test 51 (Expr.simpl e) e' 5970;; 5971 5972(* Okasaki's bootstrapping *) 5973 5974module type ORDERED = 5975 sig 5976 type t 5977 val eq: t -> t -> bool 5978 val lt: t -> t -> bool 5979 val leq: t -> t -> bool 5980 end 5981 5982module type HEAP = 5983 sig 5984 module Elem: ORDERED 5985 type heap 5986 val empty: heap 5987 val isEmpty: heap -> bool 5988 val insert: Elem.t -> heap -> heap 5989 val merge: heap -> heap -> heap 5990 val findMin: heap -> Elem.t 5991 val deleteMin: heap -> heap 5992 end 5993 5994module Bootstrap (MakeH: functor (Element:ORDERED) -> 5995 HEAP with module Elem = Element) 5996 (Element: ORDERED) : HEAP with module Elem = Element = 5997 struct 5998 module Elem = Element 5999 module rec BE 6000 : sig type t = E | H of Elem.t * PrimH.heap 6001 val eq: t -> t -> bool 6002 val lt: t -> t -> bool 6003 val leq: t -> t -> bool 6004 end 6005 = struct 6006 type t = E | H of Elem.t * PrimH.heap 6007 let leq t1 t2 = 6008 match t1, t2 with 6009 | (H(x, _)), (H(y, _)) -> Elem.leq x y 6010 | H _, E -> false 6011 | E, H _ -> true 6012 | E, E -> true 6013 let eq t1 t2 = 6014 match t1, t2 with 6015 | (H(x, _)), (H(y, _)) -> Elem.eq x y 6016 | H _, E -> false 6017 | E, H _ -> false 6018 | E, E -> true 6019 let lt t1 t2 = 6020 match t1, t2 with 6021 | (H(x, _)), (H(y, _)) -> Elem.lt x y 6022 | H _, E -> false 6023 | E, H _ -> true 6024 | E, E -> false 6025 end 6026 and PrimH 6027 : HEAP with type Elem.t = BE.t 6028 = MakeH(BE) 6029 type heap = BE.t 6030 let empty = BE.E 6031 let isEmpty = function BE.E -> true | _ -> false 6032 let rec merge x y = 6033 match (x,y) with 6034 (BE.E, _) -> y 6035 | (_, BE.E) -> x 6036 | (BE.H(e1,p1) as h1), (BE.H(e2,p2) as h2) -> 6037 if Elem.leq e1 e2 6038 then BE.H(e1, PrimH.insert h2 p1) 6039 else BE.H(e2, PrimH.insert h1 p2) 6040 let insert x h = 6041 merge (BE.H(x, PrimH.empty)) h 6042 let findMin = function 6043 BE.E -> raise Not_found 6044 | BE.H(x, _) -> x 6045 let deleteMin = function 6046 BE.E -> raise Not_found 6047 | BE.H(x, p) -> 6048 if PrimH.isEmpty p then BE.E else begin 6049 match PrimH.findMin p with 6050 | (BE.H(y, p1)) -> 6051 let p2 = PrimH.deleteMin p in 6052 BE.H(y, PrimH.merge p1 p2) 6053 | BE.E -> assert false 6054 end 6055 end 6056;; 6057 6058module LeftistHeap(Element: ORDERED): HEAP with module Elem = Element = 6059 struct 6060 module Elem = Element 6061 type heap = E | T of int * Elem.t * heap * heap 6062 let rank = function E -> 0 | T(r,_,_,_) -> r 6063 let make x a b = 6064 if rank a >= rank b 6065 then T(rank b + 1, x, a, b) 6066 else T(rank a + 1, x, b, a) 6067 let empty = E 6068 let isEmpty = function E -> true | _ -> false 6069 let rec merge h1 h2 = 6070 match (h1, h2) with 6071 (_, E) -> h1 6072 | (E, _) -> h2 6073 | (T(_, x1, a1, b1), T(_, x2, a2, b2)) -> 6074 if Elem.leq x1 x2 6075 then make x1 a1 (merge b1 h2) 6076 else make x2 a2 (merge h1 b2) 6077 let insert x h = merge (T(1, x, E, E)) h 6078 let findMin = function 6079 E -> raise Not_found 6080 | T(_, x, _, _) -> x 6081 let deleteMin = function 6082 E -> raise Not_found 6083 | T(_, x, a, b) -> merge a b 6084 end 6085;; 6086 6087module Ints = 6088 struct 6089 type t = int 6090 let eq = (=) 6091 let lt = (<) 6092 let leq = (<=) 6093 end 6094;; 6095 6096module C = Bootstrap(LeftistHeap)(Ints);; 6097 6098let _ = 6099 let h = List.fold_right C.insert [6;4;8;7;3;1] C.empty in 6100 test 60 (C.findMin h) 1; 6101 test 61 (C.findMin (C.deleteMin h)) 3; 6102 test 62 (C.findMin (C.deleteMin (C.deleteMin h))) 4 6103;; 6104 6105(* Classes *) 6106 6107module rec Class1 6108 : sig 6109 class c : object method m : int -> int end 6110 end 6111 = struct 6112 class c = 6113 object 6114 method m x = if x <= 0 then x else (new Class2.d)#m x 6115 end 6116 end 6117and Class2 6118 : sig 6119 class d : object method m : int -> int end 6120 end 6121 = struct 6122 class d = 6123 object(self) 6124 inherit Class1.c as super 6125 method m (x:int) = super#m 0 6126 end 6127 end 6128;; 6129 6130let _ = 6131 test 70 ((new Class1.c)#m 7) 0 6132;; 6133 6134let _ = 6135 try 6136 let module A = struct 6137 module rec BadClass1 6138 : sig 6139 class c : object method m : int end 6140 end 6141 = struct 6142 class c = object method m = 123 end 6143 end 6144 and BadClass2 6145 : sig 6146 val x: int 6147 end 6148 = struct 6149 let x = (new BadClass1.c)#m 6150 end 6151 end in 6152 test 71 true false 6153 with Undefined_recursive_module _ -> 6154 test 71 true true 6155;; 6156 6157(* Coercions *) 6158 6159module rec Coerce1 6160 : sig 6161 val g: int -> int 6162 val f: int -> int 6163 end 6164 = struct 6165 module A = (Coerce1: sig val f: int -> int end) 6166 let g x = x 6167 let f x = if x <= 0 then 1 else A.f (x-1) * x 6168 end 6169;; 6170 6171let _ = 6172 test 80 (Coerce1.f 10) 3628800 6173;; 6174 6175module CoerceF(S: sig end) = struct 6176 let f1 () = 1 6177 let f2 () = 2 6178 let f3 () = 3 6179 let f4 () = 4 6180 let f5 () = 5 6181end 6182 6183module rec Coerce2: sig val f1: unit -> int end = CoerceF(Coerce3) 6184 and Coerce3: sig end = struct end 6185;; 6186 6187let _ = 6188 test 81 (Coerce2.f1 ()) 1 6189;; 6190 6191module Coerce4(A : sig val f : int -> int end) = struct 6192 let x = 0 6193 let at a = A.f a 6194end 6195 6196module rec Coerce5 6197 : sig val blabla: int -> int val f: int -> int end 6198 = struct let blabla x = 0 let f x = 5 end 6199and Coerce6 6200 : sig val at: int -> int end 6201 = Coerce4(Coerce5) 6202 6203let _ = 6204 test 82 (Coerce6.at 100) 5 6205;; 6206 6207(* Miscellaneous bug reports *) 6208 6209module rec F 6210 : sig type t = X of int | Y of int 6211 val f: t -> bool 6212 end 6213 = struct 6214 type t = X of int | Y of int 6215 let f = function 6216 | X _ -> false 6217 | _ -> true 6218 end;; 6219 6220let _ = 6221 test 100 (F.f (F.X 1)) false; 6222 test 101 (F.f (F.Y 2)) true 6223 6224(* PR#4316 *) 6225module G(S : sig val x : int Lazy.t end) = struct include S end 6226 6227module M1 = struct let x = lazy 3 end 6228 6229let _ = Lazy.force M1.x 6230 6231module rec M2 : sig val x : int Lazy.t end = G(M1) 6232 6233let _ = 6234 test 102 (Lazy.force M2.x) 3 6235 6236let _ = Gc.full_major() (* will shortcut forwarding in M1.x *) 6237 6238module rec M3 : sig val x : int Lazy.t end = G(M1) 6239 6240let _ = 6241 test 103 (Lazy.force M3.x) 3 6242 6243 6244(** Pure type-checking tests: see recmod/*.ml *) 6245type t = A of {x:int; mutable y:int};; 6246let f (A r) = r;; (* -> escape *) 6247let f (A r) = r.x;; (* ok *) 6248let f x = A {x; y = x};; (* ok *) 6249let f (A r) = A {r with y = r.x + 1};; (* ok *) 6250let f () = A {a = 1};; (* customized error message *) 6251let f () = A {x = 1; y = 3};; (* ok *) 6252 6253type _ t = A: {x : 'a; y : 'b} -> 'a t;; 6254let f (A {x; y}) = A {x; y = ()};; (* ok *) 6255let f (A ({x; y} as r)) = A {x = r.x; y = r.y};; (* ok *) 6256 6257module M = struct 6258 type 'a t = 6259 | A of {x : 'a} 6260 | B: {u : 'b} -> unit t;; 6261 6262 exception Foo of {x : int};; 6263end;; 6264 6265module N : sig 6266 type 'b t = 'b M.t = 6267 | A of {x : 'b} 6268 | B: {u : 'bla} -> unit t 6269 6270 exception Foo of {x : int} 6271end = struct 6272 type 'b t = 'b M.t = 6273 | A of {x : 'b} 6274 | B: {u : 'z} -> unit t 6275 6276 exception Foo = M.Foo 6277end;; 6278 6279 6280module type S = sig exception A of {x:int} end;; 6281 6282module F (X : sig val x : (module S) end) = struct 6283 module A = (val X.x) 6284end;; (* -> this expression creates fresh types (not really!) *) 6285 6286 6287module type S = sig 6288 exception A of {x : int} 6289 exception A of {x : string} 6290end;; 6291 6292module M = struct 6293 exception A of {x : int} 6294 exception A of {x : string} 6295end;; 6296 6297 6298module M1 = struct 6299 exception A of {x : int} 6300end;; 6301 6302module M = struct 6303 include M1 6304 include M1 6305end;; 6306 6307 6308module type S1 = sig 6309 exception A of {x : int} 6310end;; 6311 6312module type S = sig 6313 include S1 6314 include S1 6315end;; 6316 6317module M = struct 6318 exception A = M1.A 6319end;; 6320 6321module X1 = struct 6322 type t = .. 6323end;; 6324module X2 = struct 6325 type t = .. 6326end;; 6327module Z = struct 6328 type X1.t += A of {x: int} 6329 type X2.t += A of {x: int} 6330end;; 6331 6332(* PR#6716 *) 6333 6334type _ c = C : [`A] c 6335type t = T : {x:[<`A] c} -> t;; 6336let f (T { x = C }) = ();; 6337module M : sig 6338 type 'a t 6339 type u = u t and v = v t 6340 val f : int -> u 6341 val g : v -> bool 6342end = struct 6343 type 'a t = 'a 6344 type u = int and v = bool 6345 let f x = x 6346 let g x = x 6347end;; 6348 6349let h (x : int) : bool = M.g (M.f x);; 6350type _ t = C : ((('a -> 'o) -> 'o) -> ('b -> 'o) -> 'o) t 6351let f : type a o. ((a -> o) -> o) t -> (a -> o) -> o = 6352 fun C k -> k (fun x -> x);; 6353module type T = sig type 'a t end 6354module Fix (T : T) = struct type r = ('r T.t as 'r) end 6355 type _ t = 6356 X of string 6357 | Y : bytes t 6358 6359let y : string t = Y 6360let f : string A.t -> unit = function 6361 A.X s -> print_endline s 6362 6363let () = f A.y 6364module rec A : sig 6365 type t 6366end = struct 6367 type t = { a : unit; b : unit } 6368 let _ = { a = () } 6369end 6370;; 6371type t = [`A | `B];; 6372type 'a u = t;; 6373let a : [< int u] = `A;; 6374 6375type 'a s = 'a;; 6376let b : [< t s] = `B;; 6377module Core = struct 6378 module Int = struct 6379 module T = struct 6380 type t = int 6381 let compare = compare 6382 let (+) x y = x + y 6383 end 6384 include T 6385 module Map = Map.Make(T) 6386 end 6387 6388 module Std = struct 6389 module Int = Int 6390 end 6391end 6392;; 6393 6394open Core.Std 6395;; 6396 6397let x = Int.Map.empty ;; 6398let y = x + x ;; 6399 6400(* Avoid ambiguity *) 6401 6402module M = struct type t = A type u = C end 6403module N = struct type t = B end 6404open M open N;; 6405A;; 6406B;; 6407C;; 6408 6409include M open M;; 6410C;; 6411 6412module L = struct type v = V end 6413open L;; 6414V;; 6415module L = struct type v = V end 6416open L;; 6417V;; 6418 6419 6420type t1 = A;; 6421module M1 = struct type u = v and v = t1 end;; 6422module N1 = struct type u = v and v = M1.v end;; 6423type t1 = B;; 6424module N2 = struct type u = v and v = M1.v end;; 6425 6426 6427(* PR#6566 *) 6428module type PR6566 = sig type t = string end;; 6429module PR6566 = struct type t = int end;; 6430module PR6566' : PR6566 = PR6566;; 6431 6432module A = struct module B = struct type t = T end end;; 6433module M2 = struct type u = A.B.t type foo = int type v = A.B.t end;; 6434(* Adapted from: An Expressive Language of Signatures 6435 by Norman Ramsey, Kathleen Fisher and Paul Govereau *) 6436 6437module type VALUE = sig 6438 type value (* a Lua value *) 6439 type state (* the state of a Lua interpreter *) 6440 type usert (* a user-defined value *) 6441end;; 6442 6443module type CORE0 = sig 6444 module V : VALUE 6445 val setglobal : V.state -> string -> V.value -> unit 6446 (* five more functions common to core and evaluator *) 6447end;; 6448 6449module type CORE = sig 6450 include CORE0 6451 val apply : V.value -> V.state -> V.value list -> V.value 6452 (* apply function f in state s to list of args *) 6453end;; 6454 6455module type AST = sig 6456 module Value : VALUE 6457 type chunk 6458 type program 6459 val get_value : chunk -> Value.value 6460end;; 6461 6462module type EVALUATOR = sig 6463 module Value : VALUE 6464 module Ast : (AST with module Value := Value) 6465 type state = Value.state 6466 type value = Value.value 6467 exception Error of string 6468 val compile : Ast.program -> string 6469 include CORE0 with module V := Value 6470end;; 6471 6472module type PARSER = sig 6473 type chunk 6474 val parse : string -> chunk 6475end;; 6476 6477module type INTERP = sig 6478 include EVALUATOR 6479 module Parser : PARSER with type chunk = Ast.chunk 6480 val dostring : state -> string -> value list 6481 val mk : unit -> state 6482end;; 6483 6484module type USERTYPE = sig 6485 type t 6486 val eq : t -> t -> bool 6487 val to_string : t -> string 6488end;; 6489 6490module type TYPEVIEW = sig 6491 type combined 6492 type t 6493 val map : (combined -> t) * (t -> combined) 6494end;; 6495 6496module type COMBINED_COMMON = sig 6497 module T : sig type t end 6498 module TV1 : TYPEVIEW with type combined := T.t 6499 module TV2 : TYPEVIEW with type combined := T.t 6500end;; 6501 6502module type COMBINED_TYPE = sig 6503 module T : USERTYPE 6504 include COMBINED_COMMON with module T := T 6505end;; 6506 6507module type BARECODE = sig 6508 type state 6509 val init : state -> unit 6510end;; 6511 6512module USERCODE(X : TYPEVIEW) = struct 6513 module type F = 6514 functor (C : CORE with type V.usert = X.combined) -> 6515 BARECODE with type state := C.V.state 6516end;; 6517 6518module Weapon = struct type t end;; 6519 6520module type WEAPON_LIB = sig 6521 type t = Weapon.t 6522 module T : USERTYPE with type t = t 6523 module Make : 6524 functor (TV : TYPEVIEW with type t = t) -> USERCODE(TV).F 6525end;; 6526 6527module type X = functor (X: CORE) -> BARECODE;; 6528module type X = functor (_: CORE) -> BARECODE;; 6529module M = struct 6530 type t = int * (< m : 'a > as 'a) 6531end;; 6532 6533module type S = 6534 sig module M : sig type t end end with module M = M 6535;; 6536module type Printable = sig 6537 type t 6538 val print : Format.formatter -> t -> unit 6539end;; 6540module type Comparable = sig 6541 type t 6542 val compare : t -> t -> int 6543end;; 6544module type PrintableComparable = sig 6545 include Printable 6546 include Comparable with type t = t 6547end;; (* Fails *) 6548module type PrintableComparable = sig 6549 type t 6550 include Printable with type t := t 6551 include Comparable with type t := t 6552end;; 6553module type PrintableComparable = sig 6554 include Printable 6555 include Comparable with type t := t 6556end;; 6557module type ComparableInt = Comparable with type t := int;; 6558module type S = sig type t val f : t -> t end;; 6559module type S' = S with type t := int;; 6560 6561module type S = sig type 'a t val map : ('a -> 'b) -> 'a t -> 'b t end;; 6562module type S1 = S with type 'a t := 'a list;; 6563module type S2 = sig 6564 type 'a dict = (string * 'a) list 6565 include S with type 'a t := 'a dict 6566end;; 6567 6568 6569module type S = 6570 sig module T : sig type exp type arg end val f : T.exp -> T.arg end;; 6571module M = struct type exp = string type arg = int end;; 6572module type S' = S with module T := M;; 6573 6574 6575module type S = sig type 'a t end with type 'a t := unit;; (* Fails *) 6576let property (type t) () = 6577 let module M = struct exception E of t end in 6578 (fun x -> M.E x), (function M.E x -> Some x | _ -> None) 6579;; 6580 6581let () = 6582 let (int_inj, int_proj) = property () in 6583 let (string_inj, string_proj) = property () in 6584 6585 let i = int_inj 3 in 6586 let s = string_inj "abc" in 6587 6588 Printf.printf "%b\n%!" (int_proj i = None); 6589 Printf.printf "%b\n%!" (int_proj s = None); 6590 Printf.printf "%b\n%!" (string_proj i = None); 6591 Printf.printf "%b\n%!" (string_proj s = None) 6592;; 6593 6594let sort_uniq (type s) cmp l = 6595 let module S = Set.Make(struct type t = s let compare = cmp end) in 6596 S.elements (List.fold_right S.add l S.empty) 6597;; 6598 6599let () = 6600 print_endline (String.concat "," (sort_uniq compare [ "abc"; "xyz"; "abc" ])) 6601;; 6602 6603let f x (type a) (y : a) = (x = y);; (* Fails *) 6604class ['a] c = object (self) 6605 method m : 'a -> 'a = fun x -> x 6606 method n : 'a -> 'a = fun (type g) (x:g) -> self#m x 6607end;; (* Fails *) 6608 6609external a : (int [@untagged]) -> unit = "a" "a_nat" 6610external b : (int32 [@unboxed]) -> unit = "b" "b_nat" 6611external c : (int64 [@unboxed]) -> unit = "c" "c_nat" 6612external d : (nativeint [@unboxed]) -> unit = "d" "d_nat" 6613external e : (float [@unboxed]) -> unit = "e" "e_nat" 6614 6615type t = private int 6616 6617external f : (t [@untagged]) -> unit = "f" "f_nat" 6618 6619module M : sig 6620 external a : int -> (int [@untagged]) = "a" "a_nat" 6621 external b : (int [@untagged]) -> int = "b" "b_nat" 6622end = struct 6623 external a : int -> (int [@untagged]) = "a" "a_nat" 6624 external b : (int [@untagged]) -> int = "b" "b_nat" 6625end;; 6626 6627module Global_attributes = struct 6628 [@@@ocaml.warning "-3"] 6629 6630 external a : float -> float = "a" "noalloc" "a_nat" "float" 6631 external b : float -> float = "b" "noalloc" "b_nat" 6632 external c : float -> float = "c" "c_nat" "float" 6633 external d : float -> float = "d" "noalloc" 6634 external e : float -> float = "e" 6635 6636 (* Should output a warning: no native implementation provided *) 6637 external f : (int32 [@unboxed]) -> (int32 [@unboxed]) = "f" "noalloc" 6638 external g : int32 -> int32 = "g" "g_nat" [@@unboxed] [@@noalloc] 6639 6640 external h : (int [@untagged]) -> (int [@untagged]) = "h" "h_nat" "noalloc" 6641 external i : int -> int = "i" "i_nat" [@@untagged] [@@noalloc] 6642end;; 6643 6644module Old_style_warning = struct 6645 [@@@ocaml.warning "+3"] 6646 external a : float -> float = "a" "noalloc" "a_nat" "float" 6647 external b : float -> float = "b" "noalloc" "b_nat" 6648 external c : float -> float = "c" "c_nat" "float" 6649 external d : float -> float = "d" "noalloc" 6650 external e : float -> float = "c" "float" 6651end 6652 6653(* Bad: attributes not reported in the interface *) 6654 6655module Bad1 : sig 6656 external f : int -> int = "f" "f_nat" 6657end = struct 6658 external f : int -> (int [@untagged]) = "f" "f_nat" 6659end;; 6660 6661module Bad2 : sig 6662 external f : int -> int = "a" "a_nat" 6663end = struct 6664 external f : (int [@untagged]) -> int = "f" "f_nat" 6665end;; 6666 6667module Bad3 : sig 6668 external f : float -> float = "f" "f_nat" 6669end = struct 6670 external f : float -> (float [@unboxed]) = "f" "f_nat" 6671end;; 6672 6673module Bad4 : sig 6674 external f : float -> float = "a" "a_nat" 6675end = struct 6676 external f : (float [@unboxed]) -> float = "f" "f_nat" 6677end;; 6678 6679(* Bad: attributes in the interface but not in the implementation *) 6680 6681module Bad5 : sig 6682 external f : int -> (int [@untagged]) = "f" "f_nat" 6683end = struct 6684 external f : int -> int = "f" "f_nat" 6685end;; 6686 6687module Bad6 : sig 6688 external f : (int [@untagged]) -> int = "f" "f_nat" 6689end = struct 6690 external f : int -> int = "a" "a_nat" 6691end;; 6692 6693module Bad7 : sig 6694 external f : float -> (float [@unboxed]) = "f" "f_nat" 6695end = struct 6696 external f : float -> float = "f" "f_nat" 6697end;; 6698 6699module Bad8 : sig 6700 external f : (float [@unboxed]) -> float = "f" "f_nat" 6701end = struct 6702 external f : float -> float = "a" "a_nat" 6703end;; 6704 6705(* Bad: unboxed or untagged with the wrong type *) 6706 6707external g : (float [@untagged]) -> float = "g" "g_nat";; 6708external h : (int [@unboxed]) -> float = "h" "h_nat";; 6709 6710(* Bad: unboxing the function type *) 6711external i : int -> float [@unboxed] = "i" "i_nat";; 6712 6713(* Bad: unboxing a "deep" sub-type. *) 6714external j : int -> (float [@unboxed]) * float = "j" "j_nat";; 6715 6716(* This should be rejected, but it is quite complicated to do 6717 in the current state of things *) 6718 6719external k : int -> (float [@unboxd]) = "k" "k_nat";; 6720 6721(* Bad: old style annotations + new style attributes *) 6722 6723external l : float -> float = "l" "l_nat" "float" [@@unboxed];; 6724external m : (float [@unboxed]) -> float = "m" "m_nat" "float";; 6725external n : float -> float = "n" "noalloc" [@@noalloc];; 6726 6727(* Warnings: unboxed / untagged without any native implementation *) 6728external o : (float[@unboxed]) -> float = "o";; 6729external p : float -> (float[@unboxed]) = "p";; 6730external q : (int[@untagged]) -> float = "q";; 6731external r : int -> (int[@untagged]) = "r";; 6732external s : int -> int = "s" [@@untagged];; 6733external t : float -> float = "t" [@@unboxed];; 6734let _ = ignore (+);; 6735let _ = raise Exit 3;; 6736(* comment 9644 of PR#6000 *) 6737 6738fun b -> if b then format_of_string "x" else "y";; 6739fun b -> if b then "x" else format_of_string "y";; 6740fun b : (_,_,_) format -> if b then "x" else "y";; 6741 6742(* PR#7135 *) 6743 6744module PR7135 = struct 6745 module M : sig type t = private int end = struct type t = int end 6746 include M 6747 6748 let lift2 (f : int -> int -> int) (x : t) (y : t) = 6749 f (x :> int) (y :> int) 6750end;; 6751 6752(* exemple of non-ground coercion *) 6753 6754module Test1 = struct 6755 type t = private int 6756 let f x = let y = if true then x else (x:t) in (y :> int) 6757end;; 6758(* Warn about all relevant cases when possible *) 6759let f = function 6760 None, None -> 1 6761 | Some _, Some _ -> 2;; 6762 6763(* Exhaustiveness check is very slow *) 6764type _ t = 6765 A : int t | B : bool t | C : char t | D : float t 6766type (_,_,_,_) u = U : (int, int, int, int) u 6767type v = E | F | G 6768;; 6769 6770let f : type a b c d e f g. 6771 a t * b t * c t * d t * e t * f t * g t * v 6772 * (a,b,c,d) u * (e,f,g,g) u -> int = 6773 function A, A, A, A, A, A, A, _, U, U -> 1 6774 | _, _, _, _, _, _, _, G, _, _ -> 1 6775 (*| _ -> _ *) 6776;; 6777 6778(* Unused cases *) 6779let f (x : int t) = match x with A -> 1 | _ -> 2;; (* warn *) 6780let f (x : unit t option) = match x with None -> 1 | _ -> 2 ;; (* warn? *) 6781let f (x : unit t option) = match x with None -> 1 | Some _ -> 2 ;; (* warn *) 6782let f (x : int t option) = match x with None -> 1 | _ -> 2;; 6783let f (x : int t option) = match x with None -> 1;; (* warn *) 6784 6785(* Example with record, type, single case *) 6786 6787type 'a box = Box of 'a 6788type 'a pair = {left: 'a; right: 'a};; 6789 6790let f : (int t box pair * bool) option -> unit = function None -> ();; 6791let f : (string t box pair * bool) option -> unit = function None -> ();; 6792 6793 6794(* Examples from ML2015 paper *) 6795 6796type _ t = 6797 | Int : int t 6798 | Bool : bool t 6799;; 6800 6801let f : type a. a t -> a = function 6802 | Int -> 1 6803 | Bool -> true 6804;; 6805let g : int t -> int = function 6806 | Int -> 1 6807;; 6808let h : type a. a t -> a t -> bool = 6809 fun x y -> match x, y with 6810 | Int, Int -> true 6811 | Bool, Bool -> true 6812;; 6813type (_, _) cmp = 6814 | Eq : ('a, 'a) cmp 6815 | Any: ('a, 'b) cmp 6816module A : sig type a type b val eq : (a, b) cmp end 6817 = struct type a type b = a let eq = Eq end 6818;; 6819let f : (A.a, A.b) cmp -> unit = function Any -> () 6820;; 6821let deep : char t option -> char = 6822 function None -> 'c' 6823;; 6824type zero = Zero 6825type _ succ = Succ 6826;; 6827type (_,_,_) plus = 6828 | Plus0 : (zero, 'a, 'a) plus 6829 | PlusS : ('a, 'b, 'c) plus -> 6830 ('a succ, 'b, 'c succ) plus 6831;; 6832let trivial : (zero succ, zero, zero) plus option -> bool = 6833 function None -> false 6834;; 6835let easy : (zero, zero succ, zero) plus option -> bool = 6836 function None -> false 6837;; 6838let harder : (zero succ, zero succ, zero succ) plus option -> bool = 6839 function None -> false 6840;; 6841let harder : (zero succ, zero succ, zero succ) plus option -> bool = 6842 function None -> false | Some (PlusS _) -> . 6843;; 6844let inv_zero : type a b c d. (a,b,c) plus -> (c,d,zero) plus -> bool = 6845 fun p1 p2 -> 6846 match p1, p2 with 6847 | Plus0, Plus0 -> true 6848;; 6849 6850 6851(* Empty match *) 6852 6853type _ t = Int : int t;; 6854let f (x : bool t) = match x with _ -> . ;; (* ok *) 6855 6856 6857(* trefis in PR#6437 *) 6858 6859let f () = match None with _ -> .;; (* error *) 6860let g () = match None with _ -> () | exception _ -> .;; (* error *) 6861let h () = match None with _ -> . | exception _ -> .;; (* error *) 6862let f x = match x with _ -> () | None -> .;; (* do not warn *) 6863 6864(* #7059, all clauses guarded *) 6865 6866let f x y = match 1 with 1 when x = y -> 1;; 6867open CamlinternalOO;; 6868type _ choice = Left : label choice | Right : tag choice;; 6869let f : label choice -> bool = function Left -> true;; (* warn *) 6870exception A;; 6871type a = A;; 6872 6873A;; 6874raise A;; 6875fun (A : a) -> ();; 6876function Not_found -> 1 | A -> 2 | _ -> 3;; 6877try raise A with A -> 2;; 6878module TypEq = struct 6879 type (_, _) t = Eq : ('a, 'a) t 6880end 6881 6882module type T = sig 6883 type _ is_t = Is : ('a, 'b) TypEq.t -> 'a is_t 6884 val is_t : unit -> unit is_t option 6885end 6886 6887module Make (M : T) = 6888 struct 6889 let _ = 6890 match M.is_t () with 6891 | None -> 0 6892 | Some _ -> 0 6893 let f () = 6894 match M.is_t () with None -> 0 6895end;; 6896 6897module Make2 (M : T) = struct 6898 type t = T of unit M.is_t 6899 let g : t -> int = function _ -> . 6900end;; 6901type t = A : t;; 6902 6903module X1 : sig end = struct 6904 let _f ~x (* x unused argument *) = function 6905 | A -> let x = () in x 6906end;; 6907 6908module X2 : sig end = struct 6909 let x = 42 (* unused value *) 6910 let _f = function 6911 | A -> let x = () in x 6912end;; 6913 6914module X3 : sig end = struct 6915 module O = struct let x = 42 (* unused *) end 6916 open O (* unused open *) 6917 6918 let _f = function 6919 | A -> let x = () in x 6920end;; 6921(* Use type information *) 6922module M1 = struct 6923 type t = {x: int; y: int} 6924 type u = {x: bool; y: bool} 6925end;; 6926 6927module OK = struct 6928 open M1 6929 let f1 (r:t) = r.x (* ok *) 6930 let f2 r = ignore (r:t); r.x (* non principal *) 6931 6932 let f3 (r: t) = 6933 match r with {x; y} -> y + y (* ok *) 6934end;; 6935 6936module F1 = struct 6937 open M1 6938 let f r = match r with {x; y} -> y + y 6939end;; (* fails *) 6940 6941module F2 = struct 6942 open M1 6943 let f r = 6944 ignore (r: t); 6945 match r with 6946 {x; y} -> y + y 6947end;; (* fails for -principal *) 6948 6949(* Use type information with modules*) 6950module M = struct 6951 type t = {x:int} 6952 type u = {x:bool} 6953end;; 6954let f (r:M.t) = r.M.x;; (* ok *) 6955let f (r:M.t) = r.x;; (* warning *) 6956let f ({x}:M.t) = x;; (* warning *) 6957 6958module M = struct 6959 type t = {x: int; y: int} 6960end;; 6961module N = struct 6962 type u = {x: bool; y: bool} 6963end;; 6964module OK = struct 6965 open M 6966 open N 6967 let f (r:M.t) = r.x 6968end;; 6969 6970module M = struct 6971 type t = {x:int} 6972 module N = struct type s = t = {x:int} end 6973 type u = {x:bool} 6974end;; 6975module OK = struct 6976 open M.N 6977 let f (r:M.t) = r.x 6978end;; 6979 6980(* Use field information *) 6981module M = struct 6982 type u = {x:bool;y:int;z:char} 6983 type t = {x:int;y:bool} 6984end;; 6985module OK = struct 6986 open M 6987 let f {x;z} = x,z 6988end;; (* ok *) 6989module F3 = struct 6990 open M 6991 let r = {x=true;z='z'} 6992end;; (* fail for missing label *) 6993 6994module OK = struct 6995 type u = {x:int;y:bool} 6996 type t = {x:bool;y:int;z:char} 6997 let r = {x=3; y=true} 6998end;; (* ok *) 6999 7000(* Corner cases *) 7001 7002module F4 = struct 7003 type foo = {x:int; y:int} 7004 type bar = {x:int} 7005 let b : bar = {x=3; y=4} 7006end;; (* fail but don't warn *) 7007 7008module M = struct type foo = {x:int;y:int} end;; 7009module N = struct type bar = {x:int;y:int} end;; 7010let r = { M.x = 3; N.y = 4; };; (* error: different definitions *) 7011 7012module MN = struct include M include N end 7013module NM = struct include N include M end;; 7014let r = {MN.x = 3; NM.y = 4};; (* error: type would change with order *) 7015 7016(* Lpw25 *) 7017 7018module M = struct 7019 type foo = { x: int; y: int } 7020 type bar = { x:int; y: int; z: int} 7021end;; 7022module F5 = struct 7023 open M 7024 let f r = ignore (r: foo); {r with x = 2; z = 3} 7025end;; 7026module M = struct 7027 include M 7028 type other = { a: int; b: int } 7029end;; 7030module F6 = struct 7031 open M 7032 let f r = ignore (r: foo); { r with x = 3; a = 4 } 7033end;; 7034module F7 = struct 7035 open M 7036 let r = {x=1; y=2} 7037 let r: other = {x=1; y=2} 7038end;; 7039 7040module A = struct type t = {x: int} end 7041module B = struct type t = {x: int} end;; 7042let f (r : B.t) = r.A.x;; (* fail *) 7043 7044(* Spellchecking *) 7045 7046module F8 = struct 7047 type t = {x:int; yyy:int} 7048 let a : t = {x=1;yyz=2} 7049end;; 7050 7051(* PR#6004 *) 7052 7053type t = A 7054type s = A 7055 7056class f (_ : t) = object end;; 7057class g = f A;; (* ok *) 7058 7059class f (_ : 'a) (_ : 'a) = object end;; 7060class g = f (A : t) A;; (* warn with -principal *) 7061 7062 7063(* PR#5980 *) 7064 7065module Shadow1 = struct 7066 type t = {x: int} 7067 module M = struct 7068 type s = {x: string} 7069 end 7070 open M (* this open is unused, it isn't reported as shadowing 'x' *) 7071 let y : t = {x = 0} 7072end;; 7073module Shadow2 = struct 7074 type t = {x: int} 7075 module M = struct 7076 type s = {x: string} 7077 end 7078 open M (* this open shadows label 'x' *) 7079 let y = {x = ""} 7080end;; 7081 7082(* PR#6235 *) 7083 7084module P6235 = struct 7085 type t = { loc : string; } 7086 type v = { loc : string; x : int; } 7087 type u = [ `Key of t ] 7088 let f (u : u) = match u with `Key {loc} -> loc 7089end;; 7090 7091(* Remove interaction between branches *) 7092 7093module P6235' = struct 7094 type t = { loc : string; } 7095 type v = { loc : string; x : int; } 7096 type u = [ `Key of t ] 7097 let f = function 7098 | (_ : u) when false -> "" 7099 |`Key {loc} -> loc 7100end;; 7101module Unused : sig 7102end = struct 7103 type unused = int 7104end 7105;; 7106 7107module Unused_nonrec : sig 7108end = struct 7109 type nonrec used = int 7110 type nonrec unused = used 7111end 7112;; 7113 7114module Unused_rec : sig 7115end = struct 7116 type unused = A of unused 7117end 7118;; 7119 7120module Unused_exception : sig 7121end = struct 7122 exception Nobody_uses_me 7123end 7124;; 7125 7126module Unused_extension_constructor : sig 7127 type t = .. 7128end = struct 7129 type t = .. 7130 type t += Nobody_uses_me 7131end 7132;; 7133 7134module Unused_exception_outside_patterns : sig 7135 val falsity : exn -> bool 7136end = struct 7137 exception Nobody_constructs_me 7138 let falsity = function 7139 | Nobody_constructs_me -> true 7140 | _ -> false 7141end 7142;; 7143 7144module Unused_extension_outside_patterns : sig 7145 type t = .. 7146 val falsity : t -> bool 7147end = struct 7148 type t = .. 7149 type t += Nobody_constructs_me 7150 let falsity = function 7151 | Nobody_constructs_me -> true 7152 | _ -> false 7153end 7154;; 7155 7156module Unused_private_exception : sig 7157 type exn += private Private_exn 7158end = struct 7159 exception Private_exn 7160end 7161;; 7162 7163module Unused_private_extension : sig 7164 type t = .. 7165 type t += private Private_ext 7166end = struct 7167 type t = .. 7168 type t += Private_ext 7169end 7170;; 7171 7172for i = 10 downto 0 do () done 7173 7174type t = < foo: int [@foo] > 7175 7176let _ = [%foo: < foo : t > ] 7177 7178type foo += private A of int 7179 7180let f : 'a 'b 'c. < .. > = assert false 7181 7182let () = 7183 let module M = (functor (T : sig end) -> struct end)(struct end) in () 7184 7185class c = object inherit ((fun () -> object end [@wee]: object end) ()) end 7186 7187 7188let f = function x[@wee] -> () 7189let f = function 7190 | '1'..'9' | '1' .. '8'-> () 7191 | 'a'..'z' -> () 7192 7193let f = function 7194 | [| x1; x2 |] -> () 7195 | [| |] -> () 7196 | [|x|][@foo] -> () 7197 | _ -> () 7198 7199let g = function 7200 | {l=x} -> () 7201 | {l1=x; l2=y}[@foo] -> () 7202 | {l1=x; l2=y; _} -> () 7203 7204let h = fun ?l:(p=1) ?y:u ?x:(x=3) -> 2 7205 7206let _ = function 7207 | a, s, ba1, ba2, ba3, bg -> begin 7208 ignore (Array.get x 1 + Array.get [| |] 0 + 7209 Array.get [| 1 |] 1 + Array.get [|1; 2|] 2); 7210 ignore ([String.get s 1; String.get "" 2; String.get "123" 3]); 7211 ignore (ba1.{0} + ba2.{1, 2} + ba3.{3, 4, 5}) 7212 ignore (bg.{1, 2, 3, 4}) 7213 end 7214 | b, s, ba1, ba2, ba3, bg -> begin 7215 y.(0) <- 1; s.[1] <- 'c'; 7216 ba1.{1} <- 2; ba2.{1, 2} <- 3; ba3.{1, 2, 3} <- 4; 7217 bg.{1, 2, 3, 4, 5} <- 0 7218 end 7219 7220let f (type t) () = 7221 let exception F of t in (); 7222 let exception G of t in (); 7223 let exception E of t in 7224 (fun x -> E x), (function E _ -> print_endline "OK" | _ -> print_endline "KO") 7225 7226let inj1, proj1 = f () 7227let inj2, proj2 = f () 7228 7229let () = proj1 (inj1 42) 7230let () = proj1 (inj2 42) 7231 7232let _ = ~-1 7233 7234class id = [%exp] 7235(* checkpoint *) 7236 7237(* Subtyping is "syntactic" *) 7238let _ = fun (x : < x : int >) y z -> (y :> 'a), (x :> 'a), (z :> 'a);; 7239(* - : (< x : int > as 'a) -> 'a -> 'a * 'a = <fun> *) 7240 7241class ['a] c () = object 7242 method f = (new c (): int c) 7243end and ['a] d () = object 7244 inherit ['a] c () 7245end;; 7246 7247(* PR#7329 Pattern open *) 7248let _ = 7249 let module M = struct type t = { x : int } end in 7250 let f M.(x) = () in 7251 let g M.{x} = () in 7252 let h = function M.[] | M.[a] | M.(a::q) -> () in 7253 let i = function M.[||] | M.[|x|] -> true | _ -> false in 7254 () 7255 7256class ['a] c () = object 7257 constraint 'a = < .. > -> unit 7258 method m = (fun x -> () : 'a) 7259end 7260 7261let f: type a'.a' = assert false 7262let foo : type a' b'. a' -> b' = fun a -> assert false 7263let foo : type t' . t' = fun (type t') -> (assert false : t') 7264let foo : 't . 't = fun (type t) -> (assert false : t) 7265let foo : type a' b' c' t. a' -> b' -> c' -> t = fun a b c -> assert false 7266 7267let f x = 7268 x.contents <- (print_string "coucou" ; x.contents) 7269 7270let ( ~$ ) x = Some x 7271let g x = 7272 ~$ (x.contents) 7273 7274let ( ~$ ) x y = (x, y) 7275let g x y = 7276 ~$ (x.contents) (y.contents) 7277