[_CD6_]<interscript>DraftStd>ISSemantics.mesa!8

ISSemantics.mesa

Last edited by Mitchell on December 15, 1983 5:49 pm

-- TO DO
-- sort out the V versus Vs issue by making a Vs one of the V alternatives explicitly.

DIRECTORY Real, String;

ISSemantics: PROGRAM IMPORTS Real, String =

BEGIN

Lefthand Side Alternative S[e, Alternative]

script ::= node S[X, node]

items ::= empty empty
| items item {t: V=S[e, items]; RETURN[
ConcatVs[t, S[ConcatVs[e, Bindings[t]], item]}

tag ::= primary MkTag[e, S[e, primary]]

scope ::= items MkScope[S[e, items]]

openedNode ::= term Items[S[e, term]]
| name MkV[m: onodeStruc,
cVs: Items[EvalName[e, S[NIL, name]]], name]

binding ::= name term MkBinding[e, S[e, term], S[NIL, name], bind]

sBinding ::= name sRhs MkBinding[e, S[e, sRhs], S[NIL, name], bindStruc]

quoted ::= term MkV[m: quotedTerm, cTerm: term]

term ::= term op primary apply[op, S[e, term], S[e, primary]]

literal ::= name MkV[m: atom, xName: S[NIL, name]]
| number MkV[m: num, cNum: number]
| string MkV[m: string, cStr: string]

name ::= id MkAtom[id]
| name id CONS[MkAtom[id], S[NIL, name]]

invocation ::= primary EvalName[e, S[e, primary].xName]

indirection ::= name MkV[m: evalStruc, cV: EvalName[e, S[NIL, name]],
xName: S[NIL, name]]

node ::= items {t: Vs=S[e, items]; RETURN[
MkNode[ConcatVs[e, bindings[t]], t]

NonTerminal: TYPE = REF NTRec;

NTRec: TYPE = RECORD[type: NTType, son, next: NonTerminal ← NIL,

num: Number𡤀.0, str: STRING←NIL, id: Id←NIL];

NTType: TYPE = {binding, sBinding, indirection, invocation, id, items, literal, name, node, number, openedNode, quoted, scope, script, string, tag, term};

NameFromNT: PROC[nt: NonTerminal] RETURNS[n: Name] = {

RETURN[VsAsV[S[NIL, nt--name--]].xName]};

S: PROC[e: Env, nt: NonTerminal] RETURNS[vs: Vs] = {

SELECT nt.type FROM

script => RETURN[S[X, nt.son--node--]];

items => IF nt.son=NIL THEN RETURN[NIL]

ELSE {ts: Vs=S[e, nt.son--items--];

RETURN[ConcatVs[ts, S[ConcatVs[e, GetBindings[ts]], nt.son.next--item--]]]};

tag => RETURN[MkVs[MkTag[e, VsAsV[S[e, nt.son--primary--]].xName]]];

scope => RETURN[MkScope[S[e, nt.son--items--]]];

openedNode => SELECT nt.son.type FROM

term => RETURN[Items[VsAsV[S[e, nt.son--term--]]]];

name => {n: Name = NameFromNT[nt.son];

RETURN[MkVs[MkV[m: onodeStruc, cVs: Items[EvalName[e, n]], xName: n]]]};

ENDCASE;

binding => RETURN[MkVs[MkBinding[e, VsAsV[S[e, nt.son.next--term--]], NameFromNT[nt.son], bind]]];

sBinding => RETURN[MkVs[MkBinding[e, VsAsV[S[e, nt.son.next--sRhs--]], NameFromNT[nt.son], bindStruc]]];

quoted => RETURN[MkVs[MkV[m: quotedTerm, cTerm: nt.son--term--]]];

term => RETURN[MkVs[Apply[nt.son.next.id--op--, VsAsV[S[e, nt.son--term--]], VsAsV[S[e, nt.son.next.next--primary--]]]]];

literal => SELECT nt.son.type FROM

name => RETURN[MkVs[MkV[m: atom, xName: MkName[nt.son]]]];

number => RETURN[MkVs[MkV[m: num, cNum: nt.son.num--number--]]];

string => RETURN[MkVs[MkV[m: str, cStr: nt.son.str--string--]]];

ENDCASE;

name => IF nt.son.type=id THEN RETURN[MkVs[MkV[m: name, xName: MkName[nt.son.id--id--]]]]

ELSE RETURN[MkVs[MkV[m: name, xName: MkName[nt.son.next.id--id--, NameFromNT[nt.son--name--]]]]];

invocation => RETURN[EvalName[e, S[e, nt.son--primary--].xName]];

indirection => RETURN[MkV[m: evalStruc, cV: EvalName[e, S[NIL, nt.son--name--]],
xName: S[NIL, nt.son--name--]]];

node =>{t: Vs=S[e, nt.son--items--];

RETURN[MkNode[ConcatVs[e, Bindings[t]], t]]};

ENDCASE => RETURN[S[e, nt.son--default--]];

};

2.3.2. Definitions of semantics as a Mesa function

Groundrules: Once constructed, no values or lists of values are ever modified (except in Lookup). Therefore, they can be handed around without regard for being changed in situ later.

Error: ERROR[ec: {BoundsFault, InvalidTag, NotSingleton, UnboundId, WrongType}] = CODE;

*******VALUES*******

V: TYPE = REF VRec;

Number: TYPE = REAL;

VRec: TYPE = RECORD[m: Mark,

cVs: Vs←NIL, cV: V←NIL, cNum: Number𡤀.0, cStr: STRING←NIL, cId: Id←NIL, -- Contents

cTerm: NonTerminal←NIL, -- used for representing quoted terms

xId: Id←NIL, xName: Name←NIL, xEnv: Env←NIL]; -- extra information

Mark: TYPE= {atom, num, str, node, -- base values
tag, bind, scope, bindStruc, evalStruc, onodeStruc, quotedTerm, vOfQ, evalSentinel,
id, name}; -- temp for names from nonterminals

MarkAsAtom: ARRAY Mark OF ATOM = [$atom, $num, $str, $node, $tag, $bind, $scope, $bindStruc, $evalStruc, $onodeStruc, $quotedTerm, $vOfQ, $evalSentinel];

Vs, Env: TYPE=LIST OF V; -- for an Env, all items have mark bind or bindStruc

X: Env ← NIL; -- stand-in for the eXternal environment

MkV: PROC[m: Mark, cVs: Vs←NIL, cV: V←NIL, cNum: Number𡤀.0, cStr: STRING←NIL,
cId: Id←NIL, cTerm: NonTerminal←NIL, xId: Id←NIL, xName: Name←NIL, xEnv: Env←NIL] RETURNS[V] = {

RETURN[NEW[VRec ← [m: m, cVs: cVs, cV: cV, cNum: cNum, cStr: cStr, cId: cId, cTerm: cTerm, xId: xId, xName: xName, xEnv: xEnv]]]};

True: V=MkV[m: num, cNum: 1.0]; False: V=MkV[m: num, cNum: 0.0];

MkVs: PROC[v1, v2, v3: V←NIL] RETURNS [vs: Vs] = {

vs←NIL; IF v3#NIL THEN vs←CONS[v3, vs];

IF v2#NIL THEN vs←CONS[v2, vs]; IF v1#NIL THEN vs←CONS[v1, vs] };

ConcatVs: PROC[v1, v2, v3: Vs←NIL] RETURNS [vs: Vs] = {

AppendToT: PROC[list: Vs] = {

UNTIL list=NIL DO t.rest ← CONS[list.first, NIL]; t ← t.rest; list ← list.rest ENDLOOP};

t: Vs ← (vs←CONS[NIL, NIL]);

AppendToT[v1]; AppendToT[v2]; AppendToT[v3]};

VsAsV: PROC[vs: Vs] RETURNS[v: V] = {

IF vs.rest#NIL THEN Error[NotSingleton];

RETURN[vs.first]};

NthItem: PROC[vs: Vs, n: INT] RETURNS [V] = {

IF vs=NIL OR n<0 THEN Error[BoundsFault];

RETURN[ IF n=0 THEN vs.first ELSE NthItem[vs.rest, n-1] ]};

Note that a Name is never empty; it always comes from the parser

Name, Ids: TYPE=LIST OF Id; Id: TYPE = ATOM;

MkName: PROC[a: ATOM, hd: Name←NIL] RETURNS[Name] = {RETURN[CONS[a, hd]]};

EqName: PROC[n1, n2: Name] RETURNS[BOOL] = {

UNTIL n1=NIL OR n2=NIL DO

IF n1.first#n2.first THEN RETURN[FALSE];

n1←n1.rest; n2←n2.rest;

ENDLOOP;

RETURN[n1=n2]};

*******REAL WORK*******

MkScope: PROC[vs: Vs] RETURNS [Vs] = {RETURN[

(IF HasStruc[vs] THEN MkVs[MkV[m: scope, cVs: Contents[vs]]] ELSE Contents[vs])]};

HasStruc: PROC[vs: Vs] RETURNS [BOOL] = {

One: PROC[v: V] RETURNS [BOOL] = {

RETURN[v.m=bindStruc OR v.m=evalStruc OR v.m=onodeStruc OR v.m=quotedTerm]};

RETURN[ IF vs=NIL THEN FALSE ELSE (One[vs.first] OR HasStruc[vs.rest]) ]};

All the relevant attributes for each tag are listed at the end of a node, even if the node's tags' relevant attribute sets are not disjoint. To place some bindings in a node without regard for using a specific node type indicated by tags, each binding must be a structural binding.

MkTag: PROC[e: Env, n: Name] RETURNS [V --tag--] = {

tagDef: --node--V = EvalName[e, n];

IF NOT HasTag[tagDef.cVs, $TAG] THEN Error[InvalidTag];

RETURN[MkV[m: tag, cV: tagDef, xName: n]]};

MkNode: PROC[e: Env, vs: Vs] RETURNS [V -- node--] = { --[note 1]--

RETURN[MkV[node, ConcatVs[Tags[vs], Contents[vs], RelBindings[e, Tags[vs]]]]]};

MkBinding: PROC[e: Env, v: V, n: Name, kind: Mark --bind|bindStruc--]
RETURNS [--bind|bindStruc-- V] = {

IF n.rest=NIL THEN RETURN[MkV[m: kind, cV: v, xId: n.first]] -- simple Id

ELSE {t: V=EvalName[e, n.rest]; IF t.m#node THEN Error[WrongType];

RETURN[MkBinding[e, MkNode[e, ConcatVs[t.cVs, MkVs[MkV[m: kind, cV: v, xId: n.first]]]], n.rest, kind]]};

};

Lookup: PROC[e: Env, n: Name] RETURNS [V] = {

One: PROC[e: Env, id: Id] RETURNS [V] = {

b: V ← IF e=NIL THEN NIL ELSE IF e.first.xId=id THEN e.first ELSE One[e.rest, id];

IF e.first.m=evalSentinel AND b#NIL THEN e.first.xEnv ← CONS[b, e.first.xEnv];

RETURN[b.cV]};

RETURN[ IF n=NIL THEN NIL ELSE One[Bindings[EvalName[e, n.rest]], n.first] ]};

EvalName: PROC[e: Env, n: Name] RETURNS [V] = {

RETURN[Eval[e, Lookup[e, n]]]};

Eval: PROC[e: Env, v: V] RETURNS [V] = {

IF v.m=quotedTerm THEN {

ePlus: Env = CONS[MkV[m: evalSentinel, xId: NIL], e]; -- sentinel to capture environment

RETURN MkV[m: vOfQ, cV: S[ePlus, v.cTerm].first, xEnv: ePlus.first.xEnv]}

ELSE RETURN[BaseVal[v]]};

BaseVal: PROC[v: V] RETURNS [V] = { RETURN[

(IF v.m=evalStruc THEN BaseVal[v.cV.cV -- it must be a vOfQ--] ELSE v)]};

IsInteger: PROC[v: V] RETURNS[BOOL] = {

IF v.m#num THEN Error[WrongType];

RETURN[Real.Float[Real.Fix[v.cNum]]=v.cNum]};

Apply: PROC[op: ATOM, v1: V, v2: V] RETURNS [result: V] = {

vv1: V = BaseVal[v1]; vv2: V = BaseVal[v2];

SELECT op FROM

$ADD, $SUB, $MUL, $DIV, $LT => {IF vv1.m#num OR vv2.m#num THEN Error[WrongType];

RETURN[(SELECT op FROM

$ADD => MkV[m: num, cNum: (vv1.cNum+vv2.cNum)],

$SUB => MkV[m: num, cNum: (vv1.cNum-vv2.cNum)],

$MUL => MkV[m: num, cNum: (vv1.cNum*vv2.cNum)],

$DIV => MkV[m: num, cNum: (vv1.cNum/vv2.cNum)],

$LT => (IF vv1.cNum<vv2.cNum THEN True ELSE False),

ENDCASE => NIL)]};

$EQ => {IF v1.m#v2.m THEN RETURN[False];

SELECT vv1.m FROM

node => RETURN[False];

atom => RETURN[IF (vv1.cId=vv2.cId) THEN True ELSE False];

num => RETURN[IF (vv1.cNum=vv2.cNum) THEN True ELSE False];

str => RETURN[IF String.EqualString[vv1.cStr, vv2.cStr] THEN True ELSE False];

ENDCASE => Error[WrongType]};

$SUBSCRIPT => IF NOT IsInteger[vv2] OR vv1.m#node THEN Error[WrongType]

ELSE RETURN[NthItem[Contents[Items[vv1]], Real.Fix[vv2.cNum]]];

ENDCASE};

Tags: PROC[vs: Vs] RETURNS [Vs --tag items only--] = {RETURN[(Sort[GetTags[vs]])]};

GetTags: PROC[vs: Vs] RETURNS [Vs --tag items only--] = {

One: PROC[v: V] RETURNS[Vs] = {RETURN[(IF v.m=tag THEN MkVs[v] ELSE NIL)]};

RETURN[ IF vs=NIL THEN NIL ELSE ConcatVs[One[vs.first], GetTags[vs.rest]] ]};

Sort: PROC[vs: Vs --tag items only--] RETURNS [sVs: Vs --tag items only--] = {--[note 2]--};

Items: PROC[v: V] RETURNS [Vs] = {

IF v.m=node THEN RETURN[RawItems[v.cVs]] ELSE Error[WrongType]};

RawItems: PROC[vs: Vs] RETURNS[Vs] = {

One: PROC[v: V] RETURNS[Vs] = {RETURN[

(SELECT v.m FROM

evalStruc, onodeStruc => v.cVs,

scope => RawItems[v.cVs],

ENDCASE => MkVs[v])]};

RETURN[IF vs=NIL THEN NIL ELSE ConcatVs[One[vs.first], RawItems[vs.rest]]]};

Bindings: PROC[v: V] RETURNS [Env] = {

IF v.m=node THEN RETURN[GetBindings[Items[v]]] ELSE Error[WrongType]};

GetBindings: PROC[vs: Vs] RETURNS[e: Env] = {

One: PROC[v: V] RETURNS[e: Env] = {

RETURN[IF v.m=bind OR v.m=bindStruc THEN MkVs[v] ELSE NIL]};

RETURN[IF vs=NIL THEN NIL ELSE ConcatVs[One[vs.first], GetBindings[vs.rest]]]};

RelBindings: PROC[e: Env, vs: Vs --tag items only--] RETURNS [Env] = {

One: PROC[e: Env, v: V] RETURNS [Env] = {

IF v.m#tag THEN Error[WrongType];

RETURN[RefineBindings[e, PullDefaults[Bindings[
EvalName[e, MkName[$attributes, v.xName]]]]]]};

RETURN[IF vs=NIL THEN NIL ELSE ConcatVs[One[e, vs.first], RelBindings[e, vs.rest]]]};

RefineBindings: PROC[e: Env, basis: Env] RETURNS [Env] = {

One: PROC[e: Env, b: V] RETURNS [Env] = {

IF b.m#bind AND b.m#bindStruc THEN Error[WrongType];

RETURN[IF b.m=bindStruc THEN NIL

ELSE MkVs[MkV[
m: bind, cV: Lookup[ConcatVs[MkVs[b], e], MkName[b.xId]], xId: b.xId]]]};

RETURN[IF basis=NIL THEN NIL

ELSE ConcatVs[One[e, basis.first], RefineBindings[e, basis.rest]]]};

PullDefaults: PROC[e: Env] RETURNS [Env] = {

One: PROC[b: V] RETURNS [Env] = {

IF b.cV.m=node AND HasTag[Items[b.cV], $TYPE] THEN

RETURN[MkVs[MkV
[m: bind, cV: Lookup[Bindings[b.cV], MkName[$default]], xId: b.xId]]]

ELSE Error[WrongType]};

RETURN[IF e=NIL THEN NIL ELSE ConcatVs[One[e.first], PullDefaults[e.rest]]]};

HasTag: PROC[vs: Vs, id: Id] RETURNS[BOOL] = {

RETURN[ IF vs.first.m=tag AND vs.first.cId=id THEN TRUE ELSE HasTag[vs.rest, id] ]};

Contents: PROC[vs: Vs] RETURNS [Vs] = {

One: PROC[v: V] RETURNS [Vs] = {

RETURN[(IF v.m=tag OR v.m=bind THEN NIL ELSE MkVs[v])]};

RETURN[ IF vs=NIL THEN NIL ELSE ConcatVs[One[vs.first], Contents[vs.rest]] ]};

3.1.2 Defining types

HasType: PROC[v: V, T: --node--V] RETURNS[r: BOOL ← FALSE] = {

bt: Env = Bindings[T];

IF NOT (EqName[Lookup[bt, MkName[$code]].xName, MkName[$Any]] OR EqName[Lookup[bt, MkName[$code]].xName, MkName[MarkAsAtom[v.m]]])

THEN RETURN[FALSE];

IF EqName[Lookup[bt, MkName[$code]].xName, MkName[$node]] THEN

IF NOT Subset[Tags[v.cVs], Lookup[bt, MkName[$tags]].cVs] THEN RETURN[FALSE];

FOR tt: Vs ← Lookup[bt, MkName[$union]].cVs, tt.rest UNTIL tt=NIL DO

IF HasType[v, tt.first] THEN EXIT; -- can stop checking unions as soon as one works

REPEAT

FINISHED => RETURN[FALSE]; -- v didn't satisfy any of the types in the union

ENDLOOP;

RETURN[ ApplyPred[arg: v, pred: Lookup[bt, MkName[$predicate]]] ]};

ApplyPred: PROC[arg: V, pred: V] RETURNS[t: BOOL] = {

predEnv: Env = CONS[MkBinding[X, arg, MkName[$A], bind], X]; -- just the external environment plus A𡤊rg

r: V = Eval[e: predEnv, v: pred];

RETURN[IF r.m#num THEN FALSE ELSE (r.cNum#0) ]};

Subset: PROC[sub, set: Vs--all atoms--] RETURNS[BOOL] = {

One: PROC[a: V, set: Vs] RETURNS [BOOL] = { RETURN[

(IF set=NIL THEN FALSE

ELSE IF EqName[a.xName, set.first.xName] THEN TRUE ELSE One[a, set.rest])]};

RETURN[IF sub=NIL THEN TRUE ELSE (One[sub.first, set] AND Subset[sub.rest, set])]};

3.1.3. The invariant associated with a node

NodeValidity: TYPE = {yes, no, ifExternalInvariantHolds};

NodeInvariant: PROC[n: --node--V] RETURNS[r: NodeValidity←yes] = {

IF n.m#node THEN Error[WrongType];

FOR t: Vs ← Tags[n.cVs], t.rest UNTIL t=NIL DO

SELECT TagCorrect[n, t.first.cV] FROM

no => RETURN[no];

ifExternalInvariantHolds => r ← ifExternalInvariantHolds;

ENDCASE;

ENDLOOP;

RETURN[r]};

TagCorrect: PROC[n, tagType: --node--V] RETURNS[NodeValidity] = {

bt: Env = Bindings[tagType];

RETURN[ IF

CheckAttributes[bs: Bindings[n],
types: Bindings[Lookup[bt, MkName[$attributes]]]] AND

CheckContents[Contents[n.cVs], Lookup[bt, MkName[$contentType]].cV] AND

Subset[Lookup[bt, MkName[$requiredTags]].cVs, Tags[n.cVs]] AND

ApplyPred[arg: Stripped[n], pred: Lookup[bt, MkName[$nodeInvariant]]]

THEN (IF Lookup[bt, MkName[$hasMoreInv]].cNum=1 THEN yes

ELSE ifExternalInvariantHolds)

ELSE no]};

CheckAttributes: PROC[bs, types: Env] RETURNS[BOOL] = {

One: PROC[b: --bind|bindStruc-- V] RETURNS[BOOL] = {

t: --bind|bindStruc-- V = Lookup[types, MkName[b.xId]];

RETURN[IF t=NIL THEN TRUE ELSE HasType[b.cV, t.cV]]};

RETURN[IF bs=NIL THEN TRUE
ELSE (One[bs.first] AND CheckAttributes[bs.rest, types])]};

CheckContents: PROC[vs: Vs, type: V] RETURNS[BOOL] = {

One: PROC[c: V] RETURNS[BOOL] = {

RETURN[IF c.m=bindStruc THEN TRUE ELSE HasType[c, type]]};

RETURN[IF vs=NIL THEN TRUE ELSE (One[vs.first] AND CheckContents[vs.rest, type])]};

Stripped: PROC[n: --node--V] RETURNS[--node--V] = {

RETURN[MkV[m: node, cVs: Strip[Items[n]]]]};

Strip: PROC[vs: Vs] RETURNS[svs: Vs] = {

One: PROC[v: V] RETURNS[Vs] = {

SELECT v.m FROM

bind => RETURN[MkVs[MkV[m: bind, cV: One[v.cV].first, xId: v.xId]]];

node => RETURN[IF ShouldStrip[v] THEN MkVs[MkV[m: node, cVs: Tags[v.cVs]]]
ELSE MkVs[Stripped[v]]];

ENDCASE => RETURN[MkVs[v]]};

RETURN[IF vs=NIL THEN NIL ELSE ConcatVs[One[vs.first], Strip[vs.rest]]]};

ShouldStrip: PROC[v: --node--V] RETURNS[BOOL] = {

all of v's tags must agree on tagOnly for it to be true

tags: Vs = Tags[v.cVs];

FOR tags: Vs ← Tags[v.cVs], tags.rest UNTIL tags=NIL DO

tDef: V = tags.first.cV;

btDef: Env = Bindings[tDef];

IF Lookup[btDef, MkName[$tagOnly]].cNum#1 THEN RETURN[FALSE];

ENDLOOP;

RETURN[TRUE]};

END.