d57d60a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use a Set for universe constraints

commitd57d60a744246e4cccf874c8cb18304f8fac01e0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 21 Mar 2015, 20:27 (12 years ago) parente10c205

8 files changed+76−52

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6−3 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/Core/Binary.hs+17−2 src/Idris/Core/Constraints.hs+33−30 src/Idris/Core/Evaluate.hs+3−4 src/Idris/Core/TT.hs+10−8 src/Idris/IBC.hs+1−1 src/Idris/REPL.hs+4−2

src/Idris/AbsSyntax.hs+6−3

@@ -543,10 +543,13 @@ addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()

543543addConstraints fc (v, cs)

544544 = do i <- getIState

545545 let ctxt = tt_ctxt i

546− let ctxt' = ctxt { uconstraints = nub cs ++ uconstraints ctxt,

547− next_tvar = v }

548− let ics = zip cs (repeat fc) ++ idris_constraints i

546+ let ctxt' = ctxt { next_tvar = v }

547+ let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)

549548 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }

549+ where

550+ insertAll [] c = c

551+ insertAll ((c, fc) : cs) ics

552+ = insertAll cs $ S.insert (ConstraintFC c fc) ics

550553

551554addDeferred = addDeferred' Ref

552555addDeferredTyCon = addDeferred' (TCon 0 0)

src/Idris/AbsSyntaxTree.hs+2−2

@@ -157,7 +157,7 @@ data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines sh

157157-- | The global state used in the Idris monad

158158data IState = IState {

159159 tt_ctxt :: Context, -- ^ All the currently defined names and their terms

160− idris_constraints :: [(UConstraint, FC)],

160+ idris_constraints :: S.Set ConstraintFC,

161161 -- ^ A list of universe constraints and their corresponding source locations

162162 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators

163163 idris_implicits :: Ctxt [PArg],

@@ -309,7 +309,7 @@ data IBCWrite = IBCFix FixDecl

309309

310310-- | The initial state for the compiler

311311idrisInit :: IState

312−idrisInit = IState initContext [] []

312+idrisInit = IState initContext S.empty []

313313 emptyContext emptyContext emptyContext emptyContext

314314 emptyContext emptyContext emptyContext emptyContext

315315 emptyContext emptyContext emptyContext emptyContext

src/Idris/Core/Binary.hs+17−2

@@ -546,6 +546,21 @@ instance Binary NameType where

546546 return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))

547547 _ -> error "Corrupted binary data for NameType"

548548

549+-- record concrete levels only, for now

550+instance Binary UExp where

551+ put x = case x of

552+ UVar t -> do putWord8 0

553+ put ((-1) :: Int) -- TMP HACK!

554+ UVal t -> do putWord8 1

555+ put t

556+

557+ get = do i <- getWord8

558+ case i of

559+ 0 -> do x1 <- get

560+ return (UVar x1)

561+ 1 -> do x1 <- get

562+ return (UVal x1)

563+ _ -> error "Corrupted binary data for UExp"

549564

550565instance {- (Binary n) => -} Binary (TT Name) where

551566 put x

@@ -600,8 +615,8 @@ instance {- (Binary n) => -} Binary (TT Name) where

600615 x2 <- getWord8

601616 return (Proj x1 ((fromEnum x2)-1))

602617 6 -> return Erased

603− 7 -> do _x1 <- get :: Get UExp

604− return (TType (UVar (-1))) -- TODO: temp hack, make Edwin fix this!

618+ 7 -> do x1 <- get

619+ return (TType x1)

605620 8 -> return Impossible

606621 9 -> do x1 <- get

607622 return (V x1)

src/Idris/Core/Constraints.hs+33−30

@@ -1,72 +1,72 @@

11-- | Check universe constraints.

22module Idris.Core.Constraints ( ucheck ) where

4−import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..), Err'(..) )

4+import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..),

5+ ConstraintFC(..), Err'(..) )

67import Control.Applicative

