]>
matita.cs.unibo.it Git - helm.git/log
Andrea Berlingieri [Sat, 13 Apr 2019 15:32:48 +0000 (17:32 +0200)]
Many changes
Change auto_params in grafiteAst.ml from being abstract on the 'term list
to being concretized to nterm list. Modify type just accordingly. Modify ntactic
types accordingly.
Add ExistsElim, AndElim, RewritingStep, Thesisbecomes types to ntactic.
Add pretty printing for ExistsElim, AndElim, RewritingStep, Thesisbecomes.
Add calls in grafite engine for the implementation of ExistsElim, AndElim, Thesisbecomes.
Add parsing rule for the "let x := t" tactic. It uses the NLetIn
ntactic.
Add parsing rules for Thesisbecomes and Rewritingstep (conclude, obtain
and =).
Modify mk_just to use the new auto_lowtac entry point for automation for
LCF-like tactics.
Remove same_type function in declarative.ml.
Add are_convertible function in declarative that uses beta-conversion.
Add a lambda_abstract tactic that abstracts the common parts of suppose
and assume. Add 3 Exception types for this tactic to handle error
situations. Modify assume and suppose accordingly
Add assert_tac that verifies that a given term is the same as the
conclusion and that two given types are beta-convertible, if a second
type is given. If all checks pass a continuation is exec'd, otherwise an
exception is raised.
Modify we_need_to_prove, by_just_we_proved to use assert_tac.
Add implementation of thesisbecomes.
Add implementation of existselim and andelim.
Modify declarative signature to add the new tactics.
Add a flag to index_local_equations and index_local_equations2 to
inhibit the use of global candidates. Modify all the functions that call
these two functions and the calls to those functions accordingly
(auto_main, do_something, top_cache, intros, auto_clusters)
Add a flag to auto_tac' to specify whether to use local candidates or
not. Modify the part where the local cands are calculated to check the
flag before proceeding.
Add auto_params to nnAuto.
Modify auto_tac to auto_tac' which takes the candidates to use
explicitly as a parameter and two flags that indicate whether to use
local candidates and whether to use only the given candidates.
Add a candidates_from_ctx function to calculate the candidates in a
given context.
Add a auto_lowtac entry point for LCF-like tactics.
Modify nnAuto signature to use auto_params instead of its explicit
version (nterm list * (string * string) list).
Add new "keywords" to matita.lang.
Add debug prints for a bug where the program would freeze. (They can
probably be removed)
Andrea Berlingieri [Sun, 31 Mar 2019 12:58:51 +0000 (14:58 +0200)]
Add drafts for some tactics
Add drafts for assume, suppose, we_need_to_prove.
Add a just type to handle justfications in tactics.
Add drafts for the by_done and by_just_we_proved tactics.
Everything needs testing
Andrea Berlingieri [Thu, 14 Mar 2019 09:31:01 +0000 (10:31 +0100)]
Partially restore the suppose tactic
Add a type for the suppose tactic in GrafiteAst
Add pretty printing code for the suppose tactic
Add a parsing rule for the suppose tactic in GrafiteParser
Add a call in to the suppose tactic in GrafiteEngine
Add code for the suppose tactic in Declarative
Add syntax highlight tag for the suppose tactic
Andrea Berlingieri [Wed, 13 Mar 2019 22:18:13 +0000 (23:18 +0100)]
Partially restore the assume tactic
Add a type for the assume tactic in GrafiteAst
Add pretty printing code for the assume tactic
Add a parsing rule for the assume tactic in GrafiteParser
Add a call in to the assume tactic in GrafiteEngine
Add a file for the declarative tactics to the ng_tactics module
Add code for the assume tactic in Declarative
Add syntax highlight tag for the assume tactic
Add the exact_tac signature to the interface file of nTactics
Claudio Sacerdoti Coen [Fri, 27 Sep 2019 13:55:14 +0000 (15:55 +0200)]
porting to recent ocaml
Claudio Sacerdoti Coen [Fri, 27 Sep 2019 13:54:23 +0000 (15:54 +0200)]
...
Claudio Sacerdoti Coen [Fri, 27 Sep 2019 13:51:52 +0000 (15:51 +0200)]
lablgtk3.sourceview3 => lablgtk3-sourceview3
Ferruccio Guidi [Tue, 8 Jan 2019 15:34:20 +0000 (16:34 +0100)]
patches for compilation with ocaml 4.0.5
+ lambdadelta website update
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 15:31:45 +0000 (16:31 +0100)]
finite_lambda restored
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 15:25:21 +0000 (16:25 +0100)]
reverse_complexity lib restored
the toolkit.ma file contains errors. I have
commented out a few places
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 14:33:07 +0000 (15:33 +0100)]
make depend.opt
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 13:02:54 +0000 (14:02 +0100)]
make dist repaired
- svn export => git archive
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 12:52:04 +0000 (13:52 +0100)]
version upgrade
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 00:25:46 +0000 (01:25 +0100)]
added missing libs detection
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 00:19:15 +0000 (01:19 +0100)]
Most warnings turned into errors and avoided
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 21:17:21 +0000 (22:17 +0100)]
0.99.3 -> 0.99.4
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 21:01:16 +0000 (22:01 +0100)]
report_error dialog ported to gtk3
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 20:46:50 +0000 (21:46 +0100)]
Quit without saving dialog fixed
Ported to gtk3
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:40:44 +0000 (19:40 +0100)]
useful comment
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:20:21 +0000 (19:20 +0100)]
automatically inserted aliases
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:18:24 +0000 (19:18 +0100)]
Matita 0.99.* bug fixed: new alias insertion
Fixed a bug that was there since the new Matita
generation: new_aliases were always computed
as empty and thus never inserted.
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 16:03:07 +0000 (17:03 +0100)]
use #run for dialog
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:38:07 +0000 (16:38 +0100)]
Let the widget expand in the old way
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:11:24 +0000 (16:11 +0100)]
Old glade2 file removed
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:09:34 +0000 (16:09 +0100)]
Broken libs moved to broken_lib
Some can probably be restored with some love.
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 12:38:12 +0000 (13:38 +0100)]
lablgladecc => lablgladecc3
It now compiles with lablgtk3 opam package
Claudio Sacerdoti Coen [Mon, 24 Dec 2018 00:05:41 +0000 (01:05 +0100)]
disambiguationErrors now uses #run
correct Gtk behavior
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 14:32:24 +0000 (15:32 +0100)]
code for DisambiguationErrors simplified
Still not working (since matita 0.99x?)
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 00:19:30 +0000 (01:19 +0100)]
several dialog boxes no longer used removed
they were dead code in current Matita
I only left the AutoWin and the ones used
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 00:12:51 +0000 (01:12 +0100)]
last deprecated widget updated
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 00:09:10 +0000 (01:09 +0100)]
findReplace ported from GtkTable to GtkGrid
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:42:49 +0000 (00:42 +0100)]
More H/V deprecated widgets replaced
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:39:03 +0000 (00:39 +0100)]
GtkHSeparator deprecated
GtkSeparator used instead
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:35:11 +0000 (00:35 +0100)]
HandleBox deprecated and no longer working
Replace with Box. It is used for natural
deduction palette that is not very useful
yet in the new Matita.
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:06:14 +0000 (00:06 +0100)]
comment
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:05:24 +0000 (00:05 +0100)]
Fixes to show coercion graph
- new bug in dot avoided (graphviz commands
no longer chainable)
- avoided bug that printed a broken icon in
place of an empty graph; now we print
nothing (a cleared pixbuf) which is not
white. It would be better to show
something to make clear the graph is empty
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 20:47:51 +0000 (21:47 +0100)]
Fix dialog win
It used to be destroyed when closed the first time
Claudio Sacerdoti Coen [Thu, 20 Dec 2018 22:12:36 +0000 (23:12 +0100)]
Use lablgladecc -embed again
Claudio Sacerdoti Coen [Fri, 14 Dec 2018 23:15:58 +0000 (00:15 +0100)]
On-going porting to lablgtk3
Ferruccio Guidi [Mon, 23 Sep 2019 13:00:45 +0000 (15:00 +0200)]
update in basic_2
+ main result on acle proved
Ferruccio Guidi [Wed, 18 Sep 2019 16:39:16 +0000 (18:39 +0200)]
update in static_2
+ preorder on applicability domains
+ minor bug fixes
Ferruccio Guidi [Wed, 18 Sep 2019 16:36:13 +0000 (18:36 +0200)]
new web site page
change log for λδ begins
Ferruccio Guidi [Wed, 18 Sep 2019 16:30:22 +0000 (18:30 +0200)]
update in static_2 and basic_2
+ advances on ntas for the article
+ minor corrections
+ notation update for: ac, cnv, lsubv, nta, ntas
+ bold digits in predefined virtuals
Ferruccio Guidi [Tue, 3 Sep 2019 17:36:47 +0000 (19:36 +0200)]
milestone in basic_2
We parametrize applicability condition with a generic subset of numbers.
Ferruccio Guidi [Sat, 31 Aug 2019 20:01:18 +0000 (22:01 +0200)]
update in static_2 and basic_2
+ a weaker version of tueq reintroduced
+ some renaming
+ one conjecture to prove
Ferruccio Guidi [Fri, 23 Aug 2019 19:24:02 +0000 (21:24 +0200)]
update in ground_2 static_2 basic_2
+ the applicability parameter is now a predicate
+ tueq removed in favor of theq
+ two conjectures to prove ...
Ferruccio Guidi [Mon, 19 Aug 2019 21:31:18 +0000 (23:31 +0200)]
still more additions and corrections for the article
+ one theorem was missing
+ some renaming
Ferruccio Guidi [Fri, 26 Jul 2019 14:52:57 +0000 (16:52 +0200)]
still more additions and corrections for the article
+ new proof of csx_rsx
+ more results on jsx
+ extra parameter removed from jsx
+ minor corrections on lsubr
+ some renaming
Ferruccio Guidi [Sat, 20 Jul 2019 20:13:45 +0000 (22:13 +0200)]
more additions and corrections for the article
+ fqu_clear excluded from (fqu true)
+ some renaming and changes of notation (esp. lsubsx)
+ more comments and additions to etc
+ matitadep: -b show the recursive backward dependences of a file
Ferruccio Guidi [Mon, 15 Jul 2019 17:40:22 +0000 (19:40 +0200)]
additions and corrections for the article on λδ-2B
+ candidates: condition S4 removed
+ arity assignment: decidability proved
+ minor additions
Ferruccio Guidi [Sat, 15 Jun 2019 13:19:59 +0000 (15:19 +0200)]
updating the structures for sorts
+ strict monotonicity is now an optional property
+ new optional properties: acyclicity and decidability
+ "next" now has a specific notation
+ refactored sort degree is now based on acyclicity and decidability
Ferruccio Guidi [Thu, 13 Jun 2019 15:07:51 +0000 (17:07 +0200)]
some restyling ...
+ fixing some notations
+ fixing some spaces
Ferruccio Guidi [Sun, 2 Jun 2019 13:52:42 +0000 (15:52 +0200)]
milestone in basic_2
+ Parametrized applicability condition allows λδ-2B to generalize both λδ-1A and λδ-1B.
+ ground_2: minor additions
Ferruccio Guidi [Thu, 30 May 2019 13:59:32 +0000 (15:59 +0200)]
update in basic_2
one file was missing in last commit :(
Ferruccio Guidi [Wed, 29 May 2019 19:52:30 +0000 (21:52 +0200)]
update in basic_2
+ totality for fixed cpce
+ Makefile: bug fixed
Ferruccio Guidi [Thu, 16 May 2019 21:55:15 +0000 (23:55 +0200)]
decentralizing core notation continues ...
+ apart, napart decentralized
Ferruccio Guidi [Wed, 17 Apr 2019 18:30:00 +0000 (20:30 +0200)]
update in basic_2
+ decidability of type inference
+ decidability of type checking
Ferruccio Guidi [Tue, 16 Apr 2019 21:11:59 +0000 (23:11 +0200)]
milestone in basic_2 with additions in static_2
+ validity is decidable
+ some renaming
+ batch compilation handles each specification separately
otherwise matitac opens too many files
Ferruccio Guidi [Mon, 8 Apr 2019 16:47:22 +0000 (18:47 +0200)]
update in basic_2
+ decidability of cpes
+ some renaming
Ferruccio Guidi [Fri, 5 Apr 2019 13:34:26 +0000 (15:34 +0200)]
update in ground_2 static_2 basic_2
structures for decidability of the validity predicate
+ cpes, cnr, cpre resumed
+ minor corrections
Ferruccio Guidi [Mon, 25 Mar 2019 16:32:22 +0000 (17:32 +0100)]
milestone in basic_2
preservation of validity for rt-computation does not need the sort degree parameter (i.e. no induction on the degree).
Ferruccio Guidi [Wed, 20 Mar 2019 11:30:38 +0000 (12:30 +0100)]
update in ground_2 static_2 basic_2
+ whd normal forms for terms with arity
+ positive abbreviations are not whd normal forms
+ minor additions
Ferruccio Guidi [Mon, 4 Mar 2019 23:35:54 +0000 (00:35 +0100)]
first steps towards decidability of the validity predicate
+ tentative definition of cwhx
Ferruccio Guidi [Mon, 4 Feb 2019 16:06:36 +0000 (17:06 +0100)]
minor corrections and updates
intensional and extensional equivalence on lists coincide
Ferruccio Guidi [Tue, 8 Jan 2019 15:34:20 +0000 (16:34 +0100)]
patches for compilation with ocaml 4.0.5
+ lambdadelta website update
Ferruccio Guidi [Tue, 1 Jan 2019 13:30:18 +0000 (14:30 +0100)]
the decentralization of core notation continues ...
subseteq notation decentralized
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 15:31:45 +0000 (16:31 +0100)]
finite_lambda restored
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 15:25:21 +0000 (16:25 +0100)]
reverse_complexity lib restored
the toolkit.ma file contains errors. I have
commented out a few places
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 14:33:07 +0000 (15:33 +0100)]
make depend.opt
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 13:02:54 +0000 (14:02 +0100)]
make dist repaired
- svn export => git archive
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 12:52:04 +0000 (13:52 +0100)]
version upgrade
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 00:25:46 +0000 (01:25 +0100)]
added missing libs detection
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 00:19:15 +0000 (01:19 +0100)]
Most warnings turned into errors and avoided
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 21:17:21 +0000 (22:17 +0100)]
0.99.3 -> 0.99.4
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 21:01:16 +0000 (22:01 +0100)]
report_error dialog ported to gtk3
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 20:46:50 +0000 (21:46 +0100)]
Quit without saving dialog fixed
Ported to gtk3
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:40:44 +0000 (19:40 +0100)]
useful comment
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:20:21 +0000 (19:20 +0100)]
automatically inserted aliases
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:18:24 +0000 (19:18 +0100)]
Matita 0.99.* bug fixed: new alias insertion
Fixed a bug that was there since the new Matita
generation: new_aliases were always computed
as empty and thus never inserted.
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 16:03:07 +0000 (17:03 +0100)]
use #run for dialog
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:38:07 +0000 (16:38 +0100)]
Let the widget expand in the old way
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:11:24 +0000 (16:11 +0100)]
Old glade2 file removed
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:09:34 +0000 (16:09 +0100)]
Broken libs moved to broken_lib
Some can probably be restored with some love.
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 12:38:12 +0000 (13:38 +0100)]
lablgladecc => lablgladecc3
It now compiles with lablgtk3 opam package
Claudio Sacerdoti Coen [Mon, 24 Dec 2018 00:05:41 +0000 (01:05 +0100)]
disambiguationErrors now uses #run
correct Gtk behavior
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 14:32:24 +0000 (15:32 +0100)]
code for DisambiguationErrors simplified
Still not working (since matita 0.99x?)
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 00:19:30 +0000 (01:19 +0100)]
several dialog boxes no longer used removed
they were dead code in current Matita
I only left the AutoWin and the ones used
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 00:12:51 +0000 (01:12 +0100)]
last deprecated widget updated
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 00:09:10 +0000 (01:09 +0100)]
findReplace ported from GtkTable to GtkGrid
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:42:49 +0000 (00:42 +0100)]
More H/V deprecated widgets replaced
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:39:03 +0000 (00:39 +0100)]
GtkHSeparator deprecated
GtkSeparator used instead
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:35:11 +0000 (00:35 +0100)]
HandleBox deprecated and no longer working
Replace with Box. It is used for natural
deduction palette that is not very useful
yet in the new Matita.
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:06:14 +0000 (00:06 +0100)]
comment
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:05:24 +0000 (00:05 +0100)]
Fixes to show coercion graph
- new bug in dot avoided (graphviz commands
no longer chainable)
- avoided bug that printed a broken icon in
place of an empty graph; now we print
nothing (a cleared pixbuf) which is not
white. It would be better to show
something to make clear the graph is empty
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 20:47:51 +0000 (21:47 +0100)]
Fix dialog win
It used to be destroyed when closed the first time
Claudio Sacerdoti Coen [Thu, 20 Dec 2018 22:12:36 +0000 (23:12 +0100)]
Use lablgladecc -embed again
Ferruccio Guidi [Thu, 20 Dec 2018 15:46:01 +0000 (16:46 +0100)]
xoa utility updated
+ two missing cases implemented
+ dependences fixed in Makefile
Claudio Sacerdoti Coen [Fri, 14 Dec 2018 23:15:58 +0000 (00:15 +0100)]
On-going porting to lablgtk3
Ferruccio Guidi [Mon, 17 Dec 2018 20:11:50 +0000 (21:11 +0100)]
list of failing files updated
+ one file added
Ferruccio Guidi [Mon, 10 Dec 2018 20:13:41 +0000 (21:13 +0100)]
web site update
one css stylesheet improved