]> matita.cs.unibo.it Git - helm.git/log
helm.git
15 years agolambda-delta:
Ferruccio Guidi [Mon, 29 Jun 2009 17:46:08 +0000 (17:46 +0000)]
lambda-delta:
- lib/output: infrastructrure for reduction reporting
  we found just one instance of "referene typing" in the "Grundlagen"
  rt.txt reports where it occurs
- lib/time: bugfix
- basic_rg: bugfix (some relocations were missing)
  the "Grundlagen" now typechecks :)

15 years ago...
Enrico Tassi [Mon, 29 Jun 2009 14:44:21 +0000 (14:44 +0000)]
...

15 years agodo not infer on closed goals
Enrico Tassi [Mon, 29 Jun 2009 14:36:37 +0000 (14:36 +0000)]
do not infer on closed goals

15 years agoremoved a maybe diverging test
Enrico Tassi [Mon, 29 Jun 2009 14:30:18 +0000 (14:30 +0000)]
removed a maybe diverging test

15 years ago...
Enrico Tassi [Mon, 29 Jun 2009 13:45:03 +0000 (13:45 +0000)]
...

15 years agoFirst attempt for refined goal selection strategy
denes [Mon, 29 Jun 2009 13:33:42 +0000 (13:33 +0000)]
First attempt for refined goal selection strategy

15 years agoadded (but not active) last chance idea
Enrico Tassi [Mon, 29 Jun 2009 12:59:20 +0000 (12:59 +0000)]
added (but not active) last chance idea

15 years agoImplemented orphan murdering technique
denes [Mon, 29 Jun 2009 10:41:50 +0000 (10:41 +0000)]
Implemented orphan murdering technique

15 years agonew make test target
Enrico Tassi [Mon, 29 Jun 2009 10:16:17 +0000 (10:16 +0000)]
new make test target

15 years agonew kernel basic_rg: implements ufficial lambda-delta with de Bruijn indexes
Ferruccio Guidi [Sun, 28 Jun 2009 17:59:13 +0000 (17:59 +0000)]
new kernel basic_rg: implements ufficial lambda-delta with de Bruijn indexes

15 years agoattempt to run a last chance procedure after the timeout
Andrea Asperti [Fri, 26 Jun 2009 15:38:56 +0000 (15:38 +0000)]
attempt to run a last chance procedure after the timeout

15 years agothe timeout is passed to test last chance
Andrea Asperti [Fri, 26 Jun 2009 15:38:02 +0000 (15:38 +0000)]
the timeout is passed to test last chance

15 years agothis case is not assert false since it can happen if occur_check
Andrea Asperti [Fri, 26 Jun 2009 13:47:25 +0000 (13:47 +0000)]
this case is not assert false since it can happen if occur_check
makes fail the unification

15 years agofixed parsing
Andrea Asperti [Fri, 26 Jun 2009 13:21:55 +0000 (13:21 +0000)]
fixed parsing

15 years agoconvenient problem lists
Andrea Asperti [Fri, 26 Jun 2009 12:01:30 +0000 (12:01 +0000)]
convenient problem lists

15 years agoan easy for loop
Andrea Asperti [Fri, 26 Jun 2009 12:01:01 +0000 (12:01 +0000)]
an easy for loop

15 years agodeep subsumption activated
Andrea Asperti [Fri, 26 Jun 2009 11:02:11 +0000 (11:02 +0000)]
deep subsumption activated

15 years agotest for deep subsumption added
Andrea Asperti [Fri, 26 Jun 2009 11:00:20 +0000 (11:00 +0000)]
test for deep subsumption added

15 years agoImplemented orphan murder test (clauses are not discarded for now)
denes [Fri, 26 Jun 2009 09:46:23 +0000 (09:46 +0000)]
Implemented orphan murder test (clauses are not discarded for now)
Re-enabled zero weight trick

15 years ago...
Enrico Tassi [Thu, 25 Jun 2009 21:29:22 +0000 (21:29 +0000)]
...

15 years agobetter doc
Enrico Tassi [Thu, 25 Jun 2009 21:23:44 +0000 (21:23 +0000)]
better doc

