Source file `signature_with_global_bindings.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
[@@@ocaml.warning "+a-9-40-41-42"]

type t = {
  sign : Subst.Lazy.persistent_signature;
  bound_globals : Global_module.With_precision.t array;
}

let read_from_cmi (cmi : Cmi_format.cmi_infos_lazy) =
  let cmi_sign, staticity = cmi.cmi_sign in
  let sign =
    (* Freshen identifiers bound by signature *)
    Subst.Lazy.signature Make_local (Subst.for_loading_cmi ()) cmi_sign in
  let bound_globals = cmi.cmi_globals in
  { sign = (sign, staticity); bound_globals }

let array_fold_left_filter_map f init array =
  let ans, new_array = Array.fold_left_map f init array in
  let new_array =
    (* To be replaced with something faster if we need it *)
    Array.of_seq (Seq.filter_map (fun a -> a) (Array.to_seq new_array))
  in
  ans, new_array

let name_in_subst (name : Global_module.Name.t) subst =
  match name with
  | { head; args = [] } ->
    (* Not generally okay to just convert to a parameter name, but we're only doing this
       to check whether there happens to be a parameter with this name in the subst *)
    let head_as_param_name = head |> Global_module.Parameter_name.of_string in
    Global_module.Parameter_name.Map.mem head_as_param_name subst
  | _ -> false

let subst t (args : (Global_module.Parameter_name.t * Global_module.t) list) =
  let { sign = (sign, staticity); bound_globals } = t in
  match args with
  | [] -> t
  | _ ->
      (* The global-level substitution *)
      let arg_subst = Global_module.Parameter_name.Map.of_list args in
      (* Take a bound global, substitute arguments into it, then return the
         updated global while also adding it to the term-level substitution *)
      let add_and_update_binding subst (bound_global, prec) =
        let name = Global_module.to_name bound_global in
        if name_in_subst name arg_subst then
          (* This shouldn't happen: only globals with hidden arguments should be
             in [bound_globals], and parameters shouldn't have arguments.
             Previous code that was meant to handle parameterised parameters
             was simply saying [subst, None] here since [add_arg] would handle
             adding to [subst] and we can drop the global from [bound_globals]
             if we're substituting for it. *)
          Misc.fatal_error "Unexpected parameterised parameter"
        else
          begin
            let value, changed = Global_module.subst bound_global arg_subst in
            let name_id = Ident.create_global name in
            let value_as_name = Global_module.to_name value in
            let value_id = Ident.create_global value_as_name in
            let subst =
              match changed with
              | `Changed ->
                  Subst.add_module name_id (Pident value_id) subst
              | `Did_not_change ->
                  subst
            in
            let new_bound_global =
              if Global_module.is_complete value then
                (* No explicit binding for unparameterised or
                   completely-applied global *)
                None
              else
                Some (value, prec)
            in
            subst, new_bound_global
          end
      in
      let subst = Subst.identity in
      let subst, bound_globals =
        array_fold_left_filter_map add_and_update_binding subst bound_globals
      in
      (* Add an argument to the substitution. *)
      let add_arg subst (name, value) =
        let name_id =
          Ident.create_global (name |> Global_module.Name.of_parameter_name)
        in
        let value_as_name = Global_module.to_name value in
        let value_id = Ident.create_global value_as_name in
        Subst.add_module name_id (Pident value_id) subst
      in
      let subst = List.fold_left add_arg subst args in
      let sign = Subst.Lazy.signature Keep subst sign in
      { sign = (sign, staticity); bound_globals }
Source file signature_with_global_bindings.ml

Source file `signature_with_global_bindings.ml`
