From 13586cbafa1364f30d9e0f757d1fdfd21aba24ed Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Tue, 15 May 2018 16:45:02 +0200 Subject: [PATCH] Initial commit --- .gitignore | 4 + Makefile | 12 ++ lambda.h | 28 ++++ lambda.l | 24 +++ lambda.y | 92 ++++++++++ lambda.yy.h | 474 ++++++++++++++++++++++++++++++++++++++++++++++++++++ main.c | 24 +++ mem.c | 22 +++ mem.h | 7 + print.c | 30 ++++ print.h | 7 + reduce.c | 81 +++++++++ reduce.h | 7 + 13 files changed, 812 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 lambda.h create mode 100644 lambda.l create mode 100644 lambda.y create mode 100644 lambda.yy.h create mode 100644 main.c create mode 100644 mem.c create mode 100644 mem.h create mode 100644 print.c create mode 100644 print.h create mode 100644 reduce.c create mode 100644 reduce.h 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 +#include +#include + +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 +#include +#include +#include + +/* end standard C headers. */ + +/* flex integer type definitions */ + +#ifndef FLEXINT_H +#define FLEXINT_H + +/* C99 systems have . 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 +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 +#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 + +#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 +#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 +#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 +#include +#include +#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 -- 2.20.1