fdfa04c · Idris-dev · git.iko.soy

libs/base/Language/Reflection/Utils.idr+4−4

compare with master

unifiedsplit

@@ -122,13 +122,13 @@ mutual

122 _ == _ = False

123

124implementation Show TTUExp where

125− showPrec d (UVar i) = showCon d "UVar" $ showArg i

125+ showPrec d (UVar ns i) = showCon d "UVar" $ showArg ns ++ showArg i

126 showPrec d (UVal i) = showCon d "UVal" $ showArg i

127

128implementation Eq TTUExp where

129− (UVar i) == (UVar j) = i == j

129+ (UVar nsi i) == (UVar nsj j) = nsi == nsj && i == j

130− (UVal i) == (UVal j) = i == j

130+ (UVal i) == (UVal j) = i == j

131− x == y = False

131+ x == y = False

132

133implementation Show NativeTy where

134 show IT8 = "IT8"

libs/prelude/Language/Reflection.idr+3−3

@@ -573,7 +573,7 @@ implementation DecEq SpecialName where

573

574data TTUExp =

575 ||| Universe variable

576− UVar Int |

576+ UVar String Int |

577 ||| Explicit universe level

578 UVal Int

579%name TTUExp uexp

@@ -1026,12 +1026,12 @@ mutual

1026

1027implementation Quotable TTUExp TT where

1028 quotedTy = `(TTUExp)

1029− quote (UVar x) = `(UVar ~(quote x))

1029+ quote (UVar ns x) = `(UVar ~(quote ns) ~(quote x))

1030 quote (UVal x) = `(UVal ~(quote x))

1031

1032implementation Quotable TTUExp Raw where

1033 quotedTy = `(TTUExp)

1034− quote (UVar x) = `(UVar ~(quote {t=Raw} x))

1034+ quote (UVar ns x) = `(UVar ~(quote ns) ~(quote {t=Raw} x))

1035 quote (UVal x) = `(UVal ~(quote {t=Raw} x))

1036

1037implementation Quotable NativeTy TT where

src/Idris/AbsSyntax.hs+2

@@ -700,6 +700,8 @@ addConstraints fc (v, cs)

700 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }

701 where

702 insertAll [] c = c

703+ insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics

704+ insertAll ((ULE x y, fc) : cs) ics | x == y = insertAll cs ics

703 insertAll ((c, fc) : cs) ics

705 insertAll ((c, fc) : cs) ics

704 = insertAll cs $ S.insert (ConstraintFC c fc) ics

706 = insertAll cs $ S.insert (ConstraintFC c fc) ics

705

707

src/Idris/AbsSyntaxTree.hs+15−9

@@ -65,8 +65,9 @@ data ElabInfo = EInfo {

65 params :: [(Name, PTerm)]

66 , inblock :: Ctxt [Name] -- ^ names in the block, and their params

67 , liftname :: Name -> Name

68− , namespace :: Maybe [String]

68+ , namespace :: [String]

69 , elabFC :: Maybe FC

70+ , constraintNS :: String -- ^ filename for adding to constraint variables

70 , pe_depth :: Int

71 , pe_depth :: Int

71

72

72 -- | We may, recursively, collect transformations to do on the rhs,

73 -- | We may, recursively, collect transformations to do on the rhs,

@@ -76,7 +77,10 @@ data ElabInfo = EInfo {

76 }

77 }

77

78

78toplevel :: ElabInfo

79toplevel :: ElabInfo

79−toplevel = EInfo [] emptyContext id Nothing Nothing 0 id (\_ _ _ -> fail "Not implemented")

80+toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 id (\_ _ _ -> fail "Not implemented")

81+

82+toplevelWith :: String -> ElabInfo

83+toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 id (\_ _ _ -> fail "Not implemented")

80

84

81eInfoNames :: ElabInfo -> [Name]

85eInfoNames :: ElabInfo -> [Name]

82eInfoNames info = map fst (params info) ++ M.keys (inblock info)

86eInfoNames info = map fst (params info) ++ M.keys (inblock info)

@@ -378,6 +382,7 @@ data IBCWrite = IBCFix FixDecl

378 | IBCAutoHint Name Name

382 | IBCAutoHint Name Name

379 | IBCDeprecate Name String

383 | IBCDeprecate Name String

380 | IBCFragile Name String

384 | IBCFragile Name String

385+ | IBCConstraint FC UConstraint

381 deriving Show

386 deriving Show

382

387

383-- | The initial state for the compiler

388-- | The initial state for the compiler

@@ -1668,13 +1673,14 @@ expandNS syn n = case syn_namespace syn of

1668-- For inferring types of things

1673-- For inferring types of things

1669

1674

1670bi = fileFC "builtin"

1675bi = fileFC "builtin"

1676+primfc = fileFC "(primitive)"

1671

1677

1672inferTy = sMN 0 "__Infer"

1678inferTy = sMN 0 "__Infer"

1673inferCon = sMN 0 "__infer"

1679inferCon = sMN 0 "__infer"

1674−inferDecl = PDatadecl inferTy NoFC

1680+inferDecl = PDatadecl inferTy primfc

1675 (PType bi)

1681 (PType bi)

1676− [(emptyDocstring, [], inferCon, NoFC, PPi impl (sMN 0 "iType") NoFC (PType bi) (

1682+ [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (

1677− PPi expl (sMN 0 "ival") NoFC (PRef bi [] (sMN 0 "iType"))

1683+ PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))

1678 (PRef bi [] inferTy)), bi, [])]

1684 (PRef bi [] inferTy)), bi, [])]

1679inferOpts = []

1685inferOpts = []

1680

1686

@@ -1687,7 +1693,7 @@ getInferTerm (App _ (App _ _ _) tm) = tm

1687getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

1693getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

1688

1694

1689getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc

1695getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc

1690− where toTy (Lam t) = Pi Nothing t (TType (UVar 0))

1696+ where toTy (Lam t) = Pi Nothing t (TType (UVar [] 0))

1691 toTy (PVar t) = PVTy t

1697 toTy (PVar t) = PVTy t

1692 toTy b = b

1698 toTy b = b

1693getInferType (App _ (App _ _ ty) _) = ty

1699getInferType (App _ (App _ _ ty) _) = ty

@@ -1728,12 +1734,12 @@ eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $

1728 "\n\n" ++

1734 "\n\n" ++

1729 "You may need to use `(~=~)` to explicitly request heterogeneous equality."

1735 "You may need to use `(~=~)` to explicitly request heterogeneous equality."

1730

1736

1731−eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]

1737+eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]

1732 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]

1738 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]

1733 (PType bi)))

1739 (PType bi)))

1734 [(reflDoc, reflParamDoc,

1740 [(reflDoc, reflParamDoc,

1735− eqCon, NoFC, PPi impl (n "A") NoFC (PType bi) (

1741+ eqCon, primfc, PPi impl (n "A") primfc (PType bi) (

1736− PPi impl (n "x") NoFC (PRef bi [] (n "A"))

1742+ PPi impl (n "x") primfc (PRef bi [] (n "A"))

1737 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,

1743 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,

1738 pimp (n "B") Placeholder False,

1744 pimp (n "B") Placeholder False,

1739 pexp (PRef bi [] (n "x")),

1745 pexp (PRef bi [] (n "x")),

src/Idris/CaseSplit.hs+2−2

@@ -68,7 +68,7 @@ split n t'

68 mapM_ (\n -> setAccessibility n Public) (allNamesIn t')

69 -- ETyDecl rather then ELHS because there'll be explicit type

70 -- matching

71− (tm, ty, pats) <- elabValBind recinfo ETyDecl True (addImplPat ist t')

71+ (tm, ty, pats) <- elabValBind (recinfo (fileFC "casesplit")) ETyDecl True (addImplPat ist t')

72 -- ASSUMPTION: tm is in normal form after elabValBind, so we don't

73 -- need to do anything special to find out what family each argument

74 -- is in

@@ -242,7 +242,7 @@ tidy ist tm ty = return tm

242-- tidyVar t = t

243

244elabNewPat :: PTerm -> Idris (Bool, PTerm)

245−elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t

245+elabNewPat t = idrisCatch (do (tm, ty) <- elabVal (recinfo (fileFC "casesplit")) ELHS t

246 i <- getIState

247 return (True, delab i tm))

248 (\e -> do i <- getIState

src/Idris/Core/Binary.hs+5−3

@@ -592,15 +592,17 @@ instance Binary NameType where

592-- record concrete levels only, for now

593instance Binary UExp where

594 put x = case x of

595− UVar t -> do putWord8 0

595+ UVar ns t -> do putWord8 0

596− put ((-1) :: Int) -- TMP HACK!

596+ put ns

597+ put t

597 UVal t -> do putWord8 1

598 UVal t -> do putWord8 1

598 put t

599 put t

599

600

600 get = do i <- getWord8

601 get = do i <- getWord8

601 case i of

602 case i of

602 0 -> do x1 <- get

603 0 -> do x1 <- get

604+ x2 <- get

603− return (UVar x1)

605+ return (UVar x1 x2)

604 1 -> do x1 <- get

606 1 -> do x1 <- get

605 return (UVal x1)

607 return (UVal x1)

606 _ -> error "Corrupted binary data for UExp"

608 _ -> error "Corrupted binary data for UExp"

src/Idris/Core/Constraints.hs+19−20

@@ -16,17 +16,16 @@ import Data.List ( partition )

16import qualified Data.Map.Strict as M

17import qualified Data.Set as S

18

19−

20-- | Check that a list of universe constraints can be satisfied.

19-- | Check that a list of universe constraints can be satisfied.

21ucheck :: S.Set ConstraintFC -> TC ()

20ucheck :: S.Set ConstraintFC -> TC ()

22ucheck = void . solve 10 . S.filter (not . ignore)

21ucheck = void . solve 10 . S.filter (not . ignore)

23 where

22 where

24 -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with

23 -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with

25− ignore (ConstraintFC c _) | any (== Var (-1)) (varsIn c) = True

24+ ignore (ConstraintFC c _) | any (== Var [] (-1)) (varsIn c) = True

26 ignore (ConstraintFC (ULE a b) _) = a == b

25 ignore (ConstraintFC (ULE a b) _) = a == b

27 ignore _ = False

26 ignore _ = False

28

27

29−newtype Var = Var Int

28+data Var = Var String Int

30 deriving (Eq, Ord, Show)

29 deriving (Eq, Ord, Show)

31

30

32data Domain = Domain Int Int

31data Domain = Domain Int Int

@@ -72,12 +71,12 @@ solve maxUniverseLevel ucs =

72 , cons_rhs = constraintsRHS

71 , cons_rhs = constraintsRHS

73 }

72 }

74

73

75− lhs (ULT (UVar x) _) = Just (Var x)

74+ lhs (ULT (UVar ns x) _) = Just (Var ns x)

76− lhs (ULE (UVar x) _) = Just (Var x)

75+ lhs (ULE (UVar ns x) _) = Just (Var ns x)

77 lhs _ = Nothing

76 lhs _ = Nothing

78

77

79− rhs (ULT _ (UVar x)) = Just (Var x)

78+ rhs (ULT _ (UVar ns x)) = Just (Var ns x)

80− rhs (ULE _ (UVar x)) = Just (Var x)

79+ rhs (ULE _ (UVar ns x)) = Just (Var ns x)

81 rhs _ = Nothing

80 rhs _ = Nothing

82

81

83 -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)

82 -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)

@@ -148,38 +147,38 @@ solve maxUniverseLevel ucs =

148 -- | look up the domain of a variable from the state.

147 -- | look up the domain of a variable from the state.

149 -- for convenience, this function also accepts UVal's and returns a singleton domain for them.

148 -- for convenience, this function also accepts UVal's and returns a singleton domain for them.

150 domainOf :: MonadState SolverState m => UExp -> m Domain

149 domainOf :: MonadState SolverState m => UExp -> m Domain

151− domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)

150+ domainOf (UVar ns var) = gets (fst . (M.! Var ns var) . domainStore)

152 domainOf (UVal val) = return (Domain val val)

151 domainOf (UVal val) = return (Domain val val)

153

152

154 asPair :: Domain -> (Int, Int)

153 asPair :: Domain -> (Int, Int)

155 asPair (Domain x y) = (x, y)

154 asPair (Domain x y) = (x, y)

156

155

157 updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()

156 updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()

158− updateUpperBoundOf suspect (UVar var) upper = do

157+ updateUpperBoundOf suspect (UVar ns var) upper = do

159 doms <- gets domainStore

158 doms <- gets domainStore

160− let (oldDom@(Domain lower _), suspects) = doms M.! Var var

159+ let (oldDom@(Domain lower _), suspects) = doms M.! Var ns var

161 let newDom = Domain lower upper

160 let newDom = Domain lower upper

162 when (wipeOut newDom) $

161 when (wipeOut newDom) $

163 lift $ Error $

162 lift $ Error $

164− UniverseError (ufc suspect) (UVar var)

163+ UniverseError (ufc suspect) (UVar ns var)

165 (asPair oldDom) (asPair newDom)

164 (asPair oldDom) (asPair newDom)

166 (suspect : S.toList suspects)

165 (suspect : S.toList suspects)

167− modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }

166+ modify $ \ st -> st { domainStore = M.insert (Var ns var) (newDom, S.insert suspect suspects) doms }

168− addToQueueRHS (uconstraint suspect) (Var var)

167+ addToQueueRHS (uconstraint suspect) (Var ns var)

169 updateUpperBoundOf _ UVal{} _ = return ()

168 updateUpperBoundOf _ UVal{} _ = return ()

170

169

171 updateLowerBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()

170 updateLowerBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()

172− updateLowerBoundOf suspect (UVar var) lower = do

171+ updateLowerBoundOf suspect (UVar ns var) lower = do

173 doms <- gets domainStore

172 doms <- gets domainStore

174− let (oldDom@(Domain _ upper), suspects) = doms M.! Var var

173+ let (oldDom@(Domain _ upper), suspects) = doms M.! Var ns var

175 let newDom = Domain lower upper

174 let newDom = Domain lower upper

176 when (wipeOut newDom) $

175 when (wipeOut newDom) $

177 lift $ Error $

176 lift $ Error $

178− UniverseError (ufc suspect) (UVar var)

177+ UniverseError (ufc suspect) (UVar ns var)

179 (asPair oldDom) (asPair newDom)

178 (asPair oldDom) (asPair newDom)

180 (suspect : S.toList suspects)

179 (suspect : S.toList suspects)

181− modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }

180+ modify $ \ st -> st { domainStore = M.insert (Var ns var) (newDom, S.insert suspect suspects) doms }

182− addToQueueLHS (uconstraint suspect) (Var var)

181+ addToQueueLHS (uconstraint suspect) (Var ns var)

183 updateLowerBoundOf _ UVal{} _ = return ()

182 updateLowerBoundOf _ UVal{} _ = return ()

184

183

185 -- | add all constraints (with the given var on the lhs) to the queue

184 -- | add all constraints (with the given var on the lhs) to the queue

@@ -224,5 +223,5 @@ ordNub = S.toList . S.fromList

224

223

225-- | variables in a constraint

224-- | variables in a constraint

226varsIn :: UConstraint -> [Var]

225varsIn :: UConstraint -> [Var]

227−varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]

226+varsIn (ULT a b) = [ Var ns v | UVar ns v <- [a,b] ]

228−varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]

227+varsIn (ULE a b) = [ Var ns v | UVar ns v <- [a,b] ]

src/Idris/Core/DeepSeq.hs+1−1

@@ -188,7 +188,7 @@ instance (NFData b) => NFData (Binder b) where

188 rnf (PVTy x1) = rnf x1 `seq` ()

189

190instance NFData UExp where

191− rnf (UVar x1) = rnf x1 `seq` ()

191+ rnf (UVar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

192 rnf (UVal x1) = rnf x1 `seq` ()

193

194instance NFData NameType where

src/Idris/Core/Elaborate.hs+4−3

@@ -151,6 +151,7 @@ execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)

151execElab a e ps = execStateT e (ES (ps, a) "" Nothing)

152

153initElaborator :: Name -- ^ the name of what's to be elaborated

154+ -> String -- ^ the current source file

154 -> Context -- ^ the current global context

155 -> Context -- ^ the current global context

155 -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState

156 -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState

156 -> Int -- ^ the value of the idris_name field of IState

157 -> Int -- ^ the value of the idris_name field of IState

@@ -158,9 +159,9 @@ initElaborator :: Name -- ^ the name of what's to be elaborated

158 -> ProofState

159 -> ProofState

159initElaborator = newProof

160initElaborator = newProof

160

161

161−elaborate :: Context -> Ctxt TypeInfo -> Int -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)

