X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_exportation%2FcicExportation.ml;h=e5f1face1e9eb854049ba089b723f8d0a8705321;hb=935c5379057ce2fe11fc660b55937ff1b153a670;hp=8acb873a914399939d03b900914adfb7819077a9;hpb=d16f0f84149954af38ea8c05e750091635d1a130;p=helm.git

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index 8acb873a9..e5f1face1 100644
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -44,12 +44,13 @@ let analyze_term context t =
 let analyze_type context t =
  let rec aux =
   function
-     Cic.Sort _ -> `Sort
-   | Cic.Prod (_,_,t) -> aux t
+     Cic.Sort s -> `Sort s
+   | Cic.Prod (_,_,t)
+   | Cic.Lambda (_,_,t) -> aux t
    | _ -> `SomethingElse
  in
  match aux t with
-    `Sort -> `Sort
+    `Sort _ as res -> res
   | `SomethingElse ->
       match
        fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)
@@ -84,11 +85,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 +120,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 ->
@@ -152,7 +169,7 @@ let rec pp t context =
     | C.Cast (v,t) -> pp v context
     | C.Lambda (b,s,t) ->
        (match analyze_type context s with
-           `Sort
+           `Sort _
          | `Statement -> pp t ((Some (b,Cic.Decl s))::context)
          | `Type -> "(function " ^ ppname b ^ " -> " ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")")
     | C.LetIn (b,s,t) ->
@@ -165,13 +182,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 +202,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 +231,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
         )
@@ -296,63 +323,84 @@ in
  pp
 ;;
 
+let ppty current_module_name =
+ let rec args context =
+  function
+     Cic.Prod (n,s,t) ->
+       (match analyze_type context s with
+           `Sort Cic.Prop -> args ((Some (n,Cic.Decl s))::context) t
+         | `Statement
+         | `Sort _ ->
+             let n =
+              match n with
+                 Cic.Anonymous -> Cic.Anonymous
+               | Cic.Name name -> Cic.Name ("'" ^ name) in
+             let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
+              (match n with
+                  Cic.Anonymous -> abstr
+                | Cic.Name name -> name::abstr),
+              args
+         | `Type ->
+             let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
+              abstr,pp current_module_name s context::args)
+   | _ -> [],[]
+ in
+  args
+;;
+
 (* ppinductiveType (typename, inductive, arity, cons)                       *)
 (* pretty-prints a single inductive definition                              *)
 (* (typename, inductive, arity, cons)                                       *)
-let ppinductiveType (typename, inductive, arity, cons) =
- let abstr,scons =
-  List.fold_right
-   (fun (id,ty) (abstr,i) ->
-     let rec args context =
-      function
-         Cic.Prod (n,s,t) ->
-           (match analyze_type context s with
-               `Statement
-             | `Sort ->
-                 let n =
-                  match n with
-                     Cic.Anonymous -> Cic.Anonymous
-                   | Cic.Name name -> Cic.Name ("'" ^ name) in
-                 let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
-                  (match n with
-                      Cic.Anonymous -> abstr
-                    | Cic.Name name -> name::abstr),
-                  args
-             | `Type ->
-                 let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
-                  abstr,pp s context::args)
-       | _ -> [],[]
+let ppinductiveType current_module_name (typename, inductive, arity, cons) =
+ match analyze_type [] arity with
+    `Sort Cic.Prop -> ""
+  | `Statement
+  | `Type -> assert false
+  | `Sort _ ->
+    let abstr,scons =
+     List.fold_right
+      (fun (id,ty) (abstr,i) ->
+         let abstr',sargs = ppty current_module_name [] ty in
+         let sargs = String.concat " * " sargs in
+          abstr'@abstr,
+          String.capitalize id ^
+           (if sargs = "" then "" else " of " ^ sargs) ^
+           (if i = "" then "\n" else "\n | ") ^ i)
+      cons ([],"")
      in
-      let abstr',sargs = args [] ty in
-      let sargs = String.concat " * " sargs in
-       abstr'@abstr,
-       String.capitalize id ^
-        (if sargs = "" then "" else " of " ^ sargs) ^
-        (if i = "" then "\n" else "\n | ") ^ i)
-   cons ([],"")
-  in
-   let abstr =
-    let s = String.concat "," abstr in
-    if s = "" then "" else "(" ^ s ^ ") "
-   in
-   "type " ^ abstr ^ typename ^ " =\n" ^ scons
+      let abstr =
+       let s = String.concat "," abstr in
+       if s = "" then "" else "(" ^ s ^ ") "
+      in
+      "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n"
 ;;
 
-(* 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
-          `Statement -> ""
-        | `Type
-        | `Sort -> "let " ^ ppid name ^ " =\n" ^ pp t1 [] ^ "\n")
+          `Sort Cic.Prop
+        | `Statement -> ""
+        | `Type -> "let " ^ ppid name ^ " =\n" ^ pp t1 [] ^ "\n"
+        | `Sort _ ->
+            match analyze_type [] t1 with
+               `Sort Cic.Prop -> ""
+             | _ ->
+               let abstr,args = ppty current_module_name [] t1 in
+               let abstr =
+                let s = String.concat "," abstr in
+                if s = "" then "" else "(" ^ s ^ ") "
+               in
+                "type " ^ abstr ^ ppid name ^ " = " ^ String.concat "->" args ^
+                "\n")
    | C.Constant (name, None, ty, params, _) ->
       (match analyze_type [] ty with
-          `Statement -> ""
-        | `Sort -> "type " ^ ppid name ^ "\n"
+          `Sort Cic.Prop
+        | `Statement -> ""
+        | `Sort _ -> "type " ^ ppid name ^ "\n"
         | `Type -> "let " ^ ppid name ^ " = assert false\n")
    | C.Variable (name, bo, ty, params, _) ->
       "Variable " ^ name ^
@@ -392,10 +440,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 ""
 ;;
 
-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"
 ;;