parsing working with app using (), main can eval using cbn, cbv and lo

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

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 

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 }

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 <lambda term>" ^ tab 2 ^ "Displays the written lambda with the pretty printer");
+	print_endline ("cbn -f <filename>" ^ tab 2 ^ "Eval the lambda term <filename> using call by name strategy");
+   print_endline ("cbv -f <filename>" ^ tab 2 ^ "Eval the lambda term <filename> using call by value strategy");
+   print_endline ("lo -f <filename>" ^ tab 2 ^ "Eval the lambda term <filename> 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

lambda/parser.mly

@@ -0,0 +1,25 @@
+%token LEFT_PAR RIGHT_PAR
+%token <string> VAR
+%token DOT
+%token LAMBDA
+%token SPACE
+%left SPACE
+%token END
+
+%start <Lambda.term> 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 { ( ) } *)

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)