I am trying to define translations for function spaces. There are different function spaces for individuals `i`

and types `t`

.

Is there some way to make all of the following type? Sadly(?), there is no filtering/backtracking for translations according to the reference manual

```
theory Scratch
imports HOL.HOL
begin
typedecl i
typedecl t
consts
set_dep_fun :: "i ⇒ (i ⇒ i) ⇒ i"
type_dep_fun :: "t ⇒ (i ⇒ t) ⇒ t"
elem :: "i ⇒ i ⇒ bool" (infix "∈" 50)
has_type :: "i ⇒ t ⇒ bool" (infix ":" 50)
abbreviation "set_fun A B ≡ set_dep_fun A (λ_. B)"
abbreviation "type_fun A B ≡ type_dep_fun A (λ_. B)"
syntax
"_telescope" :: "logic ⇒ logic ⇒ logic" (infixr "→" 55)
translations
"(x ∈ A) args → B" ⇀ "(x ∈ A) → args → B"
"(x ∈ A) → B" ⇌ "CONST set_dep_fun A (λx. B)"
"(x : A) args → B" ⇀ "(x : A) → args → B"
"(x : A) → B" ⇌ "CONST type_dep_fun A (λx. B)"
(* Optimally, instead of the next two translations, I would love to say:
if `A → B` is of type `t` then use `type_fun` otherwise use `set_fun`. *)
"(A :: t) → B" ⇌ "CONST type_fun A B"
"A → B" ⇌ "CONST set_fun A B"
declare [[show_types]]
term "(x ∈ A) → B x"
term "(x : A) → B x"
term "A → (x ∈ B) → (C x)"
term "(A :: i) → (x ∈ B) → C x" (*same as line above*)
term "(A :: t) → (x : B) → (C x)"
term "(x ∈ A) → B → C x"
term "(x : A) → (B :: t) → C x"
term "(x : A) → B → C x" (*fails*)
term "A → B"
term "(A :: i) → B" (*same as line above*)
term "(A :: t) → B"
term "(A → B) :: t" (*fails*)
term "(A → B) = ((x ∈ A) → B)"
term "((A :: t) → B) = ((x : A) → B)"
term "(A → B) = ((x ∈ A) → B)"
term "(A → B) = ((x : A) → B)" (*fails*)
end
```

I am not sure how this stuff works but could you use a parse translation? In a parse translation you can use arbitrary ML code to produce the result.

I may be mistaken about this, but don't translations (including parse translations) work entirely on the syntactic stage, i.e. before the terms even have any type information at all?

In that case, I think the only way to achieve what you want to do would be to add a checking stage that changes the placeholder constant of the input syntax into what you actually want it to be as soon as the type is known.

This is pretty much what `adhoc_overloading`

does.

Of course, there is the fundamental problem of "what happens if the type is neither `i`

nor `t`

", or if the type is completely polymorphic. (`adhoc_overloading`

then fails with an error message)

Such additional checking phases are also notoriously problematic when you have several of them, since they can then interact with each other poorly (e.g. `adhoc_overloading`

plus coercions)

Then again I may also have completely misunderstood what you are trying to do; in that case just ignore my ramblings.

As far as I can see (having skimmed the documentation), you are right Manuel and an additional phase during type checking would be necessary.

Last updated: Aug 15 2022 at 02:13 UTC