Quellcode-Bibliothek vernacentries.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)         *)
(************************************************************************)

(* Concrete syntax of the mathematical vernacular MV V2.6 *)

open Pp
open CErrors
open CAst
open Util
open Names
open Printer
open Goptions
open Libnames
open Vernacexpr
open Locality
open Attributes
open Synterp

module NamedDecl = Context.Named.Declaration

(* Utility functions, at some point they should all disappear and
   instead enviroment/state selection should be done at the Vernac DSL
   level. *)

let get_current_or_global_context ~pstate =
  match pstate with
  | None -> let env = Global.env () in Evd.(from_env env, env)
  | Some p -> Declare.Proof.get_current_context p

let get_goal_or_global_context ~pstate glnum =
  match pstate with
  | None -> let env = Global.env () in Evd.(from_env env, env)
  | Some p -> Declare.Proof.get_goal_context p glnum

let cl_of_qualid = function
  | FunClass -> Coercionops.CL_FUN
  | SortClass -> Coercionops.CL_SORT
  | RefClass r -> ComCoercion.class_of_global (Smartlocate.smart_global ~head:true r)

let scope_class_of_qualid qid =
  Notation.scope_class_of_class (cl_of_qualid qid)

(** Standard attributes for definition-like commands. *)
module DefAttributes = struct
  type t = {
    scope : definition_scope;
    locality : bool option;
    polymorphic : bool;
    program : bool;
    user_warns : Globnames.extended_global_reference UserWarn.with_qf option;
    canonical_instance : bool;
    typing_flags : Declarations.typing_flags option;
    using : Vernacexpr.section_subset_expr option;
    reversible : bool;
    clearbody: bool option;
  }
  (* [locality] is used for [vernac_definition_hook],
     the raw Local/Global attribute is also used to generate [scope].
     [locality] can't be computed back from [scope]
     because [Let Coercion] outside section generates [locality = None]
     but [scope = Global ImportNeedQualified]
     (which is otherwise associated with [locality = Some true]).

     Since [Let] (ie discharge = DoDischarge) does not allow explicit locality
     we could alternatively decide to change the default locality
     of the coercion from out-of-section [Let Coercion].
  *)

  let importability_of_bool = function
    | true -> ImportNeedQualified
    | false -> ImportDefaultBehavior

  let warn_declaration_outside_section =
    CWarnings.create ~name:"declaration-outside-section"
      ~category:CWarnings.CoreCategories.vernacular
      ~default:CWarnings.AsError
      Pp.(fun (unexpected_thing, replacement) ->
          strbrk "Use of " ++ str unexpected_thing
          ++ strbrk " outside sections behaves as " ++ str replacement ++ str ".")

  let scope_of_locality locality_flag discharge deprecated_thing replacement : definition_scope =
    let open Vernacexpr in
    match locality_flag, discharge with
    | Some b, NoDischarge -> Global (importability_of_bool b)
    | None, NoDischarge -> Global ImportDefaultBehavior
    | None, DoDischarge when not (Lib.sections_are_opened ()) ->
      (* If a Let/Variable is defined outside a section, then we consider it as a local definition *)
      warn_declaration_outside_section (deprecated_thing, replacement);
      Global ImportNeedQualified
    | None, DoDischarge -> Discharge
    | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case")
    | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case")

  open Attributes
  open Attributes.Notations

  let clearbody = bool_attribute ~name:"clearbody"

  (* [XXX] EJGA: coercion is unused here *)
  let def_attributes_gen ?(coercion=false) ?(discharge=NoDischarge,"","") () =
    let discharge, deprecated_thing, replacement = discharge in
    let clearbody = match discharge with DoDischarge -> clearbody | NoDischarge -> return None in
    (locality ++ user_warns_with_use_globref_instead ++ polymorphic ++ program ++
               canonical_instance ++ typing_flags ++ using ++
               reversible ++ clearbody) >>= fun ((((((((locality, user_warns), polymorphic), program),
           canonical_instance), typing_flags), using),
           reversible), clearbody) ->
      let using = Option.map Proof_using.using_from_string using in
      let reversible = Option.default false reversible in
      let () = if Option.has_some clearbody && not (Lib.sections_are_opened())
        then CErrors.user_err Pp.(str "Cannot use attribute clearbody outside sections.")
      in
      let scope = scope_of_locality locality discharge deprecated_thing replacement in
      return { scope; locality; polymorphic; program; user_warns; canonical_instance; typing_flags; using; reversible; clearbody }

  let parse ?coercion ?discharge f =
    Attributes.parse (def_attributes_gen ?coercion ?discharge ()) f

  let def_attributes = def_attributes_gen ()

end

let with_def_attributes ?coercion ?discharge ~atts f =
  let atts = DefAttributes.parse ?coercion ?discharge atts in
  if atts.DefAttributes.program then Declare.Obls.check_program_libraries ();
  f ~atts

let with_section_locality ~atts f =
  let local = Attributes.(parse locality atts) in
  let section_local = make_section_locality local in
  f ~section_local

(*******************)
(* "Show" commands *)

let show_proof ~pstate =
  (* spiwack: this would probably be cooler with a bit of polishing. *)
  try
    let pstate = Option.get pstate in
    let p = Declare.Proof.get pstate in
    let sigma, _ = Declare.Proof.get_current_context pstate in
    let pprf = Proof.partial_proof p in
    (* In the absence of an environment explicitly attached to the
       proof and on top of which side effects of the proof would be pushed, ,
       we take the global environment which in practise should be a
       superset of the initial environment in which the proof was
       started *)
    let env = Global.env() in
    Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
  (* We print nothing if there are no goals left *)
  with
  | Proof.NoSuchGoal _
  | Option.IsNone ->
    user_err (str "No goals to show.")

let show_top_evars ~proof =
  (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
  let Proof.{goals; sigma} = Proof.data proof in
  let shelf = Evd.shelf sigma in
  let given_up = Evar.Set.elements @@ Evd.given_up sigma in
  pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)

let show_universes ~proof =
  let Proof.{goals;sigma} = Proof.data proof in
  let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in
  UState.pr (Evd.ustate sigma) ++ fnl () ++
  v 1 (str "Normalized constraints:" ++ cut() ++
       Univ.ContextSet.pr (Termops.pr_evd_level sigma) ctx)

(* Simulate the Intro(s) tactic *)
let show_intro ~proof all =
  let open EConstr in
  let Proof.{goals;sigma} = Proof.data proof in
  if not (List.is_empty goals) then begin
    let evi = Evd.find_undefined sigma (List.hd goals) in
    let env = Evd.evar_filtered_env (Global.env ()) evi in
    let l,_= decompose_prod_decls sigma (Termops.strip_outer_cast sigma (Evd.evar_concl evi)) in
    if all then
      let lid = Tactics.find_intro_names env sigma l in
      hov 0 (prlist_with_sep  spc Id.print lid)
    else if not (List.is_empty l) then
      let n = List.last l in
      Id.print (List.hd (Tactics.find_intro_names env sigma [n]))
    else mt ()
  end else mt ()

(** Textual display of a generic "match" template *)

let show_match id =
  let patterns =
    try ComInductive.make_cases (Nametab.global_inductive id)
    with Not_found -> user_err Pp.(str "Unknown inductive type.")
  in
  let pr_branch l =
    str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>"
  in
  v 1 (str "match # with" ++ fnl () ++
       prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ())

(* "Print" commands *)

let print_loadpath dir =
  let l = Loadpath.get_load_paths () in
  let l = match dir with
  | None -> l
  | Some dir ->
    let filter p = is_dirpath_prefix_of dir (Loadpath.logical p) in
    List.filter filter l
  in
  str "Installed / Logical Path / Physical path:" ++ fnl () ++
    prlist_with_sep fnl Loadpath.pp l

let print_libraries () =
  let loaded = Library.loaded_libraries () in
  str"Loaded library files: " ++
  pr_vertical_list DirPath.print loaded


let print_module qid =
  match Nametab.locate_module qid with
  | mp -> Printmod.print_module ~with_body:true mp
  | exception Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid ++ str".")

let print_modtype qid =
  try
    let kn = Nametab.locate_modtype qid in
    Printmod.print_modtype kn
  with Not_found ->
    (* Is there a module of this name ? If yes we display its type *)
    try
      let mp = Nametab.locate_module qid in
      Printmod.print_module ~with_body:false mp
    with Not_found ->
      user_err (str"Unknown Module Type or Module " ++ pr_qualid qid ++ str".")

