| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
This bug was introduced by
commit 34ef02fac1110673ae74c41c185c228ff7876de2
Author: Matej Kosik <m4tej.kosik@gmail.com>
Date: Fri Jan 29 10:13:12 2016 +0100
CLEANUP: Context.{Rel,Named}.Declaration.t
|
| |
|
|
|
|
| |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | |
|
| | |
|
| | |
|
| |\
| |
| |
| | |
defs in Print Assumptions"
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| | |
The name in the return clause has no semantic meaning, we must not
look at it.
|
| | |
| |
| |
| |
| | |
Substitution on bound modules was incorrectly extended without sequential
composition.
|
| | |
| |
| |
| |
| | |
This was because the traversal algorithm used canonical names instead of user
names, confusing which term was defined and which term was an axiom.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch implements the traversal of inductive definitions in the
traverse function of toplevel/assumptions.ml which recursively
collects references in terms. In my opinion, this fixes a bug (but it
could be argued that inductive definitions were not traversed on
purpose). I think that is not possible to use this bug to hide a
meaningful use of an axiom.
You can try the patch with the following coq script:
Axiom n1 : nat.
Axiom n2 : nat.
Axiom n3 : nat.
Inductive I1 (p := n1) : Type := c1.
Inductive I2 : let p := n2 in Type := c2.
Inductive I3 : Type := c3 : let p := n3 in I3.
Inductive J : I1 -> I2 -> I3 -> Type :=
| cj : J c1 c2 c3.
Inductive K : I1 -> I2 -> I3 -> Type := .
Definition T := I1 -> I2 -> I3.
Definition C := c1.
Print Assumptions I1.
Print Assumptions I2.
Print Assumptions I3.
Print Assumptions J.
Print Assumptions K.
Print Assumptions T.
Print Assumptions C.
Print Assumptions c1.
Print Assumptions c2.
Print Assumptions c3.
Print Assumptions cj.
The patch is a bit more complicated that I would have liked due to
the feature introduced in commit 2defd4c. Since this commit,
Print Assumptions also displays the type proved when one destruct
an axiom inhabiting an empty type. This provides more information
about where the old implementation of the admit tactic is used.
I am not a big fan of this feature, especially since the change in
the admit tactic.
PS: In order to write some tests, I had to change the criteria for
picking which axiom destruction are printed. The original
criteria was :
| Case (_,oty,c,[||]) ->
(* non dependent match on an inductive with no constructor *)
begin match Constr.(kind oty, kind c) with
| Lambda(Anonymous,_,oty), Const (kn, _)
when Vars.noccurn 1 oty &&
not (Declareops.constant_has_body (lookup_constant kn)) ->
and I replaced Anonymous by _. Indeed, an Anonymous name here could
only be built using the "case" tactic and the pretyper seems to always
provide a name when compiling "match axiom as _ with end". And I
wanted to test what happened when this destruction occurs in
inductive definitions (which is of course weird in practice), for
instance:
Inductive I4 (X : Type) (p := match absurd return X with end)
: Type -> Type :=
c4 : forall (q := match absurd return X with end)
(Y : Type) (r := match absurd return Y with end), I4 X Y.
The ability of "triggering" the display of this information only when
using the "case" tactic (and not destruct or pattern matching written
by hand) could have been a feature. If so, please feel free to
change back the criteria to "Anonymous".
|
| | |
|
|
|
When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).
E.g.
Lemma w : True.
Proof. case demon. Qed.
Lemma x y : y = 0 /\ True /\ forall w, w = y.
Proof. split. case demon. split; [ exact w | case demon ]. Qed.
Print Assumptions x.
Prints:
Axioms:
demon : False
used in x to prove: forall w : nat, w = y
used in w to prove: True
used in x to prove: y = 0
|
Cyprien Mangin
Guillaume Melquiond
Pierre Letouzey
Pierre-Marie Pédrot
Matej Kosik
Maxime Dénès
Enrico Tassi
mlasson