78import Control.Monad.State.Strict

8−import Data.Function ( on )

9−import Data.List ( partition, nubBy )

9+import Data.List ( partition )

1010import qualified Data.Map.Strict as M

1111import qualified Data.Set as S

1212

1313

1414-- | Check that a list of universe constraints can be satisfied.

15−ucheck :: [(UConstraint, FC)] -> TC ()

16−ucheck = void . solve 10 . nubBy ((==) `on` fst) . filter (not . ignore)

15+ucheck :: S.Set ConstraintFC -> TC ()

16+ucheck = void . solve 10 . S.filter (not . ignore)

1717 where

1818 -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with

19− ignore (c,_) | any (== Var (-1)) (varsIn c) = True

20− ignore (ULE a b, _) = a == b

19+ ignore (ConstraintFC c _) | any (== Var (-1)) (varsIn c) = True

20+ ignore (ConstraintFC (ULE a b) _) = a == b

2121 ignore _ = False

2222

2323newtype Var = Var Int

2424 deriving (Eq, Ord, Show)

2525

26−data Domain = Domain {-# UNPACK #-} !Int

27− {-# UNPACK #-} !Int

26+data Domain = Domain Int Int

2827 deriving (Eq, Ord, Show)

2928

3029data SolverState =

3130 SolverState

3231 { queue :: Queue

3332 , domainStore :: M.Map Var ( Domain

34− , S.Set (UConstraint, FC) -- constraints that effected this variable

33+ , S.Set ConstraintFC -- constraints that effected this variable

3534 )

3635 }

3736

38−data Queue = Queue [(UConstraint, FC)] (S.Set UConstraint)

37+data Queue = Queue [ConstraintFC] (S.Set UConstraint)

3938

4039

41−solve :: Int -> [(UConstraint, FC)] -> TC (M.Map Var Int)

42−solve maxUniverseLevel inpConstraints =

40+solve :: Int -> S.Set ConstraintFC -> TC (M.Map Var Int)

41+solve maxUniverseLevel ucs =

4342 evalStateT (propagate >> extractSolution) initSolverState

4443

4544 where

45+ inpConstraints = S.toAscList ucs

4646

4747 -- | initial solver state.

4848 -- the queue contains all constraints, the domain store contains the initial domains.

4949 initSolverState :: SolverState

5050 initSolverState =

5151 let

52− (initUnaryQueue, initQueue) = partition (\ (c,_) -> length (varsIn c) == 1) inpConstraints

52+ (initUnaryQueue, initQueue) = partition (\ c -> length (varsIn (uconstraint c)) == 1) inpConstraints

5353 in

5454 SolverState

55− { queue = Queue (initUnaryQueue ++ initQueue) (S.fromList (map fst (initUnaryQueue ++ initQueue)))

55+ { queue = Queue (initUnaryQueue ++ initQueue) (S.fromList (map uconstraint (initUnaryQueue ++ initQueue)))

5656 , domainStore = M.fromList

5757 [ (v, (Domain 0 maxUniverseLevel, S.empty))

5858 | v <- ordNub [ v

59− | (c, _) <- inpConstraints

59+ | ConstraintFC c _ <- inpConstraints

6060 , v <- varsIn c

6161 ]

6262 ]

6363 }

6464

6565 -- | a map from variables to the list of constraints the variable occurs in.

66− constraints :: M.Map Var (S.Set (UConstraint, FC))

66+ constraints :: M.Map Var (S.Set ConstraintFC)

6767 constraints = M.fromListWith S.union

68− [ (v, S.singleton (c,fc))

69− | (c, fc) <- inpConstraints

68+ [ (v, S.singleton (ConstraintFC c fc))

69+ | ConstraintFC c fc <- inpConstraints

7070 , let vars = varsIn c

7171 , length vars > 1 -- do not register unary constraints

7272 , v <- vars

@@ -82,20 +82,20 @@ solve maxUniverseLevel inpConstraints =

8282 mcons <- nextConstraint

8383 case mcons of

8484 Nothing -> return ()

85− Just (cons, fc) -> do

85+ Just (ConstraintFC cons fc) -> do

8686 case cons of

8787 ULE a b -> do

8888 Domain lowerA upperA <- domainOf a

8989 Domain lowerB upperB <- domainOf b

90− when (upperB < upperA) $ updateDomainOf (cons, fc) a (Domain lowerA upperB)

91− when (lowerA > lowerB) $ updateDomainOf (cons, fc) b (Domain lowerA upperB)

90+ when (upperB < upperA) $ updateDomainOf (ConstraintFC cons fc) a (Domain lowerA upperB)

91+ when (lowerA > lowerB) $ updateDomainOf (ConstraintFC cons fc) b (Domain lowerA upperB)

9292 ULT a b -> do

9393 Domain lowerA upperA <- domainOf a

9494 Domain lowerB upperB <- domainOf b

9595 let upperB_pred = pred upperB

9696 let lowerA_succ = succ lowerA

97− when (upperB_pred < upperA) $ updateDomainOf (cons, fc) a (Domain lowerA upperB_pred)

98− when (lowerA_succ > lowerB) $ updateDomainOf (cons, fc) b (Domain lowerA_succ upperB)

97+ when (upperB_pred < upperA) $ updateDomainOf (ConstraintFC cons fc) a (Domain lowerA upperB_pred)

98+ when (lowerA_succ > lowerB) $ updateDomainOf (ConstraintFC cons fc) b (Domain lowerA_succ upperB)

9999 propagate

100100

101101 -- | extract a solution from the state.

@@ -106,13 +106,13 @@ solve maxUniverseLevel inpConstraints =

106106 extractValue (Domain x _) = x

107107

108108 -- | dequeue the first constraint.

109− nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))

109+ nextConstraint :: MonadState SolverState m => m (Maybe ConstraintFC)

110110 nextConstraint = do

111111 Queue list set <- gets queue

112112 case list of

113113 [] -> return Nothing

114114 (q:qs) -> do

115− modify $ \ st -> st { queue = Queue qs (S.delete (fst q) set) }

115+ modify $ \ st -> st { queue = Queue qs (S.delete (uconstraint q) set) }

116116 return (Just q)

117117

118118 -- | look up the domain of a variable from the state.

@@ -123,11 +123,11 @@ solve maxUniverseLevel inpConstraints =

123123

124124 -- | updates the domain of a variable.

125125 -- this function is also where we fail, inc ase of a domain wipe-out.

126− updateDomainOf :: (UConstraint, FC) -> UExp -> Domain -> StateT SolverState TC ()

126+ updateDomainOf :: ConstraintFC -> UExp -> Domain -> StateT SolverState TC ()

127127 updateDomainOf suspect (UVar var) newDom = do

128128 doms <- gets domainStore

129129 let (oldDom, suspects) = doms M.! Var var

130− when (wipeOut newDom) $ lift $ Error $ At (snd suspect) $ Msg $ unlines

130+ when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines

131131 $ "Universe inconsistency."

132132 : ("Working on: " ++ show (UVar var))

133133 : ("Old domain: " ++ show oldDom)

@@ -145,11 +145,14 @@ solve maxUniverseLevel inpConstraints =

145145 Nothing -> return ()

146146 Just cs -> do

147147 Queue list set <- gets queue

148− let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set ]

148+ let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set ]

149149 if null newCons

150150 then return ()

151151 else modify $ \ st -> st { queue = Queue (list ++ newCons)

152− (S.union set (S.fromList (map fst newCons))) }

152+ (insertAll (map uconstraint newCons) set) }