15 years agotimeouts are passed as arguments, so that tptpprover can
Enrico Tassi [Thu, 25 Jun 2009 20:54:52 +0000 (20:54 +0000)]
timeouts are passed as arguments, so that tptpprover can
accept --timeout argument. Moreover it prints the proof
according to the SZS ontology

15 years ago- some depend files :)
Ferruccio Guidi [Thu, 25 Jun 2009 19:16:36 +0000 (19:16 +0000)]
- some depend files :)

15 years agothe prover is almost OK, types in fuctors a bit extended to
Enrico Tassi [Thu, 25 Jun 2009 16:47:21 +0000 (16:47 +0000)]
the prover is almost OK, types in fuctors a bit extended to
ease their instantiation

15 years agoFirst version of deep_subsumption.
Andrea Asperti [Thu, 25 Jun 2009 15:55:14 +0000 (15:55 +0000)]
First version of deep_subsumption.

15 years agoVarious fixes
denes [Thu, 25 Jun 2009 15:24:09 +0000 (15:24 +0000)]
Various fixes

15 years agonew function
Enrico Tassi [Thu, 25 Jun 2009 15:10:43 +0000 (15:10 +0000)]
new function

15 years ago...
Enrico Tassi [Thu, 25 Jun 2009 14:45:37 +0000 (14:45 +0000)]
...

15 years agomatitaprover is almost there
Enrico Tassi [Thu, 25 Jun 2009 14:42:56 +0000 (14:42 +0000)]
matitaprover is almost there

15 years ago...
Enrico Tassi [Thu, 25 Jun 2009 13:12:52 +0000 (13:12 +0000)]
...

15 years agoinitial import of standalone matitaprover binary
Enrico Tassi [Thu, 25 Jun 2009 13:08:35 +0000 (13:08 +0000)]
initial import of standalone matitaprover binary

15 years agoNow using age selection
denes [Thu, 25 Jun 2009 12:19:45 +0000 (12:19 +0000)]
Now using age selection

15 years agocode refactoring for paramodulation
Enrico Tassi [Thu, 25 Jun 2009 10:17:36 +0000 (10:17 +0000)]
code refactoring for paramodulation

15 years agonew function list_mapi_acc
Enrico Tassi [Thu, 25 Jun 2009 10:17:13 +0000 (10:17 +0000)]
new function list_mapi_acc

15 years agoFixed is_identity for facts
denes [Thu, 25 Jun 2009 09:52:58 +0000 (09:52 +0000)]
Fixed is_identity for facts

15 years agoFixed insertion of passive clauses
denes [Thu, 25 Jun 2009 08:54:30 +0000 (08:54 +0000)]
Fixed insertion of passive clauses

15 years agoCode factorization
Andrea Asperti [Thu, 25 Jun 2009 08:53:38 +0000 (08:53 +0000)]
Code factorization

15 years agoRemoved debug printing
denes [Wed, 24 Jun 2009 17:02:25 +0000 (17:02 +0000)]
Removed debug printing

15 years agoNow inserting hypothesis and goal with zero weight
denes [Wed, 24 Jun 2009 16:59:41 +0000 (16:59 +0000)]
Now inserting hypothesis and goal with zero weight

15 years agoExtended is_identity test
denes [Wed, 24 Jun 2009 16:00:35 +0000 (16:00 +0000)]
Extended is_identity test
First step towards age selection

15 years agoImplemented check for duplicates (in goals)
denes [Wed, 24 Jun 2009 12:30:56 +0000 (12:30 +0000)]
Implemented check for duplicates (in goals)

15 years agoRemoved old debugging assertion
denes [Tue, 23 Jun 2009 22:46:49 +0000 (22:46 +0000)]
Removed old debugging assertion

