(* ||M|| This file is part of HELM, an Hypertextual, Electronic ||A|| Library of Mathematics, developed at the Computer Science ||T|| Department, University of Bologna, Italy. ||I|| ||T|| HELM is free software; you can redistribute it and/or ||A|| modify it under the terms of the GNU General Public License \ / version 2 or (at your option) any later version. \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module KF = Filename module KP = Printf 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 version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true) let ok = ref true let uris = ref [] let chunk = ref 0 let sub_och = ref stdout let top_age = 7000 let size = 250 let base = "lp" let ext_lp = ".elpi" let reserved = ["pi"; "sigma"; "nil"; "delay"; "in"; "with"; "resume"; "context"] let alpha n = if List.mem n reserved then !G.alpha ^ n else n let out_preamble och = 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 = KP.fprintf och "%% %s\n\n" msg let out_comment och msg = KP.fprintf och "%% %s\n" msg let out_clause och msg = KP.fprintf och "%s\n\n" msg let out_uri och u = let str = U.string_of_uri u in let rec aux i = let c = str.[i] in if c = '.' then () else begin output_char och (if c = '/' then '_' else c); aux (succ i) end in let rec strip i n = if n <= 0 then succ i else strip (String.index_from str (succ i) '/') (pred n) in aux (strip 0 3) let out_name och a = let f n = function | true -> KP.fprintf och "%s" (alpha n) | false -> KP.fprintf och "_" in let err () = f "" false in E.name err f a let rec out_term st e och = function | B.Sort k -> let sort = if k = 0 then "(s+type 0)" else if k = 1 then "(s+prop 0)" else assert false in KP.fprintf och "(sort %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 "(abbr %a %a x\\ x)" (out_term st e) t (out_term st e) u | B.Appl (_, v, t) -> KP.fprintf och "(appl %a %a)" (out_term st e) t (out_term st e) v | B.Bind (y, B.Abst (r, n, w), t) -> 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 c = match r, N.to_string st n with | false, "1" -> "prod" | false, "2" -> "abst" | _ -> ok := false; "?" in KP.fprintf och "(%s %a %a\\ %a)" c (out_term st e) w out_name y (out_term st ee) t | B.Bind (_, B.Void, _) -> C.err () | B.Bind (_, B.Abbr _, _) -> C.err () (* PTS variant 2 ************************************************************) let output_entity_pts2 och st (_, na, u, b) = if na.E.n_apix < !G.first then begin match b with | E.Abbr (_, B.Cast (w, v)) -> KP.fprintf och "get_expansion %a %u %a.\n" out_uri u na.E.n_apix (out_term st B.empty) v; KP.fprintf och "get_type %a %a.\n\n" out_uri u (out_term st B.empty) w; !ok | E.Abst (_, w) -> KP.fprintf och "get_type %a %a.\n\n" out_uri u (out_term st B.empty) w; !ok | _ -> C.err () end else if na.E.n_apix <= !G.last then begin match b with | E.Abbr (_, B.Cast (w, v)) -> KP.fprintf och "g+line+2 %a %u\n %a\n %a\n.\n\n" out_uri u na.E.n_apix (out_term st B.empty) v (out_term st B.empty) w; uris := (true, u) :: !uris; !ok | E.Abst (_, w) -> KP.fprintf och "g+line+1 %a %u\n %a\n.\n\n" out_uri u na.E.n_apix (out_term st B.empty) w; uris := (false, u) :: !uris; !ok | _ -> C.err () end else !ok let close_out_pts2 och () = let aux_name (b, s) = let gde = if b then "gdef" else "gdec" in KP.fprintf och "(%s %a\n" gde out_uri s in let aux_sep _ = KP.fprintf och "%s" ")" in out_clause och "grundlagen :- is+valid"; List.iter aux_name (List.rev !uris); KP.fprintf och "%s" "gtop"; List.iter aux_sep !uris; out_clause och "\n\n."; close_out och (* Interface functions ******************************************************) let open_out_pts2 fname = let dir = KF.concat !G.manager_dir base in let path = KF.concat dir fname in let och = open_out (path ^ "b_pts" ^ ext_lp) in out_preamble och; out_top_comment och version; output_entity_pts2 och, close_out_pts2 och END