Merge commit '6c54683e2ad37ea4530953b33fc5aa1c8efd5e4d' into probabil…

…ity_dev

src/datatype/Datatype.sig

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

src/datatype/Datatype.sml

@@ -179,7 +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 => ())
+val typecheck_listener : (string Symtab.table * pretype * hol_type) Listener.t =
+    Listener.new_listener()
 
 local
   fun strvariant avoids s = if mem s avoids then strvariant avoids (s ^ "a")
@@ -223,7 +224,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
+       val _ = Listener.call_listener 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,6 +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
+val parse_listener : (AST list) Listener.t
 
 end

src/parse/ParseDatatype.sml

@@ -350,13 +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 => ())
+val parse_listener : AST list Listener.t = Listener.new_listener ()
 
 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
+  val _ = Listener.call_listener parse_listener result
 in
   case qbuf.current qb of
       (base_tokens.BT_EOI,_) => result

src/parse/Preterm.sig

@@ -70,7 +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 typecheck_listener : (preterm * Pretype.Env.t) Listener.t
   val last_tcerror : (tcheck_error * locn.locn) option ref
 
 end

src/parse/Preterm.sml

@@ -858,7 +858,8 @@ 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 => ());
+val typecheck_listener : (preterm * Pretype.Env.t) Listener.t =
+    Listener.new_listener()
 
 fun typecheck pfns ptm0 =
   let
@@ -869,7 +870,7 @@ fun typecheck pfns ptm0 =
           overloading_resolution ptm0 >-                     (fn (ptm,b) =>
           (report_ovl_ambiguity b >> to_term ptm) >-         (fn t =>
          fn e => (
-          !typecheck_listener ptm e;
+          ignore (Listener.call_listener typecheck_listener (ptm, e));
           errormonad.Some(e, !post_process_term t)))))
   end
 
@@ -881,7 +882,7 @@ fun typecheckS ptm =
     lift (!post_process_term o remove_case_magic)
          (fromErr TC' >> overloading_resolutionS ptm >-
           (fn ptm' => fromErr (errormonad.bind (to_term ptm', fn t => fn e => (
-            !typecheck_listener ptm' e;
+            ignore (Listener.call_listener typecheck_listener (ptm', e));
             errormonad.Some(e, t))))))
   end
 

src/portableML/Listener.sig

