Quelle coq_module.ml Sprache: SML

(************************************************************************)
(* This file is licensed under The MIT License                          *)
(* See LICENSE for more information                                     *)
(* (c) MINES ParisTech 2018-2019                                        *)
(* (c) INRIA 2020-2022                                                  *)
(* Written by: Emilio Jesús Gallego Arias                               *)
(* Written by: Rudi Grinberg                                            *)
(************************************************************************)

let with_timing = true

type t =
  { source : Path.t
  ; prefix : string list
  ; name : string
  }

let pp fmt { source; prefix; name } =
  Format.fprintf fmt "@[{%s : %a}@]" (String.concat "." (prefix@[name]) ) Path.pp source

let make ~source ~prefix ~name = { source; prefix; name }
let source { source; _ } = source
let prefix { prefix; _ } = prefix

let mod_to_obj ~ext { name; _ } = name ^ ext

module Rule_type = struct

  type native = Disabled | Coqc | CoqNative
  type t =
    | Regular of { native : native }

  let native_coqc = function
    | Regular { native = Coqc } -> true
    | Regular { native = CoqNative }
    | Regular { native = Disabled } -> false

end

let native_obj_files ~install ~tname { prefix; name; _ } =
  let base_theory = tname in
  let native_base = "N" ^ String.concat "_" (base_theory @ prefix @ [name]) in
  let prefix file = if install then Filename.concat ".coq-native" file else file in
  [ prefix @@ native_base ^ ".cmi"; prefix @@ native_base ^ ".cmxs" ]

let base_obj_files coq_module =
  [ mod_to_obj coq_module ~ext:".glob"
  ; mod_to_obj coq_module ~ext:".vos"
  ; mod_to_obj coq_module ~ext:".vo"
  ]

let obj_files ~tname ~rule coq_module =
  let native = Rule_type.native_coqc rule in
  let native_objs = if native then native_obj_files ~tname ~install:false coq_module else [] in
  let timing_objs = if with_timing then [ mod_to_obj coq_module ~ext:".timing" ] else [] in
  timing_objs @ native_objs @ base_obj_files coq_module

let prefix_to_dir = String.concat Filename.dir_sep

let native_install_files ~tname ~rule coq_module =
  match rule with
  | Rule_type.Regular { native = CoqNative }
  | Regular { native = Coqc } ->
    native_obj_files ~tname ~install:false coq_module
  , native_obj_files ~tname ~install:true coq_module
  | Regular { native = Disabled } -> [], []

(* quick/vio woes... it does produce a different set of targets than
   regular compilation *)
let base_install_files coq_module =
  mod_to_obj coq_module ~ext:".v" :: base_obj_files coq_module

let install_files ~tname ~rule coq_module =
  let src_base = base_install_files coq_module in
  let src_native, dst_native = native_install_files ~tname ~rule coq_module in
  let src = src_base @ src_native in
  let ppath = prefix_to_dir (prefix coq_module) in
  let dst = List.map (Filename.concat ppath) (src_base @ dst_native) in
  List.combine src dst

let native_obj_files = native_obj_files ~install:false

quality100%

¤ Dauer der Verarbeitung: 0.34 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.