include "Maybe.ma".
include "Nat.ma".
include "Util.ma".

ninductive List (A: Type[0]): Type[0] ≝
  Empty: List A
| Cons: A → List A → List A.

notation "hvbox(hd break :: tl)"
  right associative with precedence 47
  for @{ 'Cons $hd $tl }.

interpretation "Empty" 'Empty = (Empty ?).
interpretation "Cons" 'Cons = (Cons ?).
  
notation "[ list0 x sep ; ]"
  non associative with precedence 90
  for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }.
  
nlet rec length (A: Type[0]) (l: List A) on l ≝
  match l with
    [ Empty ⇒ Z
    | Cons hd tl ⇒ S $ length A tl
    ].
    
nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝
  match l with
    [ Empty ⇒ m
    | Cons hd tl ⇒ hd :: (append A tl l)
    ].
    
notation "hvbox(l break @ r)"
  right associative with precedence 47
  for @{ 'append $l $r }.
  
interpretation "Append" 'append = (append ?).
  
nlet rec fold_right (A: Type[0]) (B: Type[0])
                    (f: A → B → B) (x: B) (l: List A) on l ≝
  match l with
    [ Empty ⇒ x
    | Cons hd tl ⇒ f hd (fold_right A B f x tl)
    ].
    
nlet rec fold_left (A: Type[0]) (B: Type[0])
                   (f: A → B → A) (x: A) (l: List B) on l ≝
  match l with
    [ Empty ⇒ x
    | Cons hd tl ⇒ f (fold_left A B f x tl) hd
    ].
    
nlet rec map (A: Type[0]) (B: Type[0])
             (f: A → B) (l: List A) on l ≝
  match l with
    [ Empty ⇒ Empty B
    | Cons hd tl ⇒ f hd :: map A B f tl
    ].
    
nlet rec null (A: Type[0]) (l: List A) on l ≝
  match l with
    [ Empty ⇒ True
    | Cons hd tl ⇒ False
    ].
    
nlet rec reverse (A: Type[0]) (l: List A) on l ≝
  match l with
    [ Empty ⇒ Empty A
    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
    ].
    
ndefinition head ≝
  λA: Type[0].
  λl: List A.
    match l with
      [ Empty ⇒ Nothing A
      | Cons hd tl ⇒ Just A hd
      ].
    
ndefinition tail ≝
  λA: Type[0].
  λl: List A.
    match l with
      [ Empty ⇒ Nothing (List A)
      | Cons hd tl ⇒ Just (List A) tl
      ].
      
nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝
  match n with
    [ Z ⇒ Empty A
    | S o ⇒ a :: replicate A o a
    ].