Module Qcert.Translation.Operators.ForeignToEJsonRuntime

Require Import EquivDec.
Require Import List.
Require Import String.
Require Import Ascii.
Require Import Utils.
Require Import DataRuntime.
Require Import EJsonRuntime.
Require Import ForeignDataToEJson.
Require Import DataToEJson.

Section ForeignToEJsonRuntime.

  Class foreign_to_ejson_runtime
        {foreign_ejson_model:Set}
        {foreign_ejson_runtime_op:Set}
        {fejson:foreign_ejson foreign_ejson_model}
        {fruntime:foreign_runtime}
        {fetojson:foreign_to_ejson foreign_ejson_model foreign_ejson_runtime_op}
        {fejsonops:foreign_ejson_runtime foreign_ejson_runtime_op}
      : Type
      := mk_foreign_to_ejson_runtime {
             foreign_to_ejson_runtime_of_unary_op
               (uop:foreign_operators_unary) : foreign_ejson_runtime_op
             ; foreign_to_ejson_runtime_of_unary_op_correct
                 (uop:foreign_operators_unary)
                 (br:brand_relation_t)
                 (d:data) :
                 lift data_to_ejson (foreign_operators_unary_interp br uop d) =
                 foreign_ejson_runtime_op_interp (foreign_to_ejson_runtime_of_unary_op uop)
                                                 (data_to_ejson d::nil)
             ; foreign_to_ejson_runtime_of_binary_op
               (bop:foreign_operators_binary) : foreign_ejson_runtime_op
             ; foreign_to_ejson_runtime_of_binary_op_correct
                 (bop:foreign_operators_binary)
                 (br:brand_relation_t)
                 (d1 d2:data) :
                 lift data_to_ejson (foreign_operators_binary_interp br bop d1 d2) =
                 foreign_ejson_runtime_op_interp (foreign_to_ejson_runtime_of_binary_op bop)
                                                 (data_to_ejson d1::data_to_ejson d2::nil)
             ; foreign_to_ejson_runtime_tostring_correct
                 (d:data) :
                 foreign_operators_unary_data_tostring d =
                 foreign_ejson_runtime_tostring (data_to_ejson d)
             ; foreign_to_ejson_runtime_totext_correct
                 (d:data) :
                 foreign_operators_unary_data_totext d =
                 foreign_ejson_runtime_totext (data_to_ejson d)
         }.

  Section defaultToString.
    Context {fruntime:foreign_runtime}.
    Context {foreign_ejson_model:Set}.
    Context {fejson:foreign_ejson foreign_ejson_model}.
    Context {foreign_ejson_runtime_op : Set}.
    Context {fetojson:foreign_to_ejson foreign_ejson_model foreign_ejson_runtime_op}.

    Ltac rewrite_string_dec_from_neq H
      := let d := fresh "d" in
          let neq := fresh "neq" in
          destruct (string_dec_from_neq H) as [d neq]
          ; repeat rewrite neq in *
          ; clear d neq.

    Lemma default_ejson_rec_aux1 j r :
      ejson_is_record j = Some r ->
      defaultEJsonToString j = string_bracket
          "{"%string
          (String.concat ", "%string
                         (map (fun xy => let '(x,y):=xy in
                                         (append (stringToString (key_decode x)) (append "->"%string (defaultEJsonToString y)))
                              ) r))
          "}"%string.

    Lemma default_ejson_rec_aux2 r:
      @Forall (prod string (@data (@foreign_runtime_data fruntime)))
              (fun ab : prod string (@data (@foreign_runtime_data fruntime)) =>
                 @eq string
                     (@defaultDataToString (@foreign_runtime_data fruntime)
                                           (@snd string (@data (@foreign_runtime_data fruntime)) ab))
                     (@defaultEJsonToString foreign_ejson_model fejson
                                            (@data_to_ejson fruntime foreign_ejson_model fejson foreign_ejson_runtime_op fetojson
                                                            (@snd string (@data (@foreign_runtime_data fruntime)) ab)))) r
      ->
      @eq string (@defaultDataToString (@foreign_runtime_data fruntime) (@drec (@foreign_runtime_data fruntime) r))
          (@defaultEJsonToString foreign_ejson_model fejson
                                 (@data_to_ejson fruntime foreign_ejson_model fejson foreign_ejson_runtime_op fetojson (@drec (@foreign_runtime_data fruntime) r))).

    Lemma default_to_ejson_tostring_correct :
      (forall fd : foreign_data_model,
          toString fd = toString (foreign_to_ejson_from_data fd)) ->
      forall d:data, defaultDataToString d = defaultEJsonToString (data_to_ejson d).
  End defaultToString.
End ForeignToEJsonRuntime.