Re: [isabelle] Hide all constructors of a datatype automatically



Am 14.12.2013 13:41, schrieb Yannick Duchêne (Hibou57):
> Le Sat, 14 Dec 2013 13:27:01 +0100, Yannick Duchêne (Hibou57)
> <yannick_duchene at yahoo.fr> a écrit:
> 
>> Hello,
>>
>> May a solution can be found somewhere in “implementation.pdf”, from
>> the documentation pan. I believe it's possible to modify a theory
>> context using an embedded SML function (embedded in the theory file),
>> without a need for modifying Isabelle internal (I'm looking at it,
>> will be back if I feel I've found anything useful in
>> “implementation.pdf”).
>>
> 
> May be looking at page 10 and later, “0.2 SML embedded into
> Isabelle/Isar”, then at page 59 and later, “2.1 Types”.

I came up with the following short snippet:

setup {*
  let
    fun hide_const (c,_) thy = Sign.hide_const false c thy;
    fun hide_type t thy =
         let
           val t = Sign.intern_type thy t;
           val thy = case Datatype.get_constrs thy t of
                       NONE => thy (* Error would be better *)
                     | SOME xs => fold hide_const xs thy
         in
           Sign.hide_type false t thy
         end
    fun hide_all ts thy =
        fold hide_type ts thy
  in
    hide_all ["binOp", …]
  end
*}

Probably specifying the list explicitly at the end can also scripted
away :).

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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