That's reasonable, and it would still be linear time, just linear in the
number of productions instead of the number of klabels. Go ahead and make
the change, since it shouldn't be too hard.


On Fri, Mar 7, 2014 at 8:13 AM, Andrei Stefanescu
<notifications@github.com>wrote:

> In
> src/javasources/KTool/src/org/kframework/backend/java/indexing/IndexingTable.java:
>
> > +    public IndexingTable(Definition definition) {
> > +        this.definition = definition;
> > +        buildBasicIndex();
> > +    }
> > +
> > +    private void buildBasicIndex() {
> > +
> > +        /* populate the table of rules rewriting the top configuration */
> > +        List<Index> indices = new ArrayList<Index>();
> > +        indices.add(TopIndex.TOP);
> > +        indices.add(BottomIndex.BOTTOM);
> > +        for (KLabelConstant kLabel : definition.kLabels()) {
> > +            indices.add(new KLabelIndex(kLabel));
> > +            indices.add(new FreezerIndex(kLabel, -1));
> > +            if (!kLabel.productions().isEmpty()) {
> > +                for (int i = 0; i < kLabel.productions().get(0).getArity(); ++i) {
>
> I agree with you that it is a potentially latent bug...I supposed this
> could be fixed by just taking the maximum arity over all the productions.
>
> --
> Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/271/files#r10388014>
> .
>