(* Copyright (C) 1989, Digital Equipment Corporation           *)
(* All rights reserved.                                        *)
(* See the file COPYRIGHT for a full description.              *)

(* File: Revelation.m3                                         *)
(* Last modified on Fri May 11 11:09:02 1990 by muller         *)
(*      modified on Sat Feb 10 22:14:45 1990 by kalsow         *)


MODULE Revelation;

IMPORT String, Value, Type, Module, Error, OpaqueType, Scope;
IMPORT ObjectType, RefType, Emit, Scanner, Token, Scanner;
IMPORT Host, Text, FPrint, Wr, TextWr, Decl;
FROM Scanner IMPORT GetToken, Fail, Match, MatchID, cur;

TYPE
  T = UNTRACED REF RECORD
        qid     : String.QID;
        obj     : Value.T; (* value named by qid *)
        value   : Type.T;  (* REVEAL qid <:/== value *)
        opaque  : Type.T;  (* == type that corresponds to qid *)
        equal   : BOOLEAN; (* TRUE => (qid = value), FALSE => (qid <: value) *)
        bound   : BOOLEAN;
        inBind  : BOOLEAN;
        checked : BOOLEAN;
        depth   : INTEGER;
        origin  : INTEGER;
      END;

TYPE
  List = UNTRACED REF RECORD
           next  : List;
	   ident : T;
	   local : BOOLEAN;
	   used  : BOOLEAN;
         END;

REVEAL
  Set = UNTRACED BRANDED REF RECORD
          idents : List;
          next   : Set;
        END;

VAR
  all: List;
  top: Set;

PROCEDURE PushNew (): Set =
  VAR s: Set;
  BEGIN
    s := NEW (Set);
    s.next   := top;
    s.idents := NIL;
    top      := s;
    RETURN s;
  END PushNew;

PROCEDURE Push (s: Set) =
  BEGIN
    <* ASSERT s # NIL AND s.next = NIL *>
    s.next := top;
    top    := s;
  END Push;

PROCEDURE Pop () =
  VAR s: Set;
  BEGIN
    s      := top;
    top    := s.next;
    s.next := NIL;
  END Pop;

PROCEDURE Parse (READONLY fail: Token.Set; att: Decl.Attributes) =
  TYPE TK = Token.T;
  VAR fail2: Token.Set;  id, id2: String.T;  loc: INTEGER;
  BEGIN
    IF att.isExternal THEN Error.Msg ("a revelation cannot be external"); END;
    IF att.isInline   THEN Error.Msg ("a revelation cannot be inline"); END;
    IF att.isObsolete THEN Error.Msg ("a revelation cannot be obsolete"); END;
    IF att.isUnused   THEN Error.Msg ("a revelation cannot be unused"); END;

    Match (TK.tREVEAL, fail, Token.Set {TK.tSEMI});
    fail2 := fail + Token.Set {TK.tSEMI};
    WHILE (cur.token = TK.tIDENT) DO
      id2 := NIL;
      id  := MatchID (fail2, Token.TypeStart
                               + Token.Set {TK.tEQUAL, TK.tDOT, TK.tSUBTYPE});
      IF (cur.token = TK.tDOT) THEN
        GetToken (); (* . *)
        id2 := id;
        id := MatchID (fail2, Token.Set {TK.tEQUAL, TK.tSUBTYPE});
      END;
      loc := Scanner.offset;
      CASE cur.token OF
      | TK.tEQUAL =>
          GetToken (); (* = *)
          New (id2, id, Type.Parse (fail2), TRUE, loc);
      | TK.tSUBTYPE =>
          GetToken (); (* <: *)
          New (id2, id, Type.Parse (fail2), FALSE, loc);
      ELSE Fail ("missing \'=\' or \'<:\'", fail);
      END;
      Match (TK.tSEMI, fail, Token.Set {});
    END;
  END Parse;

PROCEDURE New (module, name: String.T;  value: Type.T;
                                                 eq: BOOLEAN;  loc: INTEGER) =
  VAR t: T; l: List;
  BEGIN
    t := NEW (T);
    t.qid.module := module;
    t.qid.item   := name;
    t.obj        := NIL;
    t.value      := value;
    t.opaque     := NIL;
    t.equal      := eq;
    t.bound      := FALSE;
    t.inBind     := FALSE;
    t.checked    := FALSE;
    t.depth      := Module.depth;
    t.origin     := loc;

    l := NEW (List);
    l.next  := top.idents;   top.idents := l;
    l.ident := t;
    l.local := TRUE;
    l.used  := FALSE;

    l := NEW (List);
    l.next  := all;  all := l;
    l.ident := t;

  END New;

