Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[coq] Introduce Coq_scope #3280

Closed
wants to merge 1 commit into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion src/dune/coq_rules.ml
Original file line number Diff line number Diff line change
Expand Up @@ -240,8 +240,9 @@ let setup_rules ~sctx ~build_dir ~dir ~dir_contents (s : Dune_file.Coq.t) =
let cc = create_ccoq sctx ~dir in
let name = snd s.name in
let scope = SC.find_scope_by_dir sctx dir in
let coq_scope = SC.find_coq_scope_by_dir sctx dir in
let lib_db = Scope.libs scope in
let coq_lib_db = Scope.coq_libs scope in
let coq_lib_db = Coq_scope.libs coq_scope in
let expander = SC.expander sctx ~dir in

let theory = Coq_lib.DB.resolve coq_lib_db s.name |> Result.ok_exn in
Expand Down
59 changes: 59 additions & 0 deletions src/dune/coq_scope.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
(* This file is licensed under The MIT License *)
(* (c) MINES ParisTech 2019 *)
(* (c) INRIA 2020 *)
(* Written by: Emilio Jesús Gallego Arias *)

open! Stdune

type t = { db : Coq_lib.DB.t }

let libs { db; _ } = db

module DB = struct
type scope = t

type t =
{ by_dir : scope Path.Source.Map.t
; context : Context_name.t
}

let find_by_dir t (dir : Path.Source.t) =
let rec loop d =
match Path.Source.Map.find t.by_dir d with
| Some s -> s
| None -> (
match Path.Source.parent d with
| Some d -> loop d
| None ->
Code_error.raise "find_by_dir: invalid directory"
[ ("d", Path.Source.to_dyn d); ("dir", Path.Source.to_dyn dir) ] )
in
loop dir

let find_by_project t project =
Path.Source.Map.find_exn t.by_dir (Dune_project.root project)

let scopes_by_dir stanzas =
let stanzas_by_project_dir =
List.map stanzas
~f:(fun ((dir, stanza) : Path.Build.t * Dune_file.Coq.t) ->
let project = stanza.project in
(Dune_project.root project, (dir, stanza)))
|> Path.Source.Map.of_list_multi
in
Path.Source.Map.map stanzas_by_project_dir ~f:(fun stanza ->
let db = Coq_lib.DB.create_from_coqlib_stanzas stanza in
{ db })

let create ~context stanzas =
let by_dir = scopes_by_dir stanzas in
{ by_dir; context }

let find_by_dir t dir =
if Path.Build.is_root dir then
Code_error.raise "Scope.DB.find_by_dir got an invalid path"
[ ("dir", Path.Build.to_dyn dir)
; ("context", Context_name.to_dyn t.context)
];
find_by_dir t (Path.Build.drop_build_context_exn dir)
end
25 changes: 25 additions & 0 deletions src/dune/coq_scope.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
(* This file is licensed under The MIT License *)
(* (c) MINES ParisTech 2019 *)
(* (c) INRIA 2020 *)
(* Written by: Emilio Jesús Gallego Arias *)

open! Stdune

type t

(** Return the library database associated to this scope *)
val libs : t -> Coq_lib.DB.t

module DB : sig
type scope = t

type t

val create :
context:Context_name.t -> (Path.Build.t * Dune_file.Coq.t) list -> t

val find_by_dir : t -> Path.Build.t -> scope

val find_by_project : t -> Dune_project.t -> scope
end
with type scope := t
9 changes: 2 additions & 7 deletions src/dune/lib.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1683,7 +1683,6 @@ module DB = struct
| Library of Path.Build.t * Dune_file.Library.t
| External_variant of Dune_file.External_variant.t
| Deprecated_library_name of Dune_file.Deprecated_library_name.t
| Coq_theory of Path.Build.t * Dune_file.Coq.t
end

