X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgGrafite.ml;h=493ad3cac848532158ada852d01665d1062d69c8;hb=433d9c9612c1557e03a549e004c796c1137d4b4a;hp=53956d932ba79185dd03c88657afcfa1ca6d3734;hpb=04ffe68396b98bbf21bcd403ffba03b94eaebadc;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml
index 53956d932..493ad3cac 100644
--- a/helm/software/helena/src/basic_rg/brgGrafite.ml
+++ b/helm/software/helena/src/basic_rg/brgGrafite.ml
@@ -9,16 +9,16 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module F = Filename
-module P = Printf
+module KF = Filename
+module KP = Printf
 
-module U = NUri
-module C = Cps
-module G = Options
-module N = Level
-module E = Entity
-module R = Alpha
-module B = Brg
+module U  = NUri
+module C  = Cps
+module G  = Options
+module N  = Layer
+module E  = Entity
+module R  = Alpha
+module B  = Brg
 
 (* Internal functions *******************************************************)
 
@@ -32,19 +32,19 @@ let width = 70
 
 let out_preamble och =
    let ich = open_in !G.ma_preamble in
-   let rec aux () = P.fprintf och "%s\n" (input_line ich); aux () in
+   let rec aux () = KP.fprintf och "%s\n" (input_line ich); aux () in
    try aux () with End_of_file -> close_in ich
 
 let out_top_comment och msg =
    let padding = width - String.length msg in
    let padding = if padding >= 0 then padding else 0 in
-   P.fprintf och "(* %s %s*)\n\n" msg (String.make padding '*')
+   KP.fprintf och "(* %s %s*)\n\n" msg (String.make padding '*')
 
 let out_comment och msg =
-   P.fprintf och "(* %s *)\n" msg 
+   KP.fprintf och "(* %s *)\n" msg 
 
 let out_include och src =
-   P.fprintf och "include \"%s.ma\".\n\n" src
+   KP.fprintf och "include \"%s.ma\".\n\n" src
 
 let out_uri och u =
    let str = U.string_of_uri u in
@@ -63,26 +63,27 @@ let out_uri och u =
 
 let out_name och a =
    let f n = function 
-      | true  -> P.fprintf och "%s" n
-      | false -> C.err ()
+      | true  -> KP.fprintf och "%s" n
+      | false -> KP.fprintf och "_"
    in
-   E.name C.err f a
+   let err () = f "" false in
+   E.name err f a
 
 let rec out_term st p e och = function
    | B.Sort (_, h)           -> 
       let sort = if h = 0 then "Type[0]" else if h = 1 then "Prop" else assert false in
-      P.fprintf och "%s" sort
+      KP.fprintf och "%s" sort
    | B.LRef (_, i)           ->       
       let _, _, a, b = B.get e i in
-      P.fprintf och "%a" out_name a
+      KP.fprintf och "%a" out_name a
    | B.GRef (_, s)           ->
-      P.fprintf och "%a" out_uri s
+      KP.fprintf och "%a" out_uri s
    | B.Cast (_, u, t)        ->
-      P.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u 
+      KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u 
    | B.Appl (_, v, t)        ->
       let pt = match t with B.Appl _ -> false | _ -> true in
       let op, cp = if p then "(", ")" else "", "" in
-      P.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp
+      KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp
    | B.Bind (a, B.Abst (n, w), t) ->
       let op, cp = if p then "(", ")" else "", "" in
       let a = R.alpha B.mem e a in
@@ -93,34 +94,34 @@ let rec out_term st p e och = function
          | "2", _ -> "λ"
          | _      -> ok := false; "?"
       in
-      P.fprintf och "%s%s%a:%a.%a%s"
+      KP.fprintf och "%s%s%a:%a.%a%s"
          op binder out_name a (out_term st false e) w (out_term st false ee) t cp
    | B.Bind (a, B.Abbr v, t) ->
       let op, cp = if p then "(", ")" else "", "" in
       let a = R.alpha B.mem e a in
       let ee = B.push e B.empty a (B.abbr v) in
-      P.fprintf och "%slet %a ≝ %a in %a%s"
+      KP.fprintf och "%slet %a ≝ %a in %a%s"
          op out_name a (out_term st false e) v (out_term st false ee) t cp
    | B.Bind (a, B.Void, t)   -> C.err ()
 
 (* Interface functions ******************************************************)
 
 let open_out fname =
-   let dir = F.concat !G.ma_dir base in 
-   let path = F.concat dir fname in
+   let dir = KF.concat !G.ma_dir base in 
+   let path = KF.concat dir fname in
    let och = open_out (path ^ ext) in
    out_preamble och;
-   out_top_comment och (P.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
    out_include och "basics/pts";
    och
 
 let output_entity st och (_, na, s, b) =
-   out_comment och (P.sprintf "constant %u" na.E.n_apix);
+   out_comment och (KP.sprintf "constant %u" na.E.n_apix);
    match b with
       | E.Abbr t ->
-         P.fprintf och "definition %a ≝ %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
+         KP.fprintf och "definition %a ≝ %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
       | E.Abst t ->
-         P.fprintf och "axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
+         KP.fprintf och "axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
       | E.Void   -> C.err ()
 
 let close_out och = close_out och