Demo.ml

open Pervasives

(** 
 *
 * This file contains unit tests for testing the generation of
 * characteristic formulae, their display, and their associated
 * tactics.
 *)


(*--TODO

let f () =
  let r : '_a ref = ref [] in
  !r

let f () =
  let r : int ref = ref [] in
  !r

let f () : 'a list =
  let r : 'a ref = ref [] in
  !r

*)

(********************************************************************)
(* ** Encoding of names *)

(* type renaming_t_ = int   --rejected *)
(* type renaming_t__ = int  --rejected *)
(* type renaming_t1 = C_  --rejected *)

type renaming_t' = int
type renaming_t2 = C'
type 'a renaming_t3 = int 
type 'a_ renaming_t4 = int 

let renaming_demo () =
   (* let x_ = 3 in   --rejected *)
   (* let x__ = 3 in  --rejected *)
   let x = 3 in
   let x' = 3 in
   let x_' = 3 in
   let exists = 3 in
   let array = 3 in
   ()


(********************************************************************)
(* ** Return *) 

let ret_unit x =
  ()

let ret_int () =
  3

let ret_int_pair () =
  (3,4)

let ret_poly () =
  []


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

let seq_ret_unit () =
   ret_unit 1; 
   ret_unit 2; 
   ret_unit 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) 

let let_fun_in_let () =
  let f = (assert (true); fun x -> x) in
  f


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

let app_partial_builtin_add () =
  let f = (+) 1 in
  f 2

let app_partial_builtin_and () =
  let f = (&&) true in
  f false


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

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


(********************************************************************)
(* ** Infix functions *)

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

let infix_aux x y = x +++ y

let (---) = infix_aux


(********************************************************************)
(* ** Lazy binary operators *)

let lazyop_val () =
  if true && (false || true) then 1 else 0

let lazyop_term () =
  let f x = (x = 0) in
  if f 1 || f 0 then 1 else 0

let lazyop_mixed () =
  let f x = (x = 0) in
  if true && (f 1 || (f 0 && true)) then 1 else 0


(********************************************************************)
(* ** Comparison operators *)

let compare_int () =
  (1 <> 0 && 1 <= 2) || (0 = 1 && 1 >= 2 && 1 < 2 && 2 > 1)

let compare_min () =
  (min 0 1)

(*
let compare_float () =
  (1. <> 0. && 1. <= 2.) || (0. = 1. && 1. >= 2. && 1. < 2. && 2. > 1.)
*)

(********************************************************************)
(* ** List operators *)

let list_ops () =
  let x = [1] in
  List.length (List.rev (List.concat (List.append [x] [x; x])))


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

let inlined_fun_arith () =
   let n = 2 in
   1 - (1 / n) + ((2 * 2) / 2) mod (- 3)

let inlined_fun_others n =
  fst (succ n, ignore (pred n))



(********************************************************************)
(* ** 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 = ([],[])

(* TODO

let (top_val_pair_int_1,top_val_pair_int_2) = (1,2)

let (top_val_pair_fun_1,top_val_pair_fun_2) =
  ((fun () -> 1), (fun () -> 1))
*)

(* problematic generalization
let (top_val_pair_fun_1,top_val_pair_fun_2) =
  ((fun x -> x), (fun x -> x))
*)


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



(********************************************************************)
(* ** Type annotations *)

let annot_let () =
   let x : int = 3 in x

let annot_tuple_arg () =
   (3, ([] : int list))

let annot_pattern_var x =
   match (x : int list) with [] -> 1 | _ -> 0

let annot_pattern_constr () =
   match ([] : int list) with [] -> 1 | _ -> 0


(********************************************************************)
(* ** 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
  | _ -> [(2,2)]

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

let assert_let () =
  assert (let x = true in true); 
  3

let assert_seq () =
  let r = ref 0 in
  assert (incr r; true); 
  !r

let assert_in_seq () =
  (assert (true); 3) + 1


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



(********************************************************************)
(* ** Evaluation order *)

let order_app () =
  let r = ref 0 in
  let h () = assert (!r = 2); (fun a b -> a + b) in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); incr r; 1 in
  (h()) (g()) (f())

let order_constr () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  (g() :: f() :: [])

let order_list () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  [ g() ; f() ]

let order_tuple () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  (g(), f())

let order_record () : 'a sitems =
  let r = ref 0 in
  let g () : 'a list = incr r; [] in
  let f () = assert (!r = 1); 1 in
  { nb = f(); items = g() }

(* not yet supported : relaxed value restriction;
   (below, the call to g() results in a fresh type variable).
   The work around is to annotate a bit more, as done above;
   this avoids having a type for [g] that is too general.

let order_record () =
  let r = ref 0 in
  let g () = incr r; [] in
  let f () = assert (!r = 1); 1 in
  { nb = f(); items = g() }
*)

let order_array () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  [| g() ; f() |]


(********************************************************************)
(* ** References *)

let ref_gc () =
  let r1 = ref 1 in
  let r2 = ref 1 in
  let r3 = ref 1 in
  let r4 = ref 1 in
  let x = 
     let r5 = ref 2 in
     !r5 
     in
  x + !r1


(********************************************************************)
(* ** Arrays *)

let array_ops () =
  (* TODO let u = ([||]  : int array) in *)
  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_to_incr r =
   let n = ref 0 in
   for i = 0 to pred r do
      incr n;
   done;
   !n

(*
let for_downto r =
   let n = ref 0 in
   for i = pred r downto 0 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)

let rec rec_mutual_f x =
  if x <= 0 then x else 1 + rec_mutual_g (x-2)
and rec_mutual_g x =
  rec_mutual_f (x+1)


(********************************************************************)
(* ** 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 = { 
   mutable recorda1 : int; 
   mutable recorda2 : int }

(*----*)

type ('a,'b) recordb = 
  { mutable recordb1 : 'a ; 
    mutable recordb2 : 'b -> 'b }

(* not supported: record overloading of fields 
  -- else would need to prefix all fields with the type... *)


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

(*----*)

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

(*----*)

(* not supported: recursive definitions using abbreviation

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

   --> the work around by inlining, e.g.:
*)

type typerecc1 = | Typerecc_1 of typerecc1 list
type typerecc2 = typerecc1 list

(*----*)

(* not supported: recursive definition of inductive and pure records
   -- technically could be supported, if the record was encoded
      on the fly into a coq mutual inductive
type typerecb1 = | Typerecb_1 of typerecb2
 and typerecb2 = { typerecb_2 : typerecb1 }

  --> the work around is to break circularity using polymorphism, e.g.:
*)

type 'a typerecb2 = { mutable typerecb_2 : 'a }
type typerecb1 = | Typerecb_1 of typerecb1 typerecb2

(*----*)

(* Circularity between mutable records and inductive is broken 
   through the indirection at type loc *)

type 'a typerecd1 = { mutable typerecd1_f : 'a typerecd2 }
and 'a typerecd2 = 
   | Typerecd_2a 
   | Typerecd_2b of 'a typerecd1 
   | Typerecd_2c of 'a typerecd3 
and 'a typerecd3 = { mutable typerecd3_f : 'a typerecd2 }



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