Error: Parse error: Expression syntax in pattern: Forall @"x" ▫︎ Found: " skolemEx4 = sat cs\n where cs :: ConstraintSet\n> cs = do constrain $ taggedSkolemize \"c1\" $ \\(Forall @\"x\" x) (Exists @\"y\" y) -> x .== (y :: SInteger)\n constrain $ taggedSkolemize \"c2\" $ \\(Forall @\"x\" x) (Exists @\"y\" y) -> x .== (y-1 :: SInteger)\n"

Error: Parse error: Unsupported extension: OverloadedRecordDot ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.Puzzles.Orangutans\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: erkokl@gmail.com\n-- Stability : experimental\n--\n-- Based on <http://github.com/goldfirere/video-resources/blob/main/2022-08-12-java/Haskell.hs>\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE DeriveAnyClass #-}\n{-# LANGUAGE DeriveDataTypeable #-}\n{-# LANGUAGE DeriveGeneric #-}\n{-# LANGUAGE FlexibleContexts #-}\n{-# LANGUAGE TemplateHaskell #-}\n{-# LANGUAGE StandaloneDeriving #-}\n{-# LANGUAGE OverloadedRecordDot #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Documentation.SBV.Examples.Puzzles.Orangutans where\n\nimport Data.SBV\nimport GHC.Generics (Generic)\n\n-- $setup\n-- >>> -- For doctest purposes only:\n-- >>> import Data.SBV\n\n-- | Orangutans in the puzzle.\ndata Orangutan = Merah | Ofallo | Quirrel | Shamir deriving (Enum, Bounded)\n\n-- | Handlers for each orangutan.\ndata Handler = Dolly | Eva | Francine | Gracie\n\n-- | Location for each orangutan.\ndata Location = Ambalat | Basahan | Kendisi | Tarakan\n\nmkSymbolicEnumeration ''Orangutan\nmkSymbolicEnumeration ''Handler\nmkSymbolicEnumeration ''Location\n\n-- | An assignment is solution to the puzzle\ndata Assignment = MkAssignment { orangutan :: SOrangutan\n , handler :: SHandler\n , location :: SLocation\n , age :: SInteger\n }\n deriving (Generic, Mergeable)\n\n-- | Create a symbolic assignment, using symbolic fields.\nmkSym :: Orangutan -> Symbolic Assignment\nmkSym o = do let h = show o ++ \".handler\"\n l = show o ++ \".location\"\n a = show o ++ \".age\"\n s <- MkAssignment (literal o) <$> free h <*> free l <*> free a\n constrain $ s.age `sElem` [4, 7, 10, 13]\n pure s\n\n-- | We get:\n--\n-- >>> allSat puzzle\n-- Solution #1:\n-- Merah.handler = Gracie :: Handler\n-- Merah.location = Tarakan :: Location\n-- Merah.age = 10 :: Integer\n-- Ofallo.handler = Eva :: Handler\n-- Ofallo.location = Kendisi :: Location\n-- Ofallo.age = 13 :: Integer\n-- Quirrel.handler = Dolly :: Handler\n-- Quirrel.location = Basahan :: Location\n-- Quirrel.age = 4 :: Integer\n-- Shamir.handler = Francine :: Handler\n-- Shamir.location = Ambalat :: Location\n-- Shamir.age = 7 :: Integer\n-- This is the only solution.\npuzzle :: ConstraintSet\npuzzle = do\n solution@[_merah, ofallo, quirrel, shamir] <- mapM mkSym [minBound .. maxBound]\n\n let find f = foldr1 (\\a1 a2 -> ite (f a1) a1 a2) solution\n\n -- 0. All are different in terms of handlers, locations, and ages\n constrain $ distinct (map (.handler) solution)\n constrain $ distinct (map (.location) solution)\n constrain $ distinct (map (.age) solution)\n\n -- 1. Shamir is 7 years old.\n constrain $ shamir.age .== 7\n\n -- 2. Shamir came from Ambalat.\n constrain $ shamir.location .== sAmbalat\n\n -- 3. Quirrel is younger than the ape that was found in Tarakan.\n let tarakan = find (\\a -> a.location .== sTarakan)\n constrain $ quirrel.age .< tarakan.age\n\n -- 4. Of Ofallo and the ape that was found in Tarakan, one is cared for by Gracie and the other is 13 years old.\n let clue4 a1 a2 = a1.handler .== sGracie .&& a2.age .== 13\n constrain $ clue4 ofallo tarakan .|| clue4 tarakan ofallo\n constrain $ sOfallo ./= tarakan.orangutan\n\n -- 5. The animal that was found in Ambalat is either the 10-year-old or the animal Francine works with.\n let ambalat = find (\\a -> a.location .== sAmbalat)\n constrain $ ambalat.age .== 10 .|| ambalat.handler .== sFrancine\n\n -- 6. Ofallo isn't 10 years old.\n constrain $ ofallo.age ./= 10\n\n -- 7. The ape that was found in Kendisi is older than the ape Dolly works with.\n let kendisi = find (\\a -> a.location .== sKendisi)\n let dolly = find (\\a -> a.handler .== sDolly)\n constrain $ kendisi.age .> dolly.age\n"

