source: sizechecking/trunk/README.html

Last change on this file was 18, checked in by gobi, 11 years ago

creating a branch
File size: 4.5 KB
Line 
1<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
2<html xmlns="http://www.w3.org/1999/xhtml">
3<head>
4  <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
5  <meta http-equiv="Content-Style-Type" content="text/css" />
6  <meta name="generator" content="pandoc" />
7  <title></title>
8</head>
9<body>
10<h2 id="prerequisites">Prerequisites</h2>
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 packages <code>sbv</code> and <code>value-supply</code>. If you have a working Haskell platform installed you can install value-supply by typing</p>
12<pre><code>cabal install value-supply sbv</code></pre>
13<h2 id="source-files">Source files</h2>
14<dl>
15<dt>Examples.hs</dt>
16<dd>Some examples
17</dd>
18<dt>SizedExp.hs</dt>
19<dd>Embedded language to prove size expressions
20</dd>
21<dt>Lambda.hs</dt>
22<dd>Size expressions
23</dd>
24<dt>Constraints.hs</dt>
25<dd>Constraint solver
26</dd>
27</dl>
28<h2 id="using-the-examples">Using the examples</h2>
29<pre><code>$ ghci Examples.hs
30GHCi, version 7.0.4: http://www.haskell.org/ghc/  :? for help
31Loading package ghc-prim ... linking ... done.
32Loading package integer-gmp ... linking ... done.
33Loading package base ... linking ... done.
34Loading package ffi-1.0 ... linking ... done.
35[1 of 4] Compiling Lambda           ( Lambda.hs, interpreted )
36[2 of 4] Compiling Constraints      ( Constraints.hs, interpreted )
37[3 of 4] Compiling SizedExp         ( SizedExp.hs, interpreted )
38[4 of 4] Compiling Main             ( Examples.hs, interpreted )
39Ok, modules loaded: Lambda, SizedExp, Constraints, Main.
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>
42<h2 id="under-windows">Under Windows</h2>
43<p>It is not perfect, and you will see a box after every special character, but at least it works.</p>
44<ul>
45<li>Open a console by running the program <code>cmd</code></li>
46<li>Issue the command <code>chcp 65001</code></li>
47<li>In the console cd to the trunk directory</li>
48<li>Now, you can run <code>ghci Examples.hs</code></li>
49</ul>
50<h2 id="introduction-to-haskell-syntax">Introduction to Haskell syntax</h2>
51<p>Haskell syntax is very much like Clean, however there are some expressions you cannot find in Clean.</p>
52<h3 id="backtick">Backtick</h3>
53<p>Every haskell function can be used as infix operator. For example the following two expressions are the same.</p>
54<pre><code>func a b
55a `func` b</code></pre>
56<h3 id="dollar">Dollar</h3>
57<p>Dollar sign is just explicit application (but with different precedence), so it can be used as a backward pipe operator. The following expressions are the same.</p>
58<pre><code>func (a b)
59func $ a b</code></pre>
60<h2 id="the-embedded-language">The Embedded Language</h2>
61<p>As an example the function <code>map</code> is examined.</p>
62<pre><code>1 smap  = Abs 5 $ AAbs 18 6 $ List (Var 18) (Abs 8$ App (Var 5) (App (Var 6) (Var 8)))
632 map :: (SizedExp se)  =&gt; Size se ( (a-&gt;b) -&gt; [a] -&gt; [b] )
643 map = bind smap body
654     where body f l = match l (nil)
665             ( \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>
68<pre><code>*Main&gt; smap
69λf.Λs,g.List s (λi.f (g i))</code></pre>
70<p>The type of the function tells us the underlying type, ie. <code>(a-&gt;b) -&gt; [a] -&gt; [b]</code>.</p>
71<p>The body of map corresponds to the following expression</p>
72<pre><code>match l of
73   nil       -&gt; nil
74   cons x xs -&gt; cons (f x) (map f xs)</code></pre>
75<p>In the embedded language <code>bind</code>, <code>match</code> and <code>app</code> are supercombinators.</p>
76<dl>
77<dt><code>bind sexp exp</code></dt>
78<dd><p>combines a size and an expression and creates a top-level binding</p>
79</dd>
80<dt><code>match list nilexp consexp</code></dt>
81<dd><p>embedding of the match operator of our language to haskell</p>
82</dd>
83<dt><code>app exp1 exp2</code></dt>
84<dd><p>embedding of the function application of our language to haskell</p>
85</dd>
86</dl>
87<p>There is also a function called <code>true</code> to denote that we do not want to prove that branch.</p>
88</body>
89</html>
Note: See TracBrowser for help on using the repository browser.