(*
%use "Sundry/tautology.fsh" ;;
*)

(* The tautology problem.


(1) Write a program that takes as inputs a number k and a boolean
proposition p in k variables, and determines whether or not p is a
tautology. 


(2) The typical program requires that k be at least as big as the number
of variables in p to succeed. Ensure that the compiler detects such
violations statically. 

*)



(* book-keeping, exponentials  *)

let is_zero n = if n=0 then true else false ;;

let if0 n x y = if is_zero n then x else y ;;

let conjunction x y = x && y ;;

let double_second (m:size) (n:size) = 2 * n ;;

let power_of_2  = primrec double_second (1:size) ;;


let diagarray n = 
  new #x = {n:int_shape} in 
    for i<n do 
      x[i] := i 
    done 
  return x ;;

(* base_bool converts an integer into a vector of booleans (its binary
representation, least significant bits first. The first argument
provides an upper bound on the length of the binary representation. *)

let base_bool_sh n sh = {n:bool_shape} ;;

let base_bool_pr (n:size) (res: var b) (arg: var a) =  

 for i < n do
   res[i] := is_zero (arg mod 2) ;
   arg := arg div 2
 done
;;

let base_bool n = proc2fun (base_bool_pr n) (base_bool_sh n) ;;

(* taut_tests n generates all boolean vectors of length n.
taut n prop checks to see if prop : vec[bool] -> bool 
is true for all vectors of length n *)


let taut_tests (n:size) = map (base_bool n) (diagarray (power_of_2 n)) ;;
let taut n prop = reduce conjunction true (map prop (taut_tests n)) ;;

(* Now build some propositional constructors *)

let K (i:size) v = check (lendim #v > i) v[i] ;;

let conj p q v = (p v) && (q v) ;;
let disj p q v = (p v) || (q v) ;;
let neg p v = not (p v) ;;



(* examples 

let prop1 = disj (conj (K 0) (K 1)) (K 2) ;;


let test1 = taut 3 prop1 ;;
let test2 = taut 2 prop1 ;;

*)