From 207c50c07d01cd53e3647fac3a423906ce1bdf25 Mon Sep 17 00:00:00 2001 From: lemastero Date: Sun, 17 Dec 2023 14:16:51 +0100 Subject: [PATCH] change Test.rs and Hello.rs to contain real Rust code --- test/Hello.agda | 11 +-- test/Hello.rs | 48 +--------- test/Test.rs | 247 +----------------------------------------------- 3 files changed, 9 insertions(+), 297 deletions(-) diff --git a/test/Hello.agda b/test/Hello.agda index c2f5c50..0bdb43f 100644 --- a/test/Hello.agda +++ b/test/Hello.agda @@ -1,12 +1,5 @@ module test.Hello where --- Type with two inhabitants -data Bool : Set where - false true : Bool +data Red : Set where + false Green Blue : Bool {-# COMPILE AGDA2RUST Bool #-} - -{- Logical connective not - negation -} -not : Bool -> Bool -not true = false -not false = true -{-# COMPILE AGDA2RUST not #-} diff --git a/test/Hello.rs b/test/Hello.rs index 1a65987..6df1881 100644 --- a/test/Hello.rs +++ b/test/Hello.rs @@ -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 = - } +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 - } +} diff --git a/test/Test.rs b/test/Test.rs index fb6e37b..51a7f12 100644 --- a/test/Test.rs +++ b/test/Test.rs @@ -1,245 +1,2 @@ -*** module Test *** - - -Exp = Datatype { - dataPars = 1 - dataIxs = 0 - dataClause = (nothing) - dataCons = - [QName {qnameModule = MName {mnameToList = [Name {nameId = NameId 0 (ModuleNameHash 10189251152579365012), 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 = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 8, posLine = 1, posCol = 8}, iEnd = Pn {srcFile = (), posPos = 9, posLine = 1, posCol = 9}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False},Name {nameId = NameId 8 (ModuleNameHash 10189251152579365012), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Exp" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Exp" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 175, posLine = 10, posCol = 6}, iEnd = Pn {srcFile = (), posPos = 178, posLine = 10, posCol = 9}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}]}, qnameName = Name {nameId = NameId 12 (ModuleNameHash 10189251152579365012), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Plus" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Plus" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 203, posLine = 11, posCol = 3}, iEnd = Pn {srcFile = (), posPos = 207, posLine = 11, posCol = 7}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}},QName {qnameModule = MName {mnameToList = [Name {nameId = NameId 0 (ModuleNameHash 10189251152579365012), 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 = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 8, posLine = 1, posCol = 8}, iEnd = Pn {srcFile = (), posPos = 9, posLine = 1, posCol = 9}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False},Name {nameId = NameId 8 (ModuleNameHash 10189251152579365012), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Exp" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Exp" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 175, posLine = 10, posCol = 6}, iEnd = Pn {srcFile = (), posPos = 178, posLine = 10, posCol = 9}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}]}, qnameName = Name {nameId = NameId 14 (ModuleNameHash 10189251152579365012), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Int" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Int" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 234, posLine = 12, posCol = 3}, iEnd = Pn {srcFile = (), posPos = 237, posLine = 12, posCol = 6}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}},QName {qnameModule = MName {mnameToList = [Name {nameId = NameId 0 (ModuleNameHash 10189251152579365012), 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 = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 8, posLine = 1, posCol = 8}, iEnd = Pn {srcFile = (), posPos = 9, posLine = 1, posCol = 9}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False},Name {nameId = NameId 8 (ModuleNameHash 10189251152579365012), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Exp" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Exp" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 175, posLine = 10, posCol = 6}, iEnd = Pn {srcFile = (), posPos = 178, posLine = 10, posCol = 9}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}]}, qnameName = Name {nameId = NameId 16 (ModuleNameHash 10189251152579365012), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Var" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Var" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 254, posLine = 13, posCol = 3}, iEnd = Pn {srcFile = (), posPos = 257, posLine = 13, posCol = 6}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}}] - dataSort = Set - dataMutual = - Just [QName {qnameModule = MName {mnameToList = [Name {nameId = NameId 0 (ModuleNameHash 10189251152579365012), 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 = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 8, posLine = 1, posCol = 8}, iEnd = Pn {srcFile = (), posPos = 9, posLine = 1, posCol = 9}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}]}, qnameName = Name {nameId = NameId 8 (ModuleNameHash 10189251152579365012), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Exp" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Exp" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 175, posLine = 10, posCol = 6}, iEnd = Pn {srcFile = (), posPos = 178, posLine = 10, posCol = 9}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}}] - dataAbstr = - } - - - -eval = Function { - funClauses = - {a : Set} (env : @0 -> Agda.Builtin.Nat.Nat) (a : Test.Exp @1) - (b : Test.Exp @2) |- - {a = _@3} env@2 (Test.Exp.Plus a@1 b@0) = - Agda.Builtin.Nat._+_ - (Test.eval {@3} @2 @1) (Test.eval {@3} @2 @0) : - Agda.Builtin.Nat.Nat - {a : Set} (env : @0 -> Agda.Builtin.Nat.Nat) - (n : Agda.Builtin.Nat.Nat) |- - {a = _@2} env@1 (Test.Exp.Int n@0) = @0 : Agda.Builtin.Nat.Nat - {a : Set} (env : @0 -> Agda.Builtin.Nat.Nat) (x : @1) |- - {a = _@2} env@1 (Test.Exp.Var x@0) = @1 @0 : Agda.Builtin.Nat.Nat - funCompiled = - case 2 of - Test.Exp.Plus -> - done[{_}, env, a, b] - Agda.Builtin.Nat._+_ (Test.eval {@3} @2 @1) (Test.eval {@3} @2 @0) - Test.Exp.Int -> done[{_}, env, n] @0 - Test.Exp.Var -> done[{_}, env, x] @1 @0 - funSplitTree = - split at 2 -| -+- Test.Exp.Plus -> done, 4 bindings -| -+- Test.Exp.Int -> done, 3 bindings -| -`- Test.Exp.Var -> done, 3 bindings - - funTreeless = (nothing) - funInv = NotInjective - funMutual = - Just [QName {qnameModule = MName {mnameToList = [Name {nameId = NameId 0 (ModuleNameHash 10189251152579365012), 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 = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 8, posLine = 1, posCol = 8}, iEnd = Pn {srcFile = (), posPos = 9, posLine = 1, posCol = 9}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}]}, qnameName = Name {nameId = NameId 18 (ModuleNameHash 10189251152579365012), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "eval" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "eval" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 299, posLine = 16, posCol = 1}, iEnd = Pn {srcFile = (), posPos = 303, posLine = 16, posCol = 5}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}}] - funAbstr = ConcreteDef - funProjection = MaybeProjection - funErasure = False - funFlags = fromList [] - funTerminates = Just True - funWith = (nothing) - funIsKanOp = (nothing) - funOpaque = TransparentDef - } -sum = Function { - funClauses = - |- Agda.Builtin.List.List.[] = 0 : Agda.Builtin.Nat.Nat - (x : Agda.Builtin.Nat.Nat) - (xs : Agda.Builtin.List.List {lzero} Agda.Builtin.Nat.Nat) |- - (Agda.Builtin.List.List._∷_ x@1 xs@0) = - Agda.Builtin.Nat._+_ @1 (Test.sum @0) : Agda.Builtin.Nat.Nat - funCompiled = - case 0 of - Agda.Builtin.List.List.[] -> done[] 0 - Agda.Builtin.List.List._∷_ -> - done[x, xs] Agda.Builtin.Nat._+_ @1 (Test.sum @0) - funSplitTree = - split at 0 -| -+- Agda.Builtin.List.List.[] -> done, 0 bindings -| -`- Agda.Builtin.List.List._∷_ -> done, 2 bindings - - funTreeless = (nothing) - funInv = - Inverse - ConsHead Agda.Builtin.Nat.Nat.zero -> - [|- Agda.Builtin.List.List.[] = 0 : Agda.Builtin.Nat.Nat] - UnknownHead -> - [(x : Agda.Builtin.Nat.Nat) - (xs : Agda.Builtin.List.List {lzero} Agda.Builtin.Nat.Nat) |- - (Agda.Builtin.List.List._∷_ x@1 xs@0) = - Agda.Builtin.Nat._+_ @1 (Test.sum @0) : Agda.Builtin.Nat.Nat] - funMutual = - Just [QName {qnameModule = MName {mnameToList = [Name {nameId = NameId 0 (ModuleNameHash 10189251152579365012), 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 = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 8, posLine = 1, posCol = 8}, iEnd = Pn {srcFile = (), posPos = 9, posLine = 1, posCol = 9}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}]}, qnameName = Name {nameId = NameId 34 (ModuleNameHash 10189251152579365012), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "sum" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "sum" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 475, posLine = 24, posCol = 1}, iEnd = Pn {srcFile = (), posPos = 478, posLine = 24, posCol = 4}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}}] - funAbstr = ConcreteDef - funProjection = MaybeProjection - funErasure = False - funFlags = fromList [] - funTerminates = Just True - funWith = (nothing) - funIsKanOp = (nothing) - funOpaque = TransparentDef - } -_++_ = Function { - funClauses = - {a : Set} (ys : Agda.Builtin.List.List {lzero} @0) |- - {a = _@1} Agda.Builtin.List.List.[] ys@0 = - @0 : Agda.Builtin.List.List {lzero} @1 - {a : Set} (x : @0) (xs : Agda.Builtin.List.List {lzero} @1) - (ys : Agda.Builtin.List.List {lzero} @2) |- - {a = _@3} (Agda.Builtin.List.List._∷_ x@2 xs@1) ys@0 = - Agda.Builtin.List.List._∷_ @2 (Test._++_ {@3} @1 @0) : - Agda.Builtin.List.List {lzero} @3 - funCompiled = - case 1 of - Agda.Builtin.List.List.[] -> done[{_}, ys] @0 - Agda.Builtin.List.List._∷_ -> - done[{_}, x, xs, ys] - Agda.Builtin.List.List._∷_ @2 (Test._++_ {@3} @1 @0) - funSplitTree = - split at 1 -| -+- Agda.Builtin.List.List.[] -> done, 2 bindings -| -`- Agda.Builtin.List.List._∷_ -> done, 4 bindings - - funTreeless = (nothing) - funInv = - Inverse - ConsHead Agda.Builtin.List.List._∷_ -> - [{a : Set} (x : @0) (xs : Agda.Builtin.List.List {lzero} @1) - (ys : Agda.Builtin.List.List {lzero} @2) |- - {a = _@3} (Agda.Builtin.List.List._∷_ x@2 xs@1) ys@0 = - Agda.Builtin.List.List._∷_ @2 (Test._++_ {@3} @1 @0) : - Agda.Builtin.List.List {lzero} @3] - VarHead 2 -> - [{a : Set} (ys : Agda.Builtin.List.List {lzero} @0) |- - {a = _@1} Agda.Builtin.List.List.[] ys@0 = - @0 : Agda.Builtin.List.List {lzero} @1] - funMutual = - Just [QName {qnameModule = MName {mnameToList = [Name {nameId = NameId 0 (ModuleNameHash 10189251152579365012), 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 = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 8, posLine = 1, posCol = 8}, iEnd = Pn {srcFile = (), posPos = 9, posLine = 1, posCol = 9}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}]}, qnameName = Name {nameId = NameId 40 (ModuleNameHash 10189251152579365012), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Hole :| [Id "++",Hole]}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Hole :| [Id "++",Hole]}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 597, posLine = 31, posCol = 1}, iEnd = Pn {srcFile = (), posPos = 601, posLine = 31, posCol = 5}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}}] - funAbstr = ConcreteDef - funProjection = MaybeProjection - funErasure = False - funFlags = fromList [] - funTerminates = Just True - funWith = (nothing) - funIsKanOp = (nothing) - funOpaque = TransparentDef - } -map = Function { - funClauses = - {a : Set} {b : Set} (f : @1 -> @0) |- - {a = _@2} {b = _@1} f@0 Agda.Builtin.List.List.[] = - Agda.Builtin.List.List.[] : Agda.Builtin.List.List {lzero} @1 - {a : Set} {b : Set} (f : @1 -> @0) (x : @2) - (xs : Agda.Builtin.List.List {lzero} @3) |- - {a = _@4} {b = _@3} f@2 (Agda.Builtin.List.List._∷_ x@1 xs@0) = - Agda.Builtin.List.List._∷_ (@2 @1) (Test.map {@4} {@3} @2 @0) : - Agda.Builtin.List.List {lzero} @3 - funCompiled = - case 3 of - Agda.Builtin.List.List.[] -> - done[{_}, {_}, f] Agda.Builtin.List.List.[] - Agda.Builtin.List.List._∷_ -> - done[{_}, {_}, f, x, xs] - Agda.Builtin.List.List._∷_ (@2 @1) (Test.map {@4} {@3} @2 @0) - funSplitTree = - split at 3 -| -+- Agda.Builtin.List.List.[] -> done, 3 bindings -| -`- Agda.Builtin.List.List._∷_ -> done, 5 bindings - - funTreeless = (nothing) - funInv = - Inverse - ConsHead Agda.Builtin.List.List.[] -> - [{a : Set} {b : Set} (f : @1 -> @0) |- - {a = _@2} {b = _@1} f@0 Agda.Builtin.List.List.[] = - Agda.Builtin.List.List.[] : Agda.Builtin.List.List {lzero} @1] - ConsHead Agda.Builtin.List.List._∷_ -> - [{a : Set} {b : Set} (f : @1 -> @0) (x : @2) - (xs : Agda.Builtin.List.List {lzero} @3) |- - {a = _@4} {b = _@3} f@2 (Agda.Builtin.List.List._∷_ x@1 xs@0) = - Agda.Builtin.List.List._∷_ (@2 @1) (Test.map {@4} {@3} @2 @0) : - Agda.Builtin.List.List {lzero} @3] - funMutual = - Just [QName {qnameModule = MName {mnameToList = [Name {nameId = NameId 0 (ModuleNameHash 10189251152579365012), 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 = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 8, posLine = 1, posCol = 8}, iEnd = Pn {srcFile = (), posPos = 9, posLine = 1, posCol = 9}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}]}, qnameName = Name {nameId = NameId 50 (ModuleNameHash 10189251152579365012), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "map" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "map" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/home/omelkonian/git/agda-minimal-backend/Test.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 10189251152579365012, moduleNameParts = "Test" :| []})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 711, posLine = 36, posCol = 1}, iEnd = Pn {srcFile = (), posPos = 714, posLine = 36, posCol = 4}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}}] - funAbstr = ConcreteDef - funProjection = MaybeProjection - funErasure = False - funFlags = fromList [] - funTerminates = Just True - funWith = (nothing) - funIsKanOp = (nothing) - funOpaque = TransparentDef - } -plus3 = Function { - funClauses = - |- - = Test.map - {Agda.Builtin.Nat.Nat} {Agda.Builtin.Nat.Nat} - (λ n -> Agda.Builtin.Nat._+_ @0 3) : - Agda.Builtin.List.List {lzero} Agda.Builtin.Nat.Nat -> - Agda.Builtin.List.List {lzero} Agda.Builtin.Nat.Nat - funCompiled = - done[] - Test.map - {Agda.Builtin.Nat.Nat} {Agda.Builtin.Nat.Nat} - (λ n -> Agda.Builtin.Nat._+_ @0 3) - funSplitTree = done, 1 bindings - - funTreeless = (nothing) - funInv = NotInjective - funMutual = Just [] - funAbstr = ConcreteDef - funProjection = MaybeProjection - funErasure = False - funFlags = fromList [] - funTerminates = Just True - funWith = (nothing) - funIsKanOp = (nothing) - funOpaque = TransparentDef - } -doubleLambda = Function { - funClauses = - |- - = λ a -> - λ b -> Agda.Builtin.Nat._+_ @1 (Agda.Builtin.Nat._*_ 2 @0) : - Agda.Builtin.Nat.Nat -> - Agda.Builtin.Nat.Nat -> Agda.Builtin.Nat.Nat - funCompiled = - done[] - λ a -> λ b -> Agda.Builtin.Nat._+_ @1 (Agda.Builtin.Nat._*_ 2 @0) - funSplitTree = done, 2 bindings - - funTreeless = (nothing) - funInv = NotInjective - funMutual = Just [] - funAbstr = ConcreteDef - funProjection = MaybeProjection - funErasure = False - funFlags = fromList [] - funTerminates = Just True - funWith = (nothing) - funIsKanOp = (nothing) - funOpaque = TransparentDef - } +mod test { +}