]> matita.cs.unibo.it Git - helm.git/log
helm.git
15 years agoefficiency improvement (buffers are now used everywhere)
Claudio Sacerdoti Coen [Sun, 17 May 2009 19:11:41 +0000 (19:11 +0000)]
efficiency improvement (buffers are now used everywhere)

15 years ago...
Claudio Sacerdoti Coen [Sun, 17 May 2009 19:11:00 +0000 (19:11 +0000)]
...

15 years agobyte tests disabled
Enrico Tassi [Sun, 17 May 2009 18:43:33 +0000 (18:43 +0000)]
byte tests disabled

15 years agoadded patch to not unify any term containing the in_scope tag with
Enrico Tassi [Fri, 15 May 2009 21:14:15 +0000 (21:14 +0000)]
added patch to not unify any term containing the in_scope tag with
an entry in the local context

15 years agoPatch to add a debugging string to HExtlib.split_nth reverted
Claudio Sacerdoti Coen [Fri, 15 May 2009 19:37:08 +0000 (19:37 +0000)]
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.

15 years agoCosmetic.
Claudio Sacerdoti Coen [Fri, 15 May 2009 19:34:31 +0000 (19:34 +0000)]
Cosmetic.

15 years ago- hExtlib: added debugging information for split_nth
Ferruccio Guidi [Thu, 14 May 2009 14:32:39 +0000 (14:32 +0000)]
- hExtlib: added debugging information for split_nth

nat/plus.ma reconstructed :)

15 years ago- libraryObjects: new default "natural numbers" with the uri of nat.
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

15 years agointerpretations placed right after the corresponding definitions (in this way the...
Ferruccio Guidi [Wed, 13 May 2009 19:30:53 +0000 (19:30 +0000)]
interpretations placed right after the corresponding definitions (in this way the script is reconstructed correctly)

logic/equality and datatypes/bool reconstructed :)

15 years ago- matitaEngine: some commands like "coercion" must not be executed when mma's are...
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?)

15 years agoThe singature of the "by" universe is added to the goal signature
Andrea Asperti [Wed, 13 May 2009 15:19:18 +0000 (15:19 +0000)]
The singature of the "by" universe is added to the goal signature
(so univ is never filtered)

15 years agoVia un'altra linea...
Andrea Asperti [Wed, 13 May 2009 09:55:04 +0000 (09:55 +0000)]
Via un'altra linea...

15 years agoSempre piu' breve
Andrea Asperti [Wed, 13 May 2009 09:37:51 +0000 (09:37 +0000)]
Sempre piu' breve

15 years agoSignature is computed on the initial goal, once and for all.
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 *

15 years agoDo we really want to generate eliminators for nested data types? :-)
Claudio Sacerdoti Coen [Tue, 12 May 2009 22:16:00 +0000 (22:16 +0000)]
Do we really want to generate eliminators for nested data types? :-)

15 years agoAll weakly positive types but imbricated ones are now accepted
Claudio Sacerdoti Coen [Tue, 12 May 2009 21:37:40 +0000 (21:37 +0000)]
All weakly positive types but imbricated ones are now accepted
(e.g. ordinals).

15 years ago- Procedural: we now reconstruct "let H := v in t" with "intros (1) H" when the goal...
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

15 years agoWe only filter the smart candidates w.r.t the signature
Andrea Asperti [Tue, 12 May 2009 13:56:17 +0000 (13:56 +0000)]
We only filter the smart candidates w.r.t the signature

15 years agoSome experiments in generation of elimination principles.
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:47:29 +0000 (21:47 +0000)]
Some experiments in generation of elimination principles.

15 years agoppsubst commented out in ppobj
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:46:42 +0000 (21:46 +0000)]
ppsubst commented out in ppobj

15 years agoBug fixed: the relevance list can be shorted then leftno args.
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:45:30 +0000 (21:45 +0000)]
Bug fixed: the relevance list can be shorted then leftno args.

15 years agoMissing spaces inserted here and there.
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:45:00 +0000 (21:45 +0000)]
Missing spaces inserted here and there.

15 years ago- non_punctuational_tacticals ported to NG
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:44:34 +0000 (21:44 +0000)]
- non_punctuational_tacticals ported to NG
- experimental generation of elimination principles passing through ASTs

15 years agoBuffers are now used everywhere for speed-up.
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:42:45 +0000 (21:42 +0000)]
Buffers are now used everywhere for speed-up.
However, the ppsubst is deadly slow even for not-that-large substitutions.

15 years agoNew function list_iter_sep.
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:42:08 +0000 (21:42 +0000)]
New function list_iter_sep.

15 years agoA few lemmas about inclusion.
Andrea Asperti [Mon, 11 May 2009 16:20:24 +0000 (16:20 +0000)]
A few lemmas about inclusion.

