matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml

   1 module EL = RecommLib
   2 module ET = RecommTypes
   3
   4 let width = ref 78
   5
   6 let replace = ref false
   7
   8 let string_length_utf8 s =
   9   let l = String.length s in
  10   let rec aux r i =
  11     if i >= l then r else
  12     if '\x80' <= s.[i] && s.[i] <= '\xBF'
  13     then aux (succ r) (succ i) else aux r (succ i)
  14   in
  15   l - aux 0 0
  16
  17 let complete s n =
  18   let l = !width - string_length_utf8 s - 5 - n in
  19   if l < 0 then begin
  20     Printf.eprintf "overfull: %S\n" s;
  21     ""
  22   end else begin
  23     String.make l '*'
  24   end
  25
  26 let out_src och = function
  27   | ET.Line s                ->
  28     Printf.fprintf och "%s" s
  29   | ET.Text s                ->
  30     Printf.fprintf och "%s" s
  31   | ET.Mark s                ->
  32     Printf.fprintf och "(* *%s*)" s
  33   | ET.Key (s1, s2)          ->
  34     let s3 =
  35       if s1 = "NOTE" then complete (s1^s2) 0 else ""
  36     in
  37     Printf.fprintf och "(* %s%s%s*)" s1 s2 s3
  38   | ET.Title ss              ->
  39     let s = String.concat " " ss in
  40     Printf.fprintf och "(* %s %s*)" s (complete s 1)
  41   | ET.Slice ss              ->
  42     let s = String.capitalize_ascii (String.concat " " ss) in
  43     Printf.fprintf och "(* %s %s*)" s (complete s 1)
  44   | ET.Other (_, s1, s2, s3) ->
  45     Printf.fprintf och "%s%s%s" s1 s2 s3
  46
  47 let write_srcs file srcs =
  48   let target =
  49     if !replace then begin
  50       Sys.rename file (file ^ ".old");
  51       file
  52     end else begin
  53       file ^ ".new"
  54     end
  55   in
  56   let och = open_out target in
  57   List.iter (out_src och) srcs;
  58   close_out och
  59
  60 let write_subst och n s =
  61   Printf.fprintf och "%s %s\n" s n
  62
  63 let rec write_fst och = function
  64   | []                                                    -> ()
  65   | ET.Other (2, _, s, _) :: ET.Line _ :: ET.Text t :: tl ->
  66     write_snd och tl s (EL.split_on_char ' ' t)
  67   | ET.Other (2, _, s, _) :: tl                           ->
  68     Printf.eprintf "skipping fst: %S\n" s;
  69     write_fst och tl
  70   | _ :: tl                                  -> write_fst och tl
  71
  72 and write_snd och tl s = function
  73   | "definition" :: n :: _
  74   | "fact" :: n :: _
  75   | "lemma" :: n :: _
  76   | "inductive" :: n :: _
  77   | "theorem" :: n :: _     ->
  78     let ss = EL.split_on_char ' ' s in
  79     List.iter (write_subst och n) (List.tl ss);
  80     write_fst och tl
  81   | t :: _       ->
  82     Printf.eprintf "skipping snd: %S %S\n" s t;
  83     write_fst och tl
  84   | []             ->
  85     Printf.eprintf "skipping snd: %S\n" s;
  86     write_fst och tl
  87
  88 let write_substs = write_fst