Mysaa/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Correction d'un bug

Browse Source
This commit is contained in:
Adrien Vannson 2022-05-08 18:10:08 +02:00
parent 4d6287f2cd
commit 15afcecabe
No known key found for this signature in database
GPG Key ID: FE2E66FD978C1A55
1 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
pieuvre.ml
View File

@ -8,7 +8,7 @@ exception IllegalVarNameException of var
let rec string_of_ty (t: ty) : string = let rec string_of_ty (t: ty) : string =
match t with match t with
| TSimple(tn) -> tn | TSimple(tn) -> tn
| TImpl(t1,t2) -> (string_of_ty t1) ^ " -> " ^ (string_of_ty t2) | TImpl(t1,t2) -> "(" ^ (string_of_ty t1) ^ " -> " ^ (string_of_ty t2) ^ ")"
| TFalse -> "⊥" | TFalse -> "⊥"
;; ;;
@ -27,7 +27,7 @@ let split, tsplit =
let xStr = matched_group 1 x in let xStr = matched_group 1 x in
let xInt = matched_group 2 x in let xInt = matched_group 2 x in
(xStr, int_of_string xInt) (xStr, int_of_string xInt)
else raise (IllegalVarNameException(x)) else raise (IllegalVarNameException(x))
in (splitter varRegex, splitter tvarRegex);; in (splitter varRegex, splitter tvarRegex);;
@ -62,7 +62,7 @@ let findTFreeName (t: ty) (x: tvar) =
(* Renvoie l[s/x] *) (* Renvoie l[s/x] *)
let rec replace (l: lam) (x: var) (s: lam) = match l with let rec replace (l: lam) (x: var) (s: lam) = match l with
| LFun(v,t,l') -> | LFun(v,t,l') ->
if(v=x) if(v=x)
then let y=findFreeName l' v in then let y=findFreeName l' v in
LFun(v,t,replace l' v (LVar(y))) LFun(v,t,replace l' v (LVar(y)))
@ -71,12 +71,12 @@ let rec replace (l: lam) (x: var) (s: lam) = match l with
| LApp(l1, l2) -> LApp(replace l1 x s, replace l2 x s) | LApp(l1, l2) -> LApp(replace l1 x s, replace l2 x s)
| LVar(v) -> if v=x then s else LVar(v) | LVar(v) -> if v=x then s else LVar(v)
| LExf(l',t) -> LExf(replace l' x s, t) | LExf(l',t) -> LExf(replace l' x s, t)
;; ;;
(* Teste si les deux λ-termes l1 et l2 sont α-convertibles *) (* Teste si les deux λ-termes l1 et l2 sont α-convertibles *)
let rec alpha (l1: lam) (l2: lam) : bool = let rec alpha (l1: lam) (l2: lam) : bool =
match (l1,l2) with match (l1,l2) with
| (LFun(v1,t1,l1'),LFun(v2,t2,l2')) -> | (LFun(v1,t1,l1'),LFun(v2,t2,l2')) ->
(t1 = t2) && (t1 = t2) &&
(* On trouve un nom libre dans les deux sous-termes *) (* On trouve un nom libre dans les deux sous-termes *)
let v' = findFreeName (LApp(l1', l2')) v1 in let v' = findFreeName (LApp(l1', l2')) v1 in
@ -90,14 +90,14 @@ let rec alpha (l1: lam) (l2: lam) : bool =
(* Fait un pas de β-réduction, et renvoie None si on a une forme normale *) (* 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 let rec betastep (l: lam) : lam option = match l with
| LFun(v,t,l') -> betastep l' | LFun(v,t,l') -> betastep l'
| LApp(lf,lx) -> | LApp(lf,lx) ->
begin begin
match (betastep lf) with match (betastep lf) with
| Some lf' -> Some (LApp(lf',lx)) | Some lf' -> Some (LApp(lf',lx))
| None -> | None ->
match (betastep lx) with match (betastep lx) with
| Some lx' -> Some (LApp(lf, lx')) | Some lx' -> Some (LApp(lf, lx'))
| None -> | None ->
match lf with match lf with
| LFun(x,_,corps) -> Some (replace corps x lx) | LFun(x,_,corps) -> Some (replace corps x lx)
| _ -> None (* On ne peut pas β-réduire *) | _ -> None (* On ne peut pas β-réduire *)
@ -120,17 +120,17 @@ let rec typecheck (env: gam) (l: lam) (t: ty) : bool =
match (l,t) with match (l,t) with
| (LFun(x,t,l'),TImpl(tx,ty)) -> typecheck ((x,tx)::env) l' ty | (LFun(x,t,l'),TImpl(tx,ty)) -> typecheck ((x,tx)::env) l' ty
| (LFun(_,_,_),_) -> false (* Une fonction est forcément une ... fonction *) | (LFun(_,_,_),_) -> false (* Une fonction est forcément une ... fonction *)
| (LApp(lf,lx),t) -> | (LApp(lf,lx),t) ->
let t' = (raise TODOException; TFalse) in let t' = (raise TODOException; TFalse) in
(typecheck env lf (TImpl(t',t))) && (typecheck env lx t') (typecheck env lf (TImpl(t',t))) && (typecheck env lx t')
| (LVar(x),t) -> | (LVar(x),t) ->
begin begin
match env with match env with
| (y,t')::env' -> if x=y then t=t' | (y,t')::env' -> if x=y then t=t'
else typecheck env' l t else typecheck env' l t
| [] -> raise TODOException | [] -> raise TODOException
end end
| (LExf(l',t'),t) -> | (LExf(l',t'),t) ->
if t=t' if t=t'
then typecheck env l' t then typecheck env l' t
else false (* Le ex falso a le mauvais type *) else false (* Le ex falso a le mauvais type *)