diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 13 | ||||
| -rw-r--r-- | engine/termops.mli | 34 | ||||
| -rw-r--r-- | engine/univNames.ml | 85 | ||||
| -rw-r--r-- | engine/univNames.mli | 18 | ||||
| -rw-r--r-- | engine/universes.ml | 5 | ||||
| -rw-r--r-- | engine/universes.mli | 10 |
6 files changed, 97 insertions, 68 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 156d1370e3..efe1525c9a 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -22,6 +22,8 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration +module Internal = struct + (* Sorts and sort family *) let print_sort = function @@ -49,6 +51,8 @@ let pr_puniverses p u = if Univ.Instance.is_empty u then p else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" +(* Minimalistic constr printer, typically for debugging *) + let rec pr_constr c = match kind c with | Rel n -> str "#"++int n | Meta n -> str "Meta(" ++ int n ++ str ")" @@ -96,12 +100,16 @@ let rec pr_constr c = match kind c with cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") -let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c)) +let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c) +let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c) +let term_printer = ref debug_print_constr_env + let print_constr_env env sigma t = !term_printer env sigma t let print_constr t = let env = Global.env () in let evd = Evd.from_env env in !term_printer env evd t + let set_print_constr f = term_printer := f module EvMap = Evar.Map @@ -1535,3 +1543,6 @@ let env_rel_context_chop k env = let ctx1,ctx2 = List.chop k rels in push_rel_context ctx2 (reset_with_named_context (named_context_val env) env), ctx1 +end + +include Internal diff --git a/engine/termops.mli b/engine/termops.mli index b967bb6abb..aa0f837938 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -311,12 +311,40 @@ val pr_metaset : Metaset.t -> Pp.t val pr_evar_universe_context : UState.t -> Pp.t val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t -(** debug printer: do not use to display terms to the casual user... *) +module Internal : sig -val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit -val print_constr : constr -> Pp.t +(** NOTE: to print terms you always want to use functions in + Printer, not these ones which are for very special cases. *) + +(** debug printers: print raw form for terms, both with + evar-substitution and without. *) +val debug_print_constr : constr -> Pp.t +val debug_print_constr_env : env -> evar_map -> constr -> Pp.t + +(** Pretty-printer hook: [print_constr_env env sigma c] will pretty + print c if the pretty printing layer has been linked into the Coq + binary. *) val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t + +(** [set_print_constr f] sets f to be the pretty printer *) +val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit + +(** Printers for contexts *) val print_named_context : env -> Pp.t val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t val print_rel_context : env -> Pp.t val print_env : env -> Pp.t + +val print_constr : constr -> Pp.t +[@@deprecated "use print_constr_env"] + +end + +val print_constr : constr -> Pp.t +[@@deprecated "use Internal.print_constr_env"] + +val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t +[@@deprecated "use Internal.print_constr_env"] + +val print_rel_context : env -> Pp.t +[@@deprecated "use Internal.print_rel_context"] diff --git a/engine/univNames.ml b/engine/univNames.ml index e861913de2..70cdd3a2db 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -8,9 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Util open Names open Univ -open Nametab let qualid_of_level l = @@ -30,20 +30,6 @@ let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l) (** Global universe information outside the kernel, to handle polymorphic universe names in sections that have to be discharged. *) -let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref) - -let add_global_universe u p = - match Level.name u with - | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map - | None -> () - -let is_polymorphic l = - match Level.name l with - | Some n -> - (try Nametab.UnivIdMap.find n !universe_map - with Not_found -> false) - | None -> false - (** Local universe names of polymorphic references *) type universe_binders = Univ.Level.t Names.Id.Map.t @@ -52,10 +38,10 @@ let empty_binders = Id.Map.empty let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders" -let universe_binders_of_global ref : universe_binders = +let universe_binders_of_global ref : Id.t list = try let l = GlobRef.Map.find ref !universe_binders_table in l - with Not_found -> Names.Id.Map.empty + with Not_found -> [] let cache_ubinder (_,(ref,l)) = universe_binders_table := GlobRef.Map.add ref l !universe_binders_table @@ -64,10 +50,28 @@ let subst_ubinder (subst,(ref,l as orig)) = let ref' = fst (Globnames.subst_global subst ref) in if ref == ref' then orig else ref', l +let name_universe lvl = + (** Best-effort naming from the string representation of the level. This is + completely hackish and should be solved in upper layers instead. *) + Id.of_string_soft (Level.to_string lvl) + let discharge_ubinder (_,(ref,l)) = + (** Expand polymorphic binders with the section context *) + let info = Lib.section_segment_of_reference ref in + let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in + let map lvl = match Level.name lvl with + | None -> (* Having Prop/Set/Var as section universes makes no sense *) + assert false + | Some na -> + try + let qid = Nametab.shortest_qualid_of_universe na in + snd (Libnames.repr_qualid qid) + with Not_found -> name_universe lvl + in + let l = List.map map sec_inst @ l in Some (Lib.discharge_global ref, l) -let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj = +let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj = let open Libobject in declare_object { (default_object "universe binder") with cache_function = cache_ubinder; @@ -78,28 +82,35 @@ let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj = rebuild_function = (fun x -> x); } let register_universe_binders ref ubinders = - (* Add the polymorphic (section) universes *) - let ubinders = UnivIdMap.fold (fun lvl poly ubinders -> - let qid = Nametab.shortest_qualid_of_universe lvl in - let level = Level.make (fst lvl) (snd lvl) in - if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders - else ubinders) - !universe_map ubinders + (** TODO: change the API to register a [Name.t list] instead. This is the last + part of the code that depends on the internal representation of names in + abstract contexts, but removing it requires quite a rework of the + callers. *) + let univs = AUContext.instance (Global.universes_of_global ref) in + let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in + let map lvl = + try LMap.find lvl revmap + with Not_found -> name_universe lvl in - if not (Id.Map.is_empty ubinders) - then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) + let ubinders = Array.map_to_list map (Instance.to_array univs) in + if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders)) type univ_name_list = Names.lname list -let universe_binders_with_opt_names ref levels = function - | None -> universe_binders_of_global ref +let universe_binders_with_opt_names ref names = + let orig = universe_binders_of_global ref in + let udecl = match names with + | None -> orig | Some udecl -> - if Int.equal(List.length levels) (List.length udecl) - then - List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with - | Anonymous -> acc - | Name na -> Names.Id.Map.add na lvl acc) - empty_binders udecl levels - else + try + List.map2 (fun orig {CAst.v = na} -> + match na with + | Anonymous -> orig + | Name id -> id) orig udecl + with Invalid_argument _ -> + let len = List.length orig in CErrors.user_err ~hdr:"universe_binders_with_opt_names" - Pp.(str "Universe instance should have length " ++ int (List.length levels)) + Pp.(str "Universe instance should have length " ++ int len) + in + let fold i acc na = Names.Id.Map.add na (Level.var i) acc in + List.fold_left_i fold 0 empty_binders udecl diff --git a/engine/univNames.mli b/engine/univNames.mli index 837beac267..bd4062ade4 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -13,13 +13,6 @@ open Univ val pr_with_global_universes : Level.t -> Pp.t val qualid_of_level : Level.t -> Libnames.qualid -(** Global universe information outside the kernel, to handle - polymorphic universes in sections that have to be discharged. *) -val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit - -(** Is [lvl] a global polymorphic universe? (ie section polymorphic universe) *) -val is_polymorphic : Level.t -> bool - (** Local universe name <-> level mapping *) type universe_binders = Univ.Level.t Names.Id.Map.t @@ -27,15 +20,14 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit -val universe_binders_of_global : Names.GlobRef.t -> universe_binders type univ_name_list = Names.lname list -(** [universe_binders_with_opt_names ref u l] +(** [universe_binders_with_opt_names ref l] - If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous). - May error if the lengths mismatch. + If [l] is [Some univs] return the universe binders naming the bound levels + of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch. - Otherwise return [universe_binders_of_global ref]. *) + Otherwise return the bound universe names registered for [ref]. *) val universe_binders_with_opt_names : Names.GlobRef.t -> - Univ.Level.t list -> univ_name_list option -> universe_binders + univ_name_list option -> universe_binders diff --git a/engine/universes.ml b/engine/universes.ml index ee9668433c..5d0157b2db 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -19,14 +19,9 @@ type univ_name_list = UnivNames.univ_name_list let pr_with_global_universes = UnivNames.pr_with_global_universes let reference_of_level = UnivNames.qualid_of_level -let add_global_universe = UnivNames.add_global_universe - -let is_polymorphic = UnivNames.is_polymorphic - let empty_binders = UnivNames.empty_binders let register_universe_binders = UnivNames.register_universe_binders -let universe_binders_of_global = UnivNames.universe_binders_of_global let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names diff --git a/engine/universes.mli b/engine/universes.mli index ad937471e9..0d3bae4c95 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -25,12 +25,6 @@ val pr_with_global_universes : Level.t -> Pp.t val reference_of_level : Level.t -> Libnames.qualid [@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"] -val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit -[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"] - -val is_polymorphic : Level.t -> bool -[@@ocaml.deprecated "Use [UnivNames.is_polymorphic]"] - type universe_binders = UnivNames.universe_binders [@@ocaml.deprecated "Use [UnivNames.universe_binders]"] @@ -39,14 +33,12 @@ val empty_binders : universe_binders val register_universe_binders : Globnames.global_reference -> universe_binders -> unit [@@ocaml.deprecated "Use [UnivNames.register_universe_binders]"] -val universe_binders_of_global : Globnames.global_reference -> universe_binders -[@@ocaml.deprecated "Use [UnivNames.universe_binders_of_global]"] type univ_name_list = UnivNames.univ_name_list [@@ocaml.deprecated "Use [UnivNames.univ_name_list]"] val universe_binders_with_opt_names : Globnames.global_reference -> - Univ.Level.t list -> univ_name_list option -> universe_binders + univ_name_list option -> universe_binders [@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"] (** ****** Deprecated: moved to [UnivGen] *) |