IMPLEMENTATION MODULE YaflGPreconditions;

FROM YaflGCode         IMPORT GC;
FROM YaflType          IMPORT TypedNonTerminal;
FROM Streams           IMPORT StdOut;
FROM YaflCfg           IMPORT YaflCfg;
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,
                              PreCondition,
                              PostCondition,
                              Invariant,
                              ClassInvariant,
                              LoopInvariant,
                              MethodAssertion,
                              OldExpression;
FROM YaflAsGC          IMPORT AssertionGC;                     
                              
                              
  CLASS AssertionCodeGenerator(ObjType IN Assertion, CtxType IN GcContext);
    INHERITS GC(ObjType, CtxType);
    
  END AssertionCodeGenerator;

----------------------------------------------------------
   CLASS MethAssertCodeGenerator(ObjType IN MethodAssertion, CtxType IN GcContext);
     INHERITS AssertionCodeGenerator(ObjType, CtxType);
     
     METHOD MetImplementation: MethodImplementation;
       BEGIN
       WHAT Obj.Method OF
         IN MethodImplementation:
           RESULT := TAG;
           END;
         END;
       END MetImplementation;

   END MethAssertCodeGenerator;
----------------------------------------------------------

   CLASS PreCondCodeGenerator(CtxType IN GcContext);
     INHERITS MethAssertCodeGenerator(PreCondition, CtxType);
   
   END PreCondCodeGenerator;

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

   CLASS PostCondCodeGenerator(CtxType IN GcContext);
     INHERITS MethAssertCodeGenerator(PostCondition, CtxType);
   
   END PostCondCodeGenerator;

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

   CLASS InvCodeGenerator(ObjType IN Invariant, CtxType IN GcContext);
     INHERITS AssertionCodeGenerator(ObjType, CtxType);
     
   END InvCodeGenerator;

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

   CLASS ClassInvCodeGenerator(CtxType IN GcContext);
     INHERITS InvCodeGenerator(ClassInvariant, CtxType);
   
   END ClassInvCodeGenerator;

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

   CLASS LoopInvCodeGenerator(CtxType IN GcContext);
     INHERITS InvCodeGenerator(LoopInvariant, CtxType);
   
   END LoopInvCodeGenerator;

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

   CLASS PostExprCodeGenerator(ObjType IN PostExpression, CtxType IN GcContext);
     INHERITS TypedNTCodeGenerator(ObjType, CtxType);
     
   END PostExprCodeGenerator;
   
----------------------------------------------------------

   CLASS OldExprCodeGenerator(CtxType IN GcContext);
     INHERITS PostExprCodeGenerator(OldExpression, CtxType);
     
   END OldExprCodeGenerator;
     
END YaflGPreconditions;
