[CakeML-dev] Using multiple basis modules

[Ramana Kumar]

Common problems include:
- The spec theorem has type variables that need instantiation,
- The function is not in scope,
- The function is applied to the wrong number of arguments

I think the middle one can reduce your goal to false whereas the others can
raise exceptions. Does your p variable have 'ffi ffi_proj type?

I'll try to have a look at some point. (Currently at AITP.)

On 25 Mar 2017 20:09, "Yong Kiam" <tanyongkiam at gmail.com> wrote:

> Those tactics are defined in the tactic libs in characteristic/, I fixed a
> few issues back on env-refactor by stepping through them.
>
> On Sat, Mar 25, 2017 at 2:46 PM, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>
>> Ok. I think I have the dependencies right now. However, I still have 4
>> cf_apps where xapp and xapp_spec fail, and I have no idea why, or how to
>> even start debugging the problem. This is on the sort_example branch,
>> characteristic/examples/sortProgScript.sml. Any hints would be greatly
>> appreciated.
>>
>> Scott
>>
>> > On 2017/03/25, at 02:46, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
>> wrote:
>> >
>> > Add arrays into the same linear sequence that includes I/O and update
>> the basis/dependency-order file accordingly.
>> >
>> > The longer term solution is to get the abstract translator working.
>> (There is an issue, and was some discussion on a wiki page.)
>> >
>> > On Friday, 24 March 2017, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>> > > I’m trying to verify a program with CF that uses both arrays and I/O
>> from the basis. I don’t see how to make this work, since you only seem to
>> be able to do 1 translation_extends. Any ideas?
>> > >
>> > > Scott
>> > > _______________________________________________
>> > > Developers mailing list
>> > > Developers at cakeml.org
>> > > https://lists.cakeml.org/listinfo/developers
>> > >
>>
>> _______________________________________________
>> Developers mailing list
>> Developers at cakeml.org
>> https://lists.cakeml.org/listinfo/developers
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170326/ee9d0d62/attachment.html>