IMPLEMENTATION MODULE YaflPreconditions;

FROM YaflExpressions       IMPORT Expression;
FROM YaflType              IMPORT TypedNonTerminal, 
                                  Type; 
FROM YaflIdentifiers       IMPORT Ident;
FROM YaflPredefined        IMPORT PredefItems,
                                  PredefClass,
                                  PredefNoChangeMethod;
FROM YaflDeclarations      IMPORT SingleDataItem;
FROM Streams               IMPORT StdOut;
FROM YaflSymbols           IMPORT SymbolTable;
FROM List                  IMPORT List;
FROM Conversions           IMPORT IntConversions;
FROM YaflMethods           IMPORT MethodDeclaration, 
                                  Formal,
                                  FormalList;
FROM YaflMetImplementation IMPORT MethodImplementation;
FROM YaflMetDefinition     IMPORT MethodDefinition;
FROM YaflClasses           IMPORT ClassDeclaration;
FROM YaflModules           IMPORT CompilationUnit;
FROM YaflAsGC              IMPORT AssertionGC;    
FROM YaflCfg               IMPORT YaflCfg;
FROM YaflIdentifiers       IMPORT Ident;
FROM YaflParser            IMPORT LimitedWalker;
FROM YaflDesignator        IMPORT Desig,
                                  DesigElement;
IMPORT LookAhead;


   CLASS Assertion(gc IN AssertionCodeGenerator);
     INHERITS NonTerminal(gc);

     VAR
       ExprDeclaredFlag: BOOLEAN;
     
     REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
       BEGIN
       RESULT := "Assertion";
       END WhatAmI;
        
       
     REDEFINE METHOD Parse(Lkh: LookAhead);
       BEGIN   
       BASE(Lkh);
       END Parse;
       
     REDEFINE METHOD Tag;
       BEGIN   
       DEBUG
         StdOut.WriteLine("I am : " + WhatAmI);
         IF Father = VOID THEN
           StdOut.WriteLine("I do not have Father");
           END;
         END;
       END Tag;
   
     REDEFINE METHOD CheckType;
       BEGIN   
       --StdOut.WriteLine("General Assertion CheckType : " + WhatAmI);
       END CheckType;
       

   END Assertion;

----------------------------------------------------------
   CLASS MethodAssertion(gc IN MethAssertCodeGenerator);
     INHERITS Assertion(gc);
     
     METHOD Method: MethodDeclaration;
       BEGIN
       WHAT Father OF
         IN MethodDeclaration:
           RESULT := TAG;
           END;
         END;
       END Method;
    
    
     METHOD EnterThis;
       BEGIN
       Method.This.Enter;
       END EnterThis;  
       
     METHOD ReferToFormal(Root: TypedNonTerminal): BOOLEAN;
       VAR
         Walk: LimitedWalker(DesigElement);
         Tmp:  DesigElement;
       BEGIN
       Walk.CREATE(Root);
       Tmp := Walk.Next;
       WHILE (NOT RESULT) AND (Tmp <> VOID) DO
         ASSERT Tmp.Id <> VOID;
         ASSERT Tmp.Id.GetRef <> VOID;
         WHAT Tmp.Id.GetRef OF
           IN SingleDataItem:
             IF TAG.IsFormal THEN
               RESULT := TRUE;
               END;
             END;
         ELSE
           END;    
         Tmp := Walk.Next;  
         END;
       END ReferToFormal;

   END MethodAssertion;
