more static analysis on the Automath text

[helm.git] / helm / software / lambda-delta / automath / autProcess.ml

diff --git a/helm/software/lambda-delta/automath/autProcess.ml b/helm/software/lambda-delta/automath/autProcess.ml
index c6ef561f0b26c49bf189ff1b984f841b11ced4fb..87fe418650e6779603def9db0e1dd72c32d94ca4 100644 (file)
--- a/helm/software/lambda-delta/automath/autProcess.ml
+++ b/helm/software/lambda-delta/automath/autProcess.ml
@@ -15,39 +15,63 @@ 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 *)
+   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} 
+   | None            -> f {st with closing = true}
 
 let proc_context f st =
-   f {st with opening = false; reopening = false; closing = false} 
+   orc_reset f {st with explicit = true}
 
-let proc_proper 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
-   proc_context f st
+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_item f st item = match item with
    | A.Section section -> proc_section f st section item
    | A.Context _       -> proc_context f st item  
-   | _                 -> proc_proper f st item
-
+   | A.Block _         -> proc_block f st item
+   | A.Decl _          -> proc_global f st item
+   | A.Def _           -> proc_global f st item
+   
 (* interface functions ******************************************************)
 
 let initial_status = {
-   opening = false; reopening = false; closing = false;
-   iao = 0; iar = 0; iac = 0
+   opening = false; reopening = false; closing = false; 
+   explicit = false; block = false;
+   iao = 0; iar = 0; iac = 0; iag = 0
 }
 
 let process_item = proc_item
 
-let get_counters f st = f st.iao st.iar st.iac
+let get_counters f st = f st.iao st.iar st.iac st.iag