Module Qcert.Translation.Lang.NNRCtoJava

Require Import List.
Require Import String.
Require Import BinInt.
Require Import Ascii.
Require Import Peano_dec.
Require Import EquivDec.
Require Import Utils.
Require Import DataRuntime.
Require Import JavaRuntime.
Require Import NNRCRuntime.
Require Import ForeignToJava.

Import ListNotations.
Local Open Scope string_scope.

Section NNRCtoJava.
  Section sanitizer.
    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.

  Context {fruntime:foreign_runtime}.

  Section DataJava.
    Context {ftojavajson:foreign_to_java}.

    Definition mk_java_json_brands (quotel:string) (b:brands) : java_json
      := mk_java_json_array (map (mk_java_json_string quotel) b).

    Fixpoint mk_java_json_data (quotel:string) (d : data) : java_json :=
      match d with
      | dunit => java_json_NULL
      | dnat n => mk_java_json_nat quotel n
      | dfloat n => mk_java_json_number 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.
    Import ListNotations.
    
    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}.
    Import ListNotations.

    Definition uarithToJavaMethod (u:nat_arith_unary_op) :=
      match u with
      | NatAbs => "abs"
      | NatLog2 => "log2"
      | NatSqrt =>"sqrt"
      end.

    Definition float_uarithToJavaMethod (fu:float_arith_unary_op) :=
      match fu with
      | FloatNeg => "float_neg"
      | FloatSqrt => "float_sqrt"
      | FloatExp => "float_exp"
      | FloatLog => "float_log"
      | FloatLog10 => "float_log10"
      | FloatCeil => "float_ceil"
      | FloatFloor => "float_floor"
      | FloatAbs => "float_abs"
      end.

    Definition nat_barithToJavaMethod (b:nat_arith_binary_op) :=
      match b with
      | NatPlus => "plus"
      | NatMinus => "minus "
      | NatMult => "mult"
      | NatDiv => "divide"
      | NatRem => "rem"
      | NatMin => "min"
      | NatMax => "max"
      end.

    Definition float_barithToJavaMethod (fb:float_arith_binary_op)
      := match fb with
         | FloatPlus => "float_plus"
         | FloatMinus => "float_minus"
         | FloatMult => "float_mult"
         | FloatDiv => "float_divide"
         | FloatPow => "float_pow"
         | FloatMin => "float_min"
         | FloatMax => "float_max"
         end.

    Definition float_bcompareToJavaMethod (fb:float_compare_binary_op)
      := match fb with
         | FloatLt => "float_lt"
         | FloatLe => "float_le"
         | FloatGt => "float_gt"
         | FloatGe => "float_ge"
         end.

    Definition like_clause_to_java (lc:like_clause)
      := match lc with
         | like_literal literal => "new UnaryOperators.LiteralLikeClause(" ++ (mk_java_string literal) ++ ")"
         | like_any_char => "new UnaryOperators.AnyCharLikeClause()"
         | like_any_string => "new UnaryOperators.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
         | NNRCGetConstant v =>
           ("", mk_java_json ("v" ++ v), t)
         | 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
                     | OpIdentity => e1
                     | OpNeg => mk_java_unary_op0 "neg" e1
                     | OpRec s => mk_java_unary_op1 "rec" (mk_java_string s) e1
                     | OpDot s => mk_java_unary_op1 "dot" (mk_java_string s) e1
                     | OpRecRemove s => mk_java_unary_op1 "remove" (mk_java_string s) e1
                     | OpRecProject sl => mk_java_unary_op1 "project" (mk_java_string_collection sl) e1
                     | OpBag => mk_java_unary_op0 "coll" e1
                     | OpSingleton => mk_java_unary_op0 "singleton" e1
                     | OpFlatten => mk_java_unary_op0 "flatten" e1
                     | OpDistinct => mk_java_unary_op0 "distinct" e1
                     | OpOrderBy sl =>
                       mk_java_unary_op1 "sort" (mk_java_sort_criterias quotel sl) e1
                     | OpCount => mk_java_unary_op0 "count" e1
                     | OpToString => mk_java_unary_op0 "tostring" e1
                     | OpToText => mk_java_unary_op0 "totext" 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
                       | None => mk_java_unary_op1 "substring" (toString start) e1
                       end
                     | OpLike pat =>
                       let lc := make_like_clause pat None in
                       mk_java_unary_op1 "string_like" ("new UnaryOperators.LikeClause[]{"
                                         ++ (map_concat "," like_clause_to_java lc) ++ "}") e1
                     | OpLeft => mk_java_unary_op0 "left" e1
                     | OpRight => mk_java_unary_op0 "right" e1
                     | OpBrand b =>mk_java_unary_op1 "brand" (mk_java_string_collection b) e1
                     | OpUnbrand => mk_java_unary_op0 "unbrand" e1
                     | OpCast b => mk_java_unary_opn "cast" ["inheritance"; (mk_java_string_collection b)] e1
                     | OpNatUnary u => mk_java_unary_op0 (uarithToJavaMethod u) e1
                     | OpNatSum => mk_java_unary_op0 "sum" e1
                     | OpNatMin => mk_java_unary_op0 "list_min" e1
                     | OpNatMax => mk_java_unary_op0 "list_max" e1
                     | OpNatMean => mk_java_unary_op0 "list_mean" e1
                     | OpFloatOfNat => mk_java_unary_op0 "float_of_int" e1
                     | OpFloatUnary u => mk_java_unary_op0 (float_uarithToJavaMethod u) e1
                     | OpFloatTruncate => mk_java_unary_op0 "float_truncate" e1
                     | OpFloatSum => mk_java_unary_op0 "float_sum" e1
                     | OpFloatBagMin => mk_java_unary_op0 "float_list_min" e1
                     | OpFloatBagMax => mk_java_unary_op0 "float_list_max" e1
                     | OpFloatMean => mk_java_unary_op0 "float_list_mean" e1
                     | OpForeignUnary 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
                     | OpEqual => mk_java_binary_op0 "equals" e1 e2
                     | OpRecConcat => mk_java_binary_op0 "concat" e1 e2
                     | OpRecMerge => mk_java_binary_op0 "mergeConcat" e1 e2
                     | OpAnd => mk_java_binary_op0 "and" e1 e2
                     | OpOr => mk_java_binary_op0 "or" e1 e2
                     | OpLt => mk_java_binary_op0 "lt" e1 e2
                     | OpLe => mk_java_binary_op0 "le" e1 e2
                     | OpBagUnion => mk_java_binary_op0 "union" e1 e2
                     | OpBagDiff => mk_java_binary_op0 "bag_minus" e1 e2
                     | OpBagMin => mk_java_binary_op0 "bag_min" e1 e2
                     | OpBagMax => mk_java_binary_op0 "bag_max" e1 e2
                     | OpBagNth => mk_java_binary_op0 "bag_nth" e1 e2
                     | OpContains => mk_java_binary_op0 "contains" e1 e2
                     | OpStringConcat => mk_java_binary_op0 "stringConcat" e1 e2
                     | OpStringJoin => mk_java_binary_op0 "stringJoin" e1 e2
                     | OpNatBinary b => mk_java_binary_op0 (nat_barithToJavaMethod b) e1 e2
                     | OpFloatBinary b => mk_java_binary_op0 (float_barithToJavaMethod b) e1 e2
                     | OpFloatCompare b => mk_java_binary_op0 (float_bcompareToJavaMethod b) e1 e2
                     | OpForeignBinary 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.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.getRight(" ++ (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)) :=
      map_concat ", " (fun elem => "JsonElement " ++ snd elem) ivs.

    Definition closeFreeVars (input:string) (e:nnrc) (ivs:list(string*string)) : nnrc :=
      let all_free_vars := nnrc_global_vars e in
      let wrap_one_free_var (e':nnrc) (fv:string) : nnrc :=
          if (assoc_lookupr equiv_dec ivs fv)
          then e'
          else
            (NNRCLet fv (NNRCUnop (OpDot 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"::"inheritance"::(List.map fst ivs)) ivs in
      (indent i) ++ "public JsonElement " ++ fname ++ "(Inheritance inheritance, " ++ (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 nnrc_to_java_top (class_name:string) (imports:string) (e:nnrc) : java :=
      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.