]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agoThe type of the left parameters of an inductive type can now be omitted.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 16:02:39 +0000 (16:02 +0000)]
The type of the left parameters of an inductive type can now be omitted.

19 years agoGot rid of a few bugs.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 15:47:37 +0000 (15:47 +0000)]
Got rid of a few bugs.

19 years agoGot rid of a few warnings.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 15:45:35 +0000 (15:45 +0000)]
Got rid of a few warnings.

19 years agoGot rid of a few warnings.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 15:39:29 +0000 (15:39 +0000)]
Got rid of a few warnings.

19 years agoan assert failure changed to an exception and a bit of code cleanupt
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 14:51:04 +0000 (14:51 +0000)]
an assert failure changed to an exception and a bit of code cleanupt

19 years agoThe user is no longer obliged to give the types for definitions.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 14:31:43 +0000 (14:31 +0000)]
The user is no longer obliged to give the types for definitions.

19 years agointegrated indexing.ml, breaks everything :-P (previous working version tagged PRE_IN...
Alberto Griggio [Fri, 10 Jun 2005 14:16:29 +0000 (14:16 +0000)]
integrated indexing.ml, breaks everything :-P (previous working version tagged PRE_INDEXING_1)

19 years agodebugging to false
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 14:11:59 +0000 (14:11 +0000)]
debugging to false

19 years ago* (Head) beta reduction functions factorized
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 14:03:41 +0000 (14:03 +0000)]
* (Head) beta reduction functions factorized
* the type inferred for a match both in the kernel and in the refiner
  are now beta reduced

19 years agoMore debugging infos.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 13:42:47 +0000 (13:42 +0000)]
More debugging infos.

19 years ago...
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 13:00:51 +0000 (13:00 +0000)]
...

19 years agounshare.ml*
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 12:55:23 +0000 (12:55 +0000)]
unshare.ml*

19 years agoComplete unsharing of terms.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 12:54:44 +0000 (12:54 +0000)]
Complete unsharing of terms.

19 years ago- bound GtkSourceLanguagesManager (only get_lang..from_mime_type)
Stefano Zacchiroli [Fri, 10 Jun 2005 12:35:49 +0000 (12:35 +0000)]
- bound GtkSourceLanguagesManager (only get_lang..from_mime_type)

19 years agosnaphot
Stefano Zacchiroli [Fri, 10 Jun 2005 11:38:53 +0000 (11:38 +0000)]
snaphot
- better creation of GtkSourceView (using C constructor)
- bound GtkSourceLanguage
- preliminary binding of GtkSourceLanguagesManager

19 years agohead_beta_reduce used to create applications of applications. Fixed.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 11:06:24 +0000 (11:06 +0000)]
head_beta_reduce used to create applications of applications. Fixed.
head_beta_reduce renamed to beta_reduce (since it performs full beta reduction).

19 years ago...
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 09:26:29 +0000 (09:26 +0000)]
...

19 years agoadded source_view ?text constructor parameter
Stefano Zacchiroli [Thu, 9 Jun 2005 21:12:20 +0000 (21:12 +0000)]
added source_view ?text constructor parameter

19 years agotest file
Stefano Zacchiroli [Thu, 9 Jun 2005 21:12:04 +0000 (21:12 +0000)]
test file

19 years agoload "test.txt" and show it in a scrolled win
Stefano Zacchiroli [Thu, 9 Jun 2005 21:11:52 +0000 (21:11 +0000)]
load "test.txt" and show it in a scrolled win

19 years agosnapshot
Stefano Zacchiroli [Thu, 9 Jun 2005 20:48:04 +0000 (20:48 +0000)]
snapshot
- implemented many methods of GtkSourceBuffer
- fixed creation of GtkSourceView (no longer assert failure on undo)

19 years agoprima implementazione di demodulate, superposition_left e superposition_right
Alberto Griggio [Thu, 9 Jun 2005 17:19:17 +0000 (17:19 +0000)]
prima implementazione di demodulate, superposition_left e superposition_right
con gli "indici"...

19 years agocambiato il tipo equality, aggiunto l'ordinamento tra left e right
Alberto Griggio [Thu, 9 Jun 2005 17:17:30 +0000 (17:17 +0000)]
cambiato il tipo equality, aggiunto l'ordinamento tra left e right

19 years ago...
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:28:34 +0000 (16:28 +0000)]
...

19 years agotest_instance.ma moved to interactive/ (whose tests are not executed for
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:24:24 +0000 (16:24 +0000)]
test_instance.ma moved to interactive/ (whose tests are not executed for
regression testing)

19 years agointro ==> intros
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:23:05 +0000 (16:23 +0000)]
intro ==> intros

19 years agoError message improved.
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:22:51 +0000 (16:22 +0000)]
Error message improved.

