helm/software/helena/src/basic_rg/brgLYP.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module KF = Filename
  13 module KP = Printf
  14
  15 module U  = NUri
  16 module C  = Cps
  17 module G  = Options
  18 module N  = Layer
  19 module E  = Entity
  20 module R  = Alpha
  21 module B  = Brg
  22
  23 IFDEF MANAGER THEN
  24
  25 (* Internal functions *******************************************************)
  26
  27 let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true)
  28
  29 let affiliation = "This file is part of the LYP engine"
  30
  31 let description = "This file contains the Grundlagen for lyp_global: validate by invoking clause (grundlagen)"
  32
  33 let ok = ref true
  34
  35 let trusted = ref false (* "trusted" indicator out? *)
  36
  37 let untrusted = ref false (* "untrusted" indicator out? *)
  38
  39 let uris = ref []
  40
  41 let chunk = ref 0
  42
  43 let sub_och = ref stdout
  44
  45 let top_age = 7000
  46
  47 let size = 250
  48
  49 let base = "lp"
  50
  51 let ext_lp = ".elpi"
  52 let ext_tj = ".mod"
  53 let ext_tj_sig = ".sig"
  54
  55 let reserved = ["pi"; "sigma"; "nil"; "delay"; "in"; "with"; "resume"; "context"]
  56
  57 let alpha n =
  58    if List.mem n reserved then !G.alpha ^ n else n
  59
  60 let appl_fragment (_, ds) (_, dm) = match ds, dm with
  61    | 2, 2 -> "ss"
  62    | 2, 1 -> "sb"
  63    | 1, 2 -> "bs"
  64    | 1, 1 -> "bb"
  65    | _    -> ok := false; "??"
  66
  67 let abst_fragment (_, ds) (_, dm) = match ds, dm with
  68    | 1, 2 -> "ss"
  69    | 1, 1 -> "sb"
  70    | 0, 2 -> "bs"
  71    | 0, 1 -> "bb"
  72    | _    -> ok := false; "??"
  73
  74 let prod_fragment (_, ds) (_, dm) = match ds, dm with
  75    | 1, 1 -> "ss"
  76    | 1, 0 -> "sb"
  77    | 0, 1 -> "bs"
  78    | 0, 0 -> "bb"
  79    | _    -> ok := false; "??"
  80
  81 let entity_level (_, ds) = match ds with
  82    | 1 -> "1"
  83    | 2 -> "2"
  84    | _ -> ok := false; "?"
  85
  86 let out_preamble och =
  87    let ich = open_in !G.preamble in
  88    let rec aux () = KP.fprintf och "%s\n" (input_line ich); aux () in
  89    try aux () with End_of_file -> close_in ich
  90
  91 let out_top_comment och msg =
  92    KP.fprintf och "%% %s\n\n" msg
  93
  94 let out_comment och msg =
  95    KP.fprintf och "%% %s\n" msg
  96
  97 let out_clause och msg =
  98    KP.fprintf och "%s\n\n" msg
  99
 100 let out_uri och u =
 101    let str = U.string_of_uri u in
 102    let rec aux i =
 103      let c = str.[i] in
 104      if c = '.' then () else begin
 105         output_char och (if c = '/' then '_' else c);
 106         aux (succ i)
 107      end
 108    in
 109    let rec strip i n =
 110       if n <= 0 then succ i else
 111       strip (String.index_from str (succ i) '/') (pred n)
 112    in
 113    aux (strip 0 3)
 114
 115 let out_name och a =
 116    let f n = function
 117       | true  -> KP.fprintf och "%s" (alpha n)
 118       | false -> KP.fprintf och "_"
 119    in
 120    let err () = f "" false in
 121    E.name err f a
 122
 123 let rec out_term st e och = function
 124    | B.Sort k                        ->
 125       KP.fprintf och "sort"
 126    | B.LRef (_, i)                   ->
 127       let _, _, _, y, b = B.get e i in
 128       KP.fprintf och "%a" out_name y
 129    | B.GRef (_, s)                   ->
 130       KP.fprintf och "%a" out_uri s
 131    | B.Cast (u, t)                   ->
 132       C.err ()
 133    | B.Appl (a, v, t)                ->
 134       let f = appl_fragment a.E.a_side a.E.a_main in
 135       KP.fprintf och "(appl f_%s %a %a)" f (out_term st e) v (out_term st e) t
 136    | B.Bind (a, B.Abst (r, n, w), t) -> (* r *)
 137       let a = R.alpha B.mem e a in
 138       let ee = B.push e B.empty E.empty_node a (B.abst r n w) in
 139       let lf = match N.to_string st n with
 140          | "1" -> "prod", prod_fragment a.E.b_side a.E.b_main
 141          | "2" -> "abst", abst_fragment a.E.b_side a.E.b_main
 142          | _   -> ok := false; "????", "??"
 143       in
 144       let l, f = match lf with
 145          | "abst", "bs" -> "rest", "bs"
 146          | "prod", "bs" -> "rest", "ho"
 147          | "abst", "bb" -> "rest", "ho"
 148          | "prod", "bb" -> "rest", "bb"
 149          | lf           -> lf
 150       in
 151       KP.fprintf och "(%s f_%s %a %a\\ %a)"
 152          l f (out_term st e) w out_name a (out_term st ee) t
 153    | B.Bind (_, B.Abbr _, _)         -> C.err ()
 154    | B.Bind (_, B.Void, _)           -> C.err ()
 155
 156 (* LYP variant 2 ***********************************************************)
 157
 158 let output_entity_lyp2 och st (_, na, u, b) =
 159    begin match !trusted, !untrusted with
 160       | false, _ when na.E.n_apix < !G.first ->
 161          out_top_comment och "Trusted part";
 162          trusted := true
 163       | _ , false when !G.first <= na.E.n_apix && na.E.n_apix <= !G.last ->
 164          out_top_comment och "Untrusted part";
 165          untrusted := true
 166       | _ -> ()
 167    end;
 168    if na.E.n_apix < !G.first then match b with
 169       | E.Abbr (a, B.Cast (w, v)) ->
 170          KP.fprintf och "type %a @id.\n" out_uri u;
 171          KP.fprintf och "dec_l %a d_%s\n      %a\n.\n"
 172             out_uri u (entity_level a.E.e_side) (out_term st B.empty) w;
 173          KP.fprintf och "def_l %a\n      %a\n.\n\n"
 174             out_uri u (out_term st B.empty) v;
 175          !ok
 176       | E.Abst (a, w)             ->
 177          KP.fprintf och "type %a @id.\n" out_uri u;
 178          KP.fprintf och "dec_l %a d_%s\n      %a\n.\n\n"
 179             out_uri u (entity_level a.E.e_side) (out_term st B.empty) w;
 180          !ok
 181       | _                         -> C.err ()
 182    else if na.E.n_apix <= !G.last then match b with
 183       | E.Abbr (a, B.Cast (w, v)) ->
 184          KP.fprintf och "type %a @id.\n" out_uri u;
 185          KP.fprintf och "type c_%u ann.\n" na.E.n_apix;
 186          KP.fprintf och "cast_g %a c_%u d_%s\n       %a\n       %a\n.\n\n"
 187             out_uri u na.E.n_apix (entity_level a.E.e_side)
 188             (out_term st B.empty) w (out_term st B.empty) v;
 189          uris := (true, u) :: !uris; !ok
 190       | E.Abst (a, w)             ->
 191          KP.fprintf och "type %a @id.\n" out_uri u;
 192          KP.fprintf och "type c_%u ann.\n" na.E.n_apix;
 193          KP.fprintf och "type_g %a c_%u d_%s\n       %a\n.\n\n"
 194             out_uri u na.E.n_apix (entity_level a.E.e_side)
 195             (out_term st B.empty) w;
 196          uris := (false, u) :: !uris; !ok
 197       | _                         -> C.err ()
 198    else !ok
 199
 200 let close_out_lyp2 och () =
 201    let aux_name (b, s) =
 202       let gde = if b then "g_def" else "g_dec" in
 203       KP.fprintf och "(%s %a\n" gde out_uri s
 204    in
 205    let aux_sep _ = KP.fprintf och "%s" ")" in
 206    out_clause och "type grundlagen prop.";
 207    out_clause och "grundlagen :- valid_g";
 208    List.iter aux_name (List.rev !uris);
 209    KP.fprintf och "%s" "g_top";
 210    List.iter aux_sep !uris;
 211    out_clause och "\n\n.";
 212    close_out och
 213
 214 (* Interface functions ******************************************************)
 215
 216 let open_out_lyp2 fname =
 217    let dir = KF.concat !G.manager_dir base in
 218    let path = KF.concat dir fname in
 219    let och = open_out (path ^ "b_lyp" ^ ext_lp) in
 220    out_preamble och;
 221    out_comment och version;
 222    out_comment och affiliation;
 223    out_top_comment och description;
 224    output_entity_lyp2 och, close_out_lyp2 och
 225
 226 END