(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.              
     \ /   This software is distributed as is, NO WARRANTY.              
      V_______________________________________________________________ *)

module A = Aut

type status = {
   opening  : bool; (* just opened section *)
   reopening: bool; (* just reopened section *)
   closing  : bool; (* just closed section *)
   explicit : bool; (* just found explicit context *)
   block    : bool; (* just found block opener *)
   iao      : int;  (* implicit context after opening section *)
   iar      : int;  (* implicit context after reopening section *)
   iac      : int;  (* implicit context after closing section *)
   iag      : int   (* implicit context after global statement *)
}

(* internal functions *******************************************************)

let orc_reset f st =
   f {st with opening = false; reopening = false; closing = false}

let orc_count f st =
   let st = if st.opening then {st with iao = succ st.iao} else st in
   let st = if st.reopening then {st with iar = succ st.iar} else st in
   let st = if st.closing then {st with iac = succ st.iac} else st in
   f st

let exp_count f st =
   let st = 
      if st.explicit || st.block then st else {st with iag = succ st.iag} 
   in
   f st

let proc_section f st = function
   | Some (true, _)  -> f {st with opening = true} 
   | Some (false, _) -> f {st with reopening = true} 
   | None            -> f {st with closing = true}

let proc_context f st =
   orc_reset f {st with explicit = true}

let proc_block f st =
   orc_count (orc_reset f) {st with explicit = false; block = true}

let proc_global f st =
   let f st = 
      orc_count (orc_reset f) {st with explicit = false; block = false}
   in
   exp_count f st

let proc_entity f st entity = match entity with
   | A.Section section -> proc_section f st section entity
   | A.Context _       -> proc_context f st entity  
   | A.Block _         -> proc_block f st entity
   | A.Decl _          -> proc_global f st entity
   | A.Def _           -> proc_global f st entity
   
(* interface functions ******************************************************)

let initial_status = {
   opening = false; reopening = false; closing = false; 
   explicit = false; block = false;
   iao = 0; iar = 0; iac = 0; iag = 0
}

let process_entity = proc_entity

let get_counters f st = f st.iao st.iar st.iac st.iag