Fixing of guarded_by_constructors completed.
This is the idea of the implementation:
1) The guarded_by_constructors is called on a term which is going to produce
an inductive type (in every branch).
2) The guarded_by_constructors now has also a parameter which is the list
of arguments that are applied to the inductive type that the term
we are cheking is going to produce.
3) Once the constructor is found, its type is "applied" to the list of
arguments its inductive type is applied to. This operation gives us
an instantiated constructor type.
4) Depending on the type of every argument in the instantiated constructor
type, we call either the does_not_occur or the guarded_by_constructors
on every term the constructor is applied to. In case we call the
guarded_by_constructors, we also compute the new parameter (list of
arguments the new inductive type was applied to).
Note that the analysis of the type of the constructors is based very closely
on the analysis of positivy of an inductive type.
Note also that some cases (e.g. a MutCase, a Fix or a CoFix in head position
in the backbone of the type of a constructor) has not been considered and
raises an exception.
PARTIAL COMMIT:
The whole logic of the guarded_by_constructors is being changed.
The new idea is this one:
1) The guarded_by_constructors is applied to a term t which must always
generate an inhabitant of an inductive data type or of a co-inductive
data type.
2) When it find a constructor in head position, then the constructor
must construct the inductive or co-inductive data type of 1).
3) The type of the formal parameter of a constructor determines what
condition is checked on the actual parameters of the constructors:
a) Not recursive: the function must not occur in the actual parameter
b) Simply recursive (to be defined): the function must occur in the
actual parameter only guarded by constructors (where the constructor
has already been found).
c) Imbricated (i.e. it is another inductive type applied to the one
that is going to be recursively defined): in this case the guarded
by constructors (where the constructor has already been found) must
be called, but:
I) the expected inductive data type is no more the old one, but
the one of the inductive data type that is in head position in
the type.
II) Once (if) one constructor of I) will be found, its type must
be considered only after the substitution of the left (?)
parameters and considering recursion IN THE CO-INDUCTIVE TYPE
THAT IS THE OUTPUT TYPE OF THE WHOLE COFIX.
What is still wrong with this commit is that we don't have the notion of
imbricated argument yet. So, as soon as an imbricated argument is found,
the invariant 1-3 are broken and sooner or later an exception is raised
or false is returned.
Irene Schena [Mon, 10 Dec 2001 16:28:04 +0000 (16:28 +0000)]
----------------------------------------------------------------------
Modified Files:
1) schema-h.rdf, schema-hth.rdf: updated DC schemas + class and
property refinements + value types.
----------------------------------------------------------------------
Bug partially fixed: the branch of a case of type Prod can be not a Lambda.
(e.g. a Rel, a MutConstruct, etc.) I have fixed only the two cases of a
Rel and a MutConstruct.
The definition of small inductive types has been relaxed: a constructor
is now considered small when its type without the parameters was small
with the previous definition. This is consistent with Coq's behaviour.
* Code improvement: there were two different functions both named eat_prods.
One has been renamed drop_prods.
* Bug fix: decast was still too weak. Replaced by CicReduction.whd everywhere.
Irene Schena [Mon, 3 Dec 2001 16:17:59 +0000 (16:17 +0000)]
----------------------------------------------------------------------
Added Files:
1) schema-h.rdf, schema-hth.rdf: first draft of rdf schemas for objects
and theories
----------------------------------------------------------------------
New implementation of the proof-checker daemon: there is now
only one sequential (= non concurrent) proof-checker that process
one request at a time. The next big step will be to make it re-entrant.
A .cmo file inside a .cma is linked iff it is referenced at least once.
This was not the case for cicCooking, that simply worked using side-effects
(i.e. registering one function of him to cicEnvironment).
So, I have created a new init function to initialize the wall proof-checker.
META files are now automatically generated from META-*.src files.
In this way all the hard-coded file paths have been removed.
Installation and uninstallation (still not implemented) should be also
easier.
Moreover, an error in a sub-directory now stops the whole processing.
Debianize.helm stuff.
Now you can check out a cvs revision and obtain a *clean* debianized source
tree executing "debian/debianize.helm".
Moreover the generated debian packages are native debian packages.
BUG FIXED:
An maction with only one child does not have the same semantic
of an mrow. E.g.: when I click to un-expand a node, the first enclosing
maction is the one I am acting on. If it has only one child, nothing
happens. So, if an maction with only one child is put inside an maction with
two children, the inner one stops any possibility to unexpand the outer one.
projects / helm.git / log