fa5f1cd · Idris-dev · git.iko.soy

lib/builtins.idr+3−1

@@ -21,6 +21,8 @@ lazy x = x; -- compiled specially

2121

2222believe_me : a -> b; -- compiled specially as id, use with care!

2323

24+namespace builtins {

25+

2426id : a -> a;

2527id x = x;

2628

@@ -184,4 +186,4 @@ div = prim__divInt;

184186(++) : String -> String -> String;

185187(++) = prim__concat;

186188

187−

189+}

lib/list.idr+3

@@ -1,5 +1,7 @@

11import builtins;

22

3+namespace list {

4+

35data List a = Nil | Cons a (List a);

46

57rev : List a -> List a;

@@ -34,3 +36,4 @@ filter pred (Cons x xs) with (pred x, filter pred xs) {

3436 filter pred (Cons x xs) | (False, fxs) = fxs;

3537}

3638

39+}

lib/maybe.idr+3

@@ -1,4 +1,6 @@

11

2+namespace maybe {

3+

24data Maybe a = Nothing | Just a;

35

46maybe : b -> (a -> b) -> Maybe a -> b;

@@ -9,3 +11,4 @@ maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b;

911maybe_bind Nothing k = Nothing;

1012maybe_bind (Just x) k = k x;

1113

14+}

lib/nat.idr+3

@@ -1,5 +1,7 @@

11import builtins;

22

3+namespace nat {

4+

35data Nat = O | S Nat;

46

57plus : Nat -> Nat -> Nat;

@@ -64,3 +66,4 @@ plus_commutes_Sk = proof {

6466 refine plusn_Sm;

6567};

6668

69+}

lib/prelude.idr+3

@@ -8,6 +8,8 @@ import io;

88

99-- Show and instances

1010

11+namespace prelude {

12+

1113class Show a where {

1214 show : a -> String;

1315}

@@ -115,3 +117,4 @@ print = putStrLn . show;

115117readLine : IO String;

116118readLine = mkForeign (FFun "readStr" Nil FString);

117119

120+}

lib/vect.idr+6−3

@@ -1,5 +1,7 @@

11import nat;

22

