From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 22 May 2018 06:20:30 +0000 (+0200)
Subject: add strictness
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=a02241a0882b32366d90e5f49029ab567cb434cf;p=lambda.git

add strictness
---

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 <stdio.h>
 #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);
 	}
 }