let print_namespace ~pstate ns =
  let ns = List.rev (Names.DirPath.repr ns) in
  (* [match_dirpath], [match_modulpath] are helpers for [matches]
     which checks whether a constant is in the namespace [ns]. *)
  let rec match_dirpath ns = function
    | [] -> Some ns
    | id::dir ->
        begin match match_dirpath ns dir with
        | Some [] as y -> y
        | Some (a::ns') ->
            if Names.Id.equal a id then Some ns'
            else None
        | None -> None
        end
  in
  let rec match_modulepath ns = function
    | MPbound _ -> None (* Not a proper namespace. *)
    | MPfile dir -> match_dirpath ns (Names.DirPath.repr dir)
    | MPdot (mp,lbl) ->
        let id = Names.Label.to_id lbl in
        begin match match_modulepath ns mp with
        | Some [] as y -> y
        | Some (a::ns') ->
            if Names.Id.equal a id then Some ns'
            else None
        | None -> None
        end
  in
  (* [qualified_minus n mp] returns a list of qualifiers representing
     [mp] except the [n] first (in the concrete syntax order).  The
     idea is that if [mp] matches [ns], then [qualified_minus mp
     (length ns)] will be the correct representation of [mp] assuming
     [ns] is imported. *)
  (* precondition: [mp] matches some namespace of length [n] *)
  let qualified_minus n mp =
    let rec list_of_modulepath = function
      | MPbound _ -> assert false (* MPbound never matches *)
      | MPfile dir -> Names.DirPath.repr dir
      | MPdot (mp,lbl) -> (Names.Label.to_id lbl)::(list_of_modulepath mp)
    in
    snd (Util.List.chop n (List.rev (list_of_modulepath mp)))
  in
  let print_list pr l = prlist_with_sep (fun () -> str".") pr l in
  let print_kn kn =
    let (mp,lbl) = Names.KerName.repr kn in
    let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in
    print_list Id.print qn
  in
  let print_constant ~pstate k body =
    (* FIXME: universes *)
    let t = body.Declarations.const_type in
    let sigma, env = get_current_or_global_context ~pstate in
    print_kn k ++ str":" ++ spc() ++ Printer.pr_type_env env sigma t
  in
  let matches mp = match match_modulepath ns mp with
  | Some [] -> true
  | _ -> false in
  let constants_in_namespace =
    Environ.fold_constants (fun c body acc ->
        let kn = Constant.user c in
        if matches (KerName.modpath kn)
        then acc++fnl()++hov 2 (print_constant ~pstate kn body)
        else acc)
      (Global.env ()) (str"")
  in
  (print_list Id.print ns)++str":"++fnl()++constants_in_namespace

let print_strategy r =
  let open Conv_oracle in
  let pr_level = function
  | Expand -> str "expand"
  | Level 0 -> str "transparent"
  | Level n -> str "level" ++ spc() ++ int n
  | Opaque -> str "opaque"
  in
  let pr_strategy (ref, lvl) = pr_global ref ++ str " : " ++ pr_level lvl in
  let oracle = Environ.oracle (Global.env ()) in
  match r with
  | None ->
    let fold key lvl (vacc, cacc, pacc) = match key with
    | Conv_oracle.EvalVarRef id -> ((GlobRef.VarRef id, lvl) :: vacc, cacc, pacc)
    | Conv_oracle.EvalConstRef cst -> (vacc, (GlobRef.ConstRef cst, lvl) :: cacc, pacc)
    | Conv_oracle.EvalProjectionRef p -> (vacc, cacc, (GlobRef.ConstRef (Projection.Repr.constant p), lvl) :: pacc)
    in
    let var_lvl, cst_lvl, prj_lvl = fold_strategy fold oracle ([], [], []) in
    let var_msg =
      if List.is_empty var_lvl then mt ()
      else str "Variable strategies" ++ fnl () ++
        hov 0 (prlist_with_sep fnl pr_strategy var_lvl) ++ fnl ()
    in
    let cst_msg =
      if List.is_empty cst_lvl then mt ()
      else str "Constant strategies" ++ fnl () ++
        hov 0 (prlist_with_sep fnl pr_strategy cst_lvl)
    in
    let prj_msg =
      if List.is_empty prj_lvl then mt ()
      else str "Projection strategies" ++ fnl () ++
        hov 0 (prlist_with_sep fnl pr_strategy prj_lvl)
    in
    var_msg ++ cst_msg ++ prj_msg
  | Some r ->
    let r = Smartlocate.smart_global r in
    let key = let open GlobRef in match r with
    | VarRef id -> Evaluable.EvalVarRef id
    | ConstRef cst -> Evaluable.EvalConstRef cst
    | IndRef _ | ConstructRef _ -> user_err Pp.(str "The reference is not unfoldable.")
    in
    let lvl = get_strategy oracle (Evaluable.to_kevaluable key) in
    pr_strategy (r, lvl)

let print_registered () =
  let pr_lib_ref (s,r) =
    pr_global r ++ str " registered as " ++ str s
  in
  hov 0 (prlist_with_sep fnl pr_lib_ref @@ Rocqlib.get_lib_refs ())

let print_registered_schemes () =
  let schemes = DeclareScheme.all_schemes() in
  let pr_one_scheme ind (kind, c) =
    pr_global (ConstRef c) ++ str " registered as " ++ str kind ++ str " for " ++ pr_global (IndRef ind)
  in
  let pr_schemes_of_ind (ind, schemes) =
    prlist_with_sep fnl (pr_one_scheme ind) (CString.Map.bindings schemes)
  in
  hov 0 (prlist_with_sep fnl pr_schemes_of_ind (Indmap.bindings schemes))

let dump_universes output g =
  let open Univ in
  let dump_arc u = function
    | UGraph.Node ltle ->
      Univ.Level.Map.iter (fun v strict ->
          let typ = if strict then Lt else Le in
          output typ u v) ltle;
    | UGraph.Alias v ->
      output Eq u v
  in
  Univ.Level.Map.iter dump_arc g

let dump_universes_gen prl g s =
  let fulls = System.get_output_path s in
  System.mkdir (Filename.dirname fulls);
  let output = open_out fulls in
  let output_constraint, close =
    if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin
      (* the lazy unit is to handle errors while printing the first line *)
      let init = lazy (Printf.fprintf output "digraph universes {\n") in
      begin fun kind left right ->
        let () = Lazy.force init in
        match kind with
          | Univ.Lt ->
            Printf.fprintf output " \"%s\" -> \"%s\" [style=bold];\n" right left
          | Univ.Le ->
            Printf.fprintf output " \"%s\" -> \"%s\" [style=solid];\n" right left
          | Univ.Eq ->
            Printf.fprintf output " \"%s\" -> \"%s\" [style=dashed];\n" left right
      end, begin fun () ->
        if Lazy.is_val init then Printf.fprintf output "}\n";
        close_out output
      end
    end else begin
      begin fun kind left right ->
        let kind = match kind with
          | Univ.Lt -> "<"
          | Univ.Le -> "<="
          | Univ.Eq -> "="
        in
        Printf.fprintf output "%s %s %s ;\n" left kind right
      end, (fun () -> close_out output)
    end
  in
  let output_constraint k l r = output_constraint k (prl l) (prl r) in
  try
    dump_universes output_constraint g;
    close ();
    str "Universes written to file \"" ++ str s ++ str "\"."
  with reraise ->
    let reraise = Exninfo.capture reraise in
    close ();
    Exninfo.iraise reraise

let universe_subgraph kept univ =
  let open Univ in
  let parse = function
    | NamedUniv q ->
      begin try Level.make (Nametab.locate_universe q)
      with Not_found ->
        CErrors.user_err ?loc:q.loc Pp.(str "Undeclared universe " ++ pr_qualid q ++ str".")
      end
    | RawUniv { CAst.v = s; loc } ->
      let parts = String.split_on_char '.' s in
      let () = if CList.is_empty parts then CErrors.user_err ?loc Pp.(str "Invalid raw universe.") in
      let i, dp = List.sep_last parts in
      let dp = Libnames.dirpath_of_string (String.concat "." dp) in
      let i = match int_of_string_opt i with
        | Some i -> i
        | None -> CErrors.user_err ?loc Pp.(str "Invalid raw universe.")
      in
      let u = UGlobal.make dp "" i in
      let u = Level.make u in
      begin match UGraph.check_declared_universes univ (Level.Set.singleton u) with
      | Ok () -> u
      | Error _ -> CErrors.user_err ?loc Pp.(str "Undeclared universe " ++ Level.raw_pr u ++ str".")
      end
  in
  let kept = List.fold_left (fun kept q -> Level.Set.add (parse q) kept) Level.Set.empty kept in
  let csts = UGraph.constraints_for ~kept univ in
  let add u newgraph =
    let strict = UGraph.check_constraint univ (Level.set,Lt,u) in
    UGraph.add_universe u ~strict newgraph
  in
  let univ = Level.Set.fold add kept UGraph.initial_universes in
  UGraph.merge_constraints csts univ

let sort_universes g =
  let open Univ in
  let rec normalize u = match Level.Map.find u g with
  | UGraph.Alias u -> normalize u
  | UGraph.Node _ -> u
  in
  let get_next u = match Level.Map.find u g with
  | UGraph.Alias u -> assert false (* nodes are normalized *)
  | UGraph.Node ltle -> ltle
  in
  (* Compute the longest chain of Lt constraints from Set to any universe *)
  let rec traverse accu todo = match todo with
  | [] -> accu
  | (u, n) :: todo ->
    let () = assert (Level.equal (normalize u) u) in
    let n = match Level.Map.find u accu with
    | m -> if m < n then Some n else None
    | exception Not_found -> Some n
    in
    match n with
    | None -> traverse accu todo
    | Some n ->
      let accu = Level.Map.add u n accu in
      let next = get_next u in
      let fold v lt todo =
        let v = normalize v in
        if lt then (v, n + 1) :: todo else (v, n) :: todo
      in
      let todo = Level.Map.fold fold next todo in
      traverse accu todo
  in
  (* Only contains normalized nodes *)
  let levels = traverse Level.Map.empty [normalize Level.set, 0] in
  let max_level = Level.Map.fold (fun _ n accu -> max n accu) levels 0 in
  let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] in
  let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp "" i))) in
  (* Add the normal universes *)
  let fold (cur, ans) u =
    let ans = Level.Map.add cur (UGraph.Node (Level.Map.singleton u true)) ans in
    (u, ans)
  in
  let _, ans = Array.fold_left fold (Level.set, Level.Map.empty) ulevels in
  let ulevels = Array.cons Level.set ulevels in
  (* Add alias pointers *)
  let fold u _ ans =
    if Level.is_set u then ans
    else
      let n = Level.Map.find (normalize u) levels in
      Level.Map.add u (UGraph.Alias ulevels.(n)) ans
  in
  Level.Map.fold fold g ans