153+

154+ insertAll [] s = s

155+ insertAll (x : xs) s = insertAll xs (S.insert x s)

153156

154157 -- | check if a domain is wiped out.

155158 wipeOut :: Domain -> Bool

src/Idris/Core/Evaluate.hs+3−4

@@ -5,7 +5,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

55 rt_simplify, simplify, specialise, hnf, convEq, convEq',

66 Def(..), CaseInfo(..), CaseDefs(..),

77 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),

8− Context, initContext, ctxtAlist, uconstraints, next_tvar,

8+ Context, initContext, ctxtAlist, next_tvar,

99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

1010 addDatatype, addCasedef, simplifyCasedef, addOperator,

1111 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

@@ -786,16 +786,15 @@ data MetaInformation =

786786-- | Contexts used for global definitions and for proof state. They contain

787787-- universe constraints and existing definitions.

788788data Context = MkContext {

789− uconstraints :: [UConstraint],

790789 next_tvar :: Int,

791790 definitions :: Ctxt (Def, Accessibility, Totality, MetaInformation)

792791 } deriving Show

793792

794793-- | The initial empty context

795−initContext = MkContext [] 0 emptyContext

794+initContext = MkContext 0 emptyContext

796795

797796mapDefCtxt :: (Def -> Def) -> Context -> Context

