| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
This has different behaviour if called on an applied Rel, not sure if
that ever happens.
|
|
|
|
|
|
The code to generate the legacy bodies is moved to its only user in
extraction.
It almost seems like we could remove it (ie no special extraction code
for primitive projection constants) but then we run into issues with
automatic unboxing eg `Record foo := { a : nat; b : a <= 5 }.` gets
extracted to `type foo = nat` and (if we remove the special code) `let
a = a`.
|
|
|
|
Since it returns an Id.t and not a Pp.t.
|
|
|
|
|
|
|
|
|
|
comments.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id.
Remove the ability to split the argument of `Univ.Level.Level` into a
dirpath*int pair (except by going through string hacks like
detyping/pretyping(/funind) does).
Id.of_string_soft to turn unnamed universes into qualid is pushed up
to detyping. (TODO some followup PR clean up more)
This makes it pointless to have an opaque type for ints in
Univ.Level: it would only be used as argument to
Univ.Level.UGlobal.make, ie
~~~
open Univ.Level
let x = UGlobal.make dp (Id.make n)
(* vs *)
let x = UGlobal.make dp n
~~~
Remaining places which create levels from ints are various hacks (eg
the dummy in inductive.ml, the Type.n universes in ugraph
sort_universes) and univgen.
UnivGen does have an opaque type for ints used as univ ids since they
get manipulated by the stm.
NB: build breaks due to ocamldep issue if UGlobal is named Global instead.
|
|
Remote counters were trying to build universe levels (as opposed to
simple integers), but did not have access to the right dirpath at
construction time. We fix it by constructing the level only at use time,
and we introduce some abstractions for qualified and unqualified level
names.
|
|
|
|
|
|
This makes setting the option outside of the synchronized summary impossible.
|
|
write_function
|
|
|
|
|
|
This introduces the warning “not-a-class” in the “typeclasses” category.
|
|
cleanups
|
|
|
