quickchick / luck Goto Github PK

Luck -- A Language for Property-Based Generators

License: MIT License

Coq 39.58% Makefile 0.07% Haskell 56.42% Logos 1.40% Yacc 2.52%

luck's Introduction

Luck -- A Language for Property-Based Generators

Accompanying material for the following POPL 2017 paper: Beginner's Luck: A Language for Property-Based Generators. Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu, John Hughes, Benjamin C. Pierce, Li-yao Xia. https://arxiv.org/abs/1607.05443

/coq

Coq proofs for narrowing fragment of the Luck core language. Works with Coq 8.4pl6. Simply run make there to check proofs.

/luck

Luck interpreter. Known to work with GHC 7.10 -- 8.01

Running cabal install there will produce a luck executable. Try out luck examples/BST.luck. luck --help provides a list of useful flags.

luck's People

Contributors

Stargazers

Watchers

Forkers

pirapira ulysses4ever

luck's Issues

Usage of `debug-trygen`

Hello! I'm trying to use Luck to generate well-typed STLC-terms. I need lots of them for testing my compiler. So far I was only able to generate one term at a time. I see debug-trygen option in the help output.

     --debug-trygen=TYPE,SIZE,RPT ---trygenerator  Generate RPT random values
                                                   of type TYPE with size SIZE,
                                                   ex: "[[Bool]]",14,4

So I tried

dist/build/luck/luck --debug-trygen="[[Bool]]",14,4 examples/STLC.luck

and got

e@53:
  App
    (TArrow TInt TInt)
    (Abs
       16
       (TArrow TInt TInt)
       (App ...[3 nodes] ...[2 nodes] ...[2 nodes]))
    ...[6 nodes]

This seems to completely ignore the option. What is the right way to use it?

Generally, I'd suggest to add top-level use cases either to examples directory or directly to the README file (which is, by the way, too succinct at the moment): how would one call luck to get various kinds of output. Also, how would one use luck as a library from Haskell?

Recent new type of Luck.Main.parse breaks the template examples

A recent change 84d8bd3 seems to have broken the build of combinations.hs example in examples-tempalte directory.

Before the change:

[12:41] yh@sri: ~/infra-src/Luck/luck(:c64d06e|…)$ stack build && stack runghc examples-template/combination.hs
There were multiple candidates for the Cabal entry "Outer.Parser" (/home/yh/infra-src/Luck/luck/src/Outer/Parser.y), picking /home/yh/infra-src/Luck/luck/src/Outer/Parser.hs
Just [1,0,0,0,0,0,0,0,0,0,1,1,0]
Just [1,0,0,0,0,0,0,0,1,1,0,0,0]
Just [0,0,1,0,0,1,0,0,0,1,0,0,0]
Just [0,0,0,0,1,0,1,1,0,0,0,0,0]
Just [1,0,0,0,0,0,0,0,0,0,1,1,0]
Just [0,0,1,1,0,0,0,0,0,0,0,0,1]
Just [0,0,0,0,0,1,0,1,1,0,0,0,0]
Just [0,0,0,0,0,1,1,0,0,0,0,1,0]
Just [0,0,1,0,0,0,0,0,0,0,0,1,1]
Just [0,1,0,0,1,0,0,0,0,1,0,0,0]
Just [1,0,0,0,0,0,1,0,0,1,0,0,0]

After the change:

[12:44] yh@sri: ~/infra-src/Luck/luck(master|…)$ git show | head -n 1
commit 84d8bd30901b81ba57a3ec0696cd17e5b7d83e68
[12:45] yh@sri: ~/infra-src/Luck/luck(master|…)$ stack build && stack runghc examples-template/combination.hs
There were multiple candidates for the Cabal entry "Outer.Parser" (/home/yh/infra-src/Luck/luck/src/Outer/Parser.y), picking /home/yh/infra-src/Luck/luck/src/Outer/Parser.hs

