text \<open>Command to print names of a theorem statement\<close>
theory Names_Of_Thm
  imports Main
  keywords "print_names_of_thm" :: diag
       and "print_dup_thms" :: diag
begin

ML \<open>

  signature NAMES_OF_THM = sig
    (* dynamic \<rightarrow> _ \<rightarrow> _: get all facts from context. *)
    val all_facts_of : bool -> Proof.context -> (Facts.ref * thm) list
    (* Find nicest name in list. Returns empty or singleton list. *)
    val nicest_name_of: Proof.context -> Facts.ref list -> Facts.ref list
  
    (* Beta-Eta normalize term, and standardize variable names *)
    val norm_term: term -> term
    
    type configT = {dynamic: bool, rdups: bool}
    
    (* Obtain names for given theorem *)
    val names_of: configT -> Proof.context -> term -> Facts.ref list
    val names_of_thm: configT -> Proof.context -> thm -> Facts.ref list
    

    (* Pretty print theorem name *)    
    val pretty_ref: Proof.context -> Facts.ref -> Pretty.T
    val pretty_refs: Proof.context -> Facts.ref list -> Pretty.T
    

    val analyze_dup_names: Proof.context -> string -> (term * Facts.ref list) list
    
    val pretty_dup_name: Proof.context -> (term * Facts.ref list) -> Pretty.T
    val pretty_dup_names: Proof.context -> (term * Facts.ref list) list -> Pretty.T

    
  end

  structure Names_Of_Thm : NAMES_OF_THM = struct

    fun all_facts_of dynamic ctxt =
      let
        val dest = if dynamic then Facts.dest_all (Context.Proof ctxt) false else Facts.dest_static false
        val thy = Proof_Context.theory_of ctxt;
        val transfer = Global_Theory.transfer_theories thy;
        val local_facts = Proof_Context.facts_of ctxt
        val global_facts = Global_Theory.facts_of thy;
      in
       (dest [global_facts] local_facts @
         dest [] global_facts)
       |> maps Facts.selections
       |> map (apsnd transfer)
      end;

    local
    
      val index_ord = option_ord (K EQUAL);
      val hidden_ord = bool_ord o apply2 Long_Name.is_hidden;
      val qual_ord = int_ord o apply2 Long_Name.qualification;
      val txt_ord = int_ord o apply2 size;
      
      fun nicer_name ((a, x), i) ((b, y), j) =
        (case bool_ord (a, b) of EQUAL =>
          (case hidden_ord (x, y) of EQUAL =>
            (case index_ord (i, j) of EQUAL =>
              (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
            | ord => ord)
          | ord => ord)
        | ord => ord) <> GREATER;
    
    in
    
      fun nicer_shortest ctxt =
        let
          fun extern_shortest name =
            let
              val facts = Proof_Context.facts_of_fact ctxt name;
              val space = Facts.space_of facts;
            in (Facts.is_dynamic facts name, Name_Space.extern_shortest ctxt space name) end;
      
          fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
                nicer_name (extern_shortest x, i) (extern_shortest y, j)
            | nicer (Facts.Fact _) (Facts.Named _) = true
            | nicer (Facts.Named _) (Facts.Fact _) = false
            | nicer (Facts.Fact _) (Facts.Fact _) = true;
        in nicer end;
    
      fun nicest_name_of _ [] = []
        | nicest_name_of ctxt (x::xs) = let
            fun rem x [] = x
              | rem x (y::ys) = rem (if nicer_shortest ctxt x y then x else y) ys
          in
            [rem x xs]
          end  
      
    end;

    
    fun norm_term t = let
      val t = Envir.beta_eta_contract t
    
      val tfs = Term.add_tvars t []
      val tfs = tfs ~~ (1 upto length tfs)
        |> map (fn ((n,s),i) => (TVar (n,s), TVar (("T"^Int.toString i,0),s)))
        |> Typtab.make
      fun mapT T = the_default T (Typtab.lookup tfs T)
      
      val fs = Term.add_vars t []
      val fs = fs ~~ (1 upto length fs)
        |> map (fn ((n,T),i) => (Var (n,T), Var ( ("x"^Int.toString i,0) ,T )))
        |> Termtab.make
      
      fun mapV V = the_default V (Termtab.lookup fs V)  
        
      val t = t
        |> map_aterms mapV
        |> map_types (map_atyps mapT)
    
    in t end
    
    type configT = { dynamic : bool, rdups : bool }
    
    fun names_of { dynamic, rdups } ctxt : term -> Facts.ref list = let
      val tab = all_facts_of dynamic ctxt 
       |> map (swap #>> Thm.prop_of #>> norm_term)
       |> Termtab.make_list
    in
         norm_term  
      #> Termtab.lookup_list tab
      #> rdups? nicest_name_of ctxt
    end

    fun names_of_thm cfg ctxt = names_of cfg ctxt o Thm.prop_of 
        
    fun pretty_ref ctxt thmref =
      let
        val (name, sel) =
          (case thmref of
            Facts.Named ((name, _), sel) => (name, sel)
          | Facts.Fact _ => raise Fail "Illegal literal fact");
      in
        Pretty.block [Pretty.marks_str (#1 (Proof_Context.markup_extern_fact ctxt name), name),
          Pretty.str (Facts.string_of_selection sel)]
      end;
    
    fun pretty_refs ctxt refs = 
      map (pretty_ref ctxt) refs |> Pretty.fbreaks |> Pretty.block  
      
    fun analyze_dup_names ctxt pat = let
    
      val match = match_string pat o Facts.name_of_ref
    
      fun sort xs = filter match xs @ filter_out match xs
      
      val res = all_facts_of false ctxt 
        |> map (swap #>> Thm.prop_of #>> norm_term)
        |> Termtab.make_list
        |> Termtab.dest
        |> filter (fn (_,xs) => length xs > 1)
        |> filter (exists match o snd)
        |> map (apsnd sort)
        
    
    in res end     

    fun pretty_dup_name ctxt (t,names) =
      Pretty.block [ Pretty.cartouche (Syntax.pretty_term ctxt t), Pretty.str ":", Pretty.brk 1, map (pretty_ref ctxt) names |> Pretty.breaks |> Pretty.block ]
          
    fun pretty_dup_names ctxt dups =
      Pretty.fbreaks (map (pretty_dup_name ctxt) dups) |> Pretty.block 
      
      
    val _ =
      Outer_Syntax.command \<^command_keyword>\<open>print_names_of_thm\<close>
        "print theorem names under which given statement is available"
        (Args.mode "dynamic" -- Parse.prop >> (fn (dynamic,t) =>
          Toplevel.keep (fn st => let
            val ctxt = Toplevel.context_of st
            val t = Syntax.read_prop ctxt t
            val t = singleton (Variable.export_terms (Variable.auto_fixes t ctxt) ctxt) t
            
            val names = names_of {dynamic=dynamic, rdups=false} ctxt t
            
            
            val pretty_t = Pretty.cartouche (Syntax.pretty_term ctxt t)
            
            val res = case names of
              [] => Pretty.block [Pretty.str "No named theorem for statement ",pretty_t]
            | _ =>  Pretty.block [Pretty.str "Names of",Pretty.brk 1,pretty_t,Pretty.str ":", Pretty.fbrk, pretty_refs ctxt names] 
            
          in 
            Pretty.string_of res |> writeln
          end)));
      
      
    val _ =
      Outer_Syntax.command \<^command_keyword>\<open>print_dup_thms\<close>
        "print duplicate theorems"
        (Scan.option Parse.name >> (fn pat =>
          Toplevel.keep (fn st => let
            val ctxt = Toplevel.context_of st

            val pat = the_default (Context.theory_name (Proof_Context.theory_of ctxt) ^ ".*") pat
            
            val dups = analyze_dup_names ctxt pat
                    
            val pretty_pat = Pretty.cartouche (Pretty.str pat)
                
            val res = case dups of
              [] => Pretty.block [Pretty.str "No duplicate theorems matching",Pretty.brk 1,pretty_pat]
            | _ =>  Pretty.block [Pretty.str "Duplicate theorems matching ",Pretty.brk 1,pretty_pat,Pretty.str ":", Pretty.fbrk, pretty_dup_names ctxt dups] 
            
          in 
            Pretty.string_of res |> writeln
          end)));
      
  end
\<close>

end