-
Notifications
You must be signed in to change notification settings - Fork 8
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Python POC #282
Closed
Closed
Python POC #282
Changes from 1 commit
Commits
Show all changes
445 commits
Select commit
Hold shift + click to select a range
a4bbd4d
comment
22eb959
wrap configs
884706f
utf8
3fd241a
fix stdlib
cb030b2
clarify
3a13661
fix
23ae9f3
catch more exceptions
795c148
changes
5c5b04a
refactor
ca6acb0
fix
d105232
fix
7bec002
clean externs
8e49dcb
fix
a5d1a6d
update gitignore
41e7e81
fix
34ea223
todos
bc67cd4
Merge branch 'main-1.x' into lucmcdon/python-poc
lucasmcdonald3 a361478
fix
959bb0a
Merge branch 'lucmcdon/python-poc' of github.com:smithy-lang/smithy-d…
99a2074
beta codegen for recursive structures via explicit conversion functions
847a792
fixed circular dependency on dafny_to_smithy
2c29c19
non-service codegen
471bea1
fix unions
ca0bb2b
dependencies
92c638b
refactor
871cfe0
fix
867d999
fix
bc34466
refactors
1b0bc2b
fix deps
51d1fa7
cleanup for conversions PR
1433680
refactor for cli integration pr
412b416
fix
808ced5
fixes
d195d89
refactor cli
48626a0
makefile
160ac0f
temp makefile
c4f22de
fix
c470ddb
fix?
77f4e16
cleanup
d7c7520
cleanup
331a534
??
bf87655
fix?
791ef2c
fix
43e9067
?
4226669
Merge branch 'temp' into lucmcdon/python-poc
b9bb983
...
e19b2a2
debug
7117525
?
a337b13
changes
d374fd4
changes
1876a61
fix net
f27a49f
cleanup
0a8d226
add types for completeness since these are benerated
6a0312a
foo
8a254c5
Merge branch 'main-1.x' of github.com:lucasmcdonald3/smithy-dafny int…
f9f5b5a
Merge branch 'main-1.x' into lucmcdon/python-poc
cb619a8
refactor
34cb179
fix
358496e
fix
60e73f6
fix
ec10c29
clean comment
cb99d88
changes
09fc556
update submodule
98d4f48
Merge branch 'lucmcdon/python-poc' into lucmcdon/python-kms
e6337da
with the new setup
58083f7
checkpoint
45465ef
check
de602c6
checkpoint
8d5fc09
checkpoint
60a98d8
sdks ok
86b2685
localservices back
eee69a6
changes
8d05edd
progress
93d2fce
refactor
6d41d44
kms pass again
daadf0f
changes
53a69ee
cleanup
a09bf5b
contraint pass again
c3bff79
constraints gen and pass
e945b8d
rm
663d510
dependencies
767ba3f
ddb
00d23a1
run sdks on gha
203308f
update submodule
47e44e9
fix
f3d21d9
fix
6dba062
fix
87aea4a
fix
9f775d9
fix refinement
dd2d0be
help aws
294fa95
pretend net
449abf0
tox MUST pass env varx
2a856c7
fix union
c91e3a6
fix extendable
bc3f71a
fix enum
4d376b8
fix deps
46e4b01
testtest
eb3cf75
debug
2ef71f0
debug
300032a
debug
a76a365
changes
8581680
fix
790adaa
fix
57b65f2
cleanup
0075c74
cleanup
edac414
cleanup
fec3c4b
testmodels cleanup
af8261f
refactor
71cd9aa
finish errors todos
01bc1dd
cleanup for overwrites
abbf4e2
update submodule
b600f2f
add resource reference shapes as resources to model
d978a91
mpl progress
6a816f9
sync
56eaee2
work on gen for mpl
5a5ebec
wip
dbf8b33
add missing file
b2fa87a
generating testvectors
lucasmcdonald3 4d9e418
wip, errors
lucasmcdonald3 85a0a97
generating passing the mpl tests
lucasmcdonald3 14880d0
cleanup
lucasmcdonald3 930ab50
progress
lucasmcdonald3 d153d24
fix constructor
lucasmcdonald3 af5a05f
Merge branch 'main-1.x' into lucmcdon/python-poc
lucasmcdonald3 c170266
changes
lucasmcdonald3 d76c268
fix"
lucasmcdonald3 2188f47
changes
lucasmcdonald3 81f71ee
missing... file?
lucasmcdonald3 97e180e
changes
lucasmcdonald3 467b8e4
changes
lucasmcdonald3 2be673a
changes
lucasmcdonald3 8107384
cleanup
lucasmcdonald3 97be79e
migrate more
lucasmcdonald3 131a7ef
missing'
lucasmcdonald3 164dd43
m
lucasmcdonald3 d619c8d
m
lucasmcdonald3 4a67e9b
union
lucasmcdonald3 9348145
extendable
lucasmcdonald3 79763c8
more
lucasmcdonald3 c705b79
add missing
lucasmcdonald3 0e7521b
remove wrapped smithygenerated dir
lucasmcdonald3 f5a591f
fix deps?
lucasmcdonald3 d61d685
missing'
lucasmcdonald3 43711c7
fix ref?
lucasmcdonald3 88a8106
fixes
lucasmcdonald3 6c91dd0
fix ref?
lucasmcdonald3 f8850c1
fix sks
lucasmcdonald3 1d689e8
ls
lucasmcdonald3 de53492
ls
lucasmcdonald3 39f4ace
gha
lucasmcdonald3 e4597a3
fix
lucasmcdonald3 e0d5502
fix
lucasmcdonald3 6a97852
?
lucasmcdonald3 6068db2
wipmultiple
lucasmcdonald3 3727791
MM
lucasmcdonald3 c166ced
missing
lucasmcdonald3 98fa1ce
some simples
lucasmcdonald3 1a85aac
sipmles
lucasmcdonald3 e0b1077
refactor untested
lucasmcdonald3 4fc56ea
refactor untested
lucasmcdonald3 d3d29ab
fix
lucasmcdonald3 fc5df6d
changes
lucasmcdonald3 b0aaeca
changes
lucasmcdonald3 8d33264
change
lucasmcdonald3 d75eb94
fix
lucasmcdonald3 6f347b0
fix
lucasmcdonald3 9f47d5f
fix
lucasmcdonald3 801eaaf
fix
lucasmcdonald3 fc86290
fix
lucasmcdonald3 c3ad149
bump verify java version
lucasmcdonald3 4b9c537
SOME pydoc
lucasmcdonald3 2117aee
slightly better pydoc
lucasmcdonald3 1311fc3
docs, typehints, multiple codes fixes
lucasmcdonald3 0cd72e3
revert errors any
lucasmcdonald3 da4b7d6
changes
lucasmcdonald3 8f5f023
use alternate constructor in deps
lucasmcdonald3 41ff714
gen mpl
lucasmcdonald3 9168edb
fix override?
lucasmcdonald3 9ca71ac
fix override?
lucasmcdonald3 6fba573
fix override?
lucasmcdonald3 11b64f3
gen services
lucasmcdonald3 856553e
refs symbols as forward references; remove as/fromdict
lucasmcdonald3 455c7a1
actual reference typehints
lucasmcdonald3 c9de9fc
as/from dict on references
lucasmcdonald3 b239641
cleanup
lucasmcdonald3 ff9ba38
fix
lucasmcdonald3 cb2b5f2
cleanup
lucasmcdonald3 c841864
cleanup
lucasmcdonald3 3bce489
clenaup, some test
lucasmcdonald3 0398e15
clenaup, some test
lucasmcdonald3 ee41dfa
clenaup, some test
lucasmcdonald3 6891280
clenaup, some test
lucasmcdonald3 fbb547b
update smithy-python
lucasmcdonald3 f632f5d
debug mpl
lucasmcdonald3 692842b
fix deps
lucasmcdonald3 bfa69ec
docs improvements
lucasmcdonald3 33a2754
fix up typehints on references
lucasmcdonald3 7b1d967
cleanup
lucasmcdonald3 dc2d170
FINALLY fix finding refs
lucasmcdonald3 1d20318
remove local PythonDafnyRuntime
lucasmcdonald3 f489cad
changes; refs, errors
lucasmcdonald3 771d1ad
changes
lucasmcdonald3 a57dadb
sync upstream
lucasmcdonald3 8728872
wip
lucasmcdonald3 c235930
merge
lucasmcdonald3 75fa068
fixes
lucasmcdonald3 619d675
fix python mk
lucasmcdonald3 291fbdf
merge
lucasmcdonald3 a09898a
Merge branch 'main-1.x' into lucmcdon/python-poc
lucasmcdonald3 ca2e438
debug merge
lucasmcdonald3 c1924a9
update smithy-python
lucasmcdonald3 865dd75
fixes
lucasmcdonald3 57aacab
doc
lucasmcdonald3 028321e
doc
lucasmcdonald3 86beecb
mk
lucasmcdonald3 00123bf
doc
lucasmcdonald3 baa153c
doc
lucasmcdonald3 aca426b
doc
lucasmcdonald3 086cf0e
doc
lucasmcdonald3 1eb058b
fixes
lucasmcdonald3 ea69ed2
fix exception msg
lucasmcdonald3 2c9d4f5
sdks
lucasmcdonald3 1e82a3f
fix
lucasmcdonald3 4bc0584
fix
lucasmcdonald3 0445306
fix
lucasmcdonald3 0593eca
fix
lucasmcdonald3 02c26e3
fix
lucasmcdonald3 ff57913
fix
lucasmcdonald3 66836ce
add module
lucasmcdonald3 efc2281
settings
lucasmcdonald3 d3fc5c8
rm gitmodules
lucasmcdonald3 0552eeb
rm
lucasmcdonald3 ed4ce50
rm
lucasmcdonald3 c438ce4
change
lucasmcdonald3 de1e084
commit modules
lucasmcdonald3 9b0388f
debug
lucasmcdonald3 e55545f
debug
lucasmcdonald3 f8c9b1f
wrap dep errors
lucasmcdonald3 9840d89
wrap dep errors
lucasmcdonald3 0767125
gen enum shapes
lucasmcdonald3 06f764b
enum conversion
lucasmcdonald3 e2b9cea
fix
lucasmcdonald3 6a9596f
fix
lucasmcdonald3 d9e0b32
fix
lucasmcdonald3 8980c96
merge
lucasmcdonald3 b2e3c8a
fix merge
lucasmcdonald3 acd1957
update path
lucasmcdonald3 2ff0001
fix
lucasmcdonald3 a2ad26a
chore: add SimpleEnumV2 TestModel for Python (#346)
justplaz 30ee7dd
copyright
lucasmcdonald3 File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
86 changes: 86 additions & 0 deletions
86
...ls/dafny-dependencies/StandardLibrary/runtimes/python/src/standard_library/extern/UTF8.py
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,86 @@ | ||
from standard_library.internal_generated_dafny.UTF8 import * | ||
import standard_library.internal_generated_dafny.UTF8 | ||
import _dafny | ||
import struct | ||
|
||
''' | ||
Extern UTF8 encode and decode methods. | ||
|
||
Note: | ||
Python's `.encode('utf-8')` does not handle surrogates. | ||
These methods are expected to handle surrogates (e.g. "\uD808\uDC00"). | ||
To work around this, we encode Dafny strings into UTF-16-LE (little endian) | ||
and decode them before encoding into UTF-8 (`_strict_tostring`). | ||
To decode, we reverse the encode step. (`_reverse_strict_tostring`) | ||
''' | ||
|
||
# Extend the Dafny-generated class with our extern methods | ||
class default__(standard_library.internal_generated_dafny.UTF8.default__): | ||
|
||
@staticmethod | ||
def Encode(s): | ||
try: | ||
return Wrappers.Result_Success(_dafny.Seq( | ||
default__._strict_tostring(s).encode('utf-8') | ||
)) | ||
# Catch both Encode and Decode errors. | ||
# The `try` block involves both encoding and decoding. | ||
except (UnicodeEncodeError, UnicodeDecodeError): | ||
return Wrappers.Result_Failure(_dafny.Seq("Could not encode input to Dafny Bytes.")) | ||
|
||
@staticmethod | ||
def _strict_tostring(s): | ||
''' | ||
Converts a Dafny Seq of ASCII characters | ||
into a string by writing a UTF-16-LE decoding, | ||
texastony marked this conversation as resolved.
Show resolved
Hide resolved
|
||
then decoding it to ASCII with `strict` encoding. | ||
|
||
This encoding-decoding allows subsequent ASCII-to-UTF8 encodings | ||
to handle surrogates as expected by Dafny code. | ||
|
||
This is exactly the `_dafny.string_from_utf_16` method, except with | ||
lucasmcdonald3 marked this conversation as resolved.
Show resolved
Hide resolved
|
||
`errors = 'strict'` in our code | ||
instead of | ||
`errors = 'replace'` in the `_dafny.string_from_utf_16` function. | ||
`strict` will throw an exception for invalid encodings, allowing us | ||
to detect invalid encodings and raise exceptions. | ||
:param s: | ||
:return: | ||
''' | ||
return b''.join(ord(c).to_bytes(2, 'little') for c in s).decode("utf-16-le", errors = 'strict') | ||
|
||
@staticmethod | ||
def Decode(s): | ||
try: | ||
a = bytes(s).decode('utf-8') | ||
out = default__._reverse_strict_tostring(a) | ||
return Wrappers.Result_Success(out) | ||
# Catch both Encode and Decode errors. | ||
# The `try` block involves both encoding and decoding. | ||
except (UnicodeDecodeError, UnicodeEncodeError): | ||
return Wrappers.Result_Failure(_dafny.Seq("Could not decode input from Dafny Bytes.")) | ||
|
||
|
||
@staticmethod | ||
def _reverse_strict_tostring(s): | ||
''' | ||
Converts a string into a Dafny Seq of ASCII characters. | ||
This will undo the `_strict_tostring` function in this file. | ||
:param s: | ||
:return: | ||
''' | ||
b = s.encode("utf-16-le", errors = "strict") | ||
out = [] | ||
# len(b)/2 is an integer by construction of UTF-16 encoding (2 bytes per encoded character) | ||
for i in range(int(len(b)/2)): | ||
# Take two consecutive bytes; | ||
c = b[2*i:2*i+2] | ||
# Unpack them into an ordinal representation; | ||
d = struct.unpack('<H', c) | ||
# Convert into a character representation; | ||
e = chr(d[0]) | ||
# Append to returned string | ||
out.append(e) | ||
return _dafny.Seq(out) | ||
lucasmcdonald3 marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
standard_library.internal_generated_dafny.UTF8.default__ = default__ |
22 changes: 22 additions & 0 deletions
22
...y-dependencies/StandardLibrary/runtimes/python/src/standard_library/extern/pyproject.toml
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
[tool.poetry] | ||
name = "standard-library-externs" | ||
version = "0.1.0" | ||
description = "" | ||
authors = ["AWS <[email protected]>"] | ||
packages = [ | ||
# Globally install all internaldafny modules | ||
# such that a module X can be imported with `import X` | ||
# from anywhere in the Python runtime that installs this module | ||
{ include = "*.py" }, | ||
] | ||
# Include all of the following .gitignored files in package distributions, | ||
# even though it is not included in version control | ||
include = ["*.py"] | ||
|
||
[tool.poetry.dependencies] | ||
python = "^3.11.0" | ||
standard-library-internaldafny = { path = "../internal_generated_dafny", develop = false} | ||
|
||
[build-system] | ||
requires = ["poetry-core"] | ||
build-backend = "poetry.core.masonry.api" |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Question: Tell me about the performance characteristics of this implementation.
It appears that we parse every character three times.
For Encoding:
For Decode:
Is this correct?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We are parsing each character 3 times on decode as well (reverse of encode).
(Obviously I'm not happy about this, but I struggled to handle surrogate characters, and this seemed to be the most commonly suggested pattern to handle those...)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We do not need to block development on this.
But we should not ship a product with this deficiency.
I do not know how often we convert strings,
but I imagine it's often.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This might be a good time to at least discuss the eventual path to using
--unicode-char:true
in Dafny. A big part of supporting that mode is avoiding exactly this annoying edge case.