Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

This commit adds full universe polymorphism to Coq.

Add [Polymorphic] and [Monomorphic] local flag for definitions as well as
[Set Universe Polymorphism] global flag to make all following definitions
polymorphic. Mainly syntax for now.

First part of the big changes to the kernel:
- Const, Ind, Construct now come with a universe level instance
- It is used for type inference in the kernel, which now also takes
a graph as input: actually a set of local universe variables and their
constraints. Type inference just checks that the constraints are enough
to satisfy its own rules.
- Remove polymorphic_arity and _knowing_parameters everywhere: we
don't need full applications for polymorphism to apply anymore, as
we generate fresh variables at each constant/inductive/constructor
application. However knowing_parameters variants might be reinstated
later for optimization.
- New structures exported in univ.mli:
  - universe_list for universe level instances
  - universe_context(_set) for the local universe constraints, also
recording which variables will be local and hence generalized after
inference if defining a polymorphic ind/constant.
- this patch makes coq stop compiling at indtypes.ml

Adapt kernel, library, pretyping, tactics and toplevel to universe polymorphism.
Various degrees of integration, places where I was not sure what to do or
just postponed bigger reorganizations of the code are marked with FIXMEs.
Main changes:
- Kernel now checks constraints and does not infer them anymore.
- The inference functions produce a context of constraints that were checked
during inference, useful to do double-checking of the univ. poly. code
but might be removed later.
- Constant, Inductive entries now have a universe context (local variables
and constraints) associated to them.
- Printing, debugging functions for the new structures are also implemented.
- Now stopping at Logic.v
- Lots of new code in kernel/univ.ml that should be reviewed.
- kernel/indtypes probably does not do what's right when inferring inductive
type constraints.
- Adapted evd to use the new universe context structure.
- Did not deal with unification/evar_conv.

- Add externalisation code for universe level instances.
- Support for polymorphism in pretyping/command and proofs/proofview etc.
  Needed wrapping of [fresh_.._instance] through the evar_map, which
  contains the local state of universes during type-checking.
- Correct the inductive scheme generation to support polymorphism as well.
- Have to review kernel code for correctness, and especially rework the
  computation of universe constraints for inductives.
Stops somewhat later in Logic.v

- Fix naming of local/toplevel universes to be correctly done at typechecking time:
  local variables have no dirpath.
- Add code to do substitution of universes in modules, not finished yet.
- Move fresh_* functions out of kernel, it won't ever build a universe level again!
- Adapt a lot of new_Type to use the correct dirpath and declare the new types in the evar_map
so we keep track of them.
- A bit of code factorization (evd_comb moved, pretype_global).

- Refactor more code
- Adapt plugins code (sometimes wrong, marked with FIXME)
- Fix cases generating unneeded universe (not sure it's ok though)
- Fix scheme generation for good, might have opportunity to cleanup
the terms later.

Init compiles now (which means rewrite, inversion, elim etc.. work as well).
- Unsolved issue of pretyping to lower sorts properly (to Prop for example).
  This has to do with the (Retyping.get_type_of) giving algebraic universes that
  would appear on the right of constraints.
  This makes checking for dangling universes at the end of pretyping fail,
  hence the check in kernel/univ was removed. It should come back when we have
  a fix for this.
- Correctly (?) compute the levels of inductive types.
  Removed old code pertaining to universe polymorphism. Note that we generate
  constraint variables for the conclusion of inductive types invariably.
- Shrink constraints before going to the kernel, combine substitution of the
  smaller universe set with normalization of evars (maybe not done everywhere,
  only ordinary inductives, definitions and proofs)
- More API reworks overall. tclPUSHCONTEXT can be used to add fresh universes
  to the proof goal (used in a few places to get the right instance.
- Quick fix for auto that won't work in the long run. It should always have been
  restricted to take constant references as input, without any loss of generality
  over constrs.

Fix some plugins and insertion of non-polymorphic constants in a module.
Now stops in relation classes.

Cleanup and move code from kernel to library and from pretyping to library too.
Now there is a unique universe counter declared in library/universes.ml along
with all the functions to generate new universes and get fresh constant/inductive
terms.
- Various function renamings
- One important change in kernel/univ.ml: now [sup] can be applied to Prop.
- Adapt records/classes to universe polymorphism
- Now stops in EqDepFacts due to imprecise universe polymorphism.

Forgot to git add those files.

interp_constr returns the universe context

The context is then pushed through the environment (or proof goal
sigma).
- Fix insertion of constants/inductives in env, pushing constraints to
the global env for non-polymorphic ones.
- Add Prop as a universe level to do proper type inference with sorts.
It is allowed to take [sup] of [Prop] now.
- New nf_evar based on new Evd.map(_undefined)
- In proofs/logic.ml: conv_leq_goal might create some constraints that
are now recorded.
- Adapt Program code to universes.

Merge with latest trunk + fixes

-Use new constr_of_global from universes
- fix eqschemes to use polymorphic universes
- begin fixing cctac but f_equal still fails
- fix [simpl] and rest of tacred
- all the eq_constr with mkConst foo should be fixed as well, only
partially done

- Fix term hashing function to recognize equal terms up to universe instances.
- Fix congruence closure to equate terms that differ only in universe instances,
these will be resolved by constraints.

Add a set of undefined universe variables to unification.
Universe variables can now be declared rigid or flexible (unifiable).
Flexible variables are resolved at the end of typechecking by instantiating
them to their glb, adding upper bound constraints associated to them.
Also:
- Add polymorphic flag for inductives.
- Fix cooking partially
- Fix kernel/univ.ml to do normalization of universe expressions at
the end of substitution.

Correct classes/structures universe inference

- Required a bit of extension in Univ to handle Max properly (sup u
(u+1)) was returning (max(u,u+1)) for example.
- Try a version where substitution of universe expressions for universe
levels is allowed at the end of unification. By an invariant this
should only instantiate with max() types that are morally "on the
right" only.
This is controlled using a rigidity attribute of universe variables,
also allowing to properly do unification w.r.t. universes during
typechecking/inference.
- Currently fails in Vectors/Fin.v because case compilation generates
"flexible" universes that actually appear in the term...

Fix unification of universe variables.

- Fix choice of canonical universe in presence of universe constraints,
and do so by relying on a trichotomy for universe variables: rigid
(won't be substituted), flexible (might be if not substituted by an
algebraic) and flexible_alg (always substituted).
- Fix romega code and a few more plugins, most of the standard library
goes through now.
- Had to define some inductives as Polymorphic explicitly to make
proofs go through, more to come, and definitions should be polymorphic
too, otherwise inconsistencies appear quickly (two uses of the same
polymorphic ind through monomorphic functions (like nth on lists of
Props and nats) will fix the monomorphic function's universe with eq
constraints that are incompatible).
- Correct universe polymorphism handling for fixpoint/cofixpoint
definitions.

- Fix romega to use the right universes for list constructors.
- Fix internalization/externalization to deal properly with the
implicit parsing of params.
- Fix fourier tactic w.r.t. GRefs

- Fix substitution saturation of universes.
- Fix number syntax plugin.
- Fix setoid_ring to take its coefficients in a Set rather
than a Type, avoiding a large number of useless universe constraints.

- Fix minor checker decl
- Fix btauto w.r.t. GRef
- Fix proofview to normalize universes in the original types as well.
- Fix definitions of projections to not take two universes at the same level,
but at different levels instead, avoiding unnecessary constraints that could
lower the level of one component depending on the use of the other component.

Fix simpl fst, snd to use @fst @snd as they have maximal implicits now.

- More simpl snd, fst fixes.
- Try to make the nth theory of lists polymorphic.

Check with Enrico if this change is ok. Case appearing in RingMicromega's call
to congruence l417, through a call to refine -> the_conv_x_leq.

Compile everything.
- "Fix" checker by deactivating code related to polymorphism, should
be updated.
- Make most of List.v polymorphic to help with following definitions.
- When starting a lemma, normalize w.r.t. universes, so that the types
get a fixed universe, not refinable later.
- In record, don't assign a fully flexible universe variable to the record
type if it is a definitional typeclass, as translate_constant doesn't expect
an algebraic universe in the type of a constant. It certainly should though.
- Fix micromega code.

Fix after rebase.

Update printing functions to print the polymorphic status of definitions
and their universe context.

Refine printing of universe contexts

- Fix printer for universe constraints
- Rework normalization of constraints to separate the Union-Find result
  from computation of lubs/glbs.

Keep universe contexts of inductives/constants in entries for correct
substitution inside modules. Abstract interface to get an instantiation
of an inductive with its universe substitution in the kernel (no
substitution if the inductive is not polymorphic, even if mind_universes
is non-empty).

Make fst and snd polymorphic, fix instances in RelationPairs to use
different universes for the two elements of a pair.

- Fix bug in nf_constraints: was removing Set <= constraints, but should
remove Prop <= constraints only.
- Make proj1_sig, projT1... polymorphic to avoid weird universe unifications,
giving rise to universe inconsistenties.

Adapt auto hints to polymorphic references.

Really produce polymorphic hints... second try

- Remove algebraic universes that can't appear in the goal when taking the
  type of a lemma to start.

Proper handling of universe contexts in clenv and auto so that
polymorphic hints are really refreshed at each application.

Fix erroneous shadowing of sigma variable.

- Make apparent the universe context used in pretyping, including information
about flexibility of universe variables.
- Fix induction to generate a fresh constant instance with flexible universe variables.

Add function to do conversion w.r.t. an evar map and its local universes.

- Fix define_evar_as_sort to not forget constraints coming from the refinement.
- Do not nf_constraints while we don't have the whole term at hand to substitute in.

- Move substitution of full universes to Universes
- Normalize universes inside an evar_map when doing nf_evar_map_universes.
- Normalize universes at each call to interp_ltac (potentially expensive)

Do not normalize all evars at each call to interp_gen in tactics: rather
incrementally normalize the terms at hand, supposing the normalization of universes
will concern only those appearing in it (dangerous but much more efficient).

Do not needlessly generate new universes constraints for projections of records.

Correct polymorphic discharge of section variables.

Fix autorewrite w.r.t. universes: polymorphic rewrite hints get fresh universe
instances at each application.

Fix r2l rewrite scheme to support universe polymorphism

Fix a bug in l2r_forward scheme and fix congruence scheme to handle polymorphism correctly.

Second try at fixing autorewrite, cannot do without pushing the constraints and the set of fresh
universe variables into the proof context.

- tclPUSHCONTEXT allow to set the ctx universe variables as flexible or rigid
- Fix bug in elimschemes, not taking the right sigma

Wrong sigma used in leibniz_rewrite

Avoid recomputation of bounds for equal universes in normalization of constraints,
only the canonical one need to be computed.

Make coercions work with universe polymorphic projections.

Fix eronneous bound in universes constraint solving.

Make kernel reduction and term comparison strictly aware of universe instances,
with variants for relaxed comparison that output constraints.
Otherwise some constraints that should appear during pretyping don't and we generate
unnecessary constraints/universe variables.
Have to adapt a few tactics to this new behavior by making them universe aware.

- Fix elimschemes to minimize universe variables
- Fix coercions to not forget the universe constraints generated by an application
- Change universe substitutions to maps instead of assoc lists.
- Fix absurd tactic to handle univs properly
- Make length and app polymorphic in List, unification sets their levels otherwise.

Move to modules for namespace management instead of long names in universe code.

More putting things into modules.

Change evar_map structure to support an incremental substitution of universes
(populated from Eq constraints), allowing safe and fast inference of precise levels,
without computing lubs.
- Add many printers and reorganize code
- Extend nf_evar to normalize universe variables according to the substitution.
- Fix ChoiceFacts.v in Logic, no universe inconsistencies anymore. But Diaconescu
still has one (something fixes a universe to Set).
- Adapt omega, functional induction to the changes.

Fix congruence, eq_constr implem, discharge of polymorphic inductives.

Fix merge in auto.

The [-parameters-matter] option (formerly relevant_equality).

Add -parameters-matter to coqc

Do compute the param levels at elaboration time if parameters_matter.

- Fix generalize tactic
- add ppuniverse_subst
- Start fixing normalize_universe_context w.r.t. normalize_univ_variables.

- Fix HUGE bug in Ltac interpretation not folding the sigma correctly if interpreting a tactic application
to multiple arguments.
- Fix bug in union of universe substitution.

- rename parameters-matter to indices-matter
- Fix computation of levels from indices not parameters.

- Fixing parsing so that [Polymorphic] can be applied to gallina extensions.
- When elaborating definitions, make the universes from the type rigid when
checking the term: they should stay abstracted.
- Fix typeclasses eauto's handling of universes for exact hints.

Rework all the code for infering the levels of inductives and checking their
allowed eliminations sorts.

This is based on the computation of a natural level for an inductive type I.
The natural level [nat] of [I : args -> sort := c1 : A1 -> I t1 .. cn : An -> I tn] is
computed by taking the max of the levels of the args (if indices matter) and the
levels of the constructor arguments.
The declared level [decl] of I is [sort], which might be Prop, Set or some Type u (u fresh
or not).
If [decl >= nat && not (decl = Prop && n >= 2)], the level of the inductive is [decl],
otherwise, _smashing_ occured.
If [decl] is impredicative (Prop or Set when Set is impredicative), we accept the
declared level, otherwise it's an error.

To compute the allowed elimination sorts, we have the following situations:
- No smashing occured: all sorts are allowed. (Recall props that are not
smashed are Empty/Unitary props)
- Some smashing occured:
 - if [decl] is Type, we allow all eliminations (above or below [decl],
   not sure why this is justified in general).
 - if [decl] is Set, we used smashing for impredicativity, so only
   small sorts are allowed (Prop, Set).
 - if [decl] is Prop, only logical sorts are allowed: I has either
   large universes inside it or more than 1 constructor.
   This does not treat the case where only a Set appeared in I which
   was previously accepted it seems.

All the standard library works with these changes. Still have to cleanup
kernel/indtypes.ml. It is a good time to have a whiskey with OJ.

Thanks to Peter Lumsdaine for bug reporting:
- fix externalisation of universe instances (still appearing when no Printing Universes)
- add [convert] and [convert_leq] tactics that keep track of evars and universe constraints.
- use them in [exact_check].

Fix odd behavior in inductive type declarations allowing to silently lower a Type i parameter
to Set for squashing a naturally Type i inductive to Set. Reinstate the LargeNonPropInductiveNotInType
exception.

Fix the is_small function not dealing properly with aliases of Prop/Set in Type.

Add check_leq in Evd and use it to decide if we're trying to squash an
inductive naturally in some Type to Set.

- Fix handling of universe polymorphism in typeclasses Class/Instance declarations.
- Don't allow lowering a rigid Type universe to Set silently.

- Move Ring/Field back to Type. It was silently putting R in Set due to the definition of ring_morph.
- Rework inference of universe levels for inductive definitions.
- Make fold_left/right polymorphic on both levels A and B (the list's type). They don't have to be
at the same level.

Handle selective Polymorphic/Monomorphic flag right for records.

Remove leftover command

Fix after update with latest trunk.

Backport patches on HoTT/coq to rebased version of universe polymorphism.

- Fix autorewrite wrong handling of universe-polymorphic rewrite rules. Fixes part of issue #7.
- Fix the [eq_constr_univs] and add an [leq_constr_univs] to avoid eager equation of universe
 levels that could just be inequal. Use it during kernel conversion. Fixes issue #6.
- Fix a bug in unification that was failing too early if a choice in unification of universes
 raised an inconsistency.
- While normalizing universes, remove Prop in the le part of Max expressions.
- Stop rigidifying the universes on the right hand side of a : in definitions.
- Now Hints can be declared polymorphic or not. In the first case they
 must be "refreshed" (undefined universes are renamed) at each application.
- Have to refresh the set of universe variables associated to a hint
 when it can be used multiple times in a single proof to avoid fixing
 a level... A better & less expensive solution should exist.
- Do not include the levels of let-ins as part of records levels.
- Fix a NotConvertible uncaught exception to raise a more informative
 error message.
- Better substitution of algebraics in algebraics (for universe variables that
 can be algebraics).
- Fix issue #2, Context was not properly normalizing the universe context.
- Fix issue with typeclasses that were not catching UniverseInconsistencies
  raised by unification, resulting in early failure of proof-search.
- Let the result type of definitional classes be an algebraic.
- Adapt coercions to universe polymorphic flag (Identity Coercion etc..)
- Move away a dangerous call in autoinstance that added constraints for every
polymorphic definitions once in the environment for no use.

Forgot one part of the last patch on coercions.

- Adapt auto/eauto to polymorphic hints as well.
- Factor out the function to refresh a clenv w.r.t. undefined universes.

Use leq_univ_poly in evarconv to avoid fixing universes.

Disallow polymorphic hints based on a constr as it is not possible to infer their universe
context. Only global references can be made polymorphic. Fixes issue #8.

Fix SearchAbout bug (issue #10).

Fix program w.r.t. universes: the universe context of a definition changes
according to the successive refinements due to typechecking obligations.
This requires the Proof modules to return the generated universe substitution
when finishing a proof, and this information is passed in the closing hook.
The interface is not very clean, will certainly change in the future.

- Better treatment of polymorphic hints in auto: terms can be polymorphic now, we refresh their
context as well.
- Needs a little change in test-pattern that seems breaks multiary uses of destruct in NZDiv.v, l495.
FIX to do.

Fix [make_pattern_test] to keep the universe information around and still
allow tactics to take multiple patterns at once.

- Fix printing of universe instances that should not be factorized blindly
- Fix handling of the universe context in program definitions by allowing the
hook at the end of an interactive proof to give back the refined universe context,
before it is transformed in the kernel.
- Fix a bug in evarconv where solve_evar_evar was not checking types of instances,
resulting in a loss of constraints in unification of universes and a growing number
of useless parametric universes.

- Move from universe_level_subst to universe_subst everywhere.

- Changed representation of universes for a canonical one
- Adapt the code so that universe variables might be substituted by
arbitrary universes (including algebraics). Not used yet except for
polymorphic universe variables instances.

- Adapt code to new constraint structure.
- Fix setoid rewrite handling of evars that was forgetting the initial
universe substitution !
- Fix code that was just testing conversion instead of keeping the
resulting universe constraints around in the proof engine.
- Make a version of reduction/fconv that deals with the more general
set of universe constraints.

- [auto using] should use polymorphic versions of the constants.
- When starting a proof, don't forget about the algebraic universes in
the universe context.

Rationalize substitution and normalization functions for universes.
Also change back the structure of universes to avoid considering levels
n+k as pure levels: they are universe expressions like max.
Everything is factored out in the Universes and Univ modules now and
the normalization functions can be efficient in the sense that they
can cache the normalized universes incrementally.

- Adapt normalize_context code to new normalization/substitution functions.
- Set more things to be polymorphic, e.g. in Ring or SetoidList for the rest
of the code to work properly while the constraint generation code is not adapted.
And temporarily extend the universe constraint code in univ to solve max(is) = max(js)
by first-order unification (these constraints should actually be implied not enforced).
- Fix romega plugin to use the right universes for polymorphic lists.
- Fix auto not refreshing the poly hints correctly.

- Proper postponing of universe constraints during unification, avoid making
arbitrary choices.
- Fix nf_evars_and* to keep the substitution around for later normalizations.
- Do add simplified universe constraints coming from unification during typechecking.
- Fix solve_by_tac in obligations to handle universes right, and the corresponding
substitution function.

Test global universe equality early during simplication of constraints.

Better hashconsing, but still not good on universe lists.

- Add postponing of "lub" constraints that should not be checked early,
they are implied by the others.
- Fix constructor tactic to use a fresh constructor instance avoiding
fixing universes.
- Use [eq_constr_universes] instead of [eq_constr_univs] everywhere,
this is the comparison function that doesn't care about the universe
instances.
- Almost all the library compiles in this new setting, but some more tactics
need to be adapted.

- Reinstate hconsing.
- Keep Prop <= u constraints that can be used to set the level of a universe
metavariable.

Add better hashconsing and unionfind in normalisation of constraints.
Fix a few problems in choose_canonical, normalization and substitution functions.

Fix after merge

Fixes after rebase with latest Coq trunk, everything compiles again,
albeit slowly in some cases.
- Fix module substitution and comparison of table keys in conversion
using the wrong order (should always be UserOrd now)
- Cleanup in universes, removing commented code.
- Fix normalization of universe context which was assigning global
levels to local ones. Should always be the other way!
- Fix universe implementation to implement sorted cons of universes
preserving order. Makes Univ.sup correct again, keeping universe in
normalized form.
- In evarconv.ml, allow again a Fix to appear as head of a weak-head normal
form (due to partially applied fixpoints).
- Catch anomalies of conversion as errors in reductionops.ml, sad but
necessary as eta-expansion might build ill-typed stacks like FProd,
[shift;app Rel 1], as it expands not only if the other side is rigid.
- Fix module substitution bug in auto.ml

- Fix case compilation: impossible cases compilation was generating useless universe
levels. Use an IDProp constant instead of the polymorphic identity to not influence
the level of the original type when building the case construct for the return type.
- Simplify normalization of universe constraints.
- Compute constructor levels of records correctly.

Fall back to levels for universe instances, avoiding issues of unification.
Add more to the test-suite for universe polymorphism.

Fix after rebase with trunk

Fix substitution of universes inside fields/params of records to be made
after all normalization is done and the level of the record has been
computed.

Proper sharing of lower bounds with fixed universes.

Conflicts:
	library/universes.ml
	library/universes.mli

Constraints were not enforced in compilation of cases

Fix after rebase with trunk

- Canonical projections up to universes
- Fix computation of class/record universe levels to allow
squashing to Prop/Set in impredicative set mode.

- Fix descend_in_conjunctions to properly instantiate projections with universes
- Avoid Context-bound variables taking extra universes in their associated universe context.

- Fix evar_define using the wrong direction when refreshing a universe under cumulativity
- Do not instantiate a local universe with some lower bound to a global one just because
they have the same local glb (they might not have the same one globally).

- Was loosing some global constraints during normalization (brought again by the kernel), fixed now.
- Proper [abstract] with polymorphic lemmas (polymorphic if the current proof is).
- Fix silly bug in autorewrite: any hint after the first one was always monomorphic.

- Fix fourier after rebase
- Refresh universes when checking types of metas in unification (avoid (sup (sup univ))).
- Speedup a script in FSetPositive.v

Rework definitions in RelationClasses and Morphisms to share universe
levels as much as possible. This factorizes many useless x <=
RelationClasses.foo constraints in code that uses setoid rewriting.
Slight incompatible change in the implicits for Reflexivity and
Irreflexivity as well.

- Share even more universes in Morphisms using a let.
- Use splay_prod instead of splay_prod_assum which doesn't reduce let's
to find a relation in setoid_rewrite
- Fix [Declare Instance] not properly dealing with let's in typeclass contexts.

Fixes in inductiveops, evarutil.

Patch by Yves Bertot to allow naming universes in inductive definitions.

Fixes in tacinterp not propagating evars correctly.

Fix for issue #27: lowering a Type to Prop is allowed during
inference (resulting in a Type (* Set *)) but kernel reduction
was wrongly refusing the equation [Type (*Set*) = Set].
  • Loading branch information...
commit 40a379bf1966531489ba9f0fe0df90437b357e3e 1 parent f98de3a
@mattam82 mattam82 authored
Showing with 8,859 additions and 4,369 deletions.
  1. +1 −0  .gitignore
  2. +15 −1 Makefile
  3. +13 −34 checker/declarations.ml
  4. +4 −15 checker/declarations.mli
  5. +1 −1  checker/environ.ml
  6. +12 −12 checker/indtypes.ml
  7. +19 −23 checker/inductive.ml
  8. +2 −2 checker/inductive.mli
  9. +18 −18 checker/mod_checking.ml
  10. +1 −1  checker/term.ml
  11. +25 −26 checker/typeops.ml
  12. +3 −3 checker/typeops.mli
  13. +1 −0  dev/base_include
  14. +15 −2 dev/include
  15. +7 −0 dev/printers.mllib
  16. +49 −15 dev/top_printers.ml
  17. +2 −2 grammar/q_constr.ml4
  18. +4 −3 grammar/q_coqast.ml4
  19. +16 −10 interp/constrexpr_ops.ml
  20. +24 −20 interp/constrextern.ml
  21. +42 −34 interp/constrintern.ml
  22. +16 −11 interp/constrintern.mli
  23. +37 −6 interp/coqlib.ml
  24. +2 −0  interp/coqlib.mli
  25. +9 −9 interp/implicit_quantifiers.ml
  26. +1 −1  interp/modintern.ml
  27. +7 −7 interp/notation.ml
  28. +6 −6 interp/notation_ops.ml
  29. +4 −4 interp/topconstr.ml
  30. +2 −2 intf/constrexpr.mli
  31. +5 −3 intf/decl_kinds.mli
  32. +1 −1  intf/glob_term.mli
  33. +7 −6 intf/vernacexpr.mli
  34. +9 −9 kernel/cbytegen.ml
  35. +4 −4 kernel/cemitcodes.ml
  36. +16 −13 kernel/closure.ml
  37. +3 −3 kernel/closure.mli
  38. +3 −3 kernel/conv_oracle.mli
  39. +41 −29 kernel/cooking.ml
  40. +4 −4 kernel/cooking.mli
  41. +9 −18 kernel/declarations.mli
  42. +17 −31 kernel/declareops.ml
  43. +9 −4 kernel/entries.mli
  44. +110 −32 kernel/environ.ml
  45. +23 −3 kernel/environ.mli
  46. +170 −145 kernel/indtypes.ml
  47. +6 −2 kernel/indtypes.mli
  48. +97 −117 kernel/inductive.ml
  49. +25 −18 kernel/inductive.mli
  50. +34 −10 kernel/mod_subst.ml
  51. +18 −1 kernel/mod_subst.mli
  52. +32 −29 kernel/mod_typing.ml
  53. +4 −4 kernel/modops.ml
  54. +15 −8 kernel/names.ml
  55. +8 −3 kernel/names.mli
  56. +3 −3 kernel/nativecode.ml
  57. +1 −1  kernel/nativeconv.ml
  58. +3 −3 kernel/nativelambda.ml
  59. +84 −22 kernel/reduction.ml
  60. +12 −1 kernel/reduction.mli
  61. +46 −23 kernel/safe_typing.ml
  62. +10 −1 kernel/safe_typing.mli
  63. +3 −0  kernel/sign.ml
  64. +2 −0  kernel/sign.mli
  65. +30 −18 kernel/subtyping.ml
  66. +245 −29 kernel/term.ml
  67. +52 −6 kernel/term.mli
  68. +55 −51 kernel/term_typing.ml
  69. +9 −5 kernel/term_typing.mli
  70. +3 −3 kernel/type_errors.ml
  71. +5 −5 kernel/type_errors.mli
  72. +93 −112 kernel/typeops.ml
  73. +29 −24 kernel/typeops.mli
  74. +1,358 −323 kernel/univ.ml
  75. +286 −29 kernel/univ.mli
  76. +14 −6 kernel/vconv.ml
  77. +5 −5 lib/cList.ml
  78. +2 −1  lib/cList.mli
  79. +12 −0 lib/flags.ml
  80. +8 −0 lib/flags.mli
  81. +2 −6 library/assumptions.ml
  82. +28 −19 library/declare.ml
  83. +3 −3 library/declare.mli
  84. +6 −5 library/decls.ml
  85. +2 −1  library/decls.mli
  86. +34 −8 library/global.ml
  87. +19 −7 library/global.mli
  88. +32 −17 library/globnames.ml
  89. +5 −5 library/globnames.mli
  90. +8 −5 library/heads.ml
  91. +13 −11 library/impargs.ml
  92. +23 −18 library/lib.ml
  93. +8 −9 library/lib.mli
  94. +1 −0  library/library.mllib
  95. +599 −0 library/universes.ml
  96. +157 −0 library/universes.mli
  97. +2 −2 parsing/egramcoq.ml
  98. +7 −7 parsing/g_constr.ml4
  99. +8 −4 parsing/g_proofs.ml4
  100. +1 −1  parsing/g_tactic.ml4
  101. +51 −26 parsing/g_vernac.ml4
  102. +3 −3 parsing/g_xml.ml4
  103. +1 −1  plugins/btauto/refl_btauto.ml
  104. +14 −14 plugins/cc/ccalgo.ml
  105. +1 −1  plugins/cc/ccalgo.mli
  106. +1 −1  plugins/cc/ccproof.ml
  107. +1 −1  plugins/cc/ccproof.mli
  108. +69 −72 plugins/cc/cctac.ml
  109. +1 −0  plugins/cc/cctac.mli
  110. +13 −13 plugins/decl_mode/decl_interp.ml
  111. +15 −14 plugins/decl_mode/decl_proof_instr.ml
  112. +2 −2 plugins/decl_mode/g_decl_mode.ml4
  113. +1 −1  plugins/extraction/extract_env.ml
  114. +28 −26 plugins/extraction/extraction.ml
  115. +2 −2 plugins/extraction/table.ml
  116. +16 −16 plugins/firstorder/formula.ml
  117. +9 −9 plugins/firstorder/formula.mli
  118. +1 −1  plugins/firstorder/ground.ml
  119. +3 −1 plugins/firstorder/instances.ml
  120. +6 −6 plugins/firstorder/rules.ml
  121. +4 −4 plugins/firstorder/rules.mli
  122. +3 −3 plugins/firstorder/sequent.ml
  123. +1 −1  plugins/firstorder/unify.ml
  124. +7 −7 plugins/fourier/fourierR.ml
  125. +13 −11 plugins/funind/functional_principles_proofs.ml
  126. +29 −24 plugins/funind/functional_principles_types.ml
  127. +4 −4 plugins/funind/g_indfun.ml4
  128. +38 −38 plugins/funind/glob_term_to_relation.ml
  129. +1 −1  plugins/funind/glob_termops.ml
  130. +18 −20 plugins/funind/indfun.ml
  131. +11 −8 plugins/funind/indfun_common.ml
  132. +1 −1  plugins/funind/indfun_common.mli
  133. +27 −23 plugins/funind/invfun.ml
  134. +5 −9 plugins/funind/merge.ml
  135. +22 −18 plugins/funind/recdef.ml
  136. +3 −3 plugins/funind/recdef.mli
  137. +2 −2 plugins/micromega/RingMicromega.v
  138. +6 −6 plugins/micromega/coq_micromega.ml
  139. +5 −5 plugins/omega/coq_omega.ml
  140. +3 −3 plugins/quote/quote.ml
  141. +1 −1  plugins/romega/ReflOmegaCore.v
  142. +20 −13 plugins/romega/const_omega.ml
  143. +1 −0  plugins/romega/const_omega.mli
  144. +14 −12 plugins/setoid_ring/Ring_polynom.v
  145. +1 −2  plugins/setoid_ring/Ring_theory.v
  146. +30 −24 plugins/setoid_ring/newring.ml4
  147. +6 −6 plugins/syntax/ascii_syntax.ml
  148. +5 −5 plugins/syntax/nat_syntax.ml
  149. +23 −23 plugins/syntax/numbers_syntax.ml
  150. +20 −19 plugins/syntax/r_syntax.ml
  151. +6 −6 plugins/syntax/string_syntax.ml
  152. +23 −23 plugins/syntax/z_syntax.ml
  153. +5 −7 plugins/xml/cic2acic.ml
  154. +3 −3 plugins/xml/doubleTypeInference.ml
  155. +6 −6 plugins/xml/xmlcommand.ml
  156. +14 −12 pretyping/arguments_renaming.ml
  157. +4 −4 pretyping/arguments_renaming.mli
  158. +42 −25 pretyping/cases.ml
  159. +6 −6 pretyping/cbv.ml
  160. +1 −1  pretyping/cbv.mli
  161. +35 −30 pretyping/classops.ml
  162. +4 −4 pretyping/classops.mli
  163. +39 −31 pretyping/coercion.ml
  164. +15 −14 pretyping/detyping.ml
  165. +57 −28 pretyping/evarconv.ml
  166. +1 −1  pretyping/evarconv.mli
  167. +28 −7 pretyping/evarsolve.ml
  168. +3 −1 pretyping/evarsolve.mli
  169. +79 −33 pretyping/evarutil.ml
  170. +24 −1 pretyping/evarutil.mli
  171. +533 −78 pretyping/evd.ml
  172. +97 −4 pretyping/evd.mli
  173. +5 −5 pretyping/glob_ops.ml
  174. +78 −63 pretyping/indrec.ml
  175. +16 −14 pretyping/indrec.mli
  176. +40 −67 pretyping/inductiveops.ml
  177. +18 −18 pretyping/inductiveops.mli
  178. +13 −4 pretyping/matching.ml
  179. +3 −3 pretyping/namegen.ml
  180. +13 −13 pretyping/nativenorm.ml
  181. +8 −8 pretyping/patternops.ml
  182. +1 −1  pretyping/pretype_errors.mli
  183. +67 −64 pretyping/pretyping.ml
  184. +14 −6 pretyping/pretyping.mli
  185. +1 −1  pretyping/program.ml
  186. +21 −11 pretyping/recordops.ml
  187. +2 −1  pretyping/recordops.mli
  188. +44 −17 pretyping/reductionops.ml
  189. +4 −1 pretyping/reductionops.mli
  190. +14 −24 pretyping/retyping.ml
  191. +1 −2  pretyping/retyping.mli
  192. +154 −104 pretyping/tacred.ml
  193. +3 −3 pretyping/tacred.mli
  194. +3 −3 pretyping/term_dnet.ml
  195. +45 −49 pretyping/termops.ml
  196. +12 −11 pretyping/termops.mli
  197. +56 −26 pretyping/typeclasses.ml
  198. +13 −7 pretyping/typeclasses.mli
  199. +14 −15 pretyping/typing.ml
  200. +1 −1  pretyping/typing.mli
  201. +79 −51 pretyping/unification.ml
  202. +12 −0 pretyping/unification.mli
  203. +15 −14 pretyping/vnorm.ml
  204. +15 −8 printing/ppconstr.ml
  205. +23 −14 printing/ppvernac.ml
  206. +7 −8 printing/prettyp.ml
  207. +36 −11 printing/printer.ml
  208. +7 −0 printing/printer.mli
  209. +1 −2  printing/printmod.ml
  210. +15 −0 proofs/clenv.ml
  211. +5 −0 proofs/clenv.mli
  212. +20 −12 proofs/logic.ml
  213. +6 −4 proofs/pfedit.ml
  214. +7 −5 proofs/pfedit.mli
  215. +2 −2 proofs/proof.ml
  216. +2 −2 proofs/proof.mli
  217. +10 −8 proofs/proof_global.ml
  218. +5 −3 proofs/proof_global.mli
  219. +6 −2 proofs/proofview.ml
  220. +2 −2 proofs/proofview.mli
  221. +13 −0 proofs/refiner.ml
  222. +6 −0 proofs/refiner.mli
  223. +3 −3 proofs/tacmach.ml
  224. +3 −3 proofs/tacmach.mli
  225. +1 −1  scripts/coqc.ml
  226. +161 −93 tactics/auto.ml
  227. +30 −21 tactics/auto.mli
  228. +13 −6 tactics/autorewrite.ml
  229. +2 −1  tactics/autorewrite.mli
  230. +5 −5 tactics/btermdn.ml
  231. +32 −22 tactics/class_tactics.ml4
  232. +3 −3 tactics/contradiction.ml
  233. +25 −13 tactics/eauto.ml4
  234. +1 −1  tactics/elim.ml
  235. +30 −8 tactics/elimschemes.ml
  236. +1 −1  tactics/eqdecide.ml4
  237. +136 −81 tactics/eqschemes.ml
  238. +10 −7 tactics/eqschemes.mli
  239. +61 −48 tactics/equality.ml
  240. +22 −9 tactics/extratactics.ml4
  241. +35 −29 tactics/hipattern.ml4
  242. +3 −3 tactics/hipattern.mli
  243. +15 −12 tactics/inv.ml
  244. +9 −5 tactics/leminv.ml
  245. +2 −2 tactics/nbtermdn.ml
  246. +80 −38 tactics/rewrite.ml4
  247. +5 −4 tactics/tacintern.ml
  248. +38 −17 tactics/tacinterp.ml
  249. +2 −2 tactics/tacsubst.ml
  250. +15 −7 tactics/tacticals.ml
  251. +8 −5 tactics/tacticals.mli
  252. +167 −107 tactics/tactics.ml
  253. +3 −0  tactics/tactics.mli
  254. +3 −3 tactics/tauto.ml4
  255. +5 −5 tactics/termdn.ml
  256. +61 −0 test-suite/success/indelim.v
  257. +173 −2 test-suite/success/polymorphism.v
  258. +1 −1  theories/Arith/Compare_dec.v
  259. +1 −1  theories/Arith/Le.v
  260. +1 −0  theories/Classes/EquivDec.v
  261. +300 −270 theories/Classes/Morphisms.v
  262. +4 −4 theories/Classes/Morphisms_Prop.v
  263. +2 −4 theories/Classes/Morphisms_Relations.v
  264. +223 −201 theories/Classes/RelationClasses.v
  265. +60 −56 theories/Classes/RelationPairs.v
  266. +2 −2 theories/FSets/FMapAVL.v
  267. +3 −4 theories/FSets/FMapList.v
  268. +3 −3 theories/FSets/FSetPositive.v
  269. +16 −10 theories/Init/Datatypes.v
  270. +4 −3 theories/Init/Logic.v
  271. +13 −10 theories/Init/Specif.v
  272. +9 −11 theories/Lists/List.v
  273. +3 −3 theories/Lists/SetoidList.v
  274. +2 −1  theories/Lists/SetoidPermutation.v
  275. +30 −24 theories/Logic/ChoiceFacts.v
  276. +2 −2 theories/Logic/Diaconescu.v
  277. +5 −4 theories/Logic/EqdepFacts.v
  278. +1 −1  theories/MSets/MSetInterface.v
  279. +2 −2 theories/MSets/MSetList.v
  280. +3 −3 theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
  281. +10 −7 theories/Numbers/Cyclic/Int31/Cyclic31.v
  282. +1 −1  theories/Numbers/NatInt/NZParity.v
  283. +0 −1  theories/Numbers/Natural/Abstract/NDefOps.v
  284. +1 −2  theories/Numbers/Natural/Abstract/NStrongRec.v
  285. +2 −2 theories/Numbers/Rational/BigQ/QMake.v
  286. +1 −1  theories/PArith/BinPosDef.v
  287. +3 −3 theories/Program/Wf.v
  288. +1 −1  theories/Reals/SeqSeries.v
  289. +2 −2 theories/Structures/DecidableType.v
  290. +1 −1  theories/Structures/Equalities.v
  291. +4 −4 theories/Structures/GenericMinMax.v
  292. +1 −1  theories/Structures/OrderedType.v
  293. +1 −1  theories/Structures/OrdersFacts.v
  294. +1 −1  theories/Structures/OrdersTac.v
  295. +7 −7 theories/Vectors/VectorDef.v
  296. +1 −1  theories/Vectors/VectorSpec.v
  297. +3 −2 theories/Wellfounded/Lexicographic_Exponentiation.v
  298. +3 −5 theories/ZArith/Wf_Z.v
  299. +5 −4 theories/ZArith/Zcomplements.v
  300. +57 −47 toplevel/auto_ind_decl.ml
Sorry, we could not display the entire diff because too many files (328) changed.
View
1  .gitignore
@@ -154,3 +154,4 @@ ide/index_urls.txt
dev/ocamldoc/html/
dev/ocamldoc/coq.*
dev/ocamldoc/ocamldoc.sty
+dev/myinclude
View
16 Makefile
@@ -237,7 +237,21 @@ devdocclean:
.PHONY: tags
tags:
- echo $(MLIFILES) $(MLSTATICFILES) $(ML4FILES) | sort -r | xargs \
+ echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \
+ etags --language=none\
+ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
+ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
+ "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
+ "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
+ "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
+ "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
+ "--regex=/module[ \t]+\([^ \t]+\)/\1/"
+ echo $(ML4FILES) | sort -r | xargs \
+ etags --append --language=none\
+ "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/"
+
+checker-tags:
+ echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \
etags --language=none\
"--regex=/let[ \t]+\([^ \t]+\)/\1/" \
"--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
View
47 checker/declarations.ml
@@ -16,20 +16,7 @@ type retroknowledge
type engagement = ImpredicativeSet
let val_eng = val_enum "eng" 1
-
-type polymorphic_arity = {
- poly_param_levels : Univ.universe option list;
- poly_level : Univ.universe;
-}
-let val_pol_arity =
- val_tuple ~name:"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|]
-
-type constant_type =
- | NonPolymorphicType of constr
- | PolymorphicArity of rel_context * polymorphic_arity
-
-let val_cst_type =
- val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|]
+let val_cst_type = val_constr
(** Substitutions, code imported from kernel/mod_subst *)
@@ -531,10 +518,13 @@ let subst_constant_def sub = function
| Def c -> Def (subst_constr_subst sub c)
| OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
+(** Local variables and graph *)
+type universe_context = Univ.LSet.t * Univ.constraints
+
type constant_body = {
const_hyps : section_context; (* New: younger hyp at top *)
const_body : constant_def;
- const_type : constant_type;
+ const_type : constr;
const_body_code : to_patch_substituted;
const_constraints : Univ.constraints;
const_native_name : native_name ref;
@@ -611,18 +601,12 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
*)
-type monomorphic_inductive_arity = {
+type inductive_arity = {
mind_user_arity : constr;
mind_sort : sorts;
}
-let val_mono_ind_arity =
- val_tuple ~name:"monomorphic_inductive_arity"[|val_constr;val_sort|]
-
-type inductive_arity =
-| Monomorphic of monomorphic_inductive_arity
-| Polymorphic of polymorphic_arity
-let val_ind_arity = val_sum "inductive_arity" 0
- [|[|val_mono_ind_arity|];[|val_pol_arity|]|]
+let val_ind_arity =
+ val_tuple ~name:"inductive_arity"[|val_constr;val_sort|]
type one_inductive_body = {
@@ -720,9 +704,7 @@ let val_ind_pack = val_tuple ~name:"mutual_inductive_body"
val_int; val_int; val_rctxt;val_cstrs;no_val|]
-let subst_arity sub = function
-| NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
-| PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s)
+let subst_arity sub s = (subst_mps sub s)
(* TODO: should be changed to non-coping after Term.subst_mps *)
(* NB: we leave bytecode and native code fields untouched *)
@@ -732,13 +714,10 @@ let subst_const_body sub cb =
const_body = subst_constant_def sub cb.const_body;
const_type = subst_arity sub cb.const_type }
-let subst_arity sub = function
-| Monomorphic s ->
- Monomorphic {
- mind_user_arity = subst_mps sub s.mind_user_arity;
- mind_sort = s.mind_sort;
- }
-| Polymorphic s as x -> x
+let subst_arity sub s =
+ { mind_user_arity = subst_mps sub s.mind_user_arity;
+ mind_sort = s.mind_sort;
+ }
let subst_mind_packet sub mbp =
{ mind_consnames = mbp.mind_consnames;
View
19 checker/declarations.mli
@@ -17,15 +17,6 @@ type engagement = ImpredicativeSet
(* Constants *)
-type polymorphic_arity = {
- poly_param_levels : Univ.universe option list;
- poly_level : Univ.universe;
-}
-
-type constant_type =
- | NonPolymorphicType of constr
- | PolymorphicArity of rel_context * polymorphic_arity
-
type constr_substituted
val force_constr : constr_substituted -> constr
val from_val : constr -> constr_substituted
@@ -47,10 +38,12 @@ type constant_def =
| Def of constr_substituted
| OpaqueDef of lazy_constr
+(** Local variables and graph *)
+
type constant_body = {
const_hyps : section_context; (* New: younger hyp at top *)
const_body : constant_def;
- const_type : constant_type;
+ const_type : constr;
const_body_code : to_patch_substituted;
const_constraints : Univ.constraints;
const_native_name : native_name ref;
@@ -74,15 +67,11 @@ val mk_paths : recarg -> wf_paths list array -> wf_paths
val dest_recarg : wf_paths -> recarg
val dest_subterms : wf_paths -> wf_paths list array
-type monomorphic_inductive_arity = {
+type inductive_arity = {
mind_user_arity : constr;
mind_sort : sorts;
}
-type inductive_arity =
-| Monomorphic of monomorphic_inductive_arity
-| Polymorphic of polymorphic_arity
-
type one_inductive_body = {
(* Primitive datas *)
View
2  checker/environ.ml
@@ -99,7 +99,7 @@ let named_type id env =
(* Universe constraints *)
let add_constraints c env =
- if c == empty_constraint then
+ if c == Constraint.empty then
env
else
let s = env.env_stratification in
View
24 checker/indtypes.ml
@@ -136,14 +136,14 @@ let typecheck_arity env params inds =
let nparamargs = rel_context_nhyps params in
let nparamdecls = rel_context_length params in
let check_arity arctxt = function
- Monomorphic mar ->
+ mar ->
let ar = mar.mind_user_arity in
let _ = infer_type env ar in
conv env (it_mkProd_or_LetIn (Sort mar.mind_sort) arctxt) ar;
- ar
- | Polymorphic par ->
- check_polymorphic_arity env params par;
- it_mkProd_or_LetIn (Sort(Type par.poly_level)) arctxt in
+ ar in
+ (* | Polymorphic par -> *)
+ (* check_polymorphic_arity env params par; *)
+ (* it_mkProd_or_LetIn (Sort(Type par.poly_level)) arctxt in *)
let env_arities =
Array.fold_left
(fun env_ar ind ->
@@ -175,11 +175,11 @@ let typecheck_arity env params inds =
let check_predicativity env s small level =
match s, engagement env with
Type u, _ ->
- let u' = fresh_local_univ () in
- let cst =
- merge_constraints (enforce_leq u u' empty_constraint)
- (universes env) in
- if not (check_leq cst level u') then
+ (* let u' = fresh_local_univ () in *)
+ (* let cst = *)
+ (* merge_constraints (enforce_leq u u' empty_constraint) *)
+ (* (universes env) in *)
+ if not (check_leq (universes env) level u) then
failwith "impredicative Type inductive type"
| Prop Pos, Some ImpredicativeSet -> ()
| Prop Pos, _ ->
@@ -188,8 +188,8 @@ let check_predicativity env s small level =
let sort_of_ind = function
- Monomorphic mar -> mar.mind_sort
- | Polymorphic par -> Type par.poly_level
+ mar -> mar.mind_sort
+ (* | Polymorphic par -> Type par.poly_level *)
let all_sorts = [InProp;InSet;InType]
let small_sorts = [InProp;InSet]
View
42 checker/inductive.ml
@@ -158,11 +158,11 @@ let rec make_subst env = function
(* (actualize_decl_level), then to the conclusion of the arity (via *)
(* the substitution) *)
let ctx,subst = make_subst env (sign, exp, []) in
- if polymorphism_on_non_applied_parameters then
- let s = fresh_local_univ () in
- let t = actualize_decl_level env (Type s) t in
- (na,None,t)::ctx, cons_subst u s subst
- else
+ (* if polymorphism_on_non_applied_parameters then *)
+ (* let s = fresh_local_univ () in *)
+ (* let t = actualize_decl_level env (Type s) t in *)
+ (* (na,None,t)::ctx, cons_subst u s subst *)
+ (* else *)
d::ctx, subst
| sign, [], _ ->
(* Uniform parameters are exhausted *)
@@ -170,23 +170,21 @@ let rec make_subst env = function
| [], _, _ ->
assert false
-let instantiate_universes env ctx ar argsorts =
- let args = Array.to_list argsorts in
- let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in
- let level = subst_large_constraints subst ar.poly_level in
- ctx,
- if is_type0m_univ level then Prop Null
- else if is_type0_univ level then Prop Pos
- else Type level
+(* let instantiate_universes env ctx ar argsorts = *)
+(* let args = Array.to_list argsorts in *)
+(* let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in *)
+(* let level = subst_large_constraints subst ar.poly_level in *)
+(* ctx, *)
+(* if is_type0m_univ level then Prop Null *)
+(* else if is_type0_univ level then Prop Pos *)
+(* else Type level *)
let type_of_inductive_knowing_parameters env mip paramtyps =
- match mip.mind_arity with
- | Monomorphic s ->
- s.mind_user_arity
- | Polymorphic ar ->
- let ctx = List.rev mip.mind_arity_ctxt in
- let ctx,s = instantiate_universes env ctx ar paramtyps in
- mkArity (List.rev ctx,s)
+ mip.mind_arity.mind_user_arity
+ (* | Polymorphic ar -> *)
+ (* let ctx = List.rev mip.mind_arity_ctxt in *)
+ (* let ctx,s = instantiate_universes env ctx ar paramtyps in *)
+ (* mkArity (List.rev ctx,s) *)
(* Type of a (non applied) inductive type *)
@@ -233,9 +231,7 @@ let error_elim_expln kp ki =
(* Get type of inductive, with parameters instantiated *)
let inductive_sort_family mip =
- match mip.mind_arity with
- | Monomorphic s -> family_of_sort s.mind_sort
- | Polymorphic _ -> InType
+ family_of_sort mip.mind_arity.mind_sort
let mind_arity mip =
mip.mind_arity_ctxt, inductive_sort_family mip
View
4 checker/inductive.mli
@@ -55,8 +55,8 @@ val type_of_inductive_knowing_parameters :
val max_inductive_sort : sorts array -> Univ.universe
-val instantiate_universes : env -> rel_context ->
- polymorphic_arity -> constr array -> rel_context * sorts
+(* val instantiate_universes : env -> rel_context -> *)
+(* inductive_arity -> constr array -> rel_context * sorts *)
(***************************************************************)
(* Debug *)
View
36 checker/mod_checking.ml
@@ -15,32 +15,32 @@ open Environ
(************************************************************************)
(* Checking constants *)
-let refresh_arity ar =
- let ctxt, hd = decompose_prod_assum ar in
- match hd with
- Sort (Type u) when not (Univ.is_univ_variable u) ->
- let u' = Univ.fresh_local_univ() in
- mkArity (ctxt,Type u'),
- Univ.enforce_leq u u' Univ.empty_constraint
- | _ -> ar, Univ.empty_constraint
+(* let refresh_arity ar = *)
+(* let ctxt, hd = decompose_prod_assum ar in *)
+(* match hd with *)
+(* Sort (Type u) when not (Univ.is_univ_variable u) -> *)
+(* let u' = Univ.fresh_local_univ() in *)
+(* mkArity (ctxt,Type u'), *)
+(* Univ.enforce_leq u u' Univ.empty_constraint *)
+(* | _ -> ar, Univ.empty_constraint *)
let check_constant_declaration env kn cb =
Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn);
(* let env = add_constraints cb.const_constraints env in*)
let env' = check_named_ctxt env cb.const_hyps in
(match cb.const_type with
- NonPolymorphicType ty ->
- let ty, cu = refresh_arity ty in
- let envty = add_constraints cu env' in
- let _ = infer_type envty ty in
+ ty ->
+ (* let ty, cu = refresh_arity ty in *)
+ (* let envty = add_constraints cu env' in *)
+ let _ = infer_type env' ty in
(match body_of_constant cb with
| Some bd ->
let j = infer env' bd in
- conv_leq envty j ty
+ conv_leq env' j ty
| None -> ())
- | PolymorphicArity(ctxt,par) ->
- let _ = check_ctxt env ctxt in
- check_polymorphic_arity env ctxt par);
+ (* | PolymorphicArity(ctxt,par) -> *)
+ (* let _ = check_ctxt env ctxt in *)
+ (* check_polymorphic_arity env ctxt par *));
add_constant kn cb env
(************************************************************************)
@@ -244,13 +244,13 @@ and check_module env mp mb =
{typ_mp=mp;
typ_expr=sign;
typ_expr_alg=None;
- typ_constraints=Univ.empty_constraint;
+ typ_constraints=Univ.Constraint.empty;
typ_delta = mb.mod_delta;}
and mtb2 =
{typ_mp=mp;
typ_expr=mb.mod_type;
typ_expr_alg=None;
- typ_constraints=Univ.empty_constraint;
+ typ_constraints=Univ.Constraint.empty;
typ_delta = mb.mod_delta;}
in
let env = add_module (module_body_of_type mp mtb1) env in
View
2  checker/term.ml
@@ -466,7 +466,7 @@ let compare_sorts s1 s2 = match s1, s2 with
| Pos, Null -> false
| Null, Pos -> false
end
-| Type u1, Type u2 -> Universe.equal u1 u2
+| Type u1, Type u2 -> Universe.eq u1 u2
| Prop _, Type _ -> false
| Type _, Prop _ -> false
View
51 checker/typeops.ml
@@ -93,12 +93,11 @@ let check_args env c hyps =
(* Type of constants *)
let type_of_constant_knowing_parameters env t paramtyps =
- match t with
- | NonPolymorphicType t -> t
- | PolymorphicArity (sign,ar) ->
- let ctx = List.rev sign in
- let ctx,s = instantiate_universes env ctx ar paramtyps in
- mkArity (List.rev ctx,s)
+ t
+ (* | PolymorphicArity (sign,ar) -> *)
+ (* let ctx = List.rev sign in *)
+ (* let ctx,s = instantiate_universes env ctx ar paramtyps in *)
+ (* mkArity (List.rev ctx,s) *)
let type_of_constant_type env t =
type_of_constant_knowing_parameters env t [||]
@@ -251,14 +250,14 @@ let type_fixpoint env lna lar lbody vdefj =
(************************************************************************)
-let refresh_arity env ar =
- let ctxt, hd = decompose_prod_assum ar in
- match hd with
- Sort (Type u) when not (is_univ_variable u) ->
- let u' = fresh_local_univ() in
- let env' = add_constraints (enforce_leq u u' empty_constraint) env in
- env', mkArity (ctxt,Type u')
- | _ -> env, ar
+(* let refresh_arity env ar = *)
+(* let ctxt, hd = decompose_prod_assum ar in *)
+(* match hd with *)
+(* Sort (Type u) when not (is_univ_variable u) -> *)
+(* let u' = fresh_local_univ() in *)
+(* let env' = add_constraints (enforce_leq u u' empty_constraint) env in *)
+(* env', mkArity (ctxt,Type u') *)
+(* | _ -> env, ar *)
(* The typing machine. *)
@@ -313,7 +312,7 @@ let rec execute env cstr =
(* /!\ c2 can be an inferred type => refresh
(but the pushed type is still c2) *)
let _ =
- let env',c2' = refresh_arity env c2 in
+ let env',c2' = (* refresh_arity env *) env, c2 in
let _ = execute_type env' c2' in
judge_of_cast env' (c1,j1) DEFAULTcast c2' in
let env1 = push_rel (name,Some c1,c2) env in
@@ -414,14 +413,14 @@ let check_kind env ar u =
if snd (dest_prod env ar) = Sort(Type u) then ()
else failwith "not the correct sort"
-let check_polymorphic_arity env params par =
- let pl = par.poly_param_levels in
- let rec check_p env pl params =
- match pl, params with
- Some u::pl, (na,None,ty)::params ->
- check_kind env ty u;
- check_p (push_rel (na,None,ty) env) pl params
- | None::pl,d::params -> check_p (push_rel d env) pl params
- | [], _ -> ()
- | _ -> failwith "check_poly: not the right number of params" in
- check_p env pl (List.rev params)
+(* let check_polymorphic_arity env params par = *)
+(* let pl = par.poly_param_levels in *)
+(* let rec check_p env pl params = *)
+(* match pl, params with *)
+(* Some u::pl, (na,None,ty)::params -> *)
+(* check_kind env ty u; *)
+(* check_p (push_rel (na,None,ty) env) pl params *)
+(* | None::pl,d::params -> check_p (push_rel d env) pl params *)
+(* | [], _ -> () *)
+(* | _ -> failwith "check_poly: not the right number of params" in *)
+(* check_p env pl (List.rev params) *)
View
6 checker/typeops.mli
@@ -19,8 +19,8 @@ val infer : env -> constr -> constr
val infer_type : env -> constr -> sorts
val check_ctxt : env -> rel_context -> env
val check_named_ctxt : env -> named_context -> env
-val check_polymorphic_arity :
- env -> rel_context -> polymorphic_arity -> unit
+(* val check_polymorphic_arity : *)
+(* env -> rel_context -> inductive_arity -> unit *)
-val type_of_constant_type : env -> constant_type -> constr
+val type_of_constant_type : env -> constr -> constr
View
1  dev/base_include
@@ -91,6 +91,7 @@ open Evarutil
open Evarsolve
open Tacred
open Evd
+open Universes
open Termops
open Namegen
open Indrec
View
17 dev/include
@@ -28,12 +28,25 @@
#install_printer (* pattern *) pppattern;;
#install_printer (* glob_constr *) ppglob_constr;;
-
+#install_printer (* open constr *) ppopenconstr;;
#install_printer (* constr *) ppconstr;;
#install_printer (* constr_substituted *) ppsconstr;;
+#install_printer (* constraints *) ppconstraints;;
+#install_printer (* univ constraints *) ppuniverseconstraints;;
#install_printer (* universe *) ppuni;;
#install_printer (* universes *) ppuniverses;;
-#install_printer (* constraints *) ppconstraints;;
+#install_printer (* univ level *) ppuni_level;;
+#install_printer (* univ context *) ppuniverse_context;;
+#install_printer (* univ context set *) ppuniverse_context_set;;
+#install_printer (* univ set *) ppuniverse_set;;
+#install_printer (* univ instance *) ppuniverse_instance;;
+#install_printer (* univ list *) ppuniverse_list;;
+#install_printer (* univ subst *) ppuniverse_subst;;
+#install_printer (* univ full subst *) ppuniverse_level_subst;;
+#install_printer (* univ opt subst *) ppuniverse_opt_subst;;
+#install_printer (* evar univ ctx *) ppevar_universe_context;;
+#install_printer (* inductive *) ppind;;
+#install_printer (* 'a scheme_kind *) ppscheme;;
#install_printer (* type_judgement *) pptype;;
#install_printer (* judgement *) ppj;;
View
7 dev/printers.mllib
@@ -71,6 +71,7 @@ Subtyping
Mod_typing
Nativelibrary
Safe_typing
+Unionfind
Summary
Nameops
@@ -88,6 +89,7 @@ Locusops
Miscops
Termops
Namegen
+Universes
Evd
Glob_ops
Redops
@@ -162,4 +164,9 @@ Himsg
Cerrors
Locality
Vernacinterp
+Dischargedhypsmap
+Discharge
+Declare
+Ind_tables
Top_printers
+
View
64 dev/top_printers.ml
@@ -22,6 +22,7 @@ open Evd
open Goptions
open Genarg
open Clenv
+open Universes
let _ = Constrextern.print_evar_arguments := true
let _ = Constrextern.print_universes := true
@@ -40,13 +41,16 @@ let ppmp mp = pp(str (string_of_mp mp))
let ppcon con = pp(debug_pr_con con)
let ppkn kn = pp(pr_kn kn)
let ppmind kn = pp(debug_pr_mind kn)
+let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i)
let ppsp sp = pp(pr_path sp)
let ppqualid qid = pp(pr_qualid qid)
let ppclindex cl = pp(Classops.pr_cl_index cl)
+let ppscheme k = pp (Ind_tables.pr_scheme_kind k)
(* term printers *)
let rawdebug = ref false
let ppconstr x = pp (Termops.print_constr x)
+let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x)
let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x)
let ppterm = ppconstr
let ppsconstr x = ppconstr (Lazyconstr.force x)
@@ -54,7 +58,6 @@ let ppconstr_univ x = Constrextern.with_universes ppconstr x
let ppglob_constr = (fun x -> pp(pr_lglob_constr x))
let pppattern = (fun x -> pp(pr_constr_pattern x))
let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e)))
-
let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
let ppbigint n = pp (str (Bigint.to_string n));;
@@ -116,6 +119,10 @@ let ppexistentialset evars =
let ppclenv clenv = pp(pr_clenv clenv)
let ppgoalgoal gl = pp(Goal.pr_goal gl)
let ppgoal g = pp(Printer.pr_goal g)
+let ppgoalsigma g = pp(Printer.pr_goal g ++ pr_evar_map None (Refiner.project g))
+
+let ppopenconstr (x : Evd.open_constr) =
+ let (evd,c) = x in pp (pr_evar_map (Some 2) evd ++ pr_constr c)
(* spiwack: deactivated until a replacement is found
let pppftreestate p = pp(print_pftreestate p)
*)
@@ -134,10 +141,21 @@ let pppftreestate p = pp(print_pftreestate p)
(* let pproof p = pp(print_proof Evd.empty empty_named_context p) *)
let ppuni u = pp(pr_uni u)
-
-let ppuniverses u = pp (str"[" ++ pr_universes u ++ str"]")
+let ppuni_level u = pp (Level.pr u)
+let ppuniverses u = pp (str"[" ++ Universe.pr u ++ str"]")
+
+let ppuniverse_set l = pp (LSet.pr l)
+let ppuniverse_instance l = pp (Instance.pr l)
+let ppuniverse_list l = pp (pr_universe_list l)
+let ppuniverse_context l = pp (pr_universe_context l)
+let ppuniverse_context_set l = pp (pr_universe_context_set l)
+let ppuniverse_subst l = pp (Univ.pr_universe_subst l)
+let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l)
+let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l)
+let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l)
let ppconstraints c = pp (pr_constraints c)
+let ppuniverseconstraints c = pp (UniverseConstraints.pr c)
let ppenv e = pp
(str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++
@@ -175,12 +193,12 @@ let constr_display csr =
^(term_display t)^","^(term_display c)^")"
| App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
| Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")"
- | Const c -> "Const("^(string_of_con c)^")"
- | Ind (sp,i) ->
- "MutInd("^(string_of_mind sp)^","^(string_of_int i)^")"
- | Construct ((sp,i),j) ->
+ | Const (c,u) -> "Const("^(string_of_con c)^","^(universes_display u)^")"
+ | Ind ((sp,i),u) ->
+ "MutInd("^(string_of_mind sp)^","^(string_of_int i)^","^(universes_display u)^")"
+ | Construct (((sp,i),j),u) ->
"MutConstruct(("^(string_of_mind sp)^","^(string_of_int i)^"),"
- ^(string_of_int j)^")"
+ ^","^(universes_display u)^(string_of_int j)^")"
| Case (ci,p,c,bl) ->
"MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
^(array_display bl)^")"
@@ -204,13 +222,22 @@ let constr_display csr =
(fun x i -> (term_display x)^(if not(i="") then (";"^i) else ""))
v "")^"|]"
+ and univ_display u =
+ incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ pr_uni u ++ fnl ())
+
+ and level_display u =
+ incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.pr u ++ fnl ())
+
and sort_display = function
| Prop(Pos) -> "Prop(Pos)"
| Prop(Null) -> "Prop(Null)"
- | Type u ->
- incr cnt; pp (str "with " ++ int !cnt ++ pr_uni u ++ fnl ());
+ | Type u -> univ_display u;
"Type("^(string_of_int !cnt)^")"
+ and universes_display l =
+ Array.fold_right (fun x i -> level_display x; (string_of_int !cnt)^(if not(i="")
+ then (" "^i) else "")) (Instance.to_array l) ""
+
and name_display = function
| Name id -> "Name("^(Id.to_string id)^")"
| Anonymous -> "Anonymous"
@@ -255,19 +282,23 @@ let print_pure_constr csr =
| Evar (e,l) -> print_string "Evar#"; print_int e; print_string "{";
Array.iter (fun x -> print_space (); box_display x) l;
print_string"}"
- | Const c -> print_string "Cons(";
+ | Const (c,u) -> print_string "Cons(";
sp_con_display c;
+ print_string ","; universes_display u;
print_string ")"
- | Ind (sp,i) ->
+ | Ind ((sp,i),u) ->
print_string "Ind(";
sp_display sp;
print_string ","; print_int i;
+ print_string ","; universes_display u;
print_string ")"
- | Construct ((sp,i),j) ->
+ | Construct (((sp,i),j),u) ->
print_string "Constr(";
sp_display sp;
print_string ",";
- print_int i; print_string ","; print_int j; print_string ")"
+ print_int i; print_string ","; print_int j;
+ print_string ","; universes_display u;
+ print_string ")"
| Case (ci,p,c,bl) ->
open_vbox 0;
print_string "<"; box_display p; print_string ">";
@@ -309,6 +340,9 @@ let print_pure_constr csr =
and box_display c = open_hovbox 1; term_display c; close_box()
+ and universes_display u =
+ Array.iter (fun u -> print_space (); pp (Level.pr u)) (Instance.to_array u)
+
and sort_display = function
| Prop(Pos) -> print_string "Set"
| Prop(Null) -> print_string "Prop"
@@ -391,7 +425,7 @@ let in_current_context f c =
let (evmap,sign) =
try Pfedit.get_current_goal_context ()
with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in
- f (Constrintern.interp_constr evmap sign c)
+ f (fst (Constrintern.interp_constr evmap sign c))(*FIXME*)
(* We expand the result of preprocessing to be independent of camlp4
View
4 grammar/q_constr.ml4
@@ -18,7 +18,7 @@ let dloc = <:expr< Loc.ghost >>
let apply_ref f l =
<:expr<
- Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$)
+ Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$, None), $mlexpr_of_list (fun x -> x) l$)
>>
EXTEND
@@ -74,7 +74,7 @@ EXTEND
| "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >>
| "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" ->
apply_ref <:expr< coq_sumbool_ref >> [c1;c2]
- | "%"; e = string -> <:expr< Glob_term.GRef ($dloc$,Lazy.force $lid:e$) >>
+ | "%"; e = string -> <:expr< Glob_term.GRef ($dloc$,Lazy.force $lid:e$, None) >>
| c = match_constr -> c
| "("; c = constr LEVEL "200"; ")" -> c ] ]
;
View
7 grammar/q_coqast.ml4
@@ -139,10 +139,10 @@ let mlexpr_of_binder_kind = function
$mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >>
let rec mlexpr_of_constr = function
- | Constrexpr.CRef (Libnames.Ident (loc,id)) when is_meta (Id.to_string id) ->
+ | Constrexpr.CRef (Libnames.Ident (loc,id),_) when is_meta (Id.to_string id) ->
let loc = of_coqloc loc in
anti loc (Id.to_string id)
- | Constrexpr.CRef r -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ >>
+ | Constrexpr.CRef (r,n) -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ None >>
| Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
| Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
| Constrexpr.CProdN (loc,l,a) ->
@@ -153,8 +153,9 @@ let rec mlexpr_of_constr = function
let loc = of_coqloc loc in
<:expr< Constrexpr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
| Constrexpr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
- | Constrexpr.CAppExpl (loc,a,l) ->
+ | Constrexpr.CAppExpl (loc,(p,r,us),l) ->
let loc = of_coqloc loc in
+ let a = (p,r) in
<:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
| Constrexpr.CApp (loc,a,l) ->
let loc = of_coqloc loc in
View
26 interp/constrexpr_ops.ml
@@ -92,10 +92,16 @@ and cases_pattern_notation_substitution_eq (s1, n1) (s2, n2) =
List.equal cases_pattern_expr_eq s1 s2 &&
List.equal (List.equal cases_pattern_expr_eq) n1 n2
+let eq_universes u1 u2 =
+ match u1, u2 with
+ | None, None -> true
+ | Some l, Some l' -> l = l'
+ | _, _ -> false
+
let rec constr_expr_eq e1 e2 =
if e1 == e2 then true
else match e1, e2 with
- | CRef r1, CRef r2 -> eq_reference r1 r2
+ | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2
| CFix(_,id1,fl1), CFix(_,id2,fl2) ->
eq_located Id.equal id1 id2 &&
List.equal fix_expr_eq fl1 fl2
@@ -112,7 +118,7 @@ let rec constr_expr_eq e1 e2 =
Name.equal na1 na2 &&
constr_expr_eq a1 a2 &&
constr_expr_eq b1 b2
- | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) ->
+ | CAppExpl(_,(proj1,r1,_),al1), CAppExpl(_,(proj2,r2,_),al2) ->
Option.equal Int.equal proj1 proj2 &&
eq_reference r1 r2 &&
List.equal constr_expr_eq al1 al2
@@ -222,8 +228,8 @@ and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) =
List.equal (List.equal local_binder_eq) bl1 bl2
let constr_loc = function
- | CRef (Ident (loc,_)) -> loc
- | CRef (Qualid (loc,_)) -> loc
+ | CRef (Ident (loc,_),_) -> loc
+ | CRef (Qualid (loc,_),_) -> loc
| CFix (loc,_,_) -> loc
| CCoFix (loc,_,_) -> loc
| CProdN (loc,_,_) -> loc
@@ -273,8 +279,8 @@ let local_binders_loc bll = match bll with
(** Pseudo-constructors *)
-let mkIdentC id = CRef (Ident (Loc.ghost, id))
-let mkRefC r = CRef r
+let mkIdentC id = CRef (Ident (Loc.ghost, id),None)
+let mkRefC r = CRef (r,None)
let mkCastC (a,k) = CCast (Loc.ghost,a,k)
let mkLambdaC (idl,bk,a,b) = CLambdaN (Loc.ghost,[idl,bk,a],b)
let mkLetInC (id,a,b) = CLetIn (Loc.ghost,id,a,b)
@@ -325,13 +331,13 @@ let coerce_reference_to_id = function
str "This expression should be a simple identifier.")
let coerce_to_id = function
- | CRef (Ident (loc,id)) -> (loc,id)
+ | CRef (Ident (loc,id),_) -> (loc,id)
| a -> Errors.user_err_loc
(constr_loc a,"coerce_to_id",
str "This expression should be a simple identifier.")
let coerce_to_name = function
- | CRef (Ident (loc,id)) -> (loc,Name id)
+ | CRef (Ident (loc,id),_) -> (loc,Name id)
| CHole (loc,_) -> (loc,Anonymous)
| a -> Errors.user_err_loc
(constr_loc a,"coerce_to_name",
@@ -340,10 +346,10 @@ let coerce_to_name = function
let rec raw_cases_pattern_expr_of_glob_constr looked_for = function
| GVar (loc,id) -> RCPatAtom (loc,Some id)
| GHole (loc,_) -> RCPatAtom (loc,None)
- | GRef (loc,g) ->
+ | GRef (loc,g,_) ->
looked_for g;
RCPatCstr (loc, g,[],[])
- | GApp (loc,GRef (_,g),l) ->
+ | GApp (loc,GRef (_,g,_),l) ->
looked_for g;
RCPatCstr (loc, g,List.map (raw_cases_pattern_expr_of_glob_constr looked_for) l,[])
| _ -> raise Not_found
View
44 interp/constrextern.ml
@@ -473,8 +473,8 @@ let explicitize loc inctx impl (cf,f) args =
match is_projection (List.length args) cf with
| Some i as ip ->
if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then
- let f' = match f with CRef f -> f | _ -> assert false in
- CAppExpl (loc,(ip,f'),args)
+ let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in
+ CAppExpl (loc,(ip,f',us),args)
else
let (args1,args2) = List.chop i args in
let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in
@@ -485,26 +485,26 @@ let explicitize loc inctx impl (cf,f) args =
let args = exprec 1 (args,impl) in
if List.is_empty args then f else CApp (loc, (None, f), args)
-let extern_global loc impl f =
+let extern_global loc impl f us =
if not !Constrintern.parsing_explicit &&
not (List.is_empty impl) && List.for_all is_status_implicit impl
then
- CAppExpl (loc, (None, f), [])
+ CAppExpl (loc, (None, f, us), [])
else
- CRef f
+ CRef (f,us)
-let extern_app loc inctx impl (cf,f) args =
+let extern_app loc inctx impl (cf,f) us args =
if List.is_empty args then
(* If coming from a notation "Notation a := @b" *)
- CAppExpl (loc, (None, f), [])
+ CAppExpl (loc, (None, f, us), [])
else if not !Constrintern.parsing_explicit &&
((!Flags.raw_print ||
(!print_implicits & not !print_implicits_explicit_args)) &
List.exists is_status_implicit impl)
then
- CAppExpl (loc, (is_projection (List.length args) cf, f), args)
+ CAppExpl (loc, (is_projection (List.length args) cf,f,us), args)
else
- explicitize loc inctx impl (cf,CRef f) args
+ explicitize loc inctx impl (cf,CRef (f,us)) args
let rec extern_args extern scopes env args subscopes =
match args with
@@ -516,7 +516,7 @@ let rec extern_args extern scopes env args subscopes =
extern argscopes env a :: extern_args extern scopes env args subscopes
let rec remove_coercions inctx = function
- | GApp (loc,GRef (_,r),args) as c
+ | GApp (loc,GRef (_,r,_),args) as c
when not (!Flags.raw_print or !print_coercions)
->
let nargs = List.length args in
@@ -573,6 +573,10 @@ let extern_glob_sort = function
| GType (Some _) as s when !print_universes -> s
| GType _ -> GType None
+let extern_universes = function
+ | Some _ as l when !print_universes -> l
+ | _ -> None
+
let rec extern inctx scopes vars r =
let r' = remove_coercions inctx r in
try
@@ -584,11 +588,11 @@ let rec extern inctx scopes vars r =
if !Flags.raw_print or !print_no_symbol then raise No_match;
extern_symbol scopes vars r'' (uninterp_notations r'')
with No_match -> match r' with
- | GRef (loc,ref) ->
+ | GRef (loc,ref,us) ->
extern_global loc (select_stronger_impargs (implicits_of_global ref))
- (extern_reference loc vars ref)
+ (extern_reference loc vars ref) (extern_universes us)
- | GVar (loc,id) -> CRef (Ident (loc,id))
+ | GVar (loc,id) -> CRef (Ident (loc,id),None)
| GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None)
@@ -600,7 +604,7 @@ let rec extern inctx scopes vars r =
| GApp (loc,f,args) ->
(match f with
- | GRef (rloc,ref) ->
+ | GRef (rloc,ref,us) ->
let subscopes = find_arguments_scope ref in
let args =
extern_args (extern true) (snd scopes) vars args subscopes in
@@ -646,7 +650,7 @@ let rec extern inctx scopes vars r =
| Not_found | No_match | Exit ->
extern_app loc inctx
(select_stronger_impargs (implicits_of_global ref))
- (Some ref,extern_reference rloc vars ref) args
+ (Some ref,extern_reference rloc vars ref) (extern_universes us) args
end
| _ ->
explicitize loc inctx [] (None,sub_extern false scopes vars f)
@@ -809,7 +813,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
let args1, args2 = List.chop n args in
let subscopes, impls =
match f with
- | GRef (_,ref) ->
+ | GRef (_,ref,us) ->
let subscopes =
try List.skipn n (find_arguments_scope ref)
with Failure _ -> [] in
@@ -823,13 +827,13 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
[], [] in
(if Int.equal n 0 then f else GApp (Loc.ghost,f,args1)),
args2, subscopes, impls
- | GApp (_,(GRef (_,ref) as f),args), None ->
+ | GApp (_,(GRef (_,ref,us) as f),args), None ->
let subscopes = find_arguments_scope ref in
let impls =
select_impargs_size
(List.length args) (implicits_of_global ref) in
f, args, subscopes, impls
- | GRef _, Some 0 -> GApp (Loc.ghost,t,[]), [], [], []
+ | GRef (_,ref,us), Some 0 -> GApp (Loc.ghost,t,[]), [], [], []
| _, None -> t, [], [], []
| _ -> raise No_match in
(* Try matching ... *)
@@ -864,7 +868,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
List.map (fun (c,(scopt,scl)) ->
extern true (scopt,scl@scopes) vars c, None)
terms in
- let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
+ let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn),None) in
if List.is_empty l then a else CApp (loc,(None,a),l) in
if List.is_empty args then e
else
@@ -927,7 +931,7 @@ let any_any_branch =
(loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole))
let rec glob_of_pat env = function
- | PRef ref -> GRef (loc,ref)
+ | PRef ref -> GRef (loc,ref,None)
| PVar id -> GVar (loc,id)
| PEvar (n,l) -> GEvar (loc,n,Some (Array.map_to_list (glob_of_pat env) l))
| PRel n ->
View
76 interp/constrintern.ml
@@ -94,7 +94,7 @@ let global_reference_of_reference ref =
locate_reference (snd (qualid_of_reference ref))
let global_reference id =
- constr_of_global (locate_reference (qualid_of_ident id))
+ Universes.constr_of_global (locate_reference (qualid_of_ident id))
let construct_reference ctx id =
try
@@ -103,7 +103,7 @@ let construct_reference ctx id =
global_reference id
let global_reference_in_absolute_module dir id =
- constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
+ Universes.constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
(**********************************************************************)
(* Internalization errors *)
@@ -297,7 +297,7 @@ let reset_tmp_scope env = {env with tmp_scope = None}
let set_scope env = function
| CastConv (GSort _) -> set_type_scope env
- | CastConv (GRef (_,ref) | GApp (_,GRef (_,ref),_)) ->
+ | CastConv (GRef (_,ref,_) | GApp (_,GRef (_,ref,_),_)) ->
{env with tmp_scope = compute_scope_of_global ref}
| _ -> env
@@ -406,7 +406,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
let name =
let id =
match ty with
- | CApp (_, (_, CRef (Ident (loc,id))), _) -> id
+ | CApp (_, (_, CRef (Ident (loc,id),_)), _) -> id
| _ -> Id.of_string "H"
in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
in Name name
@@ -609,7 +609,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
try
let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
let expl_impls = List.map
- (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in
+ (fun id -> CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
let tys = string_of_ty ty in
Dumpglob.dump_reference loc "<>" (Id.to_string id) tys;
GVar (loc,id), make_implicits_list impls, argsc, expl_impls
@@ -644,15 +644,15 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
- GRef (loc, ref), impls, scopes, []
+ GRef (loc, ref, None), impls, scopes, []
with e when Errors.noncritical e ->
(* [id] a goal variable *)
GVar (loc,id), [], [], []
let find_appl_head_data = function
- | GRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
- | GApp (_,GRef (_,ref),l) as x
- when l != [] && Flags.version_strictly_greater Flags.V8_2 ->
+ | GRef (_,ref,_) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
+ | GApp (_,GRef (_,ref,_),l) as x
+ when l != [] & Flags.version_strictly_greater Flags.V8_2 ->
let n = List.length l in
x,List.map (drop_first_implicits n) (implicits_of_global ref),
List.skipn_at_least n (find_arguments_scope ref),[]
@@ -689,7 +689,7 @@ let intern_reference ref =
let intern_qualid loc qid intern env lvar args =
match intern_extended_global_of_qualid (loc,qid) with
| TrueGlobal ref ->
- GRef (loc, ref), args
+ GRef (loc, ref, None), args
| SynDef sp ->
let (ids,c) = Syntax_def.search_syntactic_definition sp in
let nids = List.length ids in
@@ -702,7 +702,7 @@ let intern_qualid loc qid intern env lvar args =
(* Rule out section vars since these should have been found by intern_var *)
let intern_non_secvar_qualid loc qid intern env lvar args =
match intern_qualid loc qid intern env lvar args with
- | GRef (_, VarRef _),_ -> raise Not_found
+ | GRef (_, VarRef _, _),_ -> raise Not_found
| r -> r
let intern_applied_reference intern env namedctx lvar args = function
@@ -1213,7 +1213,7 @@ let merge_impargs l args =
let check_projection isproj nargs r =
match (r,isproj) with
- | GRef (loc, ref), Some _ ->
+ | GRef (loc, ref, _), Some _ ->
(try
let n = Recordops.find_projection_nparams ref + 1 in
if not (Int.equal nargs n) then
@@ -1228,7 +1228,7 @@ let get_implicit_name n imps =
Some (Impargs.name_of_implicit (List.nth imps (n-1)))
let set_hole_implicit i b = function
- | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b))
+ | GRef (loc,r,_) | GApp (_,GRef (loc,r,_),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b))
| GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b))
| _ -> anomaly (Pp.str "Only refs have implicits")
@@ -1274,7 +1274,7 @@ let extract_explicit_arg imps args =
let internalize sigma globalenv env allow_patvar lvar c =
let rec intern env = function
- | CRef ref as x ->
+ | CRef (ref,us) as x ->
let (c,imp,subscopes,l),_ =
intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in
(match intern_impargs c env imp subscopes l with
@@ -1372,7 +1372,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
| CDelimiters (loc, key, e) ->
intern {env with tmp_scope = None;
scopes = find_delimiters_scope loc key :: env.scopes} e
- | CAppExpl (loc, (isproj,ref), args) ->
+ | CAppExpl (loc, (isproj,ref,us), args) ->
let (f,_,args_scopes,_),args =
let args = List.map (fun a -> (a,None)) args in
intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref in
@@ -1387,7 +1387,8 @@ let internalize sigma globalenv env allow_patvar lvar c =
| _ -> isproj,f,args in
let (c,impargs,args_scopes,l),args =
match f with
- | CRef ref -> intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref
+ | CRef (ref,us) ->
+ intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref
| CNotation (loc,ntn,([],[],[])) ->
let c = intern_notation intern env lvar loc ntn ([],[],[]) in
find_appl_head_data c, args
@@ -1409,7 +1410,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
| None -> user_err_loc (loc, "intern", str"No constructor inference.")
| Some (n, constrname, args) ->
let pars = List.make n (CHole (loc, None)) in
- let app = CAppExpl (loc, (None, constrname), List.rev_append pars args) in
+ let app = CAppExpl (loc, (None, constrname,None), List.rev_append pars args) in
intern env app
end
| CCases (loc, sty, rtnpo, tms, eqns) ->
@@ -1437,7 +1438,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
| [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *)
| l -> let thevars,thepats=List.split l in
Some (
- GCases(Loc.ghost,Term.RegularStyle,Some (GSort (Loc.ghost,GType None)), (* "return Type" *)
+ GCases(Loc.ghost,Term.RegularStyle,(* Some (GSort (Loc.ghost,GType None)) *)None, (* "return Type" *)
List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *)
[Loc.ghost,[],thepats, (* "|p1,..,pn" *)
Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *)
@@ -1516,7 +1517,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
(* the "as" part *)
let extra_id,na = match tm', na with
| GVar (loc,id), None when not (List.mem_assoc id (snd lvar)) -> Some id,(loc,Name id)
- | GRef (loc, VarRef id), None -> Some id,(loc,Name id)
+ | GRef (loc, VarRef id, _), None -> Some id,(loc,Name id)
| _, None -> None,(Loc.ghost,Anonymous)
| _, Some (loc,na) -> None,(loc,na) in
(* the "in" part *)
@@ -1690,7 +1691,7 @@ let interp_open_constr_patvar sigma env c =
| GPatVar (loc,(_,id)) ->
( try Id.Map.find id !evars
with Not_found ->
- let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in
+ let ev,_ = Evarutil.e_new_type_evar sigma Evd.univ_flexible_alg env in
let ev = Evarutil.e_new_evar sigma env ev in
let rev = GEvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in
evars := Id.Map.add id rev !evars;
@@ -1701,7 +1702,7 @@ let interp_open_constr_patvar sigma env c =
understand_tcc !sigma env raw
let interp_constr_judgment sigma env c =
- understand_judgment sigma env (intern_constr sigma env c)
+ understand_judgment sigma env None (intern_constr sigma env c)
let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
env ?(impls=empty_internalization_env) kind c =
@@ -1787,13 +1788,13 @@ let intern_context global_level sigma env impl_env params =
user_err_loc (loc,"internalize", explain_internalization_error e)
let interp_rawcontext_gen understand_type understand_judgment env bl =
- let (env, par, _, impls) =
+ let (env, ctx, sorts, par, _, impls) =
List.fold_left
- (fun (env,params,n,impls) (na, k, b, t) ->
+ (fun (env,ctx,sorts,params,n,impls) (na, k, b, t) ->
match b with
None ->
let t' = locate_if_isevar (loc_of_glob_constr t) na t in
- let t = understand_type env t' in
+ let {utj_val = t; utj_type = s},ctx' = understand_type env t' in
let d = (na,None,t) in
let impls =
if k == Implicit then
@@ -1801,23 +1802,30 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
(ExplByPos (n, na), (true, true, true)) :: impls
else impls
in
- (push_rel d env, d::params, succ n, impls)
+ let ctx'' = Evd.union_evar_universe_context ctx ctx' in
+ (push_rel d env, ctx'', s::sorts, d::params, succ n, impls)
| Some b ->
- let c = understand_judgment env b in
- let d = (na, Some c.uj_val, Termops.refresh_universes c.uj_type) in
- (push_rel d env, d::params, succ n, impls))
- (env,[],1,[]) (List.rev bl)
- in (env, par), impls
+ let {utj_val = t; utj_type = s},ctx' = understand_type env t in
+ let c,ctx' = understand_judgment env (Some t) b in
+ let d = (na, Some c.uj_val, c.uj_type) in
+ let ctx'' = Evd.union_evar_universe_context ctx ctx' in
+ (push_rel d env, ctx'', s::sorts, d::params, succ n, impls))
+ (env,Evd.empty_evar_universe_context,[],[],1,[]) (List.rev bl)
+ in (env, ctx, par, sorts), impls
let interp_context_gen understand_type understand_judgment ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params =
let int_env,bl = intern_context global_level sigma env impl_env params in
int_env, interp_rawcontext_gen understand_type understand_judgment env bl
let interp_context ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params =
- interp_context_gen (understand_type sigma)
+ interp_context_gen (understand_type_judgment sigma)
(understand_judgment sigma) ~global_level ~impl_env sigma env params
let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params =
- interp_context_gen (fun env t -> understand_tcc_evars evdref env IsType t)
- (understand_judgment_tcc evdref) ~global_level ~impl_env !evdref env params
-
+ let int_env, ((env, ctx, par, sorts), impls) =
+ interp_context_gen (fun env t -> let t' = understand_type_judgment_tcc evdref env t in
+ t', Evd.empty_evar_universe_context)
+ (fun env tycon gc ->
+ let j = understand_judgment_tcc evdref env tycon gc in
+ j, Evd.empty_evar_universe_context) ~global_level ~impl_env !evdref env params
+ in int_env, ((env, par), impls)
View
27 interp/constrintern.mli
@@ -94,22 +94,22 @@ val intern_context : bool -> evar_map -> env -> internalization_env -> local_bin
val interp_gen : typing_constraint -> evar_map -> env ->
?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
- constr_expr -> constr
+ constr_expr -> constr Univ.in_universe_context_set
(** Particular instances *)
val interp_constr : evar_map -> env ->
- constr_expr -> constr
+ constr_expr -> constr Univ.in_universe_context_set
val interp_type : evar_map -> env -> ?impls:internalization_env ->
- constr_expr -> types
+ constr_expr -> types Univ.in_universe_context_set
val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr
val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * constr
val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
- constr_expr -> types -> constr
+ constr_expr -> types -> constr Univ.in_universe_context_set
(** Accepting evars and giving back the manual implicits in addition. *)
@@ -132,7 +132,8 @@ val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env ->
(** {6 Build a judgment } *)
-val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
+val interp_constr_judgment : evar_map -> env -> constr_expr ->
+ unsafe_judgment Evd.in_evar_universe_context
(** Interprets constr patterns *)
@@ -148,22 +149,26 @@ val interp_reference : ltac_sign -> reference -> glob_constr
(** Interpret binders *)
-val interp_binder : evar_map -> env -> Name.t -> constr_expr -> types
+val interp_binder : evar_map -> env -> Name.t -> constr_expr -> types Univ.in_universe_context_set
val interp_binder_evars : evar_map ref -> env -> Name.t -> constr_expr -> types
(** Interpret contexts: returns extended env and context *)
-val interp_context_gen : (env -> glob_constr -> types) ->
- (env -> glob_constr -> unsafe_judgment) ->
+val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) ->
+ (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) ->
?global_level:bool -> ?impl_env:internalization_env ->
- evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+ evar_map -> env -> local_binder list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits)
val interp_context : ?global_level:bool -> ?impl_env:internalization_env ->
- evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+ evar_map -> env -> local_binder list ->
+ internalization_env *
+ ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits)
val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env ->
- evar_map ref -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+ evar_map ref -> env -> local_binder list ->
+ internalization_env *
+ ((env * rel_context) * Impargs.manual_implicits)
(** Locating references of constructions, possibly via a syntactic definition
(these functions do not modify the glob file) *)
View
43 interp/coqlib.ml
@@ -30,7 +30,7 @@ let find_reference locstr dir s =
anomaly ~label:locstr (str "cannot find " ++ Libnames.pr_path sp)
let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
-let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s)
+let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s)
let gen_reference = coq_reference
let gen_constant = coq_constant
@@ -49,7 +49,7 @@ let gen_constant_in_modules locstr dirs s =
let all = List.uniquize (List.map_filter global_of_extended all) in
let these = List.filter (has_suffix_in_dirs dirs) all in
match these with
- | [x] -> constr_of_global x
+ | [x] -> Universes.constr_of_global x
| [] ->
anomaly ~label:locstr (str ("cannot find "^s^
" in module"^(if List.length dirs > 1 then "s " else " ")) ++
@@ -86,6 +86,7 @@ let check_required_library d =
let init_reference dir s = gen_reference "Coqlib" ("Init"::dir) s
let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s
+let init_constant_ dir s = coq_reference "Coqlib" ("Init"::dir) s
let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s
@@ -130,10 +131,14 @@ let make_con dir id = Globnames.encode_con dir (Id.of_string id)
(** Identity *)
-let id = make_con datatypes_module "id"
-let type_of_id = make_con datatypes_module "ID"
+let id = make_con datatypes_module "idProp"
+let type_of_id = make_con datatypes_module "IDProp"
-let _ = Termops.set_impossible_default_clause (mkConst id,mkConst type_of_id)
+let _ = Termops.set_impossible_default_clause
+ (fun () ->
+ let c, ctx = Universes.fresh_global_instance (Global.env()) (ConstRef id) in
+ let (_, u) = destConst c in
+ (c,mkConstU (type_of_id,u)), ctx)
(** Natural numbers *)
let nat_kn = make_ind datatypes_module "nat"
@@ -246,6 +251,32 @@ let build_coq_eq_data () =
trans = Lazy.force coq_eq_trans;
congr = Lazy.force coq_eq_congr }
+let make_dirpath dir =
+ Names.make_dirpath (List.map id_of_string dir)
+
+let lazy_init_constant_in env dir id ctx =
+ let c = init_constant_ dir id in
+ let pc, ctx' = Universes.fresh_global_instance env c in
+ pc, Univ.ContextSet.union ctx ctx'
+
+let seq_ctx ma f = fun ctx ->
+ let a, ctx' = ma ctx in f a ctx'
+let ret_ctx a = fun ctx -> a, ctx
+
+let build_coq_eq_data_in env =
+ let _ = check_required_library logic_module_name in
+ let f id = lazy_init_constant_in env ["Logic"] id in
+ let record =
+ seq_ctx (f "eq") (fun eq ->
+ seq_ctx (f "eq_refl") (fun eq_refl ->
+ seq_ctx (f "eq_sym") (fun eq_sym ->
+ seq_ctx (f "eq_ind") (fun eq_ind ->
+ seq_ctx (f "eq_trans") (fun eq_trans ->
+ seq_ctx (f "f_equal") (fun eq_congr ->
+ ret_ctx {eq = eq; ind = eq_ind; refl = eq_refl;
+ sym = eq_sym; trans = eq_trans; congr = eq_congr}))))))
+ in record Univ.ContextSet.empty
+
let build_coq_eq () = Lazy.force coq_eq_eq
let build_coq_eq_refl () = Lazy.force coq_eq_refl
let build_coq_eq_sym () = Lazy.force coq_eq_sym
@@ -278,7 +309,7 @@ let build_coq_jmeq_data () =
congr = Lazy.force coq_jmeq_congr }
let join_jmeq_types eq =
- mkLambda(Name (Id.of_string "A"),Termops.new_Type(),
+ mkLambda(Name (Id.of_string "A"),Universes.new_Type (Global.current_dirpath ()),
mkLambda(Name (Id.of_string "x"),mkRel 1,
mkApp (eq,[|mkRel 2;mkRel 1;mkRel 2|])))
View
2  interp/coqlib.mli
@@ -120,6 +120,8 @@ type coq_eq_data = {
congr: constr }
val build_coq_eq_data : coq_eq_data delayed
+val build_coq_eq_data_in : Environ.env -> coq_eq_data Univ.in_universe_context_set
+
val build_coq_identity_data : coq_eq_data delayed
val build_coq_jmeq_data : coq_eq_data delayed
View
18 interp/implicit_quantifiers.ml
@@ -97,8 +97,8 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
else l
in
let rec aux bdvars l c = match c with
- | CRef (Ident (loc,id)) -> found loc id bdvars l
- | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Id.Set.mem id bdvars) ->