Constructors are closed with thier types when computing the signatur

versione automatizzata

symmetry of inequality sym_neq

documentation for the inline command

- dependenciesParser: updated to new inline syntax

LAMBDA-TYPES: mma's recommitted because inline syntax changed

- 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 :(

apply and auto.equational_case call saturation.solve_narrowing
that performs goal inference and demodulation

updated comment

- Procedural: new flag "level=n" to control the reconstruction level (defaults to maximum level available). Level 1 reconstruction activated.

- 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

- 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

more tests

Nuova gestione di "by" per auto.

autobatch by

- 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

run check_if_goal_is_solved on all goals (active+passive)

Added an option --enable-annot to the configure to compile with -dtypes

Minor changes pro-automation

Added a passive table

Calling paramodulation instead of demod_all

Refinement of inductive type implemented.
Some functions have been exported from the kernel :-( to avoid code
duplication.

Note: the code seem to be bugged (wrong context), but the operations are taken
verbatim from the kernel. Have we really tested it on inductive types?

- 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 !!

...

call paramod instead of solve_Rewrite

no typing

many checks guarded with if Utils.debug_metas

Records are now interpreted in the NG (but I am sure there is some bug
somewhere).

Inductive definitions are now interpreted (but records are not interpreted yet).

Last commit by Ferruccio reverted since it breaks the library.
If there is a bug in default, it must be fixed.

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.

depenalization of smart apply inside auto, that is now much faster

fixed bug, demodulation was keeping results not strictly smaller

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

matitacLib: bugfix in .moo generation
applyTransformation.ml: highlevel prettyprinter disabled when reconstructing inductive types (was re-enabled by mistake)
procedural/Makefile.common: bugfix in entry names
matitaEngine: unused callback removed
lexiconAstPp: output bugfix

The first reconstructed .ma's form library now compile :)))))))

The backward compatible management of aliases for NG is now fully completed.
Enjoy the NG Matita!

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: lexicon status and grafite status where lost after handling a macro. Fixed.

The translation from old aliases to new references is now completely
implemented. It cannot be correct, but it is not supposed to be anyway.

Apply subst implemented also for Fixpoints.

Type for list_index improved.

Slightly improved type for list_index.

New utility function list_index (useful in many places, I think).

Better error message.

Debug option reverted.

- 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.

Quick&dirty implementation of neqd:
 a) nCicLibrary has a new function add_obj to add objects to the storage
    (that is, so far, an associative list)
 b) new command nqed
 c) GrafiteDisambiguate modified so that identifiers are resolved
    in the new storage, if possible, before going back to translating
    the old library
 d) implementation of apply_subst for terms and objects (used during nqed)
    Note: these functions are currently in nTacStatus but should be moved
    elsewhere

- transcript: we have now two styles of mma's from grafite:
  1) each includes its source (minimum choice)
  2) each includes the theory file of the source devel (maximim choice)
- matitadep: creation of the theory file is now optional and defaults to no
- procedural/library: we use style 1) above so library/theory is not needed

syntax colouring for inverters

Disabled debug prints in the inversion principle.

New command "inverter" used to generate an induction/inversion principle for
inductive types. The syntax is:

  inverter name_of_the_principle for name_of_inductive_type param_selection

where param_selection is of the form

 (# # # ... #)

where # can be either ? or %. The length of param_selection must match the
number of right parameters of the inverted inductive_type. A % means that the
corresponding parameter will have an inversion hypothesis, while a ? means that
the parameter won't have an inversion hypothesis. Therefore, a selection
(??...?) will generate the traditional elimination principle, while (%%...%)
will generate a full inversion principle.

Induction/inversion principles are useful for treating inductive types such that
some of their right parameters are used uniformly in one or more constructors.
If the inverted parameters are used uniformly in some constructor, the
induction/inversion principle will provide an induction hypothesis for that
branch (while a full inversion, also ranging on non-uniform parameters, would no
provide a useful induction hypothesis).

demodulate takes an extra argument 'all', if present it attempts to solve
the goal demodulating it in any possible way. an extra steps argument may
be used to increase the default maximum number of demodulation steps (1).
pump may also affect the result.

- MatitaMisc: we factorized here the function out_preamble used in matitadep
              and MatitacLib
- ApplyTransformation: we moved some "\n" hoping in a better rendering :)
- matitadep: we now generate a "theory" file (dfault name "theory.ma" but can
- MatitaMisc: we factorized here the function out_preamble used in matitadep
              and MatitacLib
- ApplyTransformation: we moved some "\n" hoping in a better rendering :)
- matitadep: we now generate a "theory" file (dfault name "theory.ma" but can
             be changed via the -theory cmdline option) that includes all the
     files of the devel so the devel itself can be included just
             including the theory file. To speed up the inclusion process, only
             the "top level" files are included (inclusion seems slow anyway)
