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