15 years agoMore automation
Andrea Asperti [Mon, 11 May 2009 16:19:42 +0000 (16:19 +0000)]
More automation

15 years ago- critical bug fixed in NCicSubstitution.lift:
Claudio Sacerdoti Coen [Sun, 10 May 2009 10:51:06 +0000 (10:51 +0000)]
- 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.

15 years agoStupid typing error fixed.
Claudio Sacerdoti Coen [Fri, 8 May 2009 22:27:02 +0000 (22:27 +0000)]
Stupid typing error fixed.

15 years ago...
Claudio Sacerdoti Coen [Fri, 8 May 2009 22:26:18 +0000 (22:26 +0000)]
...

15 years ago...
Claudio Sacerdoti Coen [Fri, 8 May 2009 22:25:59 +0000 (22:25 +0000)]
...

15 years agoBug fixed: left parameters of constructors were unified before refining them.
Claudio Sacerdoti Coen [Fri, 8 May 2009 22:07:55 +0000 (22:07 +0000)]
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?

15 years agoBug fixed: refinement of mutual recursive definitions used to invert the
Claudio Sacerdoti Coen [Fri, 8 May 2009 21:20:22 +0000 (21:20 +0000)]
Bug fixed: refinement of mutual recursive definitions used to invert the
definitions.

15 years agoImproved tests (for left parameters and mutual recursive definitions).
Claudio Sacerdoti Coen [Fri, 8 May 2009 21:06:29 +0000 (21:06 +0000)]
Improved tests (for left parameters and mutual recursive definitions).

15 years agoBug fixed in refinement of inductive types: left parameters were forgot
Claudio Sacerdoti Coen [Fri, 8 May 2009 18:05:00 +0000 (18:05 +0000)]
Bug fixed in refinement of inductive types: left parameters were forgot
during reconstruction of refined object.

15 years ago1) better implementation of NObj that now calls recursively NQed
Claudio Sacerdoti Coen [Fri, 8 May 2009 16:47:23 +0000 (16:47 +0000)]
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)

15 years agoThe relevance list can be shorter than leftno (when the default is used).
Claudio Sacerdoti Coen [Fri, 8 May 2009 16:29:45 +0000 (16:29 +0000)]
The relevance list can be shorter than leftno (when the default is used).

15 years agoBug fixed in interpretation of records (the type was unbound in the fields).
Claudio Sacerdoti Coen [Fri, 8 May 2009 15:00:03 +0000 (15:00 +0000)]
Bug fixed in interpretation of records (the type was unbound in the fields).

15 years agoConstructors are closed with thier types when computing the signatur
Andrea Asperti [Fri, 8 May 2009 14:50:27 +0000 (14:50 +0000)]
Constructors are closed with thier types when computing the signatur

15 years agoversione automatizzata
Andrea Asperti [Fri, 8 May 2009 14:40:41 +0000 (14:40 +0000)]
versione automatizzata

15 years agosymmetry of inequality sym_neq
Andrea Asperti [Fri, 8 May 2009 14:39:54 +0000 (14:39 +0000)]
symmetry of inequality sym_neq

15 years agodocumentation for the inline command
Ferruccio Guidi [Thu, 7 May 2009 14:30:26 +0000 (14:30 +0000)]
documentation for the inline command

15 years ago- dependenciesParser: updated to new inline syntax
Ferruccio Guidi [Wed, 6 May 2009 19:20:32 +0000 (19:20 +0000)]
- dependenciesParser: updated to new inline syntax

15 years agoLAMBDA-TYPES: mma's recommitted because inline syntax changed
Ferruccio Guidi [Wed, 6 May 2009 19:01:31 +0000 (19:01 +0000)]
LAMBDA-TYPES: mma's recommitted because inline syntax changed

