mirror of
https://github.com/sdiehl/wiwinwlh.git
synced 2024-08-16 23:40:41 +03:00
liquidhaskell
This commit is contained in:
parent
c558356b4c
commit
d9b0154a99
2
Makefile
2
Makefile
@ -1,7 +1,7 @@
|
||||
PANDOC = pandoc
|
||||
IFORMAT = markdown
|
||||
FLAGS = --standalone --toc --toc-depth=2 --highlight-style pygments
|
||||
TEMPLATE = page.tmpl
|
||||
TEMPLATE = resources/page.tmpl
|
||||
STYLE = css/style.css
|
||||
|
||||
HTML = tutorial.html
|
||||
|
6
css/bootstrap-min.css
vendored
Normal file
6
css/bootstrap-min.css
vendored
Normal file
File diff suppressed because one or more lines are too long
@ -30,6 +30,13 @@ h1, h2, h3, h4, h5 {
|
||||
line-height: 1.1;
|
||||
}
|
||||
|
||||
pre {
|
||||
/* Override bootstrap */
|
||||
border: none;
|
||||
border-radius: 0px;
|
||||
background-color: inherit;
|
||||
}
|
||||
|
||||
pre code {
|
||||
/*font: 15px/19px Inconsolata, Monaco,"Lucida Console",Terminal,"Courier New",Courier;*/
|
||||
font: 12pt "Source Code Pro";
|
||||
|
@ -11,7 +11,8 @@
|
||||
<style type="text/css">
|
||||
$header-includes$
|
||||
</style>
|
||||
<link href="css/bootstrap-responsive.min.css" rel="stylesheet">
|
||||
<!--<link href="css/bootstrap-responsive.min.css" rel="stylesheet">-->
|
||||
<link href="css/bootstrap-min.css" rel="stylesheet">
|
||||
|
||||
<script>
|
||||
(function(i,s,o,g,r,a,m){i['GoogleAnalyticsObject']=r;i[r]=i[r]||function(){
|
||||
@ -29,9 +30,11 @@
|
||||
$highlighting-css$
|
||||
</style>
|
||||
$endif$
|
||||
|
||||
$for(css)$
|
||||
<link rel="stylesheet" href="$css$" $if(html5)$$else$type="text/css" $endif$/>
|
||||
$endfor$
|
||||
|
||||
$if(math)$
|
||||
$if(html5)$
|
||||
$else$
|
||||
@ -65,6 +68,6 @@ $body$
|
||||
|
||||
</div>
|
||||
<script src="https://code.jquery.com/jquery.js"></script>
|
||||
<script src="nav.js"></script>
|
||||
<script src="js/nav.js"></script>
|
||||
</body>
|
||||
</html>
|
15
src/01-basics/README.md
Normal file
15
src/01-basics/README.md
Normal file
@ -0,0 +1,15 @@
|
||||
Monads
|
||||
======
|
||||
|
||||
```bash
|
||||
$ stach exec list.hs
|
||||
$ stach exec list_impl.hs
|
||||
$ stach exec maybe.hs
|
||||
$ stach exec maybe_impl.hs
|
||||
$ stach exec reader.hs
|
||||
$ stach exec reader_impl.hs
|
||||
$ stach exec state.hs
|
||||
$ stach exec state_impl.hs
|
||||
$ stach exec writer.hs
|
||||
$ stach exec writer_impl.hs
|
||||
```
|
15
src/02-monads/README.md
Normal file
15
src/02-monads/README.md
Normal file
@ -0,0 +1,15 @@
|
||||
Monads
|
||||
======
|
||||
|
||||
```bash
|
||||
$ stach exec list.hs
|
||||
$ stach exec list_impl.hs
|
||||
$ stach exec maybe.hs
|
||||
$ stach exec maybe_impl.hs
|
||||
$ stach exec reader.hs
|
||||
$ stach exec reader_impl.hs
|
||||
$ stach exec state.hs
|
||||
$ stach exec state_impl.hs
|
||||
$ stach exec writer.hs
|
||||
$ stach exec writer_impl.hs
|
||||
```
|
15
src/03-monad-transformers/README.md
Normal file
15
src/03-monad-transformers/README.md
Normal file
@ -0,0 +1,15 @@
|
||||
Monads
|
||||
======
|
||||
|
||||
```bash
|
||||
$ stach exec list.hs
|
||||
$ stach exec list_impl.hs
|
||||
$ stach exec maybe.hs
|
||||
$ stach exec maybe_impl.hs
|
||||
$ stach exec reader.hs
|
||||
$ stach exec reader_impl.hs
|
||||
$ stach exec state.hs
|
||||
$ stach exec state_impl.hs
|
||||
$ stach exec writer.hs
|
||||
$ stach exec writer_impl.hs
|
||||
```
|
15
src/04-extensions/README.md
Normal file
15
src/04-extensions/README.md
Normal file
@ -0,0 +1,15 @@
|
||||
Monads
|
||||
======
|
||||
|
||||
```bash
|
||||
$ stach exec list.hs
|
||||
$ stach exec list_impl.hs
|
||||
$ stach exec maybe.hs
|
||||
$ stach exec maybe_impl.hs
|
||||
$ stach exec reader.hs
|
||||
$ stach exec reader_impl.hs
|
||||
$ stach exec state.hs
|
||||
$ stach exec state_impl.hs
|
||||
$ stach exec writer.hs
|
||||
$ stach exec writer_impl.hs
|
||||
```
|
15
src/05-laziness/README.md
Normal file
15
src/05-laziness/README.md
Normal file
@ -0,0 +1,15 @@
|
||||
Monads
|
||||
======
|
||||
|
||||
```bash
|
||||
$ stach exec list.hs
|
||||
$ stach exec list_impl.hs
|
||||
$ stach exec maybe.hs
|
||||
$ stach exec maybe_impl.hs
|
||||
$ stach exec reader.hs
|
||||
$ stach exec reader_impl.hs
|
||||
$ stach exec state.hs
|
||||
$ stach exec state_impl.hs
|
||||
$ stach exec writer.hs
|
||||
$ stach exec writer_impl.hs
|
||||
```
|
30
tutorial.md
30
tutorial.md
@ -1144,6 +1144,8 @@ Shake
|
||||
This is an advanced section, and is not typically necessary to write Haskell.
|
||||
</div>
|
||||
|
||||
* [Shake Manual](https://github.com/ndmitchell/shake/blob/master/docs/Manual.md)
|
||||
|
||||
<hr/>
|
||||
|
||||
Monads
|
||||
@ -6169,19 +6171,31 @@ Liquid Haskell
|
||||
LiquidHaskell is not typically necessary to write Haskell.
|
||||
</div>
|
||||
|
||||
Add the following line to your ``/etc/sources.list``:
|
||||
LiquidHaskell is an extension to GHC's typesystem that adds the capactity for
|
||||
refinement types using the annotation syntax. The type signatures of functions
|
||||
can be checked by the external for richer type semantics than default GHC
|
||||
provides, including non-exhaustive patterns and complex arithemtic properties
|
||||
that require external SMT solvers to verify. For instance LiquidHaskell can
|
||||
statically verify that a function that operates over a ``Maybe a`` is always
|
||||
given a ``Just`` or that an arithmetic functions always yields an Int that is
|
||||
even positive number.
|
||||
|
||||
To Install LiquidHaskell in Ubuntu add the following line to your
|
||||
``/etc/sources.list``:
|
||||
|
||||
```bash
|
||||
deb http://ppa.launchpad.net/hvr/z3/ubuntu trusty main
|
||||
```
|
||||
|
||||
Install the
|
||||
And then install the external SMT solver.
|
||||
|
||||
```bash
|
||||
$ sudo apt-key adv --keyserver keyserver.ubuntu.com --recv-keys F6F88286
|
||||
$ sudo apt-get install z3
|
||||
```
|
||||
|
||||
Then clone the repo and build it using stack.
|
||||
|
||||
```bash
|
||||
$ git clone --recursive git@github.com:ucsd-progsys/liquidhaskell.git
|
||||
$ cd liquidhaskell
|
||||
@ -6220,6 +6234,13 @@ Done solving.
|
||||
**** RESULT: SAFE **************************************************************
|
||||
```
|
||||
|
||||
For more extensive documentation and further use cases see the official
|
||||
documentation:
|
||||
|
||||
* [Liquid Haskell Documentation](https://ucsd-progsys.github.io/liquidhaskell-tutorial/01-intro.html)
|
||||
|
||||
</hr>
|
||||
|
||||
Generics
|
||||
========
|
||||
|
||||
@ -7860,6 +7881,11 @@ TODO
|
||||
~~~~ {.haskell include="src/24-parsing/happy/input.test"}
|
||||
~~~~
|
||||
|
||||
Configurator
|
||||
------------
|
||||
|
||||
TODO
|
||||
|
||||
Streaming
|
||||
=========
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user