diff --git a/src/Demo/Lib.hs b/src/Demo/Lib.hs index a4420e9..d08929b 100644 --- a/src/Demo/Lib.hs +++ b/src/Demo/Lib.hs @@ -16,7 +16,7 @@ elts (x:xs) = singleton x `union` elts xs {-@ rev :: xs:_ -> {v:_ | elts v == elts xs} @-} rev :: [a] -> [a] -rev = go [] +rev = go [] where {-@ go :: acc:_ -> xs:_ -> {v:_ | elts v == union (elts acc) (elts xs)} @-} go acc [] = acc diff --git a/stack.yaml b/stack.yaml index 597751b..986a4b3 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,20 +1,23 @@ -resolver: lts-20.1 +# resolver: lts-20.1 +resolver: nightly-2024-01-26 + packages: - . extra-deps: - - hashable-1.3.5.0 - - rest-rewrite-0.4.1 - - smtlib-backends-0.3 - - smtlib-backends-process-0.3 + - store-0.7.18@sha256:af32079e0d31413b97a1759f8ad8555507857cd4ac4015e195fb5b0a27a3ce9f,8159 + - store-core-0.4.4.7@sha256:a2ea427ff0dde30252474dcb0641cb6928cb8a93cd5ee27d4c22adba8e729683,1489 + - rest-rewrite-0.4.3 + - smtlib-backends-0.3@rev:2 + - smtlib-backends-process-0.3@rev:2 - git: https://github.com/ucsd-progsys/liquidhaskell - commit: fc4a89b91fad8b7a02b72901381d4358a470e230 + commit: 4b20537529b2143cab0214564422c94fb93df9d9 subdirs: - . - liquidhaskell-boot - liquid-prelude - liquid-vector - git: https://github.com/ucsd-progsys/liquid-fixpoint - commit: eb339f9abdf073f8d9f0c446c309006fdf49ed42 + commit: 5b39f1a3c49190f9e438f9cdefd7d2635c5bf7f2 nix: packages: [cacert, git, hostname, z3] diff --git a/stack.yaml.lock b/stack.yaml.lock index 9aa3590..b176c39 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -5,95 +5,106 @@ packages: - completed: - subdir: . - name: liquidhaskell - version: 0.8.10.7.1 - git: https://github.com/ucsd-progsys/liquidhaskell + hackage: store-0.7.18@sha256:af32079e0d31413b97a1759f8ad8555507857cd4ac4015e195fb5b0a27a3ce9f,8159 pantry-tree: - size: 327940 - sha256: f4ed5616abda8f6d2367efa18841907cf0ac0ac55a78a811918f7286a0de3c14 - commit: a4f2198f894810a729feb0f8d06301790ee8d1fb + sha256: 6e9fb2c1c59a9f2fb62abd0016841417b57b9a3e045088d48d65cc740cb1eeb9 + size: 1292 original: - subdir: . - git: https://github.com/ucsd-progsys/liquidhaskell - commit: a4f2198f894810a729feb0f8d06301790ee8d1fb + hackage: store-0.7.18@sha256:af32079e0d31413b97a1759f8ad8555507857cd4ac4015e195fb5b0a27a3ce9f,8159 +- completed: + hackage: store-core-0.4.4.7@sha256:a2ea427ff0dde30252474dcb0641cb6928cb8a93cd5ee27d4c22adba8e729683,1489 + pantry-tree: + sha256: 67828df739695d14f81cd572a3085c76f65ac75f8417095afef8dfb2815f523e + size: 271 + original: + hackage: store-core-0.4.4.7@sha256:a2ea427ff0dde30252474dcb0641cb6928cb8a93cd5ee27d4c22adba8e729683,1489 - completed: - subdir: liquid-base - name: liquid-base - version: 4.14.3.0 + hackage: rest-rewrite-0.4.3@sha256:915fb98b8c0a0f518c1a4b75bcf3ae27a3ebd5b10d60cc16a216c2fca2148ab0,3929 + pantry-tree: + sha256: 4de44fbeb7bd655caeafe605406c0bc5fe1788d9cf37cdac2f18b018ee4cf5e6 + size: 4075 + original: + hackage: rest-rewrite-0.4.3 +- completed: + hackage: smtlib-backends-0.3@sha256:a947aead99f6a314833bddca9b502d5faea8d3bd2fc76ffb53c34d5c5b7557bc,1211 + pantry-tree: + sha256: 97b88a647ac996808a93b2eab62e9e8574d9b9a451ee37a9103e209b63be012d + size: 275 + original: + hackage: smtlib-backends-0.3@rev:2 +- completed: + hackage: smtlib-backends-process-0.3@sha256:caf131d3d6f6825e3a3182713130a8e14d0bd6530eeda643e8a511b546ff1a26,1676 + pantry-tree: + sha256: 7147fef29b4270275168a285fc0c68784329d1276ab9e44e9a45f8d79b526220 + size: 461 + original: + hackage: smtlib-backends-process-0.3@rev:2 +- completed: + commit: 4b20537529b2143cab0214564422c94fb93df9d9 git: https://github.com/ucsd-progsys/liquidhaskell + name: liquidhaskell pantry-tree: - size: 15057 - sha256: ec6292884597585ab0a007b242bf5c711466a9b91fd5f3b2fbcac3602594f140 - commit: a4f2198f894810a729feb0f8d06301790ee8d1fb + sha256: 9211c87ebc9f044a017c7ea04b81f391fed0d5ac02813c226a2540b5ed5086cb + size: 326126 + subdir: . + version: 0.9.8.1 original: - subdir: liquid-base + commit: 4b20537529b2143cab0214564422c94fb93df9d9 git: https://github.com/ucsd-progsys/liquidhaskell - commit: a4f2198f894810a729feb0f8d06301790ee8d1fb + subdir: . - completed: - subdir: liquid-prelude - name: liquid-prelude - version: 0.8.10.2 + commit: 4b20537529b2143cab0214564422c94fb93df9d9 git: https://github.com/ucsd-progsys/liquidhaskell + name: liquidhaskell-boot pantry-tree: - size: 1029 - sha256: c7f41d6fe87cb7d02944834ff59c5d3c7f29b1bd0c83dec5095fed21362c2546 - commit: a4f2198f894810a729feb0f8d06301790ee8d1fb + sha256: f187ea8674d6e8ccdfcc49500b0dac0a9ad87b952bb0f567c842557787cd9da3 + size: 8175 + subdir: liquidhaskell-boot + version: 0.9.8.1 original: - subdir: liquid-prelude + commit: 4b20537529b2143cab0214564422c94fb93df9d9 git: https://github.com/ucsd-progsys/liquidhaskell - commit: a4f2198f894810a729feb0f8d06301790ee8d1fb + subdir: liquidhaskell-boot - completed: - subdir: liquid-ghc-prim - name: liquid-ghc-prim - version: 0.6.1 + commit: 4b20537529b2143cab0214564422c94fb93df9d9 git: https://github.com/ucsd-progsys/liquidhaskell + name: liquid-prelude pantry-tree: - size: 912 - sha256: a1b1fbc8fda0d355f390bfe8ec3036e935b9d4c244217cce6e24363472cd66bd - commit: a4f2198f894810a729feb0f8d06301790ee8d1fb + sha256: e0b5d3b89feec11451cc17f17fb4712e7eff48ca200f1ce6ea1aba45c0aa8f98 + size: 882 + subdir: liquid-prelude + version: 0.9.2.8 original: - subdir: liquid-ghc-prim + commit: 4b20537529b2143cab0214564422c94fb93df9d9 git: https://github.com/ucsd-progsys/liquidhaskell - commit: a4f2198f894810a729feb0f8d06301790ee8d1fb + subdir: liquid-prelude - completed: - subdir: liquid-containers - name: liquid-containers - version: 0.6.2.1 + commit: 4b20537529b2143cab0214564422c94fb93df9d9 git: https://github.com/ucsd-progsys/liquidhaskell + name: liquid-vector pantry-tree: - size: 2143 - sha256: 64ab781aea3b709196876c58ec418a1e8ef93418c71ba7f373658641beabdc7b - commit: a4f2198f894810a729feb0f8d06301790ee8d1fb + sha256: bafea6cf606205b60695b6cdfa6b64c60c7cc8f9054b7fa5ed460d4c633ac39c + size: 231 + subdir: liquid-vector + version: 0.13.1.0 original: - subdir: liquid-containers + commit: 4b20537529b2143cab0214564422c94fb93df9d9 git: https://github.com/ucsd-progsys/liquidhaskell - commit: a4f2198f894810a729feb0f8d06301790ee8d1fb + subdir: liquid-vector - completed: - name: liquid-fixpoint - version: 0.8.10.7.1 + commit: 5b39f1a3c49190f9e438f9cdefd7d2635c5bf7f2 git: https://github.com/ucsd-progsys/liquid-fixpoint + name: liquid-fixpoint pantry-tree: - size: 22311 - sha256: 08c682e475986bae0560d92c115eff6561aea261be0a358a1aab72aa221aa4f4 - commit: 08fa6b6e0001c2da6b96a135523ca56107a3c0d6 + sha256: f703433c37df88b1c1264cc3d5ff33f7cd1ee98a2b4381870ab8b3690be9eef8 + size: 23600 + version: 0.9.6.3 original: + commit: 5b39f1a3c49190f9e438f9cdefd7d2635c5bf7f2 git: https://github.com/ucsd-progsys/liquid-fixpoint - commit: 08fa6b6e0001c2da6b96a135523ca56107a3c0d6 -- completed: - name: rest-rewrite - version: 0.2.0 - git: https://github.com/facundominguez/rest - pantry-tree: - size: 4013 - sha256: 2a91674ccab6b0bd43dcc41fa5e2cb60cbfd35ad585df8293c2884466091d0c0 - commit: 31e974979c90e910efe5199ee0d3721b791667f6 - original: - git: https://github.com/facundominguez/rest - commit: 31e974979c90e910efe5199ee0d3721b791667f6 snapshots: - completed: - size: 590102 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/27.yaml - sha256: 79a786674930a89301b0e908fad2822a48882f3d01486117693c377b8edffdbe - original: lts-18.27 + sha256: 876a5c75d90718add42e1ad36d66000bf35050ce1c66748119897a32df613186 + size: 563963 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2024/1/26.yaml + original: nightly-2024-01-26