examples-template/combination.hs:6:9: error:
    • Couldn't match type ‘Data.ByteString.Internal.ByteString’
                     with ‘[Outer.AST.Decl]’
      Expected type: Outer.AST.Prg
        Actual type: Data.ByteString.Internal.ByteString
    • In the second argument of ‘Luck.Main.parse’, namely
        ‘Data.ByteString.Char8.pack

I used GHC 8.0.1 for both experiments.

$ stack ghc -- --version
The Glorious Glasgow Haskell Compilation System, version 8.0.1

An error "Pat shouldnot happen"

Sometimes the error Pat shouldnothappen happens.

The luck file.

$ git clone [email protected]:pirapira/minus-minus-solidity.git
$ mkdir minus-minus-solidity
$ git checkout shouldnot
$ stack build && stack exec mms-exe
mms-exe: Pat shouldnot happen
CallStack (from HasCallStack):
  error, called at src/Core/Semantics.hs:429:26 in luck-0.1.0.0-LJij1R78ObT1aQOfaHb3dW:Core.Semantics

This error happens with 70% probability.

Build failure

I tried to build Luck on a freshly installed Ubuntu 16.04 system and got the following error:

yilongl@node:~/Luck/luck$ ghc --version                                                           
The Glorious Glasgow Haskell Compilation System, version 7.10.3                                   
yilongl@node:~/Luck/luck$ cabal --version                                                         
cabal-install version 1.22.6.0                                                                    
using version 1.22.5.0 of the Cabal library                                                       
yilongl@node:~/Luck/luck$ lsb_release -a                                                          
No LSB modules are available.                                                                     
Distributor ID: Ubuntu                                                                            
Description:    Ubuntu 16.04.1 LTS                                                                
Release:        16.04                                                                             
Codename:       xenial                                                                            

yilongl@node:~/Luck/luck$ cabal install                                                           
Resolving dependencies...                                                                         
Configuring luck-0.1.0.0...                                                                       
Building luck-0.1.0.0...                                                                          
Failed to install luck-0.1.0.0                                                                    
Build log ( /users/yilongl/.cabal/logs/luck-0.1.0.0.log ):                                        
Configuring luck-0.1.0.0...                                                                       
Building luck-0.1.0.0...                                                                          
Preprocessing library luck-0.1.0.0...                                                             
[ 1 of 27] Compiling Paths_luck       ( dist/build/autogen/Paths_luck.hs, dist/build/Paths_luck.o 
)                                                                                                 
[ 2 of 27] Compiling Common.Pretty    ( src/Common/Pretty.hs, dist/build/Common/Pretty.o )        
[ 3 of 27] Compiling Common.Types     ( src/Common/Types.hs, dist/build/Common/Types.o )          
[ 4 of 27] Compiling Common.SrcLoc    ( src/Common/SrcLoc.hs, dist/build/Common/SrcLoc.o )        
[ 5 of 27] Compiling Outer.AST        ( src/Outer/AST.hs, dist/build/Outer/AST.o )                
[ 6 of 27] Compiling Core.AST         ( src/Core/AST.hs, dist/build/Core/AST.o )                  
[ 7 of 27] Compiling Common.Error     ( src/Common/Error.hs, dist/build/Common/Error.o )          
[ 8 of 27] Compiling Common.Util      ( src/Common/Util.hs, dist/build/Common/Util.o )            
[ 9 of 27] Compiling Core.IntRep      ( src/Core/IntRep.hs, dist/build/Core/IntRep.o )            
[10 of 27] Compiling Core.Pretty      ( src/Core/Pretty.hs, dist/build/Core/Pretty.o )            
[11 of 27] Compiling Core.CSet        ( src/Core/CSet.hs, dist/build/Core/CSet.o )                
[12 of 27] Compiling Core.Optimizations ( src/Core/Optimizations.hs, dist/build/Core/Optimizations
.o )                                                                                              
[13 of 27] Compiling Core.Rigidify.Generator ( src/Core/Rigidify/Generator.hs, dist/build/Core/Rig
idify/Generator.o )                                                                               
[14 of 27] Compiling Core.Rigidify.Pretty ( src/Core/Rigidify/Pretty.hs, dist/build/Core/Rigidify/
Pretty.o )                                                                                        
[15 of 27] Compiling Outer.Types      ( src/Outer/Types.hs, dist/build/Outer/Types.o )            
[16 of 27] Compiling Common.Conversions ( src/Common/Conversions.hs, dist/build/Common/Conversions
.o )                                                                                              
[17 of 27] Compiling Core.Rigidify.Data ( src/Core/Rigidify/Data.hs, dist/build/Core/Rigidify/Data
.o )                                                                                              
[18 of 27] Compiling Core.Rigidify    ( src/Core/Rigidify.hs, dist/build/Core/Rigidify.o )        
[19 of 27] Compiling Outer.ParseMonad ( src/Outer/ParseMonad.hs, dist/build/Outer/ParseMonad.o )  
[20 of 27] Compiling Outer.Lexer      ( dist/build/Outer/Lexer.hs, dist/build/Outer/Lexer.o )     
[21 of 27] Compiling Outer.Parser     ( dist/build/Outer/Parser.hs, dist/build/Outer/Parser.o )   
[22 of 27] Compiling Outer.Renamer    ( src/Outer/Renamer.hs, dist/build/Outer/Renamer.o )        
[23 of 27] Compiling Outer.Expander   ( src/Outer/Expander.hs, dist/build/Outer/Expander.o )      
[24 of 27] Compiling Outer.ClassMono  ( src/Outer/ClassMono.hs, dist/build/Outer/ClassMono.o )    
[25 of 27] Compiling Core.Semantics   ( src/Core/Semantics.hs, dist/build/Core/Semantics.o )      
                                                                                                  