15 years ago- cicUtil: is_sober now detects folded applications
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 :(

15 years agoapply and auto.equational_case call saturation.solve_narrowing
Enrico Tassi [Wed, 6 May 2009 14:26:06 +0000 (14:26 +0000)]
apply and auto.equational_case call saturation.solve_narrowing
that performs goal inference and demodulation

15 years agoupdated comment
Enrico Tassi [Wed, 6 May 2009 10:52:37 +0000 (10:52 +0000)]
updated comment

15 years ago- Procedural: new flag "level=n" to control the reconstruction level (defaults to...
Ferruccio Guidi [Tue, 5 May 2009 18:57:21 +0000 (18:57 +0000)]
- Procedural: new flag "level=n" to control the reconstruction level (defaults to maximum level available). Level 1 reconstruction activated.

15 years ago- hExtlib: new function "list_assoc_all"
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

15 years ago- pretty printer made robust in face of list_nth
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

15 years agomore tests
Enrico Tassi [Tue, 5 May 2009 16:52:32 +0000 (16:52 +0000)]
more tests

15 years agoNuova gestione di "by" per auto.
Andrea Asperti [Tue, 5 May 2009 11:11:00 +0000 (11:11 +0000)]
Nuova gestione di "by" per auto.

15 years agoautobatch by
Andrea Asperti [Tue, 5 May 2009 11:09:36 +0000 (11:09 +0000)]
autobatch by

15 years ago- librarian: 3 bugs fixed in the building system:
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

15 years agorun check_if_goal_is_solved on all goals (active+passive)
Enrico Tassi [Thu, 30 Apr 2009 14:53:46 +0000 (14:53 +0000)]
run check_if_goal_is_solved on all goals (active+passive)

15 years agoAdded an option --enable-annot to the configure to compile with -dtypes
Matthias Puech [Thu, 30 Apr 2009 13:28:13 +0000 (13:28 +0000)]
Added an option --enable-annot to the configure to compile with -dtypes

15 years agoMinor changes pro-automation
Andrea Asperti [Thu, 30 Apr 2009 13:04:28 +0000 (13:04 +0000)]
Minor changes pro-automation

15 years agoAdded a passive table
Andrea Asperti [Thu, 30 Apr 2009 13:03:25 +0000 (13:03 +0000)]
Added a passive table

15 years agoCalling paramodulation instead of demod_all
Andrea Asperti [Thu, 30 Apr 2009 13:02:14 +0000 (13:02 +0000)]
Calling paramodulation instead of demod_all

15 years agoRefinement of inductive type implemented.
Claudio Sacerdoti Coen [Wed, 29 Apr 2009 22:11:08 +0000 (22:11 +0000)]
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?

15 years ago- procedural: bugfix in "Barendregt convention" test
Ferruccio Guidi [Wed, 29 Apr 2009 20:58:49 +0000 (20:58 +0000)]
- 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 !!

15 years ago...
Enrico Tassi [Wed, 29 Apr 2009 13:37:58 +0000 (13:37 +0000)]
...

15 years agocall paramod instead of solve_Rewrite
Enrico Tassi [Wed, 29 Apr 2009 13:37:41 +0000 (13:37 +0000)]
call paramod instead of solve_Rewrite

15 years agono typing
Enrico Tassi [Wed, 29 Apr 2009 13:37:24 +0000 (13:37 +0000)]
no typing

15 years agomany checks guarded with if Utils.debug_metas
Enrico Tassi [Wed, 29 Apr 2009 10:47:55 +0000 (10:47 +0000)]
many checks guarded with if Utils.debug_metas

15 years agoRecords are now interpreted in the NG (but I am sure there is some bug
Claudio Sacerdoti Coen [Wed, 29 Apr 2009 00:04:12 +0000 (00:04 +0000)]
Records are now interpreted in the NG (but I am sure there is some bug
somewhere).

15 years agoInductive definitions are now interpreted (but records are not interpreted yet).
Claudio Sacerdoti Coen [Tue, 28 Apr 2009 23:35:27 +0000 (23:35 +0000)]
Inductive definitions are now interpreted (but records are not interpreted yet).

15 years agoLast commit by Ferruccio reverted since it breaks the library.
Claudio Sacerdoti Coen [Tue, 28 Apr 2009 23:33:49 +0000 (23:33 +0000)]
Last commit by Ferruccio reverted since it breaks the library.
If there is a bug in default, it must be fixed.

15 years agocicNotationUtil: in fresh_name_generator, "\eta" replaced with "eta", which is an...
Ferruccio Guidi [Tue, 28 Apr 2009 19:30:21 +0000 (19:30 +0000)]
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.

15 years agodepenalization of smart apply inside auto, that is now much faster
Enrico Tassi [Tue, 28 Apr 2009 16:23:14 +0000 (16:23 +0000)]
depenalization of smart apply inside auto, that is now much faster

15 years agofixed bug, demodulation was keeping results not strictly smaller
Enrico Tassi [Tue, 28 Apr 2009 16:13:37 +0000 (16:13 +0000)]
fixed bug, demodulation was keeping results not strictly smaller

15 years agohuge commit in automation:
Enrico Tassi [Tue, 28 Apr 2009 13:59:26 +0000 (13:59 +0000)]
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

15 years agomatitacLib: bugfix in .moo generation
Ferruccio Guidi [Mon, 27 Apr 2009 15:51:31 +0000 (15:51 +0000)]
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 :)))))))

15 years agoThe backward compatible management of aliases for NG is now fully completed.
Claudio Sacerdoti Coen [Sun, 26 Apr 2009 10:51:38 +0000 (10:51 +0000)]
The backward compatible management of aliases for NG is now fully completed.
Enjoy the NG Matita!

