aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Collapse)AuthorAge
* Reactivating option "Set Printing Existential Instances" for asking printing ↵Gravatar Hugo Herbelin2014-12-04
| | | | full instances.
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
| | | | | | | | | | | - Registering strict implicit arguments systematically (35fc7d728168) - Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6) - Fixing Coq compilation (894a3d16471) Systematically computing strict implicit arguments can lead to big computations, so I suspend this attempt, waiting for improved computation of implicit arguments, or alternative heuristics going toward having more conversion in rewrite.
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
| | | | in tactic unification.
* Printing function for [uconstr].Gravatar Arnaud Spiwack2014-11-19
| | | | The core is a "detyping" function for [closed_glob_constr]. Which interpretes the variable names according to the Ltac context, and apply the standard detyping procedure to typed terms in the closure.
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | reference" and "simpl pattern" in the code (maybe we should have merged them instead, but I finally decided to enforce their difference, even if some compatibility is to be preversed - the idea is that at some time "simpl reference" would only call a weak-head simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for better using induction hypotheses. In the process we also implement the following: - 'simpl "+"' is accepted to reduce all applicative subterms whose head symbol is written "+" (in the toplevel scope); idem for vm_compute and native_compute - 'simpl reference' works even if reference has maximally inserted implicit arguments (this solves the "simpl fst" incompatibility) - compatibility of ltac expressions referring to vm_compute and native_compute with functor application should now work (i.e. vm_compute and native_compute are now taken into account in tacsubst.ml) - for compatibility, "simpl eq" (assuming no maximal implicit args in eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed. By the way, is "mul" on nat defined optimally? "3*n" simplifies to "n+(n+(n+0))". Are there some advantages of this compared to have it simplified to "n+n+n" (i.e. to "(n+n)+n").
* Fixing what really looks like a bug in the initial implementation ofGravatar Hugo Herbelin2014-10-22
| | | | coqdoc links for modules (#3756).
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
| | | | | | | | | | | but the internal representation dropped let-in. Ideally, the internal representation of the "match" should use contexts for the predicate and the branches. This would however be a rather significant change. In the meantime, just a hack. To do, there is still an extra @ in the constructor name that does not need to be there.
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
| | | | | | | | will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise.
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
| | | | | | | | | | | so that one can retrieve them and pass them to third party tools (i.e. print the AST with the notations attached to the nodes concerned). Available syntax: - all in one: Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2"). - a posteriori: Format Notation "a /\ b" "latex" "#1 \wedge #2".
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
| | | | | | | | so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
| | | | | | | Add a flag to indicate if we're in the toplevel or debuggger to not try to retype terms in the wrong environment (and making find_rectype, get_type_of untraceable). This fixes bug #3638 along with the previous commit.
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
| | | | | | | | contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now.
* More on printing references applied to implicit arguments.Gravatar Hugo Herbelin2014-09-16
|
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
|
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
|
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
| | | | | instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.
* Parsing and printing of primitive projections, fix buggy behavior whenGravatar Matthieu Sozeau2014-09-10
| | | | implicits do not allow to parse as an application and cleanup code.
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
| | | | | | | | Printing All cases (bug #3597). - Fix Ltac matching with primitive projections (bug #3598). - Spotted a problem with printing of constants with maximally implicit arguments due to strange "compatibility" interpretation of Arguments [X] as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
* Fix bug #3591: print differently eta-expanded projection implicit ↵Gravatar Matthieu Sozeau2014-09-08
| | | | | | application and primitive projection when they would otherwise be ambiguous.
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
|
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
| | | | Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
* Simplification of Genarg unpackers.Gravatar Pierre-Marie Pédrot2014-08-29
| | | | | Instead of having a version of unpackers for each level, we use a dummy argument to force unification of types.
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
| | | | | | | can be given with second H bound by the first one. Not very satisfied by passing closure to tactics.ml, but otherwise tactics would have to be aware of glob_constr.
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
| | | | "pat/term" for "apply term on current_hyp as pat".
* Spotted a source of failure of the constr printer in debugger.Gravatar Hugo Herbelin2014-08-18
|
* Fix non-printing of coercions for primitive projections (fixes bug #3433).Gravatar Matthieu Sozeau2014-08-14
|
* Change internalization of primitive projections to allow parsing [p t] asGravatar Matthieu Sozeau2014-08-08
| | | | | | | a primitive application only if all parameters of [p] are implicit, falling back to the internalization of the eta-expanded version otherwise. This makes apply [p] succeed even if its record argument is not implicit, ensuring better compatibility.
* Revert the change in Constrintern introduced by "Add a type of untyped term ↵Gravatar Arnaud Spiwack2014-08-06
| | | | | | | to Ltac's value." It was commit 52247f50fa9aed83cc4a9a714b6b8f779479fd9b. The closure in uconstr renders these changes (pertaining to substitution of ltac variables during internalisation) obsolete.
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
| | | | | This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine. As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile.
* Fix [uconstr] name for argextend.Gravatar Arnaud Spiwack2014-08-05
|
* Better fix of e5c025Gravatar Pierre Boutillier2014-08-05
|
* Fixing #3483 (graceful failing with notations to non-constructors in "match").Gravatar Hugo Herbelin2014-08-03
|
* Better struture for Ltac internalization environments in Constrintern.Gravatar Pierre-Marie Pédrot2014-08-02
|
* Faster uconstr.Gravatar Arnaud Spiwack2014-08-01
| | | Detyping was called on every typed constr in the Ltac context which was costly as most of the context is likely not to be refered to in a particular uconstr. This commit calls detyping lazily instead.
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
| | | | | | | | | | | | - realargs: refers either to the indices of an inductive, or to the proper args of a constructor - params: refers to parameters (which are common to inductive and constructors) - allargs = params + realargs - realdecls: refers to the defining context of indices or proper args of a constructor (it includes letins) - paramdecls: refers to the defining context of params (it includes letins) - alldecls = paramdecls + realdecls
* Finish fixes on notations and primitive projections, add test-suite files ↵Gravatar Matthieu Sozeau2014-07-31
| | | | for closed bugs
* Consistent pretty-printing of primitive projections and their expanded forms.Gravatar Matthieu Sozeau2014-07-31
|
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
| | | | | | It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218. The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation.
* Fix treatment of notations containing applications of projections (fixes bug ↵Gravatar Matthieu Sozeau2014-07-29
| | | | #3454).
* smartlocate: look for the head symbol for realGravatar Enrico Tassi2014-07-14
| | | | | | This bug was hacked around in ssreflect, but with the new idea that parsing and interpretation are done in distinct phases the work around could not be implemented anymore.
* Export type_of_global_ref (useful for external users of glob files)Gravatar Enrico Tassi2014-07-11
|
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - The earlier proof-of-concept file NPeano (which instantiates the "Numbers" framework for nat) becomes now the entry point in the Arith lib, and gets renamed PeanoNat. It still provides an inner module "Nat" which sums up everything about type nat (functions, predicates and properties of them). This inner module Nat is usable as soon as you Require Import Arith, or just Arith_base, or simply PeanoNat. - Definitions of operations over type nat are now grouped in a new file Init/Nat.v. This file is meant to be used without "Import", hence providing for instance Nat.add or Nat.sqrt as soon as coqtop starts (but no proofs about them). - The definitions that used to be in Init/Peano.v (pred, plus, minus, mult) are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul where here Nat is Init/Nat.v). - This Coq.Init.Nat module (with only pure definitions) is Include'd in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat sometimes instead of just Nat (for instance when doing "Print plus"). Normally it should be ok to just ignore these "Init" since Init.Nat is included in the full PeanoNat.Nat. I'm investigating if it's possible to get rid of these "Init" prefixes. - Concerning predicates, orders le and lt are still defined in Init/Peano.v, with their notations "<=" and "<". Properties in PeanoNat.Nat directly refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le", we cannot yet include an Inductive to implement a Parameter), but these aliased predicates won't probably be very convenient to use. - Technical remark: I've split the previous property functor NProp in two parts (NBasicProp and NExtraProp), it helps a lot for building PeanoNat.Nat incrementally. Roughly speaking, we have the following schema: Module Nat. Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *) ... (** proofs of specifications for basic ops such as + * - *) Include NBasicProp. (** generic properties of these basic ops *) ... (** proofs of specifications for advanced ops (pow sqrt log2...) that may rely on proofs for + * - *) Include NExtraProp. (** all remaining properties *) End Nat. - All other files in directory Arith are now taking advantage of PeanoNat : they are now filled with compatibility notations (when earlier lemmas have exact counterpart in the Nat module) or lemmas with one-line proofs based on the Nat module. All hints for database "arith" remain declared in these old-style file (such as Plus.v, Lt.v, etc). All the old-style files are still Require'd (or not) by Arith.v, just as before. - Compatibility should be almost complete. For instance in the stdlib, the only adaptations were due to .ml code referring to some Coq constant name such as Coq.Init.Peano.pred, which doesn't live well with the new compatibility notations.
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
| | | | | | | | | | | | | | | | | | | | lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/
* Continue fix on argument scopes of primitive projections.Gravatar Matthieu Sozeau2014-06-17
|
* Fix HoTT bug #84, binding scopes to projections.Gravatar Matthieu Sozeau2014-06-17
|
* Fixing #3292 (locations of notations shifted by 1 in glob files in trunk).Gravatar Hugo Herbelin2014-06-17
| | | | | Thanks to David M. Cooke on coq-bugs for pointing out one part of the problem.
* Fixing #3282 (two bugs in the presence of let-in's in "fix").Gravatar Hugo Herbelin2014-06-17
|
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
|
* Fix bug #3289Gravatar Matthieu Sozeau2014-06-11
|
* Collecting in Namegen those conventional default names that are used in ↵Gravatar Hugo Herbelin2014-06-04
| | | | different places