diff options
Diffstat (limited to 'doc/Tutorial.md')
| -rw-r--r-- | doc/Tutorial.md | 103 |
1 files changed, 85 insertions, 18 deletions
diff --git a/doc/Tutorial.md b/doc/Tutorial.md index b9a5896..439d245 100644 --- a/doc/Tutorial.md +++ b/doc/Tutorial.md @@ -241,34 +241,101 @@ setoid package doesn't use them, we'll use them in a few examples. The `Overlap` relation from Examples 1 and 2 is symmetric: <code class="IdrisCode"> -Symm<span class="IdrisKeyword">e</span>tric (List a) Overlap where<br /> - symmetric xs\_overlaps\_ys = Overlapping<br /> - { common = xs\_overlaps\_ys.common<br /> - , lhsPos = xs\_overlaps\_ys.rhsPos<br /> - , rhsPos = xs\_overlaps\_ys.lhsPos<br /> - }<br /> +<span class="IdrisType">Symmetric</span> <span class="IdrisKeyword">(</span><span class="IdrisType">List</span> <span class="IdrisBound">a</span><span class="IdrisKeyword">)</span> <span class="IdrisType">Overlap</span> <span class="IdrisKeyword">where</span><br /> + <span class="IdrisFunction">symmetric</span> <span class="IdrisBound">xs\_overlaps\_ys</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Overlapping</span><br /> + <span class="IdrisKeyword">{</span> <span class="IdrisBound">common</span> <span class="IdrisKeyword">=</span> <span class="IdrisBound">xs\_overlaps\_ys</span><span class="IdrisFunction">.common</span><br /> + <span class="IdrisKeyword">,</span> <span class="IdrisBound">lhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisBound">xs\_overlaps\_ys</span><span class="IdrisFunction">.rhsPos</span><br /> + <span class="IdrisKeyword">,</span> <span class="IdrisBound">rhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisBound">xs\_overlaps\_ys</span><span class="IdrisFunction">.lhsPos</span><br /> + <span class="IdrisKeyword">}</span><br /> </code> However, `Overlap` is neither reflexive nor transitive: * The empty list doesn't overlap with itself: <code class="IdrisCode"> -Ex3 : Not (Overlap [] [])<br /> -Ex3 nil\_overlaps\_nil = case nil\_overlaps\_nil.lhsPos of<br /> -<span class="IdrisFunction"> \_</span> <span class="IdrisKeyword">i</span>m<span class="IdrisKeyword">p</span>o<span class="IdrisType">ssible</span><br /> +<span class="IdrisFunction">Ex3</span> <span class="IdrisKeyword">:</span> <span class="IdrisFunction">Not</span> <span class="IdrisKeyword">(</span><span class="IdrisType">Overlap</span> <span class="IdrisData">[]</span> <span class="IdrisData">[]</span><span class="IdrisKeyword">)</span><br /> +<span class="IdrisFunction">Ex3</span> <span class="IdrisBound">nil\_overlaps\_nil</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">case</span> <span class="IdrisBound">nil\_overlaps\_nil</span><span class="IdrisFunction">.lhsPos</span> <span class="IdrisKeyword">of</span><br /> + <span class="IdrisKeyword">\_</span> <span class="IdrisKeyword">impossible</span><br /> </code> * Two lists may overlap with a middle list, but on different elements. For example: <code class="IdrisCode"> -Ex<span class="IdrisData">4</span> <span class="IdrisData">: ( Overlap</span> <span class="IdrisData">[</span>1<span class="IdrisKeyword">]</span><span class="IdrisData"> [1,2</span>]<br /> - <span class="IdrisData"> </span> <span class="IdrisKeyword"> </span> <span class="IdrisBound">, Overlap [1,2] </span>[<span class="IdrisKeyword">2]</span><br /> - <span class="IdrisData"> , No</span>t<span class="IdrisKeyword"> </span>(<span class="IdrisKeyword">Overlap [1</span>] [2]))<br /> -Ex<span class="IdrisKeyword">4</span> =<br /> - ( Overlapping 1 Here Here<br /> - , Overlapping 2 (There Here) Here<br /> - , \ one\_overlaps\_two => case one\_overlaps\_two.lhsPos of<br /> - There \_ impossible<br /> - )<br /> +<span class="IdrisFunction">Ex4</span> <span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1]</span> <span class="IdrisData">[1,2]</span><br /> + <span class="IdrisType">,</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1,2]</span> <span class="IdrisData">[2]</span><br /> + <span class="IdrisType">,</span> <span class="IdrisFunction">Not</span> <span class="IdrisKeyword">(</span><span class="IdrisType">Overlap</span> <span class="IdrisData">[1]</span> <span class="IdrisData">[2]</span><span class="IdrisKeyword">))</span><br /> +<span class="IdrisFunction">Ex4</span> <span class="IdrisKeyword">=</span><br /> + <span class="IdrisKeyword">(</span> <span class="IdrisData">Overlapping</span> <span class="IdrisData">1</span> <span class="IdrisData">Here</span> <span class="IdrisData">Here</span><br /> + <span class="IdrisData">,</span> <span class="IdrisData">Overlapping</span> <span class="IdrisData">2</span> <span class="IdrisKeyword">(</span><span class="IdrisData">There</span> <span class="IdrisData">Here</span><span class="IdrisKeyword">)</span> <span class="IdrisData">Here</span><br /> + <span class="IdrisData">,</span> <span class="IdrisKeyword">\</span> <span class="IdrisBound">one\_overlaps\_two</span> <span class="IdrisKeyword">=></span> <span class="IdrisKeyword">case</span> <span class="IdrisBound">one\_overlaps\_two</span><span class="IdrisFunction">.lhsPos</span> <span class="IdrisKeyword">of</span><br /> + <span class="IdrisData">There</span> <span class="IdrisKeyword">\_</span> <span class="IdrisKeyword">impossible</span><br /> + <span class="IdrisKeyword">)</span><br /> </code> The outer lists agree on `1` and `2`, respectively, but they can't overlap on on the first element of either, which exhausts all possibilities of overlap. + + +<code class="IdrisCode"> +<span class="IdrisBound">-</span>-<span class="IdrisFunction"> TO</span>D<span class="IdrisBound">O</span>:<span class="IdrisKeyword"> </span>c<span class="IdrisKeyword">l</span><span class="IdrisBound">e</span><span class="IdrisFunction">an t</span>h<span class="IdrisFunction">i</span>s<span class="IdrisBound"> </span><span class="IdrisFunction">up</span><br /> +(.+.) : (x, y : INT) -> INT<br /> +<span class="IdrisFunction">x .+.</span> <span class="IdrisKeyword">y</span> <span class="IdrisKeyword">=</span><span class="IdrisBound"> </span><span class="IdrisKeyword">(</span>x<span class="IdrisBound">.</span>p<span class="IdrisKeyword">o</span>s<span class="IdrisType"> + </span><span class="IdrisKeyword">y</span>.<span class="IdrisKeyword">po</span>s<span class="IdrisType">) .</span>-. (x.neg + y.neg)<br /> +<br /> +(.\*.) : (x, y : INT) -> INT<br /> +<span class="IdrisFunction">x</span><span class="IdrisKeyword"> </span>.<span class="IdrisFunction">\*</span>.<span class="IdrisKeyword"> </span>y<span class="IdrisType"> = </span>(x.pos \* y.pos + x.neg \* y.neg) .-. (x.pos \* y.neg + x.neg \* y.pos)<br /> +<br /> +<span class="IdrisFunction">O</span>,<span class="IdrisKeyword"> </span>I<span class="IdrisData"> </span>:<span class="IdrisData"> IN</span>T<br /> +<span class="IdrisFunction">O = 0 .-. 0</span><br /> +<span class="IdrisFunction">I = 1 .-. 0</span><br /> +plusIntZeroLftNeutral : (x : INT) -> O .+. x `SameDiff` x<br /> +<span class="IdrisFunction">plusIntZeroLftNeutral</span> <span class="IdrisKeyword">x</span> <span class="IdrisKeyword">=</span><span class="IdrisBound"> </span>C<span class="IdrisKeyword">h</span>e<span class="IdrisType">ck </span><span class="IdrisKeyword">R</span>e<span class="IdrisKeyword">fl</span><br /> +<br /> +plusIntZeroRgtNeutral : (x : INT) -> <span class="IdrisKeyword">x</span><span class="IdrisBound"> </span>.<span class="IdrisKeyword">+</span>.<span class="IdrisFunction"> O `SameDiff</span><span class="IdrisKeyword">`</span> x<br /> +plusIntZeroRgtNeutral x = Check (solv<span class="IdrisKeyword">e</span><span class="IdrisFunction"> </span>2<span class="IdrisData"> </span>M<span class="IdrisFunction">ono</span>i<span class="IdrisFunction">d.</span><span class="IdrisKeyword">C</span>o<span class="IdrisFunction">mmu</span>t<span class="IdrisFunction">a</span>t<span class="IdrisData">i</span>ve.Free.Free<br /> + <span class="IdrisFunction"> </span> <span class="IdrisFunction">{</span>a<span class="IdrisData"> </span>=<span class="IdrisFunction"> Na</span>t<span class="IdrisKeyword">.</span><span class="IdrisFunction">A</span>d<span class="IdrisData">d</span>i<span class="IdrisFunction">tiv</span>e<span class="IdrisFunction">} </span><span class="IdrisKeyword">$</span><br /> + (X 0 .+. O1) .+. X 1<br /> +<span class="IdrisFunction"> </span> <span class="IdrisKeyword"> </span> <span class="IdrisKeyword"> </span><span class="IdrisBound"> </span><span class="IdrisKeyword"> </span><span class="IdrisBound"> </span><span class="IdrisKeyword"> </span><span class="IdrisBound"> </span> <span class="IdrisKeyword"> </span> <span class="IdrisType"> </span><span class="IdrisKeyword">=</span>-<span class="IdrisKeyword">= </span>X<span class="IdrisBound"> </span>0<span class="IdrisFunction"> .+</span>.<span class="IdrisKeyword"> </span><span class="IdrisBound">(</span>X<span class="IdrisFunction"> 1 </span>.<span class="IdrisBound">+</span><span class="IdrisKeyword">.</span> <span class="IdrisType">O1))</span><br /> +<br /> +plusInrAssociative : (x,y,z : INT) -><span class="IdrisKeyword"> </span><span class="IdrisBound">x</span> <span class="IdrisKeyword">.</span>+<span class="IdrisFunction">. (y .+. z) </span><span class="IdrisKeyword">`</span>SameDiff` (x .+. y) .+. z<br /> +plusInrAssociative x y z = Check $<span class="IdrisKeyword"> </span><span class="IdrisFunction">(</span>s<span class="IdrisData">o</span>l<span class="IdrisFunction">ve </span>6<span class="IdrisKeyword"> </span><span class="IdrisFunction">M</span>o<span class="IdrisData">n</span>o<span class="IdrisFunction">id.</span>C<span class="IdrisFunction">o</span>m<span class="IdrisData">m</span><span class="IdrisKeyword">ut</span>a<span class="IdrisFunction">tiv</span>e<span class="IdrisKeyword">.F</span><span class="IdrisFunction">r</span>e<span class="IdrisData">e</span>.<span class="IdrisFunction">Fre</span>e<br /> + <span class="IdrisFunction"> </span>{<span class="IdrisKeyword">a</span><span class="IdrisFunction"> </span>=<span class="IdrisData"> </span>N<span class="IdrisFunction">at.</span>A<span class="IdrisFunction">d</span>d<span class="IdrisData">i</span>t<span class="IdrisFunction">ive</span>}<span class="IdrisFunction"> </span>$<br /> + (X 0 .+. (X 1 .+. X 2)) .+. ((X 3 .+. X 4) .+. X 5)<br /> +<span class="IdrisKeyword"> </span> <span class="IdrisType"> </span> <span class="IdrisKeyword"> </span> <span class="IdrisType"> </span> <span class="IdrisKeyword"> </span> =-= (X 0 .+. X 1 .+. X 2) .+. (X 3 .+. (X 4 .+. X 5)))<br /> +<br /> +da<span class="IdrisData">ta IN</span>T<span class="IdrisKeyword">'</span> <span class="IdrisType">: T</span>y<span class="IdrisKeyword">pe</span> <span class="IdrisType">wher</span>e<br /> + IPos : Nat -> INT'<br /> +<span class="IdrisType"> IN</span>e<span class="IdrisType">gS :</span> <span class="IdrisType">Nat -> </span>I<span class="IdrisKeyword">NT'</span><br /> +<br /> +Ca<span class="IdrisFunction">st I</span>N<span class="IdrisKeyword">T</span><span class="IdrisData">' Int</span>e<span class="IdrisBound">g</span><span class="IdrisKeyword">e</span>r<span class="IdrisKeyword"> </span>w<span class="IdrisFunction">h</span>e<span class="IdrisFunction">re</span><br /> + cast (IPos k) = cast k<br /> +<span class="IdrisType"> ca</span>s<span class="IdrisType">t (I</span>N<span class="IdrisType">egS</span> <span class="IdrisKeyword">k) = </span>- cast (S k)<br /> +<br /> +Ca<span class="IdrisFunction">st I</span>N<span class="IdrisKeyword">T</span><span class="IdrisData">' INT</span> <span class="IdrisBound">w</span><span class="IdrisKeyword">h</span>e<span class="IdrisKeyword">r</span>e<br /> + cast (IPos k) = k .-. 0<br /> +<span class="IdrisFunction"> cast (I</span>N<span class="IdrisKeyword">e</span>g<span class="IdrisType">S k</span>)<span class="IdrisKeyword"> =</span> <span class="IdrisType">0 .</span>-. (S k)<br /> +<br /> +<span class="IdrisFunction">normalise</span> <span class="IdrisBound">:</span><span class="IdrisKeyword"> IN</span><span class="IdrisData">T</span> <span class="IdrisBound">-</span><span class="IdrisKeyword">></span> <span class="IdrisData">INT</span><br /> +<span class="IdrisFunction">normalise</span> <span class="IdrisBound">i</span><span class="IdrisKeyword">@(0</span><span class="IdrisData"> </span>.<span class="IdrisBound">-</span><span class="IdrisKeyword">.</span> <span class="IdrisData">neg</span> <span class="IdrisKeyword"> </span><span class="IdrisData"> </span> <span class="IdrisBound"> </span><span class="IdrisKeyword"> )</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">i</span><br /> +normalise i@((S k) .-. 0 ) = i<br /> +<span class="IdrisFunction">normalise i@((S k) </span>.<span class="IdrisKeyword">-</span>.<span class="IdrisKeyword"> </span><span class="IdrisBound">(</span>S<span class="IdrisKeyword"> </span>j<span class="IdrisType">)) </span><span class="IdrisKeyword">=</span> <span class="IdrisKeyword">no</span>r<span class="IdrisType">malise</span> <span class="IdrisKeyword">(k</span><span class="IdrisFunction"> .-. j)</span><br /> +<br /> +<span class="IdrisFunction">normaliseEitherZero</span> <span class="IdrisBound">:</span><span class="IdrisKeyword"> (x</span><span class="IdrisData"> </span>:<span class="IdrisBound"> </span><span class="IdrisKeyword">I</span>N<span class="IdrisData">T) </span>-<span class="IdrisData">></span> Eit<span class="IdrisKeyword">h</span>e<span class="IdrisKeyword">r</span> <span class="IdrisData">((nor</span>m<span class="IdrisData">alis</span>e x).pos = Z) ((normalise x).neg = Z)<br /> +<span class="IdrisFunction">normaliseEitherZero</span> <span class="IdrisBound">i</span><span class="IdrisKeyword">@(0</span><span class="IdrisData"> </span>.<span class="IdrisBound">-</span><span class="IdrisKeyword">.</span> <span class="IdrisData">neg</span> <span class="IdrisKeyword"> </span><span class="IdrisData"> </span> <span class="IdrisBound"> </span><span class="IdrisKeyword"> )</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">Left Refl</span><br /> +normaliseEitherZero i@((S k) .-. 0 ) = Right Refl<br /> +<span class="IdrisType">norm</span>a<span class="IdrisType">lis</span>e<span class="IdrisType">Eith</span>e<span class="IdrisKeyword">rZero</span> i@((S k) .-. (S j)) = normaliseEitherZero (k .-. j)<br /> +<br /> +Cast<span class="IdrisKeyword"> INT</span> <span class="IdrisFunction">INT' where</span><br /> + cast<span class="IdrisKeyword"> </span><span class="IdrisData">x = </span>l<span class="IdrisBound">e</span><span class="IdrisKeyword">t</span> <span class="IdrisKeyword">(p</span>o<span class="IdrisKeyword">s .-</span>.<span class="IdrisBound"> ne</span>g<span class="IdrisKeyword">) </span>= normalise x in<br /> + case<span class="IdrisData"> </span>n<span class="IdrisKeyword">or</span>m<span class="IdrisData">alis</span>e<span class="IdrisData">E</span>itherZero x of<br /> + (L<span class="IdrisKeyword">e</span><span class="IdrisData">f</span>t<span class="IdrisBound"> </span><span class="IdrisKeyword">y</span>)<span class="IdrisKeyword"> =</span>><span class="IdrisData"> case</span> <span class="IdrisBound">n</span>eg of<br /> + <span class="IdrisKeyword"> </span><span class="IdrisData"> 0 =></span> <span class="IdrisBound">I</span><span class="IdrisKeyword">P</span>o<span class="IdrisKeyword">s </span>0<br /> + (S k) => INegS k<br /> +<span class="IdrisComment"> (Right y) => IPo</span>s pos<br /> +<br /> +<span class="IdrisComment">-- stuff you can show:</span><br /> +<br /> +<span class="IdrisBound">-</span>-<span class="IdrisFunction"> x </span>`<span class="IdrisBound">S</span>a<span class="IdrisKeyword">m</span>e<span class="IdrisFunction">Diff</span>`<span class="IdrisKeyword"> </span><span class="IdrisFunction">y -></span> <span class="IdrisBound">n</span>o<span class="IdrisFunction">rma</span>l<span class="IdrisFunction">ise </span>x<span class="IdrisBound"> </span><span class="IdrisKeyword">=</span> normalise y<br /> +<span class="IdrisBound">(</span>:<span class="IdrisFunction">\*:)</span>,<span class="IdrisBound"> </span>(<span class="IdrisKeyword">:</span>+<span class="IdrisFunction">:) :</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">x,y </span>:<span class="IdrisBound"> </span>I<span class="IdrisFunction">NT'</span>)<span class="IdrisFunction"> -> </span>I<span class="IdrisBound">N</span><span class="IdrisKeyword">T</span>'<br /> +x :+: y = cast (cast x .+. cast y)<br /> +x :\*: y = cast (cast x .\*. cast y)<br /> +<br /> +</code> + |