From 02bc09794f012dcdf4cf618210f83577392c46e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 27 Sep 2024 20:13:19 +0000 Subject: [PATCH] Parameterize Reft with the variable type --- .../Fixpoint/Solver/EnvironmentReduction.hs | 6 +- src/Language/Fixpoint/Solver/Interpreter.hs | 1 + src/Language/Fixpoint/Solver/Prettify.hs | 2 +- src/Language/Fixpoint/Types/Refinements.hs | 74 +++++++++++-------- src/Language/Fixpoint/Types/Templates.hs | 3 +- tests/tasty/Arbitrary.hs | 1 + tests/tasty/InterpretTests.hs | 2 +- tests/tasty/SimplifyTests.hs | 2 +- 8 files changed, 54 insertions(+), 37 deletions(-) diff --git a/src/Language/Fixpoint/Solver/EnvironmentReduction.hs b/src/Language/Fixpoint/Solver/EnvironmentReduction.hs index ebf38d053..7d08637c6 100644 --- a/src/Language/Fixpoint/Solver/EnvironmentReduction.hs +++ b/src/Language/Fixpoint/Solver/EnvironmentReduction.hs @@ -71,10 +71,12 @@ import Language.Fixpoint.Types.Names import Language.Fixpoint.Types.PrettyPrint import Language.Fixpoint.Types.Refinements ( Brel(..) - , Expr(..) + , ExprV(..) + , Expr , KVar(..) , SortedReft(..) - , Subst(..) + , Subst + , SubstV(..) , pattern PTrue , pattern PFalse , dropECst diff --git a/src/Language/Fixpoint/Solver/Interpreter.hs b/src/Language/Fixpoint/Solver/Interpreter.hs index 230ed7a95..b1ffdbb0c 100644 --- a/src/Language/Fixpoint/Solver/Interpreter.hs +++ b/src/Language/Fixpoint/Solver/Interpreter.hs @@ -12,6 +12,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RecordWildCards #-} diff --git a/src/Language/Fixpoint/Solver/Prettify.hs b/src/Language/Fixpoint/Solver/Prettify.hs index 74ba773f4..bd6109e8c 100644 --- a/src/Language/Fixpoint/Solver/Prettify.hs +++ b/src/Language/Fixpoint/Solver/Prettify.hs @@ -38,7 +38,7 @@ import Language.Fixpoint.Types.Names ) import Language.Fixpoint.Types.PrettyPrint import Language.Fixpoint.Types.Refinements - ( Expr(..) + ( ExprV(..) , pattern PFalse , Reft , SortedReft(..) diff --git a/src/Language/Fixpoint/Types/Refinements.hs b/src/Language/Fixpoint/Types/Refinements.hs index a58464a49..012d9b2ef 100644 --- a/src/Language/Fixpoint/Types/Refinements.hs +++ b/src/Language/Fixpoint/Types/Refinements.hs @@ -25,15 +25,18 @@ module Language.Fixpoint.Types.Refinements ( , Constant (..) , Bop (..) , Brel (..) - , Expr (..), Pred + , ExprV (..), Pred + , Expr , GradInfo (..) , pattern PTrue, pattern PTop, pattern PFalse, pattern EBot , pattern ETimes, pattern ERTimes, pattern EDiv, pattern ERDiv , pattern EEq , KVar (..) - , Subst (..) + , Subst + , SubstV (..) , KVSub (..) - , Reft (..) + , Reft + , ReftV (..) , SortedReft (..) -- * Constructing Terms @@ -148,7 +151,7 @@ instance NFData Constant instance NFData SymConst instance NFData Brel instance NFData Bop -instance NFData Expr +instance NFData v => NFData (ExprV v) instance NFData Reft instance NFData SortedReft @@ -181,7 +184,7 @@ instance (Hashable k, Eq k, B.Binary k, B.Binary v) => B.Binary (M.HashMap k v) get = M.fromList <$> B.get instance B.Binary Subst -instance B.Binary Expr +instance B.Binary v => B.Binary (ExprV v) instance B.Binary Reft @@ -257,14 +260,18 @@ instance Hashable SymConst instance Hashable Constant instance Hashable GradInfo instance Hashable Subst -instance Hashable Expr +instance Hashable v => Hashable (ExprV v) instance Hashable Reft -------------------------------------------------------------------------------- -- | Substitutions ------------------------------------------------------------- -------------------------------------------------------------------------------- -newtype Subst = Su (M.HashMap Symbol Expr) - deriving (Eq, Data, Ord, Typeable, Generic, ToJSON, FromJSON) +type Subst = SubstV Symbol +newtype SubstV v = Su (M.HashMap Symbol (ExprV v)) + deriving (Eq, Data, Ord, Typeable, Generic) + +instance ToJSON Subst +instance FromJSON Subst instance Show Subst where show = showFix @@ -319,28 +326,31 @@ instance FromJSON Bop where instance FromJSON Expr where -data Expr = ESym !SymConst +type Expr = ExprV Symbol + +data ExprV v + = ESym !SymConst | ECon !Constant - | EVar !Symbol - | EApp !Expr !Expr - | ENeg !Expr - | EBin !Bop !Expr !Expr - | EIte !Expr !Expr !Expr - | ECst !Expr !Sort - | ELam !(Symbol, Sort) !Expr - | ETApp !Expr !Sort - | ETAbs !Expr !Symbol - | PAnd ![Expr] - | POr ![Expr] - | PNot !Expr - | PImp !Expr !Expr - | PIff !Expr !Expr - | PAtom !Brel !Expr !Expr + | EVar !v + | EApp !(ExprV v) !(ExprV v) + | ENeg !(ExprV v) + | EBin !Bop !(ExprV v) !(ExprV v) + | EIte !(ExprV v) !(ExprV v) !(ExprV v) + | ECst !(ExprV v) !Sort + | ELam !(Symbol, Sort) !(ExprV v) + | ETApp !(ExprV v) !Sort + | ETAbs !(ExprV v) !Symbol + | PAnd ![ExprV v] + | POr ![ExprV v] + | PNot !(ExprV v) + | PImp !(ExprV v) !(ExprV v) + | PIff !(ExprV v) !(ExprV v) + | PAtom !Brel !(ExprV v) !(ExprV v) | PKVar !KVar !Subst - | PAll ![(Symbol, Sort)] !Expr - | PExist ![(Symbol, Sort)] !Expr - | PGrad !KVar !Subst !GradInfo !Expr - | ECoerc !Sort !Sort !Expr + | PAll ![(Symbol, Sort)] !(ExprV v) + | PExist ![(Symbol, Sort)] !(ExprV v) + | PGrad !KVar !Subst !GradInfo !(ExprV v) + | ECoerc !Sort !Sort !(ExprV v) deriving (Eq, Show, Ord, Data, Typeable, Generic) onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr @@ -511,9 +521,11 @@ debruijnIndex = go go (PGrad _ _ _ e) = go e go (ECoerc _ _ e) = go e --- | Parsed refinement of @Symbol@ as @Expr@ --- e.g. in '{v: _ | e }' v is the @Symbol@ and e the @Expr@ -newtype Reft = Reft (Symbol, Expr) +type Reft = ReftV Symbol + +-- | Refinement of @v@ satisfying a predicate +-- e.g. in '{x: _ | e }' x is the @Symbol@ and e the @ExprV v@ +newtype ReftV v = Reft (Symbol, ExprV v) deriving (Eq, Ord, Data, Typeable, Generic) data SortedReft = RR { sr_sort :: !Sort, sr_reft :: !Reft } diff --git a/src/Language/Fixpoint/Types/Templates.hs b/src/Language/Fixpoint/Types/Templates.hs index e11365b67..5220a55aa 100644 --- a/src/Language/Fixpoint/Types/Templates.hs +++ b/src/Language/Fixpoint/Types/Templates.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE FlexibleInstances #-} module Language.Fixpoint.Types.Templates ( anything, Templates, makeTemplates, @@ -103,4 +104,4 @@ instance Monoid Templates where mempty = TExprs [] instance PPrint Templates where - pprintTidy _ = text . show \ No newline at end of file + pprintTidy _ = text . show diff --git a/tests/tasty/Arbitrary.hs b/tests/tasty/Arbitrary.hs index 619f7e27a..6d359750f 100644 --- a/tests/tasty/Arbitrary.hs +++ b/tests/tasty/Arbitrary.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TupleSections #-} {-# OPTIONS_GHC -Wno-orphans #-} diff --git a/tests/tasty/InterpretTests.hs b/tests/tasty/InterpretTests.hs index 9e9f82c7d..2ce865740 100644 --- a/tests/tasty/InterpretTests.hs +++ b/tests/tasty/InterpretTests.hs @@ -1,7 +1,7 @@ module InterpretTests (tests) where import Arbitrary () -import Language.Fixpoint.Types.Refinements (Expr (..)) +import Language.Fixpoint.Types.Refinements (Expr) import qualified SimplifyInterpreter import Test.Tasty ( TestTree, diff --git a/tests/tasty/SimplifyTests.hs b/tests/tasty/SimplifyTests.hs index 6d31ac0b3..e6be2857a 100644 --- a/tests/tasty/SimplifyTests.hs +++ b/tests/tasty/SimplifyTests.hs @@ -1,7 +1,7 @@ module SimplifyTests (tests) where import Arbitrary (subexprs) -import Language.Fixpoint.Types.Refinements (Bop (Minus), Constant (I), Expr (..)) +import Language.Fixpoint.Types.Refinements (Bop (Minus), Constant (I), Expr, ExprV (..)) import qualified SimplifyInterpreter import qualified SimplifyPLE import Test.Tasty