| Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2)
| Ast.LetIn (var, t1, t3) ->
Ast.LetIn (aux_capture_variable var, k t1, k t3)
- | Ast.LetRec (kind, definitions, term) ->
- let definitions =
- List.map
- (fun (params, var, ty, decrno) ->
- List.map aux_capture_variable params, aux_capture_variable var,
- k ty, decrno)
- definitions
- in
- Ast.LetRec (kind, definitions, k term)
| Ast.Ident (name, Some substs) ->
Ast.Ident (name, Some (aux_substs substs))
| Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs substs))
| Ast.Ascription (t, s) -> Ast.Ascription (k t, s)
let variables_of_term t =
- let rec vars = ref [] in
+ let vars = ref [] in
let add_variable v =
if List.mem v !vars then ()
else vars := v :: !vars
List.map aux (variables_of_term t)
let keywords_of_term t =
- let rec keywords = ref [] in
+ let keywords = ref [] in
let add_keyword k = keywords := k :: !keywords in
let rec aux = function
| Ast.AttributedTerm (_, t) -> aux t
| Ast.AttributedTerm (_, term) -> strip_attributes term
| Ast.Magic m -> Ast.Magic (visit_magic strip_attributes m)
| Ast.Variable _ as t -> t
- | t -> assert false
+ | _t -> assert false
in
visit_ast ~special_k strip_attributes t
| _ -> []
let meta_names_of_term term =
- let rec names = ref [] in
+ let names = ref [] in
let add_name n =
if List.mem n !names then ()
else names := n :: !names
| Ast.AttributedTerm (_, term) -> aux term
| Ast.Appl terms -> List.iter aux terms
| Ast.Binder (_, _, body) -> aux body
- | Ast.Case (term, indty, outty_opt, patterns) ->
+ | Ast.Case (term, _indty, outty_opt, patterns) ->
aux term ;
aux_opt outty_opt ;
List.iter aux_branch patterns
| Ast.LetIn (_, t1, t3) ->
aux t1 ;
aux t3
- | Ast.LetRec (_, definitions, body) ->
- List.iter aux_definition definitions ;
- aux body
| Ast.Uri (_, Some substs) -> aux_substs substs
| Ast.Ident (_, Some substs) -> aux_substs substs
| Ast.Meta (_, substs) -> aux_meta_substs substs
aux term
and aux_pattern =
function
- Ast.Pattern (head, _, vars) -> List.iter aux_capture_var vars
+ Ast.Pattern (_head, _, vars) -> List.iter aux_capture_var vars
| Ast.Wildcard -> ()
- and aux_definition (params, var, term, decrno) =
- List.iter aux_capture_var params ;
- aux_capture_var var ;
- aux term
and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
and aux_variable = function
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
!fresh_index
(* TODO ensure that names generated by fresh_var do not clash with user's *)
- (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
+ (* FG: "η" is not an identifier (it is rendered, but not parsed) *)
let fresh_name () = "eta" ^ string_of_int (fresh_id ())
let rec freshen_term ?(index = ref 0) term =
| _ -> assert false
in
match term with
- | Ast.Symbol (s, instance) -> Ast.Symbol (s, fresh_instance ())
- | Ast.Num (s, instance) -> Ast.Num (s, fresh_instance ())
+ | Ast.Symbol (s, _instance) -> Ast.Symbol (s, fresh_instance ())
+ | Ast.Num (s, _instance) -> Ast.Num (s, fresh_instance ())
| t -> visit_ast ~special_k freshen_term t
let freshen_obj obj =
let freshen_term = freshen_term ~index in
let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in
let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in
- let freshen_capture_variables =
- List.map (fun (n,t) -> (freshen_term n, HExtlib.map_option freshen_term t))
- in
+ let freshen_capture_variable (n, t) = freshen_term n, HExtlib.map_option freshen_term t in
+ let freshen_capture_variables = List.map freshen_capture_variable in
match obj with
- | NotationPt.Inductive (params, indtypes) ->
+ | NotationPt.Inductive (params, indtypes, attrs) ->
let indtypes =
List.map
(fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors))
indtypes
in
- NotationPt.Inductive (freshen_capture_variables params, indtypes)
- | NotationPt.Theorem (flav, n, t, ty_opt,p) ->
+ NotationPt.Inductive (freshen_capture_variables params, indtypes, attrs)
+ | 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.Record (params, n, ty, fields) ->
+ NotationPt.Theorem (n, freshen_term t, ty_opt, attrs)
+ | NotationPt.Record (params, n, ty, fields, attrs) ->
NotationPt.Record (freshen_capture_variables params, n,
- freshen_term ty, freshen_name_ty_b fields)
+ freshen_term ty, freshen_name_ty_b fields, attrs)
+ | NotationPt.LetRec (kind, definitions, attrs) ->
+ let definitions =
+ List.map
+ (fun (params, var, ty, decrno) ->
+ freshen_capture_variables params, freshen_capture_variable var,
+ freshen_term ty, decrno)
+ definitions
+ in
+ NotationPt.LetRec (kind, definitions, attrs)
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)
+;;
projects / helm.git / blobdiff