<html dir="ltr"><head></head><body style="text-align:left; direction:ltr;"><div>Hi,</div><div><br></div><div>nice that term handling from ML gets some attention now.</div><div>Just as a remark, and maybe "feature request" of what I would like to see, I'm using the following antiquotations for several years now. They are in the AFP. </div><div><a href="https://www.isa-afp.org/browser_info/current/AFP/Automatic_Refinement/Mpat_Antiquot.html">https://www.isa-afp.org/browser_info/current/AFP/Automatic_Refinement/Mpat_Antiquot.html</a></div><div><br></div><div><a href="https://www.isa-afp.org/browser_info/current/AFP/Automatic_Refinement/Mk_Term_Antiquot.html">https://www.isa-afp.org/browser_info/current/AFP/Automatic_Refinement/Mk_Term_Antiquot.html</a></div><div><br></div><div><br></div><div>There is an antiquotation @{mpat} that generates a ML matching pattern from a term, and one @{mk_term} that constructs a term. </div><div>mk_term also tries hard to infer types from the arguments (examples below). </div><div><br></div><div>These are definitely not include-in-distribution quality yet, as they use a hack of identifying term-variables (?x) with ML variables. However, I use them a lot, and would like to </div><div>ultimately see robust and clean means to efficiently match against and constructs complex terms from ML level in a readable way.</div><div><br></div><div>--</div><div> Peter</div><div><br></div><div>Examples to generate matching patterns from terms:</div><div><br></div><div><pre class="source" style="direction: ltr; unicode-bidi: bidi-override; padding: 10px; font-family: "Isabelle DejaVu Sans Mono", monospace; font-size: medium; font-variant-ligatures: normal; orphans: 2; widows: 2; text-decoration-thickness: initial;"><span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);"> <span class="keyword1" style="color: rgb(0, 102, 153);"><span class="keyword" style="font-weight: bold;">fun</span></span> <span class="entity">dest_pair_singleton</span> <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="entity"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">mpat</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">"<span class="main">{</span><span class="main">(</span><span class="var" style="color: rgb(0, 0, 155);">?a</span><span class="main">,</span><span class="main">_</span><span class="main">)</span><span class="main">}</span>"</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span></span> <span class="main">=</span> <span class="main">(</span><span class="entity">a</span><span class="main">)</span>
<span class="main">|</span> <span class="entity">dest_pair_singleton</span> <span class="entity">t</span> <span class="main">=</span> <span class="keyword3" style="color: rgb(0, 153, 255);"><span class="keyword" style="font-weight: bold;">raise</span></span> TERM <span class="main">(</span><span class="inner_quoted" style="color: rgb(255, 0, 204);">"dest_pair_singleton"</span><span class="main">,</span><span class="main">[</span><span class="entity">t</span><span class="main">]</span><span class="main">)</span>
<span class="keyword1" style="color: rgb(0, 102, 153);"><span class="keyword" style="font-weight: bold;">fun</span></span> <span class="entity">dest_nat_pair_singleton</span> <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="entity"><span class="entity"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">mpat</span> <span class="main">(</span><span class="quasi_keyword" style="color: rgb(153, 102, 255);">typs</span><span class="main">)</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">"<span class="main">{</span><span class="main">(</span><span class="var" style="color: rgb(0, 0, 155);">?a</span><span class="main">::</span>nat<span class="main">,</span><span class="var" style="color: rgb(0, 0, 155);">?b</span><span class="main">::</span>nat<span class="main">)</span><span class="main">}</span>"</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span></span></span> <span class="main">=</span> <span class="main">(</span><span class="entity">a</span><span class="main">,</span><span class="entity">b</span><span class="main">)</span>
<span class="main">|</span> <span class="entity">dest_nat_pair_singleton</span> <span class="entity">t</span> <span class="main">=</span> <span class="keyword3" style="color: rgb(0, 153, 255);"><span class="keyword" style="font-weight: bold;">raise</span></span> TERM <span class="main">(</span><span class="inner_quoted" style="color: rgb(255, 0, 204);">"dest_nat_pair_singleton"</span><span class="main">,</span><span class="main">[</span><span class="entity">t</span><span class="main">]</span><span class="main">)</span>
<span class="keyword1" style="color: rgb(0, 102, 153);"><span class="keyword" style="font-weight: bold;">fun</span></span> <span class="entity">dest_pair_singleton_T</span> <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">mpat</span> <span class="main">(</span><span class="quasi_keyword" style="color: rgb(153, 102, 255);">typs</span><span class="main">)</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">"<span class="main">{</span><span class="main">(</span><span class="var" style="color: rgb(0, 0, 155);">?a</span><span class="main">::</span><span class="main">_</span> <span class="main">⇒</span> <span class="tvar" style="color: rgb(160, 32, 240);">?'v_Ta</span><span class="main">,</span><span class="var" style="color: rgb(0, 0, 155);">?b</span><span class="main">::</span><span class="tvar" style="color: rgb(160, 32, 240);">?'v_Tb</span><span class="main">)</span><span class="main">}</span>"</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span></span></span></span></span> <span class="main">=</span>
<span class="main">(</span><span class="main">(</span><span class="entity">a</span><span class="main">,</span><span class="entity">Ta</span><span class="main">)</span><span class="main">,</span><span class="main">(</span><span class="entity">b</span><span class="main">,</span><span class="entity">Tb</span><span class="main">)</span><span class="main">)</span>
<span class="main">|</span> <span class="entity">dest_pair_singleton_T</span> <span class="entity">t</span> <span class="main">=</span> <span class="keyword3" style="color: rgb(0, 153, 255);"><span class="keyword" style="font-weight: bold;">raise</span></span> TERM <span class="main">(</span><span class="inner_quoted" style="color: rgb(255, 0, 204);">"dest_pair_singleton_T"</span><span class="main">,</span><span class="main">[</span><span class="entity">t</span><span class="main">]</span><span class="main">)</span>
<span class="keyword1" style="color: rgb(0, 102, 153);"><span class="keyword" style="font-weight: bold;">fun</span></span> <span class="entity">dest_pair_lambda</span> <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">mpat</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">"<span class="main">{</span><span class="main">(</span><span class="main">λ</span><span class="bound" style="color: rgb(0, 128, 0);">a</span> <span class="main"><span class="bound" style="color: rgb(0, 128, 0);">_</span></span> <span class="main"><span class="bound" style="color: rgb(0, 128, 0);">_</span></span><span class="main">.</span> <span class="var" style="color: rgb(0, 0, 155);">?Ta</span><span class="main">,</span> <span class="main">λ</span><span class="bound" style="color: rgb(0, 128, 0);">b</span><span class="main">.</span> <span class="var" style="color: rgb(0, 0, 155);">?Tb</span><span class="main">)</span><span class="main">}</span>"</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span></span></span></span></span></span></span> <span class="main">=</span> <span class="main">(</span><span class="entity">a</span><span class="main">,</span><span class="entity">a_T</span><span class="main">,</span><span class="entity">b</span><span class="main">,</span><span class="entity">b_T</span><span class="main">,</span><span class="entity">Ta</span><span class="main">,</span><span class="entity">Tb</span><span class="main">)</span>
<span class="main">|</span> <span class="entity">dest_pair_lambda</span> <span class="entity">t</span> <span class="main">=</span> <span class="keyword3" style="color: rgb(0, 153, 255);"><span class="keyword" style="font-weight: bold;">raise</span></span> TERM <span class="main">(</span><span class="inner_quoted" style="color: rgb(255, 0, 204);">"dest_pair_lambda"</span><span class="main">,</span><span class="main">[</span><span class="entity">t</span><span class="main">]</span><span class="main">)</span>
<span class="keyword1" style="color: rgb(0, 102, 153);"><span class="keyword" style="font-weight: bold;">fun</span></span> <span class="entity">foo</span> <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">mpat</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">"<span class="main">[</span><span class="var" style="color: rgb(0, 0, 155);">?a</span><span class="main">,</span><span class="var" style="color: rgb(0, 0, 155);">?b</span> <span class="keyword1" style="color: rgb(0, 102, 153);">AS<span class="hidden" style="font-family: Vacuous; font-size: 6px; color: rgba(255, 255, 255, 0);">⇩</span><sub>s</sub></span> mpaq_Bound <span class="var" style="color: rgb(0, 0, 155);">?i</span><span class="main">,</span><span class="var" style="color: rgb(0, 0, 155);">?c</span> <span class="keyword1" style="color: rgb(0, 102, 153);">AS<span class="hidden" style="font-family: Vacuous; font-size: 6px; color: rgba(255, 255, 255, 0);">⇩</span><sub>p</sub></span> <span class="main">[</span><span class="var" style="color: rgb(0, 0, 155);">?n</span><span class="main">]</span><span class="main">]</span>"</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span></span></span></span></span></span> <span class="main">=</span>
<span class="main">(</span><span class="entity">a</span><span class="main">,</span><span class="entity">b</span><span class="main">,</span><span class="entity">i</span><span class="main">,</span><span class="entity">c</span><span class="main">,</span><span class="entity">n</span><span class="main">)</span>
<span class="main">|</span> <span class="entity">foo</span> <span class="entity">t</span> <span class="main">=</span> <span class="keyword3" style="color: rgb(0, 153, 255);"><span class="keyword" style="font-weight: bold;">raise</span></span> TERM <span class="main">(</span><span class="inner_quoted" style="color: rgb(255, 0, 204);">"foo"</span><span class="main">,</span><span class="main">[</span><span class="entity">t</span><span class="main">]</span><span class="main">)</span>
</span></pre></div><div>Examples to generate term templates:</div><div><pre class="source" style="direction: ltr; unicode-bidi: bidi-override; padding: 10px; font-family: "Isabelle DejaVu Sans Mono", monospace; font-size: medium; font-variant-ligatures: normal; orphans: 2; widows: 2; text-decoration-thickness: initial;"><span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);"> <span class="keyword1" style="color: rgb(0, 102, 153);"><span class="keyword" style="font-weight: bold;">fun</span></span> <span class="entity">mk_2elem_list</span> <span class="entity">a</span> <span class="entity">b</span> <span class="main">=</span> <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">mk_term</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">"<span class="main">[</span><span class="var" style="color: rgb(0, 0, 155);">?a</span><span class="main">,</span><span class="var" style="color: rgb(0, 0, 155);">?b</span><span class="main">]</span>"</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span></span></span></span></span></span></span></span></span></span></span></span></span>
<span class="keyword1" style="color: rgb(0, 102, 153);"><span class="keyword" style="font-weight: bold;">fun</span></span> <span class="entity">mk_compr</span> <span class="entity">s</span> <span class="entity">P</span> <span class="main">=</span> <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">mk_term</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">"<span class="main">{</span> <span class="bound" style="color: rgb(0, 128, 0);"><span class="bound">x</span></span><span class="main">∈</span><span class="var" style="color: rgb(0, 0, 155);">?s</span><span class="main">.</span> <span class="var" style="color: rgb(0, 0, 155);">?P</span> <span class="bound" style="color: rgb(0, 128, 0);">x</span><span class="main">}</span>"</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span></span></span></span></span></span></span></span></span></span></span></span></span>
<span class="keyword1" style="color: rgb(0, 102, 153);"><span class="keyword" style="font-weight: bold;">val</span></span> <span class="entity">test1</span> <span class="main">=</span> <span class="entity">mk_2elem_list</span> <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">term</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">"<span class="main">1</span><span class="main">::</span>nat"</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span> <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">term</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">"<span class="numeral">2</span><span class="main">::</span>nat"</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span> |> Thm.cterm_of <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="entity"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">context</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span></span>
<span class="keyword1" style="color: rgb(0, 102, 153);"><span class="keyword" style="font-weight: bold;">val</span></span> <span class="entity">test2</span> <span class="main">=</span> <span class="entity">mk_compr</span> <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">term</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">"<span class="main">{</span><span class="main">1</span><span class="main">,</span><span class="numeral">2</span><span class="main">,</span><span class="numeral">3</span><span class="main">::</span>nat<span class="main">}</span>"</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span> <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">term</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">"<span class="main">(<)</span> <span class="main">(</span><span class="numeral">2</span><span class="main">::</span>nat<span class="main">)</span>"</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span> |> Thm.cterm_of <span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="entity"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">context</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span></span>
<span class="keyword1" style="color: rgb(0, 102, 153);"><span class="keyword" style="font-weight: bold;">val</span></span> <span class="entity">test3</span> <span class="main">=</span> <span class="keyword2" style="color: rgb(0, 153, 102);"><span class="keyword" style="font-weight: bold;">let</span></span>
<span class="keyword1" style="color: rgb(0, 102, 153);"><span class="keyword" style="font-weight: bold;">val</span></span> <span class="entity">x</span> <span class="main">=</span> Bound <span class="inner_numeral" style="color: rgb(255, 0, 0);">0</span>
<span class="keyword1" style="color: rgb(0, 102, 153);"><span class="keyword" style="font-weight: bold;">val</span></span> <span class="entity">env</span> <span class="main">=</span> <span class="main">[</span><span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">typ</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">nat</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span><span class="main">]</span>
<span class="keyword2" style="color: rgb(0, 153, 102);"><span class="keyword" style="font-weight: bold;">in</span></span>
<span class="antiquoted" style="background-color: rgba(255, 200, 50, 0.1);"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="entity"><span class="antiquote" style="color: rgb(102, 0, 204);">@{</span><span class="operator" style="color: rgb(50, 50, 50);">mk_term</span> env<span class="main">:</span> <span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);">"<span class="var" style="color: rgb(0, 0, 155);">?x</span><span class="main">+</span><span class="var" style="color: rgb(0, 0, 155);">?x</span>"</span><span class="antiquote" style="color: rgb(102, 0, 204);">}</span></span></span></span></span></span></span></span></span></span>
<span class="keyword2" style="color: rgb(0, 153, 102);"><span class="keyword" style="font-weight: bold;">end</span></span>
</span></pre><div><span class="quoted" style="background-color: rgba(139, 139, 139, 0.05);"><span class="keyword2" style="color: rgb(0, 153, 102);"><span class="keyword" style="font-weight: bold;"><br></span></span></span></div></div><div><br></div><div>On Wed, 2021-09-22 at 12:50 +0200, Makarius wrote:</div><blockquote type="cite" style="margin:0 0 0 .8ex; border-left:2px #729fcf solid;padding-left:1ex"><div>*** ML ***</div><div><br></div><div>* ML antiquotations for type constructors and term constants:</div><div><br></div><div> \<^Type>‹c›</div><div> \<^Type>‹c T …› ― ‹same with type arguments›</div><div> \<^Type>_fn‹c T …› ― ‹fn abstraction, failure via exception TYPE›</div><div> \<^Const>‹c›</div><div> \<^Const>‹c T …› ― ‹same with type arguments›</div><div> \<^Const>‹c for t …› ― ‹same with term arguments›</div><div> \<^Const_>‹c …› ― ‹same for patterns: case, let, fn›</div><div> \<^Const>_fn‹c T …› ― ‹fn abstraction, failure via exception TERM›</div><div><br></div><div>Examples in HOL:</div><div><br></div><div> val natT = \<^Type>‹nat›;</div><div> fun mk_funT (A, B) = \<^Type>‹fun A B›;</div><div> val dest_funT = fn \<^Type>‹fun A B› => (A, B);</div><div> fun mk_conj (A, B) = \<^Const>‹conj for A B›;</div><div> val dest_conj = fn \<^Const_>‹conj for A B› => (A, B);</div><div> fun mk_eq T (t, u) = \<^Const>‹HOL.eq T for t u›;</div><div> val dest_eq = fn \<^Const_>‹HOL.eq T for t u› => (T, (t, u));</div><div><br></div><div><br></div><div>This refers to Isabelle/4974c3697fee.</div><div><br></div><div>The question of how to represent outlines for type and term expressions</div><div>adequately and robustly in Isabelle/ML has remained open for a long time.</div><div>After 2007/2008, I always thought that we should use more concrete syntax</div><div>(namely inner syntax).</div><div><br></div><div>After rethinking it thoroughly, the outcome is now as above. The key idea is</div><div>to nest ML source inside antiquotations: this has become possible in recent</div><div>antiquotations \<^try>‹expr› and \<^can>‹expr›.</div><div><br></div><div>The result looks a bit like enhanced S-expressions from the old LISP days:</div><div>this fits perfectly well into the idea of antiquotations and nesting of</div><div>sublanguages via cartouches --- instead of lots of silly parentheses.</div><div><br></div><div><br></div><div>Another motivation: the Const antiquotations already use "typargs", e.g. just</div><div>one type T for overloaded "plus", instead of "T => T => T". When all</div><div>Isabelle/ML have been upgraded to use that form, we may have a chance to trim</div><div>down the redundant type information in datatype term for Const (within a few</div><div>years).</div><div><br></div><div>This has the potential to speed-up term/type</div><div>instantiation/matching/unification considerably: profiles always show a lot of</div><div>activity on types, rather than actual term structure.</div><div><br></div><div><br></div><div> Makarius</div><div>_______________________________________________</div><div>isabelle-dev mailing list</div><div><a href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a></div><div><a href="https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a></div></blockquote></body></html>