b26716a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Collect cumulativity constraints on universes

b26716aEdwin Brady15 years ago

src/Core/CoreParser.hs+2−2

compare with master

unifiedsplit

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

127 lchar '.';

128 sc <- pTerm

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

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

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

131− return (RSet (fromInteger i)))

131+ return RSet)

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

133 return (Var x))

134

src/Core/Elaborate.hs+4−4

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

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

135uniqueNameCtxt ctxt n hs

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

138 | otherwise = return n

139

140elog :: String -> Elab ()

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

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

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

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

323− claim a (RSet 0)

323+ claim a RSet

324− claim b (RSet 0)

324+ claim b RSet

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

326 start_unify s

327 claim s (Var a)

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

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

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

341arg n tyhole = do ty <- unique_hole tyhole

342− claim ty (RSet 0)

342+ claim ty RSet

343 forall n (Var ty)

344

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

src/Core/Evaluate.hs+45−25

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

2 PatternGuards #-}

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

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

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

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

6 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,

7 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,

7 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

8 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

8 Value(..)) where

9 Value(..)) where

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

25 | VV Int

26 | VV Int

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

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

27 | VApp Value Value

28 | VApp Value Value

28− | VSet Int

29+ | VSet UExp

29 | VConstant Const

30 | VConstant Const

30 | VTmp Int

31 | VTmp Int

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

33 | HV Int

34 | HV Int

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

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

35 | HApp HNF [HNF] [TT Name]

36 | HApp HNF [HNF] [TT Name]

36− | HSet Int

37+ | HSet UExp

37 | HConstant Const

38 | HConstant Const

38 | HTmp Int

39 | HTmp Int

39 deriving Show

40 deriving Show

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

438

439

439-------

440-------

440

441

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)

442

450

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

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

444

452

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

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

454+addToCtxt n tm ty uctxt

455+ = let ctxt = definitions uctxt

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

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

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

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

