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

Correction de l'α-conversion.

Browse Source
This commit is contained in:
Mysaa 2022-05-11 22:36:31 +02:00
parent 09ebe6339e
commit 905b86af2d
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
2 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
pieuvre.ml
View File

@ -23,11 +23,11 @@ let rec string_of_lam (l: lam) : string = match l with
let split, tsplit =
let splitter regex x =
if string_match regex x 0
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)
(xStr, if xInt="" then 0 else (int_of_string xInt))
else raise (IllegalVarNameException(x))
in (splitter varRegex, splitter tvarRegex);;
@ -81,7 +81,7 @@ let rec alpha (l1: lam) (l2: lam) : bool =
(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')))
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')

4
structs.ml
View File

@ -1,13 +1,13 @@
(* Variables des λ-termes *)
type var_lambda = string;;
type var = var_lambda;; (* TODEL *)
let varRegex = Str.regexp "^([a-z]+)([0-9]*)$";;
let varRegex = Str.regexp "^\\([a-z]+\\)\\([0-9]*\\)$";;
(* Variable des types simples *)
type var_type = string;;
type tvar = var_type;; (* TODEL *)
let tvarRegex = Str.regexp "^([A-Z]+)([0-9]*)$";;
let tvarRegex = Str.regexp "^([A-Z]+)([0-9]*)?$";;
(* Type complexe *)
type ty =