]> matita.cs.unibo.it Git - helm.git/log
helm.git
22 years agoAvoided some bugs of libxslt.
Claudio Sacerdoti Coen [Tue, 26 Feb 2002 10:28:15 +0000 (10:28 +0000)]
Avoided some bugs of libxslt.

22 years agoSome code factorization: towards a frame-free site.
Claudio Sacerdoti Coen [Mon, 25 Feb 2002 16:36:08 +0000 (16:36 +0000)]
Some code factorization: towards a frame-free site.

22 years agoIt was not XHTML valid.
Claudio Sacerdoti Coen [Mon, 25 Feb 2002 15:59:53 +0000 (15:59 +0000)]
It was not XHTML valid.

22 years agoGreat changes in all the stylesheets. Every page is now generated in two
Claudio Sacerdoti Coen [Mon, 25 Feb 2002 15:47:02 +0000 (15:47 +0000)]
Great changes in all the stylesheets. Every page is now generated in two
phases:

1) A stylesheet from XML to XHTML that generates the page.
   This stylesheet no more bothers with the layout of the page w.r.t. the
   rest of the site (i.e. it doesn't add the link to CSS; it doesn't call
   the head and foot templates)
2) A common stylesheet from XHTML to HTML that just adds the header, footer
   and CSS link to the page.

The idea is that in this way it is easier to change the overall layout of
the site (e.g. removing frames). Moreover, less code is required.

Problem: xsltproc is too intelligent (= rather stupid), so that it
recognises XHTML pages and fails in applying the stylesheet. So, in the
Makefile, care (= sed) must be taken to remove the DOCTYPE definitions
from XHTML files.

22 years ago* <I> ==> <em> everywhere
Claudio Sacerdoti Coen [Mon, 25 Feb 2002 14:31:17 +0000 (14:31 +0000)]
* <I> ==> <em> everywhere
* xml/Makefile added: typing make checks the validity of every .xml file in
  the xml directory
* every XML file now has a DTD. The files that are pure XHTML documents
  use the on-line XHTML 1.0 Transitional DTD.
* A new DTD mowgli-xhtml1-transitional.dtd added. It is an extension of
  the XHTML1 Transitional DTD to allow markup in the MOWGLI namespace.

22 years agoSome clean-up (unuseful sed removed from Makefile).
Claudio Sacerdoti Coen [Mon, 25 Feb 2002 10:42:44 +0000 (10:42 +0000)]
Some clean-up (unuseful sed removed from Makefile).

22 years agoMore cleanup: the home page is now generated by means of XSLT only.
Claudio Sacerdoti Coen [Sun, 24 Feb 2002 14:36:50 +0000 (14:36 +0000)]
More cleanup: the home page is now generated by means of XSLT only.
(i.e. no more cat ... >> $@)

22 years ago* Rendering of publications improved.
Claudio Sacerdoti Coen [Fri, 22 Feb 2002 18:23:32 +0000 (18:23 +0000)]
* Rendering of publications improved.
* Small typos fixed.
* Some clean-up.

22 years agoWarning changed.
Claudio Sacerdoti Coen [Fri, 22 Feb 2002 17:16:28 +0000 (17:16 +0000)]
Warning changed.

22 years agoNews updated.
Claudio Sacerdoti Coen [Fri, 22 Feb 2002 17:11:23 +0000 (17:11 +0000)]
News updated.

22 years ago* Notion of future and past events/deadlines introduced.
Claudio Sacerdoti Coen [Fri, 22 Feb 2002 16:59:20 +0000 (16:59 +0000)]
* Notion of future and past events/deadlines introduced.
* Approaching deadlines added to the front page. Should we keep them?
* The stylesheet mess done by Luca has been fixed (i.e. removed) ;-)

22 years agoA big commit:
Claudio Sacerdoti Coen [Fri, 22 Feb 2002 16:09:17 +0000 (16:09 +0000)]
A big commit:

