From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 3 Jul 2009 18:11:04 +0000 (+0000)
Subject: more static analysis on the Automath text
X-Git-Tag: make_still_working~3751
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ca9fe133125cb84c5223029995cb72e973a2d695

more static analysis on the Automath text
---

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index b102e20ae..eb7f894e2 100644
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -1,13 +1,23 @@
+lib/nUri.cmi: 
 lib/nUri.cmo: lib/nUri.cmi 
 lib/nUri.cmx: lib/nUri.cmi 
+lib/cps.cmo: 
+lib/cps.cmx: 
+lib/share.cmo: 
+lib/share.cmx: 
+lib/log.cmi: 
 lib/log.cmo: lib/cps.cmx lib/log.cmi 
 lib/log.cmx: lib/cps.cmx lib/log.cmi 
 lib/time.cmo: lib/log.cmi 
 lib/time.cmx: lib/log.cmx 
+lib/hierarchy.cmi: 
 lib/hierarchy.cmo: lib/cps.cmx lib/hierarchy.cmi 
 lib/hierarchy.cmx: lib/cps.cmx lib/hierarchy.cmi 
+lib/output.cmi: 
 lib/output.cmo: lib/log.cmi lib/output.cmi 
 lib/output.cmx: lib/log.cmx lib/output.cmi 
+automath/aut.cmo: 
+automath/aut.cmx: 
 automath/autProcess.cmi: automath/aut.cmx 
 automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi 
 automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi 
diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml
index 6ca42e6c6..2f1a4d91c 100644
--- a/helm/software/lambda-delta/automath/autOutput.ml
+++ b/helm/software/lambda-delta/automath/autOutput.ml
@@ -88,11 +88,12 @@ let print_counters f c =
    f ()
 
 let print_process_counters f c =
-   let f iao iar iac =
+   let f iao iar iac iag =
       L.warn (P.sprintf "  Automath process summary");
       L.warn (P.sprintf "    Implicit after opening:   %7u" iao);
       L.warn (P.sprintf "    Implicit after reopening: %7u" iar);
       L.warn (P.sprintf "    Implicit after closing:   %7u" iac);
+      L.warn (P.sprintf "    Implicit after global:    %7u" iag);
       f ()
    in
    R.get_counters f c
diff --git a/helm/software/lambda-delta/automath/autProcess.ml b/helm/software/lambda-delta/automath/autProcess.ml
index c6ef561f0..87fe41865 100644
--- 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
diff --git a/helm/software/lambda-delta/automath/autProcess.mli b/helm/software/lambda-delta/automath/autProcess.mli
index 61cd61d05..373935e9e 100644
--- a/helm/software/lambda-delta/automath/autProcess.mli
+++ b/helm/software/lambda-delta/automath/autProcess.mli
@@ -15,4 +15,4 @@ val initial_status: status
 
 val process_item: (status -> Aut.item -> 'a) -> status -> Aut.item -> 'a
 
-val get_counters: (int -> int -> int -> 'a) -> status -> 'a
+val get_counters: (int -> int -> int -> int -> 'a) -> status -> 'a