]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

19 years agomoogle syntax help page, actually contains only syntax and examples for
Stefano Zacchiroli [Fri, 3 Dec 2004 16:05:27 +0000 (16:05 +0000)]
moogle syntax help page, actually contains only syntax and examples for
the "locate" query. "hint", "match" and "elim" syntaxes are currently
undocumented

19 years agochanged "locate" so that it supports shell-like pattern matching with
Stefano Zacchiroli [Fri, 3 Dec 2004 16:04:01 +0000 (16:04 +0000)]
changed "locate" so that it supports shell-like pattern matching with
'*' and '?' wildcards