[CakeML-dev] Array basis not type checking properly

[Yong Kiam]

There was more than one problem with it:

The parsed AST gives (Con (SOME (Short "SOME")) [Var (Short "n"); Var
(Short "d")]) for SOME(n,d)

But the inner argument to SOME should be tupled.

This is a known bug, see: https://github.com/CakeML/cakeml/issues/25

I'll temporarily fix this by putting in the correct AST for array_findi
instead of using process_topdecs.

Also, it's worth noting that the CF normalisation step doesn't produce
efficient code for common subexpressions:

      fun  foldr_aux f init arr n =
        let val  a = n = 0
         in
          if  a
           then  init
           else  (let val  e = n - 1
                      val  b = n - 1
                      val  c = sub arr b
                      val  d = f c init
                   in
                    foldr_aux f d arr e
                   end)
        end;

CC-ing dev for recording purposes.


On Wed, Apr 5, 2017 at 8:30 AM, Yong Kiam <tanyongkiam at gmail.com> wrote:

> Actually, the array one is obvious now: https://github.com/CakeML/
> cakeml/blob/master/basis/mlarrayProgScript.sml#L173
>
> That should recursively call findi_aux not find_aux
>
> On Wed, Apr 5, 2017 at 5:04 AM, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>
>> My verified sort utility also doesn’t type check, and I don’t know why.
>> I’m in the middle of adding error locations to the inferencer errors so
>> that we can debug these things.
>>
>> Scott
>>
>> > On 2017/04/04, at 22:57, Yong Kiam <tanyongkiam at gmail.com> wrote:
>> >
>> > Sorry, message got cut off at the end:
>> >
>> > I'm running
>> >
>> > val foo1= rconc (EVAL``case EL 80 basis of Tmod a b ls => Tmod a b
>> (TAKE 30 ls)``)
>> > val foo = (rconc (inf_eval ``infertype_prog init_config (TAKE 80 basis
>> ++ [^(foo1)])``))
>> >
>> > in benchmarkScript in case you want to try this out.
>> >
>> > On Tue, Apr 4, 2017 at 5:56 PM, Yong Kiam <tanyongkiam at gmail.com>
>> wrote:
>> > Hi all,
>> >
>> > I'm looking a little at the benchmarks right now, and the basis fails
>> to typecheck for me.
>> >
>> > I've traced it down to this declaration in the Array module:
>> >
>> >       fun findi_aux f arr max n =
>> >         let val a = n = max
>> >         in
>> >           if a
>> >           then NONE
>> >           else (let val b = sub arr n
>> >                     val c = f n b
>> >                 in
>> >                   if c
>> >                   then (let val d = sub arr n
>> >                         in
>> >                           SOME(n,d)
>> >                         end)
>> >                   else (let val e = n + 1
>> >                         in
>> >                           find_aux f arr max e
>> >                         end)
>> >                 end)
>> >         end;
>> >
>> > (This is pretty printed)
>> >
>> > I can't quite tell what's wrong with it though.
>> >
>> > I'm running
>> >
>> >
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170405/ae3ef936/attachment.html>