module Ast = CicNotationPt
-let visit_ast ?(special_k = fun _ -> assert false) k =
+let visit_ast ?(special_k = fun _ -> assert false)
+ ?(map_xref_option= fun x -> x) ?(map_case_indty= fun x -> x)
+ ?(map_case_outtype=
+ fun k x -> match x with None -> None | Some x -> Some (k x))
+ k
+=
let rec aux = function
| Ast.Appl terms -> Ast.Appl (List.map k terms)
| Ast.Binder (kind, var, body) ->
Ast.Binder (kind, aux_capture_variable var, k body)
| Ast.Case (term, indtype, typ, patterns) ->
- Ast.Case (k term, indtype, aux_opt typ, aux_patterns patterns)
+ Ast.Case (k term, map_case_indty indtype, map_case_outtype k typ,
+ aux_patterns map_xref_option patterns)
| Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2)
- | Ast.LetIn (var, t1, t2) ->
- Ast.LetIn (aux_capture_variable var, 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 (var, ty, n) -> aux_capture_variable var, k ty, n)
+ (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)
| None -> None
| Some term -> Some (k term)
and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
- and aux_patterns patterns = List.map aux_pattern patterns
- and aux_pattern ((head, hrefs, vars), term) =
- ((head, hrefs, List.map aux_capture_variable vars), k term)
+ and aux_patterns k_xref patterns = List.map (aux_pattern k_xref) patterns
+ and aux_pattern k_xref =
+ function
+ Ast.Pattern (head, hrefs, vars), term ->
+ Ast.Pattern (head, k_xref hrefs, List.map aux_capture_variable vars), k term
+ | Ast.Wildcard, term -> Ast.Wildcard, k term
and aux_subst (name, term) = (name, k term)
and aux_substs substs = List.map aux_subst substs
in
| Ast.Over (t1, t2) -> Ast.Over (k t1, k t2)
| Ast.Atop (t1, t2) -> Ast.Atop (k t1, k t2)
| Ast.Frac (t1, t2) -> Ast.Frac (k t1, k t2)
+ | Ast.InfRule (t1, t2, t3) -> Ast.InfRule (k t1, k t2, k t3)
| Ast.Sqrt t -> Ast.Sqrt (k t)
| Ast.Root (arg, index) -> Ast.Root (k arg, k index)
| Ast.Break -> Ast.Break
| Ast.Box (kind, terms) -> Ast.Box (kind, List.map k terms)
| Ast.Group terms -> Ast.Group (List.map k terms)
+ | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term)
+ | Ast.Mpadded (l, term) -> Ast.Mpadded (l, List.map k term)
+ | Ast.Maction terms -> Ast.Maction (List.map k terms)
let visit_magic k = function
| Ast.List0 (t, l) -> Ast.List0 (k t, l)
let aux = function
| Ast.NumVar s
| Ast.IdentVar s
- | Ast.TermVar s -> s
+ | Ast.TermVar (s,_) -> s
| _ -> assert false
in
List.map aux (variables_of_term t)
aux term ;
aux_opt outty_opt ;
List.iter aux_branch patterns
- | Ast.LetIn (_, t1, t2) ->
+ | Ast.LetIn (_, t1, t3) ->
aux t1 ;
- aux t2
+ aux t3
| Ast.LetRec (_, definitions, body) ->
List.iter aux_definition definitions ;
aux body
and aux_branch (pattern, term) =
aux_pattern pattern ;
aux term
- and aux_pattern (head, _, vars) =
- List.iter aux_capture_var vars
- and aux_definition (var, term, i) =
+ and aux_pattern =
+ function
+ 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_variable = function
| Ast.NumVar name -> add_name name
| Ast.IdentVar name -> add_name name
- | Ast.TermVar name -> add_name name
+ | Ast.TermVar (name,_) -> add_name name
| Ast.FreshVar _ -> ()
| Ast.Ascription _ -> assert false
and aux_magic = function
!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 ())
+ (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
+let fresh_name () = "eta" ^ string_of_int (fresh_id ())
let rec freshen_term ?(index = ref 0) term =
let freshen_term = freshen_term ~index in
let index = ref 0 in
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) -> (n, freshen_term t, b)) 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
match obj with
| CicNotationPt.Inductive (params, indtypes) ->
let indtypes =
(fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors))
indtypes
in
- CicNotationPt.Inductive (freshen_name_ty params, indtypes)
+ CicNotationPt.Inductive (freshen_capture_variables params, indtypes)
| CicNotationPt.Theorem (flav, n, t, ty_opt) ->
let ty_opt =
match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
in
CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
| CicNotationPt.Record (params, n, ty, fields) ->
- CicNotationPt.Record (freshen_name_ty params, n, freshen_term ty,
- freshen_name_ty_b fields)
+ CicNotationPt.Record (freshen_capture_variables params, n,
+ freshen_term ty, freshen_name_ty_b fields)
let freshen_term = freshen_term ?index:None