X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationUtil.ml;h=f2c2539cde31f20e5c4a8a7a2c6019b327e189fe;hb=1bcad789810fd37d346e690f18557aeedc6fe08c;hp=1f9d9f5ccee6ad17203c5f0d0fb761ccc31d3c88;hpb=ba2dfe6409e95bf9e558dc0d4be382b068671409;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index 1f9d9f5cc..f2c2539cd 100644
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -25,13 +25,6 @@
 
 open CicNotationPt
 
-  (* TODO ensure that names generated by fresh_var do not clash with user's *)
-let fresh_name =
-  let index = ref ~-1 in
-  fun () ->
-    incr index;
-    "fresh" ^ string_of_int !index
-
 (* let meta_names_of term = *)
 (*   let rec names = ref [] in *)
 (*   let add_name n = *)
@@ -105,6 +98,7 @@ let visit_ast ?(special_k = fun _ -> assert false) k =
         Binder (kind, aux_capture_variable var, k body) 
     | Case (term, indtype, typ, patterns) ->
         Case (k term, indtype, aux_opt typ, aux_patterns patterns)
+    | Cast (t1, t2) -> Cast (k t1, k t2)
     | LetIn (var, t1, t2) -> LetIn (aux_capture_variable var, k t1, k t2)
     | LetRec (kind, definitions, term) ->
         let definitions =
@@ -152,6 +146,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 +319,32 @@ let boxify = function
   | [ a ] -> a
   | l -> Layout (Box ((H, false, false), l))
 
+let unboxify = function
+  | Layout (Box ((H, false, false), [ a ])) -> a
+  | l -> 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
@@ -332,6 +353,7 @@ let find_appl_pattern_uris ap =
           ignore (List.find (fun uri' -> UriManager.eq uri uri') acc);
           acc
         with Not_found -> uri :: acc)
+    | ImplicitPattern
     | VarPattern _ -> acc
     | ApplPattern apl -> List.fold_left aux acc apl
   in
@@ -342,3 +364,24 @@ let rec find_branch =
       Magic (If (_, Magic Fail, t)) -> find_branch t
     | Magic (If (_, t, _)) -> find_branch t
     | t -> t
+
+let cic_name_of_name = function
+  | CicNotationPt.Ident ("_", None) -> Cic.Anonymous
+  | CicNotationPt.Ident (name, None) -> Cic.Name name
+  | _ -> assert false
+
+let name_of_cic_name = function
+  | Cic.Name s -> CicNotationPt.Ident (s, None)
+  | Cic.Anonymous -> CicNotationPt.Ident ("_", None)
+
+let fresh_index = ref ~-1
+
+type notation_id = int
+
+let fresh_id () =
+  incr fresh_index;
+  !fresh_index
+
+  (* TODO ensure that names generated by fresh_var do not clash with user's *)
+let fresh_name () = "fresh" ^ string_of_int (fresh_id ())
+