91 lines
3.0 KiB
OCaml
91 lines
3.0 KiB
OCaml
open Structs
|
||
open Str
|
||
|
||
exception TODOException;;
|
||
exception IllegalVarNameException of var
|
||
|
||
(* Affiche un λ-terme avec la même syntaxe qu’en entrée *)
|
||
let rec string_of_ty (t: ty) : string =
|
||
match t with
|
||
| TSimple(tn) -> tn
|
||
| TImpl(t1,t2) -> (string_of_ty t1) ^ " -> " ^ (string_of_ty t2)
|
||
| TFalse -> "⊥"
|
||
;;
|
||
|
||
(* Affiche un λ-terme avec la même syntaxe qu’en entrée *)
|
||
let rec string_of_lam (l: lam) : string = match l with
|
||
| LFun(v,t,l') -> "λ"^v^":"^(string_of_ty t)^" . "^(string_of_lam l')
|
||
| LApp(l1, l2) -> (string_of_lam l1)^" "^(string_of_lam l2)
|
||
| LVar(v) -> v
|
||
| LExf(l',t) -> "exf("^(string_of_lam l')^" : "^(string_of_ty t)^")"
|
||
;;
|
||
|
||
let split (x:var) : string * int =
|
||
if string_match varRegex x 0
|
||
then
|
||
let xStr = matched_group 1 x in
|
||
let xInt = matched_group 2 x in
|
||
(xStr, int_of_string xInt)
|
||
|
||
else raise (IllegalVarNameException(x))
|
||
;;
|
||
|
||
(* Renvoie un nom non utilisé dans la formule l qui commence par x *)
|
||
let findFreeName (l: lam) (x: var) =
|
||
let xStr = fst (split x) in
|
||
let maxi = ref 0 in
|
||
let rec finder l = match l with
|
||
| LFun(v,t,l') -> (finder (LVar(v));finder l')
|
||
| LApp(l1, l2) -> (finder l1;finder l2)
|
||
| LVar(v) -> let (vS,vI) = split v in
|
||
if xStr=vS then maxi := max !maxi vI
|
||
| LExf(l',t) -> finder l'
|
||
in
|
||
finder l;
|
||
xStr ^ (string_of_int (!maxi+1))
|
||
|
||
|
||
;;
|
||
|
||
(* Renvoie l[s/x] *)
|
||
let rec replace (l: lam) (x: var) (s: lam) = match l with
|
||
| LFun(v,t,l') ->
|
||
if(v=x)
|
||
then let y=findFreeName l' v in
|
||
LFun(v,t,replace l' v (LVar(y)))
|
||
(* Pas besoin replace les x, ils ont tous été déjà remplacés *)
|
||
else LFun(v,t,replace l' x s)
|
||
| LApp(l1, l2) -> LApp(replace l1 x s, replace l2 x s)
|
||
| LVar(v) -> if v=x then s else LVar(v)
|
||
| LExf(l',t) -> LExf(replace l' x s, t)
|
||
;;
|
||
|
||
(* Teste si les deux λ-termes l1 et l2 sont α-convertibles *)
|
||
let rec alpha (l1: lam) (l2: lam) : bool =
|
||
match (l1,l2) with
|
||
| (LFun(v1,t1,l1'),LFun(v2,t2,l2')) ->
|
||
(t1 = t2) &&
|
||
(* On trouve un nom libre dans les deux sous-termes *)
|
||
let v' = findFreeName (LApp(l1', l2')) v1 in
|
||
alpha (replace l1 v1 (LVar(v'))) (replace l2 v2 (LVar(v')))
|
||
| (LApp(lf1,lx1),LApp(lf2,lx2)) -> (alpha lf1 lf2) && (alpha lx1 lx2)
|
||
| (LVar(x1),LVar(x2)) -> x1 = x2
|
||
| (LExf(l1', t1),LExf(l2', t2)) -> t1=t2 && (alpha l1' l2')
|
||
| _ -> false (* Les deux formules n'ont pas la même structure *)
|
||
;;
|
||
|
||
(* Fait un pas de β-réduction, et renvoie None si on a une forme normale *)
|
||
let betastep (l: lam) : lam option =
|
||
raise TODOException
|
||
;;
|
||
|
||
(* Affiche les réductions du λ-terme l jusqu’à atteindre une forme normale, ou part en boucle infinie *)
|
||
let reduce (l:lam) : unit =
|
||
raise TODOException
|
||
;;
|
||
|
||
(* Vérifie que le λ-terme l sous l'environnement env a bien le type t *)
|
||
let typecheck (env: gam) (l: lam) (t: ty) : bool =
|
||
raise TODOException
|
||
;;
|