Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

quiet load #1336

Merged
merged 2 commits into from
Nov 13, 2024
Merged

quiet load #1336

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2a64ec8
Fix otknl build due to slightly reordered goals in prove_base_assumsT…
binghe Nov 13, 2024
f855e83
quiet load
digama0 Nov 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 17 additions & 17 deletions src/boss/prove_base_assumsScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand All @@ -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 =
Expand Down
36 changes: 20 additions & 16 deletions tools-poly/poly/poly-init2.ML
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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 =
Expand Down