Error: Parse error: Expression syntax in pattern: ExistsN @4 ▫︎ Found: " ]\n \n> others = [ goldenCapturedIO \"quantifiedB_0\" $ check $ \\(ExistsN @4 xs) -> sAll (.< (20 :: SWord8)) xs .&& sum (1 : xs) .== (0::SWord8)\n , goldenCapturedIO \"quantifiedB_1\" $ check $ \\(ExistsN @4 xs) -> sum xs .== (0::SWord8)\n , goldenCapturedIO \"quantifiedB_2\" $ check $ \\k (ForallN @4 xs) -> sum xs .== (k::SWord8)\n"

Error: Parse error: Expression syntax in pattern: Forall @"x" ▫︎ Found: " appendFile rf (\"\\n FINAL:\\n\" ++ show r ++ \"\\nDONE!\\n\")\n \n> where t = do constrain $ skolemize $ \\(Forall @\"x\" x) (Exists @\"y\" y) -> y .== 3*(x::SInteger)\n query $ do cs <- checkSat\n case cs of\n"

The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, rwe/actions-hlint-setup@v1, rwe/actions-hlint-run@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/

Suggestion in zeroExtend, signExtend in module Data.SBV.Core.Sized: Reduce duplication ▫︎ Found: "nv = intOfProxy (Proxy @n)\nmv = intOfProxy (Proxy @m)\ni = fromIntegral (mv - nv)\n" ▫︎ Perhaps: "Combine with Data/SBV/Core/Sized.hs:338:9-34"

Warning in module Data.SBV.Tools.BoundedList: Unused LANGUAGE pragma ▫︎ Found: "{-# LANGUAGE OverloadedLists #-}"

Suggestion in runAESTests, aes128IsCorrect in module Documentation.SBV.Examples.Crypto.AES: Reduce duplication ▫︎ Found: "(encKS, decKS) = aesKeySchedule key\nct = aesEncrypt pt encKS\npt' = aesDecrypt ct decKS\n" ▫︎ Perhaps: "Combine with Documentation/SBV/Examples/Crypto/AES.hs:708:10-44"

Suggestion in memsetExample, outOfInit in module Documentation.SBV.Examples.Misc.LambdaArray: Reduce duplication ▫︎ Found: "mem <- newArray \"mem\" Nothing\nlo <- sInteger \"lo\"\nhi <- sInteger \"hi\"\nzero <- sInteger \"zero\"\n" ▫︎ Perhaps: "Combine with Documentation/SBV/Examples/Misc/LambdaArray.hs:56:4-33"

Warning in checkPuzzle in module BenchSuite.Puzzles.Sudoku: Use Just ▫︎ Found: "fromMaybe False (unliteral vld)" ▫︎ Perhaps: "(Just True == unliteral vld)"

Warning in checkPuzzle in module TestSuite.Puzzles.Sudoku: Use Just ▫︎ Found: "fromMaybe False (unliteral vld)" ▫︎ Perhaps: "(Just True == unliteral vld)"

The `set-output` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see: https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/

The `set-output` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see: https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/

The `set-output` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see: https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/