[WIP] Adding agda system and agda checking script

Deducteam / Logipedia

An encyclopedia of proofs

57 stars 11 forks source link

[WIP] Adding agda system and agda checking script #35

Open tdelort opened 4 years ago

tdelort commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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