Remove closure type parameter from Value (#856)

Author: MatthewDaggitt

vehicle/src/Vehicle/Backend/LossFunction/Core.hs

@@ -8,7 +8,7 @@ import GHC.Generics (Generic)
 import Vehicle.Backend.Prelude (DifferentiableLogicID)
 import Vehicle.Compile.Prelude
 import Vehicle.Data.Builtin.Loss
-import Vehicle.Data.Code.Value (Value (..), WHNFBinder, WHNFBoundEnv, WHNFClosure (..), WHNFValue)
+import Vehicle.Data.Code.Value (BoundEnv, Closure (..), VBinder, Value (..))
 import Vehicle.Libraries.StandardLibrary.Definitions (StdLibFunction (..))
 
 --------------------------------------------------------------------------------
@@ -56,7 +56,7 @@ instance Pretty TensorDifferentiableLogicField where
   pretty = pretty . show
 
 type DifferentiableLogicImplementation =
-  Map TensorDifferentiableLogicField (WHNFValue LossTensorBuiltin)
+  Map TensorDifferentiableLogicField (Value LossTensorBuiltin)
 
 type CompiledDifferentiableLogic = (DifferentiableLogicID, DifferentiableLogicImplementation)
 
@@ -130,7 +130,7 @@ data RatTensorView expr
   | VReduceMaxRatTensor expr
   | VSearchRatTensor expr expr expr expr
 
-fromRatTensorView :: (BuiltinHasRatTensor builtin, BuiltinHasDimensionData builtin) => RatTensorView (WHNFValue builtin) -> WHNFValue builtin
+fromRatTensorView :: (BuiltinHasRatTensor builtin, BuiltinHasDimensionData builtin) => RatTensorView (Value builtin) -> Value builtin
 fromRatTensorView = \case
   VRatTensor y -> INullaryRatTensorOp (RatTensor y)
   VNegRatTensor x -> IRatTensorOp NegRatTensor (explicit <$> [x])
@@ -149,7 +149,7 @@ fromRatTensorView = \case
   VSearchRatTensor reduce lower upper fn -> IRatTensorOp SearchRatTensor (explicit <$> [reduce, lower, upper, fn])
   VRatTensorVar v -> VBoundVar v []
 
-toRatTensorView :: (BuiltinHasRatTensor builtin, BuiltinHasDimensionData builtin) => WHNFValue builtin -> RatTensorView (WHNFValue builtin)
+toRatTensorView :: (BuiltinHasRatTensor builtin, BuiltinHasDimensionData builtin) => Value builtin -> RatTensorView (Value builtin)
 toRatTensorView expr = case getRatTensorOp expr of
   Just (RatTensor b, []) -> VRatTensor b
   Just (NegRatTensor, [x]) -> VNegRatTensor (argExpr x)
@@ -181,5 +181,5 @@ preservedStdLibOps =
     [ StdForeachIndex
     ]
 
-pattern VLam2 :: WHNFBinder builtin -> WHNFBoundEnv builtin -> Binder builtin -> Expr builtin -> WHNFValue builtin
-pattern VLam2 binder1 env binder2 body <- VLam binder1 (WHNFClosure env (Lam _ binder2 body))
+pattern VLam2 :: VBinder builtin -> BoundEnv builtin -> Binder builtin -> Expr builtin -> Value builtin
+pattern VLam2 binder1 env binder2 body <- VLam binder1 (Closure env (Lam _ binder2 body))

vehicle/src/Vehicle/Backend/LossFunction/Domain.hs

@@ -48,17 +48,17 @@ type MonadDomain m =
   )
 
 data Domain = Domain
