matita gtk3: some bugs fixed

+ status#stack is a list of 5 components, not 4
+ removed reference to Stdlib (was Pervasives) to comple with erlier versions of ocaml (ok with 4.0.5)

Merge branch 'matita-lablgtk3' of ssh://matita.cs.unibo.it:/srv/git/helm into matita-lablgtk3

debugging code removed

Merge branch 'declarative' into matita-lablgtk3

Change Sort.merge (deprecated) with List.merge

Test pretty printg of declarative tactics

Fix indentation in grafiteAstPp.ml and matitaEnginge.ml with ocp-indent

Add a comment and remove dead code in declarative.ml

Turn off automation weakenings

Generate new .depend files for ng_tactics, syntax_extensions

Add a function that prints a tactic term with the user defined notation
in applyTransformation

Add a function that pretty prints the tactics ASTs to a file while a
script is being parsed and executed

Make 'that is equivalent to' a standalone tactic

Simplify AST types, parsing rules and pp of tactics that had
'that is equivalent to' or 'or equivalently'

Modify grafiteEngine accordingly

Simplify the signature and the code of the implementations of tactics
that had 'that is equivalent to' or 'or equivalently'

A new "volatile_hypo" key is added to the parameter list of the currest
stack level to indicate that the beta rewriting should happen on that
hypothesis, instead of the thesis

Modify beta_rewrite accordingly

Add some "obvious" terms to the given candidates for the automation
(such as refl, sym_eq, trans_eq, etc.)

The weakening of the automation is now only partial: the second flag for
weakening is off. Setting it on makes theorem proving pretty impossible
with the declarative fragment.

Many changes

Add a BetaRewritingStep tactic, for multiple 'or equivalently'
statements in theorems proofs

Remove old code

Add a key-value list to the tiny-cals stack (parameters list) for
context related infos. Can be used as a general purpose store for
key-value pairs

Adapt code that works on the stack to work with the new parameter list

Add function to add and retrieve key-value pairs to the parameters list

Add the concept of volatile-context: they are contexts that are cleared
after the application of some tactics. E.g., the context for a
beta_rewriting (sequence of 'or equivalently') is a volatile context, as
any tactic breaks the chain

Add a function to clear volatile parameters from the paramters list

Add a case in extract_first_goal_from_status for the case where the
stack is empty

Make the tactics that make use of distribute High tactics

Reimplement the dot tac on top of the stack to handle branching. This
makes use of the second iterator list of the stack

Add a "done_continuation" function that checks whether it needs to dot
or recursively merge branches after a done statement

Add a function to push goals from the focus iterator list of the
previous level on the stack to the second iteretaor list of the current
level

Change conclude and obtain to use a volatile context to obligate the
user to only use = inside it

Change the add_names_to_goals function to use the stack instead of the
metasenv directly

Add a unfocus_branch_tac to unfocus from goals in a stack level (useful
for cases and induction)

Change induction and cases to use a context to obligate the user to use
case only inside it. Furthermore, the new stack based branching for
declarative tactics obligates the user to only switch between cases of
the last level

Change induction and cases to start without focusing on any goal and
without automatically focusing on the next goal after a done. The user
is compelled to use case to switch between each case

Change the case to only change case when the current case has been dealt
with

Attempt to fix automation

Add first draft for matita's helper

Fix indentation

Add support for proving cases in a different order

Add some debug pretty printing methods and tactics.

Add a tactic to add names to metasenv goals from a given constructor
list

Modify "we_proceed_by_induction_on" to gather info on the inductive type of
the term being eliminated, apply the right constructor to the right
number of Implicit arguments, and name the new open goals

Modify "we_proceed_by_cases_on" in an analogous way to
"we_proceed_by_induction_on"

Add a tactic to focus on a given case, if present, with helper functions
for it

Modify case to search for the given case and focus on it

Modify indtyinfo to memorize also the costructor list of the inductive
type

Remove a useless if-then-else in index_local_equations2

Remove some old code, comments and trailing spaces

Add last declarative tactics, modify rewriting tactics

Add types for induction and case analysis to grafiteAst. Add new types
for obtain and conclude

Add pp code for induction, case, obtain, conclude

Add calls in grafiteEngine for induction, case, obtain, conclude

Add parsing rules for induction, case, obtain, conclude

Rename a function for code clarity

Add function to swap two goals on the stack (useful for obtain)

Add a conclude function that checks that the given term is the lhs of
the current goal

Add a obtain function that starts an equality chain beginning with the
given term in a new goal

Modify rewriting step to only handle single equality chains steps

Add implementation for induction and case.

Add signatures for induction, case, conclude, obtain

Add keywords to matita.lang for induction, case, conclude, obtain

Changes to declarative tactics, implementation of equality chain

Fix type for RewritingStep, add a type for Print Stack (a debug tool)

Fix PP for RewritingStep, generalized just_to_tactic_just for the type
[>`Auto of auto_params | `Term of NotationPt.term]

Add parsing rule for print_stack, fix parsing rules for obtain, conclude
e =

