9ceece1 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+3

compare with master

unifiedsplit

@@ -713,6 +713,7 @@ data PTerm = PQuote Raw

713 | PAlternative Bool [PTerm] -- True if only one may work

714 | PHidden PTerm -- ^ Irrelevant or hidden pattern

715 | PType -- ^ 'Type' type

716+ | PUniverse Universe -- ^ Some universe

716 | PGoal FC PTerm Name PTerm

717 | PGoal FC PTerm Name PTerm

717 | PConstant Const -- ^ Builtin types

718 | PConstant Const -- ^ Builtin types

718 | Placeholder

719 | Placeholder

@@ -1380,6 +1381,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1380 prettyAs =

1381 prettyAs =

1381 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as

1382 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as

1382 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1383 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1384+ prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

1383 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1385 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1384 -- XXX: add pretty for tactics

1386 -- XXX: add pretty for tactics

1385 prettySe p bnd (PProof ts) =

1387 prettySe p bnd (PProof ts) =

@@ -1644,6 +1646,7 @@ instance Sized PTerm where

1644 size (PDisamb _ tm) = size tm

1646 size (PDisamb _ tm) = size tm

1645 size (PNoImplicits tm) = size tm

1647 size (PNoImplicits tm) = size tm

1646 size PType = 1

1648 size PType = 1

1649+ size (PUniverse _) = 1

1647 size (PConstant const) = 1 + size const

1650 size (PConstant const) = 1 + size const

1648 size Placeholder = 1

1651 size Placeholder = 1

1649 size (PDoBlock dos) = 1 + size dos

1652 size (PDoBlock dos) = 1 + size dos

src/Idris/Core/Binary.hs+14

@@ -275,6 +275,16 @@ instance (Binary b) => Binary (Binder b) where

275 _ -> error "Corrupted binary data for Binder"

276

277

278+instance Binary Universe where

279+ put x = case x of

280+ UniqueType -> putWord8 0

281+ AllTypes -> putWord8 1

282+ get = do i <- getWord8

283+ case i of

284+ 0 -> return UniqueType

285+ 1 -> return AllTypes

286+ _ -> error "Corrupted binary data for Universe"

287+

278instance Binary NameType where

288instance Binary NameType where

279 put x

289 put x

280 = case x of

290 = case x of

@@ -325,6 +335,8 @@ instance {- (Binary n) => -} Binary (TT Name) where

325 TType x1 -> do putWord8 7

335 TType x1 -> do putWord8 7

326 put x1

336 put x1

327 Impossible -> putWord8 8

337 Impossible -> putWord8 8

338+ UType x1 -> do putWord8 10

339+ put x1

328 get

340 get

329 = do i <- getWord8

341 = do i <- getWord8

330 case i of

342 case i of

@@ -352,5 +364,7 @@ instance {- (Binary n) => -} Binary (TT Name) where

352 8 -> return Impossible

364 8 -> return Impossible

353 9 -> do x1 <- get

365 9 -> do x1 <- get

354 return (V x1)

366 return (V x1)

367+ 10 -> do x1 <- get

368+ return (UType x1)

355 _ -> error "Corrupted binary data for TT"

369 _ -> error "Corrupted binary data for TT"

356

370

src/Idris/Core/DeepSeq.hs+1

@@ -98,6 +98,7 @@ instance (NFData n) => NFData (TT n) where

98 rnf Erased = ()

99 rnf Impossible = ()

100 rnf (TType x1) = rnf x1 `seq` ()

101+ rnf (UType _) = ()

101

102

