X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationUtil.ml;h=887f5bf0564f1e1c20cbec279b91c46e0f0cbb81;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=a7d7e733d437d0b8e3d66fe5f022bb1c335ea74e;hpb=1ca0ec89cfc2c3f85af95d5b1bdad07597d976bd;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index a7d7e733d..887f5bf05 100644
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -63,8 +63,8 @@ let visit_ast ?(special_k = fun _ -> assert false) k =
     | Some term -> Some (k term)
   and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
   and aux_patterns patterns = List.map aux_pattern patterns
-  and aux_pattern ((head, vars), term) =
-    ((head, List.map aux_capture_variable vars), k term)
+  and aux_pattern ((head, hrefs, vars), term) =
+    ((head, hrefs, List.map aux_capture_variable vars), k term)
   and aux_subst (name, term) = (name, k term)
   and aux_substs substs = List.map aux_subst substs
   in
@@ -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 =
@@ -153,6 +160,12 @@ let rec strip_attributes t =
   in
   visit_ast ~special_k strip_attributes t
 
+let rec get_idrefs =
+  function
+  | Ast.AttributedTerm (`IdRef id, t) -> id :: get_idrefs t
+  | Ast.AttributedTerm (_, t) -> get_idrefs t
+  | _ -> []
+
 let meta_names_of_term term =
   let rec names = ref [] in
   let add_name n =
@@ -196,7 +209,7 @@ let meta_names_of_term term =
   and aux_branch (pattern, term) =
     aux_pattern pattern ;
     aux term
-  and aux_pattern (head, vars) = 
+  and aux_pattern (head, _, vars) = 
     List.iter aux_capture_var vars
   and aux_definition (var, term, i) =
     aux_capture_var var ;
@@ -293,16 +306,13 @@ let dressn ~sep:sauces =
 let find_appl_pattern_uris ap =
   let rec aux acc =
     function
-    | Ast.UriPattern uri ->
-        (try
-          ignore (List.find (fun uri' -> UriManager.eq uri uri') acc);
-          acc
-        with Not_found -> uri :: acc)
+    | Ast.UriPattern uri -> uri :: acc
     | Ast.ImplicitPattern
     | Ast.VarPattern _ -> acc
     | Ast.ApplPattern apl -> List.fold_left aux acc apl
   in
-  aux [] ap
+  let uris = aux [] ap in
+  HExtlib.list_uniq (List.fast_sort UriManager.compare uris)
 
 let rec find_branch =
   function
@@ -334,3 +344,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
+