15 years ago- procedural: basic support for lapply (solves a problem in the reconstruction of...
Ferruccio Guidi [Tue, 23 Jun 2009 21:00:06 +0000 (21:00 +0000)]
- procedural: basic support for lapply (solves a problem in the reconstruction of algebra/groups.ma)
- lambda-delta: bugfix in line counts and nodes counts

15 years agoRemoved debug printing raising Failure
denes [Tue, 23 Jun 2009 17:57:40 +0000 (17:57 +0000)]
Removed debug printing raising Failure

15 years agoRemoved debug printing
denes [Tue, 23 Jun 2009 17:10:40 +0000 (17:10 +0000)]
Removed debug printing

15 years agoRewrote the main loop for paramodulation
denes [Tue, 23 Jun 2009 16:56:02 +0000 (16:56 +0000)]
Rewrote the main loop for paramodulation

15 years agoundo/serialization for universes implemented
Enrico Tassi [Tue, 23 Jun 2009 16:00:55 +0000 (16:00 +0000)]
undo/serialization for universes implemented

15 years agoDebugging prerr_endlines removed.
Claudio Sacerdoti Coen [Tue, 23 Jun 2009 11:46:42 +0000 (11:46 +0000)]
Debugging prerr_endlines removed.

15 years ago1) NCicTypechecker.typecheck_obj removed, since it did not add to the
Claudio Sacerdoti Coen [Tue, 23 Jun 2009 11:46:16 +0000 (11:46 +0000)]
1) NCicTypechecker.typecheck_obj removed, since it did not add to the
   environment (and thus all objects were type-checked at least twice)
2) NCicEnvironment.check_and_add_obj that checks and add an object
3) added NCicEnvironment.invalidate_obj that invalidate all objects after a
   given one (that comprised)
4) NCicLibrary.add_obj now calls the NCicEnvironment.check_and_add_obj;
   NCicLibrary.time_travel now calls NCicEnvironment.invalidate_obj

Note: it could happen that an object is in the environment but not in the
      library and thus it could not be invalidated by time_travel.
      In practice, this is safe anyway and it will never happen.

15 years agoFixed nasty bug in maxvar updating
denes [Tue, 23 Jun 2009 10:30:55 +0000 (10:30 +0000)]
Fixed nasty bug in maxvar updating

15 years ago- Bug fixed: removed URIs were not removed from the dependencies DB.
Claudio Sacerdoti Coen [Tue, 23 Jun 2009 10:23:59 +0000 (10:23 +0000)]
- Bug fixed: removed URIs were not removed from the dependencies DB.
- The assert failure has been removed since in some situations (????) an
  empty dir (no new objects) was not created and thus it was normal that it
  was not removed. TO BE BETTER UNDERSTOOD

15 years agoremoved problem not in UEQ
Enrico Tassi [Tue, 23 Jun 2009 08:07:22 +0000 (08:07 +0000)]
removed problem not in UEQ

15 years ago- nodes count is now working for aut and meta
Ferruccio Guidi [Mon, 22 Jun 2009 22:53:12 +0000 (22:53 +0000)]
- nodes count is now working for aut and meta
- bugfix in autLexer
- comment fix in aut

15 years agoAdded more precise time information
denes [Mon, 22 Jun 2009 17:12:49 +0000 (17:12 +0000)]
Added more precise time information

15 years agoAdded problems from CASC 208
denes [Mon, 22 Jun 2009 17:03:32 +0000 (17:03 +0000)]
Added problems from CASC 208

15 years agoRegenerated problems with corrected tptp2grafite
denes [Mon, 22 Jun 2009 16:58:17 +0000 (16:58 +0000)]
Regenerated problems with corrected tptp2grafite

15 years agoCorrected proof visiting (topological sort)
denes [Mon, 22 Jun 2009 16:51:14 +0000 (16:51 +0000)]
Corrected proof visiting (topological sort)

15 years agoSmall debugging in tptp2grafite
denes [Mon, 22 Jun 2009 16:50:37 +0000 (16:50 +0000)]
Small debugging in tptp2grafite

15 years agoAdded injective compose
Wilmer Ricciotti [Sun, 21 Jun 2009 18:32:22 +0000 (18:32 +0000)]
Added injective compose

15 years ago- cicNotationPp: bugfix in record syntax
Ferruccio Guidi [Sun, 21 Jun 2009 08:21:50 +0000 (08:21 +0000)]
- cicNotationPp: bugfix in record syntax
- lambda-delta: version update

