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.
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
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
- 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
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
- 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"
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.
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.
- character: we adjusted some "autobatch" parameters
- limits: in classes and subssets we now ensure the compatibility between the
inhabitance predicate and the equivalence relation
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.
is considered as a pattern-driven delifting.
- the case ? args v.s. t is reduced to ?[args] v.s. t
- eta-contraction reimplemented
- beta-expand no longer used
delift:
- handle out/in scope tag
ntactics:
- elim sets the out_scope tag for 1 entry
- Procedural: now we generate the exact tactic (in place of some apply tactics) and we do not perform conversion steps before it (1104 change tactics omitted in the lambda-delta devel)
- new target for the PREDICATIVE-TOPOLOGY devel: now is "limits"
1) mk_meta now returns also the index of the created meta
2) added datatypes for new patterns
3) added tactic nchange (using new patterns)
4) changed the type lowtac so that they no longer return the
lists of open and closed goals, that are always computable
in the new system
5) added some wrappers for kernel/refinement functions that
work on statuses and terms labelled with their context
6) new implementation of select that performs subst-expansion.
in-scope/out-scope used to mark regions selected by the pattern
7) ugly implementation of change based on re-opening of tagged
subst entries
projects / helm.git / log