Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

new_type_definition produces bad error messages #128

Closed
mn200 opened this issue Aug 12, 2013 · 4 comments
Closed

new_type_definition produces bad error messages #128

mn200 opened this issue Aug 12, 2013 · 4 comments

Comments

@mn200
Copy link
Member

mn200 commented Aug 12, 2013

Reported by Rob Arthan

I think the section on new_type_definition in the HOL 4 reference manual should say that it fails if the theorem in the parameter has free variables. E.g.,

app load ["PairedLambda", "Q"]; open PairedLambda pairTheory;
val tyax1 = new_type_definition ("bad1", Q.prove(`?p.(\(x,y). ~(x /\ y /\ z)) p`,
Q.EXISTS_TAC `(F,F)` THEN GEN_BETA_TAC THEN REWRITE_TAC []));

correctly results in an error:

Exception-
   HOL_ERR
  {message =
  "at Thm.prim_type_definition:\nsubset predicate must be a closed term",
  origin_function = "new_type_definition", origin_structure = "Definition"}
   raised

In fact, this is the only error message I can provoke:

val tyax2 = new_type_definition ("bad1", Q.prove(`?p.FST p \/ SND p`,
Q.EXISTS_TAC `(T,T)` THEN REWRITE_TAC []));

results in the same exception even though what is wrong here is that the theorem doesn't have the form |= ?x.t x

@ghost ghost assigned mn200 Aug 12, 2013
@mn200
Copy link
Member Author

mn200 commented Aug 12, 2013

Strictly, that error message is “sort of” legitimate: the existing code sees ?p. FST p \/ SND p and takes it apart to match a predicate applied to an argument, giving the predicate as ((\/) (FST p)) and the argument as SND p. The predicate is indeed of type α → bool for some α, but the predicate includes a free variable (p) and so you get the error you do.

Of course, this is not as helpful as it might be. I will shortly change the code to check that the argument is the bound variable of the existential before falling through to the free variable check.

@konrad-slind
Copy link
Contributor

Hi Michael,

As the person who wrote that code some years ago, I thought I'd offer my
fix. See how it fits with your
view.

Thanks,
Konrad.

fun dest_type_def thm =
let val (x,M) = dest_exists (concl thm)
val (P,y) = dest_comb M
in if x=y then P
else raise ERR "" ""
end
handle HOL_ERR _
=> raise TYDEF_ERR "expected a theorem of the form "?x. P x"";

fun prim_type_definition (name as {Thy, Tyop}, thm) =
let val checked = check_null_hyp thm TYDEF_ERR
val P = dest_type_def thm
val Pty = type_of P
val (dom,rng) = Type.dom_rng Pty
val checked = assert_exn null (free_vars P)
(TYDEF_ERR "subset predicate must be a closed term")
val tyvars = Listsort.sort Type.compare (type_vars_in_term P)
val _ = Type.prim_new_type name (List.length tyvars)
val newty = Type.mk_thy_type{Tyop=Tyop,Thy=Thy,Args=tyvars}
val repty = newty --> dom
val rep = mk_primed_var("rep", repty)
val TYDEF = mk_thy_const{Thy="bool",
Name="TYPE_DEFINITION",
Ty = Pty --> (repty-->bool)}
in
mk_defn_thm(tag thm,
mk_exists(rep, list_mk_comb(TYDEF,[P,rep])))
end

On Sun, Aug 11, 2013 at 9:31 PM, Michael Norrish
[email protected]:

Strictly, that error message is “sort of” legitimate: the existing code
sees ?p. FST p / SND p and takes it apart to match a predicate applied
to an argument, giving the predicate as ((/) (FST p)) and the argument
as SND p. The predicate is indeed of type α → bool for some α, but the
predicate includes a free variable (p) and so you get the error you do.

Of course, this is not as helpful as it might be. I will shortly change
the code to check that the argument is the bound variable of the
existential before falling through to the free variable check.


Reply to this email directly or view it on GitHubhttps://github.com//issues/128#issuecomment-22469555
.

@mn200
Copy link
Member Author

mn200 commented Aug 12, 2013

I've done something very similar, inlining to get

 val (bv,Body) = with_exn dest_exists (concl thm) TYDEF_FORM_ERR
 val (P,v)     = with_exn dest_comb Body TYDEF_FORM_ERR
 val _         = assert_exn (equal bv) v TYDEF_FORM_ERR

I’ll check this in shortly (just running the selftest build now).

@konrad-slind
Copy link
Contributor

Looks good. --Konrad.

On Sun, Aug 11, 2013 at 10:11 PM, Michael Norrish
[email protected]:

I've done something very similar, inlining to get

val (bv,Body) = with_exn dest_exists (concl thm) TYDEF_FORM_ERR
val (P,v) = with_exn dest_comb Body TYDEF_FORM_ERR
val _ = assert_exn (equal bv) v TYDEF_FORM_ERR

I’ll check this in shortly (just running the selftest build now).


Reply to this email directly or view it on GitHubhttps://github.com//issues/128#issuecomment-22470234
.

@mn200 mn200 closed this as completed in a64ae98 Aug 12, 2013
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants