1open OUnit
2open Term
3open Term.Notations
4open Extensions
5open Test_helper
6
7let norm_tests =
8  "Norm" >:::
9    [
10      "[(x\\ x) c]" >::
11        (fun () ->
12           let c = uconst "c" in
13           let t = (1 /// db 1) ^^ [c] in
14           let t = hnorm t in
15             assert_term_equal c t) ;
16
17      "[(x\\ y\\ x) a b]" >::
18        (fun () ->
19           let a = uconst "a" in
20           let b = uconst "b" in
21           let t = (2 /// db 2) ^^ [a; b] in
22           let t = hnorm t in
23             assert_term_equal a t) ;
24
25      "[(x\\ y\\ y) a b]" >::
26        (fun () ->
27           let a = uconst "a" in
28           let b = uconst "b" in
29           let t = (2 /// db 1) ^^ [a; b] in
30           let t = hnorm t in
31             assert_term_equal b t) ;
32
33      "[(x\\ y\\ z\\ x)]" >::
34        (fun () ->
35           let t = (3 /// db 3) in
36           let t = hnorm t in
37             assert_term_equal (3 /// db 3) t) ;
38
39      "[(x\\ y\\ z\\ x) a]" >::
40        (fun () ->
41           let a = uconst "a" in
42           let t = (3 /// db 3) ^^ [a] in
43           let t = hnorm t in
44             assert_term_equal (2 /// a) t) ;
45
46      "[(x\\ x (x\\ x)) (x\\y\\ x y)]" >::
47        (fun () ->
48           let t = 1 /// (db 1 ^^ [1 /// db 1]) in
49           let t = t ^^ [ 2 /// (db 2 ^^ [db 1]) ] in
50           let t = hnorm t in
51             assert_term_equal (1 /// ((1 /// db 1) ^^ [db 1]))  t) ;
52      "[(x\\ x (x\\ x)) (x\\y\\ x y) c]" >::
53        (fun () ->
54           let c = uconst "c" in
55           let t = 1 /// (db 1 ^^ [1 /// db 1]) in
56           let t = t ^^ [ 2 /// (db 2 ^^ [db 1]) ; c ] in
57           let t = hnorm t in
58             assert_term_equal c t) ;
59
60      "[x\\ c x]" >::
61        (fun () ->
62           let c = uconst "c" in
63           let t = 1 /// (c ^^ [db 1]) in
64           let t = hnorm t in
65             assert_term_equal (1 /// (c ^^ [db 1])) t) ;
66
67      (* This is a normalization pb which appeared to be causing
68       * a failure in an unification test below. *)
69      "[x\\y\\((a\\b\\ a b) x y)]" >::
70        (fun () ->
71           let ii = 2 /// (db 2 ^^ [db 1]) in
72           let t = 2 /// (ii ^^ [db 2;db 1]) in
73           let t = hnorm t in
74             assert_term_equal (2///(db 2 ^^ [db 1])) t) ;
75
76      (* Test that Term.App is flattened *)
77      "[(a b) c]" >::
78        (fun () ->
79           let a = uconst "a" in
80           let b = uconst "b" in
81           let c = uconst "c" in
82           let t = (a ^^ [b]) ^^ [c] in
83           let t = hnorm t in
84             assert_term_equal (a ^^ [b ; c]) t) ;
85
86      (* Test that Term.Lam is flattened *)
87      "[x\\ (y\\ x)]" >::
88        (fun () ->
89           let t = 1 /// (1 /// db 2) in
90           let t = hnorm t in
91             assert_term_equal (2 /// db 2) t) ;
92    ]
93
94let pprint_tests =
95  "Pprint" >:::
96    [
97      "eval P V" >::
98        (fun () ->
99           let p = uconst "P" in
100           let v = uconst "V" in
101           let t = app (uconst "eval") [p; v] in
102             assert_term_pprint_equal "eval P V" t) ;
103
104      "eval (abs R) (abs R)" >::
105        (fun () ->
106           let absR = (app (uconst "abs") [uconst "R"]) in
107           let t = app (uconst "eval") [absR; absR] in
108             assert_term_pprint_equal "eval (abs R) (abs R)" t) ;
109
110      "A => B" >::
111        (fun () ->
112           let a = uconst "A" in
113           let b = uconst "B" in
114           let t = app (uconst "=>") [a; b] in
115             assert_term_pprint_equal "A => B" t) ;
116
117      "pi x\\eq x x" >::
118        (fun () ->
119           let t = app (uconst "pi") [1 /// (app (uconst "eq") [db 1; db 1])] in
120             assert_term_pprint_equal "pi x1\\eq x1 x1" t) ;
121
122      "pi x\\typeof x U => typeof (R x) T" >::
123        (fun () ->
124           let typeofxU = app (uconst "typeof") [db 1; uconst "U"] in
125           let rx = app (uconst "R") [db 1] in
126           let typeofRxT = app (uconst "typeof") [rx; uconst "T"] in
127           let t = app (uconst "pi")
128             [1 /// (app (uconst "=>") [typeofxU; typeofRxT])] in
129             assert_term_pprint_equal
130               "pi x1\\typeof x1 U => typeof (R x1) T" t) ;
131
132      "pi (A B)" >::
133        (fun () ->
134           let t = app (uconst "pi") [app (uconst "A") [uconst "B"]] in
135             assert_term_pprint_equal "pi (A B)" t) ;
136
137      "((pi x\\p x) => qx) != (pi x\\(p x => q x))" >::
138        (fun () ->
139          let p = const "p" (tyarrow [tybase (atybase "x")] oty) in
140          let q = const "q" (tyarrow [tybase (atybase "x")] oty) in
141          let mkpi x ty f =
142            app (const "pi" (tyarrow [tyarrow [ty] oty] oty)) [lambda [x, ty] f] in
143          let mkimp f g =
144            app (const "=>" (tyarrow [oty ; oty] oty)) [f ; g] in
145          let ity = tybase (atybase "i") in
146          let t1 =
147            mkpi "x" ity (mkimp (app p [db 1]) (app q [db 1])) |> term_to_string in
148          let t2 =
149            mkimp (mkpi "x" ity (app p [db 1])) (app q [db 1]) |> term_to_string in
150          assert_bool (t1 ^ " == " ^ t2) (t1 <> t2)) ;
151    ]
152
153let typing_tests =
154  "Typing" >:::
155    [
156      "F:(a->b->c) A:a B:b" >::
157        (fun () ->
158           let f = const "F" (tyarrow [aty; bty] cty) in
159           let a = const "A" aty in
160           let b = const "B" bty in
161             assert_ty_equal cty (tc [] (f ^^ [a; b]))) ;
162
163      "x:a\\y:b\\x" >::
164        (fun () ->
165           assert_ty_equal
166             (tyarrow [aty; bty] aty)
167             (tc [] ([("x",aty); ("y",bty)] // db 2))) ;
168    ]
169
170let binding_tests =
171  "Binding" >:::
172    [
173      "Should not bind variable to itself" >::
174        (fun () ->
175           let v1 = uvar Logic "v1" 0 in
176             assert_raises_any
177               (fun () -> bind v1 v1)) ;
178
179      "Should not bind variable to itself (2)" >::
180        (fun () ->
181           let v1 = uvar Logic "v1" 0 in
182           let v2 = uvar Logic "v2" 0 in
183             bind v1 v2 ;
184             assert_raises_any
185               (fun () -> bind v2 v1)) ;
186    ]
187
188let abstract_tests =
189  "Abstract" >:::
190    [
191      "Should not capture unprotected dB's (single layer)" >::
192        (fun () ->
193          let g = uconst "g" in
194          let h = uconst "h" in
195          let x = uconst "X" in
196          (*    `1 (g (y\ h `1 X)) *)
197          let t = db 1 ^^ [(g ^^ [1 /// (h ^^ [db 1; x])])] in
198          let actual = abstract "X" emptyty t in
199          (* x\ `2 (g (y\ h y  x)) *)
200          let expected = 1 /// (db 2 ^^ [(g ^^ [1 /// (h ^^ [db 1; db 2])])]) in
201          assert_term_equal expected actual) ;
202
203      "Should not capture unprotected dB's (multilayer)" >::
204        (fun () ->
205          let x = uconst "X" in
206          let y = uconst "Y" in
207          let z = uconst "Z" in
208          (*       X `1 (w\ Y w) Z *)
209          let t = x ^^ [db 1; (1 /// (y ^^ [db 1])); z] in
210          let actual = abstract "Y" emptyty (abstract "Z" emptyty t) in
211          (* y\ z\ X `3 (w\ y w) z *)
212          let expected = 2 /// (x ^^ [db 3; (1 /// (db 3 ^^ [db 1])); db 1]) in
213          assert_term_equal expected actual) ;
214    ]
215
216let tests =
217  "Term" >:::
218    [
219      norm_tests;
220      pprint_tests;
221      typing_tests;
222      binding_tests;
223      abstract_tests
224    ]
225