-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathBasicsTest2.hs.html
46 lines (45 loc) · 8.01 KB
/
BasicsTest2.hs.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<html>
<head>
<title>/home/michael/liquidmeta_public/BasicsTest2.hs</title>
</head>
<head>
<link type='text/css' rel='stylesheet' href='liquid.css' />
</head>
<body>
<hr>
Put mouse over identifiers to see inferred types
<pre><span class=hs-linenum> 1: </span><a class=annot href="#"><span class=annottext>GHC.Types.Module</span><span class='hs-comment'>{-# LANGUAGE GADTs #-}</span></a>
<span class=hs-linenum> 2: </span>
<span class=hs-linenum> 3: </span><span class='hs-keyword'>{-@</span> <span class='hs-conid'>LIQUID</span> <span class='hs-str'>"--reflection"</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum> 4: </span><span class='hs-keyword'>{-@</span> <span class='hs-conid'>LIQUID</span> <span class='hs-str'>"--ple"</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum> 5: </span><span class='hs-keyword'>{-@</span> <span class='hs-conid'>LIQUID</span> <span class='hs-str'>"--short-names"</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum> 6: </span>
<span class=hs-linenum> 7: </span><span class='hs-keyword'>module</span> <span class='hs-conid'>BasicsTest2</span> <span class='hs-keyword'>where</span>
<span class=hs-linenum> 8: </span>
<span class=hs-linenum> 9: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Prelude</span> <span class='hs-varid'>hiding</span> <span class='hs-layout'>(</span><span class='hs-varid'>max</span><span class='hs-layout'>)</span>
<span class=hs-linenum>10: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Language.Haskell.Liquid.ProofCombinators</span> <span class='hs-varid'>hiding</span> <span class='hs-layout'>(</span><span class='hs-varid'>withProof</span><span class='hs-layout'>)</span>
<span class=hs-linenum>11: </span><span class='hs-keyword'>import</span> <span class='hs-keyword'>qualified</span> <span class='hs-conid'>Data.Set</span> <span class='hs-keyword'>as</span> <span class='hs-conid'>S</span>
<span class=hs-linenum>12: </span>
<span class=hs-linenum>13: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>BasicsTest1</span>
<span class=hs-linenum>14: </span>
<span class=hs-linenum>15: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>simple'</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>g</span><span class='hs-conop'>:</span><span class='hs-conid'>FEnv</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{ a:</span><span class='hs-conid'>Vname</span> <span class='hs-keyword'>| in_envF a g }</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{ k:</span><span class='hs-conid'>Kind</span> <span class='hs-keyword'>| tv_bound_inF a k g }</span>
<span class=hs-linenum>16: </span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{ g':</span><span class='hs-conid'>FEnv</span> <span class='hs-keyword'>| not (in_envF a g') }</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>17: </span><span class='hs-definition'>simple'</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>FEnv</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Vname</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Kind</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>FEnv</span>
<span class=hs-linenum>18: </span><a class=annot href="#"><span class=annottext>x1:BasicsTest1.FEnv -> x2:{VV : GHC.Types.Int | in_envF VV x1} -> {k : BasicsTest1.Kind | tv_bound_inF x2 k x1} -> {g' : BasicsTest1.FEnv | not (in_envF x2 g')}</span><span class='hs-definition'>simple'</span></a> <a class=annot href="#"><span class=annottext>BasicsTest1.FEnv</span><span class='hs-varid'>g</span></a> <a class=annot href="#"><span class=annottext>{VV : GHC.Types.Int | in_envF VV g}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>{k : BasicsTest1.Kind | tv_bound_inF a k g}</span><span class='hs-varid'>k</span></a> <span class='hs-keyglyph'>=</span> <span class='hs-keyword'>case</span> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | v == g}</span><span class='hs-varid'>g</span></a> <span class='hs-keyword'>of</span>
<span class=hs-linenum>19: </span> <span class='hs-layout'>(</span><span class='hs-conid'>FCons</span> <span class='hs-varid'>y</span> <span class='hs-varid'>s</span> <span class='hs-varid'>g'</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>case</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Bool | (v <=> a == y)
&& v == == a y}</span><span class='hs-layout'>(</span></a> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | in_envF v g
&& v == a}</span><span class='hs-varid'>a</span></a> <span class='hs-varop'>==</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == y}</span><span class='hs-varid'>y</span></a> <span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<span class=hs-linenum>20: </span> <span class='hs-layout'>(</span><span class='hs-conid'>False</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>x1:BasicsTest1.FEnv -> x2:{VV : GHC.Types.Int | in_envF VV x1} -> {k : BasicsTest1.Kind | tv_bound_inF x2 k x1} -> {g' : BasicsTest1.FEnv | not (in_envF x2 g')}</span><span class='hs-varid'>simple'</span></a> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | v == g'}</span><span class='hs-varid'>g'</span></a> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | in_envF v g
&& v == a}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.Kind | tv_bound_inF a v g
&& v == k}</span><span class='hs-varid'>k</span></a>
<span class=hs-linenum>21: </span> <span class='hs-layout'>(</span><span class='hs-conid'>FConsT</span> <span class='hs-varid'>a'</span> <span class='hs-varid'>k'</span> <span class='hs-varid'>g'</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>case</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Bool | (v <=> a == a')
&& v == == a a'}</span><span class='hs-layout'>(</span></a> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | in_envF v g
&& v == a}</span><span class='hs-varid'>a</span></a> <span class='hs-varop'>==</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == a'}</span><span class='hs-varid'>a'</span></a> <span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<span class=hs-linenum>22: </span> <span class='hs-layout'>(</span><span class='hs-conid'>True</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class=hs-error><a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | v == g'}</span><span class='hs-varid'>g'</span></a></span>
<span class=hs-linenum>23: </span> <span class='hs-layout'>(</span><span class='hs-conid'>False</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>x1:BasicsTest1.FEnv -> x2:{VV : GHC.Types.Int | in_envF VV x1} -> {k : BasicsTest1.Kind | tv_bound_inF x2 k x1} -> {g' : BasicsTest1.FEnv | not (in_envF x2 g')}</span><span class='hs-varid'>simple'</span></a> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | v == g'}</span><span class='hs-varid'>g'</span></a> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | in_envF v g
&& v == a}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.Kind | tv_bound_inF a v g
&& v == k}</span><span class='hs-varid'>k</span></a>
</pre>
</body>
</html>