Module CldMRtoCloudant

Require Import List.
Require Import String.
Require Import Utils.
Require Import BasicRuntime.
Require Import ForeignToJavaScript.
Require Import ForeignCloudant.
Require Import NNRCRuntime.
Require Import CldMRRuntime.
Require Import CloudantRuntime.
Require Import NNRCtoJavaScript.

Local Open Scope string_scope.

Section CldMRtoCloudant.

  Context {fruntime:foreign_runtime}.
  Context {ftojavascript:foreign_to_javascript}.
  Context {fcloudant:foreign_cloudant}.

  Section MRJS.

    Definition emitIdToString (vkey vout:string) (eol:string) (quotel:string) : string :=
      " emit(" ++ vkey ++ ", " ++ vout ++ ");" ++ eol.

    Definition emitConstIdToString (n:nat) (vkey vout:string) (eol:string) (quotel:string) : string :=
      " emit(" ++ (nat_to_string10 n) ++ ", " ++ vout ++ ");" ++ eol.
    
    Definition emitConstToString (n:nat) (vkey vout:string) (eol:string) (quotel:string) : string :=
        " for (var srcout="
          ++ vout ++ ", iout=0; iout<" ++ vout ++ ".length; iout++) {" ++ eol
          ++ " emit(" ++ (nat_to_string10 n) ++ ",srcout[iout]);" ++ eol
          ++ " }" ++ eol.
    
    Definition emitInventToString (vkey vout:string) (eol:string) (quotel:string) : string :=
        " for (var srcout="
          ++ vout ++ ", iout=0; iout<" ++ vout ++ ".length; iout++) {" ++ eol
          ++ " emit(" ++ vkey ++ ".concat(iout),srcout[iout]);" ++ eol
          ++ " }" ++ eol.

    Definition createMapFunFirst (v_map:string) (e:nnrc) (emitString:string) (harness:bool) (eol:string) (quotel:string) : string :=
          let '(j0, v0, t0) := nnrcToJSunshadow e 1 1 eol quotel (v_map::nil) ((v_map,"doc")::nil) in
          "function (doc) {" ++ eol
                             ++ " var v0 = null;" ++ eol
                             ++ " var key = doc._id;" ++ eol
                             ++ " var doc = unwrap(doc);" ++ eol
                             ++ " if (doc != null) {" ++ eol
                             ++ j0
                             ++ " var out = " ++ v0 ++ ";" ++ eol
                             ++ emitString ++ eol
                             ++ " }"
                             ++ (if harness then " %HARNESS% " else "")
                             ++ "}".
    
    Definition createMapFunRest (v_map:string) (e:nnrc) (emitString:string) (harness:bool) (eol:string) (quotel:string) : string :=
          let '(j0, v0, t0) := nnrcToJSunshadow e 1 1 eol quotel (v_map::nil) ((v_map,"doc")::nil) in
          "function (doc) {" ++ eol
                             ++ " var v0 = null;" ++ eol
                             ++ " var key = doc.key;" ++ eol
                             ++ " var doc = doc.value;" ++ eol
                             ++ j0
                             ++ " var out = " ++ v0 ++ ";" ++ eol
                             ++ emitString ++ eol
                             ++ (if harness then " %HARNESS% " else "")
                             ++ "}".

    Definition nnrcToJSMapFirst (cldmap:cld_map) (h:list (string*string)) (harness:bool) (eol:string) (quotel:string) : string :=
      match map_fun cldmap with
      | CldMapId (v_map, e) =>
        match map_emit cldmap with
        | CldEmitDist =>
          createMapFunFirst v_map e (emitIdToString "key" "out" eol quotel) harness eol quotel
        | CldEmitCollect index =>
          createMapFunFirst v_map e (emitConstIdToString index "key" "out" eol quotel) harness eol quotel
        end
      | CldMapFlatten (v_map, e) =>
        match map_emit cldmap with
        | CldEmitDist =>
          createMapFunFirst v_map e (emitInventToString "key" "out" eol quotel) harness eol quotel
        | CldEmitCollect index =>
          createMapFunFirst v_map e (emitConstToString index "key" "out" eol quotel) harness eol quotel
        end
      end.

    Definition nnrcToJSMapRest (cldmap:cld_map) (h:list (string*string)) (harness:bool) (eol:string) (quotel:string) : string :=
      match map_fun cldmap with
      | CldMapId (v_map, e) =>
        match map_emit cldmap with
        | CldEmitDist =>
          createMapFunRest v_map e (emitIdToString "key" "out" eol quotel) harness eol quotel
        | CldEmitCollect index =>
          createMapFunRest v_map e (emitConstIdToString index "key" "out" eol quotel) harness eol quotel
        end
      | CldMapFlatten (v_map, e) =>
        match map_emit cldmap with
        | CldEmitDist =>
          createMapFunRest v_map e (emitInventToString "key" "out" eol quotel) harness eol quotel
        | CldEmitCollect index =>
          createMapFunRest v_map e (emitConstToString index "key" "out" eol quotel) harness eol quotel
        end
      end.

    Definition nnrcToJSReduce (e1:nnrc) (e2:nnrc) (h:list (string*string)) (harness:bool) (eol:string) (quotel:string) (values_iv:string) : string :=
      let '(j0, v0, t0) := nnrcToJSunshadow e1 1 1 eol quotel (values_iv::nil) ((values_iv,"values")::nil) in
      let '(j1, v1, t1) := nnrcToJSunshadow e2 t0 1 eol quotel (values_iv::nil) ((values_iv,"values")::nil) in
      "function (keys, values, rereduce) {" ++ eol
                                            ++ " if (rereduce) {" ++ eol
                                            ++ j1
                                            ++ " return " ++ v1 ++ ";" ++ eol
                                            ++ " }" ++ eol
                                            ++ " else {" ++ eol
                                            ++ j0
                                            ++ " return " ++ v0 ++ ";" ++ eol
                                            ++ " }" ++ eol
                                            ++ (if harness then " %HARNESS% " else "")
                                            ++ "}".

    Definition idJSReduce (h:list (string*string)) (harness:bool) (eol:string) (quotel:string) : string :=
      "function (keys, values, rereduce) {" ++ eol
                                            ++ " return values[0];" ++ eol
                                            ++ "}".

    Definition nnrcToJSDefault (harness:bool) (e_def:nnrc) (eol:string) (quotel:string) :=
      let '(j0, v0, t0) := nnrcToJSunshadow e_def 1 1 eol quotel nil nil in
      nnrcToJSFunStub harness e_def eol quotel nil "db_default".
    
    Definition nnrcToJSGen (harness:bool) (e_closure:(list var) * nnrc) (eol:string) (quotel:string) :=
      let (params, e) := e_closure in
      nnrcToJSFunStub harness e eol quotel params "db_post".
    
    Definition mapReduceStringstoJS_pair (eol:string) (index:nat) (mr:option string * option string * option string * option string * string) : string :=
      match mr with
      | (i,o,def,None,m) =>
        let iname :=
            match i with
            | None => "INPUT"
            | Some s => s
            end
        in
        let oname :=
            match o with
            | None => "RESULT"
            | Some s => s
            end
        in
        "// Input DB: " ++ iname ++ eol
                        ++ "// Output DB: " ++ oname ++ eol
                        ++ "// Map Nb " ++ (nat_to_string10 index) ++ eol ++ m ++ eol ++ eol
      | (i,o,def, Some r, m) =>
        let iname :=
            match i with
            | None => "INPUT"
            | Some s => s
            end
        in
        let oname :=
            match o with
            | None => "RESULT"
            | Some s => s
            end
        in
        "// Input DB: " ++ iname ++ eol
                        ++ "// Output DB: " ++ oname ++ eol
                        ++ "// Map Nb " ++ (nat_to_string10 index) ++ eol ++ m ++ eol
                        ++ "// Reduce Nb " ++ (nat_to_string10 index) ++ eol ++ r ++ eol ++ eol
      end.

    Definition mapReduceStringstoJS (eol:string) (mrp:list (option string * option string * option string * option string * string)) : string :=
      fst (fold_right (fun x y => (append (mapReduceStringstoJS_pair eol (snd y) x) (fst y), S (snd y))) ("",0) mrp).
  
  End MRJS.

  Section CloudantJS.
    
    Definition cldmrToJS (h:list (string*string)) (ini:bool) (harness:bool) (eol:string) (quotel:string) (mr:cldmr_step) : option string * option string * option string * option string * string :=
      let v_input := cldmr_step_input mr in
      let vs_input := Some v_input in
      let cldmap := cldmr_step_map mr in
      let clddefault := cldmr_step_reduce_default mr in
      let map_string :=
          if ini
          then nnrcToJSMapFirst cldmap h harness eol quotel
          else nnrcToJSMapRest cldmap h harness eol quotel
      in
      let default_string :=
          match clddefault with
          | None => None
          | Some clddef =>
            Some (nnrcToJSDefault harness clddef eol quotel)
          end
      in
      match cldmr_step_reduce mr with
      | None =>
        (vs_input, None, default_string, None, map_string)
      | Some mred =>
        let v_output := reduce_output mred in
        let vs_output :=
            match v_output with
            | None => None
            | Some v => Some v
            end
        in
        match mred.(reduce_fun) with
        | CldRedId =>
          let reduce_string := idJSReduce h harness eol quotel in
          (vs_input, vs_output, default_string, Some reduce_string, map_string)
        | CldRedAggregate (vs_reduce, f_reduce) (v_rereduce, f_rereduce) =>
          let (v_key, v_reduce) := vs_reduce in
          let reduce_string := nnrcToJSReduce f_reduce f_rereduce h harness eol quotel v_reduce in
          (vs_input, vs_output, default_string, Some reduce_string, map_string)
        | CldRedOp CldRedOpCount =>
          (vs_input, vs_output, default_string, Some "_count", map_string)
        | CldRedOp (CldRedOpSum _) =>
          (vs_input, vs_output, default_string, Some "_sum", map_string)
        | CldRedOp (CldRedOpStats _) =>
          (vs_input, vs_output, default_string, Some "_stats", map_string)
        end
      end.

    Definition cld_mr_chainToJS (h:list (string*string)) (harness:bool) (eol:string) (quotel:string) (mrl:list cldmr_step) : list (option string * option string * option string * option string * string) :=
      match mrl with
      | nil => nil
      | mr1 :: mrl' =>
        (cldmrToJS h true harness eol quotel mr1)
          :: (map (cldmrToJS h false harness eol quotel) mrl')
      end.

    Definition cld_mrToJS (h:list (string*string)) (harness:bool) (eol:string) (quotel:string) (mrl:cldmr) : list (option string * option string * option string * option string * string) :=
      cld_mr_chainToJS h harness eol quotel mrl.(cldmr_chain).

    Definition cld_mrToLastJS (h:list (string*string)) (harness:bool) (eol:string) (quotel:string) (e_closure: (list var) * nnrc) : string :=
      nnrcToJSGen harness e_closure eol quotel.

    Definition buildDesignDoc (view_name:string) (s_map:string) (s_reduce:option string) (s_dboutput:option string) (s_dbdefault:option string) :=
      let dmap := ("map", dstring s_map) in
      let dreduce :=
          match s_reduce with
          | None => nil
          | Some s_r => ("reduce", dstring s_r)::nil
          end
      in
      let dbcopy :=
          match s_dboutput with
          | None => nil
          | Some s_db => ("dbcopy", dstring (view_name ++ s_db))::nil
          end
      in
      let dbdefault :=
          match s_dbdefault with
          | None => nil
          | Some s_dbd => ("dbdefault", dstring s_dbd)::nil
          end
      in
      drec (("views", drec ((view_name, drec (dmap::(List.app dreduce (List.app dbcopy dbdefault))))::nil))::nil).


    Definition db_of_var (rulename:string) (var:string) : string := rulename ++ var.
    
    Definition makeInputDB (rulename:string) (ins: option string) : string :=
      match ins with
      | None => rulename
      | Some x => db_of_var rulename x
      end.

    Definition makeInputDesignDoc
               (quotel:string)
               (rulename:string)
               (mrp:option string * option string * option string * option string * string)
      : cloudant_design :=
      match mrp with
      | (inputdb, outputdb, defaultdb, mreduce, mmap) =>
        mkCloudantDesign
          (makeInputDB rulename None)
          (dataToJS quotel (buildDesignDoc rulename mmap mreduce outputdb defaultdb))
      end.
    
    Definition makeDesignDoc (quotel:string) (rulename:string) (mrp:option string * option string * option string * option string * string) : cloudant_design :=
      match mrp with
      | (inputdb, outputdb, defaultdb, mreduce, mmap) =>
        mkCloudantDesign
          (makeInputDB rulename inputdb)
          (dataToJS quotel (buildDesignDoc rulename mmap mreduce outputdb defaultdb))
      end.
    
    Definition makeCloudantDesignDocs (quotel:string) (rulename:string) (mrp:list (option string * option string * option string * option string * string)) : list cloudant_design :=
      List.map (fun x => makeDesignDoc quotel rulename x) mrp.
    
    Definition makeCloudantDesignDocsTop
               (quotel:string)
               (rulename:string)
               (mrp:list (option string * option string * option string * option string * string))
               (last_expr:string)
               (cld_eff:list string)
      : cloudant :=
      match mrp with
      | nil =>
        mkCloudant
          nil
          last_expr
          cld_eff
      | x :: nil =>
        mkCloudant
          ((makeInputDesignDoc quotel rulename x) :: nil)
          last_expr
          cld_eff
      | x :: mrp' =>
        mkCloudant
          ((makeInputDesignDoc quotel rulename x)
             :: (makeCloudantDesignDocs quotel rulename mrp'))
          last_expr
          cld_eff
     end.
    
    Definition makeOneCurl (mrp: string*string) : string :=
      match mrp with
      | (dbname,design) =>
        "curl -X PUT ""https://fe0a4004-9ff8-4bc4-9de8-906e1831cc78-bluemix:8a67972aa73304b3b7cc9b0cc4525d2e6c26988dd08c787ae29d5d68079c0b54@fe0a4004-9ff8-4bc4-9de8-906e1831cc78-bluemix.cloudant.com/" ++ dbname ++ "/_design/" ++ dbname ++ """ -H 'Content-type: application/json' -d '" ++ design ++ "'" ++ eol_newline
      end.

    Definition mapReduceStringstoDesignDocs (mrp:list (option string * option string * option string * option string * string)) (last_expr:string) (cld_eff:list string) (rulename:string) : cloudant :=
      makeCloudantDesignDocsTop quotel_double rulename mrp last_expr cld_eff.

    Definition cld_mrParamsLast (rulename:string) (params:list var) :=
      map (db_of_var rulename) params.

    Definition mapReducePairstoCloudant (h:list (string*string)) (mrl : cldmr) (rulename:string) : cloudant :=
      let mrpl := cld_mrToJS h true eol_backn quotel_double mrl in
      let last_fun := cld_mrToLastJS h true eol_backn quotel_backdouble (fst (mrl.(cldmr_last))) in
      let cld_eff_params := cld_mrParamsLast rulename (snd (mrl.(cldmr_last))) in
      mapReduceStringstoDesignDocs mrpl last_fun cld_eff_params rulename.

  End CloudantJS.
  
End CldMRtoCloudant.