(feat) Add String length operator

coq/Common/Data/DataLift.v

@@ -54,6 +54,20 @@ Section DataLift.
   Definition unbdata (f:data -> data -> bool) (d1 d2:data) : option data :=
     Some (dbool (f d1 d2)).
 
+  Definition unndstring (f:string -> Z) (d1:data) : option data :=
+    match d1 with
+    | dstring s1 => (Some (dnat (f s1)))
+    | _ => None
+    end.
+
+  Lemma unndstring_is_nat f d1 d2:
+    unndstring f d1 = Some d2 -> exists z:Z, d2 = dnat z.
+  Proof.
+    intros.
+    destruct d1; simpl in *; try congruence.
+    exists (f s); inversion H; reflexivity.
+  Qed.
+
   Definition unsdstring (f:string -> string -> string) (d1 d2:data) : option data :=
     match d1 with
     | dstring s1 =>

coq/Common/Operators/BinaryOperatorsSem.v

@@ -28,7 +28,7 @@ Require Import ForeignOperators.
 Require Import OperatorsUtils.
 Require Import Iterators.
 Require Export BinaryOperators.
-  
+
 Section BinaryOperatorsSem.
   (* Algebra Unary/Binary Ops *)
   Definition nat_arith_binary_op_eval (op:nat_arith_binary_op) (z1 z2:Z) : Z :=

coq/Common/Operators/UnaryOperators.v

@@ -61,6 +61,7 @@ Section UnaryOperators.
   | OpOrderBy : SortCriterias -> unary_op             (**r sorts a collection of records *)
   | OpCount : unary_op                                (**r bag count *)
   | OpToString : unary_op                             (**r convert any data to a string *)
+  | OpLength : unary_op                               (**r the length of a string *)
   | OpSubstring : Z -> option Z -> unary_op           (**r returns the substring starting with the nth character, for m characters (or the rest of the string) *)
   | OpLike (pattern:string)
               (escape:option ascii) : unary_op        (**r like expression (as in sql) *)
@@ -180,6 +181,7 @@ Section UnaryOperators.
                 ++ ")"
             | OpCount => "OpCount"
             | OpToString => "OpToString"