15 years agoSome notation and additional lemmata.
Wilmer Ricciotti [Sat, 20 Jun 2009 16:53:44 +0000 (16:53 +0000)]
Some notation and additional lemmata.

15 years agoDebugging
Claudio Sacerdoti Coen [Sat, 20 Jun 2009 13:47:57 +0000 (13:47 +0000)]
Debugging

15 years ago"matitaclean all" ported to NG
Claudio Sacerdoti Coen [Fri, 19 Jun 2009 15:49:45 +0000 (15:49 +0000)]
"matitaclean all" ported to NG

15 years agoInvert dependencies between baseuris (files) are now stored in the db.
Claudio Sacerdoti Coen [Fri, 19 Jun 2009 15:43:10 +0000 (15:43 +0000)]
Invert dependencies between baseuris (files) are now stored in the db.
Hence decompilation is now fully correct (???).

15 years agoBug fixed: refreshing of uris for the db.
Claudio Sacerdoti Coen [Fri, 19 Jun 2009 14:59:35 +0000 (14:59 +0000)]
Bug fixed: refreshing of uris for the db.

15 years agoMore improvements.
Wilmer Ricciotti [Fri, 19 Jun 2009 14:53:57 +0000 (14:53 +0000)]
More improvements.

15 years agoThe global db is now updated during decompilation.
Claudio Sacerdoti Coen [Fri, 19 Jun 2009 14:20:00 +0000 (14:20 +0000)]
The global db is now updated during decompilation.

15 years agoPersistent db (to lookup names in the library) inefficiently implemented as
Claudio Sacerdoti Coen [Fri, 19 Jun 2009 14:05:18 +0000 (14:05 +0000)]
Persistent db (to lookup names in the library) inefficiently implemented as
an associative list which is:

 1) loaded from disk and stored in memory when matita starts
 2) updated every time a file is saved

Still to be implemented: decompilation.

15 years agoNG decompilation is now activated. However, it is called from the old
Claudio Sacerdoti Coen [Fri, 19 Jun 2009 12:42:05 +0000 (12:42 +0000)]
NG decompilation is now activated. However, it is called from the old
decompilation that cannot detect when a NG-only file A is used by another
NG-only file B. As a consequence, decompiling A does not decompile B too.

15 years agoEstatus finally merged into the global status using inheritance.
Claudio Sacerdoti Coen [Fri, 19 Jun 2009 10:16:23 +0000 (10:16 +0000)]
Estatus finally merged into the global status using inheritance.
Major code simplification everywhere :-)

15 years agoUseless GrafiteTypes.get_baseuri removed.
Claudio Sacerdoti Coen [Fri, 19 Jun 2009 08:40:48 +0000 (08:40 +0000)]
Useless GrafiteTypes.get_baseuri removed.

15 years agoMore statuses converted to objects.
Claudio Sacerdoti Coen [Fri, 19 Jun 2009 08:34:19 +0000 (08:34 +0000)]
More statuses converted to objects.

15 years agoGood:
Claudio Sacerdoti Coen [Fri, 19 Jun 2009 07:21:49 +0000 (07:21 +0000)]
Good:
1) all set_* methods are now polymorphic
2) no more :> coercions
3) no more technical class types

Bad:
1) some polymorphic set_* methods have explicit row types that are
   problematic when extending another class in another file. The
   row types should just be #classname, but ocaml rejects them that
   way.

15 years agodebug pps removed
Enrico Tassi [Thu, 18 Jun 2009 17:26:41 +0000 (17:26 +0000)]
debug pps removed

15 years agobetter exception handling
Enrico Tassi [Thu, 18 Jun 2009 17:26:27 +0000 (17:26 +0000)]
better exception handling

15 years agoproof patching!
Enrico Tassi [Thu, 18 Jun 2009 16:58:39 +0000 (16:58 +0000)]
proof patching!

15 years agoObjects are now used to represent also the tactic status.
Claudio Sacerdoti Coen [Thu, 18 Jun 2009 16:48:35 +0000 (16:48 +0000)]
Objects are now used to represent also the tactic status.
Cool (but error messages can be bad).

