Qcert.Backend.NNRCtoJava
Section sanitizer.
Definition javaAllowedIdentifierInitialCharacters := ["A";"B";"C";"D";"E";"F";"G";"H";"I";"J";"K";"L";"M";"N";"O";"P";"Q";"R";"S";"T";"U";"V";"W";"X";"Y";"Z";"a";"b";"c";"d";"e";"f";"g";"h";"i";"j";"k";"l";"m";"n";"o";"p";"q";"r";"s";"t";"u";"v";"w";"x";"y";"z"]%char.
Definition javaAllowedIdentifierCharacters := ["A";"B";"C";"D";"E";"F";"G";"H";"I";"J";"K";"L";"M";"N";"O";"P";"Q";"R";"S";"T";"U";"V";"W";"X";"Y";"Z";"a";"b";"c";"d";"e";"f";"g";"h";"i";"j";"k";"l";"m";"n";"o";"p";"q";"r";"s";"t";"u";"v";"w";"x";"y";"z";"0";"1";"2";"3";"4";"5";"6";"7";"8";"9";"_";"$"]%char.
Definition javaIdentifierInitialCharacterToAdd := "X"%char.
Definition javaIdenitiferCharacterForReplacement := "X"%char.
Definition javaIdentifierFixInitial (ident:string) : string
:= match ident with
| EmptyString ⇒
String javaIdentifierInitialCharacterToAdd EmptyString
| String a _ ⇒
if in_dec ascii_dec a javaAllowedIdentifierInitialCharacters
then ident
else String javaIdentifierInitialCharacterToAdd ident
end.
Definition javaIdentifierSanitizeChar (a:ascii)
:= if in_dec ascii_dec a javaAllowedIdentifierCharacters
then a
else javaIdenitiferCharacterForReplacement.
Definition javaIdentifierSanitizeBody (ident:string)
:= map_string javaIdentifierSanitizeChar ident.
Definition javaIdentifierSanitize (ident:string)
:= javaIdentifierFixInitial (javaIdentifierSanitizeBody ident).
Definition javaSafeSeparator := "_".
Definition javaAvoidList :=
["abstract"; "assert"; "boolean"; "break"; "byte"; "case"; "catch"; "char"; "class"; "const"; "continue"; "default"; "do"; "double"; "else"; "enum"; "extends"; "false"; "final"; "finally"; "float"; "for"; "goto"; "if"; "implements"; "import"; "instanceof"; "int"; "interface"; "long"; "native"; "new"; "null"; "package"; "private"; "protected"; "public"; "return"; "short"; "static"; "strictfp"; "super"; "switch"; "synchronized"; "this"; "throw"; "throws"; "transient"; "true"; "try"; "void"; "volatile"; "while"].
Definition unshadow_java {fruntime:foreign_runtime} (avoid:list var) (e:nnrc) : nnrc
:= unshadow javaSafeSeparator javaIdentifierSanitize (avoid++javaAvoidList) e.
Definition javaSanitizeNNRC {fruntime:foreign_runtime} (e:nnrc) : nnrc
:= unshadow_java nil e.
End sanitizer.
Section NNRCtoJava.
Context {fruntime:foreign_runtime}.
Section javaUtil.
Definition eol_newline := String (Ascii.ascii_of_nat 10) EmptyString.
Definition eol_backn := "\n".
Definition quotel_double := """".
Definition quotel_backdouble := "\""".
Fixpoint indent (i : nat) : string
:= match i with
| 0 ⇒ ""
| S j ⇒ " " ++ (indent j)
end.
End javaUtil.
Section DataJava.
Definition mk_java_json_array (l:list java_json) : java_json
:= mk_java_json ("RuntimeUtils.createJsonArray"
++ bracketString "("
(joinStrings ", " (map from_java_json l))
")").
Definition mk_java_json_object (quotel:string) (l:list (string×java_json)) : java_json
:= mk_java_json ("new RuntimeUtils.JsonObjectBuilder()"
++ (joinStrings "" (map (fun elem ⇒
bracketString
".add("
(quotel ++ (fst elem) ++ quotel ++ ", " ++
(from_java_json (snd elem)))
")") l))
++ ".toJsonObject()").
Definition mk_java_json_brands (quotel:string) (b:brands) : java_json
:= mk_java_json_array (map (mk_java_json_string quotel) b).
Context {ftojavajson:foreign_to_java}.
Fixpoint mk_java_json_data (quotel:string) (d : data) : java_json
:= match d with
| dunit ⇒ java_json_NULL
| dnat n ⇒ mk_java_json_nat n
| dbool b ⇒ mk_java_json_bool b
| dstring s ⇒ mk_java_json_string quotel s
| dcoll ls ⇒ mk_java_json_array (map (mk_java_json_data quotel) ls)
| drec ls ⇒ mk_java_json_object quotel
(map (fun kv ⇒
let '(k,v) := kv in
(k, (mk_java_json_data quotel v))) ls)
| dleft d ⇒ mk_java_json_object quotel
[("left", (mk_java_json_data quotel d))]
| dright d ⇒ mk_java_json_object quotel
[("right", (mk_java_json_data quotel d))]
| dbrand b d ⇒
mk_java_json_object quotel
[("data", mk_java_json_data quotel d)
; ("type", mk_java_json_brands quotel b)]
| dforeign fd ⇒ foreign_to_java_data quotel fd
end.
End DataJava.
Section test.
Definition testd
:= drec (rec_sort [
("hi", dcoll [dnat 3; dnat 4])
; ("there", dbool false)
; ("is", dstring "hi")
; ("b", dbrand ["C1"; "I1"; "C2"]
(dcoll [dbool true; dbool false]))]).
Context {ftojavajson:foreign_to_java}.
End test.
Section NNRCJava.
Context {ftojavajson:foreign_to_java}.
Definition mk_java_string (s:string) : string
:= quotel_double ++ s ++ quotel_double.
Definition mk_java_unary_op0 (opname:string) (e:java_json) : java_json
:= mk_java_json ("UnaryOperators." ++ opname ++ "(" ++ (from_java_json e) ++ ")").
Definition mk_java_unary_op1 (opname:string) (s:string) (e:java_json) : java_json
:= mk_java_json
("UnaryOperators."
++ opname
++ "("
++ s ++ ", "
++ (from_java_json e) ++ ")").
Definition mk_java_unary_opn (opname:string) (sn:list string) (e:java_json) : java_json
:= mk_java_json
("UnaryOperators."
++ opname
++ "("
++ (joinStrings ", " (List.app sn [(from_java_json e)]))
++ ")").
Definition mk_java_collection(typ:string) (s:list string) : string
:= "new RuntimeUtils.CollectionBuilder<" ++ typ ++ ">("
++ (nat_to_string10 (Datatypes.length s)) ++ ")"
++ joinStrings "" (map (fun elem ⇒ ".add(" ++ elem ++ ")") s)
++ ".result()".
Definition mk_java_string_collection(s:list string) : string
:= mk_java_collection "String" (map mk_java_string s).
Definition mk_java_binary_op0 (opname:string) (e1 e2:java_json) : java_json
:= mk_java_json ("BinaryOperators." ++ opname ++ "(" ++ (from_java_json e1) ++ ", " ++ (from_java_json e2) ++ ")").
Definition uarithToJavaMethod (u:ArithUOp) :=
match u with
| ArithAbs ⇒ "abs"
| ArithLog2 ⇒ "log2"
| ArithSqrt ⇒"sqrt"
end.
Definition barithToJavaMethod (b:ArithBOp) :=
match b with
| ArithPlus ⇒ "plus"
| ArithMinus ⇒ "minus "
| ArithMult ⇒ "mult"
| ArithDivide ⇒ "divide"
| ArithRem ⇒ "rem"
| ArithMin ⇒ "min"
| ArithMax ⇒ "max"
end.
Definition like_clause_to_java (lc:like_clause)
:= match lc with
| like_literal literal ⇒ "new UnaryOperator.LiteralLikeClause(" ++ (mk_java_string literal) ++ ")"
| like_any_char ⇒ "new UnaryOperator.AnyCharLikeClause()"
| like_any_string ⇒ "new UnaryOperator.AnyStringLikeClause()"
end.
Fixpoint nnrcToJava
(n : nnrc)
(t : nat)
(i : nat)
(eol : string)
(quotel : string)
(ivs : list (string × string))
: string
× java_json
× nat
:= match n with
| NNRCVar v ⇒
match assoc_lookupr equiv_dec ivs v with
| Some v_string ⇒ ("", mk_java_json v_string, t)
| None ⇒ ("", mk_java_json ("v" ++ v), t)
end
| NNRCConst d ⇒ ("", (mk_java_json_data quotel d), t)
| NNRCUnop op n1 ⇒
let '(s1, e1, t0) := nnrcToJava n1 t i eol quotel ivs in
let e0 := match op with
| AIdOp ⇒ e1
| AUArith u ⇒ mk_java_unary_op0 (uarithToJavaMethod u) e1
| ANeg ⇒ mk_java_unary_op0 "neg" e1
| AColl ⇒ mk_java_unary_op0 "coll" e1
| ACount ⇒ mk_java_unary_op0 "count" e1
| AFlatten ⇒ mk_java_unary_op0 "flatten" e1
| ARec s ⇒ mk_java_unary_op1 "rec" (mk_java_string s) e1
| ADot s ⇒ mk_java_unary_op1 "dot" (mk_java_string s) e1
| ARecRemove s ⇒ mk_java_unary_op1 "remove" (mk_java_string s) e1
| ARecProject sl ⇒ mk_java_unary_op1 "project" (mk_java_string_collection sl) e1
| ADistinct ⇒ mk_java_unary_op0 "distinct" e1
| AOrderBy sl ⇒ mk_java_unary_op1 "sort" (mk_java_string_collection (List.map fst sl)) e1
| ASum ⇒ mk_java_unary_op0 "sum" e1
| AArithMean ⇒ mk_java_unary_op0 "list_mean" e1
| AToString ⇒ mk_java_unary_op0 "tostring" e1
| ASubstring start olen ⇒
match olen with
| Some len ⇒ mk_java_unary_opn "substring" (map toString [start; len]) e1
| None ⇒ mk_java_unary_op1 "substring" (toString start) e1
end
| ALike pat oescape ⇒
let lc := make_like_clause pat oescape in
mk_java_unary_op1 "string_like" ("new LikeClause[]{" ++ (joinStrings "," (map like_clause_to_java lc)) ++ "}") e1
| ALeft ⇒ mk_java_unary_op0 "left" e1
| ARight ⇒ mk_java_unary_op0 "right" e1
| ABrand b ⇒mk_java_unary_op1 "brand" (mk_java_string_collection b) e1
| AUnbrand ⇒ mk_java_unary_op0 "unbrand" e1
| ACast b ⇒ mk_java_unary_opn "cast" ["hierarchy"; (mk_java_string_collection b)] e1
| ASingleton ⇒ mk_java_unary_op0 "singleton" e1
| ANumMin ⇒ mk_java_unary_op0 "list_min" e1
| ANumMax ⇒ mk_java_unary_op0 "list_max" e1
| AForeignUnaryOp fu
⇒ foreign_to_java_unary_op i eol quotel fu e1
end in
(s1, e0, t0)
| NNRCBinop op n1 n2 ⇒
let '(s1, e1, t2) := nnrcToJava n1 t i eol quotel ivs in
let '(s2, e2, t0) := nnrcToJava n2 t2 i eol quotel ivs in
let e0 := match op with
| ABArith b ⇒ mk_java_binary_op0 (barithToJavaMethod b) e1 e2
| AEq ⇒ mk_java_binary_op0 "equals" e1 e2
| AUnion ⇒ mk_java_binary_op0 "union" e1 e2
| AConcat ⇒ mk_java_binary_op0 "concat" e1 e2
| AMergeConcat ⇒ mk_java_binary_op0 "mergeConcat" e1 e2
| AAnd ⇒ mk_java_binary_op0 "and" e1 e2
| AOr ⇒ mk_java_binary_op0 "or" e1 e2
| ALt ⇒ mk_java_binary_op0 "lt" e1 e2
| ALe ⇒ mk_java_binary_op0 "le" e1 e2
| AMinus ⇒ mk_java_binary_op0 "bag_minus" e1 e2
| AMin ⇒ mk_java_binary_op0 "bag_min" e1 e2
| AMax ⇒ mk_java_binary_op0 "bag_max" e1 e2
| AContains ⇒ mk_java_binary_op0 "contains" e1 e2
| ASConcat ⇒ mk_java_binary_op0 "stringConcat" e1 e2
| AForeignBinaryOp fb
⇒ foreign_to_java_binary_op i eol quotel fb e1 e2
end in
(s1 ++ s2, e0, t0)
| NNRCLet v bind body ⇒
let '(s1, e1, t2) := nnrcToJava bind t i eol quotel ivs in
let '(s2, e2, t0) := nnrcToJava body t2 i eol quotel ivs in
let v0 := "v" ++ v in
let ret := "vletvar$" ++ v ++ "$" ++ (nat_to_string10 t0) in
(s1
++ (indent i) ++ "final JsonElement " ++ ret ++ ";" ++ eol
++ (indent i) ++ "{ // new scope introduced for a let statement" ++ eol
++ (indent (i+1)) ++ "final JsonElement " ++ v0 ++ " = " ++ (from_java_json e1) ++ ";" ++ eol
++ s2
++ (indent (i+1)) ++ ret ++ " = " ++ (from_java_json e2) ++ ";" ++ eol
++ (indent i) ++ "}" ++ eol,
mk_java_json ret, t0+1)
| NNRCFor v iter body ⇒
let '(s1, e1, t2) := nnrcToJava iter t i eol quotel ivs in
let '(s2, e2, t0) := nnrcToJava body t2 (i+1) eol quotel ivs in
let elm := "v" ++ v in
let src := "src" ++ (nat_to_string10 t0) in
let idx := "i" ++ (nat_to_string10 t0) in
let dst := "dst" ++ (nat_to_string10 t0) in
(s1 ++ (indent i) ++ "final JsonArray " ++ src ++ " = (JsonArray) " ++ (from_java_json e1) ++ ";" ++ eol
++ (indent i) ++ "final JsonArray " ++ dst ++ " = new JsonArray();" ++ eol
++ (indent i) ++ "for(int " ++ idx ++ " = 0; " ++ idx ++ " < " ++ src ++ ".size(); " ++ idx ++ "++) {" ++ eol
++ (indent (i+1)) ++ "final JsonElement " ++ elm ++ " = " ++ src ++ ".get(" ++ idx ++ ");" ++ eol
++ s2
++ (indent (i+1)) ++ dst ++ ".add(" ++ (from_java_json e2) ++ ");" ++ eol
++ (indent i) ++ "}" ++ eol,
(mk_java_json dst), t0 + 1)
| NNRCIf c n1 n2 ⇒
let '(s1, e1, t2) := nnrcToJava c t i eol quotel ivs in
let '(s2, e2, t3) := nnrcToJava n1 t2 (i+1) eol quotel ivs in
let '(s3, e3, t0) := nnrcToJava n2 t3 (i+1) eol quotel ivs in
let v0 := "t" ++ (nat_to_string10 t0) in
(s1 ++ (indent i) ++ "final JsonElement " ++ v0 ++ ";" ++ eol
++ (indent i) ++ "if (RuntimeUtils.asBoolean(" ++ (from_java_json e1) ++ ")) {" ++ eol
++ s2
++ (indent (i+1)) ++ v0 ++ " = " ++ (from_java_json e2) ++ ";" ++ eol
++ (indent i) ++ "} else {" ++ eol
++ s3
++ (indent (i+1)) ++ v0 ++ " = " ++ (from_java_json e3) ++ ";" ++ eol
++ (indent i) ++ "}" ++ eol,
(mk_java_json v0), t0 + 1)
| NNRCEither nd xl nl xr nr ⇒
let '(s1, e1, t2) := nnrcToJava nd t i eol quotel ivs in
let '(s2, e2, t1) := nnrcToJava nl t2 (i+1) eol quotel ivs in
let '(s3, e3, t0) := nnrcToJava nr t1 (i+1) eol quotel ivs in
let vl := "v" ++ xl in
let vr := "v" ++ xr in
let res := "res" ++ (nat_to_string10 t0) in
(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
++ 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
++ s3
++ (indent (i+1)) ++ res ++ " = " ++ (from_java_json e3) ++ ";" ++ eol
++ (indent i) ++ "}" ++ eol,
mk_java_json res, t0 + 1)
| NNRCGroupBy g sl n1 ⇒
let '(s1, e1, t0) := nnrcToJava n1 t i eol quotel ivs in
let e0 := mk_java_unary_opn "groupby" [(mk_java_string g);(mk_java_string_collection sl)] e1 in
(s1, e0, t0)
end.
Definition nnrcToJavaunshadow (n : nnrc) (t : nat) (i : nat) (eol : string) (quotel : string) (avoid: list var) (ivs : list (string × string)) :=
let n := unshadow_java avoid n in
nnrcToJava n t i eol quotel ivs.
Definition makeJavaParams (ivs: list(string×string)) :=
joinStrings ", " (map (fun elem ⇒ "JsonElement " ++ snd elem) ivs).
Definition closeFreeVars (input:string) (e:nnrc) (ivs:list(string×string)) : nnrc :=
let all_free_vars := nnrc_free_vars e in
let wrap_one_free_var (e':nnrc) (fv:string) : nnrc :=
if (assoc_lookupr equiv_dec ivs fv)
then e'
else
let unconsted_fv := unConstVar fv in
(NNRCLet fv (NNRCUnop (ADot unconsted_fv) (NNRCVar input)) e')
in
fold_left wrap_one_free_var all_free_vars e.
Definition nnrcToJavaFun (i:nat) (input_v:string) (e:nnrc) (eol:string) (quotel:string) (ivs : list (string × string)) (fname:string) :=
let e' := closeFreeVars input_v e ivs in
let '(j0, v0, t0) := nnrcToJavaunshadow e' 1 (i + 1) eol quotel ("constants"::"hierarchy"::(List.map fst ivs)) ivs in
(indent i) ++ "public JsonElement " ++ fname ++ "(Hierarchy hierarchy, "++ (makeJavaParams ivs) ++ ") {" ++ eol
++ j0
++ (indent i) ++ " return " ++ (from_java_json v0) ++ ";" ++ eol
++ (indent i) ++ "}" ++ eol.
Definition nnrcToJavaClass (class_name:string) (package_name:string) (imports:string) (input_v:string) (e:nnrc) (eol:string) (quotel:string) (ivs : list (string × string)) (fname:string) :=
let f := nnrcToJavaFun 1 input_v e eol quotel ivs fname in
(if(package_name == "")
then ""
else "package " ++ package_name ++ ";" ++ eol ++ eol)
++ "import com.google.gson.*;" ++ eol
++ (if(imports == "")
then ""
else "import " ++ imports ++ ";" ++ eol)
++ (if(package_name == "org.qcert.runtime")
then ""
else "import org.qcert.runtime.*;" ++ eol)
++ eol
++ "public class " ++ class_name ++ " implements JavaQuery { " ++ eol
++ f
++ "}" ++ eol
.
Definition nnrcToJavaTop (class_name:string) (imports:string) (e:nnrc) : string :=
let input_f := "query" in
let input_v := "constants" in
nnrcToJavaClass class_name "" imports input_v e eol_newline quotel_double ((input_v, input_v)::nil) input_f.
End NNRCJava.
End NNRCtoJava.