Changeset 11


Ignore:
Timestamp:
Nov 15, 2012, 12:16:02 AM (13 years ago)
Author:
gobi
Message:

cabal file

Location:
sizechecking
Files:
4 added
1 deleted
4 edited

Legend:

Unmodified
Added
Removed

  • sizechecking/Examples.hs

    r10 r11  
    262262        if P.not s then 
    263263            M.return [name] 
    264         else 
     264          else 
    265265            M.return [] 
    266266 
    … …  
    268268    if List.null f then  
    269269        P.putStrLn "All ok." 
    270     else do 
     270      else do 
    271271        P.putStr $ "\n\nFailed test cases: " 
    272272        P.putStrLn $ List.intercalate ", " f 
     273 

  • sizechecking/README.html

    r5 r11  
    99<body> 
    1010<h2 id="prerequisites">Prerequisites</h2> 
    11 <p>You need at least version 2011.4.0.0 of haskell platform and the package value-supply. If you have haskell platform installed you can install value-supply by typing</p> 
     11<p>You need at least version 2011.4.0.0 of the Haskell platform, an installed <a href="http://research.microsoft.com/en-us/um/redmond/projects/z3/">Z3</a> and the package value-supply. If you have a working Haskell platform installed you can install value-supply by typing</p> 
    1212<pre><code>cabal install value-supply</code></pre> 
    1313<h2 id="source-files">Source files</h2> 
    … …  
    2727</dl> 
    2828<h2 id="using-the-examples">Using the examples</h2> 
    29 <pre><code>$ ghci Examples.hs  
     29<pre><code>$ ghci Examples.hs 
    3030GHCi, version 7.0.4: http://www.haskell.org/ghc/  :? for help 
    3131Loading package ghc-prim ... linking ... done. 
    … …  
    3838[4 of 4] Compiling Main             ( Examples.hs, interpreted ) 
    3939Ok, modules loaded: Lambda, SizedExp, Constraints, Main. 
    40 *Main&gt; </code></pre> 
    41 <p>Type “<code>runTests</code>” to run all test cases or type “<code>prove map</code>” to prove the function named map.</p> 
     40*Main&gt;</code></pre> 
     41<p>Type &quot;<code>runTests</code>&quot; to run all test cases or type &quot;<code>prove map</code>&quot; to prove the function named map.</p> 
    4242<h2 id="under-windows">Under Windows</h2> 
    4343<p>It is not perfect, and you will see a box after every special character, but at least it works.</p> 
    … …  
    65654     where body f l = match l (nil) 
    66665             ( \x xs -&gt;  cons `app` (f `app` x) `app` (map `app` f `app` xs ))</code></pre> 
    67 <p>Here line 3 tells us map is a top-level binding, where the body of the function is defined in line 4–5 and its size expression is in line 1. Unfortunately the size expression language has not yet been embedded, so it is a bit difficult to read. Type <code>smap</code> in the GHC console to get a pretty printed form.</p> 
     67<p>Here line 3 tells us map is a top-level binding, where the body of the function is defined in line 4--5 and its size expression is in line 1. Unfortunately the size expression language has not yet been embedded, so it is a bit difficult to read. Type <code>smap</code> in the GHC console to get a pretty printed form.</p> 
    6868<pre><code>*Main&gt; smap 
    6969λf.Λs,g.List s (λi.f (g i))</code></pre> 

  • sizechecking/README.txt

    r5 r11  
    22------------- 
    33 
    4 You need at least version 2011.4.0.0 of haskell platform and the package 
    5 value-supply. If you have haskell platform installed you can install 
    6 value-supply by typing  
     4You need at least version 2011.4.0.0 of the Haskell platform, an installed 
     5[Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/) 
     6and the packages `sbv` and `value-supply`. If you have a working Haskell platform installed you can 
     7install value-supply by typing 
    78 
    8         cabal install value-supply 
     9        cabal install value-supply sbv 
    910 
    1011 
    … …  
    2526 
    2627~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
    27 $ ghci Examples.hs  
     28$ ghci Examples.hs 
    2829GHCi, version 7.0.4: http://www.haskell.org/ghc/  :? for help 
    2930Loading package ghc-prim ... linking ... done. 
    … …  
    3637[4 of 4] Compiling Main             ( Examples.hs, interpreted ) 
    3738Ok, modules loaded: Lambda, SizedExp, Constraints, Main. 
    38 *Main>  
     39*Main> 
    3940~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
    4041 
    … …  
    7980func $ a b 
    8081~~~~~~~~~~~~~~ 
    81  
    8282 
    8383 
    … …  
    130130  : embedding of the function application of our language to haskell 
    131131 
    132 There is also a function called `true` to denote we do not want to prove that 
     132There is also a function called `true` to denote that we do not want to prove that 
    133133branch. 
    134  
    135  

  • sizechecking/SizedExp.hs

    r5 r11  
    172172        putStrLn "QED" 
    173173        return True 
    174     else do 
     174      else do 
    175175        putStrLn "------------" 
    176176        putStrLn "Cannot prove: " 
Note: See TracChangeset for help on using the changeset viewer.