type constraint_source = GlobRef of GlobRef.t | Library of DirPath.t

(* The [edges] fields give the edges of the graph.
   For [u <= v] and [u < v] we have [u |-> v |-> gref, k],
   for [u = v] we have both directions.

   When there are edges with different constraint types between the
   same univs (eg [u < v] and [u <= v]) we keep the strictest one
   (either [<] or [=], NB we can't get both at the same time).
*)
type constraint_sources = {
  edges : (constraint_source * Univ.constraint_type) Univ.Level.Map.t Univ.Level.Map.t;
}

let empty_sources = { edges = Univ.Level.Map.empty }

let mk_sources () =
  let open Univ in
  let srcs = DeclareUniv.constraint_sources () in
  let pick_stricter_constraint (_,k as v) (_,k' as v') =
    match k, k' with
    | Le, Lt | Le, Eq -> v'
    | Lt, Le | Eq, Le -> v
    | Le, Le | Lt, Lt | Eq, Eq ->
      (* same: prefer [v]
         (the older refs are encountered last, and fallback libraries first) *)
      v
    | Lt, Eq | Eq, Lt ->
      (* XXX don't assert in case of type in type? *)
      assert false
  in
  let add_edge_unidirectional (u,k,v) ref edges =
    Level.Map.update u (fun uedges ->
        let uedges = Option.default Level.Map.empty uedges in
        Some (Level.Map.update v (function
            | None -> Some (ref, k)
            | Some v' -> Some (pick_stricter_constraint (ref, k) v'))
            uedges))
      edges
  in
  let add_edge (u,k,v as cst) ref edges =
    let edges = add_edge_unidirectional cst ref edges in
    if k = Eq then add_edge_unidirectional (v,k,u) ref edges else edges
  in
  let edges = Level.Map.empty in
  let edges =
    let libs = Library.loaded_libraries () in
    List.fold_left (fun edges dp ->
        let _, (_, csts) = Safe_typing.univs_of_library @@ Library.library_compiled dp in
        Constraints.fold (fun cst edges -> add_edge cst (Library dp) edges)
          csts edges)
      edges libs
  in
  let edges =
    List.fold_left (fun edges (ref,csts) ->
        Constraints.fold (fun cst edges -> add_edge cst (GlobRef ref) edges)
          csts edges)
      edges srcs
  in
  {
    edges;
  }

exception Found of (Univ.constraint_type * Univ.Level.t * constraint_source) list

(* We are looking for a path from [source] to [target].
   If [k] is [Lt] the path must contain at least one [Lt].
   If [k] is [Eq] the path must contain no [Lt].

   [visited] is a map which for each level we have visited says if the
   path had enough [Lt] (always true if the original [k] is [Le] or [Eq]).
*)
let search src ~target k ~source =
  let module UMap = Univ.Level.Map in
  let rec loop visited todo next_todo =
    match todo, next_todo with
    | [], [] -> ()
    | _, _ :: _ -> loop visited next_todo []
    | (source,k,revpath)::todo, _ ->
      let is_visited = match UMap.find_opt source visited with
        | None -> false
        | Some has_enough_lt ->
          if has_enough_lt then true
          else (* original k was [Lt], if current k is also [Lt] we have no new info on this path *)
            k = Univ.Lt
      in
      if is_visited then loop visited todo next_todo
      else
        let visited = UMap.add source (k <> Univ.Lt) visited in
        let visited, next_todo =
          UMap.fold (fun u (ref,k') (visited,next_todo) ->
              if k = Univ.Eq && k' = Univ.Lt then
                (* no point searching for a loop involving [u]  *)
                (UMap.add u true visited, next_todo)
              else
                let next_k = if k = Univ.Lt && k' = Univ.Lt then Univ.Le
                  else k
                in
                let revpath = (k',u,ref) :: revpath in
                if Univ.Level.equal u target && next_k <> Univ.Lt
                then raise (Found revpath)
                else (visited, (u, next_k, revpath) :: next_todo))
            (Option.default UMap.empty (UMap.find_opt source src.edges))
            (visited,next_todo)
        in
        loop visited todo next_todo
  in
  try loop UMap.empty [source,k,[]] []; None
  with Found l -> Some (List.rev l)

let search src (u,k,v) =
  let path = search src ~source:u k ~target:v in
  match path with
  | None -> None
  | Some path ->
    if k = Univ.Eq && not (List.for_all (fun (k',_,_) -> k' = Univ.Eq) path) then
      let path' = search src ~source:v k ~target:u in
      begin match path' with
      | None -> None
      | Some path' -> Some (path @ path')
      end
    else Some path

let find_source (u,k,v as cst) src =
  if Univ.Level.is_set u && k = Univ.Lt then []
  else Option.default [] (search src cst)

let pr_constraint_source = function
  | GlobRef ref -> begin try pr_global ref
      with Not_found ->
        (* global in a module type or functor *)
        GlobRef.print ref
    end
  | Library dp -> str "library " ++ pr_qualid (Nametab.shortest_qualid_of_module (MPfile dp))

let pr_source_path prl u src =
  if CList.is_empty src then mt()
  else
    let pr_rel = function
      | Univ.Eq -> str"=" | Lt -> str"<" | Le -> str"<="
    in
    let pr_one (k,v,ref) =
      spc() ++
      h (pr_rel k ++ surround (str "from " ++ pr_constraint_source ref) ++
         spc() ++ prl v)
    in
    spc() ++ surround (str"because" ++ spc() ++ prl u ++ prlist_with_sep mt pr_one src)

let pr_pmap sep pr map =
  let cmp (u,_) (v,_) = Univ.Level.compare u v in
  Pp.prlist_with_sep sep pr (List.sort cmp (Univ.Level.Map.bindings map))

let pr_arc srcs prl = let open Pp in
  function
  | u, UGraph.Node ltle ->
    if Univ.Level.Map.is_empty ltle then mt ()
    else
      prl u ++ str " " ++
      v 0
        (pr_pmap spc (fun (v, strict) ->
             let k = if strict then Univ.Lt else Univ.Le in
             let src = find_source (u,k,v) srcs in
             hov 2 ((if strict then str "< " else str "<= ") ++ prl v ++ pr_source_path prl u src))
            ltle) ++
      fnl ()
  | u, UGraph.Alias v ->
    let src = find_source (u,Eq,v) srcs in
    prl u  ++ str " = " ++ prl v ++ pr_source_path prl u src ++ fnl ()

let pr_universes srcs prl g = pr_pmap Pp.mt (pr_arc srcs prl) g

let print_universes { sort; subgraph; with_sources; file; } =
  let univ = Global.universes () in
  let univ = match subgraph with
    | None -> univ
    | Some g -> universe_subgraph g univ
  in
  let univ = UGraph.repr univ in
  let univ = if sort then sort_universes univ else univ in
  let pr_remaining =
    if Global.is_joined_environment () then mt ()
    else str"There may remain asynchronous universe constraints"
  in
  let prl = UnivNames.pr_level_with_global_universes in
  begin match file with
  | None ->
    let with_sources = match with_sources, subgraph with
      | Some b, _ -> b
      | _, None -> false
      | _, Some _ -> true
    in
    let srcs = if with_sources then mk_sources () else empty_sources in
    pr_universes srcs prl univ ++ pr_remaining
  | Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s
  end

let print_sorts () =
  let qualities = Sorts.QVar.Set.elements (Global.qualities ()) in
  let prq = UnivNames.pr_quality_with_global_universes in
  Pp.prlist_with_sep Pp.spc prq qualities

(*********************)
(* "Locate" commands *)

let locate_file f =
  let file = Flags.silently Loadpath.locate_file f in
  str file

let msg_found_library (fulldir, file) =
  if Library.library_is_loaded fulldir then
    hov 0 (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ str file)
  else
    hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file)

let print_located_library qid =
  let open Loadpath in
  match locate_qualified_library qid with
  | Ok lib -> msg_found_library lib
  | Error LibUnmappedDir -> raise (UnmappedLibrary (None, qid))
  | Error LibNotFound    -> raise (NotFoundLibrary (None, qid))

let smart_global r =
  let gr = Smartlocate.smart_global r in
  Dumpglob.add_glob ?loc:r.loc gr;
  gr

let qualid_global id = smart_global (make ?loc:id.loc @@ Constrexpr.AN id)

(**********)
(* Syntax *)

let vernac_declare_scope ~module_local sc =
  Metasyntax.declare_scope module_local sc

let vernac_delimiters ~module_local sc action =
  match action with
  | Some lr -> Metasyntax.add_delimiters module_local sc lr
  | None -> Metasyntax.remove_delimiters module_local sc

let vernac_bind_scope ~atts sc cll =
  let module_local, where = Attributes.(parse Notations.(module_locality ++ bind_scope_where) atts) in
  Metasyntax.add_class_scope module_local sc where (List.map scope_class_of_qualid cll)

let vernac_open_close_scope ~section_local (to_open,s) =
  Metasyntax.open_close_scope section_local ~to_open s

let interp_enable_notation_rule on ntn interp flags scope =
  let open Notation in
  let rule = Option.map (function
    | Inl ntn -> Inl (interpret_notation_string ntn)
    | Inr (vars,qid) -> Inr qid) ntn in
  let rec parse_notation_enable_flags all query = function
    | [] -> all, query
    | EnableNotationEntry CAst.{loc;v=entry} :: flags ->
      (match entry with InCustomEntry s when not (Egramrocq.exists_custom_entry s) -> user_err ?loc (str "Unknown custom entry.") | _ -> ());
      parse_notation_enable_flags all { query with notation_entry_pattern = entry :: query.notation_entry_pattern } flags
    | EnableNotationOnly use :: flags ->
      parse_notation_enable_flags all { query with use_pattern = use } flags
    | EnableNotationAll :: flags -> parse_notation_enable_flags true query flags in
  let interp = Option.map (fun c ->
      let vars, recvars =
        match ntn with
        | None ->
          (* We expect the right-hand side to mention "_" in place of proper variables *)
          (* Or should we instead deactivate the check of free variables? *)
          ([], [])
        | Some (Inl ntn) -> let {recvars; mainvars} = decompose_raw_notation ntn in (mainvars, recvars)
        | Some (Inr (vars,qid)) -> (vars, [])
      in
      let ninterp_var_type = Id.Map.of_list (List.map (fun x -> (x, Notation_term.NtnInternTypeAny None)) vars) in
      let ninterp_rec_vars = Id.Map.of_list recvars in
      let nenv = Notation_term.{ ninterp_var_type; ninterp_rec_vars } in
      let (_acvars, ac, _reversibility) = Constrintern.interp_notation_constr (Global.env ()) nenv c in
      ([], ac)) interp in
  let default_notation_enable_pattern = {
    notation_entry_pattern = [];
    interp_rule_key_pattern = rule;
    use_pattern = ParsingAndPrinting;
    scope_pattern = scope;
    interpretation_pattern = interp;
    }
  in
  let all, notation_pattern =
    parse_notation_enable_flags false default_notation_enable_pattern flags in
  on, all, notation_pattern

let vernac_enable_notation ~module_local on rule interp flags scope =
  let () = match rule, interp, scope with
    | None, None, None -> user_err (str "No notation provided.") | _ -> () in
  let on, all, notation_pattern = interp_enable_notation_rule on rule interp flags scope in
  Metasyntax.declare_notation_toggle module_local ~on ~all notation_pattern

(***********)
(* Gallina *)

let check_name_freshness locality {CAst.loc;v=id} : unit =
  (* We check existence here: it's a bit late at Qed time *)
  if Termops.is_section_variable (Global.env ()) id ||
     locality <> Discharge && Nametab.exists_cci (Lib.make_path id) ||
     locality <> Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
  then
    user_err ?loc  (Id.print id ++ str " already exists.")

let vernac_definition_hook ~canonical_instance ~local ~poly ~reversible = let open Decls in function
| Coercion ->
  Some (ComCoercion.add_coercion_hook ~reversible)
| CanonicalStructure ->
  Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
| SubClass ->
  Some (ComCoercion.add_subclass_hook ~poly ~reversible)
| Definition when canonical_instance ->
  Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
| Let when canonical_instance ->
  Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref)))