15 years agoAdded ntry and nassumption tactics
denes [Thu, 18 Jun 2009 15:26:24 +0000 (15:26 +0000)]
Added ntry and nassumption tactics

15 years agocallbacks were taking in input a status bu were not using them.
Enrico Tassi [Thu, 18 Jun 2009 14:46:17 +0000 (14:46 +0000)]
callbacks were taking in input a status bu were not using them.
thanks to the new #type for statuses this was a problem, and Obj.magic
was required to fix them. Removed both the dummy parameter and the
unsafe cast

15 years agoFixed stupid path
denes [Thu, 18 Jun 2009 11:43:51 +0000 (11:43 +0000)]
Fixed stupid path

15 years agoAdded script useful for running benchmarks
denes [Thu, 18 Jun 2009 11:23:18 +0000 (11:23 +0000)]
Added script useful for running benchmarks

15 years agoChanged parenthesis to optional around letin ident (and type)
denes [Thu, 18 Jun 2009 11:01:08 +0000 (11:01 +0000)]
Changed parenthesis to optional around letin ident (and type)

15 years agoFixed wrong types in proof terms
denes [Thu, 18 Jun 2009 10:59:22 +0000 (10:59 +0000)]
Fixed wrong types in proof terms

15 years agoStricter type: the type now shows that disambiguation only alter the lexicon.
Claudio Sacerdoti Coen [Thu, 18 Jun 2009 09:17:53 +0000 (09:17 +0000)]
Stricter type: the type now shows that disambiguation only alter the lexicon.
In this way we are forced to manually set the content of the object in place of
setting the whole object, that leads to information loss since in the meanwhile
new commands may have altered the rest of the state.

15 years ago1) grafiteWalker removed
Claudio Sacerdoti Coen [Thu, 18 Jun 2009 09:07:37 +0000 (09:07 +0000)]
1) grafiteWalker removed
2) ncommands and commands are now two distinct syntactic entries
3) NEstatus.status and LexiconEngine.status are now objects

15 years agoproof reconstruction almost OK
Enrico Tassi [Wed, 17 Jun 2009 13:35:12 +0000 (13:35 +0000)]
proof reconstruction almost OK

15 years agoInitial implementation of statuses using objects in place of nested records.
Claudio Sacerdoti Coen [Wed, 17 Jun 2009 11:47:59 +0000 (11:47 +0000)]
Initial implementation of statuses using objects in place of nested records.
So nicer!

The only major problem is that the NCicLibrary functor does not return a
function #status as 'status -> 'status, but a function status -> status.
Thus I have to painfully wrap NCicLibrary.Realizer(...).require in NRstatus.

TO REMEMBER:
- every function that works on a data type that used to be put in the status
  (e.g. a db) must now work on a functional class with just two members
  (db and set_db). Moreover, every function in the module must work on the
  open variants of the class type, i.e. #status

15 years agoAdded optionnal one pass simplification (instead of keep_simplified)
denes [Wed, 17 Jun 2009 08:47:34 +0000 (08:47 +0000)]
Added optionnal one pass simplification (instead of keep_simplified)
Fix for varlists (we traverse the term to collect occuring variables)

15 years agofirst proof reconstruction attempt, still bugged since it
Enrico Tassi [Tue, 16 Jun 2009 23:07:35 +0000 (23:07 +0000)]
first proof reconstruction attempt, still bugged since it
does all steps in a forward fashion

15 years ago1) unification hint now takes NG terms (as it should have been from the very
Claudio Sacerdoti Coen [Tue, 16 Jun 2009 23:00:56 +0000 (23:00 +0000)]
1) unification hint now takes NG terms (as it should have been from the very
   beginning)
2) refresh_uris_in_term is now passed to the constructor of the
   existential/universal data type in NCicLibrary
3) URIs are now refreshed in unification hint data

15 years ago1) NCicLibrary (which is untrusted) moved after NCicUntrusted.
Claudio Sacerdoti Coen [Tue, 16 Jun 2009 22:35:03 +0000 (22:35 +0000)]
1) NCicLibrary (which is untrusted) moved after NCicUntrusted.
   NCicLibrary registers get_obj to NCicEnvironemnt (and to NCicPp)
