+let rec freshen_term ?(index = ref 0) term =
+ let freshen_term = freshen_term ~index in
+ let fresh_instance () = incr index; !index in
+ let special_k = function
+ | Ast.AttributedTerm (attr, t) -> Ast.AttributedTerm (attr, freshen_term t)
+ | Ast.Layout l -> Ast.Layout (visit_layout freshen_term l)
+ | Ast.Magic m -> Ast.Magic (visit_magic freshen_term m)
+ | Ast.Variable v -> Ast.Variable (visit_variable freshen_term v)
+ | Ast.Literal _ as t -> t
+ | _ -> assert false
+ in
+ match term with
+ | 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 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
+ match obj with
+ | GrafiteAst.Inductive (params, indtypes) ->
+ let indtypes =
+ List.map
+ (fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors))
+ indtypes
+ in
+ GrafiteAst.Inductive (freshen_name_ty params, indtypes)
+ | GrafiteAst.Theorem (flav, n, t, ty_opt) ->
+ let ty_opt =
+ match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
+ in
+ GrafiteAst.Theorem (flav, n, freshen_term t, ty_opt)
+ | GrafiteAst.Record (params, n, ty, fields) ->
+ GrafiteAst.Record (freshen_name_ty params, n, freshen_term ty,
+ freshen_name_ty fields)
+
+let freshen_term = freshen_term ?index:None
+