162+elaborate :: String -> Context -> Ctxt TypeInfo -> Int -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)

162−elaborate ctxt datatypes globalNames n ty d elab =

163+elaborate tcns ctxt datatypes globalNames n ty d elab =

163− do let ps = initElaborator n ctxt datatypes globalNames ty

164+ do let ps = initElaborator n tcns ctxt datatypes globalNames ty

164 (a, ES ps' str _) <- runElab d elab ps

165 (a, ES ps' str _) <- runElab d elab ps

165 return $! (a, str)

166 return $! (a, str)

166

167

src/Idris/Core/Evaluate.hs+5−3

@@ -633,9 +633,11 @@ convEq ctxt holes topx topy = ceq [] topx topy where

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

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

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

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

636+ ceq ps (TType x) (TType y) | x == y = return True

637+ ceq ps (TType (UVal 0)) (TType y) = return True

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

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

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

638− return True

640+ return True

639 ceq ps (UType AllTypes) x = return (isUsableUniverse x)

641 ceq ps (UType AllTypes) x = return (isUsableUniverse x)

640 ceq ps x (UType AllTypes) = return (isUsableUniverse x)

642 ceq ps x (UType AllTypes) = return (isUsableUniverse x)

641 ceq ps (UType u) (UType v) = return (u == v)

643 ceq ps (UType u) (UType v) = return (u == v)

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

@@ -60,7 +60,8 @@ data ProofState = PS { thname :: Name,

60 unifylog :: Bool,

61 done :: Bool,

62 recents :: [Name],

63− while_elaborating :: [FailContext]

63+ while_elaborating :: [FailContext],

64+ constraint_ns :: String

64 }

65 }

65

66

66data Tactic = Attack

67data Tactic = Attack

@@ -319,19 +320,20 @@ addLog :: Monad m => String -> StateT TState m ()

319addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

320addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

320

321

321newProof :: Name -- ^ the name of what's to be elaborated

322newProof :: Name -- ^ the name of what's to be elaborated

323+ -> String -- ^ current source file

322 -> Context -- ^ the current global context

324 -> Context -- ^ the current global context

323 -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState

325 -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState

324 -> Int -- ^ the value of the idris_name field of IState

326 -> Int -- ^ the value of the idris_name field of IState

325 -> Type -- ^ the goal type

327 -> Type -- ^ the goal type

326 -> ProofState

328 -> ProofState

327−newProof n ctxt datatypes globalNames ty =

329+newProof n tcns ctxt datatypes globalNames ty =

328 let h = holeName 0

330 let h = holeName 0

329 ty' = vToP ty

331 ty' = vToP ty

330 in PS n [h] [] 1 globalNames (mkProofTerm (Bind h (Hole ty')

332 in PS n [h] [] 1 globalNames (mkProofTerm (Bind h (Hole ty')

331 (P Bound h ty'))) ty [] (h, []) [] []

333 (P Bound h ty'))) ty [] (h, []) [] []

332 Nothing [] []

334 Nothing [] []

333 [] [] [] []

335 [] [] [] []

334− Nothing ctxt datatypes "" False False [] []

336+ Nothing ctxt datatypes "" False False [] [] tcns

335

337

336type TState = ProofState -- [TacticAction])

338type TState = ProofState -- [TacticAction])

337type RunTactic = RunTactic' TState

339type RunTactic = RunTactic' TState

@@ -468,7 +470,7 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

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

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

469 where

471 where

470 mkTy [] t = t

472 mkTy [] t = t

471− mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar 0))) (mkTy bs t)

473+ mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar [] 0))) (mkTy bs t)

472

474

473 getP (n, b) = P Bound n (binderTy b)

475 getP (n, b) = P Bound n (binderTy b)

474defer dropped n ctxt env _ = fail "Can't defer a non-hole focus."

476defer dropped n ctxt env _ = fail "Can't defer a non-hole focus."

@@ -683,9 +685,9 @@ intro n ctxt env _ = fail "Can't introduce here."

683forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic

685forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic

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

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

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

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

686− unify' ctxt env (tyt, Nothing) (TType (UVar 0), Nothing)

688+ unify' ctxt env (tyt, Nothing) (TType (UVar [] 0), Nothing)

687− unify' ctxt env (t, Nothing) (TType (UVar 0), Nothing)

689+ unify' ctxt env (t, Nothing) (TType (UVar [] 0), Nothing)

688− return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

690+ return $ Bind n (Pi impl tyv (TType (UVar [] 0))) (Bind x (Hole t) (P Bound x t))

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

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

690

692

691patvar :: Name -> RunTactic

693patvar :: Name -> RunTactic

@@ -1020,7 +1022,7 @@ matchProblems all ps updates probs = up updates probs where

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

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

1021processTactic QED ps = case holes ps of

1023processTactic QED ps = case holes ps of

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

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

1023− (tm', ty', _) <- recheck (context ps) [] (forget tm) tm

1025+ (tm', ty', _) <- recheck (constraint_ns ps) (context ps) [] (forget tm) tm

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

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

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

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

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

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

src/Idris/Core/TT.hs+8−4

@@ -38,7 +38,7 @@ module Idris.Core.TT(

38 , bindingOf, bindTyArgs, caseName, constDocs, constIsType, deleteDefExact

39 , discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname

40 , fc_start, fcIn, fileFC, finalise, fmapMB, forget, forgetEnv

41− , freeNames, getArgTys, getRetTy, implicitable, instantiate

41+ , freeNames, getArgTys, getRetTy, implicitable, instantiate, internalNS

42 , intTyName, isInjective, isTypeConst, lookupCtxt

43 , lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth

44 , nextName, noOccurrence, nsroot, occurrences

@@ -945,8 +945,11 @@ raw_unapply t = ua [] t where

945

946-- WELL TYPED TERMS ---------------------------------------------------------

947

948+internalNS :: String

949+internalNS = "(internal)"

950+

948-- | Universe expressions for universe checking

951-- | Universe expressions for universe checking

949−data UExp = UVar Int -- ^ universe variable

952+data UExp = UVar String Int -- ^ universe variable, with source file to disambiguate

950 | UVal Int -- ^ explicit universe level

953 | UVal Int -- ^ explicit universe level

951 deriving (Eq, Ord, Data, Typeable)

954 deriving (Eq, Ord, Data, Typeable)

952{-!

955{-!

@@ -957,8 +960,9 @@ instance Sized UExp where

957 size _ = 1

960 size _ = 1

958

961

959instance Show UExp where

962instance Show UExp where

963+ show (UVar ns x)

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

964+ | x < 26 = ns ++ "." ++ [toEnum (x + fromEnum 'a')]

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

965+ | otherwise = ns ++ "." ++ toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)

962 show (UVal x) = show x

966 show (UVal x) = show x

963-- show (UMax l r) = "max(" ++ show l ++ ", " ++ show r ++")"

967-- show (UMax l r) = "max(" ++ show l ++ ", " ++ show r ++")"

964

968

src/Idris/Core/Typecheck.hs+27−28

@@ -58,22 +58,22 @@ isType ctxt env tm = isType' (normalise ctxt env tm)

58 where isType' tm | isUniverse tm = return ()

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

60

61−convType :: Context -> Env -> Term -> StateT UCs TC ()

61+convType :: String -> Context -> Env -> Term -> StateT UCs TC ()

62−convType ctxt env tm =

62+convType tcns ctxt env tm =

63 do (v, cs) <- get

64 put (v + 1, cs)

65 case normalise ctxt env tm of

66 UType _ -> return ()

67− _ -> convertsC ctxt env tm (TType (UVar v))

67+ _ -> convertsC ctxt env tm (TType (UVar tcns v))

68

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

69+recheck :: String -> Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)

70recheck = recheck_borrowing False []

71

72−recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term ->

72+recheck_borrowing :: Bool -> [Name] -> String -> Context -> Env -> Raw -> Term ->

73 TC (Term, Type, UCs)

74−recheck_borrowing uniq_check bs ctxt env tm orig

74+recheck_borrowing uniq_check bs tcns ctxt env tm orig

75 = let v = next_tvar ctxt in

76− case runStateT (check' False ctxt env tm) (v, []) of -- holes banned

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

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

78 Error e -> Error e

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

@@ -82,10 +82,11 @@ recheck_borrowing uniq_check bs ctxt env tm orig

82

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

84check ctxt env tm

85+ -- Holes allowed, so constraint namespace doesn't matter

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

86+ = evalStateT (check' True [] ctxt env tm) (0, [])

86

87

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

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

88−check' holes ctxt env top = chk (TType (UVar (-5))) env top where

89+check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

89

90

90 smaller (UType NullType) _ = UType NullType

91 smaller (UType NullType) _ = UType NullType

91 smaller _ (UType NullType) = UType NullType

92 smaller _ (UType NullType) = UType NullType

@@ -120,10 +121,10 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

120 case fty' of

121 case fty' of

121 Bind x (Pi i (TType v') k) t ->

122 Bind x (Pi i (TType v') k) t ->

122 do (v, cs) <- get

123 do (v, cs) <- get

123− put (v+1, ULT (UVar v) v' : cs)

124+ put (v+1, ULT (UVar tcns v) v' : cs)

124 let apty = simplify initContext env

125 let apty = simplify initContext env

125− (Bind x (Let (TType v') (TType (UVar v))) t)

126+ (Bind x (Let (TType v') (TType (UVar tcns v))) t)

126− return (App Complete fv (TType (UVar v)), apty)

127+ return (App Complete fv (TType (UVar tcns v)), apty)

127 Bind x (Pi i s k) t ->

128 Bind x (Pi i s k) t ->

128 do (av, aty) <- chk u env RType

129 do (av, aty) <- chk u env RType

129 convertsC ctxt env aty s

130 convertsC ctxt env aty s

@@ -150,9 +151,9 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

150 chk u env RType

151 chk u env RType

151 | holes = return (TType (UVal 0), TType (UVal 0))

152 | holes = return (TType (UVal 0), TType (UVal 0))

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

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

153− let c = ULT (UVar v) (UVar (v+1))

154+ let c = ULT (UVar tcns v) (UVar tcns (v+1))

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

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

155− return (TType (UVar v), TType (UVar (v+1)))

156+ return (TType (UVar tcns v), TType (UVar tcns (v+1)))

156 chk u env (RUType un)

157 chk u env (RUType un)

157 | holes = return (UType un, TType (UVal 0))

158 | holes = return (UType un, TType (UVal 0))

158 | otherwise = do -- TODO! Issue #1715 on the issue tracker.

159 | otherwise = do -- TODO! Issue #1715 on the issue tracker.

@@ -181,7 +182,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

181 (v, cs) <- get

182 (v, cs) <- get

182 (kv, kt) <- chk u env k -- no need to validate these constraints, they are independent

183 (kv, kt) <- chk u env k -- no need to validate these constraints, they are independent

183 put (v+1, cs)

184 put (v+1, cs)

184− let maxu = UVar v

185+ let maxu = UVar tcns v

185 (tv, tt) <- chk st ((n, Pi i sv kv) : env) t

186 (tv, tt) <- chk st ((n, Pi i sv kv) : env) t

186

187

187-- convertsC ctxt env st (TType maxu)

188-- convertsC ctxt env st (TType maxu)

@@ -195,7 +196,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

195 when (not holes) $ do (v, cs) <- get

196 when (not holes) $ do (v, cs) <- get

196 put (v, ULE su maxu :

197 put (v, ULE su maxu :

197 ULE tu maxu : cs)

198 ULE tu maxu : cs)

198− let k' = TType (UVar v) `smaller` st `smaller` kv `smaller` u

199+ let k' = TType (UVar tcns v) `smaller` st `smaller` kv `smaller` u

199 return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')

200 return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')

200 (pToV n tv), k')

201 (pToV n tv), k')

201 (un, un') ->

202 (un, un') ->

@@ -225,33 +226,33 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

225 where checkBinder (Lam t)

226 where checkBinder (Lam t)

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

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

227 let tv' = normalise ctxt env tv

228 let tv' = normalise ctxt env tv

228− convType ctxt env tt

229+ convType tcns ctxt env tt

229 return (Lam tv, tt)

230 return (Lam tv, tt)

230 checkBinder (Let t v)

231 checkBinder (Let t v)

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

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

232 (vv, vt) <- chk u env v

233 (vv, vt) <- chk u env v

233 let tv' = normalise ctxt env tv

234 let tv' = normalise ctxt env tv

234 convertsC ctxt env vt tv

235 convertsC ctxt env vt tv

235− convType ctxt env tt

236+ convType tcns ctxt env tt

236 return (Let tv vv, tt)

237 return (Let tv vv, tt)

237 checkBinder (NLet t v)

238 checkBinder (NLet t v)

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

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

239 (vv, vt) <- chk u env v

240 (vv, vt) <- chk u env v

240 let tv' = normalise ctxt env tv

241 let tv' = normalise ctxt env tv

241 convertsC ctxt env vt tv

242 convertsC ctxt env vt tv

242− convType ctxt env tt

243+ convType tcns ctxt env tt

243 return (NLet tv vv, tt)

244 return (NLet tv vv, tt)

244 checkBinder (Hole t)

245 checkBinder (Hole t)

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

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

246 | otherwise

247 | otherwise

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

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

248 let tv' = normalise ctxt env tv

249 let tv' = normalise ctxt env tv

249− convType ctxt env tt

250+ convType tcns ctxt env tt

250 return (Hole tv, tt)

251 return (Hole tv, tt)

251 checkBinder (GHole i ns t)

252 checkBinder (GHole i ns t)

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

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

253 let tv' = normalise ctxt env tv

254 let tv' = normalise ctxt env tv

254− convType ctxt env tt

255+ convType tcns ctxt env tt

255 return (GHole i ns tv, tt)

256 return (GHole i ns tv, tt)

256 checkBinder (Guess t v)

257 checkBinder (Guess t v)

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

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

@@ -260,19 +261,19 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

260 (vv, vt) <- chk u env v

261 (vv, vt) <- chk u env v

261 let tv' = normalise ctxt env tv

262 let tv' = normalise ctxt env tv

262 convertsC ctxt env vt tv

263 convertsC ctxt env vt tv

263− convType ctxt env tt

264+ convType tcns ctxt env tt

264 return (Guess tv vv, tt)

265 return (Guess tv vv, tt)

265 checkBinder (PVar t)

266 checkBinder (PVar t)

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

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

267 let tv' = normalise ctxt env tv

268 let tv' = normalise ctxt env tv

268− convType ctxt env tt

269+ convType tcns ctxt env tt

269 -- Normalised version, for erasure purposes (it's easier

270 -- Normalised version, for erasure purposes (it's easier

270 -- to tell if it's a collapsible variable)

271 -- to tell if it's a collapsible variable)

271 return (PVar tv, tt)

272 return (PVar tv, tt)

272 checkBinder (PVTy t)

273 checkBinder (PVTy t)

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

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

274 let tv' = normalise ctxt env tv

275 let tv' = normalise ctxt env tv

275− convType ctxt env tt

276+ convType tcns ctxt env tt

276 return (PVTy tv, tt)

277 return (PVTy tv, tt)

277

278

278 discharge n (Lam t) bt scv sct

279 discharge n (Lam t) bt scv sct

@@ -339,9 +340,7 @@ checkUnique borrowed ctxt env tm

339 StateT [(Name, (UniqueUse, Universe))] TC ()

340 StateT [(Name, (UniqueUse, Universe))] TC ()

340 chkBinderName env n b

341 chkBinderName env n b

341 = do let rawty = forgetEnv (map fst env) (binderTy b)

342 = do let rawty = forgetEnv (map fst env) (binderTy b)

342− (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?

343+ (_, kind) <- lift $ check ctxt env rawty

343− -- Issue #1714 on the issue tracker

344− -- https://github.com/idris-lang/Idris-dev/issues/1714

345 case kind of

344 case kind of

346 UType UniqueType -> do ns <- get

345 UType UniqueType -> do ns <- get

347 if n `elem` borrowed

346 if n `elem` borrowed

src/Idris/Core/Unify.hs+2−2

@@ -494,14 +494,14 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

494 un' env fn bnames (App _ f x) (Bind n (Pi i t k) y)

495 | noOccurrence n y && injectiveApp f

496 = do ux <- un' env False bnames x y

497− uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

497+ uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar [] 0)))

498 (Bind n (Pi i t k) (V 1)))

499 combine env bnames ux uf

500

501 un' env fn bnames (Bind n (Pi i t k) y) (App _ f x)

502 | noOccurrence n y && injectiveApp f

503 = do ux <- un' env False bnames y x

504− uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

504+ uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar [] 0)))

505 (Bind n (Pi i t k) (V 1))) f

506 combine env bnames ux uf

507

src/Idris/DeepSeq.hs+1

@@ -318,6 +318,7 @@ instance NFData IBCWrite where

318 rnf (IBCDeprecate n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

319 rnf (IBCRecord x) = rnf x `seq` ()

320 rnf (IBCFragile n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

321+ rnf (IBCConstraint n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

321

322

323

323instance NFData a => NFData (D.Block a) where

324instance NFData a => NFData (D.Block a) where

src/Idris/Elab/Clause.hs+18−17

@@ -497,7 +497,7 @@ checkPossible info fc tcgen fname lhs_in

497 i <- getIState

498 let lhs = addImplPat i lhs_in

499 -- if the LHS type checks, it is possible

500− case elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

500+ case elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

501 (erun fc (buildTC i info ELHS [] fname

502 (allNamesIn lhs_in)

503 (infTerm lhs))) of

@@ -507,7 +507,7 @@ checkPossible info fc tcgen fname lhs_in

507 sendHighlighting highlights

508 updateIState $ \i -> i { idris_name = newGName }

509 let lhs_tm = orderPats (getInferTerm lhs')

510− case recheck ctxt' [] (forget lhs_tm) lhs_tm of

510+ case recheck (constraintNS info) ctxt' [] (forget lhs_tm) lhs_tm of

511 OK _ -> return True

512 err -> return False

513 -- if it's a recoverable error, the case may become possible

@@ -580,7 +580,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

580 "\n" ++ show (fn_ty, fn_is))

581

582 ((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-

583− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

583+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

584 (do res <- errAt "left hand side of " fname Nothing

585 (erun fc (buildTC i info ELHS opts fname

586 (allNamesIn lhs_in)

@@ -608,7 +608,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

608 ctxt <- getContext

609 (clhs_c, clhsty) <- if not inf

610 then recheckC_borrowing False (PEGenerated `notElem` opts)

611− [] fc id [] lhs_tm

611+ [] (constraintNS info) fc id [] lhs_tm

612 else return (lhs_tm, lhs_ty)

613 let clhs = Idris.Core.Evaluate.simplify ctxt [] clhs_c

614 let borrowed = borrowedNames [] clhs

@@ -666,7 +666,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

666 ctxt <- getContext -- new context with where block added

667 logElab 5 "STARTING CHECK"

668 ((rhs', defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-

669− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState

669+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState

670 (do pbinds ist lhs_tm

671 -- proof search can use explicitly written names

672 mapM_ addPSname (allNamesIn lhs_in)

@@ -697,7 +697,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

697 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)

698

699 -- If there's holes, set the metavariables as undefinable

700− def' <- checkDef fc (\n -> Elaborating "deferred type of " n Nothing) (null holes) defer

700+ def' <- checkDef info fc (\n -> Elaborating "deferred type of " n Nothing) (null holes) defer

701 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, null holes))) def'

702 addDeferred def''

703

@@ -723,7 +723,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

723 -- things)

724 <- if (null holes || null def') && not inf

725 then recheckC_borrowing True (PEGenerated `notElem` opts)

726− borrowed fc id [] rhs'

726+ borrowed (constraintNS info) fc id [] rhs'

727 else return (rhs', clhsty)

728

729 logElab 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty

@@ -738,6 +738,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

738 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of

739 OK (_, cs) -> when (PEGenerated `notElem` opts) $ do

740 addConstraints fc cs

741+ mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)

741 logElab 6 $ "CONSTRAINTS ADDED: " ++ show cs ++ "\n" ++ show (clhsty, crhsty)

742 logElab 6 $ "CONSTRAINTS ADDED: " ++ show cs ++ "\n" ++ show (clhsty, crhsty)

742 return ()

743 return ()

743 Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))

744 Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))

@@ -832,7 +833,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

832 (addImplPat i lhs_in)

833 (addImplPat i lhs_in)

833 logElab 2 ("LHS: " ++ show lhs)

834 logElab 2 ("LHS: " ++ show lhs)

834 (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-

835 (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-

835− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

836+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

836 (errAt "left hand side of with in " fname Nothing

837 (errAt "left hand side of with in " fname Nothing

837 (erun fc (buildTC i info ELHS opts fname

838 (erun fc (buildTC i info ELHS opts fname

838 (allNamesIn lhs_in)

839 (allNamesIn lhs_in)

@@ -848,14 +849,14 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

848 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

849 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

849 let static_names = getStaticNames i lhs_tm

850 let static_names = getStaticNames i lhs_tm

850 logElab 5 (show lhs_tm ++ "\n" ++ show static_names)

851 logElab 5 (show lhs_tm ++ "\n" ++ show static_names)

851− (clhs, clhsty) <- recheckC fc id [] lhs_tm

852+ (clhs, clhsty) <- recheckC (constraintNS info) fc id [] lhs_tm

852 logElab 5 ("Checked " ++ show clhs)

853 logElab 5 ("Checked " ++ show clhs)

853 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

854 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

854 let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in

855 let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in

855 logElab 5 ("Checking " ++ showTmImpls wval)

856 logElab 5 ("Checking " ++ showTmImpls wval)

856 -- Elaborate wval in this context

857 -- Elaborate wval in this context

857 ((wval', defer, is, ctxt', newDecls, highlights, newGName), _) <-

858 ((wval', defer, is, ctxt', newDecls, highlights, newGName), _) <-

858− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS")

859+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS")

859 (bindTyArgs PVTy bargs infP) initEState

860 (bindTyArgs PVTy bargs infP) initEState

860 (do pbinds i lhs_tm

861 (do pbinds i lhs_tm

861 -- proof search can use explicitly written names

862 -- proof search can use explicitly written names

@@ -872,14 +873,14 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

872 sendHighlighting highlights

873 sendHighlighting highlights

873 updateIState $ \i -> i { idris_name = newGName }

874 updateIState $ \i -> i { idris_name = newGName }

874

875

875− def' <- checkDef fc iderr True defer

876+ def' <- checkDef info fc iderr True defer

876 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

877 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

877 addDeferred def''

878 addDeferred def''

878 mapM_ (elabCaseBlock info opts) is

879 mapM_ (elabCaseBlock info opts) is

879 logElab 5 ("Checked wval " ++ show wval')

880 logElab 5 ("Checked wval " ++ show wval')

880

881

881 ctxt <- getContext

882 ctxt <- getContext

882− (cwval, cwvalty) <- recheckC fc id [] (getInferTerm wval')

883+ (cwval, cwvalty) <- recheckC (constraintNS info) fc id [] (getInferTerm wval')

883 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)

884 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)

884 let cwvalN = explicitNames (normalise ctxt [] cwval)

885 let cwvalN = explicitNames (normalise ctxt [] cwval)

885 logElab 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

886 logElab 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

@@ -914,7 +915,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

914 let wargname = sMN windex "warg"

915 let wargname = sMN windex "warg"

915

916

916 logElab 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)

917 logElab 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)

917− let wtype = bindTyArgs (flip (Pi Nothing) (TType (UVar 0))) (bargs_pre ++

918+ let wtype = bindTyArgs (flip (Pi Nothing) (TType (UVar [] 0))) (bargs_pre ++

918 (wargname, wargtype) :

919 (wargname, wargtype) :

919 map (abstract wargname wargval wargtype) bargs_post ++

920 map (abstract wargname wargval wargtype) bargs_post ++

920 case mpn of

921 case mpn of

@@ -937,7 +938,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

937 addIBC (IBCImp wname)

938 addIBC (IBCImp wname)

938 addIBC (IBCStatic wname)

939 addIBC (IBCStatic wname)

939

940

940− def' <- checkDef fc iderr True [(wname, (-1, Nothing, wtype, []))]

941+ def' <- checkDef info fc iderr True [(wname, (-1, Nothing, wtype, []))]

941 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

942 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

942 addDeferred def''

943 addDeferred def''

943

944

@@ -970,7 +971,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

970 ctxt <- getContext -- New context with block added

971 ctxt <- getContext -- New context with block added

971 i <- getIState

972 i <- getIState

972 ((rhs', defer, is, ctxt', newDecls, highlights, newGName), _) <-

973 ((rhs', defer, is, ctxt', newDecls, highlights, newGName), _) <-

973− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState

974+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState

974 (do pbinds i lhs_tm

975 (do pbinds i lhs_tm

975 setNextName

976 setNextName

976 (ElabResult _ d is ctxt' newDecls highlights newGName) <-

977 (ElabResult _ d is ctxt' newDecls highlights newGName) <-

@@ -983,12 +984,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

983 sendHighlighting highlights

984 sendHighlighting highlights

984 updateIState $ \i -> i { idris_name = newGName }

985 updateIState $ \i -> i { idris_name = newGName }

985

986

986− def' <- checkDef fc iderr True defer

987+ def' <- checkDef info fc iderr True defer

987 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

988 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

988 addDeferred def''

989 addDeferred def''

989 mapM_ (elabCaseBlock info opts) is

990 mapM_ (elabCaseBlock info opts) is

990 logElab 5 ("Checked RHS " ++ show rhs')

991 logElab 5 ("Checked RHS " ++ show rhs')

991− (crhs, crhsty) <- recheckC fc id [] rhs'

992+ (crhs, crhsty) <- recheckC (constraintNS info) fc id [] rhs'

992 return $ (Right (clhs, crhs), lhs)

993 return $ (Right (clhs, crhs), lhs)

993 where

994 where

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

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

src/Idris/Elab/Data.hs+7−6

@@ -287,6 +287,7 @@ addParamConstraints fc ps cty cons

287 then ULE avar cvar

288 else ULT avar cvar

289 addConstraints fc (tv, [con])

290+ addIBC (IBCConstraint fc con)

290 _ -> return ()

291 _ -> return ()

291 constraintTy t = return ()

292 constraintTy t = return ()

292

293

@@ -318,30 +319,30 @@ elabCaseFun ind paramPos n ty cons info = do

318 let motiveConstr = [(motiveName, expl, motive)]

319 let motiveConstr = [(motiveName, expl, motive)]

319 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

320 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

320 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC [] n) scrutineeIdxs) (PRef elimFC [] scrutineeName))

321 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC [] n) scrutineeIdxs) (PRef elimFC [] scrutineeName))

321− let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName NoFC eliminatorTy

322+ let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName elimFC eliminatorTy

322 let clauseConsElimArgs = map getPiName consTerms

323 let clauseConsElimArgs = map getPiName consTerms

323 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

324 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

324 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC [] arg)) clauseGeneralArgs'

325 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC [] arg)) clauseGeneralArgs'

325 let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy

326 let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy

326 elimLog elimSig

327 elimLog elimSig

327 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

328 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

328− let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

329+ let eliminatorDef = PClauses elimFC [TotalFn] elimDeclName eliminatorClauses

329 elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

330 elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

330 State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)

331 State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)

331 (ierror . Elaborating "type declaration of " elimDeclName Nothing)

332 (ierror . Elaborating "type declaration of " elimDeclName Nothing)

332 -- Do not elaborate clauses if there aren't any

333 -- Do not elaborate clauses if there aren't any

333 case eliminatorClauses of

334 case eliminatorClauses of

334− [] -> State.lift $ solveDeferred emptyFC elimDeclName -- Remove meta-variable for type

335+ [] -> State.lift $ solveDeferred elimFC elimDeclName -- Remove meta-variable for type

335 _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)

336 _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)

336 (ierror . Elaborating "clauses of " elimDeclName Nothing)

337 (ierror . Elaborating "clauses of " elimDeclName Nothing)

337 where elimLog :: String -> EliminatorState ()

338 where elimLog :: String -> EliminatorState ()

338 elimLog s = State.lift (logElab 2 s)

339 elimLog s = State.lift (logElab 2 s)

339

340

340 elimFC :: FC

341 elimFC :: FC

341− elimFC = fileFC "(casefun)"

342+ elimFC = fileFC $ "(casefun " ++ show n ++ ")"

342

343

343 elimDeclName :: Name

344 elimDeclName :: Name

344− elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' emptyFC) $ n

345+ elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ n

345

346

346 applyNS :: Name -> [String] -> Name

347 applyNS :: Name -> [String] -> Name

347 applyNS n [] = n

348 applyNS n [] = n

@@ -415,7 +416,7 @@ elabCaseFun ind paramPos n ty cons info = do

415

416

416 piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm

417 piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm

417 piConstr [] ty = ty

418 piConstr [] ty = ty

418− piConstr ((n, pl, tyb):tyr) ty = PPi pl n NoFC tyb (piConstr tyr ty)

419+ piConstr ((n, pl, tyb):tyr) ty = PPi pl n elimFC tyb (piConstr tyr ty)

419

420

420 interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]

421 interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]

421 interlievePos idxs [] l2 i = l2

422 interlievePos idxs [] l2 i = l2

src/Idris/Elab/Instance.hs+4−4

@@ -217,8 +217,8 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

217 mkiname n' ns ps' expn' =

218 case expn' of

219 Nothing -> case ns of

220− Nothing -> SN (sInstanceN n' (map show ps'))

220+ [] -> SN (sInstanceN n' (map show ps'))

221− Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

221+ m -> sNS (SN (sInstanceN n' (map show ps'))) m

222 Just nm -> nm

223

224 substInstance ips pnames (PInstance doc argDocs syn _ cs parents acc opts n nfc ps pextra t expn ds)

@@ -245,7 +245,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

245 let ty = addImpl [] i ty'

246 ctxt <- getContext

247 (ElabResult tyT _ _ ctxt' newDecls highlights newGName, _) <-

248− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) iname (TType (UVal 0)) initEState

248+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) iname (TType (UVal 0)) initEState

249 (errAt "type of " iname Nothing (erun fc (build i info ERHS [] iname ty)))

250 setContext ctxt'

251 processTacticDecls info newDecls

@@ -253,7 +253,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

253 updateIState $ \i -> i { idris_name = newGName }

254

255 ctxt <- getContext

256− (cty, _) <- recheckC fc id [] tyT

256+ (cty, _) <- recheckC (constraintNS info) fc id [] tyT

257 let nty = normalise ctxt [] cty

258 return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (map fst $ class_instances ci)

259

src/Idris/Elab/RunElab.hs+2−2

@@ -40,9 +40,9 @@ elabRunElab info fc script' ns =

40 ist <- getIState

41 ctxt <- getContext

42 (ElabResult tyT' defer is ctxt' newDecls highlights newGName, log) <-

43− tclift $ elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "toplLevelElab") elabScriptTy initEState

43+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "toplLevelElab") elabScriptTy initEState

44 (transformErr RunningElabScript

45− (erun fc (do tm <- runElabAction ist fc [] script ns

45+ (erun fc (do tm <- runElabAction info ist fc [] script ns

46 EState is _ impls highlights _ _ <- getAux

47 ctxt <- get_context

48 let ds = [] -- todo

src/Idris/Elab/Term.hs+21−21

@@ -815,8 +815,8 @@ elab ist info emode opts fn tm

815 mkN n@(NS _ _) = n

816 mkN n@(SN _) = n

817 mkN n = case namespace info of

818− Just xs@(_:_) -> sNS n xs

818+ xs@(_:_) -> sNS n xs

819− _ -> n

819+ _ -> n

820

821 elab' ina _ (PMatchApp fc fn)

822 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

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

1089-- mkCaseName (MN i x) = MN i (x ++ "_case")

1090 mkN n@(NS _ _) = n

1091 mkN n = case namespace info of

1092− Just xs@(_:_) -> sNS n xs

1092+ xs@(_:_) -> sNS n xs

1093 _ -> n

1094

1095 getScrType [] = Nothing

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

1157 g_nextname <- get_global_nextname

1158 saveState

1159 updatePS (const .

1160− newProof (sMN 0 "q") ctxt datatypes g_nextname $

1160+ newProof (sMN 0 "q") (constraintNS info) ctxt datatypes g_nextname $

1161 P Ref (reflm "TT") Erased)

1162

1163 -- Re-add the unquotes, letting Idris infer the (fictional)

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

1208 _ -> False

1209 case quoted of

1210 Just q -> do ctxt <- get_context

1211− (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1211+ (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1212 if pattern

1213 then if isRaw

1214 then reflectRawQuotePattern unquoteNames (forget q')

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

1279 fullyElaborated script

1280 solve -- eliminate the hole. Becuase there are no references, the script is only in the binding

1281 env <- get_env

1282− runElabAction ist (maybe fc' id fc) env script ns

1282+ runElabAction info ist (maybe fc' id fc) env script ns

1283 solve

1284 elab' ina fc (PConstSugar constFC tm) =

1285 -- Here we elaborate the contained term, then calculate

@@ -1862,14 +1862,14 @@ case_ ind autoSolve ist fn tm = do

1862 when autoSolve solveAll

1863

1864-- | Compute the appropriate name for a top-level metavariable

1865−metavarName :: Maybe [String] -> Name -> Name

1865+metavarName :: [String] -> Name -> Name

1866−metavarName _ n@(NS _ _) = n

1866+metavarName _ n@(NS _ _) = n

1867−metavarName (Just (ns@(_:_))) n = sNS n ns

1867+metavarName (ns@(_:_)) n = sNS n ns

1868−metavarName _ n = n

1868+metavarName _ n = n

1869

1870−runElabAction :: IState -> FC -> Env -> Term -> [String] -> ElabD Term

1870+runElabAction :: ElabInfo -> IState -> FC -> Env -> Term -> [String] -> ElabD Term

1871−runElabAction ist fc env tm ns = do tm' <- eval tm

1871+runElabAction info ist fc env tm ns = do tm' <- eval tm

1872− runTacTm tm'

1872+ runTacTm tm'

1873

1874 where

1875 eval tm = do ctxt <- get_context

@@ -1899,7 +1899,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1899 _ -> P Ref n Erased

1900 fakeTT (RBind n b body) = Bind n (fmap fakeTT b) (fakeTT body)

1901 fakeTT (RApp f a) = App Complete (fakeTT f) (fakeTT a)

1902− fakeTT RType = TType (UVar (-1))

1902+ fakeTT RType = TType (UVar [] (-1))

1903 fakeTT (RUType u) = UType u

1904 fakeTT (RConstant c) = Constant c

1905

@@ -2308,10 +2308,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2308 (ctxt', ES (p, aux') _ _) <-

2309 do (ES (current_p, _) _ _) <- get

2310 lift $ runElab aux

2311− (do runElabAction ist fc [] script ns

2311+ (do runElabAction info ist fc [] script ns

2312 ctxt' <- get_context

2313 return ctxt')

2314− ((newProof recH ctxt datatypes g_next goalTT)

2314+ ((newProof recH (constraintNS info) ctxt datatypes g_next goalTT)

2315 { nextname = nextname current_p })

2316 set_context ctxt'

2317

@@ -2322,7 +2322,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2322 }

2323 put (ES (p', aux') s e)

2324 env' <- get_env

2325− (tm, ty, _) <- lift $ recheck ctxt' env (forget tm_out) tm_out

2325+ (tm, ty, _) <- lift $ recheck (constraintNS info) ctxt' env (forget tm_out) tm_out

2326 let (tm', ty') = (reflect tm, reflect ty)

2327 fmap fst . checkClosed $

2328 rawPair (Var $ reflm "TT", Var $ reflm "TT")

@@ -2333,7 +2333,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2333 ptm <- get_term

2334 -- See documentation above in the elab case for PMetavar

2335 let unique_used = getUniqueUsed ctxt ptm

2336− let mvn = metavarName (Just ns) n'

2336+ let mvn = metavarName ns n'

2337 attack

2338 defer unique_used mvn

2339 solve

@@ -2699,7 +2699,7 @@ processTacticDecls info steps =

2699 updateIState $ \i -> i { idris_implicits =

2700 addDef n impls (idris_implicits i) }

2701 addIBC (IBCImp n)

2702− ds <- checkDef fc (\_ e -> e) True [(n, (-1, Nothing, ty, []))]

2702+ ds <- checkDef info fc (\_ e -> e) True [(n, (-1, Nothing, ty, []))]

2703 addIBC (IBCDef n)

2704 ctxt <- getContext

2705 case lookupDef n ctxt of

@@ -2817,7 +2817,7 @@ processTacticDecls info steps =

2817 let lhs = addImplPat ist lhs_in

2818 let fc = fileFC "elab_reflected_totality"

2819 let tcgen = False -- TODO: later we may support dictionary generation

2820− case elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState

2820+ case elaborate (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState

2821 (erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in)

2822 (infTerm lhs))) of

2823 OK (ElabResult lhs' _ _ _ _ _ name', _) ->

@@ -2825,7 +2825,7 @@ processTacticDecls info steps =

2825 -- want to run infinitely many times

2826 let lhs_tm = orderPats (getInferTerm lhs')

2827 updateIState $ \i -> i { idris_name = name' }

2828− case recheck ctxt [] (forget lhs_tm) lhs_tm of

2828+ case recheck (constraintNS info) ctxt [] (forget lhs_tm) lhs_tm of

2829 OK _ -> return True

2830 err -> return False

2831 -- if it's a recoverable error, the case may become possible

src/Idris/Elab/Transform.hs+4−4

@@ -62,7 +62,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

62 let lhs = addImplPat i lhs_in

63 logElab 5 ("Transform LHS input: " ++ showTmImpls lhs)

64 (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-

65− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transLHS") infP initEState

65+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transLHS") infP initEState

66 (erun fc (buildTC i info ETransLHS [] (sUN "transform")

67 (allNamesIn lhs_in) (infTerm lhs)))

68 setContext ctxt'

@@ -73,7 +73,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

73 let lhs_ty = getInferType lhs'

74 let newargs = pvars i lhs_tm

75

76− (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] fc id [] lhs_tm

76+ (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] (constraintNS info) fc id [] lhs_tm

77 let clhs_tm = renamepats pnames clhs_tm_in

78 logElab 3 ("Transform LHS " ++ show clhs_tm)

79 logElab 3 ("Transform type " ++ show clhs_ty)

@@ -82,7 +82,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

82 logElab 5 ("Transform RHS input: " ++ showTmImpls rhs)

83

84 ((rhs', defer, ctxt', newDecls, newGName), _) <-

85− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transRHS") clhs_ty initEState

85+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transRHS") clhs_ty initEState

86 (do pbinds i lhs_tm

87 setNextName

88 (ElabResult _ _ _ ctxt' newDecls highlights newGName) <- erun fc (build i info ERHS [] (sUN "transform") rhs)

@@ -97,7 +97,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

97 sendHighlighting highlights

98 updateIState $ \i -> i { idris_name = newGName }

99

100− (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] fc id [] rhs'

100+ (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] (constraintNS info) fc id [] rhs'

101 let crhs_tm = renamepats pnames crhs_tm_in

102 logElab 3 ("Transform RHS " ++ show crhs_tm)

103

src/Idris/Elab/Type.hs+5−5

@@ -82,7 +82,7 @@ buildType info syn fc opts n ty' = do

82 logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

83

84 ((ElabResult tyT' defer is ctxt' newDecls highlights newGName, est), log) <-

85− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState

85+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState

86 (errAt "type of " n Nothing

87 (erunAux fc (build i info ETyDecl [] n ty)))

88

@@ -96,7 +96,7 @@ buildType info syn fc opts n ty' = do

96

97 logElab 3 $ show ty ++ "\nElaborated: " ++ show tyT'

98

99− ds <- checkAddDef True False fc iderr True defer

99+ ds <- checkAddDef True False info fc iderr True defer

100 -- if the type is not complete, note that we'll need to infer

101 -- things later (for solving metavariables)

102 when (length ds > length is) -- more deferred than case blocks

@@ -107,7 +107,7 @@ buildType info syn fc opts n ty' = do

107 logElab 5 $ "Rechecking"

108 logElab 6 $ show tyT

109 logElab 10 $ "Elaborated to " ++ showEnvDbg [] tyT

110− (cty, ckind) <- recheckC fc id [] tyT

110+ (cty, ckind) <- recheckC (constraintNS info) fc id [] tyT

111

112 -- record the implicit and inaccessible arguments

113 i <- getIState

@@ -140,7 +140,7 @@ buildType info syn fc opts n ty' = do

140

141 return (cty, ckind, ty, inacc)

142 where

143− patToImp (Bind n (PVar t) sc) = Bind n (Pi Nothing t (TType (UVar 0))) (patToImp sc)

143+ patToImp (Bind n (PVar t) sc) = Bind n (Pi Nothing t (TType (UVar [] 0))) (patToImp sc)

144 patToImp (Bind n b sc) = Bind n b (patToImp sc)

145 patToImp t = t

146

@@ -203,7 +203,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

203 -- Productivity checking now via checking for guarded 'Delay'

204 let opts' = opts -- if corec then (Coinductive : opts) else opts

205 let usety = if norm then nty' else nty

206− ds <- checkDef fc iderr True [(n, (-1, Nothing, usety, []))]

206+ ds <- checkDef info fc iderr True [(n, (-1, Nothing, usety, []))]

207 addIBC (IBCDef n)

208 addDefinedName n

209 let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True, True))) ds

src/Idris/Elab/Utils.hs+13−11

@@ -35,17 +35,19 @@ import qualified Data.Map as Map

35

36recheckC = recheckC_borrowing False True []

37

38−recheckC_borrowing uniq_check addConstrs bs fc mkerr env t

38+recheckC_borrowing uniq_check addConstrs bs tcns fc mkerr env t

39 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

40+

40 ctxt <- getContext

41 ctxt <- getContext

41 t' <- case safeForget t of

42 t' <- case safeForget t of

42 Just ft -> return ft

43 Just ft -> return ft

43 Nothing -> tclift $ tfail $ mkerr (At fc (IncompleteTerm t))

44 Nothing -> tclift $ tfail $ mkerr (At fc (IncompleteTerm t))

44− (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of

45+ (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs tcns ctxt env t' t of

45 Error e -> tfail (At fc (mkerr e))

46 Error e -> tfail (At fc (mkerr e))

46 OK x -> return x

47 OK x -> return x

47 logElab 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

48 logElab 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

48− when addConstrs $ addConstraints fc cs

49+ when addConstrs $ do addConstraints fc cs

50+ mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)

49 mapM_ (checkDeprecated fc) (allTTNames tm)

51 mapM_ (checkDeprecated fc) (allTTNames tm)

50 mapM_ (checkDeprecated fc) (allTTNames ty)

52 mapM_ (checkDeprecated fc) (allTTNames ty)

51 mapM_ (checkFragile fc) (allTTNames tm)

53 mapM_ (checkFragile fc) (allTTNames tm)

@@ -80,23 +82,23 @@ checkFragile fc n = do

80iderr :: Name -> Err -> Err

82iderr :: Name -> Err -> Err

81iderr _ e = e

83iderr _ e = e

82

84

83−checkDef :: FC -> (Name -> Err -> Err) -> Bool ->

85+checkDef :: ElabInfo -> FC -> (Name -> Err -> Err) -> Bool ->

84 [(Name, (Int, Maybe Name, Type, [Name]))] ->

86 [(Name, (Int, Maybe Name, Type, [Name]))] ->

85 Idris [(Name, (Int, Maybe Name, Type, [Name]))]

87 Idris [(Name, (Int, Maybe Name, Type, [Name]))]

86−checkDef fc mkerr definable ns

88+checkDef info fc mkerr definable ns

87− = checkAddDef False True fc mkerr definable ns

89+ = checkAddDef False True info fc mkerr definable ns

88

90

89−checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err) -> Bool

91+checkAddDef :: Bool -> Bool -> ElabInfo -> FC -> (Name -> Err -> Err) -> Bool

90 -> [(Name, (Int, Maybe Name, Type, [Name]))]

92 -> [(Name, (Int, Maybe Name, Type, [Name]))]

91 -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

93 -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

92−checkAddDef add toplvl fc mkerr def [] = return []

94+checkAddDef add toplvl info fc mkerr def [] = return []

93−checkAddDef add toplvl fc mkerr definable ((n, (i, top, t, psns)) : ns)

95+checkAddDef add toplvl info fc mkerr definable ((n, (i, top, t, psns)) : ns)

94 = do ctxt <- getContext

96 = do ctxt <- getContext

95 logElab 5 $ "Rechecking deferred name " ++ show (n, t, definable)

97 logElab 5 $ "Rechecking deferred name " ++ show (n, t, definable)

96− (t', _) <- recheckC fc (mkerr n) [] t

98+ (t', _) <- recheckC (constraintNS info) fc (mkerr n) [] t

97 when add $ do addDeferred [(n, (i, top, t, psns, toplvl, definable))]

99 when add $ do addDeferred [(n, (i, top, t, psns, toplvl, definable))]

98 addIBC (IBCDef n)

100 addIBC (IBCDef n)

99− ns' <- checkAddDef add toplvl fc mkerr definable ns

101+ ns' <- checkAddDef add toplvl info fc mkerr definable ns

100 return ((n, (i, top, t', psns)) : ns')

102 return ((n, (i, top, t', psns)) : ns')

101

103

102-- | Get the list of (index, name) of inaccessible arguments from an elaborated

104-- | Get the list of (index, name) of inaccessible arguments from an elaborated

src/Idris/Elab/Value.hs+3−3

@@ -74,7 +74,7 @@ elabValBind info aspat norm tm_in

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

75

76 (ElabResult tm' defer is ctxt' newDecls highlights newGName, _) <-

77− tclift (elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "val") infP initEState

77+ tclift (elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "val") infP initEState

78 (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

79

80 -- Extend the context with new definitions created

@@ -85,13 +85,13 @@ elabValBind info aspat norm tm_in

85

86 let vtm = orderPats (getInferTerm tm')

87

88− def' <- checkDef (fileFC "(input)") iderr True defer

88+ def' <- checkDef info (fileFC "(input)") iderr True defer

89 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) def'

90 addDeferred def''

91 mapM_ (elabCaseBlock info []) is

92

93 logElab 3 ("Value: " ++ show vtm)

94− (vtm_in, vty) <- recheckC (fileFC "(input)") id [] vtm

94+ (vtm_in, vty) <- recheckC (constraintNS info) (fileFC "(input)") id [] vtm

95

96 let vtm = if norm then normalise (tt_ctxt i) [] vtm_in

97 else vtm_in

src/Idris/ElabDecls.hs+16−14

@@ -71,12 +71,12 @@ import Util.Pretty(pretty, text)

71

72

73-- | Top level elaborator info, supporting recursive elaboration

74−recinfo :: ElabInfo

74+recinfo :: FC -> ElabInfo

75−recinfo = EInfo [] emptyContext id Nothing Nothing 0 id elabDecl'

75+recinfo fc = EInfo [] emptyContext id [] (Just fc) (fc_fname fc) 0 id elabDecl'

76

77-- | Return the elaborated term which calls 'main'

78elabMain :: Idris Term

79−elabMain = do (m, _) <- elabVal recinfo ERHS

79+elabMain = do (m, _) <- elabVal (recinfo fc) ERHS

80 (PApp fc (PRef fc [] (sUN "run__IO"))

81 [pexp $ PRef fc [] (sNS (sUN "main") ["Main"])])

82 return m

@@ -89,12 +89,12 @@ elabPrims = do i <- getIState

89 let mkdec opt decl docs argdocs =

90 PData docs argdocs defaultSyntax (fileFC "builtin")

91 opt decl

92− elabDecl' EAll recinfo (mkdec inferOpts inferDecl emptyDocstring [])

92+ elabDecl' EAll (recinfo primfc) (mkdec inferOpts inferDecl emptyDocstring [])

93 -- We don't want the constraints generated by 'Infer' since

94 -- it's only scaffolding for the elaborator

95 i <- getIState

96 putIState $ i { idris_constraints = cs_in }

97− elabDecl' EAll recinfo (mkdec eqOpts eqDecl eqDoc eqParamDoc)

97+ elabDecl' EAll (recinfo primfc) (mkdec eqOpts eqDecl eqDoc eqParamDoc)

98

99 addNameHint eqTy (sUN "prf")

100 mapM_ elabPrim primitives

@@ -109,6 +109,8 @@ elabPrims = do i <- getIState

109 i <- getIState

110 putIState i { idris_scprims = (n, sc) : idris_scprims i }

111

112+ primfc = fileFC "primitive"

113+

112 valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value

114 valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value

113 valuePrim prim vals = fmap VConstant (mapM getConst vals >>= prim)

115 valuePrim prim vals = fmap VConstant (mapM getConst vals >>= prim)

114

116

@@ -118,9 +120,9 @@ elabPrims = do i <- getIState

118

120

119 p_believeMe [_,_,x] = Just x

121 p_believeMe [_,_,x] = Just x

120 p_believeMe _ = Nothing

122 p_believeMe _ = Nothing

121− believeTy = Bind (sUN "a") (Pi Nothing (TType (UVar (-2))) (TType (UVar (-1))))

123+ believeTy = Bind (sUN "a") (Pi Nothing (TType (UVar [] (-2))) (TType (UVar [] (-1))))

122− (Bind (sUN "b") (Pi Nothing (TType (UVar (-2))) (TType (UVar (-1))))

124+ (Bind (sUN "b") (Pi Nothing (TType (UVar [] (-2))) (TType (UVar [] (-1))))

123− (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar (-1)))) (V 1)))

125+ (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar [] (-1)))) (V 1)))

124 elabBelieveMe

126 elabBelieveMe

125 = do let prim__believe_me = sUN "prim__believe_me"

127 = do let prim__believe_me = sUN "prim__believe_me"

126 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

128 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

@@ -143,10 +145,10 @@ elabPrims = do i <- getIState

143 vnNothing = VP (DCon 0 1 False) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased

145 vnNothing = VP (DCon 0 1 False) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased

144 vnRefl = VP (DCon 0 2 False) eqCon VErased

146 vnRefl = VP (DCon 0 2 False) eqCon VErased

145

147

146− synEqTy = Bind (sUN "a") (Pi Nothing (TType (UVar (-3))) (TType (UVar (-2))))

148+ synEqTy = Bind (sUN "a") (Pi Nothing (TType (UVar [] (-3))) (TType (UVar [] (-2))))

147− (Bind (sUN "b") (Pi Nothing (TType (UVar (-3))) (TType (UVar (-2))))

149+ (Bind (sUN "b") (Pi Nothing (TType (UVar [] (-3))) (TType (UVar [] (-2))))

148− (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar (-2))))

150+ (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar [] (-2))))

149− (Bind (sUN "y") (Pi Nothing (V 1) (TType (UVar (-2))))

151+ (Bind (sUN "y") (Pi Nothing (V 1) (TType (UVar [] (-2))))

150 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)

152 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)

151 [V 3, V 2, V 1, V 0]]))))

153 [V 3, V 2, V 1, V 0]]))))

152 elabSynEq

154 elabSynEq

@@ -262,8 +264,8 @@ elabDecl' what info (PNamespace n nfc ps) =

262 let ns = reverse (map T.pack newNS)

264 let ns = reverse (map T.pack newNS)

263 sendHighlighting [(nfc, AnnNamespace ns Nothing)]

265 sendHighlighting [(nfc, AnnNamespace ns Nothing)]

264 where

266 where

265− newNS = maybe [n] (n:) (namespace info)

267+ newNS = n : namespace info

266− ninfo = info { namespace = Just newNS }

268+ ninfo = info { namespace = newNS }

267

269

268elabDecl' what info (PClass doc s f cs n nfc ps pdocs fds ds cn cd)

270elabDecl' what info (PClass doc s f cs n nfc ps pdocs fds ds cn cd)

269 | what /= EDefns

271 | what /= EDefns

src/Idris/Error.hs+2−1

@@ -28,6 +28,7 @@ import System.IO.Error(isUserError, ioeGetErrorString)

28import Data.Char

29import Data.List (intercalate, isPrefixOf)

30import qualified Data.Text as T

31+import qualified Data.Set as S

31import Data.Typeable

32import Data.Typeable

32import qualified Data.Traversable as Traversable

33import qualified Data.Traversable as Traversable

33import qualified Data.Foldable as Foldable

34import qualified Data.Foldable as Foldable

@@ -36,7 +37,7 @@ iucheck :: Idris ()

36iucheck = do tit <- typeInType

37iucheck = do tit <- typeInType

37 ist <- getIState

38 ist <- getIState

38 let cs = idris_constraints ist

39 let cs = idris_constraints ist

39− logLvl 7 $ "ALL CONSTRAINTS: " ++ show cs

40+ logLvl 7 $ "ALL CONSTRAINTS: " ++ show (length (S.toList cs))

40 when (not tit) $

41 when (not tit) $

41 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`

42 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`

42 (\e -> do let fc = getErrSpan e

43 (\e -> do let fc = getErrSpan e

src/Idris/IBC.hs+14−2

@@ -46,8 +46,10 @@ import System.FilePath

46import System.Directory

47import Codec.Archive.Zip

48

49+import Debug.Trace

50+

49ibcVersion :: Word16

51ibcVersion :: Word16

50−ibcVersion = 143

52+ibcVersion = 144

51

53

52-- | When IBC is being loaded - we'll load different things (and omit

54-- | When IBC is being loaded - we'll load different things (and omit

53-- different structures/definitions) depending on which phase we're in.

55-- different structures/definitions) depending on which phase we're in.

@@ -105,6 +107,7 @@ data IBCFile = IBCFile {

105 , ibc_injective :: ![(Name, Injectivity)]

107 , ibc_injective :: ![(Name, Injectivity)]

106 , ibc_access :: ![(Name, Accessibility)]

108 , ibc_access :: ![(Name, Accessibility)]

107 , ibc_fragile :: ![(Name, String)]

109 , ibc_fragile :: ![(Name, String)]

110+ , ibc_constraints :: ![(FC, UConstraint)]

108 }

111 }

109 deriving Show

112 deriving Show

110{-!

113{-!

@@ -112,7 +115,7 @@ deriving instance Binary IBCFile

112!-}

115!-}

113

116

114initIBC :: IBCFile

117initIBC :: IBCFile

115−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] []

118+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

116

119

117hasValidIBCVersion :: FilePath -> Idris Bool

120hasValidIBCVersion :: FilePath -> Idris Bool

118hasValidIBCVersion fp = do

121hasValidIBCVersion fp = do

@@ -208,6 +211,8 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

208 makeEntry "ibc_injective" (ibc_injective i),

211 makeEntry "ibc_injective" (ibc_injective i),

209 makeEntry "ibc_access" (ibc_access i),

212 makeEntry "ibc_access" (ibc_access i),

210 makeEntry "ibc_fragile" (ibc_fragile i)]

213 makeEntry "ibc_fragile" (ibc_fragile i)]

214+-- TODO: Put this back in shortly after minimising/pruning constraints

215+-- makeEntry "ibc_constraints" (ibc_constraints i)]

211

216

212writeArchive :: FilePath -> IBCFile -> Idris ()

217writeArchive :: FilePath -> IBCFile -> Idris ()

213writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArchive (entries i)

218writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArchive (entries i)

@@ -337,6 +342,7 @@ ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

337ibc i (IBCAutoHint n h) f = return f { ibc_autohints = (n, h) : ibc_autohints f }

342ibc i (IBCAutoHint n h) f = return f { ibc_autohints = (n, h) : ibc_autohints f }

338ibc i (IBCDeprecate n r) f = return f { ibc_deprecated = (n, r) : ibc_deprecated f }

343ibc i (IBCDeprecate n r) f = return f { ibc_deprecated = (n, r) : ibc_deprecated f }

339ibc i (IBCFragile n r) f = return f { ibc_fragile = (n,r) : ibc_fragile f }

344ibc i (IBCFragile n r) f = return f { ibc_fragile = (n,r) : ibc_fragile f }

345+ibc i (IBCConstraint fc u) f = return f { ibc_constraints = (fc, u) : ibc_constraints f }

340

346

341getEntry :: (Binary b, NFData b) => b -> FilePath -> Archive -> Idris b

347getEntry :: (Binary b, NFData b) => b -> FilePath -> Archive -> Idris b

342getEntry alt f a = case findEntryByPath f a of

348getEntry alt f a = case findEntryByPath f a of

@@ -408,6 +414,7 @@ process reexp phase archive fn = do

408 processInjective archive

414 processInjective archive

409 processAccess reexp phase archive

415 processAccess reexp phase archive

410 processFragile archive

416 processFragile archive

417+ processConstraints archive

411

418

412timestampOlder :: FilePath -> FilePath -> Idris ()

419timestampOlder :: FilePath -> FilePath -> Idris ()

413timestampOlder src ibc = do

420timestampOlder src ibc = do

@@ -462,6 +469,11 @@ processFragile ar = do

462 ns <- getEntry [] "ibc_fragile" ar

469 ns <- getEntry [] "ibc_fragile" ar

463 mapM_ (\(n,reason) -> addFragile n reason) ns

470 mapM_ (\(n,reason) -> addFragile n reason) ns

464

471

472+processConstraints :: Archive -> Idris ()

473+processConstraints ar = do

474+ cs <- getEntry [] "ibc_constraints" ar

475+ mapM_ (\ (fc, c) -> addConstraints fc (0, [c])) cs

476+

465processImportDirs :: Archive -> Idris ()

477processImportDirs :: Archive -> Idris ()

466processImportDirs ar = do

478processImportDirs ar = do

467 fs <- getEntry [] "ibc_importdirs" ar

479 fs <- getEntry [] "ibc_importdirs" ar

src/Idris/Interactive.hs+2−2

@@ -246,8 +246,8 @@ doProofSearch fn updatefile rec l n hints (Just depth)

246 (ProofSearch rec False depth t psnames hints)]

247 let def = PClause fc mn (PRef fc [] mn) [] (body top) []

248 newmv_pre <- idrisCatch

249− (do elabDecl' EAll recinfo (PClauses fc [] mn [def])

249+ (do elabDecl' EAll (recinfo (fileFC "proofsearch")) (PClauses fc [] mn [def])

250− (tm, ty) <- elabVal recinfo ERHS (PRef fc [] mn)

250+ (tm, ty) <- elabVal (recinfo (fileFC "proofsearch")) ERHS (PRef fc [] mn)

251 ctxt <- getContext

252 i <- getIState

253 return . flip displayS "" . renderPretty 1.0 80 $

src/Idris/Parser.hs+2−2

@@ -1804,7 +1804,7 @@ loadSource lidr f toline

1804 -- we totality check after every Mutual block, so if

1805 -- anything is a single definition, wrap it in a

1806 -- mutual block on its own

1807− elabDecls toplevel (map toMutual ds)

1807+ elabDecls (toplevelWith f) (map toMutual ds)

1808 i <- getIState

1809 -- simplify every definition do give the totality checker

1810 -- a better chance

@@ -1883,7 +1883,7 @@ loadSource lidr f toline

1883 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

1884 addModDoc syn mname docs =

1885 do ist <- getIState

1886− docs' <- elabDocTerms recinfo (parsedDocs ist)

1886+ docs' <- elabDocTerms (toplevelWith f) (parsedDocs ist)

1887 let modDocs' = addDef docName docs' (idris_moduledocs ist)

1888 putIState ist { idris_moduledocs = modDocs' }

1889 addIBC (IBCModDocs docName)

src/Idris/Primitives.hs+1−1

@@ -34,7 +34,7 @@ data Prim = Prim { p_name :: Name,

34

35ty :: [Const] -> Const -> Type

36ty [] x = Constant x

37−ty (t:ts) x = Bind (sMN 0 "T") (Pi Nothing (Constant t) (TType (UVar (-3)))) (ty ts x)

37+ty (t:ts) x = Bind (sMN 0 "T") (Pi Nothing (Constant t) (TType (UVar [] (-3)))) (ty ts x)

38

39total, partial, iopartial :: Totality

40total = Total []

src/Idris/Prover.hs+23−21

@@ -51,13 +51,13 @@ import Util.Pretty

51import Debug.Trace

52

53-- | Launch the proof shell

54−prover :: Bool -> Bool -> Name -> Idris ()

54+prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()

55−prover mode lit x =

55+prover info mode lit x =

56 do ctxt <- getContext

57 i <- getIState

58 case lookupTy x ctxt of

59 [t] -> if elem x (map fst (idris_metavars i))

60− then prove mode (idris_optimisation i) ctxt lit x t

60+ then prove mode info (idris_optimisation i) ctxt lit x t

61 else ifail $ show x ++ " is not a hole"

62 _ -> fail "No such hole"

63

@@ -89,13 +89,13 @@ assumptionNames e

89 names ((MN _ _, _) : bs) = names bs

90 names ((n, _) : bs) = show n : names bs

91

92−prove :: Bool -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()

92+prove :: Bool -> ElabInfo -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()

93−prove mode opt ctxt lit n ty

93+prove mode info opt ctxt lit n ty

94− = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) (idris_name ist) ty) getIState

94+ = do ps <- fmap (\ist -> initElaborator n (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) ty) getIState

95 idemodePutSExp "start-proof-mode" n

96 (tm, prf) <-

97 if mode

98− then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []

98+ then elabloop info n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []

99 else do iputStrLn $ "Warning: this interactive prover is deprecated and will be removed " ++

100 "in a future release. Please see :elab for a similar feature that "++

101 "will replace it."

@@ -112,7 +112,7 @@ prove mode opt ctxt lit n ty

112 putIState (i { proof_list = (n, (mode, prf)) : proofs })

113 let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

114 logLvl 3 (show tree)

115− (ptm, pty) <- recheckC (fileFC "proof") id [] tm

115+ (ptm, pty) <- recheckC (constraintNS info) (fileFC "proof") id [] tm

116 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

117 "Expected type:" ++ show ty)

118 case converts ctxt [] ty pty of

@@ -277,6 +277,8 @@ undoElab prf env st [] = ifail "Nothing to undo"

277undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h

278 return (prf', env', st', hs)

279

280+proverfc = fileFC "prover"

281+

280runWithInterrupt

282runWithInterrupt

281 :: ElabState EState

283 :: ElabState EState

282 -> Idris a -- ^ run with SIGINT handler

284 -> Idris a -- ^ run with SIGINT handler

@@ -293,8 +295,8 @@ runWithInterrupt elabState mTry mSuccess mFailure = do

293 if success then mSuccess else mFailure

295 if success then mSuccess else mFailure

294 IdeMode _ _ -> mTry >> mSuccess

296 IdeMode _ _ -> mTry >> mSuccess

295

297

296−elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])

298+elabloop :: ElabInfo -> Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])

297−elabloop fn d prompt prf e prev h env

299+elabloop info fn d prompt prf e prev h env

298 = do ist <- getIState

300 = do ist <- getIState

299 when d $ dumpState ist True env (proof e)

301 when d $ dumpState ist True env (proof e)

300 (x, h') <-

302 (x, h') <-

@@ -355,13 +357,13 @@ elabloop fn d prompt prf e prev h env

355 DoLetP {} -> ifail "Pattern-matching let not supported here"

357 DoLetP {} -> ifail "Pattern-matching let not supported here"

356 DoBindP {} -> ifail "Pattern-matching <- not supported here"

358 DoBindP {} -> ifail "Pattern-matching <- not supported here"

357 DoLet fc i ifc Placeholder expr ->

359 DoLet fc i ifc Placeholder expr ->

358− do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

360+ do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)

359 ctxt <- getContext

361 ctxt <- getContext

360 let tm' = normaliseAll ctxt [] tm

362 let tm' = normaliseAll ctxt [] tm

361 ty' = normaliseAll ctxt [] ty

363 ty' = normaliseAll ctxt [] ty

362 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))

364 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))

363 DoLet fc i ifc ty expr ->

365 DoLet fc i ifc ty expr ->

364− do (tm, ty) <- elabVal recinfo ERHS

366+ do (tm, ty) <- elabVal (recinfo proverfc) ERHS

365 (PApp NoFC (PRef NoFC [] (sUN "the"))

367 (PApp NoFC (PRef NoFC [] (sUN "the"))

366 [ pexp (inLets ist env ty)

368 [ pexp (inLets ist env ty)

367 , pexp (inLets ist env expr)

369 , pexp (inLets ist env expr)

@@ -371,34 +373,34 @@ elabloop fn d prompt prf e prev h env

371 ty' = normaliseAll ctxt [] ty

373 ty' = normaliseAll ctxt [] ty

372 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))

374 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))

373 DoBind fc i ifc expr ->

375 DoBind fc i ifc expr ->

374− do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

376+ do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)

375 (_, e') <- elabStep e saveState -- enable :undo

377 (_, e') <- elabStep e saveState -- enable :undo

376 (res, e'') <- elabStep e' $

378 (res, e'') <- elabStep e' $

377− runElabAction ist NoFC [] tm ["Shell"]

379+ runElabAction info ist NoFC [] tm ["Shell"]

378 ctxt <- getContext

380 ctxt <- getContext

379 (v, vty) <- tclift $ check ctxt [] (forget res)

381 (v, vty) <- tclift $ check ctxt [] (forget res)

380 let v' = normaliseAll ctxt [] v

382 let v' = normaliseAll ctxt [] v

381 vty' = normaliseAll ctxt [] vty

383 vty' = normaliseAll ctxt [] vty

382 return (True, BothStep:prev, e'', False, prf ++ [step], (i, vty', v') : env, Right (iPrintResult ""))

384 return (True, BothStep:prev, e'', False, prf ++ [step], (i, vty', v') : env, Right (iPrintResult ""))

383 DoExp fc expr ->

385 DoExp fc expr ->

384− do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

386+ do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)

385 -- TODO: call elaborator with Elab () as goal here

387 -- TODO: call elaborator with Elab () as goal here

386 (_, e') <- elabStep e saveState -- enable :undo

388 (_, e') <- elabStep e saveState -- enable :undo

387 (_, e'') <- elabStep e' $

389 (_, e'') <- elabStep e' $

388− runElabAction ist NoFC [] tm ["Shell"]

390+ runElabAction info ist NoFC [] tm ["Shell"]

389 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))

391 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))

