1#!/usr/bin/env python3
2#
3# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
4#
5# SPDX-License-Identifier: BSD-2-Clause
6#
7
8#
9# Generate an Isabelle "ROOT" build file containing all examples
10# in the given directories.
11#
12
13import os
14import optparse
15import glob
16
17# Parse arguments
18parser = optparse.OptionParser()
19parser.add_option("-o", "--output", dest="output",
20                  help="output file", metavar="FILE")
21parser.add_option("-i", "--input-dir", dest="input_dir",
22                  help="input directory", action="append", default=[],
23                  metavar="DIR")
24parser.add_option("-s", "--session-name", dest="session_name",
25                  help="isabelle session name", metavar="NAME")
26parser.add_option("-b", "--base-session", dest="base_session",
27                  help="isabelle base session", metavar="NAME")
28parser.add_option("-d", "--named-session-dependency", dest="session_dependencies",
29                  help="additional named session dependency", action="append", default=[],
30                  metavar="NAME")
31parser.add_option("-q", "--quick-and-dirty", dest="quick_and_dirty",
32                  help="ROOT file should compile with \"quick and dirty\" enabled.",
33                  action="store_true", default=False)
34parser.add_option("-T", "--generate-theory", dest="theory_file",
35                  action="store_true", default=False,
36                  help="Generate a theory file instead of a ROOT file.")
37parser.add_option("--dir", dest="dirs",
38                  help="additional session directory", action="append",
39                  default=[], metavar="NAME")
40(options, args) = parser.parse_args()
41
42# Check arguments
43if len(args) != 0:
44    parser.error("Additional arguments passed in.")
45if options.output == None:
46    parser.error("Require an output filename.")
47if len(options.input_dir) == 0:
48    parser.error("Require at least one input directory.")
49if options.session_name == None and not options.theory_file:
50    parser.error("Require a session name.")
51if options.base_session == None and not options.theory_file:
52    parser.error("Require a base session.")
53output_dir = os.path.dirname(options.output)
54
55# Generate ROOT file.
56with open(options.output, "w") as output:
57    # Fetch list of files to test.
58    theories = []
59    for d in options.input_dir:
60        theories += sorted(glob.glob(os.path.join(d, "*.thy")))
61
62    if options.theory_file:
63        session_name = os.path.splitext(os.path.basename(options.output))[0]
64
65        def import_name(file):
66            return os.path.splitext(os.path.relpath(file, os.path.dirname(options.output)))[0]
67
68        # Write a theory file.
69        output.write("theory %s imports\n" % session_name)
70        for i in theories:
71            # Theories have the ".thy" stripped off.
72            output.write("  \"%s\"\n" % import_name(i))
73        output.write("begin\n")
74        output.write("\n")
75        output.write("end\n")
76    else:
77        # Write our ROOT file.
78        output.write("session \"%s\" = \"%s\" +\n" % (options.session_name, options.base_session))
79        if options.session_dependencies:
80            output.write("  sessions\n")
81            for i in options.session_dependencies:
82                output.write("    \"%s\"\n" % i)
83        if options.dirs:
84            output.write("  directories\n")
85            for i in options.dirs:
86                output.write("    \"%s\"\n" % i)
87        if options.quick_and_dirty:
88            output.write("  theories [quick_and_dirty]\n")
89        else:
90            output.write("  theories\n")
91        for i in theories:
92            # Theories have the ".thy" stripped off.
93            thy = os.path.relpath(i, output_dir)
94            thy = os.path.splitext(thy)[0]
95            output.write("    \"%s\"\n" % thy)
96