3+namespace vect {

4+

35data Fin : Nat -> Set where

46 fO : Fin (S k)

57 | fS : Fin k -> Fin (S k);

@@ -15,7 +17,7 @@ instance Eq (Fin n) where {

1517infixr 7 :: ;

1618

1719data Vect : Set -> Nat -> Set where

18− VNil : Vect a O

20+ Nil : Vect a O

1921 | (::) : a -> Vect a k -> Vect a (S k);

2022

2123vlookup : Fin n -> Vect a n -> a;

@@ -23,13 +25,14 @@ vlookup fO (x :: xs) = x;

2325vlookup (fS k) (x :: xs) = vlookup k xs;

2426

2527vapp : Vect a n -> Vect a m -> Vect a (n + m);

26−vapp VNil ys = ys;

28+vapp Nil ys = ys;

2729vapp (x :: xs) ys = x :: vapp xs ys;

2830

2931vfilter : (a -> Bool) -> Vect a n -> (p ** Vect a p);

30−vfilter p VNil = ( _ ** VNil );

32+vfilter p Nil = ( _ ** Nil );

3133vfilter p (x :: xs) with (vfilter p xs) {

3234 vfilter p (x :: xs) | ( _ ** xs' )

3335 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );

3436}

3537

38+}

src/Core/CoreParser.hs+6−4

@@ -60,11 +60,13 @@ pTestFile = do p <- many1 pDef ; eof

6060iName :: [String] -> CParser a Name

6161iName bad = do x <- identifier

6262 when (x `elem` bad) $ fail "Reserved identifier"

63− return (parseName x)

63+ return $ mkNS (parseName x)

6464 where

65− parseName x = case span (/= '.') x of

66− (x, "") -> UN x

67− (x, '.':y) -> NS x (parseName y)

65+ mkNS [x] = UN x

66+ mkNS (x:xs) = NS (UN x) xs

67+ parseName x = reverse $ case span (/= '.') x of

68+ (x, "") -> [x]

69+ (x, '.':y) -> x : parseName y

6870

6971pDef :: CParser a (Name, RDef)

7072pDef = try (do x <- iName []; lchar ':'; ty <- pTerm

src/Core/Elaborate.hs+2−3

@@ -201,6 +201,7 @@ patvar :: Name -> Elab ()

201201patvar n = do n' <- case n of

202202 UN _ -> return n

203203 MN _ _ -> unique_hole n

204+ NS _ _ -> return n

204205 processTactic' (PatVar n')

205206

206207patbind :: Name -> Elab ()

@@ -256,6 +257,7 @@ prepare_apply fn imps =

256257

257258 mkMN n@(MN _ _) = n

258259 mkMN n@(UN x) = MN 0 x

260+ mkMN (NS n xs) = NS (mkMN n) xs

259261

260262apply :: Raw -> [Bool] -> Elab [Name]

261263apply fn imps =

@@ -369,6 +371,3 @@ tryAll xs = tryAll' [] (fail "Nothing to try") (map fst xs)

369371 Error err -> do put s

370372 tryAll' cs (lift (tfail err)) xs

371373

372−

373−

374−

src/Core/Evaluate.hs+4−4

@@ -494,7 +494,7 @@ addOperator n ty a op uctxt

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

495495 uctxt { definitions = ctxt' }

496496

497−lookupTy :: Maybe Name -> Name -> Context -> [Type]

497+lookupTy :: Maybe [String] -> Name -> Context -> [Type]

498498lookupTy root n ctxt

499499 = do def <- lookupCtxt root n (definitions ctxt)

500500 case def of

@@ -503,7 +503,7 @@ lookupTy root n ctxt

503503 (Operator ty _ _) -> return ty

504504 (CaseOp _ ty _ _ _) -> return ty

505505

506−lookupP :: Maybe Name -> Name -> Context -> [Term]

506+lookupP :: Maybe [String] -> Name -> Context -> [Term]

507507lookupP root n ctxt

508508 = do def <- lookupCtxt root n (definitions ctxt)

509509 case def of

@@ -512,10 +512,10 @@ lookupP root n ctxt

512512 (CaseOp _ ty _ _ _) -> return (P Ref n ty)

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

514514

515−lookupDef :: Maybe Name -> Name -> Context -> [Def]

515+lookupDef :: Maybe [String] -> Name -> Context -> [Def]

516516lookupDef root n ctxt = lookupCtxt root n (definitions ctxt)

517517

518−lookupVal :: Maybe Name -> Name -> Context -> [Value]

518+lookupVal :: Maybe [String] -> Name -> Context -> [Value]

519519lookupVal root n ctxt

520520 = do def <- lookupCtxt root n (definitions ctxt)

521521 case def of

src/Core/TT.hs+31−11

@@ -91,24 +91,31 @@ traceWhen False _ a = a

9191-- Also MN for machine chosen names

9292

9393data Name = UN String

94− | NS String Name

94+ | NS Name [String] -- root, namespaces

9595 | MN Int String

9696 deriving (Eq, Ord)

9797

9898instance Show Name where

9999 show (UN n) = n

100− show (NS s n) = s ++ "." ++ show n

100+ show (NS n s) = showSep "." s ++ "." ++ show n

101101 show (MN i s) = "{" ++ s ++ show i ++ "}"

102102

103103

104104-- Contexts allow us to map names to things

105105-- TODO: Namespaces and ambiguous names

106106

107−type Ctxt a = Map.Map Name a

107+type Ctxt a = Map.Map Name (Map.Map Name a)

108108emptyContext = Map.empty

109109

110−addDef :: Name -> a -> Ctxt a -> Ctxt a

111−addDef = Map.insert

110+nsroot (NS n _) = n

111+nsroot n = n

112+

113+addDef :: Show a => Name -> a -> Ctxt a -> Ctxt a

114+addDef n v ctxt = case Map.lookup (nsroot n) ctxt of

115+ Nothing -> Map.insert (nsroot n)

116+ (Map.insert n v Map.empty) ctxt

117+ Just xs -> Map.insert (nsroot n)

118+ (Map.insert n v xs) ctxt

112119

113120{- lookup a name in the context, given an optional namespace.

114121 The name (n) may itself have a (partial) namespace given.

@@ -122,15 +129,28 @@ addDef = Map.insert

122129

123130-}

124131

125−lookupCtxt :: Maybe Name -> Name -> Ctxt a -> [a]

126−lookupCtxt nspace n ctxt = case Map.lookup n ctxt of

127− Just x -> [x]

128− Nothing -> []

132+lookupCtxtName :: Maybe [String] -> Name -> Ctxt a -> [(Name, a)]

133+lookupCtxtName nspace n ctxt = case Map.lookup (nsroot n) ctxt of

134+ Just xs -> filterNS (Map.toList xs)

135+ Nothing -> []

136+ where

137+ filterNS [] = []

138+ filterNS ((found, v) : xs)

139+ | nsmatch n found = (found, v) : filterNS xs

140+ | otherwise = filterNS xs

141+

142+ nsmatch (NS n ns) (NS p ps) = ns `isPrefixOf` ps

143+ nsmatch (NS _ _) _ = False

144+ nsmatch looking found = True

145+

146+lookupCtxt :: Maybe [String] -> Name -> Ctxt a -> [a]

147+lookupCtxt ns n ctxt = map snd (lookupCtxtName ns n ctxt)

129148

130149toAlist :: Ctxt a -> [(Name, a)]

131−toAlist = Map.toList

150+toAlist ctxt = let allns = map snd (Map.toList ctxt) in

151+ concat (map (Map.toList) allns)

132152

133−addAlist :: [(Name, a)] -> Ctxt a -> Ctxt a

153+addAlist :: Show a => [(Name, a)] -> Ctxt a -> Ctxt a

134154addAlist [] ctxt = ctxt

135155addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

136156

src/Idris/AbsSyntax.hs+13−7

@@ -238,6 +238,7 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

238238 | PClauses FC FnOpts Name [PClause' t] -- pattern clause

239239 | PData SyntaxInfo FC (PData' t) -- data declaration

240240 | PParams FC [(Name, t)] [PDecl' t] -- params block

241+ | PNamespace String [PDecl' t] -- new namespace

241242 | PClass SyntaxInfo FC

242243 [t] -- constraints

243244 Name

@@ -277,6 +278,7 @@ declared (PClauses _ _ n _) = [] -- not a declaration

277278declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts

278279 where fstt (a, _, _) = a

279280declared (PParams _ _ ds) = concatMap declared ds

281+declared (PNamespace _ ds) = concatMap declared ds

280282-- declared (PImport _) = []

281283

282284updateN :: [(Name, Name)] -> Name -> Name

@@ -388,9 +390,9 @@ type PArg = PArg' PTerm

388390data ClassInfo = CI { instanceName :: Name,

389391 class_methods :: [(Name, PTerm)],

390392 class_params :: [Name] }

393+ deriving Show

391394

392−

393−-- Syntactic sugar info (TODO: namespaces, modules)

395+-- Syntactic sugar info

394396

395397data DSL = DSL { dsl_bind :: Name,

396398 dsl_return :: Name }

@@ -411,13 +413,14 @@ initDSL = DSL (UN ">>=") (UN "return")

411413

412414data SyntaxInfo = Syn { using :: [(Name, PTerm)],

413415 syn_params :: [(Name, PTerm)],

416+ syn_namespace :: [String],

414417 no_imp :: [Name],

415418 decoration :: Name -> Name,

416419 inPattern :: Bool,

417420 dsl_info :: DSL }

418421 deriving Show

419422

420−defaultSyntax = Syn [] [] [] id False initDSL

423+defaultSyntax = Syn [] [] [] [] id False initDSL

421424

422425--- Pretty printing declarations and terms

423426

@@ -866,11 +869,13 @@ aiFn :: IState -> FC -> Name -> [PArg] -> PTerm

866869aiFn ist fc f as

867870 | f `elem` primNames = PApp fc (PRef fc f) as

868871aiFn ist fc f as

869− -- TODO: This is where namespaces get resolved by adding

870− -- PAlternative

871− = case lookupCtxt Nothing f (idris_implicits ist) of

872− [ns] -> mkPApp fc (length ns) (PRef fc f) (insertImpl ns as)

872+ -- This is where namespaces get resolved by adding PAlternative

873+ = case lookupCtxtName Nothing f (idris_implicits ist) of

874+ [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

873875 [] -> mkPApp fc 1 (PRef fc f) as

876+ alts -> PAlternative $

877+ map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

878+ (insertImpl ns as)) alts

874879 where

875880 insertImpl :: [PArg] -> [PArg] -> [PArg]

876881 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

@@ -939,6 +944,7 @@ dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

939944dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)

940945dumpDecl (PData _ _ d) = showDImp True d

941946dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

947+dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"

942948dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

943949dumpDecl (PClass _ _ cs n ps ds)

944950 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds

src/Idris/Delaborate.hs+7−2

@@ -21,7 +21,7 @@ delab ist tm = de [] tm

2121 de env (P _ n _) | n == unitTy = PTrue un

2222 | n == unitCon = PTrue un

2323 | n == falseTy = PFalse un

24− | otherwise = PRef un n

24+ | otherwise = PRef un (dens n)

2525 de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de (n:env) sc)

2626 de env (Bind n (Pi ty) sc) = PPi expl n (de env ty) (de (n:env) sc)

2727 de env (Bind n (Let ty val) sc)

@@ -30,12 +30,17 @@ delab ist tm = de [] tm

3030 de env (Constant i) = PConstant i

3131 de env (Set i) = PSet

3232

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

34+ [_] -> n -- just one thing

35+ _ -> ns

36+ dens n = n

37+

3338 deFn env (App f a) args = deFn env f (a:args)

3439 deFn env (P _ n _) [l,r] | n == pairTy = PPair un (de env l) (de env r)

3540 | n == eqCon = PRefl un

3641 deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)

3742 | n == eqTy = PEq un (de env l) (de env r)

38− deFn env (P _ n _) args = mkPApp n (map (de env) args)

43+ deFn env (P _ n _) args = mkPApp (dens n) (map (de env) args)

3944 deFn env f args = PApp un (de env f) (map pexp (map (de env) args))

4045

4146 mkPApp n args

src/Idris/ElabDecls.hs+24−14

@@ -96,7 +96,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

9696 let tree = simpleCase tcase (map debind pats)

9797 logLvl 3 (show tree)

9898 ctxt <- getContext

99− case lookupTy Nothing n ctxt of

99+ case lookupTy (namespace info) n ctxt of

100100 [ty] -> updateContext (addCasedef n (inlinable opts)

101101 tcase (map debind pats) ty)

102102 [] -> return ()

@@ -376,16 +376,19 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

376376 [PTerm] -> PTerm -> [PDecl] -> Idris ()

377377elabInstance info syn fc cs n ps t ds

378378 = do i <- get

379− ci <- case lookupCtxt Nothing n (idris_classes i) of

380− [c] -> return c

381− _ -> fail $ show n ++ " is not a type class"

379+ (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of

380+ [c] -> return c

381+ _ -> fail $ show n ++ " is not a type class"

382382 let iname = UN ('@':show n ++ "$" ++ show ps)

383383 elabType info syn fc iname t

384384 let ips = zip (class_params ci) ps

385− let mtys = map (\ (n, t) -> (decorate n, coninsert cs $ substMatches ips t))

385+ let ns = case n of

386+ NS n ns' -> ns'

387+ _ -> []

388+ let mtys = map (\ (n, t) -> (decorate ns n, coninsert cs $ substMatches ips t))

386389 (class_methods ci)

387390 logLvl 3 (show (mtys, ips))

388− let wb = map mkTyDecl mtys ++ map decorateid ds

391+ let wb = map mkTyDecl mtys ++ map (decorateid ns) ds

389392 let lhs = PRef fc iname

390393 let rhs = PApp fc (PRef fc (instanceName ci))

391394 (map (pexp . mkMethApp) mtys)

@@ -407,14 +410,16 @@ elabInstance info syn fc cs n ps t ds

407410

408411 papp fc f [] = f

409412 papp fc f as = PApp fc f as

410− decorate (UN n) = UN ('!':n)

411− decorate (NS s n) = NS s (decorate n)

412− decorateid (PTy s f n t) = PTy s f (decorate n) t

413− decorateid (PClauses f o n cs) = PClauses f o (decorate n) (map dc cs)

414− where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds

415− dc (PWith n t as w ds) = PWith (decorate n) (dappname t) as w

416− (map decorateid ds)

417− dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

413+

414+ decorate ns (UN n) = NS (UN ('!':n)) ns

415+ decorate ns (NS (UN n) s) = NS (UN ('!':n)) ns

416+

417+ decorateid ns (PTy s f n t) = PTy s f (decorate ns n) t

418+ decorateid ns (PClauses f o n cs) = PClauses f o (decorate ns n) (map dc cs)

419+ where dc (PClause n t as w ds) = PClause (decorate ns n) (dappname t) as w ds

420+ dc (PWith n t as w ds) = PWith (decorate ns n) (dappname t) as w

421+ (map (decorateid ns) ds)

422+ dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate ns n)) as

418423 dappname t = t

419424 mkTyDecl (n, t) = PTy syn fc n t

420425

@@ -469,6 +474,11 @@ elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

469474 newb = addAlist dsParams (inblock info) in

470475 info { params = newps,

471476 inblock = newb }

477+elabDecl' info (PNamespace n ps) = mapM_ (elabDecl' ninfo) ps

478+ where

479+ ninfo = case namespace info of

480+ Nothing -> info { namespace = Just [n] }

481+ Just ns -> info { namespace = Just (n:ns) }

472482elabDecl' info (PClass s f cs n ps ds) = do iLOG $ "Elaborating class " ++ show n

473483 elabClass info s f cs n ps ds

474484elabDecl' info (PInstance s f cs n ps t ds)

src/Idris/ElabTerm.hs+19−13

@@ -15,9 +15,10 @@ import Data.List

1515

1616data ElabInfo = EInfo { params :: [(Name, PTerm)],

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

18− liftname :: Name -> Name }

18+ liftname :: Name -> Name,

19+ namespace :: Maybe [String] }

