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

19 years agoported to universes
Stefano Zacchiroli [Fri, 3 Dec 2004 15:13:29 +0000 (15:13 +0000)]
ported to universes

19 years ago*** empty log message ***
Stefano Zacchiroli [Thu, 2 Dec 2004 14:55:54 +0000 (14:55 +0000)]
*** empty log message ***

19 years agosync with universes and ~subst (and not ?(subst=[]))
Enrico Tassi [Thu, 2 Dec 2004 13:43:58 +0000 (13:43 +0000)]
sync with universes and ~subst (and not ?(subst=[]))

19 years agoAdded universes handling. Tag PRE_UNIVERSES may help ;)
Enrico Tassi [Wed, 1 Dec 2004 09:43:44 +0000 (09:43 +0000)]
Added universes handling. Tag PRE_UNIVERSES may help ;)

19 years agoAdded universes handling. The PRE_UNIVERSES tag may help ;)
Enrico Tassi [Wed, 1 Dec 2004 09:42:42 +0000 (09:42 +0000)]
Added universes handling. The PRE_UNIVERSES tag may help ;)

19 years agoBug in the management of substitutions into auto corrected.
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.

19 years ago- ported tests to newer PP / substitutions
Stefano Zacchiroli [Mon, 29 Nov 2004 12:31:21 +0000 (12:31 +0000)]
- ported tests to newer PP / substitutions

19 years ago- passes subst to FreshNameGenerator
Stefano Zacchiroli [Mon, 29 Nov 2004 12:30:31 +0000 (12:30 +0000)]
- passes subst to FreshNameGenerator
- removed some old debugging prints

19 years agoremoved old debugging prints
Stefano Zacchiroli [Mon, 29 Nov 2004 12:30:09 +0000 (12:30 +0000)]
removed old debugging prints

19 years agopasses ~subst to FreshNameGenerator
Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:47 +0000 (12:24 +0000)]
passes ~subst to FreshNameGenerator

19 years agopasses subst to FreshNameGenerator
Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:25 +0000 (12:24 +0000)]
passes subst to FreshNameGenerator

19 years ago- pass subst to FreshNameGenerator on mk_fresh_name invocations
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

19 years agobugfix: FreshNameGenerator uses the type checker on mk_fresh_name
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

19 years agobugfix in type_of_aux' which erroneously discard given substitution
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)

20 years agoported to Mysql
Stefano Zacchiroli [Fri, 26 Nov 2004 14:17:15 +0000 (14:17 +0000)]
ported to Mysql

20 years agoported to new xpointer syntax
Stefano Zacchiroli [Fri, 26 Nov 2004 14:17:01 +0000 (14:17 +0000)]
ported to new xpointer syntax

20 years agoprotected invocations to get_cooked_obj with assertion failures
Stefano Zacchiroli [Thu, 25 Nov 2004 09:05:18 +0000 (09:05 +0000)]
protected invocations to get_cooked_obj with assertion failures

20 years agoprotected invocations of 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

20 years agoguard get_cooked_obj calls with assert false in case of Not_found
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

20 years agouse get_obj instead of get_cooked_obj in order to retrieve params for
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)

20 years ago* several adjustments after introduction of the depth column
Luca Padovani [Tue, 23 Nov 2004 15:15:41 +0000 (15:15 +0000)]
* several adjustments after introduction of the depth column

20 years ago* validation scripts
Luca Padovani [Tue, 23 Nov 2004 13:39:24 +0000 (13:39 +0000)]
* validation scripts

20 years ago* basic infrastructure for collecting statistics
Luca Padovani [Tue, 23 Nov 2004 13:38:52 +0000 (13:38 +0000)]
* basic infrastructure for collecting statistics

20 years agoadded parse test for
Stefano Zacchiroli [Mon, 22 Nov 2004 17:20:15 +0000 (17:20 +0000)]
added parse test for
- expat
- libxml2 (xmlreader API)
- libxml2 (SAX2 API)

20 years agoset environment trust to false to avoid dummy proof checking
Stefano Zacchiroli [Thu, 18 Nov 2004 16:50:34 +0000 (16:50 +0000)]
set environment trust to false to avoid dummy proof checking

20 years agouse stateful logger so that the ProofChecker daemon is able to properly
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

20 years agoadded a stateful logger which remember indentation level of recursive
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

20 years agoadded set_trust to externally set the trust function (used by the proof
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)

20 years agoported to Mysql native connection
Stefano Zacchiroli [Thu, 18 Nov 2004 13:45:18 +0000 (13:45 +0000)]
ported to Mysql native connection

20 years agoResolved problem occured when "=" in MainConclusion
Matteo Selmi [Wed, 17 Nov 2004 14:47:13 +0000 (14:47 +0000)]
Resolved problem occured when "=" in MainConclusion

20 years agoRemoved duplicated uri in sigmatch
Matteo Selmi [Wed, 17 Nov 2004 12:48:55 +0000 (12:48 +0000)]
Removed duplicated uri in sigmatch

20 years agoBug fix
Matteo Selmi [Wed, 17 Nov 2004 11:13:46 +0000 (11:13 +0000)]
Bug fix

20 years agochanged reduction tactics ast
Stefano Zacchiroli [Mon, 15 Nov 2004 09:04:40 +0000 (09:04 +0000)]
changed reduction tactics ast

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

20 years agoFixed an hidden occur check problem: when a Meta is being delifted,
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.

20 years agoadded dummy entry in CicAst: UserInput
Stefano Zacchiroli [Thu, 11 Nov 2004 13:30:45 +0000 (13:30 +0000)]
added dummy entry in CicAst: UserInput

20 years agosnapshot:
Stefano Zacchiroli [Thu, 11 Nov 2004 13:30:11 +0000 (13:30 +0000)]
snapshot:
- changed interaction model

20 years agobumped changelog line to match upload date
Stefano Zacchiroli [Wed, 10 Nov 2004 13:22:34 +0000 (13:22 +0000)]
bumped changelog line to match upload date

20 years agodisabled debugging info
Stefano Zacchiroli [Wed, 10 Nov 2004 12:02:27 +0000 (12:02 +0000)]
disabled debugging info

20 years agoparse Baseuri command
Stefano Zacchiroli [Wed, 10 Nov 2004 12:02:21 +0000 (12:02 +0000)]
parse Baseuri command