1#
2# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3#
4# SPDX-License-Identifier: BSD-2-Clause
5#
6"""Parser for skeletons of theory files which are completed
7by inserting parsed Haskell."""
8
9from __future__ import print_function
10from __future__ import absolute_import
11import sys
12import lhs_pars
13import os
14import os.path
15
16
17def create_find_source():
18    dir = os.environ['L4CAP']
19    dir = os.path.join(dir, 'src')
20    return lambda x: os.path.join(dir, x)
21
22
23find_source = create_find_source()
24bad_type_assignment = False
25
26
27if sys.argv[1] == '-q':
28    instructions = open(sys.argv[2])
29    quiet = True
30else:
31    instructions = open(sys.argv[1])
32    quiet = False
33
34for line in instructions:
35    instruct = line.strip()
36    if not instruct:
37        continue
38
39    [input, output] = [bit.strip() for bit in instruct.split('-->')]
40    output_tmp = os.path.join(os.path.dirname(output), 'pars_skel.tmp')
41
42    output_f = open(output_tmp, 'w')
43    output_f.write('(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)\n')
44    output_f.write('(* instead, see the skeleton file %s *)\n' %
45                   os.path.basename(input))
46
47    input_f = open(input)
48    for line in input_f:
49        if line.startswith('#INCLUDE_HASKELL'):
50            call = lhs_pars.Call()
51
52            bits = line.split()
53
54            call.filename = find_source(bits[1])
55            call.all_bits = 'all_bits' in bits
56            call.decls_only = 'decls_only' in bits
57            call.instanceproofs = 'instanceproofs' in bits
58            call.bodies_only = 'bodies_only' in bits
59            call.moduletranslations = dict([bit.split('=')
60                                            for bit in bits if '=' in bit])
61
62            if 'CONTEXT' in bits:
63                n = bits.index('CONTEXT')
64                call.current_context.append(bits[n + 1])
65
66            if 'ONLY' in bits:
67                n = bits.index('ONLY')
68                m = set(bits[n + 1:])
69                call.restr = lambda x: x.defined in m
70            elif 'NOT' in bits:
71                n = bits.index('NOT')
72                m = set(bits[n + 1:])
73                call.restr = lambda x: not x.defined in m
74            elif 'BODY' in bits:
75                call.body = True
76                assert bits[-2] == 'BODY'
77                fn = bits[-1]
78                call.restr = lambda x: x.defined == fn
79
80            try:
81                parsed = lhs_pars.parse(call)
82            except:
83                print("%s -X-> %s" % (input, output))
84                raise
85
86            bad_type_assignment |= call.bad_type_assignment
87            if bits[0] == '#INCLUDE_HASKELL_PREPARSE':
88                pass
89            else:
90                output_f.writelines(parsed)
91        elif line.startswith("#INCLUDE_SETTINGS"):
92            (_, settings) = line.split(None, 1)
93            settings = settings.strip()
94            lhs_pars.settings_line(settings)
95        else:
96            output_f.write(line)
97
98    output_f.close()
99
100    # at this point, output_tmp should exist, but output might not exist
101    if not os.path.exists(output_tmp):
102        print('Error: {} did not generate correctly'.format(output_tmp))
103        sys.exit(1)
104
105    if os.path.exists(output):
106        try:
107            lines1 = [line for line in open(output_tmp)]
108            lines2 = [line for line in open(output)]
109            changed = not (lines1 == lines2)
110        except IOError as e:
111            print("IOError comparing {} and {}:\n{}".format(output_tmp, output, e))
112            sys.exit(1)
113    else:
114        #print('Warning: {} does not exist, assuming changed'.format(output))
115        changed = 1
116
117    if changed:
118        if not quiet:
119            print(instruct)
120        try:
121            os.unlink(output)
122        except:
123            pass
124        try:
125            os.rename(output_tmp, output)
126        except IOError as e:
127            print("IOError moving {} -> {}:\n{}".format(output_tmp, output, e))
128            sys.exit(1)
129    else:
130        os.unlink(output_tmp)
131
132if bad_type_assignment and not quiet:
133    print("Note: for type assignments with parameters, define "
134          "the type explicitly in the theory skeleton",
135          file=sys.stderr)
136lhs_pars.warn_supplied_usage()
137