244 lines
9.2 KiB
OCaml
244 lines
9.2 KiB
OCaml
open Structs
|
||
open Str
|
||
|
||
|
||
exception TODOException;;
|
||
exception IllegalVarNameException of var
|
||
|
||
(* Casse un objet option *)
|
||
let optionmatch (nonefun: 'b option) (somefun: 'a -> 'b option) (o: 'a option) : 'b option =
|
||
match o with
|
||
| Some x -> somefun x
|
||
| None -> nonefun
|
||
;;
|
||
|
||
(* 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) ^ ")"
|
||
| TAnd(t1,t2) -> "(" ^ (string_of_ty t1) ^ " /\\ " ^ (string_of_ty t2) ^ ")"
|
||
| TOr(t1,t2) -> "(" ^ (string_of_ty t1) ^ " \\/ " ^ (string_of_ty t2) ^ ")"
|
||
| TFalse -> "False"
|
||
| TTrue -> "True"
|
||
;;
|
||
|
||
(* 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') -> "(fun "^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)^")"
|
||
| LCouple(lg,ld) -> "("^(string_of_lam lg)^","^(string_of_lam ld)^")"
|
||
| LFst(ll) -> "fst("^(string_of_lam ll)^")"
|
||
| LSnd(ll) -> "snd("^(string_of_lam ll)^")"
|
||
| LIg(ll,t) -> "ig("^(string_of_lam ll)^","^(string_of_ty t)^")"
|
||
| LId(ll,t) -> "id("^(string_of_lam ll)^","^(string_of_ty t)^")"
|
||
| LCase(ll,lg,ld) -> "case("^(string_of_lam ll)^","^(string_of_lam lg)^","^(string_of_lam ld)^")"
|
||
| LI -> "I"
|
||
;;
|
||
|
||
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, if xInt="" then 0 else (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'
|
||
| LCouple(l1,l2) -> (finder l1;finder l2)
|
||
| LFst(l') -> finder l'
|
||
| LSnd(l') -> finder l'
|
||
| LIg(l',t) -> finder l'
|
||
| LId(l',t) -> finder l'
|
||
| LCase(ll,lg,ld) -> (finder ll; finder lg; finder ld)
|
||
| LI -> ()
|
||
|
||
in
|
||
finder l;
|
||
xStr ^ (string_of_int (!maxi+1))
|
||
;;
|
||
|
||
(* Renvoie un nom non utilisé dans la liste de nom donnée, basée sur le nom x *)
|
||
let findHypName (names: var list) (x: var) =
|
||
let xStr = fst (split x) in
|
||
let maxi = ref 0 in
|
||
let rec finder l = match l with
|
||
| [] -> ()
|
||
| v::r ->
|
||
begin
|
||
let (vS,vI) = split v in
|
||
(if xStr=vS then maxi := max !maxi vI);
|
||
finder r
|
||
end
|
||
in
|
||
finder names;
|
||
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
|
||
| TAnd(t1, t2) -> (finder t1;finder t2)
|
||
| TOr(t1, t2) -> (finder t1;finder t2)
|
||
| TTrue -> ()
|
||
| 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)
|
||
| LCouple(lg,ld) -> LCouple(replace lg x s, replace ld x s)
|
||
| LFst(l') -> LFst(replace l' x s)
|
||
| LSnd(l') -> LSnd(replace l' x s)
|
||
| LIg(l',t) -> LIg(replace l' x s, t)
|
||
| LId(l',t) -> LId(replace l' x s, t)
|
||
| LCase(l',lg,ld) -> LCase(replace l' x s, replace lg x s, replace ld x s)
|
||
| LI -> LI
|
||
|
||
;;
|
||
|
||
(* 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')
|
||
| (LFst(l1),LFst(l2)) -> alpha l1 l2
|
||
| (LSnd(l1),LSnd(l2)) -> alpha l1 l2
|
||
| (LIg(l1,t1),LIg(l2,t2)) -> t1=t2 && alpha l1 l2
|
||
| (LId(l1,t1),LId(l2,t2)) -> t1=t2 && alpha l1 l2
|
||
| (LCase(l1,lg1,ld1),LCase(l2,lg2,ld2)) -> (alpha l1 l2) && (alpha lg1 lg2) && (alpha ld1 ld2)
|
||
| (LI,LI) -> true
|
||
|
||
| _ -> 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') -> Option.bind (betastep l') (fun l' -> Some (LFun(v,t,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',t) -> Option.bind (betastep l') (fun l' -> Some (LExf(l',t)))
|
||
| LCouple(lg,ld) -> optionmatch (Option.bind (betastep ld) (fun lg' -> Some (LCouple(ld,lg')))) (fun lg' -> Some (LCouple(lg',ld))) (betastep lg)
|
||
| LFst(ll) -> begin
|
||
match (ll,betastep ll) with
|
||
| (_,Some ll') -> Some (LFst(ll'))
|
||
| (LCouple(lg,ld),None) -> Some lg
|
||
| (_,None) -> None
|
||
end
|
||
| LSnd(ll) -> begin
|
||
match (ll,betastep ll) with
|
||
| (_,Some ll') -> Some (LFst(ll'))
|
||
| (LCouple(lg,ld),None) -> Some ld
|
||
| (_,None) -> None
|
||
end
|
||
| LIg(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LIg(l',t)))
|
||
| LId(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LId(l',t)))
|
||
| LCase(ll,lg,ld) -> begin
|
||
match (ll,betastep ll) with
|
||
| (_,Some ll') -> Some (LFst(ll'))
|
||
| (LIg(_,_),None) -> Some lg
|
||
| (LId(_,_),None) -> Some ld
|
||
| (_,None) -> None
|
||
end
|
||
| LI -> None
|
||
|
||
;;
|
||
|
||
(* 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 -> ()
|
||
;;
|
||
|
||
(* Calcule le type du λ-terme l sous l'environnement env.
|
||
Renvoie None si la formule n'est pas typable ou si la formule n'est pas close (sous d'environnement)*)
|
||
let rec computeType (env: gam) (l: lam) : ty option =
|
||
match l with
|
||
| LFun(x,tx,l') -> Option.bind (computeType ((x,tx)::env) l') (fun ty -> Some (TImpl(tx,ty)))
|
||
| LApp(lf,lx) ->
|
||
let tx = computeType env lx in
|
||
let tf = computeType env lf in
|
||
begin
|
||
match tf with
|
||
| Some TImpl(tx',ty') -> if Some tx'=tx then Some ty' else None
|
||
| _ -> None (* Si none, l'argument n'est pas typable, si Some _, on ne peut typer l'application *)
|
||
end
|
||
| LVar(x) ->
|
||
begin
|
||
match env with
|
||
| (y,ty)::env' -> if x=y then Some ty
|
||
else computeType env' l
|
||
| [] -> None
|
||
end
|
||
| LExf(l',t) -> begin
|
||
match (computeType env l') with
|
||
| Some TFalse -> Some t (* On applique le ExFalso *)
|
||
| _ -> None (* Le ex falso a le mauvais type *)
|
||
end
|
||
| LCouple(lg,ld) -> Option.bind (computeType env lg) (fun tg -> Option.bind (computeType env ld) (fun td -> Some (TAnd(tg,td))))
|
||
| LFst(l') -> Option.bind (computeType env l') (function TAnd(t1,t2) -> Some t1 | _ -> None)
|
||
| LSnd(l') -> Option.bind (computeType env l') (function TAnd(t1,t2) -> Some t2 | _ -> None)
|
||
| LIg(l',td) -> Option.bind (computeType env l') (fun tg -> Some (TOr(tg,td)))
|
||
| LId(l',tg) -> Option.bind (computeType env l') (fun td -> Some (TOr(tg,td)))
|
||
| LCase(l',lg,ld) -> begin
|
||
match (computeType env l',computeType env lg,computeType env ld) with
|
||
| (Some TOr(t1a,t1b),Some TImpl(t2a,t2c),Some TImpl(t3b,t3c)) when t1a=t2a && t1b=t3b && t2c=t3c -> Some t3c
|
||
| _ -> None
|
||
end
|
||
| LI -> Some TTrue
|
||
;;
|
||
|
||
(* Vérifie que le λ-terme l sous l'environnement env a bien le type t *)
|
||
let typecheck (env: gam) (l: lam) (t: ty) : bool =
|
||
computeType env l = Some t;;
|