| Age | Commit message (Collapse) | Author |
|---|
|
only.
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: pi8027
|
|
|
|
In particular evar_eqappr_x tries to find a miller pattern on both sides,
while the fast path for evars tries solve_simple_eqn in one direction
only. So if you have (Evar-not-miller = Evar-miller) the code was not
trying to solve the RHS.
|
|
Previously, they were hard-wired in the ML code.
|
|
This option made the Coercions command follow non-standard scoping rules
(effect on `Require` rather than `Import`). It was already marked for deletion
in 8.8.
|
|
|
|
The `Coercion` command did report many ambiguous paths when one declared
multiple inheritances. This change makes the `Coercion` command to do not
report them when
1. all the coercion in the potentially ambiguous paths respect the uniform
inheritance condition and
2. functional compositions of the potentially ambiguous paths are convertible to
each other.
The first condition is not explicitly checked but is used to make the checking
process of the second condition easy.
The key idea of this change:
Let us consider a sequence of coercion
f_1 : C_1 >-> C_2, f_2 : C_2 >-> C_3, ..., f_n : C_n >-> C_(n+1)
which respect the uniform inheritance condition and where the user-defined
classes C_i have m_i parameters respectively (i <= n).
The functional composition f_1 . ... . f_n can be expressed as follows:
(fun x_1 ... x_(m_1) y =>
f_n _ ... _ (* m_n times repetition of holes *)
(...
(f_2 _ ... _ (* m_2 times repetition of holes *)
(f_1 x_1 ... x_(m_1) y))...)),
and the contents of all the holes can be determined (inferred) without leaving
any existential variables in them thanks to the uniform inheritance condition.
Misc:
- A test case for this change: test-suite/output/relaxed_ambiguous_paths.v
- Turn the ambiguous paths messages into warnings to do output test.
|
|
Prevent errors when under annotating binders.
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: ppedrot
|
|
Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.
Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.
|
|
See #9616
|
|
|
|
Reviewed-by: ejgallego
Ack-by: herbelin
Reviewed-by: mattam82
|
|
This is because it can raise Not_found in depth and we need to catch
it at the right time.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
I think the usage looks cleaner this way.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Remaining cases are due to map_constr_with_binders_left_to_right which
does not allow side effects on the evd yet.
|
|
Now the main functions are unify (solves the problems entirely) and
unify_delay and unify_leq (which might leave some unsolved constraints).
Deprecated the_conv_x and the_conv_x_leq (which were misnommers as they
do unification not conversion).
|
|
|
|
|
|
The code is cleaner and more self-explanatory this way.
|
|
It does checking of evar instance and Evd.define, assuming an
occur-check has already been performed.
|
|
|
|
|
|
|
|
|
|
For second_order_matching call, prefer abstraction of evar arguments,
and use same test as original (just eq_constr)
|
|
Also extend evarconv to handle frozen evars and flags for delta and
betaiota reduction.
- Make evar_conv unification take a record of flags
- Adds an imitate_defs option to evarsolve, deactivated in first-order unification
- Add a way to call back conv_algo differently on types
- We distinguish comparison of terms and types which might be different
w.r.t. delta reductions allowed (everything for types, controlled for
terms). We keep the with_cs flag even for types, to avoid
incompatibilities (in HoTT's theories/Spaces/No.v, the refine in
No_encode_le_lt would diverge due to trying a default canonical
structure during type verification).
- In evarsolve, do_project_effects checks evar instances now
- Solve evar-evar unification using miller patterns if possible.
- FO heuristic in evarconv
- Do not catch critical exceptions in evarconv
- Force HO matching to abstract toplevel evar args,
This disallows K on them, more compatible with w_unify_to_subterm.
- occur_rigidly improvement, better approx of occur-check.
- K_at_toplevel, subterm_ts, betaiota and frozen_evars flags taken into
account in apply_on_subterm and evar_conv_x.
This allow implementing a unification without reduction, e.g. for the
fast path of rewrite subterm selection.
- second_order_matching works up-to cumulativity
- pretyping/coercion: now take unification flags as argument
- pretyping/unification: default_occurrence_test takes a frozen_evars set
export elim_flags_evars to compute frozen evars before elim
- evarsolve: fix evar_define doing check in the wrong order,
as conv_algo can trigger the definition of the evar itself,
define it first in the evd.
- w_unify: disallow HO in consider_remaining. Only used in rewrite now
- use evar_abstraction info
- catch second_order_matching NoOccurrence exception in second_order_matching_with_args
- unify_with_heuristics in API
- second_order_matching: thin evars after abstraction to put in the
right env or fail.
|
|
|
|
The semantics is obviously that it is an error if not at least one
occurrence is found (natural semantics for rewriting for
example).
|
|
Named evar_abstract_arguments, this field indicates if the evar
arguments corresponding to certain hypothesis can be immitated during
inversion or not. If the argument comes from an abstraction (the evar
was of arrow type), then imitation is disallowed as it gives unnatural
solutions, and lambda abstraction is preferred.
|
|
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: mattam82
Ack-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: mattam82
|
|
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
|
|
Ack-by: herbelin
Reviewed-by: ppedrot
|
