dd5001f · Idris-dev · git.iko.soy

src/Core/CoreParser.hs+2−2

@@ -220,8 +220,8 @@ pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm

220220 lchar '.';

221221 sc <- pTerm

222222 return (RBind x (PVar ty) sc))

223− <|> try (do reserved "Set"

224− return RSet)

223+ <|> try (do reserved "Type"

224+ return RType)

225225 <|> try (do x <- iName []

226226 return (Var x))

227227

src/Core/Elaborate.hs+3−3

@@ -446,8 +446,8 @@ simple_app fun arg =

446446 b <- unique_hole (MN 0 "b")

447447 f <- unique_hole (MN 0 "f")

448448 s <- unique_hole (MN 0 "s")

449− claim a RSet

450− claim b RSet

449+ claim a RType

450+ claim b RType

451451 claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))

452452 start_unify s

453453 claim s (Var a)

@@ -471,7 +471,7 @@ simple_app fun arg =

471471-- which we'll fill with the argument type too.

472472arg :: Name -> Name -> Elab' aux ()

473473arg n tyhole = do ty <- unique_hole tyhole

474− claim ty RSet

474+ claim ty RType

475475 forall n (Var ty)

476476

477477-- Try a tactic, if it fails, try another

src/Core/Evaluate.hs+9−9

@@ -49,7 +49,7 @@ data Value = VP NameType Name Value

4949 | VV Int

5050 | VBind Name (Binder Value) (Value -> Eval Value)

5151 | VApp Value Value

52− | VSet UExp

52+ | VType UExp

5353 | VErased

5454 | VConstant Const

5555-- | VLazy Env [Value] Term

@@ -59,7 +59,7 @@ data HNF = HP NameType Name (TT Name)

5959 | HV Int

6060 | HBind Name (Binder HNF) (HNF -> Eval HNF)

6161 | HApp HNF [HNF] [TT Name]

62− | HSet UExp

62+ | HType UExp

6363 | HConstant Const

6464 | HTmp Int

6565 deriving Show

@@ -228,7 +228,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

228228 evApply ntimes stk top env [a'] f'

229229 ev ntimes stk top env (Constant c) = return $ VConstant c

230230 ev ntimes stk top env Erased = return VErased

231− ev ntimes stk top env (Set i) = return $ VSet i

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

232232

233233 evApply ntimes stk top env args (VApp f a) =

234234 evApply ntimes stk top env (a:args) f

@@ -370,7 +370,7 @@ instance Quote Value where

370370 liftM (Bind n b') (quote (i+1) sc')

371371 where quoteB t = fmapMB (quote i) t

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

373− quote i (VSet u) = return $ Set u

373+ quote i (VType u) = return $ TType u

374374 quote i VErased = return $ Erased

375375 quote i (VConstant c) = return $ Constant c

376376 quote i (VTmp x) = return $ V (i - x - 1)

@@ -388,7 +388,7 @@ instance Quote HNF where

388388 where iEnv [] a = return a

389389 iEnv (x:xs) a = do x' <- quote i x

390390 iEnv xs (weakenTm (-1) (instantiate x' a))

391− quote i (HSet u) = return $ Set u

391+ quote i (HType u) = return $ TType u

392392 quote i (HConstant c) = return $ Constant c

393393 quote i (HTmp x) = return $ V (i - x - 1)

394394

@@ -438,7 +438,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

438438 where hbind env t = fmapMB (\tm -> ev env (finalise tm)) t

439439 ev env (App f a) = evApply env [a] f

440440 ev env (Constant c) = return $ HConstant c

441− ev env (Set i) = return $ HSet i

441+ ev env (TType i) = return $ HType i

442442

443443 evApply env args (App f a) = evApply env (a : args) f

444444 evApply env args f = do f' <- ev env f

@@ -550,9 +550,9 @@ convEq ctxt = ceq [] where

550550 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')

551551 ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)

552552 ceq ps (Constant x) (Constant y) = return (x == y)

553− ceq ps (Set x) (Set y) = do (v, cs) <- get

554− put (v, ULE x y : cs)

555− return True

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

554+ put (v, ULE x y : cs)

555+ return True

556556 ceq ps Erased _ = return True

557557 ceq ps _ Erased = return True

558558 ceq ps _ _ = return False

src/Core/ProofShell.hs+1−1

@@ -26,7 +26,7 @@ processCommand :: Command -> ShellState -> (ShellState, String)

2626processCommand (Theorem n ty) state

2727 = case check (ctxt state) [] ty of

2828 OK (gl, t) ->

29− case isSet (ctxt state) [] t of

29+ case isType (ctxt state) [] t of

3030 OK _ -> (state { prf = Just (newProof n (ctxt state) gl) }, "")

3131 _ -> (state, "Goal is not a type")

3232 err -> (state, show err)

src/Core/ProofState.hs+5−5

@@ -236,7 +236,7 @@ attack ctxt env _ = fail "Not an attackable hole"

236236claim :: Name -> Raw -> RunTactic

237237claim n ty ctxt env t =

238238 do (tyv, tyt) <- lift $ check ctxt env ty

239− lift $ isSet ctxt env tyt

239+ lift $ isType ctxt env tyt

240240 action (\ps -> let (g:gs) = holes ps in

241241 ps { holes = g : n : gs } )

242242 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)

@@ -418,8 +418,8 @@ intro n ctxt env _ = fail "Can't introduce here."

418418forall :: Name -> Raw -> RunTactic

419419forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

420420 do (tyv, tyt) <- lift $ check ctxt env ty

421− lift $ isSet ctxt env tyt

422− lift $ isSet ctxt env t

421+ lift $ isType ctxt env tyt

422+ lift $ isType ctxt env t

423423 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))

