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 space_if = function true -> str " " | false -> mt ()
  36
  37 let is_invalid_id s =
  38  match s.[0] with 'a' .. 'z' | 'A' .. 'Z' -> false | _ -> true
  39
  40 let rec lowercase_id id =
  41  if id = "" then "x" else
  42  if id.[0] = '_' then lowercase_id (String.sub id 1 (String.length id - 1)) else
  43  if is_invalid_id id then lowercase_id ("x" ^ id) else
  44  String.uncapitalize_ascii id
  45
  46 let rec uppercase_id id =
  47  if id = "" then "T" else
  48  if id.[0] = '_' then uppercase_id (String.sub id 1 (String.length id - 1)) else
  49  if is_invalid_id id then uppercase_id ("x" ^ id) else
  50  String.capitalize_ascii id
  51
  52 type kind = Term | Type | Cons
  53
  54 let upperkind = function
  55   | Type
  56   | Term -> false
  57   | Cons -> true
  58
  59 let kindcase_id k id =
  60   if upperkind k then uppercase_id id else lowercase_id id
  61
  62 (*s de Bruijn environments for programs *)
  63
  64 type env = identifier list * Idset.t
  65
  66 (*s Generic renaming issues for local variable names. *)
  67
  68 let rec rename_id id avoid =
  69   if Idset.mem id avoid then rename_id (lift_subscript id) avoid else id
  70
  71 let rec rename_vars avoid = function
  72   | [] ->
  73       [], avoid
  74   | id :: idl when id == dummy_name ->
  75       (* we don't rename dummy binders *)
  76       let (idl', avoid') = rename_vars avoid idl in
  77       (id :: idl', avoid')
  78   | id :: idl ->
  79       let (idl, avoid) = rename_vars avoid idl in
  80       let id = rename_id (lowercase_id id) avoid in
  81       (id :: idl, Idset.add id avoid)
  82
  83 let rename_tvars avoid l =
  84   let rec rename avoid = function
  85     | [] -> [],avoid
  86     | id :: idl ->
  87         let id = rename_id (lowercase_id id) avoid in
  88         let idl, avoid = rename (Idset.add id avoid) idl in
  89         (id :: idl, avoid) in
  90   fst (rename avoid l)
  91
  92 let push_vars ids (db,avoid) =
  93   let ids',avoid' = rename_vars avoid ids in
  94   ids', (ids' @ db, avoid')
  95
  96 let get_db_name n (db,_) =
  97   let id = List.nth db (pred n) in
  98   if id = dummy_name then "__" else id
  99
 100 let empty_env status = [], get_global_ids status
 101
 102 let fake_spec = NReference.Fix (0,-1,-1)
 103
 104 let safe_name_of_reference status r =
 105  match r with
 106     NReference.Ref (uri, spec) when spec = fake_spec ->
 107      (* The field of a record *)
 108      NUri.name_of_uri uri
 109   | _ -> NCicPp.r2s status true r
 110
 111 let maybe_capitalize b n = if b then String.capitalize_ascii n else n
 112
 113 let modname_of_filename status capitalize name =
 114  try
 115   let name = modname_of_filename status name in
 116    status, maybe_capitalize capitalize name
 117  with Not_found ->
 118   let globs = Idset.elements (get_modnames status) in
 119   let s = next_ident_away (String.uncapitalize_ascii name) globs in
 120   let status = add_modname status s in
 121   let status = add_modname_for_filename status name s in
 122    status, maybe_capitalize capitalize s
 123
 124 let ref_renaming status (k,r) =
 125  let status,s =
 126   let rec ref_renaming status (k,r) =
 127    try status,name_of_reference status r
 128    with Not_found ->
 129    if is_projection status r then
 130     (* The reference for the projection and the field of a record are different
 131        and they would be assigned different names (name clash!). So we normalize
 132        the projection reference into the field reference *)
 133     let NReference.Ref (uri,_) = r in
 134     let fieldref = NReference.reference_of_spec uri fake_spec in
 135      ref_renaming status (k,fieldref)
 136    else
 137     let name = safe_name_of_reference status r in
 138     let globs = Idset.elements (get_global_ids status) in
 139     let s = next_ident_away (kindcase_id k name) globs in
 140     let status = add_global_ids status s in
 141     let status = add_name_for_reference status r s in
 142      status,s
 143   in
 144    ref_renaming status (k,r)
 145  in
 146   let baseuri = Filename.dirname (NReference.string_of_reference r) in
 147   if current_baseuri status = baseuri then
 148    status,s
 149   else
 150    let modname = Filename.basename (Filename.dirname (NReference.string_of_reference r)) in
 151    let status,modname = modname_of_filename status true modname in
 152     status, modname ^ "." ^ s
 153
 154 (* Main name printing function for a reference *)
 155
 156 let pp_global status k r = ref_renaming status (k,r)