1) A serious bug in deadline orderings has been fixed.
2) Events have been splitted (again) into MOWGLI Events and Other Events.
   Both of them have a menu entry.
3) The kick-off MOWGLI Event has been added.

22 years ago* "Older news" link added to the first page.
Claudio Sacerdoti Coen [Fri, 22 Feb 2002 14:16:20 +0000 (14:16 +0000)]
* "Older news" link added to the first page.
* Some more news and events.

22 years ago* Fax added.
Claudio Sacerdoti Coen [Fri, 22 Feb 2002 12:49:23 +0000 (12:49 +0000)]
* Fax added.
* Data for Theresa Velden updated.

22 years agoe-mail address fixed
Claudio Sacerdoti Coen [Fri, 22 Feb 2002 12:33:37 +0000 (12:33 +0000)]
e-mail address fixed

22 years agoMissing informations filled in.
Claudio Sacerdoti Coen [Thu, 21 Feb 2002 18:37:34 +0000 (18:37 +0000)]
Missing informations filled in.

22 years agoContract added to members area.
Claudio Sacerdoti Coen [Thu, 21 Feb 2002 17:40:16 +0000 (17:40 +0000)]
Contract added to members area.

22 years agoM.L. on-line archives are on-line!
Claudio Sacerdoti Coen [Wed, 20 Feb 2002 17:04:53 +0000 (17:04 +0000)]
M.L. on-line archives are on-line!

22 years agoWarning moved to a better position to re-balance the page.
Claudio Sacerdoti Coen [Wed, 20 Feb 2002 16:10:10 +0000 (16:10 +0000)]
Warning moved to a better position to re-balance the page.

22 years agored warning
Luca Padovani [Wed, 20 Feb 2002 15:54:01 +0000 (15:54 +0000)]
red warning

22 years agoThe list of persons in the "By Site" ordering is now also
Claudio Sacerdoti Coen [Tue, 19 Feb 2002 18:01:27 +0000 (18:01 +0000)]
The list of persons in the "By Site" ordering is now also
ordered by member status inside the site. Probably, some
more informations will be added soon (e.g. "site leader",
or "work-package leader" etc.)

22 years agoThe list of persons in alphabetical order is now in the form Surname, Name.
Claudio Sacerdoti Coen [Tue, 19 Feb 2002 17:43:06 +0000 (17:43 +0000)]
The list of persons in alphabetical order is now in the form Surname, Name.
The list ordered by site now also uses qualifications. But the output is
still not satisying to me because alphabetical order + qualifications is
quite bad. I will commit manually generated XML index files with a meaningful
order (from boss to slaves ;-)

22 years agoAdded File arch.gif, generated from .fig by Irene.
Claudio Sacerdoti Coen [Tue, 19 Feb 2002 17:37:03 +0000 (17:37 +0000)]
Added File arch.gif, generated from .fig by Irene.
The margins are not very tight: it will probably need to be redone.

22 years agoProject Objectives added.
Claudio Sacerdoti Coen [Tue, 19 Feb 2002 17:26:50 +0000 (17:26 +0000)]
Project Objectives added.

22 years ago- removed date from menu (useful?)
Luca Padovani [Tue, 19 Feb 2002 17:22:29 +0000 (17:22 +0000)]
- removed date from menu (useful?)
- added date on front page
- added warning for site under construction
- fixed deadline for extreme conference

22 years agomoved some xml files into xml root directory
Luca Padovani [Tue, 19 Feb 2002 16:52:12 +0000 (16:52 +0000)]
moved some xml files into xml root directory
fixed omdoc link from menu

22 years ago- renamed some files
Luca Padovani [Tue, 19 Feb 2002 16:43:01 +0000 (16:43 +0000)]
- renamed some files
- added links to the home page
- changed news on front page

22 years agoBroken links fixed somehow.
Claudio Sacerdoti Coen [Tue, 19 Feb 2002 15:53:11 +0000 (15:53 +0000)]
Broken links fixed somehow.
No more useful files (i.e. Nothing-yet files) removed.

