- it is not possible to match the `in intype` foo part
- it is not possible to match the outtype
eta expansion still done on Ast (hard to do it in Cic. The abstracted variable
does not have a type :-( thus you may have to double your notations. Name for fresh variables changed to \etaX instead of freshX (much shorter in terms of screen pixels)
module Ast = CicNotationPt
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) ->
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, t3) ->
Ast.LetIn (aux_capture_variable var, k t1, k t3)
| 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)
| None -> None
| Some term -> Some (k term)
and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
| 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 =
+ 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 ->
function
Ast.Pattern (head, hrefs, vars), term ->
- Ast.Pattern (head, hrefs, List.map aux_capture_variable vars), k 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
| Ast.Wildcard, term -> Ast.Wildcard, k term
and aux_subst (name, term) = (name, k term)
and aux_substs substs = List.map aux_subst substs
!fresh_index
(* TODO ensure that names generated by fresh_var do not clash with user's *)
!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 ())
+let fresh_name () = "η" ^ string_of_int (fresh_id ())
let rec freshen_term ?(index = ref 0) term =
let freshen_term = freshen_term ~index in
let rec freshen_term ?(index = ref 0) term =
let freshen_term = freshen_term ~index in
val visit_ast:
?special_k:(CicNotationPt.term -> CicNotationPt.term) ->
val visit_ast:
?special_k:(CicNotationPt.term -> CicNotationPt.term) ->
+ ?map_xref_option:(CicNotationPt.href option -> CicNotationPt.href option) ->
+ ?map_case_indty:(CicNotationPt.case_indtype option ->
+ CicNotationPt.case_indtype option) ->
+ ?map_case_outtype:((CicNotationPt.term -> CicNotationPt.term) ->
+ CicNotationPt.term option -> CicNotationPt.term
+ option) ->
(CicNotationPt.term -> CicNotationPt.term) ->
CicNotationPt.term ->
CicNotationPt.term
(CicNotationPt.term -> CicNotationPt.term) ->
CicNotationPt.term ->
CicNotationPt.term
subterms := t :: !subterms ;
Ast.Implicit
in
subterms := t :: !subterms ;
Ast.Implicit
in
- let rec aux t = CicNotationUtil.visit_ast ~special_k map_term t
+ let rec aux t =
+ CicNotationUtil.visit_ast
+ ~map_xref_option:(fun _ -> None)
+ ~map_case_indty:(fun _ -> None)
+ ~map_case_outtype:(fun _ _ -> None)
+ ~special_k map_term t
and special_k = function
| Ast.AttributedTerm (_, t) -> aux t
| _ -> assert false
and special_k = function
| Ast.AttributedTerm (_, t) -> aux t
| _ -> assert false