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

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index a05bbd26d8df836d422b6fee82dd838b44840281..50e3024605a564caad2e19be389c4984576ff9e3 100644 (file)
--- 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 7d1e20a4d65cb67ba656b07c83e133204dd7c53d..f4f25c402f813d6e5c545cdcfd13ffcacd6edfa0 100644 (file)
--- 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 3b6afc4c31ac0d54f18d58613c583311801e199d..9bb2e576c41d71f0c4e3fae06b11f64a8108af09 100644 (file)
--- 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 cc911df84ac902fe9ae43b2284d1eca430a499ad..25efa4cab4108969e83b5025dc7d3fbc322c8514 100644 (file)
--- 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 e7ee2ed8dd72adcef986ecf401336a57cf981907..6540441014d0cdce236e806f58b0625468d2f607 100644 (file)
--- 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