Module ErgoSpec.Backend.Qcert.QcertToReduceOps

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.Data.DataSystem.
Require Import Qcert.NNRCMR.Lang.ForeignReduceOps.
Require Import Qcert.Translation.Operators.ForeignToReduceOps.

Require Import QcertData.
Require Import QcertReduceOps.

Import ListNotations.
Local Open Scope list_scope.
Local Open Scope string_scope.
Local Open Scope nstring_scope.

Definition enhanced_to_reduce_op (uop:unary_op) : option NNRCMR.reduce_op :=
  match uop with
  | OpCount => Some (NNRCMR.RedOpForeign RedOpCount)
  | OpNatSum =>
    Some (NNRCMR.RedOpForeign (RedOpSum enhanced_numeric_int))
  | OpFloatSum =>
    Some (NNRCMR.RedOpForeign (RedOpSum enhanced_numeric_float))
  | OpNatMin =>
    Some (NNRCMR.RedOpForeign (RedOpMin enhanced_numeric_int))
  | OpFloatBagMin =>
    Some (NNRCMR.RedOpForeign (RedOpMin enhanced_numeric_float))
  | OpNatMax =>
    Some (NNRCMR.RedOpForeign (RedOpMax enhanced_numeric_int))
  | OpFloatBagMax =>
    Some (NNRCMR.RedOpForeign (RedOpMax enhanced_numeric_float))
  | OpNatMean =>
    Some (NNRCMR.RedOpForeign (RedOpArithMean enhanced_numeric_int))
  | OpFloatMean =>
    Some (NNRCMR.RedOpForeign (RedOpArithMean enhanced_numeric_float))
  | _ => None
  end.

Definition enhanced_of_reduce_op (rop:NNRCMR.reduce_op) : option unary_op :=
  match rop with
  | NNRCMR.RedOpForeign RedOpCount => Some OpCount
  | NNRCMR.RedOpForeign (RedOpSum enhanced_numeric_int) =>
    Some (OpNatSum)
  | NNRCMR.RedOpForeign (RedOpSum enhanced_numeric_float) =>
    Some (OpFloatSum)
  | NNRCMR.RedOpForeign (RedOpMin enhanced_numeric_int) =>
    Some (OpNatMin)
  | NNRCMR.RedOpForeign (RedOpMin enhanced_numeric_float) =>
    Some (OpFloatBagMin)
  | NNRCMR.RedOpForeign (RedOpMax enhanced_numeric_int) =>
    Some (OpNatMax)
  | NNRCMR.RedOpForeign (RedOpMax enhanced_numeric_float) =>
    Some (OpFloatBagMax)
  | NNRCMR.RedOpForeign (RedOpArithMean enhanced_numeric_int) =>
    Some (OpNatMean)
  | NNRCMR.RedOpForeign (RedOpArithMean enhanced_numeric_float) =>
    Some (OpFloatMean)
  | NNRCMR.RedOpForeign (RedOpStats _) =>
    None
  end.

Program Instance enhanced_foreign_to_reduce_op : foreign_to_reduce_op :=
  mk_foreign_to_reduce_op enhanced_foreign_runtime enhanced_foreign_reduce_op enhanced_to_reduce_op _ enhanced_of_reduce_op _.