Document universe "normalization"

[ejgallego]

Please document the several nf_* functions spread over Evarutil, Evd, and Universes. In particular, we need:

• detailed documentation of the purpose and cost of each one
• detailed documentation on how they are supposed to work together. For example, what is the proper order of calls?
• detailed relative documentation, which ones are a superset of others, and which ones are the composition of available substitution operators.

A few of the functions:

evarutil: val nf_evar :  evar_map -> constr -> constr
evarutil: val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment
evarutil: val jl_nf_evar : evar_map -> unsafe_judgment list -> unsafe_judgment list
evarutil: val jv_nf_evar : evar_map -> unsafe_judgment array -> unsafe_judgment array
evarutil: val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment
evarutil: val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
evarutil: val nf_rel_context_evar : evar_map -> rel_context -> rel_context
evarutil: val nf_env_evar : evar_map -> env -> env
evarutil: val nf_evar_info : evar_map -> evar_info -> evar_info
evarutil: val nf_evar_map : evar_map -> evar_map
evarutil: val nf_evar_map_undefined : evar_map -> evar_map
evarutil: val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr
evarutil: val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
evarutil: val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst
evarutil: val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
evd:      val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
evd:      val nf_constraints : evar_map -> evar_map
evd:      val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
evd:      val normalize_universe : evar_map -> Univ.Universe.t -> Univ.Universe.t
evd:      val normalize_universe_instance : evar_map -> Univ.Instance.t -> Univ.Instance.t
universes:val nf_evars_and_universes_opt_subst : (existential -> constr option) -> universe_opt_subst -> constr -> constr
universes:val normalize_context_set : ContextSet.t -> universe_opt_subst -> LSet.t -> (universe_opt_subst * LSet.t) in_universe_context_set
universes:val normalize_univ_variables : universe_opt_subst -> universe_opt_subst * LSet.t * LSet.t * universe_subst
universes:val normalize_univ_variable : find:(Level.t -> Universe.t) -> update:(Level.t -> Universe.t -> Universe.t) -> Level.t -> Universe.t
universes:val normalize_univ_variable_opt_subst : universe_opt_subst ref -> (Level.t -> Universe.t)
universes:val normalize_univ_variable_subst : universe_subst ref -> (Level.t -> Universe.t)
universes:val normalize_universe_opt_subst : universe_opt_subst ref -> (Universe.t -> Universe.t)
universes:val normalize_universe_subst : universe_subst ref -> (Universe.t -> Universe.t)
evardefine.mli:val env_nf_evar : evar_map -> env -> env
evardefine.mli:val env_nf_betaiotaevar : evar_map -> env -> env
reductionops.mli:val nf_evar : evar_map -> constr -> constr

[mattam82]

Will do, pinned it, but don’t hesitate to ping me again if I don’t abide :) Le mer. 13 déc. 2017 à 04:42, Emilio Jesús Gallego Arias < notifications@github.com> a écrit :

Please document the several nf_* functions spread over Evarutil, Evd, and Universes. In particular, we need:

• detailed documentation of the purpose and cost of each one
• detailed documentation on how they are supposed to work together. For example, what is the proper order of calls?
• detailed relative documentation, which ones are a superset of others.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/coq/coq/issues/6414, or mute the thread https://github.com/notifications/unsubscribe-auth/AAGARTYswPryd-pJjTcPo--J9dZ2Pw_3ks5s_1WpgaJpZM4RAAOV .

[ejgallego]

Thanks Matthieu

[ejgallego]

@SkySkimmer points at #6443:

nf_evars_and_universes and nf_constraints return the same evar_map, and also returns a nf function to perform normalization [not necessary when using EConstr].

[SkySkimmer]

"Don't use any more" was in that specific case, it might still be used in other places where it should eventually be replaced by econstr.

[ejgallego]

Oh indeed I copied too much, sorry. Comment amended.

[ejgallego]

Comment by @SkySkimmer on Gitter:

things to do when declaring something:

• minimize universes (technically optional but you really should do it)
• evar and univ-normalize your term (to_constr)
• restrict universes (technically optional but you really should do it)
• produce a universe entry
• produce universe binders (optional, you should probably do it though)
• send things off to the kernel (and extra feature management like implicits and universe binders etc)
• interp_constr returns a UState and an econstr with no evars, so we work with the ustate api. There are corresponding wrappers in Evd for evar maps with similar names when you interp in a way that returns an evar_map.

---

• minimize is UState.minimize

• you need to re-evar-and-univ-normalize your constr after minimization so wrap the minimized ustate (to pass to to_constr) using Evd.from_ctx

• for restrict you need to get the universe variables appearing in your Constr.t using Univops.universes_of_constr (comDefinition uses the econstr version because of Program silliness), then pass them to UState.restrict

• then you get the universes in the kernel format using UState.constr_univ_entry (check_univ_decl if you have a universe declaration, the @{i j} in Definition foo@{i j} ...)

• if your constr is from parsing it can probably have universe names so you should use DeclareDef.declaredefinition (the alternative would Declare.declare{constant,definition}).

• the entry argument is a record type, you can build it by hand or using Declare.definition_entry (it's just a wrapper function, slightly simplified because intended for non Qed and maybe slightly more stable for not-in-CI plugins but not by much)

• the universe_binders argument is gotten through UState.universe_binders

• the other arguments aren't really my domain, ask the crowd if you want to know about them

FIN

[ejgallego]

Some more example code from @SkySkimmer :+1:

let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
  let open EConstr in
  let env = Global.env () in
  let sigma = Evd.minimize_universes sigma in
  let body = to_constr sigma body in
  let tyopt = Option.map (to_constr sigma) tyopt in
  let uvars_fold uvars c =
    Univ.LSet.union uvars (Univops.universes_of_constr env c)
  in
  let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [body]) in
  let sigma = Evd.restrict_universe_context sigma uvars in
  let univs = Evd.check_univ_decl ~poly sigma udecl in
  let ubinders = Evd.universe_binders sigma in
  let ce = Declare.definition_entry ?types:tyopt ~univs body in
  declare_definition ident k ce ubinders imps hook

[SkySkimmer]

A few of the functions:

Can you update that list removing the deprecated ones?

[ejgallego]

Sure , I'll try, but feel absolutely free to edit it yourself of course.

[maximedenes]

Any ETA for this? I think it is a priority, this API is impossible to use today by lack of documentation.