-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Deploying to gh-pages from @ e834cf7 🚀
- Loading branch information
Showing
3 changed files
with
91 additions
and
29 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,60 @@ | ||
| <!DOCTYPE HTML> | ||
| <html><head><meta charset="utf-8"><title>Tactic.ByEq</title><link rel='stylesheet' href='https://cdnjs.cloudflare.com/ajax/libs/github-fork-ribbon-css/0.2.3/gh-fork-ribbon.min.css'/><style>.github-fork-ribbon:before { background-color: #333; }</style><link rel="stylesheet" href="css/Agda.css"></head><body><a class='github-fork-ribbon'href='https://github.com/omelkonian/agda-stdlib-meta/tree/master///Tactic/ByEq.agda'data-ribbon='Source code on Github' title='Source code on Github'>Source code on Github</a><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--safe</a> <a id="20" class="Pragma">--without-K</a> <a id="32" class="Symbol">#-}</a> | ||
| <a id="36" class="Keyword">module</a> <a id="43" href="Tactic.ByEq.html" class="Module">Tactic.ByEq</a> <a id="55" class="Keyword">where</a> | ||
|
|
||
| <a id="62" class="Keyword">open</a> <a id="67" class="Keyword">import</a> <a id="74" href="Meta.html" class="Module">Meta</a> <a id="79" class="Keyword">hiding</a> <a id="86" class="Symbol">(</a><a id="87" href="Reflection.TCI.html#616" class="Function">TC</a><a id="89" class="Symbol">)</a> | ||
| <a id="91" class="Keyword">open</a> <a id="96" class="Keyword">import</a> <a id="103" href="MetaPrelude.html" class="Module">MetaPrelude</a> | ||
| <a id="115" class="Keyword">open</a> <a id="120" class="Keyword">import</a> <a id="127" href="Class.Functor.Core.html" class="Module">Class.Functor.Core</a><a id="145" class="Symbol">;</a> <a id="147" class="Keyword">open</a> <a id="152" class="Keyword">import</a> <a id="159" href="Class.Functor.Instances.html" class="Module">Class.Functor.Instances</a> | ||
| <a id="183" class="Keyword">open</a> <a id="188" class="Keyword">import</a> <a id="195" href="Class.Monad.Core.html" class="Module">Class.Monad.Core</a><a id="211" class="Symbol">;</a> <a id="213" class="Keyword">open</a> <a id="218" class="Keyword">import</a> <a id="225" href="Class.Monad.Instances.html" class="Module">Class.Monad.Instances</a> | ||
| <a id="247" class="Keyword">open</a> <a id="252" class="Keyword">import</a> <a id="259" href="Reflection.html" class="Module">Reflection</a> <a id="270" class="Keyword">using</a> <a id="276" class="Symbol">(</a><a id="277" href="Agda.Builtin.Reflection.html#8602" class="Postulate">TC</a><a id="279" class="Symbol">;</a> <a id="281" href="Agda.Builtin.Reflection.html#10125" class="Postulate">withNormalisation</a><a id="298" class="Symbol">;</a> <a id="300" href="Agda.Builtin.Reflection.html#8878" class="Postulate">inferType</a><a id="309" class="Symbol">;</a> <a id="311" href="Agda.Builtin.Reflection.html#8775" class="Postulate">unify</a><a id="316" class="Symbol">)</a> | ||
| <a id="318" class="Keyword">open</a> <a id="323" class="Keyword">import</a> <a id="330" href="Reflection.Utils.html" class="Module">Reflection.Utils</a> | ||
|
|
||
| <a id="348" class="Comment">-- Introduce as many arguments as possible and then:</a> | ||
| <a id="401" class="Comment">-- 1. for those of type `_ ≡ _`, unify with `refl`</a> | ||
| <a id="455" class="Comment">-- 2. ignore the rest of the arguments (unify with `_`)</a> | ||
| <a id="513" class="Comment">-- 3. unify the hole with `refl`</a> | ||
| <a id="by-eq"></a><a id="548" href="Tactic.ByEq.html#548" class="Function">by-eq</a> <a id="554" class="Symbol">:</a> <a id="556" href="Reflection.Syntax.html#3517" class="Function">Hole</a> <a id="561" class="Symbol">→</a> <a id="563" href="Agda.Builtin.Reflection.html#8602" class="Postulate">TC</a> <a id="566" href="Agda.Builtin.Unit.html#175" class="Record">⊤</a> | ||
| <a id="568" href="Tactic.ByEq.html#548" class="Function">by-eq</a> <a id="574" href="Tactic.ByEq.html#574" class="Bound">hole</a> <a id="579" class="Symbol">=</a> <a id="581" class="Keyword">do</a> | ||
| <a id="586" href="Tactic.ByEq.html#586" class="Bound">ty</a> <a id="589" href="Class.Monad.Core.html#290" class="Field Operator">←</a> <a id="591" href="Agda.Builtin.Reflection.html#10125" class="Postulate">withNormalisation</a> <a id="609" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="614" href="Function.Base.html#1974" class="Function Operator">$</a> <a id="616" href="Agda.Builtin.Reflection.html#8878" class="Postulate">inferType</a> <a id="626" href="Tactic.ByEq.html#574" class="Bound">hole</a> | ||
| <a id="633" class="Keyword">let</a> <a id="637" href="Tactic.ByEq.html#637" class="Bound">ps</a> <a id="640" class="Symbol">:</a> <a id="642" href="Reflection.AST.Argument.html#1604" class="Function">Args</a> <a id="647" href="Agda.Builtin.Reflection.html#5031" class="Datatype">Pattern</a> | ||
| <a id="661" href="Tactic.ByEq.html#637" class="Bound">ps</a> <a id="664" class="Symbol">=</a> <a id="666" href="Reflection.Utils.html#2941" class="Function">argTys</a> <a id="673" href="Tactic.ByEq.html#586" class="Bound">ty</a> <a id="676" href="Class.Functor.Core.html#328" class="Function Operator"><&></a> <a id="680" href="Class.Functor.Core.html#263" class="Function">fmap</a> <a id="685" class="Symbol">λ</a> <a id="687" class="Symbol">{(</a><a id="689" href="Agda.Builtin.Reflection.html#5251" class="InductiveConstructor">def</a> <a id="693" class="Symbol">(</a><a id="694" class="Keyword">quote</a> <a id="700" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">_≡_</a><a id="703" class="Symbol">)</a> <a id="705" class="Symbol">_)</a> <a id="708" class="Symbol">→</a> <a id="710" class="Keyword">quote</a> <a id="716" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> <a id="721" href="Reflection.Syntax.html#3280" class="InductiveConstructor Operator">◇</a><a id="722" class="Symbol">;</a> <a id="724" class="CatchallClause Symbol">_</a> <a id="726" class="Symbol">→</a> <a id="728" href="Agda.Builtin.Reflection.html#5872" class="InductiveConstructor">dot</a> <a id="732" href="Agda.Builtin.Reflection.html#5594" class="InductiveConstructor">unknown</a><a id="739" class="Symbol">}</a> | ||
| <a id="743" href="Agda.Builtin.Reflection.html#8775" class="Postulate">unify</a> <a id="749" href="Tactic.ByEq.html#574" class="Bound">hole</a> <a id="754" href="Function.Base.html#1974" class="Function Operator">$</a> <a id="756" href="Agda.Builtin.Reflection.html#5361" class="InductiveConstructor">pat-lam</a> <a id="764" href="Data.List.Base.html#5244" class="Function Operator">[</a> <a id="766" href="Agda.Builtin.Reflection.html#6106" class="InductiveConstructor">clause</a> <a id="773" href="Agda.Builtin.List.html#184" class="InductiveConstructor">[]</a> <a id="776" href="Tactic.ByEq.html#637" class="Bound">ps</a> <a id="779" class="Symbol">(</a><a id="780" class="Keyword">quote</a> <a id="786" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> <a id="791" href="Reflection.Syntax.html#3162" class="InductiveConstructor Operator">◆</a><a id="792" class="Symbol">)</a> <a id="794" href="Data.List.Base.html#5244" class="Function Operator">]</a> <a id="796" href="Agda.Builtin.List.html#184" class="InductiveConstructor">[]</a> | ||
|
|
||
| <a id="800" class="Keyword">macro</a> <a id="$by-eq"></a><a id="806" href="Tactic.ByEq.html#806" class="Function">$by-eq</a> <a id="813" class="Symbol">=</a> <a id="815" href="Tactic.ByEq.html#548" class="Function">by-eq</a> | ||
|
|
||
| <a id="822" class="Keyword">private</a> | ||
| <a id="832" class="Comment">-- test that macro works</a> | ||
| <a id="859" href="Tactic.ByEq.html#859" class="Function">_</a> <a id="861" class="Symbol">:</a> <a id="863" class="Symbol">∀</a> <a id="865" class="Symbol">{</a><a id="866" href="Tactic.ByEq.html#866" class="Bound">n</a> <a id="868" href="Tactic.ByEq.html#868" class="Bound">m</a> <a id="870" href="Tactic.ByEq.html#870" class="Bound">k</a> <a id="872" class="Symbol">:</a> <a id="874" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="875" class="Symbol">}</a> <a id="877" class="Symbol">→</a> <a id="879" href="Tactic.ByEq.html#866" class="Bound">n</a> <a id="881" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="883" href="Tactic.ByEq.html#868" class="Bound">m</a> <a id="885" class="Symbol">→</a> <a id="887" href="Tactic.ByEq.html#868" class="Bound">m</a> <a id="889" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="891" href="Tactic.ByEq.html#870" class="Bound">k</a> <a id="893" class="Symbol">→</a> <a id="895" href="Tactic.ByEq.html#866" class="Bound">n</a> <a id="897" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="899" href="Tactic.ByEq.html#870" class="Bound">k</a> | ||
| <a id="903" class="Symbol">_</a> <a id="905" class="Symbol">=</a> <a id="907" href="Tactic.ByEq.html#806" class="Macro">$by-eq</a> | ||
|
|
||
| <a id="917" href="Tactic.ByEq.html#917" class="Function">_</a> <a id="919" class="Symbol">:</a> <a id="921" class="Symbol">∀</a> <a id="923" class="Symbol">{</a><a id="924" href="Tactic.ByEq.html#924" class="Bound">n</a> <a id="926" href="Tactic.ByEq.html#926" class="Bound">m</a> <a id="928" href="Tactic.ByEq.html#928" class="Bound">k</a> <a id="930" href="Tactic.ByEq.html#930" class="Bound">x</a> <a id="932" href="Tactic.ByEq.html#932" class="Bound">y</a> <a id="934" class="Symbol">:</a> <a id="936" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="937" class="Symbol">}</a> <a id="939" class="Symbol">→</a> <a id="941" href="Tactic.ByEq.html#924" class="Bound">n</a> <a id="943" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="945" href="Tactic.ByEq.html#926" class="Bound">m</a> <a id="947" class="Symbol">→</a> <a id="949" href="Tactic.ByEq.html#930" class="Bound">x</a> <a id="951" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="953" href="Tactic.ByEq.html#932" class="Bound">y</a> <a id="955" class="Symbol">→</a> <a id="957" href="Tactic.ByEq.html#926" class="Bound">m</a> <a id="959" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="961" href="Tactic.ByEq.html#924" class="Bound">n</a> | ||
| <a id="965" class="Symbol">_</a> <a id="967" class="Symbol">=</a> <a id="969" href="Tactic.ByEq.html#806" class="Macro">$by-eq</a> | ||
|
|
||
| <a id="979" class="Comment">-- test that tactic arguments work</a> | ||
| <a id="f"></a><a id="1016" href="Tactic.ByEq.html#1016" class="Function">f</a> <a id="1018" class="Symbol">:</a> <a id="1020" class="Symbol">{@(</a><a id="1023" class="Keyword">tactic</a> <a id="1030" href="Tactic.ByEq.html#548" class="Function">by-eq</a><a id="1035" class="Symbol">)</a> <a id="1037" href="Tactic.ByEq.html#1037" class="Bound">_</a> <a id="1039" class="Symbol">:</a> <a id="1041" class="Symbol">∀</a> <a id="1043" class="Symbol">{</a><a id="1044" href="Tactic.ByEq.html#1044" class="Bound">n</a> <a id="1046" href="Tactic.ByEq.html#1046" class="Bound">m</a> <a id="1048" class="Symbol">:</a> <a id="1050" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="1051" class="Symbol">}</a> <a id="1053" class="Symbol">→</a> <a id="1055" href="Tactic.ByEq.html#1044" class="Bound">n</a> <a id="1057" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="1059" href="Tactic.ByEq.html#1046" class="Bound">m</a> <a id="1061" class="Symbol">→</a> <a id="1063" href="Tactic.ByEq.html#1046" class="Bound">m</a> <a id="1065" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="1067" href="Tactic.ByEq.html#1044" class="Bound">n</a><a id="1068" class="Symbol">}</a> <a id="1070" class="Symbol">→</a> <a id="1072" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="1077" class="Symbol">→</a> <a id="1079" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> | ||
| <a id="1086" href="Tactic.ByEq.html#1016" class="Function">f</a> <a id="1088" class="Symbol">=</a> <a id="1090" href="Function.Base.html#704" class="Function">id</a> | ||
|
|
||
| <a id="1096" href="Tactic.ByEq.html#1096" class="Function">_</a> <a id="1098" class="Symbol">:</a> <a id="1100" href="Tactic.ByEq.html#1016" class="Function">f</a> <a id="1102" class="Symbol">{λ</a> <a id="1105" class="Keyword">where</a> <a id="1111" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> <a id="1116" class="Symbol">→</a> <a id="1118" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a><a id="1122" class="Symbol">}</a> <a id="1124" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="1129" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="1131" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> | ||
| <a id="1138" class="Symbol">_</a> <a id="1140" class="Symbol">=</a> <a id="1142" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> | ||
|
|
||
| <a id="1150" href="Tactic.ByEq.html#1150" class="Function">_</a> <a id="1152" class="Symbol">:</a> <a id="1154" href="Tactic.ByEq.html#1016" class="Function">f</a> <a id="1156" class="Symbol">{</a><a id="1157" href="Tactic.ByEq.html#806" class="Macro">$by-eq</a><a id="1163" class="Symbol">}</a> <a id="1165" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="1170" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="1172" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> | ||
| <a id="1179" class="Symbol">_</a> <a id="1181" class="Symbol">=</a> <a id="1183" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> | ||
|
|
||
| <a id="1191" href="Tactic.ByEq.html#1191" class="Function">_</a> <a id="1193" class="Symbol">:</a> <a id="1195" href="Tactic.ByEq.html#1016" class="Function">f</a> <a id="1197" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="1202" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="1204" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> | ||
| <a id="1211" class="Symbol">_</a> <a id="1213" class="Symbol">=</a> <a id="1215" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> | ||
|
|
||
| <a id="1223" class="Comment">-- test that normalisation works</a> | ||
| <a id="Sym"></a><a id="1258" href="Tactic.ByEq.html#1258" class="Function">Sym</a> <a id="1262" class="Symbol">=</a> <a id="1264" class="Symbol">∀</a> <a id="1266" class="Symbol">{</a><a id="1267" href="Tactic.ByEq.html#1267" class="Bound">n</a> <a id="1269" href="Tactic.ByEq.html#1269" class="Bound">m</a> <a id="1271" class="Symbol">:</a> <a id="1273" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="1274" class="Symbol">}</a> <a id="1276" class="Symbol">→</a> <a id="1278" href="Tactic.ByEq.html#1267" class="Bound">n</a> <a id="1280" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="1282" href="Tactic.ByEq.html#1269" class="Bound">m</a> <a id="1284" class="Symbol">→</a> <a id="1286" href="Tactic.ByEq.html#1269" class="Bound">m</a> <a id="1288" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="1290" href="Tactic.ByEq.html#1267" class="Bound">n</a> | ||
|
|
||
| <a id="g"></a><a id="1295" href="Tactic.ByEq.html#1295" class="Function">g</a> <a id="1297" class="Symbol">:</a> <a id="1299" class="Symbol">{@(</a><a id="1302" class="Keyword">tactic</a> <a id="1309" href="Tactic.ByEq.html#548" class="Function">by-eq</a><a id="1314" class="Symbol">)</a> <a id="1316" href="Tactic.ByEq.html#1316" class="Bound">_</a> <a id="1318" class="Symbol">:</a> <a id="1320" href="Tactic.ByEq.html#1258" class="Function">Sym</a><a id="1323" class="Symbol">}</a> <a id="1325" class="Symbol">→</a> <a id="1327" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="1332" class="Symbol">→</a> <a id="1334" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> | ||
| <a id="1341" href="Tactic.ByEq.html#1295" class="Function">g</a> <a id="1343" class="Symbol">=</a> <a id="1345" href="Function.Base.html#704" class="Function">id</a> | ||
|
|
||
| <a id="1351" href="Tactic.ByEq.html#1351" class="Function">_</a> <a id="1353" class="Symbol">:</a> <a id="1355" href="Tactic.ByEq.html#1295" class="Function">g</a> <a id="1357" class="Symbol">{λ</a> <a id="1360" class="Keyword">where</a> <a id="1366" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> <a id="1371" class="Symbol">→</a> <a id="1373" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a><a id="1377" class="Symbol">}</a> <a id="1379" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="1384" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="1386" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> | ||
| <a id="1393" class="Symbol">_</a> <a id="1395" class="Symbol">=</a> <a id="1397" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> | ||
|
|
||
| <a id="1405" href="Tactic.ByEq.html#1405" class="Function">_</a> <a id="1407" class="Symbol">:</a> <a id="1409" href="Tactic.ByEq.html#1295" class="Function">g</a> <a id="1411" class="Symbol">{</a><a id="1412" href="Tactic.ByEq.html#806" class="Macro">$by-eq</a><a id="1418" class="Symbol">}</a> <a id="1420" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="1425" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="1427" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> | ||
| <a id="1434" class="Symbol">_</a> <a id="1436" class="Symbol">=</a> <a id="1438" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> | ||
|
|
||
| <a id="1446" href="Tactic.ByEq.html#1446" class="Function">_</a> <a id="1448" class="Symbol">:</a> <a id="1450" href="Tactic.ByEq.html#1295" class="Function">g</a> <a id="1452" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="1457" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="1459" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> | ||
| <a id="1466" class="Symbol">_</a> <a id="1468" class="Symbol">=</a> <a id="1470" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> | ||
| </pre></body></html> |
Oops, something went wrong.