aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Collapse)Author
2013-11-27Adding the necessary hooks to handle tactics in terms.Pierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
parsing is plugged.
2013-11-23Fixing bug #3165.Pierre-Marie Pédrot
2013-11-08Reverting the old LIFO behaviour of the notation finding algorithm.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17072 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29Do not generate useless argument arrays in whd_* functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
To reduce the amount of syntactic noise, we now provide a few inner modules Int.List, Id.List, String.List, Sorts.List which contain some monomorphic (or semi-monomorphic) functions such as mem, assoc, ... NB: for Int.List.mem and co we reuse List.memq and so on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24Restore my version of notation_ops.ml now that List.remove_assoc_f is fixedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16932 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24Oups, repair the compilation (micromega + Morphism_prop)letouzey
It seems I forgot to fully recompile after my last bunch of syntactic changes about List.assoc_f, that weren't so syntactic after all, sorry : - Util isn't used in micromega, hence no List.assoc_f there - There is something wrong in my modifications of Notation_ops that breaks the compilation of Morphism_prop. For the moment I don't see what, so I revert all the modifications of this file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16930 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24Turn many List.assoc into List.assoc_fletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList.index is now cList.index_f, same for index0letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-14Some more hand-written comparison functions to avoid polymorphic comparison.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16887 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵xclerc
with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
casts of ints to evars. - 2 in Evarutil and Goal which are really needed, even though the Goal one could (and should) be removed; - 2 in G_xml and Detyping that are there for completeness sake, but that might be made anomalies altogether; - 1 in Newring which is quite dubious at best, and should be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-02Removing more association lists in Constrintern.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16757 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-25Actually using the domain function for maps.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16736 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Misc changes around coqtop.ml :letouzey
- Revised Coqtop.parse_args in a cleaner and lighter style - Improved error message in case of argument parse failure: * tell which option is expecting a related argument * in case of unknown options, warn about them all at once * do not hide the previous error messages by filling the screen with usage(). Instead, suggest the use of --help. - Specialized boolean config field Coq_config.arch_is_win32 - Faster Envars.coqlib, which is back to (unit->string), and just access Flags.coqlib. Caveat: it must be initialized once via Envars.set_coqlib - Avoid keeping an opened channel to the "revision" file - Direct load of theories/init/prelude.vo, no detour via Loadpath Beware : ./configure must be runned after this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Less "Coq" strings everywhereletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16725 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
The earlier type [struct_expr_body] was far too broad, leading to code with unclear invariants, many "assert false", etc etc. Its replacement [module_alg_expr] has only three constructors: * MEident * MEapply : note the module_path as 2nd arg, no more constraints here * MEwith : no more constant_body inside, constr is just fine But no more SEBfunctor or SEBstruct constructor here (see below). This way, this datatype corresponds to algebraic expressions, i.e. anything that can appear in non-interactive modules. In fact, it even coincides now with [Entries.module_struct_entry]. - Functor constructors are now necessarily on top of other structures thanks to a generic [functorize] datatype. - Structures are now separated from algebraic expressions by design : the [mod_type] and [typ_expr] fields now only contain structures (or functorized structures), while [mod_type_alg] and [typ_expr_alg] are restricted to algebraic expressions only. - Only the implementation field [mod_expr] could be either algebraic or structural. We handle this via a specialized datatype [module_implementation] with four constructors: * Abstract : no implementation (cf. for instance Declare Module) * Algebraic(_) : for non-interactive modules, e.g. Module M := N. * Struct(_) : for interactive module, e.g. Module M : T. ... End M. * FullStruct : for interactive module with no type restriction. The [FullStruct] is a particular case of [Struct] where the implementation need not be stored at all, since it is exactly equal to its expanded type present in [mod_type]. This is less fragile than hoping as earlier that pointer equality between [mod_type] and [mod_expr] will be preserved... - We clearly emphasize that only [mod_type] and [typ_expr] are relevant for the kernel, while [mod_type_alg] and [typ_expr_alg] are there only for a nicer extraction and shorter module printing. [mod_expr] is also not accessed by the kernel, but it is important for Print Assumptions later. - A few implicit invariants remain, for instance "no MEwith in mod_expr", see the final comment in Declarations - Heavy refactoring of module-related files : modops, mod_typing, safe_typing, declaremods, extraction/extract_env.ml ... - Coqchk has been adapted accordingly. The code concerning MEwith in Mod_checking is now gone, since we cannot have any in mod_expr. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16712 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Support Proof Generalgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16678 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Side effect free implementation of admit (Isabelle's oracle)gareuselesinge
new Axiom in Logic.v, proof_admitted : False. admit now simply cases proof_admitted and does not create a new Axiom in the environment. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16673 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-07Removing association lists in Constrintern.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16666 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-03Replacing uses of association lists by maps in notations.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16655 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-03Replacing an association list by a map in globalizing environment.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16654 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-17Declaremods: major refactoring, stop duplicating libobjects in modulesletouzey
When refering to a module / module type, or when doing an include, we do not duplicate and substitution original libobjects immediatly. Instead, we store the module path, plus a substitution. The libobjects are retrieved later from this module path and substituted, typically during a Require. This allows to vastly decrease vo size (up to 50% on some files in the stdlib). More work is done during load (some substitutions), but the extra time overhead appears to be negligible. Beware: all subst_function operations should now be environment-insensitive, since they may be arbitrarily delayed. Apparently only subst_arguments_scope had to be adapted. A few more remarks: - Increased code factorisation between modules and modtypes - Many errors and anomaly are now assert - One hack : brutal access of inner parts of module types (cf handle_missing_substobjs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16630 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-17More dynamic argument scopesletouzey
When arguments scopes are set manually, nothing new, they stay as they are (until maybe another Arguments invocation). But when argument scopes are computed out of the argument type and the Bind Scope information, this kind of scope is now dynamic: a later Bind Scope will be able to impact the scopes of an earlier constant. For Instance: Definition f (n:nat) := n. About f. (* Argument scope is [nat_scope] *) Bind Scope other_scope with nat. About f. (* Argument scope is [other_scope] *) This allows to get rid of hacks for modifying scopes during functor applications. Moreover, the subst_arguments_scope is now environment-insensitive (needed for forthcoming changes in declaremods). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-05Removing SortArgType.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-02Removing the use of leveled tactics wit_tacticn. It is now handledppedrot
through a unique generic argument, and the level is only considered at parsing time. This may introduce unnecessary parentheses in Ltac printing though, as every tactic argument is collapsed at the lowest level. I assume this does not matter that much, and anyway Ltac printing is quite bugged as of today. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16616 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-30Using functors to reduce the boilerplate used in registeringppedrot
generic argument stuff, including the unsafe Obj.magic-like casts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16614 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-27Removed the distinction between generic Ltac vars and Let/Introppedrot
bindings, which permits using only one environment for interning terms. Ltac semantics was sligthly changed, as it required introducing a lot of additional coercions from goal variables to other types. Ltac seemed to be quite non-uniform, as it tried to represent hypotheses with intropatterns, instead of the dedicated var type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16612 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-27Getting rid of IntroPatternArgType.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16610 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-25Useless use of maps in constr internalizing.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16607 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-24Using the whole tactic environment while Pretyping.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16605 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-22Generalizing the use of maps instead of lists in the interpretationppedrot
of tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16602 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-21Splitted up Genarg in four different levels:ppedrot
1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
related types. This will ultimately allow putting genargs into these ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-19Moving wit_unit to Stdarg.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16595 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-18Proof-of-concept: moved four easy-to-handle generic arguments toppedrot
their own file, Stdarg. This required a little trick to correctly handle wit_* naming. We use a dynamic table to remember exactly where those arguments come from. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16587 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-18Removing the various glob/subst/interp registering functions forppedrot
extra argument types and putting them into Genarg. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16586 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-18Implementing a new interface for Genarg, with centralized datappedrot
structure. The code is quite dumb for now, as it only handles basic extended generig arguments (ExtraArgTypes). Soon, code from other modules will be centralized there. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16585 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-18Now glob_sign and interp_sign only depend on structures definedppedrot
upto Genarg, so moved them there. This will allow defining the new genarg interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16584 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-12Added Genarg as generic argument type.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16575 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-12Changing the type of Ltac values. Now they are toplevel genericppedrot
arguments. That way we will be able to define interpretation of tactics without referring to tactic values. Quite ad-hoc for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16574 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-06More comments in Genarg.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16565 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-06Uniformizing generic argument types.ppedrot
Now, instead of having three unrelated types describing a dynamic type at each level (raw, glob, top), we have a "('a, 'b, 'c) genarg_type" whose parameters describe the reified type at each level. This has various advantages: - No more code duplication to handle the three level separately; - Safer code: one is not authorized to mix unrelated types when what was morally expected was a genarg_type. - Each level-specialized representation can be accessed through well-typed projections: rawwit, glbwit and topwit. Documenting a bit Genarg b.t.w. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16564 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-02Modest protection against "injection" and co raising anomaly inherbelin
-nois mode. This is not perfect yet. E.g. "injection" used while before eq is defined while compiling Logic.v would raise an anomaly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16548 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Removing useless uses of Gmap.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16520 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Getting rid of module Gmapl.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16500 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 09:11:31 +0000