From: Mart Lubbers <mart@martlubbers.net>
Date: Fri, 18 May 2018 08:15:53 +0000 (+0200)
Subject: literals
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=c3fa6b6846bb6170c2db7eb169091d2db41ff035;p=lambda.git

literals
---

diff --git a/lambda.h b/lambda.h
index a1b2ff3..457e5cf 100644
--- a/lambda.h
+++ b/lambda.h
@@ -4,6 +4,7 @@
 #include <stdio.h>
 #include <string.h>
 #include <stdlib.h>
+#include <stdbool.h>
 
 enum lambda_which {lambda_ident, lambda_abs, lambda_app};
 struct lambda {
@@ -34,6 +35,8 @@ struct decllist {
 struct lambda *make_ident(char *);
 struct lambda *make_abstraction(char *, struct lambda *);
 struct lambda *make_application(struct lambda *, struct lambda *);
+struct lambda *make_numeral(unsigned int i);
+struct lambda *make_bool(bool b);
 void decls_free();
 void decls_print();
 #define YYSTYPE struct lambda *
diff --git a/lambda.l b/lambda.l
index 689b5a4..2c74444 100644
--- a/lambda.l
+++ b/lambda.l
@@ -16,6 +16,9 @@
 \.        return DOT;
 \(        return OBRACE;
 \)        return CBRACE;
+true      yylval = make_bool(true); return LITERAL;
+false     yylval = make_bool(false); return LITERAL;
+[0-9]+    yylval = make_numeral(atoi(yytext)); return LITERAL;
 [a-z]+    yylval = make_ident(yytext); return IDENT;
 [A-Z]+    yylval = make_ident(yytext); return FUNC;
 
diff --git a/lambda.y b/lambda.y
index b7e51a8..a9b0f14 100644
--- a/lambda.y
+++ b/lambda.y
@@ -53,6 +53,21 @@ struct lambda *make_application(struct lambda *t1, struct lambda *t2)
 	return r;
 }
 
+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));
+}
+
+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")));
+}
+
 void decls_prepend(char *ident, struct lambda *value)
 {
 	struct decllist *head = malloc(sizeof (struct decllist));
@@ -109,7 +124,7 @@ void decls_free()
 
 %}
 
-%token LAMBDA DOT OBRACE CBRACE IDENT FUNC SEMICOLON ASSIGN
+%token LAMBDA DOT OBRACE CBRACE IDENT FUNC SEMICOLON ASSIGN LITERAL
 
 %%
 
@@ -129,7 +144,9 @@ term
 	| appterm
 		{ $$ = $1; }
 appterm
-	: FUNC
+	: LITERAL
+		{ $$ = $1; }
+	| FUNC
 		{
 			$$ = decls_lookup($1->data.identifier.ident);
 			lambda_free($1);
diff --git a/preamble b/preamble
index 2861a88..390bc00 100644
--- a/preamble
+++ b/preamble
@@ -7,7 +7,19 @@ 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 f x.m(n f)x;
+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;
+
+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/reduce.c b/reduce.c
index 65610e5..8ba8583 100644
--- a/reduce.c
+++ b/reduce.c
@@ -80,6 +80,8 @@ 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){
 			lambda_print(total, t);
 			printf("β -> ");
@@ -94,5 +96,8 @@ 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);
 	}
 }