search

granule-project / granule

A statically-typed linear functional language with graded modal types for fine-grained program reasoning
https://granule-project.github.io
BSD 3-Clause "New" or "Revised" License
589 stars 33 forks source link

One test for granule-frontend fails in 0.9.5.0 #240

Open andreasabel opened 6 months ago

andreasabel commented 6 months ago 
granule-frontend       > Failures:             
granule-frontend       >                       
granule-frontend       >   tests/hspec/Language/Granule/Synthesis/SynthSpec.hs:161:13: 
granule-frontend       >   1) Language.Granule.Synthesis.Synth, Construcor test for Either, Branch on (Left : a -> Either a b)
granule-frontend       >        expected: Size = 1
granule-frontend       >                   - ((T ∧ T) -> ∃ y : Nat . T ∧ T ∧ (y ⊔ y = ub0) ∧ ((1 : Nat) = y * r0) ∧ (y * r0 = r0 * r0))
granule-frontend       >         but got: Size = 1
granule-frontend       >                   - ((T ∧ T) -> ∃ y : Nat . T ∧ T ∧ (y ⊔ y = ub0) ∧ ((1 : Nat) = y * 1) ∧ (y * 1 = r0))
granule-frontend       >                       
granule-frontend       >   To rerun use: --match "/Language.Granule.Synthesis.Synth/Construcor test for Either/Branch on (Left : a -> Either a b)/"
granule-frontend       >                       
granule-frontend       > Randomized with seed 488633885
dorchard commented 5 months ago

Thanks @andreasabel . @jackohughes - this is in the tests for synthesis of case expressions. I started at the expected output and the paper and to me they appear to agree. Any ideas?