Merge pull request #1234 from CakeML/more_sml_compatibility

tanyongkiam · web-flow · commit b35d23274750 · 2025-09-13T16:09:02.000+08:00
More sml compatibility
diff --git a/basis/mlbasicsProgScript.sml b/basis/mlbasicsProgScript.sml
@@ -93,12 +93,22 @@ Proof
 QED
 
 Definition bool_toString_def:
-  bool_toString b = if b then strlit "True" else strlit"False"
+  bool_toString b = if b then strlit "True" else strlit "False"
+End
+
+Definition bool_fromString_def:
+  bool_fromString s = if s = strlit "True" then SOME T else
+                      if s = strlit "False" then SOME F else
+                      NONE
 End
 
 val _ = ml_prog_update (open_module "Bool");
+val _ = (next_ml_names := ["not"]);
+val _ = trans "not" ``\x. ~x:bool``;
 val _ = (next_ml_names := ["toString"]);
 val _ = translate bool_toString_def;
+val _ = (next_ml_names := ["fromString"]);
+val _ = translate bool_fromString_def;
 val _ = (next_ml_names := ["compare"]);
 val _ = translate comparisonTheory.bool_cmp_def;
 val _ = ml_prog_update (close_module NONE);
diff --git a/basis/types.txt b/basis/types.txt
@@ -116,7 +116,9 @@ String.collate: (char -> char -> ordering) -> string -> string -> ordering
 String.char_escape_seq: char -> string option
 String.escape_str: string -> string
 String.escape_char: char -> string
+Bool.not: bool -> bool
 Bool.toString: bool -> string
+Bool.fromString: string -> bool option
 Bool.compare: bool -> bool -> ordering
 Pair.map: ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd
 Pair.toString: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
