SSL declaremods.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp
open CErrors
open Util
open Names
open Declarations
open Mod_declarations
open Entries
open Libnames
open Libobject
open Mod_subst

(** {6 Inlining levels} *)

(** Rigid / flexible module signature *)

type 'a module_signature =
  | Enforce of 'a (** ... : T *)
  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)

(** Which module inline annotations should we honor,
    either None or the ones whose level is less or equal
    to the given integer *)

type inline =
  | NoInline
  | DefaultInline
  | InlineAt of int

let default_inline () = Some (Flags.get_inline_level ())

let inl2intopt = function
  | NoInline -> None
  | InlineAt i -> Some i
  | DefaultInline -> default_inline ()

(** These functions register the visibility of the module and iterates
    through its components. They are called by plenty of module functions *)

let consistency_checks exists dir =
  if exists then
    let _ =
      try Nametab.locate_module (qualid_of_path dir)
      with Not_found ->
        user_err
          (pr_path dir ++ str " should already exist!")
    in
    ()
  else
    if Nametab.exists_module dir then
      user_err
        (pr_path dir ++ str " already exists.")

let rec get_module_path = function
  | MEident mp -> mp
  | MEwith (me,_) -> get_module_path me
  | MEapply (me,_) -> get_module_path me

let type_of_mod mp env = function
  | true -> mod_type (Environ.lookup_module mp env)
  | false -> mod_type (Environ.lookup_modtype mp env)

(** {6 Name management}

    Auxiliary functions to transform full_path and kernel_name given
    by Lib into ModPath.t and DirPath.t needed for modules
*)

let mp_of_kn kn =
  let mp,l = KerName.repr kn in
  MPdot (mp,l)

let pop_path sp =
  path_pop_suffix sp, basename sp

let path_of_file dp =
  match DirPath.repr dp with
  | x :: dp -> make_path (DirPath.make dp) x
  | [] -> CErrors.anomaly Pp.(str "Cannot start library with empty dirpath")

(* Avoid generating a KeepObject for nothing *)
let keep_objects id keep = match keep.keep_objects with
  | [] -> []
  | _ :: _ -> [KeepObject (id, keep)]

let escape_objects id escape = match escape.escape_objects with
  | [] -> []
  | _ :: _ -> [EscapeObject (id, escape)]

(** The [ModActions] abstraction represent operations on modules
    that are specific to a given stage. Two instances are defined below,
    for Synterp and Interp. *)
module type ModActions = sig

  type typexpr
  type env

  val stage : Summary.Stage.t
  val substobjs_table_name : string
  val modobjs_table_name : string

  val enter_module : ModPath.t -> full_path -> int -> unit

  val enter_modtype : ModPath.t -> full_path -> int -> unit

  val open_module : open_filter -> ModPath.t -> full_path -> int -> unit

  module Lib : Lib.StagedLibS

  (** Create the substitution corresponding to some functor applications *)

  val compute_subst : is_mod:bool -> env -> MBId.t list -> ModPath.t -> ModPath.t list -> Entries.inline -> MBId.t list * substitution

end

module SynterpActions : ModActions with
  type env = unit with
  type typexpr = Constrexpr.universe_decl_expr option * Constrexpr.constr_expr =
struct
  type typexpr = Constrexpr.universe_decl_expr option * Constrexpr.constr_expr
  type env = unit
  let stage = Summary.Stage.Synterp
  let substobjs_table_name = "MODULE-SYNTAX-SUBSTOBJS"
  let modobjs_table_name = "MODULE-SYNTAX-OBJS"

  let enter_module obj_mp obj_path i =
    consistency_checks false obj_path;
    Nametab.push_module (Until i) obj_path obj_mp

  let enter_modtype mp sp i =
    if Nametab.exists_modtype sp then
      anomaly (pr_path sp ++ str " already exists.");
    Nametab.push_modtype (Nametab.Until i) sp mp

  let open_module f obj_mp obj_path i =
    consistency_checks true obj_path;
    if in_filter ~cat:None f then Nametab.push_module (Nametab.Exactly i) obj_path obj_mp

  module Lib = Lib.Synterp

  let rec compute_subst () mbids mp_l inl =
    match mbids,mp_l with
      | _,[] -> mbids,empty_subst
      | [],r -> user_err Pp.(str "Application of a functor with too few arguments.")
      | mbid::mbids,mp::mp_l ->
          let mbid_left,subst = compute_subst () mbids mp_l inl in
          mbid_left, join (map_mbid mbid mp (empty_delta_resolver mp)) subst

  let compute_subst ~is_mod () mbids mp1 mp_l inl =
    compute_subst () mbids mp_l inl

end

module InterpActions : ModActions
  with type env = Environ.env
  with type typexpr = Constr.t * UVars.AbstractContext.t option =
struct
  type typexpr = Constr.t * UVars.AbstractContext.t option
  type env = Environ.env
  let stage = Summary.Stage.Interp
  let substobjs_table_name = "MODULE-SUBSTOBJS"
  let modobjs_table_name = "MODULE-OBJS"

  (** {6 Current module type information}

    This information is stored by each [start_modtype] for use
    in a later [end_modtype]. *)

  let enter_module obj_mp obj_path i = ()
  let enter_modtype mp sp i = ()

  let open_module f obj_mp obj_path i = ()

  module Lib = Lib.Interp

  let rec compute_subst env mbids sign mp_l inl =
    match mbids,mp_l with
      | _,[] -> mbids,empty_subst
      | [],r -> user_err Pp.(str "Application of a functor with too few arguments.")
      | mbid::mbids,mp::mp_l ->
          let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
          let mb = Environ.lookup_module mp env in
          let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in
          let resolver = match mod_global_delta mb with
          | None -> empty_delta_resolver mp
          | Some delta ->
            Modops.inline_delta_resolver env inl mp farg_id farg_b delta
          in
          mbid_left,join (map_mbid mbid mp resolver) subst

  let compute_subst ~is_mod env mbids mp1 mp_l inl =
    let typ = type_of_mod mp1 env is_mod in
    compute_subst env mbids typ mp_l inl

end

type exp_substituted_object = (substitutive_objects, exp_algebraic_objects, Empty.t, Empty.t) object_view

and exp_algebraic_objects = { exp_algebraic_objects : exp_substituted_object list }

(* and exp_substitutive_objects = Names.MBId.t list * exp_algebraic_objects *)

type module_objects =
  { module_prefix : object_prefix;
    module_substituted_objects : exp_substituted_object list;
    module_keep_objects : keep_objects;
    module_escape_objects : escape_objects;
  }

(** The [StagedModS] abstraction describes module operations at a given stage. *)
module type StagedModS = sig

  type typexpr
  type env

  val get_module_sobjs : bool -> env -> Entries.inline -> typexpr module_alg_expr -> substitutive_objects

  val load_keep : int -> full_path -> ModPath.t -> keep_objects -> unit
  val load_escape : int -> full_path -> ModPath.t -> escape_objects -> unit
  val load_module : int -> full_path -> ModPath.t -> substitutive_objects -> unit
  val import_modules : export:Lib.export_flag -> (open_filter * ModPath.t) list -> unit

  val add_leaf : Libobject.t -> unit
  val add_leaves : Libobject.t list -> unit

  val expand_aobjs : Libobject.algebraic_objects -> Libobject.t list

  val get_applications : typexpr module_alg_expr -> ModPath.t * ModPath.t list
  val debug_print_modtab : unit -> Pp.t

  module ModObjs : sig val all : unit -> module_objects MPmap.t end

  val close_section : unit -> unit

end

(** Some utilities about substitutive objects :
    substitution, expansion *)

let sobjs_no_functor (mbids,_) = List.is_empty mbids

let subst_filtered sub (f,mp as x) =
  let mp' = subst_mp sub mp in
  if mp == mp' then x
  else f, mp'

let rec subst_aobjs sub = function
  | Objs o as objs ->
    let o' = subst_objects sub o in
    if o == o' then objs else Objs o'
  | Ref (mp, sub0) as r ->
    let sub0' = join sub0 sub in
    if sub0' == sub0 then r else Ref (mp, sub0')

and subst_sobjs sub (mbids,aobjs as sobjs) =
  let aobjs' = subst_aobjs sub aobjs in
  if aobjs' == aobjs then sobjs else (mbids, aobjs')

and subst_objects subst seg =
  let subst_one node =
    match node with
    | AtomicObject obj ->
      let obj' = Libobject.subst_object (subst,obj) in
      if obj' == obj then node else AtomicObject obj'
    | ModuleObject (id, sobjs) ->
      let sobjs' = subst_sobjs subst sobjs in
      if sobjs' == sobjs then node else ModuleObject (id, sobjs')
    | ModuleTypeObject (id, sobjs) ->
      let sobjs' = subst_sobjs subst sobjs in
      if sobjs' == sobjs then node else ModuleTypeObject (id, sobjs')
    | IncludeObject aobjs ->
      let aobjs' = subst_aobjs subst aobjs in
      if aobjs' == aobjs then node else IncludeObject aobjs'
    | ExportObject { mpl } ->
      let mpl' = List.Smart.map (subst_filtered subst) mpl in
      if mpl'==mpl then node else ExportObject { mpl = mpl' }
    | KeepObject _ | EscapeObject _ -> assert false
  in
  List.Smart.map subst_one seg

