lambda_delta: partial commit ...

Composite coercions are now extracted too.

Name mangling until separate extraction is implemented.

Code to make all global names in a file fresh.

Capitalization of variables bound in patterns fixed.

...

Fixed indentation, which is semantic in Haskell.

(Part of previous two commits)

(Part of previous commit)

Extraction is now integrated with the usual machinery for serialization of
commands.

Top used also for fixes.

Match in types handled using top.

Match in types handled using Top.

Dead code removed.

Match in classification of non-terms taken in account.
We take the sup of the classification of all branches according to the
order

`Proposition < `PropKind < `Type < `Kind < `KindOrType

Known bug fixed: the rhs of a match over a small singleton inductive type
needed delifting to take it out its lhs.

progress in uni_step

Basics/logic.ma no longer raises exception.
Many workaround introduced to feed arguments to polymorphically kinded functions.

Bug fixed: when extracting pattern matching on singleton types it is possible
that a type is faced during the computation of the type of its constructor.
Ad-hoc patch added.

...

Fixed pretty-printing of types of variables bound in patterns.

Patterns are now computed according to the extracted constructor type.

pattern arguments where printed in reverse order

Bug fixed: rhs in match were printed in wrong context.

...

...

Code for computing patterns the way Haskell likes them (lhs + rhs).
Currently bugged:
 - some DeBrujin problems in the rhs
 - ignores the extracted type of the constructor (uses the CiC type)
 - does not perform eta-expansion when needed

Fixed pretty-printing of mutual recursive stuff and improved machinery to
pretty print references.

...

1. fixed pretty-printing of constructors, type variables, etc.
2. added UnsafeCoerce to pattern matching in an over-approximating way

Self contained now.

1. added Skip to terms to maintain consistency between Rels and context
   (required for pretty printing)

Fixed left/right context distinction in inductive types.

Pretty printing of context (variable refreshing) fixed.

size_of_type fixed and simplified

No pattern matching over empty types in Haskell

Infos stored for inductive types.

Preliminary extraction of constructors.

BUG: ghc only allows forall quantifications at the beginning of the
 type! Needs re-ordering.

Added kind signatures to data declaration.

1. Dominic:
 - kinds signature in explicit for-all (if not simple kinds)
 - Haskell names of Matita names (still bugged)
 - improved pretty-printing (only necessary brackets)
2. CC types are now extracted to F_omega types even when NotInFOmega
   (exception removed altogether)

End of copy.ma

update of logo completed!

still updating ...

we are updating the logo of lambda_delta ...

sample table for character classes

- Makefile update
- for now the page related to BTM is committed here ...

- renaming complete
- noe file was missing

some renaming ...

we updated the contribution porting it to the new matita ...

Preliminary work on (co)inductive types.

progress

Work in progress.

Adding GRealize to uni_step.

porting to termination

guarded realizability

dependences update

A compiling version (not complete).

Bug fixed: the context generated by l.h.s. binders was appended in wrong order.

...

...

Pretty printing of patterns done almost correctly.

Tentative code for Fixpoint. Still to be completed.

...

Path fixed.

Code extraction branched.

Temporary stuff to test code extraction. Running make produces
extraction.hs which is checked by "ghci extraction.hs"

1. Implemented type inference for Fomega to extract term application correctly.
2. Fixed the Decl classification.

Bugs fixed:
1. the context was processed in reverse order
2. the classification of types was wrong

Bugs related to pretty printing of names fixed (capitalization, name
clashes, etc.). In particular removed binders (propositionals) were sometimes
still counted.

Tests for code extraction; to be moved elsewhere.

Bug fixed: Haskell forces capitalisation.
But still open: name clashes due to capitalisation.

Begin of porting of code extraction to the new Matita.
The file does not belong to the kernel: it will be moved away soon.
The extraction code is not branched yet and it does not need to be compiled.

work in progress

Termination!

Wip

work in progress

update in basic_2

- context free computation for terms and local environments

additions and corrections to basic_2

- support for pointwise extensions of a term relation started ...
- we now support abstract liftable relations

work in progress

work in progress

polarized binders introduced in basic_2

- matita: reset_font_size () added after matita.conf.xml is read to set
the font size specified by the user
- lambda_delta: equivalence between normal forms irreducible terms
proved (context-sensitive version)

one file was missing ...

- lambda_delta: we updated some notation
                we are switching from context-free to context-sensitive reducible terms
- basics/star:  star constructor refl renamed to srefl to avoid name clash with id constructor refl

- we polarized binders to control zeta reduction
- confluence and strong normalization proved

An executable version of the tutorial.

progress in termination of marks.ma

One less warning.

Some debugging times exposed.

Major speed up improvement after every tactic application.
Exponential algorithm (in the size of the sequent) turned into linear.
It only shows for very large sequents though.

Few changes

- intermediate commit to allow debugging of auto tactic in xprs.ma
- extended computation is now defined (its De Vrijer's reduction rt)
- stratified native validity is now defined (it's supposed to be
easier to deal with than native type assignment)

adding tutorial

porting to termination

- we added a time specification in the generated web pages
- update in basic_2

more symbols added for lambda_delta

- dynamic type assignment dismissed for now
- stratified static type assignment and unwind defined

commit by user mkmluser