458+ uctxt { definitions = ctxt' }

448

459

449addTyDecl :: Name -> Type -> Context -> Context

460addTyDecl :: Name -> Type -> Context -> Context

461+addTyDecl n ty uctxt

462+ = let ctxt = definitions uctxt

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

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

464+ uctxt { definitions = ctxt' }

451

465

452addDatatype :: Datatype Name -> Context -> Context

466addDatatype :: Datatype Name -> Context -> Context

453−addDatatype (Data n tag ty cons) ctxt

467+addDatatype (Data n tag ty cons) uctxt

468+ = let ctxt = definitions uctxt

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

469+ ty' = normalise uctxt [] ty

455− addCons 0 cons (addDef n

470+ ctxt' = addCons 0 cons (addDef n

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

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

472+ uctxt { definitions = ctxt' }

457 where

473 where

458 addCons tag [] ctxt = ctxt

474 addCons tag [] ctxt = ctxt

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

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

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

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

461 addCons (tag+1) cons (addDef n

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

463

479

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

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

465−addCasedef n alwaysInline tcase ps ty ctxt

481+addCasedef n alwaysInline tcase ps ty uctxt

482+ = let ctxt = definitions uctxt

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

483+ ps' = ps -- simpl ps in

467− case simpleCase tcase ps' of

484+ ctxt' = case simpleCase tcase ps' of

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

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

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

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

487+ uctxt { definitions = ctxt' }

470 where simpl [] = []

488 where simpl [] = []

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

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

472

490

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

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

474−addOperator n ty a op ctxt

492+addOperator n ty a op uctxt

493+ = let ctxt = definitions uctxt

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

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

495+ uctxt { definitions = ctxt' }

476

496

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

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

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

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

479 case def of

499 case def of

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

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

481 (TyDecl _ ty _) -> return ty

501 (TyDecl _ ty _) -> return ty

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

484

504

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

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

486lookupP n ctxt

506lookupP n ctxt

487− = do def <- lookupCtxt n ctxt

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

488 case def of

508 case def of

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

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

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

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

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

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

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

493

513

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

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

495−lookupDef n ctxt = lookupCtxt n ctxt

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

496

516

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

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

498lookupVal n ctxt

518lookupVal n ctxt

499− = do def <- lookupCtxt n ctxt

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

500 case def of

520 case def of

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

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

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

522 (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' =

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

326 let newt = mkP l r l t

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

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

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

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

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

331 return scv

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

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

399processTactic QED ps = case holes ps of

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

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

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

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

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

404 _ -> 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

127data Raw = Var Name

128 | RBind Name (Binder Raw) Raw

129 | RApp Raw Raw

130− | RSet Int

130+ | RSet

131 | RConstant Const

132 deriving (Show, Eq)

133

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

177

178-- WELL TYPED TERMS ---------------------------------------------------------

179

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+

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

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

181 deriving (Show, Eq)

200 deriving (Show, Eq)

182

201

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

185 | Bind n (Binder (TT n)) (TT n)

204 | Bind n (Binder (TT n)) (TT n)

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

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

187 | Constant Const

206 | Constant Const

188− | Set Int

207+ | Set UExp

189 deriving Functor

208 deriving Functor

190

209

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

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

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

201 (==) (V x) (V y) = x == y

220 (==) (V x) (V y) = x == y

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

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

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

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

205 (==) (Constant x) (Constant y) = x == y

224 (==) (Constant x) (Constant y) = x == y

206 (==) _ _ = False

225 (==) _ _ = False

207

226

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+

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

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

209

243

210instantiate :: TT n -> TT n -> TT n

244instantiate :: TT n -> TT n -> TT n

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

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

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

292 fe env (Constant c)

326 fe env (Constant c)

293 = RConstant c

327 = RConstant c

294− fe env (Set i) = RSet i

328+ fe env (Set i) = RSet

295

329

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

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

297bindAll [] t =t

331bindAll [] t =t

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

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

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

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

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

360 se p env (Constant c) = show c

394 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

362

396

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

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

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

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

src/Core/Typecheck.hs+49−26

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

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

15-- indexed with 'finalise'

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+

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

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

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

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

19 finalise (normalise ctxt env y))

28 finalise (normalise ctxt env y))

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

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

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

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

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

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

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

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

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

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

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

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

32recheck ctxt env tm

40recheck ctxt env tm

41+ = let v = next_tvar ctxt in

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

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

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

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

35− x -> x

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

45+ return (tm, ty, constraints)

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

47check :: 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

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

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

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

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

42 chk env (Var n)

52 chk env (Var n)

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

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

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

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

50 case fty' of

60 case fty' of

51 Bind x (Pi s) t ->

61 Bind x (Pi s) t ->

52− do converts ctxt env s aty

62+ do convertsC ctxt env aty s

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

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

54 return (App fv av, apty)

64 return (App fv av, apty)

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

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

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

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

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

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

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

61 (renameBinders (i+1) t)

71 (renameBinders (i+1) t)

62 renameBinders i sc = sc

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

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

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

65 where constType (I _) = Constant IType

80 where constType (I _) = Constant IType

66 constType (BI _) = Constant BIType

81 constType (BI _) = Constant BIType

67 constType (Fl _) = Constant FlType

82 constType (Fl _) = Constant FlType

68 constType (Ch _) = Constant ChType

83 constType (Ch _) = Constant ChType

69 constType (Str _) = Constant StrType

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

71 chk env (RBind n b sc)

94 chk env (RBind n b sc)

72 = do b' <- checkBinder b

95 = do b' <- checkBinder b

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

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

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

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

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

77 let tv' = normalise ctxt env tv

100 let tv' = normalise ctxt env tv

78 let tt' = normalise ctxt env tt

101 let tt' = normalise ctxt env tt

79− isSet ctxt env tt'

102+ lift $ isSet ctxt env tt'

80 return (Lam tv)

103 return (Lam tv)

81 checkBinder (Pi t)

104 checkBinder (Pi t)

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

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

83 let tv' = normalise ctxt env tv

106 let tv' = normalise ctxt env tv

84 let tt' = normalise ctxt env tt

107 let tt' = normalise ctxt env tt

85− isSet ctxt env tt'

108+ lift $ isSet ctxt env tt'

86 return (Pi tv)

109 return (Pi tv)

87 checkBinder (Let t v)

110 checkBinder (Let t v)

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

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

89 (vv, vt) <- chk env v

112 (vv, vt) <- chk env v

90 let tv' = normalise ctxt env tv

113 let tv' = normalise ctxt env tv

91 let tt' = normalise ctxt env tt

114 let tt' = normalise ctxt env tt

92− converts ctxt env tv vt

115+ convertsC ctxt env tv vt

93− isSet ctxt env tt'

116+ lift $ isSet ctxt env tt'

94 return (Let tv vv)

117 return (Let tv vv)

95 checkBinder (NLet t v)

118 checkBinder (NLet t v)

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

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

97 (vv, vt) <- chk env v

120 (vv, vt) <- chk env v

98 let tv' = normalise ctxt env tv

121 let tv' = normalise ctxt env tv

99 let tt' = normalise ctxt env tt

122 let tt' = normalise ctxt env tt

100− converts ctxt env tv vt

123+ convertsC ctxt env tv vt

101− isSet ctxt env tt'

124+ lift $ isSet ctxt env tt'

102 return (NLet tv vv)

125 return (NLet tv vv)

103 checkBinder (Hole t)

126 checkBinder (Hole t)

104− | not holes = tfail (IncompleteTerm undefined)

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

105 | otherwise

128 | otherwise

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

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

107 let tv' = normalise ctxt env tv

130 let tv' = normalise ctxt env tv

108 let tt' = normalise ctxt env tt

131 let tt' = normalise ctxt env tt

109− isSet ctxt env tt'

132+ lift $ isSet ctxt env tt'

110 return (Hole tv)

133 return (Hole tv)

111 checkBinder (GHole t)

134 checkBinder (GHole t)

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

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

113 let tv' = normalise ctxt env tv

136 let tv' = normalise ctxt env tv

114 let tt' = normalise ctxt env tt

137 let tt' = normalise ctxt env tt

115− isSet ctxt env tt'

138+ lift $ isSet ctxt env tt'

116 return (GHole tv)

139 return (GHole tv)

117 checkBinder (Guess t v)

140 checkBinder (Guess t v)

118− | not holes = tfail (IncompleteTerm undefined)

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

119 | otherwise

142 | otherwise

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

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

121 (vv, vt) <- chk env v

144 (vv, vt) <- chk env v

122 let tv' = normalise ctxt env tv

145 let tv' = normalise ctxt env tv

123 let tt' = normalise ctxt env tt

146 let tt' = normalise ctxt env tt

124− converts ctxt env tv vt

147+ convertsC ctxt env tv vt

125− isSet ctxt env tt'

148+ lift $ isSet ctxt env tt'

126 return (Guess tv vv)

149 return (Guess tv vv)

127 checkBinder (PVar t)

150 checkBinder (PVar t)

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

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

129 let tv' = normalise ctxt env tv

152 let tv' = normalise ctxt env tv

130 let tt' = normalise ctxt env tt

153 let tt' = normalise ctxt env tt

131− isSet ctxt env tt'

154+ lift $ isSet ctxt env tt'

132 return (PVar tv)

155 return (PVar tv)

133 checkBinder (PVTy t)

156 checkBinder (PVTy t)

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

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

135 let tv' = normalise ctxt env tv

158 let tv' = normalise ctxt env tv

136 let tt' = normalise ctxt env tt

159 let tt' = normalise ctxt env tt

137− isSet ctxt env tt'

160+ lift $ isSet ctxt env tt'

138 return (PVTy tv)

161 return (PVTy tv)

139

162

140 discharge n (Lam t) scv sct

163 discharge n (Lam t) scv sct

src/Idris/AbsSyntax.hs+13−5

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

47 errLine :: Maybe Int

48 }

50−idrisInit = IState emptyContext [] emptyContext emptyContext emptyContext

50+idrisInit = IState initContext [] emptyContext emptyContext emptyContext

51 "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing

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

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

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

101checkUndefined fc n

102 = do i <- getContext

103− case lookupCtxt n i of

103+ case lookupTy n i of

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

105 show n ++ " already defined"

106 _ -> return ()

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

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

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

113

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+

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

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

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

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

116 i <- get

124 i <- get

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

176

184

178 | Compile String | Execute String

186 | Compile String | Execute String

179− | Metavars | Prove Name

187+ | Metavars | Prove Name | Universes

180 | TTShell

188 | TTShell

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

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

182 | NOP

190 | NOP

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

546 where

554 where

547 ni env (PRef _ n)

555 ni env (PRef _ n)

548 | not (n `elem` env)

556 | not (n `elem` env)

549− = case lookupCtxt n (tt_ctxt ist) of

557+ = case lookupTy n (tt_ctxt ist) of

550 Nothing -> [n]

558 Nothing -> [n]

551 _ -> []

559 _ -> []

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

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

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

572 (PRef bi inferTy)), bi)]

580 (PRef bi inferTy)), bi)]

