Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Namesopen Declarationsopen Mod_declarationsopen Modopsopen Nativecode
(** This file implements separate compilation for libraries in the nativecompiler *)
let rec translate_mod mp cenv env mod_expr acc = match mod_expr with | NoFunctor struc -> List.fold_left (translate_field mp cenv env) acc struc | MoreFunctor _ -> acc
(* XXX I believe it makes no sense to extract module types *)and translate_modtype mp cenv env mod_expr reso acc = match mod_expr with | NoFunctor struc -> let env' = add_structure mp struc reso env in List.fold_left (translate_field mp cenv env') acc struc | MoreFunctor _ -> acc
and translate_field mp cenv env acc (l,x) = match x with | SFBconst cb -> let con = Constant.make2 mp l in (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in Pp.str msg)); compile_constant_field cenv env con acc cb | SFBmind mb -> (debug_native_compiler (fun () -> let id = mb.mind_packets.(0).mind_typename in let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in Pp.str msg)); compile_mind_field cenv mp l acc mb | SFBrules rrb -> (debug_native_compiler (fun () -> let msg = Printf.sprintf "Not Compiling rules %s..." (Id.to_string l) in Pp.str msg)); compile_rewrite_rules env l acc rrb | SFBmodule md -> let mp = MPdot (mp, l) in (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling module %s..." (ModPath.to_string mp) in Pp.str msg)); translate_mod mp cenv env (mod_type md) acc | SFBmodtype mdtyp -> let mp = MPdot (mp, l) in (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp) in Pp.str msg)); translate_modtype mp cenv env (mod_type mdtyp) (mod_delta mdtyp) acc
(* This function expects the contents of the module to be part of [env] already *)let dump_library mp env mod_expr = debug_native_compiler (fun () -> Pp.str "Compiling library..."); match mod_expr with | NoFunctor struc -> let t0 = Sys.time () in let cenv = Nativecode.make_cenv () in let mlcode = List.fold_left (translate_field mp cenv env) [] struc in let t1 = Sys.time () in let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in let mlcode = add_header_comment (List.rev mlcode) time_info in let symbols = Nativecode.get_cenv_symbols cenv in mlcode, symbols | _ -> assert false