(**************************************************************************
* 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 
    programs. A few comments:
    - 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).
      All these notations start with a quote symbol, e.g. ['x].
    - 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.