-  { lowerBound :: WHNFValue TensorBuiltin,
-    upperBound :: WHNFValue TensorBuiltin
+  { lowerBound :: Value TensorBuiltin,
+    upperBound :: Value TensorBuiltin
   }
 
 extractSearchDomain ::
   (MonadDomain m) =>
   DeclProvenance ->
-  WHNFBinder TensorBuiltin ->
+  VBinder TensorBuiltin ->
   Lv ->
-  WHNFValue TensorBuiltin ->
-  m (Domain, WHNFValue TensorBuiltin)
+  Value TensorBuiltin ->
+  m (Domain, Value TensorBuiltin)
 extractSearchDomain _propertyProv _binder _lv value = do
   {-
   _variableInfo <- case typeOf binder of
@@ -95,9 +95,9 @@ extractSearchDomain _propertyProv _binder _lv value = do
 --------------------------------------------------------------------------------
 -- Constraints
 
-type TensorElementInequality = Inequality UserElementVariable (WHNFValue TensorBuiltin)
+type TensorElementInequality = Inequality UserElementVariable (Value TensorBuiltin)
 
-type TensorInequality = Inequality Name (WHNFValue TensorBuiltin)
+type TensorInequality = Inequality Name (Value TensorBuiltin)
 
 type VariableConstraint = Either TensorElementInequality TensorInequality
 
@@ -109,20 +109,20 @@ splitConstraints = partitionEithers
 pattern NoConstraints :: VariableConstraints
 pattern NoConstraints = []
 
-type ConstrainedValue = (VariableConstraints, WHNFValue TensorBuiltin)
+type ConstrainedValue = (VariableConstraints, Value TensorBuiltin)
 
-unconstrained ::  WHNFValue TensorBuiltin -> ConstrainedValue
+unconstrained ::  Value TensorBuiltin -> ConstrainedValue
 unconstrained = (NoConstraints,)
 
 updateConstrainedValue ::
-  WHNFValue TensorBuiltin ->
+  Value TensorBuiltin ->
   ConstrainedValue ->
   ConstrainedValue
 updateConstrainedValue originalExpr = \case
   constr@(_ : _, _) -> constr
   ([], _) -> ([], originalExpr)
 
-instance IsConstant (WHNFValue TensorBuiltin) where
+instance IsConstant (Value TensorBuiltin) where
   isZero = \case
     -- This is only semi-decidable, probably need to think harder about what
     -- to do here.
@@ -189,18 +189,18 @@ extractDomainFromConstraints VariableInfo{..} constraints = do
 
 extractVarBounds ::
   (MonadCompile m) =>
-  ([TensorElementInequality], [(UserElementVariable, Bounds UserElementVariable (WHNFValue TensorBuiltin))]) ->
+  ([TensorElementInequality], [(UserElementVariable, Bounds UserElementVariable (Value TensorBuiltin))]) ->
   UserElementVariable ->
-  m ([TensorElementInequality], [(UserElementVariable, Bounds UserElementVariable (WHNFValue TensorBuiltin))])
+  m ([TensorElementInequality], [(UserElementVariable, Bounds UserElementVariable (Value TensorBuiltin))])
 extractVarBounds (currentConstraints, solutions) var = do
   (bounds, newInequalities) <- fourierMotzkinElimination var currentConstraints
   return (newInequalities, (var, bounds) : solutions)
 
 convertBoundToExpr ::
   Map UserElementVariable Lv ->
-  (WHNFValue TensorBuiltin -> WHNFValue TensorBuiltin -> WHNFValue TensorBuiltin) ->
-  NonEmpty (Bound UserElementVariable (WHNFValue TensorBuiltin)) ->
-  WHNFValue TensorBuiltin
+  (Value TensorBuiltin -> Value TensorBuiltin -> Value TensorBuiltin) ->
+  NonEmpty (Bound UserElementVariable (Value TensorBuiltin)) ->
+  Value TensorBuiltin
 convertBoundToExpr varMap op bounds = foldr1 _ (fmap convertBound bounds)
   where
     -- Ignore strictness for the moment.
@@ -214,7 +214,7 @@ convertBoundToExpr varMap op bounds = foldr1 _ (fmap convertBound bounds)
 --------------------------------------------------------------------------------
 -- Constraint search
 
-findConstraints :: (MonadSearch m) => WHNFValue TensorBuiltin -> m ConstrainedValue
+findConstraints :: (MonadSearch m) => Value TensorBuiltin -> m ConstrainedValue
 findConstraints expr = case toBoolTensorView expr of
   -------------------------
   -- Unuseful base cases --
@@ -246,15 +246,15 @@ findConstraints expr = case toBoolTensorView expr of
 
 handleNot ::
   forall m . (MonadSearch m) =>
-  WHNFValue TensorBuiltin ->
+  Value TensorBuiltin ->
   m ConstrainedValue
 handleNot expr = do
   loweredExpr <- lowerBoolTensor expr
   case loweredExpr of
     INot {} -> return $ unconstrained expr
     newExpr -> updateConstrainedValue expr <$> findConstraints newExpr
   where
-    lowerBoolTensor :: WHNFValue TensorBuiltin -> m (WHNFValue TensorBuiltin)
+    lowerBoolTensor :: Value TensorBuiltin -> m (Value TensorBuiltin)
     lowerBoolTensor e = fromBoolTensorView <$> case toBoolTensorView e of
       ----------------
       -- Base cases --
@@ -278,15 +278,15 @@ handleNot expr = do
       VReduceAndTensor {} -> return $ VNotTensor e
       VReduceOrTensor {} -> return $ VNotTensor e
 
-    lowerBool :: WHNFValue TensorBuiltin -> m (WHNFValue TensorBuiltin)
+    lowerBool :: Value TensorBuiltin -> m (Value TensorBuiltin)
     lowerBool = \case
       INullaryBoolTensorOp (BoolLiteral b) -> return $ INullaryBoolTensorOp (BoolLiteral b)
       e -> developerError $ "Unexpected expression of type Bool:" <+> prettyVerbose e
 
 unfoldEquality ::
-  WHNFValue TensorBuiltin ->
-  WHNFValue TensorBuiltin ->
-  WHNFValue TensorBuiltin
+  Value TensorBuiltin ->
+  Value TensorBuiltin ->
+  Value TensorBuiltin
 unfoldEquality x y = IAnd (IOrderRat Le x y) (IOrderRat Ge x y)
 
 --------------------------------------------------------------------------------
@@ -299,8 +299,8 @@ unfoldEquality x y = IAnd (IOrderRat Le x y) (IOrderRat Ge x y)
 handleRatInequality ::
   (MonadSearch m) =>
   OrderOp ->
-  WHNFValue TensorBuiltin ->
-  WHNFValue TensorBuiltin ->
+  Value TensorBuiltin ->
+  Value TensorBuiltin ->
   m ConstrainedValue
 handleRatInequality op e1 e2 = do
   result <- compileRatLinearRelation (mkInequality op) e1 e2
@@ -321,25 +321,25 @@ handleRatInequality op e1 e2 = do
 compileRatLinearRelation ::
   (MonadLogger m, MonadReader VariableInfo m) =>
   (LinearExp -> LinearExp -> relation) ->
-  WHNFValue TensorBuiltin ->
-  WHNFValue TensorBuiltin ->
-  m (Either (WHNFValue TensorBuiltin) relation)
+  Value TensorBuiltin ->
+  Value TensorBuiltin ->
+  m (Either (Value TensorBuiltin) relation)
 compileRatLinearRelation mkRelation x y = do
   runExceptT $ do
     x' <- compileRatLinearExpr x
     y' <- compileRatLinearExpr y
     return $ mkRelation x' y'
 
-type LinearExp = LinearExpr UserElementVariable (WHNFValue TensorBuiltin)
+type LinearExp = LinearExpr UserElementVariable (Value TensorBuiltin)
 
 compileRatLinearExpr ::
   forall m.
-  (MonadLogger m, MonadReader VariableInfo m, MonadError (WHNFValue TensorBuiltin) m) =>
-  WHNFValue TensorBuiltin ->
+  (MonadLogger m, MonadReader VariableInfo m, MonadError (Value TensorBuiltin) m) =>
+  Value TensorBuiltin ->
   m LinearExp
 compileRatLinearExpr = go
   where
-    go :: WHNFValue TensorBuiltin -> m LinearExp
+    go :: Value TensorBuiltin -> m LinearExp
     go expr = case toRatTensorView expr of
       ----------------
       -- Base cases --

vehicle/src/Vehicle/Backend/LossFunction/JSON.hs

@@ -154,17 +154,17 @@ convertDecl = \case
     expr' <- convertExpr mempty body
     return $ JDecl (nameOf ident) typ' expr'
 
-convertExpr :: (MonadJSON m) => WHNFBoundEnv LossTensorBuiltin -> Expr LossTensorBuiltin -> m JExpr
+convertExpr :: (MonadJSON m) => BoundEnv LossTensorBuiltin -> Expr LossTensorBuiltin -> m JExpr
 convertExpr env body = convertValue =<< eval mempty env body
 
-convertValue :: (MonadJSON m) => WHNFValue LossTensorBuiltin -> m JExpr
+convertValue :: (MonadJSON m) => Value LossTensorBuiltin -> m JExpr
 convertValue expr = do
   showEntry expr
   result <- case expr of
     VMeta {} -> resolutionError currentPass "VMeta"
     VFreeVar {} -> resolutionError currentPass "VFreeVar"
     VUniverse {} -> resolutionError currentPass "Universe"
-    VLam binder (WHNFClosure env body) -> do
+    VLam binder (Closure env body) -> do
       let name = getBinderName binder
       typ' <- convertValue (typeOf binder)
       lv <- getBinderDepth
@@ -183,7 +183,7 @@ convertValue expr = do
   showExit result
   return result
 
-convertBuiltin :: (MonadJSON m) => LossTensorBuiltin -> [WHNFValue LossTensorBuiltin] -> m JExpr
+convertBuiltin :: (MonadJSON m) => LossTensorBuiltin -> [Value LossTensorBuiltin] -> m JExpr
 convertBuiltin b spine = case b of
   LossTensorRat op -> case op of
     L.RatTensor t -> convertNullaryOp b (RatTensor $ mapTensor toRat t) spine
@@ -216,42 +216,42 @@ convertBuiltin b spine = case b of
     L.DimensionIndexType -> convertIndexType spine
     L.TensorType -> convertTensorType spine
 
-convertNullaryOp :: (MonadJSON m) => LossTensorBuiltin -> JExpr -> [WHNFValue LossTensorBuiltin] -> m JExpr
+convertNullaryOp :: (MonadJSON m) => LossTensorBuiltin -> JExpr -> [Value LossTensorBuiltin] -> m JExpr
 convertNullaryOp b fn = \case
   [] -> return fn
   spine -> arityError b 0 spine
 
-convertUnaryOp :: (MonadJSON m) => LossTensorBuiltin -> (JExpr -> JExpr) -> [WHNFValue LossTensorBuiltin] -> m JExpr
+convertUnaryOp :: (MonadJSON m) => LossTensorBuiltin -> (JExpr -> JExpr) -> [Value LossTensorBuiltin] -> m JExpr
 convertUnaryOp b fn = \case
   [x] -> fn <$> convertValue x
   spine -> arityError b 1 spine
 
-convertBinaryOp :: (MonadJSON m) => LossTensorBuiltin -> (JExpr -> JExpr -> JExpr) -> [WHNFValue LossTensorBuiltin] -> m JExpr
+convertBinaryOp :: (MonadJSON m) => LossTensorBuiltin -> (JExpr -> JExpr -> JExpr) -> [Value LossTensorBuiltin] -> m JExpr
 convertBinaryOp b fn = \case
   [x, y] -> fn <$> convertValue x <*> convertValue y
   spine -> arityError b 2 spine
 
-convertNaryOp :: (MonadJSON m) => LossTensorBuiltin -> Int -> ([JExpr] -> JExpr) -> [WHNFValue LossTensorBuiltin] -> m JExpr
+convertNaryOp :: (MonadJSON m) => LossTensorBuiltin -> Int -> ([JExpr] -> JExpr) -> [Value LossTensorBuiltin] -> m JExpr
 convertNaryOp b n fn spine
   | length spine == n = fn <$> traverse convertValue spine
   | otherwise = arityError b n spine
 
-convertTensorType :: (MonadJSON m) => [WHNFValue LossTensorBuiltin] -> m JExpr
+convertTensorType :: (MonadJSON m) => [Value LossTensorBuiltin] -> m JExpr
 convertTensorType = \case
   [tElem, _dims] -> TensorType <$> convertValue tElem
   spine -> arityError (LossTensorDimType L.TensorType) 2 spine
 
-convertIndexType :: (MonadJSON m) => [WHNFValue LossTensorBuiltin] -> m JExpr
+convertIndexType :: (MonadJSON m) => [Value LossTensorBuiltin] -> m JExpr
 convertIndexType = \case
   [_dim] -> return DimensionIndexType
   spine -> arityError (LossTensorDimType L.DimensionIndexType) 1 spine
 
-convertSearch :: (MonadJSON m) => [WHNFValue LossTensorBuiltin] -> m JExpr
+convertSearch :: (MonadJSON m) => [Value LossTensorBuiltin] -> m JExpr
 convertSearch = \case
   [unaryOp, lowerBound, upperBound, fn] -> SearchRatTensor <$> convertValue unaryOp <*> convertValue lowerBound <*> convertValue upperBound <*> convertValue fn
   spine -> arityError (show L.SearchRatTensor) 5 spine
 
-arityError :: (MonadCompile m, Pretty fn) => fn -> Arity -> [WHNFValue LossTensorBuiltin] -> m a
+arityError :: (MonadCompile m, Pretty fn) => fn -> Arity -> [Value LossTensorBuiltin] -> m a
 arityError fun arity explicitArgs =
   compilerDeveloperError $
     "Number of args is different from expected arity:"
@@ -271,7 +271,7 @@ arityError fun arity explicitArgs =
             <+> prettyVerbose explicitArgs
         )
 
-showEntry :: (MonadJSON m) => WHNFValue LossTensorBuiltin -> m ()
+showEntry :: (MonadJSON m) => Value LossTensorBuiltin -> m ()
 showEntry e = do
   logDebug MaxDetail $ "json-enter:" <+> prettyVerbose e
   incrCallDepth