IMPLEMENTATION MODULE YaflQuantifiers;

IMPORT LookAhead;   
IMPORT ModuleTable;
FROM YaflCfg            IMPORT CurrentSpot;
FROM YaflClasses        IMPORT ClassDeclaration;
FROM YaflClDefinition   IMPORT ClassDefinition;
FROM YaflDeclarations   IMPORT SingleDataItem;
FROM YaflType           IMPORT TypedNonTerminal; 
FROM YaflNTList         IMPORT NTList;
FROM YaflParamClasses   IMPORT ClassFormal;
FROM YaflParser         IMPORT NonTerminal;
FROM YaflPredefined     IMPORT PredefItems;
FROM YaflDeclarations   IMPORT Declaration, SingleDataItem;
FROM YaflMethods        IMPORT MethodDeclaration;
FROM YaflMetImplementation IMPORT MethodImplementation;
FROM YaflModules        IMPORT DefinitionModule;
FROM List               IMPORT List;
FROM YaflLex            IMPORT LexicalAnalyzer;
FROM YaflSymbols        IMPORT SymbolTable;
IMPORT Ref;
IMPORT Space;

  CLASS FreeVariableDataItem;
    INHERITS SingleDataItem;
    
    REDEFINE METHOD CREATE (Id: Ident);
      BEGIN
      BASE (Id, 
            VOID, 
            ReadOnly := TRUE, 
            Once := FALSE);
      END CREATE;
      
  END FreeVariableDataItem;

  ----------------------------
   CLASS SetSpecification;
     INHERITS NonTerminal(SetSpecCodeGenerator);
     
     
     VAR
       TheFirstRefExpression,
       TheSecondRefExpression,
       TheByExpression: TypedNonTerminal;
       TheFreeVariableId: Ident;
       TheFreeVariable: FreeVariableDataItem;
       TheFilters: NTList (TypedNonTerminal);
       TheStatus: INTEGER;
       TheForcedShouldRestoreStack: BOOLEAN;
       
     REDEFINE METHOD SubTree: ARRAY OF NonTerminal;
       BEGIN
       RESULT.CREATE (4);
       RESULT [0] := TheByExpression;
       RESULT [1] := TheFirstRefExpression;
       RESULT [2] := TheSecondRefExpression;
       RESULT [3] := TheFreeVariableId;
       IF TheFilters <> VOID THEN
         RESULT := RESULT + TheFilters.SubTree;
         END;
       END SubTree;  
       
     METHOD Status: INTEGER;
       BEGIN
       RESULT := TheStatus;
       ASSERT (RESULT = IntervalSetS) OR
         (RESULT = ArraySetS) OR
         (RESULT = RandomCollSetS);
       END Status;
       
     METHOD FirstRefExpression: TypedNonTerminal;
       BEGIN
       RESULT := TheFirstRefExpression;
       END FirstRefExpression;
       
     METHOD SecondRefExpression: TypedNonTerminal;
       BEGIN
       RESULT := TheSecondRefExpression;
       END SecondRefExpression;
       
     METHOD ByExpression: TypedNonTerminal;
       BEGIN
       RESULT := TheByExpression;
       ASSERT RESULT <> VOID IMPLIES SecondRefExpression <> VOID;
       END ByExpression;
       
     METHOD Filters: NTList(TypedNonTerminal);
       BEGIN
       RESULT := TheFilters;
       END Filters;
     
     METHOD FreeVariable: FreeVariableDataItem;
       BEGIN
       RESULT := TheFreeVariable;
       END FreeVariable;
       
     METHOD FreeVariableType: Type;
       BEGIN
       RESULT := TheFreeVariable.GetType;
       END FreeVariableType;
       
     METHOD RefType: Type;
       BEGIN
       RESULT := TheFirstRefExpression.GetType;
       END RefType;
       
    REDEFINE METHOD Parse(Lkh: LookAhead);
      VAR
        OldStyle: BOOLEAN;
      BEGIN
      TheFreeVariableId := Lkh.AcceptIdent;
      SetSon (TheFreeVariableId);
      IF Lkh.CurrentToken = Lkh.Becomes THEN
        OldStyle := TRUE;
        Lkh.GetToken;
       ELSE
        Lkh.Accept (Lkh.In);
        END;
      TheFirstRefExpression := Lkh.AcceptPlainExpr;
      SetSon (TheFirstRefExpression);
      IF OldStyle OR (Lkh.CurrentToken = Lkh.To) THEN
        Lkh.Accept (Lkh.To);
        TheSecondRefExpression := Lkh.AcceptPlainExpr;
        SetSon (TheSecondRefExpression);
        IF Lkh.CurrentToken = Lkh.By THEN
          Lkh.GetToken;
          TheByExpression := Lkh.AcceptPlainExpr;
          SetSon (TheByExpression);
          END;
        END;
      IF Lkh.CurrentToken = Lkh.Bar THEN
        Lkh.GetToken;
        TheFilters.CREATE;
        TheFilters.Append (Lkh.AcceptPlainExpr);
        WHILE Lkh.CurrentToken = Lkh.Comma DO
          Lkh.GetToken;
          TheFilters.Append (Lkh.AcceptPlainExpr);
          END;
        TheFilters.SetFather (THIS);
        END;
      END Parse;

    METHOD WithSideEffects: BOOLEAN;
      BEGIN
      RESULT := TheFirstRefExpression.WithSideEffects;
      RESULT := RESULT OR
             ((TheSecondRefExpression <> VOID) AND
              TheSecondRefExpression.WithSideEffects);
      RESULT := RESULT OR
             ((TheByExpression <> VOID) AND
              TheByExpression.WithSideEffects);
      IF Filters <> VOID THEN
        FOR i := 0 TO Filters.Size - 1 WHILE NOT RESULT DO
          RESULT := Filters.Get(i).WithSideEffects;
          END;
        END;
      END WithSideEffects;  
      
    REDEFINE METHOD Tag;
      BEGIN
      SymbolTable.PushLevel;
      TheFreeVariable.CREATE (TheFreeVariableId);
      SetSon (TheFreeVariable);                        
      TheFirstRefExpression.UniqueTag;
      IF TheSecondRefExpression <> VOID THEN
        TheSecondRefExpression.UniqueTag;
        IF TheByExpression <> VOID THEN
          TheByExpression.UniqueTag;
          END;
        END;
      IF TheFilters <> VOID THEN
        EnterFreeVariable;  
      	TheFilters.UniqueTag;
        END;
      SymbolTable.PopLevel;
      END Tag;
      
    METHOD EnterFreeVariable;
      BEGIN
      SymbolTable.Enter (TheFreeVariableId.Data,
                         TheFreeVariable);
      END EnterFreeVariable;
      
    REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
      BEGIN
      RESULT := "SetSpecification";
      END WhatAmI;
      
    METHOD UsesValueStack: BOOLEAN;
      BEGIN
      RESULT := TheFirstRefExpression.UsesValueStack OR
                ((TheSecondRefExpression <> VOID) AND
                 (TheSecondRefExpression.UsesValueStack)) OR
                ((TheByExpression <> VOID) AND
                 (TheByExpression.UsesValueStack));
      RESULT := RESULT OR (TheStatus = ArraySetS) OR 
                (TheStatus = RandomCollSetS);           
      END UsesValueStack;
      
    REDEFINE METHOD CheckType;
      VAR
        RType, IntType, BoolType: Type;
        Formal: ClassFormal;
        Actual: ClassDeclaration;
        RandomCollClass: ClassDeclaration;
      BEGIN
      IntType := PredefItems.Integer.MakeType(0);
      BoolType := PredefItems.Boolean.MakeType(0);
      IF TheSecondRefExpression = VOID THEN
        RType := RefType;
        IF RType <> VOID THEN
          IF RType.ArrayLevel > 0 THEN
            TheStatus := ArraySetS;
            TheFreeVariable.SetType( 
              RType.ConstrainedClass.MakeType (RType.ArrayLevel - 1));
           ELSE
            RandomCollClass := ModuleTable.RandomCollectionClass;
            IF RandomCollClass.Compatible(RType.SimpleType) THEN
              TheStatus := RandomCollSetS;
              ASSERT RandomCollClass.ClassFormals.Size = 1;
              Formal := RandomCollClass.ClassFormals.FormalList.Get(0);
              Actual := RType.ConstrainedClass.GetFormalValue (Formal);
              TheFreeVariable.SetType (Actual.MakeType(0));
              ForceShouldRestoreStack;
             ELSE
              TheFirstRefExpression.Error ("Not a valid collection");
              END;
            END;
          END;
       ELSE
        TheStatus := IntervalSetS;
        IF NOT TheFirstRefExpression.GetType.Match(IntType) THEN
          TheFirstRefExpression.Error ("Not an integer expression[1]");
          END;
        IF NOT TheSecondRefExpression.GetType.Match(IntType) THEN
          TheSecondRefExpression.Error ("Not an integer expression[2]");
          END;
        IF TheByExpression <> VOID THEN
          IF NOT TheByExpression.GetType.Match (IntType) THEN
            TheByExpression.Error ("Not an integer expression[3]");
           ELSIF TheByExpression.GetFolded = VOID THEN
            TheByExpression.Error ("Must be a compile-time constant");
            END;
          END;
        TheFreeVariable.SetType (IntType);
        END;
      IF FreeVariableType <> VOID THEN
        FOR f IN TheFilters | f <> VOID, f.GetType <> VOID DO
          VOID := f.GetType.Match(BoolType);
          END;
        END;
      END CheckType;
      
     METHOD ShouldRestoreStack: BOOLEAN;
       BEGIN
       RESULT := TheForcedShouldRestoreStack OR
            THERE_IS Filt IN TheFilters :- Filt.UsesValueStack;
       END ShouldRestoreStack;
       
     METHOD ForceShouldRestoreStack;
       BEGIN
       TheForcedShouldRestoreStack := TRUE;
       ASSERT ShouldRestoreStack;
       END ForceShouldRestoreStack;
        
    METHOD CheckForPossibleConflicts: Declaration;
      VAR
        EnclMeth: ONCE Ref(MethodImplementation);
        Nt: NonTerminal;
      BEGIN
      IF TheFreeVariableId <> VOID THEN
        Nt := SymbolTable.Find (TheFreeVariableId.Data);
        IF Nt <> VOID THEN
          WHAT Nt OF
            IN Declaration:
              IF EnclMeth = VOID THEN
                EnclMeth.CREATE(VOID);
                END;
              TAG.GetAncestor (EnclMeth);
              IF EnclMeth.Get = CurrentSpot.CurrentMethod THEN
                RESULT := TAG;
                END;  
              EnclMeth.Set (VOID);  
              END;
           ELSE
            END;
          END;
        END;
      END CheckForPossibleConflicts;
  
    METHOD AddMethodCalls (CallList: CallReferenceList);
      VAR
        CRef: CallReference;
        Cl: ClassDeclaration;
      BEGIN
      ASSERT CallList <> VOID;
      -- To Be filled
      CASE TheStatus OF
        ArraySetS,
        IntervalSetS:
          END;
        RandomCollSetS:
          Cl := RefType.SimpleType;
          CRef.CREATE (Cl.Module.Id.Data, Cl.Id.Data, Space.StoreString ("Get"));
          CallList.Append (CRef);
          CRef.CREATE (Cl.Module.Id.Data, Cl.Id.Data, Space.StoreString ("Size"));
          CallList.Append (CRef);
          END;
        END;
      END AddMethodCalls;
      
   END SetSpecification;
   
   -------------------------------------
   
   CLASS Quantifier;
     INHERITS TypedNonTerminal(QuantifierCodeGenerator);
     
     VAR
       TheArgument: TypedNonTerminal;
       TheSpec: SetSpecification;
       TheCode: INTEGER;
       
     METHOD Code: INTEGER;
       BEGIN
       RESULT := TheCode;
       END Code;
       
     METHOD SetSpec: SetSpecification;
       BEGIN
       RESULT := TheSpec;
       END SetSpec;
       
     REDEFINE METHOD SubTree: ARRAY OF NonTerminal;
       BEGIN
       RESULT.CREATE (2);
       RESULT [0] := TheArgument;
       RESULT [1] := TheSpec;
       END SubTree;  
       
     METHOD Argument: TypedNonTerminal;
       BEGIN
       RESULT := TheArgument;
       END Argument;
       
     METHOD FreeVariableType: Type;
       BEGIN
       RESULT := TheSpec.FreeVariableType;
       END FreeVariableType;
       
     REDEFINE METHOD GetType: Type;
       BEGIN
       RESULT := BASE;
       END GetType;
       
    REDEFINE METHOD Parse(Lkh: LookAhead);
      BEGIN
      TheCode := Lkh.CurrentToken;
      Lkh.GetToken;
      TheSpec := Lkh.AcceptSetSpecification;
      SetSon (TheSpec);
      Lkh.Accept (Lkh.BigDot);
      TheArgument := Lkh.AcceptPlainExpr;
      SetSon (TheArgument);
      END Parse;
      
    REDEFINE METHOD Tag;
      BEGIN
      TheSpec.UniqueTag;
      SymbolTable.PushLevel;
      TheSpec.EnterFreeVariable;
      TheArgument.UniqueTag;                                             
      SymbolTable.PopLevel;
      END Tag;
      
    REDEFINE METHOD Functional: BOOLEAN;
      BEGIN
      RESULT := FALSE;
      END Functional;
      
    REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
      BEGIN
      RESULT := "Quantifier";
      END WhatAmI;
      
    REDEFINE METHOD Isomorph (Other: TypedNonTerminal): BOOLEAN;
      BEGIN
      END Isomorph;
      
    REDEFINE METHOD UsesValueStack: BOOLEAN;
      BEGIN
      RESULT := TheSpec.UsesValueStack;
      END UsesValueStack;
      
    REDEFINE METHOD BuildType: Type;
      VAR
        ArgType: Type;
      BEGIN
      TheSpec.UniqueCheckType;
      ArgType := TheArgument.GetType;
      IF ArgType <> VOID THEN
        IF NOT ArgType.Match (PredefItems.Boolean.MakeType(0)) THEN
          TheArgument.Error ("Non-boolean quantifier expression");
          END;
        END;
      IF TheArgument.UsesValueStack THEN
        TheSpec.ForceShouldRestoreStack;
        END;  
      CASE TheCode OF
        LexicalAnalyzer.First,
        LexicalAnalyzer.Last:
          RESULT := FreeVariableType;
          END;
        LexicalAnalyzer.ThereIs,
        LexicalAnalyzer.ForAll:
          RESULT := PredefItems.Boolean.MakeType(0);
          END;
        LexicalAnalyzer.All:
          RESULT := 
            FreeVariableType.ConstrainedClass.
                  MakeType(FreeVariableType.ArrayLevel + 1);
     	  END;
        END;
      END BuildType;

    REDEFINE METHOD WithSideEffects: BOOLEAN;
      BEGIN
      RESULT := TheSpec.WithSideEffects OR
                TheArgument.WithSideEffects;
      END WithSideEffects;
        
   END Quantifier;
   
   
END YaflQuantifiers;
