(* ========================================================================= *)
(*               Formalization of Electromagnetic Optics                     *)
(*                                                                           *)
(*            (c) Copyright, Sanaz Khan Afshar & Vincent Aravantinos 2011-14 *)
(*                           Hardware Verification Group,                    *)
(*                           Concordia University                            *)
(*                                                                           *)
(*                Contact:   <s_khanaf@encs.concordia.ca>                    *)
(*                           <vincent@encs.concordia.ca>                     *)
(*                                                                           *)
(* This file deals with various utilities.                                   *)
(* ========================================================================= *)

Format.set_margin 154;;

let CHANGED_RULE r thm =
  let thm' = r thm in
  if equals_thm thm thm' then failwith "CHANGED_RULE" else thm';;
let MAP_ASSUMPTIONS f = REPEAT (POP_ASSUM (MP_TAC o f)) THEN REPEAT DISCH_TAC;;
let REMOVE_LETS =
  REPEAT LET_TAC THEN MAP_ASSUMPTIONS (repeat (CONV_RULE let_CONV));;
let REWRITE_ASSUMPTIONS xs = MAP_ASSUMPTIONS (REWRITE_RULE xs);;
let REWRITE_EVERYWHERE xs =
  REWRITE_TAC xs THEN MAP_ASSUMPTIONS (REWRITE_RULE xs);;
let ON_FIRST_GOAL ?(out_of=2) x =
  let rec ( * ) n x = if n<=1 then [] else x :: (n-1) * x in
  x :: out_of * ALL_TAC;;
let STRIP_ASSUMPTIONS = REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;;
let DESTRUCT_PAIR_TAC p =
  CHOOSE_THEN (CHOOSE_THEN (fun x -> PURE_REWRITE_TAC[x]))
    (ISPEC p PAIR_SURJECTIVE);;
let MAP_ANTECEDENT f = DISCH_THEN (MP_TAC o f);;

let exn_to_bool f x = try ignore (f x); true with _ -> false;;

let strip_parentheses s =
  if s.[0] = '(' && s.[String.length s-1] = ')'
  then String.sub s 1 (String.length s-2)
  else s;;
let contains_sub_term_name name t =
  exn_to_bool (find_term (fun x -> ((=) name o strip_parentheses o
    string_of_term) x)) t;;

let REAL_SIMP_TAC thms =
	ASM_REWRITE_TAC ([REAL_MUL_LZERO;REAL_MUL_RZERO;REAL_MUL_RID;REAL_MUL_LID;
    REAL_ADD_LID;REAL_ADD_RID;REAL_SUB_RZERO;REAL_NEG_0] @ thms);;
let COMPLEX_SIMPLIFY_TAC =
  ASM_REWRITE_TAC[COMPLEX_ADD_LID;COMPLEX_MUL_LID;COMPLEX_MUL_LZERO;
    COMPLEX_MUL_RZERO;COMPLEX_SUB_LZERO;COMPLEX_SUB_RZERO;COMPLEX_NEG_0 ];; 

let try_or_id f x = try f x with _ -> x;;

let SINGLE f x = f [x];;
let ASSUME_CONSEQUENCES x =
  ASM (MAP_EVERY (fun y -> try ASSUME_TAC (MATCH_MP x y) with _ -> ALL_TAC))
    [];;
let STRIP_RULE =
  repeat (CHANGED_RULE UNDISCH_ALL o try_or_id SPEC_ALL)
    o REWRITE_RULE[IMP_CONJ];;

let CSQS xs x = map (try_or_id (MATCH_MP x)) xs;; 
let CSQS_THEN xs x ttac = MAP_EVERY ttac (CSQS xs x);;
let ASM_CSQS_THEN x = ASSUM_LIST o C (C CSQS_THEN x);;

let ASM_CSQ_THEN ?(remove=false) ?(match_=true) x ttac =
  (if remove then FIRST_X_ASSUM else FIRST_ASSUM)
    (ttac o (if match_ then MATCH_MP else MP) x);;

let ASM_CSQS_THEN x ttac =
  (* looks absurd, eh? But needed in order to control the execution flow *)
  let ttac x y = ttac x y in 
  REPEAT_TCL (fun y z -> ASM_CSQ_THEN z y ORELSE ttac z) ttac x;;

let LET_SIMP_TAC = REWRITE_TAC[LET_DEF;LET_END_DEF];;

let distrib fs x = map (fun f -> f x) fs;;

let DISTRIB ttacs x = EVERY (distrib ttacs x);;
let LET_DEFs = CONJ LET_DEF LET_END_DEF;;

let GEQ_IMP x = GEN_ALL (MATCH_MP EQ_IMP (SPEC_ALL x));;