How to use 'oneof' in quickCheck (Haskell)



  • I am trying to write a prop that changes a Sudoku and then checks if it's still valid.

    However, I am not sure how to use the "oneof"-function properly. Can you give me some hints, please?

    prop_candidates :: Sudoku -> Bool
    prop_candidates su = isSudoku newSu && isOkay newSu
        where
            newSu       = update su aBlank aCandidate
            aCandidate  = oneof [return x | x <- candidates su aBlank]
            aBlank      = oneof [return x | x <- (blanks su)]
    
    

    Here are some more info...

    type Pos = (Int, Int)
    update :: Sudoku -> Pos -> Maybe Int -> Sudoku
    blanks :: Sudoku -> [Pos]
    candidates :: Sudoku -> Pos -> [Int]
    [return x | x <- (blanks example)] :: (Monad m) => [m Pos]
    
    

    I have struggeled with this prop for 3 hours now, so any ideas are welcome!

    What I was driving at is that you have a type mix-up. Namely, aBlank is not a Pos, but a Gen Pos, so update su aBlank aCandidate makes no sense! In fact, what you want is a way to generate a new sudoku given an initial sudoku; in other words a function

    similarSudoku :: Sudoku -> Gen Sudoku
    
    

    Now we can write it:

    similarSudoku su = do aBlank <- elements (blanks su) 
                          -- simpler than oneOf [return x | x <- blanks su]
                          aCandidate <- elements (candidates su aBlank)
                          return (update su aBlank aCandidate)
    
    

    or even simpler:

    similarSudoku su = liftM2 (update su) (elements (blanks su)) (elements (candidates su aBlank))
    
    

    And the property looks like

    prop_similar :: Sudoku -> Gen Bool
    prop_similar su = do newSu <- similarSudoku su
                         return (isSudoku newSu && isOkay newSu)
    
    

    Since there are instances

    Testable Bool
    Testable prop => Testable (Gen prop)
    (Arbitrary a, Show a, Testable prop) => Testable (a -> prop)
    
    

    Sudoku -> Gen Bool is Testable as well (assuming instance Arbitrary Sudoku).

    On my blog, I wrote a simple craps simulator with QuickCheck tests that use oneof to generate interesting rolls.

    Say we have a super-simple Sudoku of a single row:

    module Main where
    import Control.Monad
    import Data.List
    import Test.QuickCheck
    import Debug.Trace
    
    type Pos = Int
    data Sudoku = Sudoku [Char] deriving (Show)
    
    

    No super-simple Sudoku should have repeated values:

    prop_noRepeats :: Sudoku -> Bool
    prop_noRepeats s@(Sudoku xs) =
      trace (show s) $ all ((==1) . length) $
                       filter ((/='.') . head) $
                       group $ sort xs
    
    

    You might generate a super-simple Sudoku with

    instance Arbitrary Sudoku where
      arbitrary = sized board :: Gen Sudoku
        where board :: Int -> Gen Sudoku
              board 0 = Sudoku `liftM` shuffle values
              board n | n > 6 = resize 6 arbitrary
                      | otherwise =
                          do xs <- shuffle values
                             let removed = take n xs
                                 dots = take n $ repeat '.'
                                 remain = values \\ removed
                             ys <- shuffle $ dots ++ remain
                             return $ Sudoku ys
    
              values = ['1' .. '9']
    
              shuffle :: (Eq a) => [a] -> Gen [a]
              shuffle [] = return []
              shuffle xs = do x  <- oneof $ map return xs
                              ys <- shuffle $ delete x xs
                              return (x:ys)
    
    

    The trace is there to show the randomly generated boards:

    *Main> quickCheck prop_noRepeats 
    Sudoku "629387451"
    Sudoku "91.235786"
    Sudoku "1423.6.95"
    Sudoku "613.4..87"
    Sudoku "6..5..894"
    Sudoku "7.2..49.."
    Sudoku "24....1.."
    [...]
    +++ OK, passed 100 tests.
    
    

    it seems that aBlank :: Gen Pos which does not match the way it is used as an argument of candidates :: Sudoku -> Pos -> [Int].

    I've been looking through here to find a way to convert Gen a to a which would allow you to use it with candidates. The best i could see is the generate function.

    Tell me if I'm missing something...

    来源:https://stackoverflow.com/questions/1828850/how-to-use-oneof-in-quickcheck-haskell



最新帖子

