Add source level assert to basis

basis/AssertProgScript.sml

@@ -0,0 +1,22 @@
+(*
+  Module about CakeML assertions
+*)
+open preamble ml_translatorLib ml_progLib RuntimeProgTheory basisFunctionsLib;
+
+val _ = new_theory "AssertProg";
+
+val _ = translation_extends "RuntimeProg";
+
+val _ = ml_prog_update (open_module "Assert");
+
+val _ = process_topdecs `
+  fun assert cond msg =
+  if (cond)
+  then ()
+  else (Runtime.debugMsg (String.^ ("Assertion Failure:") (msg));
+        Runtime.abort());`
+  |> append_prog;
+
+val _ = ml_prog_update (close_module NONE);
+
+val _ = export_theory();

basis/OptionProgScript.sml

@@ -1,12 +1,12 @@
 (*
   Module about the option tyoe.
 *)
-open preamble ml_translatorLib ml_progLib RuntimeProgTheory
+open preamble ml_translatorLib ml_progLib AssertProgTheory
      mloptionTheory
 
 val _ = new_theory"OptionProg"
 
-val _ = translation_extends "RuntimeProg"
+val _ = translation_extends "AssertProg"
 
 val _ = ml_prog_update (open_module "Option");
 

basis/README.md

@@ -7,6 +7,9 @@ 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.