PROCEDURE Inherit (s: Set) =
  VAR x, y: List;
  BEGIN
    x := s.idents;
    WHILE (x # NIL) DO
      y := NEW (List);
      y.next  := top.idents;   top.idents := y;
      y.ident := x.ident;
      y.local := FALSE;
      y.used  := FALSE;
      x := x.next;
    END;
  END Inherit;

PROCEDURE Bind (s: Set) =
  VAR l: List; save: INTEGER;
  BEGIN
    save := Scanner.offset;
    l := s.idents;
    WHILE (l # NIL) DO BindLHS (l.ident); l := l.next;  END;
    (* now, LookUps are enabled *)
    l := s.idents;
    WHILE (l # NIL) DO BindRHS (l.ident); l := l.next;  END;
    Scanner.offset := save;
  END Bind;

PROCEDURE BindLHS (t: T) =
  VAR obj: Value.T;
  BEGIN
    IF (t.bound) THEN RETURN END;
    <* ASSERT NOT t.checked *>
    Scanner.offset := t.origin;
    IF (t.inBind) THEN
      Error.QID (t.qid, "recursive revelation");
      RETURN;
    END;
    t.inBind := TRUE;
    obj := Scope.LookUpQID (t.qid);
    t.obj := obj;
    IF (obj = NIL) THEN
      Error.QID (t.qid, "undefined");
      t.opaque := t.value;
    ELSIF (Value.ClassOf (obj) # Value.Class.Type) THEN
      Error.QID (t.qid, "is not a type");
      t.opaque := t.value;
    ELSE
      t.opaque := Value.ToType (obj);
      IF (t.equal) AND (t.depth # 1) THEN
        (* this is an imported revelation *)
        Type.NoteDeclaration (t.value, obj);
      END;
    END;
    t.inBind := FALSE;
  END BindLHS;

PROCEDURE BindRHS (t: T) =
  BEGIN
    IF (t.bound) THEN RETURN  END;
    <* ASSERT NOT t.checked *>
    Scanner.offset := t.origin;
    IF (t.inBind) THEN
      Error.QID (t.qid, "recursive revelation");
      t.bound := TRUE;
      RETURN ;
    END;
    t.inBind := TRUE;
    t.opaque := Type.Bind (t.opaque);
    t.value  := Type.Bind (t.value);
    t.inBind := FALSE;
    t.bound  := TRUE;
  END BindRHS;

PROCEDURE TypeCheck (s: Set) =
  VAR l: List;  save: INTEGER;
  BEGIN
    save := Scanner.offset;
    l := s.idents;
    WHILE (l # NIL) DO DoCheck (l.ident); l := l.next;  END;
    Scanner.offset := save;
  END TypeCheck;

PROCEDURE DoCheck (t: T) =
  VAR type: Type.T;
  BEGIN
    IF (t.checked) THEN RETURN  END;
    <* ASSERT t.bound *>
    Scanner.offset := t.origin;
    type := t.value;
    Type.Check (type);
    Type.Check (t.opaque);
    IF (NOT OpaqueType.Is (t.opaque)) THEN
      Error.QID (t.qid, "is not an opaque type");
    ELSIF NOT Type.IsSubtype (type, OpaqueType.Super (t.opaque)) THEN
      Error.QID (t.qid, "identification is not to a legal subtype");
    END;
    IF (t.equal) THEN
      IF NOT (RefType.IsBranded (type) OR ObjectType.IsBranded (type)) THEN
        Error.QID (t.qid,
                   "must be identified with a new branded reference type");
      END;
    END;
    t.checked := TRUE;
  END DoCheck;

PROCEDURE LookUp (key: Type.T): Type.T =
  VAR t: T;  l: List;  save: INTEGER;
  BEGIN
    l := top.idents;
    WHILE (l # NIL) DO
      t := l.ident;
      <* ASSERT t.value = NIL OR t.opaque # NIL *> (* => LHS is bound *)
      IF (t.equal) AND (t.opaque = key) THEN
        l.used := TRUE;
        IF (NOT t.bound) THEN
          (* => we're doing a lookup while binding the revelations *)
          save := Scanner.offset;
          BindRHS (t);
          Scanner.offset := save;
        END;
        RETURN t.value;
      END;
      l := l.next;
    END;
    RETURN NIL;
  END LookUp;

PROCEDURE LookUpAll (key: Type.T): Type.List =
  VAR t: T; l: List; matches, z: Type.List; save: INTEGER;
  BEGIN
    matches := NIL;
    l := top.idents;
    WHILE (l # NIL) DO
      t := l.ident;
      <* ASSERT t.value = NIL OR t.opaque # NIL *> (* => LHS is bound *)
      IF (t.opaque = key) THEN
        l.used := TRUE;
        IF (NOT t.bound) THEN
          (* => we're doing a lookup while binding the revelations *)
          save := Scanner.offset;
          BindRHS (t);
          Scanner.offset := save;
        END;
        z := NEW (Type.List);
        z.next := matches;
        z.type := t.value;
        matches := z;
      END;
      l := l.next;
    END;
    RETURN matches;
  END LookUpAll;

VAR
  typeMap: Type.Map := NIL;
  fpWriter: Wr.T;
  fpBusy: BOOLEAN;


PROCEDURE Declare (s: Set) =
  VAR l: List;
  BEGIN
    <* ASSERT NOT fpBusy *>
    fpBusy := TRUE;
    IF (typeMap = NIL) THEN
      typeMap := Type.NewMap ();
      fpWriter := TextWr.New ();
    END;

    l := s.idents;
    WHILE (l # NIL) DO
      IF (l.used) THEN DeclareOne (l.ident, l.local);  END;
      l := l.next;
    END;

    fpBusy := FALSE;
  END Declare;

PROCEDURE DeclareOne (t: T;  local: BOOLEAN) =
  VAR fpText: Text.T;  fprint: FPrint.T;
  BEGIN
    Value.Declare0 (t.obj);

    FOR i := 0 TO LAST (typeMap^) DO typeMap[i] := 0 END;

    IF Host.versionStamps THEN
      IF (t.equal)
        THEN Wr.PutText (fpWriter, "== ");
        ELSE Wr.PutText (fpWriter, "<: ");
      END;
      Type.Fingerprint (t.value, typeMap, fpWriter);
      fpText := TextWr.ToText (fpWriter);
      fprint := FPrint.FromText (fpText);
  
      IF local AND Host.incrementalVersion < 1
        THEN Emit.Op ("EXPORT ");
        ELSE Emit.Op ("IMPORT ");
      END;
      Emit.OpN ("char VS@__", t.obj);
      Emit.OpHH ("@@", fprint[0], fprint[1]);
      IF (local) AND Host.incrementalVersion < 1 THEN
        Emit.Op (" = \'\\0\'");
      END;
      Emit.Op (";\n");
      IF (Host.verbose) THEN Emit.Comment (fpText) END;
    END;
  END DeclareOne;

PROCEDURE GenIdentifications () =
  VAR t: T;  l: List;  i, j, save: INTEGER;
  BEGIN
    save := Scanner.offset;
    l := all;
    WHILE (l # NIL) DO
      t := l.ident;
      IF (t.depth = 1) AND (t.equal) THEN
        (* this is a local type identification *)
        Scanner.offset := t.origin;
        i := Type.Name (t.opaque);
        j := Type.Name (t.value);
        Emit.OpII ("IDENTIFYTYPES (TC@, TC@);\n", i, j);
      END;
      l := l.next;
    END;
    Scanner.offset := save;
  END GenIdentifications;

PROCEDURE GenSubtypeChecks () =
  VAR t: T;  l: List;  i, j, save: INTEGER;
  BEGIN
    save := Scanner.offset;
    l := all;
    WHILE (l # NIL) DO
      t := l.ident;
      IF (t.depth = 1) AND (NOT t.equal) THEN
        (* this is a local subtype revelation *)
        Scanner.offset := t.origin;
        i := Type.Name (t.opaque);
        j := Type.Name (t.value);
        Emit.OpII ("CHECKSUBTYPE (TC@, TC@);\n", i, j);
      END;
      l := l.next;
    END;
    Scanner.offset := save;
  END GenSubtypeChecks;

PROCEDURE Initialize () =
  BEGIN
    all := NEW (List);  all := NIL;
    top := NEW (Set);  top.idents := NIL;  top.next := NIL;
  END Initialize;

BEGIN
END Revelation.