| _ -> None

let default_thm_id = Id.of_string "Unnamed_thm"

let fresh_name_for_anonymous_theorem () =
  Namegen.next_global_ident_away (Global.safe_env ()) default_thm_id Id.Set.empty

let vernac_definition_name lid local =
  let lid =
    match lid with
    | { v = Name.Anonymous; loc } ->
         CAst.make ?loc (fresh_name_for_anonymous_theorem ())
    | { v = Name.Name n; loc } -> CAst.make ?loc n in
  check_name_freshness local lid;
  let () =
    if Dumpglob.dump () then
    match local with
    | Discharge -> Dumpglob.dump_definition lid true "var"
    | Global _ -> Dumpglob.dump_definition lid false "def"
  in
  lid.v

let vernac_definition_interactive ~atts (discharge, kind) (lid, udecl) bl t =
  let open DefAttributes in
  let scope, local, poly, program_mode, user_warns, typing_flags, using, clearbody =
    atts.scope, atts.locality, atts.polymorphic, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in
  let canonical_instance, reversible = atts.canonical_instance, atts.reversible in
  let hook = vernac_definition_hook ~canonical_instance ~local ~poly ~reversible kind in
  let name = vernac_definition_name lid scope in
  ComDefinition.do_definition_interactive ?loc:lid.loc ~typing_flags ~program_mode ~name ~poly ~scope ?clearbody:atts.clearbody
    ~kind:(Decls.IsDefinition kind) ?user_warns ?using:atts.using ?hook udecl bl t

let vernac_definition_refine ~atts (discharge, kind) (lid, udecl) bl red_option c typ_opt =
  if Option.has_some red_option then
    CErrors.user_err ?loc:c.loc Pp.(str "Cannot use Eval with #[refine].");
  let open DefAttributes in
  let scope, local, poly, program_mode, user_warns, typing_flags, using, clearbody =
     atts.scope, atts.locality, atts.polymorphic, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in
  let canonical_instance, reversible = atts.canonical_instance, atts.reversible in
  let hook = vernac_definition_hook ~canonical_instance ~local ~poly kind ~reversible in
  let name = vernac_definition_name lid scope in
  ComDefinition.do_definition_refine ~name ?loc:lid.loc
    ?clearbody ~poly ~typing_flags ~scope ~kind:(Decls.IsDefinition kind)
    ?user_warns ?using udecl bl c typ_opt ?hook

