dd5001f · Idris-dev · git.iko.soy

src/Core/CoreParser.hs+2−2

compare with master

unifiedsplit

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

220 lchar '.';

221 sc <- pTerm

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

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

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

224− return RSet)

224+ return RType)

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

226 return (Var x))

227

src/Core/Elaborate.hs+3−3

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

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

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

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

449− claim a RSet

449+ claim a RType

450− claim b RSet

450+ claim b RType

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

452 start_unify s

453 claim s (Var a)

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

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

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

473arg n tyhole = do ty <- unique_hole tyhole

474− claim ty RSet

474+ claim ty RType

475 forall n (Var ty)

476

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

src/Core/Evaluate.hs+9−9

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

49 | VV Int

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

51 | VApp Value Value

52− | VSet UExp

52+ | VType UExp

53 | VErased

54 | VConstant Const

55-- | VLazy Env [Value] Term

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

59 | HV Int

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

61 | HApp HNF [HNF] [TT Name]

62− | HSet UExp

62+ | HType UExp

63 | HConstant Const

64 | HTmp Int

65 deriving Show

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

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

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

230 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

232

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

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

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

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

371 where quoteB t = fmapMB (quote i) t

372 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

374 quote i VErased = return $ Erased

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

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

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

388 where iEnv [] a = return a

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

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

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

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

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

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

394

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

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

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

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

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

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

442

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

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

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

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

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

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

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

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

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

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

555− return True

555+ return True

556 ceq ps Erased _ = return True

557 ceq ps _ Erased = return True

558 ceq ps _ _ = return False

src/Core/ProofShell.hs+1−1

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

26processCommand (Theorem n ty) state

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

28 OK (gl, t) ->

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

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

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

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

32 err -> (state, show err)

src/Core/ProofState.hs+5−5

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

236claim :: Name -> Raw -> RunTactic

237claim n ty ctxt env t =

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

239− lift $ isSet ctxt env tyt

239+ lift $ isType ctxt env tyt

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

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

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

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

418forall :: Name -> Raw -> RunTactic

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

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

421− lift $ isSet ctxt env tyt

421+ lift $ isType ctxt env tyt

422− lift $ isSet ctxt env t

422+ lift $ isType ctxt env t

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

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

425

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

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

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

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

436− lift $ isSet ctxt env tyt

436+ lift $ isType ctxt env tyt

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

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

439

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

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

447 let newt = mkP l r l t

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

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

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

452 return scv

src/Core/TT.hs+12−12

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

14

15{- The language has:

16 * 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, ...

18 * Pattern matching letrec binding

19 * (primitive types defined externally)

20

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

25 programs with implicit syntax into fully explicit terms.

26-}

27

28−data Option = SetInSet

28+data Option = TTypeInTType

29 | CheckConv

30 deriving Eq

31

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

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

124

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

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

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

127

128instance Monad TC where

129 return = OK

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

291data Raw = Var Name

292 | RBind Name (Binder Raw) Raw

293 | RApp Raw Raw

294− | RSet

294+ | RType

295 | RForce Raw

296 | RConstant Const

297 deriving (Show, Eq)

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

300 size (Var name) = 1

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

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

303− size RSet = 1

303+ size RType = 1

304 size (RForce raw) = 1 + size raw

305 size (RConstant const) = size const

306

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

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

435 | Erased

436 | Impossible -- special case for totality checking

437− | Set UExp

437+ | TType UExp

438 deriving (Ord, Functor)

