nikivazou

{-@ LIQUID "--reflection"  @-}
{-@ LIQUID "--ple"         @-}
{-@ LIQUID "--no-totality" @-} 

module Fixme where 

import Language.Haskell.Liquid.ProofCombinators


bool1, bool2 :: Bool 

nikivazou

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple"        @-}
module ISort where 

import Prelude hiding (return, pure, (<*>), length, (>>=), head)

nikivazou

{-# LANGUAGE BangPatterns #-}
module Main where

main :: IO ()
main = putStrLn (show $ foo [1..10000000000])

-- without the bang assoc is not recursed
-- but it is recursed with the ! even with the rewrite Rule
withProof :: a -> () -> a 
withProof x !_ = x 

nikivazou

require 'rdl'
require 'types/core'
extend RDL::Annotate

require 'rubygems'  
require 'active_record'  


ActiveRecord::Base.establish_connection(  
:adapter  => "mysql2",  

nikivazou

(set-option :auto-config false)
(set-option :model true)
(set-option :model.partial false)

(set-option :smt.mbqi false)
(define-sort Elt () Int)
(define-sort Set () (Array Elt Bool))
(define-fun smt_set_emp () Set ((as const Set) false))
(define-fun smt_set_mem ((x Elt) (s Set)) Bool (select s x))
(define-fun smt_set_add ((s Set) (x Elt)) Set (store s x true))