Qcert.NNRC.Core.cNNRCShadow

Section cNNRCShadow.





  Context {fruntime:foreign_runtime}.

  Fixpoint nnrc_bound_vars (e:nnrc) : list var :=
    match e with
    | NNRCVar x ⇒ nil
    | NNRCConst d ⇒ nil
    | NNRCBinop bop e1 e2 ⇒ nnrc_bound_vars e1 ++ nnrc_bound_vars e2
    | NNRCUnop uop e1 ⇒ nnrc_bound_vars e1
    | NNRCLet x e1 e2 ⇒ x :: (nnrc_bound_vars e1 ++ nnrc_bound_vars e2)
    | NNRCFor x e1 e2 ⇒ x :: (nnrc_bound_vars e1 ++ nnrc_bound_vars e2)
    | NNRCIf e1 e2 e3 ⇒ nnrc_bound_vars e1 ++ nnrc_bound_vars e2 ++ nnrc_bound_vars e3
    | NNRCEither ed xl el xr er ⇒ xl :: xr :: nnrc_bound_vars ed ++ nnrc_bound_vars el++ nnrc_bound_vars er
    | NNRCGroupBy g s e ⇒ nnrc_bound_vars e
    end.

  Fixpoint nnrc_free_vars (e:nnrc) : list var :=
    match e with
    | NNRCVar x ⇒ x :: nil
    | NNRCConst d ⇒ nil
    | NNRCBinop bop e1 e2 ⇒ nnrc_free_vars e1 ++ nnrc_free_vars e2
    | NNRCUnop uop e1 ⇒ nnrc_free_vars e1
    | NNRCLet x e1 e2 ⇒ (nnrc_free_vars e1 ++ remove string_eqdec x (nnrc_free_vars e2))
    | NNRCFor x e1 e2 ⇒ (nnrc_free_vars e1 ++ remove string_eqdec x (nnrc_free_vars e2))
    | NNRCIf e1 e2 e3 ⇒ nnrc_free_vars e1 ++ nnrc_free_vars e2 ++ nnrc_free_vars e3
    | NNRCEither ed xl el xr er ⇒ nnrc_free_vars ed ++ (remove string_eqdec xl (nnrc_free_vars el)) ++ (remove string_eqdec xr (nnrc_free_vars er))
    | NNRCGroupBy g sl e ⇒ nnrc_free_vars e
    end.


  Fixpoint nnrc_subst (e:nnrc) (x:var) (e':nnrc) : nnrc
    := match e with
       | NNRCVar y ⇒ if y == x then e' else NNRCVar y
       | NNRCConst d ⇒ NNRCConst d
       | NNRCBinop bop e1 e2 ⇒ NNRCBinop bop
                                        (nnrc_subst e1 x e')
                                        (nnrc_subst e2 x e')
       | NNRCUnop uop e1 ⇒ NNRCUnop uop (nnrc_subst e1 x e')
       | NNRCLet y e1 e2 ⇒
         NNRCLet y
                (nnrc_subst e1 x e')
                (if y == x then e2 else nnrc_subst e2 x e')
       | NNRCFor y e1 e2 ⇒
         NNRCFor y
                (nnrc_subst e1 x e')
                (if y == x then e2 else nnrc_subst e2 x e')
       | NNRCIf e1 e2 e3 ⇒ NNRCIf
                              (nnrc_subst e1 x e')
                              (nnrc_subst e2 x e')
                              (nnrc_subst e3 x e')
       | NNRCEither ed xl el xr er ⇒
         NNRCEither (nnrc_subst ed x e')
                   xl
                   (if xl == x then el else nnrc_subst el x e')
                   xr
                   (if xr == x then er else nnrc_subst er x e')
       | NNRCGroupBy g sl e1 ⇒ NNRCGroupBy g sl (nnrc_subst e1 x e')
       end.

  Lemma nnrc_subst_not_free e x :
    ¬ In x (nnrc_free_vars e) →
    ∀ e', nnrc_subst e x e' = e.

  Lemma nnrc_subst_remove_one_free e x e' :
    nnrc_free_vars e' = nil →
    nnrc_free_vars (nnrc_subst e x e') = remove string_eqdec x (nnrc_free_vars e).

  Lemma nnrc_subst_not_in_free e x e':
    nnrc_free_vars e' = nil →
    ∀ y,
      In y (nnrc_free_vars (nnrc_subst e x e')) → x ≠ y.

  Lemma nnrc_subst_remove_free e x e':
    nnrc_free_vars e' = nil →
    ∀ y,
      In y (nnrc_free_vars (nnrc_subst e x e')) → In y (nnrc_free_vars e).

  Definition really_fresh_in (sep:string) (oldvar:var) (avoid:list var) (e:nnrc)
    := fresh_var_from
         sep
         oldvar
         (avoid ++ nnrc_free_vars e ++ nnrc_bound_vars e).

  Lemma really_fresh_in_fresh (sep:string) (oldvar:var) (avoid:list var) (e:nnrc) :
    ¬ In (really_fresh_in sep oldvar avoid e)
         (avoid ++ nnrc_free_vars e ++ nnrc_bound_vars e).

  Lemma really_fresh_from_avoid sep old avoid (e:nnrc) :
    ¬ In (really_fresh_in sep old avoid e) avoid.

  Lemma really_fresh_from_free sep old avoid (e:nnrc) :
    ¬ In (really_fresh_in sep old avoid e) (nnrc_free_vars e).

  Lemma really_fresh_from_bound sep old avoid (e:nnrc) :
    ¬ In (really_fresh_in sep old avoid e) (nnrc_bound_vars e).


  Fixpoint shadow_free (e:nnrc) : bool :=
    match e with
    | NNRCVar x ⇒ true
    | NNRCConst d ⇒ true
    | NNRCBinop bop e1 e2 ⇒ shadow_free e1 && shadow_free e2
    | NNRCUnop uop e1 ⇒ shadow_free e1
    | NNRCLet x e1 e2 ⇒
      (if in_dec string_eqdec x (nnrc_bound_vars e2) then false else true)
        && shadow_free e1 && shadow_free e2
    | NNRCFor x e1 e2 ⇒
      (if in_dec string_eqdec x (nnrc_bound_vars e2) then false else true)
        && shadow_free e1 && shadow_free e2
    | NNRCIf e1 e2 e3 ⇒ shadow_free e1 && shadow_free e2 && shadow_free e3
    | NNRCEither ed xl el xr er ⇒
      (if in_dec string_eqdec xl (nnrc_bound_vars el) then false else true)
        && (if in_dec string_eqdec xr (nnrc_bound_vars er) then false else true)
        && shadow_free ed && shadow_free el && shadow_free er
    | NNRCGroupBy g sl e1 ⇒ shadow_free e1
    end.

  Definition pick_new_really_fresh_in (sep:string) (name:var) (avoid:list var) (e:nnrc)
    := if in_dec string_eqdec name (avoid ++ (nnrc_free_vars e) ++ (nnrc_bound_vars e))
       then really_fresh_in sep name avoid e
       else name.

  Definition pick_same_really_fresh_in (sep:string) (name:var) (avoid:list var) (e:nnrc)
    := if in_dec string_eqdec name (avoid ++ (nnrc_bound_vars e))
       then really_fresh_in sep name avoid e
       else name.

  Section unsh.
    Definition nnrc_rename_lazy (e:nnrc) (oldvar newvar:var)
      := if oldvar == newvar
         then e
         else (nnrc_subst e oldvar (NNRCVar newvar)).

    Context (sep:string).
    Context (renamer:string→string).
    Context (avoid:list var).

    Definition nnrc_pick_name (oldvar:var) (e:nnrc)
      := let name := renamer oldvar in
         if name == oldvar
         then pick_same_really_fresh_in sep name avoid e
         else pick_new_really_fresh_in sep name avoid e.

  Fixpoint unshadow (e:nnrc) : nnrc
    :=
      match e with
      | NNRCVar x ⇒ NNRCVar x
      | NNRCConst d ⇒ NNRCConst d
      | NNRCBinop bop e1 e2 ⇒ NNRCBinop bop (unshadow e1) (unshadow e2)
      | NNRCUnop uop e1 ⇒ NNRCUnop uop (unshadow e1)
      | NNRCLet x e1 e2 ⇒
        let e1' := unshadow e1 in
        let e2' := unshadow e2 in
        let x' := nnrc_pick_name x e2' in
        NNRCLet x' e1' (nnrc_rename_lazy e2' x x')
      | NNRCFor x e1 e2 ⇒
        let e1' := unshadow e1 in
        let e2' := unshadow e2 in
        let x' := nnrc_pick_name x e2' in
        NNRCFor x' e1' (nnrc_rename_lazy e2' x x')
      | NNRCIf e1 e2 e3 ⇒ NNRCIf (unshadow e1) (unshadow e2) (unshadow e3)
      | NNRCEither ed xl el xr er ⇒
        let ed' := unshadow ed in
        let el' := unshadow el in
        let er' := unshadow er in
        let xl' := nnrc_pick_name xl el' in
        let xr' := nnrc_pick_name xr er' in
        NNRCEither ed' xl' (nnrc_rename_lazy el' xl xl') xr' (nnrc_rename_lazy er' xr xr')
      | NNRCGroupBy g sl e1 ⇒ NNRCGroupBy g sl (unshadow e1)
      end.

  Lemma nnrc_bound_vars_subst_preserved e x e' :
    nnrc_bound_vars e' = nil →
    nnrc_bound_vars (nnrc_subst e x e') = nnrc_bound_vars e.

  Lemma no_bound_shadow_free e :
    nnrc_bound_vars e = nil → shadow_free e = true.

  Lemma nnrc_shadow_free_subst_preserved e x e' :
    nnrc_bound_vars e' = nil →
    shadow_free (nnrc_subst e x e') = shadow_free e.

  Lemma nnrc_shadow_free_rename_nnrc_pick_name_preserved e v :
    shadow_free (nnrc_rename_lazy e v (nnrc_pick_name v e)) = shadow_free e.

  Lemma nnrc_bound_vars_rename_lazy_preserved e oldvar newvar :
    nnrc_bound_vars (nnrc_rename_lazy e oldvar newvar) = nnrc_bound_vars e.

  Lemma nnrc_pick_name_avoid old (e:nnrc) :
    ¬ In (nnrc_pick_name old e) avoid.

  Lemma nnrc_pick_name_bound old (e:nnrc) :
    ¬ In (nnrc_pick_name old e) (nnrc_bound_vars e).

  Lemma unshadow_shadow_free (e:nnrc) :
    shadow_free (unshadow e) = true.

  Lemma unshadow_avoid (e:nnrc) x :
    In x avoid → ¬ In x (nnrc_bound_vars (unshadow e)).

  Lemma nnrc_free_vars_subst e v n: ¬ In n (nnrc_bound_vars e) →
    nnrc_free_vars ((nnrc_subst e v (NNRCVar n))) =
    replace_all (nnrc_free_vars e) v n.

  Lemma nnrc_subst_eq e v : nnrc_subst e v (NNRCVar v) = e.

  Lemma nnrc_pick_name_remove_free v e :
  remove string_eqdec (nnrc_pick_name v e)
     (nnrc_free_vars (nnrc_rename_lazy e v (nnrc_pick_name v e))) =
   remove string_eqdec v (nnrc_free_vars e).

  Lemma unshadow_nnrc_free_vars (e:nnrc) :
    nnrc_free_vars (unshadow e) = nnrc_free_vars e.

  End unsh.

  Lemma nnrc_core_eval_remove_duplicate_env {h:brand_relation_t} l v x l' x' l'' e :
    nnrc_core_eval h (l ++ (v,x)::l' ++ (v,x')::l'') e =
    nnrc_core_eval h (l ++ (v,x)::l' ++ l'') e.

  Lemma nnrc_core_eval_remove_duplicate_env_weak {h:list (string×string)} v1 v2 x x' x'' l e :
    nnrc_core_eval h ((v1,x)::(v2,x')::(v1,x'')::l) e =
    nnrc_core_eval h ((v1,x)::(v2,x')::l) e.

  Lemma nnrc_core_eval_remove_duplicate_env_weak_cons {h:list (string×string)} v1 v2 x x' x'' l e :
    nnrc_core_eval h ((v1,x)::(v2,x')::(v2,x'')::l) e =
    nnrc_core_eval h ((v1,x)::(v2,x')::l) e.

  Lemma nnrc_core_eval_remove_free_env {h:list (string×string)} l v x l' e :
          ¬ In v (nnrc_free_vars e) →
          nnrc_core_eval h (l ++ (v,x)::l') e = nnrc_core_eval h (l ++ l') e.

  Lemma nnrc_core_eval_remove_free_env_weak {h:list (string×string)} v1 x1 v x e :
    ¬ In v (nnrc_free_vars e) →
    nnrc_core_eval h ((v1,x1)::(v,x)::nil) e = nnrc_core_eval h ((v1,x1)::nil) e.

  Lemma nnrc_core_eval_swap_neq {h:list (string×string)} l1 v1 x1 v2 x2 l2 e : v1 ≠ v2 →
           nnrc_core_eval h (l1++(v1,x1)::(v2,x2)::l2) e =
           nnrc_core_eval h (l1++(v2,x2)::(v1,x1)::l2) e.

  Lemma nnrc_core_eval_subst_dunit {h:list (string×string)} env e v :
    nnrc_core_eval h ((v,dunit)::env) e = nnrc_core_eval h env (nnrc_subst e v (NNRCConst dunit)).

  Lemma nnrc_core_eval_cons_subst {h:list (string×string)} e env v x v' :
    ¬ (In v' (nnrc_free_vars e)) →
    ¬ (In v' (nnrc_bound_vars e)) →
    nnrc_core_eval h ((v',x)::env) (nnrc_subst e v (NNRCVar v')) =
    nnrc_core_eval h ((v,x)::env) e.

  Lemma nnrc_core_eval_equiv_free_in_env:
    ∀ n,
    ∀ env1 env2,
      (∀ x, In x (nnrc_free_vars n) → lookup equiv_dec env1 x = lookup equiv_dec env2 x) →
      ∀ h,
        nnrc_core_eval h env1 n = nnrc_core_eval h env2 n.

  Lemma nnrc_core_eval_equiv_env:
    ∀ n,
    ∀ env1 env2,
      (∀ x, lookup equiv_dec env1 x = lookup equiv_dec env2 x) →
      ∀ h,
        nnrc_core_eval h env1 n = nnrc_core_eval h env2 n.

  Lemma nnrc_no_free_vars_eval_equiv_env:
    ∀ n,
    ∀ env1 env2,
      nnrc_free_vars n = nil →
      ∀ h,
        nnrc_core_eval h env1 n = nnrc_core_eval h env2 n.

  Lemma nnrc_core_eval_single_context_var_uncons h env n v d:
    lookup equiv_dec env v = Some d →
    nnrc_core_eval h env n = nnrc_core_eval h ((v, d) :: env) n.

  Lemma nnrc_core_eval_single_context_var h env n v d:
    (∀ x, In x (nnrc_free_vars n) → x = v) →
    lookup equiv_dec env v = Some d →
    nnrc_core_eval h ((v, d) :: nil) n = nnrc_core_eval h env n.

  Lemma nnrc_core_eval_single_context_var_cons h env n v d:
    (∀ x, In x (nnrc_free_vars n) → x = v) →
    nnrc_core_eval h ((v, d) :: nil) n = nnrc_core_eval h ((v,d)::env) n.

  Lemma nnrc_core_eval_single_context_var_cons_keepone h env n v d v1 d1:
    (∀ x, In x (nnrc_free_vars n) → x = v) →
    nnrc_core_eval h ((v, d) :: (v1, d1) :: nil) n = nnrc_core_eval h ((v,d) :: (v1,d1) :: env) n.

  Lemma nnrc_core_eval_single_context_var_two_cons h env n v1 d1 v2 d2 :
    (∀ x, In x (nnrc_free_vars n) → x = v1 ∨ x = v2) →
    nnrc_core_eval h ((v1,d1) :: (v2,d2) :: nil) n = nnrc_core_eval h ((v1,d1) :: (v2,d2) :: env) n.

  Lemma nnrc_core_eval_single_context_var_cons_rmap h env n v l:
    (∀ x, In x (nnrc_free_vars n) → x = v) →
    rmap (fun d ⇒ nnrc_core_eval h ((v, d) :: nil) n) l =
    rmap (fun d ⇒ nnrc_core_eval h ((v,d)::env) n) l.

  Lemma nnrc_core_eval_single_context_var_cons_keepone_rmap h env n v v1 d1 l:
    (∀ x, In x (nnrc_free_vars n) → x = v) →
    rmap (fun d ⇒ nnrc_core_eval h ((v, d) :: (v1,d1) :: nil) n) l =
    rmap (fun d ⇒ nnrc_core_eval h ((v,d) :: (v1,d1) :: env) n) l.

  Lemma rmap_skip_free_var h v1 v2 d2 n l:
    ¬ In v2 (nnrc_free_vars n) →
    (rmap (fun d : data ⇒ nnrc_core_eval h ((v1, d) :: (v2, d2) :: nil) n) l) =
    (rmap (fun d : data ⇒ nnrc_core_eval h ((v1, d) :: nil) n) l).

  Lemma nnrc_core_eval_cons_subst_disjoint {h: list (string×string)} e e' env v d :
    disjoint (nnrc_bound_vars e) (nnrc_free_vars e') →
         nnrc_core_eval h env e' = Some d →
         nnrc_core_eval h ((v,d)::env) e = nnrc_core_eval h env (nnrc_subst e v e').

  Lemma nnrc_pick_name_neq_nfree sep renamer avoid v e :
    v =/= nnrc_pick_name sep renamer avoid v e →
    ¬ In (nnrc_pick_name sep renamer avoid v e) (nnrc_free_vars e).

  Lemma nnrc_core_eval_cons_rename_pick h sep renamer avoid v e d env:
    nnrc_core_eval h ((nnrc_pick_name sep renamer avoid v e, d) :: env)
             (nnrc_rename_lazy e v (nnrc_pick_name sep renamer avoid v e)) =
    nnrc_core_eval h ((v, d) :: env) e.

  Theorem unshadow_eval {h:list (string×string)} sep renamer avoid e env :
    nnrc_core_eval h env (unshadow sep renamer avoid e) = nnrc_core_eval h env e.

  Lemma nnrc_pick_name_id_nin_eq sep avoid v e :
    ¬ In v (nnrc_bound_vars e) →
    ¬ In v avoid →
    (nnrc_pick_name sep id avoid v e) = v.

  Lemma nnrc_rename_lazy_eq e v :
    nnrc_rename_lazy e v v = e.

  Lemma shadow_free_unshadow_id sep avoid (e:nnrc) :
    shadow_free e = true →
    (∀ x, In x avoid → ¬In x (nnrc_bound_vars e)) →
    unshadow sep id avoid e = e.

  Lemma unshadow_id_idempotent sep renamer1 avoid (e:nnrc)
    : unshadow sep id avoid (unshadow sep renamer1 avoid e) = unshadow sep renamer1 avoid e.

  Definition nnrc_unshadow_sep := "$"%string.
  Definition unshadow_simpl := unshadow nnrc_unshadow_sep id.

  Definition nnrc_substlist_subst (substlist:list (var×var)) (e:nnrc) :=
    List.fold_left
      (fun e (subst: var × var) ⇒
         let (x, x') := subst in
         nnrc_subst e x (NNRCVar x'))
      substlist e.

  Section core.
    Lemma nnrc_subst_preserve_core n1 n2 v1 :
      nnrcIsCore n1 → nnrcIsCore n2 → nnrcIsCore (nnrc_subst n1 v1 n2).

    Lemma nnrc_rename_lazy_preserve_core n v1 v2 :
      nnrcIsCore n → nnrcIsCore (nnrc_rename_lazy n v1 v2).

    Lemma unshadow_simpl_preserve_core avoid n :
      nnrcIsCore n → nnrcIsCore (unshadow_simpl avoid n).

    Lemma unshadow_preserve_core sep renamer avoid n :
      nnrcIsCore n → nnrcIsCore (unshadow sep renamer avoid n).

  End core.
End cNNRCShadow.