22 years agochanged format of content file, now xhtml
Luca Padovani [Tue, 19 Feb 2002 00:49:02 +0000 (00:49 +0000)]
changed format of content file, now xhtml

22 years agook, here is the last one
Luca Padovani [Tue, 19 Feb 2002 00:24:52 +0000 (00:24 +0000)]
ok, here is the last one

22 years agoas usual forgot some files (mailing list, members' index)
Luca Padovani [Tue, 19 Feb 2002 00:24:25 +0000 (00:24 +0000)]
as usual forgot some files (mailing list, members' index)

22 years ago- added publication index
Luca Padovani [Tue, 19 Feb 2002 00:22:26 +0000 (00:22 +0000)]
- added publication index
- added software index
- added member area

22 years agoNothing yet pages added to fix broken links.
Claudio Sacerdoti Coen [Mon, 18 Feb 2002 19:00:23 +0000 (19:00 +0000)]
Nothing yet pages added to fix broken links.

22 years agoMembers area implemented.
Claudio Sacerdoti Coen [Mon, 18 Feb 2002 18:06:46 +0000 (18:06 +0000)]
Members area implemented.

22 years agohome.html.mid still around in the dependencies: removed
Luca Padovani [Mon, 18 Feb 2002 14:43:09 +0000 (14:43 +0000)]
home.html.mid still around in the dependencies: removed

22 years agoadded some stylesheets for list of people and sorting
Luca Padovani [Sat, 16 Feb 2002 02:24:54 +0000 (02:24 +0000)]
added some stylesheets for list of people and sorting

22 years ago- list of people
Luca Padovani [Sat, 16 Feb 2002 02:23:33 +0000 (02:23 +0000)]
- list of people
- fixes here and there

22 years agoEnglish errors fixed.
Claudio Sacerdoti Coen [Fri, 15 Feb 2002 14:57:17 +0000 (14:57 +0000)]
English errors fixed.

22 years agoEnglish error fixed.
Claudio Sacerdoti Coen [Fri, 15 Feb 2002 14:55:48 +0000 (14:55 +0000)]
English error fixed.

22 years agoMany improvements:
Claudio Sacerdoti Coen [Fri, 15 Feb 2002 14:37:10 +0000 (14:37 +0000)]
Many improvements:

1) a print_interval template has been put in common.xsl
2) events are now sorted by starting date
3) colors are used to differentiate between submissions, notifications,
   and so on. Is this an improvement? ;-|

22 years agoEhhm. Order ==> Sort ;-)
Claudio Sacerdoti Coen [Fri, 15 Feb 2002 13:46:29 +0000 (13:46 +0000)]
Ehhm. Order ==> Sort ;-)

22 years agoA new wonderful page that shows the deadlines ordered by date.
Claudio Sacerdoti Coen [Fri, 15 Feb 2002 13:44:09 +0000 (13:44 +0000)]
A new wonderful page that shows the deadlines ordered by date.
Moreover, I have added a new set of functions in commond.xsl
to pretty-print in English a date encoded as 20020218 (that is
easy to sort!).

22 years agoEvents added.
Claudio Sacerdoti Coen [Fri, 15 Feb 2002 11:47:30 +0000 (11:47 +0000)]
Events added.

22 years agoproject_summary.html added, but not linked yet.
Claudio Sacerdoti Coen [Fri, 15 Feb 2002 09:56:41 +0000 (09:56 +0000)]
project_summary.html added, but not linked yet.

22 years agotwo column layout. Better or worse?
Luca Padovani [Fri, 15 Feb 2002 01:19:50 +0000 (01:19 +0000)]
two column layout. Better or worse?

22 years ago- main page now generated automatically
Luca Padovani [Thu, 14 Feb 2002 21:55:02 +0000 (21:55 +0000)]
- main page now generated automatically
- latest news included in main page
- improved layout
- changed colours
- fix for IE (dismissed blockquote everywhere)