19 years agoNow CicMetaSubst.delift_rels restricts the Metas when a failure is faced.
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:09:55 +0000 (16:09 +0000)]
Now CicMetaSubst.delift_rels restricts the Metas when a failure is faced.
This closes yet another bug in the inference of the outtype for matches.

19 years agoNo more explicit types for the branches of the matches: all the bugs
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:08:57 +0000 (16:08 +0000)]
No more explicit types for the branches of the matches: all the bugs
preventing automatic type inference have been fixed.

19 years agosnapshot
Stefano Zacchiroli [Thu, 9 Jun 2005 15:34:11 +0000 (15:34 +0000)]
snapshot
- almost fully bound SourceView
- started binding of SourceBuffer

19 years agoCicSubstitution.delift ==> CicMetaSubst.delift_rels
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 15:04:49 +0000 (15:04 +0000)]
CicSubstitution.delift ==> CicMetaSubst.delift_rels
(since it will need to restrict metavariables in case of Rel capture)

19 years agolablgtksourceview: first checkin, almost nothing bound ...
Stefano Zacchiroli [Thu, 9 Jun 2005 14:11:13 +0000 (14:11 +0000)]
lablgtksourceview: first checkin, almost nothing bound ...

19 years agoException raised by delift changed:
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 13:41:22 +0000 (13:41 +0000)]
Exception raised by delift changed:
Failure ==> DeliftingWouldCaptureAFreeVariable

19 years agoDebugging code removed.
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 13:03:49 +0000 (13:03 +0000)]
Debugging code removed.

19 years agoadded debug item for coercion
Enrico Tassi [Thu, 9 Jun 2005 11:46:58 +0000 (11:46 +0000)]
added debug item for coercion

19 years agoadded \n to "file saved" message
Enrico Tassi [Thu, 9 Jun 2005 11:46:28 +0000 (11:46 +0000)]
added \n to "file saved" message

19 years agoadded whd before uri_of_term
Enrico Tassi [Thu, 9 Jun 2005 11:45:45 +0000 (11:45 +0000)]
added whd before uri_of_term

19 years agoremoved debug prints
Enrico Tassi [Thu, 9 Jun 2005 11:44:27 +0000 (11:44 +0000)]
removed debug prints

19 years agofixed remove_coercion
Enrico Tassi [Thu, 9 Jun 2005 11:43:40 +0000 (11:43 +0000)]
fixed remove_coercion

19 years agoandrea.ma removed (superseded by match.ma)
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 10:43:44 +0000 (10:43 +0000)]
andrea.ma removed (superseded by match.ma)

19 years agoUpdated to the new syntax for match.
Andrea Asperti [Thu, 9 Jun 2005 10:33:47 +0000 (10:33 +0000)]
Updated to the new syntax for match.

19 years agosimplified cicBrowser: whelp bar is now always visible
Stefano Zacchiroli [Thu, 9 Jun 2005 07:35:30 +0000 (07:35 +0000)]
simplified cicBrowser: whelp bar is now always visible

19 years ago- handles about:* uris in cicBrowser
Stefano Zacchiroli [Wed, 8 Jun 2005 20:17:03 +0000 (20:17 +0000)]
- handles about:* uris in cicBrowser
- added comboboxentry in cicBrowser (still ugly ...)

19 years agofixed history handling: now both "home" and link reached via href are
Stefano Zacchiroli [Wed, 8 Jun 2005 19:21:33 +0000 (19:21 +0000)]
fixed history handling: now both "home" and link reached via href are
correctly stored and remembered in history

19 years agorewritten cicBrowser handling of uri text entry, still some issued with browser
Stefano Zacchiroli [Wed, 8 Jun 2005 16:53:28 +0000 (16:53 +0000)]
rewritten cicBrowser handling of uri text entry, still some issued with browser
history

19 years agoThe type of a top-level "let rec" can be optional.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:50:36 +0000 (16:50 +0000)]
The type of a top-level "let rec" can be optional.

19 years agoLet's try to make the "let rec" construct infer its arguments.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:49:40 +0000 (16:49 +0000)]
Let's try to make the "let rec" construct infer its arguments.

19 years agoSyntax for top-level "let rec" fixed.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:36:55 +0000 (16:36 +0000)]
Syntax for top-level "let rec" fixed.

19 years agoUsing the lighter syntax for "let recs".
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:32:50 +0000 (16:32 +0000)]
Using the lighter syntax for "let recs".

19 years agoUsing the top-level syntax for let-rec definitions.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:31:02 +0000 (16:31 +0000)]
Using the top-level syntax for let-rec definitions.

19 years agoThe file is now well formed.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:30:04 +0000 (16:30 +0000)]
The file is now well formed.

19 years agoNew syntax (again) for let rec binders:
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:19:14 +0000 (16:19 +0000)]
New syntax (again) for let rec binders:
let rec f x y (z,w:T) h (c:T) = ...

