Stream: Beginner Questions

Topic: exception when trying to define function

Jan van Brügge (Jul 29 2022 at 10:04):

I am trying to define a recursive function, but for some reason I get an error:

exception TERM raised (line 272 of "~~/src/HOL/Tools/hologic.ML"):
  dest_eq
  |supp id| <o |UNIV|

the function in question is this:

function f :: "'a::var_τ_pre raw_τ ⇒ 'a ssfun ⇒ 'a τ" where
  "f (raw_τ_ctor x) p = CTOR (map_τ_pre id id (λt. (t, f t)) (λt. (t, f t)) (map_τ_pre id (pick0 x p) (rename_τ (pick0 x p)) id x)) p"

There are a few theorems that would require |supp id| <o |UNIV| but I do not see how they would are involved here.

Manuel Eberl (Jul 29 2022 at 10:07):

Might be a good idea to enable the ML stack trace to see where that exception comes from exactly.

Jan van Brügge (Jul 29 2022 at 10:08):

I guess this means I need to load up this code in a pure session, because the stack traces do not work with a precompiled HOL session

Manuel Eberl (Jul 29 2022 at 10:11):

ah, yes, because the function package was defined in HOL…

Manuel Eberl (Jul 29 2022 at 10:11):

yeah you don't want to do this

Manuel Eberl (Jul 29 2022 at 10:11):

well, you can try

Manuel Eberl (Jul 29 2022 at 10:11):

it might work

Manuel Eberl (Jul 29 2022 at 10:12):

I remember running into some performance issues with the whole stack trace/debugger thing, but I don't remember exactly what I was doing at the time.

Manuel Eberl (Jul 29 2022 at 10:13):

I am somewhat surprised though; this looks like some sort of cardinality constraint that I would have expected to come perhaps from the datatype package, but not the function package.

Manuel Eberl (Jul 29 2022 at 10:13):

Or are you doing something where this |supp id| <o |UNIV| might be coming from?

Jan van Brügge (Jul 29 2022 at 10:13):

The stuff I am working on is an extension of the datatype package. So yeah there are a few theorems like map_comp that require that, but I do not see how that is relevant for the function definition

Jan van Brügge (Jul 29 2022 at 10:14):

Well, currently HOL and HOL-Cardinals is loading, so let's see where this error actually comes from

Jan van Brügge (Jul 29 2022 at 10:16):

does the function package use the theorems of the datatype package?

Jan van Brügge (Jul 29 2022 at 10:17):

because that might explain it. I do register my datatypes as BNFs, but there are theorems already defined of the name <name>.map_comp that have those extra assumptions

Manuel Eberl (Jul 29 2022 at 10:27):

Hm, not sure. Maybe for the pattern matching. You could try expressing the pattern matching with a case expression and see what happens then.

Jan van Brügge (Jul 29 2022 at 10:33):

using a case expression does not change this. The stack trace tells me it happens when trying to find a congruence rule. I will investigate further once it has reloaded everything because I opened the ML files

Last updated: Dec 21 2024 at 16:20 UTC