From 7197b0c80afda28580f5b8cc5e7fb5e5697dc435 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 12 Sep 2005 09:19:28 +0000
Subject: [PATCH] - exported CPS iterator visit_magic - added CPS iterator
 vivist_variable - added freshen_term/freshen_obj which freshen instance
 numbers on ASTs

---
 helm/ocaml/cic_notation/cicNotationUtil.ml  | 46 +++++++++++++++++++++
 helm/ocaml/cic_notation/cicNotationUtil.mli | 15 +++++++
 2 files changed, 61 insertions(+)

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index a7d7e733d..29edf6e7c 100644
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -93,6 +93,13 @@ let visit_magic k = function
   | Ast.If (t1, t2, t3) -> Ast.If (k t1, k t2, k t3)
   | Ast.Fail -> Ast.Fail
 
+let visit_variable k = function
+  | Ast.NumVar _
+  | Ast.IdentVar _
+  | Ast.TermVar _
+  | Ast.FreshVar _ as t -> t
+  | Ast.Ascription (t, s) -> Ast.Ascription (k t, s)
+
 let variables_of_term t =
   let rec vars = ref [] in
   let add_variable v =
@@ -334,3 +341,42 @@ let fresh_id () =
   (* TODO ensure that names generated by fresh_var do not clash with user's *)
 let fresh_name () = "fresh" ^ string_of_int (fresh_id ())
 
+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
+
diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli
index a7dbc2aca..80e365242 100644
--- a/helm/ocaml/cic_notation/cicNotationUtil.mli
+++ b/helm/ocaml/cic_notation/cicNotationUtil.mli
@@ -42,6 +42,16 @@ val visit_layout:
   CicNotationPt.layout_pattern ->
     CicNotationPt.layout_pattern
 
+val visit_magic:
+  (CicNotationPt.term -> CicNotationPt.term) ->
+  CicNotationPt.magic_term ->
+    CicNotationPt.magic_term
+
+val visit_variable:
+  (CicNotationPt.term -> CicNotationPt.term) ->
+  CicNotationPt.pattern_variable ->
+    CicNotationPt.pattern_variable
+
 val strip_attributes: CicNotationPt.term -> CicNotationPt.term
 
   (** generalization of List.combine to n lists *)
@@ -65,6 +75,11 @@ val find_branch:
 val cic_name_of_name: CicNotationPt.term -> Cic.name
 val name_of_cic_name: Cic.name -> CicNotationPt.term
 
+  (** Symbol/Numbers instances *)
+
+val freshen_term: CicNotationPt.term -> CicNotationPt.term
+val freshen_obj: GrafiteAst.obj -> GrafiteAst.obj
+
   (** Notation id handling *)
 
 type notation_id
-- 
2.39.2