From ae34fa688ddce966fd3e63c149405145de936b1f Mon Sep 17 00:00:00 2001 From: julia Date: Sun, 25 Jun 2023 12:07:21 +0200 Subject: [PATCH] parsing working with app using (), main can eval using cbn, cbv and lo --- lambda/Makefile | 26 +++++++++ lambda/lambda.ml | 144 ++++++++++++++++++++++++++++++++++++++++++++++ lambda/lexer.mll | 18 ++++++ lambda/main.ml | 100 ++++++++++++++++++++++++++++++++ lambda/parser.mly | 25 ++++++++ lambda/tools.ml | 21 +++++++ 6 files changed, 334 insertions(+) create mode 100644 lambda/Makefile create mode 100644 lambda/lambda.ml create mode 100644 lambda/lexer.mll create mode 100644 lambda/main.ml create mode 100644 lambda/parser.mly create mode 100644 lambda/tools.ml diff --git a/lambda/Makefile b/lambda/Makefile new file mode 100644 index 0000000..a781fab --- /dev/null +++ b/lambda/Makefile @@ -0,0 +1,26 @@ +CC = ocamlc +MAIN = main + +all: $(MAIN) + +$(MAIN): tools.cmo lambda.cmo parser.cmo lexer.cmo main.cmo + $(CC) $^ -o $(MAIN) + +parser.ml: parser.mly + menhir --infer $^ + $(CC) -c parser.mli + +lexer.ml: lexer.mll + ocamllex $^ + +%.cmo: %.ml + $(CC) -c $^ + +%.cmi: %.mli + $(CC) -c $^ + +.PHONY: clean + +clean: + @echo "Project clean." + @rm -rf *.cmi *.cmo *.cmx *.mli *.o parser.ml lexer.ml parser.conflicts main \ No newline at end of file diff --git a/lambda/lambda.ml b/lambda/lambda.ml new file mode 100644 index 0000000..096799b --- /dev/null +++ b/lambda/lambda.ml @@ -0,0 +1,144 @@ +(*Terme du Lambda-Calcul*) +type term = + | Var of string + | Lambda of string * term + | App of term * term + + +let to_var x = Var x + +let to_lambda x t = Lambda (x, t) + +let to_app t u = App (t, u) + +(*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/lexer.mll b/lambda/lexer.mll new file mode 100644 index 0000000..97c8eef --- /dev/null +++ b/lambda/lexer.mll @@ -0,0 +1,18 @@ +{ + open Parser + exception Eof +} + +let var_id = ['a'-'z' 'A'-'Z' '0'-'9']+ +let space = [' ' '\t']+ +let newline = '\r' | '\n' | "\r\n" + +rule read = parse + | var_id { VAR (Lexing.lexeme lexbuf) } + | '(' { LEFT_PAR } + | ')' { RIGHT_PAR } + | '.' { DOT } + | '\\' { LAMBDA } + | space { SPACE } + | newline { read lexbuf } + | eof { exit 0 } \ No newline at end of file diff --git a/lambda/main.ml b/lambda/main.ml new file mode 100644 index 0000000..9aa36bc --- /dev/null +++ b/lambda/main.ml @@ -0,0 +1,100 @@ +open Lambda +open Parser +open Tools + +(* --------------------------------------- + Prompt + --------------------------------------- *) + +let welcome () = print_endline "Use 'help' for the list of commands." + +let tab = repeat_string "\t" + +let line = repeat_string "-" + +let commands_list () = + print_endline ("Command" ^ tab 4 ^ "Description (shortcut)"); + print_endline (line 70); + print_endline ("exit" ^ tab 4 ^ "Exits the program"); + print_endline ("display " ^ tab 2 ^ "Displays the written lambda with the pretty printer"); + print_endline ("cbn -f " ^ tab 2 ^ "Eval the lambda term using call by name strategy"); + print_endline ("cbv -f " ^ tab 2 ^ "Eval the lambda term using call by value strategy"); + print_endline ("lo -f " ^ tab 2 ^ "Eval the lambda term using the lo reduction strategy") + +let prompt () = print_string "> " +let last_command : string option ref = ref None + +(* --------------------------------------- + Main function + --------------------------------------- *) + +let _ = + welcome (); + while true do + prompt (); + let input = read_line () in + begin match String.split_on_char ' ' input with + | ["exit"] -> exit 0 + | ["help"] -> commands_list () + (*| _ as string_list -> + let lexbuf = Lexing.from_string (String.concat " " string_list) in + (try + let t = termc Lexer.read lexbuf in + (* print_endline (String.concat " " string_list); *) + print_endline (string_of_term t) + with _ -> print_endline "Syntax error. Please try again.")*) + | "display"::string_list -> + let lexbuf = Lexing.from_string (String.concat " " string_list) in + (try + let t = termc Lexer.read lexbuf in + print_endline (string_of_term t) + with _ -> print_endline "Syntax error. Please try again.") + | ["cbn"; "-f"; filename] -> + begin try + let lexbuf = Lexing.from_channel (open_in filename) in + let t = termc Lexer.read lexbuf in + let result = cbn_eval t in + print_endline (string_of_term result) + with Sys_error f -> print_endline f + end + | ["cbv"; "-f"; filename] -> + begin try + let lexbuf = Lexing.from_channel (open_in filename) in + let t = termc Lexer.read lexbuf in + let result = cbv_eval t in + print_endline (string_of_term result) + with Sys_error f -> print_endline f + end + | ["lo"; "-f"; filename] -> + begin try + let lexbuf = Lexing.from_channel (open_in filename) in + let t = termc Lexer.read lexbuf in + let result = lo_eval t in + print_endline (string_of_term result) + with Sys_error f -> print_endline f + end + | "cbn"::string_list -> + let lexbuf = Lexing.from_string (String.concat " " string_list) in + (try + let t = termc Lexer.read lexbuf in + let result = cbn_eval t in + print_endline (string_of_term result) + with _ -> print_endline "Syntax error. Please try again.") + | "cbv"::string_list -> + let lexbuf = Lexing.from_string (String.concat " " string_list) in + (try + let t = termc Lexer.read lexbuf in + let result = cbv_eval t in + print_endline (string_of_term result) + with _ -> print_endline "Syntax error. Please try again.") + | "lo"::string_list -> + let lexbuf = Lexing.from_string (String.concat " " string_list) in + (try + let t = termc Lexer.read lexbuf in + let result = lo_eval t in + print_endline (string_of_term result) + with _ -> print_endline "Syntax error. Please try again.") + | _ -> + print_endline "Invalid command. Please type 'help' for the list of commands." + end + done \ No newline at end of file diff --git a/lambda/parser.mly b/lambda/parser.mly new file mode 100644 index 0000000..19ae50f --- /dev/null +++ b/lambda/parser.mly @@ -0,0 +1,25 @@ +%token LEFT_PAR RIGHT_PAR +%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 } +| 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 diff --git a/lambda/tools.ml b/lambda/tools.ml new file mode 100644 index 0000000..2196aad --- /dev/null +++ b/lambda/tools.ml @@ -0,0 +1,21 @@ +(* --------------------------------------- + Few useful functions + --------------------------------------- *) + +let lift_pairl f (x, y) = (f x, y) +let lift_pairr f (x, y) = (x, f y) +let lift_pair f p = lift_pairr f (lift_pairl f p) + +let rec repeat_string s n = if n=0 then "" else s ^ repeat_string s (n-1) + +let foldi_left f acc l = + snd (List.fold_left (fun (i, acc') x -> (i+1, f i acc' x)) (0, acc) l) + +let without i l = foldi_left (fun j acc x -> if i=j then acc else acc@[x]) [] l + +(* --------------------------------------- + List monad (with index) + --------------------------------------- *) + +let return x = [x] +let (>>=) l f = List.flatten (List.mapi f l) \ No newline at end of file