X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationUtil.ml;h=e4145e118984e5311195000ea52d9b5edd7720b9;hb=206f96afb7097c20b3cc8bd144825467b4fde7ae;hp=4dbc83f9eb7d4ffd275fd0be51b7f0bdacd0e2d0;hpb=34113d572c334c351ba66f4b05db503eed4d48f2;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index 4dbc83f9e..e4145e118 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 = @@ -325,6 +319,10 @@ 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) @@ -338,7 +336,7 @@ let ungroup = in aux [] -let dress sauce = +let dress ~sep:sauce = let rec aux = function | [] -> [] @@ -347,16 +345,26 @@ let dress sauce = in aux +let dressn ~sep:sauces = + let rec aux = + function + | [] -> [] + | [hd] -> [hd] + | hd :: tl -> hd :: sauces @ aux tl + in + aux + let find_appl_pattern_uris ap = let rec aux acc = function - | GrafiteAst.UriPattern uri -> + | UriPattern uri -> (try ignore (List.find (fun uri' -> UriManager.eq uri uri') acc); acc with Not_found -> uri :: acc) - | GrafiteAst.VarPattern _ -> acc - | GrafiteAst.ApplPattern apl -> List.fold_left aux acc apl + | ImplicitPattern + | VarPattern _ -> acc + | ApplPattern apl -> List.fold_left aux acc apl in aux [] ap @@ -365,3 +373,26 @@ 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 = + let add_dummy_xref t = CicNotationPt.AttributedTerm (`IdRef "", t) in + function + | Cic.Name s -> add_dummy_xref (CicNotationPt.Ident (s, None)) + | Cic.Anonymous -> add_dummy_xref (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 ()) +