----------------------------------------------------------
   CLASS PreCondition;
     INHERITS MethodAssertion(PreCondCodeGenerator);
     
     VAR
       TheConditions: AssertionExpressionList;
       TheImplConditions, TheDefConditions: AssertionExpressionList;
       
     REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
       BEGIN
       RESULT := "PreCondition";
       END WhatAmI;
       
       
     REDEFINE METHOD Parse (Lkh: LookAhead);
       BEGIN   
       IF YaflCfg.VerboseLevel >= 3 THEN
         StdOut.WriteLine("Parse Precondition"); 
         END;
       ASSERT Lkh.CurrentToken = Lkh.Pre;
       Lkh.GetToken;
       TheConditions := Lkh.AcceptAssertionExpressionList (THIS);
       Lkh.Accept(Lkh.SemiColon);
       END Parse;
          
       
     REDEFINE METHOD Tag;
       BEGIN  
       ASSERT TheConditions <> VOID;  
       IF YaflCfg.VerboseLevel >= 3 THEN
         StdOut.WriteLine("Tag PreConditions " + GrandPa.Id.Data + "(" 
                        + IntConversions.IntToString(LineNr,0) + ","
                        + IntConversions.IntToString(ColNr,0) + ")" );
         END;               
       TheConditions.UniqueTag;
       IF TheConditions.Size > 16 THEN
         Warning("a precondition may not contain more than 16 conditions");
         END;
       END Tag;
     
     VAR
       ConditionsIsMerged: BOOLEAN;  

     METHOD MergePreconditions;
       BEGIN
       IF NOT ConditionsIsMerged THEN
         ConditionsIsMerged := TRUE;
         -- We merge the conditions of the definition and the implementation;
         WHAT Father OF
           IN MethodImplementation:
             TheImplConditions := TheConditions;
             IF TAG.Definition <> VOID THEN
               IF TAG.Definition.GetPreCondition <> VOID THEN
                 TheDefConditions := TAG.Definition.GetPreCondition.TheConditions;
                 -- to avoid problems, we use the same lists in both the definition
                 -- and the implementation.
                 TAG.Definition.GetPreCondition.TheDefConditions:= TheDefConditions;
                 IF NOT TAG.Definition.GetPreCondition.ConditionsIsMerged THEN
                   TAG.Definition.GetPreCondition.ConditionsIsMerged := TRUE;
                   TAG.Definition.GetPreCondition.TheImplConditions:= TheImplConditions;
                   END;
               ELSE
                 TAG.Definition.SetPreCondition(THIS);
                 END;
               END;
             END;
           IN MethodDefinition:
             TheDefConditions := TheConditions;
             END;
           END;
       ELSE
         Error("(Pre)Conditions merged twice");
         END;  
       END MergePreconditions;
       
     REDEFINE METHOD CheckType;
       BEGIN
       BASE;  
       ASSERT TheConditions <> VOID;  
       TheConditions.UniqueCheckType;
       IF YaflCfg.VerboseLevel > 2 THEN
         FOR Ind := 0 TO TheConditions.Size-1 DO
           IF ReferToFormal(TheConditions.Get(Ind)) THEN
             StdOut.WriteLine("Expr :("
              + IntConversions.IntToString(TheConditions.Get(Ind).LineNr,0)
              + ","
              + IntConversions.IntToString(TheConditions.Get(Ind).ColNr,0)
              +") refer to formal");
             END;
           END;  
         END;
       MergePreconditions;
       END CheckType;
       
     REDEFINE METHOD SubTree: ARRAY OF NonTerminal;
       BEGIN
       RESULT := TheConditions.SubTree;
       END SubTree;
            
       
     METHOD Conditions: AssertionExpressionList;
       BEGIN
       RESULT := TheConditions;
       END Conditions;  
       
     METHOD ImplementationConditions: AssertionExpressionList;
       BEGIN
       RESULT := TheImplConditions;
       END ImplementationConditions;  
       
     METHOD DefinitionConditions: AssertionExpressionList;
       BEGIN
       RESULT := TheDefConditions;
       END DefinitionConditions;  
       
   END PreCondition;

