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
Small missing arithmetic
  • Loading branch information
@Gertjan423
Gertjan423 committed May 6, 2020
commit 50c56c387b593d3eb5c76c0428a0bdcbfa521b3a
29 changes: 25 additions & 4 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 @@ -25,12 +25,18 @@ import DA.Daml.LF.Verify.Context
data ConstraintExpr
-- | Boolean value.
= CBool !Bool
-- | Integer value.
| CInt !Integer
-- | Real value.
| CReal !Rational
-- | Reference to an expression variable.
| CVar !ExprVarName
-- | Sum of two expressions.
| CAdd !ConstraintExpr !ConstraintExpr
-- | Subtraction of two expressions.
| CSub !ConstraintExpr !ConstraintExpr
-- | Equals operator.
| CEq !ConstraintExpr !ConstraintExpr
-- | Boolean and operator.
| CAnd !ConstraintExpr !ConstraintExpr
-- | Boolean not operator.
Expand All @@ -42,9 +48,12 @@ data ConstraintExpr

instance Show ConstraintExpr where
Gertjan423 marked this conversation as resolved.
Show resolved Hide resolved
show (CBool b) = show b
show (CInt i) = show i
show (CReal i) = show i
show (CVar x) = T.unpack $ unExprVarName x
show (CAdd e1 e2) = show e1 ++ " + " ++ show e2
show (CSub e1 e2) = show e1 ++ " - " ++ show e2
show (CEq e1 e2) = show e1 ++ " == " ++ show e2
show (CAnd e1 e2) = show e1 ++ " and " ++ show e2
show (CNot e) = "not " ++ show e
show (CIf e1 e2 e3) = "if " ++ show e1 ++ " then " ++ show e2 ++ " else " ++ show e3
Expand All @@ -63,12 +72,18 @@ instance ConstrExpr BoolExpr where
instance ConstrExpr Expr where
toCExp (EVar x) = CVar x
toCExp (ERecProj _ f (EVar x)) = CVar $ recProj2Var x f
toCExp (ETmApp (ETmApp (ETyApp (EBuiltin b) _) e1) e2) = case b of
BEAddNumeric -> CAdd (toCExp e1) (toCExp e2)
BESubNumeric -> CSub (toCExp e1) (toCExp e2)
_ -> error ("Builtin: " ++ show b)
toCExp (ETmApp (ETmApp op e1) e2) = case op of
(EBuiltin (BEEqual _)) -> CEq (toCExp e1) (toCExp e2)
(EBuiltin BEAddInt64) -> CAdd (toCExp e1) (toCExp e2)
(EBuiltin BESubInt64) -> CSub (toCExp e1) (toCExp e2)
(ETyApp (EBuiltin BEAddNumeric) _) -> CAdd (toCExp e1) (toCExp e2)
(ETyApp (EBuiltin BESubNumeric) _) -> CSub (toCExp e1) (toCExp e2)
_ -> error ("Builtin: " ++ show op)
toCExp (ELocation _ e) = toCExp e
toCExp (EBuiltin (BEBool b)) = CBool b
toCExp (EBuiltin (BEInt64 i)) = CInt $ toInteger i
-- TODO
-- toCExp (EBuiltin (BENumeric i)) = CReal i
toCExp e = error ("Conversion: " ++ show e)

instance ConstrExpr a => ConstrExpr (Cond a) where
Expand Down Expand Up @@ -172,6 +187,8 @@ cexp2sexp :: [(ExprVarName,S.SExpr)]
-- ^ The constraint expression to convert.
-> IO S.SExpr
cexp2sexp _vars (CBool b) = return $ S.bool b
cexp2sexp _vars (CInt i) = return $ S.int i
cexp2sexp _vars (CReal i) = return $ S.real i
cexp2sexp vars (CVar x) = case lookup x vars of
Just exp -> return exp
Nothing -> error ("Impossible: variable not found " ++ show x)
Expand All @@ -183,6 +200,10 @@ cexp2sexp vars (CSub ce1 ce2) = do
se1 <- cexp2sexp vars ce1
se2 <- cexp2sexp vars ce2
return $ S.sub se1 se2
cexp2sexp vars (CEq ce1 ce2) = do
se1 <- cexp2sexp vars ce1
se2 <- cexp2sexp vars ce2
return $ S.eq se1 se2
cexp2sexp vars (CAnd ce1 ce2) = do
se1 <- cexp2sexp vars ce1
se2 <- cexp2sexp vars ce2
Expand Down