22 years agoRendering of links to composite sites (i.e. aei) is now OK.
Claudio Sacerdoti Coen [Thu, 14 Feb 2002 18:50:46 +0000 (18:50 +0000)]
Rendering of links to composite sites (i.e. aei) is now OK.

22 years agoFixed broken links to IST images.
Claudio Sacerdoti Coen [Thu, 14 Feb 2002 17:19:57 +0000 (17:19 +0000)]
Fixed broken links to IST images.

22 years ago----------------------------------------------------------------------
Irene Schena [Thu, 14 Feb 2002 15:19:13 +0000 (15:19 +0000)]
----------------------------------------------------------------------
Added Files:
project_summary.html: chapter 1 MOWGLI proposal
----------------------------------------------------------------------

22 years agoOMDoc link fixed.
Claudio Sacerdoti Coen [Thu, 14 Feb 2002 10:07:18 +0000 (10:07 +0000)]
OMDoc link fixed.

22 years agoas usual...
Luca Padovani [Wed, 13 Feb 2002 20:01:44 +0000 (20:01 +0000)]
as usual...

22 years agopartial implementation of IST logo. Deep pages have the wrong reference
Luca Padovani [Wed, 13 Feb 2002 20:00:53 +0000 (20:00 +0000)]
partial implementation of IST logo. Deep pages have the wrong reference

22 years ago- install/uninstall targets added
Luca Padovani [Wed, 13 Feb 2002 19:17:44 +0000 (19:17 +0000)]
- install/uninstall targets added
- link to personal page now with target="_top"

22 years agoMore information added.
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 18:42:40 +0000 (18:42 +0000)]
More information added.

22 years agoProject Management template added.
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 18:33:52 +0000 (18:33 +0000)]
Project Management template added.
Not integrated in the site yet.
Maybe it will become a bunch of XML files once the management groups
will be formed (i.e. during the kick-off).

22 years agoBug fixed: the top directory has a different (relative) path depending on
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 17:58:16 +0000 (17:58 +0000)]
Bug fixed: the top directory has a different (relative) path depending on
the file directory.

22 years agoQualification now always used before name and surname.
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 17:49:10 +0000 (17:49 +0000)]
Qualification now always used before name and surname.

22 years agoMore uniform layout.
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 17:44:13 +0000 (17:44 +0000)]
More uniform layout.

22 years agoDeliverables are now described in XML.
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 17:21:24 +0000 (17:21 +0000)]
Deliverables are now described in XML.
The information comes from the table in Sect. 9.4 of the proposal.
Should we try to reproduce that table or is it uninteresting?

22 years ago- more uniform layout
Luca Padovani [Wed, 13 Feb 2002 17:18:09 +0000 (17:18 +0000)]
- more uniform layout
- a few fixes

22 years agoAnother part of the proposal encoded.
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 16:25:04 +0000 (16:25 +0000)]
Another part of the proposal encoded.

22 years agoDeliverables added.
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 15:55:21 +0000 (15:55 +0000)]
Deliverables added.
The idea is that for every deliverable we have an XML file.
When we write a deliverable, we encode it in XML in the same page,
we detect this in XSLT and we create the hyperlink to another page
that renders it.

22 years agoWork-packages DTD improved (tasks now have an identifier and a name).
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 14:20:35 +0000 (14:20 +0000)]
Work-packages DTD improved (tasks now have an identifier and a name).
Better rendering of the work-packages index (the tasks are shown).

22 years agoDTD improved (and committed) with new elements "task" and "tasks".
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 13:55:55 +0000 (13:55 +0000)]
DTD improved (and committed) with new elements "task" and "tasks".

22 years agoOrdered list (ol) replaced by a table to be able to number packages
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 12:20:17 +0000 (12:20 +0000)]
Ordered list (ol) replaced by a table to be able to number packages
starting from 0. ;-(

22 years agoThe Work-Packages index page is no more a static HTML page, but it is
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 12:07:15 +0000 (12:07 +0000)]
The Work-Packages index page is no more a static HTML page, but it is
automatically generated from xml/work-packages/index.xml (that will be
also useful in the future).