424424forall n ty ctxt env _ = fail "Can't pi bind here"

425425

@@ -433,7 +433,7 @@ letbind :: Name -> Raw -> Raw -> RunTactic

433433letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

434434 do (tyv, tyt) <- lift $ check ctxt env ty

435435 (valv, valt) <- lift $ check ctxt env val

436− lift $ isSet ctxt env tyt

436+ lift $ isType ctxt env tyt

437437 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))

438438letbind n ty val ctxt env _ = fail "Can't let bind here"

439439

@@ -446,7 +446,7 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

446446 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)

447447 let newt = mkP l r l t

448448 let sc = forget $ (Bind x (Hole newt)

449− (mkApp (P Ref (UN "replace") (Set (UVal 0)))

449+ (mkApp (P Ref (UN "replace") (TType (UVal 0)))

450450 [lt, l, r, p, tmv, xp]))

451451 (scv, sct) <- lift $ check ctxt env sc

452452 return scv

src/Core/TT.hs+12−12

@@ -14,7 +14,7 @@ import Util.Pretty hiding (Str)

1414

1515{- The language has:

1616 * Full dependent types

17− * A hierarchy of universes, with cumulativity: Set : Set1, Set1 : Set2, ...

17+ * A hierarchy of universes, with cumulativity: Type : Type1, Type1 : Type2, ...

1818 * Pattern matching letrec binding

1919 * (primitive types defined externally)

2020

@@ -25,7 +25,7 @@ import Util.Pretty hiding (Str)

2525 programs with implicit syntax into fully explicit terms.

2626-}

2727

28−data Option = SetInSet

28+data Option = TTypeInTType

2929 | CheckConv

3030 deriving Eq

3131

@@ -123,7 +123,7 @@ instance Show a => Show (TC a) where

123123 show (Error str) = "Error: " ++ show str

124124

125125-- at some point, this instance should also carry type checking options

126−-- (e.g. Set:Set)

126+-- (e.g. Type:Type)

127127

128128instance Monad TC where

129129 return = OK

@@ -291,7 +291,7 @@ instance Pretty Const where

291291data Raw = Var Name

292292 | RBind Name (Binder Raw) Raw

293293 | RApp Raw Raw

294− | RSet

294+ | RType

295295 | RForce Raw

296296 | RConstant Const

297297 deriving (Show, Eq)

@@ -300,7 +300,7 @@ instance Sized Raw where

300300 size (Var name) = 1

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

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

303− size RSet = 1

303+ size RType = 1

304304 size (RForce raw) = 1 + size raw

305305 size (RConstant const) = size const

306306

@@ -434,7 +434,7 @@ data TT n = P NameType n (TT n) -- embed type

434434 | Proj (TT n) Int -- argument projection; runtime only

435435 | Erased

436436 | Impossible -- special case for totality checking

437− | Set UExp

437+ | TType UExp

438438 deriving (Ord, Functor)

439439{-!

440440deriving instance Binary TT

@@ -465,7 +465,7 @@ instance Sized a => Sized (TT a) where

465465 size (App l r) = 1 + size l + size r

466466 size (Constant c) = size c

467467 size Erased = 1

468− size (Set u) = 1 + size u

468+ size (TType u) = 1 + size u

469469

470470instance Pretty a => Pretty (TT a) where

471471 pretty _ = text "test"

@@ -483,7 +483,7 @@ instance Eq n => Eq (TT n) where

483483 (==) (V x) (V y) = x == y

484484 (==) (Bind _ xb xs) (Bind _ yb ys) = xb == yb && xs == ys

485485 (==) (App fx ax) (App fy ay) = fx == fy && ax == ay

486− (==) (Set _) (Set _) = True -- deal with constraints later

486+ (==) (TType _) (TType _) = True -- deal with constraints later

487487 (==) (Constant x) (Constant y) = x == y

488488 (==) (Proj x i) (Proj y j) = x == y && i == j

489489 (==) Erased _ = True

@@ -496,7 +496,7 @@ isInjective :: TT n -> Bool

496496isInjective (P (DCon _ _) _ _) = True

497497isInjective (P (TCon _ _) _ _) = True

498498isInjective (Constant _) = True

499−isInjective (Set x) = True

499+isInjective (TType x) = True

500500isInjective (Bind _ (Pi _) sc) = True

501501isInjective (App f a) = isInjective f

502502isInjective _ = False

@@ -610,7 +610,7 @@ forget tm = fe [] tm

610610 fe env (App f a) = RApp (fe env f) (fe env a)

611611 fe env (Constant c)

612612 = RConstant c

613− fe env (Set i) = RSet

613+ fe env (TType i) = RType

614614 fe env Erased = RConstant Forgot

615615

616616bindAll :: [(n, Binder (TT n))] -> TT n -> TT n

@@ -719,7 +719,7 @@ prettyEnv env t = prettyEnv' env t False

719719 prettySe 1 env x debug <+> text ("!" ++ show i)

720720 prettySe p env (Constant c) debug = pretty c

721721 prettySe p env Erased debug = text "[_]"

722− prettySe p env (Set i) debug = text "Set" <+> (text . show $ i)

722+ prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)

723723

724724 prettySb env n (Lam t) = prettyB env "λ" "=>" n t

725725 prettySb env n (Hole t) = prettyB env "?defer" "." n t

@@ -751,7 +751,7 @@ showEnv' env t dbg = se 10 env t where

751751 se p env (Constant c) = show c

752752 se p env Erased = "[__]"

753753 se p env Impossible = "[impossible]"

754− se p env (Set i) = "Set " ++ show i

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

755755

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

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

src/Core/Typecheck.hs+23−23

@@ -38,10 +38,10 @@ converts ctxt env x y

3838

3939errEnv = map (\(x, b) -> (x, binderTy b))

4040

41−isSet :: Context -> Env -> Term -> TC ()

42−isSet ctxt env tm = isSet' (normalise ctxt env tm)

43− where isSet' (Set _) = return ()

44− isSet' tm = fail (showEnv env tm ++ " is not a Set")

41+isType :: Context -> Env -> Term -> TC ()

42+isType ctxt env tm = isType' (normalise ctxt env tm)

43+ where isType' (TType _) = return ()

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

4545

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

4747recheck ctxt env tm orig

@@ -87,12 +87,12 @@ check' holes ctxt env top = chk env top where

8787 where renameBinders i (Bind x (Pi s) t) = Bind (MN i "binder") (Pi s)

8888 (renameBinders (i+1) t)

8989 renameBinders i sc = sc

90− chk env RSet

91− | holes = return (Set (UVal 0), Set (UVal 0))

90+ chk env RType

91+ | holes = return (TType (UVal 0), TType (UVal 0))

9292 | otherwise = do (v, cs) <- get

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

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

95− return (Set (UVar v), Set (UVar (v+1)))

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

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

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

9898 where constType (I _) = Constant IType

@@ -103,18 +103,18 @@ check' holes ctxt env top = chk env top where

103103 constType (W8 _) = Constant W8Type

104104 constType (W16 _) = Constant W16Type

105105 constType Forgot = Erased

106− constType _ = Set (UVal 0)

106+ constType _ = TType (UVal 0)

107107 chk env (RForce t) = do (_, ty) <- chk env t

108108 return (Erased, ty)

109109 chk env (RBind n (Pi s) t)

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

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

112112 (v, cs) <- get

113− let Set su = normalise ctxt env st

114− let Set tu = normalise ctxt env tt

113+ let TType su = normalise ctxt env st

114+ let TType tu = normalise ctxt env tt

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

116116 return (Bind n (Pi (uniqueBinders (map fst env) sv))

117− (pToV n tv), Set (UVar v))

117+ (pToV n tv), TType (UVar v))