573

581

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

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

576

584

577getInferTerm, getInferType :: Term -> Term

585getInferTerm, getInferType :: Term -> Term

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

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

src/Idris/Compiler.hs+1−1

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

27mkDecls :: Idris [EpicDecl]

28mkDecls = do i <- getIState

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

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

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

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

src/Idris/ElabDecls.hs+25−21

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

29toplevel = EInfo [] emptyContext id

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

32+ addConstraints cs

33+ return (tm, ty)

34+

31checkDef ns = do ctxt <- getContext

35checkDef ns = do ctxt <- getContext

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

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

33 return (n, t')) ns

37 return (n, t')) ns

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

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

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

41 ty' <- implicit syn n ty'

45 ty' <- implicit syn n ty'

42 let ty = addImpl i ty'

46 let ty = addImpl i ty'

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

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

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

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

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

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

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

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

48 let nty = normalise ctxt [] cty

52 let nty = normalise ctxt [] cty

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

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

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

57 i <- get

61 i <- get

58 t_in <- implicit syn n t_in

62 t_in <- implicit syn n t_in

59 let t = addImpl i t_in

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

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

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

62 def' <- checkDef defer

66 def' <- checkDef defer

63 addDeferred def'

67 addDeferred def'

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

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

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

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

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

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

67 cons <- mapM (elabCon info syn) dcons

71 cons <- mapM (elabCon info syn) dcons

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

76 t_in <- implicit syn n t_in

80 t_in <- implicit syn n t_in

77 let t = addImpl i t_in

81 let t = addImpl i t_in

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

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

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

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

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

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

82 def' <- checkDef defer

86 def' <- checkDef defer

83 addDeferred def'

87 addDeferred def'

84 ctxt <- getContext

88 ctxt <- getContext

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

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

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

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

87 return (n, cty)

91 return (n, cty)

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

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

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

119 let vtm = getInferTerm tm'

123 let vtm = getInferTerm tm'

120 logLvl 2 (show vtm)

124 logLvl 2 (show vtm)

121− tclift $ recheck ctxt [] vtm

125+ recheckC ctxt [] vtm

122

126

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

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

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

128elabClause 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)

133 let lhs_tm = orderPats (getInferTerm lhs')

137 let lhs_tm = orderPats (getInferTerm lhs')

134 let lhs_ty = getInferType lhs'

138 let lhs_ty = getInferType lhs'

135 logLvl 3 (show lhs_tm)

139 logLvl 3 (show lhs_tm)

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

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

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

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

138 -- Elaborate where block

142 -- Elaborate where block

139 ist <- getIState

143 ist <- getIState

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

163 def' <- checkDef defer

167 def' <- checkDef defer

164 addDeferred def'

168 addDeferred def'

165 ctxt <- getContext

169 ctxt <- getContext

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

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

167 return (clhs, crhs)

171 return (clhs, crhs)

168 where

172 where

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

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

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

193 let lhs_ty = getInferType lhs'

197 let lhs_ty = getInferType lhs'

194 let ret_ty = getRetTy lhs_ty

198 let ret_ty = getRetTy lhs_ty

195 logLvl 3 (show lhs_tm)

199 logLvl 3 (show lhs_tm)

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

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

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

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

198 let bargs = getPBtys lhs_tm

202 let bargs = getPBtys lhs_tm

199 let wval = addImpl i wval_in

203 let wval = addImpl i wval_in

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

210 return (tt, d))

214 return (tt, d))

211 def' <- checkDef defer

215 def' <- checkDef defer

212 addDeferred def'

216 addDeferred def'

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

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

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

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

215 windex <- getName

219 windex <- getName

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

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

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

245 return (tt, d))

