typecheck listener

HOL-Theorem-Prover · Nov 17, 2024 · 714696d · 714696d
1 parent 833b239
commit 714696d
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 3 deletions.
diff --git a/src/parse/Preterm.sig b/src/parse/Preterm.sig
@@ -70,6 +70,7 @@ sig
     ((term -> string) * (hol_type -> string)) option -> preterm -> term errM
   val typecheckS : preterm -> term seqM
 
+  val typecheck_listener : (preterm -> Pretype.Env.t -> unit) ref
   val last_tcerror : (tcheck_error * locn.locn) option ref
 
 end
diff --git a/src/parse/Preterm.sml b/src/parse/Preterm.sml
@@ -858,6 +858,7 @@ fun remove_case_magic tm =
     else tm
 
 val post_process_term = ref (I : term -> term);
+val typecheck_listener = ref (fn _:preterm => fn _:Pretype.Env.t => ());
 
 fun typecheck pfns ptm0 =
   let
@@ -866,8 +867,10 @@ fun typecheck pfns ptm0 =
     lift remove_case_magic
          (TC pfns ptm0 >>
           overloading_resolution ptm0 >-                     (fn (ptm,b) =>
-          report_ovl_ambiguity b >> to_term ptm)) >-         (fn t =>
-         fn e => errormonad.Some(e, !post_process_term t))
+          (report_ovl_ambiguity b >> to_term ptm) >-         (fn t =>
+         fn e => (
+          !typecheck_listener ptm e;
+          errormonad.Some(e, !post_process_term t)))))
   end
 
 fun typecheckS ptm =
@@ -877,7 +880,9 @@ fun typecheckS ptm =
   in
     lift (!post_process_term o remove_case_magic)
          (fromErr TC' >> overloading_resolutionS ptm >-
-          (fn ptm' => fromErr (to_term ptm')))
+          (fn ptm' => fromErr (errormonad.bind (to_term ptm', fn t => fn e => (
+            !typecheck_listener ptm' e;
+            errormonad.Some(e, t))))))
   end