Rename toLeft and toRight into getLeft and getRight

querycert · Jul 27, 2021 · 36b3640 · 36b3640
1 parent fc8bc59
commit 36b3640
Show file tree

Hide file tree

Showing 7 changed files with 17 additions and 17 deletions.
diff --git a/compiler/core/EJson/Operators/EJsonRuntimeOperators.v b/compiler/core/EJson/Operators/EJsonRuntimeOperators.v
@@ -129,8 +129,8 @@ Section EJsonRuntimeOperators.
       | EJsonRuntimeArrayAccess => "arrayAccess"
       (* Sum *)
       | EJsonRuntimeEither => "either"
-      | EJsonRuntimeToLeft=> "toLeft"
-      | EJsonRuntimeToRight=> "toRight"
+      | EJsonRuntimeToLeft=> "getLeft"
+      | EJsonRuntimeToRight=> "getRight"
       (* Brand *)
       | EJsonRuntimeBrand => "brand"
       | EJsonRuntimeUnbrand => "unbrand"

diff --git a/compiler/core/Translation/Lang/NNRCtoJava.v b/compiler/core/Translation/Lang/NNRCtoJava.v
@@ -297,12 +297,12 @@ Section NNRCtoJava.
            (s1 +++ (indent i) +++ ^"final JsonElement " +++ res +++ ^";" +++ eol
                +++ (indent i) +++ ^"if (RuntimeUtils.either(" +++ (from_java_json e1) +++ ^")) {" +++ eol
                +++ (indent (i+1)) +++ ^"final JsonElement " +++ vl +++ eol
-               +++ (indent (i+1)) +++ ^" = RuntimeUtils.toLeft(" +++ (from_java_json e1) +++ ^");" +++ eol
+               +++ (indent (i+1)) +++ ^" = RuntimeUtils.getLeft(" +++ (from_java_json e1) +++ ^");" +++ eol
                +++ s2
                +++ (indent (i+1)) +++ res +++ ^" = " +++ (from_java_json e2) +++ ^";" +++ eol
                +++ (indent i) +++ ^"} else {" +++ eol
                +++ (indent (i+1)) +++ ^"final JsonElement " +++ vr  +++ eol
-               +++ (indent (i+1)) +++ ^" = RuntimeUtils.toRight(" +++ (from_java_json e1) +++ ^");" +++ eol
+               +++ (indent (i+1)) +++ ^" = RuntimeUtils.getRight(" +++ (from_java_json e1) +++ ^");" +++ eol
                +++ s3
                +++ (indent (i+1)) +++ res +++ ^" = " +++ (from_java_json e3) +++ ^";" +++ eol
                +++ (indent i) +++ ^"}" +++ eol,

diff --git a/compiler/core/Translation/Lang/NNRSimptoImpData.v b/compiler/core/Translation/Lang/NNRSimptoImpData.v
@@ -82,21 +82,21 @@ Section NNRSimptoImpData.
       (*   let e' := ImpExprVar x  in *)
       (*   ImpStmtIf *)
       (*     (ImpExprRuntimeCall DataRuntimeEither [e']) *)
-      (*     (ImpStmtBlock (* var x1 = toLeft(e); s1 *) *)
+      (*     (ImpStmtBlock (* var x1 = getLeft(e); s1 *) *)
       (*        [ (x1, Some (ImpExprRuntimeCall DataRuntimeToLeft [e'])) ] *)
       (*        [ nnrs_imp_stmt_to_imp_data s1 ]) *)
-      (*     (ImpStmtBlock (* var x2 = toRight(e); s2 *) *)
+      (*     (ImpStmtBlock (* var x2 = getRight(e); s2 *) *)
       (*        [ (x2, Some (ImpExprRuntimeCall DataRuntimeToRight [e'])) ] *)
       (*        [ nnrs_imp_stmt_to_imp_data s2 ]) *)
       | NNRSimpEither e x1 s1 x2 s2 =>
         (* XXX TODO: introduce a variable for e here or earlier in compilation? XXX *)
         let e' := nnrs_imp_expr_to_imp_data constants e in
         ImpStmtIf
           (ImpExprRuntimeCall DataRuntimeEither [e'])
-          (ImpStmtBlock (* var x1 = toLeft(e); s1 *)
+          (ImpStmtBlock (* var x1 = getLeft(e); s1 *)
              [ (x1, Some (ImpExprRuntimeCall DataRuntimeToLeft [e'])) ]
              [ nnrs_imp_stmt_to_imp_data constants s1 ])
-          (ImpStmtBlock (* var x2 = toRight(e); s2 *)
+          (ImpStmtBlock (* var x2 = getRight(e); s2 *)
              [ (x2, Some (ImpExprRuntimeCall DataRuntimeToRight [e'])) ]
              [ nnrs_imp_stmt_to_imp_data constants s2 ])
       end.

diff --git a/compiler/lib/pretty_query.ml b/compiler/lib/pretty_query.ml
@@ -493,9 +493,9 @@ let pretty_imp_data_runtime p sym pretty_imp_expr ff (op, args) =
   | Core.DataRuntimeEither, [e] ->
       fprintf ff "@[<hv 2>either@[<hv 2>(%a)@]@]" (pretty_imp_expr 0 sym) e
   | Core.DataRuntimeToLeft, [e] ->
-      fprintf ff "@[<hv 2>toLeft@[<hv 2>(%a)@]@]" (pretty_imp_expr 0 sym) e
+      fprintf ff "@[<hv 2>getLeft@[<hv 2>(%a)@]@]" (pretty_imp_expr 0 sym) e
   | Core.DataRuntimeToRight, [e] ->
-      fprintf ff "@[<hv 2>toRight@[<hv 2>(%a)@]@]" (pretty_imp_expr 0 sym) e
+      fprintf ff "@[<hv 2>getRight@[<hv 2>(%a)@]@]" (pretty_imp_expr 0 sym) e
   | _ -> assert false
   end
 

diff --git a/runtimes/java/src/org/qcert/runtime/BinaryOperators.java b/runtimes/java/src/org/qcert/runtime/BinaryOperators.java
@@ -224,7 +224,7 @@ public static JsonElement contains(JsonElement e1, JsonElement e2) {
 		final DataComparator comp = DataComparator.getComparator();
 		for(JsonElement elem : ec) {
 //			if (elem instanceof JsonObject) {
-//				elem = RuntimeUtils.toLeft(elem);
+//				elem = RuntimeUtils.getLeft(elem);
 //			}
 			if(comp.compare(elem, e1) == 0) {
 				return new JsonPrimitive(true);

diff --git a/runtimes/java/src/org/qcert/runtime/RuntimeUtils.java b/runtimes/java/src/org/qcert/runtime/RuntimeUtils.java
@@ -85,11 +85,11 @@ public static boolean either(JsonElement obj) {
         }
     }
 
-    public static JsonElement toLeft(JsonElement obj) {
+    public static JsonElement getLeft(JsonElement obj) {
         return asRec(obj).get("$left");
     }
 
-    public static JsonElement toRight(JsonElement obj) {
+    public static JsonElement getRight(JsonElement obj) {
         return asRec(obj).get("$right");
     }
 

diff --git a/runtimes/javascript/qcert-runtime-core.js b/runtimes/javascript/qcert-runtime-core.js
@@ -219,17 +219,17 @@ function either(v) {
     }
     throw new Error('TypeError: either called on non-sum');
 }
-function toLeft(v) {
+function getLeft(v) {
     if (typeof v === 'object' && isLeft(v)) {
         return unboxLeft(v);
     }
-    throw new Error('TypeError: toLeft called on non-sum');
+    throw new Error('TypeError: getLeft called on non-sum');
 }
-function toRight(v) {
+function getRight(v) {
     if (typeof v === 'object' && isRight(v)) {
         return unboxRight(v);
     }
-    throw new Error('TypeError: toRight called on non-sum');
+    throw new Error('TypeError: getRight called on non-sum');
 }
 
 /* Brand */