Module cNRAEnvContext

Section cNRAEnvContext.

  Require Import Equivalence.
  Require Import Morphisms.
  Require Import Setoid.
  Require Import EquivDec.
  Require Import Program.

  Require Import List Permutation.
  Require Import String.
  Require Import NPeano.
  Require Import Arith Bool.

  Require Import Utils BasicRuntime.
  Require Import cNRAEnv cNRAEnvEq.
  Require Import RBindingsNat.

  Local Open Scope nraenv_core_scope.

  Context {fruntime:foreign_runtime}.

  Inductive nraenv_core_ctxt : Set :=
  | CNHole : nat -> nraenv_core_ctxt
  | CNPlug : nraenv_core -> nraenv_core_ctxt
  | CANBinop : binOp -> nraenv_core_ctxt -> nraenv_core_ctxt -> nraenv_core_ctxt
  | CANUnop : unaryOp -> nraenv_core_ctxt -> nraenv_core_ctxt
  | CANMap : nraenv_core_ctxt -> nraenv_core_ctxt -> nraenv_core_ctxt
  | CANMapConcat : nraenv_core_ctxt -> nraenv_core_ctxt -> nraenv_core_ctxt
  | CANProduct : nraenv_core_ctxt -> nraenv_core_ctxt -> nraenv_core_ctxt
  | CANSelect : nraenv_core_ctxt -> nraenv_core_ctxt -> nraenv_core_ctxt
  | CANDefault : nraenv_core_ctxt -> nraenv_core_ctxt -> nraenv_core_ctxt
  | CANEither : nraenv_core_ctxt -> nraenv_core_ctxt -> nraenv_core_ctxt
  | CANEitherConcat : nraenv_core_ctxt -> nraenv_core_ctxt -> nraenv_core_ctxt
  | CANApp : nraenv_core_ctxt -> nraenv_core_ctxt -> nraenv_core_ctxt
  | CANAppEnv : nraenv_core_ctxt -> nraenv_core_ctxt -> nraenv_core_ctxt
  | CANMapEnv : nraenv_core_ctxt -> nraenv_core_ctxt
  .

  Definition CANID : nraenv_core_ctxt
    := CNPlug ANID.

    Definition CANEnv : nraenv_core_ctxt
    := CNPlug ANEnv.

    Definition CANGetConstant s : nraenv_core_ctxt
    := CNPlug (ANGetConstant s).

  Definition CANConst : data -> nraenv_core_ctxt
    := fun d => CNPlug (ANConst d).

  Fixpoint aec_holes (c:nraenv_core_ctxt) : list nat :=
    match c with
      | CNHole x => x::nil
      | CNPlug a => nil
      | CANBinop b c1 c2 => aec_holes c1 ++ aec_holes c2
      | CANUnop u c' => aec_holes c'
      | CANMap c1 c2 => aec_holes c1 ++ aec_holes c2
      | CANMapConcat c1 c2 => aec_holes c1 ++ aec_holes c2
      | CANProduct c1 c2 => aec_holes c1 ++ aec_holes c2
      | CANSelect c1 c2 => aec_holes c1 ++ aec_holes c2
      | CANDefault c1 c2 => aec_holes c1 ++ aec_holes c2
      | CANEither c1 c2 => aec_holes c1 ++ aec_holes c2
      | CANEitherConcat c1 c2 => aec_holes c1 ++ aec_holes c2
      | CANApp c1 c2 => aec_holes c1 ++ aec_holes c2
      | CANAppEnv c1 c2 => aec_holes c1 ++ aec_holes c2
      | CANMapEnv c1 => aec_holes c1
    end.

  Fixpoint aec_simplify (c:nraenv_core_ctxt) : nraenv_core_ctxt :=
    match c with
      | CNHole x => CNHole x
      | CNPlug a => CNPlug a
      | CANBinop b c1 c2 =>
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) => CNPlug (ANBinop b a1 a2)
          | c1', c2' => CANBinop b c1' c2'
        end
      | CANUnop u c =>
        match aec_simplify c with
          | CNPlug a => CNPlug (ANUnop u a)
          | c' => CANUnop u c'
        end
      | CANMap c1 c2 =>
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) => CNPlug (ANMap a1 a2)
          | c1', c2' => CANMap c1' c2'
        end
      | CANMapConcat c1 c2 =>
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) => CNPlug (ANMapConcat a1 a2)
          | c1', c2' => CANMapConcat c1' c2'
        end
      | CANProduct c1 c2 =>
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) => CNPlug (ANProduct a1 a2)
          | c1', c2' => CANProduct c1' c2'
        end
      | CANSelect c1 c2 =>
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) => CNPlug (ANSelect a1 a2)
          | c1', c2' => CANSelect c1' c2'
        end
      | CANDefault c1 c2 =>
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) => CNPlug (ANDefault a1 a2)
          | c1', c2' => CANDefault c1' c2'
        end
      | CANEither c1 c2 =>
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) => CNPlug (ANEither a1 a2)
          | c1', c2' => CANEither c1' c2'
        end
      | CANEitherConcat c1 c2 =>
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) => CNPlug (ANEitherConcat a1 a2)
          | c1', c2' => CANEitherConcat c1' c2'
        end
      | CANApp c1 c2 =>
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) => CNPlug (ANApp a1 a2)
          | c1', c2' => CANApp c1' c2'
        end
      | CANAppEnv c1 c2 =>
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) => CNPlug (ANAppEnv a1 a2)
          | c1', c2' => CANAppEnv c1' c2'
        end
      | CANMapEnv c1 =>
        match aec_simplify c1 with
          | (CNPlug a1) => CNPlug (ANMapEnv a1)
          | c1' => CANMapEnv c1'
        end
    end.

  Lemma aec_simplify_holes_preserved c :
    aec_holes (aec_simplify c) = aec_holes c.

  Definition aec_nraenv_core_of_ctxt c
    := match (aec_simplify c) with
         | CNPlug a => Some a
         | _ => None
       end.

  Lemma aec_simplify_nholes c :
    aec_holes c = nil -> {a | aec_simplify c = CNPlug a}.

  Lemma aec_nraenv_core_of_ctxt_nholes c :
    aec_holes c = nil -> {a | aec_nraenv_core_of_ctxt c = Some a}.

  Lemma aec_simplify_idempotent c :
    aec_simplify (aec_simplify c) = aec_simplify c.

  Fixpoint aec_subst (c:nraenv_core_ctxt) (x:nat) (p:nraenv_core) : nraenv_core_ctxt :=
    match c with
      | CNHole x'
        => if x == x' then CNPlug p else CNHole x'
      | CNPlug a
        => CNPlug a
      | CANBinop b c1 c2
        => CANBinop b (aec_subst c1 x p) (aec_subst c2 x p)
      | CANUnop u c
        => CANUnop u (aec_subst c x p)
      | CANMap c1 c2
        => CANMap (aec_subst c1 x p) (aec_subst c2 x p)
      | CANMapConcat c1 c2
        => CANMapConcat (aec_subst c1 x p) (aec_subst c2 x p)
      | CANProduct c1 c2
        => CANProduct (aec_subst c1 x p) (aec_subst c2 x p)
      | CANSelect c1 c2
        => CANSelect (aec_subst c1 x p) (aec_subst c2 x p)
      | CANDefault c1 c2
        => CANDefault (aec_subst c1 x p) (aec_subst c2 x p)
      | CANEither c1 c2
        => CANEither (aec_subst c1 x p) (aec_subst c2 x p)
      | CANEitherConcat c1 c2
        => CANEitherConcat (aec_subst c1 x p) (aec_subst c2 x p)
      | CANApp c1 c2
        => CANApp (aec_subst c1 x p) (aec_subst c2 x p)
      | CANAppEnv c1 c2
        => CANAppEnv (aec_subst c1 x p) (aec_subst c2 x p)
      | CANMapEnv c1
        => CANMapEnv (aec_subst c1 x p)
    end.

  Definition aec_substp (c:nraenv_core_ctxt) xp
    := let '(x, p) := xp in aec_subst c x p.
    
  Definition aec_substs c ps :=
    fold_left aec_substp ps c.

  
   Lemma aec_substs_app c ps1 ps2 :
     aec_substs c (ps1 ++ ps2) =
     aec_substs (aec_substs c ps1) ps2.

  Lemma aec_subst_holes_nin c x p :
    ~ In x (aec_holes c) -> aec_subst c x p = c.

  Lemma aec_subst_holes_remove c x p :
    aec_holes (aec_subst c x p) = remove_all x (aec_holes c).

    Lemma aec_substp_holes_remove c xp :
      aec_holes (aec_substp c xp) = remove_all (fst xp) (aec_holes c).

 Lemma aec_substs_holes_remove c ps :
    aec_holes (aec_substs c ps) =
    fold_left (fun h xy => remove_all (fst xy) h) ps (aec_holes c).
  
  Lemma aec_substs_Plug a ps :
    aec_substs (CNPlug a) ps = CNPlug a.
  
  Lemma aec_substs_Binop b c1 c2 ps :
    aec_substs (CANBinop b c1 c2) ps = CANBinop b (aec_substs c1 ps) (aec_substs c2 ps).

  Lemma aec_substs_Unop u c ps :
      aec_substs (CANUnop u c) ps = CANUnop u (aec_substs c ps).

  Lemma aec_substs_Map c1 c2 ps :
    aec_substs ( CANMap c1 c2) ps =
    CANMap (aec_substs c1 ps) (aec_substs c2 ps).

  Lemma aec_substs_MapConcat c1 c2 ps :
    aec_substs ( CANMapConcat c1 c2) ps =
    CANMapConcat (aec_substs c1 ps) (aec_substs c2 ps).
  
  Lemma aec_substs_Product c1 c2 ps :
    aec_substs ( CANProduct c1 c2) ps =
    CANProduct (aec_substs c1 ps) (aec_substs c2 ps).
  
  Lemma aec_substs_Select c1 c2 ps :
    aec_substs ( CANSelect c1 c2) ps =
    CANSelect (aec_substs c1 ps) (aec_substs c2 ps).
  
  Lemma aec_substs_Default c1 c2 ps :
    aec_substs ( CANDefault c1 c2) ps =
    CANDefault (aec_substs c1 ps) (aec_substs c2 ps).
  
  Lemma aec_substs_Either c1 c2 ps :
    aec_substs ( CANEither c1 c2) ps =
    CANEither (aec_substs c1 ps) (aec_substs c2 ps).
  
  Lemma aec_substs_EitherConcat c1 c2 ps :
    aec_substs ( CANEitherConcat c1 c2) ps =
    CANEitherConcat (aec_substs c1 ps) (aec_substs c2 ps).
  
  Lemma aec_substs_App c1 c2 ps :
    aec_substs ( CANApp c1 c2) ps =
    CANApp (aec_substs c1 ps) (aec_substs c2 ps).
  
  Lemma aec_substs_AppEnv c1 c2 ps :
    aec_substs ( CANAppEnv c1 c2) ps =
    CANAppEnv (aec_substs c1 ps) (aec_substs c2 ps).
  
  Lemma aec_substs_MapEnv c1 ps :
    aec_substs ( CANMapEnv c1) ps =
    CANMapEnv (aec_substs c1 ps).

    Hint Rewrite
       aec_substs_Plug
       aec_substs_Binop
       aec_substs_Unop
       aec_substs_Map
       aec_substs_MapConcat
       aec_substs_Product
       aec_substs_Select
       aec_substs_Default
       aec_substs_Either
       aec_substs_EitherConcat
       aec_substs_App
       aec_substs_AppEnv
       aec_substs_MapEnv : aec_substs.
  
  Lemma aec_simplify_holes_binop b c1 c2:
    aec_holes (CANBinop b c1 c2) <> nil ->
    aec_simplify (CANBinop b c1 c2) = CANBinop b (aec_simplify c1) (aec_simplify c2).

  Lemma aec_simplify_holes_unop u c:
    aec_holes (CANUnop u c ) <> nil ->
    aec_simplify (CANUnop u c) = CANUnop u (aec_simplify c).

  Lemma aec_simplify_holes_map c1 c2:
    aec_holes (CANMap c1 c2) <> nil ->
    aec_simplify (CANMap c1 c2) = CANMap (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_mapconcat c1 c2:
    aec_holes (CANMapConcat c1 c2) <> nil ->
    aec_simplify (CANMapConcat c1 c2) = CANMapConcat (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_product c1 c2:
    aec_holes (CANProduct c1 c2) <> nil ->
    aec_simplify (CANProduct c1 c2) = CANProduct (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_select c1 c2:
    aec_holes (CANSelect c1 c2) <> nil ->
    aec_simplify (CANSelect c1 c2) = CANSelect (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_default c1 c2:
    aec_holes (CANDefault c1 c2) <> nil ->
    aec_simplify (CANDefault c1 c2) = CANDefault (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_either c1 c2:
    aec_holes (CANEither c1 c2) <> nil ->
    aec_simplify (CANEither c1 c2) = CANEither (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_eitherconcat c1 c2:
    aec_holes (CANEitherConcat c1 c2) <> nil ->
    aec_simplify (CANEitherConcat c1 c2) = CANEitherConcat (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_app c1 c2:
    aec_holes (CANApp c1 c2) <> nil ->
    aec_simplify (CANApp c1 c2) = CANApp (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_appenv c1 c2:
    aec_holes (CANAppEnv c1 c2) <> nil ->
    aec_simplify (CANAppEnv c1 c2) = CANAppEnv (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_mapenv c1 :
    aec_holes (CANMapEnv c1) <> nil ->
    aec_simplify (CANMapEnv c1) = CANMapEnv (aec_simplify c1).

   Lemma aec_subst_nholes c x p :
     (aec_holes c) = nil -> aec_subst c x p = c.

   Lemma aec_subst_simplify_nholes c x p :
     (aec_holes c) = nil ->
     aec_subst (aec_simplify c) x p = aec_simplify c.

  Lemma aec_simplify_subst_simplify1 c x p :
    aec_simplify (aec_subst (aec_simplify c) x p) =
    aec_simplify (aec_subst c x p).

  Lemma aec_simplify_substs_simplify1 c ps :
    aec_simplify (aec_substs (aec_simplify c) ps) =
    aec_simplify (aec_substs c ps).

    Section equivs.
    Context (base_equiv:nraenv_core->nraenv_core->Prop).

    Definition nraenv_core_ctxt_equiv (c1 c2 : nraenv_core_ctxt)
      := forall (ps:list (nat * nraenv_core)),
           match aec_simplify (aec_substs c1 ps),
                 aec_simplify (aec_substs c2 ps)
           with
             | CNPlug a1, CNPlug a2 => base_equiv a1 a2
             | _, _ => True
           end.

   Definition nraenv_core_ctxt_equiv_strict (c1 c2 : nraenv_core_ctxt)
     := forall (ps:list (nat * nraenv_core)),
          is_list_sorted lt_dec (domain ps) = true ->
          equivlist (domain ps) (aec_holes c1 ++ aec_holes c2) ->
          match aec_simplify (aec_substs c1 ps),
                aec_simplify (aec_substs c2 ps)
          with
            | CNPlug a1, CNPlug a2 => base_equiv a1 a2
            | _, _ => True
          end.

   Global Instance aec_simplify_proper :
     Proper (nraenv_core_ctxt_equiv ==> nraenv_core_ctxt_equiv) aec_simplify.
  
  Lemma aec_simplify_proper_inv x y:
    nraenv_core_ctxt_equiv (aec_simplify x) (aec_simplify y) -> nraenv_core_ctxt_equiv x y.

 Instance aec_subst_proper_part1 :
   Proper (nraenv_core_ctxt_equiv ==> eq ==> eq ==> nraenv_core_ctxt_equiv) aec_subst.

  Global Instance aec_substs_proper_part1: Proper (nraenv_core_ctxt_equiv ==> eq ==> nraenv_core_ctxt_equiv) aec_substs.

  Definition nraenv_core_ctxt_equiv_strict1 (c1 c2 : nraenv_core_ctxt)
     := forall (ps:list (nat * nraenv_core)),
          NoDup (domain ps) ->
          equivlist (domain ps) (aec_holes c1 ++ aec_holes c2) ->
          match aec_simplify (aec_substs c1 ps),
                aec_simplify (aec_substs c2 ps)
          with
            | CNPlug a1, CNPlug a2 => base_equiv a1 a2
            | _, _ => True
          end.

   Lemma aec_subst_swap_neq c x1 x2 y1 y2 :
     x1 <> x2 ->
   aec_subst (aec_subst c x1 y1) x2 y2 =
   aec_subst (aec_subst c x2 y2) x1 y1.
   
   Lemma aec_subst_swap_eq c x1 y1 y2 :
     aec_subst (aec_subst c x1 y1) x1 y2 =
     aec_subst c x1 y1.
           
   Lemma aec_substs_subst_swap_simpl x c y ps :
     ~ In x (domain ps) ->
      aec_substs (aec_subst c x y) ps
      =
      (aec_subst (aec_substs c ps) x y).
   
   Lemma aec_substs_perm c ps1 ps2 :
     NoDup (domain ps1) ->
     Permutation ps1 ps2 ->
     (aec_substs c ps1) =
     (aec_substs c ps2).
       
   Lemma nraenv_core_ctxt_equiv_strict_equiv1 (c1 c2 : nraenv_core_ctxt) :
     nraenv_core_ctxt_equiv_strict1 c1 c2 <-> nraenv_core_ctxt_equiv_strict c1 c2.

   Definition nraenv_core_ctxt_equiv_strict2 (c1 c2 : nraenv_core_ctxt)
     := forall (ps:list (nat * nraenv_core)),
          equivlist (domain ps) (aec_holes c1 ++ aec_holes c2) ->
          match aec_simplify (aec_substs c1 ps),
                aec_simplify (aec_substs c2 ps)
          with
            | CNPlug a1, CNPlug a2 => base_equiv a1 a2
            | _, _ => True
          end.

   Lemma aec_substs_in_nholes c x ps :
         In x (domain ps) ->
      ~ In x (aec_holes (aec_substs c ps)).
    
   Lemma substs_bdistinct_domain_rev c ps :
    (aec_substs c (bdistinct_domain (rev ps)))
    =
    (aec_substs c ps).
  
   Lemma nraenv_core_ctxt_equiv_strict1_equiv2 (c1 c2 : nraenv_core_ctxt) :
     nraenv_core_ctxt_equiv_strict2 c1 c2 <-> nraenv_core_ctxt_equiv_strict1 c1 c2.

   Definition nraenv_core_ctxt_equiv_strict3 (c1 c2 : nraenv_core_ctxt)
     := forall (ps:list (nat * nraenv_core)),
          incl (aec_holes c1 ++ aec_holes c2) (domain ps) ->
          match aec_simplify (aec_substs c1 ps),
                aec_simplify (aec_substs c2 ps)
          with
            | CNPlug a1, CNPlug a2 => base_equiv a1 a2
            | _, _ => True
          end.
   
   Lemma cut_down_to_substs c ps cut :
     incl (aec_holes c) cut ->
     (aec_substs c ps) = (aec_substs c (cut_down_to ps cut)).
         
   Lemma nraenv_core_ctxt_equiv_strict2_equiv3 (c1 c2 : nraenv_core_ctxt) :
     nraenv_core_ctxt_equiv_strict3 c1 c2 <-> nraenv_core_ctxt_equiv_strict2 c1 c2.

   Lemma nraenv_core_ctxt_equiv_strict3_equiv (c1 c2 : nraenv_core_ctxt) :
     nraenv_core_ctxt_equiv c1 c2 <-> nraenv_core_ctxt_equiv_strict3 c1 c2.

   Theorem nraenv_core_ctxt_equiv_strict_equiv (c1 c2 : nraenv_core_ctxt) :
     nraenv_core_ctxt_equiv c1 c2 <-> nraenv_core_ctxt_equiv_strict c1 c2.

   Lemma aec_holes_saturated_subst {B} f c ps :
      incl (aec_holes c) (domain ps) ->
      aec_holes
        (aec_substs c
                   (map (fun xy : nat * B => (fst xy, (f (snd xy)))) ps)) = nil.

  Global Instance nraenv_core_ctxt_equiv_refl {refl:Reflexive base_equiv}: Reflexive nraenv_core_ctxt_equiv.

  Global Instance nraenv_core_ctxt_equiv_sym {sym:Symmetric base_equiv}: Symmetric nraenv_core_ctxt_equiv.

  Global Instance nraenv_core_ctxt_equiv_trans {trans:Transitive base_equiv}: Transitive nraenv_core_ctxt_equiv.

  Global Instance nraenv_core_ctxt_equiv_equivalence {equiv:Equivalence base_equiv}: Equivalence nraenv_core_ctxt_equiv.

  Global Instance nraenv_core_ctxt_equiv_preorder {pre:PreOrder base_equiv} : PreOrder nraenv_core_ctxt_equiv.

  Global Instance nraenv_core_ctxt_equiv_strict_refl {refl:Reflexive base_equiv}: Reflexive nraenv_core_ctxt_equiv_strict.

  Global Instance nraenv_core_ctxt_equiv_strict_sym {sym:Symmetric base_equiv}: Symmetric nraenv_core_ctxt_equiv_strict.

  Global Instance nraenv_core_ctxt_equiv_strict_trans {trans:Transitive base_equiv}: Transitive nraenv_core_ctxt_equiv_strict.
  
  Global Instance nraenv_core_ctxt_equiv_strict_equivalence {equiv:Equivalence base_equiv}: Equivalence nraenv_core_ctxt_equiv_strict.

  Global Instance nraenv_core_ctxt_equiv_strict_preorder {pre:PreOrder base_equiv} : PreOrder nraenv_core_ctxt_equiv_strict.

  Global Instance CNPlug_proper :
    Proper (base_equiv ==> nraenv_core_ctxt_equiv) CNPlug.

  Global Instance CNPlug_proper_strict :
    Proper (base_equiv ==> nraenv_core_ctxt_equiv_strict) CNPlug.

  End equivs.
  
End cNRAEnvContext.


Delimit Scope nraenv_core_ctxt_scope with nraenv_core_ctxt.

Notation "'ID'" := (CANID) (at level 50) : nraenv_core_ctxt_scope.
Notation "'ENV'" := (CANEnv) (at level 50) : nraenv_core_ctxt_scope.

Notation "‵‵ c" := (CANConst (dconst c)) (at level 0) : nraenv_core_ctxt_scope.
Notation "‵ c" := (CANConst c) (at level 0) : nraenv_core_ctxt_scope.
Notation "‵{||}" := (CANConst (dcoll nil)) (at level 0) : nraenv_core_ctxt_scope.
Notation "‵[||]" := (CANConst (drec nil)) (at level 50) : nraenv_core_ctxt_scope.

Notation "r1 ∧ r2" := (CANBinop AAnd r1 r2) (right associativity, at level 65): nraenv_core_ctxt_scope.
Notation "r1 ∨ r2" := (CANBinop AOr r1 r2) (right associativity, at level 70): nraenv_core_ctxt_scope.
Notation "r1 ≐ r2" := (CANBinop AEq r1 r2) (right associativity, at level 70): nraenv_core_ctxt_scope.
Notation "r1 ≤ r2" := (CANBinop ALt r1 r2) (no associativity, at level 70): nraenv_core_ctxt_scope.
Notation "r1 ⋃ r2" := (CANBinop AUnion r1 r2) (right associativity, at level 70): nraenv_core_ctxt_scope.
Notation "r1 − r2" := (CANBinop AMinus r1 r2) (right associativity, at level 70): nraenv_core_ctxt_scope.
Notation "r1 ♯min r2" := (CANBinop AMin r1 r2) (right associativity, at level 70): nraenv_core_ctxt_scope.
Notation "r1 ♯max r2" := (CANBinop AMax r1 r2) (right associativity, at level 70): nraenv_core_ctxt_scope.
Notation "p ⊕ r" := ((CANBinop AConcat) p r) (at level 70) : nraenv_core_ctxt_scope.
Notation "p ⊗ r" := ((CANBinop AMergeConcat) p r) (at level 70) : nraenv_core_ctxt_scope.

Notation "¬( r1 )" := (CANUnop ANeg r1) (right associativity, at level 70): nraenv_core_ctxt_scope.
Notation "ε( r1 )" := (CANUnop ADistinct r1) (right associativity, at level 70): nraenv_core_ctxt_scope.
Notation "♯count( r1 )" := (CANUnop ACount r1) (right associativity, at level 70): nraenv_core_ctxt_scope.
Notation "♯flatten( d )" := (CANUnop AFlatten d) (at level 50) : nraenv_core_ctxt_scope.
Notation "‵{| d |}" := ((CANUnop AColl) d) (at level 50) : nraenv_core_ctxt_scope.
Notation "‵[| ( s , r ) |]" := ((CANUnop (ARec s)) r) (at level 50) : nraenv_core_ctxt_scope.
Notation "¬π[ s1 ]( r )" := ((CANUnop (ARecRemove s1)) r) (at level 50) : nraenv_core_ctxt_scope.
Notation "p · r" := ((CANUnop (ADot r)) p) (left associativity, at level 40): nraenv_core_ctxt_scope.

Notation "χ⟨ p ⟩( r )" := (CANMap p r) (at level 70) : nraenv_core_ctxt_scope.
Notation "⋈ᵈ⟨ e2 ⟩( e1 )" := (CANMapConcat e2 e1) (at level 70) : nraenv_core_ctxt_scope.
Notation "r1 × r2" := (CANProduct r1 r2) (right associativity, at level 70): nraenv_core_ctxt_scope.
Notation "σ⟨ p ⟩( r )" := (CANSelect p r) (at level 70) : nraenv_core_ctxt_scope.
Notation "r1 ∥ r2" := (CANDefault r1 r2) (right associativity, at level 70): nraenv_core_ctxt_scope.
Notation "r1 ◯ r2" := (CANApp r1 r2) (right associativity, at level 60): nraenv_core_ctxt_scope.

Notation "r1 ◯ₑ r2" := (CANAppEnv r1 r2) (right associativity, at level 60): nraenv_core_ctxt_scope.

Notation "χᵉ⟨ p ⟩( r )" := (CANMapEnv p r) (at level 70) : nraenv_core_ctxt_scope.

Notation "$ n" := (CNHole n) (at level 50) : nraenv_core_ctxt_scope.

Notation "X ≡ₑ Y" := (nraenv_core_ctxt_equiv nraenv_core_eq X Y) (at level 90) : nraenv_core_ctxt_scope.

  Hint Rewrite
       @aec_substs_Plug
       @aec_substs_Binop
       @aec_substs_Unop
       @aec_substs_Map
       @aec_substs_MapConcat
       @aec_substs_Product
       @aec_substs_Select
       @aec_substs_Default
       @aec_substs_Either
       @aec_substs_EitherConcat
       @aec_substs_App
       @aec_substs_AppEnv
       @aec_substs_MapEnv : aec_substs.