Merge PR #12504: [states] Move States to vernac

Reviewed-by: SkySkimmer
Ack-by: maximedenes

3 files changed, 0 insertions, 485 deletions

diff --git a/printing/printing.mllib b/printing/printing.mllib
index 5b5b6590a4..39e160706b 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -3,4 +3,3 @@ Pputils
 Ppconstr
 Proof_diffs
 Printer
-Printmod
diff --git a/printing/printmod.ml b/printing/printmod.ml
deleted file mode 100644
index 9beac17546..0000000000
--- a/printing/printmod.ml
+++ /dev/null
@@ -1,458 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq 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 Util
-open Constr
-open Context
-open Pp
-open Names
-open Environ
-open Declarations
-open Libnames
-open Goptions
-
-(** Note: there is currently two modes for printing modules.
-    - The "short" one, that just prints the names of the fields.
-    - The "rich" one, that also tries to print the types of the fields.
-    The short version used to be the default behavior, but now we print
-    types by default. The following option allows changing this.
-*)
-
-module Tag =
-struct
-
-  let definition = "module.definition"
-  let keyword    = "module.keyword"
-
-end
-
-let tag t s = Pp.tag t s
-let tag_definition s = tag Tag.definition s
-let tag_keyword s = tag Tag.keyword s
-
-type short = OnlyNames | WithContents
-
-let short = ref false
-
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["Short";"Module";"Printing"];
-      optread  = (fun () -> !short) ;
-      optwrite = ((:=) short) }
-
-(** Each time we have to print a non-globally visible structure,
-    we place its elements in a fake fresh namespace. *)
-
-let mk_fake_top =
-  let r = ref 0 in
-  fun () -> incr r; Id.of_string ("FAKETOP"^(string_of_int !r))
-
-let def s = tag_definition (str s)
-let keyword s = tag_keyword (str s)
-
-let get_new_id locals id =
-  let rec get_id l id =
-    let dir = DirPath.make [id] in
-      if not (Nametab.exists_dir dir) then
-        id
-      else
-        get_id (Id.Set.add id l) (Namegen.next_ident_away id l)
-  in
-  let avoid = List.fold_left (fun accu (_, id) -> Id.Set.add id accu) Id.Set.empty locals in
-    get_id avoid id
-
-(** Inductive declarations *)
-
-open Reduction
-
-let print_params env sigma params =
-  if List.is_empty params then mt ()
-  else Printer.pr_rel_context env sigma params ++ brk(1,2)
-
-let print_constructors envpar sigma names types =
-  let pc =
-    prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
-      (fun (id,c) -> Id.print id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c)
-      (Array.to_list (Array.map2 (fun n t -> (n,t)) names types))
-  in
-  hv 0 (str "  " ++ pc)
-
-let build_ind_type mip =
-  Inductive.type_of_inductive mip
-
-let print_one_inductive env sigma mib ((_,i) as ind) =
-  let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
-  let mip = mib.mind_packets.(i) in
-  let params = Inductive.inductive_paramdecls (mib,u) in
-  let nparamdecls = Context.Rel.length params in
-  let args = Context.Rel.to_extended_list mkRel 0 params in
-  let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type ((mib,mip),u)) args in
-  let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
-  let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in
-  let envpar = push_rel_context params env in
-  let inst =
-    if Declareops.inductive_is_polymorphic mib then
-      Printer.pr_universe_instance sigma u
-    else mt ()
-  in
-  hov 0 (
-    Id.print mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++
-    str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++
-  brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes
-
-let print_mutual_inductive env mind mib udecl =
-  let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
-  in
-  let keyword =
-    let open Declarations in
-    match mib.mind_finite with
-    | Finite -> "Inductive"
-    | BiFinite -> "Variant"
-    | CoFinite -> "CoInductive"
-  in
-  let bl = Printer.universe_binders_with_opt_names
-      (Declareops.inductive_polymorphic_context mib) udecl
-  in
-  let sigma = Evd.from_ctx (UState.of_binders bl) in
-  hov 0 (def keyword ++ spc () ++
-         prlist_with_sep (fun () -> fnl () ++ str"  with ")
-           (print_one_inductive env sigma mib) inds ++
-         Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes)
-
-let get_fields =
-  let rec prodec_rec l subst c =
-    match kind c with
-    | Prod (na,t,c) ->
-        let id = match na.binder_name with Name id -> id | Anonymous -> Id.of_string "_" in
-        prodec_rec ((id,true,Vars.substl subst t)::l) (mkVar id::subst) c
-    | LetIn (na,b,_,c) ->
-        let id = match na.binder_name with Name id -> id | Anonymous -> Id.of_string "_" in
-        prodec_rec ((id,false,Vars.substl subst b)::l) (mkVar id::subst) c
-    | _               -> List.rev l
-  in
-  prodec_rec [] []
-
-let print_record env mind mib udecl =
-  let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
-  let mip = mib.mind_packets.(0) in
-  let params = Inductive.inductive_paramdecls (mib,u) in
-  let nparamdecls = Context.Rel.length params in
-  let args = Context.Rel.to_extended_list mkRel 0 params in
-  let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type ((mib,mip),u)) args in
-  let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
-  let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
-  let fields = get_fields cstrtype in
-  let envpar = push_rel_context params env in
-  let bl = Printer.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib)
-      udecl
-  in
-  let sigma = Evd.from_ctx (UState.of_binders bl) in
-  let keyword =
-    let open Declarations in
-    match mib.mind_finite with
-    | BiFinite -> "Record"
-    | Finite -> "Inductive"
-    | CoFinite -> "CoInductive"
-  in
-  hov 0 (
-    hov 0 (
-      def keyword ++ spc () ++ Id.print mip.mind_typename ++ brk(1,4) ++
-      print_params env sigma params ++
-      str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++
-      str ":= " ++ Id.print mip.mind_consnames.(0)) ++
-    brk(1,2) ++
-    hv 2 (str "{ " ++
-      prlist_with_sep (fun () -> str ";" ++ brk(2,0))
-        (fun (id,b,c) ->
-          Id.print id ++ str (if b then " : " else " := ") ++
-          Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
-    Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes
-  )
-
-let pr_mutual_inductive_body env mind mib udecl =
-  if mib.mind_record != NotRecord && not !Flags.raw_print then
-    print_record env mind mib udecl
-  else
-    print_mutual_inductive env mind mib udecl
-
-(** Modpaths *)
-
-let rec print_local_modpath locals = function
-  | MPbound mbid -> Id.print (Util.List.assoc_f MBId.equal mbid locals)
-  | MPdot(mp,l) ->
-      print_local_modpath locals mp ++ str "." ++ Label.print l
-  | MPfile _ -> raise Not_found
-
-let print_modpath locals mp =
-  try (* must be with let because streams are lazy! *)
-    let qid = Nametab.shortest_qualid_of_module mp in
-      pr_qualid qid
-  with
-    | Not_found -> print_local_modpath locals mp
-
-let print_kn locals kn =
-  try
-    let qid = Nametab.shortest_qualid_of_modtype kn in
-      pr_qualid qid
-  with
-      Not_found ->
-        try
-          print_local_modpath locals kn
-        with
-            Not_found -> print_modpath locals kn
-
-let nametab_register_dir obj_mp =
-  let id = mk_fake_top () in
-  let obj_dir = DirPath.make [id] in
-  Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; }))
-
-(** Nota: the [global_reference] we register in the nametab below
-    might differ from internal ones, since we cannot recreate here
-    the canonical part of constant and inductive names, but only
-    the user names. This works nonetheless since we search now
-    [Nametab.the_globrevtab] modulo user name. *)
-
-let nametab_register_body mp dir (l,body) =
-  let push id ref =
-    Nametab.push (Nametab.Until (1+List.length (DirPath.repr dir)))
-      (make_path dir id) ref
-  in
-  match body with
-    | SFBmodule _ -> () (* TODO *)
-    | SFBmodtype _ -> () (* TODO *)
-    | SFBconst _ ->
-      push (Label.to_id l) (GlobRef.ConstRef (Constant.make2 mp l))
-    | SFBmind mib ->
-      let mind = MutInd.make2 mp l in
-      Array.iteri
-        (fun i mip ->
-          push mip.mind_typename (GlobRef.IndRef (mind,i));
-          Array.iteri (fun j id -> push id (GlobRef.ConstructRef ((mind,i),j+1)))
-            mip.mind_consnames)
-        mib.mind_packets
-
-type mod_ops =
-  { import_module : export:bool -> ModPath.t -> unit
-  ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit
-  }
-
-let nametab_register_module_body ~mod_ops mp struc =
-  (* If [mp] is a globally visible module, we simply import it *)
-  try mod_ops.import_module ~export:false mp
-  with Not_found ->
-    (* Otherwise we try to emulate an import by playing with nametab *)
-    nametab_register_dir mp;
-    List.iter (nametab_register_body mp DirPath.empty) struc
-
-let get_typ_expr_alg mtb = match mtb.mod_type_alg with
-  | Some (NoFunctor me) -> me
-  | _ -> raise Not_found
-
-let nametab_register_modparam ~mod_ops mbid mtb =
-  let id = MBId.to_id mbid in
-  match mtb.mod_type with
-  | MoreFunctor _ -> id (* functorial param : nothing to register *)
-  | NoFunctor struc ->
-    (* We first try to use the algebraic type expression if any,
-       via a Declaremods function that converts back to module entries *)
-    try
-      let () = mod_ops.process_module_binding mbid (get_typ_expr_alg mtb) in
-      id
-    with e when CErrors.noncritical e ->
-      (* Otherwise, we try to play with the nametab ourselves *)
-      let mp = MPbound mbid in
-      let check id = Nametab.exists_dir (DirPath.make [id]) in
-      let id = Namegen.next_ident_away_from id check in
-      let dir = DirPath.make [id] in
-      nametab_register_dir mp;
-      List.iter (nametab_register_body mp dir) struc;
-      id
-
-let print_body is_impl extent env mp (l,body) =
-  let name = Label.print l in
-  hov 2 (match body with
-    | SFBmodule _ -> keyword "Module" ++ spc () ++ name
-    | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
-    | SFBconst cb ->
-       let ctx = Declareops.constant_polymorphic_context cb in
-      (match cb.const_body with
-        | Def _ -> def "Definition" ++ spc ()
-        | OpaqueDef _ when is_impl -> def "Theorem" ++ spc ()
-        | _ -> def "Parameter" ++ spc ()) ++ name ++
-      (match extent with
-         | OnlyNames -> mt ()
-         | WithContents ->
-            let bl = Printer.universe_binders_with_opt_names ctx None in
-            let sigma = Evd.from_ctx (UState.of_binders bl) in
-            str " :" ++ spc () ++
-            hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++
-            (match cb.const_body with
-              | Def l when is_impl ->
-                spc () ++
-                hov 2 (str ":= " ++
-                       Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l))
-              | _ -> mt ()) ++ str "." ++
-            Printer.pr_abstract_universe_ctx sigma ctx)
-    | SFBmind mib ->
-      match extent with
-      | WithContents ->
-        pr_mutual_inductive_body env (MutInd.make2 mp l) mib None
-      | OnlyNames ->
-        let keyword =
-          let open Declarations in
-          match mib.mind_finite with
-          | Finite -> def "Inductive"
-          | BiFinite -> def "Variant"
-          | CoFinite -> def "CoInductive"
-        in
-        keyword ++ spc () ++ name)
-
-let print_struct is_impl extent env mp struc =
-  prlist_with_sep spc (print_body is_impl extent env mp) struc
-
-let print_structure ~mod_ops is_type extent env mp locals struc =
-  let env' = Modops.add_structure mp struc Mod_subst.empty_delta_resolver env in
-  nametab_register_module_body ~mod_ops mp struc;
-  let kwd = if is_type then "Sig" else "Struct" in
-  hv 2 (keyword kwd ++ spc () ++ print_struct false extent env' mp struc ++
-        brk (1,-2) ++ keyword "End")
-
-let rec flatten_app mexpr l = match mexpr with
-  | MEapply (mexpr, arg) -> flatten_app mexpr (arg::l)
-  | MEident mp -> mp::l
-  | MEwith _ -> assert false
-
-let rec print_typ_expr extent env mp locals mty =
-  match mty with
-  | MEident kn -> print_kn locals kn
-  | MEapply _ ->
-      let lapp = flatten_app mty [] in
-      let fapp = List.hd lapp in
-      let mapp = List.tl lapp in
-      hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++
-                 prlist_with_sep spc (print_modpath locals) mapp ++ str")")
-  | MEwith(me,WithDef(idl,(c, _)))->
-      let s = String.concat "." (List.map Id.to_string idl) in
-      let body = match extent with
-        | WithContents ->
-            let sigma = Evd.from_env env in
-            spc() ++ str ":=" ++ spc() ++ Printer.pr_lconstr_env env sigma c
-        | OnlyNames ->
-            mt() in
-      hov 2 (print_typ_expr extent env mp locals me ++ spc() ++ str "with" ++ spc()
-             ++ def "Definition"++ spc() ++ str s ++ body)
-  | MEwith(me,WithMod(idl,mp'))->
-      let s = String.concat "." (List.map Id.to_string idl) in
-      let body = match extent with
-        | WithContents ->
-            spc() ++ str ":="++ spc() ++ print_modpath locals mp'
-        | OnlyNames -> mt () in
-      hov 2 (print_typ_expr extent env mp locals me ++ spc() ++ str "with" ++ spc() ++
-             keyword "Module"++ spc() ++ str s ++ body)
-
-let print_mod_expr env mp locals = function
-  | MEident mp -> print_modpath locals mp
-  | MEapply _ as me ->
-      let lapp = flatten_app me [] in
-      hov 3
-        (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
-  | MEwith _ -> assert false (* No 'with' syntax for modules *)
-
-let rec print_functor ~mod_ops fty fatom is_type extent env mp locals = function
-  | NoFunctor me -> fatom ~mod_ops is_type extent env mp locals me
-  | MoreFunctor (mbid,mtb1,me2) ->
-      let id = nametab_register_modparam ~mod_ops mbid mtb1 in
-      let mp1 = MPbound mbid in
-      let pr_mtb1 = fty ~mod_ops extent env mp1 locals mtb1 in
-      let env' = Modops.add_module_type mp1 mtb1 env in
-      let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in
-      let kwd = if is_type then "Funsig" else "Functor" in
-      hov 2
-        (keyword kwd ++ spc () ++
-         str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++
-         spc() ++ print_functor ~mod_ops fty fatom is_type extent env' mp locals' me2)
-
-let rec print_expression ~mod_ops x =
-  print_functor ~mod_ops
-    print_modtype
-    (fun ~mod_ops -> function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x
-
-and print_signature ~mod_ops x =
-  print_functor ~mod_ops print_modtype print_structure x
-
-and print_modtype ~mod_ops extent env mp locals mtb = match mtb.mod_type_alg with
-  | Some me -> print_expression ~mod_ops true extent env mp locals me
-  | None -> print_signature ~mod_ops true extent env mp locals mtb.mod_type
-
-let rec printable_body dir =
-  let dir = pop_dirpath dir in
-    DirPath.is_empty dir ||
-    try
-      let open Nametab.GlobDirRef in
-      match Nametab.locate_dir (qualid_of_dirpath dir) with
-          DirOpenModtype _ -> false
-        | DirModule _ | DirOpenModule _ -> printable_body dir
-        | _ -> true
-    with
-        Not_found -> true
-
-(** Since we might play with nametab above, we should reset to prior
-    state after the printing *)
-
-let print_expression' ~mod_ops is_type extent env mp me =
-  States.with_state_protection
-    (fun e -> print_expression ~mod_ops is_type extent env mp [] e) me
-
-let print_signature' ~mod_ops is_type extent env mp me =
-  States.with_state_protection
-    (fun e -> print_signature ~mod_ops is_type extent env mp [] e) me
-
-let unsafe_print_module ~mod_ops extent env mp with_body mb =
-  let name = print_modpath [] mp in
-  let pr_equals = spc () ++ str ":= " in
-  let body = match with_body, mb.mod_expr with
-    | false, _
-    | true, Abstract -> mt()
-    | _, Algebraic me -> pr_equals ++ print_expression' ~mod_ops false extent env mp me
-    | _, Struct sign -> pr_equals ++ print_signature' ~mod_ops false extent env mp sign
-    | _, FullStruct -> pr_equals ++ print_signature' ~mod_ops false extent env mp mb.mod_type
-  in
-  let modtype = match mb.mod_expr, mb.mod_type_alg with
-    | FullStruct, _ -> mt ()
-    | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' ~mod_ops true extent env mp ty
-    | _, _ -> brk (1,1) ++ str": " ++ print_signature' ~mod_ops true extent env mp mb.mod_type
-  in
-  hv 0 (keyword "Module" ++ spc () ++ name ++ modtype ++ body)
-
-exception ShortPrinting
-
-let print_module ~mod_ops with_body mp =
-  let me = Global.lookup_module mp in
-  try
-    if !short then raise ShortPrinting;
-    unsafe_print_module ~mod_ops WithContents
-      (Global.env ()) mp with_body me ++ fnl ()
-  with e when CErrors.noncritical e ->
-    unsafe_print_module ~mod_ops OnlyNames
-      (Global.env ()) mp with_body me ++ fnl ()
-
-let print_modtype ~mod_ops kn =
-  let mtb = Global.lookup_modtype kn in
-  let name = print_kn [] kn in
-  hv 1
-    (keyword "Module Type" ++ spc () ++ name ++ str " =" ++ spc () ++
-     try
-      if !short then raise ShortPrinting;
-      print_signature' ~mod_ops true WithContents
-        (Global.env ()) kn mtb.mod_type
-     with e when CErrors.noncritical e ->
-      print_signature' ~mod_ops true OnlyNames
-        (Global.env ()) kn mtb.mod_type)
diff --git a/printing/printmod.mli b/printing/printmod.mli
deleted file mode 100644
index c7f056063b..0000000000
--- a/printing/printmod.mli
+++ /dev/null
@@ -1,26 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq 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 Names
-
-(** false iff the module is an element of an open module type *)
-val printable_body : DirPath.t -> bool
-
-val pr_mutual_inductive_body : Environ.env ->
-  MutInd.t -> Declarations.mutual_inductive_body ->
-  UnivNames.univ_name_list option -> Pp.t
-
-type mod_ops =
-  { import_module : export:bool -> ModPath.t -> unit
-  ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit
-  }
-
-val print_module : mod_ops:mod_ops -> bool -> ModPath.t -> Pp.t
-val print_modtype : mod_ops:mod_ops -> ModPath.t -> Pp.t