----------------------------------------------------------

   CLASS PostCondition;
     INHERITS MethodAssertion(PostCondCodeGenerator);
     
     VAR
       TheConditions: PostExpressionList;
       TheImplConditions, TheDefConditions: PostExpressionList;
       TheOldExprs: List(TypedNonTerminal);
       
     METHOD Conditions: PostExpressionList;
       BEGIN
       RESULT := TheConditions;
       END Conditions;  
       
     METHOD ImplementationConditions: PostExpressionList;
       BEGIN
       RESULT := TheImplConditions;
       END ImplementationConditions;  
       
     METHOD DefinitionConditions: PostExpressionList;
       BEGIN
       RESULT := TheDefConditions;
       END DefinitionConditions;  
       
     REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
       BEGIN
       RESULT := "PostCondition";
       END WhatAmI;
       
     METHOD OldExpressions: List(TypedNonTerminal);
       BEGIN
       IF TheOldExprs = VOID THEN
         TheOldExprs.CREATE;
         END;
       RESULT := TheOldExprs;
       END OldExpressions;

     METHOD GetMethod: MethodDeclaration;
       BEGIN
       WHAT Father OF 
         IN MethodDeclaration:
           RESULT := TAG;
           END;
         END;
       END GetMethod;

     VAR
       TheClosedOldExprs: List(TypedNonTerminal);

     METHOD AttachOldExpression (TheExpr: TypedNonTerminal);
       BEGIN
       IF TheOldExprs = VOID THEN
         TheOldExprs.CREATE;
         END;
       TheOldExprs.Append(TheExpr);  
       END AttachOldExpression;
      
      
     REDEFINE METHOD Parse(Lkh: LookAhead);
       BEGIN    
       ASSERT Lkh.CurrentToken = Lkh.Post;
       Lkh.GetToken;
       TheConditions := Lkh.AcceptPostExpressionList (THIS);
       Lkh.Accept(Lkh.SemiColon);
       END Parse;
          
       
     REDEFINE METHOD Tag;
       BEGIN  
       ASSERT TheConditions <> VOID;  
       IF YaflCfg.VerboseLevel >= 3 THEN
         StdOut.WriteLine("Tag PostCondition (" 
                          + IntConversions.IntToString(LineNr,0) + ","
                          + IntConversions.IntToString(ColNr,0) + ")" );
         END;                 
       TheConditions.UniqueTag;
       -- handle the NoChange
       FOR Cond IN TheConditions DO
         WHAT Cond OF
           IN Desig:
             IF TAG.Last.Id.GetRef = PredefItems.NoChange THEN
               GetMethod.SetNoChangeRequested;
             ELSIF TAG.Last.Id.GetRef = PredefItems.NoChangeHC THEN
               GetMethod.SetNoChangeHCRequested;
               END;
             END;
         ELSE    
           END;
         END;
       IF TheConditions.Size > 16 THEN
         Warning("a postcondition may not contain more than 16 conditions");
         END;
       END Tag;

     VAR
       ConditionsIsMerged: BOOLEAN;  
       
     METHOD MergePostConditions;
       BEGIN
       IF NOT ConditionsIsMerged THEN
         ConditionsIsMerged := TRUE;
         -- We merge the conditions of the definition and the implementation;
         -- we must be sure that the OldExpressions list is created.
         VOID := OldExpressions;  
         WHAT Father OF
           IN MethodImplementation:
             TheImplConditions := Conditions;
             IF TAG.Definition <> VOID THEN
               IF TAG.Definition.GetPostCondition <> VOID THEN
                 TheDefConditions := TAG.Definition.GetPostCondition.TheConditions;
                 -- to avoid problems, we use the same list in both the definition
                 -- and the implementation.
                 TAG.Definition.GetPostCondition.TheImplConditions := TheImplConditions;
                 TAG.Definition.GetPostCondition.TheDefConditions := TheDefConditions;
                 TAG.Definition.GetPostCondition.ConditionsIsMerged := TRUE;
                 FOR Ind := 0 TO TAG.Definition.GetPostCondition.
                                                          OldExpressions.Size-1 DO
                   TheOldExprs.Append(TAG.Definition.GetPostCondition.
                                                            TheOldExprs.Get(Ind));
                   END;
                 -- to avoid problems, we use the same list in both the definition
                 -- and the implementation.
                 TAG.Definition.GetPostCondition.TheOldExprs := TheOldExprs;
               ELSE
                 TAG.Definition.SetPostCondition(THIS);
                 END;
               END;
             END;
           IN MethodDefinition:
             TheDefConditions := TheConditions;
             END;
           END;
         END;    
       END MergePostConditions;
       
     REDEFINE METHOD CheckType;
       BEGIN  
       BASE;
       ASSERT TheConditions <> VOID;  
       TheConditions.UniqueCheckType;
       MergePostConditions;
       END CheckType;
       
     REDEFINE METHOD SubTree: ARRAY OF NonTerminal;
       BEGIN
       RESULT.CREATE (TheConditions.Size);
       FOR Ind := 0 TO TheConditions.Size-1 DO
         RESULT[Ind] := TheConditions.Get(Ind);
         END;
       END SubTree;
       
    END PostCondition;

----------------------------------------------------------

   CLASS Invariant(gc IN InvCodeGenerator);
     INHERITS Assertion(gc);
     
     VAR
       TheConditions: AssertionExpressionList;
       
       
     REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
       BEGIN
       RESULT := "Invariant";
       END WhatAmI;
       
     REDEFINE METHOD Parse(Lkh: LookAhead);
       BEGIN    
       ASSERT Lkh.CurrentToken = Lkh.Invariant;
       Lkh.GetToken;
       TheConditions := Lkh.AcceptAssertionExpressionList (THIS);
       Lkh.Accept(Lkh.SemiColon);
       END Parse;
          
       
     REDEFINE METHOD Tag;
       BEGIN  
       ASSERT TheConditions <> VOID;  
       IF YaflCfg.VerboseLevel > 3 THEN
         StdOut.WriteLine ("Tagging invariant");
         END;
       TheConditions.UniqueTag;
       END Tag;
       
     REDEFINE METHOD CheckType;
       BEGIN  
       ASSERT TheConditions <> VOID;  
       IF YaflCfg.VerboseLevel > 3 THEN
         StdOut.WriteLine ("Checking Type : invariant");
         END;
       TheConditions.UniqueCheckType;
       END CheckType;
       
     REDEFINE METHOD SubTree: ARRAY OF NonTerminal;
       BEGIN
       RESULT := TheConditions.SubTree;
       END SubTree;
   
   END Invariant;