118118 chk env (RBind n b sc)

119119 = do b' <- checkBinder b

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

@@ -123,13 +123,13 @@ check' holes ctxt env top = chk env top where

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

124124 let tv' = normalise ctxt env tv

125125 let tt' = normalise ctxt env tt

126− lift $ isSet ctxt env tt'

126+ lift $ isType ctxt env tt'

127127 return (Lam tv)

128128 checkBinder (Pi t)

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

130130 let tv' = normalise ctxt env tv

131131 let tt' = normalise ctxt env tt

132− lift $ isSet ctxt env tt'

132+ lift $ isType ctxt env tt'

133133 return (Pi tv)

134134 checkBinder (Let t v)

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

@@ -137,7 +137,7 @@ check' holes ctxt env top = chk env top where

137137 let tv' = normalise ctxt env tv

138138 let tt' = normalise ctxt env tt

139139 convertsC ctxt env vt tv

140− lift $ isSet ctxt env tt'

140+ lift $ isType ctxt env tt'

141141 return (Let tv vv)

142142 checkBinder (NLet t v)

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

@@ -145,7 +145,7 @@ check' holes ctxt env top = chk env top where

145145 let tv' = normalise ctxt env tv

146146 let tt' = normalise ctxt env tt

147147 convertsC ctxt env vt tv

