diff options
Diffstat (limited to 'testsuite/tests/typing-gadts/term-conv.ml.reference')
| -rw-r--r-- | testsuite/tests/typing-gadts/term-conv.ml.reference | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/testsuite/tests/typing-gadts/term-conv.ml.reference b/testsuite/tests/typing-gadts/term-conv.ml.reference index 3c6b335f67..cff10f16f9 100644 --- a/testsuite/tests/typing-gadts/term-conv.ml.reference +++ b/testsuite/tests/typing-gadts/term-conv.ml.reference @@ -7,48 +7,48 @@ | List : 'a ty -> 'a list ty | Pair : ('a ty * 'b ty) -> ('a * 'b) ty | Fun : ('a ty * 'b ty) -> ('a -> 'b) ty - type ('a, 'b) eq = Eq : ('a, 'a) eq + type (_, _) eq = Eq : ('a, 'a) eq exception CastFailure - val check_eq : 'a ty -> 'b ty -> ('a, 'b) eq - val gcast : 'a ty -> 'b ty -> 'a -> 'b + val check_eq : 't ty -> 't' ty -> ('t, 't') eq + val gcast : 't ty -> 't' ty -> 't -> 't' end # module HOAS : sig - type 'a term = + type _ term = Tag : 't Typeable.ty * int -> 't term | Con : 't -> 't term | Lam : 's Typeable.ty * ('s term -> 't term) -> ('s -> 't) term | App : ('s -> 't) term * 's term -> 't term - val intp : 'a term -> 'a + val intp : 't term -> 't end # module DeBruijn : sig type ('env, 't) ix = ZeroIx : ('env * 't, 't) ix | SuccIx : ('env, 't) ix -> ('env * 's, 't) ix - val to_int : ('a, 'b) ix -> int + val to_int : ('env, 't) ix -> int type ('env, 't) term = Var : ('env, 't) ix -> ('env, 't) term | Con : 't -> ('env, 't) term | Lam : ('env * 's, 't) term -> ('env, 's -> 't) term | App : ('env, 's -> 't) term * ('env, 's) term -> ('env, 't) term - type 'a stack = + type _ stack = Empty : unit stack | Push : 'env stack * 't -> ('env * 't) stack - val prj : ('a, 'b) ix -> 'a stack -> 'b - val intp : ('a, 'b) term -> 'a stack -> 'b + val prj : ('env, 't) ix -> 'env stack -> 't + val intp : ('env, 't) term -> 'env stack -> 't end # module Convert : sig - type ('a, 'b) layout = + type (_, _) layout = EmptyLayout : ('env, unit) layout | PushLayout : 't Typeable.ty * ('env, 'env') layout * ('env, 't) DeBruijn.ix -> ('env, 'env' * 't) layout - val size : ('a, 'b) layout -> int - val inc : ('a, 'b) layout -> ('a * 't, 'b) layout + val size : ('env, 'env') layout -> int + val inc : ('env, 'env') layout -> ('env * 't, 'env') layout val prj : - 'a Typeable.ty -> int -> ('b, 'c) layout -> ('b, 'a) DeBruijn.ix - val cvt : ('a, 'a) layout -> 'b HOAS.term -> ('a, 'b) DeBruijn.term + 't Typeable.ty -> int -> ('env, 'env') layout -> ('env, 't) DeBruijn.ix + val cvt : ('env, 'env) layout -> 't HOAS.term -> ('env, 't) DeBruijn.term val convert : 'a HOAS.term -> (unit, 'a) DeBruijn.term end # module Main : |