| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
This was assuming dependencies occurring in configurations of
the form x:A, y:B x, z:C x y |- match x, y, z with ... end".
But still work to do for better management of dependencies in general...
|
| |
|
|
|
|
|
|
|
|
|
|
| |
A cleaning done in ade2363e35 (Dec 2015) was hinting at bugs in typing
a matching over a "catch-all" variable, when let-ins occur in the
arity. However ade2363e35 failed to understand what was the correct
fix, introducing instead the regressions mentioned in #5322 and #5324.
This fixes all of #5322 and #5324, as well as the handling of let-ins
in the arity.
Thanks to Jason for helping in diagnosing the problem.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.
Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.
Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code
|
| |
|
|
| |
(May it fell in the case mentioned in the inner comment of Exninfo.info?)
|
| |
|
|
|
| |
When trying different possible return predicates, returns the error
given by the first try, assuming this is the most interesting one.
|
| |
|
|
|
| |
Revert "Inference of return clause: giving uniformly priority to "small inversion"."
This reverts commit 980b434552d73cb990860f8d659b64686f6dbc87.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The move to systematically trying small inversion first bumps
sometimes as feared to the weakness of unification (see #5107).
----
Revert "Posssible abstractions over goal variables when inferring match return clause."
This reverts commit 0658ba7b908dad946200f872f44260d0e4893a94.
Revert "Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given."
This reverts commit 292f365185b7acdee79f3ff7b158551c2764c548.
Revert "Trying a no-inversion no-dependency heuristic for match return clause."
This reverts commit 2422aeb2b59229891508f35890653a9737988c00.
|
| |
|
|
| |
Also getting rid of a global side-effect.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The no-inversion and maximal abstraction over dependencies now
supports abstraction over goal variables rather than only on "rel"
variables. In particular, it now works consistently using
"intro H; refine (match H with ... end)" or
"refine (fun H => match H with ... end)".
By doing so, we ensure that all three strategies are tried in all
situations where a return clause has to be inferred, even in the
context of a "refine".
See antepenultimate commit for discussion.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
even when no type constraint is given.
This no-inversion and maximal abstraction over dependencies in (rel)
variables heuristic was used only when a type constraint was given.
By doing so, we ensure that all three strategies "inversion with
dependencies as evars", "no-inversion and maximal abstraction over
dependencies in (rel) variables", "no-inversion and no abstraction
over dependencies" are tried in all situations where a return clause
has to be inferred.
See penultimate commit for discussion.
|
| |
|
|
|
|
|
|
| |
The no-inversion no-dependency heuristic was used only in the absence
of type constraint. We may now use it also in the presence of a type
constraint.
See previous commit for discussion.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As noted by Jason Gross on coq-club (Aug 18, 2016), the "small
inversion" heuristic is not used consistently depending on whether the
variables in the type constraint are Rel or Var.
This commit simply gives uniformly preference to the inversion of the
predicate along the indices of the type over other heuristics.
The next three commits will improve further a uniform use of the
different heuristics.
----------------------------------------------------------------------
Here are some extra comments on how to go further with the inference
of the return predicate:
The "small inversion" heuristic build_inversion_problem (1) is
characterized by two features:
- small inversion properly speaking (a), i.e. that is for a match on
t:I params p1(u11..u1p1) ... pn(un1..unpn) with pi exposing the
constructor structure of the indices of the type of t, a return
clause of the form "fun x1..xn (y:I params x1..xn) => match x1..xn y with
| p1(z11..z1p1) ... pn(zn1..znpn) => ?T@{z11..znpn}
| _ => IDProp
end" is used,
- the dependent subterms in the external type constraint U are replaced
by existential variables (b) which can be filled either by projecting
(i.e. installing a dependency) or imitating (i.e. no dependency);
this is obtained by solving the constraint ?T@{u11..unpn} == U by
setting ?T@{z11..znpn} := U'(...?wij@{zij:=uij}...) where U has been
written under the form U'(...uij...) highlighting all occurrences of
each of the uij occurring in U; otherwise said the problem is reduced to
the question of instantiating each wij, deciding whether wij@{zij} := zij
(projection) or wij@{zij} := uij (imitation) [There may be different
way to expose the uij in U, e.g. in the presence of overlapping, or of
evars in U; this is left undetermined].
The two other heuristics used are:
- prepare_predicate_from_arsign_tycon (2): takes the external type
constraint U and decides that each subterm of the form xi or y for a
match on "y:I params x1 ... xn" is dependent; otherwise said, it
corresponds to the degenerated form of (1) where
- no constructor structure is exposed (i.e. each pi is trivial)
- only uij that are Rel are replaced by an evar ?wij and this evar is
directly instantiated by projection (hence creating a dependency),
- simple use of of an evar in case no type constraint is given (3):
this evar is not dependent on the indices nor on the term to match.
Heuristic (1) is not strictly more powerful than other heuristics
because of (at least) two weaknesses.
- The first weakness is due to feature (b), i.e. to letting
unification decide whether these evars have to create a dependency
(projection) or not (imitation).
In particular, the heuristic (2) gives priority to systematic
abstraction over the dependencies (i.e. giving priority to
projection over imitation) and it can then be better as the
following example (from RelationClasses.v) shows:
Fixpoint arrows (l : Tlist) (r : Type) : Type :=
match l with
| Tnil => r
| A :: l' => A -> arrows l' r
end.
Fixpoint predicate_all (l : Tlist) : arrows l Prop -> Prop :=
match l with
| Tnil => fun f => f
| A :: tl => fun f => forall x : A, predicate_all tl (f x)
end.
Using (1) fails. It proposes the predicate
"fun l' => arrows ?l[l':=l'] Prop" so that typing the first branch
leads to unify "arrows ?l[l:=Tnil] Prop == Prop", a problem about
which evarconv unification is not able (yet!) to see what are the
two possible solutions. Using (2) works. It instead directly
suggests that the predicate is "fun l => arrows l Prop" is used, so
that unification is not needed.
Even if in practice the (2) is good (and hence could be added to
(1)), it is not universally better. Consider e.g.
y:bool,H1:P y,H2:P y,f:forall y, P y -> Q y |-
match y as z return Q y with
| true => f y H1
| false => f y H2
end : Q y
There is no way to type it with clause "as z return Q z" even if
trying to generalize H1 and H2 so that they get type P z.
- A second weakness is due to the interaction between small inversion
and constructors having a type whose indices havex a less refined
constructor structure than in the term to match, as in:
Inductive I : nat -> Set :=
| C1 : forall n : nat, listn n -> I n
| C2 : forall n : nat, I n -> I n.
Check (fun x : I 0 => match x with
| C1 n l => 0
| C2 n c => 0
end).
where the inverted predicate is "in I n return match n with 0 => ?T | _ => IDProp end"
but neither C1 nor C2 have fine enough types so that n becomes
constructed. There is a generic solution to that kind of situation which
is to compile the above into
Check (fun x : I 0 => match x with
| C1 n l => match n with 0 => 0 | _ -> id end
| C2 n c => match n with 0 => 0 | _ -> id end
end).
but this is not implemented yet.
In the absence of this refinement, heuristic (3) can here work
better.
So, the current status of the claim is that for (1) to be strictly
more powerful than other current heuristics, work has to be done
- (A) at the unification level (by either being able to reduce problems of
the form "match ?x[constructor] with ... end = a-rigid-term", or, at
worst, by being able to use the heuristic favoring projecting for such
a problem), so that it is better than (2),
- (B) at the match compilation level, by enforcing that, in each branch,
the corresponding constructor is refined so has to match (or
discriminate) the constraints given by the type of the term to
match, and hence being better than (3).
Moreover, (2) and (3) are disjoint. Here is an example which (3) can
solve but not (2) (and (1) cannot because of (B)). [To be fixed in
next commit.]
Inductive I : bool -> bool -> Type := C : I true true | D x : I x x.
Check fun z P Q (y:I true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
match y with
| C => f y H1
| D _ => f y H2
end : Q y z.
Indeed, (2) infers "as y' in I b z return Q y z" which does not work.
Here is an example which (2) can solve but not (3) (and (1) cannot
because of (B) again). [To be fixed in 2nd next commit].
Check fun z P Q (y:I true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
match y with
| C => f y true H1
| D b => f y b H2
end : Q y z.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is a reimplementation of Hugo's PR#117.
We are trying to address the problem that the name of some reduction functions
was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in
reduction). Like PR#117, we are careful that no function changed semantics
without changing the names. Porting existing ML code should be a matter of
renamings a few function calls.
Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX
collectively denominated iota.
We renamed the following functions:
Closure.betadeltaiota -> Closure.all
Closure.betadeltaiotanolet -> Closure.allnolet
Reductionops.beta -> Closure.beta
Reductionops.zeta -> Closure.zeta
Reductionops.betaiota -> Closure.betaiota
Reductionops.betaiotazeta -> Closure.betaiotazeta
Reductionops.delta -> Closure.delta
Reductionops.betalet -> Closure.betazeta
Reductionops.betadelta -> Closure.betadeltazeta
Reductionops.betadeltaiota -> Closure.all
Reductionops.betadeltaiotanolet -> Closure.allnolet
Closure.no_red -> Closure.nored
Reductionops.nored -> Closure.nored
Reductionops.nf_betadeltaiota -> Reductionops.nf_all
Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta
Reductionops.whd_betadeltaiota -> Reductionops.whd_all
Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet
Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack
Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack
Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack
Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state
Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state
Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state
Reductionops.whd_eta -> Reductionops.shrink_eta
Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all
Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all
And removed the following ones:
Reductionops.whd_betaetalet
Reductionops.whd_betaetalet_stack
Reductionops.whd_betaetalet_state
Reductionops.whd_betadeltaeta_stack
Reductionops.whd_betadeltaeta_state
Reductionops.whd_betadeltaeta
Reductionops.whd_betadeltaiotaeta_stack
Reductionops.whd_betadeltaiotaeta_state
Reductionops.whd_betadeltaiotaeta
They were unused and having some reduction functions perform eta is confusing
as whd_all and nf_all don't do it.
|
| |
|
|
|
|
|
| |
Unset Program Generalized Coercion to avoid coercion of general
applications.
Unset Program Cases to deactivate generation equalities and
disequalities of cases.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
By default obligations defined by tactics are defined
transparently or opaque according to the Obligations Transparent flag,
except proofs of subset obligations which are treated
as opaque by default. When the user proves the obligation using
Qed or Defined, this information takes precedence, and only
when the obligation cannot be Qed'ed because it contains
references to a recursive function an error is raised
(this prevents the guardness checker error).
Shrinked obligations were not doings this correctly.
Forcing transparency due to fixpoint prototypes
takes precedence over the user preference.
Program: do not force opacity of subset proofs,
maintaining compatibility.
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
pattern-matching"
This reverts commit be80899499094fc8a15362931e3cec650f2fb14e.
|
| | |
| |
| |
| |
| |
| | |
structure."
This reverts commit eaca8dadf7dd8152a86f4fc75631754344268dbf.
|
| | |
| |
| |
| | |
This reverts commit 94e9e28ebaa33e11164ca07f225d998ca7f8e52c.
|
| | |
| |
| |
| |
| |
| | |
pattern-matching produced by an implicit "in" clause"
This reverts commit ba9f53314ff6132d0013e53879395e0dc9d8038c.
|
| | |
| |
| |
| | |
This reverts commit d9f0daefb437955df8102de2b3c4c31749b6946e.
|
| | | |
|
| | |
| |
| |
| | |
produced by an implicit "in" clause
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
algorithm.
|
| | |
| |
| |
| |
| | |
build a default case if the pattern is irrefutable. It did not matter
in practice because we did not check for unused clauses in this case.
|
| | |
| |
| |
| |
| | |
Some parts of Evarutils were related to the management of evars under constraints.
We put them in the Evardefine file.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
Some functions were left in the old paradigm because they are only used by the
unification algorithms, so they are not worthwhile to change for now.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Originally, rel-context was represented as:
Context.rel_context = Names.Name.t * Constr.t option * Constr.t
Now it is represented as:
Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
| LocalDef of Names.Name.t * Constr.t * Constr.t
Originally, named-context was represented as:
Context.named_context = Names.Id.t * Constr.t option * Constr.t
Now it is represented as:
Context.Named.t = LocalAssum of Names.Id.t * Constr.t
| LocalDef of Names.Id.t * Constr.t * Constr.t
Motivation:
(1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
function which looked like this:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
Suppose that you do not know about rel-context and named-context.
(that is the case of people who just started to read the source code)
Merlin would tell you that the type of the value you are destructing
by "match" is:
'a * 'b option * Constr.t (* worst-case scenario *)
or
Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *)
To me, this is akin to wearing an opaque veil.
It is hard to figure out the meaning of the values you are looking at.
In particular, it is hard to discover the connection between the value
we are destructing above and the datatypes and functions defined
in the "kernel/context.ml" file.
In this case, the connection is there, but it is not visible
(between the function above and the "Context" module).
------------------------------------------------------------------------
Now consider, what happens when the reader see the same function
presented in the following form:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
to jump to the corresponding definition and learn more.
In this case, the connection is there, and it is directly visible
(between the function above and the "Context" module).
(2) Also, if we already have the concepts such as:
- local declaration
- local assumption
- local definition
and we describe these notions meticulously in the Reference Manual,
then it is a real pity not to reinforce the connection
of the actual code with the abstract description we published.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.
Some missing comments were added to the *.mli file.
The output of ocamldoc was checked whether it looks in a reasonable way.
"TODO: cleanup" was removed
The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)
The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)
The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)
The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})
The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.
Thrown exceptions are now documented.
Naming of formal parameters was made more consistent across different functions.
Comments of similar functions in different modules are now consistent.
Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
we can see the comments also there and do not need to open a different file if we want to see it.)
When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)
"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)
An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
|
| |/
|
|
|
|
|
|
|
|
| |
Redefining adjust_subst_to_rel_context from instantiate_context who
was hidden in inductiveops.ml, renamed the latter into
subst_of_rel_context_instance and moving them to Vars. The new name
highlights that the input is an instance (as for applist) and the
output a substitution (as for substl). This is a clearer unified
interface, centralizing the difficult de-Bruijn job in one place. It
saves a couple of List.rev.
|
| |
|
|
|
|
|
|
| |
dealing with "match".
Contrastingly, "fix" is considered not to count let-ins for finding
the recursive argument (which is ok because the last argument is
necessarily a lambda).
|
| | |
|
| |
|
|
|
| |
Retypecheck abstracted infered predicate to register the right
universe constraints.
|
| |
|
|
| |
clause in pattern-matching or not.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
|
| |
|
|
| |
clause in the presence of let-ins in the arity of inductive type).
|
| | |
|
| | |
|
| |
|
|
| |
pattern-matching predicate.
|
| | |
|
| | |
|
Hugo Herbelin
Matthieu Sozeau
Pierre Letouzey
Maxime Dénès
Pierre-Marie Pédrot
Matej Kosik
Matthieu Sozeau