liquid-intro

.gitignore

dist-newstyle/*
.liquid/*

liquid-intro.cabal

cabal-version:      3.0
-- The cabal-version field refers to the version of the .cabal specification,
-- and can be different from the cabal-install (the tool) version and the
-- Cabal (the library) version you are using. As such, the Cabal (the library)
-- version used must be equal or greater than the version stated in this field.
-- Starting from the specification version 2.2, the cabal-version field must be
-- the first thing in the cabal file.

-- Initial package description 'liquid-intro' generated by
-- 'cabal init'. For further documentation, see:
--   http://haskell.org/cabal/users-guide/
--
-- The name of the package.
name:               liquid-intro

-- The package version.
-- See the Haskell package versioning policy (PVP) for standards
-- guiding when and how versions should be incremented.
-- https://pvp.haskell.org
-- PVP summary:     +-+------- breaking API changes
--                  | | +----- non-breaking API additions
--                  | | | +--- code changes with no API change
version:            0.1.0.0

-- A short (one-line) description of the package.
-- synopsis:

-- A longer description of the package.
-- description:

-- The license under which the package is released.
license:            BSD-3-Clause

-- The package author(s).
author:             Armando Ramirez

-- An email address to which users can send suggestions, bug reports, and patches.
maintainer:         armando.m.ramirez@gmail.com

-- A copyright notice.
-- copyright:
category:           Math
build-type:         Simple

-- Extra source files to be distributed with the package, such as examples, or a tutorial module.
-- extra-source-files:

common warnings
    ghc-options: -Wall

library
    -- Import common warning flags.
    import:           warnings

    -- Modules exported by the library.
    exposed-modules:  MyLib

    -- Modules included in this library but not exported.
    -- other-modules:

    -- LANGUAGE extensions used by modules in this package.
    -- other-extensions:

    -- Other library packages from which modules are imported.
    build-depends:    base >= 4.11 && < 5, liquidhaskell, liquid-base

    -- Directories containing source files.
    hs-source-dirs:   .

    -- Base language which the package is written in.
    default-language: Haskell2010

MyLib.hs

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE PackageImports #-}
{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

{-@ LIQUID "--ple" @-}
{-@ LIQUID "--exact-data-cons" @-}


-- Repro of:
-- https://discourse.haskell.org/t/what-is-a-correct-scope-that-liquidhaskell-does/7565
module MyLib where

import "liquid-base" Prelude

{-@ measure fst' @-}
fst' :: (a, b) -> a
fst'  (x, _) = x

{-@ measure snd' @-}
snd' :: (a, b) -> b
snd' (_, y) = y

{-@ measure imax @-}
{-@ imax :: xy:(Int, Int) -> {z:Int | z = if (fst' xy) > (snd' xy) then (fst' xy) else (snd' xy)} @-}
imax :: (Int, Int) -> Int
imax (x, y) = if x > y then x else y

{-@ measure imin @-}
{-@ imin :: xy:(Int, Int) -> {z:Int | z = if (fst' xy) > (snd' xy) then (snd' xy) else (fst' xy)} @-}
imin :: (Int, Int) -> Int
imin (x, y) = if x > y then y else x

{-@ take' :: xs:[a] -> {i:Int | i >= 0 && i < len xs} -> {ys:[a] | len ys = imin (len xs, i)} @-}
take' :: [a] -> Int -> [a]
take' _ 0 = []
take' [] _ = []
take' (h:t) s = h : take' t (s - 1)
{-@ reflect take' @-}

{-@ ex1 :: {xs:[Int] | len xs = 4} @-}
ex1 :: [Int]
ex1 = take' [1,2,3,4,5] 4

{-@ ex2 :: {xs:[Int] | len xs = 4} @-}
ex2 :: [Int]
ex2 = take' l 4
    where l = take 5 (repeat1 3) -- [3,3,3,3,3]

-- | Per @facundominguez in this Github issue:
-- https://github.com/ucsd-progsys/liquidhaskell/issues/2218#issuecomment-1715830606
--
-- We must mark repeat1 lazy so it doesn't get checked for termination
{-@ lazy repeat1 @-}
repeat1 :: a -> [a]
repeat1 x = x : repeat1 x
{-@ reflect repeat1 @-}

nix-shell.sh

#! /usr/bin/env bash

nix-shell -p haskell.compiler.ghc902 -p z3