matita/components/ng_extraction/common.ml

   1 (************************************************************************)
   2 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
   3 (* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
   4 (*   \VV/  **************************************************************)
   5 (*    //   *      This file is distributed under the terms of the       *)
   6 (*         *       GNU Lesser General Public License Version 2.1        *)
   7 (************************************************************************)
   8
   9 (*i $Id: common.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
  10
  11 open Coq
  12 open OcamlExtractionTable
  13 open Miniml
  14 open Mlutil
  15
  16 (*s Some pretty-print utility functions. *)
  17
  18 let pp_par par st = if par then str "(" ++ st ++ str ")" else st
  19
  20 let pp_apply st par args = match args with
  21   | [] -> st
  22   | _  -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
  23
  24 let pr_binding = function
  25   | [] -> mt ()
  26   | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
  27
  28 (** By default, in module Format, you can do horizontal placing of blocks
  29     even if they include newlines, as long as the number of chars in the
  30     blocks are less that a line length. To avoid this awkward situation,
  31     we attach a big virtual size to [fnl] newlines. *)
  32
  33 let fnl () = stras (1000000,"") ++ fnl ()
  34
  35 let fnl2 () = fnl () ++ fnl ()
  36
  37 let space_if = function true -> str " " | false -> mt ()
  38
  39 let is_invalid_id s =
  40  match s.[0] with 'a' .. 'z' | 'A' .. 'Z' -> false | _ -> true
  41
  42 let rec lowercase_id id =
  43  if id = "" then "x" else
  44  if id.[0] = '_' then lowercase_id (String.sub id 1 (String.length id - 1)) else
  45  if is_invalid_id id then lowercase_id ("x" ^ id) else
  46  String.uncapitalize id
  47
  48 let rec uppercase_id id =
  49  if id = "" then "T" else
  50  if id.[0] = '_' then uppercase_id (String.sub id 1 (String.length id - 1)) else
  51  if is_invalid_id id then uppercase_id ("x" ^ id) else
  52  String.capitalize id
  53
  54 type kind = Term | Type | Cons
  55
  56 let upperkind = function
  57   | Type
  58   | Term -> false
  59   | Cons -> true
  60
  61 let kindcase_id k id =
  62   if upperkind k then uppercase_id id else lowercase_id id
  63
  64 (*s de Bruijn environments for programs *)
  65
  66 type env = identifier list * Idset.t
  67
  68 (*s Generic renaming issues for local variable names. *)
  69
  70 let rec rename_id id avoid =
  71   if Idset.mem id avoid then rename_id (lift_subscript id) avoid else id
  72
  73 let rec rename_vars avoid = function
  74   | [] ->
  75       [], avoid
  76   | id :: idl when id == dummy_name ->
  77       (* we don't rename dummy binders *)
  78       let (idl', avoid') = rename_vars avoid idl in
  79       (id :: idl', avoid')
  80   | id :: idl ->
  81       let (idl, avoid) = rename_vars avoid idl in
  82       let id = rename_id (lowercase_id id) avoid in
  83       (id :: idl, Idset.add id avoid)
  84
  85 let rename_tvars avoid l =
  86   let rec rename avoid = function
  87     | [] -> [],avoid
  88     | id :: idl ->
  89         let id = rename_id (lowercase_id id) avoid in
  90         let idl, avoid = rename (Idset.add id avoid) idl in
  91         (id :: idl, avoid) in
  92   fst (rename avoid l)
  93
  94 let push_vars ids (db,avoid) =
  95   let ids',avoid' = rename_vars avoid ids in
  96   ids', (ids' @ db, avoid')
  97
  98 let get_db_name n (db,_) =
  99   let id = List.nth db (pred n) in
 100   if id = dummy_name then "__" else id
 101
 102 let empty_env status = [], get_global_ids status
 103
 104 let fake_spec = NReference.Fix (0,-1,-1)
 105
 106 let safe_name_of_reference status r =
 107  match r with
 108     NReference.Ref (uri, spec) when spec = fake_spec ->
 109      (* The field of a record *)
 110      NUri.name_of_uri uri
 111   | _ -> NCicPp.r2s status true r
 112
 113 let maybe_capitalize b n = if b then String.capitalize n else n
 114
 115 let modname_of_filename status capitalize name =
 116  try
 117   let name = modname_of_filename status name in
 118    status, maybe_capitalize capitalize name
 119  with Not_found ->
 120   let globs = Idset.elements (get_modnames status) in
 121   let s = next_ident_away (String.uncapitalize name) globs in
 122   let status = add_modname status s in
 123   let status = add_modname_for_filename status name s in
 124    status, maybe_capitalize capitalize s
 125
 126 let ref_renaming status (k,r) =
 127  let status,s =
 128   let rec ref_renaming status (k,r) =
 129    try status,name_of_reference status r
 130    with Not_found ->
 131    if is_projection status r then
 132     (* The reference for the projection and the field of a record are different
 133        and they would be assigned different names (name clash!). So we normalize
 134        the projection reference into the field reference *)
 135     let NReference.Ref (uri,_) = r in
 136     let fieldref = NReference.reference_of_spec uri fake_spec in
 137      ref_renaming status (k,fieldref)
 138    else
 139     let name = safe_name_of_reference status r in
 140     let globs = Idset.elements (get_global_ids status) in
 141     let s = next_ident_away (kindcase_id k name) globs in
 142     let status = add_global_ids status s in
 143     let status = add_name_for_reference status r s in
 144      status,s
 145   in
 146    ref_renaming status (k,r)
 147  in
 148   let baseuri = Filename.dirname (NReference.string_of_reference r) in
 149   if current_baseuri status = baseuri then
 150    status,s
 151   else
 152    let modname = Filename.basename (Filename.dirname (NReference.string_of_reference r)) in
 153    let status,modname = modname_of_filename status true modname in
 154     status, modname ^ "." ^ s
 155
 156 (* Main name printing function for a reference *)
 157
 158 let pp_global status k r = ref_renaming status (k,r)