(* This is the algorithm for subtyping recursive types, written in Modula-3.
The original algorithm, as implemented in the Amber programming language,
and as described in the paper "Subtyping Recursive Types", is exponential
in the number of node pairs visited.
The present algorithm, as implemented in the Quest programmig language,
is only n-square in the number of node pairs visited.
The difference between the two algorithms is simply that in the exponential
case the trail is used as a stack, while in the n-square case nothing put
on the trail is ever forgotten (in practice, one would flush the trail at
module boundaries).
Currently, no known algorithms are bettern than n-square.
*)
TYPE
Type = OBJECT END;
TypeBot = Type BRANDED OBJECT END;
TypeTop = Type BRANDED OBJECT END;
TypeFun = Type BRANDED OBJECT dom,rng: Type END;
VAR
trail: ARRAY [0..1000] OF RECORD lft,rht: Type END;
top: INTEGER := -1;
PROCEDURE Notice(lft, rht: Type) =
BEGIN
INC(top);
trail[top].lft := lft;
trail[top].rht := rht;
END Notice;
PROCEDURE Seen(lft, rht: Type): BOOLEAN =
BEGIN
FOR i:=0 TO top DO
IF (trail[i].lft=lft) AND (trail[i].rht=rht) THEN RETURN TRUE END;
END;
RETURN FALSE;
END Seen;
PROCEDURE In(lft, rht: Type): BOOLEAN =
BEGIN
IF Seen(lft, rht) THEN RETURN TRUE END;
Notice(lft, rht);
TYPECASE lft OF
| TypeBot => RETURN TRUE;
| TypeTop => RETURN ISTYPE(rht, TypeTop);
| TypeFun(lftFun) =>
TYPECASE rht OF
| TypeBot => RETURN FALSE;
| TypeTop => RETURN TRUE;
| TypeFun(rhtFun) =>
RETURN
In(rhtFun.dom, lftFun.dom) AND
In(lftFun.rng, rhtFun.rng);
END;
END;
END In;