22 years agoHyperlink to the author's MOWLI home page added.
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 11:29:54 +0000 (11:29 +0000)]
Hyperlink to the author's MOWLI home page added.

22 years agoWrong cut & paste from Herbelin's data.
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 11:29:39 +0000 (11:29 +0000)]
Wrong cut & paste from Herbelin's data.

22 years ago* news.xml was not valid. DTD fixed.
Claudio Sacerdoti Coen [Wed, 13 Feb 2002 11:27:47 +0000 (11:27 +0000)]
* news.xml was not valid. DTD fixed.
* DTD Improved: who is now a pointer to the author's MOWGLI home page.

22 years ago*** empty log message ***
Luca Padovani [Wed, 13 Feb 2002 02:35:22 +0000 (02:35 +0000)]
*** empty log message ***

22 years ago- added common stylesheet
Luca Padovani [Wed, 13 Feb 2002 02:34:44 +0000 (02:34 +0000)]
- added common stylesheet
- preliminary support for news
- modified menu
- simplified makefile

22 years ago.cvsignore added where useful
Claudio Sacerdoti Coen [Tue, 12 Feb 2002 18:22:04 +0000 (18:22 +0000)]
.cvsignore added where useful

22 years agoInitial commit of the XML/XSLT stuff.
Claudio Sacerdoti Coen [Tue, 12 Feb 2002 18:11:02 +0000 (18:11 +0000)]
Initial commit of the XML/XSLT stuff.
The generated HTML files are not integrated with the rest of the site, yet.

22 years agothis is the first commit for the mowgli website.
Luca Padovani [Mon, 11 Feb 2002 17:49:44 +0000 (17:49 +0000)]
this is the first commit for the mowgli website.
The structure is temporary, as are all the files in there now.

22 years agoFirst commit toward 0.3.0.
Claudio Sacerdoti Coen [Wed, 6 Feb 2002 15:06:33 +0000 (15:06 +0000)]
First commit toward 0.3.0.
Instead of minidom, gdome and gmetadom are now used.

22 years agoUntil Garrigue puts a META file in lablgtk, we can use this one.
Claudio Sacerdoti Coen [Wed, 6 Feb 2002 14:52:29 +0000 (14:52 +0000)]
Until Garrigue puts a META file in lablgtk, we can use this one.

22 years agoDue to a syntax error, theories in MathML Presentation were broken.
Claudio Sacerdoti Coen [Tue, 5 Feb 2002 15:03:34 +0000 (15:03 +0000)]
Due to a syntax error, theories in MathML Presentation were broken.

22 years agoporting to gdome2 started
Luca Padovani [Tue, 5 Feb 2002 02:44:56 +0000 (02:44 +0000)]
porting to gdome2 started

22 years ago----------------------------------------------------------------------
Irene Schena [Fri, 1 Feb 2002 17:08:31 +0000 (17:08 +0000)]
----------------------------------------------------------------------
Modified Files:
1) arith.xsl mmlctop.xsl-0.14 mmlextension.xsl xslt_index.txt: added
mml presentation for (dis)equalities and new proof elements and some
additions for Algebra elements
Added Files:
2) mmlnotation.xsl: mml presentation notations
----------------------------------------------------------------------

22 years agoPorted to ocaml-3.04
Claudio Sacerdoti Coen [Tue, 29 Jan 2002 14:55:44 +0000 (14:55 +0000)]
Ported to ocaml-3.04

22 years agoPorted to ocaml-3.04.
Claudio Sacerdoti Coen [Tue, 29 Jan 2002 14:44:29 +0000 (14:44 +0000)]
Ported to ocaml-3.04.

