]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agoenriched error message
Stefano Zacchiroli [Tue, 1 Feb 2005 17:55:29 +0000 (17:55 +0000)]
enriched error message

19 years agoadded strip_xpointer: remove trailing #xpointer from a UriManager.uri value
Stefano Zacchiroli [Tue, 1 Feb 2005 17:54:49 +0000 (17:54 +0000)]
added strip_xpointer: remove trailing #xpointer from a UriManager.uri value

19 years agoreverder change. no more owner passed to the locate.
Enrico Tassi [Tue, 1 Feb 2005 15:40:15 +0000 (15:40 +0000)]
reverder change. no more owner passed to the locate.

19 years agoadded owner support to the disambiguator (now locate finds only objects
Enrico Tassi [Tue, 1 Feb 2005 15:21:20 +0000 (15:21 +0000)]
added owner support to the disambiguator (now locate finds only objects
of the current owner).

19 years ago*** empty log message ***
Enrico Tassi [Tue, 1 Feb 2005 13:47:00 +0000 (13:47 +0000)]
*** empty log message ***

19 years agoadded `Coer print_kind
Enrico Tassi [Tue, 1 Feb 2005 13:45:36 +0000 (13:45 +0000)]
added `Coer print_kind

19 years agoAdded Coer/Coercions print_kind
Enrico Tassi [Tue, 1 Feb 2005 13:45:05 +0000 (13:45 +0000)]
Added Coer/Coercions print_kind

19 years agoMetadataDB.clean now cleans the getter maps (calling Http_getter.unregister)
Enrico Tassi [Tue, 1 Feb 2005 13:44:27 +0000 (13:44 +0000)]
MetadataDB.clean now cleans the getter maps (calling Http_getter.unregister)
from the uris that deletes from the DB

19 years agofix in the coercions list generation and aded a function to know the
Enrico Tassi [Tue, 1 Feb 2005 13:42:35 +0000 (13:42 +0000)]
fix in the coercions list generation and aded a function to know the
known coercions

19 years agoadded the unregister method to the help page
Enrico Tassi [Tue, 1 Feb 2005 11:46:31 +0000 (11:46 +0000)]
added the unregister method to the help page

19 years agofixed coercions
Enrico Tassi [Tue, 1 Feb 2005 10:42:18 +0000 (10:42 +0000)]
fixed coercions

19 years agoremoved debug print
Enrico Tassi [Tue, 1 Feb 2005 10:05:52 +0000 (10:05 +0000)]
removed debug print

19 years agocosmetic fix to pp_location
Enrico Tassi [Tue, 1 Feb 2005 10:05:14 +0000 (10:05 +0000)]
cosmetic fix to pp_location

19 years agoadded save_object_to_disk and basedir
Enrico Tassi [Mon, 31 Jan 2005 17:29:03 +0000 (17:29 +0000)]
added save_object_to_disk and basedir

19 years agoadded delift
Enrico Tassi [Mon, 31 Jan 2005 17:18:55 +0000 (17:18 +0000)]
added delift

19 years agoadded basedir and improved let{rec} syntax
Enrico Tassi [Mon, 31 Jan 2005 17:17:32 +0000 (17:17 +0000)]
added basedir and improved let{rec} syntax

19 years agobetter debug prints
Enrico Tassi [Mon, 31 Jan 2005 17:16:41 +0000 (17:16 +0000)]
better debug prints

19 years agoadded Basedir Ast
Enrico Tassi [Mon, 31 Jan 2005 17:12:12 +0000 (17:12 +0000)]
added Basedir Ast

19 years agoAdded outtype inference to MutCase
Enrico Tassi [Mon, 31 Jan 2005 17:11:14 +0000 (17:11 +0000)]
Added outtype inference to MutCase

19 years agoFixed bug in delift. The recursive call in the Meta case was on t and not
Enrico Tassi [Mon, 31 Jan 2005 17:10:38 +0000 (17:10 +0000)]
Fixed bug in delift. The recursive call in the Meta case was on t and not
on t lifted to the meta local context.

19 years ago- removed applyStylesheets
Enrico Tassi [Tue, 25 Jan 2005 09:32:35 +0000 (09:32 +0000)]
- removed applyStylesheets
- added Print and print_kind to AST
- added coercion module

19 years agoadded list_obj and list_uri
Enrico Tassi [Tue, 25 Jan 2005 09:28:50 +0000 (09:28 +0000)]
added list_obj and list_uri

19 years ago- added code for Coercion command, Print Env command.
Enrico Tassi [Tue, 25 Jan 2005 09:26:01 +0000 (09:26 +0000)]
- added code for Coercion command, Print Env command.
- better error report in matitac

19 years ago- avoid redefinition of the same uri (checked in add_*_to_worls)
Stefano Zacchiroli [Mon, 24 Jan 2005 16:22:32 +0000 (16:22 +0000)]
- avoid redefinition of the same uri (checked in add_*_to_worls)
- defined add_inductive_def_to_world
- append owner to baseuri to minimize uri conflicts
- do not clear console!

19 years agouses CicPp.ppsort
Stefano Zacchiroli [Mon, 24 Jan 2005 16:20:29 +0000 (16:20 +0000)]
uses CicPp.ppsort

19 years ago- removed ancient debugging prints
Stefano Zacchiroli [Mon, 24 Jan 2005 16:18:13 +0000 (16:18 +0000)]
- removed ancient debugging prints

19 years ago- renamed Term_not_found exception (useless) with Object_not_found
Stefano Zacchiroli [Mon, 24 Jan 2005 16:17:33 +0000 (16:17 +0000)]
- renamed Term_not_found exception (useless) with Object_not_found
  (now used)
- added getter exception handling. Now, hopefully, we will no longer see
  Pxp_types.At exception, but more meaningful ones (like Object_not_found)
- added in_libary which checks if an object exists (either in cache
  or via getter)
- in_cache: removed old debugging messages

19 years ago- added handling of exceptions embedded in xml documents (usually coming
Stefano Zacchiroli [Mon, 24 Jan 2005 16:15:11 +0000 (16:15 +0000)]
- added handling of exceptions embedded in xml documents (usually coming
  from http_getter)
- added exception Getter_failure which wraps the above exception
- added exception Parser_failure for generic errors
- removed useless EmptyUri exception

19 years agoexception carried in response xml documents are now split in two attributes:
Stefano Zacchiroli [Mon, 24 Jan 2005 16:13:00 +0000 (16:13 +0000)]
exception carried in response xml documents are now split in two attributes:
"helm:exception" (exception name) and "helm:exception_arg" (exception
argument)

19 years agoadded helm:exception handling of Http_getter_types.Key_not_found
Stefano Zacchiroli [Mon, 24 Jan 2005 12:57:00 +0000 (12:57 +0000)]
added helm:exception handling of Http_getter_types.Key_not_found

19 years ago- sync with the new ApplyTransformation API
Enrico Tassi [Fri, 21 Jan 2005 11:52:24 +0000 (11:52 +0000)]
- sync with the new ApplyTransformation API

19 years ago- Changed ApplyTransformation API to return both the mathml and acic,
Enrico Tassi [Fri, 21 Jan 2005 11:49:03 +0000 (11:49 +0000)]
- Changed ApplyTransformation API to return both the mathml and acic,
  plus all the related tables
- Added the "Coercion" keyword to CicTextualParser2

19 years agosnapshot, notably:
Stefano Zacchiroli [Fri, 21 Jan 2005 09:40:48 +0000 (09:40 +0000)]
snapshot, notably:
- attributes support
- new ApplyTransformation interface
- simil-coma commit, browser is partially implemented :(

19 years agouniformed prototype of mml_of_cic_{object,sequent}
Stefano Zacchiroli [Fri, 21 Jan 2005 09:39:03 +0000 (09:39 +0000)]
uniformed prototype of mml_of_cic_{object,sequent}

19 years agosyntax changes: "." at the end of the phrase instead of ";;"
Stefano Zacchiroli [Fri, 21 Jan 2005 09:35:33 +0000 (09:35 +0000)]
syntax changes: "." at the end of the phrase instead of ";;"

19 years agoattributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:33:11 +0000 (09:33 +0000)]
attributes support

19 years ago- attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:30:41 +0000 (09:30 +0000)]
- attributes support
- removed ancient debug prints

19 years agoattributes support (not yet in the pretty printer)
Stefano Zacchiroli [Fri, 21 Jan 2005 09:29:48 +0000 (09:29 +0000)]
attributes support (not yet in the pretty printer)

19 years ago- attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:29:15 +0000 (09:29 +0000)]
- attributes support
- default instance is 0 (not -1 !)

