-- (C) Copyright International Business Machines Corporation 23 January 
-- 1990.  All Rights Reserved. 
--  
-- See the file USERAGREEMENT distributed with this software for full 
-- terms and conditions of use. 
-- File: defs/checkdefs_internal.d
-- Author: Jim Russell
-- SCCS Info: @(#)checkdefs_internal.d	1.4 1/9/92

-- definitions used internally by the checkdefs process and it's
-- subprocesses.

checkdefs_internal: using (checkdefs, errors, stdenv) definitions
    
    -- just like definitions_modules, except checkeddefinitions isn't
    -- in typestate
    module_table: table of definitions_module {full} keys (id);
    
    checkConstraints: callmessage (
        std: stdenv,
        id: moduleid,               -- the module to be checked
        defs: module_table,         -- the place to find modules
        typenames: checkdefs!typename_rec, -- typenames from predefined
        -- carried in from dcom in case we're checking predefined
        checkFormal_typestate: checkFormal_TypestateFn,  
                      -- procedure to check formal typestates
        checkComp_list: checkComponent_ListFn, 
                      -- procedure to check component lists
        fixfull: fixfullOutport,  -- routine to expand full(p)
        errortemplate: error,       -- template for new errors
        errors: errors
      ) 
    constant (std, id, defs, typenames, checkFormal_typestate, 
        checkComp_list, errorTemplate)
    exit { full };
    
    checkConstraintsQ: inport of checkConstraints {full};
    checkConstraintsFn: outport of checkConstraintsQ;
    
    -- procedure to compute an adds/drops given a pre-condition/post-condition pair
    FixFullCall: CALLMESSAGE (
        Definitions: module_table, -- modules for resolution
        Formal: Formal_Typestate, -- a formal typestate which is to be expanded(fixfull) or contracted(shorten)
        RootType: TypeName, -- the typename of implied root of formal
        errorTemplate: error,  -- partially filled in error
        errors: errors
      )
    CONSTANT(Definitions, RootType, errorTemplate) 
    EXIT{full}
    MINIMUM{full};
        
    FixFullInport: INPORT OF FixFullCall {Full};
    FixFullOutport: OUTPORT OF FixFullInport;

    CheckFormal_Typestate: callmessage (
        ts: formal_typestate,       -- the typestate to be checked
        basetype: typename,         -- the type of base variable 
        defs: module_table,         -- all the modules we may need
        typenames: checkdefs!typename_rec, -- typenames from predefined
        -- carried in from dcom in case we're checking predefined
        errortemplate: error,       -- template for new errors
        errors: errors,             -- where to put error messages
        checkCL: checkComponent_ListFn,  -- routine to check component lists
        fixfull: fixfullOutport  -- routine to expand full(p)
      ) 
    constant (ts, basetype, defs, typenames, errortemplate, checkCL)
    exit {full};
    
    CheckFormal_TypestateQ: inport of CheckFormal_Typestate {full};
    CheckFormal_TypestateFn: outport of CheckFormal_TypestateQ;
    
    
    CheckComponent_List: callmessage (
        cl: component_list,         -- the component_list to check
        type: typename,             -- what it's a component of (in)
                                    -- typename for last component (out)
        defs: module_table,         -- module library
        errortemplate: error,       -- template for new errors
        errors: errors              -- where to put error messages
      ) constant (cl, defs, errortemplate)
    exit{full}
    exception Error {full};
        
    CheckComponent_ListQ: inport of CheckComponent_List {full};
    CheckComponent_ListFn: outport of CheckComponent_ListQ;
    
    
    checkCircular_typestate: callmessage (
        ts: predefined!typestate,       -- the current typestate
        id: predefined!moduleid,    -- the id of definitions module we're in
        def: predefined!definitions_module,  -- actual module we're in
        seen: seenlist               -- list of constraints on this path
      ) constant (ts, id, def, seen)
    exit {full}
    exception Error {full};

    checkCircular_typestateQ: inport of checkCircular_typestate {full};
    checkCircular_typestateFn: outport of checkCircular_typestateQ;

    seenlist: table of predefined!attributeid {init(*)} keys (*);
    
    formtsentry: record (
        id: rootid,
        basetype: typename,
        ts: formal_typestate
      );
    
    formtstable: table of formtsentry {full} keys (id);
    
    
    CompareComponent_Lists: callmessage (
        L: component_list,
        R: component_list
      ) constant (L, R)
    exit {full}
    minimum {full}
    exception LprefixR {full}
    exception RprefixL {full}
    exception LequalsR {full};
    
    compareComponent_listsQ: inport of compareComponent_lists {full};
    compareComponent_listsFn: outport of compareComponent_listsQ;
    
    Implies: callmessage (
        L: predefined!formal_objects,
        R: predefined!formal_objects,
        compare: compareComponent_ListsFn,
        result: boolean
      ) constant (L, R, compare)
    exit {full};
    
    ImpliesQ: inport of implies {init(L), init(R), init(compare)};
    ImpliesFn: outport of impliesQ;
    

  end definitions
