<* PRAGMA LL *> MODULE=======================================================; IMPORT Algorithm, FormsVBT, Thread, ZeusPanel, RefList, ZeusCodeView; IMPORT SubtypeAlgClass, SubtypeIE; IMPORT Text, TextRd, Sx, Atom, VBT; <* FATAL FormsVBT.Error, FormsVBT.Unimplemented *> TYPE T = SubtypeAlgClass.T BRANDED OBJECT trail: ARRAY [0..1000] OF RECORD lft,rht: Type END; top: INTEGER := -1; travTrail: ARRAY [0..1000] OF Type; travTop: INTEGER; nodes: ARRAY [0..99] OF Type; nodeIndex: INTEGER; edgeIndex: INTEGER; OVERRIDES run := Run; END; PROCEDURE AlgSubtype New (): Algorithm.T = VAR form: FormsVBT.T; BEGIN form := ZeusPanel.NewForm("subtypeinput.fv"); FormsVBT.AttachProc(form, "ex1", Example1Proc, NIL); FormsVBT.AttachProc(form, "ex2", Example2Proc, NIL); FormsVBT.AttachProc(form, "ex3", Example3Proc, NIL); FormsVBT.AttachProc(form, "ex4", Example4Proc, NIL); FormsVBT.AttachProc(form, "ex5", Example5Proc, NIL); FormsVBT.AttachProc(form, "ex6", Example6Proc, NIL); FormsVBT.AttachProc(form, "ex7", Example7Proc, NIL); FormsVBT.AttachProc(form, "ex8", Example8Proc, NIL); FormsVBT.AttachProc(form, "ex9", Example9Proc, NIL); FormsVBT.AttachProc(form, "ex10", Example10Proc, NIL); FormsVBT.AttachProc(form, "nonex1", NonExample1Proc, NIL); FormsVBT.AttachProc(form, "nonex2", NonExample2Proc, NIL); FormsVBT.AttachProc(form, "nonex3", NonExample3Proc, NIL); FormsVBT.AttachProc(form, "nonex4", NonExample4Proc, NIL); FormsVBT.AttachProc(form, "nonex5", NonExample5Proc, NIL); FormsVBT.AttachProc(form, "nonex6", NonExample6Proc, NIL); FormsVBT.AttachProc(form, "nonex7", NonExample7Proc, NIL); FormsVBT.AttachProc(form, "nonex8", NonExample8Proc, NIL); FormsVBT.AttachProc(form, "nonex9", NonExample9Proc, NIL); FormsVBT.AttachProc(form, "nonex10", NonExample10Proc, NIL); RETURN NEW(T, data := form, codeViews := RefList.List1(RefList.List2("M3 Code View", "alg_m3.code"))).init(); END New; PROCEDUREExample1Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(top -> bot)"); FormsVBT.PutText(fv, "typeright", "(bot -> top)"); END Example1Proc; PROCEDUREExample2Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "((top -> bot) -> bot)"); FormsVBT.PutText(fv, "typeright", "(bot -> (bot -> top))"); END Example2Proc; PROCEDUREExample3Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(rec x (top -> x))"); FormsVBT.PutText(fv, "typeright", "(rec y (bot -> y))"); END Example3Proc; PROCEDUREExample4Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(rec x (top -> x))"); FormsVBT.PutText(fv, "typeright", "(rec y (bot -> (bot -> y)))"); END Example4Proc; PROCEDUREExample5Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(rec x (x -> bot))"); FormsVBT.PutText(fv, "typeright", "(rec y (y -> bot))"); END Example5Proc; PROCEDUREExample6Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(rec x ((x -> top) -> x))"); FormsVBT.PutText(fv, "typeright", "(rec y (y -> (bot -> y)))"); END Example6Proc; PROCEDUREExample7Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(rec x (x -> x))"); FormsVBT.PutText(fv, "typeright", "(rec y (y -> y))"); END Example7Proc; PROCEDUREExample8Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(rec x (x -> x))"); FormsVBT.PutText(fv, "typeright", "(rec y ((y -> y) -> y))"); END Example8Proc; PROCEDUREExample9Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(rec x (x -> (x -> x)))"); FormsVBT.PutText(fv, "typeright", "(rec y ((y -> y) -> y))"); END Example9Proc; PROCEDUREExample10Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(rec t (top -> ((t -> t) -> top)))"); FormsVBT.PutText(fv, "typeright", "(rec s (top -> ((s -> bot) -> top)))"); END Example10Proc; PROCEDURENonExample1Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(bot -> bot)"); FormsVBT.PutText(fv, "typeright", "(top -> top)"); END NonExample1Proc; PROCEDURENonExample2Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(rec x (x -> bot))"); FormsVBT.PutText(fv, "typeright", "(rec y (y -> top))"); END NonExample2Proc; PROCEDURENonExample3Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(rec x (x -> bot))"); FormsVBT.PutText(fv, "typeright", "(rec y ((y -> top) -> top))"); END NonExample3Proc; PROCEDURENonExample4Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "(rec x ((x -> bot) -> bot))"); FormsVBT.PutText(fv, "typeright", "(rec y ((y -> top) -> top))"); END NonExample4Proc; PROCEDURENonExample5Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "top"); FormsVBT.PutText(fv, "typeright", "bot"); END NonExample5Proc; PROCEDURENonExample6Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "top"); FormsVBT.PutText(fv, "typeright", "bot"); END NonExample6Proc; PROCEDURENonExample7Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "top"); FormsVBT.PutText(fv, "typeright", "bot"); END NonExample7Proc; PROCEDURENonExample8Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "top"); FormsVBT.PutText(fv, "typeright", "bot"); END NonExample8Proc; PROCEDURENonExample9Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "top"); FormsVBT.PutText(fv, "typeright", "bot"); END NonExample9Proc; PROCEDURENonExample10Proc ( fv: FormsVBT.T; <* UNUSED *> name: TEXT; <* UNUSED *> eventData: REFANY; <* UNUSED *> time: VBT.TimeStamp) = BEGIN FormsVBT.PutText(fv, "typeleft", "top"); FormsVBT.PutText(fv, "typeright", "bot"); END NonExample10Proc;
TYPE
Type = OBJECT index: INTEGER END;
TypeBot = Type BRANDED OBJECT END;
TypeTop = Type BRANDED OBJECT END;
TypeFun =
Type BRANDED OBJECT
dom,rng: Type;
domEdgeIndex,rngEdgeIndex: INTEGER;
END;
PROCEDURE Notice (alg: T; lft, rht: Type) =
BEGIN
INC(alg.top);
alg.trail[alg.top].lft := lft;
alg.trail[alg.top].rht := rht;
END Notice;
PROCEDURE Seen (alg: T; lft, rht: Type): BOOLEAN =
BEGIN
FOR i:=0 TO alg.top DO
IF (alg.trail[i].lft=lft) AND (alg.trail[i].rht=rht) THEN
RETURN TRUE
END;
END;
RETURN FALSE;
END Seen;
PROCEDURE In (alg: T; lft, rht: Type;
lftLeadingEdgeIndex, rhtLeadingEdgeIndex: INTEGER): BOOLEAN
RAISES {Thread.Alerted} =
PROCEDURE At(line: INTEGER) RAISES {Thread.Alerted} =
BEGIN ZeusCodeView.At(alg, line) END At;
VAR lftRes, rhtRes: BOOLEAN; res: BOOLEAN;
BEGIN
ZeusCodeView.Enter(alg, procedureName := "In");
SubtypeIE.Enter(alg, lft.index, rht.index,
lftLeadingEdgeIndex, rhtLeadingEdgeIndex);
At(1); IF Seen(alg, lft, rht) THEN
At(12); SubtypeIE.SeenOK(alg, lft.index, rht.index);
res := TRUE;
ELSE
At(2); SubtypeIE.Notice(alg, lft.index, rht.index);
Notice(alg, lft, rht);
At(3); TYPECASE lft OF
| TypeBot =>
At(4); SubtypeIE.BotLessAnyOK(alg, lft.index, rht.index,
lftLeadingEdgeIndex, rhtLeadingEdgeIndex);
res := TRUE;
| TypeTop =>
At(5); IF ISTYPE(rht, TypeTop)
THEN
SubtypeIE.TopLessTopOK(alg, lft.index, rht.index,
lftLeadingEdgeIndex, rhtLeadingEdgeIndex);
res := TRUE;
ELSE
SubtypeIE.TopLessNonTopKO(alg, lft.index, rht.index,
lftLeadingEdgeIndex, rhtLeadingEdgeIndex);
res := FALSE;
END;
| TypeFun(lftFun) =>
At(6); TYPECASE rht OF
| TypeBot =>
At(7); SubtypeIE.FunLessBotKO(alg, lft.index, rht.index,
lftLeadingEdgeIndex, rhtLeadingEdgeIndex );
res := FALSE;
| TypeTop =>
At(8); SubtypeIE.FunLessTopOK(alg, lft.index, rht.index,
lftLeadingEdgeIndex, rhtLeadingEdgeIndex);
res := TRUE;
| TypeFun(rhtFun) =>
At(10); SubtypeIE.FunLessFun(alg, lft.index, rht.index,
lftLeadingEdgeIndex, rhtLeadingEdgeIndex);
lftRes := In(alg, rhtFun.dom, lftFun.dom,
rhtFun.domEdgeIndex, lftFun.domEdgeIndex);
IF lftRes THEN
At(11); rhtRes := In(alg, lftFun.rng, rhtFun.rng,
lftFun.rngEdgeIndex, rhtFun.rngEdgeIndex);
res := lftRes AND rhtRes;
ELSE
res := lftRes;
END;
ELSE <* ASSERT FALSE *>
END;
ELSE <* ASSERT FALSE *>
END;
END;
SubtypeIE.Exit(alg, lft.index, rht.index,
lftLeadingEdgeIndex, rhtLeadingEdgeIndex, res);
ZeusCodeView.Exit(alg);
RETURN res;
END In;
=======================================================
PROCEDURE=======================================================TravNotice (alg: T; type: Type) = BEGIN INC(alg.travTop); alg.travTrail[alg.travTop] := type; END TravNotice; PROCEDURETravSeen (alg: T; type: Type): BOOLEAN = BEGIN FOR i:=0 TO alg.travTop DO IF alg.travTrail[i]=type THEN RETURN TRUE END; END; RETURN FALSE; END TravSeen; PROCEDURENewBot (): Type = BEGIN RETURN NEW(TypeBot, index:=-1); END NewBot; PROCEDURENewTop (): Type = BEGIN RETURN NEW(TypeTop, index:=-1); END NewTop; PROCEDURENewFun (dom, rng: Type): Type = BEGIN RETURN NEW(TypeFun, index:=-1, dom:=dom, rng:=rng); END NewFun; PROCEDURETraverse (alg: T; type: Type) RAISES {Thread.Alerted} = BEGIN alg.travTop := -1; Traverse1(alg, type, type); END Traverse; PROCEDURETraverse1 (alg: T; type: Type; parent: Type) RAISES {Thread.Alerted} = BEGIN IF TravSeen(alg, type) THEN SubtypeIE.NewLoop(alg, parent.index, type.index); RETURN END; TravNotice(alg, type); TYPECASE type OF | TypeBot => INC(alg.nodeIndex); type.index := alg.nodeIndex; alg.nodes[alg.nodeIndex] := type; SubtypeIE.NewBot(alg, type.index); | TypeTop => INC(alg.nodeIndex); type.index := alg.nodeIndex; alg.nodes[alg.nodeIndex] := type; SubtypeIE.NewTop(alg, type.index); | TypeFun(fun) => INC(alg.nodeIndex); type.index := alg.nodeIndex; alg.nodes[alg.nodeIndex] := type; INC(alg.edgeIndex); fun.domEdgeIndex := alg.edgeIndex; INC(alg.edgeIndex); fun.rngEdgeIndex := alg.edgeIndex; SubtypeIE.NewFun(alg, type.index, fun.domEdgeIndex, fun.rngEdgeIndex); Traverse1(alg, fun.dom, type); Traverse1(alg, fun.rng, type); SubtypeIE.NewDomRng(alg, type.index, fun.dom.index, fun.rng.index); ELSE <* ASSERT FALSE *> END; END Traverse1; PROCEDURERun (alg: T) RAISES {Thread.Alerted} = VAR lft, rht: Type; lftRoot, rhtRoot: INTEGER; BEGIN SubtypeIE.Setup(alg); TRY lft := ParseSx(Sx.Read(TextRd.New( FormsVBT.GetText(alg.data, "typeleft"))), NIL); EXCEPT ELSE lft := NewBot(); END; TRY rht := ParseSx(Sx.Read(TextRd.New( FormsVBT.GetText(alg.data, "typeright"))), NIL); EXCEPT ELSE rht := NewBot(); END; alg.nodeIndex := -1; alg.edgeIndex := -1; lftRoot := alg.nodeIndex+1; Traverse(alg, lft); rhtRoot := alg.nodeIndex+1; Traverse(alg, rht); SubtypeIE.Begin(alg, lftRoot, rhtRoot); IF In(alg, lft, rht, -1, -1) THEN SubtypeIE.OK(alg, lft.index, rht.index, -1, -1); ELSE SubtypeIE.KO(alg, lft.index, rht.index, -1, -1); END; END Run;
Type ::=
bot
top
FunType
( rec Ide FunType )
FunType ::=
( Type -> Type )
EXCEPTION ParseSxError;
TYPE SxEnv = OBJECT
ide: TEXT;
val: TypeFun;
rest: SxEnv;
END;
PROCEDURE NewEnv (ide: TEXT; val: TypeFun; rest: SxEnv): SxEnv =
BEGIN
RETURN NEW(SxEnv, ide:=ide, val:=val, rest:=rest);
END NewEnv;
PROCEDURE Lookup (ide: TEXT; env: SxEnv): TypeFun RAISES {ParseSxError} =
BEGIN
IF env=NIL THEN RAISE ParseSxError END;
IF Text.Equal(ide, env.ide) THEN
RETURN env.val;
ELSE
RETURN Lookup(ide, env.rest);
END;
END Lookup;
PROCEDURE IsFunSx (list: RefList.T): BOOLEAN =
BEGIN
IF RefList.Length(list) # 3 THEN RETURN FALSE END;
TYPECASE RefList.Nth(list, 1) OF
| Atom.T(atom) => RETURN Text.Equal("->", Atom.ToText(atom));
ELSE RETURN FALSE;
END;
END IsFunSx;
PROCEDURE IsRecSx (list: RefList.T): BOOLEAN =
BEGIN
IF RefList.Length(list) # 3 THEN RETURN FALSE END;
TYPECASE RefList.Nth(list, 0) OF
| Atom.T(atom) => RETURN Text.Equal("rec", Atom.ToText(atom));
ELSE RETURN FALSE;
END;
END IsRecSx;
PROCEDURE ParseSx (sx: Sx.T; env: SxEnv): Type RAISES {ParseSxError} =
VAR ide: TEXT; fun: TypeFun;
BEGIN
TYPECASE sx OF
| Atom.T(atom) =>
ide := Atom.ToText(atom);
IF Text.Equal(ide, "bot") THEN
RETURN NewBot();
ELSIF Text.Equal(ide, "top") THEN
RETURN NewTop();
ELSE RETURN Lookup(ide, env);
END;
| RefList.T(list) =>
IF IsFunSx(list) THEN
RETURN NewFun(
ParseSx(RefList.Nth(list, 0), env),
ParseSx(RefList.Nth(list, 2), env));
ELSIF IsRecSx(list) THEN
TYPECASE RefList.Nth(list, 1) OF
| Atom.T(atom) =>
ide := Atom.ToText(atom);
fun := NewFun(NIL, NIL);
TYPECASE ParseSx(RefList.Nth(list, 2), NewEnv(ide, fun, env)) OF
| TypeFun(fun2) =>
fun.dom := fun2.dom;
fun.rng := fun2.rng;
RETURN fun;
ELSE RAISE ParseSxError;
END;
ELSE RAISE ParseSxError;
END;
ELSE RAISE ParseSxError;
END;
ELSE RAISE ParseSxError;
END;
END ParseSx;
PROCEDURE FmtBool (bool: BOOLEAN): TEXT =
BEGIN
IF bool THEN RETURN "true" ELSE RETURN "false" END;
END FmtBool;
BEGIN
ZeusPanel.RegisterAlg(New, "Subtyping Recursive Types", "Subtype");
END AlgSubtype.