19 years agoattributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:26:13 +0000 (09:26 +0000)]
attributes support

19 years agoadded attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:21:35 +0000 (09:21 +0000)]
added attributes support

19 years ago- added string_of_sort
Stefano Zacchiroli [Fri, 21 Jan 2005 09:21:16 +0000 (09:21 +0000)]
- added string_of_sort
- attributes support

19 years ago- added attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:20:58 +0000 (09:20 +0000)]
- added attributes support
- uses string_of_sort from CicPp

19 years agoadded attributes
Stefano Zacchiroli [Fri, 21 Jan 2005 09:20:09 +0000 (09:20 +0000)]
added attributes

19 years agoadded attribute support (not yet in the parser)
Stefano Zacchiroli [Fri, 21 Jan 2005 09:19:02 +0000 (09:19 +0000)]
added attribute support (not yet in the parser)

19 years agosnapshot, notably:
Stefano Zacchiroli [Thu, 20 Jan 2005 10:33:50 +0000 (10:33 +0000)]
snapshot, notably:
- added hyperlink handling in check and proof window
- start implementation of cic browser

19 years agohelmns -> helm_ns
Stefano Zacchiroli [Thu, 20 Jan 2005 10:32:38 +0000 (10:32 +0000)]
helmns -> helm_ns