15 years agoIt is now possible for commands processed by grafiteEngine to either return
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 23:11:35 +0000 (23:11 +0000)]
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.

15 years agoLookup_in_library implemented for new objects. Basically, this stupid (??),
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 22:30:39 +0000 (22:30 +0000)]
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.

15 years agoIt is now possible to declare new aliases using the old syntax
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 21:24:50 +0000 (21:24 +0000)]
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.

15 years ago- matitacLib: lexicon status and grafite status where lost after handling a macro...
Ferruccio Guidi [Sat, 25 Apr 2009 21:12:49 +0000 (21:12 +0000)]
- matitacLib: lexicon status and grafite status where lost after handling a macro. Fixed.

15 years agoThe translation from old aliases to new references is now completely
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 20:30:15 +0000 (20:30 +0000)]
The translation from old aliases to new references is now completely
implemented. It cannot be correct, but it is not supposed to be anyway.

15 years agoApply subst implemented also for Fixpoints.
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 20:29:06 +0000 (20:29 +0000)]
Apply subst implemented also for Fixpoints.

15 years agoType for list_index improved.
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 20:28:07 +0000 (20:28 +0000)]
Type for list_index improved.

15 years agoSlightly improved type for list_index.
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 19:30:10 +0000 (19:30 +0000)]
Slightly improved type for list_index.

15 years agoNew utility function list_index (useful in many places, I think).
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 19:28:06 +0000 (19:28 +0000)]
New utility function list_index (useful in many places, I think).

15 years agoBetter error message.
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 19:12:03 +0000 (19:12 +0000)]
Better error message.

15 years agoDebug option reverted.
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 18:47:14 +0000 (18:47 +0000)]
Debug option reverted.

15 years ago- matitacLib: better handling of the callbacks for the dump operation
Ferruccio Guidi [Sat, 25 Apr 2009 13:16:47 +0000 (13:16 +0000)]
- 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 :(

15 years ago- Grammar for all obj commands ported to NG (let recs and inductives still need
Claudio Sacerdoti Coen [Fri, 24 Apr 2009 20:47:36 +0000 (20:47 +0000)]
- 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.

15 years agoQuick&dirty implementation of neqd:
Claudio Sacerdoti Coen [Fri, 24 Apr 2009 15:11:34 +0000 (15:11 +0000)]
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

15 years ago- transcript: we have now two styles of mma's from grafite:
Ferruccio Guidi [Wed, 22 Apr 2009 20:47:20 +0000 (20:47 +0000)]
- 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

15 years agosyntax colouring for inverters
Wilmer Ricciotti [Wed, 22 Apr 2009 11:17:44 +0000 (11:17 +0000)]
syntax colouring for inverters

15 years agoDisabled debug prints in the inversion principle.
Wilmer Ricciotti [Wed, 22 Apr 2009 10:54:26 +0000 (10:54 +0000)]
Disabled debug prints in the inversion principle.

15 years agoNew command "inverter" used to generate an induction/inversion principle for
Wilmer Ricciotti [Wed, 22 Apr 2009 10:43:52 +0000 (10:43 +0000)]
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).

15 years agodemodulate takes an extra argument 'all', if present it attempts to solve
Enrico Tassi [Wed, 22 Apr 2009 10:30:55 +0000 (10:30 +0000)]
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.

15 years ago- MatitaMisc: we factorized here the function out_preamble used in matitadep
Ferruccio Guidi [Tue, 21 Apr 2009 19:49:59 +0000 (19:49 +0000)]
- 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

15 years agofixed last file restricting auto tables
Enrico Tassi [Tue, 21 Apr 2009 13:03:55 +0000 (13:03 +0000)]
fixed last file restricting auto tables

15 years ago- init_cache_and_tables rewritten using the automation_cache
Enrico Tassi [Mon, 20 Apr 2009 07:58:14 +0000 (07:58 +0000)]
- 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

15 years agoBug fixed: variable capture in previous commit prevented all aliases insertion.
Claudio Sacerdoti Coen [Mon, 20 Apr 2009 02:26:10 +0000 (02:26 +0000)]
Bug fixed: variable capture in previous commit prevented all aliases insertion.

15 years agoSome improvements.
Claudio Sacerdoti Coen [Fri, 17 Apr 2009 12:59:20 +0000 (12:59 +0000)]
Some improvements.

15 years ago...
Claudio Sacerdoti Coen [Fri, 17 Apr 2009 12:21:54 +0000 (12:21 +0000)]
...

15 years agoProcedural: we corrected two errors about the handling of mutcase (the "cases"
Ferruccio Guidi [Thu, 16 Apr 2009 21:50:52 +0000 (21:50 +0000)]
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