Extract Java code from Coq specification#1

Open

kirillt wants to merge 36 commits into

Commits on Dec 13, 2013

Java extraction. Only inductives can be extracted now.
Kirill Taran
committed
Some cleanup; type synonyms and plain declarations. Terms are not extracted yet.
Kirill Taran
committed
Pretty-printing of ML expressions throwed away.
Kirill Taran
committed

Commits on Dec 14, 2013

Work on terms extraction started. Mocks and application of global functions are implemented so far.
Kirill Taran
committed
Let-in extraction; dirty implementation of constructor application extraction.
Kirill Taran
committed
Tiny fix with redundant space.
Kirill Taran
committed

Commits on Dec 16, 2013

Pattern matching extraction.
Kirill Taran
committed
Dirty generation of toString methods.
Kirill Taran
committed
Tiny fix.
Kirill Taran
committed

Commits on Dec 17, 2013

Little fixes: arguments order in environment and redundant space.
Kirill Taran
committed
Little fix with qualified names.
Kirill Taran
committed

Commits on Dec 18, 2013

Small fixes.
Kirill Taran
committed
Again small fixes. Brackets around expression with mt () are necessary.
Kirill Taran
committed
Arrow types, lambda representation and currying.
Kirill Taran
committed
Dirty implementation of application of non-global values.
Kirill Taran
committed
Todo: type parameters instantiation.
Kirill Taran
committed

Commits on Dec 19, 2013

Global values declaration. TODO: refactor copy-paste, etc.
Kirill Taran
committed

Commits on Dec 30, 2013

Commits on Dec 31, 2013

Cleaning.
Kirill Taran
committed

Commits on Jan 9, 2014

Possibility of saving inferred types in AST for usage in Java.
Kirill Taran
committed

Commits on Jan 12, 2014

Usage of types promotion: instantiation of generics and lambda terms are OK. There is strange code generated for complex nested patterns.
Kirill Taran
committed

Commits on Jan 13, 2014

Fixing some bugs with MLtyped.
Kirill Taran
committed

Commits on Jan 14, 2014

MLtyped bug fixed (again).
Kirill Taran
committed

Commits on Jan 15, 2014

Fix of bug with broken streams in pattern matching.
Kirill Taran
committed
Some mocking and insertion of Java into extraction test-suite.
Kirill Taran
committed

Commits on Jan 22, 2014

Tiny fix.
Kirill Taran
committed

Commits on Jan 26, 2014

Fixed bug with lack of MLtyped at pattern matching with wildcard and constructor (iter_mltyped -> map_mltyped). Some enhacements.
Kirill Taran
committed
Some enhacements.
Kirill Taran
committed

Commits on Jan 27, 2014

Non-function constants now are extracted the same way as functions (via lambda() and apply() method, but without arguments). There was bug with old representation.
Kirill Taran
committed

Commits on Jan 28, 2014

Potential bug with Tmeta fixed.
Kirill Taran
committed
Tiny fix.
Kirill Taran
committed
Tiny refactoring.
Kirill Taran
committed
Awful implementation of mutually recursive definitions (TODO: remove copy-paste and hacks).
Kirill Taran
committed
Reimplementation of methods generation. Proper mutual fix generation. Now methods with from 0 to N arguments generated for any N-ary function (this simplifies future generation due possibility not …
Kirill Taran
committed

Commits on Mar 7, 2025

Thesis paper and slides (2014)
kirillt
committed