IMPLEMENTATION MODULE CGPreconditions;

FROM Streams               IMPORT StdOut;
FROM YaflCfg               IMPORT YaflCfg;
FROM YaflAsGC              IMPORT AssertionGC;                     
FROM YaflGC                IMPORT YaflGC;
FROM CGMethods             IMPORT CMethImplCodeGenerator, CMethDefCodeGenerator;
FROM YaflPredefined        IMPORT PredefItems;
FROM List                  IMPORT List;
FROM YaflMetImplementation IMPORT MethodImplementation;

------------------------------
-- C Code Generators
------------------------------
FROM CGDeclarations IMPORT CSingleDataItemCodeGenerator;

------------------------------
-- Generic Code Generators
------------------------------
FROM YaflGCode IMPORT GC;
FROM YaflGType IMPORT TypedNTCodeGenerator;

------------------------------
-- Non Terminals
------------------------------
FROM YaflType          IMPORT TypedNonTerminal;
FROM YaflDesignator    IMPORT Desig;
FROM YaflPredefined    IMPORT PredefNoChangeMethod;
FROM YaflModules       IMPORT CompilationUnit;
FROM YaflClasses       IMPORT ClassDeclaration;
FROM YaflMethods       IMPORT MethodDeclaration, 
                              Formal,
                              FormalList;
FROM YaflPreconditions IMPORT Assertion,
                              PostExpression,
                              PreCondition,
                              PostCondition,
                              Invariant,
                              ClassInvariant,
                              LoopInvariant,
                              MethodAssertion,
                              OldExpression;
                              