102instance (NFData t) => NFData (SC' t) where

103instance (NFData t) => NFData (SC' t) where

103 rnf (Case x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

104 rnf (Case x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/Core/Elaborate.hs+3−3

@@ -404,9 +404,9 @@ matchProblems all = processTactic' (MatchProblems all)

404unifyProblems :: Elab' aux ()

405unifyProblems = processTactic' UnifyProblems

406

407−defer :: Name -> Elab' aux ()

407+defer :: [Name] -> Name -> Elab' aux ()

408−defer n = do n' <- unique_hole n

408+defer ds n = do n' <- unique_hole n

409− processTactic' (Defer n')

409+ processTactic' (Defer ds n')

410

411deferType :: Name -> Raw -> [Name] -> Elab' aux ()

412deferType n ty ns = processTactic' (DeferType n ty ns)

src/Idris/Core/Evaluate.hs+13−1

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

11 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

12 mapDefCtxt,

13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14− Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where

14+ Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

15+ isUniverse) where

15

16

16import Debug.Trace

17import Debug.Trace

17import Control.Applicative hiding (Const)

18import Control.Applicative hiding (Const)

@@ -47,6 +48,7 @@ data Value = VP NameType Name Value

47 | VBLet Int Name Value Value Value

48 | VBLet Int Name Value Value Value

48 | VApp Value Value

49 | VApp Value Value

49 | VType UExp

50 | VType UExp

51+ | VUType Universe

50 | VErased

52 | VErased

51 | VImpossible

53 | VImpossible

52 | VConstant Const

54 | VConstant Const

@@ -298,6 +300,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

298 ev ntimes stk top env Erased = return VErased

300 ev ntimes stk top env Erased = return VErased

299 ev ntimes stk top env Impossible = return VImpossible

301 ev ntimes stk top env Impossible = return VImpossible

300 ev ntimes stk top env (TType i) = return $ VType i

302 ev ntimes stk top env (TType i) = return $ VType i

303+ ev ntimes stk top env (UType u) = return $ VUType u

301

304

302 evApply ntimes stk top env args (VApp f a)

305 evApply ntimes stk top env args (VApp f a)

303 = evApply ntimes stk top env (a:args) f

306 = evApply ntimes stk top env (a:args) f

@@ -519,6 +522,7 @@ instance Quote Value where

519 return (Bind n (Let t' v') sc'')

522 return (Bind n (Let t' v') sc'')

520 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

523 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

521 quote i (VType u) = return $ TType u

524 quote i (VType u) = return $ TType u

525+ quote i (VUType u) = return $ UType u

522 quote i VErased = return $ Erased

526 quote i VErased = return $ Erased

523 quote i VImpossible = return $ Impossible

527 quote i VImpossible = return $ Impossible

524 quote i (VProj v j) = do v' <- quote i v

528 quote i (VProj v j) = do v' <- quote i v

@@ -534,6 +538,11 @@ wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b

534wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)

538wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)

535wknV i t = return t

539wknV i t = return t

536

540

541+isUniverse :: Term -> Bool

542+isUniverse (TType _) = True

543+isUniverse (UType _) = True

544+isUniverse _ = False

545+

537convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])

546convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])

538

547

539convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

548convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

@@ -573,6 +582,9 @@ convEq ctxt holes topx topy = ceq [] topx topy where

573 ceq ps (TType x) (TType y) = do (v, cs) <- get

582 ceq ps (TType x) (TType y) = do (v, cs) <- get

574 put (v, ULE x y : cs)

583 put (v, ULE x y : cs)

575 return True

584 return True

585+ ceq ps (UType AllTypes) x = return (isUniverse x)

586+ ceq ps x (UType AllTypes) = return (isUniverse x)

587+ ceq ps (UType u) (UType v) = return (u == v)

576 ceq ps Erased _ = return True

588 ceq ps Erased _ = return True

577 ceq ps _ Erased = return True

589 ceq ps _ Erased = return True

578 ceq ps x y = return False

590 ceq ps x y = return False

src/Idris/Core/ProofState.hs+8−7

@@ -75,7 +75,7 @@ data Tactic = Attack

75 | PatVar Name

76 | PatBind Name

77 | Focus Name

78− | Defer Name

78+ | Defer [Name] Name

79 | DeferType Name Raw [Name]

80 | Instance Name

81 | SetInjective Name

@@ -387,12 +387,13 @@ setinj n ctxt env (Bind x b sc)

387 ps { injective = n : is })

388 return (Bind x b sc)

389

390−defer :: Name -> RunTactic

390+defer :: [Name] -> Name -> RunTactic