22 years agoBug fix: destdir for mlminidom installation is now guessed by
Stefano Zacchiroli [Mon, 21 Jan 2002 14:36:53 +0000 (14:36 +0000)]
Bug fix: destdir for mlminidom installation is now guessed by
configure

22 years ago- Vanity: added .... me to the copyright file as author :-P
Stefano Zacchiroli [Sun, 20 Jan 2002 15:24:22 +0000 (15:24 +0000)]
- Vanity: added  .... me to the copyright file as author :-P

22 years ago- Minor fix: includes upstream changelog only if it have size
Stefano Zacchiroli [Sun, 20 Jan 2002 15:23:52 +0000 (15:23 +0000)]
- Minor fix: includes upstream changelog only if it have size
  greater than zero.

22 years agoAdded "-destdir" argument to "ocamlfind install" in "install:"
Stefano Zacchiroli [Sun, 20 Jan 2002 14:46:32 +0000 (14:46 +0000)]
Added "-destdir" argument to "ocamlfind install" in "install:"
target of Makefile.in, ease creation of debian package and non
standard installation.

22 years agoPorted to ocaml 3.04 (fixed problems with commuting label mode).
Stefano Zacchiroli [Sun, 20 Jan 2002 14:45:07 +0000 (14:45 +0000)]
Ported to ocaml 3.04 (fixed problems with commuting label mode).

22 years agoUpgraded debian package for mlminidom 0.2.2
Stefano Zacchiroli [Sun, 20 Jan 2002 14:41:51 +0000 (14:41 +0000)]
Upgraded debian package for mlminidom 0.2.2

22 years agoThere were a big bug in both Fix and CoFix: the recursive functions were
Claudio Sacerdoti Coen [Fri, 11 Jan 2002 18:25:37 +0000 (18:25 +0000)]
There were a big bug in both Fix and CoFix: the recursive functions were
not bounded in the bodies.

Fix and CoFix syntax changed to a less natural, but easier to parse one.
The above bug has been fixed.

22 years agoCIC Textual Parser added to the repository.
Claudio Sacerdoti Coen [Thu, 10 Jan 2002 16:52:05 +0000 (16:52 +0000)]
CIC Textual Parser added to the repository.
The Makefile stuff has been modified because of ocamllex and ocamlyacc rules.

22 years ago----------------------------------------------------------------------
Irene Schena [Fri, 21 Dec 2001 16:47:13 +0000 (16:47 +0000)]
----------------------------------------------------------------------
Modified Files:
1) schema-h.rdf schema-hth.rdf: bugs fixed
----------------------------------------------------------------------

22 years ago----------------------------------------------------------------------
Irene Schena [Thu, 13 Dec 2001 16:11:54 +0000 (16:11 +0000)]
----------------------------------------------------------------------
Modified Files:
1) schema-h.rdf schema-hth.rdf: added comments
Added Files:
1) 13-dcagent 21-euler dces dcq dctype eor: euler and dublin core schemas
----------------------------------------------------------------------

22 years agoGeneration of forward metadata using a lexical analyser.
Claudio Sacerdoti Coen [Thu, 13 Dec 2001 14:21:33 +0000 (14:21 +0000)]
Generation of forward metadata using a lexical analyser.

22 years agoThe hash-table used in the implementation was of "type"
Claudio Sacerdoti Coen [Thu, 13 Dec 2001 12:09:17 +0000 (12:09 +0000)]
The hash-table used in the implementation was of "type"
(UriManager.uri * int) -> Cic.obj

Is is now of type
UriManager.uri -> (int * Cic.obj) list

where the list is ordered from the most cooked to the less cooked.

There is almost no difference at all in the performance of big files
(limit_plus). The new design is easier to extend to a real cache with
rollback.

22 years agoNew architecture for the environment.
Claudio Sacerdoti Coen [Thu, 13 Dec 2001 10:09:45 +0000 (10:09 +0000)]
New architecture for the environment.
The final goal is to have a reentrant, session-aware environment that
also behaves as a true cache.

