b26716a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Collect cumulativity constraints on universes

commitb26716a2b608979ed88b2d91aba9de59ba7c21fb authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 22 Nov 2011, 15:08 (15 years ago) parent72b43b2

12 files changed+186−92

compare with master

unifiedsplit

src/Core/CoreParser.hs+2−2 src/Core/Elaborate.hs+4−4 src/Core/Evaluate.hs+45−25 src/Core/ProofState.hs+2−2 src/Core/TT.hs+39−5 src/Core/Typecheck.hs+49−26 src/Idris/AbsSyntax.hs+13−5 src/Idris/Compiler.hs+1−1 src/Idris/ElabDecls.hs+25−21 src/Idris/Prover.hs+1−1 src/Idris/REPL.hs+4 src/Idris/REPLParser.hs+1

src/Core/CoreParser.hs+2−2

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

127127 lchar '.';

128128 sc <- pTerm

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

130− <|> try (do reserved "Set"; i <- option 0 natural

131− return (RSet (fromInteger i)))

130+ <|> try (do reserved "Set"

131+ return RSet)

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

133133 return (Var x))

134134

src/Core/Elaborate.hs+4−4

@@ -134,7 +134,7 @@ unique_hole n = do ES p _ _ <- get

134134uniqueNameCtxt :: Context -> Name -> [Name] -> Elab Name

135135uniqueNameCtxt ctxt n hs

136136 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs

137− | Just _ <- lookupCtxt n ctxt = uniqueNameCtxt ctxt (nextName n) hs

137+ | Just _ <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs

138138 | otherwise = return n

139139

140140elog :: String -> Elab ()

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

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

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

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

323− claim a (RSet 0)

324− claim b (RSet 0)

323+ claim a RSet

324+ claim b RSet

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

326326 start_unify s

327327 claim s (Var a)

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

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

340340arg :: Name -> Name -> Elab ()

341341arg n tyhole = do ty <- unique_hole tyhole

342− claim ty (RSet 0)

342+ claim ty RSet

343343 forall n (Var ty)

344344

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

src/Core/Evaluate.hs+45−25

@@ -2,7 +2,8 @@

22 PatternGuards #-}

44module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf,

5− Fun(..), Def(..), Context,

5+ Fun(..), Def(..),

6+ Context, initContext, ctxtAlist, uconstraints, next_tvar,

67 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,

78 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

89 Value(..)) where

@@ -25,7 +26,7 @@ data Value = VP NameType Name Value

2526 | VV Int

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

2728 | VApp Value Value

28− | VSet Int

29+ | VSet UExp

2930 | VConstant Const

3031 | VTmp Int

3132

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

3334 | HV Int

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

3536 | HApp HNF [HNF] [TT Name]

36− | HSet Int

37+ | HSet UExp

3738 | HConstant Const

3839 | HTmp Int

3940 deriving Show

@@ -438,44 +439,63 @@ instance Show Def where

438439

439440-------

440441

441−type Context = Ctxt Def

442+data Context = MkContext { uconstraints :: [UConstraint],

443+ next_tvar :: Int,

444+ definitions :: Ctxt Def }

445+

446+initContext = MkContext [] 0 emptyContext

447+

448+ctxtAlist :: Context -> [(Name, Def)]

449+ctxtAlist ctxt = toAlist (definitions ctxt)

442450

443451veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()

444452

445453addToCtxt :: Name -> Term -> Type -> Context -> Context

446−addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (veval ctxt [] ty)

447− tm (veval ctxt [] tm))) ctxt

454+addToCtxt n tm ty uctxt

455+ = let ctxt = definitions uctxt

456+ ctxt' = addDef n (Function (Fun ty (veval uctxt [] ty)

457+ tm (veval uctxt [] tm))) ctxt in

