From a02241a0882b32366d90e5f49029ab567cb434cf Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Tue, 22 May 2018 08:20:30 +0200 Subject: [PATCH] add strictness --- Makefile | 2 +- grammar.txt | 8 +++++--- lambda.h | 3 ++- lambda.l | 1 + lambda.y | 44 ++++++++++++++++++++++++++++++-------------- mem.c | 1 + preamble | 41 ++++++++++++++++++++--------------------- print.c | 28 +++++++++++++--------------- reduce.c | 7 ++----- 9 files changed, 75 insertions(+), 60 deletions(-) diff --git a/Makefile b/Makefile index 79e13c7..55c297d 100644 --- a/Makefile +++ b/Makefile @@ -2,7 +2,7 @@ CFLAGS:=-g -Wall -Wextra -pedantic lambda: lambda.tab.o lambda.yy.o print.o mem.o reduce.o $(LINK.c) $(LDLIBS) $^ $(OUTPUT_OPTION) -%.tab.c: %.y +%.tab.c: %.y %.yy.c $(YACC.y) -db $(basename $<) $< %.yy.c: %.l diff --git a/grammar.txt b/grammar.txt index fd36183..1fab941 100644 --- a/grammar.txt +++ b/grammar.txt @@ -1,10 +1,12 @@ -program := declaration* term -declaration := func '=' term ';' +program := term ';' program + | declaration ';' program +declaration := func strictident+ '=' term ';' term := appterm term | appterm appterm := func | ident - | '\' ident+ '.' term + | '\' strictident+ '.' term | '(' term ')' +strictident := '!'? ident func := 'A' | 'B' | ... | 'Z' ident := 'a' | 'b' | ... | 'z' diff --git a/lambda.h b/lambda.h index 8256f04..ab28375 100644 --- a/lambda.h +++ b/lambda.h @@ -17,6 +17,7 @@ struct lambda { struct { char *ident; unsigned int revision; + bool strict; struct lambda *expr; } abstraction; struct { @@ -33,7 +34,7 @@ struct decllist { }; struct lambda *make_ident(char *); -struct lambda *make_abstraction(char *, struct lambda *); +struct lambda *make_abstraction(char *, bool, struct lambda *); struct lambda *make_application(struct lambda *, struct lambda *); struct lambda *make_numeral(unsigned int i); struct lambda *make_bool(bool b); diff --git a/lambda.l b/lambda.l index 2c74444..89256b4 100644 --- a/lambda.l +++ b/lambda.l @@ -16,6 +16,7 @@ \. return DOT; \( return OBRACE; \) return CBRACE; +\! return BANG; true yylval = make_bool(true); return LITERAL; false yylval = make_bool(false); return LITERAL; [0-9]+ yylval = make_numeral(atoi(yytext)); return LITERAL; diff --git a/lambda.y b/lambda.y index 813b77d..07c6b80 100644 --- a/lambda.y +++ b/lambda.y @@ -43,12 +43,13 @@ struct lambda *make_ident(char *i) return r; } -struct lambda *make_abstraction(char *i, struct lambda *t) +struct lambda *make_abstraction(char *i, bool strict, struct lambda *t) { struct lambda *r = make_lambda(); r->which = lambda_abs; r->data.abstraction.ident = strdup(i); r->data.abstraction.revision = 0; + r->data.abstraction.strict = strict; r->data.abstraction.expr = t; return r; } @@ -67,14 +68,14 @@ struct lambda *make_numeral(unsigned int i) struct lambda *body = make_ident("x"); while(i-- > 0) body = make_application(make_ident("f"), body); - return make_abstraction("f", make_abstraction("x", body)); + return make_abstraction("f", false, make_abstraction("x", false, body)); } struct lambda *make_bool(bool b) { return b - ? make_abstraction("a", make_abstraction("b", make_ident("a"))) - : make_abstraction("a", make_abstraction("b", make_ident("b"))); + ? make_abstraction("a", false, make_abstraction("b", false, make_ident("a"))) + : make_abstraction("a", false, make_abstraction("b", false, make_ident("b"))); } void decls_prepend(char *ident, struct lambda *value) @@ -106,7 +107,7 @@ int main() %} -%token LAMBDA DOT OBRACE CBRACE IDENT FUNC SEMICOLON ASSIGN LITERAL +%token LAMBDA DOT OBRACE CBRACE IDENT FUNC SEMICOLON ASSIGN LITERAL BANG %% @@ -122,11 +123,24 @@ lambda lambda_print($1, NULL); lambda_free($1); } - | FUNC ASSIGN term + | FUNC func { - decls_prepend($1->data.identifier.ident, $3); + decls_prepend($1->data.identifier.ident, $2); printf("%s = ", $1->data.identifier.ident); - lambda_print($3, NULL); + lambda_print($2, NULL); + lambda_free($1); + } +func + : ASSIGN term + { $$ = $2; } + | BANG IDENT func + { + $$ = make_abstraction($2->data.identifier.ident, true, $3); + lambda_free($2); + } + | IDENT func + { + $$ = make_abstraction($1->data.identifier.ident, false, $2); lambda_free($1); } term @@ -143,18 +157,20 @@ appterm lambda_free($1); } | IDENT - { - $$ = make_ident($1->data.identifier.ident); - lambda_free($1); - } + { $$ = $1; } | LAMBDA abstraction { $$ = $2; } | OBRACE term CBRACE { $$ = $2; } abstraction - : IDENT abstraction + : BANG IDENT abstraction + { + $$ = make_abstraction($2->data.identifier.ident, true, $3); + lambda_free($2); + } + | IDENT abstraction { - $$ = make_abstraction($1->data.identifier.ident, $2); + $$ = make_abstraction($1->data.identifier.ident, false, $2); lambda_free($1); } | DOT term diff --git a/mem.c b/mem.c index 0792a97..333038b 100644 --- a/mem.c +++ b/mem.c @@ -32,6 +32,7 @@ struct lambda *copy(struct lambda *t) break; case lambda_abs: c->data.abstraction.ident = strdup(t->data.abstraction.ident); + c->data.abstraction.strict = t->data.abstraction.strict; c->data.abstraction.expr = copy(t->data.abstraction.expr); c->data.abstraction.revision = t->data.abstraction.revision; break; diff --git a/preamble b/preamble index 390bc00..cdc65b0 100644 --- a/preamble +++ b/preamble @@ -1,25 +1,24 @@ -I=\x.x; -K=\x y.x; -S=\x y z.x y(x z); -B=\x y z.x (y z); -C=\x y z.x z y; -W=\x y.x y y; -SOMEGA=\x.x x; -OMEGA=SOMEGA SOMEGA; -Y=\g.(\x.g (x x))(\x.g (x x)); +I x = x; +K x y = x; +S x y z = x y(x z); +B x y z = x (y z); +C x y z = x z y; +W x y = x y y; +SOMEGA x = x x; +OMEGA = SOMEGA SOMEGA; +Y g = (\x.g (x x))(\x.g (x x)); -ZERO=\f x.x; -SUCC=\n f x.f(n f x); -PLUS=\m n.m SUCC n; -MULT=\m n.m (PLUS n) 0; -EXP=\b e.e b; +ZERO f !x = x; +SUCC n f x = f (n f x); +PLUS m n = m SUCC n; +MULT m n = m (PLUS n) 0; +EXP b e = e b; -PRED=\n f x.n(\g h.h(g f))(\u.x)(\u.u); -SUB=\m n.n PRED m; +PRED n f x = n(\g h.h(g f))(\u.x)(\u.u); +SUB m n = n PRED m; -ISZERO=\n.n(\x.false)true; -LEQ=\m n.ISZERO (MINUS m n); - -AND=\p q.p q p; -OR=\p.p p; +ISZERO n = n (\x.false) true; +LEQ m n = ISZERO (MINUS m n); +AND p q = p q p; +OR p = p p; diff --git a/print.c b/print.c index 6a2cba5..c50d8dc 100644 --- a/print.c +++ b/print.c @@ -1,6 +1,14 @@ #include #include "lambda.h" +#define PRINT_ABS(t) {\ + if(t->data.abstraction.strict)\ + putchar('!');\ + printf("%s", t->data.abstraction.ident);\ + print_apos(t->data.abstraction.revision);\ + } + + void print_apos(unsigned int revision) { if(revision == 1) @@ -11,31 +19,21 @@ void print_apos(unsigned int revision) } } -void print_ident(char *ident, unsigned int revision) -{ - printf("%s", ident); - while(revision > 2){ - putchar('\"'); - revision -= 2; - } - if(revision == 1) - putchar('\''); -} - void term_print(struct lambda *t, struct lambda *mark) { if(t == mark) putchar('|'); switch(t->which){ case lambda_ident: - print_ident(t->data.identifier.ident, t->data.identifier.revision); + printf("%s", t->data.identifier.ident); + print_apos(t->data.identifier.revision); break; case lambda_abs: printf("λ"); - print_ident(t->data.abstraction.ident, t->data.abstraction.revision); + PRINT_ABS(t); while((t = t->data.abstraction.expr)->which == lambda_abs){ putchar(' '); - print_ident(t->data.abstraction.ident, t->data.abstraction.revision); + PRINT_ABS(t); } putchar('.'); term_print(t, mark); @@ -63,5 +61,5 @@ void term_print(struct lambda *t, struct lambda *mark) void lambda_print(struct lambda *t, struct lambda *mark) { term_print(t, mark); - putchar('\n'); + printf(";\n"); } diff --git a/reduce.c b/reduce.c index 8ba8583..19c193c 100644 --- a/reduce.c +++ b/reduce.c @@ -80,9 +80,9 @@ void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth) t1 = t->data.application.expr1; t2 = t->data.application.expr2; lambda_reduce(t1, total, maxdepth); - //For applicative order - lambda_reduce(t2, total, maxdepth); if(t1->which == lambda_abs){ + if(t1->data.abstraction.strict) + lambda_reduce(t2, total, maxdepth); lambda_print(total, t); printf("β -> "); lambda_beta(t1, t1->data.abstraction.expr, t2, total); @@ -96,8 +96,5 @@ void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth) (*maxdepth)--; lambda_reduce(t, total, maxdepth); } - //For applicative order - } else if(t->which == lambda_abs) { - lambda_reduce(t->data.abstraction.expr, total, maxdepth); } } -- 2.20.1