let vernac_definition ~atts ~pm (discharge, kind) (lid, udecl) bl red_option c typ_opt =
  let open DefAttributes in
  let scope, local, poly, program_mode, user_warns, typing_flags, using, clearbody =
     atts.scope, atts.locality, atts.polymorphic, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in
  let canonical_instance, reversible = atts.canonical_instance, atts.reversible in
  let hook = vernac_definition_hook ~canonical_instance ~local ~poly kind ~reversible in
  let name = vernac_definition_name lid scope in
  let red_option = match red_option with
    | None -> None
    | Some r ->
      let env = Global.env () in
      let sigma = Evd.from_env env in
      Some (snd (Redexpr.interp_redexp_no_ltac env sigma r)) in
  if program_mode then
    let kind = Decls.IsDefinition kind in
    ComDefinition.do_definition_program ?loc:lid.loc ~pm ~name
      ?clearbody ~poly ?typing_flags ~scope ~kind
      ?user_warns ?using udecl bl red_option c typ_opt ?hook
  else
    let () =
      ComDefinition.do_definition ~name ?loc:lid.loc
        ?clearbody ~poly ?typing_flags ~scope ~kind
        ?user_warns ?using udecl bl red_option c typ_opt ?hook in
    pm

(* NB: pstate argument to use combinators easily *)
let vernac_start_proof ~atts kind l =
  let open DefAttributes in
  if Dumpglob.dump () then
    List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
  let scope, local, poly, program_mode, user_warns, typing_flags, using, clearbody =
    atts.scope, atts.locality, atts.polymorphic, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in
  List.iter (fun ((id, _), _) -> check_name_freshness scope id) l;
  match l with
  | [] -> assert false
  | [({v=name; loc},udecl),(bl,typ)] ->
    ComDefinition.do_definition_interactive ?loc
      ~typing_flags ~program_mode ~name ~poly ?clearbody ~scope
      ~kind:(Decls.IsProof kind) ?user_warns ?using udecl bl typ
  | ((lid,_),_) :: _ ->
    let fix = List.map (fun ((fname, univs), (binders, rtype)) ->
        { fname; binders; rtype; body_def = None; univs; notations = []}) l in
    let pm, proof =
      ComFixpoint.do_mutually_recursive ~refine:false ~program_mode ~use_inference_hook:program_mode
        ~scope ?clearbody ~kind:(Decls.IsProof kind) ~poly ?typing_flags
        ?user_warns ?using (CUnknownRecOrder, fix) in
    assert (Option.is_empty pm);
    Option.get proof

let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function
  | Admitted ->
    Declare.Proof.save_admitted ~pm ~proof:lemma
  | Proved (opaque,idopt) ->
    let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque ~idopt
    in pm

let vernac_abort ~lemma:_ ~pm = pm

let vernac_exact_proof ~lemma ~pm c =
  (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
     called only at the beginning of a proof. *)
  let lemma, status = Declare.Proof.by (Tactics.exact_proof c) lemma in
  let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque:Opaque ~idopt:None in
  if not status then Feedback.feedback Feedback.AddedAxiom;
  pm

let vernac_assumption ~atts kind l inline =
  let open DefAttributes in
  let scope, poly, program_mode, using, user_warns =
    atts.scope, atts.polymorphic, atts.program, atts.using, atts.user_warns in
  if Option.has_some using then
    Attributes.unsupported_attributes [CAst.make ("using",VernacFlagEmpty)];
  ComAssumption.do_assumptions ~poly ~program_mode ~scope ~kind ?user_warns ~inline l

let { Goptions.get = is_polymorphic_inductive_cumulativity } =
  declare_bool_option_and_ref
    ~key:["Polymorphic";"Inductive";"Cumulativity"]
    ~value:false
    ()

