Lvc.ShadowingFree

Require Import CSet Le.

Require Import Plus Util AllInRel Map.
Require Import Val Var Env EnvTy IL Annotation Liveness Restrict Bisim MoreExp SetOperations.
Require Import DecSolve RenamedApart LabelsDefined.

Set Implicit Arguments.

Inductive shadowing_free : set var → stmt → Prop :=
  | shadowing_freeExp x e s D
    : x ∉ D
      → Exp.freeVars e ⊆ D
      → shadowing_free {x; D} s
      → shadowing_free D (stmtLet x e s)
  | shadowing_freeIf D e s t
    : Exp.freeVars e ⊆ D
    → shadowing_free D s
    → shadowing_free D t
    → shadowing_free D (stmtIf e s t)
  | shadowing_freeRet D e
    : Exp.freeVars e ⊆ D
    → shadowing_free D (stmtReturn e)
  | shadowing_freeGoto D f Y
    : list_union (List.map Exp.freeVars Y) ⊆ D
    → shadowing_free D (stmtApp f Y)
  | shadowing_freeExtern x f Y s D
    : x ∉ D
      → list_union (List.map Exp.freeVars Y) ⊆ D
      → shadowing_free {x; D} s
      → shadowing_free D (stmtExtern x f Y s)
  | shadowing_freeLet D s t Z
    : of_list Z ∩ D [=] ∅
    → shadowing_free (of_list Z ∪ D) s
    → shadowing_free D t
    → shadowing_free D (stmtFun Z s t).

Lemma shadowing_free_ext s D D´
  : D´ [=] D
  → shadowing_free D s
  → shadowing_free D´ s.

Instance shadowing_free_morphism
: Proper (Equal ==> eq ==> iff) shadowing_free.

Lemma renamedApart_shadowing_free s an
  : renamedApart s an → shadowing_free (fst (getAnn an)) s.