X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgGrafite.ml;h=27ed9a1c4df539ceb454119a8a69bb9f3f78ac59;hb=fdb80b08af83b86759833142456ce3c4f84cd80e;hp=13e9ce334aee99802cd3ca0ff7bed2401674baed;hpb=3e5683b1efeb08431c8bb34718920384bfe6625a;p=helm.git diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml index 13e9ce334..27ed9a1c4 100644 --- a/helm/software/helena/src/basic_rg/brgGrafite.ml +++ b/helm/software/helena/src/basic_rg/brgGrafite.ml @@ -9,21 +9,25 @@ \ / 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 + +IFDEF MANAGER THEN (* Internal functions *******************************************************) let ok = ref true +let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true) + let base = "matita" let ext = ".ma" @@ -31,20 +35,20 @@ let ext = ".ma" 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 ich = open_in !G.preamble 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,66 +67,67 @@ 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 - | B.LRef (_, i) -> - let _, _, a, b = B.get e i in - P.fprintf och "%a" out_name a - | B.GRef (_, s) -> - P.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 - | B.Appl (_, v, t) -> + | B.Sort k -> + let sort = if k = 0 then "Type[0]" else if k = 1 then "Prop" else assert false in + KP.fprintf och "%s" sort + | B.LRef (_, i) -> + let _, _, _, y, b = B.get e i in + KP.fprintf och "%a" out_name y + | B.GRef (_, s) -> + KP.fprintf och "%a" out_uri s + | B.Cast (u, t) -> + 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 - | B.Bind (a, B.Abst (n, w), t) -> + KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp + | B.Bind (y, B.Abst (r, n, w), 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.abst n w) in - let binder = match N.to_string st n with - | "1" -> "Π" - | "2" -> "λ" - | _ -> ok := false; "?" + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abst r n w) in + let binder = match N.to_string st n, fst y.E.b_main with + | "1", 0 -> "Π" + | "1", 1 -> "∀" + | "2", _ -> "λ" + | _ -> ok := false; "?" in - P.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) -> + KP.fprintf och "%s%s%a:%a.%a%s" + op binder out_name y (out_term st false e) w (out_term st false ee) t cp + | B.Bind (y, 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" - 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 () + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abbr v) in + KP.fprintf och "%slet %a ≝ %a in %a%s" + op out_name y (out_term st false e) v (out_term st false ee) t cp + | B.Bind (a, B.Void, t) -> C.err () + +let close_out och () = close_out och + +let output_entity och st (_, na, u, b) = + out_comment och (KP.sprintf "constant %u" na.E.n_apix); + match b with + | E.Abbr v -> + KP.fprintf och "definition %a ≝ %a.\n\n%!" out_uri u (out_term st false B.empty) v; !ok + | E.Abst w -> + KP.fprintf och "axiom %a : %a.\n\n%!" out_uri u (out_term st false B.empty) w; !ok + | E.Void -> 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.manager_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 is generated by %s: do not edit" G.version_string); + out_top_comment och version; out_include och "basics/pts"; - och - -let output_entity st och (_, na, s, b) = - let f i = - out_comment och (P.sprintf "notion %u" i); - 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 - | E.Abst t -> - P.fprintf och "axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok - | E.Void -> C.err () - in - E.apix C.err f na + output_entity och, close_out och -let close_out och = close_out och +END