adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

haskell-translator: instance proofs for types without 0-arg constructors

This commit is contained in:
Gerwin Klein 2018-09-08 17:03:21 +10:00
parent d21ea9da41
commit 8356f303b6
1 changed files with 9 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
tools/haskell-translator/lhs_pars.py
View File

@ -1252,12 +1252,15 @@ def enum_instance_proofs (header, canonical, d):
lines.append('interpretation Arch .')
lines.append ('definition')
lines.append (' enum_%s: "enum_class.enum \<equiv> ' % header)
lines.append (' [ ')
for cons in cons_no_args[:-1]:
lines.append (' %s,' % cons)
for cons in cons_no_args[-1:]:
lines.append (' %s' % cons)
lines.append (' ]')
if len(cons_no_args) == 0:
lines.append (' []')
else:
lines.append (' [ ')
for cons in cons_no_args[:-1]:
lines.append (' %s,' % cons)
for cons in cons_no_args[-1:]:
lines.append (' %s' % cons)
lines.append (' ]')
for cons in cons_one_arg:
lines.append (' @ (map %s enum)' % cons)
lines[-1] = lines[-1] + '"'