Skip to content
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.

Sign up for GitHub

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

WIP: Draft version constraint generation #5472

Merged
merged 51 commits into from
May 20, 2020
Merged

WIP: Draft version constraint generation #5472

Changes from 1 commit
Commits
Show all changes
51 commits
Select commit Hold shift + click to select a range
040ef56
Draft version constraint generation
Gertjan423 Apr 7, 2020
0205507
Some code cleanup
Gertjan423 Apr 8, 2020
3476a5e
Substitution functions
Gertjan423 Apr 9, 2020
4675fdd
Template generation
Gertjan423 Apr 9, 2020
afc3766
Reformatted
Gertjan423 Apr 9, 2020
c329b37
Attempt to fix failing check
Gertjan423 Apr 9, 2020
f3e4d17
Rework generation for value definitions into 2 phase approach
Gertjan423 Apr 15, 2020
a7ef445
Various small changes
Gertjan423 Apr 16, 2020
c99827d
Rework delta to env state
Gertjan423 Apr 16, 2020
28eb1bb
Incorporate data type definitions
Gertjan423 Apr 17, 2020
80bb27a
Various constraint generation bug fixes and improvements
Gertjan423 Apr 21, 2020
220d21d
First part of constraint solving
Gertjan423 Apr 21, 2020
2bad89e
Minor bugfixes
Gertjan423 Apr 22, 2020
733f929
Added simple-smt to bazel
Gertjan423 Apr 22, 2020
5545943
Depend on z3
cocreature Apr 22, 2020
b736d85
Working pipeline
Gertjan423 Apr 23, 2020
4bc25cb
Fix overwriting value definitions, and delayed choice bindings
Gertjan423 Apr 23, 2020
310d7b0
Keep track of contract id's after fetching
Gertjan423 Apr 24, 2020
4b08356
Renaming of choice parameters
Gertjan423 Apr 24, 2020
e04944f
Cleanup
Gertjan423 Apr 24, 2020
18b0b97
Reals instead of ints
Gertjan423 Apr 27, 2020
2f3bf70
Various TODOs
Gertjan423 Apr 27, 2020
0911a90
Added function documentation
Gertjan423 Apr 27, 2020
6651d8d
Small bugfix
Gertjan423 Apr 29, 2020
a8e6c94
Conditionals and forward references
Gertjan423 Apr 29, 2020
50c56c3
Small missing arithmetic
Gertjan423 May 6, 2020
d880fa5
More small missing arithmetic
Gertjan423 May 6, 2020
aef855a
Fix daml 1.0.1 bug
Gertjan423 May 6, 2020
6c86c22
Read arguments and support fields in different templates
Gertjan423 May 7, 2020
1c21ff2
Proper verify output for testing, generate counter example, proper va…
Gertjan423 May 7, 2020
a33365c
Working testing framework, with some basic test cases
Gertjan423 May 8, 2020
64370c2
Testing: build daml instead of storing dar files
Gertjan423 May 12, 2020
f3bee74
Proper handling of update types; constraint synonyms
Gertjan423 May 11, 2020
13eb8a4
Additional equality constraints after create update
Gertjan423 May 14, 2020
16aa3e3
Make assertion print conditional
Gertjan423 May 14, 2020
642c1b9
Various improvements from PR feedback
Gertjan423 May 14, 2020
c791f31
Apply suggestions from code review
Gertjan423 May 14, 2020
ba1fad5
Small fix: Add missing import
Gertjan423 May 14, 2020
344eca8
Small fix: convert numerics
Gertjan423 May 15, 2020
1cdf6e4
Replace PRSelf with correct package reference
Gertjan423 May 15, 2020
cdbed09
Style fixes
Gertjan423 May 15, 2020
c62c276
Rework conditionals to remove When
Gertjan423 May 19, 2020
ed91ada
Cleanup test daml files
Gertjan423 May 19, 2020
b803eb9
Merge branch 'master' into daml-lf-verification
Gertjan423 May 19, 2020
a3ee542
Small style fixes
Gertjan423 May 19, 2020
91c989c
Bugfix after merge
Gertjan423 May 19, 2020
337b0ca
Attempt to fix bazel windows error
Gertjan423 May 19, 2020
49563b0
Attempt #2 to fix bazel windows error
Gertjan423 May 19, 2020
ae4a276
Attempt #3 to fix bazel windows error
Gertjan423 May 19, 2020
77ea060
Attempt #4 to fix bazel windows error
Gertjan423 May 19, 2020
2d7c840
Attempt #5 to fix bazel windows error
Gertjan423 May 19, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
More small missing arithmetic
  • Loading branch information
@Gertjan423
Gertjan423 committed May 6, 2020
commit d880fa52fe67491f832545a88d6a1d8b91ef1118
4 changes: 4 additions & 0 deletions compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,10 @@ instance ConstrExpr Expr where
(EBuiltin BESubInt64) -> CSub (toCExp e1) (toCExp e2)
(ETyApp (EBuiltin BEAddNumeric) _) -> CAdd (toCExp e1) (toCExp e2)
(ETyApp (EBuiltin BESubNumeric) _) -> CSub (toCExp e1) (toCExp e2)
(ETmApp (ETyApp (EVal (Qualified _ _ (ExprValName "+"))) _) _) ->
CAdd (toCExp e1) (toCExp e2)
(ETmApp (ETyApp (EVal (Qualified _ _ (ExprValName "-"))) _) _) ->
CSub (toCExp e1) (toCExp e2)
_ -> error ("Builtin: " ++ show op)
toCExp (ELocation _ e) = toCExp e
toCExp (EBuiltin (BEBool b)) = CBool b
Expand Down