<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Hi Jason,</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">Yes, you are right about that. I have
an inductively defined type (mimicking a part of the C++ type
system) which is quite simple.</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">Now the C++ templates (type-level
functions) allow overlapping patterns in a way that Agda also does
and a translation even of a complicated C++ template to Agda works
quite good.</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">For a bunch of these templates, which
are composed out of other ones, I am interested in their "effect"
and I (misuse?) Agda to generate all these cases.</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">That is, for a from-C++-translated f
with overlapping patterns and another from-C++-translated g with
similar but different overlapping pattern, it is of very great use
to have Agda deciding the cases where they differ.</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">These templates are so awfully to debug
just in C++ and even just this automatic decision in Agda aids a
lot.</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">It looks like this:<br>
</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">data FundT : Set where<br>
void : FundT<br>
… a long list<br>
unsigned_long_long_int : FundT<br>
<br>
data BasicT : Set where<br>
class : BasicT<br>
fund : FundT → BasicT<br>
<br>
mutual<br>
data PointerT : Set where<br>
_*ᵇ : BasicT → PointerT<br>
_*ᵖ : PointerT → PointerT<br>
_*ᶜ : ConstT → PointerT<br>
<br>
data ConstT : Set where<br>
_constᵇ : BasicT → ConstT<br>
_constᵖ : PointerT → ConstT<br>
<br>
data RefT : Set where<br>
_&ᵇ : BasicT → RefT<br>
_&ᵖ : PointerT → RefT<br>
_&ᶜ : ConstT → RefT<br>
_&&ᵇ : BasicT → RefT<br>
_&&ᵖ : PointerT → RefT<br>
_&&ᶜ : ConstT → RefT<br>
<br>
data C++Type : Set where<br>
〚_〛ᵇ : BasicT → C++Type<br>
〚_〛ᵖ : PointerT → C++Type<br>
〚_〛ᶜ : ConstT → C++Type<br>
〚_〛ʳ : RefT → C++Type</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">-- translated from C++<br>
remove-const : C++Type → C++Type<br>
remove-const 〚 x constᵇ 〛ᶜ = 〚 x 〛ᵇ<br>
remove-const 〚 x constᵖ 〛ᶜ = 〚 x 〛ᵖ<br>
remove-const x = x</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">-- translated from C++<br>
</div>
<div class="moz-cite-prefix">f : C++Type → Bool → C++Type<br>
f 〚 x &ᵇ 〛ʳ v = 〚 x &ᵇ 〛ʳ<br>
f 〚 x &ᵖ 〛ʳ v = 〚 x &ᵖ 〛ʳ<br>
f 〚 (x constᵇ) &ᶜ 〛ʳ true = 〚 x 〛ᵇ<br>
f 〚 (x constᵖ) &ᶜ 〛ʳ true = 〚 x 〛ᵖ<br>
f 〚 x &ᶜ 〛ʳ false = 〚 x &ᶜ 〛ʳ<br>
f x v = remove-const x</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">-- translated from C++<br>
g : C++Type → Bool → C++Type<br>
g 〚 x &ᵖ 〛ʳ v = 〚 x 〛ᵖ<br>
g 〚 (x constᵖ) &ᶜ 〛ʳ v = 〚 x 〛ᵖ<br>
g x v = f x v -- uses f for the default case<br>
</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">regards<br>
</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">Am 14.03.19 um 21:15 schrieb Jason
-Zhong Sheng- Hu:<br>
</div>
<blockquote type="cite"
cite="mid:YTXPR0101MB1472752CF9020AA1A839DE57AF4B0@YTXPR0101MB1472.CANPRD01.PROD.OUTLOOK.COM">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
Hi Marcus,</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
this signature looks simply a decision procedure for
propositional equality between u and v, and if agda is able to
figure out the proof term, I even speculate that u and v are of
an inductively defined type. If that's the case, why did you
involve f and g? it might hint that it's not the signature that
you might be looking for, or you are complicating a simple
problem.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
</blockquote>
<br>
</body>
</html>