1920

20−toplevel = EInfo [] emptyContext id

21+toplevel = EInfo [] emptyContext id Nothing

2122

2223-- Using the elaborator, convert a term in raw syntax to a fully

2324-- elaborated, typechecked term.

@@ -108,7 +109,7 @@ elab ist info pattern tm

108109 try (do apply (Var n) []; solve)

109110 (patvar n)

110111 else do apply (Var n) []; solve

111− where inparamBlock n = case lookupCtxt Nothing n (inblock info) of

112+ where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of

112113 [] -> False

113114 _ -> True

114115 elab' (PRef fc n) = erun fc $ do apply (Var n) []; solve

@@ -185,7 +186,10 @@ elab ist info pattern tm

185186 solve

186187 elab' Placeholder = do (h : hs) <- get_holes

187188 movelast h

188− elab' (PMetavar n) = do attack; defer n; solve

189+ elab' (PMetavar n) = let n' = case namespace info of

190+ Just xs@(_:_) -> NS n xs

191+ _ -> n in

192+ do attack; defer n'; solve

189193 elab' (PProof ts) = do mapM_ (runTac True ist) ts

190194 elab' (PTactics ts) = do mapM_ (runTac False ist) ts

191195 elab' (PElabError e) = fail e

@@ -229,16 +233,16 @@ resolveTC depth ist

