From ca9fe133125cb84c5223029995cb72e973a2d695 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 3 Jul 2009 18:11:04 +0000 Subject: [PATCH] more static analysis on the Automath text --- helm/software/lambda-delta/.depend.opt | 10 ++++ .../lambda-delta/automath/autOutput.ml | 3 +- .../lambda-delta/automath/autProcess.ml | 50 ++++++++++++++----- .../lambda-delta/automath/autProcess.mli | 2 +- 4 files changed, 50 insertions(+), 15 deletions(-) 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 -- 2.39.2