Re: [isabelle] getting past ConstDefs.add_constdefs_i



Makarius writes:
> On Tue, 28 Feb 2006, Michael Norrish wrote:
 
> > What am I likely to be doing wrong in my invocation of add_constdefs_i?
 
> This is hard to guess from a distance.

Trying to step through the code, inasmuch as this is possible without
hitting hidden functions, I get to the point where 

  ProofContext.cert_term (ProofContext.init thy) tm

fails, but 

  cterm_of thy tm

succeeds.  

Having looked at the code, I'm now pretty sure the reason for this is
that

  Sign.certify_term 

calls certify_typ on the types of its argument (using map_term_types),
but

  ProofContext.cert_term 

does not.  It would be nice if the two behaved a little more
consistently, but I can now deal with the issue.  In particular, if
you pass Consts.certify a term that doesn't have its type
abbreviations expanded, then it will complain.  The action of
certifying a type does this expansion (among other things, I'm sure).
 
> Generally speaking, add_constdefs_i is just the internal version of
> a user-level command -- it is common practice to provide both
> external and internal version just to make sure that ML packages can
> always invoke each other.  For basic definitions the primitive
> add_consts/add_defs are usually easier to use in ML.  Even more,
> constdefs is about to become a legacy feature pretty soon, being
> superceded by a more general 'definition' element.

When implemented, please document the ML API for this new entry-point!

> Note that Constdefs.add_constdefs_i produces extra noise on the message 
> channel -- this is a toplevel command after all.
 
Yes, this is what I want because I'm implementing a top-level command
myself.

Michael.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.