Module ErgoSpec.Backend.Qcert.QcertToScala

Require Import List.
Require Import ZArith.
Require Import EquivDec.
Require Import RelationClasses.
Require Import Equivalence.
Require Import String.

Require Import Qcert.Utils.Utils.
Require Import Qcert.TypeSystem.ForeignType.
Require Import Qcert.Translation.Model.ForeignTypeToJSON.
Require Import Qcert.Translation.Operators.ForeignToScala.

Require Import QcertData.
Require Import QcertEJson.
Require Import QcertDataToEJson.
Require Import QcertEJsonToJSON.
Require Import QcertToJava.
Require Import QcertType.

Local Open Scope nstring_scope.

Definition enhanced_to_scala_unary_op (op: enhanced_unary_op) (d: nstring) : nstring :=
  match op with
  | enhanced_unary_uri_op op => ^"QcertModel: uri ops not supported for now."
  | enhanced_unary_log_op op => ^"QcertModel: log ops not supported for now."
  | enhanced_unary_math_op op => ^"QcertModel: math ops not supported for now."
  | enhanced_unary_date_time_op op => ^"QcertModel: date time ops not supported for now."
  end.

Definition enhanced_to_scala_spark_datatype (ft: foreign_type_type) : nstring :=
  ^"FloatType".

Instance enhanced_foreign_to_scala:
  @foreign_to_scala enhanced_foreign_runtime _
  := mk_foreign_to_scala
       enhanced_foreign_runtime _
       enhanced_to_scala_unary_op
       enhanced_to_scala_spark_datatype.