(** The [StagedMod] abstraction factors out the code dealing with modules
  that is common to all stages. *)
module StagedMod(Actions : ModActions) = struct

type typexpr = Actions.typexpr
type env = Actions.env

(** ModSubstObjs : a cache of module substitutive objects

   This table is common to modules and module types.
   -  For a Module M:=N, the objects of N will be reloaded
      with M after substitution.
   -  For a Module M:SIG:=..., the module M gets its objects from SIG

   Invariants:
   - A alias (i.e. a module path inside a Ref constructor) should
     never lead to another alias, but rather to a concrete Objs
     constructor.

   We will plug later a handler dealing with missing entries in the
   cache. Such missing entries may come from inner parts of module
   types, which aren't registered by the standard libobject machinery.
*)

module ModSubstObjs :
sig
   val set : ModPath.t -> substitutive_objects -> unit
   val get : ModPath.t -> substitutive_objects
   val set_missing_handler : (ModPath.t -> substitutive_objects) -> unit
end =
struct
   let table =
     Summary.ref ~stage:Actions.stage (MPmap.empty : substitutive_objects MPmap.t)
       ~name:Actions.substobjs_table_name
   let missing_handler = ref (fun mp -> assert false)
   let set_missing_handler f = (missing_handler := f)
   let set mp objs = (table := MPmap.add mp objs !table)
   let get mp =
     try MPmap.find mp !table with Not_found -> !missing_handler mp
end

let expand_aobjs = function
  | Objs o -> o
  | Ref (mp, sub) ->
    match ModSubstObjs.get mp with
      | (_,Objs o) -> subst_objects sub o
      | _ -> assert false (* Invariant : any alias points to concrete objs *)

let expand_sobjs (_,aobjs) = expand_aobjs aobjs

module Expand =
struct

type exp_object = (substitutive_objects, exp_algebraic_objects, keep_objects, escape_objects) object_view

let exp_substituted_view (obj : exp_substituted_object) : exp_object = match obj with
| (AtomicObject _ | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | ExportObject _) as o -> o
| EscapeObject (_, o) | KeepObject (_, o) -> Empty.abort o

let keep_view (obj : Libobject.t) : exp_object = match obj with
| (AtomicObject _ | KeepObject _) as o -> o
| ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | ExportObject _ | EscapeObject _ ->
  assert false (** keep objects only contain atomic / keep *)

let escape_view (obj : Libobject.t) : exp_object = match obj with
| (AtomicObject _ | EscapeObject _) as o -> o
| ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | ExportObject _ | KeepObject _ ->
  assert false (** escape objects only contain atomic / escape *)

let rec substituted_object_view (obj : Libobject.t) : exp_substituted_object = match obj with
| (AtomicObject _ | ModuleObject _ | ModuleTypeObject _ | ExportObject _) as o -> o
| IncludeObject aobjs ->
  let aobjs = expand_aobjs aobjs in
  IncludeObject { exp_algebraic_objects = List.map substituted_object_view aobjs }
| EscapeObject _ | KeepObject _ ->
  (* forbidden in substitutive objects *)
  assert false

let object_view (obj : Libobject.t) : exp_object = match obj with
| (AtomicObject _ | EscapeObject _ | ModuleObject _ | ModuleTypeObject _ | ExportObject _ | KeepObject _) as o -> o
| IncludeObject aobjs ->
  let aobjs = expand_aobjs aobjs in
  IncludeObject { exp_algebraic_objects = List.map substituted_object_view aobjs }

end

(** {6 ModObjs : a cache of module objects}

   For each module, we also store a cache of
   "prefix", "substituted objects", "keep objects".
   This is used for instance to implement the "Import" command.

   substituted objects :
     roughly the objects above after the substitution - we need to
     keep them to call open_object when the module is opened (imported)

   keep objects :
     The list of non-substitutive objects - as above, for each of
     them we will call open_object when the module is opened

   (Some) Invariants:
   * If the module is a functor, it won't appear in this cache.

   * Module objects in substitutive_objects part have empty substituted
     objects.

   * Modules which where created with Module M:=mexpr or with
     Module M:SIG. ... End M. have the keep list empty.
*)

module ModObjs :
sig
   val set : ModPath.t -> module_objects -> unit
   val get : ModPath.t -> module_objects (* may raise Not_found *)
   val all : unit -> module_objects MPmap.t
end =
struct
   let table =
     Summary.ref ~stage:Actions.stage (MPmap.empty : module_objects MPmap.t)
       ~name:Actions.modobjs_table_name
   let set mp objs = (table := MPmap.add mp objs !table)
   let get mp = MPmap.find mp !table
   let all () = !table
end

open Expand

(** {6 Declaration of module substitutive objects} *)

(** Nota: Interactive modules and module types cannot be recached!
    This used to be checked here via a flag along the substobjs. *)

(** {6 Declaration of module type substitutive objects} *)

(** Nota: Interactive modules and module types cannot be recached!
    This used to be checked more properly here. *)

let load_modtype i sp mp sobjs =
  Actions.enter_modtype mp sp i;
  ModSubstObjs.set mp sobjs

(** {6 Declaration of substitutive objects for Include} *)

let rec load_object : type a. (a -> exp_object) -> int -> object_prefix * a -> unit = fun view i (prefix, obj) ->
  match view obj with
  | AtomicObject o -> Libobject.load_object i (prefix, o)
  | ModuleObject (id,sobjs) ->
    let sp, kn = Lib.make_oname prefix id in
    load_module i sp (mp_of_kn kn) sobjs
  | ModuleTypeObject (id,sobjs) ->
    let name = Lib.make_oname prefix id in
    let (sp,kn) = name in
    load_modtype i sp (mp_of_kn kn) sobjs
  | IncludeObject aobjs ->
    load_include i (prefix, aobjs)
  | ExportObject _ -> ()
  | KeepObject (id,objs) ->
    let sp, kn = Lib.make_oname prefix id in
    load_keep i sp (mp_of_kn kn) objs
  | EscapeObject (id,objs) ->
    let sp, kn = Lib.make_oname prefix id in
    load_escape i sp (mp_of_kn kn) objs

and load_objects : type a. (a -> exp_object) -> int -> object_prefix -> a list -> unit = fun view i prefix objs ->
  List.iter (fun obj -> load_object view i (prefix, obj)) objs

and load_include i (prefix, aobjs) =
  load_objects exp_substituted_view i prefix aobjs.exp_algebraic_objects

