<?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> <html> <head> <!-- Generated by HsColour, http://code.haskell.org/~malcolm/hscolour/ --> <title>src/full/Agda/TypeChecking/LevelConstraints.hs</title> <link type='text/css' rel='stylesheet' href='hscolour.css' /> </head> <body> <pre><a name="line-1"></a> <a name="line-2"></a><span class='hs-keyword'>module</span> <span class='hs-conid'>Agda</span><span class='hs-varop'>.</span><span class='hs-conid'>TypeChecking</span><span class='hs-varop'>.</span><span class='hs-conid'>LevelConstraints</span> <span class='hs-layout'>(</span> <span class='hs-varid'>simplifyLevelConstraint</span> <span class='hs-layout'>)</span> <span class='hs-keyword'>where</span> <a name="line-3"></a> <a name="line-4"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Data</span><span class='hs-varop'>.</span><span class='hs-conid'>List</span> <a name="line-5"></a> <a name="line-6"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Agda</span><span class='hs-varop'>.</span><span class='hs-conid'>Syntax</span><span class='hs-varop'>.</span><span class='hs-conid'>Common</span> <span class='hs-layout'>(</span><span class='hs-conid'>Nat</span><span class='hs-layout'>)</span> <a name="line-7"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Agda</span><span class='hs-varop'>.</span><span class='hs-conid'>Syntax</span><span class='hs-varop'>.</span><span class='hs-conid'>Internal</span> <a name="line-8"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Agda</span><span class='hs-varop'>.</span><span class='hs-conid'>TypeChecking</span><span class='hs-varop'>.</span><span class='hs-conid'>Monad</span><span class='hs-varop'>.</span><span class='hs-conid'>Base</span> <a name="line-9"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Agda</span><span class='hs-varop'>.</span><span class='hs-conid'>TypeChecking</span><span class='hs-varop'>.</span><span class='hs-conid'>Substitute</span> <a name="line-10"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Agda</span><span class='hs-varop'>.</span><span class='hs-conid'>Utils</span><span class='hs-varop'>.</span><span class='hs-conid'>Size</span> <a name="line-11"></a> <a name="line-12"></a><a name="simplifyLevelConstraint"></a><span class='hs-comment'>-- | @simplifyLevelConstraint n c cs@ turns an @c@ into an equality</span> <a name="line-13"></a><span class='hs-comment'>-- constraint if it is an inequality constraint and the reverse</span> <a name="line-14"></a><span class='hs-comment'>-- inequality is contained in @cs@. Number @n@ is the length</span> <a name="line-15"></a><span class='hs-comment'>-- of the context @c@ is defined in.</span> <a name="line-16"></a><span class='hs-definition'>simplifyLevelConstraint</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Constraint</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Constraints</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Constraint</span> <a name="line-17"></a><span class='hs-definition'>simplifyLevelConstraint</span> <span class='hs-varid'>n</span> <span class='hs-varid'>new</span> <span class='hs-varid'>old</span> <span class='hs-keyglyph'>=</span> <a name="line-18"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>inequalities</span> <span class='hs-varid'>new</span> <span class='hs-keyword'>of</span> <a name="line-19"></a> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span> <span class='hs-conop'>:=<</span> <span class='hs-varid'>b</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>elem</span> <span class='hs-layout'>(</span><span class='hs-varid'>b'</span> <span class='hs-conop'>:=<</span> <span class='hs-varid'>a'</span><span class='hs-layout'>)</span> <span class='hs-varid'>leqs</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>LevelCmp</span> <span class='hs-conid'>CmpEq</span> <span class='hs-layout'>(</span><span class='hs-conid'>Max</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-conid'>Max</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>b</span><span class='hs-keyglyph'>]</span><span class='hs-layout'>)</span> <a name="line-20"></a> <span class='hs-keyword'>where</span> <span class='hs-layout'>(</span><span class='hs-varid'>a'</span><span class='hs-layout'>,</span> <span class='hs-varid'>b'</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>raise</span> <span class='hs-layout'>(</span><span class='hs-varid'>waterLevel</span> <span class='hs-comment'>-</span> <span class='hs-varid'>n</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>a</span><span class='hs-layout'>,</span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <a name="line-21"></a> <span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>new</span> <a name="line-22"></a> <span class='hs-keyword'>where</span> <a name="line-23"></a> <span class='hs-comment'>-- get the constraints plus their "waterLevels", i.e.,</span> <a name="line-24"></a> <span class='hs-comment'>-- length of contexts they are defined in</span> <a name="line-25"></a> <span class='hs-varid'>unClosure</span> <span class='hs-varid'>c</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>(</span><span class='hs-varid'>size</span> <span class='hs-layout'>(</span><span class='hs-varid'>envContext</span> <span class='hs-varop'>$</span> <span class='hs-varid'>clEnv</span> <span class='hs-varid'>cl</span><span class='hs-layout'>)</span><span class='hs-layout'>,</span> <span class='hs-varid'>clValue</span> <span class='hs-varid'>cl</span><span class='hs-layout'>)</span> <a name="line-26"></a> <span class='hs-keyword'>where</span> <span class='hs-varid'>cl</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>theConstraint</span> <span class='hs-varid'>c</span> <a name="line-27"></a> <span class='hs-layout'>(</span><span class='hs-varid'>ns</span><span class='hs-layout'>,</span> <span class='hs-varid'>ls</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>unzip</span> <span class='hs-varop'>$</span> <span class='hs-varid'>map</span> <span class='hs-varid'>unClosure</span> <span class='hs-varid'>old</span> <a name="line-28"></a> <span class='hs-comment'>-- compute the common water level</span> <a name="line-29"></a> <span class='hs-varid'>waterLevel</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Nat</span> <a name="line-30"></a> <span class='hs-varid'>waterLevel</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>maximum</span> <span class='hs-layout'>(</span><span class='hs-varid'>n</span><span class='hs-conop'>:</span><span class='hs-varid'>ns</span><span class='hs-layout'>)</span> <a name="line-31"></a> <span class='hs-comment'>-- convert deBruijn indices to deBruijn levels to</span> <a name="line-32"></a> <span class='hs-comment'>-- enable comparing constraints under different contexts</span> <a name="line-33"></a> <span class='hs-varid'>leqs</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>concatMap</span> <span class='hs-varid'>inequalities</span> <span class='hs-varop'>$</span> <span class='hs-varid'>zipWith</span> <span class='hs-varid'>raise</span> <span class='hs-layout'>(</span><span class='hs-varid'>map</span> <span class='hs-layout'>(</span><span class='hs-varid'>waterLevel</span> <span class='hs-comment'>-</span><span class='hs-layout'>)</span> <span class='hs-varid'>ns</span><span class='hs-layout'>)</span> <span class='hs-varid'>ls</span> <a name="line-34"></a> <a name="line-35"></a><a name="Leq"></a><span class='hs-keyword'>data</span> <span class='hs-conid'>Leq</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>PlusLevel</span> <span class='hs-conop'>:=<</span> <span class='hs-conid'>PlusLevel</span> <a name="line-36"></a> <span class='hs-keyword'>deriving</span> <span class='hs-layout'>(</span><span class='hs-conid'>Show</span><span class='hs-layout'>,</span> <span class='hs-conid'>Eq</span><span class='hs-layout'>)</span> <a name="line-37"></a> <a name="line-38"></a><a name="inequalities"></a><span class='hs-definition'>inequalities</span> <span class='hs-layout'>(</span><span class='hs-conid'>LevelCmp</span> <span class='hs-conid'>CmpEq</span> <span class='hs-layout'>(</span><span class='hs-conid'>Max</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-layout'>,</span> <span class='hs-varid'>b</span><span class='hs-keyglyph'>]</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-conid'>Max</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>c</span><span class='hs-keyglyph'>]</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <a name="line-39"></a> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>a</span> <span class='hs-varop'>==</span> <span class='hs-varid'>c</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>b</span> <span class='hs-conop'>:=<</span> <span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span> <a name="line-40"></a> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>b</span> <span class='hs-varop'>==</span> <span class='hs-varid'>c</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span> <span class='hs-conop'>:=<</span> <span class='hs-varid'>b</span><span class='hs-keyglyph'>]</span> <a name="line-41"></a><span class='hs-definition'>inequalities</span> <span class='hs-layout'>(</span><span class='hs-conid'>LevelCmp</span> <span class='hs-conid'>CmpEq</span> <span class='hs-layout'>(</span><span class='hs-conid'>Max</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-conid'>Max</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>b</span><span class='hs-layout'>,</span> <span class='hs-varid'>c</span><span class='hs-keyglyph'>]</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <a name="line-42"></a> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>a</span> <span class='hs-varop'>==</span> <span class='hs-varid'>b</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>c</span> <span class='hs-conop'>:=<</span> <span class='hs-varid'>b</span><span class='hs-keyglyph'>]</span> <a name="line-43"></a> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>a</span> <span class='hs-varop'>==</span> <span class='hs-varid'>c</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>b</span> <span class='hs-conop'>:=<</span> <span class='hs-varid'>c</span><span class='hs-keyglyph'>]</span> <a name="line-44"></a><span class='hs-definition'>inequalities</span> <span class='hs-keyword'>_</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>[]</span> </pre></body> </html>