let polymorphic_cumulative =
  let error_poly_context () =
    user_err
      Pp.(str "The cumulative attribute can only be used in a polymorphic context.");
  in
  let open Attributes in
  let open Notations in
  (* EJGA: this seems redudant with code in attributes.ml *)
  qualify_attribute "universes"
    (bool_attribute ~name:"polymorphic"
     ++ bool_attribute ~name:"cumulative")
  >>= fun (poly,cumul) ->
  match poly, cumul with
  | Some poly, Some cumul ->
     (* Case of Polymorphic|Monomorphic Cumulative|NonCumulative Inductive
        and #[ universes(polymorphic|monomorphic,cumulative|noncumulative) ] Inductive *)
     if poly then return (true, cumul)
     else error_poly_context ()
  | Some poly, None ->
     (* Case of Polymorphic|Monomorphic Inductive
        and #[ universes(polymorphic|monomorphic) ] Inductive *)
     if poly then return (true, is_polymorphic_inductive_cumulativity ())
     else return (false, false)
  | None, Some cumul ->
     (* Case of Cumulative|NonCumulative Inductive *)
     if is_universe_polymorphism () then return (true, cumul)
     else error_poly_context ()
  | None, None ->
     (* Case of Inductive *)
     if is_universe_polymorphism () then
       return (true, is_polymorphic_inductive_cumulativity ())
     else
       return (false, false)

let { Goptions.get = get_uniform_inductive_parameters } =
  Goptions.declare_bool_option_and_ref
    ~key:["Uniform"; "Inductive"; "Parameters"]
    ~value:false
    ()

let should_treat_as_uniform () =
  if get_uniform_inductive_parameters ()
  then ComInductive.UniformParameters
  else ComInductive.NonUniformParameters

(* [XXX] EGJA: several arguments not used here *)
let vernac_record records =
  let map ((is_coercion, name), binders, sort, nameopt, cfs, ido) =
    let idbuild = match nameopt with
    | None -> CAst.map (Nameops.add_prefix "Build_") name
    | Some lid -> lid
    in
    let default_inhabitant_id = Option.map (fun CAst.{v=id} -> id) ido in
    Record.Ast.{ name; is_coercion; binders; cfs; idbuild; sort; default_inhabitant_id }
  in
  let records = List.map map records in
  records

let extract_inductive_udecl (indl:(inductive_expr * notation_declaration list) list) =
  match indl with
  | [] -> assert false
  | (((coe,(id,udecl)),b,c,d),e) :: rest ->
    let rest = List.map (fun (((coe,(id,udecl)),b,c,d),e) ->
        if Option.has_some udecl
        then user_err Pp.(strbrk "Universe binders must be on the first inductive of the block.")
        else (((coe,id),b,c,d),e))
        rest
    in
    udecl, (((coe,id),b,c,d),e) :: rest

let finite_of_kind = let open Declarations in function
  | Inductive_kw -> Finite
  | CoInductive -> CoFinite
  | Variant | Record | Structure | Class _ -> BiFinite

let private_ind =
  let open Attributes in
  let open Notations in
  attribute_of_list
    [ "matching"
    , single_key_parser ~name:"Private (matching) inductive type" ~key:"matching" ()
    ]
  |> qualify_attribute "private"
  >>= function
  | Some () -> return true
  | None -> return false

(** Flag governing use of primitive projections. Disabled by default. *)
let { Goptions.get = primitive_flag } =
  Goptions.declare_bool_option_and_ref
    ~key:["Primitive";"Projections"]
    ~value:false
    ()

let primitive_proj =
  let open Attributes in
  let open Notations in
  qualify_attribute "projections" (bool_attribute ~name:"primitive")
  >>= function
  | Some t -> return t
  | None -> return (primitive_flag ())

let mode_attr =
  let open Attributes in
  let open Notations in
  payload_attribute ?cat:None ~name:"mode" >>= function
  | None -> return None
  | Some mode -> return (Some (Hints.parse_modes mode))

module Preprocessed_Mind_decl = struct
  type flags = ComInductive.flags
  type record = {
    flags : flags;
    udecl : Constrexpr.cumul_univ_decl_expr option;
    primitive_proj : bool;
    kind : Vernacexpr.inductive_kind;
    records : Record.Ast.t list;
  }
  type inductive = {
    flags : flags;
    udecl : Constrexpr.cumul_univ_decl_expr option;
    typing_flags : Declarations.typing_flags option;
    private_ind : bool;
    uniform : ComInductive.uniform_inductive_flag;
    inductives : (Vernacexpr.one_inductive_expr * Vernacexpr.notation_declaration list) list;
  }
  type t =
    | Record of record
    | Inductive of inductive
end

(* Intermediate type while parsing record field flags *)
type record_field_attr = {
  rf_coercion: coercion_flag; (* the projection is an implicit coercion *)
  rf_reversible: bool option; (* coercion is reversible, if relevant *)
  rf_instance: instance_flag; (* the projection is an instance *)
  rf_priority: int option; (* priority of the instance, if relevant *)
  rf_locality: Goptions.option_locality; (* locality of coercion and instance *)
  rf_canonical: bool; (* use this projection in the search for canonical instances *)
}

let check_proj_flags rf =
  let open Vernacexpr in
  let open Record.Data in
  let () = match rf.rf_coercion, rf.rf_instance with
    | NoCoercion, NoInstance ->
      if rf.rf_locality <> Goptions.OptDefault then
        Attributes.(unsupported_attributes
                      [CAst.make ("locality (without :> or ::)",VernacFlagEmpty)])
    | AddCoercion, NoInstance ->
      if rf.rf_locality = Goptions.OptExport then
        Attributes.(unsupported_attributes
                      [CAst.make ("export (without ::)",VernacFlagEmpty)])
    | _ -> ()
  in
  let pf_coercion =
    match rf.rf_coercion with
    | AddCoercion ->
      Some {
        coe_local = rf.rf_locality = OptLocal;
        coe_reversible = Option.default true rf.rf_reversible;
      }
    | NoCoercion ->
      if rf.rf_reversible <> None then
        Attributes.(unsupported_attributes
                      [CAst.make ("reversible (without :>)",VernacFlagEmpty)]);
      None
  in
  let pf_instance =
    match rf.rf_instance with
    | NoInstance ->
      let () = if Option.has_some rf.rf_priority then
          CErrors.user_err Pp.(str "Priority not allowed without \"::\".")
      in
      None
    | BackInstance ->
      let local =
        match rf.rf_locality with
        | Goptions.OptLocal -> Hints.Local
        | Goptions.(OptDefault | OptExport) -> Hints.Export
        | Goptions.OptGlobal -> Hints.SuperGlobal
      in
      Some {
        inst_locality = local;
        inst_priority = rf.rf_priority;
      }
  in
  { pf_coercion; pf_instance; pf_canonical = rf.rf_canonical }

let preprocess_defclass ~atts udecl (id, bl, c, l) =
  let poly, mode =
    Attributes.(parse Notations.(polymorphic ++ mode_attr) atts)
  in
  let flags = {
    (* flags which don't matter for definitional classes *)
    ComInductive.template=None; cumulative=false; finite=BiFinite;
    (* real flags *)
    poly; mode;
  }
  in
  let bl = match bl with
    | bl, None -> bl
    | _ -> CErrors.user_err Pp.(str "Definitional classes do not support the \"|\" syntax.")
  in
  if fst id = AddCoercion then
    user_err Pp.(str "Definitional classes do not support the \">\" syntax.");
  let ((attr, rf_coercion, rf_instance), (lid, ce)) = l in
  let rf_locality = match rf_coercion, rf_instance with
    | AddCoercion, _ | _, BackInstance -> parse option_locality attr
    | _ -> let () = unsupported_attributes attr in Goptions.OptDefault
  in
  let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), [], ce),
          check_proj_flags
            { rf_coercion ; rf_reversible = None ; rf_instance ; rf_priority = None ;
              rf_locality ; rf_canonical = true },
          []
  in
  let recordl = [id, bl, c, None, [f], None] in
  let kind = Class true in
  let records = vernac_record recordl in
  Preprocessed_Mind_decl.(Record { flags; udecl; primitive_proj=false; kind; records })

let preprocess_record ~atts udecl kind indl =
  let () = match kind with
    | Variant ->
      user_err (str "The Variant keyword does not support syntax { ... }.")
    | Record | Structure | Class _ | Inductive_kw | CoInductive -> ()
  in
  let check_where ((_, _, _, _), wh) = match wh with
    | [] -> ()
    | _ :: _ ->
      user_err (str "\"where\" clause not supported for records.")
  in
  let () = List.iter check_where indl in
  let hint_mode_attr : Hints.hint_mode list option Attributes.attribute =
    match kind with
    | Class _ -> mode_attr
    | _ -> Notations.return None
  in
  let ((template, (poly, cumulative)), primitive_proj), mode =
    Attributes.(
      parse Notations.(
          template
          ++ polymorphic_cumulative
          ++ primitive_proj ++ hint_mode_attr)
        atts)
  in
  let finite = finite_of_kind kind in
  let flags = { ComInductive.template; cumulative; poly; finite; mode } in
  let parse_record_field_attr (x, f) =
    let attr =
      let rev = match f.rfu_coercion with
        | AddCoercion -> reversible
        | NoCoercion -> Notations.return None in
      let loc = match f.rfu_coercion, f.rfu_instance with
        | AddCoercion, _ | _, BackInstance -> option_locality
        | _ -> Notations.return Goptions.OptDefault in
      Notations.(rev ++ loc ++ canonical_field) in
    let (rf_reversible, rf_locality), rf_canonical = parse attr f.rfu_attrs in
    let flags = check_proj_flags {
        rf_coercion = f.rfu_coercion;
        rf_reversible;
        rf_instance = f.rfu_instance;
        rf_priority = f.rfu_priority;
        rf_locality;
        rf_canonical;
      }
    in
    x, flags, f.rfu_notation
  in
  let unpack ((id, bl, c, decl), _) = match decl with
    | RecordDecl (oc, fs, ido) ->
      let bl = match bl with
        | bl, None -> bl
        | _ -> CErrors.user_err Pp.(str "Records do not support the \"|\" syntax.")
      in
      (id, bl, c, oc, List.map parse_record_field_attr fs, ido)
    | Constructors _ -> assert false (* ruled out above *)
  in
  let kind = match kind with Class _ -> Class false | _ -> kind in
  let recordl = List.map unpack indl in
  let records = vernac_record recordl in
  Preprocessed_Mind_decl.(Record { flags; udecl; primitive_proj; kind; records })

let preprocess_inductive ~atts udecl kind indl =
  let () = match kind with
    | (Record | Structure) ->
      user_err (str "The Record keyword is for types defined using the syntax { ... }.")
    | Class _ ->
      user_err (str "Inductive classes not supported.")
    | Variant | Inductive_kw | CoInductive -> ()
  in
  let check_name ((na, _, _, _), _) = match na with
    | (AddCoercion, _) ->
      user_err (str "Variant types do not handle the \"> Name\" \
                     syntax, which is reserved for records. Use the \":>\" \
                     syntax on constructors instead.")
    | _ -> ()
  in
  let () = List.iter check_name indl in
  let hint_mode_attr : Hints.hint_mode list option Attributes.attribute =
    match kind with
    | Class _ -> mode_attr
    | _ -> Notations.return None
  in
  let (((template, (poly, cumulative)), private_ind), typing_flags), mode =
    Attributes.(
      parse Notations.(
          template
          ++ polymorphic_cumulative
          ++ private_ind ++ typing_flags ++ hint_mode_attr)
        atts)
  in
  let finite = finite_of_kind kind in
  let flags = { ComInductive.template; cumulative; poly; finite; mode } in
  let unpack (((_, id) , bl, c, decl), ntn) = match decl with
    | Constructors l -> (id, bl, c, l), ntn
    | RecordDecl _ -> assert false (* ruled out above *)
  in
  let inductives = List.map unpack indl in
  let uniform = should_treat_as_uniform () in
  Preprocessed_Mind_decl.(Inductive { flags; udecl; typing_flags; private_ind; uniform; inductives })

let preprocess_inductive_decl ~atts kind indl =
  let udecl, indl = extract_inductive_udecl indl in
  let v = match kind, indl with
  | Class _, [ ( id , bl , c , Constructors [l]), [] ] ->
    preprocess_defclass ~atts udecl (id,bl,c,l)
  | _ ->
    if List.for_all (function
        | ((_ , _ , _ , RecordDecl _), _) -> true
        | _ -> false) indl
    then preprocess_record ~atts udecl kind indl
    else if List.for_all (function
        | ((_ , _ , _ , Constructors _), _) -> true
        | _ -> false) indl
    then preprocess_inductive ~atts udecl kind indl
    else user_err (str "Mixed record-inductive definitions are not allowed.")
  in
  indl, v

let dump_inductive indl_for_glob decl =
  let open Preprocessed_Mind_decl in
  if Dumpglob.dump () then begin
    List.iter (fun (((coe,lid), _, _, cstrs), _) ->
        match cstrs with
        | Constructors cstrs ->
          Dumpglob.dump_definition lid false "ind";
          List.iter (fun (_, (lid, _)) ->
              Dumpglob.dump_definition lid false "constr") cstrs
        | _ -> ())
      indl_for_glob;
    match decl with
    | Record { records } ->
      let dump_glob_proj (x, _, _) = match x with
        | Vernacexpr.(AssumExpr ({loc;v=Name id}, _, _) | DefExpr ({loc;v=Name id}, _, _, _)) ->
          Dumpglob.dump_definition (make ?loc id) false "proj"
        | _ -> () in
      records |> List.iter (fun { Record.Ast.cfs; name } ->
          let () = Dumpglob.dump_definition name false "rec" in
          List.iter dump_glob_proj cfs)
    | Inductive _ -> ()
  end

let vernac_inductive ~atts kind indl =
  let open Preprocessed_Mind_decl in
  let indl_for_glob, decl = preprocess_inductive_decl ~atts kind indl in
  dump_inductive indl_for_glob decl;
  match decl with
  | Record { flags; kind; udecl; primitive_proj; records } ->
    let _ : _ list =
      Record.definition_structure ~flags udecl kind ~primitive_proj records in
    ()
  | Inductive { flags; udecl; typing_flags; private_ind; uniform; inductives } ->
    ComInductive.do_mutual_inductive ~flags udecl inductives ?typing_flags ~private_ind ~uniform

let preprocess_inductive_decl ~atts kind indl =
  snd @@ preprocess_inductive_decl ~atts kind indl

let vernac_fixpoint_common ~atts l =
  if Dumpglob.dump () then
    List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l;
  let scope = atts.DefAttributes.scope in
  List.iter (fun { fname } -> check_name_freshness scope fname) l;
  scope

let with_obligations program_mode f pm =
  if program_mode then
    f pm ~program_mode:true
  else
    let pm', proof = f None ~program_mode:false in
    assert (Option.is_empty pm');
    pm, proof

let vernac_fixpoint ~atts ~refine ~pm (rec_order,fixl) =
  let open DefAttributes in
  let scope = vernac_fixpoint_common ~atts fixl in
  let poly, typing_flags, program_mode, clearbody, using, user_warns =
    atts.polymorphic, atts.typing_flags, atts.program, atts.clearbody, atts.using, atts.user_warns in
  let () =
    if program_mode then
      (* XXX: Switch to the attribute system and match on ~atts *)
      let opens = List.exists (fun { body_def } -> Option.is_empty body_def) fixl in
      if opens then CErrors.user_err Pp.(str"Program Fixpoint requires a body.") in
  with_obligations program_mode
    (fun pm -> ComFixpoint.do_mutually_recursive ?pm ~refine ~scope ?clearbody ~kind:(IsDefinition Fixpoint) ~poly ?typing_flags ?user_warns ?using (CFixRecOrder rec_order, fixl))
    pm

let vernac_cofixpoint_common ~atts l =
  if Dumpglob.dump () then
    List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l;
  let scope = atts.DefAttributes.scope in
  List.iter (fun { fname } -> check_name_freshness scope fname) l;
  scope

let vernac_cofixpoint ~pm ~refine ~atts cofixl =
  let open DefAttributes in
  let scope = vernac_cofixpoint_common ~atts cofixl in
  let poly, typing_flags, program_mode, clearbody, using, user_warns =
    atts.polymorphic, atts.typing_flags, atts.program, atts.clearbody, atts.using, atts.user_warns in
  let () =
    if program_mode then
      let opens = List.exists (fun { body_def } -> Option.is_empty body_def) cofixl in
      if opens then
        CErrors.user_err Pp.(str"Program CoFixpoint requires a body.") in
  with_obligations program_mode
    (fun pm -> ComFixpoint.do_mutually_recursive ?pm ~refine ~scope ?clearbody ~kind:(IsDefinition CoFixpoint) ~poly ?typing_flags ?user_warns ?using (CCoFixRecOrder, cofixl))
    pm

let vernac_scheme l =
  if Dumpglob.dump () then
    List.iter (fun (lid, sch) ->
      Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid) l;
  Indschemes.do_scheme (Global.env ()) l

let vernac_scheme_equality ?locmap sch id =
  Indschemes.do_scheme_equality ?locmap sch id

(* [XXX] locmap unused here *)
let vernac_combined_scheme lid l ~locmap =
  (* XXX why does this take idents and not qualids *)
  let l = List.map (fun id -> match qualid_global (qualid_of_ident ?loc:id.loc id.v) with
      | ConstRef c -> c
      | _ -> CErrors.user_err ?loc:id.loc Pp.(Pputils.pr_lident  id ++ str " is not a constant."))
      l
  in
 Indschemes.do_combined_scheme lid l

let vernac_universe ~poly l =
  if poly && not (Lib.sections_are_opened ()) then
    user_err
                 (str"Polymorphic universes can only be declared inside sections, " ++
                  str "use Monomorphic Universe instead.");
  DeclareUniv.do_universe ~poly l

let vernac_sort ~poly l =
  if poly && not (Lib.sections_are_opened ()) then
    user_err
                 (str"Polymorphic sorts can only be declared inside sections, " ++
                  str "use #[universes(polymorphic=no)] Sort in order to declare a global sort.");
  DeclareUniv.do_sort ~poly l

let vernac_constraint ~poly l =
  if poly && not (Lib.sections_are_opened ()) then
    user_err
                 (str"Polymorphic universe constraints can only be declared"
                  ++ str " inside sections, use Monomorphic Constraint instead.");
  DeclareUniv.do_constraint ~poly l

(**********************)
(* Modules            *)

let warn_not_importable = CWarnings.create ~name:"not-importable"
    Pp.(fun c -> str "Cannot import local constant "
                 ++ Printer.pr_constant (Global.env()) c
                 ++ str ", it will be ignored.")

let importable_extended_global_of_path ?loc path =
  match Nametab.extended_global_of_path path with
  | Globnames.TrueGlobal (GlobRef.ConstRef c) as ref ->
    if Declare.is_local_constant c then begin
      warn_not_importable ?loc c;
      None
    end
    else Some ref
  | ref -> Some ref

(* [XXX] n unused here *)
let add_subnames_of ?loc len n ns full_n ref =
  let open GlobRef in
  let add1 r ns = (len, Globnames.TrueGlobal r) :: ns in
  match ref with
  | Globnames.Abbrev _ | Globnames.TrueGlobal (ConstRef _ | ConstructRef _ | VarRef _) ->
    CErrors.user_err ?loc Pp.(str "Only inductive types can be used with Import (...).")
  | Globnames.TrueGlobal (IndRef (mind,i)) ->
    let open Declarations in
    let path_prefix = path_pop_suffix full_n in
    let mib = Global.lookup_mind mind in
    let mip = mib.mind_packets.(i) in
    let ns = add1 (IndRef (mind,i)) ns in
    let ns = Array.fold_left_i (fun j ns _ -> add1 (ConstructRef ((mind,i),j+1)) ns)
        ns mip.mind_consnames
    in
    List.fold_left (fun ns q ->
        let s = Indrec.elimination_suffix q in
        let n_elim = Id.of_string (Id.to_string mip.mind_typename ^ s) in
        match importable_extended_global_of_path ?loc (Libnames.add_path_suffix path_prefix n_elim) with
        | exception Not_found -> ns
        | None -> ns
        | Some ref -> (len, ref) :: ns)
      ns UnivGen.QualityOrSet.all

let interp_names m ns =
  let dp_m = Nametab.path_of_module m in
  let ns =
    List.fold_left (fun ns (n,etc) ->
        let len, full_n =
          let dp_n,n = repr_qualid n in
          List.length (DirPath.repr dp_n), add_path_suffix (append_path dp_m dp_n) n
        in
        let ref = try importable_extended_global_of_path ?loc:n.loc full_n
          with Not_found ->
            CErrors.user_err ?loc:n.loc
              Pp.(str "Cannot find name " ++ pr_qualid n ++ spc() ++
                  str "in module " ++ pr_qualid (Nametab.shortest_qualid_of_module m) ++ str ".")
        in
        (* TODO dumpglob? *)
        match ref with
        | Some ref ->
          let ns = (len,ref) :: ns in
          if etc then add_subnames_of ?loc:n.loc len n ns full_n ref else ns
        | None -> ns)
      [] ns
  in
  ns

let cache_name (len,n) =
  let open Globnames in
  let open GlobRef in
  match n with
  | Abbrev kn -> Abbreviation.import_abbreviation (len+1) (Nametab.path_of_abbreviation kn) kn
  | TrueGlobal (VarRef _) -> assert false
  | TrueGlobal (ConstRef c) when Declare.is_local_constant c ->
    (* Can happen through functor application *)
    warn_not_importable c
  | TrueGlobal gr ->
    Nametab.(push (Exactly (len+1)) (path_of_global gr) gr)

let cache_names ns = List.iter cache_name ns

let subst_names (subst,ns) = List.Smart.map (on_snd (Globnames.subst_extended_reference subst)) ns

let inExportNames = Libobject.declare_object
    (Libobject.global_object "EXPORTNAMES"
       ~cache:cache_names ~subst:(Some subst_names)
       ~discharge:(fun x -> Some x))

let import_names ~export m ns =
  let ns = interp_names m ns in
  match export with
  | Lib.Export -> Lib.add_leaf (inExportNames ns)
  | Lib.Import -> cache_names ns

let interp_import_cats cats =
  Option.cata
    (fun cats -> Libobject.make_filter ~finite:(not cats.negative) cats.import_cats)
    Libobject.unfiltered
    cats

(* Assumes cats is irrelevant if f is ImportNames *)
let import_module_with_filter ~export cats m f =
  match f with
  | ImportAll ->
    Declaremods.Interp.import_module cats ~export m
  | ImportNames ns -> import_names ~export m ns

let check_no_filter_when_using_cats l =
  List.iter (function
      | _, ImportAll -> ()
      | q, ImportNames _ ->
        CErrors.user_err ?loc:q.loc
          Pp.(str "Cannot combine importing by categories and importing by names."))
    l

let vernac_import (export, cats) mpl =
  let import_mod (CAst.{v = mp; loc},f) =
    try
      let () = Dumpglob.dump_modref ?loc mp "mod" in
      let () = if Modops.is_functor @@ Mod_declarations.mod_type (Global.lookup_module mp)
        then CErrors.user_err ?loc Pp.(str "Cannot import functor " ++ str (ModPath.to_string mp) ++ str".")
      in
      import_module_with_filter ~export cats mp f
    with Not_found ->
        CErrors.user_err ?loc Pp.(str "Cannot find module " ++ str (ModPath.to_string mp) ++ str ".")
  in
  List.iter import_mod mpl

let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
  (* We check the state of the system (in section, in module type)
     and what module information is supplied *)
  if Lib.sections_are_opened () then
    user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
  let mp = Declaremods.Interp.declare_module id binders_ast (Declaremods.Enforce mty_ast) [] in
  Dumpglob.dump_moddef ?loc mp "mod";
  Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
  Option.iter (fun export -> vernac_import export [CAst.make ?loc mp, ImportAll]) export

let vernac_define_module export {loc;v=id} binders_ast argsexport mty_ast_o mexpr_ast_l =
  (* We check the state of the system (in section, in module type)
     and what module information is supplied *)
  if Lib.sections_are_opened () then
    user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
  match mexpr_ast_l with
    | [] ->
       let mp = Declaremods.Interp.start_module export id binders_ast mty_ast_o in
       Dumpglob.dump_moddef ?loc mp "mod";
       Flags.if_verbose Feedback.msg_info
         (str "Interactive Module " ++ Id.print id ++ str " started");
       List.iter
         (fun (export,mp) -> vernac_import export [CAst.make mp, ImportAll])
         argsexport
    | _::_ ->
       let mp =
         Declaremods.Interp.declare_module
           id binders_ast mty_ast_o mexpr_ast_l
       in
       Dumpglob.dump_moddef ?loc mp "mod";
       Flags.if_verbose Feedback.msg_info
         (str "Module " ++ Id.print id ++ str " is defined");
       Option.iter (fun export -> vernac_import export [CAst.make ?loc mp, ImportAll])
         export

let vernac_end_module export {loc;v=id} =
  let mp = Declaremods.Interp.end_module () in
  Dumpglob.dump_modref ?loc mp "mod";
  Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
  Option.iter (fun (export,filter) ->
      Declaremods.Interp.import_module filter ~export mp)
    export

let vernac_declare_module_type {loc;v=id} binders_ast argsexport mty_sign mty_ast_l =
  if Lib.sections_are_opened () then
    user_err Pp.(str "Modules and Module Types are not allowed inside sections.");

  match mty_ast_l with
    | [] ->
       let mp = Declaremods.Interp.start_modtype id binders_ast mty_sign in
       Dumpglob.dump_moddef ?loc mp "modtype";
       Flags.if_verbose Feedback.msg_info
         (str "Interactive Module Type " ++ Id.print id ++ str " started");
       List.iter
         (fun (export,mp) -> vernac_import export [CAst.make ?loc mp, ImportAll])
         argsexport

    | _ :: _ ->
        let mp = Declaremods.Interp.declare_modtype id binders_ast mty_sign mty_ast_l in
        Dumpglob.dump_moddef ?loc mp "modtype";
        Flags.if_verbose Feedback.msg_info
          (str "Module Type " ++ Id.print id ++ str " is defined")


let vernac_end_modtype {loc;v=id} =
  let mp = Declaremods.Interp.end_modtype () in
  Dumpglob.dump_modref ?loc mp "modtype";
  Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined")

let vernac_include l = Declaremods.Interp.declare_include l

(**********************)
(* Gallina extensions *)

(* Sections *)

let vernac_begin_section ~poly {v=id} =
  Lib.Interp.open_section id;
  (* If there was no polymorphism attribute this just sets the option
     to its current value ie noop. *)
  set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly

let vernac_end_section {CAst.loc; v} =
  Declaremods.Interp.close_section ()

let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set

(* Dispatcher of the "End" command *)
let msg_of_subsection ss id =
  let kind =
    match ss with
    | Lib.OpenedModule (false,_,_,_) -> "module"
    | Lib.OpenedModule (true,_,_,_) -> "module type"
    | Lib.OpenedSection _ -> "section"
    | _ -> "unknown"
  in
  Pp.str kind ++ spc () ++ Id.print id

let vernac_end_segment ~pm ~proof ({v=id; loc} as lid) =
  let ss = Lib.Interp.find_opening_node ?loc id in
  let what_for = msg_of_subsection ss lid.v in
  if Option.has_some proof then
    CErrors.user_err (Pp.str "Command not supported (Open proofs remain)");
  Declare.Obls.check_solved_obligations ~pm ~what_for;
  match ss with
  | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
  | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid
  | Lib.OpenedSection _ -> vernac_end_section lid
  | _ -> assert false

let vernac_end_segment lid =
  let open Vernactypes in
  typed_vernac { ignore_state with prog=Pop; proof=ReadOpt; }
    (fun {proof; prog} ->
       let () = vernac_end_segment ~pm:prog ~proof lid in
       no_state)

let vernac_begin_segment ~interactive f =
  let open Vernactypes in
  let proof = Proof.(if interactive then Reject else Ignore) in
  let prog = Prog.(if interactive then Push else Ignore) in
  typed_vernac { ignore_state with prog; proof; }
    (fun (_:no_state) ->
       let () = f () in
       no_state)

(* Libraries *)

let warn_require_in_section =
  CWarnings.create ~name:"require-in-section" ~category:CWarnings.CoreCategories.fragile
    (fun () -> strbrk "Use of “Require” inside a section is fragile." ++ spc() ++
               strbrk "It is not recommended to use this functionality in finished proof scripts.")

let vernac_require_interp needed modrefl export qidl =
  if Lib.sections_are_opened () then warn_require_in_section ();
  let () = match export with
    | None -> List.iter (function
        | _, ImportAll -> ()
        | {CAst.loc}, ImportNames _ ->
          CErrors.user_err ?loc Pp.(str "Used an import filter without importing."))
        qidl
    | Some (_,cats) -> if Option.has_some cats then check_no_filter_when_using_cats qidl
  in
  if Dumpglob.dump () then
    List.iter2 (fun ({CAst.loc},_) dp -> Dumpglob.dump_libref ?loc dp "lib") qidl modrefl;
  (* Load *)
  Library.require_library_from_dirpath needed;
--> --------------------

--> maximum size reached

--> --------------------