module Found_or_redirect = struct
Expand All @@ -1697,8 +1696,7 @@ module DB = struct
List.iter stanzas ~f:(fun (stanza : Library_related_stanza.t) ->
match stanza with
| Library _
| Deprecated_library_name _
| Coq_theory _ ->
| Deprecated_library_name _ ->
()
| External_variant ev -> (
let loc, virtual_lib = ev.virtual_lib in
Expand Down Expand Up @@ -1816,10 +1814,7 @@ module DB = struct
else
[ (name, Found info)
; (Lib_name.of_local conf.name, Redirect p.name)
] )
| Coq_theory _ ->
(* As of today Coq theories do live in a separate namespace *)
[])
] ))
|> Lib_name.Map.of_list_reducei
~f:(fun name (v1 : Found_or_redirect.t) v2 ->
let res =
Expand Down
1 change: 0 additions & 1 deletion src/dune/lib.mli
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,6 @@ module DB : sig
| Library of Path.Build.t * Dune_file.Library.t
| External_variant of Dune_file.External_variant.t
| Deprecated_library_name of Dune_file.Deprecated_library_name.t
| Coq_theory of Path.Build.t * Dune_file.Coq.t
end

(** Create a database from a list of library/variants stanzas *)
Expand Down
18 changes: 2 additions & 16 deletions src/dune/scope.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ open Import
type t =
{ project : Dune_project.t
; db : Lib.DB.t
; coq_db : Coq_lib.DB.t
; root : Path.Build.t
}

Expand All @@ -16,8 +15,6 @@ let project t = t.project

let libs t = t.db

let coq_libs t = t.coq_db

module DB = struct
type scope = t

Expand Down Expand Up @@ -71,11 +68,7 @@ module DB = struct
; _
} ->
Some
(Dune_file.Public_lib.name old_public_name, Name new_public_name)
| Coq_theory _ ->
(* All libraries in Coq are private to a scope for now, we will lift
this restriction soon *)
None)
(Dune_file.Public_lib.name old_public_name, Name new_public_name))
|> Lib_name.Map.of_list
|> function
| Ok x -> x
Expand Down Expand Up @@ -119,7 +112,6 @@ module DB = struct
| Library (_, lib) -> lib.project
| External_variant ev -> ev.project
| Deprecated_library_name x -> x.project
| Coq_theory (_, thr) -> thr.project
in
(Dune_project.root project, stanza))
|> Path.Source.Map.of_list_multi
Expand All @@ -131,16 +123,10 @@ module DB = struct
let db =
Lib.DB.create_from_stanzas stanzas ~parent:public_libs ~lib_config
in
let coq_stanzas =
List.filter_map stanzas ~f:(function
| Coq_theory (p, l) -> Some (p, l)
| _ -> None)
in
let coq_db = Coq_lib.DB.create_from_coqlib_stanzas coq_stanzas in
let root =
Path.Build.append_source build_context_dir (Dune_project.root project)
in
Some { project; db; coq_db; root })
Some { project; db; root })

let create ~projects ~context ~installed_libs ~lib_config stanzas =
let t = Fdecl.create Dyn.Encoder.opaque in
Expand Down
2 changes: 0 additions & 2 deletions src/dune/scope.mli
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,6 @@ val project : t -> Dune_project.t
(** Return the library database associated to this scope *)
val libs : t -> Lib.DB.t

val coq_libs : t -> Coq_lib.DB.t

(** Scope databases *)
module DB : sig
type scope = t
Expand Down
21 changes: 17 additions & 4 deletions src/dune/super_context.ml
Original file line number Diff line number Diff line change
Expand Up @@ -175,6 +175,7 @@ end
type t =
{ context : Context.t
; scopes : Scope.DB.t
; coq_scopes : Coq_scope.DB.t
; public_libs : Lib.DB.t
; installed_libs : Lib.DB.t
; stanzas : Dune_file.Stanzas.t Dir_with_dune.t list
Expand Down Expand Up @@ -242,6 +243,8 @@ let installed_libs t = t.installed_libs

let find_scope_by_dir t dir = Scope.DB.find_by_dir t.scopes dir

let find_coq_scope_by_dir t dir = Coq_scope.DB.find_by_dir t.coq_scopes dir

let find_scope_by_project t = Scope.DB.find_by_project t.scopes

let find_project_by_key t = Dune_project.File_key.Map.find_exn t.projects_by_key
Expand Down Expand Up @@ -441,15 +444,24 @@ let create ~(context : Context.t) ?host ~projects ~packages ~stanzas
| Dune_file.External_variant ev -> External_variant ev :: acc
| Dune_file.Deprecated_library_name d ->
Deprecated_library_name d :: acc
| Dune_file.Coq.T coq_lib ->
| _ -> acc)
in
Scope.DB.create ~projects ~context:context.name ~installed_libs ~lib_config
stanzas
in
let coq_scopes =
let stanzas =
Dune_load.Dune_file.fold_stanzas stanzas ~init:[]
~f:(fun dune_file stanza acc ->
match stanza with
| Dune_file.Coq.T theory ->
let ctx_dir =
Path.Build.append_source context.build_dir dune_file.dir
in
Coq_theory (ctx_dir, coq_lib) :: acc
(ctx_dir, theory) :: acc
| _ -> acc)
in
Scope.DB.create ~projects ~context:context.name ~installed_libs ~lib_config
stanzas
Coq_scope.DB.create ~context:context.name stanzas
in
let stanzas =
List.map stanzas ~f:(fun { Dune_load.Dune_file.dir; project; stanzas } ->
Expand Down Expand Up @@ -524,6 +536,7 @@ let create ~(context : Context.t) ?host ~projects ~packages ~stanzas
; root_expander
; host
; scopes
; coq_scopes
; public_libs
; installed_libs
; stanzas
Expand Down
2 changes: 2 additions & 0 deletions src/dune/super_context.mli
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,8 @@ val dump_env : t -> dir:Path.Build.t -> Dune_lang.t list Build.t

val find_scope_by_dir : t -> Path.Build.t -> Scope.t

val find_coq_scope_by_dir : t -> Path.Build.t -> Coq_scope.t

val find_scope_by_project : t -> Dune_project.t -> Scope.t

val find_project_by_key : t -> Dune_project.File_key.t -> Dune_project.t
Expand Down