(* 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;