# HG changeset patch
# User wenzelm
# Date 1737296022 -3600
# Node ID 402660d4558e51d97cc6eaf1a1be00812ce7efba
# Parent  27854cbcadf14d28c072b8b62ed0c254a1009877
support tracing (with proper guard);
clarified signature: more explicit type name;

diff -r 27854cbcadf1 -r 402660d4558e src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Sun Jan 19 14:33:14 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Sun Jan 19 15:13:42 2025 +0100
@@ -9,6 +9,8 @@
 
 signature IMPORT_RULE =
 sig
+  val trace : bool Config.T
+  type name = {hol: string, isabelle: string}
   val beta : cterm -> thm
   val eq_mp : thm -> thm -> thm
   val comb : thm -> thm -> thm
@@ -19,10 +21,9 @@
   val refl : cterm -> thm
   val abs : cterm -> thm -> thm
   val mdef : theory -> string -> thm
-  val def : string -> cterm -> theory -> thm * theory
+  val def : name -> cterm -> theory -> thm * theory
   val mtydef : theory -> string -> thm
-  val tydef :
-    string -> string -> string -> cterm -> cterm -> thm -> theory -> thm * theory
+  val tydef : name -> string -> string -> cterm -> cterm -> thm -> theory -> thm * theory
   val inst_type : (ctyp * ctyp) list -> thm -> thm
   val inst : (cterm * cterm) list -> thm -> thm
   val import_file : Path.T -> theory -> theory
@@ -31,6 +32,24 @@
 structure Import_Rule: IMPORT_RULE =
 struct
 
+(* tracing *)
+
+val trace = Attrib.setup_config_bool \<^binding>\<open>import_trace\<close> (K false)
+
+type name = {hol: string, isabelle: string}
+
+fun print_name {hol, isabelle} =
+  if hol = isabelle then quote hol
+  else quote hol ^ " = " ^ quote isabelle
+
+fun print_item kind name =
+  Markup.markup Markup.keyword1 kind ^ " " ^ print_name name
+
+fun tracing_item thy kind name =
+  if Config.get_global thy trace then tracing (print_item kind name) else ()
+
+
+
 (** primitive rules of HOL Light **)
 
 (* basic logic *)
@@ -195,8 +214,9 @@
 
 (* constant definitions *)
 
-fun def' c rhs thy =
+fun def' (name as {isabelle = c, ...}) rhs thy =
   let
+    val _ = tracing_item thy "const" name;
     val b = Binding.name c
     val ty = type_of rhs
     val thy1 = Sign.add_consts [(b, ty, NoSyn)] thy
@@ -212,10 +232,10 @@
     SOME th => th
   | NONE => error ("Constant mapped, but no definition: " ^ quote name))
 
-fun def c rhs thy =
+fun def (name as {isabelle = c, ...}) rhs thy =
   if is_some (Import_Data.get_const_def thy c) then
     (warning ("Const mapped, but def provided: " ^ quote c); (mdef thy c, thy))
-  else def' c (Thm.term_of rhs) thy
+  else def' name (Thm.term_of rhs) thy
 
 
 (* type definitions *)
@@ -237,8 +257,10 @@
     typedef_hol2hollight A B rep abs P (Thm.free ("a", A)) (Thm.free ("r", B))
   end
 
-fun tydef' tycname abs_name rep_name cP ct td_th thy =
+fun tydef' (name as {isabelle = tycname, ...}) abs_name rep_name cP ct td_th thy =
   let
+    val _ = tracing_item thy "type" name;
+
     val ctT = Thm.ctyp_of_cterm ct
     val nonempty =
       Thm.instantiate' [SOME ctT] [SOME cP, SOME ct]
@@ -274,10 +296,10 @@
     SOME th => meta_mp (typedef_hollight th) th
   | NONE => error ("Type mapped, but no tydef thm registered: " ^ quote name))
 
