Library liblayers.logic.PTreeModules

Require Import Coq.ZArith.ZArith.
Require Import Coq.Lists.List.
Require Import compcert.common.AST. Require Import liblayers.lib.Decision.
Require Import liblayers.logic.PseudoJoin.
Require Import liblayers.logic.OptionOrders.
Require Import liblayers.logic.PTrees.
Require Export liblayers.logic.Modules.
Require Import liblayers.compcertx.ErrorMonad.

Construction of modules

Modules are maps from identifiers to definitions, extended with an extra element id, which represents the module that passes along all of the primitives in the underlying layer.

Definition ptree_module F V :=
  (PTree.t (res F) × PTree.t (res V))%type.

Local Existing Instance ptree_le_op.
Local Existing Instance ptree_emptyset.
Local Existing Instance ptree_oplus.
Local Existing Instance ptree_mapsto.

Querying functions


Definition ptree_module_conflict i: errmsg :=
  MSG "duplicate symbol in module: " :: CTX i :: nil.

Section PTREE_MODULE_QUERY.
  Context {F V : Type}.

  Definition ptree_module_function i (M: ptree_module F V) :=
    option_res_flip ((fst M) ! i).

  Definition ptree_module_variable i (M: ptree_module F V): res (option V) :=
    option_res_flip ((snd M) ! i).

  Lemma ptree_module_function_mapsto (i: ident) (f: F):
    ptree_module_function i (i ↦ OK f, @PTree.empty _) = OK (Some f).
  Proof.
    unfold ptree_module_function.
    repeat (unfold mapsto, ptree_mapsto; simpl).
    rewrite PTree.gss.
    reflexivity.
  Qed.

  Global Instance ptree_module_function_monotonic:
    Proper
      (- ==>
       ptree_rel (option_le (res_le eq)) × ptree_rel (option_le (res_le eq)) ++>
       res_le (option_le eq))
      ptree_module_function.
  Proof.
    intros i M1 M2 HM.
    unfold ptree_module_function.
    solve_monotonic.
  Qed.

  Lemma ptree_module_variable_mapsto (i: ident) (τ: V):
    ptree_module_variable i (@PTree.empty _, i ↦ OK τ) = OK (Some τ).
  Proof.
    unfold ptree_module_variable.
    repeat (unfold mapsto, ptree_mapsto; simpl).
    rewrite PTree.gss.
    reflexivity.
  Qed.

  Global Instance ptree_module_variable_monotonic:
    Proper
      (- ==>
       ptree_rel (option_le (res_le eq)) × ptree_rel (option_le (res_le eq)) ++>
       res_le (option_le eq))
      ptree_module_variable.
  Proof with eauto 10 with liblayers.
    intros M1 M2 HM.
    unfold ptree_module_variable.
    solve_monotonic.
  Qed.
End PTREE_MODULE_QUERY.

Instance of Modules

A work around for code extraction. The extracted OCaml code is not polymorphic enough if these two are not declared at top level as functions.

Local Instance ptree_module_le F V: Le (ptree_module F V) :=
  {
    le := ptree_rel (option_le (res_le eq)) × ptree_rel (option_le (res_le eq))
  }.

Local Instance ptree_module_empty F V: Emptyset (ptree_module F V) :=
  {
    emptyset := (@PTree.empty _, @PTree.empty _)
  }.

Local Instance ptree_module_oplus {F V}: Oplus (ptree_module F V) :=
  {
    oplus M1 M2 := oplus (Oplus := prod_oplus) M1 M2
  }.

Local Instance ptree_module_ops {F V}: ModuleOps ident F V (ptree_module F V) :=
  {
    module_mapsto_fundef := {| mapsto i κ := (i ↦ OK κ, @PTree.empty _) |};
    module_mapsto_vardef := {| mapsto i τ := (@PTree.empty _, i ↦ OK τ) |};
    get_module_function := ptree_module_function;
    get_module_variable := ptree_module_variable
  }.