2) URIs are now refreshed when objects are included from disk

Observation: even NCicPp is untrusted. Thus its implementation should be put
at the end and some references set to one early module. Which one? Two
choices: NCic or NCicPp (two modules, one with the implementation follows).
Could the same be done for NCicLibrary too in order to bring back the explicit
dependency of NCicEnvironment over NCicLibrary? [ In that case, remember to
change back the exception caught by GrafiteDisambiguate ]

15 years agoImplementation of existential type improved (more strict checking).
Claudio Sacerdoti Coen [Tue, 16 Jun 2009 21:58:28 +0000 (21:58 +0000)]
Implementation of existential type improved (more strict checking).

15 years agoavoid fixing non-recursive terms
Enrico Tassi [Tue, 16 Jun 2009 21:57:36 +0000 (21:57 +0000)]
avoid fixing non-recursive terms

15 years agowe fix recursive object reference with the correct height
Enrico Tassi [Tue, 16 Jun 2009 18:28:17 +0000 (18:28 +0000)]
we fix recursive object reference with the correct height
just before adding it to the library

15 years agoFIX OF THE PREVIOUS EXPERIMENTAL COMMIT:
Claudio Sacerdoti Coen [Tue, 16 Jun 2009 17:37:05 +0000 (17:37 +0000)]
FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:

Instead of serializing closures (of type status -> status), we now
serialize data. This is achieved by implementing an existential type

       NCicLibrary.Serializer(struct type status end).obj

whose semantics is "\exists 'a. 'a -> status -> status"
and by putting in the dump a list of these existential types.

The current implementation is the type-unsafe one based internally on Obj.magic.
However, the interface is (should be?) type-safe.
Other type-safe implementations could be derived by the ocaml m.l. thread on
existential types. In particular, I remember implementations via:
  - references
  - functors
  - exceptions
  - impredicative encoding via polymorphic methods

This fix allow to change the Matita code without invalidating the library.

(Critical) things still to be done:
 - decompilation
 - refreshment of URIs

15 years agowe corrected some reduction bugs about renaming.
Ferruccio Guidi [Tue, 16 Jun 2009 14:20:34 +0000 (14:20 +0000)]
we corrected some reduction bugs about renaming.

The grundlagen is now fully typechecked :)

15 years agowe removed some old code and fixed a reduction bug: two instances fo the
Ferruccio Guidi [Mon, 15 Jun 2009 21:15:57 +0000 (21:15 +0000)]
we removed some old code and fixed a reduction bug: two instances fo the
same constant applied to a different number of arguments may be convertible

We now check grundlagen up to item 109 :) (with naive sort inclusion :( puah)

15 years agoEXPERIMENTAL COMMIT (part B, by CSC :-):
Enrico Tassi [Mon, 15 Jun 2009 16:41:47 +0000 (16:41 +0000)]
EXPERIMENTAL COMMIT (part B, by CSC :-):
 - objects are now individually serialized too
   (but never decompiled)

CRITICAL OBSERVATION:
 - closures in ocaml are pointers in the binary, hence the library
   must be decompiled at every single change in matita's code

15 years agoEXPERIMENTAL COMMIT (by CSC,actuall :-)
Enrico Tassi [Mon, 15 Jun 2009 16:22:18 +0000 (16:22 +0000)]
EXPERIMENTAL COMMIT (by CSC,actuall :-)
This commit partially implements (in NCicLibrary) serialization for NG.
It creates several .matita/matita/.../foo.ng files that are ocaml dumps
of closures (NRstatus.refiner_status -> NRstatus.refiner_status) to be applied
to the current status.

The test tests/ng_includeB.ma shows how unification hints are preserved.

TODO:
 a) decompilation is implemented in NCicLibrary, but not called anywhere
 b) serialization of objects (and "query" db (and old to new cache??)) not
    implemented yet
 c) objects are removed from the library, but not from the environment!

15 years ago...
Enrico Tassi [Mon, 15 Jun 2009 11:18:02 +0000 (11:18 +0000)]
...