Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
git-svn-id: https://slps.svn.sourceforge.net/svnroot/slps@722 ab42f6e0-554d-0410-b580-99e487e6eeb2
- Loading branch information
1 parent
eee440c
commit 21ced2f
Showing
9 changed files
with
409 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
test: | ||
swipl -f RunTypeChecker.pro -t "main('input.txt')" | ||
|
||
debug: | ||
cat input.txt | ||
swipl -s RunTypeChecker.pro | ||
|
||
clean: | ||
rm -rf *~ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,147 @@ | ||
%% Parser for While language | ||
% Program is a list of statements | ||
program(S) --> statements(S). | ||
|
||
% Non-empty list | ||
statements(slist(H,T)) --> | ||
statement(H), | ||
keyword(";"), | ||
statements(T). | ||
|
||
% Empty list | ||
statements(S) --> statement(S). | ||
|
||
%% Statements | ||
% Variable declaration | ||
statement(decl(V)) --> | ||
keyword("var"), | ||
identifier(V). | ||
|
||
% Skip statement | ||
statement(skip) --> | ||
keyword("skip"). | ||
|
||
% Assign statement | ||
statement(assign(identifier(V),E)) --> | ||
identifier(V), | ||
keyword(":="), | ||
aexpression(E). | ||
|
||
% Conditional statement | ||
statement(ifthenelse(E,S1,S2)) --> | ||
keyword("if"), | ||
bexpression(E), | ||
keyword("then"), | ||
statement(S1), | ||
keyword("else"), | ||
statement(S2). | ||
|
||
% Loop statement | ||
statement(while(E,S)) --> | ||
keyword("while"), | ||
bexpression(E), | ||
keyword("do"), | ||
statement(S). | ||
|
||
|
||
%% Arithmetic expressions | ||
% Number is a an arithmetic expression | ||
aexpression(number(N)) --> number(N). | ||
|
||
% Variable reference is a an arithmetic expression | ||
aexpression(identifier(V)) --> identifier(V). | ||
|
||
% A sum of arithmetic expressions is also an arithmetic expression | ||
aexpression(add(E1,E2)) --> | ||
keyword("("), | ||
aexpression(E1), | ||
keyword("+"), | ||
aexpression(E2), | ||
keyword(")"). | ||
|
||
% Same with subtraction | ||
aexpression(sub(E1,E2)) --> | ||
keyword("("), | ||
aexpression(E1), | ||
keyword("-"), | ||
aexpression(E2), | ||
keyword(")"). | ||
|
||
% ...and multiplication | ||
aexpression(mul(E1,E2)) --> | ||
keyword("("), | ||
aexpression(E1), | ||
keyword("*"), | ||
aexpression(E2), | ||
keyword(")"). | ||
|
||
|
||
%% Boolean expressions | ||
% Boolean primitives are boolean expressions | ||
bexpression(true) --> keyword("true"). | ||
bexpression(false) --> keyword("false"). | ||
|
||
% Comparison is a boolean expression: equality | ||
bexpression(equals(E1,E2)) --> | ||
aexpression(E1), | ||
keyword("="), | ||
aexpression(E2). | ||
|
||
% Comparison is a boolean expression: less than or equal to | ||
bexpression(lte(E1,E2)) --> | ||
aexpression(E1), | ||
keyword("≤"), | ||
aexpression(E2). | ||
|
||
% Negation is a boolean expression | ||
bexpression(not(E)) --> | ||
keyword("¬"), | ||
bexpression(E). | ||
|
||
% Disjunction of boolean expressions is also a boolean expression | ||
bexpression(and(E1,E2)) --> | ||
keyword("("), | ||
bexpression(E1), | ||
keyword("^"), | ||
bexpression(E2), | ||
keyword(")"). | ||
|
||
|
||
%% Low-level details | ||
% Dealing with layout | ||
layout --> [0' ], layout. %' space | ||
layout --> [0' ], layout. %' tab | ||
layout --> [10], layout. % newline | ||
layout --> []. | ||
|
||
% Keywords are space-consuming strings | ||
keyword(X) --> | ||
layout, | ||
string(X). | ||
|
||
% Bare strings | ||
string([],X,X). | ||
string([H|T1],[H|T2],X) :- string(T1,T2,X). | ||
|
||
% Numbers are space-consuming digits | ||
number(N) --> | ||
layout, | ||
digit(H), digits(T), | ||
{ number_chars(N,[H|T]) }. | ||
|
||
% Bare digits | ||
digits([H|T]) --> digit(H), digits(T). | ||
digits([]) --> []. | ||
digit(H,[H|T],T) :- H >= 0'0, H =< 0'9. | ||
|
||
% Identifiers are space-consuming letters | ||
identifier(V) --> | ||
layout, | ||
letter(H), letters(T), | ||
{ atom_chars(V,[H|T]) }. | ||
|
||
% Bare letters | ||
letters([H|T]) --> letter(H), letters(T). | ||
letters([]) --> []. | ||
letter(H,[H|T],T) :- H >= 0'a, H =< 0'z. | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
:- ['Parser.pro','mappings.pro','compExpr.pro','smallStm.pro','Types.pro']. | ||
|
||
main(File) :- | ||
parseFile(File,program,S), | ||
write(S),nl,nl, | ||
type(S,[],M,T), | ||
%execute(S,[],M), | ||
write(M),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). | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,39 @@ | ||
:- ['Parser.pro']. | ||
|
||
% type(Expression,DeclaredIn,DeclaredOut,Type), where Type = unit | ||
% type(Expression,Declared,Type), where Type = bool or nat | ||
|
||
%% StateDents have the 'unit' type | ||
type(slist(S1,S2),D1,D2,unit) :- | ||
type(S1,D1,D3,unit), | ||
type(S2,D3,D2,unit). | ||
|
||
type(skip,D,D,unit). | ||
type(decl(X),D1,D2,unit) :- declare(D1,X,D2). | ||
type(assign(identifier(X),E),D,D,unit) :- | ||
type(E,D,nat), | ||
isdeclared(D,X). | ||
type(ifthenelse(E,S1,S2),D1,D2,unit) :- | ||
type(E,D1,bool), | ||
% we assume no local variable declarations | ||
type(S1,D1,D2,unit), | ||
type(S2,D1,D2,unit). | ||
|
||
type(while(E,S),D1,D2,unit) :- | ||
type(E,D1,bool), | ||
type(S,D1,D2,unit). | ||
|
||
%% Arithmetic expressions have the 'nat' type | ||
type(number(N),_,nat). | ||
type(identifier(N),D,nat) :- isdeclared(D,N). | ||
type(add(E1,E2),D,nat) :- type(E1,D,nat), type(E2,D,nat). | ||
type(sub(E1,E2),D,nat) :- type(E1,D,nat), type(E2,D,nat). | ||
type(Dul(E1,E2),D,nat) :- type(E1,D,nat), type(E2,D,nat). | ||
|
||
%% Boolean expressions have the 'bool' type | ||
type(true,_,bool). | ||
type(false,_,bool). | ||
type(equals(E1,E2),D,bool) :- type(E1,D,nat), type(E2,D,nat). | ||
type(lte(E1,E2),D,bool) :- type(E1,D,nat), type(E2,D,nat). | ||
type(not(E),D,bool) :- type(E,D,bool). | ||
type(and(E1,E2),D,bool) :- type(E1,D,bool), type(E2,D,bool). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,121 @@ | ||
%% Small-step transition relation for expressions | ||
/* | ||
% Closure for arithmetic expressions | ||
evala(A,M,V) :- | ||
evalastep(A,M,V), | ||
number(V). | ||
evala(A1,M,V) :- | ||
evalastep(A1,M,A2), | ||
evala(A2,M,V). | ||
% Closure for boolean expressions | ||
evalb(B,M,V) :- | ||
evalbstep(B,M,V), | ||
isbool(V). | ||
evalb(B1,M,V) :- | ||
evalbstep(B1,M,B2), | ||
evalb(B2,M,V). | ||
*/ | ||
|
||
%% Evaluate arithmetic expressions | ||
% Number is evaluated to its value | ||
evalastep(number(V),_,V). | ||
|
||
% Variable reference is evaluated to its current value | ||
evalastep(identifier(X),M,number(Y)) :- lookup(M,X,Y). | ||
|
||
%% Adddition | ||
% Case 1: add number to number | ||
evalastep(add(number(V1),number(V2)),_,number(V)) :- V is V1 + V2. | ||
% Case 2: add number to expression | ||
evalastep(add(number(V1),A2),M,add(number(V1),A3)) :- evalastep(A2,M,A3). | ||
% Case 3: add expression to something | ||
evalastep(add(A1,A2),M,add(A3,A2)) :- evalastep(A1,M,A3). | ||
|
||
%% Subtraction | ||
% Case 1: subtract number from number | ||
evalastep(sub(number(V1),number(V2)),_,number(V)) :- V is V1 - V2. | ||
% Case 2: subtract number from expression | ||
evalastep(sub(number(V1),A2),M,sub(number(V1),A3)) :- evalastep(A2,M,A3). | ||
% Case 3: subtract expression from something | ||
evalastep(sub(A1,A2),M,sub(A3,A2)) :- evalastep(A1,M,A3). | ||
|
||
%% Multiplication | ||
% Case 1: number times number | ||
evalastep(mul(number(V1),number(V2)),_,number(V)) :- V is V1 * V2. | ||
% Case 2: number times expression | ||
evalastep(mul(number(V1),A2),M,sub(number(V1),A3)) :- evalastep(A2,M,A3). | ||
% Case 3: expression times something | ||
evalastep(mul(A1,A2),M,sub(A3,A2)) :- evalastep(A1,M,A3). | ||
|
||
%% Evaluate Boolean expressions | ||
% True is tt | ||
evalbstep(true,_,tt). | ||
|
||
% False is ff | ||
evalbstep(false,_,ff). | ||
|
||
%% Negation | ||
% One small step is enough | ||
evalbstep(not(B),M,V) :- | ||
evalbstep(B,M,V1), | ||
isbool(V1), | ||
not(V1,V). | ||
% One small step is not enough | ||
evalbstep(not(B1),M,not(B2)) :- | ||
evalbstep(B1,M,B2). | ||
|
||
%% Conjunction | ||
% Case 1: atomic boolean and atomic boolean | ||
evalbstep(and(B1,B2),_,V) :- | ||
isbool(B1), | ||
isbool(B2), | ||
and(B1,B2,V). | ||
% Case 2: atomic boolean and non-atomic boolean | ||
evalbstep(and(B1,B2),M,and(B1,B3)) :- | ||
isbool(B1), | ||
evalbstep(B2,M,B3). | ||
% Case 3: non-atomic boolean and something | ||
evalbstep(and(B1,B2),M,and(B3,B2)) :- | ||
evalbstep(B1,M,B3). | ||
|
||
%% Test for equality | ||
% Case 1: compare number with number | ||
evalbstep(equals(V1,V2),_,V) :- | ||
number(V1), | ||
number(V2), | ||
equals(V1,V2,V). | ||
% Case 2: compare number with expression | ||
evalbstep(equals(V1,A2),M,equals(V1,A3)) :- | ||
number(V1), | ||
evalastep(A2,M,A3). | ||
% Case 3: compare expression with something | ||
evalbstep(equals(A1,A2),M,equals(A3,A2)) :- evalastep(A1,M,A3). | ||
|
||
% Test for being less than or equal | ||
% Case 1: compare number with number | ||
evalbstep(lte(V1,V2),_,V) :- | ||
number(V1), | ||
number(V2), | ||
lte(V1,V2,V). | ||
% Case 2: compare number with expression | ||
evalbstep(lte(V1,A2),M,lte(V1,A3)) :- | ||
number(V1), | ||
evalastep(A2,M,A3). | ||
% Case 3: compare expression with something | ||
evalbstep(lte(A1,A2),M,lte(A3,A2)) :- evalastep(A1,M,A3). | ||
|
||
%% Basic operations | ||
equals(V1,V2,tt) :- V1 == V2. | ||
equals(V1,V2,ff) :- \+ V1 == V2. | ||
lte(V1,V2,tt) :- V1 =< V2. | ||
lte(V1,V2,ff) :- \+ V1 =< V2. | ||
not(tt,ff). | ||
not(ff,tt). | ||
and(tt,tt,tt). | ||
and(ff,_,ff). | ||
and(_,ff,ff). | ||
isbool(tt). | ||
isbool(ff). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
var x; | ||
var y; | ||
var z; | ||
y:=2; | ||
x:=(y+4); | ||
if (y = 2 ^ x = 6) | ||
then | ||
z := y | ||
else | ||
z := 1000; | ||
while x≤10 do x := (x + 1) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
% Function lookup for functions represented as lists of pairs | ||
lookup(M,X,Y) :- append(_,[(X,Y)|_],M). | ||
isdeclared(D,X) :- member(X,D). | ||
|
||
% Fresh variables can be declared | ||
declare([],X,[X]). | ||
declare([H|T1],X,[H|T2]) :- | ||
\+ H = X, | ||
declare(T1,X,T2). | ||
|
||
% Variable values can be updated | ||
update([(X,_)|M],X,Y,[(X,Y)|M]). | ||
update([(X1,Y1)|M1],X2,Y2,[(X1,Y1)|M2]) :- | ||
\+ X1 = X2, | ||
update(M1,X2,Y2,M2). | ||
|
||
|
Oops, something went wrong.