and load_keep i obj_path obj_mp kobjs =
  (* Invariant : seg isn't empty *)
  let prefix = { obj_path ; obj_mp; } in
  let modobjs =
    try ModObjs.get obj_mp
    with Not_found -> assert false (* a substobjs should already be loaded *)
  in
  assert (eq_object_prefix modobjs.module_prefix prefix);
  assert (List.is_empty modobjs.module_keep_objects.keep_objects);
  ModObjs.set obj_mp { modobjs with module_keep_objects = kobjs };
  load_objects keep_view (i+1) prefix kobjs.keep_objects

and load_escape i obj_path obj_mp eobjs =
  (* Invariant : seg isn't empty *)
  let prefix = { obj_path ; obj_mp; } in
  let modobjs =
    try ModObjs.get obj_mp
    with Not_found ->
      (* escape objects can exist even if there is no corresponding real module *)
      { module_prefix = prefix;
        module_substituted_objects = [];
        module_keep_objects = { keep_objects = [] };
        module_escape_objects = { escape_objects = [] };
      }
  in
  assert (eq_object_prefix modobjs.module_prefix prefix);
  assert (List.is_empty modobjs.module_escape_objects.escape_objects);
  ModObjs.set obj_mp { modobjs with module_escape_objects = eobjs };
  load_objects escape_view (i+1) prefix eobjs.escape_objects

and load_module i obj_path obj_mp sobjs =
  let prefix = { obj_path ; obj_mp; } in
  Actions.enter_module obj_mp obj_path i;
  ModSubstObjs.set obj_mp sobjs;
  (* If we're not a functor, let's iter on the internal components *)
  if sobjs_no_functor sobjs then begin
    let objs = expand_sobjs sobjs in
    let objs = List.map substituted_object_view objs in
    let module_objects =
      { module_prefix = prefix;
        module_substituted_objects = objs;
        module_keep_objects = { keep_objects = [] };
        module_escape_objects = { escape_objects = [] };
      }
    in
    ModObjs.set obj_mp module_objects;
    load_objects exp_substituted_view (i+1) prefix objs
  end

(** {6 Implementation of Import and Export commands} *)

let mark_object f obj (exports,acc) =
  (exports, (f,obj)::acc)

let rec collect_module (f,mp) acc =
  try
    (* May raise Not_found for unknown module and for functors *)
    let modobjs = ModObjs.get mp in
    let prefix = modobjs.module_prefix in
    let acc = collect_objects escape_view f 1 prefix modobjs.module_escape_objects.escape_objects acc in
    let acc = collect_objects keep_view f 1 prefix modobjs.module_keep_objects.keep_objects acc in
    collect_objects exp_substituted_view f 1 prefix modobjs.module_substituted_objects acc
  with Not_found when Actions.stage = Summary.Stage.Synterp ->
    acc

and collect_object : type a. (a -> exp_object) -> _ -> _ -> _ -> a -> _ -> _ = fun view f i prefix obj acc ->
  match view obj with
  | ExportObject { mpl } -> collect_exports f i mpl acc
  | (AtomicObject _ | IncludeObject _ | KeepObject _ | EscapeObject _
  | ModuleObject _ | ModuleTypeObject _) as obj -> mark_object f (prefix,obj) acc

and collect_objects : type a. (a -> exp_object) -> _ -> _ -> _ -> a list -> _ = fun view f i prefix objs acc ->
  List.fold_left (fun acc obj -> collect_object view f i prefix obj acc)
    acc
    (List.rev objs)

and collect_export f (f',mp) (exports,objs as acc) =
  match filter_and f f' with
  | None -> acc
  | Some f ->
    let exports' = MPmap.update mp (function
        | None -> Some f
        | Some f0 ->
          let f' = filter_or f f0 in
          if filter_eq f' f0 then Some f0 else Some f')
        exports
    in
    (* If the map doesn't change there is nothing new to export. *)
    if exports == exports' then acc
    else
      collect_module (f,mp) (exports', objs)

and collect_exports f i mpl acc =
  if Int.equal i 1 then
    List.fold_left (fun acc fmp -> collect_export f fmp acc) acc (List.rev mpl)
  else acc

let collect_modules mpl =
  List.fold_left (fun acc fmp -> collect_module fmp acc)  (MPmap.empty, []) (List.rev mpl)

let open_modtype i ((sp,kn),_) =
  let mp = mp_of_kn kn in
  let mp' =
    try Nametab.locate_modtype (qualid_of_path sp)
    with Not_found ->
      anomaly (pr_path sp ++ str " should already exist!");
  in
  assert (ModPath.equal mp mp');
  Nametab.push_modtype (Nametab.Exactly i) sp mp

let rec open_object : type a. (a -> exp_object) -> _ -> _ -> _ * a -> _ = fun view f i (prefix, obj) ->
  match view obj with
  | AtomicObject o -> Libobject.open_object f i (prefix, o)
  | ModuleObject (id,sobjs) ->
    let sp, kn = Lib.make_oname prefix id in
    let mp = mp_of_kn kn in
    open_module f i sp mp sobjs
  | ModuleTypeObject (id,sobjs) ->
    let name = Lib.make_oname prefix id in
    open_modtype i (name, sobjs)
  | IncludeObject aobjs ->
    open_include f i (prefix, aobjs)
  | ExportObject { mpl } -> open_export f i mpl
  | KeepObject (id,objs) ->
    let name = Lib.make_oname prefix id in
    open_keep f i (name, objs)
  | EscapeObject (id,objs) ->
    let name = Lib.make_oname prefix id in
    open_escape f i (name, objs)

and open_module f i obj_path obj_mp sobjs =
  Actions.open_module f obj_mp obj_path i;
  (* If we're not a functor, let's iter on the internal components *)
  if sobjs_no_functor sobjs then begin
    let modobjs = ModObjs.get obj_mp in
    open_objects exp_substituted_view f (i+1) modobjs.module_prefix modobjs.module_substituted_objects
  end

and open_objects : type a. (a -> exp_object) -> _ -> _ -> _ -> a list -> _ = fun view f i prefix objs ->
  List.iter (fun obj -> open_object view f i (prefix, obj)) objs

and open_include f i (prefix, aobjs) =
  open_objects exp_substituted_view f i prefix aobjs.exp_algebraic_objects

and open_export f i mpl =
  let _,objs = collect_exports f i mpl (MPmap.empty, []) in
  List.iter (fun (f,o) -> open_object (fun x -> x) f 1 o) objs

and open_keep f i ((sp,kn),kobjs) =
  let obj_mp = mp_of_kn kn in
  let prefix = { obj_path=sp; obj_mp; } in
  open_objects keep_view f (i+1) prefix kobjs.keep_objects

and open_escape f i ((sp,kn),kobjs) =
  let obj_mp = mp_of_kn kn in
  let prefix = { obj_path=sp; obj_mp; } in
  open_objects escape_view f (i+1) prefix kobjs.escape_objects

let cache_include (prefix, aobjs) =
  let o = expand_aobjs aobjs in
  let o = List.map substituted_object_view o in
  load_objects exp_substituted_view 1 prefix o;
  open_objects exp_substituted_view unfiltered 1 prefix o

let cache_object (prefix, obj) =
  match obj with
  | AtomicObject o -> Libobject.cache_object (prefix, o)
  | ModuleObject _ -> load_object object_view 1 (prefix,obj)
  | ModuleTypeObject _ -> load_object object_view 0 (prefix,obj)
  | IncludeObject aobjs -> cache_include (prefix, aobjs)
  | ExportObject { mpl } -> anomaly Pp.(str "Export should not be cached")
  | KeepObject _ | EscapeObject _ -> anomaly (Pp.str "This module should not be cached!")

(* Adding operations with containers *)

let add_leaf_entry =
  match Actions.stage with
  | Summary.Stage.Synterp -> Lib.Synterp.add_leaf_entry
  | Summary.Stage.Interp -> Lib.Interp.add_leaf_entry

let add_leaf obj =
  cache_object (Lib.prefix (),obj);
  add_leaf_entry obj

let add_leaves objs =
  let add_obj obj =
    add_leaf_entry obj;
    load_object object_view 1 (Lib.prefix (),obj)
  in
  List.iter add_obj objs

let import_modules ~export mpl =
  let _,objs = collect_modules mpl in
  List.iter (fun (f,o) -> open_object (fun x -> x) f 1 o) objs;
  match export with
  | Lib.Import -> ()
  | Lib.Export ->
    let entry = ExportObject { mpl } in
    add_leaf_entry entry

(** {6 Handler for missing entries in ModSubstObjs} *)

(** Since the inner of Module Types are not added by default to
    the ModSubstObjs table, we compensate this by explicit traversal
    of Module Types inner objects when needed. Quite a hack... *)

let mp_id mp id = MPdot (mp, Label.of_id id)

let rec register_mod_objs mp obj = match obj with
  | ModuleObject (id,sobjs) -> ModSubstObjs.set (mp_id mp id) sobjs
  | ModuleTypeObject (id,sobjs) -> ModSubstObjs.set (mp_id mp id) sobjs
  | IncludeObject aobjs ->
    List.iter (register_mod_objs mp) (expand_aobjs aobjs)
  | _ -> ()

let handle_missing_substobjs mp = match mp with
  | MPdot (mp',l) ->
    let objs = expand_sobjs (ModSubstObjs.get mp') in
    List.iter (register_mod_objs mp') objs;
    ModSubstObjs.get mp
  | _ ->
    assert false (* Only inner parts of module types should be missing *)

let () = ModSubstObjs.set_missing_handler handle_missing_substobjs

(** {6 From module expression to substitutive objects} *)

(** Turn a chain of [MSEapply] into the head ModPath.t and the
    list of ModPath.t parameters (deepest param coming first).
    The left part of a [MSEapply] must be either [MSEident] or
    another [MSEapply]. *)

let get_applications mexpr =
  let rec get params = function
    | MEident mp -> mp, params
    | MEapply (fexpr, mp) -> get (mp::params) fexpr
    | MEwith _ -> user_err Pp.(str "Non-atomic functor application.")
  in get [] mexpr

(** Create the objects of a "with Module" structure. *)

let rec replace_module_object idl mp0 objs0 mp1 objs1 =
  match idl, objs0 with
  | _,[] -> []
  | id::idl,(ModuleObject (id', sobjs))::tail when Id.equal id id' ->
    begin
      let mp_id = MPdot(mp0, Label.of_id id) in
      let objs = match idl with
        | [] -> subst_objects (map_mp mp1 mp_id (empty_delta_resolver mp_id)) objs1
        | _ ->
          let objs_id = expand_sobjs sobjs in
          replace_module_object idl mp_id objs_id mp1 objs1
      in
      (ModuleObject (id, ([], Objs objs)))::tail
    end
  | idl,lobj::tail -> lobj::replace_module_object idl mp0 tail mp1 objs1

(** Substitutive objects of a module expression (or module type) *)

let rec get_module_sobjs is_mod env inl = function
  | MEident mp ->
    begin match ModSubstObjs.get mp with
    | (mbids,Objs _) when not (ModPath.is_bound mp) ->
      (mbids,Ref (mp, empty_subst)) (* we create an alias *)
    | sobjs -> sobjs
    end
  | MEwith (mty, WithDef _) -> get_module_sobjs is_mod env inl mty
  | MEwith (mty, WithMod (idl,mp1)) ->
    assert (not is_mod);
    let sobjs0 = get_module_sobjs is_mod env inl mty in
    if not (sobjs_no_functor sobjs0) then
      user_err Pp.(str "Illegal use of a functor.");
    (* For now, we expand everything, to be safe *)
    let mp0 = get_module_path mty in
    let objs0 = expand_sobjs sobjs0 in
    let objs1 = expand_sobjs (ModSubstObjs.get mp1) in
    ([], Objs (replace_module_object idl mp0 objs0 mp1 objs1))
  | MEapply _ as me ->
    let mp1, mp_l = get_applications me in
    let mbids, aobjs = get_module_sobjs is_mod env inl (MEident mp1) in
    let mbids_left,subst = Actions.compute_subst ~is_mod env mbids mp1 mp_l inl in
    (mbids_left, subst_aobjs subst aobjs)

let debug_print_modtab () =
  let pr_seg = function
    | 0 -> str "[]"
    | l -> str "[." ++ int l ++ str ".]"
  in
  let pr_modinfo mp modobjs s =
    let objs = List.length modobjs.module_substituted_objects + List.length modobjs.module_keep_objects.keep_objects in
    s ++ str (ModPath.to_string mp) ++ spc () ++ pr_seg objs
  in
  let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in
  hov 0 modules

let add_discharged_item : Lib.discharged_item -> unit = function
  | DischargedExport { mpl } -> import_modules ~export:Export mpl
  | DischargedLeaf o -> Lib.add_discharged_leaf o

let close_section () =
  let objs = Actions.Lib.close_section () in
  List.iter add_discharged_item objs

end

module SynterpVisitor : StagedModS
  with type env = SynterpActions.env
  with type typexpr = Constrexpr.universe_decl_expr option * Constrexpr.constr_expr
  = StagedMod(SynterpActions)

module InterpVisitor : StagedModS
  with type env = InterpActions.env
  with type typexpr = Constr.t * UVars.AbstractContext.t option
= StagedMod(InterpActions)

(** {6 Modules : start, end, declare} *)

type current_module_syntax_info = {
  cur_mp : ModPath.t;
  cur_typ : ((Constrexpr.universe_decl_expr option * Constrexpr.constr_expr) module_alg_expr * int option) option;
  cur_mbids : MBId.t list;
}

let default_module_syntax_info mp = { cur_mp = mp; cur_typ = None; cur_mbids = [] }

let openmod_syntax_info =
  Summary.ref None ~stage:Summary.Stage.Synterp ~name:"MODULE-SYNTAX-INFO"

(** {6 Current module information}

    This information is stored by each [start_module] for use
    in a later [end_module]. *)

type current_module_info = {
  cur_typ : (module_struct_entry * int option) option; (** type via ":" *)
  cur_typs : module_type_body list (** types via "<:" *)
}

let default_module_info = { cur_typ = None; cur_typs = [] }

let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO"

let start_library dir =
  let mp = Global.start_library dir in
  openmod_info := default_module_info;
  openmod_syntax_info := Some (default_module_syntax_info mp);
  Lib.start_compilation dir mp

let set_openmod_syntax_info info = match !openmod_syntax_info with
  | None -> anomaly Pp.(str "bad init of openmod_syntax_info")
  | Some _ -> openmod_syntax_info := Some info

let openmod_syntax_info () = match !openmod_syntax_info with
  | None -> anomaly Pp.(str "missing init of openmod_syntax_info")
  | Some v -> v

let vm_state =
  (* VM bytecode is not needed here *)
  let vm_handler _ _ _ () = (), None in
  ((), { Mod_typing.vm_handler })

module RawModOps = struct

module Synterp = struct

let build_subtypes mtys =
  List.map
    (fun (m,ann) ->
       let inl = inl2intopt ann in
       let mte, base, kind = Modintern.intern_module_ast Modintern.ModType m in
       (mte, base, kind, inl))
  mtys

let intern_arg (idl,(typ,ann)) =
  let inl = inl2intopt ann in
  let lib_dir = Lib.library_dp() in
  let (mty, base, kind) = Modintern.intern_module_ast Modintern.ModType typ in
  let sobjs = SynterpVisitor.get_module_sobjs false () inl mty in
  let mp0 = get_module_path mty in
  let map {CAst.v=id} =
    let sp = Libnames.make_path DirPath.empty id in
    let mbid = MBId.make lib_dir id in
    let mp = MPbound mbid in
    (* We can use an empty delta resolver because we load only syntax objects *)
    let sobjs = subst_sobjs (map_mp mp0 mp (empty_delta_resolver mp)) sobjs in
    SynterpVisitor.load_module 1 sp mp sobjs;
    mbid
  in
  List.map map idl, (mty, base, kind, inl)

let intern_args params =
  List.map intern_arg params

let start_module_core id args res =
  (* Loads the parsing objects in arguments *)
  let args = intern_args args in
  let mbids = List.flatten @@ List.map (fun (mbidl,_) -> mbidl) args in
  let res_entry_o, sign = match res with
    | Enforce (res,ann) ->
        let inl = inl2intopt ann in
        let (mte, base, kind) = Modintern.intern_module_ast Modintern.ModType res in
        Some (mte, inl), Enforce (mte, base, kind, inl)
    | Check resl -> None, Check (build_subtypes resl)
  in
  let mp = ModPath.MPdot((openmod_syntax_info ()).cur_mp, Label.of_id id) in
  mp, res_entry_o, mbids, sign, args

let start_module export id args res =
  let () = if Option.has_some export && not (CList.is_empty args)
    then user_err Pp.(str "Cannot import functors.")
  in
  let fs = Summary.Synterp.freeze_summaries () in
  let mp, res_entry_o, mbids, sign, args = start_module_core id args res in
  set_openmod_syntax_info { cur_mp = mp; cur_typ = res_entry_o; cur_mbids = mbids };
  let prefix = Lib.Synterp.start_module export id mp fs in
  Nametab.(push_dir (Until 1) (prefix.obj_path) (GlobDirRef.DirOpenModule prefix.obj_mp));
  mp, args, sign

let end_module_core id (m_info : current_module_syntax_info) objects fs =
  let {Lib.substobjs = substitute; keepobjs = keep; escapeobjs = escape; anticipateobjs = special; } = objects in

  (* For sealed modules, we use the substitutive objects of their signatures *)
  let sobjs0, keep = match m_info.cur_typ with
    | None -> ([], Objs substitute), keep
    | Some (mty, inline) ->
      SynterpVisitor.get_module_sobjs false () inline mty, { keep_objects = [] }
  in
  Summary.Synterp.unfreeze_summaries fs;
  let sobjs = let (ms,objs) = sobjs0 in (m_info.cur_mbids@ms,objs) in

  (* We substitute objects if the module is sealed by a signature *)
  let sobjs =
    match m_info.cur_typ with
      | None -> sobjs
      | Some (mty, _) ->
        subst_sobjs (map_mp (get_module_path mty) m_info.cur_mp (empty_delta_resolver m_info.cur_mp)) sobjs
  in
  let node = ModuleObject (id,sobjs) in
  (* We add the keep objects, if any, and if this isn't a functor *)
  let keep = if not (CList.is_empty m_info.cur_mbids) then [] else keep_objects id keep in
  let escape = escape_objects id escape in
  let objects = special@[node]@keep@escape in

  m_info.cur_mp, objects

let end_module () =
  let oldprefix,fs,objects = Lib.Synterp.end_module () in
  let m_info = openmod_syntax_info () in
  let olddp, id = pop_path oldprefix.obj_path in
  let mp,objects = end_module_core id m_info objects fs in

  let () = SynterpVisitor.add_leaves objects in

  assert (eq_full_path (Lib.prefix()).obj_path olddp);
  mp

let get_functor_sobjs is_mod inl (mbids,mexpr) =
  let (mbids0, aobjs) = SynterpVisitor.get_module_sobjs is_mod () inl mexpr in
  (mbids @ mbids0, aobjs)

let declare_module id args res mexpr_o =
  let fs = Summary.Synterp.freeze_summaries () in
  (* We simulate the beginning of an interactive module,
     then we adds the module parameters to the global env. *)
  let mp = ModPath.MPdot((openmod_syntax_info ()).cur_mp, Label.of_id id) in
  let args = intern_args args in
  let mbids = List.flatten @@ List.map fst args in
  let mty_entry_o = match res with
    | Enforce (mty,ann) ->
        let inl = inl2intopt ann in
        let (mte, base, kind) = Modintern.intern_module_ast Modintern.ModType mty in
        Enforce (mte, base, kind, inl)
    | Check mtys ->
      Check (build_subtypes mtys)
  in
  let mexpr_entry_o = match mexpr_o with
    | None -> None
    | Some (mexpr,ann) ->
      let (mte, base, kind) = Modintern.intern_module_ast Modintern.Module mexpr in
      Some (mte, base, kind, inl2intopt ann)
  in
  let sobjs, mp0 = match mexpr_entry_o, mty_entry_o with
    | None, Check _ -> assert false (* No body, no type ... *)
    | _, Enforce (typ,_,_,inl_res) -> get_functor_sobjs false inl_res (mbids,typ), get_module_path typ
    | Some (body, _, _, inl_expr), Check _ ->
      get_functor_sobjs true inl_expr (mbids,body), get_module_path body
  in
  (* Undo the simulated interactive building of the module
     and declare the module as a whole *)
  Summary.Synterp.unfreeze_summaries fs;

  (* We can use an empty delta resolver on syntax objects *)
  let sobjs = subst_sobjs (map_mp mp0 mp (empty_delta_resolver mp)) sobjs in
  ignore (SynterpVisitor.add_leaf (ModuleObject (id,sobjs)));
  mp, args, mexpr_entry_o, mty_entry_o

end

module Interp = struct

(** {6 Auxiliary functions concerning subtyping checks} *)

let check_sub mp mtb sub_mtb_l =
  let fold sub_mtb (cst, env) =
    let state = ((Environ.universes env, cst), Reductionops.inferred_universes) in
    let graph, cst = Subtyping.check_subtypes state env mp mtb mp sub_mtb in
    (cst, Environ.set_universes graph env)
  in
  let cst, _ = List.fold_right fold sub_mtb_l (Univ.Constraints.empty, Global.env ()) in
  Global.add_constraints cst

(** This function checks if the type calculated for the module [mp] is
    a "<:"-like subtype of all signatures in [sub_mtb_l]. Uses only
    the global environment. *)

let check_subtypes mp sub_mtb_l =
  let mb =
    try Global.lookup_module mp with Not_found -> assert false
  in
  let mtb = Modops.module_type_of_module mb in
  check_sub mp mtb sub_mtb_l

(** Same for module type [mp] *)

let check_subtypes_mt mp sub_mtb_l =
  let mtb =
    try Global.lookup_modtype mp with Not_found -> assert false
  in
  check_sub mp mtb sub_mtb_l

let current_modresolver () =
  Safe_typing.delta_of_senv @@ Global.safe_env ()

let current_struct () =
  let struc = Safe_typing.structure_body_of_safe_env @@ Global.safe_env () in
  NoFunctor (List.rev struc)

(** Prepare the module type list for check of subtypes *)

let build_subtypes env mp args mtys =
  let (ctx, ans) = List.fold_left_map
    (fun ctx (mte,base,kind,inl) ->
       let mte, ctx' = Modintern.interp_module_ast env Modintern.ModType base mte in
       let env = Environ.push_context_set ~strict:true ctx' env in
       let ctx = Univ.ContextSet.union ctx ctx' in
       let state = ((Environ.universes env, Univ.Constraints.empty), Reductionops.inferred_universes) in
       let mtb, (_, cst), _ = Mod_typing.translate_modtype state vm_state env mp inl (args,mte) in
       let ctx = Univ.ContextSet.add_constraints cst ctx in
       ctx, mtb)
    Univ.ContextSet.empty mtys
  in
  (ans, ctx)

(** Process a declaration of functor parameter(s) (Id1 .. Idn : Typ)
    i.e. possibly multiple names with the same module type.
    Global environment is updated on the fly.
    Objects in these parameters are also loaded.
    Output is accumulated on top of [acc] (in reverse order). *)

let intern_arg (acc, cst) (mbidl,(mty, base, kind, inl)) =
  let env = Global.env() in
  let (mty, cst') = Modintern.interp_module_ast env kind base mty in
  let () = Global.push_context_set cst' in
  let () =
    let state = ((Global.universes (), Univ.Constraints.empty), Reductionops.inferred_universes) in
    let _, (_, cst), _ = Mod_typing.translate_modtype state vm_state (Global.env ()) base inl ([], mty) in
    Global.add_constraints cst
  in
  let env = Global.env () in
  let sobjs = InterpVisitor.get_module_sobjs false env inl mty in
  let mp0 = get_module_path mty in
  let fold acc mbid =
    let id = MBId.to_id mbid in
    let sp = Libnames.make_path DirPath.empty id in
    let mp = MPbound mbid in
    let resolver = Global.add_module_parameter mbid mty inl in
    let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
    InterpVisitor.load_module 1 sp mp sobjs;
    (mbid,mty,inl)::acc
  in
  let acc = List.fold_left fold acc mbidl in
  (acc, Univ.ContextSet.union cst cst')

(** Process a list of declarations of functor parameters
    (Id11 .. Id1n : Typ1)..(Idk1 .. Idkm : Typk)
    Global environment is updated on the fly.
    The calls to [interp_modast] should be interleaved with these
    env updates, otherwise some "with Definition" could be rejected.
    Returns a list of mbids and entries (in reversed order).

    This used to be a [List.concat (List.map ...)], but this should
    be more efficient and independent of [List.map] eval order.
*)

let intern_args params =
  let args, ctx = List.fold_left intern_arg ([], Univ.ContextSet.empty) params in
  List.rev args, ctx

let start_module_core id args res =
  let mp = Global.start_module id in
  let params, ctx = intern_args args in
  let () = Global.push_context_set ctx in
  let env = Global.env () in
  let res_entry_o, subtyps, ctx' = match res with
    | Enforce (mte, base, kind, inl) ->
        let (mte, ctx) = Modintern.interp_module_ast env kind base mte in
        let env = Environ.push_context_set ctx env in
        (* We check immediately that mte is well-formed *)
        let state = ((Environ.universes env, Univ.Constraints.empty), Reductionops.inferred_universes) in
        let _, (_, cst), _ = Mod_typing.translate_modtype state vm_state env mp inl ([], mte) in
        let ctx = Univ.ContextSet.add_constraints cst ctx in
        Some (mte, inl), [], ctx
    | Check resl ->
      let typs, ctx = build_subtypes env mp params resl in
      None, typs, ctx
  in
  let () = Global.push_context_set ctx' in
  mp, res_entry_o, subtyps, params, Univ.ContextSet.union ctx ctx'

let start_module export id args res =
  let fs = Summary.Interp.freeze_summaries () in
  let mp, res_entry_o, subtyps, _, _ = start_module_core id args res in
  openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
  let _ : object_prefix = Lib.Interp.start_module export id mp fs in
  mp

let end_module_core id m_info objects fs =
  let {Lib.substobjs = substitute; keepobjs = keep; escapeobjs = escape; anticipateobjs = special; } = objects in

  (* For sealed modules, we use the substitutive objects of their signatures *)
  let sobjs0, keep = match m_info.cur_typ with
    | None -> ([], Objs substitute), keep
    | Some (mty, inline) ->
      InterpVisitor.get_module_sobjs false (Global.env()) inline mty, { keep_objects = [] }
  in

  let struc = current_struct () in
  let restype' = Option.map (fun (ty,inl) -> (([],ty),inl)) m_info.cur_typ in
  let state = ((Global.universes (), Univ.Constraints.empty), Reductionops.inferred_universes) in
  let _, (_, cst), _ =
    Mod_typing.finalize_module state vm_state (Global.env ()) (Global.current_modpath ())
      (struc, current_modresolver ()) restype'
  in
  let () = Global.add_constraints cst in

  let mp,mbids,resolver = Global.end_module fs id m_info.cur_typ in
  let sobjs = let (ms,objs) = sobjs0 in (mbids@ms,objs) in

  let () = check_subtypes mp m_info.cur_typs in

  (* We substitute objects if the module is sealed by a signature *)
  let sobjs =
    match m_info.cur_typ with
      | None -> sobjs
      | Some (mty, _) ->
        subst_sobjs (map_mp (get_module_path mty) mp resolver) sobjs
  in
  let node = ModuleObject (id,sobjs) in
  (* We add the keep objects, if any, and if this isn't a functor *)
  let keep = if not (CList.is_empty mbids) then [] else keep_objects id keep in
  (* NB: escape objects are added even for sealed modules, not sure if want *)
  let escape = escape_objects id escape in
  let objects = special@[node]@keep@escape in

  mp, objects

let end_module () =
  let oldprefix,fs,objects = Lib.Interp.end_module () in
  let m_info = !openmod_info in
  let _olddp, id = pop_path oldprefix.obj_path in
  let mp,objects = end_module_core id m_info objects fs in

  let () = InterpVisitor.add_leaves objects in

  (* Name consistency check : kernel vs. library *)
  assert (ModPath.equal oldprefix.obj_mp mp);

  mp

let get_functor_sobjs is_mod env inl (params,mexpr) =
  let (mbids, aobjs) = InterpVisitor.get_module_sobjs is_mod env inl mexpr in
  (List.map pi1 params @ mbids, aobjs)

(* TODO cleanup push universes directly to global env *)
let declare_module id args res mexpr_o =
  let fs = Summary.Interp.freeze_summaries () in
  (* We simulate the beginning of an interactive module,
     then we adds the module parameters to the global env. *)
  let mp, mty_entry_o, subs, params, ctx = start_module_core id args res in
  let env = Global.env () in
  let mexpr_entry_o, inl_expr, ctx' = match mexpr_o with
    | None -> None, default_inline (), Univ.ContextSet.empty
    | Some (mte, base, kind, inl) ->
      let (mte, ctx) = Modintern.interp_module_ast env kind base mte in
      Some mte, inl, ctx
  in
  let env = Environ.push_context_set ctx' env in
  let ctx = Univ.ContextSet.union ctx ctx' in
  let entry, inl_res = match mexpr_entry_o, mty_entry_o with
    | None, None -> assert false (* No body, no type ... *)
    | None, Some (typ, inl) -> MType (params, typ), inl
    | Some body, otyp -> MExpr (params, body, Option.map fst otyp), Option.cata snd (default_inline ()) otyp
  in
  let sobjs, mp0 = match entry with
    | MType (_,mte) | MExpr (_,_,Some mte) ->
      get_functor_sobjs false env inl_res (params,mte), get_module_path mte
    | MExpr (_,me,None) ->
      get_functor_sobjs true env inl_expr (params,me), get_module_path me
  in
  (* Undo the simulated interactive building of the module
     and declare the module as a whole *)
  Summary.Interp.unfreeze_summaries fs;
  let inl = match inl_expr with
  | None -> None
  | _ -> inl_res
  in
  let () = Global.push_context_set ctx in
  let state = ((Global.universes (), Univ.Constraints.empty), Reductionops.inferred_universes) in
  let _, (_, cst), _ = Mod_typing.translate_module state vm_state (Global.env ()) mp inl entry in
  let () = Global.add_constraints cst in
  let mp_env,resolver = Global.add_module id entry inl in

  (* Name consistency check : kernel vs. library *)
  assert (ModPath.equal mp (mp_of_kn (Lib.make_kn id)));
  assert (ModPath.equal mp mp_env);

  let () = check_subtypes mp subs in

  let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
  InterpVisitor.add_leaf (ModuleObject (id,sobjs));
  mp

end

end

(** {6 Module types : start, end, declare} *)

module RawModTypeOps = struct

module Synterp = struct

let start_modtype_core id cur_mp args mtys =
  let mp = ModPath.MPdot(cur_mp, Label.of_id id) in
  let args = RawModOps.Synterp.intern_args args in
  let mbids = List.flatten @@ List.map (fun (mbidl,_) -> mbidl) args in
  let sub_mty_l = RawModOps.Synterp.build_subtypes mtys in
  mp, mbids, args, sub_mty_l

let start_modtype id args mtys =
  let fs = Summary.Synterp.freeze_summaries () in
  let mp, mbids, args, sub_mty_l = start_modtype_core id (openmod_syntax_info ()).cur_mp args mtys in
  set_openmod_syntax_info { cur_mp = mp; cur_typ = None; cur_mbids = mbids };
  let prefix = Lib.Synterp.start_modtype id mp fs in
  Nametab.(push_dir (Until 1) (prefix.obj_path) (GlobDirRef.DirOpenModtype prefix.obj_mp));
  mp, args, sub_mty_l

let end_modtype_core id mbids objects fs =
  let {Lib.substobjs = substitute; keepobjs = _; escapeobjs = escape; anticipateobjs = special; } = objects in
  Summary.Synterp.unfreeze_summaries fs;
  let modtypeobjs = (mbids, Objs substitute) in
  special@[ModuleTypeObject (id,modtypeobjs)]@(escape_objects id escape)

let end_modtype () =
  let oldprefix,fs,objects = Lib.Synterp.end_modtype () in
  let _olddp, id = pop_path oldprefix.obj_path in
  let objects = end_modtype_core id (openmod_syntax_info ()).cur_mbids objects fs in
  SynterpVisitor.add_leaves objects;
  (openmod_syntax_info ()).cur_mp

let declare_modtype id args mtys (mty,ann) =
  let fs = Summary.Synterp.freeze_summaries () in
  let inl = inl2intopt ann in
  (* We simulate the beginning of an interactive module,
     then we adds the module parameters to the global env. *)
  let mp, mbids, args, sub_mty_l = start_modtype_core id (openmod_syntax_info ()).cur_mp args mtys in
  let mte, base, kind = Modintern.intern_module_ast Modintern.ModType mty in
  let entry = mbids, mte in
  let sobjs = RawModOps.Synterp.get_functor_sobjs false inl entry in
  let subst = map_mp (get_module_path (snd entry)) mp (empty_delta_resolver mp) in
  let sobjs = subst_sobjs subst sobjs in

  (* Undo the simulated interactive building of the module type
     and declare the module type as a whole *)
  Summary.Synterp.unfreeze_summaries fs;
  ignore (SynterpVisitor.add_leaf (ModuleTypeObject (id,sobjs)));
  mp, args, (mte, base, kind, inl), sub_mty_l

end

module Interp = struct

let openmodtype_info =
  Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO"

let start_modtype_core id args mtys =
  let mp = Global.start_modtype id in
  let params, params_ctx = RawModOps.Interp.intern_args args in
  let () = Global.push_context_set params_ctx in
  let env = Global.env () in
  let sub_mty_l, sub_mty_ctx = RawModOps.Interp.build_subtypes env mp params mtys in
  let () = Global.push_context_set sub_mty_ctx in
  mp, params, sub_mty_l, Univ.ContextSet.union params_ctx sub_mty_ctx

let start_modtype id args mtys =
  let fs = Summary.Interp.freeze_summaries () in
  let mp, _, sub_mty_l, _ = start_modtype_core id args mtys in
  openmodtype_info := sub_mty_l;
  let prefix = Lib.Interp.start_modtype id mp fs in
  Nametab.(push_dir (Until 1) (prefix.obj_path) (GlobDirRef.DirOpenModtype mp));
  mp

let end_modtype_core id sub_mty_l objects fs =
  let {Lib.substobjs = substitute; keepobjs = _; escapeobjs = escape; anticipateobjs = special; } = objects in
  let mp, mbids = Global.end_modtype fs id in
  let () = RawModOps.Interp.check_subtypes_mt mp sub_mty_l in
  let modtypeobjs = (mbids, Objs substitute) in
  let objects = special@[ModuleTypeObject (id,modtypeobjs)]@(escape_objects id escape) in
  mp, objects

let end_modtype () =
  let oldprefix,fs,objects = Lib.Interp.end_modtype () in
  let olddp, id = pop_path oldprefix.obj_path in
  let sub_mty_l = !openmodtype_info in
  let mp, objects = end_modtype_core id sub_mty_l objects fs in
  let () = InterpVisitor.add_leaves objects in
  (* Check name consistence : start_ vs. end_modtype, kernel vs. library *)
  assert (eq_full_path (Lib.prefix()).obj_path olddp);
  assert (ModPath.equal oldprefix.obj_mp mp);
  mp

let declare_modtype id args mtys (mte,base,kind,inl) =
  let fs = Summary.Interp.freeze_summaries () in
  (* We simulate the beginning of an interactive module,
     then we adds the module parameters to the global env. *)
  let mp, params, sub_mty_l, ctx = start_modtype_core id args mtys in
  let env = Global.env () in
  let mte, mte_ctx = Modintern.interp_module_ast env kind base mte in
  let () = Global.push_context_set mte_ctx in
  let env = Global.env () in
  (* We check immediately that mte is well-formed *)
  let state = ((Global.universes (), Univ.Constraints.empty), Reductionops.inferred_universes) in
  let _, (_, mte_cst), _ = Mod_typing.translate_modtype state vm_state env mp inl ([], mte) in
  let () = Global.push_context_set (Univ.Level.Set.empty,mte_cst) in
  let entry = params, mte in
  let env = Global.env () in
  let sobjs = RawModOps.Interp.get_functor_sobjs false env inl entry in
  let subst = map_mp (get_module_path (snd entry)) mp (empty_delta_resolver mp) in
  let sobjs = subst_sobjs subst sobjs in

  (* Undo the simulated interactive building of the module type
     and declare the module type as a whole *)
  Summary.Interp.unfreeze_summaries fs;

  (* We enrich the global environment *)
  let () = Global.push_context_set ctx in
  let () = Global.push_context_set mte_ctx in
  let () = Global.push_context_set (Univ.Level.Set.empty,mte_cst) in
  let mp_env = Global.add_modtype id entry inl in

  (* Name consistency check : kernel vs. library *)
  assert (ModPath.equal mp_env mp);

  (* Subtyping checks *)
  let () = RawModOps.Interp.check_subtypes_mt mp sub_mty_l in

  InterpVisitor.add_leaf (ModuleTypeObject (id, sobjs));
  mp

end

end

(** {6 Include} *)

module RawIncludeOps = struct

exception NoIncludeSelf

module Synterp = struct

let rec include_subst mp mbids = match mbids with
  | [] -> empty_subst
  | mbid::mbids ->
    let subst = include_subst mp mbids in
    join (map_mbid mbid mp (empty_delta_resolver mp)) subst

let declare_one_include_core cur_mp (me_ast,annot) =
  let me, base, kind = Modintern.intern_module_ast Modintern.ModAny me_ast in
  let is_mod = (kind == Modintern.Module) in
  let inl = inl2intopt annot in
  let mbids,aobjs = SynterpVisitor.get_module_sobjs is_mod () inl me in
  let subst_self =
    try
      if List.is_empty mbids then raise NoIncludeSelf;
      include_subst cur_mp mbids
    with NoIncludeSelf -> empty_subst
  in
  let base_mp = get_module_path me in
  (* We can use an empty delta resolver on syntax objects *)
  let subst = join subst_self (map_mp base_mp cur_mp (empty_delta_resolver cur_mp)) in
  let aobjs = subst_aobjs subst aobjs in
  (me, base, kind, inl), aobjs

let declare_one_include (me_ast,annot) =
  let res, aobjs = declare_one_include_core (openmod_syntax_info ()).cur_mp (me_ast,annot) in
  SynterpVisitor.add_leaf (IncludeObject aobjs);
  res

let declare_include me_asts = List.map declare_one_include me_asts

end

module Interp = struct

let rec include_subst env mp reso mbids sign inline = match mbids with
  | [] -> empty_subst
  | mbid::mbids ->
    let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
    let subst = include_subst env mp reso mbids fbody_b inline in
    let mp_delta =
      Modops.inline_delta_resolver env inline mp farg_id farg_b reso
    in
    join (map_mbid mbid mp mp_delta) subst

let rec decompose_functor mpl typ =
  match mpl, typ with
  | [], _ -> typ
  | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str
  | _ -> user_err Pp.(str "Application of a functor with too much arguments.")

let type_of_incl env is_mod = function
  | MEident mp -> type_of_mod mp env is_mod
  | MEapply _ as me ->
    let mp0, mp_l = InterpVisitor.get_applications me in
    decompose_functor mp_l (type_of_mod mp0 env is_mod)
  | MEwith _ -> raise NoIncludeSelf

(** Implements [Include F] where [F] has parameters [mbids] to be
    instantiated by fields of the current "self" module, i.e. using
    subtyping, by the current module itself. *)

let declare_one_include_core (me,base,kind,inl) =
  let env = Global.env() in
  let me, cst = Modintern.interp_module_ast env kind base me in
  let () = Global.push_context_set cst in
  let env = Global.env () in
  let is_mod = (kind == Modintern.Module) in
  let cur_mp = Global.current_modpath () in
  let mbids,aobjs = InterpVisitor.get_module_sobjs is_mod env inl me in
  let subst_self =
    try
      if List.is_empty mbids then raise NoIncludeSelf;
      let typ = type_of_incl env is_mod me in
      let reso = RawModOps.Interp.current_modresolver () in
      include_subst env cur_mp reso mbids typ inl
    with NoIncludeSelf -> empty_subst
  in
  let base_mp = get_module_path me in

  let state = ((Global.universes (), Univ.Constraints.empty), Reductionops.inferred_universes) in
  let sign, (), resolver, (_, cst), _ =
    Mod_typing.translate_mse_include is_mod state vm_state (Global.env ()) (Global.current_modpath ()) inl me
  in
  let () = Global.add_constraints cst in
  let () = assert (ModPath.equal cur_mp (Global.current_modpath ())) in
  (* Include Self support  *)
  let mb = make_module_type (RawModOps.Interp.current_struct ()) (RawModOps.Interp.current_modresolver ()) in
  let rec compute_sign sign =
    match sign with
    | MoreFunctor(mbid,mtb,str) ->
      let state = ((Global.universes (), Univ.Constraints.empty), Reductionops.inferred_universes) in
      let (_, cst) = Subtyping.check_subtypes state (Global.env ()) cur_mp mb (MPbound mbid) mtb in
      let () = Global.add_constraints cst in
      let mpsup_delta = match mod_global_delta mb with
      | None -> assert false (* mb is guaranteed not to be a functor here *)
      | Some delta ->
        Modops.inline_delta_resolver (Global.env ()) inl cur_mp mbid mtb delta
      in
      let subst = Mod_subst.map_mbid mbid cur_mp mpsup_delta in
      compute_sign (Modops.subst_signature subst cur_mp str)
    | NoFunctor str -> ()
  in
  let () = compute_sign sign in

  let resolver = Global.add_include me is_mod inl in
  let subst = join subst_self (map_mp base_mp cur_mp resolver) in
  subst_aobjs subst aobjs

let declare_one_include (me,base,kind,inl) =
  let aobjs = declare_one_include_core (me,base,kind,inl) in
  InterpVisitor.add_leaf (IncludeObject aobjs)

let declare_include me_asts = List.iter declare_one_include me_asts

end

end

(** {6 Libraries} *)

type library_name = DirPath.t

(** A library object is made of some substitutive objects
    and some "keep" and "escape" objects. *)

type library_objects = Libobject.t list * keep_objects * escape_objects

module Synterp = struct

let start_module export id args res =
  RawModOps.Synterp.start_module export id args res

let end_module = RawModOps.Synterp.end_module

(** Declare a module in terms of a list of module bodies, by including them.
Typically used for `Module M := N <+ P`.
*)
let declare_module_includes id args res mexpr_l =
  let fs = Summary.Synterp.freeze_summaries () in
  let mp, res_entry_o, mbids, sign, args = RawModOps.Synterp.start_module_core id args res in
  let mod_info = { cur_mp = mp; cur_typ = res_entry_o; cur_mbids = mbids } in
  let includes = List.map_left (RawIncludeOps.Synterp.declare_one_include_core mp) mexpr_l in
  let bodies, incl_objs = List.split includes in
  let incl_objs = List.map (fun x -> IncludeObject x) incl_objs in
  let objects = {
    Lib.substobjs = incl_objs;
    keepobjs = { keep_objects = [] };
    escapeobjs = { escape_objects = [] };
    anticipateobjs = [];
  } in
  let mp, objects = RawModOps.Synterp.end_module_core id mod_info objects fs in
  SynterpVisitor.add_leaves objects;
  mp, args, bodies, sign

(** Declare a module type in terms of a list of module bodies, by including them.
Typically used for `Module Type M := N <+ P`.
*)
let declare_modtype_includes id args res mexpr_l =
  let fs = Summary.Synterp.freeze_summaries () in
  let mp, mbids, args, subtyps = RawModTypeOps.Synterp.start_modtype_core id (openmod_syntax_info ()).cur_mp args res in
  let includes = List.map_left (RawIncludeOps.Synterp.declare_one_include_core mp) mexpr_l in
  let bodies, incl_objs = List.split includes in
  let incl_objs = List.map (fun x -> IncludeObject x) incl_objs in
  let objects = {
    Lib.substobjs = incl_objs;
    keepobjs = { keep_objects = [] };
    escapeobjs = { escape_objects = [] };
    anticipateobjs = [];
  } in
  let objects = RawModTypeOps.Synterp.end_modtype_core id mbids objects fs in
  SynterpVisitor.add_leaves objects;
  mp, args, bodies, subtyps

let declare_module id args mtys me_l =
  match me_l with
  | [] ->
    let mp, args, body, sign = RawModOps.Synterp.declare_module id args mtys None in
    assert (Option.is_empty body);
    mp, args, [], sign
  | [me] ->
    let mp, args, body, sign = RawModOps.Synterp.declare_module id args mtys (Some me) in
    mp, args, [Option.get body], sign
  | me_l -> declare_module_includes id args mtys me_l

let start_modtype id args mtys =
  RawModTypeOps.Synterp.start_modtype id args mtys

let end_modtype = RawModTypeOps.Synterp.end_modtype

let declare_modtype id args mtys mty_l =
  match mty_l with
    | [] -> assert false
    | [mty] ->
      let mp, args, body, sign = RawModTypeOps.Synterp.declare_modtype id args mtys mty in
      mp, args, [body], sign
    | mty_l -> declare_modtype_includes id args mtys mty_l

let declare_include = RawIncludeOps.Synterp.declare_include

let register_library dir (objs:library_objects) =
  let mp = MPfile dir in
  let sp = path_of_file dir in
  let sobjs,keepobjs,escapeobjs = objs in
  SynterpVisitor.load_module 1 sp mp ([],Objs sobjs);
  SynterpVisitor.load_escape 2 sp mp escapeobjs;
  SynterpVisitor.load_keep 2 sp mp keepobjs

let import_modules = SynterpVisitor.import_modules

let import_module f ~export mp =
  import_modules ~export [f,mp]

let close_section = SynterpVisitor.close_section

end

module Interp = struct

let start_module = RawModOps.Interp.start_module

let end_module = RawModOps.Interp.end_module

(** Declare a module in terms of a list of module bodies, by including them.
Typically used for `Module M := N <+ P`.
*)
let declare_module_includes id args res mexpr_l =
  let fs = Summary.Interp.freeze_summaries () in
  let mp, res_entry_o, subtyps, _, _ = RawModOps.Interp.start_module_core id args res in
  let mod_info = { cur_typ = res_entry_o; cur_typs = subtyps } in
  let incl_objs = List.map_left (fun x -> IncludeObject (RawIncludeOps.Interp.declare_one_include_core x)) mexpr_l in
  let objects = {
    Lib.substobjs = incl_objs;
    keepobjs = { keep_objects = [] };
    escapeobjs = { escape_objects = [] };
    anticipateobjs = [];
  } in
  let mp, objects = RawModOps.Interp.end_module_core id mod_info objects fs in
  InterpVisitor.add_leaves objects;
  mp

(** Declare a module type in terms of a list of module bodies, by including them.
Typically used for `Module Type M := N <+ P`.
*)
let declare_modtype_includes id args res mexpr_l =
  let fs = Summary.Interp.freeze_summaries () in
  let mp, _, subtyps, _ = RawModTypeOps.Interp.start_modtype_core id args res in
  let incl_objs = List.map_left (fun x -> IncludeObject (RawIncludeOps.Interp.declare_one_include_core x)) mexpr_l in
  let objects = {
    Lib.substobjs = incl_objs;
    keepobjs = { keep_objects = [] };
    escapeobjs = { escape_objects = [] };
    anticipateobjs = [];
  } in
  let mp, objects = RawModTypeOps.Interp.end_modtype_core id subtyps objects fs in
  InterpVisitor.add_leaves objects;
  mp

let declare_module id args mtys me_l =
  match me_l with
  | [] -> RawModOps.Interp.declare_module id args mtys None
  | [me] -> RawModOps.Interp.declare_module id args mtys (Some me)
  | me_l -> declare_module_includes id args mtys me_l

let start_modtype = RawModTypeOps.Interp.start_modtype

let end_modtype = RawModTypeOps.Interp.end_modtype

let declare_modtype id args mtys mty_l =
  match mty_l with
  | [] -> assert false
  | [mty] -> RawModTypeOps.Interp.declare_modtype id args mtys mty
  | mty_l -> declare_modtype_includes id args mtys mty_l

let declare_include me_asts =
  if Lib.sections_are_opened () then
    user_err Pp.(str "Include is not allowed inside sections.");
  RawIncludeOps.Interp.declare_include me_asts

let register_library dir cenv (objs:library_objects) digest vmtab =
  let mp = MPfile dir in
  let sp = path_of_file dir in
  let () =
    try
      (* If the library was loaded inside a module or section, the
         end_segment will replay the library object for non-kernel
         effects but the kernel did not forget the library. *)
      ignore(Global.lookup_module mp);
    with Not_found ->
      begin
      let mp' = Global.import cenv vmtab digest in
      if not (ModPath.equal mp mp') then
        anomaly (Pp.str "Unexpected disk module name.")
      end
  in
  let sobjs,keepobjs,escapeobjs = objs in
  InterpVisitor.load_module 1 sp mp ([],Objs sobjs);
  InterpVisitor.load_escape 1 sp mp escapeobjs;
  InterpVisitor.load_keep 1 sp mp keepobjs

let import_modules = InterpVisitor.import_modules

let import_module f ~export mp =
  import_modules ~export [f,mp]

let close_section = InterpVisitor.close_section

end

let end_library_hook = ref []
let append_end_library_hook f =
  end_library_hook := f :: !end_library_hook

let end_library_hook () =
  List.iter (fun f -> f ()) (List.rev !end_library_hook)

let end_library ~output_native_objects dir =
  end_library_hook();
  let { Lib.info; interp_objects = lib_stack; synterp_objects = lib_stack_syntax; } =
    Lib.end_compilation dir
  in
  let mp,cenv,vmlib,ast = Global.export ~output_native_objects dir in
  assert (ModPath.equal mp (MPfile dir));
  let drop_anticipate {Lib.substobjs; keepobjs; escapeobjs; anticipateobjs=_} =
    (substobjs, keepobjs, escapeobjs)
  in
  cenv,(drop_anticipate lib_stack),(drop_anticipate lib_stack_syntax),vmlib,ast,info

(** {6 Iterators} *)

let iter_all_interp_segments f =
  let rec apply_obj prefix obj = match obj with
    | IncludeObject aobjs ->
      let objs = InterpVisitor.expand_aobjs aobjs in
      List.iter (apply_obj prefix) objs
    | _ -> f prefix obj
  in
  let rec subst_view (obj : exp_substituted_object) : Libobject.t = match obj with
  | KeepObject (_, o) | EscapeObject (_, o) -> Empty.abort o
  | (AtomicObject _ | ExportObject _ | ModuleObject _ | ModuleTypeObject _) as o -> o
  | IncludeObject aobjs ->
    let aobjs = aobjs.exp_algebraic_objects in
    IncludeObject (Objs (List.map subst_view aobjs))
  in
  let apply_mod_obj _ modobjs =
    let prefix = modobjs.module_prefix in
    List.iter (fun obj -> apply_obj prefix (subst_view obj)) modobjs.module_substituted_objects;
    List.iter (fun obj -> apply_obj prefix obj) modobjs.module_keep_objects.keep_objects
  in
  let apply_nodes (node, os) = List.iter (fun o -> apply_obj (Lib.node_prefix node) o) os in
  MPmap.iter apply_mod_obj (InterpVisitor.ModObjs.all ());
  List.iter apply_nodes (Lib.contents ())

(** {6 Some types used to shorten declaremods.mli} *)

type module_params = (lident list * (Constrexpr.module_ast * inline)) list
type module_expr = (Modintern.module_struct_expr * ModPath.t * Modintern.module_kind * Entries.inline)
type module_params_expr = (MBId.t list * module_expr) list

(** {6 Debug} *)

let debug_print_modtab () = InterpVisitor.debug_print_modtab ()

(** For printing modules, [process_module_binding] adds names of
    bound module (and its components) to Nametab. It also loads
    objects associated to it. *)

let process_module_binding mbid me =
  let sp = Libnames.make_path DirPath.empty (MBId.to_id mbid) in
  let mp = MPbound mbid in
  let sobjs = InterpVisitor.get_module_sobjs false (Global.env()) (default_inline ()) me in
  let subst = map_mp (get_module_path me) mp (empty_delta_resolver mp) in
  let sobjs = subst_sobjs subst sobjs in
  SynterpVisitor.load_module 1 sp mp sobjs;
  InterpVisitor.load_module 1 sp mp sobjs

(** Compatibility layer *)
let import_module f ~export mp =
  Synterp.import_module f ~export mp;
  Interp.import_module f ~export mp

let declare_module id args mtys me_l =
  let mp, args, bodies, sign = Synterp.declare_module id args mtys me_l in
  Interp.declare_module id args sign bodies

let start_module export id args res =
  let mp, args, sign = Synterp.start_module export id args res in
  Interp.start_module export id args sign

let end_module () =
  let _mp = Synterp.end_module () in
  Interp.end_module ()

let declare_modtype id args mtys mty_l =
  let mp, args, bodies, subtyps = Synterp.declare_modtype id args mtys mty_l in
  Interp.declare_modtype id args subtyps bodies

let start_modtype id args mtys =
  let mp, args, sub_mty_l = Synterp.start_modtype id args mtys in
  Interp.start_modtype id args sub_mty_l

let end_modtype () =
  let _mp = Synterp.end_modtype () in
  Interp.end_modtype ()

let declare_include me_asts =
  let l = Synterp.declare_include me_asts in
  Interp.declare_include l

let () = append_end_library_hook Profile_tactic.do_print_results_at_close

quality100%

¤ Dauer der Verarbeitung: 0.44 Sekunden ¤

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.