All names are now qualified. This avoids the need for "open" statements.

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index 8acb873a914399939d03b900914adfb7819077a9..b493c4e4096faca4029f32916f8cc39ec2dce42d 100644 (file)
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -84,11 +84,26 @@ let rec get_nth l n =
   | (_,_) -> raise NotEnoughElements
 ;;
 
+let qualified_name_of_uri current_module_name ?(capitalize=false) uri =
+ let name =
+  if capitalize then
+   String.capitalize (UriManager.name_of_uri uri)
+  else
+   ppid (UriManager.name_of_uri uri) in
+ let buri = UriManager.buri_of_uri uri in
+ let index = String.rindex buri '/' in
+ let filename = String.sub buri (index + 1) (String.length buri - index - 1) in
+  if current_module_name = filename then
+   name
+  else
+   String.capitalize filename ^ "." ^ name
+;;
+
 (* pp t l                                                                  *)
 (* pretty-prints a term t of cic in an environment l where l is a list of  *)
 (* identifier names used to resolve DeBrujin indexes. The head of l is the *)
 (* name associated to the greatest DeBrujin index in t                     *)
-let pp ?metasenv =
+let pp current_module_name ?metasenv =
 let rec pp t context =
  let module C = Cic in
    match t with
@@ -104,7 +119,8 @@ let rec pp t context =
          NotEnoughElements -> string_of_int (List.length context - n)
        end
     | C.Var (uri,exp_named_subst) ->
-       UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst context
+        qualified_name_of_uri current_module_name uri ^
+         pp_exp_named_subst exp_named_subst context
     | C.Meta (n,l1) ->
        (match metasenv with
            None ->
@@ -165,13 +181,17 @@ let rec pp t context =
     | C.Appl li ->
        "(" ^ String.concat " " (clean_args context li) ^ ")"
     | C.Const (uri,exp_named_subst) ->
-       ppid (UriManager.name_of_uri uri) ^ pp_exp_named_subst exp_named_subst context
+       qualified_name_of_uri current_module_name uri ^
+        pp_exp_named_subst exp_named_subst context
     | C.MutInd (uri,n,exp_named_subst) ->
        (try
          match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
             C.InductiveDefinition (dl,_,_,_) ->
              let (name,_,_,_) = get_nth dl (n+1) in
-              ppid name ^ pp_exp_named_subst exp_named_subst context
+              qualified_name_of_uri current_module_name
+               (UriManager.uri_of_string
+                 (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
+              pp_exp_named_subst exp_named_subst context
           | _ -> raise CicExportationInternalError
         with
            Sys.Break as exn -> raise exn
@@ -181,9 +201,12 @@ let rec pp t context =
        (try
          match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
             C.InductiveDefinition (dl,_,_,_) ->
-             let (_,_,_,cons) = get_nth dl (n1+1) in
-              let (id,_) = get_nth cons n2 in
-               String.capitalize id ^ pp_exp_named_subst exp_named_subst context
+             let _,_,_,cons = get_nth dl (n1+1) in
+              let id,_ = get_nth cons n2 in
+               qualified_name_of_uri current_module_name ~capitalize:true
+                (UriManager.uri_of_string
+                  (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
+               pp_exp_named_subst exp_named_subst context
           | _ -> raise CicExportationInternalError
         with
            Sys.Break as exn -> raise exn
@@ -207,7 +230,10 @@ let rec pp t context =
                    | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
                    | _ -> 0
                  in
-                  String.capitalize id, count_prods paramsno ty
+                  qualified_name_of_uri current_module_name ~capitalize:true
+                   (UriManager.uri_of_string
+                     (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
+                  count_prods paramsno ty
                ) cons
           | _ -> raise CicExportationInternalError
         )
@@ -299,7 +325,7 @@ in
 (* ppinductiveType (typename, inductive, arity, cons)                       *)
 (* pretty-prints a single inductive definition                              *)
 (* (typename, inductive, arity, cons)                                       *)
-let ppinductiveType (typename, inductive, arity, cons) =
+let ppinductiveType current_module_name (typename, inductive, arity, cons) =
  let abstr,scons =
   List.fold_right
    (fun (id,ty) (abstr,i) ->
@@ -320,7 +346,7 @@ let ppinductiveType (typename, inductive, arity, cons) =
                   args
              | `Type ->
                  let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
-                  abstr,pp s context::args)
+                  abstr,pp current_module_name s context::args)
        | _ -> [],[]
      in
       let abstr',sargs = args [] ty in
@@ -338,11 +364,10 @@ let ppinductiveType (typename, inductive, arity, cons) =
    "type " ^ abstr ^ typename ^ " =\n" ^ scons
 ;;
 
-(* ppobj obj  returns a string with describing the cic object obj in a syntax *)
-(* similar to the one used by Coq                                             *)
-let ppobj obj =
+let ppobj current_module_name obj =
  let module C = Cic in
  let module U = UriManager in
+  let pp = pp current_module_name in
   match obj with
     C.Constant (name, Some t1, t2, params, _) ->
       (match analyze_type [] t2 with
@@ -392,10 +417,11 @@ let ppobj obj =
         "\n" ^ pp ~metasenv:conjectures value [] ^ " : " ^
           pp ~metasenv:conjectures ty [] 
    | C.InductiveDefinition (l, params, nparams, _) ->
-      List.fold_right (fun x i -> ppinductiveType x ^ i) l "\n"
+      List.fold_right
+       (fun x i -> ppinductiveType current_module_name x ^ i) l "\n"
 ;;
 
-let ppobj obj =
- let res = ppobj obj in
+let ppobj current_module_name obj =
+ let res = ppobj current_module_name obj in
   if res = "" then "" else res ^ ";;\n"
 ;;