source: sizechecking/README.html @ 7

Last change on this file since 7 was 5, checked in by gobi, 13 years ago

size checking
File size: 4.3 KB
RevLine 
[5]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 haskell platform and the package value-supply. If you have haskell platform installed you can install value-supply by typing</p>
12<pre><code>cabal install value-supply</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 “<code>runTests</code>” to run all test cases or type “<code>prove map</code>” 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 we do not want to prove that branch.</p>
88</body>
89</html>
Note: See TracBrowser for help on using the repository browser.