- exported CPS iterator visit_magic

- added CPS iterator vivist_variable
- added freshen_term/freshen_obj which freshen instance numbers on ASTs

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
+

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli
index a7dbc2aca8d139d4f7532bc7cba4b5c245cba121..80e36524225339c3ab6f2fe05e7bd3d23d17f2c6 100644 (file)
--- 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