Module Qcert.EJson.Operators.EJsonOperators

Require Import Bool.
Require Import EquivDec.
Require Import String.
Require Import List.
Require Import ZArith.
Require Import Utils.
Require Import FloatAdd.
Require Import ListAdd.
Require Import Lift.
Require Import Assoc.
Require Import Bindings.
Require Import ForeignEJson.
Require Import EJson.

Section EJsonOperators.

  Import ListNotations.

  Inductive ejson_op :=
  | EJsonOpNot : ejson_op
  | EJsonOpNeg : ejson_op
  | EJsonOpAnd : ejson_op
  | EJsonOpOr : ejson_op
  | EJsonOpLt : ejson_op
  | EJsonOpLe : ejson_op
  | EJsonOpGt : ejson_op
  | EJsonOpGe : ejson_op
  | EJsonOpAddString : ejson_op
  | EJsonOpAddNumber : ejson_op
  | EJsonOpSub : ejson_op
  | EJsonOpMult : ejson_op
  | EJsonOpDiv : ejson_op
  | EJsonOpStrictEqual : ejson_op
  | EJsonOpStrictDisequal : ejson_op
  | EJsonOpArray : ejson_op
  | EJsonOpArrayLength : ejson_op
  | EJsonOpArrayPush : ejson_op
  | EJsonOpArrayAccess : ejson_op
  | EJsonOpObject : list string -> ejson_op
  | EJsonOpAccess : string -> ejson_op
  | EJsonOpHasOwnProperty : string -> ejson_op
  | EJsonOpMathMin : ejson_op
  | EJsonOpMathMax : ejson_op
  | EJsonOpMathPow : ejson_op
  | EJsonOpMathExp : ejson_op
  | EJsonOpMathAbs : ejson_op
  | EJsonOpMathLog : ejson_op
  | EJsonOpMathLog10 : ejson_op
  | EJsonOpMathSqrt : ejson_op
  | EJsonOpMathCeil : ejson_op
  | EJsonOpMathFloor : ejson_op
  | EJsonOpMathTrunc : ejson_op
  .

  Section Evaluation.
    Context {foreign_ejson_model:Set}.
    Context {fejson:foreign_ejson foreign_ejson_model}.

    Definition ejson_op_eval (op:ejson_op) (j:list (@ejson foreign_ejson_model)) : option ejson :=
      match op with
      | EJsonOpNot =>
        match j with
        | [ejbool b] => Some (ejbool (negb b))
        | _ => None
        end
      | EJsonOpNeg =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_neg n))
        | _ => None
        end
      | EJsonOpAnd =>
        match j with
        | [ejbool b1; ejbool b2] => Some (ejbool (andb b1 b2))
        | _ => None
        end
      | EJsonOpOr =>
        match j with
        | [ejbool b1; ejbool b2] => Some (ejbool (orb b1 b2))
        | _ => None
        end
      | EJsonOpLt =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejbool (float_lt n1 n2))
        | _ => None
        end
      | EJsonOpLe =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejbool (float_le n1 n2))
        | _ => None
        end
      | EJsonOpGt =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejbool (float_gt n1 n2))
        | _ => None
        end
      | EJsonOpGe =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejbool (float_ge n1 n2))
        | _ => None
        end
      | EJsonOpAddString =>
        match j with
        | [ejstring s1; ejstring s2] => Some (ejstring (s1 ++ s2))
        | _ => None
        end
      | EJsonOpAddNumber =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_add n1 n2))
        | _ => None
        end
      | EJsonOpSub =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_sub n1 n2))
        | _ => None
        end
      | EJsonOpMult =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_mult n1 n2))
        | _ => None
        end
      | EJsonOpDiv =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_div n1 n2))
        | _ => None
        end
      | EJsonOpStrictEqual =>
        match j with
        | [ejnull; ejnull] => Some (ejbool true)
        | [ejbool b1; ejbool b2] => Some (ejbool (if bool_dec b1 b2 then true else false))
        | [ejnumber n1; ejnumber n2] => Some (ejbool (if float_eq_dec n1 n2 then true else false))
        | [ejbigint n1; ejbigint n2] => Some (ejbool (if Z.eq_dec n1 n2 then true else false))
        | [ejstring s1; ejstring s2] => Some (ejbool (if string_dec s1 s2 then true else false))
        | _ => Some (ejbool false)
        end
      | EJsonOpStrictDisequal =>
        match j with
        | [ejnull; ejnull] => Some (ejbool false)
        | [ejbool b1; ejbool b2] => Some (ejbool (if bool_dec b1 b2 then false else true))
        | [ejnumber n1; ejnumber n2] => Some (ejbool (if float_eq_dec n1 n2 then false else true))
        | [ejbigint n1; ejbigint n2] => Some (ejbool (if Z.eq_dec n1 n2 then false else true))
        | [ejstring s1; ejstring s2] => Some (ejbool (if string_dec s1 s2 then false else true))
        | _ => Some (ejbool false)
        end
      | EJsonOpArray => Some (ejarray j)
      | EJsonOpArrayLength =>
        match j with
        | [ejarray ja] => Some (ejbigint (Z_of_nat (List.length ja)))
        | _ => None
        end
      | EJsonOpArrayPush =>
        match j with
        | [ejarray ja; je] => Some (ejarray (ja ++ [je]))
        | _ => None
        end
      | EJsonOpArrayAccess =>
        match j with
        | [ejarray ja; ejbigint n] =>
          let natish := ZToSignedNat n in
          if (fst natish) then
            match List.nth_error ja (snd natish) with
            | None => None
            | Some d => Some d
            end
          else None
        | _ => None
        end
      | EJsonOpObject atts =>
        lift ejobject (zip atts j)
      | EJsonOpAccess att =>
        match j with
        | [ejobject jl] =>
          edot jl att
        | _ => None
        end
      | EJsonOpHasOwnProperty a =>
        match j with
        | [ejobject jl] =>
          if in_dec string_dec a (domain jl)
          then Some (ejbool true)
          else Some (ejbool false)
        | _ => None
        end
      | EJsonOpMathMin =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_min n1 n2))
        | _ => None
        end
      | EJsonOpMathMax =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_max n1 n2))
        | _ => None
        end
      | EJsonOpMathExp =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_exp n))
        | _ => None
        end
      | EJsonOpMathPow =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_pow n1 n2))
        | _ => None
        end
      | EJsonOpMathAbs =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_absolute n))
        | _ => None
        end
      | EJsonOpMathLog =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_log n))
        | _ => None
        end
      | EJsonOpMathLog10 =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_log10 n))
        | _ => None
        end
      | EJsonOpMathSqrt =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_sqrt n))
        | _ => None
        end
      | EJsonOpMathCeil =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_ceil n))
        | _ => None
        end
      | EJsonOpMathFloor =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_floor n))
        | _ => None
        end
      | EJsonOpMathTrunc =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_of_int (float_truncate n)))
        | _ => None
        end
      end.
  End Evaluation.

End EJsonOperators.