structure markerLib :> markerLib =
struct

open HolKernel boolLib markerTheory markerSyntax;

val ERR = mk_HOL_ERR "markerLib" ;

(*---------------------------------------------------------------------------*)
(* Support for "short-term markers".                                         *)
(*---------------------------------------------------------------------------*)

val stmark_term = REWR_CONV (GSYM stmarker_def)

fun stmark_conjunct P tm = let
in
  if is_conj tm then
    LAND_CONV (stmark_conjunct P) ORELSEC RAND_CONV (stmark_conjunct P)
  else if P tm then stmark_term
  else NO_CONV
end tm

fun stmark_disjunct P tm = let
in
  if is_disj tm then
    LAND_CONV (stmark_disjunct P) ORELSEC RAND_CONV (stmark_disjunct P)
  else if P tm then stmark_term
  else NO_CONV
end tm

fun is_stmarked t = same_const stmarker_tm (rator t) handle HOL_ERR _ => false

val [comm, assoc, commassoc] = CONJUNCTS (SPEC_ALL markerTheory.move_left_conj)

fun move_stmarked_conj_left tm = let
in
  if is_stmarked tm then ALL_CONV
  else if is_conj tm then
    (LAND_CONV move_stmarked_conj_left THENC TRY_CONV (REWR_CONV assoc))
      ORELSEC
    (RAND_CONV move_stmarked_conj_left THENC
     (REWR_CONV commassoc ORELSEC REWR_CONV comm))
  else NO_CONV
end tm

val move_stmarked_conj_left =
    move_stmarked_conj_left THENC
    (LAND_CONV (REWR_CONV stmarker_def) ORELSEC REWR_CONV stmarker_def)

val move_stmarked_conj_right =
    PURE_REWRITE_CONV [move_right_conj] THENC
    (RAND_CONV (REWR_CONV stmarker_def) ORELSEC REWR_CONV stmarker_def)
val move_stmarked_disj_left =
    PURE_REWRITE_CONV [move_left_disj] THENC
    (LAND_CONV (REWR_CONV stmarker_def) ORELSEC REWR_CONV stmarker_def)

val move_stmarked_disj_right =
    PURE_REWRITE_CONV [move_right_conj] THENC
    (RAND_CONV (REWR_CONV stmarker_def) ORELSEC REWR_CONV stmarker_def)

fun move_conj_left P = stmark_conjunct P THENC move_stmarked_conj_left
fun move_conj_right P = stmark_conjunct P THENC move_stmarked_conj_right
fun move_disj_left P = stmark_disjunct P THENC move_stmarked_disj_left
fun move_disj_right P = stmark_disjunct P THENC move_stmarked_disj_right

(*---------------------------------------------------------------------------*)
(* Dealing with simplifier directives encoded as tags on theorems.           *)
(*---------------------------------------------------------------------------*)

fun AC th1 th2 =
  EQ_MP (SYM (SPECL [concl th1, concl th2] markerTheory.AC_DEF))
        (CONJ th1 th2);

fun unAC th = let val th1 = PURE_REWRITE_RULE [AC_DEF] th
              in (CONJUNCT1 th1, CONJUNCT2 th1)
              end;

fun Cong th = EQ_MP (SYM(SPEC (concl th) markerTheory.Cong_def)) th;

fun unCong th = PURE_REWRITE_RULE [Cong_def] th;

fun Excl nm =
    let val v = mk_var(nm, alpha)
    in
      EQT_ELIM (SPEC v markerTheory.Exclude_def)
    end

