From e260c203fa74a587bd78b2803c8ee046ff3df20a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 12 Jun 2020 04:37:50 +0200 Subject: [states] Move States to vernac We continue to push state layers upwards, in preparation of a functional vernacular interpretation. Now we move `States` and `Printmod` which messes with the global state as to temporarily create envs with modules. --- library/library.mllib | 2 - library/states.ml | 33 ---- library/states.mli | 33 ---- printing/printing.mllib | 1 - printing/printmod.ml | 458 ------------------------------------------------ printing/printmod.mli | 26 --- vernac/printmod.ml | 458 ++++++++++++++++++++++++++++++++++++++++++++++++ vernac/printmod.mli | 26 +++ vernac/states.ml | 33 ++++ vernac/states.mli | 32 ++++ vernac/vernac.mllib | 2 + 11 files changed, 551 insertions(+), 553 deletions(-) delete mode 100644 library/states.ml delete mode 100644 library/states.mli delete mode 100644 printing/printmod.ml delete mode 100644 printing/printmod.mli create mode 100644 vernac/printmod.ml create mode 100644 vernac/printmod.mli create mode 100644 vernac/states.ml create mode 100644 vernac/states.mli diff --git a/library/library.mllib b/library/library.mllib index a6188f7661..cdc131cfab 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -5,7 +5,5 @@ Summary Nametab Global Lib -States -Kindops Goptions Coqlib diff --git a/library/states.ml b/library/states.ml deleted file mode 100644 index b6904263df..0000000000 --- a/library/states.ml +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* - let reraise = Exninfo.capture reraise in - (unfreeze st; Exninfo.iraise reraise) diff --git a/library/states.mli b/library/states.mli deleted file mode 100644 index fb50a1a8bd..0000000000 --- a/library/states.mli +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* state -val unfreeze : state -> unit - -val summary_of_state : state -> Summary.frozen -val lib_of_state : state -> Lib.frozen -val replace_summary : state -> Summary.frozen -> state -val replace_lib : state -> Lib.frozen -> state - -(** {6 Rollback } *) - -(** [with_state_protection f x] applies [f] to [x] and restores the - state of the whole system as it was before applying [f] *) - -val with_state_protection : ('a -> 'b) -> 'a -> 'b - 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 *) -(* !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 *) -(* 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 diff --git a/vernac/printmod.ml b/vernac/printmod.ml new file mode 100644 index 0000000000..9beac17546 --- /dev/null +++ b/vernac/printmod.ml @@ -0,0 +1,458 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* !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/vernac/printmod.mli b/vernac/printmod.mli new file mode 100644 index 0000000000..c7f056063b --- /dev/null +++ b/vernac/printmod.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* 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 diff --git a/vernac/states.ml b/vernac/states.ml new file mode 100644 index 0000000000..b6904263df --- /dev/null +++ b/vernac/states.ml @@ -0,0 +1,33 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + let reraise = Exninfo.capture reraise in + (unfreeze st; Exninfo.iraise reraise) diff --git a/vernac/states.mli b/vernac/states.mli new file mode 100644 index 0000000000..51db83ca03 --- /dev/null +++ b/vernac/states.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* state +val unfreeze : state -> unit + +val summary_of_state : state -> Summary.frozen +val lib_of_state : state -> Lib.frozen +val replace_summary : state -> Summary.frozen -> state +val replace_lib : state -> Lib.frozen -> state + +(** {6 Rollback } *) + +(** [with_state_protection f x] applies [f] to [x] and restores the + state of the whole system as it was before applying [f] *) + +val with_state_protection : ('a -> 'b) -> 'a -> 'b diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 23dde0dd29..085e2e35bc 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -1,6 +1,8 @@ Vernacexpr Attributes Pvernac +States +Printmod Declaremods G_vernac G_proofs -- cgit v1.2.3