more typecheck listeners

src/datatype/Datatype.sig

@@ -34,6 +34,7 @@ sig
  (* into their tyinfo to do inequality resolution.                            *)
  (*---------------------------------------------------------------------------*)
 
+ val typecheck_listener : (string Symtab.table -> ParseDatatype.pretype -> hol_type -> unit) ref
  val build_tyinfos : typeBase
                          -> {induction:thm, recursion:thm}
                            -> tyinfo list

src/datatype/Datatype.sml

@@ -179,6 +179,8 @@ fun ast_tyvar_strings (dAQ ty) = map dest_vartype $ type_vars ty
   | ast_tyvar_strings (dTyop {Args, ...}) =
       List.concat (map ast_tyvar_strings Args)
 
+val typecheck_listener = ref (fn _: string Symtab.table => fn _: pretype => fn _:hol_type => ())
+
 local
   fun strvariant avoids s = if mem s avoids then strvariant avoids (s ^ "a")
                             else s
@@ -221,6 +223,7 @@ fun to_tyspecs ASTs =
                                        Args = map (mk_hol_ty d) Args}
      fun mk_hol_type d pty = let
        val ty = mk_hol_ty d pty
+       val _ = !typecheck_listener d pty ty
      in
        if Theory.uptodate_type ty then ty
        else let val tyname = #1 (dest_type ty)

src/parse/ParseDatatype.sig

@@ -41,4 +41,6 @@ val hparse : type_grammar.grammar -> Type.hol_type Portable.quotation ->
   or a type-constant of arity 0, or one of the types being defined.
 *)
 
+val parse_listener : (AST list -> unit) ref
+
 end

src/parse/ParseDatatype.sml

@@ -350,11 +350,13 @@ end
 fun hide_tynames q G0 =
   List.foldl (uncurry type_grammar.hide_tyop) G0 (extract_tynames q)
 
+val parse_listener = ref (fn _: (string * datatypeForm) list => ())
 
 fun core_parse G0 phrase_p q = let
   val G = hide_tynames q G0
   val qb = qbuf.new_buffer q
   val result = termsepby1 ";" base_tokens.BT_EOI (parse_g G phrase_p) qb
+  val _ = !parse_listener result
 in
   case qbuf.current qb of
       (base_tokens.BT_EOI,_) => result

src/parse/Pretype.sig

@@ -34,6 +34,7 @@ val fromType : Type.hol_type -> pretype
 val remove_made_links : pretype -> pretype in_env
 val replace_null_links :
     pretype -> (Env.t * string list, pretype, error) errormonad.t
+val typecheck_listener : (pretype -> Env.t -> unit) ref
 val clean : pretype -> Type.hol_type
 val toTypeM : pretype -> Type.hol_type in_env
 val toType : pretype -> Type.hol_type

src/parse/Pretype.sml

@@ -184,10 +184,15 @@ fun clean ty =
       Type.mk_thy_type{Tyop = s, Thy = Thy, Args = map clean Args}
   | _ => raise Fail "Don't expect to see links remaining at this stage"
 
+val typecheck_listener = ref (fn _:pretype => fn _:Env.t => ());
+
 fun toTypeM ty : Type.hol_type in_env =
   remove_made_links ty >-
   (fn ty => tyvars ty >-
-  (fn vs => lift (clean o #2) (addState vs (replace_null_links ty))))
+  (fn vs => lift #2 (addState vs (replace_null_links ty)) >-
+  (fn pty => fn e => (
+    !typecheck_listener pty e;
+    return (clean pty) e))))
 
 fun toType pty =
   case toTypeM pty Env.empty of

src/tfl/src/Defn.sml

@@ -1778,8 +1778,9 @@ fun defn_absyn_to_term a = let
     in
       overloading_resolution ptm >- (fn (pt,b) =>
       report_ovl_ambiguity b     >>
-      to_term pt                 >- (fn t =>
-      return (t |> remove_case_magic |> !post_process_term)))
+      to_term pt                 >- (fn t => fn e => (
+      !Preterm.typecheck_listener pt e;
+      return (t |> remove_case_magic |> !post_process_term) e)))
     end
   val M =
     ptsM >-