390 (\err -> return (False, prev, e, False, prf, env, Left err))

392 (\err -> return (False, prev, e, False, prf, env, Left err))

391 idemodePutSExp "write-proof-state" (prf', length prf')

393 idemodePutSExp "write-proof-state" (prf', length prf')

392 case res of

394 case res of

393 Left err -> do ist <- getIState

395 Left err -> do ist <- getIState

394 iRenderError $ pprintErr ist err

396 iRenderError $ pprintErr ist err

395− elabloop fn d prompt prf' st prev' h' env'

397+ elabloop info fn d prompt prf' st prev' h' env'

396 Right ok ->

398 Right ok ->

397 if done then do (tm, _) <- elabStep st get_term

399 if done then do (tm, _) <- elabStep st get_term

398 return (tm, prf')

400 return (tm, prf')

399 else runWithInterrupt e ok

401 else runWithInterrupt e ok

400− (elabloop fn d prompt prf' st prev' h' env')

402+ (elabloop info fn d prompt prf' st prev' h' env')

401− (elabloop fn d prompt prf e prev h' env)

403+ (elabloop info fn d prompt prf e prev h' env)

402

404

403 where

405 where

404 -- A bit of a hack: wrap the value up in a let binding, which will

406 -- A bit of a hack: wrap the value up in a let binding, which will

@@ -502,7 +504,7 @@ checkType e prf t = do

502 let OK env = envAtFocus (proof e)

504 let OK env = envAtFocus (proof e)

503 ctxt' = envCtxt env ctxt

505 ctxt' = envCtxt env ctxt

504 putIState ist { tt_ctxt = ctxt' }

506 putIState ist { tt_ctxt = ctxt' }

505− (tm, ty) <- elabVal recinfo ERHS t

507+ (tm, ty) <- elabVal (recinfo proverfc) ERHS t

506 let ppo = ppOptionIst ist

508 let ppo = ppOptionIst ist

507 ty' = normaliseC ctxt [] ty

509 ty' = normaliseC ctxt [] ty

508 infixes = idris_infixes ist

510 infixes = idris_infixes ist

@@ -528,7 +530,7 @@ evalTerm e prf t = withErrorReflection $

528 ist' = ist { tt_ctxt = ctxt' }

530 ist' = ist { tt_ctxt = ctxt' }

529 bnd = map (\x -> (fst x, False)) env

531 bnd = map (\x -> (fst x, False)) env

530 putIState ist'

532 putIState ist'

531− (tm, ty) <- elabVal recinfo ERHS t

533+ (tm, ty) <- elabVal (recinfo proverfc) ERHS t

532 let tm' = force (normaliseAll ctxt' env tm)

534 let tm' = force (normaliseAll ctxt' env tm)

533 ty' = force (normaliseAll ctxt' env ty)

535 ty' = force (normaliseAll ctxt' env ty)

