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
)
);;