open PL

(* Unordered append, tail-recursive *)
let cat =
  let rec aux outlist = function
  | x::xs -> aux (x::outlist) xs
  | [] -> outlist
  in aux

(* Generate a randomly-structured propositional formula, where the leaves are 
   variables (generated by f_var) or constants. *)
let generate_random_prop f_var n_depth =
  let rt () = Random.int 5 in
  let rec aux n rndno = 
    if n = 0
    then match rndno with
    | 0 -> (Constant(True),[])
    | 1 -> (Constant(False),[])
    | _ -> let v = f_var () in (v,[v])
    else match rndno with
    | 0 -> 
      let le,lv = aux (n-1) (rt ()) in
      let re,rv = aux (n-1) (rt ()) in
     (Or(le,re),cat lv rv)
    | 1 ->
      let le,lv = aux (n-1) (rt ()) in
      let re,rv = aux (n-1) (rt ()) in
     (And(le,re),cat lv rv)
    | 2 ->
      let ce,cv = aux (n-1) (rt ()) in
     (Not(ce),cv)
    | 3 ->
      let le,lv = aux (n-1) (rt ()) in
      let re,rv = aux (n-1) (rt ()) in
     (Implies(le,re),cat lv rv)
    | 4 ->
      let le,lv = aux (n-1) (rt ()) in
      let re,rv = aux (n-1) (rt ()) in
     (Iff(le,re),cat lv rv)
    | _ -> failwith "impossible lkjtkjsagt"
  in
  aux n_depth (rt ())

(* New intermediate variable producer *)
let f_newvar_with_prefix prefix =
  let counter = ref 0 in
 (fun () -> 
    let i = !counter in
    incr counter;
    Variable(prefix^string_of_int i))

let random_newvar = f_newvar_with_prefix "_rnd#"

let generate_random_prop_new_vars = generate_random_prop random_newvar 

(* Funny probability trick here, do the math and you'll see why this algorithm
   chooses an element from the list uniformly at random, without knowing a 
   priori the size of the list:  on iteration i, the current element is chosen
   with 1/i probability.  It is mathematically correct (assuming the PRNG is 
   uniform, blah blah).  I learned this trick at a bar in Berkeley from a
   machine learning specialist. *)
let pick_random_element list =
  let rec aux i res = function
  | x::xs -> aux (i+1) (if Random.int i = 0 then Some(x) else res) xs 
  | [] -> res
  in 
  match aux 1 (None) list with
  | None -> invalid_arg "pick_random_element: empty list"
  | Some(x) -> x

let generate_random_prop_existing_vars ev = 
  let f () = pick_random_element ev in
  generate_random_prop f

let _ = 
   let ev = PL.([Variable("a");Variable("b");Variable("c");Variable("d")]) in
   let rec aux i = 
     if i = 4
     then ()
     else 
       let _ = Printf.printf "Depth %d\n" i in
       let rec aux2 j = 
         if j = 100
         then ()
         else
           let _ = Printf.printf "%s\n" (PL.string_of_prop (fst (generate_random_prop_existing_vars ev i))) in
           aux2 (j+1)
       in 
       aux2 0;
       aux (i+1)
  in
  aux 0