Gbury

module M : sig
  type t = private int
  val make : int -> t
 end = struct
  type t = int
  let make i =
    if i mod 2 = 0 then i
    else raise (Invalid_argument "not an even number !")
 end

Gbury

(* Overly simplified example *)

type _ foo =
  | Foo : int -> [< `A | `B ] foo
  | Bar : int -> [< `B | `C ] foo

(* The most general type for foo is:
   int -> [< `A | `B ] foo
   But, because of the call in bar, the type actually inferred is:
   int -> _[< `B ] foo

Gbury

let fix f x =
  match f x with
  | `Ok -> Gen.singleton x
  | `Gen gen ->
    let s = Stack.create () in
    Stack.push gen s;
    let rec aux () =
      if Stack.is_empty s then None
      else begin
        let g = Stack.top s in

Gbury

Pipeline.(
    run ~handle_exn:Out.print_exn g opt' (
      (
        ~~~ (op ~name:"includes" Pipe.expand_include)
        @** (op ~name:"expand" Pipe.expand_pack)
        @<< (op ~name:"execute" Pipe.execute)
        @++ (po ~name:"typecheck" Pipe.typecheck)
        @++ (po ~name:"solve" Pipe.solve)
        @++ (op ~name:"print_res" Pipe.print_res)
        @|| (op fst)

Gbury

(** Some aliases for readibility *)
type opt = Options.copts

type 'a gen = 'a Gen.t
type 'a fix = [ `Ok | `Gen of 'a gen ]

type ('a, 'b) op = {
  name : string;
  f : 'a -> 'b;
}

Gbury

./run_test.native
[✗] (   1)    1 ;    0 ;    0 /    1 --     0.0s -- dummy_fail
[✗] (   1)    0 ;    1 ;    0 /    1 --     0.0s -- dummy_error
[✓] ( 130)    0 ;    0 ;  100 /  100 --     0.2s -- fixpoint_occur
[✓] ( 130)    0 ;    0 ;  100 /  100 --     0.2s -- fixpoint_is_proj
[✓] ( 230)    0 ;    0 ;   19 /   30 --     0.3s -- match_subst
[✓] ( 141)    0 ;    0 ;  100 /  100 --     0.2s -- subst_match
[✓] (  57)    0 ;    0 ;   10 /   10 --     0.1s -- robinson_subst
[✓] ( 141)    0 ;    0 ;  100 /  100 --     0.2s -- subst_robinson
[✓] (  10)    0 ;    0 ;   10 /   10 --     1.8s -- naive_correct_match

Gbury

random seed: 92577147
law dummy_fail: 1 relevant cases (1 total)
  test `dummy_fail`
  failed on ≥ 1 cases:
  ⟦∀ v0 : list(a), v1 : list(a), v2 : list(a), v3 : list(a), v4 : list(a), v5 : list(a), v6 : list(a), v7 : list(a), v8 : list(a), v9 : list(a), v0 : a, v1 : a, v2 : a, v3 : a, v4 : a, v5 : a, v6 : a, v7 : a, v8 : a, v9 : a, v0 : b, v1 : b, v2 : b, v4 : b, v5 : b, v6 : b, v7 : b, v9 : b, v0 : pair(a, b), v1 : pair(a, b), v5 : pair(a, b). f_p(h_a(cons(a; h_a(cons(a; g_a(h_a(cons(a; g_a(f_a(h_a(cons(a; h_a(cons(a; f_a(h_a(cons(a; g_a(f_a(g_a(h_a(nil(a; )), b_0)), g_b(h_b(pair(a, b; h_a(cons(a; g_a(a_1, b_1), v3)), h_b(pair(a, b; g_a(a_1, b_1), h_b(pair(a, b; v3, g_b(h_b(pair(a, b; v4, g_b(v0, a_2))), a_1))))))), f_a(f_a(f_a(h_a(cons(a; h_a(cons(a; f_a(a_2), v1)), v3))))))), nil(a; )))), cons(a; v9, nil(a; )))), cons(a; a_0, cons(a; v8, cons(a; f_a(h_a(cons(a; f_a(g_a(f_a(a_0), b_0)), v9))), cons(a; h_a(cons(a; h_a(v1), nil(a; ))), cons(a; f_a(a_1), v6)))))))), h_b(pair(a, b; f_a(a_0), h_b(pair(a, b; a_2, 

Gbury

module type S = sig
  type t
  val to_string : t -> string
end

module Make(T : S) : S with type t = int = struct
  type t = int
  let to_string i = Printf.sprintf "%d" i
end

Gbury

module Id : sig
  type 'a t
  val hash : 'a t -> int
  val equal : 'a t -> 'a t -> bool
  val create : 'a -> 'a t
end = struct
  type 'a t = {
    id : int;
    contents : 'a;
  }

Gbury

type t = { foo : 'a. 'a -> 'a }

let id = { foo = (fun x -> x) }

let phi id () = id.foo 1, id.foo true