Skip to content

Commit

Permalink
Rust examples compiles (#16)
Browse files Browse the repository at this point in the history 
* change Test.rs and Hello.rs to contain real Rust code

* add docs about testing compiled Rust code

* fix Hello.agda after changing Bool to Rgb
  • Loading branch information
@lemastero
lemastero authored Dec 17, 2023
1 parent 5d7e569 commit dcdb272
Show file tree
Hide file tree
Showing 4 changed files with 21 additions and 301 deletions.
14 changes: 11 additions & 3 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,16 +14,24 @@ ghcid
cabal build all
```

* Run
* Compile Rust code

The `test/` directory contains an example compilation of `Test.agda` to `Test.rs`
and `Hello.agda` to `Hello.rs`:

```sh
cabal run -- agda2rust --help
cabal run -- agda2rust ./test/Hello.agda
cabal run -- agda2rust ./test/Test.agda
cabal run -- agda2rust test/Hello.agda
cabal run -- agda2rust test/Test.agda
```
* Testing compiled Rust code

```sh
cd test
rustc --crate-type=lib test/Hello.rs
rustc --crate-type=lib test/Test.rs
```

* Run tests

```sh
Expand Down
13 changes: 3 additions & 10 deletions test/Hello.agda
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,5 @@
module test.Hello where

-- Type with two inhabitants
data Bool : Set where
false true : Bool
{-# COMPILE AGDA2RUST Bool #-}

{- Logical connective not - negation -}
not : Bool -> Bool
not true = false
not false = true
{-# COMPILE AGDA2RUST not #-}
data Rgb : Set where
false Green Blue : Rgb
{-# COMPILE AGDA2RUST Rgb #-}
48 changes: 5 additions & 43 deletions test/Hello.rs
View file
Original file line number Diff line number Diff line change
@@ -1,45 +1,7 @@
*** module test.Hello ***
Bool = Datatype {
dataPars = 0
dataIxs = 0
dataClause = (nothing)
dataCons =
[QName {qnameModule = MName {mnameToList = [Name {nameId = NameId 0 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "test" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "test" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 8, posLine = 1, posCol = 8}, iEnd = Pn {srcFile = (), posPos = 13, posLine = 1, posCol = 13}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False},Name {nameId = NameId 2 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Hello" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Hello" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 13, posLine = 1, posCol = 13}, iEnd = Pn {srcFile = (), posPos = 18, posLine = 1, posCol = 18}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False},Name {nameId = NameId 4 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Bool" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Bool" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 60, posLine = 4, posCol = 6}, iEnd = Pn {srcFile = (), posPos = 64, posLine = 4, posCol = 10}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}]}, qnameName = Name {nameId = NameId 6 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "false" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "false" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 79, posLine = 5, posCol = 3}, iEnd = Pn {srcFile = (), posPos = 84, posLine = 5, posCol = 8}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}},QName {qnameModule = MName {mnameToList = [Name {nameId = NameId 0 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "test" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "test" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 8, posLine = 1, posCol = 8}, iEnd = Pn {srcFile = (), posPos = 13, posLine = 1, posCol = 13}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False},Name {nameId = NameId 2 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Hello" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Hello" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 13, posLine = 1, posCol = 13}, iEnd = Pn {srcFile = (), posPos = 18, posLine = 1, posCol = 18}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False},Name {nameId = NameId 4 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Bool" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Bool" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 60, posLine = 4, posCol = 6}, iEnd = Pn {srcFile = (), posPos = 64, posLine = 4, posCol = 10}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}]}, qnameName = Name {nameId = NameId 8 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "true" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "true" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 85, posLine = 5, posCol = 9}, iEnd = Pn {srcFile = (), posPos = 89, posLine = 5, posCol = 13}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}}]
dataSort = Set
dataMutual = Nothing
dataAbstr = <function>
}
mod hello {

enum Rgb {
Red, Green, Blue
}

not = Function {
funClauses =
|- test.Hello.Bool.true = test.Hello.Bool.false : test.Hello.Bool
|- test.Hello.Bool.false = test.Hello.Bool.true : test.Hello.Bool
funCompiled =
case 0 of
test.Hello.Bool.false -> done[] test.Hello.Bool.true
test.Hello.Bool.true -> done[] test.Hello.Bool.false
funSplitTree =
split at 0
|
+- test.Hello.Bool.false -> done, 0 bindings
|
`- test.Hello.Bool.true -> done, 0 bindings

funTreeless = (nothing)
funInv =
Inverse
ConsHead test.Hello.Bool.false ->
[|- test.Hello.Bool.true = test.Hello.Bool.false : test.Hello.Bool]
ConsHead test.Hello.Bool.true ->
[|- test.Hello.Bool.false = test.Hello.Bool.true : test.Hello.Bool]
funMutual = Just []
funAbstr = ConcreteDef
funProjection = MaybeProjection
funErasure = False
funFlags = fromList []
funTerminates = Just True
funWith = (nothing)
funIsKanOp = (nothing)
funOpaque = TransparentDef
}
}
Loading

0 comments on commit dcdb272

Please sign in to comment.