@@ -0,0 +1,13 @@
+signature Listener = sig
+
+  type 'a t
+  exception DUP of string
+  val add_listener : 'a t -> (string * ('a -> unit)) -> unit
+  val remove_listener : 'a t -> string -> ('a -> unit) option
+  val listeners : 'a t -> (string * ('a -> unit)) list
+  val new_listener : unit -> 'a t
+  val call_listener : 'a t -> 'a -> (string * ('a -> unit) * exn) list
+  val without_one : 'a t -> string -> ('b -> 'c) -> ('b -> 'c)
+  val without_all : 'a t -> ('b -> 'c) -> ('b -> 'c)
+
+end

src/portableML/Listener.sml

@@ -0,0 +1,52 @@
+structure Listener :> Listener =
+struct
+
+open Unsynchronized
+type 'a t = (string * ('a -> unit)) list ref
+exception DUP of string
+
+fun new_listener () : 'a t = ref []
+
+fun add_listener (r:'a t) (sf as (s,f)) =
+    let
+      val t = !r
+    in
+      case List.find (fn (s', _) => s' = s) t of
+        NONE => r := sf :: t
+      | SOME _ => raise DUP s
+    end
+
+fun remove_listener (r:'a t) s =
+    let
+      val t = !r
+      val (fopt, rest) =
+          Portable.trypluck' (fn (s',f) => if s' = s then SOME f else NONE) t
+    in
+      r := rest;
+      fopt
+    end
+
+fun listeners (t:'a t) = (!t)
+
+fun call_listener (t:'a t) v =
+    let
+      fun foldthis (kf as (k,f), A) =
+          case Exn.capture f v of
+              Exn.Res () => A
+            | Exn.Exn e => (k,f,e) :: A
+    in
+      List.foldr foldthis [] (!t)
+    end
+
+fun without_one (r:'a t) s f x =
+    let
+      val t = !r
+      val (_, t') =
+          Portable.trypluck' (fn (s',f) => if s' = s then SOME () else NONE) t
+    in
+      setmp r t' f x
+    end
+
+fun without_all r f x = setmp r [] f x
+
+end (* struct *)

src/postkernel/Theory.sig

@@ -60,11 +60,9 @@ sig
 
 (* Make hooks available so that theory changes can be seen by
    "interested parties" *)
+  val delta_hook : TheoryDelta.t Listener.t
   val register_hook : string * (TheoryDelta.t -> unit) -> unit
-  val delete_hook : string -> unit
-  val get_hooks : unit -> (string * (TheoryDelta.t -> unit)) list
-  val disable_hook : string -> ('a -> 'b) -> 'a -> 'b
-  val enable_hook : string -> ('a -> 'b) -> 'a -> 'b
+    (* alias for Listener.add_listener delta_hook *)
 
 (* -- and persistent data added to theories *)
   structure LoadableThyData : sig

src/postkernel/Theory.sml

@@ -68,91 +68,23 @@ type thy_addon = {sig_ps    : (unit -> PP.pretty) option,
                   struct_ps : (unit -> PP.pretty) option}
 open DB_dtype
 
-local
-  val hooks =
-    (* hooks are stored in the order they are registered, with later
-       hooks earlier in the list.
-       The set component is the list of the disabled hooks.
-     *)
-      ref (HOLset.empty String.compare,
-           [] : (string * (TheoryDelta.t -> unit)) list)
-in
-fun call_hooks td = let
-  val (disabled, hooks) = !hooks
-  val hooks_rev = List.rev hooks
-  fun protect nm (f:TheoryDelta.t -> unit) td = let
-    fun error_pfx() =
-        "Hook "^nm^" failed on event " ^ TheoryDelta.toString td
-  in
-    f td
-    handle e as HOL_ERR _ =>
-           Feedback.HOL_WARNING
-               "Theory"
-               "callhooks"
-               (error_pfx() ^ " with problem " ^
-                Feedback.exn_to_string e)
-         | Match =>
-           Feedback.HOL_WARNING
-               "Theory"
-               "callhooks"
-               (error_pfx() ^ " with a Match exception")
-  end
-  fun recurse l =
-      case l of
-        [] => ()
-      | (nm, f) :: rest => let
-        in
-          if HOLset.member(disabled,nm) then ()
-          else protect nm f td;
-          recurse rest
-        end
-in
-  recurse hooks_rev
-end
-
-fun register_hook (nm, f) = let
-  val (disabled, hooks0) = !hooks
-  val hooks0 = List.filter (fn (nm',f) => nm' <> nm) hooks0
-in
-  hooks := (disabled, (nm,f) :: hooks0)
-end
-
-fun delete_hook nm = let
-  val (disabled, hookfns) = !hooks
-  val (deleting, remaining) = Lib.partition (fn (nm', _) => nm' = nm) hookfns
-in
-  case deleting of
-    [] => HOL_WARNING "Theory" "delete_hook" ("No hook with name: "^nm)
-  | _ => ();
-  hooks := (HOLset.delete(disabled,nm), remaining)
-end
-
-fun get_hooks () = #2 (!hooks)
-
-fun hook_modify act f x =
-  let
-    val (disabled0, fns) = !hooks
-    fun finish() = hooks := (disabled0, fns)
-    val _ = hooks := (act disabled0, fns)
-    val result = f x handle e => (finish(); raise e)
-  in
-    finish();
-    result
-  end
+val delta_hook : TheoryDelta.t Listener.t = Listener.new_listener()
 
-fun disable_hook nm f x =
-  hook_modify (fn s => HOLset.add(s,nm)) f x
+fun register_hook sf = Listener.add_listener delta_hook sf
 
-fun safedel_fromset nm s =
-  HOLset.delete(s, nm) handle HOLset.NotFound => s
-fun enable_hook nm f x =
-  hook_modify (safedel_fromset nm) f x
-
-
-end (* local block enclosing declaration of hooks variable *)
+fun call_hooks td =
+    let
+      fun error_report (s,_,e) =
+          Feedback.HOL_WARNING
+            "Theory"
+            "callhooks"
+            ("Hook " ^ s ^ " failed on event " ^ TheoryDelta.toString td ^
+             " with problem " ^ Feedback.exn_to_string e)
+    in
+      List.app error_report (Listener.call_listener delta_hook td)
+    end
 
 (* This reference is set in course of loading the parsing library *)
-
 val pp_thm = ref (fn _:thm => PP.add_string "<thm>")
 
 (*---------------------------------------------------------------------------*

src/prekernel/Feedback.sml

@@ -92,10 +92,10 @@ fun quiet_messages f = Portable.with_flag (emit_MESG, false) f
 fun format_err_rec {message, origin_function, origin_structure, source_location} =
    String.concat
       ["at ", origin_structure, ".", origin_function, ":\n",
-        case source_location of
-          Loc_Unknown => ""
-        | _ => locn.toString source_location ^ ":\n",
-        message]
+       case source_location of
+           locn.Loc_Unknown => ""
+         | _ => locn.toString source_location ^ ":\n",
+       message]
 
 fun format_ERR err_rec =
    String.concat ["\nException raised ", format_err_rec err_rec, "\n"]

src/simp/src/Trace.sig

@@ -15,7 +15,7 @@ sig
            | IGNORE              of (string * thm)
            | MORE_CONTEXT        of thm
 
-   val trace_hook  : (int * action -> unit) ref;
+   val trace_hook  : (int * action) Listener.t
    val trace       : int * action -> unit
    val trace_level : int ref
    val tty_trace   : action -> unit

src/simp/src/Trace.sml

@@ -24,8 +24,8 @@ val say = Lib.say
            | IGNORE of (string * Thm.thm)
            | MORE_CONTEXT of Thm.thm;
 
-   val trace_hook : ((int * action) -> unit) ref = ref (fn (n,s) => ());
-   fun trace x = (!trace_hook) x
+   val trace_hook : (int * action) Listener.t = Listener.new_listener()
+   fun trace x = ignore (Listener.call_listener trace_hook x)
 
 val trace_level = ref 0;
 val _ = Feedback.register_trace("simplifier", trace_level, 7);
@@ -57,14 +57,15 @@ fun tty_trace (LZ_TEXT fs) = (say "  "; say (fs ()); say "\n")
 *)
 fun fudge t = Time.+(t, Time.fromSeconds 10)
 
-val _ = trace_hook :=
-        (fn (n,a) => if (n <= !trace_level) then
-                       (say "[";
-                        say ((Arbnum.toString o #usec o Portable.dest_time o
-                              fudge)
-                             (#usr (Timer.checkCPUTimer Globals.hol_clock)));
-                        say "]: ";
-                        tty_trace a)
-                     else ())
+val _ = Listener.add_listener trace_hook
+        ("default",
+         (fn (n,a) => if (n <= !trace_level) then
+                        (say "[";
+                         say ((Arbnum.toString o #usec o Portable.dest_time o
+                               fudge)
+                                (#usr (Timer.checkCPUTimer Globals.hol_clock)));
+                         say "]: ";
+                         tty_trace a)
+                      else ()))
 
 end (* struct *)

src/tfl/src/Defn.sml

@@ -1779,7 +1779,7 @@ fun defn_absyn_to_term a = let
       overloading_resolution ptm >- (fn (pt,b) =>
       report_ovl_ambiguity b     >>
       to_term pt                 >- (fn t => fn e => (
-      !Preterm.typecheck_listener pt e;
+      ignore (Listener.call_listener Preterm.typecheck_listener (pt, e));
       return (t |> remove_case_magic |> !post_process_term) e)))
     end
   val M =