From mininix Require Export nix.operational.

(* Influenced by
https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris_heap_lang/notation.v
But always uses ":" instead of a scope. *)

Coercion EId' : string >-> expr.
Coercion NInt : Z >-> num.
Coercion NFloat : float >-> num.
Coercion LitNum : num >-> base_lit.
Coercion LitBool : bool >-> base_lit.
Coercion ELit : base_lit >-> expr.
Coercion EApp : expr >-> Funclass.

Notation "λattr: a , e" := (EAbsMatch a true e)
  (at level 200, e, a at level 200,
   format "'[' 'λattr:'  a  ,  '/  ' e ']'").
Notation "λattr: a .., e" := (EAbsMatch a false e)
  (at level 200, e, a at level 200,
   format "'[' 'λattr:'  a  ..,  '/  ' e ']'").

Notation "λ: x .. y , e" := (EAbs x .. (EAbs y e) ..)
  (at level 200, x, y at level 1, e at level 200,
   format "'[' 'λ:'  x  ..  y ,  '/  ' e ']'").
Notation "'let:' x := e1 'in' e2" := (ELet x e1 e2)
  (at level 200, x at level 1, e1, e2 at level 200,
   format "'[' 'let:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'").
Notation "'with:' a 'in' e" := (EWith a e)
  (at level 200, a, e at level 200,
   format "'[' 'with:'  a  'in'  '/' e ']'").

Notation "'if:' e1 'then' e2 'else' e3" := (EIf e1 e2 e3)
  (at level 200, e1, e2, e3 at level 200).

Notation "e1 .: e2" := (ESelect e1 e2) (at level 70, no associativity).

Notation "e1 +: e2" := (EBinOp AddOp e1 e2) (at level 50, left associativity).
Notation "e1 *: e2" := (EBinOp MulOp e1 e2).
Notation "e1 -: e2" := (EBinOp SubOp e1 e2) (at level 50, left associativity).
Notation "e1 /: e2" := (EBinOp DivOp e1 e2) (at level 40).
Notation "e1 =: e2" := (EBinOp EqOp e1 e2) (at level 70, no associativity).
Notation "e1 <: e2" := (EBinOp LtOp e1 e2) (at level 70, no associativity).
Notation "'ceil:' e" := (EBinOp (RoundOp Ceil) e LitNull) (at level 10).