Sounds like a bug. Can you send me sources?
Thanks,
Konrad.
On Wed, Jun 6, 2012 at 1:30 PM, Ramana Kumar <ramana.ku...@gmail.com> wrote:
> On Wed, Jun 6, 2012 at 7:20 PM, Konrad Slind <konrad.sl...@gmail.com> wrote:
>>
>> Note that Datatype.build_tyinfos is only guaranteed to work on
>> types that Hol_datatype produces. Does your datatype have
>> some other features?
>
>
> Yes, recursion through the range of a finite map.
>
> It wasn't _too_ difficult to prove what look like the right theorems
> manually, but it will be a pain if the type base still can't do anything
> even with those theorems.
> If it does work, though, I might look later into how to generalise this code
> to allow more datatypes with this kind of recursion to be defined (I've only
> done it for a specific datatype that I need).
>
>>
>> In any case, what happens with
>> gen_datatype_info?
>
>
> Fails the same way:
> Exception- HOL_ERR {message = "", origin_function = "list_mk_binder",
> origin_structure = "Term"} raised
>
>>
>>
>> Thanks,
>> Konrad.
>>
>>
>> On Wed, Jun 6, 2012 at 12:33 PM, Ramana Kumar <ramana.ku...@gmail.com>
>> wrote:
>> > Dear Konrad,
>> > Thanks a lot for your reply.
>> > I'm going to take this discussion onto the mailing list rather than the
>> > issue tracker.
>> > Further comments and questions below.
>> >
>> > On Wed, Jun 6, 2012 at 6:09 PM, Konrad Slind
>> >
>> > <reply+i-4768236-445b46219fa700ba592ca0826c0c435b3111c21c-181...@reply.github.com>
>> > wrote:
>> >>
>> >> Right, that's exactly the situation that should be documented. You
>> >> want to use
>> >>
>> >> TypeBase.write
>> >> [TypeBasePure.mk_datatype_info {...}];
>> >>
>> >> which creates the required tyinfo datastructure and installs it into
>> >> theTypeBase, which is the collection of useful type information used
>> >> by a variety of tools. There's a simple version of this invocation
>> >> at the end of
>> >>
>> >> src/sum/sumScript.sml
>> >>
>> >> There is something wrong with it, which I will discuss later. But
>> >> first,
>> >> let's
>> >> go through the supplied fields in the record.
>> >>
>> >> ax=TypeBasePure.ORIG sum_Axiom,
>> >>
>> >> This is the prim.rec. axiom characterizing the datatype, in the format
>> >> determined by the datatype package. The "TypeBasePure.ORIG"
>> >> constructor is needed because each type in a mutually recursive type
>> >> declaration will end up having the same axiom, and I didn't want to
>> >> barf out the same redundant info when printing out tyinfo information
>> >> when TypeBase.elts() is invoked. When dealing with a non-mutually
>> >> recursive type, just use TypeBasePure.ORIG <axiom>. If the type
>> >> is mutually recursive, you have to write each type separately; for
>> >> all but the first type, use TypeBasePure.COPY((thy,ty),axiom).
>> >>
>> >> case_def=sum_case_def,
>> >>
>> >> Definition of the case construct for the type.
>> >>
>> >> case_cong=sum_case_cong,
>> >>
>> >> Case cong theorem for the type.
>> >>
>> >> induction=TypeBasePure.ORIG sum_INDUCT,
>> >>
>> >> Induction theorem for the type. See discussion on ORIG and COPY
>> >> above.
>> >>
>> >> nchotomy=sum_CASES,
>> >>
>> >> Cases theorem for the type.
>> >>
>> >> size=NONE,
>> >>
>> >> Definition of a size function for the type. This is used when
>> >> synthesizing
>> >> termination measures used by Define's termination prover. In the case
>> >> of sums, size=NONE because of a bootstrapping issue: numbers haven't
>> >> been defined at this point in the system build, so I fill in the field
>> >> with NONE,
>> >> and replace it later (see src/num/theories/basicSize.sml).
>> >>
>> >> encode=NONE,
>> >>
>> >> The encode field is a vestigal remainder from some work I did with Joe
>> >> Hurd on
>> >> automatic generation and application of serializers for datatypes. Safe
>> >> to
>> >> leave
>> >> it as NONE.
>> >>
>> >> fields=[], accessors=[], updates=[],
>> >>
>> >> These are needed for record types. The way to figure out what they do
>> >> is
>> >> to
>> >> defined some simple record type "foo" then invoke
>> >>
>> >> TypeBase.fields_of ``:foo``;
>> >> TypeBase.accessors_of ``:foo``;
>> >> TypeBase.updates_of ``:foo``;
>> >>
>> >> recognizers = [ISL,ISR],
>> >> destructors = [OUTL,OUTR],
>> >>
>> >> We allow destructors and recognizers to be defined over
>> >> datatypes. I use this feature in Guardol, but if you aren't
>> >> going to do that for your application, you can leave the
>> >> lists empty.
>> >>
>> >> lift=SOME(mk_var("sumSyntax.lift_sum",
>> >> Parse.Type`:'type -> ('a -> 'term) ->
>> >> ('b -> 'term) ->
>> >> ('a,'b)sum -> 'term`)),
>> >>
>> >> lift is another vestigial field left over from the encoding experiment.
>> >> Actually, it is used to automate the extraction of HOL terms from
>> >> the results of ML evaluation. Unused at the moment.
>> >>
>> >> one_one=SOME INR_INL_11,
>> >> distinct=SOME sum_distinct
>> >>
>> >> You know what these are.
>> >>
>> >> Now, returning to what's wrogn with this: it occurs at the end of
>> >> sumScript.sml,
>> >> so a tyinfo for sum is duly made and installed in the TypeBase.
>> >> However,
>> >> then
>> >> evaluation of sumScript terminates and the sum tyinfo is thrown away.
>> >> So it seems
>> >> un-needed. However, the
>> >>
>> >> val _ = adjoin_to_theory
>> >> {sig_ps = NONE,
>> >> struct_ps = SOME(fn ppstrm =>
>> >> let val S = PP.add_string ppstrm
>> >> fun NL() = PP.add_newline ppstrm
>> >> in
>> >> ...
>> >> end)};
>> >>
>> >> just before that is needed in order to make the tyinfo addition to the
>> >> TypeBase persistent.
>> >
>> >
>> > I thought I saw something in Datatype.sml that automated the process of
>> > writing the correct "adjoin_to_theory" code. Is that reusable, or do I
>> > have
>> > to call adjoin_to_theory manually?
>> >
>> >>
>> >>
>> >> You might also have a look at Datatype.build_tyinfos, which automates
>> >> much of the drudgery of mk_datatype_info. All you need to do is
>> >> give the induction and prim.rec. theorems as input.
>> >>
>> >> val build_tyinfos : typeBase
>> >> -> {induction:thm, recursion:thm}
>> >> -> tyinfo list
>> >>
>> >> See src/datatype/Datatype.{sig,sml} for more details.
>> >
>> >
>> > build_tyinfos fails on my theorems with this error:
>> > HOL_ERR {message = "", origin_function = "list_mk_binder",
>> > origin_structure
>> > = "Term"}
>> > and I haven't yet tried to track down where exactly that is being
>> > raised.
>> >
>> > But it is a worry that build_tyinfos fails, because maybe more stuff
>> > will
>> > choke on the theorems I want to put into the TypeBase.
>> > Can you see anything easily fixable, or equally anything dooming my
>> > attempts
>> > to failure, in these theorems?
>> >
>> >> Cv1_induction;
>> > val it =
>> > |- ∀P0 P1 P2.
>> > (∀l. P0 (CLitv l)) ∧ (∀vs. P2 vs ⇒ ∀n. P0 (CConv n vs)) ∧
>> > (∀env. P1 env ⇒ ∀xs b. P0 (CClosure env xs b)) ∧
>> > (∀env. P1 env ⇒ ∀ns defs d. P0 (CRecClos env ns defs d)) ∧
>> > P1 FEMPTY ∧ (∀s v env. P0 v ∧ P1 env ⇒ P1 (env |+ (s,v))) ∧ P2 [] ∧
>> > (∀v vs. P0 v ∧ P2 vs ⇒ P2 (v::vs)) ⇒
>> > (∀v. P0 v) ∧ (∀env. P1 env) ∧ ∀vs. P2 vs:
>> > thm
>> >
>> >> Cv1_Axiom;
>> > val it =
>> > |- ∀f0 f1 f2 f3 f4 f5 f6 f7.
>> > ∃fn0 fn1 fn2.
>> > (∀l. fn0 (CLitv l) = f0 l) ∧
>> > (∀m vs. fn0 (CConv m vs) = f1 m vs (fn1 vs)) ∧
>> > (∀env xs b. fn0 (CClosure env xs b) = f2 env xs b (fn2 env)) ∧
>> > (∀env ns defs d.
>> > fn0 (CRecClos env ns defs d) = f3 env ns defs d (fn2 env)) ∧
>> > (fn1 [] = f4) ∧ (∀v vs. fn1 (v::vs) = f5 v vs (fn0 v) (fn1 vs)) ∧
>> > ∀env. fn2 env = f6 env (f7 o_f env):
>> > thm
>> >
>> >
>> >>
>> >>
>> >> Cheers,
>> >> Konrad.
>> >>
>> >>
>> >>
>> >>
>> >>
>> >> On Wed, Jun 6, 2012 at 5:08 AM, Ramana Kumar
>> >> <re...@reply.github.com>
>> >>
>> >> wrote:
>> >> > It would probably be more useful if there were suitable entrypoints
>> >> > for
>> >> > someone in the following situation (like me): I have manually proved
>> >> > * `ty_induction`
>> >> > * `ty_11`
>> >> > * `ty_distinct`
>> >> > * `ty_nchotomy`
>> >> > * `ty_Axiom`
>> >> > * `ty_case_def`
>> >> > * `ty_case_cong`
>> >> >
>> >> > And I think they are all of the correct form (but I don't know since
>> >> > those forms aren't documented), judging by the generated theorems for
>> >> > a very
>> >> > similar type.
>> >> > Now I want to add `ty` to the type base and make it persistent etc.
>> >> > (In particular I want to be able to use `Define` with my constructors
>> >> > and use tactics like `Induct` and `Cases`.)
>> >> > How can I do that?
>> >> >
>> >>
>> >> > ---
>> >> > Reply to this email directly or view it on GitHub:
>> >> > https://github.com/mn200/HOL/issues/65#issuecomment-6147028
>> >>
>> >>
>> >> ---
>> >> Reply to this email directly or view it on GitHub:
>> >> https://github.com/mn200/HOL/issues/65#issuecomment-6156553
>> >
>> >
>
>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