798−mapDefCtxt f (MkContext c t defs) = MkContext c t (mapCtxt f' defs)

797+mapDefCtxt f (MkContext t defs) = MkContext t (mapCtxt f' defs)

799798 where f' (d, a, t, m) = f' (f d, a, t, m)

800799

801800-- | Get the definitions from a context

src/Idris/Core/TT.hs+10−8

@@ -782,14 +782,6 @@ deriving instance NFData UExp

782782instance Sized UExp where

783783 size _ = 1

784784

785−-- We assume that universe levels have been checked, so anything external

786−-- can just have the same universe variable and we won't get any new

787−-- cycles.

788−

789−instance Binary UExp where

790− put x = return ()

791− get = return (UVar (-1))

792−

793785instance Show UExp where

794786 show (UVar x) | x < 26 = [toEnum (x + fromEnum 'a')]

795787 | otherwise = toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)

@@ -801,6 +793,16 @@ data UConstraint = ULT UExp UExp -- ^ Strictly less than

801793 | ULE UExp UExp -- ^ Less than or equal to

802794 deriving (Eq, Ord)

803795

796+data ConstraintFC = ConstraintFC { uconstraint :: UConstraint,

797+ ufc :: FC }

798+ deriving Show

799+

800+instance Eq ConstraintFC where

801+ x == y = uconstraint x == uconstraint y

802+

803+instance Ord ConstraintFC where

804+ compare x y = compare (uconstraint x) (uconstraint y)

805+

804806instance Show UConstraint where

805807 show (ULT x y) = show x ++ " < " ++ show y

806808 show (ULE x y) = show x ++ " <= " ++ show y

src/Idris/IBC.hs+1−1

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

3737import Util.Zlib (decompressEither)

3838

3939ibcVersion :: Word8

40−ibcVersion = 100

40+ibcVersion = 101

4141

4242data IBCFile = IBCFile { ver :: Word8,

4343 sourcefile :: FilePath,

src/Idris/REPL.hs+4−2

@@ -87,6 +87,7 @@ import Control.Concurrent

8787import Data.Maybe

8888import Data.List hiding (group)

8989import Data.Char

90+import qualified Data.Set as S

9091import Data.Version

9192import Data.Word (Word)

9293import Data.Either (partitionEithers)

@@ -945,9 +946,10 @@ process fn (DocStr (Right c) _) -- constants only have overviews

945946process fn Universes

946947 = do i <- getIState

947948 let cs = idris_constraints i

949+ let cslist = S.toAscList cs

948950-- iputStrLn $ showSep "\n" (map show cs)

949− iputStrLn $ show (map fst cs)

950− let n = length cs

951+ iputStrLn $ show (map uconstraint cslist)

952+ let n = length cslist

951953 iputStrLn $ "(" ++ show n ++ " constraints)"

952954 case ucheck cs of

953955 Error e -> iPrintError $ pshow i e