d57d60a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Use a Set for universe constraints

d57d60aEdwin Brady12 years ago

src/Idris/AbsSyntax.hs+6−3

compare with master

unifiedsplit

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

543addConstraints fc (v, cs)

544 = do i <- getIState

545 let ctxt = tt_ctxt i

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

547− next_tvar = v }

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

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

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

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

548 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

550

553

551addDeferred = addDeferred' Ref

554addDeferred = addDeferred' Ref

552addDeferredTyCon = addDeferred' (TCon 0 0)

555addDeferredTyCon = addDeferred' (TCon 0 0)

src/Idris/AbsSyntaxTree.hs+2−2

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

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

158data IState = IState {

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

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

160+ idris_constraints :: S.Set ConstraintFC,

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

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

163 idris_implicits :: Ctxt [PArg],

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

309

310-- | The initial state for the compiler

311idrisInit :: IState

312−idrisInit = IState initContext [] []

312+idrisInit = IState initContext S.empty []

313 emptyContext emptyContext emptyContext emptyContext

314 emptyContext emptyContext emptyContext emptyContext

315 emptyContext emptyContext emptyContext emptyContext

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

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

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

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

548

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"

549

564

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

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

551 put x

566 put x

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

600 x2 <- getWord8

615 x2 <- getWord8

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

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

602 6 -> return Erased

617 6 -> return Erased

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

618+ 7 -> do x1 <- get

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

619+ return (TType x1)

605 8 -> return Impossible

620 8 -> return Impossible

606 9 -> do x1 <- get

621 9 -> do x1 <- get

607 return (V x1)

622 return (V x1)

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

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

1-- | Check universe constraints.

2module 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'(..) )

6import Control.Applicative

7import Control.Applicative

7import Control.Monad.State.Strict

8import Control.Monad.State.Strict

8−import Data.Function ( on )

9−import Data.List ( partition, nubBy )

9+import Data.List ( partition )

10import qualified Data.Map.Strict as M

11import qualified Data.Set as S

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

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

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

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

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

17 where

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

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

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

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

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

21 ignore _ = False

23newtype Var = Var Int

24 deriving (Eq, Ord, Show)

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

26+data Domain = Domain Int Int

27− {-# UNPACK #-} !Int

28 deriving (Eq, Ord, Show)

27 deriving (Eq, Ord, Show)

30data SolverState =

29data SolverState =

31 SolverState

30 SolverState

32 { queue :: Queue

31 { queue :: Queue

33 , domainStore :: M.Map Var ( Domain

32 , domainStore :: M.Map Var ( Domain

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

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

35 )

34 )

36 }

35 }

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

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

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

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

42−solve maxUniverseLevel inpConstraints =

41+solve maxUniverseLevel ucs =

43 evalStateT (propagate >> extractSolution) initSolverState

42 evalStateT (propagate >> extractSolution) initSolverState

45 where

44 where

45+ inpConstraints = S.toAscList ucs

47 -- | initial solver state.

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

49 initSolverState :: SolverState

50 initSolverState =

51 let

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

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

53 in

54 SolverState

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

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

56 , domainStore = M.fromList

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

58 | v <- ordNub [ v

59− | (c, _) <- inpConstraints

59+ | ConstraintFC c _ <- inpConstraints

60 , v <- varsIn c

61 ]

62 ]

63 }

65 -- | 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)

67 constraints = M.fromListWith S.union

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

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

69− | (c, fc) <- inpConstraints

69+ | ConstraintFC c fc <- inpConstraints

70 , let vars = varsIn c

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

72 , v <- vars

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

82 mcons <- nextConstraint

83 case mcons of

84 Nothing -> return ()

85− Just (cons, fc) -> do

85+ Just (ConstraintFC cons fc) -> do

86 case cons of

87 ULE a b -> do

88 Domain lowerA upperA <- domainOf a

89 Domain lowerB upperB <- domainOf b

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

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

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

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

92 ULT a b -> do

93 Domain lowerA upperA <- domainOf a

94 Domain lowerB upperB <- domainOf b

95 let upperB_pred = pred upperB

96 let lowerA_succ = succ lowerA

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

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

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

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

99 propagate

100

101 -- | extract a solution from the state.

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

106 extractValue (Domain x _) = x

107

108 -- | dequeue the first constraint.

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

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

110 nextConstraint = do

111 Queue list set <- gets queue

112 case list of

113 [] -> return Nothing

114 (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) }

116 return (Just q)

117

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

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

123

124 -- | updates the domain of a variable.

125 -- 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 ()

127 updateDomainOf suspect (UVar var) newDom = do

128 doms <- gets domainStore

129 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

131 $ "Universe inconsistency."

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

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

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

145 Nothing -> return ()

146 Just cs -> do

147 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 ]

149 if null newCons

150 then return ()

151 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)

153

156

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

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

155 wipeOut :: Domain -> Bool

158 wipeOut :: Domain -> Bool

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

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

5 rt_simplify, simplify, specialise, hnf, convEq, convEq',

6 Def(..), CaseInfo(..), CaseDefs(..),

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

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

8+ Context, initContext, ctxtAlist, next_tvar,

9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

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

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

787-- universe constraints and existing definitions.

788data Context = MkContext {

789− uconstraints :: [UConstraint],

790 next_tvar :: Int,

789 next_tvar :: Int,

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

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

792 } deriving Show

791 } deriving Show

793

792

794-- | The initial empty context

793-- | The initial empty context

795−initContext = MkContext [] 0 emptyContext

794+initContext = MkContext 0 emptyContext

796

795

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

796mapDefCtxt :: (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)

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

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

800

799

801-- | Get the definitions from a context

800-- | Get the definitions from a context

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

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

782instance Sized UExp where

783 size _ = 1

784

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−

793instance Show UExp where

785instance Show UExp where

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

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

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

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

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

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

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

802 deriving (Eq, Ord)

794 deriving (Eq, Ord)

803

795

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+

804instance Show UConstraint where

806instance Show UConstraint where

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

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

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

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

src/Idris/IBC.hs+1−1

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

37import Util.Zlib (decompressEither)

39ibcVersion :: Word8

40−ibcVersion = 100

40+ibcVersion = 101

42data IBCFile = IBCFile { ver :: Word8,

43 sourcefile :: FilePath,

src/Idris/REPL.hs+4−2

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

87import Data.Maybe

88import Data.List hiding (group)

89import Data.Char

90+import qualified Data.Set as S

90import Data.Version

91import Data.Version

91import Data.Word (Word)

92import Data.Word (Word)

92import Data.Either (partitionEithers)

93import Data.Either (partitionEithers)

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

945process fn Universes

946process fn Universes

946 = do i <- getIState

947 = do i <- getIState

947 let cs = idris_constraints i

948 let cs = idris_constraints i

949+ let cslist = S.toAscList cs

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

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

949− iputStrLn $ show (map fst cs)

951+ iputStrLn $ show (map uconstraint cslist)

950− let n = length cs

952+ let n = length cslist

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

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

952 case ucheck cs of

954 case ucheck cs of

953 Error e -> iPrintError $ pshow i e

955 Error e -> iPrintError $ pshow i e