249 return (tt, d))

246 def' <- checkDef defer

250 def' <- checkDef defer

247 addDeferred def'

251 addDeferred def'

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

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

249 return (clhs, crhs)

253 return (clhs, crhs)

250 where

254 where

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

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

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

522 local f = do e <- get_env

526 local f = do e <- get_env

523 return (f `elem` map fst e)

527 return (f `elem` map fst e)

524

528

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

529+ elab' PSet = do fill RSet; solve

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

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

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

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

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

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

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

560 pexp l, pexp r])

564 pexp l, pexp r])

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

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

562 = do ctxt <- get_context

566 = do ctxt <- get_context

563− let sc = case lookupCtxt n ctxt of

567+ let sc = case lookupTy n ctxt of

564 Nothing -> True

568 Nothing -> True

565 _ -> False

569 _ -> False

566 if sc

570 if sc

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

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

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

577 elab' (PLam n ty sc)

581 elab' (PLam n ty sc)

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

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

579− claim tyn (RSet 0)

583+ claim tyn RSet

580 attack

584 attack

581 introTy (Var tyn) (Just n)

585 introTy (Var tyn) (Just n)

582 -- end_unify

586 -- end_unify

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

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

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

589 elab' (PPi _ n ty sc)

593 elab' (PPi _ n ty sc)

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

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