+            | OpLength => "OpLength"
             | OpSubstring start len =>
               "(OpSubstring " ++ (toString start)
                                  ++ (match len with
@@ -232,6 +234,7 @@ Tactic Notation "unary_op_cases" tactic(first) ident(c) :=
   | Case_aux c "OpOrderBy"%string
   | Case_aux c "OpCount"%string
   | Case_aux c "OpToString"%string
+  | Case_aux c "OpLength"%string
   | Case_aux c "OpSubstring"%string
   | Case_aux c "OpLike"%string
   | Case_aux c "OpLeft"%string

coq/Common/Operators/UnaryOperatorsSem.v

@@ -94,6 +94,8 @@ Section UnaryOperatorsSem.
       lift dnat (ondcoll (fun z => Z_of_nat (bcount z)) d)
     | OpToString =>
       Some (dstring (dataToString d))
+    | OpLength =>
+      unndstring (fun s => Z_of_nat (String.length s)) d
     | OpSubstring start olen =>
       match d with
       | dstring s =>

coq/Common/OperatorsTyping/TOperatorsInfer.v

@@ -297,6 +297,11 @@ Section TOperatorsInfer.
         | _ => None
         end
       | OpToString => Some String
+      | OpLength =>
+        match `τ₁ with
+        | String₀ => Some Nat
+        | _ => None
+        end
       | OpSubstring _ _ =>
         match `τ₁ with
         | String₀ => Some String

coq/Common/OperatorsTyping/TOperatorsInferSub.v

@@ -196,6 +196,10 @@ Section TOperatorsInferSub.
         lift (fun τ => (Nat, τ₁')) (tuncoll τ₁')
       | OpToString =>
         Some (String, τ₁)
+      | OpLength =>
+        if (subtype_dec τ₁ String)
+        then Some (Nat, String)
+        else None
       | OpSubstring _ _ =>
         if (subtype_dec τ₁ String)
         then Some (String, String)

coq/Common/OperatorsTyping/TUnaryOperators.v

@@ -75,6 +75,8 @@ Section TUnaryOperators.
         unary_op_type OpCount (Coll τ) Nat
     | type_OpToString τ:
         unary_op_type OpToString τ String
+    | type_OpLength:
+        unary_op_type OpLength String Nat
     | type_OpSubstring start olen:
         unary_op_type (OpSubstring start olen) String String
     | type_OpLike pat oescape:
@@ -134,6 +136,7 @@ Section TUnaryOperators.
     | Case_aux c "type_OpOrderBy"%string
     | Case_aux c "type_OpCount"%string
     | Case_aux c "type_OpToString"%string
+    | Case_aux c "type_OpLength"%string
     | Case_aux c "type_OpSubstring"%string
     | Case_aux c "type_OpLike"%string
     | Case_aux c "type_OpLeft"%string
@@ -386,6 +389,9 @@ Section TUnaryOperators.
       split; [reflexivity|apply dtnat].
     - Case "type_OpToString"%string.
       eauto.
+    - Case "type_OpLength"%string.
+      dtype_inverter.
+      eauto.
     - Case "type_OpSubstring"%string.
       dtype_inverter.
       eauto.
@@ -587,6 +593,7 @@ Tactic Notation "unary_op_type_cases" tactic(first) ident(c) :=
   | Case_aux c "type_OpOrderBy"%string
   | Case_aux c "type_OpCount"%string
   | Case_aux c "type_OpToString"%string
+  | Case_aux c "type_OpLength"%string
   | Case_aux c "type_OpSubstring"%string
   | Case_aux c "type_OpLike"%string
   | Case_aux c "type_OpLeft"%string

coq/Compiler/QLib/QOperators.v

@@ -81,6 +81,8 @@ Module QOperators(runtime:CompilerRuntime).
       := UnaryOperators.OpCount.
     Definition optostring : op 
       := UnaryOperators.OpToString.
+    Definition oplength : op 
+      := UnaryOperators.OpLength.
     Definition opsubstring : Z -> option Z -> op 
       := UnaryOperators.OpSubstring.
     Definition oplike : String.string -> option Ascii.ascii -> op 

coq/Translation/NNRCtoJava.v

@@ -330,6 +330,7 @@ Section NNRCtoJava.
                      | OpOrderBy sl => mk_java_unary_op1 "sort" (mk_java_string_collection (List.map fst sl)) e1 (* XXX TO FIX XXX *)
                      | OpCount => mk_java_unary_op0 "count" e1
                      | OpToString =>  mk_java_unary_op0 "tostring" e1
+                     | OpLength =>  mk_java_unary_op0 "stringlength" e1
                      | OpSubstring start olen =>
                        match olen with
                        | Some len => mk_java_unary_opn "substring" (map toString [start; len]) e1

coq/Translation/NNRCtoJavaScript.v

@@ -276,6 +276,7 @@ Section NNRCtoJavaScript.
                      | OpOrderBy scl => "sort(" ++ e1 ++ ", " ++ (sortCriteriaToJs quotel scl) ++ ")"
                      | OpCount => "count(" ++ e1 ++ ")"
                      | OpToString => "toString(" ++ e1 ++ ")"
+                     | OpLength => "stringLength(" ++ e1 ++ ")"
                      | OpSubstring start olen =>
                        match olen with
                        | None =>

coq/Translation/NNRSimptoJavaScriptAst.v

@@ -48,6 +48,9 @@ Section NNRSimptoJavaScriptAst.
   Definition toString e :=
     expr_call (expr_identifier "toString") [ e ].
 
+  Definition stringLength e :=
+    expr_call (expr_identifier "stringLength") [ e ].
+
   Definition substring e start len_opt :=
     let start := expr_literal (literal_number (start)) in
     let args :=
@@ -382,6 +385,8 @@ Section NNRSimptoJavaScriptAst.
       runtime_nat_mean e'
     | OpToString =>
       toString e'
+    | OpLength =>
+      stringLength e'
     | OpSubstring start olen =>
       let start_num := float_of_int start in
       match olen with

coq/Translation/tDNNRCtoSparkDF.v

@@ -211,6 +211,7 @@ Section tDNNRCtoSparkDF.
     | OpDistinct => postfix "distinct"
     | OpCount => postfix "length"
     | OpToString => prefix "toQcertString"
+    | OpLength => "(" ++ x ++ ").length()"
     | OpSubstring start olen =>
       "(" ++ x ++ ").substring(" ++ toString start ++
           match olen with

ocaml/src/AstsToSExp.ml

@@ -251,6 +251,7 @@ let unary_op_to_sexp (u:unary_op) : sexp =
   | OpDistinct -> STerm ("OpDistinct",[])
   | OpOrderBy sl -> STerm ("OpOrderBy", coq_string_list_to_sstring_list_with_order sl)
   | OpToString -> STerm ("OpToString",[])
+  | OpLength -> STerm ("OpLength",[])
   | OpSubstring (n,None) -> STerm ("OpSubstring",[SInt n])
   | OpSubstring (n1,(Some n2)) -> STerm ("OpSubstring",[SInt n1;SInt n2])
   | OpLike (p,None) -> STerm ("OpLike",[coq_string_to_sstring p])
@@ -298,6 +299,7 @@ let sexp_to_unary_op (se:sexp) : unary_op =
   | STerm ("OpDistinct",[]) -> OpDistinct
   | STerm ("OpOrderBy",sl) -> OpOrderBy (sstring_list_with_order_to_coq_string_list sl)
   | STerm ("OpToString",[]) -> OpToString
+  | STerm ("OpLength",[]) -> OpLength
   | STerm ("OpSubstring",[SInt n1]) -> OpSubstring (n1,None)
   | STerm ("OpSubstring",[SInt n1;SInt n2]) -> OpSubstring (n1,Some n2)
   | STerm ("OpLike",[p]) -> OpLike (sstring_to_coq_string p,None)

ocaml/src/OQLParser.mly

@@ -27,51 +27,53 @@
   let resolve_call fname el =
     begin match fname,el with
     | "not", [e] ->
-	QOQL.ounop QOps.Unary.opneg e
+	      QOQL.ounop QOps.Unary.opneg e
     | "flatten", [e] ->
-	QOQL.ounop QOps.Unary.opflatten e
+	      QOQL.ounop QOps.Unary.opflatten e
     | "sum", [e] ->
-	QOQL.ounop QOps.Unary.opnatsum e
+	      QOQL.ounop QOps.Unary.opnatsum e
     | "fsum", [e] ->
-	QOQL.ounop QOps.Unary.opfloatsum e
+	      QOQL.ounop QOps.Unary.opfloatsum e
     | "avg", [e] ->
-	QOQL.ounop QOps.Unary.opnatmean e
+	      QOQL.ounop QOps.Unary.opnatmean e
     | "favg", [e] ->
-	QOQL.ounop QOps.Unary.opfloatmean e
+	      QOQL.ounop QOps.Unary.opfloatmean e
     | "count", [e] ->
-	QOQL.ounop QOps.Unary.opcount e
+	      QOQL.ounop QOps.Unary.opcount e
+    | "length", [e] ->
+	      QOQL.ounop QOps.Unary.oplength e
     | "max", [e] ->
-	QOQL.ounop QOps.Unary.opnatmax e
+	      QOQL.ounop QOps.Unary.opnatmax e
     | "min", [e] ->
-	QOQL.ounop QOps.Unary.opnatmin e
+	      QOQL.ounop QOps.Unary.opnatmin e
     | "substring", [e1;e2] ->
-	let start =
-	  begin try static_int e2 with
-	  | Not_found ->
-	      raise (Qcert_Error
-		       ("Second parameter of substring should be an integer constant"))
-	  end
-	in
-	QOQL.ounop (QOps.Unary.opsubstring start None) e1
+	      let start =
+	        begin try static_int e2 with
+	        | Not_found ->
+	            raise (Qcert_Error
+		                   ("Second parameter of substring should be an integer constant"))
+	        end
+	      in
+	      QOQL.ounop (QOps.Unary.opsubstring start None) e1
     | "substring", [e1;e2;e3] ->
-	let start =
-	  begin try static_int e2 with
-	  | Not_found ->
-	      raise (Qcert_Error
-		       ("Second parameter of substring should be an integer constant"))
-	  end
-	in
-	let len =
-	  begin try static_int e3 with
-	  | Not_found ->
-	      raise (Qcert_Error
-		       ("Third parameter of substring should be an integer constant"))
-	  end
-	in
-	QOQL.ounop (QOps.Unary.opsubstring start (Some len)) e1
+	      let start =
+	        begin try static_int e2 with
+	        | Not_found ->
+	            raise (Qcert_Error
+		                   ("Second parameter of substring should be an integer constant"))
+	        end
+	      in
+	      let len =
+	        begin try static_int e3 with
+	        | Not_found ->
+	            raise (Qcert_Error
+		                   ("Third parameter of substring should be an integer constant"))
+	        end
+	      in
+	      QOQL.ounop (QOps.Unary.opsubstring start (Some len)) e1
     | _, _ ->
-	raise (Qcert_Error
-		 ("Function " ^ fname ^ " with arity " ^ (string_of_int (List.length el)) ^ " unkonwn"))
+	      raise (Qcert_Error
+		             ("Function " ^ fname ^ " with arity " ^ (string_of_int (List.length el)) ^ " unkonwn"))
     end
 
 %}

ocaml/src/PrettyCommon.ml

@@ -514,6 +514,7 @@ let pretty_unary_op p sym callb ff u a =
   | QcertCompiler.OpOrderBy atts ->
       fprintf ff "@[<hv 0>%s%a(%a)@]" "sort" (pretty_squared_names sym) (List.map fst atts) (callb 0 sym) a
   | QcertCompiler.OpToString -> pretty_unary_exp sym callb "toString" ff a
+  | QcertCompiler.OpLength -> pretty_unary_exp sym callb "length" ff a
   | QcertCompiler.OpSubstring (n1,None) -> pretty_unary_exp sym callb ("substring["^(string_of_int n1)^"]") ff a
   | QcertCompiler.OpSubstring (n1,Some n2) -> pretty_unary_exp sym callb ("substring["^(string_of_int n1)^","^(string_of_int n2)^"]") ff a
   | QcertCompiler.OpLike (n1,None) -> pretty_unary_exp sym callb ("like["^(Util.string_of_char_list n1)^"]") ff a

runtimes/java/src/org/qcert/runtime/UnaryOperators.java

@@ -65,7 +65,7 @@ public static JsonElement coll(JsonElement e) {
 		return dst;
 	}
 	public static JsonElement count(JsonElement e) {
-	        return rec("nat",new JsonPrimitive(e.getAsJsonArray().size()));
+    return rec("nat",new JsonPrimitive(e.getAsJsonArray().size()));
 	}
 
 	public static JsonElement flatten(JsonElement e) {
@@ -209,6 +209,11 @@ public static JsonPrimitive tostring(JsonElement e) {
 		return new JsonPrimitive(sb.toString());
 	}
 
+	public static JsonElement stringlength(JsonElement e) {
+		String str = e.getAsJsonPrimitive().getAsString();
+		return rec("nat",new JsonPrimitive(str.length()));
+	}
+
 	public static JsonElement substring(int start, int end, JsonElement e) {
 		String str = e.getAsJsonPrimitive().getAsString();
 		return new JsonPrimitive(str.substring(start, end));

runtimes/javascript/qcert-runtime-core.js

@@ -500,6 +500,9 @@ function natArithMean(b) {
 function count(v) {
     return { "nat" : v.length };
 }
+function stringLength(v) {
+    return { "nat" : v.length };
+}
 function floatOfNat(v) {
     return v.nat;
 }

test/Makefile

@@ -65,7 +65,7 @@ endif
 	clean
 
 ## OQL
-OQLPERSONSNUM=1 2 3 4 5 6 7 8
+OQLPERSONSNUM=1 2 3 4 5 6 7 8 9
 OQLWORLDNUM=1 2
 OQLEMPLOYEESNUM=1 2
 OQLTARGETS=oql nraenv nnrc nnrs nnrs_imp nnrcmr cldmr nra nraenv_core nnrc_core dnnrc # dnnrc_typed

test/oql/persons9.oql

@@ -0,0 +1,2 @@
+/* OQL Length of "Hello World!" */
+length("Hello World!")

test/oql/persons9.out

@@ -0,0 +1 @@
+{"nat":12}