Skip to content

Commit

Permalink
Merge pull request #279 from GaloisInc/vr/label-lenses
Browse files Browse the repository at this point in the history
switch to labels for other lenses
  • Loading branch information
Ptival authored Aug 11, 2023
2 parents 0b4106d + 29b7d9f commit e5eadc7
Show file tree
Hide file tree
Showing 4 changed files with 48 additions and 47 deletions.
13 changes: 7 additions & 6 deletions src/Reopt/TypeInference/Solver/Finalise.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE OverloadedStrings #-}

module Reopt.TypeInference.Solver.Finalise (
Expand All @@ -8,7 +9,7 @@ module Reopt.TypeInference.Solver.Finalise (
import Control.Lens (over, _3)
import Control.Monad.State (gets)
import Data.Either (lefts, partitionEithers)
import Data.Generics.Product (field)
import Data.Generics.Labels ()
import Data.Graph (SCC (..), flattenSCCs)
import Data.Graph.SCC (stronglyConnCompR)
import Data.Map.Strict (Map)
Expand Down Expand Up @@ -91,7 +92,7 @@ finalizeTypeDefs' ::
UM.UnionFindMap RowVar ki (FieldMap TyVar) ->
ConstraintSolution
finalizeTypeDefs' um@(UM.UnionFindMap teqvs tdefs) (UM.UnionFindMap _reqvs rdefs) =
over (field @"csTyVars") (Map.union eqvRes) preSoln
over #csTyVars (Map.union eqvRes) preSoln
where
-- Include equivalences.
eqvRes = Map.fromSet mkOneEqv (Map.keysSet teqvs)
Expand Down Expand Up @@ -144,7 +145,7 @@ finaliseTyF ::
ConstraintSolution ->
ConstraintSolution
finaliseTyF (ty, tv, _) r =
over (field @"csTyVars") (Map.insert tv (norm ty)) r
over #csTyVars (Map.insert tv (norm ty)) r
where
norm = \case
PtrTy rv -> FTy (PtrTy (Map.findWithDefault (StructTy emptyFieldMap) rv (csRowVars r)))
Expand All @@ -159,7 +160,7 @@ finaliseFieldMap ::
ConstraintSolution ->
ConstraintSolution
finaliseFieldMap (fm, rv, _) r =
over (field @"csRowVars") (Map.insert rv (StructTy (norm <$> fm))) r
over #csRowVars (Map.insert rv (StructTy (norm <$> fm))) r
where
norm t = Map.findWithDefault UnknownTy t (csTyVars r)

Expand All @@ -179,7 +180,7 @@ finaliseCyclic cs s
-- [ PP.pretty n PP.<+> "=" PP.<+> PP.pretty ty
-- | (ty, n, _) <- cs
-- ])) $
over (field @"csNamedStructs") (namedDefs ++) sWithTys
over #csNamedStructs (namedDefs ++) sWithTys
where
namedDefs =
[ (rowVarToStructName rv, StructTy $ resolveOne <$> fm)
Expand All @@ -190,7 +191,7 @@ finaliseCyclic cs s
-- them.
sWithTys = foldl (flip finaliseTyF) sWithNamed tys'

sWithNamed = over (field @"csRowVars") (Map.union named) s
sWithNamed = over #csRowVars (Map.union named) s

named =
Map.fromList
Expand Down
54 changes: 26 additions & 28 deletions src/Reopt/TypeInference/Solver/Monad.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE OverloadedStrings #-}

module Reopt.TypeInference.Solver.Monad (
Expand Down Expand Up @@ -42,10 +43,10 @@ module Reopt.TypeInference.Solver.Monad (
withFresh,
) where

import Control.Lens (Lens', use, (%%=), (%=), (.=), (<<+=))
import Control.Lens (Lens', use, (%%=), (%=), (<<+=))
import Control.Monad.State (MonadState, State, evalState)
import Data.Foldable (asum)
import Data.Generics.Product (field)
import Data.Generics.Labels ()
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import GHC.Generics (Generic)
Expand Down Expand Up @@ -133,7 +134,7 @@ runSolverM b o w = flip evalState (emptyContext w b o) . getSolverM
-- Adding constraints

addEqC :: EqC -> SolverM ()
addEqC eqc = field @"ctxEqCs" %= (eqc :)
addEqC eqc = #ctxEqCs %= (eqc :)

addTyVarEq :: ConstraintProvenance -> TyVar -> ITy -> SolverM ()
addTyVarEq prov tv1 tv2 = addEqC (EqC tv1 tv2 prov)
Expand All @@ -142,20 +143,20 @@ addTyVarEq' :: ConstraintProvenance -> TyVar -> TyVar -> SolverM ()
addTyVarEq' prov tv1 tv2 = addTyVarEq prov tv1 (VarTy tv2)

addEqRowC :: EqRowC -> SolverM ()
addEqRowC eqc = field @"ctxEqRowCs" %= (eqc :)
addEqRowC eqc = #ctxEqRowCs %= (eqc :)

addRowExprEq :: RowExpr -> RowExpr -> SolverM ()
addRowExprEq r1 r2 = addEqRowC (EqRowC r1 r2)

addCondEq :: Conditional' -> SolverM ()
addCondEq cs =
field @"ctxCondEqs" %= (cs :)
#ctxCondEqs %= (cs :)

addSubType :: TyVar -> TyVar -> SolverM ()
addSubType a b = field @"ctxSubTypeCs" %= ((a :<: b) :)
addSubType a b = #ctxSubTypeCs %= ((a :<: b) :)

addSubRow :: RowExpr -> RowExpr -> SolverM ()
addSubRow a b = field @"ctxSubRowCs" %= ((a :<: b) :)
addSubRow a b = #ctxSubRowCs %= ((a :<: b) :)

--------------------------------------------------------------------------------
-- Getting constraints
Expand All @@ -167,19 +168,19 @@ popField fld =
(c : cs) -> (Just c, cs)

_dequeueEqC :: SolverM (Maybe EqC)
_dequeueEqC = popField (field @"ctxEqCs")
_dequeueEqC = popField #ctxEqCs

_dequeueEqRowC :: SolverM (Maybe EqRowC)
_dequeueEqRowC = popField (field @"ctxEqRowCs")
_dequeueEqRowC = popField #ctxEqRowCs

_dequeueSubTypeC :: SolverM (Maybe SubTypeC)
_dequeueSubTypeC = popField (field @"ctxSubTypeCs")
_dequeueSubTypeC = popField #ctxSubTypeCs

--------------------------------------------------------------------------------
-- Operations over type variable state

freshRowVar :: SolverM RowVar
freshRowVar = RowVar <$> (field @"nextRowVar" <<+= 1)
freshRowVar = RowVar <$> (#nextRowVar <<+= 1)

_freshRowVarE :: RowExpr -> SolverM RowVar
_freshRowVarE e = do
Expand All @@ -197,20 +198,20 @@ freshRowVarFM fm = do
-- for @leaf@. Note that both root and leaf should be the reps. of
-- their corresponding equivalence classes.
unsafeUnifyRowVars :: RowExpr -> RowVar -> SolverM ()
unsafeUnifyRowVars root leaf = field @"ctxRowVars" %= UM.unify ki leaf
unsafeUnifyRowVars root leaf = #ctxRowVars %= UM.unify ki leaf
where
ki = RowInfo{riShift = rowExprShift root, riRowVar = rowExprVar root}

-- | Always define a row variable, even if it has a def.
defineRowVar :: RowVar -> FieldMap TyVar -> SolverM ()
defineRowVar rowv fm = field @"ctxRowVars" %= UM.insert rowv fm
defineRowVar rowv fm = #ctxRowVars %= UM.insert rowv fm

undefineRowVar :: RowVar -> SolverM ()
undefineRowVar rv = field @"ctxRowVars" %= UM.delete rv
undefineRowVar rv = #ctxRowVars %= UM.delete rv

lookupRowVarRep :: RowVar -> SolverM (Offset, RowVar)
lookupRowVarRep rv = do
ri <- field @"ctxRowVars" %%= UM.lookupRep rv
ri <- #ctxRowVars %%= UM.lookupRep rv
pure (riShift ri, riRowVar ri)

lookupRowExprRep :: RowExpr -> SolverM RowExpr
Expand All @@ -221,7 +222,7 @@ lookupRowExprRep re = do

lookupRowVar :: RowVar -> SolverM (Offset, RowVar, Maybe (FieldMap TyVar))
lookupRowVar rv = do
(ri, fm) <- field @"ctxRowVars" %%= UM.lookup rv
(ri, fm) <- #ctxRowVars %%= UM.lookup rv
pure (riShift ri, riRowVar ri, fm)

lookupRowExpr :: RowExpr -> SolverM (RowExpr, Maybe (FieldMap TyVar))
Expand All @@ -234,17 +235,17 @@ lookupRowExpr re = do
-- corresponding equivalence class. This also updates the eqv. map to
-- amortise lookups.
lookupTyVarRep :: TyVar -> SolverM TyVar
lookupTyVarRep tv0 = field @"ctxTyVars" %%= UM.lookupRep tv0
lookupTyVarRep tv0 = #ctxTyVars %%= UM.lookupRep tv0

-- | Lookup a type variable, returns the representative of the
-- corresponding equivalence class, and the definition for that type
-- var, if any.
lookupTyVar :: TyVar -> SolverM (TyVar, Maybe ITy')
lookupTyVar tv = field @"ctxTyVars" %%= UM.lookup tv
lookupTyVar tv = #ctxTyVars %%= UM.lookup tv

-- | Always return a new type variable.
freshTyVar' :: Maybe String -> SolverM TyVar
freshTyVar' orig = flip TyVar orig <$> (field @"nextTyVar" <<+= 1)
freshTyVar' orig = flip TyVar orig <$> (#nextTyVar <<+= 1)

freshTyVar :: Maybe String -> Maybe ITy -> SolverM TyVar
freshTyVar orig Nothing = freshTyVar' orig
Expand All @@ -256,31 +257,28 @@ freshTyVar orig (Just (ITy ty)) = do

-- | Always define a type variable, even if it has a def.
defineTyVar :: TyVar -> ITy' -> SolverM ()
defineTyVar tyv ty = field @"ctxTyVars" %= UM.insert tyv ty
defineTyVar tyv ty = #ctxTyVars %= UM.insert tyv ty

undefineTyVar :: TyVar -> SolverM ()
undefineTyVar ty = field @"ctxTyVars" %= UM.delete ty
undefineTyVar ty = #ctxTyVars %= UM.delete ty

-- | @unsafeUnifyTyVars root leaf@ will make @root@ the new equiv. rep
-- for @leaf@. Note that both root and leaf should be the reps. of
-- their corresponding equivalence classes.
unsafeUnifyTyVars :: TyVar -> TyVar -> SolverM ()
unsafeUnifyTyVars root leaf = field @"ctxTyVars" %= UM.unify root leaf
unsafeUnifyTyVars root leaf = #ctxTyVars %= UM.unify root leaf

--------------------------------------------------------------------------------
-- Other stuff

ptrWidthNumTy :: SolverM ITy'
ptrWidthNumTy = NumTy <$> use (field @"ptrWidth")

_setTraceUnification :: Bool -> SolverM ()
_setTraceUnification b = field @"ctxTraceUnification" .= b
ptrWidthNumTy = NumTy <$> use #ptrWidth

traceUnification :: SolverM Bool
traceUnification = use (field @"ctxTraceUnification")
traceUnification = use #ctxTraceUnification

traceConstraintOrigins :: SolverM Bool
traceConstraintOrigins = use (field @"ctxTraceConstraintOrigins")
traceConstraintOrigins = use #ctxTraceConstraintOrigins

--------------------------------------------------------------------------------
-- Conditional constraints
Expand Down
17 changes: 9 additions & 8 deletions src/Reopt/TypeInference/Solver/Solver.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE OverloadedStrings #-}

module Reopt.TypeInference.Solver.Solver (
Expand All @@ -19,7 +20,7 @@ import Control.Monad.State (MonadState (get), StateT, evalStateT, put)
import Data.Bifunctor (Bifunctor (second), first)
import Data.Foldable (traverse_)
import Data.Functor (($>))
import Data.Generics.Product (field)
import Data.Generics.Labels ()
import Data.Map.Strict qualified as Map
import Data.Maybe (fromMaybe, isNothing)
import Data.Set qualified as Set
Expand Down Expand Up @@ -96,7 +97,7 @@ unifyConstraints = do
-- | @traceContext description ctx ctx'@ reports how the context changed via @trace@.
traceContext :: PP.Doc () -> SolverM a -> SolverM a
traceContext description action = do
tId <- field @"nextTraceId" <<+= 1
tId <- #nextTraceId <<+= 1
doTraceUnification <- traceUnification
doTraceConstraintOrigins <- traceConstraintOrigins

Expand Down Expand Up @@ -252,12 +253,12 @@ solverLoop = evalStateT go =<< get
when keepGoing go

solvers =
[ solveHeadReset (field @"ctxEqCs") solveEqC
, solveHead (field @"ctxEqRowCs") solveEqRowC
, solveFirst (field @"ctxCondEqs") solveConditional
, solveFirst (field @"ctxSubTypeCs") solveSubTypeC
, preprocess (field @"ctxSubRowCs") resolveCycles
, solveFirst (field @"ctxSubRowCs") solveSubRowC
[ solveHeadReset #ctxEqCs solveEqC
, solveHead #ctxEqRowCs solveEqRowC
, solveFirst #ctxCondEqs solveConditional
, solveFirst #ctxSubTypeCs solveSubTypeC
, preprocess #ctxSubRowCs resolveCycles
, solveFirst #ctxSubRowCs solveSubRowC
]

--------------------------------------------------------------------------------
Expand Down
11 changes: 6 additions & 5 deletions src/Reopt/TypeInference/Solver/UnionFindMap.hs
Original file line number Diff line number Diff line change
@@ -1,9 +1,10 @@
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE OverloadedStrings #-}

module Reopt.TypeInference.Solver.UnionFindMap where

import Control.Lens (at, (%%~), (%~), (?~))
import Data.Generics.Product (field)
import Data.Generics.Labels ()
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import GHC.Generics (Generic)
Expand All @@ -28,7 +29,7 @@ empty :: UFMKeyInfo k ki => UnionFindMap k ki v
empty = UnionFindMap mempty mempty

lookupRep :: UFMKeyInfo k ki => k -> UnionFindMap k ki v -> (ki, UnionFindMap k ki v)
lookupRep k0 = field @"ufmEqv" %%~ go k0
lookupRep k0 = #ufmEqv %%~ go k0
where
go k m =
case Map.lookup k m of
Expand All @@ -47,18 +48,18 @@ lookup k m = ((ki', Map.lookup (projectKey ki') (ufmDefs m)), m')
(ki', m') = lookupRep k m

insert :: UFMKeyInfo k ki => k -> v -> UnionFindMap k ki v -> UnionFindMap k ki v
insert k v = field @"ufmDefs" . at k ?~ v
insert k v = #ufmDefs . at k ?~ v

-- | @delete k m@ forgets any definition for @k@, without touching any
-- equivalences.
delete :: UFMKeyInfo k ki => k -> UnionFindMap k ki v -> UnionFindMap k ki v
delete k = field @"ufmDefs" %~ Map.delete k
delete k = #ufmDefs %~ Map.delete k

-- | @unify root leaf@ will make @root@ the new equiv. rep
-- for @leaf@. Note that both root and leaf should be the reps. of
-- their corresponding equivalence classes, and that only @root@ is allowed a definition.
unify :: UFMKeyInfo k ki => ki -> k -> UnionFindMap k ki v -> UnionFindMap k ki v
unify root leaf = field @"ufmEqv" %~ Map.insert leaf root
unify root leaf = #ufmEqv %~ Map.insert leaf root

-- | Map the representative element onto the class.
eqvClasses :: UFMKeyInfo k ki => UnionFindMap k ki v -> Map k [ki]
Expand Down

0 comments on commit e5eadc7

Please sign in to comment.