458+ uctxt { definitions = ctxt' }

448459

449460addTyDecl :: Name -> Type -> Context -> Context

450−addTyDecl n ty ctxt = addDef n (TyDecl Ref ty (veval ctxt [] ty)) ctxt

461+addTyDecl n ty uctxt

462+ = let ctxt = definitions uctxt

463+ ctxt' = addDef n (TyDecl Ref ty (veval uctxt [] ty)) ctxt in

464+ uctxt { definitions = ctxt' }

451465

452466addDatatype :: Datatype Name -> Context -> Context

453−addDatatype (Data n tag ty cons) ctxt

454− = let ty' = normalise ctxt [] ty in

455− addCons 0 cons (addDef n

456− (TyDecl (TCon tag (arity ty')) ty (veval ctxt [] ty)) ctxt)

467+addDatatype (Data n tag ty cons) uctxt

468+ = let ctxt = definitions uctxt

469+ ty' = normalise uctxt [] ty

470+ ctxt' = addCons 0 cons (addDef n

471+ (TyDecl (TCon tag (arity ty')) ty (veval uctxt [] ty)) ctxt) in

472+ uctxt { definitions = ctxt' }

457473 where

458474 addCons tag [] ctxt = ctxt

459475 addCons tag ((n, ty) : cons) ctxt

460− = let ty' = normalise ctxt [] ty in

476+ = let ty' = normalise uctxt [] ty in

461477 addCons (tag+1) cons (addDef n

462− (TyDecl (DCon tag (arity ty')) ty (veval ctxt [] ty)) ctxt)

478+ (TyDecl (DCon tag (arity ty')) ty (veval uctxt [] ty)) ctxt)

463479

464480addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context

465−addCasedef n alwaysInline tcase ps ty ctxt

466− = let ps' = ps in -- simpl ps in

467− case simpleCase tcase ps' of

468− CaseDef args sc -> let inl = alwaysInline in

469− addDef n (CaseOp inl ty ps args sc) ctxt

481+addCasedef n alwaysInline tcase ps ty uctxt

482+ = let ctxt = definitions uctxt

483+ ps' = ps -- simpl ps in

484+ ctxt' = case simpleCase tcase ps' of

485+ CaseDef args sc -> let inl = alwaysInline in

486+ addDef n (CaseOp inl ty ps args sc) ctxt in

487+ uctxt { definitions = ctxt' }

470488 where simpl [] = []

471− simpl ((l,r) : xs) = (l, simplify ctxt [] r) : simpl xs

489+ simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs

472490

473491addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

474−addOperator n ty a op ctxt

475− = addDef n (Operator ty a op) ctxt

492+addOperator n ty a op uctxt

493+ = let ctxt = definitions uctxt

494+ ctxt' = addDef n (Operator ty a op) ctxt in

495+ uctxt { definitions = ctxt' }

476496

477497lookupTy :: Name -> Context -> Maybe Type

478−lookupTy n ctxt = do def <- lookupCtxt n ctxt

498+lookupTy n ctxt = do def <- lookupCtxt n (definitions ctxt)

479499 case def of

480500 (Function (Fun ty _ _ _)) -> return ty

481501 (TyDecl _ ty _) -> return ty

@@ -484,7 +504,7 @@ lookupTy n ctxt = do def <- lookupCtxt n ctxt

484504

485505lookupP :: Name -> Context -> Maybe Term

486506lookupP n ctxt

487− = do def <- lookupCtxt n ctxt

507+ = do def <- lookupCtxt n (definitions ctxt)

488508 case def of

489509 (Function (Fun ty _ tm _)) -> return (P Ref n ty)

490510 (TyDecl nt ty hty) -> return (P nt n ty)

@@ -492,11 +512,11 @@ lookupP n ctxt

492512 (Operator ty _ _) -> return (P Ref n ty)

493513

494514lookupDef :: Name -> Context -> Maybe Def

495−lookupDef n ctxt = lookupCtxt n ctxt

515+lookupDef n ctxt = lookupCtxt n (definitions ctxt)

496516

497517lookupVal :: Name -> Context -> Maybe Value

498518lookupVal n ctxt

499− = do def <- lookupCtxt n ctxt

519+ = do def <- lookupCtxt n (definitions ctxt)

500520 case def of

501521 (Function (Fun _ _ _ htm)) -> return htm

502522 (TyDecl nt ty hty) -> return (VP nt n hty)

src/Core/ProofState.hs+2−2

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

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

326326 let newt = mkP l r l t

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

328− (mkApp (P Ref (UN "replace") (Set 0))

328+ (mkApp (P Ref (UN "replace") (Set (UVal 0)))

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

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

331331 return scv

@@ -398,7 +398,7 @@ updateSolved xs t = t

398398processTactic :: Tactic -> ProofState -> TC (ProofState, String)

399399processTactic QED ps = case holes ps of

400400 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)

401− (tm', ty') <- recheck (context ps) [] tm

401+ (tm', ty', _) <- recheck (context ps) [] tm

402402 return (ps { done = True, pterm = tm' },

403403 "Proof complete: " ++ showEnv [] tm')

404404 _ -> fail "Still holes to fill."

src/Core/TT.hs+39−5

@@ -127,7 +127,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

127127data Raw = Var Name

128128 | RBind Name (Binder Raw) Raw

129129 | RApp Raw Raw

130− | RSet Int

130+ | RSet

131131 | RConstant Const

132132 deriving (Show, Eq)

133133

@@ -177,6 +177,25 @@ type RProgram = [(Name, RDef)]

177177

178178-- WELL TYPED TERMS ---------------------------------------------------------

179179

180+data UExp = UVar Int -- universe variable

181+ | UVal Int -- explicit universe level

182+ deriving Eq

183+

184+instance Show UExp where

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

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

187+ show (UVal x) = show x

188+

189+data UConstraint = ULT UExp UExp

190+ | ULE UExp UExp

191+ deriving Eq

192+

193+instance Show UConstraint where

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

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

196+

197+type UCs = (Int, [UConstraint])

198+

180199data NameType = Bound | Ref | DCon Int Int | TCon Int Int

181200 deriving (Show, Eq)

182201

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

185204 | Bind n (Binder (TT n)) (TT n)

186205 | App (TT n) (TT n) -- function, function type, arg

187206 | Constant Const

188− | Set Int

207+ | Set UExp

189208 deriving Functor

190209

191210type EnvTT n = [(n, Binder (TT n))]

@@ -201,10 +220,25 @@ instance Eq n => Eq (TT n) where

201220 (==) (V x) (V y) = x == y

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

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

204− (==) (Set x) (Set y) = x == y

223+ (==) (Set _) (Set _) = True -- deal with constraints later

205224 (==) (Constant x) (Constant y) = x == y

206225 (==) _ _ = False

207226

227+convEq :: Eq n => TT n -> TT n -> StateT UCs TC Bool

228+convEq (P xt x _) (P yt y _) = return (xt == yt && x == y)

229+convEq (V x) (V y) = return (x == y)

230+convEq (Bind _ xb xs) (Bind _ yb ys)

231+ = liftM2 (&&) (convEqB xb yb) (convEq xs ys)

232+ where convEqB (Let v t) (Let v' t') = liftM2 (&&) (convEq v v') (convEq t t')

233+ convEqB (Guess v t) (Guess v' t') = liftM2 (&&) (convEq v v') (convEq t t')

234+ convEqB b b' = convEq (binderTy b) (binderTy b')

235+convEq (App fx ax) (App fy ay) = liftM2 (&&) (convEq fx fy) (convEq ax ay)

236+convEq (Constant x) (Constant y) = return (x == y)

237+convEq (Set x) (Set y) = do (v, cs) <- get

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

239+ return True

240+convEq _ _ = return False

241+

208242-- A few handy operations on well typed terms:

209243

210244instantiate :: TT n -> TT n -> TT n

@@ -291,7 +325,7 @@ forget tm = fe [] tm

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

292326 fe env (Constant c)

293327 = RConstant c

294− fe env (Set i) = RSet i

328+ fe env (Set i) = RSet

295329

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

297331bindAll [] t =t

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

358392 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

359393 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

360394 se p env (Constant c) = show c

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

395+ se p env (Set i) = "Set " ++ show i

362396

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

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

src/Core/Typecheck.hs+49−26

@@ -14,6 +14,15 @@ import Core.Evaluate

1414-- deal with alpha conversion - we do this by making each inner term de Bruijn

1515-- indexed with 'finalise'

1616

17+convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC ()

18+convertsC ctxt env x y

19+ = do c <- convEq (finalise (normalise ctxt env x))

20+ (finalise (normalise ctxt env y))

21+ if c then return ()

22+ else fail ("Can't convert between " ++

23+ showEnv env (finalise (normalise ctxt env x)) ++ " and " ++

24+ showEnv env (finalise (normalise ctxt env y)))

25+

1726converts :: Context -> Env -> Term -> Term -> TC ()

1827converts ctxt env x y = if (finalise (normalise ctxt env x) ==

1928 finalise (normalise ctxt env y))

@@ -24,20 +33,21 @@ converts ctxt env x y = if (finalise (normalise ctxt env x) ==

2433

2534isSet :: Context -> Env -> Term -> TC ()

2635isSet ctxt env tm = isSet' (normalise ctxt env tm)

27− where isSet' :: Term -> TC ()

28− isSet' (Set _) = return ()

36+ where isSet' (Set _) = return ()

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

3038

31−recheck :: Context -> Env -> Term -> TC (Term, Type)

39+recheck :: Context -> Env -> Term -> TC (Term, Type, UCs)

3240recheck ctxt env tm

33− = case check' False ctxt env (forget tm) of -- holes banned

34− Error (IncompleteTerm _) -> Error $ IncompleteTerm tm

35− x -> x

41+ = let v = next_tvar ctxt in

42+ case runStateT (check' False ctxt env (forget tm)) (v, []) of -- holes banned

43+ Error (IncompleteTerm _) -> Error $ IncompleteTerm tm

44+ OK ((tm, ty), constraints) ->

45+ return (tm, ty, constraints)

3646

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

38−check = check' True -- Holes allowed

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

3949

40−check' :: Bool -> Context -> Env -> Raw -> TC (Term, Type)

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

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

4252 chk env (Var n)

4353 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

@@ -49,8 +59,8 @@ check' holes ctxt env top = chk env top where

4959 let fty' = renameBinders 0 $ normalise ctxt env fty

5060 case fty' of

5161 Bind x (Pi s) t ->

52− do converts ctxt env s aty

53− let apty = normalise emptyContext env (Bind x (Let aty av) t)

62+ do convertsC ctxt env aty s

63+ let apty = normalise initContext env (Bind x (Let aty av) t)

5464 return (App fv av, apty)

5565 t -> fail "Can't apply a non-function type"

5666 -- This rather unpleasant hack is needed because during incomplete

@@ -60,14 +70,27 @@ check' holes ctxt env top = chk env top where

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

6171 (renameBinders (i+1) t)

6272 renameBinders i sc = sc

63− chk env (RSet i) = return (Set i, Set i) -- LATER: (i+1))

73+ chk env RSet

74+ | holes = return (Set (UVal 0), Set (UVal 0))

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

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

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

78+ return (Set (UVar v), Set (UVar (v+1)))

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

6580 where constType (I _) = Constant IType

6681 constType (BI _) = Constant BIType

6782 constType (Fl _) = Constant FlType

6883 constType (Ch _) = Constant ChType

6984 constType (Str _) = Constant StrType

70− constType _ = Set 0

85+ constType _ = Set (UVal 0)

86+ chk env (RBind n (Pi s) t)

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

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

89+ (v, cs) <- get

90+ let Set su = normalise ctxt env st

91+ let Set tu = normalise ctxt env tt

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

93+ return (Bind n (Pi sv) (pToV n tv), Set (UVar v))

7194 chk env (RBind n b sc)

7295 = do b' <- checkBinder b

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

@@ -76,65 +99,65 @@ check' holes ctxt env top = chk env top where

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

77100 let tv' = normalise ctxt env tv

78101 let tt' = normalise ctxt env tt

79− isSet ctxt env tt'

102+ lift $ isSet ctxt env tt'

80103 return (Lam tv)

81104 checkBinder (Pi t)

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

83106 let tv' = normalise ctxt env tv

84107 let tt' = normalise ctxt env tt

85− isSet ctxt env tt'

108+ lift $ isSet ctxt env tt'

86109 return (Pi tv)

87110 checkBinder (Let t v)

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

89112 (vv, vt) <- chk env v

90113 let tv' = normalise ctxt env tv

91114 let tt' = normalise ctxt env tt

92− converts ctxt env tv vt

93− isSet ctxt env tt'

115+ convertsC ctxt env tv vt

116+ lift $ isSet ctxt env tt'

94117 return (Let tv vv)

95118 checkBinder (NLet t v)

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

97120 (vv, vt) <- chk env v

98121 let tv' = normalise ctxt env tv

99122 let tt' = normalise ctxt env tt

100− converts ctxt env tv vt

101− isSet ctxt env tt'

123+ convertsC ctxt env tv vt

124+ lift $ isSet ctxt env tt'

102125 return (NLet tv vv)

103126 checkBinder (Hole t)

104− | not holes = tfail (IncompleteTerm undefined)

127+ | not holes = lift $ tfail (IncompleteTerm undefined)

105128 | otherwise

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

107130 let tv' = normalise ctxt env tv

108131 let tt' = normalise ctxt env tt

109− isSet ctxt env tt'

132+ lift $ isSet ctxt env tt'

110133 return (Hole tv)

111134 checkBinder (GHole t)

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

113136 let tv' = normalise ctxt env tv

114137 let tt' = normalise ctxt env tt

115− isSet ctxt env tt'

138+ lift $ isSet ctxt env tt'

116139 return (GHole tv)

117140 checkBinder (Guess t v)

118− | not holes = tfail (IncompleteTerm undefined)

141+ | not holes = lift $ tfail (IncompleteTerm undefined)

119142 | otherwise

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

121144 (vv, vt) <- chk env v

122145 let tv' = normalise ctxt env tv

123146 let tt' = normalise ctxt env tt

124− converts ctxt env tv vt

125− isSet ctxt env tt'

147+ convertsC ctxt env tv vt

148+ lift $ isSet ctxt env tt'

126149 return (Guess tv vv)

127150 checkBinder (PVar t)

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

129152 let tv' = normalise ctxt env tv

130153 let tt' = normalise ctxt env tt

131− isSet ctxt env tt'

154+ lift $ isSet ctxt env tt'

132155 return (PVar tv)

133156 checkBinder (PVTy t)

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

135158 let tv' = normalise ctxt env tv

136159 let tt' = normalise ctxt env tt

137− isSet ctxt env tt'

160+ lift $ isSet ctxt env tt'

138161 return (PVTy tv)

139162

140163 discharge n (Lam t) scv sct

src/Idris/AbsSyntax.hs+13−5

@@ -47,7 +47,7 @@ data IState = IState { tt_ctxt :: Context,

4747 errLine :: Maybe Int

4848 }

4949

50−idrisInit = IState emptyContext [] emptyContext emptyContext emptyContext

50+idrisInit = IState initContext [] emptyContext emptyContext emptyContext

5151 "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing

5252

5353-- The monad for the main REPL - reading and processing files and updating

@@ -100,7 +100,7 @@ getName = do i <- get;

100100checkUndefined :: FC -> Name -> Idris ()

101101checkUndefined fc n

102102 = do i <- getContext

103− case lookupCtxt n i of

103+ case lookupTy n i of

104104 Just _ -> fail $ show fc ++ ":" ++

105105 show n ++ " already defined"

106106 _ -> return ()

@@ -111,6 +111,14 @@ setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )

111111updateContext :: (Context -> Context) -> Idris ()

112112updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )

113113

114+addConstraints :: (Int, [UConstraint]) -> Idris ()

115+addConstraints (v, cs)

116+ = do i <- get

117+ let ctxt = tt_ctxt i

118+ let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,

119+ next_tvar = v }

120+ put (i { tt_ctxt = ctxt' })

121+

114122addDeferred :: [(Name, Type)] -> Idris ()

115123addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns

116124 i <- get

@@ -176,7 +184,7 @@ setTypeCase t = do i <- get

176184

178186 | Compile String | Execute String

179− | Metavars | Prove Name

187+ | Metavars | Prove Name | Universes

180188 | TTShell

181189 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name

182190 | NOP

@@ -546,7 +554,7 @@ namesIn ist tm = nub $ ni [] tm

546554 where

547555 ni env (PRef _ n)

548556 | not (n `elem` env)

549− = case lookupCtxt n (tt_ctxt ist) of

557+ = case lookupTy n (tt_ctxt ist) of

550558 Nothing -> [n]

551559 _ -> []

552560 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

@@ -572,7 +580,7 @@ inferDecl = PDatadecl inferTy

572580 (PRef bi inferTy)), bi)]

573581

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

575−infP = P (TCon 6 0) inferTy (Set 0)

583+infP = P (TCon 6 0) inferTy (Set (UVal 0))

576584

577585getInferTerm, getInferType :: Term -> Term

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

src/Idris/Compiler.hs+1−1

@@ -26,7 +26,7 @@ compile f = do ds <- mkDecls

2626

2727mkDecls :: Idris [EpicDecl]

2828mkDecls = do i <- getIState

29− decls <- mapM build (toAlist (tt_ctxt i))

29+ decls <- mapM build (ctxtAlist (tt_ctxt i))

3030 return $ basic_defs ++ EpicFn (name "main") epicMain : decls

3131

3232ename x = name ("idris_" ++ show x)

src/Idris/ElabDecls.hs+25−21

@@ -28,8 +28,12 @@ data ElabInfo = EInfo { params :: [(Name, PTerm)],

2828

2929toplevel = EInfo [] emptyContext id

3030

31+recheckC ctxt env t = do (tm, ty, cs) <- tclift $ recheck ctxt env t

32+ addConstraints cs

33+ return (tm, ty)

34+

3135checkDef ns = do ctxt <- getContext

32− mapM (\(n, t) -> do (t', _) <- tclift $ recheck ctxt [] t

36+ mapM (\(n, t) -> do (t', _) <- recheckC ctxt [] t

3337 return (n, t')) ns

3438

3539elabType :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> Idris ()

@@ -41,9 +45,9 @@ elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in

4145 ty' <- implicit syn n ty'

4246 let ty = addImpl i ty'

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

44− ((ty', defer), log) <- tclift $ elaborate ctxt n (Set 0)

48+ ((ty', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

4549 (erun fc (build i info False ty))

46− (cty, _) <- tclift $ recheck ctxt [] ty'

50+ (cty, _) <- recheckC ctxt [] ty'

4751 logLvl 2 $ "---> " ++ show cty

4852 let nty = normalise ctxt [] cty

4953 ds <- checkDef ((n, nty):defer)

@@ -57,11 +61,11 @@ elabData info syn fc (PDatadecl n t_in dcons)

5761 i <- get

5862 t_in <- implicit syn n t_in

5963 let t = addImpl i t_in

60− ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0)

64+ ((t', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

6165 (erun fc (build i info False t))

6266 def' <- checkDef defer

6367 addDeferred def'

64− (cty, _) <- tclift $ recheck ctxt [] t'

68+ (cty, _) <- recheckC ctxt [] t'

6569 logLvl 2 $ "---> " ++ show cty

6670 updateContext (addTyDecl n cty) -- temporary, to check cons

6771 cons <- mapM (elabCon info syn) dcons

@@ -76,13 +80,13 @@ elabCon info syn (n, t_in, fc)

7680 t_in <- implicit syn n t_in

7781 let t = addImpl i t_in

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

79− ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0)

83+ ((t', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

8084 (erun fc (build i info False t))

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

8286 def' <- checkDef defer

8387 addDeferred def'

8488 ctxt <- getContext

85− (cty, _) <- tclift $ recheck ctxt [] t'

89+ (cty, _) <- recheckC ctxt [] t'

8690 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

8791 return (n, cty)

8892

@@ -118,7 +122,7 @@ elabVal info aspat tm_in

118122 logLvl 3 ("Value: " ++ show tm')

119123 let vtm = getInferTerm tm'

120124 logLvl 2 (show vtm)

121− tclift $ recheck ctxt [] vtm

125+ recheckC ctxt [] vtm

122126

123127elabClause :: ElabInfo -> FC -> PClause -> Idris (Term, Term)

124128elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

@@ -133,7 +137,7 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

133137 let lhs_tm = orderPats (getInferTerm lhs')

134138 let lhs_ty = getInferType lhs'

135139 logLvl 3 (show lhs_tm)

136− (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm

140+ (clhs, clhsty) <- recheckC ctxt [] lhs_tm

137141 logLvl 5 ("Checked " ++ show clhs)

138142 -- Elaborate where block

139143 ist <- getIState

@@ -163,7 +167,7 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

163167 def' <- checkDef defer

164168 addDeferred def'

165169 ctxt <- getContext

166− (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

170+ (crhs, crhsty) <- recheckC ctxt [] rhs'

167171 return (clhs, crhs)

168172 where

169173 decorate x = UN (show fname ++ "#" ++ show x)

@@ -193,7 +197,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

193197 let lhs_ty = getInferType lhs'

194198 let ret_ty = getRetTy lhs_ty

195199 logLvl 3 (show lhs_tm)

196− (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm

200+ (clhs, clhsty) <- recheckC ctxt [] lhs_tm

197201 logLvl 5 ("Checked " ++ show clhs)

198202 let bargs = getPBtys lhs_tm

199203 let wval = addImpl i wval_in

@@ -210,7 +214,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

210214 return (tt, d))

211215 def' <- checkDef defer

212216 addDeferred def'

213− (cwval, cwvalty) <- tclift $ recheck ctxt [] (getInferTerm wval')

217+ (cwval, cwvalty) <- recheckC ctxt [] (getInferTerm wval')

214218 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

215219 windex <- getName

216220 -- build a type declaration for the new function:

@@ -245,7 +249,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

245249 return (tt, d))

246250 def' <- checkDef defer

247251 addDeferred def'

248− (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

252+ (crhs, crhsty) <- recheckC ctxt [] rhs'

249253 return (clhs, crhs)

250254 where

251255 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

@@ -522,7 +526,7 @@ elab ist info pattern tm

522526 local f = do e <- get_env

523527 return (f `elem` map fst e)

524528

525− elab' PSet = do fill (RSet 0); solve

529+ elab' PSet = do fill RSet; solve

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

527531 elab' (PQuote r) = do fill r; solve

528532 elab' (PTrue fc) = try (elab' (PRef fc unitCon))

@@ -560,7 +564,7 @@ elab ist info pattern tm

560564 pexp l, pexp r])

561565 elab' (PRef fc n) | pattern && not (inparamBlock n)

562566 = do ctxt <- get_context

563− let sc = case lookupCtxt n ctxt of

567+ let sc = case lookupTy n ctxt of

564568 Nothing -> True

565569 _ -> False

566570 if sc

@@ -576,7 +580,7 @@ elab ist info pattern tm

576580 = do attack; intro (Just n); elabE sc; solve

577581 elab' (PLam n ty sc)

578582 = do tyn <- unique_hole (MN 0 "lamty")

579− claim tyn (RSet 0)

583+ claim tyn RSet

580584 attack

581585 introTy (Var tyn) (Just n)

582586 -- end_unify

@@ -588,7 +592,7 @@ elab ist info pattern tm

588592 = do attack; arg n (MN 0 "ty"); elabE sc; solve

589593 elab' (PPi _ n ty sc)

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

591− claim tyn (RSet 0)

595+ claim tyn RSet

592596 n' <- case n of

593597 MN _ _ -> unique_hole n

594598 _ -> return n

@@ -600,7 +604,7 @@ elab ist info pattern tm

600604 elab' (PLet n ty val sc)

601605 = do attack;

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

603− claim tyn (RSet 0)

607+ claim tyn RSet

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

605609 claim valn (Var tyn)

606610 letbind n (Var tyn) (Var valn)

@@ -682,7 +686,7 @@ resolveTC depth ist

682686 = do t <- goal

683687 tm <- get_term

684688 try (trivial ist)

685− (blunderbuss t (map fst (toAlist (tt_ctxt ist))))

689+ (blunderbuss t (map fst (ctxtAlist (tt_ctxt ist))))

686690 where

687691 blunderbuss t [] = fail $ "Can't resolve type class " ++ show t

688692 blunderbuss t (n:ns) | tcname n = try (resolve n depth)

@@ -753,7 +757,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

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

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

755759 -- start_unify h

756− claim tyn (RSet 0)

760+ claim tyn RSet

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

758762 claim valn (Var tyn)

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

@@ -765,7 +769,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

765769 runT (LetTac n tm)

766770 = do attack

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

768− claim tyn (RSet 0)

772+ claim tyn RSet

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

770774 claim valn (Var tyn)

771775 letn <- unique_hole n

src/Idris/Prover.hs+1−1

@@ -37,7 +37,7 @@ prove ctxt n ty

3737 lift $ dumpProof n prf

3838 let tree = simpleCase False [(P Ref n ty, tm)]

3939 logLvl 3 (show tree)

40− (ptm, pty) <- tclift $ recheck ctxt [] tm

40+ (ptm, pty) <- recheckC ctxt [] tm

4141 updateContext (addCasedef n True False [(P Ref n ty, ptm)] ty)

4242 solveDeferred n

4343

src/Idris/REPL.hs+4

@@ -110,6 +110,10 @@ process (Check t) = do (tm, ty) <- elabVal toplevel False t

110110 let ty' = normaliseC ctxt [] ty

111111 iputStrLn (showImp imp (delab ist tm) ++ " : " ++

112112 showImp imp (delab ist ty))

113+process Universes = do ctxt <- getContext

114+ let cs = nub $ uconstraints ctxt

115+ lift $ print cs

116+ iputStrLn $ "(" ++ show (length cs) ++ " constraints)"

113117process (Defn n) = do ctxt <- getContext

114118 lift $ print (lookupDef n ctxt)

115119process (Spec t) = do (tm, ty) <- elabVal toplevel False t

src/Idris/REPLParser.hs+1

@@ -34,6 +34,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

3434 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

3535 <|> try (do cmd ["d", "def"]; n <- pName; eof; return (Defn n))

3636 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

37+ <|> try (do cmd ["u", "universes"]; eof; return Universes)

3738 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

3839 <|> do eof; return NOP

3940