19 years agoNew lighter syntax for "let rec".
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:11:00 +0000 (16:11 +0000)]
New lighter syntax for "let rec".

19 years agoBug fixed: a symbol must be formed of just one (unicode) character.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:09:08 +0000 (16:09 +0000)]
Bug fixed: a symbol must be formed of just one (unicode) character.

19 years agoQuery results were erroneously tagged as directories.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:06:47 +0000 (16:06 +0000)]
Query results were erroneously tagged as directories.

19 years ago1. syntax of match changed
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 15:24:24 +0000 (15:24 +0000)]
1. syntax of match changed
2. syntax of the bindings of "let rec" made lighter

19 years agoYet another bug fixed in the inference of the outtype for match: convertibility
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 15:17:15 +0000 (15:17 +0000)]
Yet another bug fixed in the inference of the outtype for match: convertibility
was used in place of unification, making type inference much less powerful
in several useful cases.

19 years agoThe getter maps are now dumped also if matitac exits abruptly.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 14:11:02 +0000 (14:11 +0000)]
The getter maps are now dumped also if matitac exits abruptly.

19 years agoAdded new target "make tests" for regression testing.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 14:00:35 +0000 (14:00 +0000)]
Added new target "make tests" for regression testing.

19 years agoFixed a few bugs in the inference of the outtype for a match.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 13:47:53 +0000 (13:47 +0000)]
Fixed a few bugs in the inference of the outtype for a match.
In particular the instances of the left parameter that occur in the
outtype were not lifted properly because of the abstractions that correspond
to the right parameters.

19 years agoFixed inference of outtype for match when the inductive type has left and/or
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 10:52:20 +0000 (10:52 +0000)]
Fixed inference of outtype for match when the inductive type has left and/or
right parameters.

19 years agoHarder test (with empty inductive types and left and right arguments to
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 10:50:31 +0000 (10:50 +0000)]
Harder test (with empty inductive types and left and right arguments to
inductive types). It does not compile yet.

19 years agoMore informative error message.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 10:49:49 +0000 (10:49 +0000)]
More informative error message.

19 years agoclean now also performs clean_metas (since make also creates the metas)
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 09:45:59 +0000 (09:45 +0000)]
clean now also performs clean_metas (since make also creates the metas)

19 years agoadded icons to entries shown in cicbrowser so that directories are
Stefano Zacchiroli [Wed, 8 Jun 2005 09:10:17 +0000 (09:10 +0000)]
added icons to entries shown in cicbrowser so that directories are
distinguishable from objects

19 years agosnapshot (minor changes)
Stefano Zacchiroli [Wed, 8 Jun 2005 07:41:51 +0000 (07:41 +0000)]
snapshot (minor changes)

19 years ago* generate list elements in correct order
Luca Padovani [Tue, 7 Jun 2005 18:24:59 +0000 (18:24 +0000)]
* generate list elements in correct order
* handle list inside boxes
* handle box layout
* generate separator between elements (not after elements)

19 years agoadded test for coercions
Enrico Tassi [Tue, 7 Jun 2005 17:37:53 +0000 (17:37 +0000)]
added test for coercions

19 years agoadded coercions
Enrico Tassi [Tue, 7 Jun 2005 17:37:16 +0000 (17:37 +0000)]
added coercions

19 years agoimplemented attributes pretty printing
Stefano Zacchiroli [Tue, 7 Jun 2005 17:21:32 +0000 (17:21 +0000)]
implemented attributes pretty printing

19 years agohandles "elimCProp" value for class attribute
Stefano Zacchiroli [Tue, 7 Jun 2005 17:21:08 +0000 (17:21 +0000)]
handles "elimCProp" value for class attribute

19 years agoadded object attributes
Stefano Zacchiroli [Tue, 7 Jun 2005 17:20:33 +0000 (17:20 +0000)]
added object attributes

19 years agoremoved coercions from status
Enrico Tassi [Tue, 7 Jun 2005 16:43:33 +0000 (16:43 +0000)]
removed coercions from status

19 years agoadded support for coercions
Enrico Tassi [Tue, 7 Jun 2005 16:41:18 +0000 (16:41 +0000)]
added support for coercions

19 years agoadded letin
Enrico Tassi [Tue, 7 Jun 2005 16:32:41 +0000 (16:32 +0000)]
added letin

19 years agoadded syntax for letin
Enrico Tassi [Tue, 7 Jun 2005 16:32:20 +0000 (16:32 +0000)]
added syntax for letin

19 years ago1) Implemented inference of the outtype for empty inductive types
Enrico Tassi [Tue, 7 Jun 2005 15:51:43 +0000 (15:51 +0000)]
1) Implemented inference of the outtype for empty inductive types
2) The inferred outtype (of non empty ind types) used to omit the lambda abstraction (worked using an amazing feature ot the type checker meant for backward compatibility with Coq 7... ask Claudio).

