matita.cs.unibo.it Git - helm.git/log

]> matita.cs.unibo.it Git - helm.git/log

projects / helm.git / log

summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 24 Jan 2005 16:18:13 +0000 (16:18 +0000)]

- removed ancient debugging prints

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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)

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 24 Jan 2005 12:57:00 +0000 (12:57 +0000)]

added helm:exception handling of Http_getter_types.Key_not_found

commit | commitdiff | tree

Enrico Tassi [Fri, 21 Jan 2005 11:52:24 +0000 (11:52 +0000)]

- sync with the new ApplyTransformation API

commit | commitdiff | tree

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

commit | commitdiff | tree

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 :(

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 21 Jan 2005 09:39:03 +0000 (09:39 +0000)]

uniformed prototype of mml_of_cic_{object,sequent}

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 21 Jan 2005 09:35:33 +0000 (09:35 +0000)]

syntax changes: "." at the end of the phrase instead of ";;"

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 21 Jan 2005 09:33:11 +0000 (09:33 +0000)]

attributes support

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 21 Jan 2005 09:30:41 +0000 (09:30 +0000)]

- attributes support
- removed ancient debug prints

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 21 Jan 2005 09:29:48 +0000 (09:29 +0000)]

attributes support (not yet in the pretty printer)

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 21 Jan 2005 09:29:15 +0000 (09:29 +0000)]

- attributes support
- default instance is 0 (not -1 !)

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 21 Jan 2005 09:26:13 +0000 (09:26 +0000)]

attributes support

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 21 Jan 2005 09:21:35 +0000 (09:21 +0000)]

added attributes support

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 21 Jan 2005 09:21:16 +0000 (09:21 +0000)]

- added string_of_sort
- attributes support

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 21 Jan 2005 09:20:58 +0000 (09:20 +0000)]

- added attributes support
- uses string_of_sort from CicPp

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 21 Jan 2005 09:20:09 +0000 (09:20 +0000)]

added attributes

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 21 Jan 2005 09:19:02 +0000 (09:19 +0000)]

added attribute support (not yet in the parser)

commit | commitdiff | tree

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

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 20 Jan 2005 10:32:38 +0000 (10:32 +0000)]

helmns -> helm_ns

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 20 Jan 2005 10:32:01 +0000 (10:32 +0000)]

- added rendering of constants/variable with/without body

commit | commitdiff | tree

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

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 20 Jan 2005 10:26:58 +0000 (10:26 +0000)]

- helmns -> helm_ns
- added xlink_ns

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 20 Jan 2005 10:26:06 +0000 (10:26 +0000)]

added cast rendering (used in check window by gTopLevel/matita)

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 20 Jan 2005 10:24:59 +0000 (10:24 +0000)]

added URI concrete syntax

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 20 Jan 2005 10:24:44 +0000 (10:24 +0000)]

added cmdline alias "command" for "tactica"

commit | commitdiff | tree

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

coercion application

commit | commitdiff | tree

Enrico Tassi [Wed, 19 Jan 2005 15:48:44 +0000 (15:48 +0000)]

fix coercGraph.mli

commit | commitdiff | tree

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)" |]

commit | commitdiff | tree

Enrico Tassi [Wed, 19 Jan 2005 15:23:12 +0000 (15:23 +0000)]

Added coercion handling module

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:56 +0000 (18:18 +0000)]

license template

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:35 +0000 (18:18 +0000)]

read uri from cmdline

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:00 +0000 (18:18 +0000)]

added pp_location (pretty printer of ast location)

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 18 Jan 2005 18:17:33 +0000 (18:17 +0000)]

added script support

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 18 Jan 2005 18:16:43 +0000 (18:16 +0000)]

added latex style comment, with start token "%%"

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 18 Jan 2005 18:15:57 +0000 (18:15 +0000)]

removed spurious debugging prints

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 18 Jan 2005 18:15:25 +0000 (18:15 +0000)]

snapshot, notably:
- first commit of matitac

commit | commitdiff | tree

Enrico Tassi [Tue, 18 Jan 2005 09:21:25 +0000 (09:21 +0000)]

fixed comments

commit | commitdiff | tree

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)

commit | commitdiff | tree

Enrico Tassi [Mon, 17 Jan 2005 16:24:17 +0000 (16:24 +0000)]

new cicEnvironment implementation

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 13 Jan 2005 07:08:55 +0000 (07:08 +0000)]

snapshot (1st commit of fix body generation)

commit | commitdiff | tree

Enrico Tassi [Wed, 12 Jan 2005 15:08:35 +0000 (15:08 +0000)]

fixed clean_and_fill

commit | commitdiff | tree

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)

commit | commitdiff | tree

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

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 11 Jan 2005 16:09:20 +0000 (16:09 +0000)]

added fallback case (assertion failure) for unsupported Implicit annotations

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 11 Jan 2005 16:08:24 +0000 (16:08 +0000)]

added syntax for URIs

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 11 Jan 2005 16:05:23 +0000 (16:05 +0000)]

added search commands

commit | commitdiff | tree

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)

commit | commitdiff | tree

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

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 11 Jan 2005 16:03:13 +0000 (16:03 +0000)]

added clean_and_fill, to be invoked on qed

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 11 Jan 2005 16:02:53 +0000 (16:02 +0000)]

snapshot, not yet completed, but ...

commit | commitdiff | tree

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

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 11 Jan 2005 15:59:06 +0000 (15:59 +0000)]

cosmetic changes

