The fold tactic of proofEngine now uses ReductionTactics.fold_tac.
A parameter was added to choose if the reduction must be performed also
in the hypotheses.
New CicTextualParser: it now returns (approximately) a couple
list of free names * function from an interpretation to a Cic term
where an interpretation is a function from string (ids) to uris.
- ElimIntrosSimpl now implemented using tacticals. It becomes an
ElimSimplIntros (which does lambda-abstraction with the reduced type ;-(((
To be fixed.
- reductionTactics now also have the usual interface for tactics
- (Partial) porting to the new theory with explicit named substitutions
- Porting to the new DTD
- Porting to the new query language and to its implementation
- searchPattern implemented: it performs an old "backward" query and then
tries to apply every result to filter out false matches
Open bugs:
- ElimIntrosSimpl, Fourier and Ring still to be ported
- many, many, many others
Better implementation of the trusting machinery: some CicEnvironment functions
now have a trust optional attribute (that defaults to true). The TypeChecker
uses the false value only when type-checking the topmost object.
Every other operation of the kernel uses the true value (i.e. it trusts).
Is this really a safe behaviour? Hmmmmm. We need a proof here.
- metasenv is now checked
- the last commit introduced a bug: the debrujin function was called on
the type of a constructor _before_ removing the left parameters. Fixed.
- parser improved: constant uris and variable uris are now handled differently
- the callback function must now return a URI and no more a term
- explicit named substitutions (with syntax { V1 := t1 ; ... ; V2 := t2})
implemented
- for/of attribute no more checked ;-(
- parsing does not require any more the current uri (that was unclear
for CurrentProof)
- as a consequence of the previous change the parser should now be reentrant
- Porting of all the code to the new DTD format (with, among others, explicit
named substitutions)
- Porting to the new version of Pxp
- Porting of the cicReductionMachine code (that was abandoned for a while)
- Removal of all the cooking machinery
- Removal of the optimization (memoization) of the computation of recursive
arguments of constructors. Required to implement the next point. The actual
performance loss is minimal.
- First prototype of an environment with trusting abilities.
Notes: unification is still untested and probably wrong w.r.t. explicit
name substitutions.
Matteo Selmi [Tue, 22 Oct 2002 14:25:56 +0000 (14:25 +0000)]
- removed checkings for objects Definition and Axiom.
- inserted checkings for objects CostantType and ConstantBody.
- modified mode of view params (not "path/varname.var" but "varname").
- modified checkings for term LAMBDA, LETIN, PROD (with insertion of checkings for decl and def when used by these terms)
Better handling of queries. Now both the locate and backward queries give
the user the possibility to disambiguate the answer, and write it in the
input window. Some bugs in the disambiguation process have been fixed.
Finally the output of the query process in the outputhtml window is now
much more verbose.
When locate is used during the lexing phase, it may happen that no URI is
found or more than an URI is found. In those cases a window is now opened
and the user is asked to either enter the URI (if none was found) or
choose from the list of found URIs.
Patch applied to the locate query: when used to retrieve the first inductive
type of a mutual inductive types block, the returned URI is now the URI of
the type (with the fragment identifier!) and not the one of the block (without).
The parser (the lexer indeed) now use the locate query to locate an object
whose identifier is unknown. In ambigous cases, no choice is given to the
user and the usual exception (identifier not found) is raised. It works
only for constants and for the first inductive type of a mutual inductive
type block.
Irene Schena [Wed, 28 Aug 2002 14:57:52 +0000 (14:57 +0000)]
Modified Files:
1)core_grammar.txt grammar.txt query.xml xmathql.dtd: new version
----------------------------------------------------------------------
Many improvements in tactics (and tactical) representation:
1) tactics are no more functions from state to state, but functions from
proof * goal to proof * goal list where the goal list is the list of
new goals generated
2) proof and goal are no more optional
3) all the tactics have been slightly changed so that their type is now
param1 -> ... -> paramn -> ProofEngineTypes.tactic
4) the tactical thens has been implemented
Other changes:
1) more .mli committed
2) comments and copyright notices added where missing
projects / helm.git / log