229233 (blunderbuss t ns)

230234 | otherwise = blunderbuss t ns

231235 tcname (UN ('@':_)) = True

232− tcname (NS _ n) = tcname n

236+ tcname (NS n _) = tcname n

233237 tcname _ = False

234238

235239 resolve n depth

236240 | depth == 0 = fail $ "Can't resolve type class"

237241 | otherwise

238242 = do t <- goal

239− let imps = case lookupCtxt Nothing n (idris_implicits ist) of

243+ let imps = case lookupCtxtName Nothing n (idris_implicits ist) of

240244 [] -> []

241− [args] -> map isImp args -- won't be overloaded!

245+ [args] -> map isImp (snd args) -- won't be overloaded!

242246 args <- apply (Var n) imps

243247 mapM_ (\ (_,n) -> do focus n

244248 resolveTC (depth - 1) ist)

@@ -275,12 +279,14 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

275279 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

276280 runT (Exact tm) = do elab ist toplevel False tm

277281 when autoSolve solveAll

278− runT (Refine fn []) = do imps <- case lookupCtxt Nothing fn (idris_implicits ist) of

279− [] -> envArgs fn

280− -- FIXME: resolve ambiguities

281− [args] -> return $ map isImp args

282− ns <- apply (Var fn) imps

283− when autoSolve solveAll

