]>
matita.cs.unibo.it Git - helm.git/log
Enrico Tassi [Fri, 19 Dec 2008 10:36:00 +0000 (10:36 +0000)]
added aliases for _ and fixed greek leters thanks to wilmer
Enrico Tassi [Fri, 19 Dec 2008 10:12:15 +0000 (10:12 +0000)]
better pps
Enrico Tassi [Fri, 19 Dec 2008 10:11:39 +0000 (10:11 +0000)]
handles bad Appl
Enrico Tassi [Fri, 19 Dec 2008 10:11:14 +0000 (10:11 +0000)]
added better debug_pps and add_user_provided_unification_hint
Enrico Tassi [Fri, 19 Dec 2008 10:10:18 +0000 (10:10 +0000)]
...
Enrico Tassi [Fri, 19 Dec 2008 10:09:53 +0000 (10:09 +0000)]
added unification hint
Enrico Tassi [Fri, 19 Dec 2008 10:07:15 +0000 (10:07 +0000)]
unification hint
Enrico Tassi [Fri, 19 Dec 2008 10:06:31 +0000 (10:06 +0000)]
lambda case fixed, used to not properly use the expected type if it was not a Prod
Enrico Tassi [Fri, 19 Dec 2008 10:05:31 +0000 (10:05 +0000)]
added 'unification hint command to add a term to the new unification hint database'
Enrico Tassi [Fri, 19 Dec 2008 10:02:11 +0000 (10:02 +0000)]
identity coercions are not really inserted, just used as hints for unification
Enrico Tassi [Fri, 19 Dec 2008 09:59:54 +0000 (09:59 +0000)]
....
Claudio Sacerdoti Coen [Thu, 18 Dec 2008 20:44:31 +0000 (20:44 +0000)]
Stupid bug fixed: checkin the type in place of the sort during the refinement
of axioms.
Claudio Sacerdoti Coen [Thu, 18 Dec 2008 20:41:30 +0000 (20:41 +0000)]
New disambiguation commented out.
Claudio Sacerdoti Coen [Thu, 18 Dec 2008 20:35:07 +0000 (20:35 +0000)]
Many axioms are now proved... using many more (but simpler) axioms.
Claudio Sacerdoti Coen [Thu, 18 Dec 2008 20:32:15 +0000 (20:32 +0000)]
Now it compiles again.
Claudio Sacerdoti Coen [Thu, 18 Dec 2008 20:29:33 +0000 (20:29 +0000)]
Refinement of axioms fixed. We did not check that the declared type must be
a type.
Ferruccio Guidi [Thu, 18 Dec 2008 15:48:01 +0000 (15:48 +0000)]
- improved logging
- we started to support the coercion for "non"
Enrico Tassi [Thu, 18 Dec 2008 13:56:15 +0000 (13:56 +0000)]
...
Ferruccio Guidi [Wed, 17 Dec 2008 19:49:35 +0000 (19:49 +0000)]
we started the support for the coercions "alle" and "alli"
Enrico Tassi [Wed, 17 Dec 2008 17:52:18 +0000 (17:52 +0000)]
foo overlap
Enrico Tassi [Wed, 17 Dec 2008 17:35:00 +0000 (17:35 +0000)]
foo overlap
Enrico Tassi [Wed, 17 Dec 2008 15:20:44 +0000 (15:20 +0000)]
....
Ferruccio Guidi [Tue, 16 Dec 2008 19:32:12 +0000 (19:32 +0000)]
we added the implicit coercion for modus tollens
Enrico Tassi [Tue, 16 Dec 2008 19:14:01 +0000 (19:14 +0000)]
previous change was causing divergence
Enrico Tassi [Tue, 16 Dec 2008 19:13:46 +0000 (19:13 +0000)]
hints work better now
Enrico Tassi [Tue, 16 Dec 2008 13:58:09 +0000 (13:58 +0000)]
hints attached
Enrico Tassi [Tue, 16 Dec 2008 13:57:22 +0000 (13:57 +0000)]
removed debug code
Enrico Tassi [Tue, 16 Dec 2008 13:54:37 +0000 (13:54 +0000)]
fixed a bug, it used to report o wrong is_normal bit in case of match
Enrico Tassi [Tue, 16 Dec 2008 13:53:16 +0000 (13:53 +0000)]
make it compile again
Enrico Tassi [Tue, 16 Dec 2008 13:53:03 +0000 (13:53 +0000)]
wrap object_not_found
Enrico Tassi [Tue, 16 Dec 2008 13:50:55 +0000 (13:50 +0000)]
move the printing in the right place
Enrico Tassi [Tue, 16 Dec 2008 09:00:31 +0000 (09:00 +0000)]
auto expansion of \tex macros added as a switch in the edit menu
Enrico Tassi [Tue, 16 Dec 2008 09:00:17 +0000 (09:00 +0000)]
added one asser
Enrico Tassi [Mon, 15 Dec 2008 22:55:17 +0000 (22:55 +0000)]
dep.opt regenerated
Enrico Tassi [Mon, 15 Dec 2008 22:49:47 +0000 (22:49 +0000)]
added unification hints
Wilmer Ricciotti [Mon, 15 Dec 2008 19:20:08 +0000 (19:20 +0000)]
Some changes to the pullback test, for debugging
Wilmer Ricciotti [Mon, 15 Dec 2008 19:16:46 +0000 (19:16 +0000)]
First attempt to implement unification hints.
Enrico Tassi [Mon, 15 Dec 2008 13:50:17 +0000 (13:50 +0000)]
use named types to force some constraints asap
Enrico Tassi [Mon, 15 Dec 2008 13:26:26 +0000 (13:26 +0000)]
To check if a term is type, do a whd of its sort before matching it.
Enrico Tassi [Mon, 15 Dec 2008 13:13:33 +0000 (13:13 +0000)]
...
Enrico Tassi [Mon, 15 Dec 2008 13:12:28 +0000 (13:12 +0000)]
aded some whd, you should be able to declare something like:
inductive A : FOO :=
where FOO is defined as a sort (or unfolds to somthing ending with a sort)
Claudio Sacerdoti Coen [Sun, 14 Dec 2008 23:03:02 +0000 (23:03 +0000)]
The library is no longer automatically used during disambiguation.
It is used only when the user press the More button or when he selects
the library from the Debug (?????) menu!
Moreover, using the library or not using it has now a different behaviour:
1. when the library is NOT used, symbols with no preferences are no
longer automatically looked for in the library
2. when the library IS used, only passes 5 and 6 are tried.
CONS:
1. the Debug menu voice is now necessary: move it elsewhere? always open the
disambiguation window making it non-modal? put an hyperlink in the error
message window?
2. when the library is used, all previous preferences are completely ignored
for all symbols. This makes the system much more stupid than what it used
to be.
PROS:
disambiguation is now much faster in case of error
Ferruccio Guidi [Sun, 14 Dec 2008 22:22:38 +0000 (22:22 +0000)]
- improved logging
- optimization in subst
Ferruccio Guidi [Sun, 14 Dec 2008 19:34:19 +0000 (19:34 +0000)]
new kernel basic_ag (with absolute local references)
Ferruccio Guidi [Sun, 14 Dec 2008 15:32:38 +0000 (15:32 +0000)]
we are changing the kernel version from basic_rg to basic_ag
Ferruccio Guidi [Sun, 14 Dec 2008 15:23:54 +0000 (15:23 +0000)]
autItem : the uris of the objects involved in the implicit coercions
log : improved log output
basic_rg: improved logging
Enrico Tassi [Sun, 14 Dec 2008 11:37:50 +0000 (11:37 +0000)]
...
Enrico Tassi [Sun, 14 Dec 2008 11:36:02 +0000 (11:36 +0000)]
eureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg fd => c ] is
now correctly broken if too long
Enrico Tassi [Sun, 14 Dec 2008 10:56:38 +0000 (10:56 +0000)]
...
Ferruccio Guidi [Fri, 12 Dec 2008 21:26:57 +0000 (21:26 +0000)]
improved type hierarchy management
Claudio Sacerdoti Coen [Fri, 12 Dec 2008 14:59:39 +0000 (14:59 +0000)]
...
Claudio Sacerdoti Coen [Fri, 12 Dec 2008 14:41:18 +0000 (14:41 +0000)]
A parser (and a scanner) to import "~C" files into Matita.
Claudio Sacerdoti Coen [Fri, 12 Dec 2008 14:32:56 +0000 (14:32 +0000)]
...
Claudio Sacerdoti Coen [Fri, 12 Dec 2008 14:32:23 +0000 (14:32 +0000)]
1. new expressions AND, OR, XOR
2. constants must be initialized
3. bug fixed: the size n of an array means that the array
has (n+1) elements. Thus the last valid index is n.
Ferruccio Guidi [Fri, 12 Dec 2008 12:45:42 +0000 (12:45 +0000)]
- basic_rg: architectural bug fix
- toplevel: more help on command line options
Enrico Tassi [Fri, 12 Dec 2008 12:14:31 +0000 (12:14 +0000)]
...
Enrico Tassi [Fri, 12 Dec 2008 12:11:54 +0000 (12:11 +0000)]
added some hardcoded universes, needed to typecheck the librarya
Enrico Tassi [Fri, 12 Dec 2008 12:11:12 +0000 (12:11 +0000)]
added some messages
Enrico Tassi [Fri, 12 Dec 2008 12:10:40 +0000 (12:10 +0000)]
added empty_db, usefull to avoid translating all old coercions to obtain a new coercions database
Enrico Tassi [Fri, 12 Dec 2008 12:09:25 +0000 (12:09 +0000)]
use new function to clear caches so that objects are translated correctly
Enrico Tassi [Fri, 12 Dec 2008 12:08:16 +0000 (12:08 +0000)]
better error message, functions to clear various caches used during translation of old2new cic, logger functions implemented inside the typechecker so that
uncommenting one line makes the type checker more verbose when recursively typing stuff
Enrico Tassi [Fri, 12 Dec 2008 11:59:32 +0000 (11:59 +0000)]
thanks to the new fixes to notation, I can define \land for both pairs and
families!
Enrico Tassi [Fri, 12 Dec 2008 11:43:39 +0000 (11:43 +0000)]
pattern matching over Ast.Case simplified:
- it is not possible to match the `in intype` foo part
- it is not possible to match the outtype
eta expansion still done on Ast (hard to do it in Cic. The abstracted variable
does not have a type :-( thus you may have to double your notations. Name for fresh variables changed to \etaX instead of freshX (much shorter in terms of screen pixels)
Claudio Sacerdoti Coen [Thu, 11 Dec 2008 22:39:49 +0000 (22:39 +0000)]
Applications are now processed from left to right.
Enrico Tassi [Thu, 11 Dec 2008 14:16:47 +0000 (14:16 +0000)]
support for mathml mpadded tag added (allows to overlap two subsequent symbols); you library needs to be recompiled after the update
Ferruccio Guidi [Wed, 10 Dec 2008 21:25:21 +0000 (21:25 +0000)]
- new semantic log system
- new brg terms
- bug fix im MetaOutput and MetaBrg
Ferruccio Guidi [Tue, 9 Dec 2008 19:26:31 +0000 (19:26 +0000)]
first version of kernel "basic_rg"
the grundlagen does not typecheck because some of its lambdas are actually pis
(this is known)
Enrico Tassi [Tue, 9 Dec 2008 18:30:47 +0000 (18:30 +0000)]
new disambiguatio attached with the right universe graph
Enrico Tassi [Tue, 9 Dec 2008 18:29:37 +0000 (18:29 +0000)]
raise uncertain when a sort is not a sort but may be, use max for mixing universes, coercions to sort in the prod case are triggered before putting the source type in the context
Enrico Tassi [Tue, 9 Dec 2008 18:27:31 +0000 (18:27 +0000)]
better coercions indexing and lookup
Enrico Tassi [Tue, 9 Dec 2008 18:26:18 +0000 (18:26 +0000)]
better max function (instead of @) for combining universes
Enrico Tassi [Tue, 9 Dec 2008 18:25:04 +0000 (18:25 +0000)]
added an exception
Enrico Tassi [Tue, 9 Dec 2008 16:04:20 +0000 (16:04 +0000)]
saturate was not returning the correct (saturated) type (but a correct number
of arguments.
Enrico Tassi [Tue, 9 Dec 2008 12:18:42 +0000 (12:18 +0000)]
fixed notation
Enrico Tassi [Tue, 9 Dec 2008 09:02:08 +0000 (09:02 +0000)]
...
Enrico Tassi [Tue, 9 Dec 2008 08:57:39 +0000 (08:57 +0000)]
option to collapse all tex macros implemented
Claudio Sacerdoti Coen [Mon, 8 Dec 2008 23:56:26 +0000 (23:56 +0000)]
A (boring and long) once-in-a-life exercise on proving a trivial property
on natural numbers in ND.
Enrico Tassi [Mon, 8 Dec 2008 17:07:45 +0000 (17:07 +0000)]
non active but almost working implementation of \TeX macro substitution while colouring
Enrico Tassi [Mon, 8 Dec 2008 14:02:53 +0000 (14:02 +0000)]
alt-l for not working nymore for \fox where x was in an eq class
Enrico Tassi [Mon, 8 Dec 2008 12:50:12 +0000 (12:50 +0000)]
...
Enrico Tassi [Mon, 8 Dec 2008 09:34:40 +0000 (09:34 +0000)]
better replacement for \\def
Enrico Tassi [Mon, 8 Dec 2008 00:39:33 +0000 (00:39 +0000)]
3.5 -> 35 to help crappy latex
Claudio Sacerdoti Coen [Sun, 7 Dec 2008 19:05:29 +0000 (19:05 +0000)]
New exception considered.
Claudio Sacerdoti Coen [Sun, 7 Dec 2008 18:57:15 +0000 (18:57 +0000)]
Bug fixed: every time we form a Prod, we must typecheck it before trying
unification.
Enrico Tassi [Sun, 7 Dec 2008 18:05:18 +0000 (18:05 +0000)]
better images
Enrico Tassi [Sat, 6 Dec 2008 18:12:03 +0000 (18:12 +0000)]
new concept of virtuals, defined only in the gui that behave as the old (still
present and used) ut8tables and ligatures mapping \foo or => to unicode symbols.
support in the gui for utomatical sumstitution of a virtual with its utf8
counterpart (disabled now, grep for if false && str = " ").
support for uf8 equivalnce classes, names simalrsymbols, activated by alt-l.
alt-l is now overloaded, can expand a \foo or => to a unicode symbol
and cycle on unicode symbols in the same eq class of the one just before the
cursor.
classes are already defined for letters mapping them to variants (other
alfabets and fonts) and on arrows and <.
Ferruccio Guidi [Sat, 6 Dec 2008 14:42:09 +0000 (14:42 +0000)]
metaAut: now we use hash tables properly (processing time: 2s)
brgReduction: started
Claudio Sacerdoti Coen [Fri, 5 Dec 2008 23:27:42 +0000 (23:27 +0000)]
new exception captured
Claudio Sacerdoti Coen [Fri, 5 Dec 2008 23:12:39 +0000 (23:12 +0000)]
Added new syntax Type[n] where n is a number.
The old kernel interpretes it simply as Type.
The new kernel as Typen.
Claudio Sacerdoti Coen [Fri, 5 Dec 2008 23:03:13 +0000 (23:03 +0000)]
Debugging code removed.
Claudio Sacerdoti Coen [Fri, 5 Dec 2008 23:02:44 +0000 (23:02 +0000)]
Debugging code removed
Claudio Sacerdoti Coen [Fri, 5 Dec 2008 23:02:10 +0000 (23:02 +0000)]
Debugging instructions removed.
Claudio Sacerdoti Coen [Fri, 5 Dec 2008 21:58:39 +0000 (21:58 +0000)]
Useless code removed.
Claudio Sacerdoti Coen [Fri, 5 Dec 2008 21:42:51 +0000 (21:42 +0000)]
Useless code removed.
Claudio Sacerdoti Coen [Fri, 5 Dec 2008 21:35:37 +0000 (21:35 +0000)]
Useless code removed.
Claudio Sacerdoti Coen [Fri, 5 Dec 2008 20:34:51 +0000 (20:34 +0000)]
Case-sensitive fixes.
Enrico Tassi [Fri, 5 Dec 2008 18:16:01 +0000 (18:16 +0000)]
a few missing ~subst added to whd
Enrico Tassi [Fri, 5 Dec 2008 18:10:04 +0000 (18:10 +0000)]
coercions are there, but not heavily tested
Enrico Tassi [Fri, 5 Dec 2008 18:07:54 +0000 (18:07 +0000)]
if todo_dom was [] disambiguation was performed twice
Enrico Tassi [Fri, 5 Dec 2008 11:29:39 +0000 (11:29 +0000)]
still commented, but benchmarks the new/old disambigution process