[WIP] Adding agda system and agda checking script

[tdelort]

Changes

Agda.ml script added in src/sttfa/export and src/core/systems.ml, src/sttfa/exporter.ml and utils/export.sh file changed to allow exporting to agda.
Checking script at utils/checking/agda.sh also added.

WIP

It is still a work in progress since the exported files don't type check without --type-in-type which makes agda inconsistent, and -W noMissingDefinitions because symbols And, Not, Or, False, True, ex, equals don't have a definition.
This exporter has only been tested on arith_fermat/ but not on opentheory_stdlib/

[francoisthire]

So far, it seems correct. However, it is not clear to me what we want on the long run.

Right now, all the translations from sttfa to * are total functions, with Agda it can't be true. In particular, this means we accept to produce ill-typed Agda files.

What are your plans to overcome the universe issue?

[tdelort]

I'll see if I can use Universe Polymorphism to get rid of this problem, first by repairing by hand the files where --type-in-type needs to be used, and then finding a generic way to implement it into agda.ml.

For the -W noMissingDefinition Warning, a quick fix would be to set symbols that need a definition to postulate too. (Parameter as well as Axiom from the ast as postulate).

[tdelort]

This new version doesn't work on its own. You need to :

• Change the Set Levels by hand (for example with those given by Coq Print Sorted Universes. on the Coq version (with Prop changed to Type))
• Some axioms cannot be set universe polymorphic or Agda will not be able to infer the level. But they are used on many levels. I used Lift from the Agda stdlib to fix these problems by hand.

Set levels can't be left to _ since Agda won't be able to infer the level with this version.

One version that works is to use {-# OPTIONS --cumulativity #-} and getting the Level of the universes from Coq. To avoid cumulativity, one could instead use Lift from the Agda stdlib.

I linked files that type-check using this translation and these rules to this comment.
some_files_that_type_check.zip