fun mk_marker_const nm = prim_mk_const{Thy = "marker", Name = nm}
val Excl_t = mk_marker_const "Exclude"
fun destExcl th =
    let val c = concl th
        val f = rator c
    in
      if same_const Excl_t f then SOME (#1 (dest_var (rand c)))
      else NONE
    end handle HOL_ERR _ => NONE

val Req0_t = mk_marker_const "Req0"
val Req0_th = EQT_ELIM markerTheory.Req0_def
val ReqD_t = mk_marker_const "ReqD"
val ReqD_th = EQT_ELIM markerTheory.ReqD_def
val mk_Req0 = ADD_ASSUM Req0_t
val mk_ReqD = ADD_ASSUM ReqD_t

fun dest_Req0 th =
    if HOLset.member(hypset th, Req0_t) then SOME (PROVE_HYP Req0_th th)
    else NONE
fun dest_ReqD th =
    if HOLset.member(hypset th, ReqD_t) then SOME (PROVE_HYP ReqD_th th)
    else NONE

fun req0_modify tac th =
    case dest_Req0 th of
        NONE => (tac,th)
      | SOME th => (Ho_Rewrite.REQUIRE0_TAC th o tac, th)
fun reqD_modify tac th =
    case dest_ReqD th of
        NONE => (tac,th)
      | SOME th => (Ho_Rewrite.REQUIRE_DECREASE_TAC th o tac, th)

fun mk_require_tac tac thl =
    let
      fun recurse (accths,acctac) ths =
          case ths of
              [] => acctac (List.rev accths)
            | th::rest =>
              let
                val (tac,th) = req0_modify tac th
                val (tac,th) = reqD_modify tac th
              in
                recurse (th::accths,tac) rest
              end
    in
      recurse ([], tac) thl
    end

(*---------------------------------------------------------------------------*)
(* Support for abbreviations.                                                *)
(*---------------------------------------------------------------------------*)

val DeAbbrev = CONV_RULE (REWR_CONV Abbrev_def)

fun Abbrev_wrap eqth =
    EQ_MP (SYM (Thm.SPEC (concl eqth) Abbrev_def)) eqth

fun ABB l r =
 CHOOSE_THEN (fn th => SUBST_ALL_TAC th THEN ASSUME_TAC (Abbrev_wrap(SYM th)))
             (Thm.EXISTS(mk_exists(l, mk_eq(r, l)), r) (Thm.REFL r));

fun ABBREV_TAC eq = let val (l,r) = dest_eq eq in ABB l r end;

local
   val match_var_or_const = ref true
in
   val () = Feedback.register_btrace
               ("PAT_ABBREV_TAC: match var/const", match_var_or_const)

   fun PAT_ABBREV_TAC fv_set eq (g as (asl, w)) =
      let
         open HOLset
         val (l, r) = dest_eq eq
         val rvs = FVL [r] empty_tmset
         val l' = gen_variant Parse.is_constname ""
                              (listItems(union(fv_set, rvs))) l
         fun matchr t =
           case raw_match [] fv_set r t ([],[]) of
               ((tmsub, _), (tysub, _)) => (tmsub, tysub)
         fun finder (bvs, t) =
           case List.find (fn v => HOLset.member(rvs, v)) bvs of
               SOME _ => NONE
             | NONE =>
               if (is_var t orelse is_const t) andalso not (!match_var_or_const)
               then NONE
               else
                 case Lib.total matchr t of
                     NONE => NONE
                   | SOME (tmsub, tysub) =>
                     let
                       open HOLset
                       val bv_set = addList(empty_tmset, bvs)
                       fun badt t =
                         not (isEmpty (intersection (FVL [t] empty_tmset,
                                                     bv_set)))
                     in
                       case List.find (fn {redex,residue=t} => badt t) tmsub of
                           NONE => SOME(t, tysub)
                         | SOME _ => NONE
                     end
      in
         case gen_find_term finder w of
            NONE => raise ERR "PAT_ABBREV_TAC" "No matching term found"
          | SOME (t, tysub) => ABB (Term.inst tysub l') t g
      end
end

fun fixed_tyvars ctxt pattern =
  Lib.U (map type_vars_in_term (op_intersect aconv ctxt (free_vars pattern)))

fun ABB' {redex=l,residue=r} = ABB l r

val safe_inst_cmp = let
  fun img {redex,residue} =
      (term_size residue, (residue, #1 (dest_var redex) handle HOL_ERR _ => ""))
  val cmp = pair_compare
             (flip_cmp Int.compare, pair_compare (Term.compare, String.compare))
in
  inv_img_cmp img cmp
end
val safe_inst_sort =
    List.filter
      (fn {redex,residue} => String.sub(#1 (dest_var redex),0) <> #"_") o
    Listsort.sort safe_inst_cmp

fun MATCH_ABBREV_TAC fv_set pattern (g as (asl, w)) = let
  val ctxt = HOLset.listItems fv_set
  val (tminst,_) = match_terml (fixed_tyvars ctxt pattern) fv_set pattern w
in
  MAP_EVERY ABB' (safe_inst_sort tminst) g
end

fun MATCH_ASSUM_ABBREV_TAC fv_set pattern (g as (asl, w)) = let
  val ctxt = HOLset.listItems fv_set
  val fixed = fixed_tyvars ctxt pattern
  fun find [] = raise ERR "MATCH_ASSUM_ABBREV_TAC" "No matching assumption found"
    | find (asm::tl) =
      case total (match_terml fixed fv_set pattern) asm of
        NONE => find tl
      | SOME (tminst,_) => MAP_EVERY ABB' (safe_inst_sort tminst) g
                           handle HOL_ERR e => find tl
in find asl end

fun HO_MATCH_ABBREV_TAC fv_set pattern (gl as (asl,w)) =
 let val ctxt = HOLset.listItems fv_set
     val (tminst, tyinst) = ho_match_term (fixed_tyvars ctxt pattern) fv_set pattern w
     val unbeta_goal =
        Tactical.default_prover(mk_eq(w, subst tminst (inst tyinst pattern)),
                                BETA_TAC THEN REFL_TAC)
in
  CONV_TAC (K unbeta_goal) THEN MAP_EVERY ABB' (safe_inst_sort tminst)
end gl;

fun UNABBREV_TAC s =
 FIRST_X_ASSUM(SUBST_ALL_TAC o
               assert(equal s o fst o dest_var o lhs o concl) o
               DeAbbrev);

val UNABBREV_ALL_TAC =
 let fun ttac th0 =
      let val th = DeAbbrev th0
      in SUBST_ALL_TAC th ORELSE ASSUME_TAC th
      end
 in
  REPEAT (FIRST_X_ASSUM ttac)
end

fun RM_ABBREV_TAC s =
  FIRST_X_ASSUM (K ALL_TAC o
                 assert(equal s o fst o dest_var o lhs o concl) o
                 DeAbbrev)

val RM_ALL_ABBREVS_TAC = REPEAT (FIRST_X_ASSUM (K ALL_TAC o DeAbbrev))

(*---------------------------------------------------------------------------*)
(* Given an abbreviation context, and a goal with possibly more abbrevs,     *)
(* reabbreviate the goal.                                                    *)
(*---------------------------------------------------------------------------*)

fun CNTXT_REABBREV_TAC abbrevs (gl as (asl,_)) =
 let val abbrevs' = filter is_abbrev asl
     val ordered_abbrevs = topsort compare_abbrev (abbrevs@abbrevs')
     val lrs = map (dest_eq o rand) ordered_abbrevs
 in UNABBREV_ALL_TAC THEN MAP_EVERY (uncurry ABB) lrs
 end gl;

(*---------------------------------------------------------------------------*)
(* Execute a tactic in a goal with no abbreviations, then restore the        *)
(* abbrevs, also taking account of any new abbreviations that came in from   *)
(* the application of the tactic.                                            *)
(*---------------------------------------------------------------------------*)

fun WITHOUT_ABBREVS tac (gl as (asl,_)) =
 let val abbrevs = filter is_abbrev asl
 in UNABBREV_ALL_TAC THEN tac THEN CNTXT_REABBREV_TAC abbrevs
 end gl;

(*---------------------------------------------------------------------------*)
(* REABBREV_TAC ought to be called after BasicProvers.LET_ELIM_TAC, which    *)
(* introduces an abbrev, but doesn't propagate the abbrev. to the other      *)
(* assumptions. This has been done in basicProof/BasicProvers.               *)
(*---------------------------------------------------------------------------*)

val REABBREV_TAC = WITHOUT_ABBREVS ALL_TAC;

(*---------------------------------------------------------------------------*)
(*  ABBRS_THEN: expand specified abbreviations before applying a tactic.     *)
(* Typically, the abbreviations are designated in the thm list of a          *)
(* simplification tactic thusly:                                             *)
(*                                                                           *)
(*     ASM_SIMP_TAC ss [ ..., Abbr`m`, ... ]                                 *)
(*                                                                           *)
(* which says to find and expand the abbreviation                            *)
(*                                                                           *)
(*      Abbrev (m = tm)                                                      *)
(*                                                                           *)
(* in the assumptions of the goal before proceeding with simplification.     *)
(*---------------------------------------------------------------------------*)

fun ABBRS_THEN thl_tac thl =
 let val (abbrs, rest) = List.partition is_abbr thl
 in
  MAP_EVERY (UNABBREV_TAC o dest_abbr) abbrs THEN thl_tac rest
 end

val MK_ABBREVS_OLDSTYLE =
    RULE_ASSUM_TAC (fn th => (th |> DeAbbrev |> SYM) handle HOL_ERR _ => th)

(* ----------------------------------------------------------------------
    Abbreviation Tidying

    Abbreviations should be of the form

       Abbrev(v = e)

    with v a variable. The tidying process eliminates assumptions that
    have Abbrev present at the top with an argument that is not of the
    right shape. As simplification sees abbreviation equations as
    rewrites of the form e = v (replacing occurrences of e with the
    abbreviation), the tidying process will flip equations to keep
    this "orientation".
   ---------------------------------------------------------------------- *)

fun TIDY_ABBREV_CONV t =
    if is_malformed_abbrev t then
      (REWR_CONV markerTheory.Abbrev_def THENC TRY_CONV (REWR_CONV EQ_SYM_EQ)) t
    else ALL_CONV t
val TIDY_ABBREV_RULE = CONV_RULE TIDY_ABBREV_CONV
val TIDY_ABBREVS = RULE_ASSUM_TAC TIDY_ABBREV_RULE


(*---------------------------------------------------------------------------*)
(* Support for user-defined labels.                                          *)
(*---------------------------------------------------------------------------*)

val DEST_LABEL_CONV = REWR_CONV label_def

val DEST_LABELS_CONV = PURE_REWRITE_CONV [label_def]

val DEST_LABEL = CONV_RULE DEST_LABEL_CONV
val DEST_LABELS = CONV_RULE DEST_LABELS_CONV

val DEST_LABELS_TAC = CONV_TAC DEST_LABELS_CONV THEN RULE_ASSUM_TAC DEST_LABELS


fun MK_LABEL(s, th) = EQ_MP (SYM (SPECL [mk_label_var s, concl th] label_def)) th

fun ASSUME_NAMED_TAC s bth : tactic = ASSUME_TAC (MK_LABEL(s, bth))

(*---------------------------------------------------------------------------*)
(* Given an LB encoded label reference, finds a corresponding term in the    *)
(*   assumption list.                                                        *)
(*---------------------------------------------------------------------------*)

fun find_labelled_assumption labelth asl = let
  val labname = dest_label_ref labelth
  fun matching_asm t =
      (#1 (dest_label t) = labname) handle HOL_ERR _ => false
in
  case List.find matching_asm asl of
    SOME t => DEST_LABEL (ASSUME t)
  | NONE => raise ERR "find_labelled_assumption"
                      ("No assumption with label \""^labname^"\"")
end;

fun LABEL_ASSUM s ttac (asl, w) =
   ttac (find_labelled_assumption (L s) asl) (asl, w)

(*---------------------------------------------------------------------------*)
(* LABEL_X_ASSUM is almost identical to LABEL_ASSUM. But it is not applied   *)
(* to the goal, but to a goal with the labelled assumption removed.          *)
(*---------------------------------------------------------------------------*)

fun name_assoc s [] = NONE
  | name_assoc s (tm::rst) =
     case total dest_label tm
      of NONE => name_assoc s rst
       | SOME (n,tm') => if s=n then SOME(tm,(n,tm'))
                          else name_assoc s rst;

fun LABEL_X_ASSUM s ttac : tactic =
 fn (asl,w) =>
   case name_assoc s asl
    of NONE => raise ERR "LABEL_X_ASSUM"
                ("Can't find term named by "^Lib.quote s^" in assumptions")
     | SOME(named_tm,_)
         => ttac (DEST_LABEL(ASSUME named_tm))
                 (op_set_diff aconv asl [named_tm],w);

(*---------------------------------------------------------------------------*)
(* Given a list of theorems thl and a list of assumptions asl, return a list *)
(* consisting of (a) the elements of thl that are not just tags signifying   *)
(* which elements of asl to assume; (b) the non-labelled elements of asl     *)
(* (just ASSUME'd); (c) the elements of asl having labels obtained by        *)
(* looking at the dummy theorems in thl of the form |- label = label. This   *)
(* means that some labelled elements of asl might be excluded.               *)
(*---------------------------------------------------------------------------*)

fun LLABEL_RESOLVE thl asl = let
  val (labelled_asms, other_asms) = List.partition is_label asl
  val (labelrefs, realths) = List.partition is_label_ref thl
  val wanted_lab_assums =
      map (fn lb => find_labelled_assumption lb labelled_asms) labelrefs
in
  map ASSUME other_asms @ wanted_lab_assums @ realths
end

fun matching_asm th t =
    let
      val labname = dest_label_ref th
    in
      #1 (dest_label t) = labname
    end handle HOL_ERR _ => false

fun has_label_from lrefs t =
    List.exists (C matching_asm t) lrefs

fun LLABEL_RES_THEN thltac thl (g as (asl,w)) =
    let
      val (labelrefs, realths) = List.partition is_label_ref thl
      val (wanted_labelled_asms, rest) =
           List.partition (has_label_from labelrefs) asl
    in
      thltac (map (DEST_LABEL o ASSUME) wanted_labelled_asms @ realths) g
    end


fun LABEL_RESOLVE th (asl, w) = hd (LLABEL_RESOLVE [th] asl)

(* ----------------------------------------------------------------------
    using : tactic * thm -> tactic

    using th tac stashes theorem th in the goal so that tactic tac can
    use it if desired. If the tactic terminates, the stashed theorem
    is removed.

    Stashing is done by adding an assumption encoding the name of the
    theorem to the assumption list. This will cause mess-ups if you
    attempt something like

       pop_assum foo using bar

    so, don't do that.

    This can be nested, with multiple theorems stashed at once; the
    cleanup looks for the exact using theorem that it stashed when it
    removes it and does so with UNDISCH_THEN. So, if there are
    multiples of the same name, the most recent will be taken.

   ---------------------------------------------------------------------- *)

fun tac using th =
    let
      val uth = MK_USING th
    in
      ASSUME_TAC uth >>
      tac >>
      UNDISCH_THEN (concl uth) (K ALL_TAC)
    end

fun usingA tac th = tac using th

fun loc2thm loc =
    case loc of
        DB.Local s => (valOf (DB.local_thm s)
                       handle Option => raise ERR "loc2thm" "No such theorem")
      | DB.Stored {Name,Thy} =>
        DB.fetch Thy Name
        handle HOL_ERR _ => raise ERR "loc2thm" "No such theorem"


fun maybe_using gen ttac (g as (asl,w)) =
    case asl of
        h::_ => if is_using h then ttac (DEST_USING (ASSUME h)) g
                else MAP_FIRST ttac (gen()) g
      | _ => MAP_FIRST ttac (gen()) g

end