* added group box (?)

[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.ml

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index 1f9d9f5ccee6ad17203c5f0d0fb761ccc31d3c88..d3a87dfc1845402959012693d859361303671172 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -152,6 +152,7 @@ let visit_layout k = function
   | Root (arg, index) -> Root (k arg, k index)
   | Break -> Break
   | Box (kind, terms) -> Box (kind, List.map k terms)
+  | Group terms -> Group (List.map k terms)
 
 let visit_magic k = function
   | List0 (t, l) -> List0 (k t, l)
@@ -324,6 +325,28 @@ let boxify = function
   | [ a ] -> a
   | l -> Layout (Box ((H, false, false), l))
 
+let group = function
+  | [ a ] -> a
+  | l -> Layout (Group l)
+
+let ungroup =
+  let rec aux acc =
+    function
+       [] -> List.rev acc
+      | Layout (Group terms) :: terms' -> aux acc (terms @ terms')
+      | term :: terms -> aux (term :: acc) terms
+  in
+    aux []
+
+let dress sauce =
+  let rec aux =
+    function
+      | [] -> []
+      | [hd] -> [hd]
+      | hd :: tl -> hd :: sauce :: aux tl
+  in
+    aux
+
 let find_appl_pattern_uris ap =
   let rec aux acc =
     function