type var = string

type lambda =
  |Occ of var
  |App of lambda*lambda
  |Abs of var*lambda

(* Exercice 1 *)

type lambda_kind =
  |Infun
  |Inapp
  |Inarg

let rec chemin_valide t c = match c with
  |[]   -> true
  |h::q -> (match h with
           |Infun -> (match t with
                     |Occ(v)   -> false
                     |App(r,s) -> false
                     |Abs(v,r) -> true && (chemin_valide r q)
                     )
           |Inapp -> (match t with
                     |Occ(v)   -> false
                     |App(r,s) -> true && (chemin_valide r q)
                     |Abs(v,r) -> false
                     )
           |Inarg -> (match t with
                     |Occ(v)   -> false
                     |App(r,s) -> true && (chemin_valide s q)
                     |Abs(v,r) -> false
                     )
           );;

exception No_such_term
            
let rec sous_terme t c = match c with
  |[]   -> t
  |h::q -> (match h with
           |Infun -> (match t with
                     |Occ(v)   -> raise No_such_term
                     |App(r,s) -> raise No_such_term
                     |Abs(v,r) -> sous_terme r q
                     )
           |Inapp -> (match t with
                     |Occ(v)   -> raise No_such_term
                     |App(r,s) -> sous_terme r q
                     |Abs(v,r) -> raise No_such_term
                     )
           |Inarg -> (match t with
                     |Occ(v)   -> raise No_such_term
                     |App(r,s) -> sous_terme s q
                     |Abs(v,r) -> raise No_such_term
                     )
           );;

let rec est_occurence t c x = match c with
  |[]   -> (match t with
           |Occ(x) -> true
           |_      -> false
           )
  |h::q -> (match h with
           |Infun -> (match t with
                     |Occ(v)   -> raise No_such_term
                     |App(r,s) -> raise No_such_term
                     |Abs(v,r) -> sous_terme r q
                     )
           |Inapp -> (match t with
                     |Occ(v)   -> raise No_such_term
                     |App(r,s) -> sous_terme r q
                     |Abs(v,r) -> raise No_such_term
                     )
           |Inarg -> (match t with
                     |Occ(v)   -> raise No_such_term
                     |App(r,s) -> sous_terme s q
                     |Abs(v,r) -> raise No_such_term
                     )
           );;