Comments (6)
jfdm
commented on August 16, 2024
@ahmadsalim AVL Trees are lossy somewhere.
from idris-containers.
jfdm
commented on August 16, 2024
Actually, i might be wrong in thinking the implementation is wrong.
Yesterday, I added mroe random test data and it appeared that nodes were being dropped, however, the test data had duplicate entries. I have added better more uniquely random test data and things are passing. However, when running tests I get this warn reach error. This might be the cause of the segfault I am getting in another program that uses the tree code. This doesn't show up during installation.
Data.AVL.Tree.AVLNode: inaccessible arguments reachable:
n from PE_insert_5cf1649a arg# 4, Data.AVL.Tree.insert arg# 6, Data.AVL.Tree.rotLeft arg# 6, Data.AVL.Tree.rotRight arg# 5, with block in Data.AVL.Tree.update arg# 10
l from Data.AVL.Tree.rotLeft arg# 6
m from PE_insert_5cf1649a arg# 4, Data.AVL.Tree.insert arg# 6, Data.AVL.Tree.rotLeft arg# 6, Data.AVL.Tree.rotRight arg# 5, with block in Data.AVL.Tree.update arg# 10
r from Data.AVL.Tree.rotRight arg# 5
Data.AVL.Tree.Balanced: inaccessible arguments reachable:
n from Data.AVL.Tree.rotLeft arg# 6, Data.AVL.Tree.rotRight arg# 5
Prelude.Pairs.Element: inaccessible arguments reachable:
pf from PE_insert_5cf1649a arg# 4, Data.AVL.Tree.insert arg# 6, Data.AVL.Tree.rotLeft arg# 5, Data.AVL.Tree.rotLeft arg# 6, Data.AVL.Tree.rotRight arg# 5, Data.AVL.Tree.rotRight arg# 6, Data.AVL.Tree.update arg# 6, with block in with block in Data.AVL.Tree.insert arg# 9, with block in with block in Data.AVL.Tree.insert arg# 11, with block in with block in Data.AVL.Tree.update arg# 9, with block in with block in Data.AVL.Tree.update arg# 11
Data.AVL.Tree.LHeavy: inaccessible arguments reachable:
n from Data.AVL.Tree.rotLeft arg# 6
Data.AVL.Tree.RHeavy: inaccessible arguments reachable:
n from Data.AVL.Tree.rotRight arg# 5
Data.AVL.Tree.rotLeft: inaccessible arguments reachable:
n (no more information available)
Data.AVL.Tree.rotRight: inaccessible arguments reachable:
n (no more information available)
Data.AVL.Tree.height, height': inaccessible arguments reachable:
m (no more information available)
from idris-containers.
david-christiansen
commented on August 16, 2024
Reachability errors shouldn't make your code segfault - they should just make it eat memory and be slow. They're a sign that you've used something at runtime that was declared to be compile-time only, and therefore it had to persist into the compiled code. Here, it looks like your tests are pattern-matching on the depth of the tree at some point.
from idris-containers.
ahmadsalim
commented on August 16, 2024
@jfdm @david-christiansen It might also be because I might need the height of the tree to be actually be stored in the actual tree (and not the invariant). I will take a look on how this can be improved soon.
from idris-containers.
ahmadsalim
commented on August 16, 2024
It might also be nice to separate the proofs from the core operations, so I may also add that to the TODO list.
from idris-containers.
jfdm
commented on August 16, 2024
Just an update, I found out why my code was segfaulting. It definitely wasn't due to the containers code. It was related to the use of type-classes and over-patched code. See issue idris-lang/Idris-dev#2406. Panic over!
Also @ahmadsalim don't chase this up to much
from idris-containers.
Related Issues (13)
- Unnecessary constraints in Data.AVL.Tree HOT 1
- Dependent AVL Tree is Broken HOT 1
- Data.AVL.Tree.avlUpdate looks very wrong HOT 8
- Traversable instance for Dict HOT 1
- AVL Tree and Dict functions are not total in Idris 1.0 HOT 2
- Equality for Set HOT 3
- (lookup k (insert k v dict) dict) = Just v? HOT 3
- Can't build with Idris 1.3.2: Erasure/getArity: definition not found for Data.Tree.Empty
- Error building RedBlack tree with Idris 1.3.3
- RedBlack Trees
- Testing needs improvement.
- Improve queues HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from idris-containers.