Module TaggedExprPath

From Stdlib Require Import Lists.List.

From Verilog Require Import TaggedExpr.
From Verilog Require Export Path.
From Verilog Require Import Utils.

Import ListNotations.

Import TaggedExpr.
Import Path.
Import Utils.

# TaggedExprPath Module This module is the tagged analogue of `ExprPath`. It defines path validity and subexpression lookup for annotated expression trees (`TaggedExpr`), together with the same core correctness lemmas.

Module TaggedExprPath.

`IsTypedPath e p` states that `p` is a valid navigation path in the tagged expression `e`. Constructors follow the expression shape exactly, while preserving tag values at each visited node.

`sub_typed_expr e p` computes the tagged subexpression reached by `p`. It returns `None` precisely when the path does not match the tree shape.

  Fixpoint sub_typed_expr {T: Type} (e: TaggedExpr T) (p: path) :=
    match e, p with
    | e, [] => Some e
    | TExpr (TBinOp lhs _) _, 0 :: p => sub_typed_expr lhs p
    | TExpr (TBinOp _ rhs) _, 1 :: p => sub_typed_expr rhs p
    | TExpr (TUnOp arg) _, 0 :: p => sub_typed_expr arg p
    | TExpr (TComp lhs _) _, 0 :: p => sub_typed_expr lhs p
    | TExpr (TComp _ rhs) _, 1 :: p => sub_typed_expr rhs p
    | TExpr (TLogic lhs _) _, 0 :: p => sub_typed_expr lhs p
    | TExpr (TLogic _ rhs) _, 1 :: p => sub_typed_expr rhs p
    | TExpr (TReduction arg) _, 0 :: p => sub_typed_expr arg p
    | TExpr (TShift lhs _) _, 0 :: p => sub_typed_expr lhs p
    | TExpr (TShift _ rhs) _, 1 :: p => sub_typed_expr rhs p
    | TExpr (TAssign _ arg) _, 0 :: p => sub_typed_expr arg p
    | TExpr (TCond cond _ _) _, 0 :: p => sub_typed_expr cond p
    | TExpr (TCond _ tb _) _, 1 :: p => sub_typed_expr tb p
    | TExpr (TCond _ _ fb) _, 2 :: p => sub_typed_expr fb p
    | TExpr (TConcat args) _, i :: p =>
        match nth_error args i with
        | Some e => sub_typed_expr e p
        | None => None
        end
    | TExpr (TRepl _ arg) _, 0 :: p => sub_typed_expr arg p
    | TExpr _ _, _ :: _ => None
    end
  .

Notation for tagged subexpression lookup.

Notation "e @@[ p ]" := (sub_typed_expr e p) (at level 1).

Empty-path lookup returns the full expression.

Lemma sub_typed_expr_nil: forall T (e: TaggedExpr T), e @@[[]] = Some e.

Proof.

intros. destruct e as [[]]; reflexivity.
Qed.

Valid paths are always realizable as successful lookups.

Lemma IsTypedPath_is_sub_typed_expr: forall T (e: TaggedExpr T) p,
IsTypedPath e p -> exists e0, e @@[p] = Some e0.

Proof.

    intros. induction H; try (destruct IHIsTypedPath as [x H1]; exists x; assumption).
    - exists e. apply sub_typed_expr_nil.
    - destruct IHIsTypedPath as [x H1]; exists x. simpl. rewrite H. assumption.
  Qed.

Successful lookups always induce valid typed paths.

Lemma sub_typed_expr_valid: forall T (e: TaggedExpr T) p f,
e @@[p] = Some f -> IsTypedPath e p.

Proof.

    induction e using TaggedExpr_ind; intros;
      try (destruct p as [|[|[|[]]]]; simpl in *;
           (constructor; firstorder) || congruence).
    - destruct p.
      + constructor.
      + destruct (nth_error args n) eqn:H1; simpl in H0; rewrite H1 in H0.
        * apply (TP_ConcatArgs _ _ _ _ _ H1 (H _ _ H1 _ _ H0)).
        * congruence.
  Qed.

Path validity is equivalent to lookup success.

Lemma IsTypedPath_sub_typed_expr_iff:
forall T (e: TaggedExpr T) p, IsTypedPath e p <-> exists e0, e @@[p] = Some e0.

Proof.

    split.
    - apply IsTypedPath_is_sub_typed_expr.
    - intros [? H]. apply (sub_typed_expr_valid _ _ _ _ H).
  Qed.

Subexpression lookup composes over path concatenation. This is the tagged analogue of `ExprPath.sub_expr_chunk`.

Lemma sub_typed_expr_chunk : forall T p q (e: TaggedExpr T) g,
(exists f, e @@[p] = Some f /\ f @@[q] = Some g) <-> e @@[p ++ q] = Some g.

Proof.

    induction p; split; intros.
    - destruct H as [f [H1 H2]]. rewrite sub_typed_expr_nil in H1. inv H1. assumption.
    - exists e. split. apply sub_typed_expr_nil. assumption.
    - destruct H as [f [H1 H2]]. destruct e as [[]]; simpl in *;
        try congruence; try (destruct (nth_error _ a)); destruct a as [|[|[]]];
        congruence || (apply IHp; eexists; intuition; eassumption).
    - destruct e as [[]]; simpl in *;
        try congruence; try (destruct (nth_error _ a));
        destruct a as [|[|[]]]; congruence || apply IHp; assumption.
  Qed.

Path validity also composes over path concatenation. A path `p ++ c` is valid in `e` iff `p` reaches some intermediate node `f` and `c` is valid inside `f`.

Lemma IsTypedPath_chunk : forall T (e: TaggedExpr T) p c,
IsTypedPath e (p ++ c) <-> (exists f, e @@[p] = Some f /\ IsTypedPath f c).

Proof.

    split; intros.
    - destruct (IsTypedPath_is_sub_typed_expr _ _ _ H) as [g H1].
      apply sub_typed_expr_chunk in H1.
      destruct H1 as [f [H2 H3]]. exists f. split. assumption.
      apply IsTypedPath_sub_typed_expr_iff.
      exists g. assumption.
    - destruct H as [f [H1 H2]]. apply IsTypedPath_sub_typed_expr_iff.
      apply IsTypedPath_sub_typed_expr_iff in H2. destruct H2 as [g H2]. exists g.
      apply sub_typed_expr_chunk. exists f. intuition.
  Qed.

Decidability of typed paths.

Theorem IsTypedPath_dec : forall T (e: TaggedExpr T) p,
{IsTypedPath e p} + {~(IsTypedPath e p)}.

Proof.

    intros. destruct (e @@[p]) eqn:Hep.
    - left. apply (sub_typed_expr_valid _ _ _ _ Hep).
    - right. unfold not. intros. rewrite IsTypedPath_sub_typed_expr_iff in H. destruct H.
      congruence.
  Qed.

End TaggedExprPath.

Files

Module TaggedExprPath