19 years agochanged match syntax:
Enrico Tassi [Tue, 7 Jun 2005 15:45:19 +0000 (15:45 +0000)]
changed match syntax:
match x in type ty_x with ...

19 years agoadded whd to match argument in guarded_by_destructors;
Enrico Tassi [Tue, 7 Jun 2005 15:44:16 +0000 (15:44 +0000)]
added whd to match argument in guarded_by_destructors;
before only verbatim occurrences of safe variables were accepted.

19 years agoadded Pp of Cast
Enrico Tassi [Tue, 7 Jun 2005 15:41:09 +0000 (15:41 +0000)]
added Pp of Cast

19 years agoadded integration entry
Stefano Zacchiroli [Tue, 7 Jun 2005 15:25:11 +0000 (15:25 +0000)]
added integration entry

19 years agosnapshort
Stefano Zacchiroli [Tue, 7 Jun 2005 15:18:20 +0000 (15:18 +0000)]
snapshort
- implemented magic instantiation 2 => 1
- implemented DEFAULT pattern matching compilation 2 => 1

19 years agocontrol of dependences improved
Ferruccio Guidi [Tue, 7 Jun 2005 10:02:35 +0000 (10:02 +0000)]
control of dependences improved

19 years ago*** empty log message ***
Alberto Griggio [Tue, 7 Jun 2005 07:53:30 +0000 (07:53 +0000)]
*** empty log message ***

19 years agoMy two pennies.
Andrea Asperti [Tue, 7 Jun 2005 06:44:39 +0000 (06:44 +0000)]
My two pennies.

19 years ago- set monospace buffer using modify_font widget method
Stefano Zacchiroli [Mon, 6 Jun 2005 09:36:04 +0000 (09:36 +0000)]
- set monospace buffer using modify_font widget method
- added configuration key for user defined font and built time default

19 years ago* update
Luca Padovani [Mon, 6 Jun 2005 08:29:01 +0000 (08:29 +0000)]
* update

19 years ago* more to do
Luca Padovani [Mon, 6 Jun 2005 08:06:26 +0000 (08:06 +0000)]
* more to do

19 years ago* added todo file
Luca Padovani [Sun, 5 Jun 2005 12:32:35 +0000 (12:32 +0000)]
* added todo file

19 years agosnapshot (first version with working pattern matching both 3->2 and 2->1)
Stefano Zacchiroli [Sat, 4 Jun 2005 17:23:42 +0000 (17:23 +0000)]
snapshot (first version with working pattern matching both 3->2 and 2->1)

yupppppieeeeeeeeeeeeeeeeee!
yayyyy

19 years agoa contribution about subset theory in an intuitionistic and predicative foundation
Ferruccio Guidi [Sat, 4 Jun 2005 15:12:01 +0000 (15:12 +0000)]
a contribution about subset theory in an intuitionistic and predicative foundation

19 years agosnapshot
Stefano Zacchiroli [Sat, 4 Jun 2005 14:34:18 +0000 (14:34 +0000)]
snapshot
- regression, but better (and working!) implementation of ML pattern matching
- not yet ported 3 -> 2 pattern matching

... the dunwich horror ...

19 years agocontribution about \lambda-\delta
Ferruccio Guidi [Fri, 3 Jun 2005 21:03:39 +0000 (21:03 +0000)]
contribution about \lambda-\delta

19 years agosnapshot (added typed environment in 2 -> 1 conversion)
Stefano Zacchiroli [Thu, 2 Jun 2005 19:56:57 +0000 (19:56 +0000)]
snapshot (added typed environment in 2 -> 1 conversion)
... in the eye of the meta-vortex ...
... from Ravenna city

19 years agosnapshot (first working implementation of parttern matching from level 2
Stefano Zacchiroli [Thu, 2 Jun 2005 15:23:49 +0000 (15:23 +0000)]
snapshot (first working implementation of parttern matching from level 2
to level 1)

19 years agofix_escaping
Enrico Tassi [Wed, 1 Jun 2005 14:40:03 +0000 (14:40 +0000)]
fix_escaping

19 years agoreduce with path
Enrico Tassi [Wed, 1 Jun 2005 14:34:55 +0000 (14:34 +0000)]
reduce with path

19 years agopaths trough terms implemented with a nice hack :)
Enrico Tassi [Wed, 1 Jun 2005 14:34:36 +0000 (14:34 +0000)]
paths trough terms implemented with a nice hack :)

19 years agosome cosmetic fixes
Enrico Tassi [Wed, 1 Jun 2005 11:08:38 +0000 (11:08 +0000)]
some cosmetic fixes

19 years agofix
Enrico Tassi [Wed, 1 Jun 2005 11:06:46 +0000 (11:06 +0000)]
fix