- exported CPS iterator visit_magic

[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.ml

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index a7d7e733d437d0b8e3d66fe5f022bb1c335ea74e..29edf6e7cb6354de9f4587cf360eed2473bdd384 100644 (file)
--- 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
+