--  $Id: java_program_interpretation.ty,v 1.6 10/.0/.2 .1:.1:.4 mrusso Exp $
-- /***************************************************************************/
-- /*              Copyright (C) 1997-1999 INRIA Sophia-Antipolis             */
-- /*                   I. Attali, D. Caromel and M. Russo                    */
-- /*                              Projet OASIS                               */
-- /*                     2004, route des Lucioles, BP 93                     */
-- /*                     F-06902 Sophia Antipolis cedex                      */
-- /*                           (+33) 4 92 38 76 31                           */
-- /*                           All rights reserved                           */
-- /***************************************************************************/
--
-- /***************************************************************************/
-- /* This file contains the set that manages the interpreter                 */
-- /***************************************************************************/
program java_program_interpretation is
use java;
use PSP;

import
   interpretProgram (
      Objects, ClassVariablesL -> Objects, ClassVariablesL ) ,
   getTheNewExecutingThread (
      ClassVariablesL |- Objects -> Objects, ObjectId ) ,
   executeThread (
      Objects, ClassVariablesL, ObjectId -> Objects, ClassVariablesL )
   from java_concurrency;

import
   ENVgetUserAction ( ) ,
   ENVfreeEnvironment ( )
   from java_environment;

import
   getMainThread ( |- TypeDeclarations -> Object
      ) , areAllThreadsDead ( Objects -> Bool ) ,
   loadClasses ( TypeDeclarations -> ClassVariablesL )
   from java_object_list;

import
   setCompilationUnit ( _ ) ,
   setNewCompilationUnit ( _ ) ,
   setFirstExecutingThread ( _ ) , initialize ( )
   , deadlock ( ) from jfunctions;

export
   interpretProgram(
      |- CompUnit -> ObjL, ClVarL ) as interpret(CompUnit)
   = (ObjL, ClVarL) ;

   set interpretProgram is
   --SC: Loads the classes (retrieves the class variables), creates the "main"
   --SC: thread (the thread which executes the "main" method) and launches the 
   --SC: program interpretation.
   --
   --JC: |- Compilation Unit (i.e. the program abstract syntax tree)
   --JC: -> Final list that contains all the objects created during this
   --JC: interpretation, Final class variable list.  
   judgement |- CompilationUnit -> Objects, ClassVariablesL;
   --iJC: Objects, Class variables 
   --iJC: -> updated object list, updated class variable list
   judgement (Objects, ClassVariablesL -> Objects, ClassVariablesL);

   initialisationOfTheInterpreter:
      loadClasses( TDecL -> ClVarL1 )  &
      getMainThread( |- TDecL -> Thr )
      &  setFirstExecutingThread( objectId(true(), objectNumber 0) )
      &  (objects[Thr], ClVarL1 -> ObjL, ClVarL1_1)
      --------------------------------
      |- compilationUnit(PackName, ImportL, TDecL) -> ObjL, ClVarL1_1  ; 
               provided
                  ENVgetUserAction( )  &
                  initialize( )  &
                  setCompilationUnit( compilationUnit(PackName, ImportL, TDecL) )
                  &
                  setNewCompilationUnit( compilationUnit(PackName, ImportL, TDecL) );

   RecursiveRule_InterpretOneStep:
      getTheNewExecutingThread(
         ClVarL1 |- ObjL1 -> ObjL1_1, OThId )  &
      executeThread( ObjL1_1, ClVarL1, OThId -> ObjL1_2, ClVarL1_1 )
      &  (ObjL1_2, ClVarL1_1 -> ObjL1_3, ClVarL1_2)
      --------------------------------
      (ObjL1, ClVarL1 -> ObjL1_3, ClVarL1_2)  ; 
               provided ENVgetUserAction( );

   DeadLock:
      --RC : No thread can execute itself but there is at least one alive thread.
      --RC : Deadlock.
      areAllThreadsDead( ObjL -> false() )
      --------------------------------
      (ObjL, ClVarL -> ObjL, ClVarL)  ; 
               do
                  deadlock( )  &
                  ENVfreeEnvironment( );

   InterpretationEnd:
      --RC : All threads are dead => end of the program interpretation.
      areAllThreadsDead( ObjL -> true() )
      --------------------------------
      (ObjL, ClVarL -> ObjL, ClVarL)  ; 
               do ENVfreeEnvironment( );
   end interpretProgram; 
end java_program_interpretation