Skip to content

Commit

Permalink
(feat) Add String length operator
Browse files Browse the repository at this point in the history
Signed-off-by: Jerome Simeon <[email protected]>
  • Loading branch information
jeromesimeon committed May 23, 2019
1 parent 455644e commit 4fcc749
Show file tree
Hide file tree
Showing 20 changed files with 98 additions and 37 deletions.
14 changes: 14 additions & 0 deletions coq/Common/Data/DataLift.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 =>
Expand Down
2 changes: 1 addition & 1 deletion coq/Common/Operators/BinaryOperatorsSem.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down
3 changes: 3 additions & 0 deletions coq/Common/Operators/UnaryOperators.v
Original file line number Diff line number Diff line change
Expand Up @@ -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) *)
Expand Down Expand Up @@ -180,6 +181,7 @@ Section UnaryOperators.
++ ")"
| OpCount => "OpCount"
| OpToString => "OpToString"
| OpLength => "OpLength"
| OpSubstring start len =>
"(OpSubstring " ++ (toString start)
++ (match len with
Expand Down Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions coq/Common/Operators/UnaryOperatorsSem.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 =>
Expand Down
5 changes: 5 additions & 0 deletions coq/Common/OperatorsTyping/TOperatorsInfer.v
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 4 additions & 0 deletions coq/Common/OperatorsTyping/TOperatorsInferSub.v
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
7 changes: 7 additions & 0 deletions coq/Common/OperatorsTyping/TUnaryOperators.v
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions coq/Compiler/QLib/QOperators.v
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions coq/Translation/NNRCtoJava.v
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions coq/Translation/NNRCtoJavaScript.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 =>
Expand Down
5 changes: 5 additions & 0 deletions coq/Translation/NNRSimptoJavaScriptAst.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions coq/Translation/tDNNRCtoSparkDF.v
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions ocaml/src/AstsToSExp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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])
Expand Down Expand Up @@ -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)
Expand Down
70 changes: 36 additions & 34 deletions ocaml/src/OQLParser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -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

%}
Expand Down
1 change: 1 addition & 0 deletions ocaml/src/PrettyCommon.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
7 changes: 6 additions & 1 deletion runtimes/java/src/org/qcert/runtime/UnaryOperators.java
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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));
Expand Down
3 changes: 3 additions & 0 deletions runtimes/javascript/qcert-runtime-core.js
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
2 changes: 1 addition & 1 deletion test/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions test/oql/persons9.oql
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
/* OQL Length of "Hello World!" */
length("Hello World!")
1 change: 1 addition & 0 deletions test/oql/persons9.out
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"nat":12}

0 comments on commit 4fcc749

Please sign in to comment.