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