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.Meta (index, substs) -> Ast.Meta (index, List.map aux_opt substs)
| (Ast.AttributedTerm _
| Ast.Layout _
| Ast.Num _
| Ast.Sort _
| Ast.Symbol _
- | Ast.Uri _
| Ast.UserInput) as t -> t
and aux_opt = function
| None -> None
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
aux
| 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
| Ast.Implicit _
| Ast.Num _
| Ast.Sort _
| Ast.Symbol _
- | Ast.Uri _
| Ast.UserInput -> ()
| Ast.Magic magic -> aux_magic magic
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
| Ast.NumVar name -> add_name name
(* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
let fresh_name () = "eta" ^ string_of_int (fresh_id ())
+(* XXX FIXME: was used to add instance indices to symbols/numbers
+ * do we even need a similar operation?
+ * currently an identity function! *)
let rec freshen_term ?(index = ref 0) term =
let freshen_term = freshen_term ~index in
let fresh_instance () = incr index; !index in
| _ -> 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, x) -> Ast.Symbol (s, x (* fresh_instance () *))
+ | Ast.Num (s, x) -> Ast.Num (s, x (* fresh_instance () *))
| t -> visit_ast ~special_k freshen_term t
let freshen_obj obj =