391−defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

391+defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

392+ do let env' = filter (\(n, t) -> n `notElem` dropped) env

392− do action (\ps -> let hs = holes ps in

393+ action (\ps -> let hs = holes ps in

393 ps { holes = hs \\ [x] })

394 ps { holes = hs \\ [x] })

394− return (Bind n (GHole (length env) (mkTy (reverse env) t))

395+ return (Bind n (GHole (length env') (mkTy (reverse env') t))

395− (mkApp (P Ref n ty) (map getP (reverse env))))

396+ (mkApp (P Ref n ty) (map getP (reverse env'))))

396 where

397 where

397 mkTy [] t = t

398 mkTy [] t = t

398 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)

399 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)

@@ -952,7 +953,7 @@ process t h = tactic (Just h) (mktac t)

952 mktac (CheckIn r) = check_in r

953 mktac (CheckIn r) = check_in r

953 mktac (EvalIn r) = eval_in r

954 mktac (EvalIn r) = eval_in r

954 mktac (Focus n) = focus n

955 mktac (Focus n) = focus n

955− mktac (Defer n) = defer n

956+ mktac (Defer ns n) = defer ns n

956 mktac (DeferType n t a) = deferType n t a

957 mktac (DeferType n t a) = deferType n t a

957 mktac (Instance n) = instanceArg n

958 mktac (Instance n) = instanceArg n

958 mktac (SetInjective n) = setinj n

959 mktac (SetInjective n) = setinj n

src/Idris/Core/TT.hs+20−12

@@ -137,6 +137,7 @@ data Err' t

137 | CantResolveAlts [Name]

138 | IncompleteTerm t

139 | UniverseError

140+ | UniqueError Name

140 | ProgramLineComment

141 | ProgramLineComment

141 | Inaccessible Name

142 | Inaccessible Name

142 | NonCollapsiblePostulate Name

143 | NonCollapsiblePostulate Name

@@ -592,10 +593,14 @@ constDocs (B32V v) = "A vector of thirty-two-bit values"

592constDocs (B64V v) = "A vector of sixty-four-bit values"

593constDocs (B64V v) = "A vector of sixty-four-bit values"

593constDocs prim = "Undocumented"

594constDocs prim = "Undocumented"

594

595

596+data Universe = UniqueType | AllTypes

597+ deriving (Show, Eq, Ord)

598+

595data Raw = Var Name

599data Raw = Var Name

596 | RBind Name (Binder Raw) Raw

600 | RBind Name (Binder Raw) Raw

597 | RApp Raw Raw

601 | RApp Raw Raw

598 | RType

602 | RType

603+ | RUType Universe

599 | RForce Raw

604 | RForce Raw

600 | RConstant Const

605 | RConstant Const

601 deriving (Show, Eq)

606 deriving (Show, Eq)

@@ -605,6 +610,7 @@ instance Sized Raw where

605 size (RBind name bind right) = 1 + size bind + size right

610 size (RBind name bind right) = 1 + size bind + size right

606 size (RApp left right) = 1 + size left + size right

611 size (RApp left right) = 1 + size left + size right

607 size RType = 1

612 size RType = 1

613+ size (RUType _) = 1

608 size (RForce raw) = 1 + size raw

614 size (RForce raw) = 1 + size raw

609 size (RConstant const) = size const

615 size (RConstant const) = size const

610

616

@@ -751,6 +757,7 @@ data TT n = P NameType n (TT n) -- ^ named references with type

751 | Erased -- ^ an erased term

757 | Erased -- ^ an erased term

752 | Impossible -- ^ special case for totality checking

758 | Impossible -- ^ special case for totality checking

753 | TType UExp -- ^ the type of types at some level

759 | TType UExp -- ^ the type of types at some level

760+ | UType Universe -- ^ Uniqueness type universe (disjoint from TType)

754 deriving (Ord, Functor)

761 deriving (Ord, Functor)

755{-!

762{-!

756deriving instance Binary TT

763deriving instance Binary TT

@@ -1052,18 +1059,18 @@ unList tm = case unApply tm of

1052-- with the corresponding name. It is an error if there are free de

1059-- with the corresponding name. It is an error if there are free de

1053-- Bruijn indices.

1060-- Bruijn indices.

1054forget :: TT Name -> Raw

1061forget :: TT Name -> Raw

1055−forget tm = fe [] tm

1062+forget tm = forgetEnv [] tm

1056− where

1063+

1057− fe env (P _ n _) = Var n

1064+forgetEnv env (P _ n _) = Var n

1058− fe env (V i) = Var (env !! i)

1065+forgetEnv env (V i) = Var (env !! i)

1059− fe env (Bind n b sc) = let n' = uniqueName n env in

1066+forgetEnv env (Bind n b sc) = let n' = uniqueName n env in

1060− RBind n' (fmap (fe env) b)

1067+ RBind n' (fmap (forgetEnv env) b)

1061− (fe (n':env) sc)

1068+ (forgetEnv (n':env) sc)

1062− fe env (App f a) = RApp (fe env f) (fe env a)

1069+forgetEnv env (App f a) = RApp (forgetEnv env f) (forgetEnv env a)

1063− fe env (Constant c)

1070+forgetEnv env (Constant c) = RConstant c

1064− = RConstant c

1065− fe env (TType i) = RType

1071+forgetEnv env (TType i) = RType

1072+forgetEnv env (UType u) = RUType u

1066− fe env Erased = RConstant Forgot

1073+forgetEnv env Erased = RConstant Forgot

1067

1074

1068-- | Introduce a 'Bind' into the given term for each element of the

1075-- | Introduce a 'Bind' into the given term for each element of the

1069-- given list of (name, binder) pairs.

1076-- given list of (name, binder) pairs.

@@ -1244,6 +1251,7 @@ showEnv' env t dbg = se 10 env t where

1244 se p env Erased = "[__]"

1251 se p env Erased = "[__]"

1245 se p env Impossible = "[impossible]"

1252 se p env Impossible = "[impossible]"

1246 se p env (TType i) = "Type " ++ show i

1253 se p env (TType i) = "Type " ++ show i

1254+ se p env (UType u) = show u

1247

1255

1248 sb env n (Lam t) = showb env "\\ " " => " n t

1256 sb env n (Lam t) = showb env "\\ " " => " n t

1249 sb env n (Hole t) = showb env "? " ". " n t

1257 sb env n (Hole t) = showb env "? " ". " n t

src/Idris/Core/Typecheck.hs+60−14

@@ -47,8 +47,8 @@ errEnv = map (\(x, b) -> (x, binderTy b))

47

48isType :: Context -> Env -> Term -> TC ()

49isType ctxt env tm = isType' (normalise ctxt env tm)

50− where isType' (TType _) = return ()

50+ where isType' tm | isUniverse tm = return ()

51− isType' tm = fail (showEnv env tm ++ " is not a TType")

51+ | otherwise = fail (showEnv env tm ++ " is not a Type")

52

53recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)

54recheck ctxt env tm orig

@@ -57,10 +57,12 @@ recheck ctxt env tm orig

57 Error (IncompleteTerm _) -> Error $ IncompleteTerm orig

58 Error e -> Error e

59 OK ((tm, ty), constraints) ->

60+ do checkUnique ctxt env tm

60− return (tm, ty, constraints)

61+ return (tm, ty, constraints)

61

62

62check :: Context -> Env -> Raw -> TC (Term, Type)

63check :: Context -> Env -> Raw -> TC (Term, Type)

64+check ctxt env tm

63−check ctxt env tm = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed

65+ = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed

64

66

65check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

67check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

66check' holes ctxt env top = chk env top where

68check' holes ctxt env top = chk env top where

@@ -102,6 +104,13 @@ check' holes ctxt env top = chk env top where

102 let c = ULT (UVar v) (UVar (v+1))

104 let c = ULT (UVar v) (UVar (v+1))

103 put (v+2, (c:cs))

105 put (v+2, (c:cs))

104 return (TType (UVar v), TType (UVar (v+1)))

106 return (TType (UVar v), TType (UVar (v+1)))

107+ chk env (RUType u)

108+ | holes = return (UType u, TType (UVal 0))

109+ | otherwise = do -- TODO! (v, cs) <- get

110+ -- let c = ULT (UVar v) (UVar (v+1))

111+ -- put (v+2, (c:cs))

112+ -- return (TType (UVar v), TType (UVar (v+1)))

113+ return (UType u, TType (UVal 0))

105 chk env (RConstant Forgot) = return (Erased, Erased)

114 chk env (RConstant Forgot) = return (Erased, Erased)

106 chk env (RConstant c) = return (Constant c, constType c)

115 chk env (RConstant c) = return (Constant c, constType c)

107 where constType (I _) = Constant (AType (ATInt ITNative))

116 where constType (I _) = Constant (AType (ATInt ITNative))

@@ -125,11 +134,17 @@ check' holes ctxt env top = chk env top where

125 = do (sv, st) <- chk env s

134 = do (sv, st) <- chk env s

126 (tv, tt) <- chk ((n, Pi sv) : env) t

135 (tv, tt) <- chk ((n, Pi sv) : env) t

127 (v, cs) <- get

136 (v, cs) <- get

128− let TType su = normalise ctxt env st

137+ case (normalise ctxt env st, normalise ctxt env tt) of

129− let TType tu = normalise ctxt env tt

138+ (TType su, TType tu) -> do

130− when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)

139+ when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)

131− return (Bind n (Pi (uniqueBinders (map fst env) sv))

140+ return (Bind n (Pi (uniqueBinders (map fst env) sv))

132 (pToV n tv), TType (UVar v))

141 (pToV n tv), TType (UVar v))

142+ (UType u, _) ->

143+ return (Bind n (Pi (uniqueBinders (map fst env) sv))

144+ (pToV n tv), UType u)

145+ (_, UType u) ->

146+ return (Bind n (Pi (uniqueBinders (map fst env) sv))

147+ (pToV n tv), UType u)

133 chk env (RBind n b sc)

148 chk env (RBind n b sc)

134 = do b' <- checkBinder b

149 = do b' <- checkBinder b

135 (scv, sct) <- chk ((n, b'):env) sc

150 (scv, sct) <- chk ((n, b'):env) sc

@@ -140,12 +155,6 @@ check' holes ctxt env top = chk env top where

140 let tt' = normalise ctxt env tt

155 let tt' = normalise ctxt env tt

141 lift $ isType ctxt env tt'

156 lift $ isType ctxt env tt'

142 return (Lam tv)

157 return (Lam tv)

143− checkBinder (Pi t)

144− = do (tv, tt) <- chk env t

145− let tv' = normalise ctxt env tv

146− let tt' = normalise ctxt env tt

147− lift $ isType ctxt env tt'

148− return (Pi tv)

149 checkBinder (Let t v)

158 checkBinder (Let t v)

150 = do (tv, tt) <- chk env t

159 = do (tv, tt) <- chk env t

151 (vv, vt) <- chk env v

160 (vv, vt) <- chk env v

@@ -219,3 +228,40 @@ check' holes ctxt env top = chk env top where

219 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

228 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

220 discharge n (PVTy t) scv sct

229 discharge n (PVTy t) scv sct

221 = return (Bind n (PVTy t) scv, sct)

230 = return (Bind n (PVTy t) scv, sct)

231+

232+-- If any binders are of kind 'UniqueType' or 'AllTypes' and the name appears

233+-- in the scope more than once, this is an error.

234+checkUnique :: Context -> Env -> Term -> TC ()

235+checkUnique ctxt env tm = evalStateT (chkBinders env (explicitNames tm)) []

236+ where

237+ chkBinders :: Env -> Term -> StateT [(Name, Bool)] TC ()

238+ chkBinders env (V i) | length env > i = chkName (fst (env!!i))

239+ chkBinders env (P _ n _) = chkName n

240+ chkBinders env (App f a) = do chkBinders env f; chkBinders env a

241+ chkBinders env (Bind n b t)

242+ = do chkBinderName env n b

243+ chkBinders ((n, b) : env) t

244+ chkBinders env t = return ()

245+

246+ chkBinderName :: Env -> Name -> Binder Term -> StateT [(Name, Bool)] TC ()

247+ chkBinderName env n b

248+ = do let rawty = forgetEnv (map fst env) (binderTy b)

249+ (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?

250+ case kind of

251+ UType UniqueType -> do ns <- get

252+ put ((n, False) : ns)

253+ UType AllTypes -> do ns <- get

254+ put ((n, False) : ns)

255+ _ -> return ()

256+ chkBinders env (binderTy b)

257+ case b of

258+ Let t v -> chkBinders env v

259+ _ -> return ()

260+

261+ chkName n

262+ = do ns <- get

263+ case lookup n ns of

264+ Nothing -> return ()

265+ Just True -> lift $ tfail (UniqueError n)

266+ Just False -> put ((n, True) : filter (\x -> fst x /= n) ns)

267+

src/Idris/Core/Unify.hs+1

@@ -427,6 +427,7 @@ unify ctxt env topx topy inj holes usersupp from =

427 sameBinder _ _ = False

428 un' fn bnames x y

429 | OK True <- convEq' ctxt holes x y = do sc 1; return []

430+ | isUniverse x && isUniverse y = do sc 1; return []

430 | otherwise = do UI s f <- get

431 | otherwise = do UI s f <- get

431 let r = recoverable (normalise ctxt env x)

432 let r = recoverable (normalise ctxt env x)

432 (normalise ctxt env y)

433 (normalise ctxt env y)

src/Idris/DeepSeq.hs+1

@@ -214,6 +214,7 @@ instance NFData PTerm where

214 rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

215 rnf (PHidden x1) = rnf x1 `seq` ()

216 rnf PType = ()

217+ rnf (PUniverse _) = ()

217 rnf (PGoal x1 x2 x3 x4)

218 rnf (PGoal x1 x2 x3 x4)

218 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

219 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

219 rnf (PConstant x1) = x1 `seq` ()

220 rnf (PConstant x1) = x1 `seq` ()

src/Idris/Delaborate.hs+3

@@ -80,6 +80,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

80 de env _ Erased = Placeholder

81 de env _ Impossible = Placeholder

82 de env _ (TType i) = PType

83+ de env _ (UType u) = PUniverse u

83

84

84 dens x | fullname = x

85 dens x | fullname = x

85 dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

86 dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

@@ -223,6 +224,8 @@ pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

223pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

224pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

224pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

225pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

225pprintErr' i UniverseError = text "Universe inconsistency"

226pprintErr' i UniverseError = text "Universe inconsistency"

227+pprintErr' i (UniqueError n) = text "Unique name" <+> annName' n (showbasic n)

228+ <+> text "is used more than once"

226pprintErr' i ProgramLineComment = text "Program line next to comment"

229pprintErr' i ProgramLineComment = text "Program line next to comment"

227pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"

230pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"

228pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>

231pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>

src/Idris/ElabTerm.hs+70−3

@@ -238,6 +238,7 @@ elab ist info emode opts fn tm

238 -> ElabD ()

239 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step

240 elab' ina PType = do apply RType []; solve

241+ elab' ina (PUniverse u) = do apply (RUType u) []; solve

241-- elab' (_,_,inty) (PConstant c)

242-- elab' (_,_,inty) (PConstant c)

242-- | constType c && pattern && not reflection && not inty

243-- | constType c && pattern && not reflection && not inty

243-- = lift $ tfail (Msg "Typecase is not allowed")

244-- = lift $ tfail (Msg "Typecase is not allowed")

@@ -629,7 +630,7 @@ elab ist info emode opts fn tm

629 elab' ina Placeholder = do (h : hs) <- get_holes

630 elab' ina Placeholder = do (h : hs) <- get_holes

630 movelast h

631 movelast h

631 elab' ina (PMetavar n) = let n' = mkN n in

632 elab' ina (PMetavar n) = let n' = mkN n in

632− do attack; defer n'; solve

633+ do attack; defer [] n'; solve

633 where mkN n@(NS _ _) = n

634 where mkN n@(NS _ _) = n

634 mkN n = case namespace info of

635 mkN n = case namespace info of

635 Just xs@(_:_) -> sNS n xs

636 Just xs@(_:_) -> sNS n xs

@@ -683,14 +684,39 @@ elab ist info emode opts fn tm

683 focus valn

684 focus valn

684 elabE (True, a, inty, qq) scr

685 elabE (True, a, inty, qq) scr

685 args <- get_env

686 args <- get_env

687+ envU <- mapM (getKind args) args

688+ let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts

689+-- ++ allNamesIn scr

690+

691+ -- in the definition we build for the case, only pass through

692+ -- names which are directly used, type class constraints, and

693+ -- variables any of these depend on

694+ -- FIXME: This probably doesn't help us, but leaving it in

695+ -- temporarily (but commented out). If this comment is still

696+ -- here in master, please delete the code!

697+-- let directUse = filter (\n -> usedIn namesUsedInRHS n

698+-- || tcName (binderTy (snd n))) args

699+-- let args' = args -- chaseDeps args (map fst directUse) directUse

700+-- let argsDropped = map fst $

701+-- filter (\(n, _) -> case lookup n args' of

702+-- Nothing -> True

703+-- _ -> False) args

704+

705+ -- Drop the unique arguments used in the scrutinee (since it's

706+ -- not valid to use them again anyway)

707+ let argsDropped = filter (isUnique envU) (nub $ allNamesIn scr)

708+ let args' = filter (\(n, _) -> n `notElem` argsDropped) args

709+

686 cname <- unique_hole' True (mkCaseName fn)

710 cname <- unique_hole' True (mkCaseName fn)

687 let cname' = mkN cname

711 let cname' = mkN cname

688− elab' ina (PMetavar cname')

712+-- elab' ina (PMetavar cname')

713+ attack; defer argsDropped cname'; solve

714+

689 -- if the scrutinee is one of the 'args' in env, we should

715 -- if the scrutinee is one of the 'args' in env, we should

690 -- inspect it directly, rather than adding it as a new argument

716 -- inspect it directly, rather than adding it as a new argument

691 let newdef = PClauses fc [] cname'

717 let newdef = PClauses fc [] cname'

692 (caseBlock fc cname'

718 (caseBlock fc cname'

693− (map (isScr scr) (reverse args)) opts)

719+ (map (isScr scr) (reverse args')) opts)

694 -- elaborate case

720 -- elaborate case

695 updateAux (newdef : )

721 updateAux (newdef : )

696 -- if we haven't got the type yet, hopefully we'll get it later!

722 -- if we haven't got the type yet, hopefully we'll get it later!

@@ -704,6 +730,47 @@ elab ist info emode opts fn tm

704 mkN n = case namespace info of

730 mkN n = case namespace info of

705 Just xs@(_:_) -> sNS n xs

731 Just xs@(_:_) -> sNS n xs

706 _ -> n

732 _ -> n

733+

734+ isUnique envk n = case lookup n envk of

735+ Just u -> u

736+ _ -> False

737+

738+ getKind env (n, _)

739+ = case lookup n env of

740+ Nothing -> return (n, False) -- can't happen, actually...

741+ Just b ->

742+ do ty <- get_type (forget (binderTy b))

743+ case ty of

744+ UType UniqueType -> return (n, True)

745+ UType AllTypes -> return (n, True)

746+ _ -> return (n, False)

747+

748+ tcName tm | (P _ n _, _) <- unApply tm

749+ = case lookupCtxt n (idris_classes ist) of

750+ [_] -> True

751+ _ -> False

752+ tcName _ = False

753+

754+ usedIn ns (n, b)

755+ = n `elem` ns

756+ || any (\x -> x `elem` ns) (allTTNames (binderTy b))

757+

758+ -- FIXME: This probably doesn't help us here, but leaving

759+ -- it in temporarily... if this comment is still here in master,

760+ -- please delete the code!

761+ chaseDeps env acc [] = filter (\(n, _) -> n `elem` acc) env

762+ chaseDeps env acc ((n,b) : args)

763+ = let ns = allTTNames (binderTy b) in

764+ extendAcc ns acc args

765+ where

766+ extendAcc [] acc args = chaseDeps env acc args

767+ extendAcc (n:ns) acc args

768+ | elem n acc = extendAcc ns acc args

769+ | otherwise = case lookup n env of

770+ Just b -> extendAcc ns (n : acc)

771+ ((n,b) : args)

772+ Nothing -> extendAcc ns acc args

773+

707 elab' ina (PUnifyLog t) = do unifyLog True

774 elab' ina (PUnifyLog t) = do unifyLog True

708 elab' ina t

775 elab' ina t

709 unifyLog False

776 unifyLog False

src/Idris/IBC.hs+4

@@ -1486,6 +1486,8 @@ instance Binary PTerm where

1486 PDisamb x1 x2 -> do putWord8 37

1487 put x1

1488 put x2

1489+ PUniverse x1 -> do putWord8 38

1490+ put x1

1489

1491

1490 get

1492 get

1491 = do i <- getWord8

1493 = do i <- getWord8

@@ -1602,6 +1604,8 @@ instance Binary PTerm where

1602 37 -> do x1 <- get

1604 37 -> do x1 <- get

1603 x2 <- get

1605 x2 <- get

1604 return (PDisamb x1 x2)

1606 return (PDisamb x1 x2)

1607+ 38 -> do x1 <- get

1608+ return (PUniverse x1)

1605 _ -> error "Corrupted binary data for PTerm"

1609 _ -> error "Corrupted binary data for PTerm"

1606

1610

1607instance (Binary t) => Binary (PTactic' t) where

1611instance (Binary t) => Binary (PTactic' t) where

src/Idris/ParseExpr.hs+2

@@ -308,6 +308,8 @@ simpleExpr syn =

308 <|> proofExpr syn

309 <|> tacticsExpr syn

310 <|> do reserved "Type"; return PType

311+ <|> do reserved "UniqueType"; return $ PUniverse UniqueType

312+ <|> do reserved "AllTypes"; return $ PUniverse AllTypes

311 <|> do c <- constant

313 <|> do c <- constant

312 fc <- getFC

314 fc <- getFC

313 return (modifyConst syn fc (PConstant c))

315 return (modifyConst syn fc (PConstant c))

src/Idris/ProofSearch.hs+4−4

@@ -59,7 +59,7 @@ proofSearch False fromProver depth elab _ nroot [fn] ist

59 where

60 -- if nothing worked, make a new metavariable

61 tryAllFns [] | fromProver = cantSolveGoal

62− tryAllFns [] = do attack; defer nroot; solve

62+ tryAllFns [] = do attack; defer [] nroot; solve

63 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True

64

65 tryFn (f, args) = do let imps = map isImp args

@@ -75,7 +75,7 @@ proofSearch False fromProver depth elab _ nroot [fn] ist

75 if fromProver then cantSolveGoal

76 else do

77 mapM_ (\ h -> do focus h

78− attack; defer nroot; solve)

78+ attack; defer [] nroot; solve)

79 (hs' \\ hs)

80-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))

81 solve

@@ -96,7 +96,7 @@ proofSearch rec fromProver maxDepth elab fn nroot hints ist

96 toUN t = t

97

98 psRec _ 0 | fromProver = cantSolveGoal

99− psRec rec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"

99+ psRec rec 0 = do attack; defer [] nroot; solve --fail "Maximum depth reached"

100 psRec False d = tryCons d hints

101 psRec True d = try' (trivial elab ist)

102 (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))

@@ -104,7 +104,7 @@ proofSearch rec fromProver maxDepth elab fn nroot hints ist

104 -- if all else fails, make a new metavariable

105 (if fromProver

106 then cantSolveGoal

107− else do attack; defer nroot; solve) True) True

107+ else do attack; defer [] nroot; solve) True) True

108

109 getFn d Nothing = []

110 getFn d (Just f) | d < maxDepth-1 = [f]