282+ runT (Refine fn [])

283+ = do (fn', imps) <- case lookupCtxtName Nothing fn (idris_implicits ist) of

284+ [] -> do a <- envArgs fn

285+ return (fn, a)

286+ -- FIXME: resolve ambiguities

287+ [(n, args)] -> return $ (n, map isImp args)

288+ ns <- apply (Var fn') imps

289+ when autoSolve solveAll

284290 where isImp (PImp _ _ _ _) = True

285291 isImp _ = False

286292 envArgs n = do e <- get_env

src/Idris/Parser.hs+39−14

@@ -148,6 +148,7 @@ collect (c@(PClauses _ o _ _) : ds)

148148 getfc (PClauses fc _ _ _) = fc

149149

150150collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

151+collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

151152collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'

152153collect (PInstance f s cs n ps t ds : ds')

153154 = PInstance f s cs n ps t (collect ds) : collect ds'

@@ -168,6 +169,7 @@ pDecl syn

168169 return [d']

169170 <|> pUsing syn

170171 <|> pParams syn

172+ <|> pNamespace syn

171173 <|> pClass syn

172174 <|> pInstance syn

173175 <|> pDirective

@@ -237,7 +239,8 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'

237239 return (Symbol sym)

238240

239241pFunDecl' :: SyntaxInfo -> IParser PDecl

240−pFunDecl' syn = try (do n <- pfName;

242+pFunDecl' syn = try (do n_in <- pfName

243+ let n = expandNS syn n_in

241244 ty <- pTSig syn

242245 fc <- pfc

243246 lchar ';'

@@ -270,6 +273,20 @@ pParams syn =

270273 fc <- pfc

271274 return [PParams fc ns (concat ds)]

272275

276+pNamespace :: SyntaxInfo -> IParser [PDecl]

277+pNamespace syn =

278+ do reserved "namespace";

279+ n <- identifier

280+ lchar '{'

281+ ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })

282+ lchar '}'

283+ return [PNamespace n (concat ds)]

284+

285+expandNS :: SyntaxInfo -> Name -> Name

286+expandNS syn n = case syn_namespace syn of

287+ [] -> n

288+ xs -> NS n xs

289+

273290--------- Fixity ---------

274291

275292pFixity :: IParser PDecl

@@ -295,7 +312,7 @@ pClass :: SyntaxInfo -> IParser [PDecl]

295312pClass syn = do reserved "class"

296313 fc <- pfc

297314 cons <- pConstList syn

298− n <- pName

315+ n_in <- pName; let n = expandNS syn n_in

299316 cs <- many1 carg

300317 reserved "where"; lchar '{'

301318 ds <- many1 $ pFunDecl syn;

@@ -607,14 +624,16 @@ prefix name f = Prefix (do { reservedOp name; fc <- pfc;

607624

608625pData :: SyntaxInfo -> IParser PDecl

609626pData syn = try (do reserved "data"; fc <- pfc

610− tyn <- pfName; ty <- pTSig syn

627+ tyn_in <- pfName; ty <- pTSig syn

628+ let tyn = expandNS syn tyn_in

611629 reserved "where"

612630-- ty' <- implicit syn tyn ty

613631 cons <- sepBy (pConstructor syn) (lchar '|')

614632 lchar ';'

615633 return $ PData syn fc (PDatadecl tyn ty cons))

616634 <|> do reserved "data"; fc <- pfc

617− tyn <- pfName; args <- many pName

635+ tyn_in <- pfName; args <- many pName

636+ let tyn = expandNS syn tyn_in

618637 lchar '='

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

620639 lchar ';'

@@ -636,14 +655,16 @@ bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)

636655

637656pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)

638657pConstructor syn

639− = do cn <- pfName; fc <- pfc

658+ = do cn_in <- pfName; fc <- pfc

659+ let cn = expandNS syn cn_in

640660 ty <- pTSig syn

641661-- ty' <- implicit syn cn ty

642662 return (cn, ty, fc)

643663

644664pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)

645665pSimpleCon syn

646− = do cn <- pfName

666+ = do cn_in <- pfName

667+ let cn = expandNS syn cn_in

647668 fc <- pfc

648669 args <- many (pSimpleExpr syn)

649670 return (cn, args, fc)

@@ -668,7 +689,7 @@ pRHS syn n = do lchar '='; pExpr syn

668689

669690pClause :: SyntaxInfo -> IParser PClause

670691pClause syn

671− = try (do n <- pfName

692+ = try (do n_in <- pfName; let n = expandNS syn n_in

672693 cargs <- many (pConstraintArg syn)

673694 iargs <- many (pImplicitArg syn)

674695 fc <- pfc

@@ -677,11 +698,13 @@ pClause syn

677698 rhs <- pRHS syn n

678699 ist <- getState

679700 let ctxt = tt_ctxt ist

680− (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'

681− return ([], [])]

701+ let wsyn = syn { syn_namespace = [] }

702+ (wheres, nmap) <- choice [pWhereblock n wsyn,

703+ do lchar ';'

704+ return ([], [])]

682705 return $ PClause n (PApp fc (PRef fc n)

683706 (iargs ++ cargs ++ map pexp args)) wargs rhs wheres)

684− <|> try (do n <- pfName

707+ <|> try (do n_in <- pfName; let n = expandNS syn n_in

685708 cargs <- many (pConstraintArg syn)

686709 iargs <- many (pImplicitArg syn)

687710 fc <- pfc

@@ -698,19 +721,21 @@ pClause syn

698721

699722 <|> do l <- pArgExpr syn

700723 op <- operator

701− let n = UN op

724+ let n = expandNS syn (UN op)

702725 r <- pArgExpr syn

703726 fc <- pfc

704727 wargs <- many (pWExpr syn)

705728 rhs <- pRHS syn n

706− (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'

707− return ([], [])]

729+ let wsyn = syn { syn_namespace = [] }

730+ (wheres, nmap) <- choice [pWhereblock n wsyn,

731+ do lchar ';'

732+ return ([], [])]

708733 return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r])

709734 wargs rhs wheres

710735

711736 <|> do l <- pArgExpr syn

712737 op <- operator

713− let n = UN op

738+ let n = expandNS syn (UN op)

714739 r <- pArgExpr syn

715740 fc <- pfc

716741 wargs <- many (pWExpr syn)

test/test001/test001.idr+1−1

@@ -8,7 +8,7 @@ interpTy (TyFun s t) = interpTy s -> interpTy t;

88using (G : Vect Ty n) {

99

1010 data Env : Vect Ty n -> Set where

11− Empty : Env VNil

11+ Empty : Env Nil

1212 | Extend : interpTy a -> Env G -> Env (a :: G);

1313

1414 envLookup : (i : Fin n) -> Env G -> interpTy (vlookup i G);