]>
matita.cs.unibo.it Git - helm.git/log
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
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!
Stefano Zacchiroli [Mon, 24 Jan 2005 16:20:29 +0000 (16:20 +0000)]
uses CicPp.ppsort
Stefano Zacchiroli [Mon, 24 Jan 2005 16:18:13 +0000 (16:18 +0000)]
- removed ancient debugging prints
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
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
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)
Stefano Zacchiroli [Mon, 24 Jan 2005 12:57:00 +0000 (12:57 +0000)]
added helm:exception handling of Http_getter_types.Key_not_found
Enrico Tassi [Fri, 21 Jan 2005 11:52:24 +0000 (11:52 +0000)]
- sync with the new ApplyTransformation API
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
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 :(
Stefano Zacchiroli [Fri, 21 Jan 2005 09:39:03 +0000 (09:39 +0000)]
uniformed prototype of mml_of_cic_{object,sequent}
Stefano Zacchiroli [Fri, 21 Jan 2005 09:35:33 +0000 (09:35 +0000)]
syntax changes: "." at the end of the phrase instead of ";;"
Stefano Zacchiroli [Fri, 21 Jan 2005 09:33:11 +0000 (09:33 +0000)]
attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:30:41 +0000 (09:30 +0000)]
- attributes support
- removed ancient debug prints
Stefano Zacchiroli [Fri, 21 Jan 2005 09:29:48 +0000 (09:29 +0000)]
attributes support (not yet in the pretty printer)
Stefano Zacchiroli [Fri, 21 Jan 2005 09:29:15 +0000 (09:29 +0000)]
- attributes support
- default instance is 0 (not -1 !)
Stefano Zacchiroli [Fri, 21 Jan 2005 09:26:13 +0000 (09:26 +0000)]
attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:21:35 +0000 (09:21 +0000)]
added attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:21:16 +0000 (09:21 +0000)]
- added string_of_sort
- attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:20:58 +0000 (09:20 +0000)]
- added attributes support
- uses string_of_sort from CicPp
Stefano Zacchiroli [Fri, 21 Jan 2005 09:20:09 +0000 (09:20 +0000)]
added attributes
Stefano Zacchiroli [Fri, 21 Jan 2005 09:19:02 +0000 (09:19 +0000)]
added attribute support (not yet in the parser)
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
Stefano Zacchiroli [Thu, 20 Jan 2005 10:32:38 +0000 (10:32 +0000)]
helmns -> helm_ns
Stefano Zacchiroli [Thu, 20 Jan 2005 10:32:01 +0000 (10:32 +0000)]
- added rendering of constants/variable with/without body
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
Stefano Zacchiroli [Thu, 20 Jan 2005 10:26:58 +0000 (10:26 +0000)]
- helmns -> helm_ns
- added xlink_ns
Stefano Zacchiroli [Thu, 20 Jan 2005 10:26:06 +0000 (10:26 +0000)]
added cast rendering (used in check window by gTopLevel/matita)
Stefano Zacchiroli [Thu, 20 Jan 2005 10:24:59 +0000 (10:24 +0000)]
added URI concrete syntax
Stefano Zacchiroli [Thu, 20 Jan 2005 10:24:44 +0000 (10:24 +0000)]
added cmdline alias "command" for "tactica"
Enrico Tassi [Wed, 19 Jan 2005 16:03:27 +0000 (16:03 +0000)]
coercion application
Enrico Tassi [Wed, 19 Jan 2005 15:48:44 +0000 (15:48 +0000)]
fix coercGraph.mli
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)" |]
Enrico Tassi [Wed, 19 Jan 2005 15:23:12 +0000 (15:23 +0000)]
Added coercion handling module
Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:56 +0000 (18:18 +0000)]
license template
Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:35 +0000 (18:18 +0000)]
read uri from cmdline
Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:00 +0000 (18:18 +0000)]
added pp_location (pretty printer of ast location)
Stefano Zacchiroli [Tue, 18 Jan 2005 18:17:33 +0000 (18:17 +0000)]
added script support
Stefano Zacchiroli [Tue, 18 Jan 2005 18:16:43 +0000 (18:16 +0000)]
added latex style comment, with start token "%%"
Stefano Zacchiroli [Tue, 18 Jan 2005 18:15:57 +0000 (18:15 +0000)]
removed spurious debugging prints
Stefano Zacchiroli [Tue, 18 Jan 2005 18:15:25 +0000 (18:15 +0000)]
snapshot, notably:
- first commit of matitac
Enrico Tassi [Tue, 18 Jan 2005 09:21:25 +0000 (09:21 +0000)]
fixed comments
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)
Enrico Tassi [Mon, 17 Jan 2005 16:24:17 +0000 (16:24 +0000)]
new cicEnvironment implementation
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
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
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
Stefano Zacchiroli [Thu, 13 Jan 2005 07:08:55 +0000 (07:08 +0000)]
snapshot (1st commit of fix body generation)
Enrico Tassi [Wed, 12 Jan 2005 15:08:35 +0000 (15:08 +0000)]
fixed clean_and_fill
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)
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
Stefano Zacchiroli [Tue, 11 Jan 2005 16:09:20 +0000 (16:09 +0000)]
added fallback case (assertion failure) for unsupported Implicit annotations
Stefano Zacchiroli [Tue, 11 Jan 2005 16:08:24 +0000 (16:08 +0000)]
added syntax for URIs
Stefano Zacchiroli [Tue, 11 Jan 2005 16:05:23 +0000 (16:05 +0000)]
added search commands
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)
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
Stefano Zacchiroli [Tue, 11 Jan 2005 16:03:13 +0000 (16:03 +0000)]
added clean_and_fill, to be invoked on qed
Stefano Zacchiroli [Tue, 11 Jan 2005 16:02:53 +0000 (16:02 +0000)]
snapshot, not yet completed, but ...
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
Stefano Zacchiroli [Tue, 11 Jan 2005 15:59:06 +0000 (15:59 +0000)]
cosmetic changes
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
Stefano Zacchiroli [Wed, 5 Jan 2005 14:07:33 +0000 (14:07 +0000)]
exported lift_from
Stefano Zacchiroli [Wed, 5 Jan 2005 14:06:41 +0000 (14:06 +0000)]
snapshot
Stefano Zacchiroli [Tue, 21 Dec 2004 17:52:32 +0000 (17:52 +0000)]
added an hyperlink to the input syntax page
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
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!)
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
Stefano Zacchiroli [Sat, 11 Dec 2004 16:32:14 +0000 (16:32 +0000)]
ignores example binaries
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)
Stefano Zacchiroli [Thu, 9 Dec 2004 20:29:44 +0000 (20:29 +0000)]
(dummy) porting to universes
Stefano Zacchiroli [Thu, 9 Dec 2004 17:20:56 +0000 (17:20 +0000)]
implemented pretty printer for (mutual) (co)inductive types
Stefano Zacchiroli [Thu, 9 Dec 2004 17:20:06 +0000 (17:20 +0000)]
(first) complete implementation of (mutual) (co)inductive types syntax
Stefano Zacchiroli [Thu, 9 Dec 2004 15:18:50 +0000 (15:18 +0000)]
addded inductive definition to AST
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
Andrea Asperti [Tue, 7 Dec 2004 08:25:12 +0000 (08:25 +0000)]
symmetry of equality NOT used in auto
Andrea Asperti [Mon, 6 Dec 2004 12:16:07 +0000 (12:16 +0000)]
New version of auto with "width".
Stefano Zacchiroli [Fri, 3 Dec 2004 16:30:13 +0000 (16:30 +0000)]
snapshot
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
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
Stefano Zacchiroli [Fri, 3 Dec 2004 15:13:29 +0000 (15:13 +0000)]
ported to universes
Stefano Zacchiroli [Thu, 2 Dec 2004 14:55:54 +0000 (14:55 +0000)]
*** empty log message ***
Enrico Tassi [Thu, 2 Dec 2004 13:43:58 +0000 (13:43 +0000)]
sync with universes and ~subst (and not ?(subst=[]))
Enrico Tassi [Wed, 1 Dec 2004 09:43:44 +0000 (09:43 +0000)]
Added universes handling. Tag PRE_UNIVERSES may help ;)
Enrico Tassi [Wed, 1 Dec 2004 09:42:42 +0000 (09:42 +0000)]
Added universes handling. The PRE_UNIVERSES tag may help ;)
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.
Stefano Zacchiroli [Mon, 29 Nov 2004 12:31:21 +0000 (12:31 +0000)]
- ported tests to newer PP / substitutions
Stefano Zacchiroli [Mon, 29 Nov 2004 12:30:31 +0000 (12:30 +0000)]
- passes subst to FreshNameGenerator
- removed some old debugging prints
Stefano Zacchiroli [Mon, 29 Nov 2004 12:30:09 +0000 (12:30 +0000)]
removed old debugging prints
Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:47 +0000 (12:24 +0000)]
passes ~subst to FreshNameGenerator
Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:25 +0000 (12:24 +0000)]
passes subst to FreshNameGenerator
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
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
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)
Stefano Zacchiroli [Fri, 26 Nov 2004 14:17:15 +0000 (14:17 +0000)]
ported to Mysql
Stefano Zacchiroli [Fri, 26 Nov 2004 14:17:01 +0000 (14:17 +0000)]
ported to new xpointer syntax
Stefano Zacchiroli [Thu, 25 Nov 2004 09:05:18 +0000 (09:05 +0000)]
protected invocations to get_cooked_obj with assertion failures
Stefano Zacchiroli [Thu, 25 Nov 2004 09:00:35 +0000 (09:00 +0000)]
protected invocations of get_cooked_obj with assertion failures
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
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)