From 89519c7b52e06304a94019dd528925300380cdc0 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 26 Feb 2009 21:15:13 +0000 Subject: [PATCH] cicInspect: now we can choose not to count the Cic.Implicit constructors proceduralTypes, proceduralOptimizer: we do not count the Cic.Implict nodes proceduralTeX: bug fix --- .../acic_procedural/proceduralOptimizer.ml | 5 +- .../acic_procedural/proceduralTeX.ml | 8 ++- .../acic_procedural/proceduralTypes.ml | 8 +-- helm/software/components/cic/cicInspect.ml | 63 ++++++++++--------- helm/software/components/cic/cicInspect.mli | 3 +- 5 files changed, 46 insertions(+), 41 deletions(-) diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index a05bbd26d..50e302460 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -253,6 +253,7 @@ let wrap g st c bo = let optimize_obj = function | C.Constant (name, Some bo, ty, pars, attrs) -> + let count_nodes = I.count_nodes ~implicit:false 0 in let st, c = {info = ""; dummy = ()}, [] in let bo, ty = H.cic_bc c bo, H.cic_bc c ty in let g st bo = @@ -262,14 +263,14 @@ let optimize_obj = function Ut.pp_term prerr_string [] c bo; prerr_newline () end; (* let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in *) - let nodes = Printf.sprintf "Optimized nodes: %u" (I.count_nodes 0 bo) in + let nodes = Printf.sprintf "Optimized nodes: %u" (count_nodes bo) in let st = info st nodes in L.time_stamp ("PO: DONE " ^ name); C.Constant (name, Some bo, ty, pars, attrs), st.info in L.time_stamp ("PO: OPTIMIZING " ^ name); if !debug then Printf.eprintf "BEGIN: %s\n" name; - let nodes = Printf.sprintf "Initial nodes: %u" (I.count_nodes 0 bo) in + let nodes = Printf.sprintf "Initial nodes: %u" (count_nodes bo) in wrap g (info st nodes) c bo | obj -> obj, "" diff --git a/helm/software/components/acic_procedural/proceduralTeX.ml b/helm/software/components/acic_procedural/proceduralTeX.ml index 7d1e20a4d..f4f25c402 100644 --- a/helm/software/components/acic_procedural/proceduralTeX.ml +++ b/helm/software/components/acic_procedural/proceduralTeX.ml @@ -234,9 +234,11 @@ let rec xl frm = function | T.Elim _ :: _ -> assert false | T.Cut _ :: _ -> assert false -and xls frm ls = - let map l = F.fprintf frm "{%a}" xl l in - List.iter map (List.rev ls) +and xls frm = function + | [] -> F.fprintf frm "{}" + | ls -> + let map l = F.fprintf frm "{%a}" xl l in + List.iter map (List.rev ls) in F.fprintf frm "%a@\n" xl l diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index 3b6afc4c3..9bb2e576c 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -280,6 +280,8 @@ let rec count_step a = function and count_steps a = List.fold_left count_step a +let count = I.count_nodes ~implicit:false + let rec count_node a = function | Note _ | Inductive _ @@ -291,13 +293,11 @@ let rec count_node a = function | ClearBody _ -> a | Cut (_, t, _) | LetIn (_, t, _) - | Apply (t, _) -> I.count_nodes a (H.cic t) + | Apply (t, _) -> count a (H.cic t) | Rewrite (_, t, _, p, _) | Elim (t, _, p, _) | Cases (t, p, _) - | Change (t, _, _, p, _) -> - let a = I.count_nodes a (H.cic t) in - I.count_nodes a (H.cic p) + | Change (t, _, _, p, _) -> let a = count a (H.cic t) in count a (H.cic p) | Branch (ss, _) -> List.fold_left count_nodes a ss and count_nodes a = List.fold_left count_node a diff --git a/helm/software/components/cic/cicInspect.ml b/helm/software/components/cic/cicInspect.ml index cc911df84..25efa4cab 100644 --- a/helm/software/components/cic/cicInspect.ml +++ b/helm/software/components/cic/cicInspect.ml @@ -111,34 +111,35 @@ let get_mutinds_of_uri u t = let g a = a in aux g t S.empty -let rec aux n = function - | C.Sort _ - | C.Implicit _ - | C.Rel _ -> succ n - | C.Appl ts -> List.fold_left aux (succ n) ts - | C.Const (_, ss) - | C.MutConstruct (_, _, _, ss) - | C.MutInd (_, _, ss) - | C.Var (_, ss) -> - let map n (_, t) = aux n t in - List.fold_left map (succ n) ss - | C.Meta (_, ss) -> - let map n = function - | None -> n - | Some t -> aux n t - in - List.fold_left map (succ n) ss - | C.Cast (t1, t2) - | C.Lambda (_, t1, t2) - | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1 - | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (succ n) t2) ty) t1 - | C.MutCase (_, _, t1, t2, ss) -> - aux (aux (List.fold_left aux (succ n) ss) t2) t1 - | C.Fix (_, ss) -> - let map n (_, _, t1, t2) = aux (aux n t2) t1 in - List.fold_left map (succ n) ss - | C.CoFix (_, ss) -> - let map n (_, t1, t2) = aux (aux n t2) t1 in - List.fold_left map (succ n) ss - -let count_nodes = aux +let count_nodes ~implicit n t = + let rec aux n = function + | C.Implicit _ -> if implicit then succ n else n + | C.Sort _ + | C.Rel _ -> succ n + | C.Appl ts -> List.fold_left aux (succ n) ts + | C.Const (_, ss) + | C.MutConstruct (_, _, _, ss) + | C.MutInd (_, _, ss) + | C.Var (_, ss) -> + let map n (_, t) = aux n t in + List.fold_left map (succ n) ss + | C.Meta (_, ss) -> + let map n = function + | None -> n + | Some t -> aux n t + in + List.fold_left map (succ n) ss + | C.Cast (t1, t2) + | C.Lambda (_, t1, t2) + | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1 + | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (succ n) t2) ty) t1 + | C.MutCase (_, _, t1, t2, ss) -> + aux (aux (List.fold_left aux (succ n) ss) t2) t1 + | C.Fix (_, ss) -> + let map n (_, _, t1, t2) = aux (aux n t2) t1 in + List.fold_left map (succ n) ss + | C.CoFix (_, ss) -> + let map n (_, t1, t2) = aux (aux n t2) t1 in + List.fold_left map (succ n) ss +in +aux n t diff --git a/helm/software/components/cic/cicInspect.mli b/helm/software/components/cic/cicInspect.mli index e7ee2ed8d..654044101 100644 --- a/helm/software/components/cic/cicInspect.mli +++ b/helm/software/components/cic/cicInspect.mli @@ -32,4 +32,5 @@ val get_rels_from_premise: int -> Cic.term -> S.t val get_mutinds_of_uri: UriManager.uri -> Cic.term -> S.t (* count_nodes n t returns n + the number of nodes in t *) -val count_nodes: int -> Cic.term -> int +(* Cic.Implict nodes are counted if ~implicit:true *) +val count_nodes: implicit:bool -> int -> Cic.term -> int -- 2.39.2