Qcert.Compiler.Driver.CompEnv

Section QEnv.




  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.


  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.