Commit c81b8483 authored by charguer's avatar charguer

demos

parent 38377bdd
(**
*
* This file contains unit tests for testing the generation of
* characteristic formulae, their display, and their associated
* tactics.
*)
(*---------polymorphism -----------*)
(********************************************************************)
(* ** Top-level values *)
let poly_top = []
let top_val_int = 5
let poly_let_1 () =
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)
(********************************************************************)
(* ** 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
appto 3 ((+) 1);
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 poly_let_2 () =
let let_poly_nil_pair () =
let x = ([], []) in x
let poly_let_2_same () =
let let_poly_nil_pair_homogeneous () =
let x : ('a list * 'a list) = ([], []) in x
let poly_let_2_partial () =
let let_poly_nil_pair_heterogeneous () =
let x : ('a list * int list) = ([], []) in x
(*---------simple record------------*)
(********************************************************************)
(* ** Pattern-matching *)
type 'a myrec = {
mutable nb : int;
mutable items : 'a list; }
let match_pair_as () =
match (3,4) with (a, (b as c)) as p -> (c,p)
let myrec_incr_nb r =
r.nb <- r.nb + 1
let match_term_when () =
let f x = x + 1 in
match f 3 with
| 0 -> 1
| n when n > 0 -> 2
| _ -> 3
let match_nested () =
let l = [ (1,1), (0,0), (2,2) ] in
match l with
| _::(0,0)::q -> q
| _ -> []
let myrec_length_items r =
List.length r.items
let myrec_inv_length_items r =
r.nb
(********************************************************************)
(* ** Exceptions *)
let myrec_inv_push x r =
r.nb <- r.nb + 1;
r.items <- x :: r.items
let exn_assert_false () =
assert false
let exn_failwith () =
failwith "ok"
(*---------array as sequences------------*)
exception my_exn
let exn_raise () =
raise my_exn
let array_demo () =
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
(********************************************************************)
(* ** Conditionals *)
(*---------if------------*)
let if_true () =
if true then 1 else 0
let if_demo b =
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
let s = ref 5 in
if b
if b
then incr r;
!r
(*
(********************************************************************)
(* ** Records *)
(*---------partial recursive function------------*)
type 'a sitems = {
mutable nb : int;
mutable items : 'a list; }
let rec half x =
if x = 0 then 0
else if x = 1 then assert false
else 1 + half(x-2)
let sitems_build n =
{ nb = n; items = [] }
(*---------partial applications------------*)
let sitems_get_nb r =
r.nb
let sitems_incr_nb r =
r.nb <- r.nb + 1
let add x y =
x + y
let sitems_length_items r =
List.length r.items
let hof x f =
f x
let sitems_push x r =
r.nb <- r.nb + 1;
r.items <- x :: r.items
let test_partial_app_1 () =
let g = add 1 in
g 2
let test_partial_app_2 () =
hof 3 ((+) 1)
(********************************************************************)
(* ** Arrays *)
let func4 a b c d =
a + b + c + d
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
let test_partial_app_3 () =
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
(*---------inlining of code------------*)
let test_inlining () =
hof 3 (fun x -> x + 1)
(********************************************************************)
(* ** 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
(*---------chained lists------------*)
(********************************************************************)
(* ** 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)
type 'a cell = {
content: 'a;
mutable next: 'a cell
}
let newx x q1 q2 =
let machin = {content = x; next = q1} in
machin.next <- q2;
machin
*)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment