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

src/Idris/AbsSyntaxTree.hs+3

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

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

714714 | PHidden PTerm -- ^ Irrelevant or hidden pattern

715715 | PType -- ^ 'Type' type

716+ | PUniverse Universe -- ^ Some universe

716717 | PGoal FC PTerm Name PTerm

717718 | PConstant Const -- ^ Builtin types

718719 | Placeholder

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

13801381 prettyAs =

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

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

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

13841386 -- XXX: add pretty for tactics

13851387 prettySe p bnd (PProof ts) =

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

16441646 size (PDisamb _ tm) = size tm

16451647 size (PNoImplicits tm) = size tm

16461648 size PType = 1

1649+ size (PUniverse _) = 1

16471650 size (PConstant const) = 1 + size const

16481651 size Placeholder = 1

16491652 size (PDoBlock dos) = 1 + size dos

src/Idris/Core/Binary.hs+14

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

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

276276

277277

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+

278288instance Binary NameType where

279289 put x

280290 = case x of

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

325335 TType x1 -> do putWord8 7

326336 put x1

327337 Impossible -> putWord8 8

338+ UType x1 -> do putWord8 10

339+ put x1

328340 get

329341 = do i <- getWord8

330342 case i of

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

352364 8 -> return Impossible

353365 9 -> do x1 <- get

354366 return (V x1)

367+ 10 -> do x1 <- get

368+ return (UType x1)

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

356370

src/Idris/Core/DeepSeq.hs+1

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

9898 rnf Erased = ()

9999 rnf Impossible = ()

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

101+ rnf (UType _) = ()

101102

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

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

404404unifyProblems :: Elab' aux ()

405405unifyProblems = processTactic' UnifyProblems

406406

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

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

409− processTactic' (Defer n')

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

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

409+ processTactic' (Defer ds n')

410410

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

412412deferType 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,

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

1212 mapDefCtxt,

1313 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

1516

1617import Debug.Trace

1718import Control.Applicative hiding (Const)

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

4748 | VBLet Int Name Value Value Value

4849 | VApp Value Value

4950 | VType UExp

51+ | VUType Universe

5052 | VErased

5153 | VImpossible

5254 | VConstant Const

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

298300 ev ntimes stk top env Erased = return VErased

299301 ev ntimes stk top env Impossible = return VImpossible

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

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

301304

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

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

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

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

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

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

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

522526 quote i VErased = return $ Erased

523527 quote i VImpossible = return $ Impossible

524528 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

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

535539wknV i t = return t

536540

541+isUniverse :: Term -> Bool

542+isUniverse (TType _) = True

543+isUniverse (UType _) = True

544+isUniverse _ = False

545+

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

538547

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

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

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

574583 put (v, ULE x y : cs)

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

576588 ceq ps Erased _ = return True

577589 ceq ps _ Erased = return True

578590 ceq ps x y = return False

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

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

7575 | PatVar Name

7676 | PatBind Name

7777 | Focus Name

78− | Defer Name

78+ | Defer [Name] Name

7979 | DeferType Name Raw [Name]

8080 | Instance Name

8181 | SetInjective Name

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

387387 ps { injective = n : is })

388388 return (Bind x b sc)

389389

390−defer :: Name -> RunTactic

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

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

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

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

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

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

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

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

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

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

396397 where

397398 mkTy [] t = t

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

952953 mktac (CheckIn r) = check_in r

953954 mktac (EvalIn r) = eval_in r

954955 mktac (Focus n) = focus n

955− mktac (Defer n) = defer n

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

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

957958 mktac (Instance n) = instanceArg n

958959 mktac (SetInjective n) = setinj n

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

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

137137 | CantResolveAlts [Name]

138138 | IncompleteTerm t

139139 | UniverseError

140+ | UniqueError Name

140141 | ProgramLineComment

141142 | Inaccessible Name

142143 | NonCollapsiblePostulate Name

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

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

593594constDocs prim = "Undocumented"

594595

596+data Universe = UniqueType | AllTypes

597+ deriving (Show, Eq, Ord)

598+

595599data Raw = Var Name

596600 | RBind Name (Binder Raw) Raw

597601 | RApp Raw Raw

598602 | RType

603+ | RUType Universe

599604 | RForce Raw

600605 | RConstant Const

601606 deriving (Show, Eq)

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

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

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

607612 size RType = 1

613+ size (RUType _) = 1

608614 size (RForce raw) = 1 + size raw

609615 size (RConstant const) = size const

610616

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

751757 | Erased -- ^ an erased term

752758 | Impossible -- ^ special case for totality checking

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

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

754761 deriving (Ord, Functor)

755762{-!

756763deriving instance Binary TT

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

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

10531060-- Bruijn indices.

10541061forget :: TT Name -> Raw

1055−forget tm = fe [] tm

1056− where

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

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

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

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

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

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

1063− fe env (Constant c)

1064− = RConstant c

1065− fe env (TType i) = RType

1066− fe env Erased = RConstant Forgot

1062+forget tm = forgetEnv [] tm

1063+

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

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

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

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

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

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

1070+forgetEnv env (Constant c) = RConstant c

1071+forgetEnv env (TType i) = RType

1072+forgetEnv env (UType u) = RUType u

1073+forgetEnv env Erased = RConstant Forgot

10671074

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

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

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

12441251 se p env Erased = "[__]"

12451252 se p env Impossible = "[impossible]"

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

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

12471255

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

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

4747

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

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

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

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

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

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

5252

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

5454recheck ctxt env tm orig

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

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

5858 Error e -> Error e

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

60− return (tm, ty, constraints)

60+ do checkUnique ctxt env tm

61+ return (tm, ty, constraints)

6162

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

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

64+check ctxt env tm

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

6466

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

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

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

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

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

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

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

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

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

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

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

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

127136 (v, cs) <- get

128− let TType su = normalise ctxt env st

129− let TType tu = normalise ctxt env tt

130− 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))

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

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

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

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

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

133148 chk env (RBind n b sc)

134149 = do b' <- checkBinder b

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

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

140155 let tt' = normalise ctxt env tt

141156 lift $ isType ctxt env tt'

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

149158 checkBinder (Let t v)

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

151160 (vv, vt) <- chk env v

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

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

220229 discharge n (PVTy t) scv sct

221230 = 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 =

427427 sameBinder _ _ = False

428428 un' fn bnames x y

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

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

430431 | otherwise = do UI s f <- get

431432 let r = recoverable (normalise ctxt env x)

432433 (normalise ctxt env y)

src/Idris/DeepSeq.hs+1

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

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

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

216216 rnf PType = ()

217+ rnf (PUniverse _) = ()

217218 rnf (PGoal x1 x2 x3 x4)

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

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

src/Idris/Delaborate.hs+3

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

8080 de env _ Erased = Placeholder

8181 de env _ Impossible = Placeholder

8282 de env _ (TType i) = PType

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

8384

8485 dens x | fullname = x

8586 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

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

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

225226pprintErr' i UniverseError = text "Universe inconsistency"

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

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

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

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

228231pprintErr' 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

238238 -> ElabD ()

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

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

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

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

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

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

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

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

630631 movelast h

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

632− do attack; defer n'; solve

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

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

634635 mkN n = case namespace info of

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

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

683684 focus valn

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

685686 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+

686710 cname <- unique_hole' True (mkCaseName fn)

687711 let cname' = mkN cname

688− elab' ina (PMetavar cname')

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

713+ attack; defer argsDropped cname'; solve

714+

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

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

691717 let newdef = PClauses fc [] cname'

692718 (caseBlock fc cname'

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

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

694720 -- elaborate case

695721 updateAux (newdef : )

696722 -- 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

704730 mkN n = case namespace info of

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

706732 _ -> 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+

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

708775 elab' ina t

709776 unifyLog False

src/Idris/IBC.hs+4

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

14861486 PDisamb x1 x2 -> do putWord8 37

14871487 put x1

14881488 put x2

1489+ PUniverse x1 -> do putWord8 38

1490+ put x1

14891491

14901492 get

14911493 = do i <- getWord8

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

16021604 37 -> do x1 <- get

16031605 x2 <- get

16041606 return (PDisamb x1 x2)

1607+ 38 -> do x1 <- get

1608+ return (PUniverse x1)

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

16061610

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

src/Idris/ParseExpr.hs+2

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

308308 <|> proofExpr syn

309309 <|> tacticsExpr syn

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

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

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

311313 <|> do c <- constant

312314 fc <- getFC

313315 return (modifyConst syn fc (PConstant c))

src/Idris/ProofSearch.hs+4−4

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

5959 where

6060 -- if nothing worked, make a new metavariable

6161 tryAllFns [] | fromProver = cantSolveGoal

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

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

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

6464

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

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

7575 if fromProver then cantSolveGoal

7676 else do

7777 mapM_ (\ h -> do focus h

78− attack; defer nroot; solve)

78+ attack; defer [] nroot; solve)

7979 (hs' \\ hs)

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

8181 solve

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

9696 toUN t = t

9797

9898 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"

100100 psRec False d = tryCons d hints

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

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

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

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

105105 (if fromProver

106106 then cantSolveGoal

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

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

108108

109109 getFn d Nothing = []

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