
<<-- TypeCheckImpl.mesa
-- Last edited by Jim Sasaki on August 24, 1983 10:34 am>>

DIRECTORY Rope, Atom, TypeCheck, Unparser;

TypeCheckImpl: PROGRAM 
IMPORTS Atom, Unparser
EXPORTS TypeCheck = BEGIN

OPEN TypeCheck;

<<-- Some Atoms used as operators.>>
<<>>
arrow : ATOM = Atom.MakeAtom [ "=>" ];
asgn : ATOM = Atom.MakeAtom[ "_" ];
box : ATOM = Atom.MakeAtom[ "||" ];
colon : ATOM = Atom.MakeAtom [ ":" ];
comma : ATOM = Atom.MakeAtom[ "," ];
dblEq : ATOM = Atom.MakeAtom[ "==" ];
eq : ATOM = Atom.MakeAtom[ "=" ];
ge : ATOM = Atom.MakeAtom[ ">=" ];
gt : ATOM = Atom.MakeAtom[ ">" ];
lbrace : ATOM = Atom.MakeAtom[ "{" ];
lbracket : ATOM = Atom.MakeAtom[ "[" ];
le : ATOM = Atom.MakeAtom[ "<=" ];
lparen : ATOM = Atom.MakeAtom [ "(" ];
lt : ATOM = Atom.MakeAtom[ "<" ];
minus : ATOM = Atom.MakeAtom[ "-" ];
ne : ATOM = Atom.MakeAtom[ "#" ];
not : ATOM = Atom.MakeAtom[ "~" ];
plus : ATOM = Atom.MakeAtom[ "+" ];
rbrace : ATOM = Atom.MakeAtom[ "}" ];
rbracket : ATOM = Atom.MakeAtom[ "]" ];
rparen : ATOM = Atom.MakeAtom[ ")" ];
semicolon : ATOM = Atom.MakeAtom[";"];
star : ATOM = Atom.MakeAtom[ "*" ];
up : ATOM = Atom.MakeAtom[ "^" ];

