138 lines
4.7 KiB
OCaml
138 lines
4.7 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, tsplit =
|
||
let splitter regex x =
|
||
if string_match regex 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))
|
||
in (splitter varRegex, splitter tvarRegex);;
|
||
|
||
(* 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 un nom de type simple non utilisé dans le type t qui commence par x *)
|
||
let findTFreeName (t: ty) (x: tvar) =
|
||
let xStr = fst (tsplit x) in
|
||
let maxi = ref 0 in
|
||
let rec finder t = match t with
|
||
| TImpl(t1, t2) -> (finder t1;finder t2)
|
||
| TSimple(y) -> let (yS,yI) = split y in
|
||
if xStr=yS then maxi := max !maxi yI
|
||
| TFalse -> () (* Le faux ne réserve pas de variables *)
|
||
in
|
||
finder t;
|
||
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 rec betastep (l: lam) : lam option = match l with
|
||
| LFun(v,t,l') -> betastep l'
|
||
| LApp(lf,lx) ->
|
||
begin
|
||
match (betastep lf) with
|
||
| Some lf' -> Some (LApp(lf',lx))
|
||
| None ->
|
||
match (betastep lx) with
|
||
| Some lx' -> Some (LApp(lf, lx'))
|
||
| None ->
|
||
match lf with
|
||
| LFun(x,_,corps) -> Some (replace corps x lx)
|
||
| _ -> None (* On ne peut pas β-réduire *)
|
||
end
|
||
| LVar(x) -> None
|
||
| LExf(l',_) -> betastep l'
|
||
;;
|
||
|
||
(* Affiche les réductions du λ-terme l jusqu’à atteindre une forme normale, ou part en boucle infinie *)
|
||
let rec reduce (l:lam) : unit =
|
||
print_string (string_of_lam l);
|
||
print_newline ();
|
||
match (betastep l) with
|
||
| Some l' -> reduce l'
|
||
| None -> ()
|
||
;;
|
||
|
||
(* Vérifie que le λ-terme l sous l'environnement env a bien le type t *)
|
||
let rec typecheck (env: gam) (l: lam) (t: ty) : bool =
|
||
match (l,t) with
|
||
| (LFun(x,t,l'),TImpl(tx,ty)) -> typecheck ((x,tx)::env) l' ty
|
||
| (LFun(_,_,_),_) -> false (* Une fonction est forcément une ... fonction *)
|
||
| (LApp(lf,lx),t) ->
|
||
let t' = (raise TODOException; TFalse) in
|
||
(typecheck env lf (TImpl(t',t))) && (typecheck env lx t')
|
||
| (LVar(x),t) ->
|
||
begin
|
||
match env with
|
||
| (y,t')::env' -> if x=y then t=t'
|
||
else typecheck env' l t
|
||
| [] -> raise TODOException
|
||
end
|
||
| (LExf(l',t'),t) ->
|
||
if t=t'
|
||
then typecheck env l' t
|
||
else false (* Le ex falso a le mauvais type *)
|
||
;;
|