From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 15 May 2018 14:45:02 +0000 (+0200)
Subject: Initial commit
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=13586cbafa1364f30d9e0f757d1fdfd21aba24ed;p=lambda.git

Initial commit
---

13586cbafa1364f30d9e0f757d1fdfd21aba24ed
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..4f9401d
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,4 @@
+lambda
+*.tab.[ch]
+*.o
+*.yy.[ch]
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..04aacd6
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,12 @@
+CFLAGS:=-g -Wall -Werror -Wextra
+lambda: lambda.tab.o lambda.yy.o main.o print.o mem.o reduce.o
+	$(LINK.c) $(LDLIBS) $^ $(OUTPUT_OPTION)
+
+%.tab.c: %.y
+	$(YACC.y) -db $(basename $<) $<
+
+%.yy.c: %.l
+	$(LEX) --header-file=$*.yy.h $(OUTPUT_OPTION) $<
+
+clean:
+	$(RM) lambda *.o *.tab.[ch] *.yy.c
diff --git a/lambda.h b/lambda.h
new file mode 100644
index 0000000..2495f9d
--- /dev/null
+++ b/lambda.h
@@ -0,0 +1,28 @@
+#ifndef LAMBDA_H
+#define LAMBDA_H
+
+#include <stdio.h>
+#include <string.h>
+#include <stdlib.h>
+
+enum lambda_which {lambda_ident, lambda_abs, lambda_app};
+struct lambda {
+	enum lambda_which which;
+	union {
+		char *identifier;
+		struct {
+			char *ident;
+			struct lambda *expr;
+		} abstraction;
+		struct {
+			struct lambda *expr1;
+			struct lambda *expr2;
+		} application;
+	} data;
+};
+
+struct lambda *make_ident(char *);
+struct lambda *make_abstraction(char *, struct lambda *);
+struct lambda *make_application(struct lambda *, struct lambda *);
+#define YYSTYPE struct lambda *
+#endif
diff --git a/lambda.l b/lambda.l
new file mode 100644
index 0000000..b37d888
--- /dev/null
+++ b/lambda.l
@@ -0,0 +1,24 @@
+%option noinput
+%option nounput
+%{
+
+#include "lambda.h"
+#include "lambda.tab.h"
+
+%}
+
+%%
+
+[ \t\n]
+(\\|λ)    return LAMBDA;
+\.        return DOT;
+\(        return OBRACE;
+\)        return CBRACE;
+I         return I;
+K         return K;
+S         return S;
+F         return F;
+T         return T;
+[a-zA-Z]+ yylval = make_ident(strdup(yytext)); return IDENT;
+
+%%
diff --git a/lambda.y b/lambda.y
new file mode 100644
index 0000000..4d47f9b
--- /dev/null
+++ b/lambda.y
@@ -0,0 +1,92 @@
+%{
+#include "lambda.h"
+#include "lambda.tab.h"
+#include "mem.h"
+
+struct lambda *result;
+extern int yylex();
+
+int yydebug=1;
+void yyerror(const char *str)
+{
+	fprintf(stderr, "parse error: %s\n", str);
+}
+
+int yywrap()
+{
+	return 1;
+}
+
+struct lambda *make_lambda()
+{
+	return malloc(sizeof (struct lambda));
+}
+
+struct lambda *make_ident(char *i)
+{
+	struct lambda *r = make_lambda();
+	r->which = lambda_ident;
+	r->data.identifier = strdup(i);
+	return r;
+}
+
+struct lambda *make_abstraction(char *i, struct lambda *t)
+{
+	struct lambda *r = make_lambda();
+	r->which = lambda_abs;
+	r->data.abstraction.ident = strdup(i);
+	r->data.abstraction.expr = t;
+	return r;
+}
+
+struct lambda *make_application(struct lambda *t1, struct lambda *t2)
+{
+	struct lambda *r = make_lambda();
+	r->which = lambda_app;
+	r->data.application.expr1 = t1;
+	r->data.application.expr2 = t2;
+	return r;
+}
+
+%}
+
+%token LAMBDA DOT OBRACE CBRACE IDENT I K S T F
+
+%%
+
+lambda
+	: term
+		{ result = $$; }
+term
+	: term appterm
+		{
+			$$ = make_application($1, $2);
+		}
+	| appterm
+		{ $$ = $1; }
+appterm
+	: IDENT
+		{
+			$$ = make_ident($1->data.identifier);
+			lambda_free($1);
+		}
+	| LAMBDA IDENT DOT term
+		{
+			$$ = make_abstraction($2->data.identifier, $4);
+			lambda_free($2);
+		}
+	| OBRACE term CBRACE
+		{ $$ = $2; }
+	| I
+		{ $$ = make_abstraction("x", make_ident("x")); }
+	| K
+		{ $$ = make_abstraction("x", make_abstraction("y", make_ident("x"))); }
+	| S
+		{ $$ = make_abstraction("x", make_abstraction("y", make_abstraction("z",
+			make_application(make_application(make_ident("x"), make_ident("y")),
+				make_application(make_ident("y"), make_ident("z"))))));
+		}
+	| T
+		{ $$ = make_abstraction("x", make_abstraction("y", make_ident("x"))); }
+	| F
+		{ $$ = make_abstraction("x", make_abstraction("y", make_ident("y"))); }
diff --git a/lambda.yy.h b/lambda.yy.h
new file mode 100644
index 0000000..63c1936
--- /dev/null
+++ b/lambda.yy.h
@@ -0,0 +1,474 @@
+#ifndef yyHEADER_H
+#define yyHEADER_H 1
+#define yyIN_HEADER 1
+
+#line 6 "lambda.yy.h"
+
+#line 8 "lambda.yy.h"
+
+#define  YY_INT_ALIGNED short int
+
+/* A lexical scanner generated by flex */
+
+#define FLEX_SCANNER
+#define YY_FLEX_MAJOR_VERSION 2
+#define YY_FLEX_MINOR_VERSION 6
+#define YY_FLEX_SUBMINOR_VERSION 4
+#if YY_FLEX_SUBMINOR_VERSION > 0
+#define FLEX_BETA
+#endif
+
+/* First, we deal with  platform-specific or compiler-specific issues. */
+
+/* begin standard C headers. */
+#include <stdio.h>
+#include <string.h>
+#include <errno.h>
+#include <stdlib.h>
+
+/* end standard C headers. */
+
+/* flex integer type definitions */
+
+#ifndef FLEXINT_H
+#define FLEXINT_H
+
+/* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */
+
+#if defined (__STDC_VERSION__) && __STDC_VERSION__ >= 199901L
+
+/* C99 says to define __STDC_LIMIT_MACROS before including stdint.h,
+ * if you want the limit (max/min) macros for int types. 
+ */
+#ifndef __STDC_LIMIT_MACROS
+#define __STDC_LIMIT_MACROS 1
+#endif
+
+#include <inttypes.h>
+typedef int8_t flex_int8_t;
+typedef uint8_t flex_uint8_t;
+typedef int16_t flex_int16_t;
+typedef uint16_t flex_uint16_t;
+typedef int32_t flex_int32_t;
+typedef uint32_t flex_uint32_t;
+#else
+typedef signed char flex_int8_t;
+typedef short int flex_int16_t;
+typedef int flex_int32_t;
+typedef unsigned char flex_uint8_t; 
+typedef unsigned short int flex_uint16_t;
+typedef unsigned int flex_uint32_t;
+
+/* Limits of integral types. */
+#ifndef INT8_MIN
+#define INT8_MIN               (-128)
+#endif
+#ifndef INT16_MIN
+#define INT16_MIN              (-32767-1)
+#endif
+#ifndef INT32_MIN
+#define INT32_MIN              (-2147483647-1)
+#endif
+#ifndef INT8_MAX
+#define INT8_MAX               (127)
+#endif
+#ifndef INT16_MAX
+#define INT16_MAX              (32767)
+#endif
+#ifndef INT32_MAX
+#define INT32_MAX              (2147483647)
+#endif
+#ifndef UINT8_MAX
+#define UINT8_MAX              (255U)
+#endif
+#ifndef UINT16_MAX
+#define UINT16_MAX             (65535U)
+#endif
+#ifndef UINT32_MAX
+#define UINT32_MAX             (4294967295U)
+#endif
+
+#ifndef SIZE_MAX
+#define SIZE_MAX               (~(size_t)0)
+#endif
+
+#endif /* ! C99 */
+
+#endif /* ! FLEXINT_H */
+
+/* begin standard C++ headers. */
+
+/* TODO: this is always defined, so inline it */
+#define yyconst const
+
+#if defined(__GNUC__) && __GNUC__ >= 3
+#define yynoreturn __attribute__((__noreturn__))
+#else
+#define yynoreturn
+#endif
+
+/* Size of default input buffer. */
+#ifndef YY_BUF_SIZE
+#ifdef __ia64__
+/* On IA-64, the buffer size is 16k, not 8k.
+ * Moreover, YY_BUF_SIZE is 2*YY_READ_BUF_SIZE in the general case.
+ * Ditto for the __ia64__ case accordingly.
+ */
+#define YY_BUF_SIZE 32768
+#else
+#define YY_BUF_SIZE 16384
+#endif /* __ia64__ */
+#endif
+
+#ifndef YY_TYPEDEF_YY_BUFFER_STATE
+#define YY_TYPEDEF_YY_BUFFER_STATE
+typedef struct yy_buffer_state *YY_BUFFER_STATE;
+#endif
+
+#ifndef YY_TYPEDEF_YY_SIZE_T
+#define YY_TYPEDEF_YY_SIZE_T
+typedef size_t yy_size_t;
+#endif
+
+extern int yyleng;
+
+extern FILE *yyin, *yyout;
+
+#ifndef YY_STRUCT_YY_BUFFER_STATE
+#define YY_STRUCT_YY_BUFFER_STATE
+struct yy_buffer_state
+	{
+	FILE *yy_input_file;
+
+	char *yy_ch_buf;		/* input buffer */
+	char *yy_buf_pos;		/* current position in input buffer */
+
+	/* Size of input buffer in bytes, not including room for EOB
+	 * characters.
+	 */
+	int yy_buf_size;
+
+	/* Number of characters read into yy_ch_buf, not including EOB
+	 * characters.
+	 */
+	int yy_n_chars;
+
+	/* Whether we "own" the buffer - i.e., we know we created it,
+	 * and can realloc() it to grow it, and should free() it to
+	 * delete it.
+	 */
+	int yy_is_our_buffer;
+
+	/* Whether this is an "interactive" input source; if so, and
+	 * if we're using stdio for input, then we want to use getc()
+	 * instead of fread(), to make sure we stop fetching input after
+	 * each newline.
+	 */
+	int yy_is_interactive;
+
+	/* Whether we're considered to be at the beginning of a line.
+	 * If so, '^' rules will be active on the next match, otherwise
+	 * not.
+	 */
+	int yy_at_bol;
+
+    int yy_bs_lineno; /**< The line count. */
+    int yy_bs_column; /**< The column count. */
+
+	/* Whether to try to fill the input buffer when we reach the
+	 * end of it.
+	 */
+	int yy_fill_buffer;
+
+	int yy_buffer_status;
+
+	};
+#endif /* !YY_STRUCT_YY_BUFFER_STATE */
+
+void yyrestart ( FILE *input_file  );
+void yy_switch_to_buffer ( YY_BUFFER_STATE new_buffer  );
+YY_BUFFER_STATE yy_create_buffer ( FILE *file, int size  );
+void yy_delete_buffer ( YY_BUFFER_STATE b  );
+void yy_flush_buffer ( YY_BUFFER_STATE b  );
+void yypush_buffer_state ( YY_BUFFER_STATE new_buffer  );
+void yypop_buffer_state ( void );
+
+YY_BUFFER_STATE yy_scan_buffer ( char *base, yy_size_t size  );
+YY_BUFFER_STATE yy_scan_string ( const char *yy_str  );
+YY_BUFFER_STATE yy_scan_bytes ( const char *bytes, int len  );
+
+void *yyalloc ( yy_size_t  );
+void *yyrealloc ( void *, yy_size_t  );
+void yyfree ( void *  );
+
+/* Begin user sect3 */
+
+extern int yylineno;
+
+extern char *yytext;
+#ifdef yytext_ptr
+#undef yytext_ptr
+#endif
+#define yytext_ptr yytext
+
+#ifdef YY_HEADER_EXPORT_START_CONDITIONS
+#define INITIAL 0
+
+#endif
+
+#ifndef YY_NO_UNISTD_H
+/* Special case for "unistd.h", since it is non-ANSI. We include it way
+ * down here because we want the user's section 1 to have been scanned first.
+ * The user has a chance to override it with an option.
+ */
+#include <unistd.h>
+#endif
+
+#ifndef YY_EXTRA_TYPE
+#define YY_EXTRA_TYPE void *
+#endif
+
+/* Accessor methods to globals.
+   These are made visible to non-reentrant scanners for convenience. */
+
+int yylex_destroy ( void );
+
+int yyget_debug ( void );
+
+void yyset_debug ( int debug_flag  );
+
+YY_EXTRA_TYPE yyget_extra ( void );
+
+void yyset_extra ( YY_EXTRA_TYPE user_defined  );
+
+FILE *yyget_in ( void );
+
+void yyset_in  ( FILE * _in_str  );
+
+FILE *yyget_out ( void );
+
+void yyset_out  ( FILE * _out_str  );
+
+			int yyget_leng ( void );
+
+char *yyget_text ( void );
+
+int yyget_lineno ( void );
+
+void yyset_lineno ( int _line_number  );
+
+/* Macros after this point can all be overridden by user definitions in
+ * section 1.
+ */
+
+#ifndef YY_SKIP_YYWRAP
+#ifdef __cplusplus
+extern "C" int yywrap ( void );
+#else
+extern int yywrap ( void );
+#endif
+#endif
+
+#ifndef yytext_ptr
+static void yy_flex_strncpy ( char *, const char *, int );
+#endif
+
+#ifdef YY_NEED_STRLEN
+static int yy_flex_strlen ( const char * );
+#endif
+
+#ifndef YY_NO_INPUT
+
+#endif
+
+/* Amount of stuff to slurp up with each read. */
+#ifndef YY_READ_BUF_SIZE
+#ifdef __ia64__
+/* On IA-64, the buffer size is 16k, not 8k */
+#define YY_READ_BUF_SIZE 16384
+#else
+#define YY_READ_BUF_SIZE 8192
+#endif /* __ia64__ */
+#endif
+
+/* Number of entries by which start-condition stack grows. */
+#ifndef YY_START_STACK_INCR
+#define YY_START_STACK_INCR 25
+#endif
+
+/* Default declaration of generated scanner - a define so the user can
+ * easily add parameters.
+ */
+#ifndef YY_DECL
+#define YY_DECL_IS_OURS 1
+
+extern int yylex (void);
+
+#define YY_DECL int yylex (void)
+#endif /* !YY_DECL */
+
+/* yy_get_previous_state - get the state just before the EOB char was reached */
+
+#undef YY_NEW_FILE
+#undef YY_FLUSH_BUFFER
+#undef yy_set_bol
+#undef yy_new_buffer
+#undef yy_set_interactive
+#undef YY_DO_BEFORE_ACTION
+
+#ifdef YY_DECL_IS_OURS
+#undef YY_DECL_IS_OURS
+#undef YY_DECL
+#endif
+
+#ifndef yy_create_buffer_ALREADY_DEFINED
+#undef yy_create_buffer
+#endif
+#ifndef yy_delete_buffer_ALREADY_DEFINED
+#undef yy_delete_buffer
+#endif
+#ifndef yy_scan_buffer_ALREADY_DEFINED
+#undef yy_scan_buffer
+#endif
+#ifndef yy_scan_string_ALREADY_DEFINED
+#undef yy_scan_string
+#endif
+#ifndef yy_scan_bytes_ALREADY_DEFINED
+#undef yy_scan_bytes
+#endif
+#ifndef yy_init_buffer_ALREADY_DEFINED
+#undef yy_init_buffer
+#endif
+#ifndef yy_flush_buffer_ALREADY_DEFINED
+#undef yy_flush_buffer
+#endif
+#ifndef yy_load_buffer_state_ALREADY_DEFINED
+#undef yy_load_buffer_state
+#endif
+#ifndef yy_switch_to_buffer_ALREADY_DEFINED
+#undef yy_switch_to_buffer
+#endif
+#ifndef yypush_buffer_state_ALREADY_DEFINED
+#undef yypush_buffer_state
+#endif
+#ifndef yypop_buffer_state_ALREADY_DEFINED
+#undef yypop_buffer_state
+#endif
+#ifndef yyensure_buffer_stack_ALREADY_DEFINED
+#undef yyensure_buffer_stack
+#endif
+#ifndef yylex_ALREADY_DEFINED
+#undef yylex
+#endif
+#ifndef yyrestart_ALREADY_DEFINED
+#undef yyrestart
+#endif
+#ifndef yylex_init_ALREADY_DEFINED
+#undef yylex_init
+#endif
+#ifndef yylex_init_extra_ALREADY_DEFINED
+#undef yylex_init_extra
+#endif
+#ifndef yylex_destroy_ALREADY_DEFINED
+#undef yylex_destroy
+#endif
+#ifndef yyget_debug_ALREADY_DEFINED
+#undef yyget_debug
+#endif
+#ifndef yyset_debug_ALREADY_DEFINED
+#undef yyset_debug
+#endif
+#ifndef yyget_extra_ALREADY_DEFINED
+#undef yyget_extra
+#endif
+#ifndef yyset_extra_ALREADY_DEFINED
+#undef yyset_extra
+#endif
+#ifndef yyget_in_ALREADY_DEFINED
+#undef yyget_in
+#endif
+#ifndef yyset_in_ALREADY_DEFINED
+#undef yyset_in
+#endif
+#ifndef yyget_out_ALREADY_DEFINED
+#undef yyget_out
+#endif
+#ifndef yyset_out_ALREADY_DEFINED
+#undef yyset_out
+#endif
+#ifndef yyget_leng_ALREADY_DEFINED
+#undef yyget_leng
+#endif
+#ifndef yyget_text_ALREADY_DEFINED
+#undef yyget_text
+#endif
+#ifndef yyget_lineno_ALREADY_DEFINED
+#undef yyget_lineno
+#endif
+#ifndef yyset_lineno_ALREADY_DEFINED
+#undef yyset_lineno
+#endif
+#ifndef yyget_column_ALREADY_DEFINED
+#undef yyget_column
+#endif
+#ifndef yyset_column_ALREADY_DEFINED
+#undef yyset_column
+#endif
+#ifndef yywrap_ALREADY_DEFINED
+#undef yywrap
+#endif
+#ifndef yyget_lval_ALREADY_DEFINED
+#undef yyget_lval
+#endif
+#ifndef yyset_lval_ALREADY_DEFINED
+#undef yyset_lval
+#endif
+#ifndef yyget_lloc_ALREADY_DEFINED
+#undef yyget_lloc
+#endif
+#ifndef yyset_lloc_ALREADY_DEFINED
+#undef yyset_lloc
+#endif
+#ifndef yyalloc_ALREADY_DEFINED
+#undef yyalloc
+#endif
+#ifndef yyrealloc_ALREADY_DEFINED
+#undef yyrealloc
+#endif
+#ifndef yyfree_ALREADY_DEFINED
+#undef yyfree
+#endif
+#ifndef yytext_ALREADY_DEFINED
+#undef yytext
+#endif
+#ifndef yyleng_ALREADY_DEFINED
+#undef yyleng
+#endif
+#ifndef yyin_ALREADY_DEFINED
+#undef yyin
+#endif
+#ifndef yyout_ALREADY_DEFINED
+#undef yyout
+#endif
+#ifndef yy_flex_debug_ALREADY_DEFINED
+#undef yy_flex_debug
+#endif
+#ifndef yylineno_ALREADY_DEFINED
+#undef yylineno
+#endif
+#ifndef yytables_fload_ALREADY_DEFINED
+#undef yytables_fload
+#endif
+#ifndef yytables_destroy_ALREADY_DEFINED
+#undef yytables_destroy
+#endif
+#ifndef yyTABLES_NAME_ALREADY_DEFINED
+#undef yyTABLES_NAME
+#endif
+
+#line 24 "lambda.l"
+
+
+#line 473 "lambda.yy.h"
+#undef yyIN_HEADER
+#endif /* yyHEADER_H */
diff --git a/main.c b/main.c
new file mode 100644
index 0000000..1899d67
--- /dev/null
+++ b/main.c
@@ -0,0 +1,24 @@
+#include <stdio.h>
+
+#include "lambda.h"
+#include "lambda.tab.h"
+#include "lambda.yy.h"
+#include "reduce.h"
+#include "print.h"
+#include "mem.h"
+
+extern struct lambda *result;
+
+int main(int argc, char **argv)
+{
+	int r = yyparse();
+	int maxdepth = 1000;
+	if(r == 0){
+		printf("   ");
+		lambda_print(result);
+		lambda_reduce(result, result, &maxdepth);
+		lambda_free(result);
+	}
+	yylex_destroy();
+	return r;
+}
diff --git a/mem.c b/mem.c
new file mode 100644
index 0000000..19c5c8e
--- /dev/null
+++ b/mem.c
@@ -0,0 +1,22 @@
+#include <stdlib.h>
+#include "lambda.h"
+
+void lambda_free(struct lambda *t)
+{
+	if(t != NULL){
+		switch(t->which){
+		case lambda_ident:
+			free(t->data.identifier);
+			break;
+		case lambda_abs:
+			free(t->data.abstraction.ident);
+			lambda_free(t->data.abstraction.expr);
+			break;
+		case lambda_app:
+			lambda_free(t->data.application.expr1);
+			lambda_free(t->data.application.expr2);
+			break;
+		}
+	}
+	free(t);
+}
diff --git a/mem.h b/mem.h
new file mode 100644
index 0000000..0cbce0d
--- /dev/null
+++ b/mem.h
@@ -0,0 +1,7 @@
+#ifndef MEM_H
+#define MEM_H
+
+#include "lambda.h"
+
+void lambda_free(struct lambda *);
+#endif
diff --git a/print.c b/print.c
new file mode 100644
index 0000000..fb209f4
--- /dev/null
+++ b/print.c
@@ -0,0 +1,30 @@
+#include <stdio.h>
+#include "lambda.h"
+
+void term_print(struct lambda *t)
+{
+	switch(t->which){
+	case lambda_ident:
+		printf("%s", t->data.identifier);
+		break;
+	case lambda_abs:
+		printf("(λ");
+		printf("%s", t->data.abstraction.ident);
+		putchar('.');
+		term_print(t->data.abstraction.expr);
+		putchar(')');
+		break;
+	case lambda_app:
+		putchar('(');
+		term_print(t->data.application.expr1);
+		term_print(t->data.application.expr2);
+		putchar(')');
+		break;
+	}
+}
+
+void lambda_print(struct lambda *t)
+{
+	term_print(t);
+	putchar('\n');
+}
diff --git a/print.h b/print.h
new file mode 100644
index 0000000..2f40e36
--- /dev/null
+++ b/print.h
@@ -0,0 +1,7 @@
+#ifndef PRINT_H
+#define PRINT_H
+
+#include "lambda.h"
+
+void lambda_print(struct lambda *);
+#endif
diff --git a/reduce.c b/reduce.c
new file mode 100644
index 0000000..79cde99
--- /dev/null
+++ b/reduce.c
@@ -0,0 +1,81 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include "lambda.h"
+#include "print.h"
+#include "mem.h"
+
+struct lambda *copy(struct lambda *t)
+{
+	struct lambda *c = malloc(sizeof (struct lambda));
+	c->which = t->which;
+	switch(t->which){
+	case lambda_ident:
+		c->data.identifier = strdup(t->data.identifier);
+		break;
+	case lambda_abs:
+		c->data.abstraction.ident = strdup(t->data.abstraction.ident);
+		c->data.abstraction.expr = copy(t->data.abstraction.expr);
+		break;
+	case lambda_app:
+		c->data.application.expr1 = copy(t->data.application.expr1);
+		c->data.application.expr2 = copy(t->data.application.expr2);
+		break;
+	}
+	return c;
+}
+
+void subst(char *ident, struct lambda *t1, struct lambda *t2, struct lambda *total)
+{
+	struct lambda cpy;
+	switch(t1->which){
+	case lambda_ident:
+		if(strcmp(t1->data.identifier, ident) == 0){
+			cpy = *copy(t2);
+			free(t1->data.identifier);
+			if(total == t1)
+				*total = cpy;
+			*t1 = cpy;
+		}
+		break;
+	case lambda_abs:
+		if(strcmp(t1->data.abstraction.ident, ident) != 0)
+			subst(ident, t1->data.abstraction.expr, t2, total);
+		break;
+	case lambda_app:
+		subst(ident, t1->data.application.expr1, t2, total);
+		subst(ident, t1->data.application.expr2, t2, total);
+		break;
+	}
+
+}
+
+void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth)
+{
+	if(*maxdepth == 0)
+		return;
+	struct lambda *t1, *t2;
+	switch(t->which){
+	case lambda_ident:
+		break;
+	case lambda_abs:
+		lambda_reduce(t->data.abstraction.expr, total, maxdepth);
+		break;
+	case lambda_app:
+		//If the first argument is an abstraction, we apply
+		t1 = t->data.application.expr1;
+		t2 = t->data.application.expr2;
+		lambda_reduce(t1, total, maxdepth);
+		lambda_reduce(t2, total, maxdepth);
+		if(t1->which == lambda_abs){
+			subst(t1->data.abstraction.ident, t1->data.abstraction.expr, t2, total);
+			(*maxdepth)--;
+			if(total == t)
+				*total = *t1->data.abstraction.expr;
+			printf("-> ");
+			lambda_print(total);
+			lambda_reduce(t, total, maxdepth);
+		}
+		break;
+	}
+}
diff --git a/reduce.h b/reduce.h
new file mode 100644
index 0000000..9d9fa54
--- /dev/null
+++ b/reduce.h
@@ -0,0 +1,7 @@
+#ifndef REDUCE_H
+#define REDUCE_H
+
+#include "lambda.h"
+
+void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth);
+#endif