diff --git a/coq/Common/Data/DataLift.v b/coq/Common/Data/DataLift.v index a6cffe76f..fb1752485 100644 --- a/coq/Common/Data/DataLift.v +++ b/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 => diff --git a/coq/Common/Operators/BinaryOperatorsSem.v b/coq/Common/Operators/BinaryOperatorsSem.v index 2461607e5..4813800f9 100644 --- a/coq/Common/Operators/BinaryOperatorsSem.v +++ b/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 := diff --git a/coq/Common/Operators/UnaryOperators.v b/coq/Common/Operators/UnaryOperators.v index bfd82c277..1aebc19eb 100644 --- a/coq/Common/Operators/UnaryOperators.v +++ b/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 diff --git a/coq/Common/Operators/UnaryOperatorsSem.v b/coq/Common/Operators/UnaryOperatorsSem.v index 562f5113d..dce650755 100644 --- a/coq/Common/Operators/UnaryOperatorsSem.v +++ b/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 => diff --git a/coq/Common/OperatorsTyping/TOperatorsInfer.v b/coq/Common/OperatorsTyping/TOperatorsInfer.v index ef7e131b9..e2782796f 100644 --- a/coq/Common/OperatorsTyping/TOperatorsInfer.v +++ b/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 diff --git a/coq/Common/OperatorsTyping/TOperatorsInferSub.v b/coq/Common/OperatorsTyping/TOperatorsInferSub.v index d79ab7565..39d764b6c 100644 --- a/coq/Common/OperatorsTyping/TOperatorsInferSub.v +++ b/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) diff --git a/coq/Common/OperatorsTyping/TUnaryOperators.v b/coq/Common/OperatorsTyping/TUnaryOperators.v index 8e23ffbcf..01f4fe038 100644 --- a/coq/Common/OperatorsTyping/TUnaryOperators.v +++ b/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 diff --git a/coq/Compiler/QLib/QOperators.v b/coq/Compiler/QLib/QOperators.v index 003f1e24a..1615e063a 100644 --- a/coq/Compiler/QLib/QOperators.v +++ b/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 diff --git a/coq/Translation/NNRCtoJava.v b/coq/Translation/NNRCtoJava.v index 24a1756d9..e6a9103c9 100644 --- a/coq/Translation/NNRCtoJava.v +++ b/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 diff --git a/coq/Translation/NNRCtoJavaScript.v b/coq/Translation/NNRCtoJavaScript.v index de875d503..4dbee0ab5 100644 --- a/coq/Translation/NNRCtoJavaScript.v +++ b/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 => diff --git a/coq/Translation/NNRSimptoJavaScriptAst.v b/coq/Translation/NNRSimptoJavaScriptAst.v index 23353a179..9e4ee2d39 100644 --- a/coq/Translation/NNRSimptoJavaScriptAst.v +++ b/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 diff --git a/coq/Translation/tDNNRCtoSparkDF.v b/coq/Translation/tDNNRCtoSparkDF.v index 872f4e832..f17f7a4c9 100644 --- a/coq/Translation/tDNNRCtoSparkDF.v +++ b/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 diff --git a/ocaml/src/AstsToSExp.ml b/ocaml/src/AstsToSExp.ml index a18f5f863..5aa845158 100644 --- a/ocaml/src/AstsToSExp.ml +++ b/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) diff --git a/ocaml/src/OQLParser.mly b/ocaml/src/OQLParser.mly index 95059e6a5..bd7103b14 100644 --- a/ocaml/src/OQLParser.mly +++ b/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 %} diff --git a/ocaml/src/PrettyCommon.ml b/ocaml/src/PrettyCommon.ml index f58344a17..8e8fb3945 100644 --- a/ocaml/src/PrettyCommon.ml +++ b/ocaml/src/PrettyCommon.ml @@ -514,6 +514,7 @@ let pretty_unary_op p sym callb ff u a = | QcertCompiler.OpOrderBy atts -> fprintf ff "@[%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 diff --git a/runtimes/java/src/org/qcert/runtime/UnaryOperators.java b/runtimes/java/src/org/qcert/runtime/UnaryOperators.java index 5f18f8f28..4ce6ed32b 100644 --- a/runtimes/java/src/org/qcert/runtime/UnaryOperators.java +++ b/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)); diff --git a/runtimes/javascript/qcert-runtime-core.js b/runtimes/javascript/qcert-runtime-core.js index 8bf7be5a6..4d9201604 100644 --- a/runtimes/javascript/qcert-runtime-core.js +++ b/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; } diff --git a/test/Makefile b/test/Makefile index 828ccbd7e..202735eb2 100644 --- a/test/Makefile +++ b/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 diff --git a/test/oql/persons9.oql b/test/oql/persons9.oql new file mode 100644 index 000000000..4a88e39b6 --- /dev/null +++ b/test/oql/persons9.oql @@ -0,0 +1,2 @@ +/* OQL Length of "Hello World!" */ +length("Hello World!") diff --git a/test/oql/persons9.out b/test/oql/persons9.out new file mode 100644 index 000000000..5b735895e --- /dev/null +++ b/test/oql/persons9.out @@ -0,0 +1 @@ +{"nat":12} \ No newline at end of file