Source file compile.ml

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
(** High-level compilation functions. *)

open Lplib
open Timed
open Common open Error open Library
open Parsing
open Core open Sign open Term

(** [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 () =
    (* Searching for source is delayed because we may not need it
       in case of "ghost" signatures (such as for unification rules). *)
    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:@." Path.pp mp;
      List.iter (fatal_msg "- %a@." Path.pp) !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
      (* [sign] is added to [loaded] before processing the commands so that it
         is possible to qualify the symbols of the current modules. *)
      loaded := Path.Map.add mp sign !loaded;
      Stdlib.(Tactic.admitted := -1);
      let consume cmd =
        Stdlib.(sig_st := handle (compile_with ~handle ~force) !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;
      (* Since Unif_rule.sign is always assumed to be already loaded, we need
         to explicitly update the decision tree of Unif_rule.equiv since it is
         not done in linking which normally follows loading. *)
      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], forcing
    compilation of up-to-date files if [force] is true. *)
let compile : ?force:bool -> Path.t -> Sign.t = fun ?(force=false) ->
  compile_with ~handle:Command.handle ~force

(** [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 : ?force:bool -> string -> Sign.t =
  fun ?(force=false) fname ->
  Package.apply_config fname;
  compile ~force (path_of_file LpLexer.escape fname)

(** The functions provided in this module perform the same computations as the
   ones defined earlier, but restore the console state and the library
   mappings when they have finished. An optional library mapping or console
   state can be passed as argument to change the settings. *)
module PureUpToSign = struct

  (** [apply_cfg ?lm ?st f x] is the same as [f x] except that the console
     state and {!val:Library.lib_mappings} are restored after the evaluation
     of [f x]. [?lm] allows to set the library mappings and [?st] to set the
     console state. *)
  let apply_cfg :
    ?lm:Path.t*string -> ?st:Console.State.t -> ('a -> 'b) -> 'a -> 'b =
    fun ?lm ?st f x ->
      let lib_mappings = !Library.lib_mappings in
      Console.State.push ();
      Option.iter Library.add_mapping lm;
      Option.iter Console.State.apply st;
      let restore () =
        Library.lib_mappings := lib_mappings;
        Console.State.pop ()
      in
      try let res = f x in restore (); res
      with e -> restore (); raise e

  let compile :
  ?lm:Path.t*string -> ?st:Console.State.t -> ?force:bool -> Path.t -> Sign.t
    = fun ?lm ?st ?(force=false) -> apply_cfg ?lm ?st (compile ~force)

  let compile_file :
  ?lm:Path.t*string -> ?st:Console.State.t -> ?force:bool -> string -> Sign.t
    = fun ?lm ?st ?(force=false) -> apply_cfg ?lm ?st (compile_file ~force)

end