[Agda] Case split on λ()

[Marcus Christian Lehmann]

Hi Jason,

Yes, you are right about that. I have an inductively defined type 
(mimicking a part of the C++ type system) which is quite simple.

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.

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.

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.

These templates are so awfully to debug just in C++ and even just this 
automatic decision in Agda aids a lot.

It looks like this:

data FundT : Set where
   void                   : FundT
    … a long list
   unsigned_long_long_int : FundT

data BasicT : Set where
   class : BasicT
   fund : FundT → BasicT

mutual
   data PointerT : Set where
     _*ᵇ : BasicT   → PointerT
     _*ᵖ : PointerT → PointerT
     _*ᶜ : ConstT   → PointerT

   data ConstT : Set where
     _constᵇ : BasicT → ConstT
     _constᵖ : PointerT → ConstT

data RefT : Set where
   _&ᵇ  : BasicT   → RefT
   _&ᵖ  : PointerT → RefT
   _&ᶜ  : ConstT   → RefT
   _&&ᵇ : BasicT   → RefT
   _&&ᵖ : PointerT → RefT
   _&&ᶜ : ConstT   → RefT

data C++Type : Set where
   〚_〛ᵇ : BasicT   → C++Type
   〚_〛ᵖ : PointerT → C++Type
   〚_〛ᶜ : ConstT   → C++Type
   〚_〛ʳ : RefT     → C++Type


-- translated from C++
remove-const : C++Type → C++Type
remove-const 〚 x constᵇ 〛ᶜ = 〚 x 〛ᵇ
remove-const 〚 x constᵖ 〛ᶜ = 〚 x 〛ᵖ
remove-const x = x

-- translated from C++
f : C++Type → Bool → C++Type
f 〚 x &ᵇ 〛ʳ v = 〚 x &ᵇ 〛ʳ
f 〚 x &ᵖ 〛ʳ v = 〚 x &ᵖ 〛ʳ
f 〚 (x constᵇ) &ᶜ 〛ʳ true = 〚 x 〛ᵇ
f 〚 (x constᵖ) &ᶜ 〛ʳ true = 〚 x 〛ᵖ
f 〚 x &ᶜ 〛ʳ false = 〚 x &ᶜ 〛ʳ
f x v = remove-const x

-- translated from C++
g : C++Type → Bool → C++Type
g 〚 x &ᵖ 〛ʳ v = 〚 x 〛ᵖ
g 〚 (x constᵖ) &ᶜ 〛ʳ v = 〚 x 〛ᵖ
g x v = f x v -- uses f for the default case

regards

Am 14.03.19 um 21:15 schrieb Jason -Zhong Sheng- Hu:
> Hi Marcus,
>
> 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.
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190314/78e8e5c8/attachment.html>