1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
# module Typeable :
sig
type 'a ty =
Int : int ty
| String : string ty
| List : 'a ty -> 'a list ty
| Pair : ('a ty * 'b ty) -> ('a * 'b) ty
| Fun : ('a ty * 'b ty) -> ('a -> 'b) ty
type (_, _) eq = Eq : ('a, 'a) eq
exception CastFailure
val check_eq : 't ty -> 't' ty -> ('t, 't') eq
val gcast : 't ty -> 't' ty -> 't -> 't'
end
# module HOAS :
sig
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 : '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 : ('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 _ stack =
Empty : unit stack
| Push : 'env stack * 't -> ('env * 't) stack
val prj : ('env, 't) ix -> 'env stack -> 't
val intp : ('env, 't) term -> 'env stack -> 't
end
# module Convert :
sig
type (_, _) layout =
EmptyLayout : ('env, unit) layout
| PushLayout : 't Typeable.ty * ('env, 'env') layout *
('env, 't) DeBruijn.ix -> ('env, 'env' * 't) layout
val size : ('env, 'env') layout -> int
val inc : ('env, 'env') layout -> ('env * 't, 'env') layout
val prj :
'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 :
sig
val i : 'a Typeable.ty -> ('a -> 'a) HOAS.term
val zero : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
val one : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
val two : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
val three : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
val plus :
'a Typeable.ty ->
((('a -> 'a) -> 'a -> 'a) ->
(('a -> 'a) -> 'a -> 'a) -> ('a -> 'a) -> 'a -> 'a)
HOAS.term
val plus_2_3 : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
val i' : (unit, int -> int) DeBruijn.term
val plus_2_3' : (unit, (int -> int) -> int -> int) DeBruijn.term
val eval_plus_2_3' : int
end
#
|
