Refactor assert into RuntimeProg

CakeML · Mar 3, 2020 · fcce77b · fcce77b
1 parent 89ada40
commit fcce77b
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 27 deletions.
diff --git a/basis/AssertProgScript.sml b/basis/AssertProgScript.sml
diff --git a/basis/OptionProgScript.sml b/basis/OptionProgScript.sml
@@ -1,12 +1,12 @@
 (*
   Module about the option tyoe.
 *)
-open preamble ml_translatorLib ml_progLib AssertProgTheory
+open preamble ml_translatorLib ml_progLib RuntimeProgTheory
      mloptionTheory
 
 val _ = new_theory"OptionProg"
 
-val _ = translation_extends "AssertProg"
+val _ = translation_extends "RuntimeProg"
 
 val _ = ml_prog_update (open_module "Option");
 

diff --git a/basis/README.md b/basis/README.md
@@ -7,9 +7,6 @@ A module about Arrays for the CakeML standard basis library.
 [ArrayProofScript.sml](ArrayProofScript.sml):
 Proofs about the Array module.
 
-[AssertProgScript.sml](AssertProgScript.sml):
-Module about CakeML assertions
-
 [CharProgScript.sml](CharProgScript.sml):
 A module about the char type for the CakeML standard basis library.
 

diff --git a/basis/RuntimeProgScript.sml b/basis/RuntimeProgScript.sml
@@ -43,6 +43,14 @@ val abort = process_topdecs `fun abort u = case u of () => exit 1`
 
 val _ = append_prog abort
 
+val _ = process_topdecs `
+  fun assert cond msg =
+  if (cond)
+  then ()
+  else (debugMsg (String.^ ("Assertion Failure: ") (msg));
+        abort());`
+  |> append_prog;
+
 val _ = ml_prog_update (close_module NONE);
 
 val _ = export_theory();