534 ppo = ppOption (idris_options ist')

536 ppo = ppOption (idris_options ist')

src/Idris/REPL.hs+21−20

@@ -836,7 +836,7 @@ process fn (Eval t)

836 = withErrorReflection $

837 do logParser 5 $ show t

838 getIState >>= flip warnDisamb t

839− (tm, ty) <- elabREPL recinfo ERHS t

839+ (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

840 ctxt <- getContext

841 let tm' = perhapsForce $ normaliseBlocking ctxt []

842 [sUN "foreign",

@@ -871,12 +871,12 @@ process fn (NewDefn decls) = do

871 getClauseName (PWith fc name whole with rhs pn whereBlock) = name

872 defineName :: [PDecl] -> Idris ()

873 defineName (tyDecl@(PTy docs argdocs syn fc opts name _ ty) : decls) = do

874− elabDecl EAll recinfo tyDecl

874+ elabDecl EAll info tyDecl

875− elabClauses recinfo fc opts name (concatMap getClauses decls)

875+ elabClauses info fc opts name (concatMap getClauses decls)

876 setReplDefined (Just name)

877 defineName [PClauses fc opts _ [clause]] = do

878 let pterm = getRHS clause

879− (tm,ty) <- elabVal recinfo ERHS pterm

879+ (tm,ty) <- elabVal info ERHS pterm

880 ctxt <- getContext

881 let tm' = force (normaliseAll ctxt [] tm)

882 let ty' = force (normaliseAll ctxt [] ty)

@@ -891,7 +891,7 @@ process fn (NewDefn decls) = do

891 i <- get

892 put (addReplSyntax i syntax)

893 defineName decls = do

894− elabDecls toplevel (map fixClauses decls)

894+ elabDecls (toplevelWith fn) (map fixClauses decls)

895 setReplDefined (getName (head decls))

896 getClauses (PClauses fc opts name clauses) = clauses

897 getClauses _ = []

@@ -915,6 +915,8 @@ process fn (NewDefn decls) = do

915 fixClauses (PInstance doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty instName decls) =

916 PInstance doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty instName (map fixClauses decls)

917 fixClauses decl = decl

918+

919+ info = recinfo (fileFC "toplevel")

918

920

919process fn (Undefine names) = undefine names

921process fn (Undefine names) = undefine names

920 where

922 where

@@ -954,7 +956,7 @@ process fn (Undefine names) = undefine names

954process fn (ExecVal t)

956process fn (ExecVal t)

955 = do ctxt <- getContext

957 = do ctxt <- getContext

956 ist <- getIState

958 ist <- getIState

957− (tm, ty) <- elabVal recinfo ERHS t

959+ (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

958-- let tm' = normaliseAll ctxt [] tm

960-- let tm' = normaliseAll ctxt [] tm

959 let ty' = normaliseAll ctxt [] ty

961 let ty' = normaliseAll ctxt [] ty

960 res <- execute tm

962 res <- execute tm

@@ -1001,7 +1003,7 @@ process fn (Check (PRef _ _ n))

1001

1003

1002

1004

1003process fn (Check t)

1005process fn (Check t)

1004− = do (tm, ty) <- elabREPL recinfo ERHS t

1006+ = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

1005 ctxt <- getContext

1007 ctxt <- getContext

1006 ist <- getIState

1008 ist <- getIState

1007 let ppo = ppOptionIst ist

1009 let ppo = ppOptionIst ist

@@ -1015,7 +1017,7 @@ process fn (Check t)

1015 (pprintDelab ist ty')

1017 (pprintDelab ist ty')

1016

1018

1017process fn (Core t)

1019process fn (Core t)

1018− = do (tm, ty) <- elabREPL recinfo ERHS t

1020+ = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

1019 iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)

1021 iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)

1020

1022

1021process fn (DocStr (Left n) w)

1023process fn (DocStr (Left n) w)

@@ -1083,8 +1085,8 @@ process fn (TotCheck n)

1083 ts

1085 ts

1084

1086

1085process fn (DebugUnify l r)

1087process fn (DebugUnify l r)

1086− = do (ltm, _) <- elabVal recinfo ERHS l

1088+ = do (ltm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS l

1087− (rtm, _) <- elabVal recinfo ERHS r

1089+ (rtm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS r

1088 ctxt <- getContext

1090 ctxt <- getContext

1089 case unify ctxt [] (ltm, Nothing) (rtm, Nothing) [] [] [] [] of

1091 case unify ctxt [] (ltm, Nothing) (rtm, Nothing) [] [] [] [] of

1090 OK ans -> iputStrLn (show ans)

1092 OK ans -> iputStrLn (show ans)

@@ -1129,7 +1131,7 @@ process fn (MakeLemma updatefile l n)

1129process fn (DoProofSearch updatefile rec l n hints)

1131process fn (DoProofSearch updatefile rec l n hints)

1130 = doProofSearch fn updatefile rec l n hints Nothing

1132 = doProofSearch fn updatefile rec l n hints Nothing

1131process fn (Spec t)

1133process fn (Spec t)

1132− = do (tm, ty) <- elabVal recinfo ERHS t

1134+ = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

1133 ctxt <- getContext

1135 ctxt <- getContext

1134 ist <- getIState

1136 ist <- getIState

1135 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

1137 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

@@ -1206,22 +1208,21 @@ process fn (Prove mode n')

1206 [(_, (_,_,_,_,False))] -> ierror (Msg $ "Can't prove this hole as it depends on other holes")

1208 [(_, (_,_,_,_,False))] -> ierror (Msg $ "Can't prove this hole as it depends on other holes")

1207 [(_, (_,_,_,True,_))] -> ierror (Msg $ "Declarations not solvable using prover")

1209 [(_, (_,_,_,True,_))] -> ierror (Msg $ "Declarations not solvable using prover")

1208 ns -> ierror (CantResolveAlts (map fst ns))

1210 ns -> ierror (CantResolveAlts (map fst ns))

1209− prover mode (lit fn) n

1211+ prover (toplevelWith fn) mode (lit fn) n

1210 -- recheck totality

1212 -- recheck totality

1211 i <- getIState

1213 i <- getIState

1212 totcheck (fileFC "(input)", n)

1214 totcheck (fileFC "(input)", n)

1213 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

1215 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

1214 mapM_ checkDeclTotality (idris_totcheck i)

1216 mapM_ checkDeclTotality (idris_totcheck i)

1215 warnTotality

1217 warnTotality

1216−

1217process fn (WHNF t)

1218process fn (WHNF t)

1218− = do (tm, ty) <- elabVal recinfo ERHS t

1219+ = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

1219 ctxt <- getContext

1220 ctxt <- getContext

1220 ist <- getIState

1221 ist <- getIState

1221 let tm' = whnf ctxt tm

1222 let tm' = whnf ctxt tm

1222 iPrintResult (show (delab ist tm'))

1223 iPrintResult (show (delab ist tm'))

1223process fn (TestInline t)

1224process fn (TestInline t)

1224− = do (tm, ty) <- elabVal recinfo ERHS t

1225+ = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

1225 ctxt <- getContext

1226 ctxt <- getContext

1226 ist <- getIState

1227 ist <- getIState

1227 let tm' = inlineTerm ist tm

1228 let tm' = inlineTerm ist tm

@@ -1230,7 +1231,7 @@ process fn (TestInline t)

1230process fn (Execute tm)

1231process fn (Execute tm)

1231 = idrisCatch

1232 = idrisCatch

1232 (do ist <- getIState

1233 (do ist <- getIState

1233− (m, _) <- elabVal recinfo ERHS (elabExec fc tm)

1234+ (m, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS (elabExec fc tm)

1234 (tmpn, tmph) <- runIO $ tempfile ""

1235 (tmpn, tmph) <- runIO $ tempfile ""

1235 runIO $ hClose tmph

1236 runIO $ hClose tmph

1236 t <- codegen

1237 t <- codegen

@@ -1253,7 +1254,7 @@ process fn (Compile codegen f)

1253 let mainname = sNS (sUN "main") ["Main"]

1254 let mainname = sNS (sUN "main") ["Main"]

1254

1255

1255 m <- if iface then return Nothing else

1256 m <- if iface then return Nothing else

1256− do (m', _) <- elabVal recinfo ERHS

1257+ do (m', _) <- elabVal (recinfo (fileFC "compiler")) ERHS

1257 (PApp fc (PRef fc [] (sUN "run__IO"))

1258 (PApp fc (PRef fc [] (sUN "run__IO"))

1258 [pexp $ PRef fc [] mainname])

1259 [pexp $ PRef fc [] mainname])

1259 return (Just m')

1260 return (Just m')

@@ -1265,7 +1266,7 @@ process fn (LogLvl i) = setLogLevel i

1265process fn (LogCategory cs) = setLogCats cs

1266process fn (LogCategory cs) = setLogCats cs

1266-- Elaborate as if LHS of a pattern (debug command)

1267-- Elaborate as if LHS of a pattern (debug command)

1267process fn (Pattelab t)

1268process fn (Pattelab t)

1268− = do (tm, ty) <- elabVal recinfo ELHS t

1269+ = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ELHS t

1269 iPrintResult $ show tm ++ "\n\n : " ++ show ty

1270 iPrintResult $ show tm ++ "\n\n : " ++ show ty

1270

1271

1271process fn (Missing n)

1272process fn (Missing n)

@@ -1442,7 +1443,7 @@ process fn (PPrint fmt width (PRef _ _ n))

1442

1443

1444

1444process fn (PPrint fmt width t)

1445process fn (PPrint fmt width t)

1445− = do (tm, ty) <- elabVal recinfo ERHS t

1446+ = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

1446 ctxt <- getContext

1447 ctxt <- getContext

1447 ist <- getIState

1448 ist <- getIState

1448 let ppo = ppOptionIst ist

1449 let ppo = ppOptionIst ist

@@ -1845,7 +1846,7 @@ execScript expr = do i <- getIState

1845 Failure err -> do iputStrLn $ show (fixColour c err)

1846 Failure err -> do iputStrLn $ show (fixColour c err)

1846 runIO $ exitWith (ExitFailure 1)

1847 runIO $ exitWith (ExitFailure 1)

1847 Success term -> do ctxt <- getContext

1848 Success term -> do ctxt <- getContext

1848− (tm, _) <- elabVal recinfo ERHS term

1849+ (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

1849 res <- execute tm

1850 res <- execute tm

1850 runIO $ exitWith ExitSuccess

1851 runIO $ exitWith ExitSuccess

1851

1852

src/Idris/Reflection.hs+8−6

@@ -389,8 +389,10 @@ reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"

389reifyTTUExp :: Term -> ElabD UExp

390reifyTTUExp t@(App _ _ _)

391 = case unApply t of

392+ (P _ f _, [Constant (Str str), Constant (I i)])

392− (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i

393+ | f == reflm "UVar" -> return $ UVar str i

394+ (P _ f _, [Constant (I i)])

393− (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i

395+ | f == reflm "UVal" -> return $ UVal i

394 _ -> fail ("Unknown reflection type universe expression: " ++ show t)

396 _ -> fail ("Unknown reflection type universe expression: " ++ show t)

395reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)

397reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)

396

398

@@ -792,7 +794,7 @@ reflectConstant WorldType = Var (reflm "WorldType")

792reflectConstant TheWorld = Var (reflm "TheWorld")

794reflectConstant TheWorld = Var (reflm "TheWorld")

793

795

794reflectUExp :: UExp -> Raw

796reflectUExp :: UExp -> Raw

795−reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]

797+reflectUExp (UVar ns i) = reflCall "UVar" [RConstant (Str ns), RConstant (I i)]

796reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]

798reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]

797

799

798-- | Reflect the environment of a proof into a List (TTName, Binder TT)

800-- | Reflect the environment of a proof into a List (TTName, Binder TT)

@@ -972,7 +974,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "

972 Right (TextPart msg)

974 Right (TextPart msg)

973reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

975reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

974 | n == reflm "NamePart" =

976 | n == reflm "NamePart" =

975− case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of

977+ case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") internalNS initContext emptyContext 0 Erased) of

976 Error e -> Left . InternalMsg $

978 Error e -> Left . InternalMsg $

977 "could not reify name term " ++

979 "could not reify name term " ++

978 show ttn ++

980 show ttn ++

@@ -980,7 +982,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

980 OK (n', _)-> Right $ NamePart n'

982 OK (n', _)-> Right $ NamePart n'

981reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

983reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

982 | n == reflm "TermPart" =

984 | n == reflm "TermPart" =

983− case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of

985+ case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") internalNS initContext emptyContext 0 Erased) of

984 Error e -> Left . InternalMsg $

986 Error e -> Left . InternalMsg $

985 "could not reify reflected term " ++

987 "could not reify reflected term " ++

986 show tm ++

988 show tm ++

@@ -988,7 +990,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

988 OK (tm', _) -> Right $ TermPart tm'

990 OK (tm', _) -> Right $ TermPart tm'

989reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

991reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

990 | n == reflm "RawPart" =

992 | n == reflm "RawPart" =

991− case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of

993+ case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") internalNS initContext emptyContext 0 Erased) of

992 Error e -> Left . InternalMsg $

994 Error e -> Left . InternalMsg $

993 "could not reify reflected raw term " ++

995 "could not reify reflected raw term " ++

994 show tm ++

996 show tm ++

src/Idris/TypeSearch.hs+1−1

@@ -436,7 +436,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

436 unifyQueue state [] = return state

437 unifyQueue state ((ty1, ty2) : queue) = do

438 --trace ("go: \n" ++ show state) True `seq` return ()

439− res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar 0))) | (n, ty) <- holes state]

439+ res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar [] 0))) | (n, ty) <- holes state]

440 (ty1, Nothing)

441 (ty2, Nothing) [] (map fst $ holes state) []

442 (state', queueAdditions) <- resolveUnis res state

test/error001/expected+4−4

@@ -1,8 +1,8 @@

1test002.idr:1:6:Universe inconsistency.

2− Working on: z

2+ Working on: ./test002.idr.z

3 Old domain: (6,6)

4 New domain: (6,5)

5 Involved constraints:

6− ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}

6+ ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}

7− ConstraintFC {uconstraint = y < z, ufc = test002.idr:1:6}

7+ ConstraintFC {uconstraint = ./test002.idr.y < ./test002.idr.z, ufc = test002.idr:1:6}

8− ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}

8+ ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}

test/interactive010/expected+2−2

@@ -4,9 +4,9 @@ a is not an implicit argument of Prelude.Interfaces./

4Usage is :doc <functionname>

5Usage is :wc <functionname>

6Usage is :printdef <functionname>

7−pat {ty504} : Type u. pat {__class505} : Prelude.Interfaces.Fractional {ty504}. Prelude.Interfaces./ {ty504} {__class505}

7+pat {ty504} : Type toplevel.u. pat {__class505} : Prelude.Interfaces.Fractional {ty504}. Prelude.Interfaces./ {ty504} {__class505}

8

9− : pty {ty504} : Type u. pty {__class505} : Prelude.Interfaces.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}

9+ : pty {ty504} : Type toplevel.u. pty {__class505} : Prelude.Interfaces.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}

10(input):1:1: error: expected: ":",

11 dependent type signature,

12 end of input

test/quasiquote001/expected+3−3

@@ -1,5 +1,5 @@

1−App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))))

1+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar "./Builtins.idr" 20)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar "./Builtins.idr" 20)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 25)) (TType (UVar "./Prelude/List.idr" 27))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar "./Builtins.idr" 20)))))