148− lift $ isSet ctxt env tt'

148+ lift $ isType ctxt env tt'

149149 return (NLet tv vv)

150150 checkBinder (Hole t)

151151 | not holes = lift $ tfail (IncompleteTerm undefined)

@@ -153,13 +153,13 @@ check' holes ctxt env top = chk env top where

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

154154 let tv' = normalise ctxt env tv

155155 let tt' = normalise ctxt env tt

156− lift $ isSet ctxt env tt'

156+ lift $ isType ctxt env tt'

157157 return (Hole tv)

158158 checkBinder (GHole t)

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

160160 let tv' = normalise ctxt env tv

161161 let tt' = normalise ctxt env tt

162− lift $ isSet ctxt env tt'

162+ lift $ isType ctxt env tt'

163163 return (GHole tv)

164164 checkBinder (Guess t v)

165165 | not holes = lift $ tfail (IncompleteTerm undefined)

@@ -169,19 +169,19 @@ check' holes ctxt env top = chk env top where

169169 let tv' = normalise ctxt env tv

170170 let tt' = normalise ctxt env tt

171171 convertsC ctxt env vt tv

172− lift $ isSet ctxt env tt'

172+ lift $ isType ctxt env tt'

173173 return (Guess tv vv)

174174 checkBinder (PVar t)

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

176176 let tv' = normalise ctxt env tv

177177 let tt' = normalise ctxt env tt

178− lift $ isSet ctxt env tt'

178+ lift $ isType ctxt env tt'

179179 return (PVar tv)

180180 checkBinder (PVTy t)

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

182182 let tv' = normalise ctxt env tv

183183 let tt' = normalise ctxt env tt

184− lift $ isSet ctxt env tt'

184+ lift $ isType ctxt env tt'

185185 return (PVTy tv)

186186

187187 discharge n (Lam t) scv sct

@@ -221,17 +221,17 @@ checkProgram :: Context -> RProgram -> TC Context

221221checkProgram ctxt [] = return ctxt

222222checkProgram ctxt ((n, RConst t) : xs)

223223 = do (t', tt') <- trace (show n) $ check ctxt [] t

224− isSet ctxt [] tt'

224+ isType ctxt [] tt'