439{-!

440deriving instance Binary TT

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

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

466 size (Constant c) = size c

467 size Erased = 1

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

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

469

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

471 pretty _ = text "test"

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

483 (==) (V x) (V y) = x == y

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

485 (==) (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

487 (==) (Constant x) (Constant y) = x == y

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

489 (==) Erased _ = True

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

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

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

498isInjective (Constant _) = True

499−isInjective (Set x) = True

499+isInjective (TType x) = True

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

501isInjective (App f a) = isInjective f

502isInjective _ = False

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

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

611 fe env (Constant c)

612 = RConstant c

613− fe env (Set i) = RSet

613+ fe env (TType i) = RType

614 fe env Erased = RConstant Forgot

615

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

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

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

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

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

723

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

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

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

751 se p env (Constant c) = show c

752 se p env Erased = "[__]"

753 se p env Impossible = "[impossible]"

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

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

755

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

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

src/Core/Typecheck.hs+23−23

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

38

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

40

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

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

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

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

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

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

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

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

45

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

47recheck ctxt env tm orig

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

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

88 (renameBinders (i+1) t)

89 renameBinders i sc = sc

90− chk env RSet

90+ chk env RType

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

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

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

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

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

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

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

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

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

98 where constType (I _) = Constant IType

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

103 constType (W8 _) = Constant W8Type

104 constType (W16 _) = Constant W16Type

105 constType Forgot = Erased

106− constType _ = Set (UVal 0)

106+ constType _ = TType (UVal 0)

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

108 return (Erased, ty)

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

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

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

112 (v, cs) <- get

113− let Set su = normalise ctxt env st

113+ let TType su = normalise ctxt env st

114− let Set tu = normalise ctxt env tt

114+ let TType tu = normalise ctxt env tt

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

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

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

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

118 chk env (RBind n b sc)

119 = do b' <- checkBinder b

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

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

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

124 let tv' = normalise ctxt env tv

125 let tt' = normalise ctxt env tt

126− lift $ isSet ctxt env tt'

126+ lift $ isType ctxt env tt'

127 return (Lam tv)

128 checkBinder (Pi t)

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

130 let tv' = normalise ctxt env tv

131 let tt' = normalise ctxt env tt

132− lift $ isSet ctxt env tt'

132+ lift $ isType ctxt env tt'

133 return (Pi tv)

134 checkBinder (Let t v)

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

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

137 let tv' = normalise ctxt env tv

138 let tt' = normalise ctxt env tt

139 convertsC ctxt env vt tv

140− lift $ isSet ctxt env tt'

140+ lift $ isType ctxt env tt'

141 return (Let tv vv)

142 checkBinder (NLet t v)

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

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

145 let tv' = normalise ctxt env tv

146 let tt' = normalise ctxt env tt

147 convertsC ctxt env vt tv

148− lift $ isSet ctxt env tt'

148+ lift $ isType ctxt env tt'

149 return (NLet tv vv)

150 checkBinder (Hole t)

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

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

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

154 let tv' = normalise ctxt env tv

155 let tt' = normalise ctxt env tt

156− lift $ isSet ctxt env tt'

156+ lift $ isType ctxt env tt'

157 return (Hole tv)

158 checkBinder (GHole t)

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

160 let tv' = normalise ctxt env tv

161 let tt' = normalise ctxt env tt

162− lift $ isSet ctxt env tt'

162+ lift $ isType ctxt env tt'

163 return (GHole tv)

164 checkBinder (Guess t v)

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

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

169 let tv' = normalise ctxt env tv

170 let tt' = normalise ctxt env tt

171 convertsC ctxt env vt tv

172− lift $ isSet ctxt env tt'

172+ lift $ isType ctxt env tt'

173 return (Guess tv vv)

174 checkBinder (PVar t)

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

176 let tv' = normalise ctxt env tv

177 let tt' = normalise ctxt env tt

178− lift $ isSet ctxt env tt'

178+ lift $ isType ctxt env tt'

179 return (PVar tv)

180 checkBinder (PVTy t)

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

182 let tv' = normalise ctxt env tv

183 let tt' = normalise ctxt env tt

184− lift $ isSet ctxt env tt'

184+ lift $ isType ctxt env tt'

185 return (PVTy tv)

186

187 discharge n (Lam t) scv sct

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

221checkProgram ctxt [] = return ctxt

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

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

224− isSet ctxt [] tt'

224+ isType ctxt [] tt'

225 checkProgram (addTyDecl n t' ctxt) xs

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

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

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

229− isSet ctxt [] tyt'

229+ isType ctxt [] tyt'

230 converts ctxt [] ty' valt'

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

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

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

234− isSet ctxt [] tyt'

234+ isType ctxt [] tyt'

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

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

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

src/IRTS/Compiler.hs+1−1

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

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

236 return $ LProj t' i

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

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

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

239 ir' env Erased = return $ LNothing

240 ir' env Impossible = return $ LNothing

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

src/Idris/AbsSyntax.hs+4−4

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

352 $ do liftIO (putStrLn str)

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

354

355−cmdOptSet :: Opt -> Idris Bool

355+cmdOptType :: Opt -> Idris Bool

356−cmdOptSet x = do i <- get

356+cmdOptType x = do i <- get

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

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

358

359iLOG :: String -> Idris ()

360iLOG = logLvl 1

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

385 (PRef bi inferTy)), bi)]

386

387infTerm 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))

389

390getInferTerm, getInferType :: Term -> Term

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

src/Idris/AbsSyntaxTree.hs+2−2

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

873 where

874 prettyAs =

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

876− prettySe p PType = text "Set"

876+ prettySe p PType = text "Type"

877 prettySe p (PConstant c) = pretty c

878 -- XXX: add pretty for tactics

879 prettySe p (PProof ts) =

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

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

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

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

968− se p PType = "Set"

968+ se p PType = "Type"

969 se p (PConstant c) = show c

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

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

src/Idris/Compiler.hs+1−1

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

147 return (f' @@ a')

148 epic' env (Constant c) = epic c

149 epic' env Erased = return impossible

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

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

151

152 epicCon env t arity n args

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

src/Idris/Coverage.hs+1−1

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

360 case t' of

361 Total _ -> return t'

362 Productive -> return t'

363− e -> do w <- cmdOptSet WarnPartial

363+ e -> do w <- cmdOptType WarnPartial

364 if TotalFn `elem` opts

365 then totalityError t'

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

src/Idris/Delaborate.hs+1−1

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

38 de env (Constant i) = PConstant i

39 de env Erased = Placeholder

40 de env Impossible = Placeholder

41− de env (Set i) = PType

41+ de env (TType i) = PType

42

43 dens x | fullname = x

44 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