2--------------

3−App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 27))) (TType (UVar 28))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 29))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 23))) (TType (UVar 24))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1))))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1)))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 30))))

3+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar "./QuasiquoteBasics.idr" 27))) (TType (UVar "./QuasiquoteBasics.idr" 28))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar "./QuasiquoteBasics.idr" 29))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 74)) (TType (UVar "./Builtins.idr" 76))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 77)) (TType (UVar "./Builtins.idr" 79))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 80))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 81))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar "./Prelude/Nat.idr" 20)))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar "./Prelude/Nat.idr" 20))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 25)) (TType (UVar "./Prelude/List.idr" 27))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar "./QuasiquoteBasics.idr" 30))))

4--------------

5−App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 23))) (TType (UVar 24))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 28))) (TType (UVar 28)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 28))) (TType (UVar 28)))

5+App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 74)) (TType (UVar "./Builtins.idr" 76))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 77)) (TType (UVar "./Builtins.idr" 79))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 80))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 81))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 74)) (TType (UVar "./Builtins.idr" 76))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 77)) (TType (UVar "./Builtins.idr" 79))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 80))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 81))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (TType (UVar "./QuasiquoteBasics.idr" 28))) (TType (UVar "./QuasiquoteBasics.idr" 28)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 74)) (TType (UVar "./Builtins.idr" 76))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 77)) (TType (UVar "./Builtins.idr" 79))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 80))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 81))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (TType (UVar "./QuasiquoteBasics.idr" 28))) (TType (UVar "./QuasiquoteBasics.idr" 28)))

