matita/components/ng_extraction/coq.ml

   1 type identifier = string
   2
   3 (* Util.ml *)
   4
   5 let is_digit c = (c >= '0' && c <= '9')
   6
   7 (* Nameops.ml *)
   8
   9 let has_subscript id =
  10   is_digit (id.[String.length id - 1])
  11
  12 let code_of_0 = Char.code '0'
  13 let code_of_9 = Char.code '9'
  14
  15 let cut_ident skip_quote s =
  16   let slen = String.length s in
  17   (* [n'] is the position of the first non nullary digit *)
  18   let rec numpart n n' =
  19     if n = 0 then
  20       (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *)
  21       slen
  22     else
  23       let c = Char.code (String.get s (n-1)) in
  24       if c = code_of_0 && n <> slen then
  25         numpart (n-1) n'
  26       else if code_of_0 <= c && c <= code_of_9 then
  27         numpart (n-1) (n-1)
  28       else if skip_quote && (c = Char.code '\'' || c = Char.code '_') then
  29         numpart (n-1) (n-1)
  30       else
  31         n'
  32   in
  33   numpart slen slen
  34
  35 let forget_subscript id =
  36   let numstart = cut_ident false id in
  37   let newid = Bytes.make (numstart+1) '0' in
  38   String.blit id 0 newid 0 numstart;
  39   Bytes.to_string newid
  40
  41 (* Namegen.ml *)
  42
  43 let restart_subscript id =
  44   if not (has_subscript id) then id else
  45     (* Ce serait sans doute mieux avec quelque chose inspiré de
  46      *** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
  47     forget_subscript id
  48
  49 (* Rem: semantics is a bit different, if an ident starts with toto00 then
  50   after successive renamings it comes to toto09, then it goes on with toto10 *)
  51 let lift_subscript id =
  52   let len = String.length id in
  53   let rec add carrypos =
  54     let c = id.[carrypos] in
  55     if is_digit c then
  56       if c = '9' then begin
  57         assert (carrypos>0);
  58         add (carrypos-1)
  59       end
  60       else begin
  61         let newid = Bytes.of_string id in
  62         Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
  63         Bytes.set newid  carrypos (Char.chr (Char.code c + 1));
  64         Bytes.to_string newid
  65       end
  66     else begin
  67       let newid = Bytes.of_string (id^"0") in
  68       if carrypos < len-1 then begin
  69         Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
  70         Bytes.set newid (carrypos+1) '1'
  71       end;
  72       Bytes.to_string newid
  73     end
  74   in add (len-1)
  75
  76 let next_ident_away_from id bad =
  77   let rec name_rec id = if bad id then name_rec (lift_subscript id) else id in
  78   name_rec id
  79
  80 let next_ident_away id avoid =
  81   if List.mem id avoid then
  82     next_ident_away_from (restart_subscript id) (fun id -> List.mem id avoid)
  83   else id
  84
  85 (* ----- *)
  86
  87 type label
  88 type reference
  89
  90 type env
  91 type constant_body
  92 type ('a,'b) prec_declaration
  93
  94 type module_path
  95 type mod_bound_id
  96
  97 module Intmap = Map.Make(struct type t = int let compare = compare end)
  98
  99 module Intset = Set.Make(struct type t = int let compare = compare end)
 100
 101 module Idset = Set.Make(struct type t = identifier let compare = compare end)
 102
 103 module Uriset = Set.Make(struct type t = NUri.uri let compare = NUri.compare end)
 104
 105 module Refmap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
 106
 107 module Stringmap = Map.Make(String)
 108
 109 (* Pp_control.ml *)
 110
 111 module Pp_control =
 112  struct
 113   let with_output_to _ = assert false
 114   let get_margin _ = assert false
 115  end
 116
 117 (* Util.ml *)
 118
 119 let list_map_i f =
 120   let rec map_i_rec i = function
 121     | [] -> []
 122     | x::l -> let v = f i x in v :: map_i_rec (i+1) l
 123   in
 124   map_i_rec
 125
 126 let list_map_i_status status f =
 127   let rec map_i_rec status i = function
 128     | [] -> status,[]
 129     | x::l -> let status,v = f status i x in
 130       let status,res = map_i_rec status (i+1) l in
 131        status,v :: res
 132   in
 133   map_i_rec status
 134
 135 let iterate f =
 136   let rec iterate_f n x =
 137     if n <= 0 then x else iterate_f (pred n) (f x)
 138   in
 139   iterate_f
 140
 141 let rec list_skipn n l = match n,l with
 142   | 0, _ -> l
 143   | _, [] -> failwith "list_skipn"
 144   | n, _::l -> list_skipn (pred n) l
 145
 146 let list_split_at index l =
 147   let rec aux i acc = function
 148       tl when i = index -> (List.rev acc), tl
 149     | hd :: tl -> aux (succ i) (hd :: acc) tl
 150     | [] -> failwith "list_split_at: Invalid argument"
 151   in aux 0 [] l
 152
 153 let list_chop n l =
 154   let rec chop_aux acc = function
 155     | (0, l2) -> (List.rev acc, l2)
 156     | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
 157     | (_, []) -> failwith "list_chop"
 158   in
 159   chop_aux [] (n,l)
 160
 161 let list_firstn n l =
 162   let rec aux acc = function
 163     | (0, _l) -> List.rev acc
 164     | (n, (h::t)) -> aux (h::acc) (pred n, t)
 165     | _ -> failwith "firstn"
 166   in
 167   aux [] (n,l)
 168
 169 let list_fold_left_i f =
 170   let rec it_list_f i a = function
 171     | [] -> a
 172     | b::l -> it_list_f (i+1) (f i a b) l
 173   in
 174   it_list_f
 175
 176 let list_iter_i f l = list_fold_left_i (fun i _ x -> f i x) 0 () l
 177
 178 let list_lastn n l =
 179   let len = List.length l in
 180   let rec aux m l =
 181     if m = n then l else aux (m - 1) (List.tl l)
 182   in
 183   if len < n then failwith "lastn" else aux len l
 184
 185 let array_map2 f v1 v2 =
 186   if Array.length v1 <> Array.length v2 then invalid_arg "array_map2";
 187   if Array.length v1 == 0 then
 188     [| |]
 189   else begin
 190     let res = Array.make (Array.length v1) (f v1.(0) v2.(0)) in
 191     for i = 1 to pred (Array.length v1) do
 192       res.(i) <- f v1.(i) v2.(i)
 193     done;
 194     res
 195   end
 196
 197 let array_for_all f v =
 198   let rec allrec = function
 199     | -1 -> true
 200     | n -> (f v.(n)) && (allrec (n-1))
 201   in
 202   allrec ((Array.length v)-1)
 203
 204 let array_fold_right_i f v a =
 205   let rec fold a n =
 206     if n=0 then a
 207     else
 208       let k = n-1 in
 209       fold (f k v.(k) a) k in
 210   fold a (Array.length v)
 211
 212 let identity x = x
 213
 214 let interval n m =
 215   let rec interval_n (l,m) =
 216     if n > m then l else interval_n (m::l,pred m)
 217   in
 218   interval_n ([],m)
 219
 220 let map_status status f l =
 221  List.fold_right
 222   (fun x (status,res)->let status,y = f status x in status,y::res) l (status,[])
 223
 224 (* CSC: Inefficiently implemented *)
 225 let array_map_status status f l =
 226  let status,res = map_status status f (Array.to_list l) in
 227   status,Array.of_list res
 228
 229 (* CSC: Inefficiently implemented *)
 230 let array_mapi_status status f l =
 231  let status,res = list_map_i_status status f 0 (Array.to_list l) in
 232   status,Array.of_list res
 233
 234 (* Pp.ml4 *)
 235
 236 type block_type =
 237   | Pp_hbox of int
 238   | Pp_vbox of int
 239   | Pp_hvbox of int
 240   | Pp_hovbox of int
 241   | Pp_tbox
 242
 243 type 'a ppcmd_token =
 244   | Ppcmd_print of 'a
 245   | Ppcmd_box of block_type * ('a ppcmd_token Stream.t)
 246   | Ppcmd_print_break of int * int
 247   | Ppcmd_set_tab
 248   | Ppcmd_print_tbreak of int * int
 249   | Ppcmd_white_space of int
 250   | Ppcmd_force_newline
 251   | Ppcmd_print_if_broken
 252   | Ppcmd_open_box of block_type
 253   | Ppcmd_close_box
 254   | Ppcmd_close_tbox
 255   | Ppcmd_comment of int
 256
 257 type ppcmd = (int*string) ppcmd_token
 258
 259 type std_ppcmds = ppcmd Stream.t
 260
 261 type 'a ppdir_token =
 262   | Ppdir_ppcmds of 'a ppcmd_token Stream.t
 263   | Ppdir_print_newline
 264   | Ppdir_print_flush
 265
 266 let utf8_length s =
 267   let len = String.length s
 268   and cnt = ref 0
 269   and nc = ref 0
 270   and p = ref 0 in
 271   while !p < len do
 272     begin
 273       match s.[!p] with
 274       | '\000'..'\127' -> nc := 0 (* ascii char *)
 275       | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *)
 276       | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *)
 277       | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *)
 278       | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *)
 279       | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *)
 280       | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *)
 281       | '\254'..'\255' -> nc := 0 (* invalid byte *)
 282     end ;
 283     incr p ;
 284     while !p < len && !nc > 0 do
 285       match s.[!p] with
 286       | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc
 287       | _ (* not a continuation byte *) -> nc := 0
 288     done ;
 289     incr cnt
 290   done ;
 291   !cnt
 292
 293 let (++) = Stream.iapp
 294 let str s = [< 'Ppcmd_print (utf8_length s,s) >]
 295 let spc () = [< 'Ppcmd_print_break (1,0) >]
 296 let mt () = [< >]
 297 let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >]
 298 let hv n s = [< 'Ppcmd_box(Pp_hvbox n,s) >]
 299 let hov n s = [< 'Ppcmd_box(Pp_hovbox n,s) >]
 300 let int n = str (string_of_int n)
 301 let stras (i,s) = [< 'Ppcmd_print (i,s) >]
 302 let fnl () = [< 'Ppcmd_force_newline >]
 303
 304 let com_eol = ref false
 305
 306 let com_brk _ft = com_eol := false
 307 let com_if ft f =
 308   if !com_eol then (com_eol := false; Format.pp_force_newline ft ())
 309   else Lazy.force f
 310
 311 let comments = ref []
 312
 313 let rec split_com comacc acc pos = function
 314     [] -> comments := List.rev acc; comacc
 315   | ((b,e),c as com)::coms ->
 316       (* Take all comments that terminates before pos, or begin exactly
 317          at pos (used to print comments attached after an expression) *)
 318       if e<=pos || pos=b then split_com (c::comacc) acc pos coms
 319       else  split_com comacc (com::acc) pos coms
 320
 321 let rec pr_com ft s =
 322   let (s1,os) =
 323     try
 324       let n = String.index s '\n' in
 325       String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1))
 326     with Not_found -> s,None in
 327   com_if ft (Lazy.from_val());
 328 (*  let s1 =
 329     if String.length s1 <> 0 && s1.[0] = ' ' then
 330       (Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1))
 331     else s1 in*)
 332   Format.pp_print_as ft (utf8_length s1) s1;
 333   match os with
 334       Some s2 ->
 335         if String.length s2 = 0 then (com_eol := true)
 336         else
 337           (Format.pp_force_newline ft (); pr_com ft s2)
 338     | None -> ()
 339
 340 let pp_dirs ft =
 341   let pp_open_box = function
 342     | Pp_hbox _n   -> Format.pp_open_hbox ft ()
 343     | Pp_vbox n   -> Format.pp_open_vbox ft n
 344     | Pp_hvbox n  -> Format.pp_open_hvbox ft n
 345     | Pp_hovbox n -> Format.pp_open_hovbox ft n
 346     | Pp_tbox     -> Format.pp_open_tbox ft ()
 347   in
 348   let rec pp_cmd = function
 349     | Ppcmd_print(n,s)        ->
 350         com_if ft (Lazy.from_val()); Format.pp_print_as ft n s
 351     | Ppcmd_box(bty,ss)       -> (* Prevent evaluation of the stream! *)
 352         com_if ft (Lazy.from_val());
 353         pp_open_box bty ;
 354         if not (Format.over_max_boxes ()) then Stream.iter pp_cmd ss;
 355         Format.pp_close_box ft ()
 356     | Ppcmd_open_box bty      -> com_if ft (Lazy.from_val()); pp_open_box bty
 357     | Ppcmd_close_box         -> Format.pp_close_box ft ()
 358     | Ppcmd_close_tbox        -> Format.pp_close_tbox ft ()
 359     | Ppcmd_white_space n     ->
 360         com_if ft (Lazy.from_fun (fun()->Format.pp_print_break ft n 0))
 361     | Ppcmd_print_break(m,n)  ->
 362         com_if ft (Lazy.from_fun(fun()->Format.pp_print_break ft m n))
 363     | Ppcmd_set_tab           -> Format.pp_set_tab ft ()
 364     | Ppcmd_print_tbreak(m,n) ->
 365         com_if ft (Lazy.from_fun(fun()->Format.pp_print_tbreak ft m n))
 366     | Ppcmd_force_newline     ->
 367         com_brk ft; Format.pp_force_newline ft ()
 368     | Ppcmd_print_if_broken   ->
 369         com_if ft (Lazy.from_fun(fun()->Format.pp_print_if_newline ft ()))
 370     | Ppcmd_comment i         ->
 371         let coms = split_com [] [] i !comments in
 372 (*        Format.pp_open_hvbox ft 0;*)
 373         List.iter (pr_com ft) coms(*;
 374         Format.pp_close_box ft ()*)
 375   in
 376   let pp_dir = function
 377     | Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream
 378     | Ppdir_print_newline    ->
 379         com_brk ft; Format.pp_print_newline ft ()
 380     | Ppdir_print_flush      -> Format.pp_print_flush ft ()
 381   in
 382   fun dirstream ->
 383     try
 384       Stream.iter pp_dir dirstream; com_brk ft
 385     with
 386       | e -> Format.pp_print_flush ft () ; raise e
 387
 388 let pp_with ft strm =
 389   pp_dirs ft [< 'Ppdir_ppcmds strm >]
 390
 391 (* Util.ml *)
 392
 393 let rec prlist_with_sep sep elem l = match l with
 394   | []   -> mt ()
 395   | [h]  -> elem h
 396   | h::t ->
 397       let e = elem h and s = sep() and r = prlist_with_sep sep elem t in
 398       e ++ s ++ r
 399
 400 let rec prlist_with_sep_status status sep elem l = match l with
 401   | []   -> status,mt ()
 402   | [h]  -> elem status h
 403   | h::t ->
 404       let status,e = elem status h in
 405       let s = sep() in
 406       let status,r = prlist_with_sep_status status sep elem t in
 407       status, e ++ s ++ r
 408
 409 let rec prlist elem l = match l with
 410   | []   -> mt ()
 411   | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
 412
 413 let rec prlist_strict elem l = match l with
 414   | []   -> mt ()
 415   | h::t ->
 416       let e = elem h in let r = prlist_strict elem t in e++r
 417
 418 let prvecti_with_sep sep elem v =
 419   let rec pr i =
 420     if i = 0 then
 421       elem 0 v.(0)
 422     else
 423       let r = pr (i-1) and s = sep () and e = elem i v.(i) in
 424       r ++ s ++ e
 425   in
 426   let n = Array.length v in
 427   if n = 0 then mt () else pr (n - 1)
 428
 429 let prvecti_with_sep_status status sep elem v =
 430   let rec pr status i =
 431     if i = 0 then
 432      elem status 0 v.(0)
 433     else
 434       let status,r = pr status (i-1) in
 435       let s = sep () in
 436       let status,e = elem status i v.(i) in
 437       status, r ++ s ++ e
 438   in
 439   let n = Array.length v in
 440   if n = 0 then status,mt () else pr status (n - 1)
 441
 442 let prvecti elem v = prvecti_with_sep mt elem v
 443
 444 let prvecti_status status elem v = prvecti_with_sep_status status mt elem v
 445
 446 let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
 447
 448 let prvect_with_sep_status status sep elem v =
 449  prvecti_with_sep_status status sep (fun status _ -> elem status) v
 450
 451 let prvect elem v = prvect_with_sep mt elem v
 452
 453 (* Nameops.ml *)
 454
 455 let pr_id id = str id
 456
 457 (* ---- *)