From 31c9a45265e8836291569171bc39c3ad602950d2 Mon Sep 17 00:00:00 2001 From: julia Date: Tue, 27 Jun 2023 21:00:05 +0200 Subject: [PATCH] working parser but app must be used with (), working notation of \x y. for \x. \y. --- lambda.ml | 137 ---------------------------------------------- lambda/lambda.ml | 5 +- lambda/lexer.mll | 2 +- lambda/parser.mly | 16 +----- 4 files changed, 7 insertions(+), 153 deletions(-) delete mode 100644 lambda.ml diff --git a/lambda.ml b/lambda.ml deleted file mode 100644 index 43221ca..0000000 --- a/lambda.ml +++ /dev/null @@ -1,137 +0,0 @@ -(*Terme du Lambda-Calcul*) -type term = - | Var of string - | Lambda of string * term - | App of term * term - -(*Applique une substitution de x par sub à un terme t*) -let rec apply x sub = function - | Var (y) -> if y = x then sub else Var (y) - | Lambda (y,t) -> Lambda (y, apply x sub t) - | App (t1, t2) -> App (apply x sub t1, apply x sub t2) - -(*Applique une liste de substition à un terme*) -let rec subst t sub_list = - List.fold_left (fun t (x, sub) -> apply x sub t) t sub_list - -(* Applique la beta réduction, qui transforme (lambda x. t)u en t[x:=u] *) -let rec beta = function - | App (Lambda (x, t), u) -> subst t [(x, u)] - | _ -> failwith "This term is not a redex" - -(* --------------------------------------- - Exemples - --------------------------------------- *) - -let x = Var "x";; -let y = Var "y";; -let a = Var "a" ;; -let b = Var "b" ;; -let i = Lambda ("x", x);; - -(*(λx. x x) a — duplication*) -let n1 = App (Lambda ("x", App (x, x)), a);; -(*(λx. x x) (λa. a) — passage de fonction / ordre supérieur*) -let n2 = App (Lambda ("x", App (x, x)), Lambda (("a"), a));; -(*(λx. x (λx.x)) y — variable libres/liées*) -let n3 = App (Lambda ("x", App (x, Lambda ("x", x) ) ), y) ;; -(*(λx. x (λy. x y)) y — capture de variable*) -let n4 = App (Lambda ("x", App(x, Lambda ("y", App (x, y)))), y);; -(*(λxy. x) a b — fonction à deux entrées et effacement*) -let n5 = App ( App ( Lambda ("x", ( Lambda ("y", x))), a), b);; -(*(λxy. x) a — application partielle pour deux entrées*) -let n6 = App ( Lambda ("x", ( Lambda ("y", x))), a);; -(*(λxy. x) I a b — sur application pour deux entrées*) -let n7 = App (App ( App (Lambda ("x", ( Lambda ("y", x))), i), a), b);; -(*(λx. x x) (I I) — duplication inutile dans une stratégie*) -let n8 = App ( Lambda ("x", App (x, x)), App ( i, i));; -(*(λxy. y) (I I) I — différence de complexité selon la stratégie*) -let n9 = App ( App (Lambda ("x", ( Lambda ("y", y))), App (i, i)), i);; - -(* --------------------------------------- - Display - --------------------------------------- *) - -let rec string_of_list printer sep = function - | [] -> "" - | [x] -> printer x - | h::t -> - (printer h) ^ sep ^ (string_of_list printer sep t) - - -let rec string_of_term = function - | Var x -> x - | Lambda (x, Lambda (y, t)) -> "λ" ^ x ^ y ^ ". " ^ string_of_term t ^ "" - | Lambda (x, t) -> "λ" ^ x ^ ". " ^ string_of_term t ^ "" - | App (Var x, Var y) -> x ^ " " ^ y - | App (t, Var x) -> "(" ^ string_of_term t ^ ") " ^ x - | App ( App ( t, u), v) -> "(" ^ string_of_term (App (t, u)) ^ ") " ^ string_of_term v - | App ( u, App ( t, v)) -> string_of_term u ^ " (" ^ string_of_term (App (t, v)) ^ ")" - | App ( Lambda (x, App (t, y)), v) -> "(" ^ string_of_term (Lambda (x, App (t, y))) ^ ") " ^ string_of_term v - | App ( Lambda (x, t), u) -> string_of_term (Lambda (x,t)) ^ " (" ^ string_of_term u ^")" - | App (t, u) -> string_of_term t ^ " (" ^ string_of_term u ^ ")" - - -(* --------------------------------------- - Réduction - --------------------------------------- *) - -exception Irreductible -(* Vérifie si un terme est une valeur, c'est à dire qu'on ne peut plus le réduire *) -let is_value = function - | Lambda (_, _) -> true - | Var _ -> true - | _ -> false - -(* Vérifie si un lambda est linéaire, i.e. qu'il n'y a qu'une seule occurence de son paramètre *) - -let rec count_freevars x = function - | Lambda (y, t) -> count_freevars x t - | App (t, u) -> (count_freevars x t) + (count_freevars x u) - | Var y -> if x = y then 1 else 0 - - let rec is_linear = function - | Lambda (x, t) -> (count_freevars x t) = 1 && is_linear t - | App(t, u) -> is_linear t && is_linear u - | Var x -> true - -(* Réduit d'un pas les termes par l -'extérieur puis l'intérieur *) -let rec lo_reduction = function - | App ( Lambda (x, t), u) as redex -> (beta redex) - | App (Var x, (_ as t)) -> App (Var x, lo_reduction t) - | App (App (_,_) as t, Var x) -> App (lo_reduction t, Var x) - | App (App (_,_) as t, (_ as u)) -> App (lo_reduction t, u) - (*| App (t, u) -> (App (lo_reduction t, lo_reduction u))*) - | Lambda (x, t) -> Lambda (x, lo_reduction t) - | _ -> raise Irreductible - -(* Boucle sur la lo_reduction pour appliquer cette stratégie de réduction jusqu'à la fin *) -let rec lo_eval t = - try let t' = lo_reduction t in - lo_eval t' with Irreductible -> t - -(* Réduit d'un pas les termes en commençant par l'argument puis réduit les fonctions *) -let rec cbv = function - | App ( Lambda (x, t), v) as redex when is_value v -> (*cbv*) (beta redex) - | App (t, u) when is_value u -> (App (cbv t, u)) - | App (t, u) -> (App (t, cbv u)) - | Lambda (x, t) -> raise Irreductible - | Var x -> raise Irreductible - -(* Boucle sur call_by_value pour appliquer cette stratégie de réduction jusqu'à la fin *) -let rec cbv_eval t = - try let t' = cbv t in - cbv_eval t' with Irreductible -> t - -(* Réduit d'un pas les termes en commençant par la fonction puis passe à l'argument*) -let rec cbn = function - | App ( Lambda (x, t), v) as redex -> beta redex - | App (t, u) -> (App (cbn t, u)) - | Lambda (x, t) -> raise Irreductible - | Var x -> raise Irreductible - -(* Boucle sur call_by_name pour appliquer cette stratégie de réduction jusqu'à la fin *) -let rec cbn_eval t = - try let t' = cbv t in - cbn_eval t' with Irreductible -> t diff --git a/lambda/lambda.ml b/lambda/lambda.ml index 096799b..ac9063d 100644 --- a/lambda/lambda.ml +++ b/lambda/lambda.ml @@ -7,7 +7,10 @@ type term = let to_var x = Var x -let to_lambda x t = Lambda (x, t) +let rec to_lambda l t = + match l with + | h::tail -> Lambda (h, to_lambda tail t) + | [] -> t let to_app t u = App (t, u) diff --git a/lambda/lexer.mll b/lambda/lexer.mll index 97c8eef..c52d561 100644 --- a/lambda/lexer.mll +++ b/lambda/lexer.mll @@ -13,6 +13,6 @@ rule read = parse | ')' { RIGHT_PAR } | '.' { DOT } | '\\' { LAMBDA } - | space { SPACE } + | space { read lexbuf } | newline { read lexbuf } | eof { exit 0 } \ No newline at end of file diff --git a/lambda/parser.mly b/lambda/parser.mly index 19ae50f..d2ac72c 100644 --- a/lambda/parser.mly +++ b/lambda/parser.mly @@ -2,24 +2,12 @@ %token VAR %token DOT %token LAMBDA -%token SPACE -%left SPACE -%token END - %start termc %% -(* -mainc: -| t = termc END { t }*) - termc: | x = VAR { Lambda.to_var x } -| LAMBDA ; x = VAR ; DOT; SPACE; t = termc { Lambda.to_lambda x t } -| LEFT_PAR ; t = termc ; SPACE ; u = termc ; RIGHT_PAR { Lambda.to_app t u } +| LAMBDA ; l = nonempty_list(VAR) ; DOT; t = termc { Lambda.to_lambda l t } +| LEFT_PAR ; t = termc ; u = termc ; RIGHT_PAR { Lambda.to_app t u } | LEFT_PAR ; t = termc ; RIGHT_PAR { t } -(*| tu = separated_pair (termc, SPACE, termc) {let (t, u) = tu in Lambda.to_app t u }*) - -(* %inline sp: -| SPACE { ( ) } *) \ No newline at end of file