----------------------------------------                              


   CLASS CPreCondCodeGenerator;
     INHERITS PreCondCodeGenerator(CGcContext);
   
     REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
       BEGIN
       RESULT := "CPreCondCodeGenerator";
       END WhatAmI;      

     METHOD Output: YaflGC;
       BEGIN
       RESULT := Ctx.Output;
       END Output;

     REDEFINE METHOD GenerateFunctionDeclaration(UseSemi: BOOLEAN);
       BEGIN
       Output.IfDefined(Output.FullTraceModeLabel);
       Output.IfDefined(Output.CheckPreCondLabel);
       GenerateContextFreeFuncDeclaration(UseSemi);
       GenerateContextDependentFuncDeclaration(UseSemi);
       Output.EndIf;
       Output.EndIf;
       END GenerateFunctionDeclaration;

     METHOD ExitMethod;
       BEGIN
       Output.ExitMethod;
       Output.IfDefined(Output.FullTraceModeLabel);
       Output.DbxPopCall;
       Output.LeftParent;
       Output.RightParent;
       Output.SemiColon;
       Output.WriteLn;
       Output.EndIf;
       END ExitMethod;

     METHOD GenerateContextFreeFuncDeclaration(UseSemi: BOOLEAN);
       VAR
         TheMethod: MethodDeclaration;
         TheClass:  ClassDeclaration;
         TheModule: CompilationUnit;
       BEGIN      
       TheMethod := Obj.Method;                       
       TheClass  := TheMethod.Class;
       TheModule := TheClass.Module;
       Output.WriteString (PredefItems.Integer.CName);
       Output.ContextFreePreCondFName(TheModule.Id.Data, 
                                      TheClass.Id.Data,
                                      TheMethod.Id.Data);
       Output.LeftParent;
       Output.ObjPtr;
       Output.This;
       Output.RightParent;
       IF UseSemi THEN
         Output.SemiColon;
         END;
       Output.WriteLn;
       END GenerateContextFreeFuncDeclaration;
       
     METHOD GenerateContextDependentFuncDeclaration(UseSemi: BOOLEAN);
       VAR
         TheMethod: MethodDeclaration;
         TheClass:  ClassDeclaration;
         TheModule: CompilationUnit;
       BEGIN      
       TheMethod := Obj.Method;
       TheClass  := TheMethod.Class;
       TheModule := TheClass.Module;
       Output.WriteString (PredefItems.Integer.CName);
       Output.ContextDepPreCondFName(TheModule.Id.Data, 
                                     TheClass.Id.Data,
                                     TheMethod.Id.Data);
       Output.LeftParent;
       Output.ObjPtr;
       Output.This;
       Output.RightParent;
       IF UseSemi THEN
         Output.SemiColon;
         END;
       Output.WriteLn;
       END GenerateContextDependentFuncDeclaration;
       
     METHOD GenerateLocalsDeclaration(Meth: MethodDeclaration);
       BEGIN
       Ctx.MethAssertGenerateFormalParamAccessDecl(THIS, Meth);
       END GenerateLocalsDeclaration;

     METHOD GenerateLocalsInit(Meth: MethodDeclaration);
       BEGIN
       Ctx.MethAssertGenerateFormalParamAccessInit(THIS, 
                                                   Meth,
                                                   FALSE);
       Output.WriteString(AssertionGC.LocalResult);
       Output.Becomes;
       Output.False;
       Output.SemiColon;
       Output.WriteLn;
       END GenerateLocalsInit;

     METHOD GenerateLocalResult;
       BEGIN
       Output.WriteString (PredefItems.Integer.CName);
       Output.WriteString(AssertionGC.LocalResult);
       Output.Becomes;
       Output.WriteInt(0,0);
       Output.SemiColon;
       Output.WriteLn;
       END GenerateLocalResult;
                          
     METHOD GenerateContextFreeFunc(Meth: MethodDeclaration);
       VAR
         NoExit: BOOLEAN;
       BEGIN
       Output.IfDefined(Output.FullTraceModeLabel);
       Output.IfDefined(Output.CheckPreCondLabel);
       GenerateContextFreeFuncDeclaration(FALSE);
       Output.LeftBrace;
       GenerateLocalResult;
       GenerateLocalsDeclaration(Meth);
       GenerateLocalsInit(Meth);
       WHAT Obj.Method.Gc OF 
         IN CMethImplCodeGenerator:
           TAG.DbxEnterMethod;
           END;
       ELSE
         WHAT Meth.Gc OF
           IN CMethImplCodeGenerator:
             TAG.DbxEnterMethod;
             END;
           IN CMethDefCodeGenerator:
             TAG.DbxEnterMethod;
             END;
         ELSE
           NoExit := TRUE;
           END;
         END;
       IF Obj.ImplementationConditions <> VOID THEN
         FOR Ind := 0 TO Obj.ImplementationConditions.Size -1 DO
           IF Obj.ReferToFormal(Obj.ImplementationConditions.Get(Ind)) THEN
               Ctx.AssertionGenerateTestExpression(THIS,
                                                   Obj.ImplementationConditions.Get(Ind),
                                                   Ind);
             END;
           END;
         END;
       IF Obj.DefinitionConditions <> VOID THEN
         FOR Ind := 0 TO Obj.DefinitionConditions.Size -1 DO
           IF Obj.ReferToFormal(Obj.DefinitionConditions.Get(Ind)) THEN
               Ctx.AssertionGenerateTestExpression(THIS,
                                                   Obj.DefinitionConditions.Get(Ind),
                                                   Ind + 16);
             END;
           END;  
         END;
       Output.WriteLn;
       IF NOT NoExit THEN
         ExitMethod;
         END;
       Output.Return;
       Output.WriteString(AssertionGC.LocalResult);
       Output.SemiColon;
       Output.WriteLn;
       Output.RightBrace;
       Output.WriteLn;
       Output.EndIf;
       Output.EndIf;
       END GenerateContextFreeFunc;
       
     METHOD GenerateContextDependentFunc(Meth: MethodDeclaration);
       VAR
         NoExit: BOOLEAN;
       BEGIN
       Output.IfDefined(Output.FullTraceModeLabel);
       Output.IfDefined(Output.CheckPreCondLabel);
       GenerateContextDependentFuncDeclaration(FALSE);
       Output.LeftBrace;
       GenerateLocalResult;
       GenerateLocalsDeclaration(Meth);
       GenerateLocalsInit(Meth);
       WHAT Obj.Method.Gc OF 
         IN CMethImplCodeGenerator:
           TAG.DbxEnterMethod;
           END;
       ELSE
         WHAT Meth.Gc OF
           IN CMethImplCodeGenerator:
             TAG.DbxEnterMethod;
             END;
           IN CMethDefCodeGenerator:
             TAG.DbxEnterMethod;
             END;
         ELSE
           NoExit := TRUE;
           END;
         END;
       IF Obj.ImplementationConditions <> VOID THEN
         FOR Ind := 0 TO Obj.ImplementationConditions.Size -1 DO
           IF NOT Obj.ReferToFormal(Obj.ImplementationConditions.Get(Ind)) THEN
               Ctx.AssertionGenerateTestExpression(THIS,
                                                   Obj.ImplementationConditions.Get(Ind),
                                                   Ind);
             END;
           END;
         END;
       IF Obj.DefinitionConditions <> VOID THEN
         FOR Ind := 0 TO Obj.DefinitionConditions.Size -1 DO
           IF NOT Obj.ReferToFormal(Obj.DefinitionConditions.Get(Ind)) THEN
               Ctx.AssertionGenerateTestExpression(THIS,
                                                   Obj.DefinitionConditions.Get(Ind),
                                                   Ind + 16);
             END;
           END;  
         END;
       Output.WriteLn;
       IF NOT NoExit THEN
         ExitMethod;
         END;
       Output.WriteLn;
       Output.Return;
       Output.WriteString(AssertionGC.LocalResult);
       Output.SemiColon;
       Output.WriteLn;
       Output.RightBrace;
       Output.WriteLn;
       Output.EndIf;
       Output.EndIf;
       END GenerateContextDependentFunc;

   END CPreCondCodeGenerator;

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

   CLASS CPostCondCodeGenerator;
     INHERITS PostCondCodeGenerator(CGcContext);
   
     REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
       BEGIN
       RESULT := "CPostCondCodeGenerator";
       END WhatAmI;      

     METHOD Output: YaflGC;
       BEGIN
       RESULT := Ctx.Output;
       END Output;

     METHOD ExitMethod;
       BEGIN
       Output.ExitMethod;
       Output.IfDefined(Output.FullTraceModeLabel);
       Output.DbxPopCall;
       Output.LeftParent;
       Output.RightParent;
       Output.SemiColon;
       Output.WriteLn;
       Output.EndIf;
       END ExitMethod;

     METHOD GenerateOldExprInitDeclaration(UseSemi: BOOLEAN);
       VAR
         TheMethod: MethodDeclaration;
         TheClass:  ClassDeclaration;
         TheModule: CompilationUnit;
       BEGIN      
       TheMethod := Obj.Method;
       TheClass  := TheMethod.Class;
       TheModule := TheClass.Module;
       Output.WriteString (PredefItems.Integer.CName);
       Output.ComputeOldExprFName(TheModule.Id.Data, 
                                  TheClass.Id.Data,
                                  TheMethod.Id.Data);
       Output.LeftParent;
       Output.ObjPtr;
       Output.This;
       Output.RightParent;
       IF UseSemi THEN
         Output.SemiColon;
         END;
       Output.WriteLn;
       END GenerateOldExprInitDeclaration;
       
     METHOD GenerateLocalResult;
       BEGIN
       Output.WriteString (PredefItems.Integer.CName);
       Output.WriteString(AssertionGC.LocalResult);
       Output.Becomes;
       Output.False;
       Output.SemiColon;
       Output.WriteLn;
       END GenerateLocalResult;

     METHOD GeneratePostEvalDeclaration(UseSemi: BOOLEAN);
       VAR
         TheMethod: MethodDeclaration;
         TheClass:  ClassDeclaration;
         TheModule: CompilationUnit;
       BEGIN      
       TheMethod := Obj.Method;
       TheClass  := TheMethod.Class;
       TheModule := TheClass.Module;
       Output.WriteString (PredefItems.Integer.CName);
       Output.PostConditionFName(TheModule.Id.Data, 
                                 TheClass.Id.Data,
                                 TheMethod.Id.Data);
       Output.LeftParent;
       Output.ObjPtr;
       Output.This;
       Output.RightParent;
       IF UseSemi THEN
         Output.SemiColon;
         END;
       Output.WriteLn;
       END GeneratePostEvalDeclaration;
       
     REDEFINE METHOD GenerateFunctionDeclaration(UseSemi: BOOLEAN);
       BEGIN
       GenerateOldExprInitDeclaration(UseSemi);
       GeneratePostEvalDeclaration(UseSemi);
       END GenerateFunctionDeclaration;
       
     METHOD GenerateLocalsDeclaration(Meth: MethodDeclaration);
       BEGIN
       Ctx.MethAssertGenerateFormalParamAccessDecl(THIS, Meth);
       IF Obj.Method.Return <> VOID THEN
         Ctx.MethAssertGenerateResultAccessDecl(THIS, Meth);
         END;
       Ctx.MethAssertGenerateOldExprAccessDecl(THIS);
       END GenerateLocalsDeclaration;

     METHOD GenerateLocalsInit(Meth: MethodDeclaration);
       BEGIN
       IF Obj.Method.Return <> VOID THEN
         Ctx.MethAssertGenerateFormalParamAccessInit(THIS, 
                                                     Meth, 
                                                     TRUE);
         Ctx.MethAssertGenerateResultAccessInit(THIS, Meth);
       ELSE
         Ctx.MethAssertGenerateFormalParamAccessInit(THIS, Meth, FALSE);
         END;
       END GenerateLocalsInit;

     METHOD GenerateOldsInit;
       BEGIN
       Ctx.MethAssertGenerateOldExprAccess(THIS);
       END GenerateOldsInit;
                          
     METHOD GenerateOldExprInitFunc(Meth: MethodDeclaration);
       VAR
         TheOlds: List(TypedNonTerminal);
       BEGIN
       Output.IfDefined(Output.FullTraceModeLabel);
       Output.IfDefined(Output.CheckPostCondLabel);
       GenerateOldExprInitDeclaration(FALSE);
       Output.LeftBrace;
       GenerateLocalsDeclaration(Meth);
       Ctx.MethAssertGenerateFormalParamAccessInit(THIS, Meth, FALSE);
       TheOlds := Obj.OldExpressions;
       FOR Ind := TheOlds.Size-1 TO 0 BY -1 DO
         AssertionGC.MethAssertPushOldExpr(Output, TheOlds.Get(Ind));
         END;
       Output.RightBrace;
       Output.EndIf;
       Output.EndIf;
       END GenerateOldExprInitFunc;

     METHOD GenerateFunction(Meth: MethodDeclaration);
       VAR
         NoExit: BOOLEAN;
       BEGIN
       Output.IfDefined(Output.FullTraceModeLabel);
       Output.IfDefined(Output.CheckPostCondLabel);
       GeneratePostEvalDeclaration(FALSE);
       Output.LeftBrace;
       GenerateLocalResult;
       GenerateLocalsDeclaration(Meth);
       GenerateLocalsInit(Meth);
       GenerateOldsInit;
       WHAT Obj.Method.Gc OF 
         IN CMethImplCodeGenerator:
           TAG.DbxEnterMethod;
           END;
       ELSE
         WHAT Meth.Gc OF
           IN CMethImplCodeGenerator:
             TAG.DbxEnterMethod;
             END;
           IN CMethDefCodeGenerator:
             TAG.DbxEnterMethod;
             END;
         ELSE
           NoExit := TRUE;
	       -- nothing at this time,
	       -- must be reviewed.
           END;
         END;
       IF Obj.ImplementationConditions <> VOID THEN
         FOR Ind := 0 TO Obj.ImplementationConditions.Size -1 DO
           Ctx.AssertionGenerateTestExpression(THIS,
                                               Obj.ImplementationConditions.Get(Ind),
                                               Ind);
           END;
         END;
       IF Obj.DefinitionConditions <> VOID THEN
         FOR Ind := 0 TO Obj.DefinitionConditions.Size -1 DO
           Ctx.AssertionGenerateTestExpression(THIS,
                                               Obj.DefinitionConditions.Get(Ind),
                                               Ind);
           END;
         END;  
       Output.WriteLn;
       IF NOT NoExit THEN 
         ExitMethod;
         END;
       Output.WriteLn;
       Output.Return;
       Output.WriteString(AssertionGC.LocalResult);
       Output.SemiColon;
       Output.WriteLn;
       Output.RightBrace;
       Output.WriteLn;
       Output.EndIf;
       Output.EndIf;
       END GenerateFunction;
 
   END CPostCondCodeGenerator;

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

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

   END CClassInvCodeGenerator;

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

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

   END CLoopInvCodeGenerator;

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

   CLASS COldExprCodeGenerator;
     INHERITS OldExprCodeGenerator(CGcContext);

     VAR
       TheUniqueNr: INTEGER;

    REDEFINE METHOD WhatAmI: ARRAY OF CHAR;
      BEGIN
      RESULT := "COldExprCodeGenerator";
      END WhatAmI;      

     METHOD Output: YaflGC;
       BEGIN
       RESULT := Ctx.Output;
       END Output;

     METHOD GenerateExprName;
       BEGIN
       IF TheUniqueNr = 0 THEN
         TheUniqueNr := YaflCfg.UniqueNumber;
         END;
       Output.UniqueItem(TheUniqueNr);
       END GenerateExprName;

     REDEFINE METHOD GenerateEvaluationCode;
       BEGIN
       GenerateExprName;
       --StdOut.WriteLine("Generate Evaluation Code : " + WhatAmI);
       END GenerateEvaluationCode;


     REDEFINE METHOD GenerateCode;
       BEGIN   
       ASSERT Obj.GetExpr <> VOID;
       Obj.GetExpr.Gc.GenerateEvaluationCode;
       END GenerateCode;

   END COldExprCodeGenerator;
     
END CGPreconditions;