最新内容

  • S

    Based on the screenshot you just added, you want to change the error messages the browser renders to the client. This can be done by adding an oninvalid attribute to your field.

    Here is how it's done in your forms.py file:

    from django import forms from SharedApps_Application.models import certificateDb from django.contrib.admin.widgets import AdminDateWidget from django.forms.fields import DateField class CertificateForm(forms.ModelForm): app_attributes = {'oninvalid': 'this.setCustomValidity("Application field is required")', 'oninput': 'this.setCustomValidity("")'} startdate = forms.DateField(widget = forms.SelectDateWidget(years=range(1995, 2100))) expiredate = forms.DateField(widget = forms.SelectDateWidget(years=range(1995, 2100))) application = forms.CharField(widget=forms.TextInput(attrs=app_attributes) class Meta: model = certificateDb fields = ('application', 'startdate', 'expiredate', 'environment_type','File' ) error_messages = { 'application': { 'required': ("Application field is required"), }, }

    Assuming the field you want to override is 'application'. Add a error_messages dictionary under your class Meta like this:

    OLD ANSWER - Overriding Django forms validation error messages

    from django import forms from SharedApps_Application.models import certificateDb from django.contrib.admin.widgets import AdminDateWidget from django.forms.fields import DateField class CertificateForm(forms.ModelForm): startdate = forms.DateField(widget = forms.SelectDateWidget(years=range(1995, 2100))) expiredate = forms.DateField(widget = forms.SelectDateWidget(years=range(1995, 2100))) application = forms.CharField() class Meta: model = certificateDb fields = ('application', 'startdate', 'expiredate', 'environment_type','File' ) error_messages = { 'application': { 'required': ("Application field is required"), }, }

    read more
  • S

    I try this but it doesn't work. default error message is shown only.please help............

    from django import forms from SharedApps_Application.models import certificateDb from django.contrib.admin.widgets import AdminDateWidget from django.forms.fields import DateField my_default_errors = { 'required': 'Application field is required', } class CertificateForm(forms.ModelForm): startdate = forms.DateField(widget = forms.SelectDateWidget(years=range(1995, 2100))) expiredate = forms.DateField(widget = forms.SelectDateWidget(years=range(1995, 2100))) application = forms.CharField(error_messages = my_default_errors) class Meta: model = certificateDb fields = ('application', 'startdate', 'expiredate', 'environment_type','File' )

    screenshot

    [1]: https://i.stack.imgur.com/8zhM6.png

    update

    from django import forms from SharedApps_Application.models import certificateDb from django.contrib.admin.widgets import AdminDateWidget from django.forms.fields import DateField class CertificateForm(forms.ModelForm): startdate = forms.DateField(widget = forms.SelectDateWidget(years=range(1995, 2100))) expiredate = forms.DateField(widget = forms.SelectDateWidget(years=range(1995, 2100))) application = forms.CharField() class Meta: model = certificateDb fields = ('application', 'startdate', 'expiredate', 'environment_type','File' ) error_messages = { 'application': { 'required': ("Application field is required"), }, }

    read more
  • S

    I have the following situation: I need to get xml file from the Internet and then get lyrics from this file. Here's the url of this xml. Here's the code, which I wrote and which should do it.

    private static class NetworkLyricsDownload extends AsyncTask<Void, Void, Void> { @Override protected Void doInBackground(Void... voids) { try { URL url = new URL("http://api.chartlyrics.com/apiv1.asmx/SearchLyricDirect?artist=Eminem&song=Lose%20Yourself"); XmlPullParserFactory factory = XmlPullParserFactory.newInstance(); factory.setNamespaceAware(false); XmlPullParser xmlPullParser = factory.newPullParser(); xmlPullParser.setInput(getInputStream(url), "UTF-8"); boolean insideItem = false; int eventType = xmlPullParser.getEventType(); while (eventType!=XmlPullParser.END_DOCUMENT){ if (eventType == XmlPullParser.START_TAG){ if (xmlPullParser.getName().equalsIgnoreCase("lyric")){ insideItem = true; Log.i(getClass().getName(), xmlPullParser.nextText()); } } eventType = xmlPullParser.next(); } } catch (MalformedURLException e) { e.printStackTrace(); } catch (XmlPullParserException e) { e.printStackTrace(); } catch (IOException e) { e.printStackTrace(); } return null; } private InputStream getInputStream(URL url){ try { return url.openConnection().getInputStream(); } catch (IOException e) { e.printStackTrace(); } return null; } }

    But when I run the app, I have the following error:

    E/AndroidRuntime: FATAL EXCEPTION: AsyncTask #2 Process: asus.example.com.player, PID: 14458 java.lang.RuntimeException: An error occurred while executing doInBackground() at android.os.AsyncTask$3.done(AsyncTask.java:354) at java.util.concurrent.FutureTask.finishCompletion(FutureTask.java:383) at java.util.concurrent.FutureTask.setException(FutureTask.java:252) at java.util.concurrent.FutureTask.run(FutureTask.java:271) at android.os.AsyncTask$SerialExecutor$1.run(AsyncTask.java:245) at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1167) at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:641) at java.lang.Thread.run(Thread.java:764) Caused by: java.lang.IllegalArgumentException: is == null at org.kxml2.io.KXmlParser.setInput(KXmlParser.java:1636) at asus.example.com.player.UploadLyricsActivity$NetworkLyricsDownload.doInBackground(UploadLyricsActivity.java:114) at asus.example.com.player.UploadLyricsActivity$NetworkLyricsDownload.doInBackground(UploadLyricsActivity.java:86) at android.os.AsyncTask$2.call(AsyncTask.java:333) at java.util.concurrent.FutureTask.run(FutureTask.java:266) at android.os.AsyncTask$SerialExecutor$1.run(AsyncTask.java:245)  at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1167)  at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:641)  at java.lang.Thread.run(Thread.java:764) 

    I have permission in manifest file ( <uses-permission android:name="android.permission.INTERNET"/>) but it still doesn't help. So, what's the matter and how can I solve it?

    UPD

    Here's my manifest file:

    <?xml version="1.0" encoding="utf-8"?> <manifest xmlns:android="http://schemas.android.com/apk/res/android" xmlns:tools="http://schemas.android.com/tools" package="asus.example.com.player" android:targetSandboxVersion="1"> <uses-permission android:name="android.permission.WAKE_LOCK" /> <uses-permission android:name="android.permission.READ_EXTERNAL_STORAGE" /> <uses-permission android:name="android.permission.INTERNET"/> <application android:allowBackup="true" android:icon="@mipmap/ic_launcher" android:label="@string/app_name" android:roundIcon="@mipmap/ic_launcher_round" android:supportsRtl="true" android:theme="@style/AppTheme" android:networkSecurityConfig="@xml/network_security_config" android:usesCleartextTraffic="true" tools:ignore="AllowBackup,GoogleAppIndexingWarning,UnusedAttribute"> <activity android:name=".SongLyricsActivity"/> <activity android:name=".UploadLyricsActivity" /> <activity android:name=".ListOfSongsActivity" android:launchMode="singleTask"> <intent-filter> <action android:name="android.intent.action.MAIN" /> <category android:name="android.intent.category.LAUNCHER" /> </intent-filter> </activity> <activity android:name=".MainActivity" /> <service android:name=".MyService" android:enabled="true" android:exported="true" tools:ignore="ExportedService" /> </application> </manifest>

    read more
  • S

    You are almost there:

    @echo off set "currentfolder=D:\some directory\" pushd "%directory%" for /f "delims=" %%i in ('dir /b /a-d /od') do ( set "file=%%i" set "moddate=%%~ti" goto :done ) popd :done echo %file% %moddate%

    So we sort by date (oldest first) then set the first filename as %file% and it's date to %moddate% then we exit the loop so it does not do the same for the other files in the folder.

    read more
  • S

    The problem is caused by the fact that your current working directory referred to by for /F is not the same as the directory you are searching files in by dir.

    This can be fixed like this (omitting grep as I do not understand its purpose here):

    <pre class="lang-cmd prettyprint-override">``` rem // Temporarily change to the directory containing the files of interest: pushd "%currentfolder%" rem /* The current working directory is now the target directory; rem thus both `dir` and `for /F` work in the same directory: */ for /F "delims=" %%x in ('dir /B /A:-D /O:-D') do (set "FILEINFO=%%~tx") rem // Restore the former working directory: popd rem // Just output the gathered information: echo/%FILEINFO% Alternatively, the `pushd` command line could be replaced by `cd /D "%currentfolder%"` when `popd` is removed, given that you do not need the original working directory to be restored. - - - - - - To understand what was going on in your original code, let us assume: - the current working directory is `C:\TEST`; - the content of variable `currentfolder` is `D:\DATA`; - the directory `C:\TEST` contains nothing but the batch file; - the directory `D:\DATA` contains a file called `some.txt`; The command line `dir /b /o-d /a-d %currentfolder%` returns only pure file names (due to its option `/B`), so based on the predefined sample data, the output would be: > ``` > <pre class="lang-cmd prettyprint-override">``` > some.txt > > ``` > ``` Now this text is captured by the `for /F` loop. Now the last modification date/time is queried by `%%~tx`, which of course requires access to the file system. Remember that the current working directory is `C:\TEST`, so the `for /F` loop tries to gather the information from the following file: > ``` > <pre class="lang-cmd prettyprint-override">``` > C:\TEST\some.txt > > ``` > ``` Since such a file does not exist, the output is blank. To prove that, simply place a new file `some.txt` into the directory `C:\TEST`, then you would receive the last modification date/time of that file.

    read more

推荐阅读

  • 1
  • 8
  • 4
  • 1
  • 2
  • 2
  • 1
  • 1