matita/components/ng_extraction/ocamlExtractionTable.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: table.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
  10
  11 open Coq
  12 open Miniml
  13
  14 type info_el =
  15    TypeInfo of NReference.reference * ml_schema
  16  | TermInfo of NReference.reference * ml_decl
  17  | InductiveInfo of NUri.uri * ml_ind
  18  | GuessProjectionInfo of NUri.uri * int
  19  | ConfirmProjectionInfo of NReference.reference
  20  | RegisterId of string
  21  | ReferenceNameInfo of NReference.reference * string
  22  | RegisterModname of string
  23  | ModnameInfo of string * string
  24
  25 type info = info_el list
  26
  27 type db =
  28  ml_schema Refmap.t *
  29  ml_decl Refmap.t *
  30  ml_ind NUri.UriMap.t *
  31  int NUri.UriMap.t *
  32  int Refmap.t *
  33  Idset.t *
  34  string Refmap.t *
  35  ((out_channel * Format.formatter) * (out_channel * Format.formatter)) option *
  36  Idset.t *
  37  string Stringmap.t *
  38  Uriset.t *
  39  string *
  40  info
  41
  42 let set_keywords,get_keywords =
  43  let keywords = ref Idset.empty in
  44   ((:=) keywords),(fun () -> !keywords)
  45
  46 let preamble = "preamble.ml"
  47 let upreamble = "Preamble"
  48 let empty_info = []
  49 let empty_modset = Idset.add preamble Idset.empty
  50 let empty_db () =
  51  Refmap.empty,Refmap.empty,NUri.UriMap.empty,NUri.UriMap.empty,Refmap.empty,get_keywords (),Refmap.empty,None,empty_modset,Stringmap.empty,Uriset.empty,"",empty_info
  52
  53 let register_info (dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos) info =
  54  match info with
  55     TypeInfo (ref,schema) ->
  56      Refmap.add ref schema dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
  57   | TermInfo (ref,schema) ->
  58      dbty,Refmap.add ref schema dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
  59   | InductiveInfo (uri,ind) ->
  60      dbty,dbt,NUri.UriMap.add uri ind dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
  61   | GuessProjectionInfo (uri,n) ->
  62      dbty,dbt,dbi,NUri.UriMap.add uri n dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
  63   | ConfirmProjectionInfo (NReference.Ref (uri,_) as ref) ->
  64      (try
  65        let n = NUri.UriMap.find uri dbgp in
  66        let dbgp = NUri.UriMap.remove uri dbgp in
  67         dbty,dbt,dbi,dbgp,Refmap.add ref n dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
  68       with Not_found -> dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos)
  69   | RegisterId s ->
  70      dbty,dbt,dbi,dbgp,dbp,Idset.add s dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
  71   | ReferenceNameInfo (ref,name) ->
  72      dbty,dbt,dbi,dbgp,dbp,dbids,Refmap.add ref name dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
  73   | RegisterModname s ->
  74      dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,Idset.add s dbmn1,dbmn2,dbo,curi,infos
  75   | ModnameInfo (s,name) ->
  76      dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,Stringmap.add s name dbmn2,dbo,curi,infos
  77
  78 let add_info_to_db (dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos) info =
  79  dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,info::infos
  80
  81 let register_and_add_info ?(dummy=false) status info =
  82  let db = status#ocaml_extraction_db in
  83  let db = register_info db info in
  84  let db = if dummy then db else add_info_to_db db info in
  85   status#set_ocaml_extraction_db db
  86
  87 let register_infos = List.fold_left register_info
  88
  89 let refresh_uri_in_type ~refresh_uri_in_reference =
  90  let rec aux =
  91   function
  92    | Tarr (t1,t2) -> Tarr (aux t1, aux t2)
  93    | Tglob (r,tl) -> Tglob (refresh_uri_in_reference r, List.map aux tl)
  94    | Tmeta { id=id; contents=contents } ->
  95       let contents' =
  96        match contents with
  97           None -> None
  98         | Some typ -> Some (aux typ)
  99        in
 100         Tmeta { id=id; contents=contents' }
 101    | t -> t
 102  in
 103   aux
 104
 105 let refresh_uri_in_kind ~refresh_uri_in_reference =
 106  function
 107     Singleton
 108   | Coinductive
 109   | Standard as k -> k
 110   | Record rl -> Record (List.map refresh_uri_in_reference rl)
 111
 112 let refresh_uri_in_packet ~refresh_uri_in_reference
 113  { ip_reference = r;
 114    ip_consreferences = rs;
 115    ip_typename = n;
 116    ip_consnames = ns;
 117    ip_logical = l;
 118    ip_sign = s;
 119    ip_vars = v;
 120    ip_types = tys } =
 121  { ip_reference = refresh_uri_in_reference r;
 122    ip_consreferences = Array.map refresh_uri_in_reference rs;
 123    ip_typename = n;
 124    ip_consnames = ns;
 125    ip_logical = l;
 126    ip_sign = s;
 127    ip_vars = v;
 128    ip_types = Array.map (List.map (refresh_uri_in_type ~refresh_uri_in_reference)) tys }
 129
 130 let refresh_uri_in_ind ~refresh_uri_in_reference
 131  {ind_kind=k; ind_nparams=n; ind_packets=pa}
 132 =
 133  let k = refresh_uri_in_kind ~refresh_uri_in_reference k in
 134  let pa = Array.map (refresh_uri_in_packet ~refresh_uri_in_reference) pa in
 135  {ind_kind=k; ind_nparams=n; ind_packets=pa}
 136
 137 let refresh_uri_in_ast ~refresh_uri_in_reference =
 138  let rec aux =
 139   function
 140    | MLapp (t,tl) -> MLapp (aux t, List.map aux tl)
 141    | MLlam (id,t) -> MLlam (id, aux t)
 142    | MLletin (id,t1,t2) -> MLletin (id, aux t1, aux t2)
 143    | MLglob r -> MLglob (refresh_uri_in_reference r)
 144    | MLcons ({c_kind=ckind; c_typs=ctyps}, r, tl) ->
 145       let cinfo =
 146        {c_kind=refresh_uri_in_kind ~refresh_uri_in_reference ckind;
 147         c_typs=List.map (refresh_uri_in_type ~refresh_uri_in_reference) ctyps}
 148       in
 149        MLcons (cinfo, refresh_uri_in_reference r, List.map aux tl)
 150    | MLcase ({m_kind=k; m_typs=typs; m_same=same},t,ba) ->
 151       let info =
 152        {m_kind=refresh_uri_in_kind ~refresh_uri_in_reference k;
 153         m_typs=List.map (refresh_uri_in_type ~refresh_uri_in_reference) typs;
 154         m_same=same} in
 155       let ba =
 156        Array.map
 157         (fun (r,il,t) -> refresh_uri_in_reference r,il,aux t) ba in
 158       MLcase (info,aux t,ba)
 159    | MLfix (n,ida,ta) -> MLfix (n,ida,Array.map aux ta)
 160    | MLmagic t -> MLmagic (aux t)
 161    | MLrel _
 162    | MLexn _
 163    | MLdummy
 164    | MLaxiom as t -> t
 165  in
 166   aux
 167
 168 let refresh_uri_in_decl ~refresh_uri_in_reference =
 169  function
 170     Dind ind -> Dind (refresh_uri_in_ind ~refresh_uri_in_reference ind)
 171   | Dtype (ref,il,ty) ->
 172      Dtype
 173       (refresh_uri_in_reference ref, il,
 174        refresh_uri_in_type ~refresh_uri_in_reference ty)
 175   | Dterm (ref,ast,ty) ->
 176      Dterm
 177       (refresh_uri_in_reference ref,
 178        refresh_uri_in_ast ~refresh_uri_in_reference ast,
 179        refresh_uri_in_type ~refresh_uri_in_reference ty)
 180   | Dfix (refa, asta, tya) ->
 181      Dfix
 182       (Array.map refresh_uri_in_reference refa,
 183        Array.map (refresh_uri_in_ast ~refresh_uri_in_reference) asta,
 184        Array.map (refresh_uri_in_type ~refresh_uri_in_reference) tya)
 185
 186 let refresh_uri_in_info_el ~refresh_uri_in_reference ~refresh_uri =
 187  function
 188     TypeInfo (ref,(n,typ)) ->
 189      TypeInfo
 190       (refresh_uri_in_reference ref,
 191        (n,refresh_uri_in_type ~refresh_uri_in_reference typ))
 192   | TermInfo (ref,decl) ->
 193      TermInfo
 194       (refresh_uri_in_reference ref,
 195        refresh_uri_in_decl ~refresh_uri_in_reference decl)
 196   | InductiveInfo (uri,ind) ->
 197      InductiveInfo
 198       (refresh_uri uri, refresh_uri_in_ind ~refresh_uri_in_reference ind)
 199   | GuessProjectionInfo (uri,n) ->
 200      GuessProjectionInfo (refresh_uri uri, n)
 201   | ConfirmProjectionInfo ref ->
 202      ConfirmProjectionInfo (refresh_uri_in_reference ref)
 203   | RegisterId s -> RegisterId s
 204   | ReferenceNameInfo (ref,name) ->
 205      ReferenceNameInfo (refresh_uri_in_reference ref,name)
 206   | RegisterModname s -> RegisterModname s
 207   | ModnameInfo (s,name) -> ModnameInfo (s,name)
 208
 209 let refresh_uri_in_info ~refresh_uri_in_reference ~refresh_uri infos =
 210  List.map
 211   (refresh_uri_in_info_el ~refresh_uri_in_reference ~refresh_uri)
 212   infos
 213
 214 class type g_status =
 215  object ('self)
 216   method ocaml_extraction_db: db
 217   method get_info: info * 'self
 218  end
 219
 220 class virtual status =
 221  object (self)
 222   inherit NCic.status
 223   val ocaml_extraction_db = empty_db ()
 224   method ocaml_extraction_db = ocaml_extraction_db
 225   method get_info =
 226    let db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos = self#ocaml_extraction_db in
 227     infos,{< ocaml_extraction_db =
 228               db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,empty_info >}
 229   method set_ocaml_extraction_db v = {< ocaml_extraction_db = v >}
 230   method set_ocaml_extraction_status
 231    : 'status. #g_status as 'status -> 'self
 232    = fun o -> {< ocaml_extraction_db = o#ocaml_extraction_db >}
 233  end
 234
 235 let open_file status ~baseuri filename =
 236  let db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,_,infos = status#ocaml_extraction_db in
 237  assert (ch=None);
 238  let chml = open_out filename in
 239  let chml = chml,Format.formatter_of_out_channel chml in
 240  let chmli = open_out (filename ^ "i") in
 241  let chmli = chmli,Format.formatter_of_out_channel chmli in
 242  pp_with (snd chml) (str ("open " ^ upreamble ^ "\n") ++ fnl ());
 243  pp_with (snd chmli) (str ("open " ^ upreamble ^ "\n") ++ fnl ());
 244  let db = db1,db2,dbi,dbgp,dbp,dbids,dbrefs,Some (chml,chmli),dbmn1,dbmn2,dbo,baseuri,infos in
 245  status#set_ocaml_extraction_db db
 246
 247 let close_file status =
 248  let db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos = status#ocaml_extraction_db in
 249  match ch with
 250     None -> assert false
 251   | Some ch ->
 252      Format.pp_print_flush (snd (fst ch)) ();
 253      Format.pp_print_flush (snd (snd ch)) ();
 254      close_out (fst (fst ch));
 255      close_out (fst (snd ch));
 256      let ch = None in
 257      let db = db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos in
 258      status#set_ocaml_extraction_db db
 259
 260 let print_ppcmds status ~in_ml cmds =
 261  let _,_,_,_,_,_,_,ch,_,_,_,_,_ = status#ocaml_extraction_db in
 262  match ch with
 263     None -> assert false
 264   | Some ch ->
 265      let ch = if in_ml then fst ch else snd ch in
 266      pp_with (snd ch) cmds
 267
 268 let to_be_included status uri =
 269  let dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos =
 270   status#ocaml_extraction_db
 271  in
 272   if Uriset.mem uri dbo then
 273    status,false
 274   else
 275    let dbo = Uriset.add uri dbo in
 276    let status =
 277     status#set_ocaml_extraction_db
 278      (dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos) in
 279    status,true
 280
 281 let add_term status ref decl =
 282  let info = TermInfo (ref,decl) in
 283   register_and_add_info status info
 284
 285 let lookup_term status ref =
 286  let _,dbt,_,_,_,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
 287   Refmap.find ref dbt
 288
 289 let add_type status ref schema =
 290  let info = TypeInfo (ref,schema) in
 291   register_and_add_info status info
 292
 293 let lookup_type status ref =
 294  let dbty,_,_,_,_,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
 295   Refmap.find ref dbty
 296
 297 let add_name_for_reference status ref name =
 298  let info = ReferenceNameInfo (ref,name) in
 299   register_and_add_info status info
 300
 301 let name_of_reference status ref =
 302  let _,_,_,_,_,_,dbrefs,_,_,_,_,_,_ = status#ocaml_extraction_db in
 303   Refmap.find ref dbrefs
 304
 305 let add_modname_for_filename status ref name =
 306  let info = ModnameInfo (ref,name) in
 307   register_and_add_info status info
 308
 309 let modname_of_filename status ref =
 310  let _,_,_,_,_,_,_,_,_,dbmn2,_,_,_ = status#ocaml_extraction_db in
 311   Stringmap.find ref dbmn2
 312
 313 let add_global_ids status id =
 314  let info = RegisterId id in
 315   register_and_add_info status info
 316
 317 let get_global_ids status =
 318  let _,_,_,_,_,dbids,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
 319   dbids
 320
 321 let add_modname status id =
 322  let info = RegisterModname id in
 323   register_and_add_info status info
 324
 325 let get_modnames status =
 326  let _,_,_,_,_,_,_,_,dbmn1,_,_,_,_ = status#ocaml_extraction_db in
 327   dbmn1
 328
 329 let add_ind status ?dummy uri ind =
 330  let info = InductiveInfo (uri,ind) in
 331   register_and_add_info ?dummy status info
 332
 333 let lookup_ind status uri =
 334  let _,_,dbi,_,_,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
 335   NUri.UriMap.find uri dbi
 336
 337 let current_baseuri status =
 338  let _,_,_,_,_,_,_,_,_,_,_,suri,_ = status#ocaml_extraction_db in suri
 339
 340 let guess_projection status ref n =
 341  let info = GuessProjectionInfo (ref,n) in
 342   register_and_add_info status info
 343
 344 let confirm_projection status ref =
 345  let info = ConfirmProjectionInfo ref in
 346   register_and_add_info status info
 347
 348 let is_projection status ref =
 349  let _,_,_,_,dbp,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
 350   Refmap.mem ref dbp
 351
 352 let projection_arity status ref =
 353  let _,_,_,_,dbp,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
 354   Refmap.find ref dbp
 355
 356 let type_expand () = true
 357
 358 (*s Extraction Optimize *)
 359
 360 type opt_flag =
 361     { opt_kill_dum : bool; (* 1 *)
 362       opt_fix_fun : bool;   (* 2 *)
 363       opt_case_iot : bool;  (* 4 *)
 364       opt_case_idr : bool;  (* 8 *)
 365       opt_case_idg : bool;  (* 16 *)
 366       opt_case_cst : bool;  (* 32 *)
 367       opt_case_fun : bool;  (* 64 *)
 368       opt_case_app : bool;  (* 128 *)
 369       opt_let_app : bool;   (* 256 *)
 370       opt_lin_let : bool;   (* 512 *)
 371       opt_lin_beta : bool } (* 1024 *)
 372
 373 let kth_digit n k = (n land (1 lsl k) <> 0)
 374
 375 let flag_of_int n =
 376     { opt_kill_dum = kth_digit n 0;
 377       opt_fix_fun = kth_digit n 1;
 378       opt_case_iot = kth_digit n 2;
 379       opt_case_idr = kth_digit n 3;
 380       opt_case_idg = kth_digit n 4;
 381       opt_case_cst = kth_digit n 5;
 382       opt_case_fun = kth_digit n 6;
 383       opt_case_app = kth_digit n 7;
 384       opt_let_app = kth_digit n 8;
 385       opt_lin_let = kth_digit n 9;
 386       opt_lin_beta = kth_digit n 10 }
 387
 388 (* For the moment, we allow by default everything except :
 389    - the type-unsafe optimization [opt_case_idg], which anyway
 390      cannot be activated currently (cf [Mlutil.branch_as_fun])
 391    - the linear let and beta reduction [opt_lin_let] and [opt_lin_beta]
 392      (may lead to complexity blow-up, subsumed by finer reductions
 393       when inlining recursors).
 394 *)
 395
 396 let int_flag_init = 1 + 2 + 4 + 8 (*+ 16*) + 32 + 64 + 128 + 256 (*+ 512 + 1024*)
 397
 398 let opt_flag_ref = ref (flag_of_int int_flag_init)
 399
 400 let optims () = !opt_flag_ref