remove _ from sexp op names

CakeML · Feb 19, 2024 · 078b5da · 078b5da
1 parent edf8414
commit 078b5da
Showing 1 changed file with 10 additions and 10 deletions.
diff --git a/compiler/parsing/fromSexpScript.sml b/compiler/parsing/fromSexpScript.sml
@@ -696,8 +696,8 @@ val sexpop_def = Define`
   if s = "Aw8sub" then SOME Aw8sub else
   if s = "Aw8length" then SOME Aw8length else
   if s = "Aw8update" then SOME Aw8update else
-  if s = "Aw8sub_unsafe" then SOME Aw8sub_unsafe else
-  if s = "Aw8update_unsafe" then SOME Aw8update_unsafe else
+  if s = "Aw8subunsafe" then SOME Aw8sub_unsafe else
+  if s = "Aw8updateunsafe" then SOME Aw8update_unsafe else
   if s = "CopyStrStr" then SOME CopyStrStr else
   if s = "CopyStrAw8" then SOME CopyStrAw8 else
   if s = "CopyAw8Str" then SOME CopyAw8Str else
@@ -727,11 +727,11 @@ val sexpop_def = Define`
   if s = "Asub" then SOME Asub else
   if s = "Alength" then SOME Alength else
   if s = "Aupdate" then SOME Aupdate else
-  if s = "Asub_unsafe" then SOME Asub_unsafe else
-  if s = "Aupdate_unsafe" then SOME Aupdate_unsafe else
+  if s = "Asubunsafe" then SOME Asub_unsafe else
+  if s = "Aupdateunsafe" then SOME Aupdate_unsafe else
   if s = "ConfigGC" then SOME ConfigGC else
   if s = "Eval" then SOME Eval else
-  if s = "Env_id" then SOME Env_id else NONE) ∧
+  if s = "Envid" then SOME Env_id else NONE) ∧
   (sexpop (SX_CONS (SX_SYM s) (SX_STR s')) =
      if s = "FFI" then OPTION_MAP FFI (decode_control s') else NONE
    ) ∧
@@ -1343,8 +1343,8 @@ val opsexp_def = Define`
   (opsexp Aw8sub = SX_SYM "Aw8sub") ∧
   (opsexp Aw8length = SX_SYM "Aw8length") ∧
   (opsexp Aw8update = SX_SYM "Aw8update") ∧
-  (opsexp Aw8sub_unsafe = SX_SYM "Aw8sub_unsafe") ∧
-  (opsexp Aw8update_unsafe = SX_SYM "Aw8update_unsafe") ∧
+  (opsexp Aw8sub_unsafe = SX_SYM "Aw8subunsafe") ∧
+  (opsexp Aw8update_unsafe = SX_SYM "Aw8updateunsafe") ∧
   (opsexp CopyStrStr = SX_SYM "CopyStrStr") ∧
   (opsexp CopyStrAw8 = SX_SYM "CopyStrAw8") ∧
   (opsexp CopyAw8Str = SX_SYM "CopyAw8Str") ∧
@@ -1374,11 +1374,11 @@ val opsexp_def = Define`
   (opsexp Asub = SX_SYM "Asub") ∧
   (opsexp Alength = SX_SYM "Alength") ∧
   (opsexp Aupdate = SX_SYM "Aupdate") ∧
-  (opsexp Asub_unsafe = SX_SYM "Asub_unsafe") ∧
-  (opsexp Aupdate_unsafe = SX_SYM "Aupdate_unsafe") ∧
+  (opsexp Asub_unsafe = SX_SYM "Asubunsafe") ∧
+  (opsexp Aupdate_unsafe = SX_SYM "Aupdateunsafe") ∧
   (opsexp ConfigGC = SX_SYM "ConfigGC") ∧
   (opsexp Eval = SX_SYM "Eval") ∧
-  (opsexp Env_id = SX_SYM "Env_id") ∧
+  (opsexp Env_id = SX_SYM "Envid") ∧
   (opsexp (FFI s) = SX_CONS (SX_SYM "FFI") (SEXSTR s))`;
 
 Theorem sexpop_opsexp[simp]: