| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| | |
This simplifies the representation of values, and brings it closer to
the ones of the native compiler.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit was motivated by true spurious conversions arising in my
`to_constr` debug branch.
The changes here need careful review as the tradeoffs are subtle and
still a lot of clean up remains to be done in `vernac/*`.
We have opted for penalize [minimally] the few users coming from true
`Constr`-land, but I am sure we can tweak code in a much better way.
In particular, it is not clear if internalization should take an
`evar_map` even in the cases where it is not triggered, see the
changes under `plugins` for a good example.
Also, the new return type of `Pretyping.understand` should undergo
careful review.
We don't touch `Impargs` as it is not clear how to proceed, however,
the current type of `compute_implicits_gen` looks very suspicious as
it is called often with free evars.
Some TODOs are:
- impargs was calling whd_all, the Econstr equivalent can be either
+ Reductionops.whd_all [which does refolding and no sharing]
+ Reductionops.clos_whd_flags with all as a flag.
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
Computation of the sort of the inductive type was done before ensuring
that the arguments of the inductive type had the correct types,
possibly brutally failing with `NotArity` in case one of the types
expected to be typed with an arity was not so.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Example which is now reprinted as parsed:
fun '((x,y) as z) => (y,x)=z
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
For instance, the following is now possible:
Check {(x,y)|x+y=0}.
Some questions remains. Maybe, by consistency, the notation should be
"{'(x,y)|x+y=0}"...
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The motivations are:
- To reflect the concrete syntax more closely.
- To factorize the different places where "contexts" are internalized:
before this patch, there is a different treatment of `Definition f
'(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack
to interpret `Definition f `pat := c : t`. With the patch, the fix
to avoid seeing a variable named `pat` works for both `fun 'x =>
...` and `Definition f 'x := ...`.
The drawbacks are:
- Counterpart to reflecting the concrete syntax more closerly, there
are more redundancies in the syntax. For instance, the case `CLetIn
(na,b,t,c)` can appears also in the form `CProdN (CLocalDef
(na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`.
- Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| |
| | |
No using a mutable counter to skip them, instead we keep them in the
environment.
|
| | |
| |
| |
| |
| |
| | |
The only difference is when we have a rel local definition in the
initial environment, which isn't actually possible. However that
depends on the specific way we treat parameters.
|
| |/ |
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
information.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This ensures by construction that we never infer constraints outside
the variance model.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.
As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).
Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie
Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
Print Foo.
gives
Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
{ foo : Type@{i} -> Type@{j} }
(* =i +j *k |= *)
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The part in Reduction should be semantics preserving, but Reductionops
only tried cumulativity if equality fails. This is probably wrong so I
changed it.
|
| | |_|/ /
|/| | | |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | | |
|
| | |_|/ /
|/| | | |
|
| |/ / / |
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
There is no way today to distinguish primitive projections from
compatibility constants, at least in the case of a record without
parameters.
We remedy to this by always using the r.(p) syntax when printing
primitive projections, even with Set Printing All.
The input syntax r.(p) is still elaborated to GApp, so that we can preserve
the compatibility layer. Hopefully we can make up a plan to get rid of that
layer, but it will require fixing a few problems.
|
| |\ \ \
| | | |
| | | |
| | | | |
records for cbv and native_compute
|
| | | | |
| | | |
| | | |
| | | | |
Fixes #5286 (last remaining part).
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We separate functions dealing with VM values (vmvalues.ml) and
interfaces of the bytecode interpreter (vm.ml). Only the former relies
on untyped constructions.
This also makes the VM architecture closer to the one of native_compute,
another patch could probably try to share more code between the two for
conversion and reification (not trivial, though).
This is also preliminary work for integers and arrays.
|
| |\ \ \
| | | |
| | | |
| | | | |
for primitive projections
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The constant_value function was actually not behaving the same as
constant_value_in w.r.t. projections. The former was not used, and
the only place that used the latter was in Tacred and was statically
insensitive to the use of projections.
|
| | | | | |
|
| |/ / / |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
We simply use a record and pack the rel and var substitutions in it. We also
properly compose variable substitutions.
Fixes #6534: Fresh variable generation in case of clash is buggy.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
|
| |/ / |
|
| | |
| |
| |
| |
| |
| | |
Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
Typeclasses.typeclass
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
|
| |\ \ \ |
|
Maxime Dénès
Emilio Jesus Gallego Arias
Enrico Tassi
Hugo Herbelin
Gaëtan Gilbert
Paul Steckler
Pierre-Marie Pédrot
Cyprien Mangin