19 years ago- added rendering of constants/variable with/without body
Stefano Zacchiroli [Thu, 20 Jan 2005 10:32:01 +0000 (10:32 +0000)]
- added rendering of constants/variable with/without body

19 years agorendering fixes:
Stefano Zacchiroli [Thu, 20 Jan 2005 10:31:25 +0000 (10:31 +0000)]
rendering fixes:
- does not assert false for a missing idref on a symbol (which is not
  available when rendering ast coming from parsing)
- fixed pattern matching rendering

19 years ago- helmns -> helm_ns
Stefano Zacchiroli [Thu, 20 Jan 2005 10:26:58 +0000 (10:26 +0000)]
- helmns -> helm_ns
- added xlink_ns

19 years agoadded cast rendering (used in check window by gTopLevel/matita)
Stefano Zacchiroli [Thu, 20 Jan 2005 10:26:06 +0000 (10:26 +0000)]
added cast rendering (used in check window by gTopLevel/matita)

19 years agoadded URI concrete syntax
Stefano Zacchiroli [Thu, 20 Jan 2005 10:24:59 +0000 (10:24 +0000)]
added URI concrete syntax

19 years agoadded cmdline alias "command" for "tactica"
Stefano Zacchiroli [Thu, 20 Jan 2005 10:24:44 +0000 (10:24 +0000)]
added cmdline alias "command" for "tactica"

19 years agocoercion application
Enrico Tassi [Wed, 19 Jan 2005 16:03:27 +0000 (16:03 +0000)]
coercion application

19 years agofix coercGraph.mli
Enrico Tassi [Wed, 19 Jan 2005 15:48:44 +0000 (15:48 +0000)]
fix coercGraph.mli

19 years agofixed #xpointer handling in uri_of_string. new examples :
Enrico Tassi [Wed, 19 Jan 2005 15:26:12 +0000 (15:26 +0000)]
fixed #xpointer handling in uri_of_string. new examples :

"cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "" |]

"cic:/a/b/c.ind#xpointer(1/1)" =>
  [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1)" |]

"cic:/a/b/c.ind#xpointer(1/1/1)" =>
  [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1/1)" |]

19 years agoAdded coercion handling module
Enrico Tassi [Wed, 19 Jan 2005 15:23:12 +0000 (15:23 +0000)]
Added coercion handling module

19 years agolicense template
Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:56 +0000 (18:18 +0000)]
license template

19 years agoread uri from cmdline
Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:35 +0000 (18:18 +0000)]
read uri from cmdline

19 years agoadded pp_location (pretty printer of ast location)
Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:00 +0000 (18:18 +0000)]
added pp_location (pretty printer of ast location)

19 years agoadded script support
Stefano Zacchiroli [Tue, 18 Jan 2005 18:17:33 +0000 (18:17 +0000)]
added script support

19 years agoadded latex style comment, with start token "%%"
Stefano Zacchiroli [Tue, 18 Jan 2005 18:16:43 +0000 (18:16 +0000)]
added latex style comment, with start token "%%"

19 years agoremoved spurious debugging prints
Stefano Zacchiroli [Tue, 18 Jan 2005 18:15:57 +0000 (18:15 +0000)]
removed spurious debugging prints

