build

#!/usr/bin/env python3

import sys
from os import (path, environ)
import functools

repo_dir = path.dirname(__file__)
sys.path.append(path.join(repo_dir, 'ext/'))
from kninja import *
environ['PATH'] = path.join(repo_dir, 'ext/k-light/bin/') + ':' + environ['PATH']

# Project Definition
# ==================

proj = KProject()

# Executing Kore using the Kore backend
# -------------------------------------

kore_from_config = proj.rule( 'kore-from-config'
                            , description = 'kore-from-config: $in'
                            , command = 'lib/kore-from-config "$in" "$out" || (cat "$in" ; false)'
                            , ext = 'kore'
                            )
k_from_config = proj.rule( 'k-from-config'
                         , description = 'k-from-config'
                         , command = 'lib/k-from-config "$in" "$out" || (cat "$in" ; false)'
                         , ext = 'kore'
                         )
def kore_exec(kore, ext = 'kore-exec'):
    return proj.rule( 'kore-exec'
                    , description = 'kore-exec'
                    , command     = '$k_bindir/kore-exec $kore --module "$module" --pattern $in > $out'
                    ) \
                    .variables(kore = kore) \
                    .implicit([kore, proj.build_k('haskell')])

# Parsing Outer K using k-light
# -----------------------------

def build_k_light():
    return proj.rule( 'build-k-light'
                    , description = 'Building K-light'
                    , command = '(cd ext/k-light && mvn package -q -DskipTests) && touch $out'
                    ) \
                    .output(proj.builddir('k-light.timestamp'))
k_light = proj.dotTarget().then(build_k_light())

# Kore to K Pipeline
# ------------------

ekore  = 'src/ekore.md'
kore   = 'src/kore.md'
parser = 'src/parser-util.md'
file   = 'src/file-util.md'

kink = proj.definition( backend   = 'ocaml'
                      , main      = 'src/kink.md'
                      , other     = [kore, ekore, parser, file, 'src/command-line.md', k_light]
                      , directory = proj.builddir('kink')
                      , flags     = '--syntax-module KINK-SYNTAX'
                      , alias     = 'kink'
                      , runner_script = './kink'
                      )

def pipeline(commandline, extension):
    return kink.krun().ext(extension).variables(
                flags = "-cCOMMANDLINE='%s' -cKINKDEPLOYEDDIR=%s"
                      % (commandline, kink.directory()))

def kink_test(base_dir, test_file, pipeline):
    input = path.join(base_dir, test_file)
    expected = path.join(base_dir, 'expected.ekore')
    return proj.source(input) \
               .then(pipeline) \
               .then(kore_from_config) \
               .then(proj.check(proj.source(expected))
                         .variables(flags = '--ignore-all-space --ignore-blank-lines')) \
               .default()

ekore_test = functools.partial(kink_test, pipeline = pipeline('ekore-to-kore'   , 'ekorePipeline'))

def parse_test(base_dir, def_file, input_program):
    def_path = path.join(base_dir, def_file)
    prog_path = path.join(base_dir, 'programs', input_program)
    expected = prog_path + '.kast'
    return proj.source(def_path) \
               .then(pipeline('kast ' + prog_path
                             , 'parse-' + input_program
                             ).implicit([prog_path])) \
               .then(k_from_config) \
               .then(proj.check(proj.source(expected))
                         .variables(flags = '--ignore-all-space --ignore-blank-lines')) \
               .default()

def lang_test(base_dir, module, program):
    language_kore    = path.join(base_dir, 'expected.ekore')
    program_pattern  = path.join(base_dir, 'programs', program + '.kast')
    expected_pattern = path.join(base_dir, 'programs', program + '.expected')
    runWithHaskell_pipeline = pipeline('kompile', 'noFrontend')

    lang_no_frontend_kore =  proj.source(language_kore) \
                                 .then(runWithHaskell_pipeline \
                                          .ext('noFrontend')) \
                                 .then(kore_from_config.variables(cell = 'definition'))
    return proj.source(program_pattern).then(kore_exec(lang_no_frontend_kore)
                                                 .ext('kore-exec')
                                                 .variables(module = module)
                                            ) \
                                       .then(proj.check(expected_pattern) \
                                                 .variables(flags = '--ignore-all-space --ignore-blank-lines')) \
                                       .default()

# Foobar
foobar_tests = []
foobar_tests += [ ekore_test('t/foobar', 'foobar.ekore')            ]
foobar_tests += [ ekore_test('t/foobar', 'expected.ekore')          ]
foobar_tests += [ parse_test('t/foobar', 'foobar.k', 'bar.foobar')  ]
foobar_tests += [ lang_test('t/foobar', 'FOOBAR', 'bar.foobar')     ]
proj.build('t/foobar', 'phony', inputs = Target.to_paths(foobar_tests))

# Peano
peano_tests = []
peano_tests += [ ekore_test('t/peano', 'peano.ekore')    ]
peano_tests += [ ekore_test('t/peano', 'expected.ekore') ]
peano_tests += [ lang_test('t/peano', 'PEANO', 'two-plus-two.peano') ]
peano_tests += [ parse_test('t/peano', 'peano.k', 'two-plus-two.peano') ]
proj.build('t/peano', 'phony', inputs = Target.to_paths(peano_tests))

# Imp
imp_tests = []
imp_tests += [ ekore_test('t/imp-simple', 'imp-simple.ekore') ]
imp_tests += [ ekore_test('t/imp-simple', 'expected.ekore') ]
imp_tests += [ lang_test('t/imp-simple', 'IMP-SIMPLE', 'conjunction.imp') ]
imp_tests += [ parse_test('t/imp-simple', 'imp-simple.k', 'conjunction.imp') ]
proj.build('t/imp', 'phony', inputs = Target.to_paths(imp_tests))

proj.main()