open Pervasives (** * * This file contains unit tests for testing the generation of * characteristic formulae, their display, and their associated * tactics. *) (********************************************************************) (* ** 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 = ([],[]) (********************************************************************) (* ** 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) (********************************************************************) (* ** 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 (********************************************************************) (* ** 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 () = let _x = [] in 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 let _r = appto 3 ((+) 1) in 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 () = let x = [] in x let let_poly_nil_pair () = let x = ([], []) in x let let_poly_nil_pair_homogeneous () = let x : ('a list * 'a list) = ([], []) in x let let_poly_nil_pair_heterogeneous () = let x : ('a list * int list) = ([], []) in x (********************************************************************) (* ** Pattern-matching *) let match_pair_as () = match (3,4) with (a, (b as c)) as p -> (c,p) let match_nested () = let l = [ (1,1); (0,0); (2,2) ] in match l with | _::(0,0)::q -> q | _ -> [] (* not yet supported when clauses let match_term_when () = let f x = x + 1 in match f 3 with | 0 -> 1 | n when n > 0 -> 2 | _ -> 3 *) (********************************************************************) (* ** Fatal Exceptions *) let exn_assert_false () = assert false let exn_failwith () = failwith "ok" exception My_exn let exn_raise () = raise My_exn (********************************************************************) (* ** 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 (********************************************************************) (* ** Conditionals *) let if_true () = if true then 1 else 0 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 = let r = ref 0 in if b then incr r; !r (********************************************************************) (* ** Records *) type 'a sitems = { mutable nb : int; mutable items : 'a list; } let sitems_build n = { nb = n; items = [] } let sitems_get_nb r = r.nb let sitems_incr_nb r = r.nb <- r.nb + 1 let sitems_length_items r = List.length r.items let sitems_push x r = r.nb <- r.nb + 1; r.items <- x :: r.items (********************************************************************) (* ** Arrays *) let array_ops () = let t = Array.make 3 0 in let _x = t.(1) in t.(2) <- 4; let _y = t.(2) in let _z = t.(1) in Array.length t (********************************************************************) (* ** 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 (********************************************************************) (* ** 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) (********************************************************************) (* ** 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)) let type_clashing_with_var = 3 type type_clashing_with_var = int (********************************************************************) (* ** 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 | Algb_B of (int -> 'b) (********************************************************************) (* ** 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.: *) type typerecc1 = | Typerecc_1 of typerecc1 list type typerecc2 = typerecc1 list (********************************************************************) (* ** Local module *) module ModFoo = struct type t = int let x : t = 3 end (********************************************************************) (* ** Local module signature *) module type ModBarType = sig type t val x : t end module ModBar : ModBarType = struct type t = int let x : t = 3 end (********************************************************************) (* ** Functor *) module ModFunctor (Bar : ModBarType) = struct type u = Bar.t let x : u = Bar.x end module ModFunctorTyped (Bar : ModBarType) : ModBarType = struct type t = Bar.t let x : t = Bar.x end (********************************************************************) (* ** TODO: import of auxiliary files, like in examples/DemoMake *)