```(**************************************************************************
* Proving functional programs through a deep embedding                    *
* Pretty-printer for the embedded language                                *
***************************************************************************)

Set Implicit Arguments.
Require Export LibCore DeepSyntax.

(** This file describes pretty-printing rules for deeply-embedded
- Variables (type [var]) and constructors are described using
notations for binary numbers (the use of strings is not
possible due to significant inefficiencies in their handling).
- Boolean and integer constants from Coq can be used directly,
thanks to the use of coercions (explained further).

The most important pieces of notation are listed below.
Language constructs:
- [\ v] describes the value [v] lifted in the syntax of terms.
The symbol [\] is usually hidden (it stands for a coercion),
and used only to resolve ambiguities.
- [t1 ' t2] the application of [t1] onto [t2],
- ['fun p1 .. pN '-> t] for the N-ary function with input
patterns [pi] and body [t],
- ['let p '= t1 'in t2] for a let-expression binding a
pattern [p] to [t1] into [t2],
- ['let f p1 .. pN '= t1 in t2] defines and binds a function,
- ['let 'rec f p1 .. pN '= t1 in t2] defines and binds
a recursive function,
- ['match t 'with '| p1 '-> t1 .. '| pN '-> tN] for
pattern-matching on a value [t],
- ['function '| p1 '-> t1 .. '| pN '-> tN] defines a function
by pattern matching on [N] clauses,
- ['try t 'catch 'h] for evaluating [t] with the exception
handler [h],
- ['try t 'with '| p1 '-> t1 .. '| pN '-> tN] for evaluating
[t] with an exception-handler defined by pattern matching.
- ['throw t] for raising exceptions.
Language values:
- ['x] a notation for variable [x].
- [#(t1,..,tN)] describes a tuple,
- [C#(t1,..,tN)] describes an n-ary data constructor,
- ['exn C] describes an exception built on constructor [C],
- ['exn C#(t1,..,tN)] describes an exception built on a,
N-ary constructor [C],
- ['\[\]] stands for the empty list,
- [t1 ':: t2] describes list consing.
Language patterns: in addition to data constructors, we have:
- ['_] for the wildcard pattern,
- [p 'as x] for introducing an alias during pattern matching.

To distinguish between values represented as terms and
values represented as values, two technique are used.
The printing scope [()%val] is used for data constructors,
e.g. [#(v1,v2)] stands for a term while [(#(v1,v2))%val]
stands for a value. For functions, an upper case keyword
is used: ['fun 'x '-> 'x] stands for a term while
['Fun 'x '-> 'x] stands for a value.

*)

(************************************************************)
(* ** Coercions. *)

(** Coercions are functions that are automatically inserted
when they help resolving a typing conflict. For instance,
if a term (type [trm]) is expected but a value
(type [val]) is found, then the constructor [trm_val]
will be automatically added in front of the value. *)

Coercion trm_val : val >-> trm.
Coercion trm_var : var >-> trm.
Coercion pat_var : var >-> pat.
Coercion val_int : int >-> val.
Coercion val_nat (x:nat) := val_int (x:int).
Coercion _Bool : bool >-> val.
Coercion _Unit : unit >-> val.

(************************************************************)
(* ** Scope declaration (technicalities) *)

Definition newscope := True.
Notation "'__trm_scope_init__'" := newscope : trm_scope.
Notation "'__val_scope_init__'" := newscope : val_scope.
Notation "'__pat_scope_init__'" := newscope : pat_scope.

Open Scope pat_scope.
Open Scope val_scope.
Open Scope trm_scope.

Delimit Scope trm_scope with trm.
Delimit Scope val_scope with val.
Delimit Scope pat_scope with pat.

Bind Scope trm_scope with trm.
Bind Scope val_scope with val.
Bind Scope pat_scope with pat.

Open Scope var_scope.
Delimit Scope var_scope with var.
Bind Scope var_scope with var.

(************************************************************)
(* ** Hints for parsing (technicalities) *)

Arguments Scope trm_val [ val_scope ].
Arguments Scope trm_exn [ val_scope ].
Arguments Scope trm_app [ trm_scope trm_scope ].
Arguments Scope trm_try [ trm_scope trm_scope ].
Arguments Scope trm_fix [ var_scope pat_scope trm_scope trm_scope ].
Arguments Scope val_fix [ var_scope pat_scope trm_scope trm_scope ].
Arguments Scope trm_con [ _ trm_scope ].
Arguments Scope val_con [ _ val_scope ].
Arguments Scope pat_con [ _ pat_scope ].
Arguments Scope pat_con [ var_scope pat_scope ].
Arguments Scope pat_var [ var_scope ].
Arguments Scope trm_var [ var_scope ].

(************************************************************)
(* ** Notations for values, application, and exceptions *)

Notation "'\' v" := (trm_val v)
(at level 28) : trm_scope.
Notation "t1 ' t2" := (trm_app t1 t2)
(at level 29, left associativity) : trm_scope.

Notation "'exn' v" := (trm_exn v)
(at level 29) : trm_scope.
Notation "'Exn' c" := (exn (val_con c nil))
(at level 29) : trm_scope.

Notation "''raise'" := (\ val_builtin builtin_throw)
(at level 0) : trm_scope.
Notation "''throw' t" := ('raise ' t)
(at level 29) : trm_scope.
Notation "''Throw' c" := ('throw (Exn c))
(at level 29) : trm_scope.
Notation "''crash'" := ('Throw con_match_failure)
(at level 0) : trm_scope.
Notation "''fail'" := ('Throw con_user_failure)
(at level 0) : trm_scope.

(************************************************************)
(* ** Notations for n-ary constructors *)

Notation "c '#'" := (pat_con c nil)
(at level 27, format "c #") : pat_scope.
Notation "c '#' '(' x1 ')'" := (pat_con c ((x1%pat)::(@nil pat)))
(at level 27, format "c # ( x1 )") : pat_scope.
Notation "c '#' '(' x1 ',' x2 ')'" := (pat_con c ((x1%pat)::(x2%pat)::(@nil pat)))
(at level 27, format "c # ( x1 ,  x2 )") : pat_scope.
Notation "c '#' '(' x1 ',' x2 ',' x3 ')'" := (pat_con c ((x1%pat)::(x2%pat)::(x3%pat)::(@nil pat)))
(at level 27, format "c # ( x1 ,  x2  , x3 )") : pat_scope.

Notation "c '#'" := (trm_con c nil)
(at level 27, format "c #") : trm_scope.
Notation "c '#' '(' x1 ')'" := (trm_con c ((x1%trm)::(@nil trm)))
(at level 27, format "c # ( x1 )") : trm_scope.
Notation "c '#' '(' x1 ',' x2 ')'" := (trm_con c ((x1%trm)::(x2%trm)::(@nil trm)))
(at level 27, format "c # ( x1 ,  x2 )") : trm_scope.
Notation "c '#' '(' x1 ',' x2 ',' x3 ')'" := (trm_con c ((x1%trm)::(x2%trm)::(x3%trm)::(@nil trm)))
(at level 27, format "c # ( x1 ,  x2  , x3 )") : trm_scope.

Notation "c '#'" := (val_con c nil)
(at level 27, format "c #").
Notation "c '#' '(' x1 ')'" := (val_con c ((x1%val)::(@nil val)))
(at level 27, format "c # ( x1 )") : val_scope.
Notation "c '#' '(' x1 ',' x2 ')'" := (val_con c ((x1%val)::(x2%val)::(@nil val)))
(at level 27, format "c # ( x1 ,  x2 )") : val_scope.
Notation "c '#' '(' x1 ',' x2 ',' x3 ')'" := (val_con c ((x1%val)::(x2%val)::(x3%val)::(@nil val)))
(at level 27, format "c # ( x1 ,  x2  , x3 )") : val_scope.

Notation "c '##' vs '++' t '++' ts" :=
(trm_con c ((LibList.map trm_val vs) ++ t::ts))
(at level 28, vs at level 0, t at level 0, ts at level 0,
format "c '##' vs '++' t '++' ts") : trm_scope.

(************************************************************)
(* ** Notations for n-ary tuples *)

Notation "'pat_tuple' xs" := (pat_con con_tuple xs)
(at level 29, only parsing) : pat_scope.
Notation "'trm_tuple' xs" := (trm_con con_tuple xs)
(at level 29, only parsing) : trm_scope.
Notation "'val_tuple' xs" := (val_con con_tuple xs)
(at level 29, only parsing) : val_scope.

Notation "'#'" := (pat_tuple nil)
(at level 28) : pat_scope.
Notation "'#' '(' x1 ')'" := (pat_tuple ((x1%pat)::(@nil pat)))
(at level 28, format "# '(' x1 ')'") : pat_scope.
Notation "'#' '(' x1 ',' x2 ')'" := (pat_tuple ((x1%pat)::(x2%pat)::(@nil pat)))
(at level 28, format "# ( x1 ,  x2 )") : pat_scope.
Notation "'#' '(' x1 ',' x2 ',' x3 ')'" := (pat_tuple ((x1%pat)::(x2%pat)::(x3%pat)::(@nil pat)))
(at level 28, format "# ( x1 ,  x2 ,  x3 )") : pat_scope.

Notation "'#'" := (trm_tuple nil)
(at level 28) : trm_scope.
Notation "'#' '(' x1 ')'" := (trm_tuple ((x1%trm)::(@nil trm)))
(at level 28, format "# '(' x1 ')'") : trm_scope.
Notation "'#' '(' x1 ',' x2 ')'" := (trm_tuple ((x1%trm)::(x2%trm)::(@nil trm)))
(at level 28, format "# ( x1 ,  x2 )") : trm_scope.
Notation "'#' '(' x1 ',' x2 ',' x3 ')'" := (trm_tuple ((x1%trm)::(x2%trm)::(x3%trm)::(@nil trm)))
(at level 28, format "# ( x1 ,  x2 ,  x3 )") : trm_scope.

Notation "'#'" := (val_tuple nil)
(at level 28) : val_scope.
Notation "'#' '(' x1 ')'" := (val_tuple ((x1%val)::(@nil val)))
(at level 28, format "# '(' x1 ')'") : val_scope.
Notation "'#' '(' x1 ',' x2 ')'" := (val_tuple ((x1%val)::(x2%val)::(@nil val)))
(at level 28, format "# ( x1 ,  x2 )") : val_scope.
Notation "'#' '(' x1 ',' x2 ',' x3 ')'" := (val_tuple ((x1%val)::(x2%val)::(x3%val)::(@nil val)))
(at level 28, format "# ( x1 ,  x2 ,  x3 )") : val_scope.

(************************************************************)
(* ** Notations for n-ary constructors *)

Notation "c '#'" := (pat_con c nil)
(at level 27, format "c #") : pat_scope.
Notation "c '#' '(' x1 ')'" := (pat_con c ((x1:pat)::nil))
(at level 27, format "c # ( x1 )") : pat_scope.
Notation "c '#' '(' x1 ',' x2 ')'" := (pat_con c ((x1:pat)::(x2:pat)::nil))
(at level 27, format "c # ( x1 ,  x2 )") : pat_scope.
Notation "c '#' '(' x1 ',' x2 ',' x3 ')'" := (pat_con c ((x1:pat)::(x2:pat)::(x3:pat)::nil))
(at level 27, format "c # ( x1 ,  x2  , x3 )") : pat_scope.

Notation "c '#'" := (trm_con c nil)
(at level 27, format "c #") : trm_scope.
Notation "c '#' '(' x1 ')'" := (trm_con c ((x1:trm)::nil))
(at level 27, format "c # ( x1 )") : trm_scope.
Notation "c '#' '(' x1 ',' x2 ')'" := (trm_con c ((x1:trm)::(x2:trm)::nil))
(at level 27, format "c # ( x1 ,  x2 )") : trm_scope.
Notation "c '#' '(' x1 ',' x2 ',' x3 ')'" := (trm_con c ((x1:trm)::(x2:trm)::(x3:trm)::nil))
(at level 27, format "c # ( x1 ,  x2  , x3 )") : trm_scope.

Notation "c '#'" := (val_con c nil)
(at level 27, format "c #") : val_scope.
Notation "c '#' '(' x1 ')'" := (val_con c ((x1:val)::nil))
(at level 27, format "c # ( x1 )") : val_scope.
Notation "c '#' '(' x1 ',' x2 ')'" := (val_con c ((x1:val)::(x2:val)::nil))
(at level 27, format "c # ( x1 ,  x2 )") : val_scope.
Notation "c '#' '(' x1 ',' x2 ',' x3 ')'" := (val_con c ((x1:val)::(x2:val)::(x3:val)::nil))
(at level 27, format "c # ( x1 ,  x2  , x3 )") : val_scope.

(************************************************************)
(* ** Notations for n-ary tuples *)

Notation "'pat_tuple' xs" := (pat_con con_tuple xs)
(at level 29, only parsing) : pat_scope.
Notation "'trm_tuple' xs" := (trm_con con_tuple xs)
(at level 29, only parsing) : trm_scope.
Notation "'val_tuple' xs" := (val_con con_tuple xs)
(at level 29, only parsing) : val_scope.

Notation "'#'" := (pat_tuple nil)
(at level 28) : pat_scope.
Notation "'#' '(' x1 ')'" := (pat_tuple ((x1:pat)::nil))
(at level 28, format "# '(' x1 ')'") : pat_scope.
Notation "'#' '(' x1 ',' x2 ')'" := (pat_tuple ((x1:pat)::(x2:pat)::nil))
(at level 28, format "# ( x1 ,  x2 )") : pat_scope.
Notation "'#' '(' x1 ',' x2 ',' x3 ')'" := (pat_tuple ((x1:pat)::(x2:pat)::(x3:pat)::nil))
(at level 28, format "# ( x1 ,  x2 ,  x3 )") : pat_scope.

Notation "'#'" := (trm_tuple nil)
(at level 28) : trm_scope.
Notation "'#' '(' x1 ')'" := (trm_tuple ((x1:trm)::nil))
(at level 28, format "# '(' x1 ')'") : trm_scope.
Notation "'#' '(' x1 ',' x2 ')'" := (trm_tuple ((x1:trm)::(x2:trm)::nil))
(at level 28, format "# ( x1 ,  x2 )") : trm_scope.
Notation "'#' '(' x1 ',' x2 ',' x3 ')'" := (trm_tuple ((x1:trm)::(x2:trm)::(x3:trm)::nil))
(at level 28, format "# ( x1 ,  x2 ,  x3 )") : trm_scope.

Notation "'#'" := (val_tuple nil)
(at level 28) : val_scope.
Notation "'#' '(' x1 ')'" := (val_tuple ((x1:val)::nil))
(at level 28, format "# '(' x1 ')'") : val_scope.
Notation "'#' '(' x1 ',' x2 ')'" := (val_tuple ((x1:val)::(x2:val)::nil))
(at level 28, format "# ( x1 ,  x2 )") : val_scope.
Notation "'#' '(' x1 ',' x2 ',' x3 ')'" := (val_tuple ((x1:val)::(x2:val)::(x3:val)::nil))
(at level 28, format "# ( x1 ,  x2 ,  x3 )") : val_scope.

(************************************************************)
(* ** Anonymous functions *)

Notation "''fun' p1 ''->' t" :=
(trm_fix novar p1 t 'crash)
(at level 200, p1 at level 0) : trm_scope.

Notation "''fun' p1 p2 '-> t" :=
('fun p1 '-> 'fun p2 '-> t)
(at level 200, p1 at level 0, p2 at level 0) : trm_scope.

Notation "''fun' p1 p2 p3 '-> t" :=
('fun p1 '-> 'fun p2 p3 '-> t)
(at level 200, p1 at level 0, p2 at level 0,
p3 at level 0) : trm_scope.

Notation "''fun' p1 p2 p3 p4 '-> t" :=
('fun p1 '-> 'fun p2 p3 p4 '-> t)
(at level 200, p1 at level 0, p2 at level 0, p3 at level 0,
p4 at level 0) : trm_scope.

Notation "''fun' p1 p2 p3 p4 p5 '-> t" :=
('fun p1 '-> 'fun p2 p3 p4 p5 '-> t)
(at level 200, p1 at level 0, p2 at level 0, p3 at level 0,
p4 at level 0, p5 at level 0) : trm_scope.

(************************************************************)
(* ** Anonymous functions with pattern matching *)

Notation "''function' '| p1 '-> t1" :=
('fun p1 '-> t1)
(at level 200, only parsing) : trm_scope.

Notation "''function' ''|' p1 ''->' t1 ''|' p2 ''->' t2" :=
(trm_fix novar p1 t1 ('fun p2 '-> t2))
(at level 200) : trm_scope.

Notation "''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3" :=
(trm_fix novar p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3))
(at level 200) : trm_scope.

Notation "''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4" :=
(trm_fix novar p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4))
(at level 200) : trm_scope.

Notation "''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5" :=
(trm_fix novar p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5))
(at level 200) : trm_scope.

(************************************************************)
(* ** Pattern matching *)

Notation "''match' t ''with' '| p1 '-> t1" :=
(('function '| p1%pat '-> t1) ' t)
(at level 200) : trm_scope.

Notation "''match' t ''with' '| p1 '-> t1 '| p2 '-> t2" :=
(('function '| p1%pat '-> t1 '| p2%pat '-> t2) ' t)
(at level 200) : trm_scope.

Notation "''match' t ''with' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3" :=
(('function '| p1%pat '-> t1 '| p2%pat '-> t2 '| p3%pat '-> t3) ' t)
(at level 200) : trm_scope.

Notation "''match' t ''with' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4" :=
(('function '| p1%pat '-> t1 '| p2%pat '-> t2 '| p3%pat '-> t3 '| p4%pat '-> t4) ' t)
(at level 200) : trm_scope.

Notation "''match' t ''with' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5" :=
(('function '| p1%pat '-> t1 '| p2%pat '-> t2 '| p3%pat '-> t3 '| p4%pat '-> t4 '| p5%pat '-> t5) ' t)
(at level 200) : trm_scope.

(************************************************************)
(* ** Exception handlers *)

Notation "''try' t1 ''catch' t2" := (trm_try t1 t2)
(at level 60) : trm_scope.

Notation "''try' t ''with' '| p1 '-> t1 'end" :=
(trm_try t ('function '| p1 '-> t1))
(at level 60) : trm_scope.

Notation "''try' t ''with' '| p1 '-> t1 '| p2 '-> t2 'end" :=
(trm_try t ('function '| p1 '-> t1 '| p2 '-> t2))
(at level 60) : trm_scope.

Notation "''Match_failure'" := (con_match_failure) (at level 0).
Notation "''Div_by_zero'" := (con_div_by_zero) (at level 0).
Notation "''Not_found'" := (con_not_found) (at level 0).

Notation "''match_failure'" := (val_con con_match_failure nil)
(at level 0) : val_scope.
Notation "''div_by_zero'" := (val_con con_div_by_zero nil)
(at level 0) : val_scope.
Notation "''not_found'" := (val_con con_not_found nil)
(at level 0) : val_scope.

(************************************************************)
(* ** Let-expressions *)

Notation "''let' p '= t1 ''in' t2" :=
(('fun p '-> t2) ' t1)
(at level 200, p at level 0) : trm_scope.

Notation "''let' f p1 '= t1 ''in' t2" :=
('let f '= ('fun p1 '-> t1) 'in t2)
(at level 200, f at level 0, p1 at level 0) : trm_scope.

Notation "''let' f p1 p2 '= t1 ''in' t2" :=
('let f '= ('fun p1 p2 '-> t1) 'in t2)
(at level 200, f at level 0, p1 at level 0,
p2 at level 0) : trm_scope.

Notation "''let' f p1 p2 p3 '= t1 ''in' t2" :=
('let f '= ('fun p1 p2 p3 '-> t1) 'in t2)
(at level 200, f at level 0, p1 at level 0,
p2 at level 0) : trm_scope.

(************************************************************)
(* ** Recursive functions *)

Notation "''let_rec_fun' f '= ''fun' p1 '-> t ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 t 'crash) 'in e)
(at level 200, f at level 0, p1 at level 0) : trm_scope.

Notation "''let_rec_fun' f '= ''fun' p1 '-> ''fun' p2 '-> t ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 ('fun p2 '-> t) 'crash) 'in e)
(at level 200, f at level 0, p1 at level 0, p2 at level 0) : trm_scope.

Notation "''let_rec_fun' f '= ''fun' p1 '-> ''fun' p2 '-> ''fun' p3 '-> t ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 ('fun p2 p3 '-> t) 'crash) 'in e)
(at level 200, f at level 0, p1 at level 0, p2 at level 0, p3 at level 0) : trm_scope.

Notation "''let_rec_fun' f '= ''fun' p1 '-> ''fun' p2 '-> ''fun' p3 '-> ''fun' p4 '-> t ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 ('fun p2 p3 p4 '-> t) 'crash) 'in e)
(at level 200, f at level 0, p1 at level 0, p2 at level 0, p3 at level 0, p4 at level 0) : trm_scope.

(************************************************************)
(* ** Recursive functions with pattern matching *)

Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 t1 'crash) 'in e)
(at level 200, only parsing) : trm_scope.

Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 t1 ('fun p2 '-> t2)) 'in e)
(at level 200) : trm_scope.

Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3)) 'in e)
(at level 200) : trm_scope.

Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4)) 'in e)
(at level 200) : trm_scope.

Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5 ''in' e" :=
('let (pat_var f) '= (trm_fix f p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5)) 'in e)
(at level 200) : trm_scope.

(************************************************************)
(* ** If-expressions *)

Notation "''if' t1 ''then' t2 ''else' t3" :=
('match t1 'with '| pat_con con_true nil '-> t2
'| pat_con con_false nil '-> t3)
(at level 200, right associativity,
format "''if'  t1  '/' ''then'  t2  '/' ''else'  t3").

(************************************************************)
(* ** Patterns *)

Notation "'_" :=
(pat_wildcard) (at level 0) : pat_scope.

Notation "p 'as x" := (pat_alias x p)
(at level 60, only parsing) : pat_scope.

Notation "'##' n" := (pat_int n)
(at level 50, format "## n") : pat_scope.

Notation "'##' 'true'" := (pat_con con_true nil)
(at level 50, format "## true") : pat_scope.
Notation "'##' 'false'" := (pat_con con_false nil)
(at level 50, format "## false") : pat_scope.

(************************************************************)
(* ** Lists *)

Notation "'[]" := (pat_con con_nil nil)
(at level 0) : pat_scope.
Notation "'[]" := (trm_con con_nil nil)
(at level 0) : trm_scope.
Notation "'[]" := (val_con con_nil nil)
(at level 0) : val_scope.

Notation "h ':: t" := (pat_con con_cons ((h%pat)::(t%pat)::nil))
(at level 41, right associativity) : pat_scope.
Notation "h ':: t" := (trm_con con_cons ((h%trm)::(t%trm)::nil))
(at level 41, right associativity) : trm_scope.
Notation "h ':: t" := (val_con con_cons ((h%val)::(t%val)::nil))
(at level 41, right associativity) : val_scope.

Notation "h ':: t" := (pat_con con_cons (((h:pat)%pat)::((t:pat)%pat)::nil))
(at level 41, right associativity) : pat_scope.
Notation "h ':: t" := (trm_con con_cons (((h:trm)%trm)::((t:trm)%trm)::nil))
(at level 41, right associativity) : trm_scope.
Notation "h ':: t" := (val_con con_cons (((h:val)%val)::((t:val)%val)::nil))
(at level 41, right associativity) : val_scope.

Notation "''[' x1 ]" := (((x1:trm) ':: '[]))
(at level 50) : trm_scope.
Notation "''[' x1 ; x2 ]" := (((x1:trm) ':: (x2:trm) ':: '[]))
(at level 50) : trm_scope.
Notation "''[' x1 ; x2 ; x3 ]" := (((x1:trm) ':: (x2:trm) ':: (x3:trm) ':: '[]))
(at level 50) : trm_scope.

(************************************************************)
(* ** Closed recursive functions *)

Notation "''let_rec_fun' f '= ''fun' p1 '-> t" :=
(val_fix f p1 t 'crash)
(at level 200, f at level 0, p1 at level 0) : val_scope.

Notation "''let_rec_fun' f '= ''fun' p1 '-> ''fun' p2 '-> t" :=
(val_fix f p1 ('fun p2 '-> t) 'crash)
(at level 200, f at level 0, p1 at level 0, p2 at level 0) : val_scope.

Notation "''let_rec_fun' f '= ''fun' p1 '-> ''fun' p2 '-> ''fun' p3 '-> t" :=
(val_fix f p1 ('fun p2 p3 '-> t) 'crash)
(at level 200, f at level 0, p1 at level 0, p2 at level 0, p3 at level 0) : val_scope.

Notation "''let_rec_fun' f '= ''fun' p1 '-> ''fun' p2 '-> ''fun' p3 '-> ''fun' p4 '-> t" :=
(val_fix f p1 ('fun p2 p3 p4 '-> t) 'crash)
(at level 200, f at level 0, p1 at level 0, p2 at level 0, p3 at level 0, p4 at level 0) : val_scope.

(************************************************************)
(* ** Closed recursive functions with pattern matching *)

Notation "''let_rec_function' f '= ''function' '| p1 '-> t1" :=
(val_fix f p1 t1 'crash)
(at level 200, f at level 0, only parsing) : val_scope.

Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2" :=
(val_fix f p1 t1 ('fun p2 '-> t2))
(at level 200, f at level 0) : val_scope.

Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3" :=
(val_fix f p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3))
(at level 200, f at level 0) : val_scope.

Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4" :=
(val_fix f p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4))
(at level 200, f at level 0) : val_scope.

Notation "''let_rec_function' f '= ''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5" :=
(val_fix f p1 t1 ('function '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5))
(at level 200, f at level 0) : val_scope.

(************************************************************)
(* ** Closed anonymous functions *)

Notation "''fun' p1 ''->' t" :=
(val_fix novar p1 t 'crash)
(at level 200, p1 at level 0) : val_scope.

Notation "''fun' p1 p2 '-> t" :=
(('fun p1%pat '-> ('fun p2%pat '-> t)%trm)%val)
(at level 200, p1 at level 0, p2 at level 0) : val_scope.

Notation "''fun' p1 p2 p3 '-> t" :=
(('fun p1%pat '-> ('fun p2%pat p3%pat '-> t)%trm)%val)
(at level 200, p1 at level 0, p2 at level 0,
p3 at level 0) : val_scope.

Notation "''fun' p1 p2 p3 p4 '-> t" :=
(('fun p1%pat '-> ('fun p2%pat p3%pat p4%pat '-> t)%trm)%val)
(at level 200, p1 at level 0, p2 at level 0, p3 at level 0,
p4 at level 0) : val_scope.

Notation "''fun' p1 p2 p3 p4 p5 '-> t" :=
(('fun p1%pat '-> ('fun p2%pat p3%pat p4%pat p5%pat '-> t)%trm)%val)
(at level 200, p1 at level 0, p2 at level 0, p3 at level 0,
p4 at level 0, p5 at level 0) : val_scope.

(************************************************************)
(* ** Closed anonymous functions with pattern matching *)

Notation "''function' '| p1 '-> t1" :=
(('fun p1%pat '-> t1)%val)
(at level 200, only parsing) : val_scope.

Notation "''function' '| p1 '-> t1 '| p2 '-> t2" :=
(val_fix novar p1%pat t1 ('function '| p2%pat '-> t2)%trm)
(at level 200) : val_scope.

Notation "''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3" :=
(val_fix novar p1%pat t1 ('function '| p2%pat '-> t2 '| p3%pat '-> t3)%trm)
(at level 200) : val_scope.

Notation "''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4" :=
(val_fix novar p1%pat t1 ('function '| p2%pat '-> t2 '| p3%pat '-> t3 '| p4%pat '-> t4)%trm)
(at level 200) : val_scope.

Notation "''function' '| p1 '-> t1 '| p2 '-> t2 '| p3 '-> t3 '| p4 '-> t4 '| p5 '-> t5" :=
(val_fix novar p1%pat t1 ('function '| p2%pat '-> t2 '| p3%pat '-> t3 '| p4%pat '-> t4 '| p5%pat '-> t5)%trm)
(at level 200) : val_scope.

(************************************************************)
(* ** Notation for pairs without parentheses *)

Notation "x1 ', x2" := ((#((x1:pat),(x2:pat)))%pat) (at level 42) : pat_scope.
Notation "x1 ', x2" := ((#((x1:trm),(x2:trm)))%trm) (at level 42) : trm_scope.
Notation "x1 ', x2" := ((#((x1:val),(x2:val)))%val) (at level 42) : val_scope.
```