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

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

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 22 Nov 2004 17:20:15 +0000 (17:20 +0000)]

added parse test for
- expat
- libxml2 (xmlreader API)
- libxml2 (SAX2 API)

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 18 Nov 2004 16:50:34 +0000 (16:50 +0000)]

set environment trust to false to avoid dummy proof checking

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 18 Nov 2004 16:47:28 +0000 (16:47 +0000)]

use stateful logger so that the ProofChecker daemon is able to properly
indent proof checking messages

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 18 Nov 2004 16:46:23 +0000 (16:46 +0000)]

added a stateful logger which remember indentation level of recursive
type checking

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 18 Nov 2004 16:45:43 +0000 (16:45 +0000)]

added set_trust to externally set the trust function (used by the proof
checking daemon)

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 18 Nov 2004 13:45:18 +0000 (13:45 +0000)]

ported to Mysql native connection

commit | commitdiff | tree

Matteo Selmi [Wed, 17 Nov 2004 14:47:13 +0000 (14:47 +0000)]

Resolved problem occured when "=" in MainConclusion

commit | commitdiff | tree

Matteo Selmi [Wed, 17 Nov 2004 12:48:55 +0000 (12:48 +0000)]

Removed duplicated uri in sigmatch

commit | commitdiff | tree

Matteo Selmi [Wed, 17 Nov 2004 11:13:46 +0000 (11:13 +0000)]

Bug fix

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 15 Nov 2004 09:04:40 +0000 (09:04 +0000)]

changed reduction tactics ast

commit | commitdiff | tree

Stefano Zacchiroli [Mon, 15 Nov 2004 09:03:45 +0000 (09:03 +0000)]

snapshot

commit | commitdiff | tree

Stefano Zacchiroli [Fri, 12 Nov 2004 18:13:17 +0000 (18:13 +0000)]

Fixed an hidden occur check problem: when a Meta is being delifted,
apply substitution on the fly and delift the result. Previously we did
not recursively check the instantiation of the Meta.

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 11 Nov 2004 13:30:45 +0000 (13:30 +0000)]

added dummy entry in CicAst: UserInput

commit | commitdiff | tree

Stefano Zacchiroli [Thu, 11 Nov 2004 13:30:11 +0000 (13:30 +0000)]

snapshot:
- changed interaction model

commit | commitdiff | tree

Stefano Zacchiroli [Wed, 10 Nov 2004 13:22:34 +0000 (13:22 +0000)]

bumped changelog line to match upload date

commit | commitdiff | tree

Stefano Zacchiroli [Wed, 10 Nov 2004 12:02:27 +0000 (12:02 +0000)]

disabled debugging info

commit | commitdiff | tree

Stefano Zacchiroli [Wed, 10 Nov 2004 12:02:21 +0000 (12:02 +0000)]

parse Baseuri command

commit | commitdiff | tree

Stefano Zacchiroli [Wed, 10 Nov 2004 12:01:52 +0000 (12:01 +0000)]

added Baseuri command

commit | commitdiff | tree

Stefano Zacchiroli [Wed, 10 Nov 2004 12:01:39 +0000 (12:01 +0000)]

commented out some timing messages

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 9 Nov 2004 17:23:18 +0000 (17:23 +0000)]

snapshot, notably:
- fixed "noshow" bugs in sequents notebook and proof window
- implemented interpretation choice

commit | commitdiff | tree

Luca Padovani [Tue, 9 Nov 2004 15:30:33 +0000 (15:30 +0000)]

* compressed statistics committed

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 9 Nov 2004 14:38:20 +0000 (14:38 +0000)]

- split compound fields
- rounded to integer floating point values

commit | commitdiff | tree

Luca Padovani [Tue, 9 Nov 2004 13:56:59 +0000 (13:56 +0000)]

* snapshot

commit | commitdiff | tree

Andrea Asperti [Tue, 9 Nov 2004 12:16:24 +0000 (12:16 +0000)]

Aggiunta l'introduzione alla prima sezione:.

commit | commitdiff | tree

Luca Padovani [Tue, 9 Nov 2004 12:07:55 +0000 (12:07 +0000)]

* output of XML file size

commit | commitdiff | tree

Luca Padovani [Tue, 9 Nov 2004 12:05:09 +0000 (12:05 +0000)]

* fix bug detect blank nodes
* output of file size

commit | commitdiff | tree

Luca Padovani [Tue, 9 Nov 2004 08:22:37 +0000 (08:22 +0000)]

* added stylesheet to render the results

commit | commitdiff | tree

Stefano Zacchiroli [Tue, 9 Nov 2004 08:15:43 +0000 (08:15 +0000)]

added filling of no_concl_hyp

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