----------------------------------------------------------

   CLASS ClassInvariant;
     INHERITS Invariant(ClassInvCodeGenerator);
   
     REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
       BEGIN
       RESULT := "ClassInvariant";
       END WhatAmI;
       
   END ClassInvariant;

----------------------------------------------------------

   CLASS LoopInvariant;
     INHERITS Invariant(LoopInvCodeGenerator);
   
     REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
       BEGIN
       RESULT := "LoopInvariant";
       END WhatAmI;
       
   END LoopInvariant;

----------------------------------------------------------

   CLASS PostExpression(gc IN PostExprCodeGenerator);
     INHERITS TypedNonTerminal(gc);
       
     REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
       BEGIN
       RESULT := "PostExpression";
       END WhatAmI;
       
       
     REDEFINE METHOD Tag;
       BEGIN   
       StdOut.WriteLine("Tag : " + WhatAmI);
       END Tag;
   
     REDEFINE METHOD CheckType;
       BEGIN   
       StdOut.WriteLine("CheckType : " + WhatAmI);
       END CheckType;
       
     REDEFINE METHOD BuildType: Type;
       BEGIN
       RESULT := PredefItems.Boolean.MakeType(0);
       END BuildType;
       
   END PostExpression;
   
--------------------------------------------------------------------

   CLASS OldExpression;
     INHERITS PostExpression(OldExprCodeGenerator);
     VAR 
       TheExpr: TypedNonTerminal; 
                                  
       
     REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
       BEGIN
       RESULT := "OldExpression";
       END WhatAmI;

     METHOD GetExpr: TypedNonTerminal;
       BEGIN
       RESULT := TheExpr;
       END GetExpr;
       
     REDEFINE METHOD Parse(Lkh: LookAhead);
       BEGIN 
       Lkh.Accept(Lkh.Old);
       TheExpr := Lkh.AcceptFactor(Lkh.PostConditionContext);
       SetSon(TheExpr);
       END Parse;

     REDEFINE METHOD Functional: BOOLEAN;
       BEGIN
       RESULT := TheExpr.Functional;
       END Functional;
       
     METHOD AttachExpression;
       VAR
         p: NonTerminal;
         Done: BOOLEAN;
       BEGIN   
       p := Father;
       ASSERT p <> VOID;
       WHILE NOT Done DO
         WHAT p OF
           IN PostCondition:
             TAG.AttachOldExpression(THIS);
             Done := TRUE;
             END;
         ELSE
           p := p.Father;    
           ASSERT p <> VOID;
           END;    
         END;
       END AttachExpression;
       
     REDEFINE METHOD Tag;
       BEGIN 
       IF TheExpr <> VOID THEN
         TheExpr.UniqueTag;
         AttachExpression;
         END;
       END Tag;
       
     REDEFINE METHOD CheckType;
       BEGIN 
       ASSERT FALSE;
       END CheckType;
       
     REDEFINE METHOD GetType: Type;
       BEGIN
       RESULT := TheExpr.GetType;
       END GetType;  

     REDEFINE METHOD SubTree: ARRAY OF NonTerminal;
       BEGIN
       RESULT.CREATE(1);
       RESULT[0] := TheExpr;
       END SubTree;
       
   END OldExpression;
     
--------------------------------------------------------------------

   CLASS AssertionExpressionList;
     INHERITS NTList(TypedNonTerminal);
     
     METHOD WhatAmI: ARRAY OF CHAR;
       BEGIN
       RESULT := "AssertionExpressionList";
       END WhatAmI;
        
     REDEFINE METHOD UniqueCheckType;
       VAR
         Elem: TypedNonTerminal;
       BEGIN
       FOR Ind := 0 TO Size - 1 DO 
         Elem := Get(Ind); 
         ASSERT Elem <> VOID;
         IF (Elem.GetType <> VOID) THEN 
           IF NOT Elem.GetType.Compatible(PredefItems.Boolean.MakeType(0)) THEN
             Get(Ind).Error ("Expression must be BOOLEAN");
             END;
           END;  
         END;
       END UniqueCheckType;  
       
   END AssertionExpressionList;
   
----------------------------------------------------------

   CLASS PostExpressionList;
     INHERITS AssertionExpressionList;
     
     REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
       BEGIN
       RESULT := "PostExpressionList";
       END WhatAmI;
       
   END PostExpressionList;
   
END YaflPreconditions;




