k/kernel/src/main/java/org/kframework/compile/AddCoolLikeAtt.java at master · https-github-com-goodman-ops/k · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
// Copyright (c) 2019 K Team. All Rights Reserved.
package org.kframework.compile;

import org.kframework.attributes.Att;
import org.kframework.definition.Context;
import org.kframework.definition.ContextAlias;
import org.kframework.definition.Module;
import org.kframework.definition.Rule;
import org.kframework.definition.Sentence;
import org.kframework.kore.K;
import org.kframework.kore.KApply;
import org.kframework.kore.KSequence;
import org.kframework.kore.KVariable;
import org.kframework.kore.FoldK;

public class AddCoolLikeAtt {

    private final Module mod;

    public AddCoolLikeAtt(Module mod) {
      this.mod = mod;
    }

    private Rule add(Rule rule) {
        return new Rule(
                rule.body(),
                rule.requires(),
                rule.ensures(),
                transform(rule.body(), rule.att()));
    }

    private Context add(Context context) {
        return new Context(
                context.body(),
                context.requires(),
                transform(context.body(), context.att()));
    }

    private ContextAlias add(ContextAlias context) {
        return new ContextAlias(
                context.body(),
                context.requires(),
                transform(context.body(), context.att()));
    }

    private Att transform(K body, Att att) {
        if (new FoldK<Boolean>() {
            @Override
            public Boolean unit() {
                return false;
            }

            @Override
            public Boolean apply(KApply k) {
                if (mod.attributesFor().get(k.klabel()).getOrElse(() -> Att.empty()).contains("maincell")) {
                    if (k.items().get(0) instanceof KSequence) {
                        KSequence seq = (KSequence) k.items().get(0);
                        if (seq.items().size() > 0 && seq.items().get(0) instanceof KVariable) {
                            return true;
                        }
                    }
                }
                return super.apply(k);
            }

            @Override
            public Boolean merge(Boolean a, Boolean b) {
                return a || b;
            }
        }.apply(body)) {
          return att.add("cool-like");
        }
        return att;
    }

    public synchronized Sentence add(Sentence s) {
        if (s instanceof Rule) {
            return add((Rule) s);
        } else if (s instanceof Context) {
            return add((Context) s);
        } else if (s instanceof ContextAlias) {
            return add((ContextAlias) s);
        } else {
            return s;
        }
    }
}