Fix indentation for declarative.ml

Change mk_just to return a tactic (instead of a lowtactic)

Modify extract_first_goal_from_status to take the first goal from the
stack, instead of the metasenv

Change assume, suppose, andelim and existselim to use distribute_tac

Add a mustdot function to check whether there's the need to call the
dot_tactic at the end. The dot tactic is used to focus on a single goal
at the time when there are multiple open goals

Change bydone to use the dot tactic to switch between multiple goals

Modify we_need_to_prove to use the dot_tac to focus on a single goal

Add a type_of_tactic_term function to extract the type of a tactic_term
(used in RewritingStep)

Implement rewritingstep, which covers conclude and =; obtain is in the
works

Implement print_stack, for debug purposes (prints the stack to stderr)

Modify declarative's signature to add the new functions

Add firs_tac to nTactic's signature

Change auto_lowtac's signature to return a tactic

Correct natural_deduction.ma for the new version. Had to change some
\forall with \Pi

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)

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

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

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

porting to recent ocaml

...

lablgtk3.sourceview3 => lablgtk3-sourceview3

patches for compilation with ocaml 4.0.5

+ lambdadelta website update

finite_lambda restored

reverse_complexity lib restored

the toolkit.ma file contains errors. I have
commented out a few places

make depend.opt

make dist repaired

- svn export => git archive

version upgrade

added missing libs detection

Most warnings turned into errors and avoided

0.99.3 -> 0.99.4

report_error dialog ported to gtk3

Quit without saving dialog fixed

Ported to gtk3

useful comment

automatically inserted aliases

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.

use #run for dialog

Let the widget expand in the old way

Old glade2 file removed

Broken libs moved to broken_lib

Some can probably be restored with some love.

lablgladecc => lablgladecc3

It now compiles with lablgtk3 opam package

disambiguationErrors now uses #run

correct Gtk behavior

code for DisambiguationErrors simplified

Still not working (since matita 0.99x?)

several dialog boxes no longer used removed

they were dead code in current Matita
I only left the AutoWin and the ones used

last deprecated widget updated

findReplace ported from GtkTable to GtkGrid

More H/V deprecated widgets replaced

GtkHSeparator deprecated

GtkSeparator used instead

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.

comment

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

Fix dialog win

It used to be destroyed when closed the first time

Use lablgladecc -embed again

On-going porting to lablgtk3

update in basic_2

+ main result on acle proved

update in static_2

+ preorder on applicability domains
+ minor bug fixes

new web site page

change log for λδ begins

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

milestone in basic_2

We parametrize applicability condition with a generic subset of numbers.

update in static_2 and basic_2

+ a weaker version of tueq reintroduced
+ some renaming
+ one conjecture to prove

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 ...

still more additions and corrections for the article

+ one theorem was missing
+ some renaming

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

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

additions and corrections for the article on λδ-2B

+ candidates: condition S4 removed
+ arity assignment: decidability proved
+ minor additions

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

some restyling ...

+ fixing some notations
+ fixing some spaces

milestone in basic_2

+ Parametrized applicability condition allows λδ-2B to generalize both λδ-1A and λδ-1B.
+ ground_2: minor additions

update in basic_2

one file was missing in last commit :(

update in basic_2

+ totality for fixed cpce
+ Makefile: bug fixed

decentralizing core notation continues ...

+ apart, napart decentralized

update in basic_2

+ decidability of type inference
+ decidability of type checking

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

update in basic_2

+ decidability of cpes
+ some renaming

update in ground_2 static_2 basic_2

structures for decidability of the validity predicate

+ cpes, cnr, cpre resumed
+ minor corrections

milestone in basic_2

preservation of validity for rt-computation does not need the sort degree parameter (i.e. no induction on the degree).

update in ground_2 static_2 basic_2

+ whd normal forms for terms with arity
+ positive abbreviations are not whd normal forms
+ minor additions

first steps towards decidability of the validity predicate

+ tentative definition of cwhx

minor corrections and updates

intensional and extensional equivalence on lists coincide

patches for compilation with ocaml 4.0.5

+ lambdadelta website update

the decentralization of core notation continues ...

subseteq notation decentralized

finite_lambda restored

reverse_complexity lib restored

the toolkit.ma file contains errors. I have
commented out a few places

make depend.opt

make dist repaired

- svn export => git archive

version upgrade

added missing libs detection

Most warnings turned into errors and avoided

0.99.3 -> 0.99.4

report_error dialog ported to gtk3

Quit without saving dialog fixed

Ported to gtk3

useful comment

automatically inserted aliases

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.

use #run for dialog

Let the widget expand in the old way

Old glade2 file removed

Broken libs moved to broken_lib

Some can probably be restored with some love.

lablgladecc => lablgladecc3

It now compiles with lablgtk3 opam package

disambiguationErrors now uses #run

correct Gtk behavior

code for DisambiguationErrors simplified

Still not working (since matita 0.99x?)

several dialog boxes no longer used removed

they were dead code in current Matita
I only left the AutoWin and the ones used

last deprecated widget updated