225225 checkProgram (addTyDecl n t' ctxt) xs

226226checkProgram ctxt ((n, RFunction (RawFun ty val)) : xs)

227227 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty

228228 (val', valt') <- check ctxt [] val

229− isSet ctxt [] tyt'

229+ isType ctxt [] tyt'

230230 converts ctxt [] ty' valt'

231231 checkProgram (addToCtxt n val' ty' ctxt) xs

232232checkProgram ctxt ((n, RData (RDatatype _ ty cons)) : xs)

233233 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty

234− isSet ctxt [] tyt'

234+ isType ctxt [] tyt'

235235 -- add the tycon temporarily so we can check constructors

236236 let ctxt' = addDatatype (Data n 0 ty' []) ctxt

237237 cons' <- mapM (checkCon ctxt') cons

src/IRTS/Compiler.hs+1−1

@@ -235,7 +235,7 @@ instance ToIR (TT Name) where

235235 ir' env (Proj t i) = do t' <- ir' env t

236236 return $ LProj t' i

237237 ir' env (Constant c) = return $ LConst c

238− ir' env (Set _) = return $ LNothing

238+ ir' env (TType _) = return $ LNothing

239239 ir' env Erased = return $ LNothing

240240 ir' env Impossible = return $ LNothing

241241-- ir' env _ = return $ LError "Impossible"

src/Idris/AbsSyntax.hs+4−4

@@ -352,9 +352,9 @@ logLvl l str = do i <- get

352352 $ do liftIO (putStrLn str)

353353 put (i { idris_log = idris_log i ++ str ++ "\n" } )

354354

355−cmdOptSet :: Opt -> Idris Bool

356−cmdOptSet x = do i <- get

357− return $ x `elem` opt_cmdline (idris_options i)

355+cmdOptType :: Opt -> Idris Bool

356+cmdOptType x = do i <- get

357+ return $ x `elem` opt_cmdline (idris_options i)

358358

359359iLOG :: String -> Idris ()

360360iLOG = logLvl 1

@@ -385,7 +385,7 @@ inferDecl = PDatadecl inferTy

385385 (PRef bi inferTy)), bi)]

386386

387387infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]

388−infP = P (TCon 6 0) inferTy (Set (UVal 0))

388+infP = P (TCon 6 0) inferTy (TType (UVal 0))

389389

390390getInferTerm, getInferType :: Term -> Term

391391getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

src/Idris/AbsSyntaxTree.hs+2−2

@@ -873,7 +873,7 @@ prettyImp impl = prettySe 10

873873 where

874874 prettyAs =

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

876− prettySe p PType = text "Set"

876+ prettySe p PType = text "Type"

877877 prettySe p (PConstant c) = pretty c

878878 -- XXX: add pretty for tactics

879879 prettySe p (PProof ts) =

@@ -965,7 +965,7 @@ showImp impl tm = se 10 tm where

965965 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

966966 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

967967 se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"

968− se p PType = "Set"

968+ se p PType = "Type"

969969 se p (PConstant c) = show c

970970 se p (PProof ts) = "proof { " ++ show ts ++ "}"

971971 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"

src/Idris/Compiler.hs+1−1

@@ -147,7 +147,7 @@ instance ToEpic (TT Name) where

147147 return (f' @@ a')

148148 epic' env (Constant c) = epic c

149149 epic' env Erased = return impossible

150− epic' env (Set _) = return impossible

150+ epic' env (TType _) = return impossible

151151

152152 epicCon env t arity n args

153153 | length args == arity = buildApp env (con_ t) args

src/Idris/Coverage.hs+1−1

@@ -360,7 +360,7 @@ checkTotality path fc n

360360 case t' of

361361 Total _ -> return t'

362362 Productive -> return t'

363− e -> do w <- cmdOptSet WarnPartial

363+ e -> do w <- cmdOptType WarnPartial

364364 if TotalFn `elem` opts

365365 then totalityError t'

366366 else do when (w && not (PartialFn `elem` opts)) $

src/Idris/Delaborate.hs+1−1

@@ -38,7 +38,7 @@ delab' ist tm fullname = de [] tm

3838 de env (Constant i) = PConstant i

3939 de env Erased = Placeholder

4040 de env Impossible = Placeholder

41− de env (Set i) = PType

41+ de env (TType i) = PType

4242

4343 dens x | fullname = x

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

src/Idris/ElabDecls.hs+10−10

@@ -49,7 +49,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

4949 ty' <- implicit syn n ty'

5050 let ty = addImpl i ty'

5151 logLvl 2 $ show n ++ " type " ++ showImp True ty

