final lab preparations

git-svn-id: https://slps.svn.sourceforge.net/svnroot/slps@710 ab42f6e0-554d-0410-b580-99e487e6eeb2
grammarware · Nov 15, 2009 · f708834 · f708834
1 parent 4f979ef
commit f708834
Show file tree

Hide file tree

Showing 14 changed files with 118 additions and 61 deletions.
diff --git a/topics/exercises/README.txt b/topics/exercises/README.txt
@@ -5,4 +5,8 @@ while4	- small step semantics for While (+ a DCG parser)
 xml1	- a DCG parser for XML subset (elements only)
 xml2	- a DCG parser for XML subset (elements and attributes)
 nb1	- abstract syntax for NB
-nb1	- typed NB abstract syntax
+nb2	- semantics and types for NB
+lambda1	- lambda calculus abstract and concrete syntax in Prolog
+lambda2	- obsolete
+lambda3 - lambda calculus abstract syntax, free variables, substitution, evaluation
+
diff --git a/topics/exercises/lambda1/Makefile b/topics/exercises/lambda1/Makefile
@@ -1,6 +1,5 @@
 test:
-	swipl -f syntax.pro -t "write(term(`cat input.txt`)),nl"
-
-prompt:
-	swipl -s syntax.pro
+	swipl -f run.pro -t "main('input.txt')"
 
+clean:
+	rm -rf *~
diff --git a/topics/exercises/lambda1/input.txt b/topics/exercises/lambda1/input.txt
@@ -1 +1 @@
-lambda(f,lambda(g,lambda(x,apply(f,apply(g,x)))))
+lambda f . lambda g . lambda x . app f : app g : x
diff --git a/topics/exercises/lambda1/parser.pro b/topics/exercises/lambda1/parser.pro
@@ -0,0 +1,29 @@
+% Program is a list of statements
+expression(app(M,N)) --> keyword("app"), expression(M), keyword(":"), expression(N).
+expression(lam(X,N)) --> keyword("lambda"), name(X), keyword("."), expression(N).
+expression(var(N)) --> name(N).
+
+% Dealing with spaces
+spaces --> [0' ], spaces. %'
+spaces --> [].
+
+% Keywords are space-consuming strings
+keyword(X) -->
+ spaces,
+ string(X).
+
+% Bare strings
+string([],X,X).
+string([H|T1],[H|T2],X) :- string(T1,T2,X).
+
+% Identifiers are space-consuming letters
+name(V) -->
+ spaces,
+ letter(H),
+ { atom_chars(V,[H]) }.
+
+% Bare letters
+letters([H|T]) --> letter(H), letters(T).
+letters([]) --> [].
+letter(H,[H|T],T) :- H >= 0'a, H =< 0'z.
+
diff --git a/topics/exercises/lambda1/run.pro b/topics/exercises/lambda1/run.pro
@@ -0,0 +1,17 @@
+:- ['parser.pro','syntax.pro'].
+
+main(File) :-
+ parseFile(File,expression,E),
+ term(E),
+ write(E),nl.
+
+parseFile(File,P,R) :-
+ open(File,read,Stream,[]), 
+ read_stream_to_codes(Stream, Contents),
+ close(Stream),
+ apply(P,[R,Contents,Rest]),
+ eof(Rest,_).
+
+eof([],[]).
+eof([0' |T],R) :- eof(T,R). %'
+eof([10|T],R) :- eof(T,R).
diff --git a/topics/exercises/lambda1/syntax.pro b/topics/exercises/lambda1/syntax.pro
@@ -1,12 +1,21 @@
-% see slides #147
+% See slide 174
 
-term(x).
-term(y).
-term(z).
-term(f).
-term(g).
-term(h).
+term(var(X)) :- variable(X).
+term(app(T1,T2)) :- term(T1), term(T2).
+term(lam(X,T)) :- variable(X), term(T).
 
-term(apply(M,N)) :- term(M), term(N).
-term(lambda(X,M)) :- term(X), term(M).
+value(lam(X,T)) :- variable(X), term(T).
+value(var(X)) :- variable(X). % pragmatic extension to deal with open terms
 
+variable(a).
+variable(f).
+variable(g).
+variable(l).
+variable(m).
+variable(n).
+variable(t).
+variable(v).
+variable(w).
+variable(x).
+variable(y).
+variable(z).
diff --git a/topics/exercises/lambda2/Makefile b/topics/exercises/lambda2/Makefile
diff --git a/topics/exercises/lambda2/input.txt b/topics/exercises/lambda2/input.txt
diff --git a/topics/exercises/lambda2/syntax.pro b/topics/exercises/lambda2/syntax.pro
diff --git a/topics/exercises/lambda2/variables.pro b/topics/exercises/lambda2/variables.pro
diff --git a/topics/exercises/nb1/Makefile b/topics/exercises/nb1/Makefile
@@ -1,5 +1,5 @@
 test:
-	swipl -f syntax.pro -t "term(`cat input.txt`)"
+	swipl -f syntax.pro -t "write(term(`cat input.txt`))"
 
 prompt:
 	swipl -s syntax.pro

diff --git a/topics/exercises/nb2/Makefile b/topics/exercises/nb2/Makefile
@@ -1,4 +1,8 @@
 test:
+	swipl -f semantics.pro -t "eval(`cat input1.txt`,V,T),write(V),write(':'),write(T),nl"
+	swipl -f semantics.pro -t "eval(`cat input2.txt`,V,T),write(V),write(':'),write(T),nl"
+
+types:
 	swipl -f types.pro -t "type(`cat input1.txt`,T),write(T),nl"
 	swipl -f types.pro -t "type(`cat input2.txt`,T),write(T),nl"
 

diff --git a/topics/exercises/nb2/input1.txt b/topics/exercises/nb2/input1.txt
@@ -1 +1 @@
-if(iszero(zero),zero,succ(succ(zero)))
+if(iszero(pred(succ(zero))),zero,succ(succ(zero)))
diff --git a/topics/exercises/nb2/semantics.pro b/topics/exercises/nb2/semantics.pro
@@ -0,0 +1,39 @@
+:- ['syntax.pro'].
+
+%% Small-step transition relation: slide 120
+eval(E,V,T) :-
+ evalstep(E,V,T),
+ isfinal(V).
+
+eval(E1,V,T) :-
+ evalstep(E1,E2,T),
+ eval(E2,V,T).
+
+evalstep(true,tt,bool).
+evalstep(false,ff,bool).
+evalstep(zero,0,nat).
+% E-Succ
+evalstep(succ(E1),succ(E2),nat) :- evalstep(E1,E2,nat).
+% E-PredZero
+evalstep(pred(zero),zero,nat).
+% E-PredSucc
+evalstep(pred(succ(N)),N,nat).
+% E-Pred
+evalstep(pred(E1),pred(E2),nat) :- evalstep(E1,E2,nat).
+% E-Iszero-Zero
+evalstep(iszero(zero),tt,bool).
+% E-Iszero
+evalstep(iszero(T1),iszero(T2),bool) :- evalstep(T1,T2,nat).
+% E-IszeroSucc
+evalstep(iszero(succ(_)),ff,bool).
+% E-IfTrue
+evalstep(if(tt,T2,_),T2,_).
+% E-IfFalse
+evalstep(if(ff,_,T3),T3,_).
+% E-If
+evalstep(if(T1,T2,T3),if(T4,T2,T3),_) :- evalstep(T1,T4,bool).
+
+isfinal(tt).
+isfinal(ff).
+isfinal(0).
+isfinal(succ(T)) :- isfinal(T).