Library CoqWorkshop.NotationsMITPresentation

Require Import Coq.ZArith.BinInt.
Inductive type := Z | prod (A B : type) | arrow (s d : type).
Inductive expr {var:type → Type} : type → Type :=
| LetIn {s d} (x : expr s) (f : var s → expr d) : expr d
| App {s d} (f : expr (arrow s d)) (x : expr s) : expr d
| Abs {s d} (f : var s → expr d) : expr (arrow s d)
| Var {t} (v : var t) : expr t
| Pair {A B} (x : expr A) (y : expr B) : expr (prod A B)
| Fst {A B} (x : expr (prod A B)) : expr A
| Snd {A B} (x : expr (prod A B)) : expr B
| Add (x y : expr Z) : expr Z
| Mul (x y : expr Z) : expr Z
| Sub (x y : expr Z) : expr Z
| Opp (x : expr Z) : expr Z
| Literal (v : BinInt.Z) : expr Z
| AddWithGetCarry (x y c : expr Z) : expr (prod Z Z)
| CastToSize (lower upper : BinInt.Z) (v : expr Z) : expr Z.

Delimit Scope etype_scope with etype.
Delimit Scope expr_scope with expr.
Bind Scope etype_scope with type.
Bind Scope expr_scope with expr.
Infix "×" := prod : etype_scope.
Infix "×" := Mul : expr_scope.
Infix "→" := arrow : etype_scope.
Infix "-" := Sub : expr_scope.
Infix "+" := Add : expr_scope.

Check (_ + _ × _ - _)%expr.
Notation "- x" := (Opp x) : expr_scope.
Print Grammar constr.
Notation "# x" := (Literal x) (at level 10, format "# x") : expr_scope.
Open Scope expr_scope.
Check fun x ⇒ #(Z.succ x).
Notation "$ x" := (Var x) (at level 10, format "$ x") : expr_scope.
Check #1 + #1.
Notation "'expr_let' x := y 'in' f"
  := (LetIn y (fun x ⇒ f%expr))
       (at level 200, right associativity,
        format "'[' 'expr_let' x := y 'in' '//' f ']'") : expr_scope.
Check (expr_let x := #1 in expr_let y := $x + #2 in $y + $x).

Module MorePretty.
  Notation "x" := (Literal x) (only printing, at level 10) : expr_scope.
  Notation "x" := (Var x) (only printing, at level 10) : expr_scope.
  Notation "T x = y ; f"
    := (LetIn (s:=T) y (fun x ⇒ f%expr))
         (only printing, at level 200, right associativity,
          format "'[' T x = y ; '//' f ']'") : expr_scope.
  Notation int := Z.
  Fail Notation "T x = y ; .. ; T' x' = y' ;; 'return' f"
    := (LetIn (s:=T) y (fun x ⇒ .. (LetIn (s:=T') y' (fun x' ⇒ f%expr)) .. ))
         (only printing, at level 200, right associativity) : expr_scope.
  Check (expr_let x := #1 in expr_let y := $x + #2 in $y + $x).
End MorePretty.

Notation "( x , y , .. , z )" := (Pair .. (Pair x y) .. z) : expr_scope.
Print Grammar constr.
Notation "\ x .. y , f"
  := (Abs (fun x ⇒ .. (Abs (fun y ⇒ f%expr)) .. ))
       (at level 99, x binder, y binder, right associativity, f at level 200) : expr_scope.