Read arguments and support fields in different templates

digital-asset · Gertjan423 · May 20, 2020 · Apr 7, 2020 · Apr 8, 2020 · Apr 9, 2020
commit 6c86c22fe208e741cbb9d08ceadc5370d99e7a69
diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs
@@ -6,6 +6,7 @@
 -- | Static verification of DAML packages.
 module DA.Daml.LF.Verify ( main ) where
 
+import Data.Text
 import Options.Applicative
 
 import DA.Daml.LF.Ast.Base
@@ -15,22 +16,15 @@ import DA.Daml.LF.Verify.Read
 import DA.Daml.LF.Verify.Context
 import DA.Bazel.Runfiles
 
--- TODO: temporarily hardcoded
--- TODO: Allow for choice and field in different templates.
-templName :: TypeConName
-templName = TypeConName ["Iou"]
-
-choiceName :: ChoiceName
-choiceName = ChoiceName "Iou_Merge"
-
-fieldName :: FieldName
-fieldName = FieldName "content"
-
 main :: IO ()
 main = do
   Options{..} <- execParser optionsParserInfo
+  let choiceTmpl = TypeConName [pack optChoiceTmpl]
+      choiceName = ChoiceName (pack optChoiceName)
+      fieldTmpl = TypeConName [pack optFieldTmpl]
+      fieldName = FieldName (pack optFieldName)
   solver <- locateRunfiles "z3_nix/bin/z3"
-  pkgs <- readPackages optInputDars
+  pkgs <- readPackages [optInputDar]
   putStrLn "Start value gathering"
   case runEnv (genPackages pkgs) (emptyEnv :: Env 'ValueGathering) of
     Left err-> putStrLn "Value phase finished with error: " >> print err
@@ -44,7 +38,7 @@ main = do
           putStrLn "Start choice solving"
           let env4 = solveChoiceReferences env3
           putStrLn "Start constraint solving phase"
-          let cset = constructConstr env4 templName choiceName fieldName
+          let cset = constructConstr env4 choiceTmpl choiceName fieldTmpl fieldName
           putStr "Create: " >> print (_cCres cset)
           putStr "Archive: " >> print (_cArcs cset)
           solveConstr solver cset
diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Read.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Read.hs
@@ -24,15 +24,35 @@ import Options.Applicative
 import DA.Daml.LF.Ast
 
 data Options = Options
-    { optInputDars :: [FilePath]
+    { optInputDar :: FilePath
+    , optChoiceTmpl :: String
+    , optChoiceName :: String
+    , optFieldTmpl :: String
+    , optFieldName :: String
     }
 
 optionsParser :: Parser Options
 optionsParser = Options
-    <$> some ( argument str
-        (  metavar "DAR-FILES"
-        <> help "DAR files to analyse"
-        ) )
+    <$> argument str
+        (  metavar "DAR-FILE"
+        <> help "DAR file to analyse"
+        )
+    <*> argument str
+        (  metavar "CHOICE-TEMPLATE"
+        <> help "Template of the choice to analyse"
+        )
+    <*> argument str
+        (  metavar "CHOICE-NAME"
+        <> help "Name of the choice to analyse"
+        )
+    <*> argument str
+        (  metavar "FIELD-TEMPLATE"
+        <> help "Template of the field to verify"
+        )
+    <*> argument str
+        (  metavar "FIELD-NAME"
+        <> help "Name of the field to verify"
+        )
 
 optionsParserInfo :: ParserInfo Options
 optionsParserInfo = info (optionsParser <**> helper)

diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs
@@ -168,19 +168,21 @@ filterCondUpd tem f (Conditional b x (Just y)) =
 constructConstr :: Env 'Solving
   -- ^ The generator environment to convert.
   -> TypeConName
-  -- ^ The template name to be verified.
+  -- ^ The template name of the choice to be verified.
   -> ChoiceName
   -- ^ The choice name to be verified.
+  -> TypeConName
+  -- ^ The template name of the field to be verified.
   -> FieldName
   -- ^ The field name to be verified.
   -> ConstraintSet
-constructConstr env tem ch f =
-  case lookupChoInHMap (_envschs env) tem ch of
+constructConstr env chtem ch ftem f =
+  case lookupChoInHMap (_envschs env) chtem ch of
     Just (self, this, arg, updSubst) ->
       let upds = _ussUpdate $ updSubst (EVar self) (EVar this) (EVar arg)
           vars = concatMap skol2var (_envsskol env)
           (cres, arcs) = foldl
-            (\(cs,as) upd -> let (cs',as') = filterCondUpd tem f upd in (cs ++ cs',as ++ as'))
+            (\(cs,as) upd -> let (cs',as') = filterCondUpd ftem f upd in (cs ++ cs',as ++ as'))
             ([],[]) upds
       in ConstraintSet vars cres arcs
     Nothing -> error "Choice not found"