module Pa :
  sig
    val CONTEXT_TAC : ((string * pretype) list -> tactic) -> tactic
    val PARSE_IN_CONTEXT : (term -> tactic) -> (string -> tactic)
    val EXISTS_TAC : string -> tactic
    val SUBGOAL_THEN : string -> thm_tactic -> tactic
    val SUBGOAL_TAC : string -> string -> tactic list -> tactic
    val ASM_CASES_TAC : string -> tactic
    val BOOL_CASES_TAC : string -> tactic
    val SPEC_TAC : string * string -> tactic
    val SPEC : string -> thm -> thm
    val SPECL : string list -> thm -> thm
    val GEN : string -> thm -> thm
    val GENL : string list -> thm -> thm
    val X_GEN_TAC : string -> tactic
    val REAL_ARITH : string -> thm
    val REAL_FIELD : string -> thm
    val REAL_RING : string -> thm
    val ARITH_RULE : string -> thm
    val NUM_RING : string -> thm
    val INT_ARITH : string -> thm
    val call_with_interface : (unit -> 'a) -> (term -> 'b) -> string -> 'b
  end
  =
  struct
    let parse_preterm = fst o parse_preterm o lex o explode

    let CONTEXT_TAC ttac (asms,c as g) =
      let vs = frees c @ freesl (map (concl o snd) asms) in
      ttac (map (fun x -> name_of x,pretype_of_type(type_of x)) vs) g

    let PARSE_IN_CONTEXT ttac s =
      CONTEXT_TAC (fun env ->
        ttac (term_of_preterm (retypecheck env (parse_preterm s))))

    let type_of_forall = type_of o fst o dest_forall

    let force_type ?(env=[]) s ty =
      let pty = pretype_of_type ty in
      term_of_preterm (retypecheck env (Typing(parse_preterm s,pty)))

    let BOOL_CONTEXT_TAC ttac s =
      CONTEXT_TAC (fun env -> ttac (force_type ~env s bool_ty))

    let SUBGOAL_THEN s ttac = BOOL_CONTEXT_TAC (C SUBGOAL_THEN ttac) s
    let SUBGOAL_TAC l s tacs = BOOL_CONTEXT_TAC (C (SUBGOAL_TAC l) tacs) s

    let ASM_CASES_TAC = BOOL_CONTEXT_TAC ASM_CASES_TAC
    let BOOL_CASES_TAC = BOOL_CONTEXT_TAC BOOL_CASES_TAC

    let EXISTS_TAC s (_,c as g) =
      CONTEXT_TAC (fun env ->
        EXISTS_TAC (force_type ~env s (type_of (fst (dest_exists c))))) g
        
    let SPEC_TAC (u,x) =
      PARSE_IN_CONTEXT (fun u' -> SPEC_TAC (u',force_type x (type_of u'))) u

    let SPEC s th = SPEC (force_type s (type_of_forall (concl th))) th

    let SPECL tms th =
      try rev_itlist SPEC tms th with Failure _ -> failwith "SPECL"

    let GEN s th =
      GEN (try find ((=) s o name_of) (frees (concl th)) with _ -> parse_term s)
        th

    let GENL = itlist GEN

    let X_GEN_TAC s (_,c as g) = X_GEN_TAC (force_type s (type_of_forall c)) g

    let call_with_interface p f s =
      let i = !the_interface in
      p ();
      let res = f (parse_term s) in
      the_interface := i;
      res

    let [REAL_ARITH;REAL_FIELD;REAL_RING] =
      map (call_with_interface prioritize_real) [REAL_ARITH;REAL_FIELD;REAL_RING]
    let [ARITH_RULE;NUM_RING] =
      map (call_with_interface prioritize_num) [ARITH_RULE;NUM_RING]
    let INT_ARITH = call_with_interface prioritize_int INT_ARITH
  end;;

module Pa =
  struct
    include Pa
    let COMPLEX_FIELD = call_with_interface prioritize_complex COMPLEX_FIELD;;
    let SIMPLE_COMPLEX_ARITH =
      call_with_interface prioritize_complex SIMPLE_COMPLEX_ARITH;
  end;;

let MP_REWRITE_TAC th (_,c as g) =
  let [th] = mk_rewrites true th [] in
  let PART_MATCH = PART_MATCH (lhs o snd o strip_forall o snd o dest_imp) th in
  let th = ref TRUTH in
  ignore (find_term (fun t -> try th := PART_MATCH t; true with _ -> false) c);
  (SUBGOAL_THEN (lhand (concl !th)) (fun x ->
    REWRITE_TAC[MP !th x] THEN STRIP_ASSUME_TAC x)) g;;

let CASES_REWRITE_TAC th (_,c as g) =
  let [th] = mk_rewrites true th [] in
  let PART_MATCH = PART_MATCH (lhs o snd o strip_forall o snd o dest_imp) th in
  let th = ref TRUTH in
  ignore (find_term (fun t -> try th := PART_MATCH t; true with _ -> false) c);
  (ASM_CASES_TAC (lhand (concl !th)) THENL [
    POP_ASSUM (fun x -> REWRITE_TAC[MP !th x] THEN ASSUME_TAC x);
    POP_ASSUM (ASSUME_TAC o REWRITE_RULE[NOT_CLAUSES])]) g;;

let wrap f x = f [x];;

let CONJS xs = end_itlist CONJ xs;;

let rec simp_horn_conv =
  let is_atomic (x,y) = if x = [] then y else failwith "" in
  let rec tl = function [] -> [] | _::xs -> xs in
  fun l ->
    let fixpoint = ref true in
    let l' =
      rev_itlist (fun (hs,cs) (dones,todos) ->
        let atomics = flat (mapfilter is_atomic (dones@todos)) in
        let f = filter (not o C mem atomics) in
        let hs' = f hs and cs' = f cs in
        if not (hs' = hs) or not (cs' = cs) then fixpoint := false;
        if (cs' = [] && cs <> [])
        then (dones,tl todos)
        else ((hs',cs')::dones),tl todos)
      l ([],tl l)
    in
    if !fixpoint then l else simp_horn_conv (fst l');;

let horns_of_term =
  let strip_conj = binops `(/\)` in
  fun t -> map (fun t ->
    try
      let h,c = dest_imp t in
      strip_conj h,strip_conj c
    with _ -> [],[t]) (strip_conj t);;

let term_of_horns =
  let term_of_horn = function
    |[],cs -> list_mk_conj cs
    |_,[] -> (print_endline "ici";`T`)
    |hs,cs -> mk_imp (list_mk_conj hs,list_mk_conj cs)
  in
  list_mk_conj o map term_of_horn;;

let SIMP_HORN_CONV t =
  TAUT (mk_eq (t,((term_of_horns o simp_horn_conv o horns_of_term) t)));;

let SIMP_HORN_TAC =
  REWRITE_TAC[IMP_IMP]
  THEN CONV_TAC (TOP_DEPTH_CONV (CHANGED_CONV SIMP_HORN_CONV));;

let HINT_EXISTS_TAC =
  let strip_conj = binops `/\` in
  let P = `P:bool` in
  fun (hs,c as g) ->
    let hs = map snd hs in
    let vars = flat (map thm_frees hs) in
    let vs,c' = strip_exists c in
    let cs = strip_conj c' in
    let hyp_match c h = term_match (subtract vars vs) c (concl h), h in
    let (_,fosubs,_),h = tryfind (fun c -> tryfind (hyp_match c) hs) cs in
    let ts,vs' = unzip fosubs in
    let vs'' = subtract vs vs' in
    let th = MESON[] (mk_eq(list_mk_exists(vs,P),list_mk_exists(vs'@vs'',P))) in
    (REWRITE_TAC [th] THEN MAP_EVERY EXISTS_TAC ts THEN REWRITE_TAC [h]) g;;

let rec fixpoint f x =
  let y = f x in
  if y = x then y else fixpoint f y;;

let GIMP_IMP =
  GEN_ALL o REWRITE_RULE[IMP_IMP;GSYM CONJ_ASSOC] o DISCH_ALL o fixpoint
    (UNDISCH_ALL o SPEC_ALL);;