52− ((tyT, defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []

52+ ((tyT, defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

5353 (erun fc (build i info False n ty))

5454 ds <- checkDef fc defer

5555 addDeferred ds

@@ -113,7 +113,7 @@ elabData info syn doc fc codata (PLaterdecl n t_in)

113113 i <- get

114114 t_in <- implicit syn n t_in

115115 let t = addImpl i t_in

116− ((t', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []

116+ ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

117117 (erun fc (build i info False n t))

118118 def' <- checkDef fc defer

119119 addDeferred def'

@@ -129,7 +129,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

129129 i <- get

130130 t_in <- implicit syn n t_in

131131 let t = addImpl i t_in

132− ((t', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []

132+ ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

133133 (erun fc (build i info False n t))

134134 def' <- checkDef fc defer

135135 addDeferred def'

@@ -218,9 +218,9 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

218218 mkImp (MN i n) = MN i ("implicit_" ++ n)

219219 mkImp (NS n s) = NS (mkImp n) s

220220

221− mkSet (UN n) = UN ("set_" ++ n)

222− mkSet (MN i n) = MN i ("set_" ++ n)

223− mkSet (NS n s) = NS (mkSet n) s

221+ mkType (UN n) = UN ("set_" ++ n)

222+ mkType (MN i n) = MN i ("set_" ++ n)

223+ mkType (NS n s) = NS (mkType n) s

224224

225225 mkProj recty substs cimp ((pn_in, pty), pos)

226226 = do let pn = expandNS syn pn_in

@@ -241,7 +241,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

241241 implicitise (pa, t) = pa { getTm = t }

242242

243243 mkUpdate recty k num ((pn, pty), pos)

244− = do let setname = expandNS syn $ mkSet pn

244+ = do let setname = expandNS syn $ mkType pn

245245 let valname = MN 0 "updateval"

246246 let pt = k (PPi expl pn pty

247247 (PPi expl rec recty recty))

@@ -269,7 +269,7 @@ elabCon info syn tn codata (doc, n, t_in, fc)

269269 t_in <- implicit syn n (if codata then mkLazy t_in else t_in)

270270 let t = addImpl i t_in

271271 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True t

272− ((t', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []

272+ ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

273273 (erun fc (build i info False n t))

274274 logLvl 2 $ "Rechecking " ++ show t'

275275 def' <- checkDef fc defer

@@ -449,11 +449,11 @@ elabVal info aspat tm_in

449449 logLvl 10 (showImp True tm)

450450 -- try:

451451 -- * ordinary elaboration

452− -- * elaboration as a Set

452+ -- * elaboration as a Type

453453 -- * elaboration as a function a -> b

454454

455455 ((tm', defer, is), _) <-

456− tctry (elaborate ctxt (MN 0 "val") (Set (UVal 0)) []

456+ tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []

457457 (build i info aspat (MN 0 "val") tm))

458458 (elaborate ctxt (MN 0 "val") infP []

459459 (build i info aspat (MN 0 "val") (infTerm tm)))

src/Idris/ElabTerm.hs+9−9

@@ -101,7 +101,7 @@ elab ist info pattern tcgen fn tm

101101 local f = do e <- get_env

102102 return (f `elem` map fst e)

103103

104− elab' ina PType = do apply RSet []; solve

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

105105 elab' ina (PConstant c) = do apply (RConstant c) []; solve

106106 elab' ina (PQuote r) = do fill r; solve

107107 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))

@@ -191,7 +191,7 @@ elab ist info pattern tcgen fn tm

191191 = do hsin <- get_holes

192192 ptmin <- get_term

193193 tyn <- unique_hole (MN 0 "lamty")

194− claim tyn RSet

194+ claim tyn RType

195195 attack

196196 ptm <- get_term

197197 hs <- get_holes

@@ -209,7 +209,7 @@ elab ist info pattern tcgen fn tm

209209 = do attack; arg n (MN 0 "ty"); elabE (True, a) sc; solve

210210 elab' ina@(_,a) (PPi _ n ty sc)

211211 = do attack; tyn <- unique_hole (MN 0 "ty")

212− claim tyn RSet

212+ claim tyn RType

213213 n' <- case n of

214214 MN _ _ -> unique_hole n

215215 _ -> return n

@@ -221,7 +221,7 @@ elab ist info pattern tcgen fn tm

221221 elab' ina@(_,a) (PLet n ty val sc)

222222 = do attack;

223223 tyn <- unique_hole (MN 0 "letty")

224− claim tyn RSet

224+ claim tyn RType

225225 valn <- unique_hole (MN 0 "letval")

226226 claim valn (Var tyn)

227227 letbind n (Var tyn) (Var valn)

@@ -257,7 +257,7 @@ elab ist info pattern tcgen fn tm

257257 claimArgTys env (_ : xs)

258258 = do an <- unique_hole (MN 0 "inf_argTy")

259259 aval <- unique_hole (MN 0 "inf_arg")

260− claim an RSet

260+ claim an RType

261261 claim aval (Var an)

262262 ans <- claimArgTys env xs

263263 return ((aval, (True, (Var an))) : ans)

@@ -338,7 +338,7 @@ elab ist info pattern tcgen fn tm

338338 elab' ina@(_, a) c@(PCase fc scr opts)

339339 = do attack

340340 tyn <- unique_hole (MN 0 "scty")

341− claim tyn RSet

341+ claim tyn RType

342342 valn <- unique_hole (MN 0 "scval")

343343 scvn <- unique_hole (MN 0 "scvar")

344344 claim valn (Var tyn)

@@ -592,7 +592,7 @@ runTac autoSolve ist tac = do env <- get_env

592592 = do attack; -- (h:_) <- get_holes

593593 tyn <- unique_hole (MN 0 "rty")

594594 -- start_unify h

595− claim tyn RSet

595+ claim tyn RType

596596 valn <- unique_hole (MN 0 "rval")

597597 claim valn (Var tyn)

598598 letn <- unique_hole (MN 0 "rewrite_rule")

@@ -604,7 +604,7 @@ runTac autoSolve ist tac = do env <- get_env

604604 runT (LetTac n tm)

605605 = do attack

606606 tyn <- unique_hole (MN 0 "letty")

607− claim tyn RSet

607+ claim tyn RType

608608 valn <- unique_hole (MN 0 "letval")

609609 claim valn (Var tyn)

610610 letn <- unique_hole n

@@ -615,7 +615,7 @@ runTac autoSolve ist tac = do env <- get_env

615615 runT (LetTacTy n ty tm)

616616 = do attack

617617 tyn <- unique_hole (MN 0 "letty")

618− claim tyn RSet

618+ claim tyn RType

619619 valn <- unique_hole (MN 0 "letval")

620620 claim valn (Var tyn)

621621 letn <- unique_hole n

src/Idris/IBC.hs+5−5

@@ -402,7 +402,7 @@ instance Binary Raw where

402402 RApp x1 x2 -> do putWord8 2

403403 put x1

404404 put x2

405− RSet -> putWord8 3

405+ RType -> putWord8 3

406406 RConstant x1 -> do putWord8 4

407407 put x1

408408 RForce x1 -> do putWord8 5

@@ -419,7 +419,7 @@ instance Binary Raw where

419419 2 -> do x1 <- get

420420 x2 <- get

421421 return (RApp x1 x2)

422− 3 -> return RSet

422+ 3 -> return RType

423423 4 -> do x1 <- get

424424 return (RConstant x1)

425425 5 -> do x1 <- get

@@ -525,8 +525,8 @@ instance (Binary n) => Binary (TT n) where

525525 put x1

526526 put x2

527527 Erased -> putWord8 6

528− Set x1 -> do putWord8 7

529− put x1

528+ TType x1 -> do putWord8 7

529+ put x1

530530 Impossible -> putWord8 8

531531 get

532532 = do i <- getWord8

@@ -551,7 +551,7 @@ instance (Binary n) => Binary (TT n) where

551551 return (Proj x1 x2)

552552 6 -> return Erased

553553 7 -> do x1 <- get

554− return (Set x1)

554+ return (TType x1)

555555 8 -> return Impossible

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

557557

src/Idris/Parser.hs+16−16

@@ -599,7 +599,7 @@ pSimpleExtExpr syn = do i <- getState

599599

600600pNoExtExpr syn =

601601 try (pApp syn)

602− <|> pRecordSet syn

602+ <|> pRecordType syn

603603 <|> try (pSimpleExpr syn)

604604 <|> pLambda syn

605605 <|> pLet syn

@@ -879,10 +879,10 @@ pConstraintArg syn = do symbol "@{"

879879 symbol "}"

880880 return (pconst e)

881881

882−pRecordSet syn

882+pRecordType syn

883883 = do reserved "record"

884884 lchar '{'

885− fields <- sepBy1 pFieldSet (lchar ',')

885+ fields <- sepBy1 pFieldType (lchar ',')

886886 lchar '}'

887887 fc <- pfc

888888 rec <- option Nothing (do e <- pSimpleExpr syn

@@ -892,17 +892,17 @@ pRecordSet syn

892892 return (PLam (MN 0 "fldx") Placeholder

893893 (applyAll fc fields (PRef fc (MN 0 "fldx"))))

894894 Just v -> return (applyAll fc fields v)

895− where pFieldSet = do n <- pfName

896− lchar '='

897− e <- pExpr syn

898− return (n, e)

895+ where pFieldType = do n <- pfName

896+ lchar '='

897+ e <- pExpr syn

898+ return (n, e)

899899 applyAll fc [] x = x

900900 applyAll fc ((n, e) : es) x

901− = applyAll fc es (PApp fc (PRef fc (mkSet n)) [pexp e, pexp x])

901+ = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])

902902

903−mkSet (UN n) = UN ("set_" ++ n)

904−mkSet (MN 0 n) = MN 0 ("set_" ++ n)

905−mkSet (NS n s) = NS (mkSet n) s

903+mkType (UN n) = UN ("set_" ++ n)

904+mkType (MN 0 n) = MN 0 ("set_" ++ n)

905+mkType (NS n s) = NS (mkType n) s

906906

907907noImp syn = syn { implicitAllowed = False }

908908impOK syn = syn { implicitAllowed = True }

@@ -1156,7 +1156,7 @@ pRecord syn = do acc <- pAccessibility

11561156 mapM_ (\n -> addAcc n acc) fns

11571157 return $ PRecord "" rsyn fc tyn ty cdoc cn cty

11581158 where

1159− getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkSet n)]

1159+ getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]

11601160 ++ getRecNames syn sc

11611161 getRecNames _ _ = []

11621162

@@ -1201,11 +1201,11 @@ pData syn = try (do doc <- option "" (pDocComment '|')

12011201 let n = show tyn_in ++ " "

12021202 let s = kw ++ n

12031203 let as = concat (intersperse " " $ map show args) ++ " "

1204− let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Set)") . show) args)

1205− let ss = concat (intersperse " -> " $ map (const "Set") args)

1204+ let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)

1205+ let ss = concat (intersperse " -> " $ map (const "Type") args)

12061206 let fix1 = s ++ as ++ " = ..."

1207− let fix2 = s ++ ": " ++ ns ++ " -> Set where\n ..."

1208− let fix3 = s ++ ": " ++ ss ++ " -> Set where\n ..."

1207+ let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

1208+ let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

12091209 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

12101210

12111211 cons <- sepBy1 (pSimpleCon syn) (lchar '|')

src/Idris/Primitives.hs+2−2

@@ -23,8 +23,8 @@ data Prim = Prim { p_name :: Name,

2323ty [] x = Constant x

2424ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)

2525

26−believeTy = Bind (UN "a") (Pi (Set (UVar (-2))))

27− (Bind (UN "b") (Pi (Set (UVar (-2))))

26+believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))

27+ (Bind (UN "b") (Pi (TType (UVar (-2))))

2828 (Bind (UN "x") (Pi (V 1)) (V 1)))

2929

3030total = Total []

src/Main.hs+2−2

@@ -86,10 +86,10 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

8686 "\t--total Require functions to be total by default\n" ++

8787 "\t--warnpartial Warn about undeclared partial functions\n" ++

8888 "\t--typeintype Disable universe checking\n" ++

89− "\t--log [level] Set debugging log level\n" ++

89+ "\t--log [level] Type debugging log level\n" ++

9090 "\t-S Do no further compilation of code generator output\n" ++

9191 "\t-c Compile to object files rather than an executable\n" ++

9292 "\t--libdir Show library install directory and exit\n" ++

9393 "\t--link Show C library directories and exit (for C linking)\n" ++

9494 "\t--include Show C include directories and exit (for C linking)\n" ++

95− "\t--target [target] Set the target: C, Java, bytecode\n"

95+ "\t--target [target] Type the target: C, Java, bytecode\n"