Qcert.Tests.NRAEnvTest

Notation "⊥" := (dunit) : data_scope.
Notation "[||]" := (drec nil) : data_scope. Notation "[| x1 ; .. ; xn |]" := (RData.drec (cons x1 .. (cons xn nil) ..)) : data_scope.

Notation "{||}" := (dcoll nil) : data_scope. Notation "{| x1 ; .. ; xn |}" := (dcoll (cons x1 .. (cons xn nil) ..)) : data_scope.

Section NRAEnvTest.



  Example merge_env_example
    := [| ("A", dconst 1); ("B", dconst 3) |].

  Example merge_succeeds : cnraenv
    := χᵉ⟨ (ENV·"A") ♯+ (ENV·"C") ⟩ ◯ₑ (ENV ⊗ ‵ [| ("B", dconst 3) ; ("C", dconst 4) |]).

  Remark merge_succeeds_result :
    nil ⊢ₑ merge_succeeds @ₑ dunit ⊣ nil ; merge_env_example =
                                           Some {| dconst 5 |}.

  Example merge_fails : cnraenv
    := χᵉ⟨ (ENV·"A") ♯+ (ENV·"C") ⟩ ◯ₑ (ENV ⊗ ‵ [| ("B", dconst 2) ; ("C", dconst 4) |]).

  Remark merge_fails_result :
    nil ⊢ₑ merge_fails @ₑ dunit ⊣ nil ; merge_env_example =
                                           Some {||}.

End NRAEnvTest.