Module CompEnv

Section QEnv.

  Require Import String List String EquivDec.
  
  Require Import BasicRuntime.


  Definition init_vid := "id"%string.
  Definition init_venv := "env"%string.
  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.

  Require Import DData.

  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 QEnv.

Ltac fast_refl := vm_compute; reflexivity.