Psamathe/flow at master · ReedOei/Psamathe · 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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
#!/usr/bin/env bash

set -e

KDISTR="$HOME/k-framework/k-distribution/bin"
FLAGS=()

RED='\033[0;31m'
GREEN='\033[0;32m'
NC='\033[0m' # No Color

directory="dynamic/"

if [[ "$1" == "typecheck" ]]; then
    shift
    directory="static/"

    if [[ "$1" == "debug" ]]; then
        shift
        FLAGS+=("--log")
        FLAGS+=("--log-cells")
        FLAGS+=("(k),(#pc),#result,(typeEnv)")
        # FLAGS+=("--search")
    else
        # FLAGS+=("--output")
        # FLAGS+=("none")
        FLAGS+=("--search")
        FLAGS+=("--pattern")
        FLAGS+=("<k> . </k>")
        FLAGS+=("--bound")
        FLAGS+=("1")
    fi
elif [[ "$1" == "compile" ]]; then
    shift
    directory="compiler/"
    if [[ "$1" == "debug" ]]; then
        shift
        FLAGS+=("--log")
        FLAGS+=("--log-cells")
        FLAGS+=("(k),(#pc),#result")
    fi
elif [[ "$1" == "pure" ]]; then
    shift
    directory="pure-flow/"
elif [[ "$1" == "pure-compile" ]]; then
    shift
    directory="pure-flow-compiler/"
else
    directory="dynamic/"
    if [[ "$1" == "debug" ]]; then
        shift
        FLAGS+=("--log")
        FLAGS+=("--log-cells")
        FLAGS+=("(k),(#pc),#result,(storage),(lookup),(localTypeEnv)")
    fi

    if [[ "$1" == "test" ]]; then
        FLAGS+=("--pattern")
        FLAGS+=("<k> . </k>")
    fi
fi

if [[ "$1" == "test" ]]; then
    shift

    fname=""

    for arg in "$@"; do
        if [[ ! "$arg" =~ "^--" ]]; then
            fname="$arg"
            break
        fi
    done

    if [[ -z "$fname" ]]; then
        echo "No filename specified!"
        exit 1
    fi

    if [[ -e "$fname.pat" ]]; then
        FLAGS+=("--pattern")
        FLAGS+=("$(cat "$fname.pat")")
    fi

    result="fail"
    if [[ -e "$fname.out" ]]; then
        if "$KDISTR/krun" "${FLAGS[@]}" --directory "$directory" "$@" | diff - "$fname.out"; then
            result="pass"
        fi
    else
        echo "[WARNING] No output file for $fname!"
        exit 0
    fi

    if [[ "$result" == "fail" ]]; then
        echo -e "${RED}[ERROR] $fname failed${NC}"
        exit 1
    else
        echo -e "${GREEN}[INFO] $fname passed${NC}"
    fi
else
    if [[ "$1" == "log" ]]; then
        shift

        if [[ "$1" == "skip" ]]; then
            shift
            depth="$1"
            shift
        else
            depth=1
        fi
        prev_output=""

        set +e
        pkill -f "kserver"
        set -e
        "$KDISTR/kserver" &> /dev/null &

        while true; do
            set -x
            output="$(time "$KDISTR/krun" --directory "$directory" --depth "$depth" "${FLAGS[@]}" "$@")"
            set +x
            if [[ "$output" == "$prev_output" ]]; then
                break
            else
                prev_output="$output"
            fi
            depth=$((depth + 1))
        done
        pkill -f "kserver"
    else
        set -x
        "$KDISTR/krun" --directory "$directory" "${FLAGS[@]}" "$@"
    fi
fi