22 years agoFixing of guarded_by_constructors completed.
Claudio Sacerdoti Coen [Wed, 12 Dec 2001 18:43:17 +0000 (18:43 +0000)]
Fixing of guarded_by_constructors completed.
This is the idea of the implementation:
1) The guarded_by_constructors is called on a term which is going to produce
   an inductive type (in every branch).
2) The guarded_by_constructors now has also a parameter which is the list
   of arguments that are applied to the inductive type that the term
   we are cheking is going to produce.
3) Once the constructor is found, its type is "applied" to the list of
   arguments its inductive type is applied to. This operation gives us
   an instantiated constructor type.
4) Depending on the type of every argument in the instantiated constructor
   type, we call either the does_not_occur or the guarded_by_constructors
   on every term the constructor is applied to. In case we call the
   guarded_by_constructors, we also compute the new parameter (list of
   arguments the new inductive type was applied to).

Note that the analysis of the type of the constructors is based very closely
on the analysis of positivy of an inductive type.

Note also that some cases (e.g. a MutCase, a Fix or a CoFix in head position
in the backbone of the type of a constructor) has not been considered and
raises an exception.

22 years agoPARTIAL COMMIT:
Claudio Sacerdoti Coen [Tue, 11 Dec 2001 14:21:33 +0000 (14:21 +0000)]
PARTIAL COMMIT:
 The whole logic of the guarded_by_constructors is being changed.
 The new idea is this one:
  1) The guarded_by_constructors is applied to a term t which must always
     generate an inhabitant of an inductive data type or of a co-inductive
     data type.
  2) When it find a constructor in head position, then the constructor
     must construct the inductive or co-inductive data type of 1).
  3) The type of the formal parameter of a constructor determines what
     condition is checked on the actual parameters of the constructors:
     a) Not recursive: the function must not occur in the actual parameter
     b) Simply recursive (to be defined): the function must occur in the
        actual parameter only guarded by constructors (where the constructor
        has already been found).
     c) Imbricated (i.e. it is another inductive type applied to the one
        that is going to be recursively defined): in this case the guarded
        by constructors (where the constructor has already been found) must
        be called, but:
         I) the expected inductive data type is no more the old one, but
            the one of the inductive data type that is in head position in
            the type.
        II) Once (if) one constructor of I) will be found, its type must
            be considered only after the substitution of the left (?)
            parameters and considering recursion IN THE CO-INDUCTIVE TYPE
            THAT IS THE OUTPUT TYPE OF THE WHOLE COFIX.

What is still wrong with this commit is that we don't have the notion of
imbricated argument yet. So, as soon as an imbricated argument is found,
the invariant 1-3 are broken and sooner or later an exception is raised
or false is returned.

22 years ago----------------------------------------------------------------------
Irene Schena [Mon, 10 Dec 2001 16:28:04 +0000 (16:28 +0000)]
----------------------------------------------------------------------
Modified Files:
1) schema-h.rdf, schema-hth.rdf: updated DC schemas + class and
property refinements + value types.
----------------------------------------------------------------------

22 years agoBug fixed: the strictly_positive condition was unnecessarily too tight.
Claudio Sacerdoti Coen [Mon, 10 Dec 2001 12:00:39 +0000 (12:00 +0000)]
Bug fixed: the strictly_positive condition was unnecessarily too tight.

22 years agoThe typing rule for LetIn was simply wrong. Fixed.
Claudio Sacerdoti Coen [Fri, 7 Dec 2001 17:08:07 +0000 (17:08 +0000)]
The typing rule for LetIn was simply wrong. Fixed.

22 years agoBug partially fixed: the branch of a case of type Prod can be not a Lambda.
Claudio Sacerdoti Coen [Fri, 7 Dec 2001 15:34:41 +0000 (15:34 +0000)]
Bug partially fixed: the branch of a case of type Prod can be not a Lambda.
(e.g. a Rel, a MutConstruct, etc.) I have fixed only the two cases of a
Rel and a MutConstruct.