Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Data.SBV.Tools.KnuckleDragger\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- A lightweight theorem proving like interface, built on top of SBV.\n-- Inspired by and modeled after Philip Zucker's tool with the same\n-- name, see <http://github.com/philzook58/knuckledragger>.\n--\n-- Example uses:\n--\n-- * Proving Kleene algebra properties: \"Documentation.SBV.Examples.KnuckleDragger.Kleene\"\n-- * Several induction examples: \"Documentation.SBV.Examples.KnuckleDragger.Induction\"\n-- * Sample list properties: \"Documentation.SBV.Examples.KnuckleDragger.Lists\"\n-- * Proving square-root-of-2 is irrational: \"Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational\"\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE ConstraintKinds #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE MultiParamTypeClasses #-}\n{-# LANGUAGE FunctionalDependencies #-}\n{-# LANGUAGE FlexibleContexts #-}\n{-# LANGUAGE FlexibleInstances #-}\n{-# LANGUAGE TypeAbstractions #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Data.SBV.Tools.KnuckleDragger (\n -- * Propositions and proven statements\n Proposition, Proven\n -- * Adding axioms/definitions\n , axiom\n -- * Basic proofs\n , lemma, lemmaWith\n , theorem, theoremWith\n -- * Chain of reasoning\n , chainLemma, chainLemmaWith\n , chainTheorem, chainTheoremWith\n -- * Induction\n , Induction(..)\n -- * Faking proofs\n , sorry\n ) where\n\nimport Data.SBV\nimport Data.SBV.Tools.KDKernel\n\nimport Control.Monad(when)\n\n-- | A class for doing equational reasoning style chained proofs. Use 'chainLemma' to prove a given theorem\n-- as a sequence of equalities, each step following from the previous.\nclass ChainLemma steps step | steps -> step where\n\n -- | Prove a property via a series of equality steps, using the default solver.\n -- Let @h@ be a list of already established lemmas. Let @p@ be a property we wanted to prove, named @name@.\n -- Consider a call of the form @chainLemma name P [A, B, C, D] H@. Note that @h@ is\n -- a list of already proven facts, ensured by the type signature. We proceed as follows:\n --\n -- * Prove: @h -> A == B@\n -- * Prove: @h && A == B -> B == C@\n -- * Prove: @h && A == B && B == C -> C == D@\n -- * Prove: @h && A == B && B == C && C == D -> P@\n -- * If all of the above steps succeed, conclude @p@.\n --\n -- So, chain-lemma is essentially modus-ponens, applied in a sequence of stepwise equality reasoning.\n --\n -- If there are no helpers given (i.e., if @h@ is empty), then this call is equivalent to 'lemmaWith'.\n -- If @h@ is a singleton, then we error-out. A single step in @h@ indicates a user-error, since there's\n -- no sequence of steps to reason about.\n chainLemma :: Proposition a => String -> a -> steps -> [Proven] -> IO Proven\n\n -- | Same as chainLemma, except tagged as Theorem\n chainTheorem :: Proposition a => String -> a -> steps -> [Proven] -> IO Proven\n\n -- | Prove a property via a series of equality steps, using the given solver.\n chainLemmaWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proven] -> IO Proven\n\n -- | Same as chainLemmaWith, except tagged as Theorem\n chainTheoremWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proven] -> IO Proven\n\n -- | Internal, shouldn't be needed outside the library\n makeSteps :: steps -> [step]\n makeInter :: steps -> step -> step -> SBool\n\n chainLemma = chainLemmaWith defaultSMTCfg\n chainTheorem = chainTheoremWith defaultSMTCfg\n\n chainLemmaWith = chainGeneric False\n chainTheoremWith = chainGeneric True\n\n chainGeneric :: Proposition a => Bool -> SMTConfig -> String -> a -> steps -> [Proven] -> IO Proven\n chainGeneric taggedTheorem cfg nm result steps base = do\n putStrLn $ \"Chain: \" ++ nm\n let proofSteps = makeSteps steps\n len = length proofSteps\n when (len == 1) $\n error $ unl

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.Induction\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Example use of the KnuckleDragger, for some inductive proofs\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE TypeAbstractions #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.Induction where\n\nimport Prelude hiding (sum, length)\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\n-- | Prove that sum of numbers from @0@ to @n@ is @n*(n-1)/2@.\n--\n-- We have:\n--\n-- >>> sumProof\n-- Axiom: Nat.induction Admitted.\n-- Lemma: sum_correct Q.E.D.\nsumProof :: IO Proven\nsumProof = do\n let sum :: SInteger -> SInteger\n sum = smtFunction \"sum\" $ \\n -> ite (n .== 0) 0 (n + sum (n - 1))\n\n spec :: SInteger -> SInteger\n spec n = (n * (n+1)) `sDiv` 2\n\n p :: SInteger -> SBool\n p n = observe \"imp\" (sum n) .== observe \"spec\" (spec n)\n\n induct <- inductionPrinciple p\n\n lemma \"sum_correct\" (\\(Forall @\"n\" n) -> n .>= 0 .=> p n) [induct]\n\n-- | Prove that sum of square of numbers from @0@ to @n@ is @n*(n+1)*(2n+1)/6@.\n--\n-- We have:\n--\n-- >>> sumSquareProof\n-- Axiom: Nat.induction Admitted.\n-- Lemma: sumSquare_correct Q.E.D.\nsumSquareProof :: IO Proven\nsumSquareProof = do\n let sumSquare :: SInteger -> SInteger\n sumSquare = smtFunction \"sumSquare\" $ \\n -> ite (n .== 0) 0 (n * n + sumSquare (n - 1))\n\n spec :: SInteger -> SInteger\n spec n = (n * (n+1) * (2*n+1)) `sDiv` 6\n\n p :: SInteger -> SBool\n p n = observe \"imp\" (sumSquare n) .== observe \"spec\" (spec n)\n\n induct <- inductionPrinciple p\n\n lemma \"sumSquare_correct\" (\\(Forall @\"n\" n) -> n .>= 0 .=> p n) [induct]\n"

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.Kleene\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Example use of the KnuckleDragger layer, proving some Kleene algebra theorems.\n--\n-- Based on <http://www.philipzucker.com/bryzzowski_kat/>\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE DeriveAnyClass #-}\n{-# LANGUAGE DeriveDataTypeable #-}\n{-# LANGUAGE FlexibleInstances #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n{-# LANGUAGE StandaloneDeriving #-}\n{-# LANGUAGE TemplateHaskell #-}\n{-# LANGUAGE TypeAbstractions #-}\n{-# LANGUAGE TypeSynonymInstances #-}\n\n{-# OPTIONS_GHC -Wall -Werror -Wno-unused-matches #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.Kleene where\n\nimport Prelude hiding((<=))\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\n-- | An uninterpreted sort, corresponding to the type of Kleene algebra strings.\ndata Kleene\nmkUninterpretedSort ''Kleene\n\n-- | Star operator over kleene algebras. We're leaving this uninterpreted.\nstar :: SKleene -> SKleene\nstar = uninterpret \"star\"\n\n-- | The 'Num' instance for Kleene makes it easy to write regular expressions\n-- in the more familiar form.\ninstance Num SKleene where\n (+) = uninterpret \"par\"\n (*) = uninterpret \"seq\"\n\n abs = error \"SKleene: not defined: abs\"\n signum = error \"SKleene: not defined: signum\"\n negate = error \"SKleene: not defined: signum\"\n\n fromInteger 0 = uninterpret \"zero\"\n fromInteger 1 = uninterpret \"one\"\n fromInteger n = error $ \"SKleene: not defined: fromInteger \" ++ show n\n\n-- | The set of strings matched by one regular expression is a subset of the second,\n-- if adding it to the second doesn't change the second set.\n(<=) :: SKleene -> SKleene -> SBool\nx <= y = x + y .== y\n\n-- | A sequence of Kleene algebra proofs. See <http://www.cs.cornell.edu/~kozen/Papers/ka.pdf>\n--\n-- We have:\n--\n-- >>> kleeneProofs\n-- Axiom: par_assoc Admitted.\n-- Axiom: par_comm Admitted.\n-- Axiom: par_idem Admitted.\n-- Axiom: par_zero Admitted.\n-- Axiom: seq_assoc Admitted.\n-- Axiom: seq_zero Admitted.\n-- Axiom: seq_one Admitted.\n-- Axiom: rdistrib Admitted.\n-- Axiom: ldistrib Admitted.\n-- Axiom: unfold Admitted.\n-- Axiom: least_fix Admitted.\n-- Lemma: par_lzero Q.E.D.\n-- Lemma: par_monotone Q.E.D.\n-- Lemma: seq_monotone Q.E.D.\n-- Chain: star_star_1\n-- Lemma: star_star_1.1 Q.E.D.\n-- Lemma: star_star_1.2 Q.E.D.\n-- Lemma: star_star_1.3 Q.E.D.\n-- Lemma: star_star_1.4 Q.E.D.\n-- Lemma: star_star_1 Q.E.D.\n-- Lemma: subset_eq Q.E.D.\n-- Lemma: star_star_2_2 Q.E.D.\n-- Lemma: star_star_2_3 Q.E.D.\n-- Lemma: star_star_2_1 Q.E.D.\n-- Lemma: star_star_2 Q.E.D.\nkleeneProofs :: IO ()\nkleeneProofs = do\n\n -- Kozen axioms\n par_assoc <- axiom \"par_assoc\" $ \\(Forall @\"x\" (x :: SKleene)) (Forall @\"y\" y) (Forall @\"z\" z) -> x + (y + z) .== (x + y) + z\n par_comm <- axiom \"par_comm\" $ \\(Forall @\"x\" (x :: SKleene)) (Forall @\"y\" y) -> x + y .== y + x\n par_idem <- axiom \"par_idem\" $ \\(Forall @\"x\" (x :: SKleene)) -> x + x .== x\n par_zero <- axiom \"par_zero\" $ \\(Forall @\"x\" (x :: SKleene)) -> x + 0 .== x\n\n seq_assoc <- axiom \"seq_assoc\" $ \\(Forall @\"x\" (x :: SKleene)) (Forall @\"y\" y) (Forall @\"z\" z) -> x * (y * z) .== (x * y) * z\n seq_zero <- axiom \"seq_zero\" $ \\(Forall @\"x\" (x :: SKleene)) -> x * 0 .== 0\n seq_one <- axiom \"seq_one\" $ \\(Forall @\"x\" (x :: SKleene)) -> x * 1 .== x\n\n rdistrib <- axiom \"rdistrib\" $ \\(Forall @\"x\" (x :: SKleene)) (Forall @\"y\" y) (Forall @\"z\" z) -> x * (y + z) .== x * y + x * z\n ldistrib <- axiom \"ldistrib\" $ \\(Forall @\"x\" (x :: SKleene)) (Forall @\"y\" y) (Forall @\"z\" z) -> (y + z) * x .== y * x + z * x\n\n unfold <- axiom \"unfold\" $ \\(Forall @\"e\" e) -> star e .== 1 + e * star e\n\n least_fix

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.Lists\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Example use of the KnuckleDragger, on lists.\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n{-# LANGUAGE TypeAbstractions #-}\n{-# LANGUAGE TypeApplications #-}\n\n{-# OPTIONS_GHC -Wall -Werror -Wno-unused-do-bind #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.Lists where\n\nimport Prelude hiding (sum, length, (++))\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\nimport Data.SBV.List ((.:))\nimport qualified Data.SBV.List as SL\n\n-- $setup\n-- >>> -- For doctest purposes only:\n-- >>> :set -XScopedTypeVariables\n-- >>> import Control.Exception\n\n-- | Prove that the length of a list is one more than the length of its tail.\n--\n-- We have:\n--\n-- >>> listLengthProof\n-- Axiom: List(a).induction Admitted.\n-- Lemma: length_correct Q.E.D.\nlistLengthProof :: IO Proven\nlistLengthProof = do\n let length :: SList Integer -> SInteger\n length = smtFunction \"length\" $ \\xs -> ite (SL.null xs) 0 (1 + length (SL.tail xs))\n\n spec :: SList Integer -> SInteger\n spec = SL.length\n\n p :: SList Integer -> SBool\n p xs = observe \"imp\" (length xs) .== observe \"spec\" (spec xs)\n\n induct <- inductionPrinciple p\n\n lemma \"length_correct\" (\\(Forall @\"xs\" xs) -> p xs) [induct]\n\n-- | It is instructive to see what kind of counter-example we get if a lemma fails to prove.\n-- Below, we do a variant of the 'listLengthProof', but with a bad implementation, and see the\n-- counter-example. Our implementation returns an incorrect answer if the given list is longer\n-- than 5 elements and have 42 in it. We have:\n--\n-- >>> badProof `catch` (\\(_ :: SomeException) -> pure ())\n-- Axiom: List(a).induction Admitted.\n-- Lemma: bad\n-- *** Failed to prove bad.\n-- Falsifiable. Counter-example:\n-- xs = [42,99,100,101,59,102] :: [Integer]\n-- imp = 42 :: Integer\n-- spec = 6 :: Integer\nbadProof :: IO ()\nbadProof = do\n let length :: SList Integer -> SInteger\n length = smtFunction \"length\" $ \\xs -> ite (SL.length xs .> 5 .&& 42 `SL.elem` xs) 42\n $ ite (SL.null xs) 0 (1 + length (SL.tail xs))\n\n spec :: SList Integer -> SInteger\n spec = SL.length\n\n p :: SList Integer -> SBool\n p xs = observe \"imp\" (length xs) .== observe \"spec\" (spec xs)\n\n induct <- inductionPrinciple p\n\n lemma \"bad\" (\\(Forall @\"xs\" xs) -> p xs) [induct]\n\n pure ()\n\n-- | Prove that list concatenation is associative.\n--\n-- We have:\n--\n-- >>> concatAssoc\n-- Axiom: List(a).induction Admitted.\n-- Lemma: cons_app Q.E.D.\n-- Lemma: concatAssoc Q.E.D.\nconcatAssoc :: IO Proven\nconcatAssoc = do\n -- Definition of concat\n let (++) :: SymVal a => SList a -> SList a -> SList a\n (++) = smtFunction \"concat\" $ \\xs ys -> ite (SL.null xs) ys (SL.head xs .: SL.tail xs ++ ys)\n infixr 5 ++\n\n -- The classic proof by induction on xs\n let p :: SymVal a => SList a -> SList a -> SList a -> SBool\n p xs ys zs = xs ++ (ys ++ zs) .== (xs ++ ys) ++ zs\n\n -- Do the proof over integers:\n induct <- inductionPrinciple3 (p @integer)\n\n cons_app <- lemma \"cons_app\"\n (\\(Forall @\"x\" (x :: SInteger)) (Forall @\"xs\" xs) (Forall @\"ys\" ys) -> x .: (xs ++ ys) .== (x .: xs) ++ ys)\n []\n\n lemma \"concatAssoc\"\n (\\(Forall @\"xs\" (xs :: SList Integer)) (Forall @\"ys\" ys) (Forall @\"zs\" zs) -> p xs ys zs)\n [cons_app, induct]\n"

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Prove that square-root of 2 is irrational.\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n{-# LANGUAGE TypeAbstractions #-}\n\n{-# OPTIONS_GHC -Wall -Werror -Wno-unused-matches #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational where\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\n-- | Prove that square-root of @2@ is irrational. That is, we can never find @A@ and @b@ such that\n-- @sqrt 2 == a / b@ and @A@ and @b@ are co-prime.\n--\n-- In order not to deal with reals and square-roots, we prove the integer-only alternative:\n-- If @A^2 = 2b^2@, then @A@ and @b@ cannot be co-prime. We proceed (roughly) as follows:\n--\n-- (1) Start with @A^2 = 2b^2@.\n-- (2) Thus, @A^2@ is even.\n-- (3) Thus, @A@ is even.\n-- (4) Thus, @A@ is a multiple of @2@, meaning @A^2@ is a multiple of @4@.\n-- (5) Thus, @b^2@ must be even.\n-- (6) Thus, @b@ is even.\n-- (7) Since @A@ and @b@ are both even, they cannot be co-prime.\n--\n-- Note that KnuckleDragger will fill in most of these gaps, but we'll help it along\n-- with several helpers.\n--\n-- We have:\n--\n-- >>> sqrt2IsIrrational\n-- Chain: evenSquaredIsEven\n-- Lemma: evenSquaredIsEven.1 Q.E.D.\n-- Lemma: evenSquaredIsEven Q.E.D.\n-- Chain: oddSquaredIsOdd\n-- Lemma: oddSquaredIsOdd.1 Q.E.D.\n-- Lemma: oddSquaredIsOdd Q.E.D.\n-- Chain: evenIfSquareIsEven\n-- Lemma: evenIfSquareIsEven.1 Q.E.D.\n-- Lemma: evenIfSquareIsEven Q.E.D.\n-- Chain: sqrt2IsIrrational\n-- Lemma: sqrt2IsIrrational.1 Q.E.D.\n-- Theorem: sqrt2IsIrrational Q.E.D.\nsqrt2IsIrrational :: IO Proven\nsqrt2IsIrrational = do\n let isEven :: SInteger -> SBool\n isEven = (2 `sDivides`)\n\n isOdd :: SInteger -> SBool\n isOdd = sNot . isEven\n\n -- Prove that an even number squared gives you an even number\n evenSquaredIsEven <- chainLemma \"evenSquaredIsEven\"\n (\\(Forall @\"x\" x) -> isEven x .=> isEven (x * x))\n (\\x -> let h, hx :: SInteger\n h = x `sDiv` 2\n hx = h * 2\n in [x .== hx, hx * hx .== x * x]\n ) []\n\n -- Prove that an odd number squared gives you an odd number\n oddSquaredIsOdd <- chainLemma \"oddSquaredIsOdd\"\n (\\(Forall @\"x\" x) -> isOdd x .=> isOdd (x * x))\n (\\x -> let h, hx :: SInteger\n h = x `sDiv` 2\n hx = h * 2 + 1\n in [hx .== x, hx * hx .== x * x]\n ) []\n\n -- Prove that if a number squared is even, then it must be even as well\n evenIfSquareIsEven <- chainLemma \"evenIfSquareIsEven\"\n (\\(Forall @\"x\" x) -> isEven (x * x) .=> isEven x)\n (\\x -> [isOdd x, isOdd (x * x)])\n [evenSquaredIsEven, oddSquaredIsOdd]\n\n -- Define what it means to be co-prime. Note that we use euclidian notion of modulus here\n -- as z3 deals with that much better. Two numbers are co-prime if for all @z@ that divides both,\n -- @z@ must equal 1.\n let coPrime :: SInteger -> SInteger -> SBool\n coPrime x y = quantifiedBool (\\(Forall @\"z\" z) -> (x `sEMod` z .== 0 .&& y `sEMod` z .== 0) .=> z .== 1)\n\n -- Prove that if a is an even number, then its square four times the square of another.\n evenSquareMult4 <- lemma \"evenSquareMult4\"\n (\\(Forall @\"a\" a) -> isEven a .=> quantifiedBool (\\(Exists @\"b\" b) -> a * a .== 4 * b * b))\n []\n\n -- Prove that square-root of 2 is irrational, by showing for all pairs of integers @A@ and @b@\n -- such that @A*a == 2*b*b@, we can show that @A@ and @b@ are not co-prime:\n lemma \"sqrt2IsIrrational\"\n (\\(Forall @\"a\" a) (Forall @\"b\" b) -> ((a*a .== 2*b*b) .=> sNot (coPrime a b)))\n [evenIfSquareIsEven, evenSquareMult4]\n"

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: [email protected]\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/

The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, rwe/actions-hlint-setup@v1, rwe/actions-hlint-run@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SInteger)" ▫︎ Perhaps: "SInteger"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(KUnbounded)" ▫︎ Perhaps: "KUnbounded"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(KUnbounded)" ▫︎ Perhaps: "KUnbounded"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SWord8)" ▫︎ Perhaps: "SWord8"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SWord16)" ▫︎ Perhaps: "SWord16"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SWord32)" ▫︎ Perhaps: "SWord32"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SWord64)" ▫︎ Perhaps: "SWord64"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SInt8)" ▫︎ Perhaps: "SInt8"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SInt16)" ▫︎ Perhaps: "SInt16"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SInt32)" ▫︎ Perhaps: "SInt32"

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/