add strictness

diff --git a/Makefile b/Makefile
index 79e13c7..55c297d 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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);
        }
 }