-fun tydef tycname abs_name rep_name P t td_th thy =
+fun tydef (name as {hol = tycname, ...}) abs_name rep_name P t td_th thy =
   if is_some (Import_Data.get_typ_def thy tycname) then
     (warning ("Type mapped but proofs provided: " ^ quote tycname); (mtydef thy tycname, thy))
-  else tydef' tycname abs_name rep_name P t td_th thy
+  else tydef' name abs_name rep_name P t td_th thy
 
 
 
@@ -285,9 +307,10 @@
 
 (* basic entities *)
 
-val make_name = String.translate (fn #"." => "dot" | c => Char.toString c)
+fun make_name hol =
+  {hol = hol, isabelle = String.translate (fn #"." => "dot" | c => Char.toString c) hol}
 
-fun make_free x ty = Thm.free (make_name x, ty);
+fun make_free x ty = Thm.free (#isabelle (make_name x), ty);
 
 fun make_tfree thy a =
   let val b = "'" ^ String.translate (fn #"?" => "t" | c => Char.toString c) a
@@ -298,7 +321,7 @@
     val d =
       (case Import_Data.get_typ_map thy c of
         SOME d => d
-      | NONE => Sign.full_bname thy (make_name c))
+      | NONE => Sign.full_bname thy (#isabelle (make_name c)))
     val T = Thm.global_ctyp_of thy (Type (d, replicate (length args) dummyT))
   in Thm.make_ctyp T args end
 
@@ -307,7 +330,7 @@
     val d =
       (case Import_Data.get_const_map thy c of
         SOME d => d
-      | NONE => Sign.full_bname thy (make_name c))
+      | NONE => Sign.full_bname thy (#isabelle (make_name c)))
   in Thm.global_cterm_of thy (Const (d, Thm.typ_of ty)) end
 
 val make_thm = Skip_Proof.make_thm_cterm o Thm.apply \<^cterm>\<open>Trueprop\<close>
@@ -353,6 +376,8 @@
 
 fun store_thm name (State (thy, a, b, c as (tab, reg))) =
   let
+    val _ = tracing_item thy "thm" name;
+
     val th =
       (case Inttab.lookup tab reg of
         NONE => raise Fail "store_thm: lookup failed"
@@ -366,7 +391,7 @@
         (TVars.list_set tvars) names)
 
     val th' = Thm.instantiate (tyinst, Vars.empty) th
-    val thy' = #2 (Global_Theory.add_thm ((Binding.name (make_name name), th'), []) thy)
+    val thy' = #2 (Global_Theory.add_thm ((Binding.name (#isabelle name), th'), []) thy)
   in State (thy', a, b, c) end
 
 fun pair_list (x :: y :: zs) = ((x, y) :: pair_list zs)
@@ -404,7 +429,7 @@
   | command (#"F", [name]) = theory #-> (fn thy => set_thm (mdef thy name))
   | command (#"Y", [name, abs, rep, t1, t2, th]) =
       thm th #-> (fn th => term t1 #-> (fn t1 => term t2 #-> (fn t2 =>
-        theory_op (tydef name abs rep t1 t2 th) #-> set_thm)))
+        theory_op (tydef (make_name name) abs rep t1 t2 th) #-> set_thm)))
   | command (#"Y", [name, _, _]) = theory #-> (fn thy => set_thm (mtydef thy name))
   | command (#"t", [a]) = theory #-> (fn thy => set_typ (make_tfree thy a))
   | command (#"a", c :: tys) = theory #-> (fn thy => typs tys #>> make_type thy c #-> set_typ)
@@ -412,7 +437,7 @@
   | command (#"c", [c, ty]) = theory #-> (fn thy => typ ty #>> make_const thy c #-> set_term)
   | command (#"f", [t, u]) = term t #-> (fn t => term u #-> (fn u => set_term (Thm.apply t u)))
   | command (#"l", [x, t]) = term x #-> (fn x => term t #-> (fn t => set_term (Thm.lambda x t)))
-  | command (#"+", [name]) = store_thm name
+  | command (#"+", [name]) = store_thm (make_name name)
   | command (c, _) = raise Fail ("process: unknown command: " ^ String.str c)
 
 in