Merge remote-tracking branch 'origin/develop' into probability_dev

binghe · Nov 13, 2024 · d270269 · d270269
2 parents 360e0b3 + f08ee00
commit d270269
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 33 deletions.
diff --git a/src/boss/prove_base_assumsScript.sml b/src/boss/prove_base_assumsScript.sml
@@ -893,15 +893,28 @@ val th59 = store_thm
   conj_tac >- MATCH_ACCEPT_TAC filter_nil
   \\ MATCH_ACCEPT_TAC filter_cons);
 
+val map_nil = hd(amatch``Data_List_map _ Data_List_nil``);
+val map_cons = hd(amatch``Data_List_map _ (Data_List_cons _ _)``);
+
+(* |- (!f. Data_List_map f Data_List_nil = Data_List_nil) /\
+      !f h t.
+          Data_List_map f (Data_List_cons h t) =
+          Data_List_cons (f h) (Data_List_map f t)
+ *)
+val th60 = store_thm
+  ("th60", el 60 goals |> concl,
+  conj_tac >- MATCH_ACCEPT_TAC map_nil
+  \\ MATCH_ACCEPT_TAC map_cons);
+
 val any_nil = hd(amatch``Data_List_any _ Data_List_nil``);
 val any_cons = hd(amatch``Data_List_any _ (Data_List_cons _ _)``);
 
 (* |- (!P. Data_List_any P Data_List_nil <=> F) /\
       !P h t.
           Data_List_any P (Data_List_cons h t) <=> P h \/ Data_List_any P t
  *)
-val th60 = store_thm
-  ("th60", el 60 goals |> concl,
+val th61 = store_thm
+  ("th61", el 61 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL any_nil))
   \\ MATCH_ACCEPT_TAC any_cons);
 
@@ -912,23 +925,10 @@ val all_cons = hd(amatch``Data_List_all _ (Data_List_cons _ _)``);
       !P h t.
           Data_List_all P (Data_List_cons h t) <=> P h /\ Data_List_all P t
  *)
-val th61 = store_thm
-  ("th61", el 61 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO (SPEC_ALL all_nil))
-  \\ MATCH_ACCEPT_TAC all_cons);
-
-val map_nil = hd(amatch``Data_List_map _ Data_List_nil``);
-val map_cons = hd(amatch``Data_List_map _ (Data_List_cons _ _)``);
-
-(* |- (!f. Data_List_map f Data_List_nil = Data_List_nil) /\
-      !f h t.
-          Data_List_map f (Data_List_cons h t) =
-          Data_List_cons (f h) (Data_List_map f t)
- *)
 val th62 = store_thm
   ("th62", el 62 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC map_nil
-  \\ MATCH_ACCEPT_TAC map_cons);
+  conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO (SPEC_ALL all_nil))
+  \\ MATCH_ACCEPT_TAC all_cons);
 
 val append_nil = hd(amatch``Data_List_append Data_List_nil``);
 val append_cons =

diff --git a/tools-poly/poly/poly-init2.ML b/tools-poly/poly/poly-init2.ML
@@ -22,12 +22,15 @@ val _ = use "poly/quse.sml";
 
 local
 
-  fun die s = (TextIO.output(TextIO.stdErr, s ^ "\n");
-               TextIO.flushOut TextIO.stdErr;
-               raise Fail s)
+  val quiet_load = ref false;
+  fun maybeWriteStderr s =
+    if !quiet_load then () else
+    (TextIO.output(TextIO.stdErr, s ^ "\n");
+     TextIO.flushOut TextIO.stdErr);
 
-  fun warn s = (TextIO.output(TextIO.stdErr, "WARNING: " ^ s ^ "\n");
-                TextIO.flushOut TextIO.stdErr)
+  fun die s = (maybeWriteStderr s; raise Fail s)
+
+  fun warn s = maybeWriteStderr ("WARNING: " ^ s)
 
   val meta_debug = ref false
 
@@ -53,12 +56,11 @@ fun quse s = let
 in
   QUse.use s ;
   loadpathdb := Binarymap.insert(!loadpathdb,OS.Path.file full,OS.Path.dir full)
-end handle OS.Path.Path => die ("Path exception in quse "^s)
-             | e => (TextIO.output(TextIO.stdErr,
-                                   "error in quse " ^ s ^ " : " ^
-                                   General.exnMessage e ^ "\n");
-                     TextIO.flushOut TextIO.stdErr;
-                     PolyML.Exception.reraise e)
+end handle
+    OS.Path.Path => die ("Path exception in quse "^s)
+  | e => (
+    maybeWriteStderr("error in quse " ^ s ^ " : " ^ General.exnMessage e);
+    PolyML.Exception.reraise e)
 
 fun myuse f =
   let val op ++ = OS.Path.concat
@@ -131,16 +133,18 @@ and load ps modPath =
        handle e =>
               (loadedMods := Binaryset.delete (!loadedMods, modName);
                PolyML.Exception.reraise e))
-  end handle e => (TextIO.output(TextIO.stdErr,
-                                 "error in load " ^ modPath ^ " : " ^
-                                 General.exnMessage e ^ "\n");
-                   TextIO.flushOut TextIO.stdErr;
-                   PolyML.Exception.reraise e)
+  end handle e => (
+    maybeWriteStderr("error in load " ^ modPath ^ " : " ^ General.exnMessage e);
+    PolyML.Exception.reraise e)
 in
 
   structure Meta = struct
     val meta_debug = meta_debug
+    val quiet_load = quiet_load
     val load = load []
+    fun qload s = let
+      val x = !quiet_load
+      in quiet_load := true; load s; quiet_load := x end
     val loadPath = loadPath;
     fun loaded () = Binaryset.listItems (!loadedMods);
     fun fakeload s =