Demo.ml 8.7 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
charguer committed
11

charguer's avatar
demos  
charguer committed
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
(********************************************************************)
(* ** 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
50
   let _x = [] in
charguer's avatar
demos  
charguer committed
51 52 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 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
   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
116
  let _r = appto 3 ((+) 1) in
charguer's avatar
demos  
charguer committed
117 118 119 120 121 122 123 124 125
  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

charguer's avatar
charguer committed
126 127 128 129 130
let app_partial_builtin () =
  let f = (+) 1 in
  f 2


charguer's avatar
demos  
charguer committed
131 132 133 134 135 136 137 138
(********************************************************************)
(* ** Over applications *)

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


charguer's avatar
charguer committed
139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
(********************************************************************)
(* ** Infix functions *)

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

let infix_aux x y = x + y

let (---) = infix_aux


(********************************************************************)
(* ** Inlined total functions *)

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


(********************************************************************)
(* ** 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)


(********************************************************************)
(* ** Top-level values *)

let top_val_int = 5

let top_val_int_list : int list = []

let top_val_poly_list = []

let top_val_poly_list_pair = ([],[])


charguer's avatar
demos  
charguer committed
181 182 183 184
(********************************************************************)
(* ** Polymorphic let bindings *)

let let_poly_nil () = 
charguer's avatar
polylet  
charguer committed
185 186
  let x = [] in x

charguer's avatar
demos  
charguer committed
187
let let_poly_nil_pair () = 
charguer's avatar
polylet  
charguer committed
188 189
  let x = ([], []) in x

charguer's avatar
demos  
charguer committed
190
let let_poly_nil_pair_homogeneous () =
charguer's avatar
polylet  
charguer committed
191 192
  let x : ('a list * 'a list) = ([], []) in x
 
charguer's avatar
demos  
charguer committed
193
let let_poly_nil_pair_heterogeneous () =
charguer's avatar
polylet  
charguer committed
194
  let x : ('a list * int list) = ([], []) in x
charguer's avatar
encours  
charguer committed
195 196


charguer's avatar
demos  
charguer committed
197 198
(********************************************************************)
(* ** Pattern-matching *)
charguer's avatar
init  
charguer committed
199

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

charguer's avatar
charguer committed
203 204 205 206 207 208 209
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
210 211 212 213 214 215
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
216
*)
charguer's avatar
init  
charguer committed
217 218


charguer's avatar
demos  
charguer committed
219
(********************************************************************)
charguer's avatar
charguer committed
220
(* ** Fatal Exceptions *)
charguer's avatar
init  
charguer committed
221

charguer's avatar
demos  
charguer committed
222 223
let exn_assert_false () =
   assert false
charguer's avatar
init  
charguer committed
224

charguer's avatar
demos  
charguer committed
225 226
let exn_failwith () =
   failwith "ok"
charguer's avatar
init  
charguer committed
227

charguer's avatar
demos  
charguer committed
228 229
exception My_exn 

charguer's avatar
demos  
charguer committed
230
let exn_raise () =
charguer's avatar
demos  
charguer committed
231
   raise My_exn
charguer's avatar
init  
charguer committed
232 233


charguer's avatar
charguer committed
234 235 236 237 238 239 240 241 242 243 244 245 246 247
(********************************************************************)
(* ** 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
248 249
(********************************************************************)
(* ** Conditionals *)
charguer's avatar
init  
charguer committed
250

charguer's avatar
demos  
charguer committed
251 252
let if_true () =
   if true then 1 else 0
charguer's avatar
init  
charguer committed
253

charguer's avatar
demos  
charguer committed
254 255 256 257 258 259 260 261 262 263 264
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
265
  let r = ref 0 in
charguer's avatar
demos  
charguer committed
266
  if b
charguer's avatar
init  
charguer committed
267 268 269 270
     then incr r; 
  !r


charguer's avatar
demos  
charguer committed
271 272
(********************************************************************)
(* ** Records *)
charguer's avatar
init  
charguer committed
273

charguer's avatar
demos  
charguer committed
274 275 276
type 'a sitems = {
  mutable nb : int;
  mutable items : 'a list; }
charguer's avatar
init  
charguer committed
277

charguer's avatar
demos  
charguer committed
278 279
let sitems_build n =
  { nb = n; items = [] }
charguer's avatar
init  
charguer committed
280

charguer's avatar
demos  
charguer committed
281 282
let sitems_get_nb r =
  r.nb
charguer's avatar
init  
charguer committed
283

charguer's avatar
demos  
charguer committed
284 285
let sitems_incr_nb r =
  r.nb <- r.nb + 1 
charguer's avatar
init  
charguer committed
286

charguer's avatar
demos  
charguer committed
287 288
let sitems_length_items r =
  List.length r.items
charguer's avatar
init  
charguer committed
289

charguer's avatar
demos  
charguer committed
290 291 292
let sitems_push x r =
  r.nb <- r.nb + 1;
  r.items <- x :: r.items
charguer's avatar
init  
charguer committed
293 294


charguer's avatar
demos  
charguer committed
295 296
(********************************************************************)
(* ** Arrays *)
charguer's avatar
init  
charguer committed
297

charguer's avatar
demos  
charguer committed
298 299
let array_ops () =
  let t = Array.make 3 0 in
charguer's avatar
charguer committed
300
  let _x = t.(1) in
charguer's avatar
demos  
charguer committed
301
  t.(2) <- 4;
charguer's avatar
charguer committed
302 303
  let _y = t.(2) in
  let _z = t.(1) in
charguer's avatar
demos  
charguer committed
304
  Array.length t
charguer's avatar
init  
charguer committed
305 306


charguer's avatar
demos  
charguer committed
307 308 309 310 311 312 313 314 315 316 317 318 319 320
(********************************************************************)
(* ** 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
321 322


charguer's avatar
demos  
charguer committed
323 324 325 326 327 328 329 330 331 332
(********************************************************************)
(* ** For loops *)

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

charguer's avatar
charguer committed
333 334 335
(* "for .. down to" not yet supported *)


charguer's avatar
demos  
charguer committed
336 337 338 339 340 341 342
(********************************************************************)
(* ** 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
343 344


charguer's avatar
charguer committed
345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360
(********************************************************************)
(* ** 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
361 362 363
let type_clashing_with_var = 3
type type_clashing_with_var = int

charguer's avatar
charguer committed
364 365 366 367 368 369 370 371 372 373 374 375 376

(********************************************************************)
(* ** 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
377
  | Algb_B of (int -> 'b)
charguer's avatar
charguer committed
378 379 380 381 382 383 384


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

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

charguer's avatar
charguer committed
385 386 387 388
type ('a,'b) recordb = { recordb1 : 'a ; recordb2 : 'b -> 'b }

(* not supported: record overloading of fields 
  -- else would need to prefix all fields with the type... *)
charguer's avatar
charguer committed
389 390 391 392 393 394 395 396


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

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

charguer's avatar
charguer committed
397 398 399
(* not supported: recursive definition of inductive and record
   -- technically could be supported, if the record was encoded
      on the fly into a coq mutual inductive
charguer's avatar
charguer committed
400 401
type typerecb1 = | Typerecb_1 of typerecb2
 and typerecb2 = { typerecb_2 : typerecb1 }
charguer's avatar
charguer committed
402 403

  --> the work around is to break circularity using polymorphism, e.g.:
charguer's avatar
charguer committed
404
*)
charguer's avatar
charguer committed
405

charguer's avatar
charguer committed
406 407 408
type 'a typerecb2 = { typerecb_2 : 'a }
type typerecb1 = | Typerecb_1 of typerecb1 typerecb2

charguer's avatar
charguer committed
409 410 411 412 413
(* not supported: recursive definitions using abbreviation

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

charguer's avatar
charguer committed
414
   --> the work around by inlining, e.g.:
charguer's avatar
charguer committed
415 416
*)

charguer's avatar
charguer committed
417 418
type typerecc1 = | Typerecc_1 of typerecc1 list
type typerecc2 = typerecc1 list
charguer's avatar
charguer committed
419 420 421 422 423 424 425 426 427



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

module ModFoo = struct
   
   type t = int
charguer's avatar
charguer committed
428
   let x : t = 3
charguer's avatar
charguer committed
429 430 431 432 433 434 435

end

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

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

charguer's avatar
charguer committed
437 438
   type t
   val x : t
charguer's avatar
init  
charguer committed
439

charguer's avatar
charguer committed
440 441 442 443 444
end

module ModBar : ModBarType = struct
   
   type t = int
charguer's avatar
charguer committed
445
   let x : t = 3
charguer's avatar
charguer committed
446 447 448 449 450 451 452 453 454 455

end


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

module ModFunctor (Bar : ModBarType) = struct
   
   type u = Bar.t
charguer's avatar
charguer committed
456
   let x : u = Bar.x
charguer's avatar
charguer committed
457 458 459 460 461 462

end

module ModFunctorTyped (Bar : ModBarType) : ModBarType = struct
   
   type t = Bar.t
charguer's avatar
charguer committed
463
   let x : t = Bar.x
charguer's avatar
charguer committed
464 465 466 467 468 469

end


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