Examples - sidprasad/sidbison GitHub Wiki

Example
Programming Computable Functions
Lambda Calculus

Programming Computable Functions

PCF is a simple typed functional language proposed by Dana Scott in 1969. A lexer and parser for PCF are presented in the pcfexample directory. This allows for simple PCF programs to be debugged in sidBison.

Specification

The example flex specification for PCF (pcf.l) looks like this:

%{
# include "pcf.tab.h"
# undef yywrap
# define yywrap() 1

%}

%option noyywrap

blank [ \t]
word [a-zA-Z][a-zA-Z0-9]*


%%
{blank}+
[\n]+
0           return ZERO;
:           return COLON;
"true"      return TRUE;
"false"     return FALSE;
\.          return DOT;
\(          return LPAREN;
\)          return RPAREN;
"fix"       return FIX;
"zero"      return ZEROFUNC;
"succ"      return SUCC;
"pred"      return PRED;
"if"        return IF;
"then"      return THEN;
"else"      return ELSE;
"fn"        return FN;
"nat"       return NAT;
"bool"      return BOOL;
"->"        return ARROW;
{word}      return IDEN;
.           {fprintf(stderr, "Invalid token!\n");}

%%

pcf.tab.h is included and is generated using the ibison -d option.

---

The provided grammar spec (pcf.y) for PCF looks like this:

%{

/* A simple PCF grammar */

%}

%token ZERO
%token TRUE
%token FALSE
%token IDEN
%token FIX
%token ZEROFUNC
%token LPAREN
%token RPAREN
%token SUCC
%token PRED
%token IF
%token THEN
%token ELSE
%token FN
%token COLON
%token DOT
%token NAT
%token ARROW
%token BOOL

%left ARROW
 
%%


m : ZERO
  | TRUE
  | FALSE
  | var
  | zerofunc
  | succ
  | pred
  | ifelse
  | fun
  | app
  | fix

fix : FIX LPAREN m RPAREN

app : LPAREN callfunc argfunc RPAREN

callfunc : m
argfunc : m


tau : NAT
	| BOOL
	| funtau
	| LPAREN funtau  RPAREN

funtau : tau ARROW tau


fun : FN var COLON tau DOT m

succ : SUCC LPAREN m RPAREN

pred : PRED LPAREN m RPAREN

zerofunc : ZEROFUNC LPAREN m RPAREN

var : IDEN

ifelse : IF m THEN m ELSE m

%%
/*

app : funcexp argexp

succ : SUCC LPAREN m RPAREN
pred : PRED LPAREN m RPAREN
fix : FIX LPAREN m RPAREN

funcexp : m
argexp : m

fix : LPAREN m RPAREN

func : FN var COLON tau DOT m

*/
void yyerror (const char *s)
{
fprintf(stderr, "Syntax error: %s\n", s);
}

---

Compiling

The code can be compiled as follows. Make sure BISON_PKGDATADIR points to the iBison data directory.

ibison -d pcf.y
flex pcf.l
gcc -c -fPIC lex.yy.c
gcc -shared -o lex.so lex.yy.o

pcf.y and lex.so can now be used as arguments to sidBison, where test can be called on any example in the pcfexample/input directory.

---

Lambda Calculus

Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It was first introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics.Wikipedia

Specification

The example flex specification for the lambda calculus (lambdacalc.l) looks like this:

%{
# include "lambdacalc.tab.h"
# undef yywrap
# define yywrap() 1

%}

%option noyywrap

blank [ \t]
word [a-zA-Z][a-zA-Z0-9]*
int [0-9]+


%%
{blank}+
[\n]+
{int}       return CONSTANT;
{word}      return IDENT;
\.          return DOT;
\\          return LAMBDA;
\(          return LPAREN;
\)          return RPAREN;
.           {fprintf(stderr, "Invalid token!\n");}

%%

lambdacalc.tab.h is included and is generated using the ibison -d option.

---

The provided grammar spec (lambdacalc.y) for PCF looks like this:

%{
/* Untyped lambda calculus */
void yyerror(const char *s);

%}

%token  IDENT
%token  CONSTANT
%token  LPAREN
%token  RPAREN
%token  LAMBDA
%token  DOT

%%

exp : var
	| func
	| app
	| CONSTANT

func : LAMBDA var DOT scope

app : LPAREN funcexp argexp  RPAREN

scope : exp

funcexp : exp

argexp : exp

var : IDENT


;

%%
void
yyerror(const char *s)
{
	fprintf(stderr, "Syntax error: %s\n", s);
}

---

Compiling

The code can be compiled as follows. Make sure BISON_PKGDATADIR points to the iBison src directory.

ibison -d lambdacalc.y
flex lambdacalc.l
gcc -c -fPIC lex.yy.c
gcc -shared -o lex.so lex.yy.o

lambdacalc.y and lex.so can now be used as arguments to sidBison, where test can be called on any example in the lambdacalcexample/input directory.