Wlp: PUBLIC PROCEDURE [ s : Stmt, p : Predicate ]  RETURNS [ q : Predicate ] =
{
<<-- We calculate the weakest liberal precondition (wlp) of a statement S and a predicate P; it is the weakest predicate Q such 
that if you start S in state Q and S halts (i.e., doesn't abort or run forever) then P is true afterwards.>>
<<>>
IF s = NIL THEN ERROR;

SELECT Optr [ s ] FROM

asgn => q _ Substitute  [ VarOfAsgn [ s ], Arg2 [ s ], p ];
semicolon => q _ Wlp [ Arg1 [ s ], Wlp [ Arg2 [ s ], p ] ];
$if => q _ WlpIfCmdList [ GcmdsOfIf [ s ], p ];
$do => q _ WlpDo [ s, p ];

ENDCASE => ERROR;
};

Substitute:
  PRIVATE PROCEDURE [ v : Term, t : Term, p : ParseTree ] RETURNS [ q : ParseTree ] =
{
<<-- Substitute terms t for variables v in parse tree p.  Note that t and v are either individual terms or lists separated by 
commas.>>
<<>>
IF p = NIL THEN RETURN [ p ];

WITH p SELECT FROM

a : ATOM => q _ SubstituteForVar [ v, t, a ];

n : REF INT => q _ n;

l : List =>
q _ CONS
[ Substitute [ v, t, l.first ], NARROW [ Substitute [ v, t, l.rest ], List ] ]

ENDCASE => ERROR;
};

SubstituteForVar:
  PRIVATE PROCEDURE [ v : Term, t : Term, a : ATOM ] RETURNS [ q : ParseTree ] =
{
<<-- If the atom a is among the variables v, then substitute the corresponding term from t for it.  Note that t and v are either 
individual terms or lists separated by commas.>>
<<>>
IF v = NIL THEN RETURN [ a ];

IF ISTYPE [ v, ATOM ] THEN
IF NARROW [ v, ATOM ] = a THEN RETURN [ t ] ELSE RETURN [ a ];

IF ( a = NARROW [ Arg1 [ v ], ATOM ] ) THEN
q _ Arg1 [ t ]
ELSE
q _ SubstituteForVar [ Arg2 [ v ], Arg2 [ t ], a ];
};

WlpIfCmdList:
  PRIVATE PROCEDURE [ gcs : ParseTree, p : Predicate ] RETURNS [ q : Predicate ] =
{
<<-- We take the guarded commands of an if ... fi and return the and of their wlp's.>>
<<>>
moreThanOne : BOOL;  -- TRUE if there is more than one guard in the list.
wlpFirst, wlpRest : ParseTree;  -- wlp's of first and other guards of the list.
<<>>
IF gcs = NIL THEN RETURN [ $true ];

IF ( moreThanOne _ ( Optr [ gcs ] = box ) ) THEN
{
wlpFirst _ WlpIfCmd [ Arg1 [ gcs ], p ];
wlpRest _ WlpIfCmdList [ Arg2 [ gcs ], p ];

q _ Binary [ $and, Parenthesize [ wlpFirst ], wlpRest ]
}
ELSE
q _ Parenthesize [ WlpIfCmd [ gcs, p ] ];
};

WlpIfCmd:
  PRIVATE PROCEDURE [ gc : Stmt, p : Predicate ] RETURNS [ q : Predicate ] =
{
<<-- We have a guarded command of the form G => S where G is a guard.  If G is R, return ( R impl wlp(S,P) ).  If G is of the form 
x : R, return all x : ( R impl wlp(S,P) ).>>
<<>>
x, R, S : ParseTree;  -- as above.
impl : ParseTree;  -- the tree ( R impl wlp(S,P)).
<<>>
IF gc = NIL OR Optr [ gc ] # arrow THEN ERROR;

[ x, R, S ] _ SplitGcmd [ gc ];

impl _ PBinary [ $impl, R, Wlp [ S, p ] ];

IF x = NIL THEN
q _ PUnary [ $all, PBinary [ colon, x, impl ] ]
ELSE
q _ impl;
};

WlpDo:
  PRIVATE PROCEDURE [ s : ParseTree, p : Predicate ] RETURNS [ F1 : Predicate ] =
{
<<-- Wlp ( do I inv G1 => S1 || ... Gn => Sn od, P ) =>>
<<>>
<<I and all u : I impl ((P and not OR(i) Ri) or AND(i) (Ri => Wlp(Si,I)))>>
<<    1   2    3     4       5   6    7        8  9         10>>
<<>>
<<where>>
<<OR(i) Ri means (R1 or R2 or ... Rn)>>
<<AND(i) R1 means (R1 and R2 and ... Rn)>>
<<u is the list of free variables of the loop that are assigned to (in the loop).>>
<<>>
<<and the numbers under the operators indicate which formula is which.  (That is, F1 is (I and F2), F2 is (all F3), and so on.)>>
<<>>
<<If u is empty, return>>
<<    I and ((P and not OR(i) Ri) or AND(i) (Ri => Wlp(Si,I)))>>
<<       1       5  6    7        8   9         10>>

F2, F3, F4, F5, F6, F7, F8, F9 : Predicate;
u : Term;  -- the free variables of s that are assigned to in s.
inv : ParseTree _ InvOfDo [ s ];
gcs : ParseTree _ GcmdsOfDo [ s ];

[ F7, F9 ] _ WlpDoGcmds [ gcs, inv ];

F6 _ PUnary [ not, F7 ];
F5 _ PBinary [ $and, p, F6 ];
F8 _ PBinary [ $or, F5, F9 ];

IF ( u _ FreeAsgVars [ s ] ) = NIL THEN
F1 _ PBinary [ $and, inv, F8 ]
ELSE
{
F4 _ PBinary [ $impl, inv, F8 ];
F3 _ PBinary [ colon, u, F4 ];
F2 _ PUnary [ $all, F3 ];
F1 _ PBinary [ $and, inv, F2 ]
};
};

WlpDoGcmds:
  PRIVATE PROCEDURE [ gcs : ParseTree, inv : Predicate ] RETURNS [ F7, F9 : Predicate ] =
{
<<-- Calculate formulas F7 and F9 as defined in WlpDo.>>
<<>>
moreThanOne : BOOL;  -- TRUE if there is more than one guard in the list.
x, R, S : ParseTree;  -- the current guard, broken into its parts, x : R => S.

IF gcs = NIL THEN RETURN [ F7 : $false, F9 : $true ];

IF ( moreThanOne _ ( Optr [ gcs ] = box ) ) THEN
{
[ F7, F9 ] _ WlpDoGcmds [ Arg2 [ gcs ], inv ];
[ x, R, S ] _ SplitGcmd [ Arg1 [ gcs ] ];
F7 _ Binary [ $or, Parenthesize [ R ], F7 ];
F9 _ PBinary [ $and, PBinary [ $impl, R, Wlp [ S, inv ] ], F9 ]
}
ELSE
{
[ x, R, S ] _ SplitGcmd [ gcs ];
F7 _ Parenthesize [ R ];
F9 _ Parenthesize [ PBinary [ $impl, R, Wlp [ S, inv ] ] ]
};
};

FreeAsgVars:
  PRIVATE PROCEDURE [ s : Stmt ] RETURNS [ v : ParseTree ] =
{
<<-- We return the free variables of s that are assigned to (in s).>>
<<>>
IF s = NIL THEN RETURN [ NIL ];

SELECT Optr [ s ] FROM

asgn => v _ VarOfAsgn [ s ];
semicolon => v _ Add [ FreeAsgVars [ Arg1 [ s ] ], FreeAsgVars [ Arg2 [ s ] ] ];
$if => v _ FreeAsgVarsOfGcmds [ GcmdsOfIf [ s ] ];
$do => v _ FreeAsgVarsOfGcmds [ GcmdsOfDo [ s ] ];

ENDCASE => ERROR;
};

FreeAsgVarsOfGcmds:
  PRIVATE PROCEDURE [ gcs : ParseTree ] RETURNS [ v : Term ] =
{
<<-- We return an identifier list containing the free variables of gcs that are assigned to in gcs, where gcs is a list of guarded 
commands, G1 => S1 || ... Gn => Sn.>>
<<>>
moreThanOne : BOOL;  -- TRUE if there is more than one guard in the list.

IF gcs = NIL THEN RETURN [ NIL ];

IF ( moreThanOne _ ( Optr [ gcs ] = box ) ) THEN

v _ Add
[ FreeAsgVarsOfGcmd [ Arg1 [ gcs ] ]
, FreeAsgVarsOfGcmds [ Arg2 [ gcs ] ]
]

ELSE
v _ FreeAsgVarsOfGcmd [ gcs ]
};

FreeAsgVarsOfGcmd:
  PRIVATE PROCEDURE [ gc : Stmt ] RETURNS [ v : Term ] =
{
<<-- The guarded command gc has of the form G => S.  If G is a predicate R then fav(gc) is fav(s).  If G is a binding x : R, then 
fav(gc) = fav(s) minus the variables x.>>
<<>>
x, R, S : ParseTree;
<<>>
IF gc = NIL OR Optr [ gc ] # arrow THEN ERROR;

[ x, R, S ] _ SplitGcmd [ gc ];

IF x = NIL THEN
v _ FreeAsgVars [ S ]
ELSE
v _ Subtract [ FreeAsgVars [ S ], x ];
};

Add:
  PRIVATE PROCEDURE [ x, y : Term ] RETURNS [ z : Term ] =
{
<<-- Add together the two identifier lists x and y.  Eliminate duplications.>>
<<>>
IF x = NIL THEN RETURN [ y ];
IF y = NIL THEN RETURN [ x ];

WITH x SELECT FROM  a : ATOM => RETURN [ AddVar [ a, y ] ]  ENDCASE;

IF Optr [ x ] # comma THEN ERROR;

z _  AddVar [ NARROW [ Arg1 [ x ], ATOM ], Add [ Arg2 [ x ], y ] ]
};

AddVar:
  PRIVATE PROCEDURE [ v : ATOM, y : Term ] RETURNS [ t : Term ] =
{
<<-- Add the variable v to the term y = var1,var2,...varN.>>
<<>>
a : ATOM;  -- the first variable of y.
<<>>
IF y = NIL THEN RETURN [ v ];

WITH y SELECT FROM
a : ATOM => RETURN [ IF a = v THEN a ELSE CommaTogether [ v, a ] ]
ENDCASE;

IF Optr [ y ] # comma THEN ERROR;

IF v = ( a _ NARROW [ Arg1 [ y ], ATOM ] ) THEN
t _ y
ELSE
t _ CommaTogether [ a, AddVar [ v, Arg2 [ y ] ] ]
};

Subtract:
  PRIVATE PROCEDURE [ x, y : Term ] RETURNS [ z : Term ] =
{
<<-- Take x and subtract off the identifiers of y, where both x and y are identifier lists.>>
<<>>
IF x = NIL THEN RETURN [ NIL ];
IF y = NIL THEN RETURN [ x ];

WITH y SELECT FROM  a : ATOM => RETURN [ SubtractVar [ a, x ] ]  ENDCASE;

IF Optr [ y ] # comma THEN ERROR;

z _  SubtractVar [ NARROW [ Arg1 [ y], ATOM ], Subtract [ x, Arg2 [ y ] ] ]
};

SubtractVar:
  PRIVATE PROCEDURE [ v : ATOM, y : Term ] RETURNS [ t : Term ] =
{
<<-- Remove the variable v from the term y = var1,var2,...varN.>>
<<>>
a : ATOM;  -- the first variable of y.
<<>>
IF y = NIL THEN RETURN [ NIL ];

WITH y SELECT FROM a : ATOM => RETURN [ IF a = v THEN NIL ELSE a ] ENDCASE;

IF Optr [ y ] # comma THEN ERROR;

IF v = ( a _ NARROW [ Arg1 [ y ], ATOM ] ) THEN
t _ Arg2 [ y ]
ELSE
t _ CommaTogether [ a, SubtractVar [ v, Arg2 [ y ] ] ]
};

CommaTogether:
  PRIVATE PROCEDURE [ v : ATOM, y : Term ] RETURNS [ t : Term ] =
{
<<-- If y is nonNIL, we return (v,y) otherwise we return v.>>
<<>>
t _ IF y = NIL THEN v ELSE Binary [ comma, v, y ]
};

<<-- Tree building routines: build binary and unary trees (with and without parenthesizing the arguments), parenthesize a tree.>>

PBinary:
  PRIVATE PROCEDURE [ op : ATOM, lhs, rhs : ParseTree ] RETURNS [ t : ParseTree ] =
{
RETURN
[ CONS [ op, CONS [ Parenthesize [ lhs ], CONS [ Parenthesize [ rhs ], NIL ] ] ] ]
};

PUnary:
  PRIVATE PROCEDURE [ op : ATOM, opnd : ParseTree ] RETURNS [ t : ParseTree ] =
{
RETURN [ CONS [ op, CONS [ Parenthesize [ opnd ], NIL ] ] ]
};

Binary:
  PRIVATE PROCEDURE [ op : ATOM, lhs, rhs : ParseTree ] RETURNS [ t : ParseTree ] =
{
RETURN [ CONS [ op, CONS [ lhs, CONS [ rhs, NIL ] ] ] ]
};

Unary:
  PRIVATE PROCEDURE [ op : ATOM, opnd : ParseTree ] RETURNS [ t : ParseTree ] =
{
RETURN [ CONS [ op, CONS [ opnd, NIL ] ] ]
};

Parenthesize:
  PRIVATE PROCEDURE [ p : ParseTree ] RETURNS [ q : ParseTree ] =
{
IF NotLeaf [ p ] AND Optr [ p ] = lparen THEN RETURN [ p ];

RETURN [ Unary [ lparen, p ] ]
};

<<-- Selector routines: get various args of a tree.>>
<<>>
ArgsOf:
  PRIVATE PROCEDURE [ p : ParseTree ] RETURNS [ ParseTree, ParseTree ] =
{
RETURN [ Arg1 [ p ], Arg2 [ p ] ]
};

Optr: PROC [ r : ParseTree ] RETURNS [ a : ATOM ] = { a _ NARROW [ Car[r] ] };
Arg1: PROC [ r : ParseTree ] RETURNS [ ParseTree ] = Cadr;
Arg2: PROC [ r : ParseTree ] RETURNS [ ParseTree ] = Caddr;
<<>>
SplitGcmd: PROC [ gc : Stmt ] RETURNS [ x, R, S : ParseTree _ NIL ] =
{
<<--  Split up the guarded command, x : R => S or R => S.  (Return x = NIL in the latter case.)>>
<<>>
G : ParseTree;  -- x : R or R, as appropriate

[ G, S ] _ ArgsOf [ gc ];

IF NotLeaf [ G ] AND Optr [ G ] = colon THEN
[ x, R ] _ ArgsOf [ G ]
ELSE
R _ G;
};

VarOfAsgn: PROC [ p : ParseTree ] RETURNS [ v : ParseTree ] =
{
v _ Arg1 [ p ]  -- The variables of an assignment
};

GcmdsOfIf: PROC [ p : ParseTree ] RETURNS [ q : ParseTree ] =
{
q _ Arg1 [ p ] -- the guarded commands of if G => S ... fi
};

GcmdsOfDo: PROC [ p : ParseTree ] RETURNS [ q : ParseTree ] =
{
q _ Arg2 [ Arg1 [ p ] ] -- the guarded commands of do I inv G => S ... od
};

InvOfDo: PROC [ p : ParseTree ] RETURNS [ q : ParseTree ] =
{
q _ Arg1 [ Arg1 [ p ] ] -- the invariant of do I inv G => S ... od
};

Car: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[NARROW[NARROW[r, List].first]]};
Cdr: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[NARROW[r, List].rest]};
Cadr: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[Car[Cdr[r]]]};
Cddr: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[Cdr[Cdr[r]]]};
Caddr: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[Car[Cdr[Cdr[r]]]]};

<<-- Inspection routines: check for nonleaves.>>
<<>>
NotLeaf: PROC [ p : ParseTree ] RETURNS [ b : BOOL ] =
{
RETURN [ p # NIL AND ISTYPE [ p, List ] ]
};

<<-- Some testing routines; not normally used otherwise.>>
<<>>
Unparse:
  PRIVATE PROCEDURE [ p : ParseTree ] RETURNS [ r : ROPE ] =
{
r _ Unparser.Unparse
[ f : CONS [ p, NIL ], culprit : NIL, margin : 60, p : NIL, openCount : 0 ]
};

END.