19 years agosnapshot, notably:
Stefano Zacchiroli [Tue, 18 Jan 2005 18:15:25 +0000 (18:15 +0000)]
snapshot, notably:
- first commit of matitac

19 years agofixed comments
Enrico Tassi [Tue, 18 Jan 2005 09:21:25 +0000 (09:21 +0000)]
fixed comments

19 years ago- added helm_ns and xhtml_ns (XHTML and HELM namespace, respectively)
Stefano Zacchiroli [Mon, 17 Jan 2005 16:24:22 +0000 (16:24 +0000)]
- added helm_ns and xhtml_ns (XHTML and HELM namespace, respectively)
- changed usage string so that it is a well fermod XHTML document (added
  namespace, quoted ampersands)

19 years agonew cicEnvironment implementation
Enrico Tassi [Mon, 17 Jan 2005 16:24:17 +0000 (16:24 +0000)]
new cicEnvironment implementation

19 years agoNo longer return HTTP 400 answers or non-xml answers: all document returned
Stefano Zacchiroli [Mon, 17 Jan 2005 16:23:26 +0000 (16:23 +0000)]
No longer return HTTP 400 answers or non-xml answers: all document returned
by the getter are now XHTML documents, possibly with the addition of an
attribute helm:exception on the root <html> element in the
http://www.cs.unibo.it/helm namespace. The presence of such an attribute
means that an exception has occured, its value is meant to be a string
encoding of the relevant ocaml exception

19 years agofirst (almost) working version: apparently, only generation of coinductive
Stefano Zacchiroli [Mon, 17 Jan 2005 14:53:03 +0000 (14:53 +0000)]
first (almost) working version: apparently, only generation of coinductive
eliminators does not typecheck

19 years agosnapshot, notably:
Stefano Zacchiroli [Fri, 14 Jan 2005 17:35:26 +0000 (17:35 +0000)]
snapshot, notably:
- changed interface, now returns a Cic.obj
- added consistency check between generated body and type

19 years agosnapshot (1st commit of fix body generation)
Stefano Zacchiroli [Thu, 13 Jan 2005 07:08:55 +0000 (07:08 +0000)]
snapshot (1st commit of fix body generation)

19 years agofixed clean_and_fill
Enrico Tassi [Wed, 12 Jan 2005 15:08:35 +0000 (15:08 +0000)]
fixed clean_and_fill

