1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
(** High-level compilation functions. *)
open! Lplib
open Timed
open Common
open Error
open Parsing
open Core
open Sign
open Library
(** [gen_obj] indicates whether we should generate object files when compiling
source files. The default behaviour is not te generate them. *)
let gen_obj = Stdlib.ref false
(** [compile_with ~handle ~force mp] compiles the file corresponding to module
path [mp] using function [~handle] to process commands. Module [mp] is
processed when it is necessary, i.e. the corresponding object file does not
exist, or it must be updated, or [~force] is [true]. In that case, the
produced signature is stored in the corresponding object file if the option
[--gen_obj] or [-c] is set. *)
let rec compile_with :
handle:(Command.compiler -> Sig_state.t -> Syntax.p_command -> Sig_state.t)
-> force:bool -> Command.compiler =
fun ~handle ~force mp ->
let base = file_of_path mp in
let src () =
let lp_src = base ^ lp_src_extension in
let dk_src = base ^ dk_src_extension in
match (Sys.file_exists lp_src, Sys.file_exists dk_src) with
| (false, false) ->
fatal_no_pos "File \"%s.lp\" (or .dk) not found." base
| (true , true ) ->
wrn None "Both \"%s\" and \"%s\" exist. We take \"%s\"."
lp_src dk_src lp_src; lp_src
| (true , false) -> lp_src
| (false, true ) -> dk_src
in
let obj = base ^ obj_extension in
if List.mem mp !loading then
begin
fatal_msg "Circular dependencies detected in \"%s\".@." (src ());
fatal_msg "Dependency stack for module %a:@." Print.pp_path mp;
List.iter (fatal_msg "- %a@." Print.pp_path) !loading;
fatal_no_pos "Build aborted."
end;
match Path.Map.find_opt mp !loaded with
| Some sign -> sign
| None ->
if force || Extra.more_recent (src ()) obj then
begin
let forced = if force then " (forced)" else "" in
let src = src () in
Console.out 1 "Loading \"%s\"%s ..." src forced;
loading := mp :: !loading;
let sign = Sig_state.create_sign mp in
let sig_st = Stdlib.ref (Sig_state.of_sign sign) in
loaded := Path.Map.add mp sign !loaded;
Stdlib.(Tactic.admitted := -1);
let consume cmd =
Stdlib.(sig_st :=
handle (compile_with ~handle ~force:false) !sig_st cmd)
in
Debug.stream_iter consume (Parser.parse_file src);
Sign.strip_private sign;
if Stdlib.(!gen_obj) then Sign.write sign obj;
loading := List.tl !loading;
sign
end
else
begin
Console.out 1 "Loading \"%s\" ..." (src ());
let sign = Sign.read obj in
let compile mp _ = ignore (compile_with ~handle ~force:false mp) in
Path.Map.iter compile !(sign.sign_deps);
loaded := Path.Map.add mp sign !loaded;
Sign.link sign;
let sm = Path.Map.find Unif_rule.path !(sign.sign_deps) in
if Extra.StrMap.mem Unif_rule.equiv.sym_name sm then
Tree.update_dtree Unif_rule.equiv;
sign
end
(** [compile force mp] compiles module path [mp] using [compile_with], forcing
compilation of up-to-date files if [force] is true. *)
let compile force = compile_with ~handle:Command.handle ~force
(** [recompile] indicates whether we should recompile files who have an object
file that is already up to date. Note that this flag only applies to files
that are given on the command line explicitly, not their dependencies. *)
let recompile = Stdlib.ref false
(** [compile_file fname] looks for a package configuration file for
[fname] and compiles [fname]. It is the main compiling function. It
is called from the main program exclusively. *)
let compile_file : string -> Sign.t = fun fname ->
Package.apply_config fname;
let mp = path_of_file LpLexer.escape fname in
compile Stdlib.(!recompile) mp
open Console
(** Pure wrappers around compilation functions. Functions provided perform the
same computations as the ones defined earlier, but restores the state when
they have finished. An optional library mapping or state can be passed as
argument to change the settings. *)
module Pure : sig
val compile : ?lm:Path.t*string -> ?st:State.t -> bool -> Path.t -> Sign.t
val compile_file : ?lm:Path.t*string -> ?st:State.t -> string -> Sign.t
end = struct
let pure_apply_cfg :
?lm:Path.t*string -> ?st:State.t -> ('a -> 'b) -> 'a -> 'b =
fun ?lm ?st f x ->
let libmap = !lib_mappings in
State.push ();
Option.iter Library.add_mapping lm;
Option.iter State.apply st;
let restore () =
State.pop ();
lib_mappings := libmap
in
try
let res = f x in
restore (); res
with e -> restore (); raise e
let compile ?lm ?st force mp =
let f (force, mp) = compile force mp in
pure_apply_cfg ?lm ?st f (force, mp)
let compile_file ?lm ?st = pure_apply_cfg ?lm ?st compile_file
end