src/Core/Semantics.hs:102:5:                                                                      
    Overlapping instances for MonadError                                                          
                                Message (RandT StdGen (Either Message))                           
      arising from a use of ‘throwError’                                                          
    Matching instances:                                                                           
      instance MonadError e m => MonadError e (RandT g m)                                         
        -- Defined in ‘Control.Monad.Trans.Random.Lazy’                                           
      instance MonadError e m => MonadError e (RandT StdGen m)                                    
        -- Defined at src/Core/Semantics.hs:91:10                                                 
    In the expression: throwError                                                                 
    In a stmt of a 'do' block: throwError $ mkUnSat msg                                           
    In the expression:                                                                            
      do { backRem -= 1;                                                                          
           throwError $ mkUnSat msg }                                                             
                                                                                                  
src/Core/Semantics.hs:128:7:                                                                      
    Overlapping instances for MonadError                                                          
                                Message (RandT StdGen (Either Message))                           
      arising from a use of ‘catchError’                                                          
    Matching instances:                                                                           
      instance MonadError e m => MonadError e (RandT g m)                                         
        -- Defined in ‘Control.Monad.Trans.Random.Lazy’                                           
      instance MonadError e m => MonadError e (RandT StdGen m)                                    
        -- Defined at src/Core/Semantics.hs:91:10                                                 
    In the expression:                                                                            
      m                                                                                           
      `catchError`                                                                                
        (\ err                                                                                    
           -> if isUnSat err then do { backtrack s ms } else throwError err)                      
    In an equation for ‘backtrack’:                                                               
        backtrack s (m : ms)                                                                      
          = m                                                                                     
            `catchError`                                                                          
              (\ err                                                                              
                 -> if isUnSat err then do { backtrack s ms } else throwError err)                
cabal: Error: some packages failed to install:                                                    
luck-0.1.0.0 failed during the building phase. The exception was:                                 
ExitFailure 1                                                                                     
yilongl@node:~/Luck/luck$

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.