49 ty' <- implicit syn n ty'

50 let ty = addImpl i ty'

51 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)) []

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

54 ds <- checkDef fc defer

55 addDeferred ds

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

113 i <- get

114 t_in <- implicit syn n t_in

115 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)) []

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

118 def' <- checkDef fc defer

119 addDeferred def'

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

129 i <- get

130 t_in <- implicit syn n t_in

131 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)) []

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

134 def' <- checkDef fc defer

135 addDeferred def'

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

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

219 mkImp (NS n s) = NS (mkImp n) s

220

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

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

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

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

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

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

224

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

226 = do let pn = expandNS syn pn_in

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

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

242

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

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

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

245 let valname = MN 0 "updateval"

246 let pt = k (PPi expl pn pty

247 (PPi expl rec recty recty))

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

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

270 let t = addImpl i t_in

271 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)) []

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

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

275 def' <- checkDef fc defer

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

449 logLvl 10 (showImp True tm)

450 -- try:

451 -- * ordinary elaboration

452− -- * elaboration as a Set

452+ -- * elaboration as a Type

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

454

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

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

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

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

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

459 (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

101 local f = do e <- get_env

102 return (f `elem` map fst e)

103

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

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

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

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

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

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

191 = do hsin <- get_holes

192 ptmin <- get_term

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

194− claim tyn RSet

194+ claim tyn RType

195 attack

196 ptm <- get_term

197 hs <- get_holes

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

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

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

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

212− claim tyn RSet

212+ claim tyn RType

213 n' <- case n of

214 MN _ _ -> unique_hole n

215 _ -> return n

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

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

222 = do attack;

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

224− claim tyn RSet

224+ claim tyn RType

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

226 claim valn (Var tyn)

227 letbind n (Var tyn) (Var valn)

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

257 claimArgTys env (_ : xs)

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

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

260− claim an RSet

260+ claim an RType

261 claim aval (Var an)

262 ans <- claimArgTys env xs

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

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

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

339 = do attack

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

341− claim tyn RSet

341+ claim tyn RType

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

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

344 claim valn (Var tyn)

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

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

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

594 -- start_unify h

595− claim tyn RSet

595+ claim tyn RType

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

597 claim valn (Var tyn)

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

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

604 runT (LetTac n tm)

605 = do attack

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

607− claim tyn RSet

607+ claim tyn RType

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

609 claim valn (Var tyn)

610 letn <- unique_hole n

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

615 runT (LetTacTy n ty tm)

616 = do attack

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

618− claim tyn RSet

618+ claim tyn RType

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

620 claim valn (Var tyn)

621 letn <- unique_hole n

src/Idris/IBC.hs+5−5

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

402 RApp x1 x2 -> do putWord8 2

403 put x1

404 put x2

405− RSet -> putWord8 3

405+ RType -> putWord8 3

406 RConstant x1 -> do putWord8 4

407 put x1

408 RForce x1 -> do putWord8 5

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

419 2 -> do x1 <- get

420 x2 <- get

421 return (RApp x1 x2)

422− 3 -> return RSet

422+ 3 -> return RType

423 4 -> do x1 <- get

424 return (RConstant x1)

425 5 -> do x1 <- get

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

525 put x1

526 put x2

527 Erased -> putWord8 6

528− Set x1 -> do putWord8 7

528+ TType x1 -> do putWord8 7

529− put x1

529+ put x1

530 Impossible -> putWord8 8

531 get

532 = do i <- getWord8

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

551 return (Proj x1 x2)

552 6 -> return Erased

553 7 -> do x1 <- get

554− return (Set x1)

554+ return (TType x1)

555 8 -> return Impossible

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

557

src/Idris/Parser.hs+16−16

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

599

600pNoExtExpr syn =

601 try (pApp syn)

602− <|> pRecordSet syn

602+ <|> pRecordType syn

603 <|> try (pSimpleExpr syn)

604 <|> pLambda syn

605 <|> pLet syn

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

879 symbol "}"

880 return (pconst e)

881

882−pRecordSet syn

882+pRecordType syn

883 = do reserved "record"

884 lchar '{'

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

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

886 lchar '}'

887 fc <- pfc

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

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

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

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

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

895− where pFieldSet = do n <- pfName

895+ where pFieldType = do n <- pfName

896− lchar '='

896+ lchar '='

897− e <- pExpr syn

897+ e <- pExpr syn

898− return (n, e)

898+ return (n, e)

899 applyAll fc [] x = x

900 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])

902

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

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

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

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

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

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

906

907noImp syn = syn { implicitAllowed = False }

908impOK syn = syn { implicitAllowed = True }

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

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

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

1158 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)]

1160 ++ getRecNames syn sc

1161 getRecNames _ _ = []

1162

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

1201 let n = show tyn_in ++ " "

1202 let s = kw ++ n

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

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

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

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

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

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

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

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

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

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

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

1210

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

src/Idris/Primitives.hs+2−2

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

23ty [] x = Constant x

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

25

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

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

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

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

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

29

30total = Total []

src/Main.hs+2−2

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

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

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

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

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

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

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

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

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

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

94 "\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"