test/totality014/expected+5−5

@@ -1,9 +1,9 @@

1totality014.idr:6:9:Universe inconsistency.

2− Working on: u

2+ Working on: ./totality014.idr.u

3 Old domain: (5,5)

4 New domain: (5,4)

5 Involved constraints:

6− ConstraintFC {uconstraint = u <= w, ufc = totality014.idr:6:9}

6+ ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:9}

7− ConstraintFC {uconstraint = u < v, ufc = totality014.idr:1:6}

7+ ConstraintFC {uconstraint = ./totality014.idr.u < ./totality014.idr.v, ufc = totality014.idr:1:6}

8− ConstraintFC {uconstraint = w < u, ufc = totality014.idr:1:6}

8+ ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6}

9− ConstraintFC {uconstraint = u <= w, ufc = totality014.idr:6:9}

9+ ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:9}

test/universes001/expected+5−5

@@ -1,9 +1,9 @@

1universes001.idr:7:5:Universe inconsistency.

2− Working on: x

2+ Working on: ./universes001.idr.x

3 Old domain: (5,5)

4 New domain: (5,4)

5 Involved constraints:

6− ConstraintFC {uconstraint = x <= z, ufc = universes001.idr:7:5}

6+ ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5}

7− ConstraintFC {uconstraint = x < y, ufc = universes001.idr:1:6}