19 years agofixed bug in fill_and_clean (now the helper universes_of_obj knows that
Enrico Tassi [Wed, 12 Jan 2005 14:56:46 +0000 (14:56 +0000)]
fixed bug in fill_and_clean (now the helper universes_of_obj knows that
the uri passed as the first parameter can't be in the environment and it
doesn't requests it)

19 years agosnapshot, notably:
Stefano Zacchiroli [Tue, 11 Jan 2005 16:11:12 +0000 (16:11 +0000)]
snapshot, notably:
- added support for inductive definitions
- prelimnary support for user searches

19 years agoadded fallback case (assertion failure) for unsupported Implicit annotations
Stefano Zacchiroli [Tue, 11 Jan 2005 16:09:20 +0000 (16:09 +0000)]
added fallback case (assertion failure) for unsupported Implicit annotations

19 years agoadded syntax for URIs
Stefano Zacchiroli [Tue, 11 Jan 2005 16:08:24 +0000 (16:08 +0000)]
added syntax for URIs

19 years agoadded search commands
Stefano Zacchiroli [Tue, 11 Jan 2005 16:05:23 +0000 (16:05 +0000)]
added search commands

19 years ago- added pack/unpack over AST of terms
Stefano Zacchiroli [Tue, 11 Jan 2005 16:04:31 +0000 (16:04 +0000)]
- added pack/unpack over AST of terms
- created cicAst.mli (it was missing)

19 years ago- added pack/unpack over AST of terms
Stefano Zacchiroli [Tue, 11 Jan 2005 16:04:31 +0000 (16:04 +0000)]
- added pack/unpack over AST of terms
- created cicAst.mli (it was missing)
- added syntax for URIs

19 years agoadded clean_and_fill, to be invoked on qed
Stefano Zacchiroli [Tue, 11 Jan 2005 16:03:13 +0000 (16:03 +0000)]
added clean_and_fill, to be invoked on qed

19 years agosnapshot, not yet completed, but ...
Stefano Zacchiroli [Tue, 11 Jan 2005 16:02:53 +0000 (16:02 +0000)]
snapshot, not yet completed, but ...

19 years ago- added support for contexts (terms with holes)
Stefano Zacchiroli [Tue, 11 Jan 2005 16:01:46 +0000 (16:01 +0000)]
- added support for contexts (terms with holes)
- added CicUtil.pack/unpack to pack/unpack several terms in a single term
- added CicUtil.strip_prods to removed a given number of head prods from a term
- added CicUtil.context_of/select to create contexts/select a subterm
  matching a context

19 years agocosmetic changes
Stefano Zacchiroli [Tue, 11 Jan 2005 15:59:06 +0000 (15:59 +0000)]
cosmetic changes

19 years agoadded begin list and end list comments to help moogle search engine plugin
Enrico Tassi [Mon, 10 Jan 2005 10:47:47 +0000 (10:47 +0000)]
added begin list and end list comments to help moogle search engine plugin

19 years agoexported lift_from
Stefano Zacchiroli [Wed, 5 Jan 2005 14:07:33 +0000 (14:07 +0000)]
exported lift_from

19 years agosnapshot
Stefano Zacchiroli [Wed, 5 Jan 2005 14:06:41 +0000 (14:06 +0000)]
snapshot

19 years agoadded an hyperlink to the input syntax page
Stefano Zacchiroli [Tue, 21 Dec 2004 17:52:32 +0000 (17:52 +0000)]
added an hyperlink to the input syntax page

19 years agoimproved input syntax page with example queries of elim, match and hint
Stefano Zacchiroli [Tue, 21 Dec 2004 17:48:59 +0000 (17:48 +0000)]
improved input syntax page with example queries of elim, match and hint

19 years agoadded URI printing in the result page (so that mouse-over is not the
Stefano Zacchiroli [Tue, 21 Dec 2004 17:19:40 +0000 (17:19 +0000)]
added URI printing in the result page (so that mouse-over is not the
only way to know the URI of results!)

19 years agofirst commit (in the wrong place --by CSC) of induction principles generation
Stefano Zacchiroli [Tue, 21 Dec 2004 15:49:03 +0000 (15:49 +0000)]
first commit (in the wrong place --by CSC) of induction principles generation

19 years agoignores example binaries
Stefano Zacchiroli [Sat, 11 Dec 2004 16:32:14 +0000 (16:32 +0000)]
ignores example binaries

19 years agoported to new format of Parse_error exception (which includes error position)
Stefano Zacchiroli [Thu, 9 Dec 2004 20:31:24 +0000 (20:31 +0000)]
ported to new format of Parse_error exception (which includes error position)

19 years ago(dummy) porting to universes
Stefano Zacchiroli [Thu, 9 Dec 2004 20:29:44 +0000 (20:29 +0000)]
(dummy) porting to universes

19 years agoimplemented pretty printer for (mutual) (co)inductive types
Stefano Zacchiroli [Thu, 9 Dec 2004 17:20:56 +0000 (17:20 +0000)]
implemented pretty printer for (mutual) (co)inductive types

19 years ago(first) complete implementation of (mutual) (co)inductive types syntax
Stefano Zacchiroli [Thu, 9 Dec 2004 17:20:06 +0000 (17:20 +0000)]
(first) complete implementation of (mutual) (co)inductive types syntax

19 years agoaddded inductive definition to AST
Stefano Zacchiroli [Thu, 9 Dec 2004 15:18:50 +0000 (15:18 +0000)]
addded inductive definition to AST

19 years ago- enriched Parse_error exception with error location
Stefano Zacchiroli [Thu, 9 Dec 2004 15:18:30 +0000 (15:18 +0000)]
- enriched Parse_error exception with error location
- first implementation of inductive type definitions (not yet completed:
  mutual inductive definition are still missing)
- test parser now displays error location using ASCII escape coloring

19 years agosymmetry of equality NOT used in auto
Andrea Asperti [Tue, 7 Dec 2004 08:25:12 +0000 (08:25 +0000)]
symmetry of equality NOT used in auto

19 years agoNew version of auto with "width".
Andrea Asperti [Mon, 6 Dec 2004 12:16:07 +0000 (12:16 +0000)]
New version of auto with "width".

19 years agosnapshot
Stefano Zacchiroli [Fri, 3 Dec 2004 16:30:13 +0000 (16:30 +0000)]
snapshot