let find_appl_pattern_uris ap =
let rec aux acc =
function
- | Ast.UriPattern uri -> `Uri uri :: acc
- | Ast.NRefPattern nref -> `NRef nref :: acc
+ | Ast.NRefPattern nref -> nref :: acc
| Ast.ImplicitPattern
| Ast.VarPattern _ -> acc
| Ast.ApplPattern apl -> List.fold_left aux acc apl
in
let uris = aux [] ap in
- let cmp u1 u2 =
- match u1,u2 with
- `Uri u1, `Uri u2 -> UriManager.compare u1 u2
- | `NRef r1, `NRef r2 -> NReference.compare r1 r2
- | `Uri _,`NRef _ -> -1
- | `NRef _, `Uri _ -> 1
- in
- HExtlib.list_uniq (List.fast_sort cmp uris)
+ HExtlib.list_uniq (List.fast_sort NReference.compare uris)
let rec find_branch =
function
| Ast.Magic (Ast.If (_, t, _)) -> find_branch t
| t -> t
-let cic_name_of_name = function
- | Ast.Ident ("_", None) -> Cic.Anonymous
- | Ast.Ident (name, None) -> Cic.Name name
- | _ -> assert false
-
-let name_of_cic_name =
-(* let add_dummy_xref t = Ast.AttributedTerm (`IdRef "", t) in *)
- (* ZACK why we used to generate dummy xrefs? *)
- let add_dummy_xref t = t in
- function
- | Cic.Name s -> add_dummy_xref (Ast.Ident (s, None))
- | Cic.Anonymous -> add_dummy_xref (Ast.Ident ("_", None))
-
let fresh_index = ref ~-1
type notation_id = int
indtypes
in
NotationPt.Inductive (freshen_capture_variables params, indtypes)
- | NotationPt.Theorem (flav, n, t, ty_opt,p) ->
+ | NotationPt.Theorem (n, t, ty_opt, attrs) ->
let ty_opt =
match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
in
- NotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
+ NotationPt.Theorem (n, freshen_term t, ty_opt, attrs)
| NotationPt.Record (params, n, ty, fields) ->
NotationPt.Record (freshen_capture_variables params, n,
freshen_term ty, freshen_name_ty_b fields)
let freshen_term = freshen_term ?index:None
+let rec refresh_uri_in_term ~refresh_uri_in_term:refresh_in_cic
+ ~refresh_uri_in_reference
+=
+ function
+ NotationPt.NRef ref -> NotationPt.NRef (refresh_uri_in_reference ref)
+ | NotationPt.NCic t -> NotationPt.NCic (refresh_in_cic t)
+ | t ->
+ visit_ast
+ (refresh_uri_in_term ~refresh_uri_in_term:refresh_in_cic
+ ~refresh_uri_in_reference) t
+ ~special_k:(fun x -> x)
+ ~map_xref_option:(function Some ref -> Some (refresh_uri_in_reference ref)
+ | x -> x)
+ ~map_case_indty:(function (Some (s,Some ref)) -> Some (s, Some
+ (refresh_uri_in_reference ref)) | x -> x)
+;;