path: root/testsuite/tests/typing-gadts/omega07.ml.reference

# * * * * *                       type ('a, 'b) sum = Inl of 'a | Inr of 'b
type zero = Zero
type _ succ
type _ nat = NZ : zero nat | NS : 'a nat -> 'a succ nat
#             type (_, _) seq =
    Snil : ('a, zero) seq
  | Scons : 'a * ('a, 'n) seq -> ('a, 'n succ) seq
#   val l1 : (int, zero succ succ) seq = Scons (3, Scons (5, Snil))
#       *         type (_, _, _) plus =
    PlusZ : 'a nat -> (zero, 'a, 'a) plus
  | PlusS : ('a, 'b, 'c) plus -> ('a succ, 'b, 'c succ) plus
#         val length : ('a, 'n) seq -> 'n nat = <fun>
#   *                     type (_, _, _) app =
    App : ('a, 'p) seq * ('n, 'm, 'p) plus -> ('a, 'n, 'm) app
val app : ('a, 'n) seq -> ('a, 'm) seq -> ('a, 'n, 'm) app = <fun>
# *                           type tp
type nd
type (_, _) fk
type _ shape =
    Tp : tp shape
  | Nd : nd shape
  | Fk : 'a shape * 'b shape -> ('a, 'b) fk shape
#           type tt
type ff
type _ boolean = BT : tt boolean | BF : ff boolean
#                 type (_, _) path =
    Pnone : 'a -> (tp, 'a) path
  | Phere : (nd, 'a) path
  | Pleft : ('x, 'a) path -> (('x, 'y) fk, 'a) path
  | Pright : ('y, 'a) path -> (('x, 'y) fk, 'a) path
#         type (_, _) tree =
    Ttip : (tp, 'a) tree
  | Tnode : 'a -> (nd, 'a) tree
  | Tfork : ('x, 'a) tree * ('y, 'a) tree -> (('x, 'y) fk, 'a) tree
#   val tree1 : (((tp, nd) fk, (nd, nd) fk) fk, int) tree =
  Tfork (Tfork (Ttip, Tnode 4), Tfork (Tnode 4, Tnode 3))
#                     val find : ('a -> 'a -> bool) -> 'a -> ('sh, 'a) tree -> ('sh, 'a) path list =
  <fun>
#             val extract : ('sh, 'a) path -> ('sh, 'a) tree -> 'a = <fun>
#             type (_, _) le =
    LeZ : 'a nat -> (zero, 'a) le
  | LeS : ('n, 'm) le -> ('n succ, 'm succ) le
#       type _ even = EvenZ : zero even | EvenSS : 'n even -> 'n succ succ even
#         type one = zero succ
type two = one succ
type three = two succ
type four = three succ
#       val even0 : zero even = EvenZ
val even2 : two even = EvenSS EvenZ
val even4 : four even = EvenSS (EvenSS EvenZ)
#   val p1 : (two, one, three) plus = PlusS (PlusS (PlusZ (NS NZ)))
#         val summandLessThanSum : ('a, 'b, 'c) plus -> ('a, 'c) le = <fun>
#                                 type (_, _) equal = Eq : ('a, 'a) equal
val convert : ('a, 'b) equal -> 'a -> 'b = <fun>
val sameNat : 'a nat -> 'b nat -> ('a, 'b) equal option = <fun>
#             val smaller : ('a succ, 'b succ) le -> ('a, 'b) le = <fun>
#   type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff
#   * * * * * * * * *                 val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
#               Characters 87-243:
  ..match a, b,le with (* warning *)
    | NZ, m, LeZ _ -> Diff (m, PlusZ m)
    | NS x, NS y, LeS q ->
        match diff q x y with Diff (m, p) -> Diff (m, PlusS p)
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(NS _, NZ, _)
val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
#               val diff : ('a, 'b) le -> 'b nat -> ('a, 'b) diff = <fun>
#             type (_, _) filter = Filter : ('m, 'n) le * ('a, 'm) seq -> ('a, 'n) filter
val leS' : ('m, 'n) le -> ('m, 'n succ) le = <fun>
#                   val filter : ('a -> bool) -> ('a, 'n) seq -> ('a, 'n) filter = <fun>
#                             type (_, _, _) balance =
    Less : ('h, 'h succ, 'h succ) balance
  | Same : ('h, 'h, 'h) balance
  | More : ('h succ, 'h, 'h succ) balance
type _ avl =
    Leaf : zero avl
  | Node : ('hL, 'hR, 'hMax) balance * 'hL avl * int *
      'hR avl -> 'hMax succ avl
type avl' = Avl : 'h avl -> avl'
#                 val empty : avl' = Avl Leaf
val elem : int -> 'h avl -> bool = <fun>
#                           val rotr :
  'n succ succ avl ->
  int -> 'n avl -> ('n succ succ avl, 'n succ succ succ avl) sum = <fun>
#                         val rotl :
  'n avl ->
  int -> 'n succ succ avl -> ('n succ succ avl, 'n succ succ succ avl) sum =
  <fun>
#                                               val ins : int -> 'n avl -> ('n avl, 'n succ avl) sum = <fun>
#           val insert : int -> avl' -> avl' = <fun>
#                                                                                                                                 val del_min : 'n succ avl -> int * ('n avl, 'n succ avl) sum = <fun>
type _ avl_del =
    Dsame : 'n avl -> 'n avl_del
  | Ddecr : ('m succ, 'n) equal * 'm avl -> 'n avl_del
val del : int -> 'n avl -> 'n avl_del = <fun>
#           val delete : int -> avl' -> avl' = <fun>
#                             type red
type black
type (_, _) sub_tree =
    Bleaf : (black, zero) sub_tree
  | Rnode : (black, 'n) sub_tree * int *
      (black, 'n) sub_tree -> (red, 'n) sub_tree
  | Bnode : ('cL, 'n) sub_tree * int *
      ('cR, 'n) sub_tree -> (black, 'n succ) sub_tree
type rb_tree = Root : (black, 'n) sub_tree -> rb_tree
#               type dir = LeftD | RightD
type (_, _) ctxt =
    CNil : (black, 'n) ctxt
  | CRed : int * dir * (black, 'n) sub_tree *
      (red, 'n) ctxt -> (black, 'n) ctxt
  | CBlk : int * dir * ('c1, 'n) sub_tree *
      (black, 'n succ) ctxt -> ('c, 'n) ctxt
#                         val blacken : (red, 'a) sub_tree -> (black, 'a succ) sub_tree = <fun>
type _ crep = Red : red crep | Black : black crep
val color : ('c, 'n) sub_tree -> 'c crep = <fun>
#                   val fill : ('c, 'n) ctxt -> ('c, 'n) sub_tree -> rb_tree = <fun>
#             val recolor :
  dir ->
  int ->
  ('a, 'b) sub_tree ->
  dir ->
  int ->
  (black, 'b succ) sub_tree -> ('c, 'b) sub_tree -> (red, 'b succ) sub_tree =
  <fun>
#             val rotate :
  dir ->
  int ->
  (black, 'a) sub_tree ->
  dir ->
  int ->
  (black, 'a) sub_tree -> (red, 'a) sub_tree -> (black, 'a succ) sub_tree =
  <fun>
#                     val repair : (red, 'n) sub_tree -> ('c, 'n) ctxt -> rb_tree = <fun>
#                     val ins : int -> ('c, 'n) sub_tree -> ('c, 'n) ctxt -> rb_tree = <fun>
#   val insert : int -> rb_tree -> rb_tree = <fun>
#                                                                                                 type _ term =
    Const : int -> int term
  | Add : (int * int -> int) term
  | LT : (int * int -> bool) term
  | Ap : ('a -> 'b) term * 'a term -> 'b term
  | Pair : 'a term * 'b term -> ('a * 'b) term
val ex1 : int term = Ap (Add, Pair (Const 3, Const 5))
val ex2 : (int * int) term =
  Pair (Ap (Add, Pair (Const 3, Const 5)), Const 1)
val eval_term : 'a term -> 'a = <fun>
type _ rep =
    Rint : int rep
  | Rbool : bool rep
  | Rpair : 'a rep * 'b rep -> ('a * 'b) rep
  | Rfun : 'a rep * 'b rep -> ('a -> 'b) rep
type (_, _) equal = Eq : ('a, 'a) equal
val rep_equal : 'a rep -> 'b rep -> ('a, 'b) equal option = <fun>
#                                                               type assoc = Assoc : string * 'a rep * 'a -> assoc
val assoc : string -> 'a rep -> assoc list -> 'a = <fun>
type _ term =
    Var : string * 'a rep -> 'a term
  | Abs : string * 'a rep * 'b term -> ('a -> 'b) term
  | Const : int -> int term
  | Add : (int * int -> int) term
  | LT : (int * int -> bool) term
  | Ap : ('a -> 'b) term * 'a term -> 'b term
  | Pair : 'a term * 'b term -> ('a * 'b) term
val eval_term : assoc list -> 'a term -> 'a = <fun>
#           val ex3 : (int -> int) term =
  Abs ("x", Rint, Ap (Add, Pair (Var ("x", Rint), Var ("x", Rint))))
val ex4 : int term =
  Ap (Abs ("x", Rint, Ap (Add, Pair (Var ("x", Rint), Var ("x", Rint)))),
   Const 3)
val v4 : int = 6
#                                             type rnil
type (_, _, _) rcons
type _ is_row =
    Rnil : rnil is_row
  | Rcons : 'c is_row -> ('a, 'b, 'c) rcons is_row
type (_, _) lam =
    Const : int -> ('e, int) lam
  | Var : 'a -> (('a, 't, 'e) rcons, 't) lam
  | Shift : ('e, 't) lam -> (('a, 'q, 'e) rcons, 't) lam
  | Abs : 'a * (('a, 's, 'e) rcons, 't) lam -> ('e, 's -> 't) lam
  | App : ('e, 's -> 't) lam * ('e, 's) lam -> ('e, 't) lam
type x = X
type y = Y
val ex1 : ((x, 'a -> 'b, (y, 'a, 'c) rcons) rcons, 'b) lam =
  App (Var X, Shift (Var Y))
val ex2 : ('a, ('b -> 'c) -> 'b -> 'c) lam =
  Abs (<poly>, Abs (<poly>, App (Shift (Var <poly>), Var <poly>)))
#                           type _ env =
    Enil : rnil env
  | Econs : 'a * 't * 'e env -> ('a, 't, 'e) rcons env
val eval_lam : 'e env -> ('e, 't) lam -> 't = <fun>
#                               type add = Add
type suc = Suc
val env0 :
  (zero, int, (suc, int -> int, (add, int -> int -> int, rnil) rcons) rcons)
  rcons env = Econs (Zero, 0, Econs (Suc, <fun>, Econs (Add, <fun>, Enil)))
val _0 : ((zero, int, 'a) rcons, int) lam = Var Zero
val suc :
  (('a, 'b, (suc, int -> int, 'c) rcons) rcons, int) lam ->
  (('a, 'b, (suc, int -> int, 'c) rcons) rcons, int) lam = <fun>
val _1 :
  ((zero, int, (suc, int -> int, (add, int -> int -> int, '_a) rcons) rcons)
   rcons, int)
  lam = App (Shift (Var Suc), Var Zero)
val _2 :
  ((zero, int, (suc, int -> int, (add, int -> int -> int, '_a) rcons) rcons)
   rcons, int)
  lam = App (Shift (Var Suc), App (Shift (Var Suc), Var Zero))
val _3 :
  ((zero, int, (suc, int -> int, (add, int -> int -> int, '_a) rcons) rcons)
   rcons, int)
  lam =
  App (Shift (Var Suc),
   App (Shift (Var Suc), App (Shift (Var Suc), Var Zero)))
val add :
  (('a, 'b, ('c, 'd, (add, int -> int -> int, 'e) rcons) rcons) rcons,
   int -> int -> int)
  lam = Shift (Shift (Var Add))
val double :
  (('a, 'b, ('c, 'd, (add, int -> int -> int, 'e) rcons) rcons) rcons,
   int -> int)
  lam =
  Abs (<poly>,
   App (App (Shift (Shift (Shift (Var Add))), Var <poly>), Var <poly>))
val ex3 :
  ((zero, int, (suc, int -> int, (add, int -> int -> int, '_a) rcons) rcons)
   rcons, int)
  lam =
  App
   (Abs (<poly>,
     App (App (Shift (Shift (Shift (Var Add))), Var <poly>), Var <poly>)),
   App (Shift (Var Suc),
    App (Shift (Var Suc), App (Shift (Var Suc), Var Zero))))
#     val v3 : int = 6
#       *                                       type _ rep = I : int rep | Ar : 'a rep * 'b rep -> ('a -> 'b) rep
val compare : 'a rep -> 'b rep -> (string, ('a, 'b) equal) sum = <fun>
#                     type term =
    C of int
  | Ab : string * 'a rep * term -> term
  | Ap of term * term
  | V of string
type _ ctx =
    Cnil : rnil ctx
  | Ccons : 't * string * 'x rep * 'e ctx -> ('t, 'x, 'e) rcons ctx
#                             type _ checked = Cerror of string | Cok : ('e, 't) lam * 't rep -> 'e checked
val lookup : string -> 'e ctx -> 'e checked = <fun>
#                                                   val tc : 'n nat -> 'e ctx -> term -> 'e checked = <fun>
#             val ctx0 :
  (zero, int, (suc, int -> int, (add, int -> int -> int, rnil) rcons) rcons)
  rcons ctx =
  Ccons (Zero, "0", I,
   Ccons (Suc, "S", Ar (I, I), Ccons (Add, "+", Ar (I, Ar (I, I)), Cnil)))
val ex1 : term = Ab ("x", I, Ap (Ap (V "+", V "x"), V "x"))
# val c1 :
  (zero, int, (suc, int -> int, (add, int -> int -> int, rnil) rcons) rcons)
  rcons checked =
  Cok
   (Abs (<poly>,
     App (App (Shift (Shift (Shift (Var Add))), Var <poly>), Var <poly>)),
   Ar (I, I))
# val ex2 : term = Ap (Ab ("x", I, Ap (Ap (V "+", V "x"), V "x")), C 3)
# val c2 :
  (zero, int, (suc, int -> int, (add, int -> int -> int, rnil) rcons) rcons)
  rcons checked =
  Cok
   (App
     (Abs (<poly>,
       App (App (Shift (Shift (Shift (Var Add))), Var <poly>), Var <poly>)),
     Const 3),
   I)
#           val eval_checked : 'a env -> 'a checked -> int = <fun>
#   val v2 : int = 6
#                                             type pexp
type pval
type _ mode = Pexp : pexp mode | Pval : pval mode
type (_, _) tarr
type tint
type (_, _) rel =
    IntR : (tint, int) rel
  | IntTo : ('b, 's) rel -> ((tint, 'b) tarr, int -> 's) rel
type (_, _, _) lam =
    Const : ('a, 'b) rel * 'b -> (pval, 'env, 'a) lam
  | Var : 'a -> (pval, ('a, 't, 'e) rcons, 't) lam
  | Shift : ('m, 'e, 't) lam -> ('m, ('a, 'q, 'e) rcons, 't) lam
  | Lam : 'a *
      ('m, ('a, 's, 'e) rcons, 't) lam -> (pval, 'e, ('s, 't) tarr) lam
  | App : ('m1, 'e, ('s, 't) tarr) lam *
      ('m2, 'e, 's) lam -> (pexp, 'e, 't) lam
#                   val ex1 : (pexp, 'a, tint) lam =
  App (Lam (<poly>, Var <poly>), Const (IntR, <poly>))
val mode : ('m, 'e, 't) lam -> 'm mode = <fun>
#               type (_, _) sub =
    Id : ('r, 'r) sub
  | Bind : 't * ('m, 'r2, 'x) lam *
      ('r, 'r2) sub -> (('t, 'x, 'r) rcons, 'r2) sub
  | Push : ('r1, 'r2) sub -> (('a, 'b, 'r1) rcons, ('a, 'b, 'r2) rcons) sub
type (_, _) lam' = Ex : ('m, 's, 't) lam -> ('s, 't) lam'
#                               val subst : ('m1, 'r, 't) lam -> ('r, 's) sub -> ('s, 't) lam' = <fun>
#       type closed = rnil
type 'a rlam = ((pexp, closed, 'a) lam, (pval, closed, 'a) lam) sum
#                             val rule :
  (pval, closed, ('a, 'b) tarr) lam -> (pval, closed, 'a) lam -> 'b rlam =
  <fun>
#                                 val onestep : ('m, closed, 't) lam -> 't rlam = <fun>
#