591− claim tyn (RSet 0)

595+ claim tyn RSet

592 n' <- case n of

596 n' <- case n of

593 MN _ _ -> unique_hole n

597 MN _ _ -> unique_hole n

594 _ -> return n

598 _ -> return n

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

600 elab' (PLet n ty val sc)

604 elab' (PLet n ty val sc)

601 = do attack;

605 = do attack;

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

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

603− claim tyn (RSet 0)

607+ claim tyn RSet

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

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

605 claim valn (Var tyn)

609 claim valn (Var tyn)

606 letbind n (Var tyn) (Var valn)

610 letbind n (Var tyn) (Var valn)

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

682 = do t <- goal

686 = do t <- goal

683 tm <- get_term

687 tm <- get_term

684 try (trivial ist)

688 try (trivial ist)

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

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

686 where

690 where

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

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

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

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

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

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

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

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

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

755 -- start_unify h

759 -- start_unify h

756− claim tyn (RSet 0)

760+ claim tyn RSet

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

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

758 claim valn (Var tyn)

762 claim valn (Var tyn)

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

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

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

765 runT (LetTac n tm)

769 runT (LetTac n tm)

766 = do attack

770 = do attack

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

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

768− claim tyn (RSet 0)

772+ claim tyn RSet

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

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

770 claim valn (Var tyn)

774 claim valn (Var tyn)

771 letn <- unique_hole n

775 letn <- unique_hole n

src/Idris/Prover.hs+1−1

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

37 lift $ dumpProof n prf

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

39 logLvl 3 (show tree)

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

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

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

42 solveDeferred n

src/Idris/REPL.hs+4

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

110 let ty' = normaliseC ctxt [] ty

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

112 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)"

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

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

114 lift $ print (lookupDef n ctxt)

118 lift $ print (lookupDef n ctxt)

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

119process (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)

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

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

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

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

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

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

38 <|> do eof; return NOP

39 <|> do eof; return NOP