Conditionals and forward references

digital-asset · Gertjan423 · May 20, 2020 · Apr 7, 2020 · Apr 8, 2020 · Apr 9, 2020
commit a8e6c948b6d9fc8e05a067fbb9b478c9d9aeab7c
diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs
@@ -1,6 +1,8 @@
 -- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
 -- SPDX-License-Identifier: Apache-2.0
 
+{-# LANGUAGE DataKinds #-}
+
 -- | Static verification of DAML packages.
 module DA.Daml.LF.Verify ( main ) where
 
@@ -14,31 +16,35 @@ 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 "amount"
+fieldName = FieldName "content"
 
 main :: IO ()
 main = do
   Options{..} <- execParser optionsParserInfo
   solver <- locateRunfiles "z3_nix/bin/z3"
   pkgs <- readPackages optInputDars
-  putStrLn "Start value phase" >> case runEnv (genPackages ValuePhase pkgs) emptyEnv of
+  putStrLn "Start value gathering"
+  case runEnv (genPackages pkgs) (emptyEnv :: Env 'ValueGathering) of
     Left err-> putStrLn "Value phase finished with error: " >> print err
     Right env1 -> do
       putStrLn "Start value solving"
-      let env2 = solveValueUpdatesEnv env1
-      putStrLn "Start template phase" >> case runEnv (genPackages TemplatePhase pkgs) env2 of
-        Left err -> putStrLn "Template phase finished with error: " >> print err
+      let env2 = solveValueReferences env1
+      putStrLn "Start choice gathering"
+      case runEnv (genPackages pkgs) env2 of
+        Left err -> putStrLn "Choice phase finished with error: " >> print err
         Right env3 -> do
-          putStrLn "Success!"
+          putStrLn "Start choice solving"
+          let env4 = solveChoiceReferences env3
           putStrLn "Start constraint solving phase"
-          let cset = constructConstr env3 templName choiceName fieldName
+          let cset = constructConstr env4 templName choiceName fieldName
           putStr "Create: " >> print (_cCres cset)
           putStr "Archive: " >> print (_cArcs cset)
           solveConstr solver cset