1) GrafiteAst.NEval => GrafiteAst.NReduce
2) new tactic "nnormalize" implemented
3) "ngeneralize" now uses "wanted" when no term is selected
(so that it is possible to use ngeneralize to move an
hypothesis down)
4) new syntax for non punctuational tinycals was missing
1) new tactic normalize (low-level function implemented in
nCicTacReduction)
2) the select tactic used to generate fresh metavariables by unifying the
"wanted" part of the pattern in a root where "wanted" did not occur.
Those metavariables are now removed in that case
1) order of processing of case branches reverted (to generate metas in
left-to-right order)
2) metas generated by eat_prods are now re-ordered so that they occur
in left-to-right order
Patch to add a debugging string to HExtlib.split_nth reverted
(we cannot add a string to every function that raises an exception).
To know where the problem is, it is sufficient to look at the backtrace.
However:
1) it works for matitac -debug
2) ocaml is so dumb that it says "compile with -g" when it cannot find
the executable in the current working directory. Since Matita chdir
to the directory where the .ma file is, you need to put a copy of
matitac (or make a symbolic link) where the .ma file is.
Ferruccio Guidi [Thu, 14 May 2009 13:43:55 +0000 (13:43 +0000)]
- libraryObjects: new default "natural numbers" with the uri of nat.
alias num "natural number" uses this one instead of the hardcoded uri (removed)
also destroy_nat (moved to termAcicContent) looks at this default
Ferruccio Guidi [Wed, 13 May 2009 18:44:42 +0000 (18:44 +0000)]
- matitaEngine: some commands like "coercion" must not be executed when mma's are dumped. This hack will be removed when mma's will be executed while dumped
- primitiveTactics: bugxix in the generation of the predicate for elim: we leave to the refiner the task of instantiating the types of the pattern variables.
Note: the head beta-reductions after the elimination must be performed following the instantiated predicate because (\lambda x:?.t v) does not beta-reduce (bug or feature?)
Andrea Asperti [Wed, 13 May 2009 09:27:34 +0000 (09:27 +0000)]
Signature is computed on the initial goal, once and for all.
Ripristined the filtering on candidates also for non-smart applications
(was too slow on some examples, e.g. in Fsub *
Ferruccio Guidi [Tue, 12 May 2009 19:04:32 +0000 (19:04 +0000)]
- Procedural: we now reconstruct "let H := v in t" with "intros (1) H" when the goal starts with an abbreviation. Clearbody before change in reactivated (to change the inferred type of the abbreviations of sort Prop)
- RELATIONAL: notation fixup
- character: autobatch fixup
- ng_tactics: dependences were not committed correctly
- critical bug fixed in NCicSubstitution.lift:
(0,Irl 0) was lifted to (1,Irl 0)
but later on NCicTypechecker.check_metasenv_consistency assumes the
invariant that the currenct context has length (m+n) if the metavariable
is (m,Irl n). But this invariant is false in the case (m, Irl 0) when m > 0.
- in NCicRefiner there was one line to normalize (m,Irl 0) and (m,Ctx []) to
(0,...). Is it still required after the first patch to the kernel? I suspect
no, thus I put an assert false to check.
Bug fixed: left parameters of constructors were unified before refining them.
Fixed, but the new code typechecks the constructors twice (in order to
re-compute) the sort without the inductive types. Is a more efficient
implementation worth the effort?
1) better implementation of NObj that now calls recursively NQed
to avoid code duplication
2) NQed now calls the kernel to check the object, since add_obj is too
low level for that (this makes a huge difference with the previous
architecture, but will probably break when dealing with undo)
Ferruccio Guidi [Wed, 6 May 2009 18:26:56 +0000 (18:26 +0000)]
- cicUtil: is_sober now detects folded applications
- Procedural: bugfix in pattern generation for elim/rewrite, better debug output, applications are flattened before alpha-conversion to hide a bug of the double type inference :( (it generates folded applications)
- applyTransformation: coercions are shown when rendering a tactic because Procedural is not aware of coercions :(
Ferruccio Guidi [Tue, 5 May 2009 17:23:49 +0000 (17:23 +0000)]
- hExtlib: new function "list_assoc_all"
- procedural: new flag "nodefaults" to turn off "default" based tactics. The `Variant flavour is now activated
- grafiteAst: now inline accepts a list of flags that can be easily extended
current flags are: procedural, nodefaults, depth=n, prefix="string" (untested),
theorem, definition, etc.
- transcript: support for explicitly provided inline flags
Enrico Tassi [Tue, 5 May 2009 16:56:33 +0000 (16:56 +0000)]
- pretty printer made robust in face of list_nth
- bugfixed in generation of aliases in nCicLibrary:
contructor index are 1-based
- refinement of indtypes fixed:
- missing undebujinate added
- index for current indty was in the wrong order
- apply_subst moved to nCicUntrusted
- new iterator for obj_kind
Ferruccio Guidi [Fri, 1 May 2009 16:40:29 +0000 (16:40 +0000)]
- librarian: 3 bugs fixed in the building system:
1) external dependences must be built using the path relative to their baseuri
2) the path of a non-existent .ma generated by a .mma was wrong
3) the compilation status of external dependences must be cached as for the other files in order to avoid looping.
Repetition of failed compilation remains for dependences of external dependences because the the external compilation caches are lost in the building process
When a devel is entered or leaved, its baseuei is printed for reference. This helps to disambiguate the files with the same name (eg original and reconstructed)
We hope that this will not bother the tests collection mechanism.
- core_notation: notation for non-functional exists had the wrong precedence
- procedural/library/Makefile: -onepass was added by mistake: datatypes/bool.ma fails with -onepass because of the ambiguity of the /\ notation
- procedural: bugfix in "Barendregt convention" test
- library/logic/cprop_connectives.ma: reorganized.
notations must immediately follow the definition they refer to (or else another
definition can use them in the reconstructed version of the file)
- core_notation.moo: added a notation for non-functiona 'exists
eta-expansion (not a CIC conversion) should be avoided exp. if the rendered
text must be reparsed (ie. during the reconstruction)
"default" notation facility reactivated in parsing mode since it is not
equivalent to the separated rules (they cover eachother).
The bug is in the rendering mode
- applyTransformation: debugging information added (commented)
logic/cprop_connectives.ma reconstructed and compiled !!
cicNotationUtil: in fresh_name_generator, "\eta" replaced with "eta", which is an identifier
cicNotationPp: debug mode turned off
logic/cprop_connectives.ma: duplicate lines removed
matitaScript: missing "\n\n" added in front of inline output
core_notation.moo: the "default" notation directive has a bug. Commented out.
huge commit in automation:
- tactics:
- all tactics used by auto (apply, applys and thus rewrite)
do handle correctly the subst present in the status
- indexing:
- demodualte_all (and thus solve_rewriting) reimplemented,
faster and more correct
- auto:
- applyS used to apply theorems, remaining goals have a
depth penalty
It is now possible for commands processed by grafiteEngine to either return
uris for an old object or for a new one. This information is only used to
generate preferences.
Lookup_in_library implemented for new objects. Basically, this stupid (??),
inefficient (??) implementation just keeps an associative list that maps names
to URIs and is used to resolve names in the library. This functionality is
provided by ng_kernel/nCicLibrary.
Note: automatic addition of preferences is not there yet.
Thus you need to activate lookup in library to see it working.
It is now possible to declare new aliases using the old syntax
(maybe confusing, but a string is a string). Thus much code becomes
useless in GrafiteDisambiguate. But it will be moved in the next commit
to nCicLibrary to implement the nlookup_in_library function.
- matitacLib: better handling of the callbacks for the dump operation
- applyTransformation: notation disabled when rendering reconstructed inductive types to avoid notation conflict between notation and inductive type syntax
- lexicon/lexiconEngine: better error messages and one callback removed
- termAcicContent: in lookup_interpretations, sorting the returned interpretations is optional and defaults to true (as before)
- disambiguateChoices: in lookup_symbol_by_dsc, the interpretations are not sorted before choosing, sorting them here is a bug because their order is lost so the chosen one is not the most recent
- grafiteParser: better callback functions for the drop feature of matitac, we introduced module name abbreviations for our convenience
- syntax_extensions/.depend: something is wrong with the Makefiles, this .depend is commited every time :(
- Grammar for all obj commands ported to NG (let recs and inductives still need
implementation and raise assert false)
- New feature: every object can be both interactive or not, depending on the
number of metavariables in the metasenv after disambiguation
- New objects are now put in the same namespace as old ones. The creation of
aliases takes care of this by looking for new objects before looking for
old ones. Note: this way the check is done twice, also when mapping
aliases to terms. However, this is temporary code while the two "libraries"
coexist.