7+ ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6}

8− ConstraintFC {uconstraint = z < x, ufc = universes001.idr:1:6}

8+ ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6}

9− ConstraintFC {uconstraint = x <= z, ufc = universes001.idr:7:5}

9+ ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5}

test/universes002/expected+5−5

@@ -1,9 +1,9 @@

1universes002.idr:45:9:Universe inconsistency.

2− Working on: c7

2+ Working on: ./universes002.idr.c7

3 Old domain: (5,5)

4 New domain: (5,4)

5 Involved constraints:

6− ConstraintFC {uconstraint = c7 <= d1, ufc = universes002.idr:45:9}

6+ ConstraintFC {uconstraint = ./universes002.idr.c7 <= ./universes002.idr.d1, ufc = universes002.idr:45:9}

7− ConstraintFC {uconstraint = c7 < d7, ufc = universes002.idr:15:6}

7+ ConstraintFC {uconstraint = ./universes002.idr.c7 < ./universes002.idr.d7, ufc = universes002.idr:15:6}

8− ConstraintFC {uconstraint = e7 < c7, ufc = universes002.idr:15:6}

8+ ConstraintFC {uconstraint = ./universes002.idr.e7 < ./universes002.idr.c7, ufc = universes002.idr:15:6}

9− ConstraintFC {uconstraint = c7 <= d1, ufc = universes002.idr:45:9}

9+ ConstraintFC {uconstraint = ./universes002.idr.c7 <= ./universes002.idr.d1, ufc = universes002.idr:45:9}