]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationUtil.ml
snapshot, notably:
[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.ml
index 1f9d9f5ccee6ad17203c5f0d0fb761ccc31d3c88..4dbc83f9eb7d4ffd275fd0be51b7f0bdacd0e2d0 100644 (file)
@@ -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,16 +325,38 @@ 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
-    | UriPattern uri ->
+    | GrafiteAst.UriPattern uri ->
         (try
           ignore (List.find (fun uri' -> UriManager.eq uri uri') acc);
           acc
         with Not_found -> uri :: acc)
-    | VarPattern _ -> acc
-    | ApplPattern apl -> List.fold_left aux acc apl
+    | GrafiteAst.VarPattern _ -> acc
+    | GrafiteAst.ApplPattern apl -> List.fold_left aux acc apl
   in
   aux [] ap