commit | commitdiff | tree

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

commit | commitdiff | tree

Stefano Zacchiroli [Wed, 5 Jan 2005 14:07:33 +0000 (14:07 +0000)]

exported lift_from

commit | commitdiff | tree

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

snapshot

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 21 Dec 2004 17:52:32 +0000 (17:52 +0000)]

added an hyperlink to the input syntax page

commit | commitdiff | tree

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

commit | commitdiff | tree

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!)

commit | commitdiff | tree

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

commit | commitdiff | tree

Stefano Zacchiroli [Sat, 11 Dec 2004 16:32:14 +0000 (16:32 +0000)]

ignores example binaries

commit | commitdiff | tree

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)

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 9 Dec 2004 20:29:44 +0000 (20:29 +0000)]

(dummy) porting to universes

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 9 Dec 2004 17:20:56 +0000 (17:20 +0000)]

implemented pretty printer for (mutual) (co)inductive types

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 9 Dec 2004 17:20:06 +0000 (17:20 +0000)]

(first) complete implementation of (mutual) (co)inductive types syntax

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 9 Dec 2004 15:18:50 +0000 (15:18 +0000)]

addded inductive definition to AST

commit | commitdiff | tree

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

commit | commitdiff | tree

Andrea Asperti [Tue, 7 Dec 2004 08:25:12 +0000 (08:25 +0000)]

symmetry of equality NOT used in auto

commit | commitdiff | tree

Andrea Asperti [Mon, 6 Dec 2004 12:16:07 +0000 (12:16 +0000)]

New version of auto with "width".

commit | commitdiff | tree

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

snapshot

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 3 Dec 2004 15:13:29 +0000 (15:13 +0000)]

ported to universes

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 2 Dec 2004 14:55:54 +0000 (14:55 +0000)]

*** empty log message ***

commit | commitdiff | tree

Enrico Tassi [Thu, 2 Dec 2004 13:43:58 +0000 (13:43 +0000)]

sync with universes and ~subst (and not ?(subst=[]))

commit | commitdiff | tree

Enrico Tassi [Wed, 1 Dec 2004 09:43:44 +0000 (09:43 +0000)]

Added universes handling. Tag PRE_UNIVERSES may help ;)

commit | commitdiff | tree

Enrico Tassi [Wed, 1 Dec 2004 09:42:42 +0000 (09:42 +0000)]

Added universes handling. The PRE_UNIVERSES tag may help ;)

commit | commitdiff | tree

Andrea Asperti [Tue, 30 Nov 2004 14:55:27 +0000 (14:55 +0000)]

Bug in the management of substitutions into auto corrected.
No significative loss in performance.
Comments commented.

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 29 Nov 2004 12:31:21 +0000 (12:31 +0000)]

- ported tests to newer PP / substitutions

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 29 Nov 2004 12:30:31 +0000 (12:30 +0000)]

- passes subst to FreshNameGenerator
- removed some old debugging prints

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 29 Nov 2004 12:30:09 +0000 (12:30 +0000)]

removed old debugging prints

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:47 +0000 (12:24 +0000)]

passes ~subst to FreshNameGenerator

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:25 +0000 (12:24 +0000)]

passes subst to FreshNameGenerator

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:09 +0000 (12:24 +0000)]

- pass subst to FreshNameGenerator on mk_fresh_name invocations
- removed assert failures on get_cooked_obj (rolled back last commit)
- reindented (the huuuuuuuge) eat_prods function

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 29 Nov 2004 12:22:23 +0000 (12:22 +0000)]

bugfix: FreshNameGenerator uses the type checker on mk_fresh_name
invocation, thus it should receive in input a subst to be passed to the
type checker in order to avoid "unknown" Metas in the term to be type
checked

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 29 Nov 2004 12:20:06 +0000 (12:20 +0000)]

bugfix in type_of_aux' which erroneously discard given substitution
(fixes a lot of CicUtil.Meta_not_found spurious exceptions)

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 26 Nov 2004 14:17:15 +0000 (14:17 +0000)]

ported to Mysql

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 26 Nov 2004 14:17:01 +0000 (14:17 +0000)]

ported to new xpointer syntax

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 25 Nov 2004 09:05:18 +0000 (09:05 +0000)]

protected invocations to get_cooked_obj with assertion failures

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 25 Nov 2004 09:00:35 +0000 (09:00 +0000)]

protected invocations of get_cooked_obj with assertion failures

commit | commitdiff | tree

Stefano Zacchiroli [Wed, 24 Nov 2004 13:18:03 +0000 (13:18 +0000)]

guard get_cooked_obj calls with assert false in case of Not_found

commit | commitdiff | tree

Stefano Zacchiroli [Wed, 24 Nov 2004 13:17:39 +0000 (13:17 +0000)]

use get_obj instead of get_cooked_obj in order to retrieve params for
unchecked objects (fixes "not found" bug when trust in the environment
is false)

commit | commitdiff | tree

Luca Padovani [Tue, 23 Nov 2004 15:15:41 +0000 (15:15 +0000)]

* several adjustments after introduction of the depth column

commit | commitdiff | tree

Luca Padovani [Tue, 23 Nov 2004 13:39:24 +0000 (13:39 +0000)]

* validation scripts

commit | commitdiff | tree

Luca Padovani [Tue, 23 Nov 2004 13:38:52 +0000 (13:38 +0000)]

* basic infrastructure for collecting statistics

Unnamed repository; edit this file 'description' to name the repository.