Demo.ml 8.16 KB
Newer Older
charguer's avatar
charguer committed
1 2
open Pervasives

charguer's avatar
demos  
charguer committed
3 4 5 6 7 8
(** 
 *
 * This file contains unit tests for testing the generation of
 * characteristic formulae, their display, and their associated
 * tactics.
 *)
charguer's avatar
init  
charguer committed
9

charguer's avatar
encours  
charguer committed
10

charguer's avatar
demos  
charguer committed
11 12
(********************************************************************)
(* ** Top-level values *)
charguer's avatar
encours  
charguer committed
13

charguer's avatar
demos  
charguer committed
14
let top_val_int = 5
charguer's avatar
polylet  
charguer committed
15

charguer's avatar
demos  
charguer committed
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35
let top_val_int_list : int list = []

let top_val_poly_list = []

let top_val_poly_list_pair = ([],[])


(********************************************************************)
(* ** Polymorphic functions *)

let top_fun_poly_id x =
  x

let top_fun_poly_proj1 (x,y) =
  x

let top_fun_poly_pair_homogeneous (x:'a) (y:'a) =
  (x,y)


charguer's avatar
charguer committed
36 37 38 39 40 41 42 43 44 45
(********************************************************************)
(* ** Infix functions *)

let (+++) x y = x + y  

let infix_aux x y = x + y

let (---) = infix_aux


charguer's avatar
charguer committed
46 47 48 49 50 51 52
(********************************************************************)
(* ** Inlined total functions *)

let f () =
   1 - 1/(-1) + (2 / 2) mod 3


charguer's avatar
demos  
charguer committed
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
(********************************************************************)
(* ** Return *)

let ret_unit () =
  ()

let ret_int () =
  3

let ret_int_pair () =
  (3,4)

let ret_poly () =
  []


(********************************************************************)
(* ** Sequence *)

let seq_noop () =
   let f x = () in
   f 1; 
   f 2; 
   f 3


(********************************************************************)
(* ** Let-value *)

let let_val_int () =
   let x = 3 in
   x

let let_val_pair_int () =
   let x = (3,4) in
   x

let let_val_poly () =
charguer's avatar
charguer committed
91
   let _x = [] in
charguer's avatar
demos  
charguer committed
92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
   3


(********************************************************************)
(* ** Let-pattern *)

let let_pattern_pair_int () =
   let (x,y) = (3,4) in
   x

let let_pattern_pair_int_wildcard () =
   let (x,_) = (3,4) in
   x


(********************************************************************)
(* ** Let-term *)

let let_term_nested_id_calls () =
   let f x = x in
   let a = f (f (f 2)) in
   a

let let_term_nested_pairs_calls () =
   let f x y = (x,y) in
   let a = f (f 1 2) (f 3 (f 4 5)) in
   a


(********************************************************************)
(* ** Let-function *)

let let_fun_const () =
  let f () = 3 in
  f()

let let_fun_poly_id () =
  let f x = x in
  f 3

let let_fun_poly_pair_homogeneous () =
  let f (x:'a) (y:'a) = (x,y) in
  f 3 3

let let_fun_on_the_fly () =
  (fun x f -> f x) 3 (fun x -> x+1) 


(********************************************************************)
(* ** Partial applications *)

let app_partial_2_1 () =
   let f x y = (x,y) in
   f 3

let app_partial_3_2 () =
   let f x y z = (x,z) in
   f 2 4

let app_partial_add () =
  let add x y = x + y in
  let g = add 1 in g 2
 
let app_partial_appto () =
  let appto x f = f x in
charguer's avatar
charguer committed
157
  let _r = appto 3 ((+) 1) in
charguer's avatar
demos  
charguer committed
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
  appto 3 (fun x -> x + 1)

let test_partial_app_arities () =
   let func4 a b c d = a + b + c + d in
   let f1 = func4 1 in
   let f2 = func4 1 2 in
   let f3 = func4 1 2 3 in
   f1 2 3 4 + f2 3 4 + f3 4


(********************************************************************)
(* ** Over applications *)

let app_over_id () =
   let f x = x in
   f f 3


(********************************************************************)
(* ** Polymorphic let bindings *)

let let_poly_nil () = 
charguer's avatar
polylet  
charguer committed
180 181
  let x = [] in x

charguer's avatar
demos  
charguer committed
182
let let_poly_nil_pair () = 
charguer's avatar
polylet  
charguer committed
183 184
  let x = ([], []) in x

charguer's avatar
demos  
charguer committed
185
let let_poly_nil_pair_homogeneous () =
charguer's avatar
polylet  
charguer committed
186 187
  let x : ('a list * 'a list) = ([], []) in x
 
