module Palmse.Monoid.Nbe (A : Set) where

import Palmse.Monoid.Exp
open Palmse.Monoid.Exp A

[[_]] : Exp -> Exp -> Exp
[[ id ]]     e'' = e''
[[ e ○ e' ]] e'' = [[ e ]] ([[ e' ]] e'')
[[ at x ]]   e'' = at x ○ e''

reify : (Exp -> Exp) -> Exp
reify f = f id 

nbe : Exp -> Exp
nbe e = reify [[ e ]]