diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 80 | ||||
| -rw-r--r-- | engine/termops.ml | 11 | ||||
| -rw-r--r-- | engine/termops.mli | 32 | ||||
| -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 |
7 files changed, 135 insertions, 106 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 678f7c6ce6..8ab3ce821e 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -14,7 +14,23 @@ open Names open Constr open Context -include Evd.MiniEConstr +module ESorts = struct + include Evd.MiniEConstr.ESorts + + let equal sigma s1 s2 = + Sorts.equal (kind sigma s1) (kind sigma s2) +end + +module EInstance = struct + include Evd.MiniEConstr.EInstance + + let equal sigma i1 i2 = + Univ.Instance.equal (kind sigma i1) (kind sigma i2) +end + +include (Evd.MiniEConstr : module type of Evd.MiniEConstr + with module ESorts := ESorts + and module EInstance := EInstance) type types = t type constr = t @@ -445,38 +461,28 @@ let fold sigma f acc c = match kind sigma c with let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 = (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2 -let eq_einstance sigma i1 i2 = - let i1 = EInstance.kind sigma (EInstance.make i1) in - let i2 = EInstance.kind sigma (EInstance.make i2) in - Univ.Instance.equal i1 i2 - -let eq_esorts sigma s1 s2 = - let s1 = ESorts.kind sigma (ESorts.make s1) in - let s2 = ESorts.kind sigma (ESorts.make s2) in - Sorts.equal s1 s2 - let eq_constr sigma c1 c2 = - let kind c = kind_upto sigma c in - let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in - let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in + let kind c = kind sigma c in + let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in + let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in let rec eq_constr nargs c1 c2 = compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2 in - eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2) + eq_constr 0 c1 c2 let eq_constr_nounivs sigma c1 c2 = - let kind c = kind_upto sigma c in + let kind c = kind sigma c in let rec eq_constr nargs c1 c2 = compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2 in - eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2) + eq_constr 0 c1 c2 let compare_constr sigma cmp c1 c2 = - let kind c = kind_upto sigma c in - let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in - let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in - let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in - compare_gen kind eq_inst eq_sorts cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2) + let kind c = kind sigma c in + let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in + let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in + let cmp nargs c1 c2 = cmp c1 c2 in + compare_gen kind eq_inst eq_sorts cmp 0 c1 c2 let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = let open UnivProblem in @@ -528,10 +534,10 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2) let eq_universes env sigma cstrs cv_pb ref nargs l l' = - if Univ.Instance.is_empty l then (assert (Univ.Instance.is_empty l'); true) + if EInstance.is_empty l then (assert (EInstance.is_empty l'); true) else - let l = Evd.normalize_universe_instance sigma l - and l' = Evd.normalize_universe_instance sigma l' in + let l = EInstance.kind sigma l + and l' = EInstance.kind sigma l' in let open GlobRef in let open UnivProblem in match ref with @@ -549,7 +555,7 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' = let test_constr_universes env sigma leq m n = let open UnivProblem in - let kind c = kind_upto sigma c in + let kind c = kind sigma c in if m == n then Some Set.empty else let cstrs = ref Set.empty in @@ -557,16 +563,16 @@ let test_constr_universes env sigma leq m n = let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l' and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in let eq_sorts s1 s2 = - let s1 = ESorts.kind sigma (ESorts.make s1) in - let s2 = ESorts.kind sigma (ESorts.make s2) in + let s1 = ESorts.kind sigma s1 in + let s2 = ESorts.kind sigma s2 in if Sorts.equal s1 s2 then true else (cstrs := Set.add (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs; true) in let leq_sorts s1 s2 = - let s1 = ESorts.kind sigma (ESorts.make s1) in - let s2 = ESorts.kind sigma (ESorts.make s2) in + let s1 = ESorts.kind sigma s1 in + let s2 = ESorts.kind sigma s2 in if Sorts.equal s1 s2 then true else (cstrs := Set.add @@ -587,16 +593,16 @@ let test_constr_universes env sigma leq m n = if res then Some !cstrs else None let eq_constr_universes env sigma m n = - test_constr_universes env sigma false (unsafe_to_constr m) (unsafe_to_constr n) + test_constr_universes env sigma false m n let leq_constr_universes env sigma m n = - test_constr_universes env sigma true (unsafe_to_constr m) (unsafe_to_constr n) + test_constr_universes env sigma true m n let compare_head_gen_proj env sigma equ eqs eqc' nargs m n = - let kind c = kind_upto sigma c in - match kind_upto sigma m, kind_upto sigma n with + let kind c = kind sigma c in + match kind m, kind n with | Proj (p, c), App (f, args) | App (f, args), Proj (p, c) -> - (match kind_upto sigma f with + (match kind f with | Const (p', u) when Constant.equal (Projection.constant p) p' -> let npars = Projection.npars p in if Array.length args == npars + 1 then @@ -612,6 +618,8 @@ let eq_constr_universes_proj env sigma m n = let cstrs = ref Set.empty in let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in let eq_sorts s1 s2 = + let s1 = ESorts.kind sigma s1 in + let s2 = ESorts.kind sigma s2 in if Sorts.equal s1 s2 then true else (cstrs := Set.add @@ -621,7 +629,7 @@ let eq_constr_universes_proj env sigma m n = let rec eq_constr' nargs m n = m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' nargs m n in - let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in + let res = eq_constr' 0 m n in if res then Some !cstrs else None let universes_of_constr sigma c = diff --git a/engine/termops.ml b/engine/termops.ml index 710743e92d..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 @@ -98,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 @@ -1537,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 9ce2db9234..aa0f837938 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -311,18 +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 -(** Internal hook to register user-level printer *) +module Internal : sig -val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit +(** NOTE: to print terms you always want to use functions in + Printer, not these ones which are for very special cases. *) -(** User-level printers *) +(** 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 -val print_constr : 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 -(** debug printer: do not use to display terms to the casual user... *) +(** [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] *) |