- procedural/Makefile.common: new entries for single file compilation
- procedural/library: better preamble including library/theory.ma. Now the
                      devel should be reconstructed with the correct notation
- power_derivative.ma: we definitely do not want 'x' as a keyword in a serious
                       file. All files including it (for intance its
       reconstructed version) can not use 'x' as an identifier.
                       For now we replaced 'x' with 'X'
- transcript: bug fix in obtaining the list of files to be processed

fixed last file restricting auto tables

- init_cache_and_tables rewritten using the automation_cache
- new moo command Select to index an equality
- new command pump to perform some given clause steps on the automation
  cache tables
- no more imperative maxmeta in paramodulation:
  - paramodulation/* forlds a bag containing it
  - auto.ml folds tables, containing a bag

Bug fixed: variable capture in previous commit prevented all aliases insertion.

Some improvements.

...

Procedural: we corrected two errors about the handling of mutcase (the "cases"
            tactic is now disabled because it does not work well with the
    current kernel)
transcript: we immplemented uri substitution in Verbatim items
matitaInit: new option -no-default-includes for omitting the devels included by             default (this is to compile procedural/library :) )
procedural/library: bug fix

Bug: let-ins are always automatically folded!

...

test/a.ma => tests/ng_tactics.ma, with nassert here and there

Replaced long, bugged implementation of letin-tac with two lines of code :-)

Added ppterm.

The context is now parsed in the reverse (right) order.

...

Universe is used only locally to tactics/
AutomationCache.cache is part of grafite_status and will
contain tables too

added an exception

- transcript: bugfix
- library: we removed most uri's. two still remain :(

we rebuilt the dependences

- Procedural: generation of "exact" is now complete
-             relevant tactics are now counted correctly
- PrimitiveTactics: we set exact_tac = apply_tac as in NTactics
- transcript: the grafite parser is now working
              the "library" devel is parsed succesfully
- procedural/library: new devel.
                      Will contain the procedural reconstruction of "library"

Trick: the refiner always subst-expands the outtype, so that the beta-redex
that will be formed will always be reduced by substitution.

Bug fixed in two lines + 5 lines of comment.
During select, the context of the goal is changed and the conclusion
is changed too (too a ?[out_scope]). Then the changed conclusion was
relocated in the changed context, triggering a delift that in turn triggered
the unification case "something vs ?[out_of_scope]"... at the bad time!
Fixed by manually relocating the new conclusion in the new context.
Manually means opening and building again the cic_term data type, which is
ugly and sort of fragile.

assert_tac now takes a list of sequents and also checks that the number of
sequents is the appropriate one.

It is the first example of a high-tactic that works also with the stack.

New debugging tactic nassert:

 nassert H1: t1 ... Hn: tn \vdash T

asserts (using OCaml's assert) that the current goal is equal (using
OCaml equality) to the one given the user. The substitution is fully
expanded just before calling OCaml equality.

Semantic selection back again (but no semantic cut&paste yet).

Match is now rendered as best as possible.

The sequent viewer now considers the context to render the Rels.

- character: we adjusted some "autobatch" parameters
- limits: in classes and subssets we now ensure the compatibility between the
  inhabitance predicate and the equivalence relation

The substitution is now taken in account when printing sequents in the
sequent viewer. Context is not yet taken in account.

added letin, still broken

...

new tactic whd implemented

- change implemented in 4 lines
- select0 runs on hypothesis
- relocate honors conversion (but clearbody is not implemented)

- generalize finished
- relocate implemented in terms of delift

?_OS1 := C[ ?_IN ]
?_IN := m
=======================
?[m;m]  =?=  ?_OS1

used to yield ? := Rel 2 instead of Rel 1, since the first m
was still out of scope when recursion reaches ?_IN

fixed modules order

minor fixes

...

...

+ Chain  NCic.term -> content -> presentation very very roughly implemented
+ The sequent viewer now prints also the neq sequents

Just to make it compile again.

generalized is half-implemented (still broken)

Analizyng the inductive type of the eliminated term and
the sort of the goals are performed by tactics having
a side-effect. This allows to write tactics like elim and cases
as lists of tactics blocked together.

- nrewrite ((very?) rough implementation)

  PATTERNS DO NOT WORK (why?)

- more progress towards generalize, but I am stuck now
- elim completed (up to saturation)

- select_tac honors the hypotheses pattern when required to generalize them
- clear [names]
- initial generalize tac implementation