Module Qcert.Driver.CompEnv

Require Import String.
Require Import List.
Require Import String.
Require Import EquivDec.
Require Import Utils.
Require Import DataRuntime.

Section CompEnv.

  Definition init_vinit := "init"%string.

  Context {fdata:foreign_data}.
  
  Definition lift_result res :=
    match res with
    | None => None
    | Some (dcoll l) => Some l
    | Some _ => None
    end.

  Definition validate_data (oresult oexpected:option data) :=
      match oresult, oexpected with
      | None, None => true
      | Some result, Some expected =>
        if data_eq_dec result expected
        then true
        else false
      | _,_ => false
      end.

  Definition validate (oresult oexpected:option (list data)) :=
      match oresult, oexpected with
      | None, None => true
      | Some ((dcoll result)::nil), Some expected =>
        if permutation_dec result expected
        then true
        else false
      | _,_ => false
      end.
  Definition validate_success (oresult:option (list data)) (expected:list data)
    := validate oresult (Some expected).
  

  
  Definition validate_lifted_success (res:option data) exp : bool :=
    validate_success (lift_result res) exp.

End CompEnv.

Ltac fast_refl := vm_compute; reflexivity.