Skip to content

Latest commit

 

History

History
100 lines (68 loc) · 3.1 KB

changes.md

File metadata and controls

100 lines (68 loc) · 3.1 KB

Change notes

2014-05-21. Formalization in Coq. Export to Coq

A new statement in TT Lite REPL exportCoq. It works similar to exportToAgda.

2013-12-06. Import/Reload autocomplete.

Start type import " or reload " and you will have file name auto-completion via tab. Note that you need to type the first quote.

Syntax Error

2013-11-27. Formalization in Agda. Export to Agda.

A new statement in TT Lite REPL exportToAgda. Command exportToAgda exports all definitions in the current scope as Agda module. The syntax is

exportToAgda moduleName;

moduleName is a name of an Agda module which will be created in the directory generated (it is hardcoded for now).

Here is an example of its usage (see examples/test/agda/map.hs):

map =
    \ (A : Set) (B : Set) (f : forall (_ : A). B) (xs : List A) ->
        elim
            (List A)
            (\ (_ : List A) -> List B)
            (Nil (List B))
            (\ (h : A) (t : List A) (rec : List B) -> Cons (List B) (f h) rec )
            xs;

exportToAgda map;

Executing this file results in creation of the file generated/map.agda with the following content (up to formatting):

open import ttlite

module map where

map : forall
        (a : Set0)
        (b : Set0)
        (c : forall (c : a) ->  b)
        (d : List a) -> 
        List b
map = \ (a : Set0) (b : Set0) (c : forall (c : a) ->  b) (d : List a) -> 
        elimList 
            a 
            (\ (e : List a) -> List b) 
            (nil b)
            (\ (e : a) -> \ (f : List a) -> \ (g : List b) -> cons b (c e) g)
            d

The module ttlite.agda contains a definition of TT Lite types in Agda settings.

The file map.agda from the example can be checked by Agda compiler using following command (from the project directory):

agda -i generated/ -i doc/ generated/${module}.agda

Assumed variable are exported as module parameters.

Example (examples/test/agda/assumed.hs):

$A : Set;
listA = List $A;
$L2 : List listA;

g = \ (xs : List listA) -> $L2;

exportToAgda assumed;

The result of export (/generated/assumed.agda):

open import ttlite

module assumed ($A : Set0) ($L2 : List (List $A)) where

listA : Set0
listA = List $A

g : forall (a : List (List $A)) ->  List (List $A)
g = \ (a : List (List $A)) -> $L2

Definitions (transformed program and a proof of correctness) generated by supercompilation can be exported as well.

Thus this feature enables type-checking to be performed independently of TT Lite, so that the proofs of correctness produced by TT Lite can be verified by Agda.

There is a bunch of integration tests in the project. See TTLiteExportSpec and TTLiteScExportSpec for details. You can run them from sbt console using it:test. (Tests assumes that you have agda executable).