Proof.
 × intros.
   unfold ptree_module_function.
   refine (_
             (ptree_forall_decision_strong
                (fun i def ⇒ P (option_res_flip (Some def)))
                (P (OK None))
                _ _ (fst L))).
   apply decide_rewrite.
   split.
   + intros J i.
     generalize (J i).
     destruct ((fst L) ! i); simpl; monad_norm; auto.
   + intros J i.
     generalize (J i).
     destruct ((fst L) ! i); simpl; monad_norm; auto.
 × intros P DP M.
   refine (_
             (ptree_forall_decision
                (fun i _ ⇒ ptree_module_function i M = OK None ∨ P i)
                _ (fst M))).
   + apply decide_rewrite.
     unfold ptree_module_function.
     unfold ptree_forall.
     split.
     - intros J i.
       destruct ((fst M) ! i) eqn:HM; try (compute; congruence).
       rewrite <- HM.
       intro.
       destruct (J _ _ HM); try contradiction.
       assumption.
     - intros.
       destruct (decide (option_res_flip (fst M) ! i = OK None)); auto.
   + intros; typeclasses eauto.
 × intros.
   unfold ptree_module_variable.
   refine (_
             (ptree_forall_decision_strong
                (fun _ def ⇒ P (option_res_flip (Some def)))
                (P (OK None))
                _ _ (snd L))).
   apply decide_rewrite.
   split.
   + intros J i.
     generalize (J i).
     destruct ((snd L) ! i); simpl; monad_norm; auto.
   + intros J i.
     generalize (J i).
     destruct ((snd L) ! i); simpl; monad_norm; auto.
 × intros P DP M.
   refine (_
             (ptree_forall_decision
                (fun i _ ⇒ ptree_module_variable i M = OK None ∨ P i)
                _ (snd M))).
   + apply decide_rewrite.
     unfold ptree_module_variable.
     unfold ptree_forall.
     split.
     - intros J i.
       destruct ((snd M) ! i) eqn:HM; try (compute; congruence).
       rewrite <- HM.
       intro.
       destruct (J _ _ HM); try contradiction.
       assumption.
     - intros.
       destruct (decide (option_res_flip (snd M) ! i = OK None)); auto.
   + intros; typeclasses eauto.
Defined.

Now to prove the assoiated properties.

Local Existing Instance ptree_le_op.
Local Existing Instance option_le_op.
Local Existing Instance res_le_op.
Local Hint Extern 10 (Le _) ⇒ eapply trivial_le : typeclass_instances.

Local Instance: ∀ F V, PseudoJoin (ptree_module F V) (∅, ∅).
Proof.
  intros.
  change (@ptree_module_oplus F V)
    with (@prod_oplus (PTree.t (res F)) _ (PTree.t (res V)) _).
  change (@ptree_module_le F V)
    with (@prod_le_op (PTree.t (res F)) _ (PTree.t (res V)) _).
  eapply @prod_pjoin.
  × apply ptree_pseudojoin.
    + reflexivity.
    + typeclasses eauto.
  × apply ptree_pseudojoin.
    + reflexivity.
    + typeclasses eauto.
Qed.

Local Instance ptree_module_prf {F V}: Modules ident F V (ptree_module F V) :=
  {
    get_module_function_mapsto := ptree_module_function_mapsto;
    get_module_variable_mapsto := ptree_module_variable_mapsto
  }.
Proof.
  × intros i.
    simpl; unfold ptree_module_function; simpl.
    rewrite PTree.gempty; simpl.
    reflexivity.
  × intros i j κ Hij.
    simpl; unfold ptree_module_function; simpl.
    rewrite PTree.gso by assumption; simpl.
    rewrite PTree.gempty; simpl.
    reflexivity.
  × intros i j τ.
    simpl; unfold ptree_module_function; simpl.
    rewrite PTree.gempty.
    reflexivity.

  × intros i [M1f M1v] [M2f M2v].
    simpl; unfold ptree_module_function; simpl.
    rewrite PTree.gcombine by reflexivity.
    destruct (M1f ! i) as [[σ1|]|];
    destruct (M2f ! i) as [[σ2|]|];
    simpl;
    monad_norm;
    simpl;
    solve_monotonic.

  × intros i.
    simpl; unfold ptree_module_variable; simpl.
    rewrite PTree.gempty; simpl.
    reflexivity.
  × intros i j κ Hij.
    simpl; unfold ptree_module_variable; simpl.
    rewrite PTree.gso by assumption; simpl.
    rewrite PTree.gempty; simpl.
    reflexivity.
  × intros i j τ.
    simpl; unfold ptree_module_variable; simpl.
    rewrite PTree.gempty; simpl.
    reflexivity.

  × intros i [M1f M1v] [M2f M2v].
    simpl; unfold ptree_module_variable; simpl.
    rewrite PTree.gcombine by reflexivity.
    destruct (M1v ! i) as [[τ1|]|];
    destruct (M2v ! i) as [[τ2|]|];
    simpl;
    monad_norm;
    simpl;
    solve_monotonic.
Qed.

Global Opaque ptree_module.
Global Opaque ptree_module_ops.