charguer's avatar
demos  
charguer committed
188
let let_poly_nil_pair_heterogeneous () =
charguer's avatar
polylet  
charguer committed
189
  let x : ('a list * int list) = ([], []) in x
charguer's avatar
encours  
charguer committed
190 191


charguer's avatar
demos  
charguer committed
192 193
(********************************************************************)
(* ** Pattern-matching *)
charguer's avatar
init  
charguer committed
194

charguer's avatar
demos  
charguer committed
195 196
let match_pair_as () =
   match (3,4) with (a, (b as c)) as p -> (c,p)
charguer's avatar
init  
charguer committed
197

charguer's avatar
charguer committed
198 199 200 201 202 203 204
let match_nested () =
  let l = [ (1,1); (0,0); (2,2) ] in
  match l with
  | _::(0,0)::q -> q
  | _ -> []

(* not yet supported when clauses
charguer's avatar
demos  
charguer committed
205 206 207 208 209 210
let match_term_when () =
   let f x = x + 1 in
   match f 3 with 
   | 0 -> 1
   | n when n > 0 -> 2
   | _ -> 3
charguer's avatar
charguer committed
211
*)
charguer's avatar
init  
charguer committed
212 213


charguer's avatar
demos  
charguer committed
214
(********************************************************************)
charguer's avatar
charguer committed
215
(* ** Fatal Exceptions *)
charguer's avatar
init  
charguer committed
216

charguer's avatar
demos  
charguer committed
217 218
let exn_assert_false () =
   assert false
charguer's avatar
init  
charguer committed
219

charguer's avatar
demos  
charguer committed
220 221
let exn_failwith () =
   failwith "ok"
charguer's avatar
init  
charguer committed
222

charguer's avatar
demos  
charguer committed
223 224
exception My_exn 

charguer's avatar
demos  
charguer committed
225
let exn_raise () =
charguer's avatar
demos  
charguer committed
226
   raise My_exn
charguer's avatar
init  
charguer committed
227 228


charguer's avatar
charguer committed
229 230 231 232 233 234 235 236 237 238 239 240 241 242
(********************************************************************)
(* ** Assertions *)

let assert_true () =
  assert true; 3

let assert_pos x =
  assert (x > 0); 3

let assert_same (x:int) (y:int) =
  assert (x = y); 3



charguer's avatar
demos  
charguer committed
243 244
(********************************************************************)
(* ** Conditionals *)
charguer's avatar
init  
charguer committed
245

charguer's avatar
demos  
charguer committed
246 247
let if_true () =
   if true then 1 else 0
charguer's avatar
init  
charguer committed
248

charguer's avatar
demos  
charguer committed
249 250 251 252 253 254 255 256 257 258 259
let if_term () =
   let f x = true in
   if f 0 then 1 else 0

let if_else_if () =
   let f x = false in
   if f 0 then 1 
   else if f 1 then 2
   else 0

let if_then_no_else b =
charguer's avatar
init  
charguer committed
260
  let r = ref 0 in
charguer's avatar
demos  
charguer committed
261
  if b
charguer's avatar
init  
charguer committed
262 263 264 265
     then incr r; 
  !r


charguer's avatar
demos  
charguer committed
266 267
(********************************************************************)
(* ** Records *)
charguer's avatar
init  
charguer committed
268

charguer's avatar
demos  
charguer committed
269 270 271
type 'a sitems = {
  mutable nb : int;
  mutable items : 'a list; }
charguer's avatar
init  
charguer committed
272

charguer's avatar
demos  
charguer committed
273 274
let sitems_build n =
  { nb = n; items = [] }
charguer's avatar
init  
charguer committed
275

charguer's avatar
demos  
charguer committed
276 277
let sitems_get_nb r =
  r.nb
charguer's avatar
init  
charguer committed
278

charguer's avatar
demos  
charguer committed
279 280
let sitems_incr_nb r =
  r.nb <- r.nb + 1 
charguer's avatar
init  
charguer committed
281

charguer's avatar
demos  
charguer committed
282 283
let sitems_length_items r =
  List.length r.items
charguer's avatar
init  
charguer committed
284

charguer's avatar
demos  
charguer committed
285 286 287
let sitems_push x r =
  r.nb <- r.nb + 1;
  r.items <- x :: r.items
charguer's avatar
init  
charguer committed
288 289


charguer's avatar
demos  
charguer committed
290 291
(********************************************************************)
(* ** Arrays *)
charguer's avatar
init  
charguer committed
292

charguer's avatar
demos  
charguer committed
293 294
let array_ops () =
  let t = Array.make 3 0 in
charguer's avatar
charguer committed
295
  let _x = t.(1) in
charguer's avatar
demos  
charguer committed
296
  t.(2) <- 4;
charguer's avatar
charguer committed
297 298
  let _y = t.(2) in
  let _z = t.(1) in
charguer's avatar
demos  
charguer committed
299
  Array.length t
charguer's avatar
init  
charguer committed
300 301


charguer's avatar
demos  
charguer committed
302 303 304 305 306 307 308 309 310 311 312 313 314 315
(********************************************************************)
(* ** While loops *)

let while_decr () =
   let n = ref 3 in
   let c = ref 0 in
   while !n > 0 do 
      incr c;
      decr n;
   done;
   !c

let while_false () =
   while false do () done
charguer's avatar
init  
charguer committed
316 317


charguer's avatar
demos  
charguer committed
318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334
(********************************************************************)
(* ** For loops *)

let for_incr () =
   let n = ref 0 in
   for i = 1 to 10 do
      incr n;
   done;
   !n

(********************************************************************)
(* ** Recursive function *)

let rec rec_partial_half x =
  if x = 0 then 0
  else if x = 1 then assert false
  else 1 + rec_partial_half(x-2)
charguer's avatar
init  
charguer committed
335 336


charguer's avatar
charguer committed
337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352
(********************************************************************)
(* ** External *)

external external_func : int -> 'a -> 'a array = "%external_func"



(********************************************************************)
(* ** Type abbreviation *)

type type_intpair = (int * int)

type 'a type_homo_pair = ('a * 'a)

type ('a,'b) type_poly_pair = (('a * 'b) * ('a * 'b))

charguer's avatar
charguer committed
353 354 355
let type_clashing_with_var = 3
type type_clashing_with_var = int

charguer's avatar
charguer committed
356 357 358 359 360 361 362 363 364 365 366 367 368

(********************************************************************)
(* ** Type algebraic *)

type 'a alga_three = 
  | Alga_A 
  | Alga_B of int * int 
  | Alga_C of (int * int)
  | Alga_D of 'a 
  | Alga_E of 'a * ('a -> 'a)

type ('a,'b) algb_erase = 
  | Algb_A of 'a
charguer's avatar
charguer committed
369
  | Algb_B of (int -> 'b)
charguer's avatar
charguer committed
370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396


(********************************************************************)
(* ** Type record *)

type recorda = { recorda1 : int; recorda2 : int }

type ('a,'b) recordb = { recorda1 : 'a ; recorda2 : 'b -> 'b }


(********************************************************************)
(* ** Type mutual *)

type typereca1 = | Typereca_1 of typereca2
 and typereca2 = | Typereca_2 of typereca1

type typerecb1 = | Typerecb_1 of typerecb2
 and typerecb2 = { typerecb_2 : typerecb1 }

(* not supported: recursive definitions using abbreviation

type typerecb1 = | Typerecb_1 of typerecb2
 and typerecb2 = typerecb1 list

   work around by inlining, e.g.:
*)

charguer's avatar
charguer committed
397 398
type typerecc1 = | Typerecc_1 of typerecc1 list
type typerecc2 = typerecc1 list
charguer's avatar
charguer committed
399 400 401 402 403 404 405 406 407



(********************************************************************)
(* ** Local module *)

module ModFoo = struct
   
   type t = int
charguer's avatar
charguer committed
408
   let x : t = 3
charguer's avatar
charguer committed
409 410 411 412 413 414 415

end

(********************************************************************)
(* ** Local module signature *)

module type ModBarType = sig
charguer's avatar
init  
charguer committed
416

charguer's avatar
charguer committed
417 418
   type t
   val x : t
charguer's avatar
init  
charguer committed
419

charguer's avatar
charguer committed
420 421 422 423 424
end

module ModBar : ModBarType = struct
   
   type t = int
charguer's avatar
charguer committed
425
   let x : t = 3
charguer's avatar
charguer committed
426 427 428 429 430 431 432 433 434 435

end


(********************************************************************)
(* ** Functor *)

module ModFunctor (Bar : ModBarType) = struct
   
   type u = Bar.t
charguer's avatar
charguer committed
436
   let x : u = Bar.x
charguer's avatar
charguer committed
437 438 439 440 441 442

end

module ModFunctorTyped (Bar : ModBarType) : ModBarType = struct
   
   type t = Bar.t
charguer's avatar
charguer committed
443
   let x : t = Bar.x
charguer's avatar
charguer committed
444 445 446 447 448 449

end


(********************************************************************)
(* ** TODO: import of auxiliary files, like in examples/DemoMake *)