Makefile improved

The library of matita is borned! Long life to the library of matita.

ma -> moo in dependencies

more logging information on received request

uses relative OCAMLPATH

now maketests uses matitaclean (but not in the right way)
tests are made in the stupid order, not in the needed one

first snapshot of separate compilation

on is now a keyword (needed in let rec)

added uri_is_ind

matitaclean.opt, matitadep.opt

removed first Cic.term from type equality, added an int (weight of the equality)

...

TacticAst2Box no longer used.

Module TacticAst2Box unused!

count_pattern implemented

More cases implemented in tactic_count.

An interesting test for replace.

replace tactic reimplemented.
It is now able to replace several terms at once.
NOTE: it is still unable to replace terms in the hypotheses.

pattern_of function reimplemented. Now it takes a term and a list of subterms
and it returns the _minimal_ pattern for the subterms in the term.

prerr_endline -> debug_print

Signature of fwdSimpl changed to get rid of a warning.

The replace tactic is now working again. It can now replace simultaneously
n terms.

Signature of fwdSimpl changed to get rid of a warning.

uri_of_string now checks the uri is well formed

matitaclean

New syntax for patterns.

1. change_tac moved from PrimitiveTactics to ReductionTactics
2. fold_tac reimplemented using change_tac

New test.

\vdash added

Syntax of patterns changed again to make it non-ambiguous:
 [in match t] [in sequent_pattern]

in case of performace improvement there is no performace loss message

matitaclean anapshot

proofs are now built lazily at the end of the computation

...

Signature and concrete syntax of fold fixed.

The pattern of a fold cannot have the "wanted" part (for the same reasons as
rewrite)

Signature and concrete syntax of fold fixed.

lapply and fwd improved

Text fixed (due to stricter semantics for naming the binders in the patterns).

The rewrite_* set of tactics is now working again. However, as before,
they do not work yet when the user asks to rewrite somethign also in the
hypotheses.

Bug fixed: a wrong lift made select unuseful when wanted was an open term.

Pretty printing of Cic.Implict (Some `Hole) is now "%"

1. rewrite_* and rewrite_back_* merged into one function
2. signature of rewrite_* improved
3. concrete syntax for the rewrite direction fixed to ">" and "<"

NOTE: rewrite_* is still no longer working.

1. rewrite_* and rewrite_back_* merged into one function
2. signature of rewrite_* improved
3. concrete syntax for the rewrite direction fixed to ">" and "<"

NOTE: rewrite_* is still no longer working.

Oooops. I forgot the convertibility test that makes the change tactic correct!

baseuri put back

The tactic change is now working again. Moreover, it now receives a pattern
in input; moreover it handles correctly the with_what argument when it must
be put in a context different from the one it was parsed in.

A bit of renaming in the code to make it more clear.

...

A simpler implementation of inversion that does not generate the dummy
hypothesis Hcut: 0=0.

buri_of_uri is now #xpointer aware.

added license stuff

better handling of script names

added a debugging helper

Obsolete comment removed.

Stupid bug fixed (a completely erroneous assert false removed).

This commit makes ProofEngineHelpers.select reach its full potentials.
Its arguments are now a conjecture and a pattern and its output is
a conjecture-like structure made of physical pointers to matching subterms
(together with their contexts).

first matitadep snapshot

1. new syntax for patterns:
    [t] [in p]
   where t is the term to be matched and p is the pattern on the hypotheses
   and on the conclusion (whose syntax is not changed).
   All the tactics now use the new syntax.
2. several tactics have been changed to use the new kind of patterns
   (that also have the optional term in them)
3. the signature of the select function has changed to require the context
   (and return a context and not a "context patch"); moreover it performs
   now both the search for roots and the search for subterms of the roots
   that are alpha-convertible with the optional given term (if any)

WARNING!!!
The following tactics have been commented out for a while:
 replace
 rewrite
 change
 fold

1. new syntax for patterns:
    [t] [in p]
   where t is the term to be matched and p is the pattern on the hypotheses
   and on the conclusion (whose syntax is not changed).
   All the tactics now use the new syntax.
2. several tactics have been changed to use the new kind of patterns
   (that also have the optional term in them)
3. the signature of the select function has changed to require the context
   (and return a context and not a "context patch"); moreover it performs
   now both the search for roots and the search for subterms of the roots
   that are alpha-convertible with the optional given term (if any)

WARNING!!!
The following tactics have been commented out for a while:
 replace
 rewrite
 change
 fold

removed profiling function (now a stub is used instead)
added a comment in urimanager

Incredible bug of simpl fixed: the stack (in the terminology used for the
Krivine's machine) was processed in the wrong context. As a result List.nth
(to get a Rel in the context) used to raise Failure in several cases. The
Failure, however, was catched somewhere in the code of matita and the
failure of simpl was hidden in most of the cases.

various updates, removed proofs for now because they are the real bottleneck!!

lapply reimplemented using letin_tac

A few bug fixes. In particular parsing errors in matitatop when a file is
given to process used to result in entering the ocaml mode. Now the user is
left in the matita mode.

fix

now baseuri is needed in each file (and its redefinition is forbidden)
added exception prettyprinter

fixed some errers in the save/cancel ...

catches more errors

does_not_occur unexported since it did not have the expected semantics

fixed save/exit stuff

fix

the error_report window is now properly closed

Removed a dummy "let ... in" that was there only to show a bug (now fixed).

Stupid bug fixed in the refinement of let ... in

Informative message corrected: MatitacLib.go () is now redefined as the more
concise go ().

fix

better message

lapply improved

matitatop.ml is now a simple invocation of Toploop.loop and .ocamlinit is
responsible to call MatitacLib.go or MatitacLib.main.

 Cons: .ocamlinit is more dirty
 Pros: it is possible to trace something even before doing a drop!

lapply improved

New solution: instead of using matitatop.bootstrap we prefer a local .ocamlinit.
 Pro:  no need of doing the weird "#use matitatop.bootstrap" by playing with
       ocaml internals.
 Pro:  local definitions and #opens in matitatop.bootstrap were lost. They are
       preserved in .ocamlinit.
 Cons: .ocamlinit must be in "." or in $HOME
 Cons: it can interfere with other .ocamlinit

In case of EOI the "go ()" loop must exit!

matitatop

More complete bootstrapper.

* new binary matitatop
* command drop enabled for matitatop.
  Once dropped use MatitacLib.go () to enter again the matita toplevel.
  Use #trace and similar stuff for debugging.
  Add printers for abstract data types in matitatop.bootstrap

  Enjoy!

added Drop

misc -> domMisc

fixed bug in response first line parsing (arbitrary reason phrases are
now supported)

added "are you sure you want to quit with usaved script?"

New argument for LApply: the ident for the generated hypothesis.

New argument for LApply: the ident for the generated hypothesis.

changed get_pair interface, now supports different unmarshallers

added get_pair method

moved discovery of METAS dir to configure.ac: script.sh no longer needed
when invoking make in subdirectories of ocaml/

bugfix: uses awk instead of cut for splitting query output (no more empty string)

New tactics.

replace generalized to patterns

1. interface of replace generalized to patterns
2. implementation commented out (for a little while)

A few other tactics made available to matita.
A few tactics (change, fold, replace) generalized to patterns.
The argument of clear and clearbody is now an identifier.