fa5f1cd · Idris-dev · git.iko.soy

lib/builtins.idr+3−1

compare with master

unifiedsplit

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

21

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

23

24+namespace builtins {

25+

24id : a -> a;

26id : a -> a;

25id x = x;

27id x = x;

26

28

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

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

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

185(++) = prim__concat;

187(++) = prim__concat;

186

188

187−

189+}

lib/list.idr+3

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

1import builtins;

2

3+namespace list {

4+

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

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

4

6

5rev : List a -> List a;

7rev : List a -> List a;

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

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

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

35}

37}

36

38

39+}

lib/maybe.idr+3

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

1

2+namespace maybe {

3+

2data Maybe a = Nothing | Just a;

4data Maybe a = Nothing | Just a;

3

5

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

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

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

9maybe_bind Nothing k = Nothing;

11maybe_bind Nothing k = Nothing;

10maybe_bind (Just x) k = k x;

12maybe_bind (Just x) k = k x;

11

13

14+}

lib/nat.idr+3

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

1import builtins;

2

3+namespace nat {

4+

3data Nat = O | S Nat;

5data Nat = O | S Nat;

4

6

5plus : Nat -> Nat -> Nat;

7plus : Nat -> Nat -> Nat;

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

64 refine plusn_Sm;

66 refine plusn_Sm;

65};

67};

66

68

69+}

lib/prelude.idr+3

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

8

9-- Show and instances

10

11+namespace prelude {

12+

11class Show a where {

13class Show a where {

12 show : a -> String;

14 show : a -> String;

13}

15}

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

115readLine : IO String;

117readLine : IO String;

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

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

117

119

120+}

lib/vect.idr+6−3

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

1import nat;

2

3+namespace vect {

4+

3data Fin : Nat -> Set where

5data Fin : Nat -> Set where

4 fO : Fin (S k)

6 fO : Fin (S k)

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

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

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

15infixr 7 :: ;

17infixr 7 :: ;

16

18

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

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

18− VNil : Vect a O

20+ Nil : Vect a O

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

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

20

22

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

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

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

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

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

24

26

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

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

26−vapp VNil ys = ys;

28+vapp Nil ys = ys;

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

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

28

30

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

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

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

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

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

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

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

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

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

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

34}

36}

35

37

38+}

src/Core/CoreParser.hs+6−4

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

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

61iName bad = do x <- identifier

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

63− return (parseName x)

63+ return $ mkNS (parseName x)

64 where

65+ mkNS [x] = UN x

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

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

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

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

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

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

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

68

70

69pDef :: CParser a (Name, RDef)

71pDef :: CParser a (Name, RDef)

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

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

src/Core/Elaborate.hs+2−3

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

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

202 UN _ -> return n

203 MN _ _ -> unique_hole n

204+ NS _ _ -> return n

204 processTactic' (PatVar n')

205 processTactic' (PatVar n')

205

206

206patbind :: Name -> Elab ()

207patbind :: Name -> Elab ()

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

256

257

257 mkMN n@(MN _ _) = n

258 mkMN n@(MN _ _) = n

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

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

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

259

261

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

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

261apply fn imps =

263apply fn imps =

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

369 Error err -> do put s

371 Error err -> do put s

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

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

371

373

372−

373−

374−

src/Core/Evaluate.hs+4−4

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

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

495 uctxt { definitions = ctxt' }

496

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

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

498lookupTy root n ctxt

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

500 case def of

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

503 (Operator ty _ _) -> return ty

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

505

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

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

507lookupP root n ctxt

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

509 case def of

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

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

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

514

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

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

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

517

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

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

519lookupVal root n ctxt

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

521 case def of

src/Core/TT.hs+31−11

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

91-- Also MN for machine chosen names

92

93data Name = UN String

94− | NS String Name

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

95 | MN Int String

96 deriving (Eq, Ord)

97

98instance Show Name where

99 show (UN n) = n

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

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

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

102

103

104-- Contexts allow us to map names to things

105-- TODO: Namespaces and ambiguous names

106

107−type Ctxt a = Map.Map Name a

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

108emptyContext = Map.empty

109

110+nsroot (NS n _) = n

111+nsroot n = n

112+

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

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)

111−addDef = Map.insert

118+ (Map.insert n v xs) ctxt

112

119

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

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

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

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

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

122

129

123-}

130-}

124

131

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

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

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

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

127− Just x -> [x]

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

128− Nothing -> []

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)

129

148

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

149toAlist :: 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)

132

152

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

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

134addAlist [] ctxt = ctxt

154addAlist [] ctxt = ctxt

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

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

136

156

src/Idris/AbsSyntax.hs+13−7

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

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

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

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

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

241 | PClass SyntaxInfo FC

242 | PClass SyntaxInfo FC

242 [t] -- constraints

243 [t] -- constraints

243 Name

244 Name

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

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

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

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

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

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

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

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

280-- declared (PImport _) = []

282-- declared (PImport _) = []

281

283

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

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

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

388data ClassInfo = CI { instanceName :: Name,

390data ClassInfo = CI { instanceName :: Name,

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

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

390 class_params :: [Name] }

392 class_params :: [Name] }

393+ deriving Show

391

394

392−

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

395+-- Syntactic sugar info

394

396

395data DSL = DSL { dsl_bind :: Name,

397data DSL = DSL { dsl_bind :: Name,

396 dsl_return :: Name }

398 dsl_return :: Name }

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

411

413

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

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

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

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

416+ syn_namespace :: [String],

414 no_imp :: [Name],

417 no_imp :: [Name],

415 decoration :: Name -> Name,

418 decoration :: Name -> Name,

416 inPattern :: Bool,

419 inPattern :: Bool,

417 dsl_info :: DSL }

420 dsl_info :: DSL }

418 deriving Show

421 deriving Show

419

422

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

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

421

424

422--- Pretty printing declarations and terms

425--- Pretty printing declarations and terms

423

426

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

866aiFn ist fc f as

869aiFn ist fc f as

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

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

868aiFn ist fc f as

871aiFn ist fc f as

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

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

870− -- PAlternative

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

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

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

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

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

875 [] -> 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

874 where

879 where

875 insertImpl :: [PArg] -> [PArg] -> [PArg]

880 insertImpl :: [PArg] -> [PArg] -> [PArg]

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

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

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

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

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

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

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

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

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

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

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

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

943dumpDecl (PClass _ _ cs n ps ds)

949dumpDecl (PClass _ _ cs n ps ds)

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

950 = "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

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

22 | n == unitCon = PTrue un

23 | n == falseTy = PFalse un

24− | otherwise = PRef un n

24+ | otherwise = PRef un (dens n)

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

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

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

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

30 de env (Constant i) = PConstant i

31 de env (Set i) = PSet

32

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+

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

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

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

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

35 | n == eqCon = PRefl un

40 | n == eqCon = PRefl un

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

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

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

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

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

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

40

45

41 mkPApp n args

46 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

96 let tree = simpleCase tcase (map debind pats)

97 logLvl 3 (show tree)

98 ctxt <- getContext

99− case lookupTy Nothing n ctxt of

99+ case lookupTy (namespace info) n ctxt of

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

101 tcase (map debind pats) ty)

102 [] -> return ()

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

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

377elabInstance info syn fc cs n ps t ds

378 = do i <- get

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

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

380− [c] -> return c

380+ [c] -> return c

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

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

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

383 elabType info syn fc iname t

384 let ips = zip (class_params ci) ps

385+ let ns = case n of

386+ NS n ns' -> ns'

387+ _ -> []

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

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

386 (class_methods ci)

389 (class_methods ci)

387 logLvl 3 (show (mtys, ips))

390 logLvl 3 (show (mtys, ips))

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

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

389 let lhs = PRef fc iname

392 let lhs = PRef fc iname

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

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

391 (map (pexp . mkMethApp) mtys)

394 (map (pexp . mkMethApp) mtys)

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

407

410

408 papp fc f [] = f

411 papp fc f [] = f

409 papp fc f as = PApp fc f as

412 papp fc f as = PApp fc f as

413+

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

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

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

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

416+

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

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

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

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

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

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

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

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

416− (map decorateid ds)

421+ (map (decorateid ns) ds)

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

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

418 dappname t = t

423 dappname t = t

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

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

420

425

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

469 newb = addAlist dsParams (inblock info) in

474 newb = addAlist dsParams (inblock info) in

470 info { params = newps,

475 info { params = newps,

471 inblock = newb }

476 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) }

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

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

473 elabClass info s f cs n ps ds

483 elabClass info s f cs n ps ds

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

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

src/Idris/ElabTerm.hs+19−13

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

15

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

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

18− liftname :: Name -> Name }

18+ liftname :: Name -> Name,

19+ namespace :: Maybe [String] }

19

20

20−toplevel = EInfo [] emptyContext id

21+toplevel = EInfo [] emptyContext id Nothing

21

22

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

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

23-- elaborated, typechecked term.

24-- elaborated, typechecked term.

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

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

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

109 (patvar n)

110 (patvar n)

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

111 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

112 [] -> False

113 [] -> False

113 _ -> True

114 _ -> True

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

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

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

185 solve

186 solve

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

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

187 movelast h

188 movelast h

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

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

191+ _ -> n in

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

192+ do attack; defer n'; solve

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

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

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

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

191 elab' (PElabError e) = fail e

195 elab' (PElabError e) = fail e

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

229 (blunderbuss t ns)

233 (blunderbuss t ns)

230 | otherwise = blunderbuss t ns

234 | otherwise = blunderbuss t ns

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

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

232− tcname (NS _ n) = tcname n

236+ tcname (NS n _) = tcname n

233 tcname _ = False

237 tcname _ = False

234

238

235 resolve n depth

239 resolve n depth

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

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

237 | otherwise

241 | otherwise

238 = do t <- goal

242 = 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

240 [] -> []

244 [] -> []

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

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

242 args <- apply (Var n) imps

246 args <- apply (Var n) imps

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

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

244 resolveTC (depth - 1) ist)

248 resolveTC (depth - 1) ist)

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

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

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

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

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

277 when autoSolve solveAll

281 when autoSolve solveAll

282+ runT (Refine fn [])

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

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

279− [] -> envArgs fn

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

285+ return (fn, a)

280− -- FIXME: resolve ambiguities

286+ -- FIXME: resolve ambiguities

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

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

282− ns <- apply (Var fn) imps

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

283− when autoSolve solveAll

289+ when autoSolve solveAll

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

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

285 isImp _ = False

291 isImp _ = False

286 envArgs n = do e <- get_env

292 envArgs n = do e <- get_env

src/Idris/Parser.hs+39−14

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

148 getfc (PClauses fc _ _ _) = fc

149

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

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

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

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

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

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

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

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

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

168 return [d']

169 return [d']

169 <|> pUsing syn

170 <|> pUsing syn

170 <|> pParams syn

171 <|> pParams syn

172+ <|> pNamespace syn

171 <|> pClass syn

173 <|> pClass syn

172 <|> pInstance syn

174 <|> pInstance syn

173 <|> pDirective

175 <|> pDirective

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

237 return (Symbol sym)

239 return (Symbol sym)

238

240

239pFunDecl' :: SyntaxInfo -> IParser PDecl

241pFunDecl' :: 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

241 ty <- pTSig syn

244 ty <- pTSig syn

242 fc <- pfc

245 fc <- pfc

243 lchar ';'

246 lchar ';'

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

270 fc <- pfc

273 fc <- pfc

271 return [PParams fc ns (concat ds)]

274 return [PParams fc ns (concat ds)]

272

275

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+

273--------- Fixity ---------

290--------- Fixity ---------

274

291

275pFixity :: IParser PDecl

292pFixity :: IParser PDecl

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

295pClass syn = do reserved "class"

312pClass syn = do reserved "class"

296 fc <- pfc

313 fc <- pfc

297 cons <- pConstList syn

314 cons <- pConstList syn

298− n <- pName

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

299 cs <- many1 carg

316 cs <- many1 carg

300 reserved "where"; lchar '{'

317 reserved "where"; lchar '{'

301 ds <- many1 $ pFunDecl syn;

318 ds <- many1 $ pFunDecl syn;

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

607

624

608pData :: SyntaxInfo -> IParser PDecl

625pData :: SyntaxInfo -> IParser PDecl

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

626pData 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

611 reserved "where"

629 reserved "where"

612-- ty' <- implicit syn tyn ty

630-- ty' <- implicit syn tyn ty

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

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

614 lchar ';'

632 lchar ';'

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

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

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

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

618 lchar '='

637 lchar '='

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

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

620 lchar ';'

639 lchar ';'

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

636

655

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

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

638pConstructor syn

657pConstructor syn

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

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

659+ let cn = expandNS syn cn_in

640 ty <- pTSig syn

660 ty <- pTSig syn

641-- ty' <- implicit syn cn ty

661-- ty' <- implicit syn cn ty

642 return (cn, ty, fc)

662 return (cn, ty, fc)

643

663

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

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

645pSimpleCon syn

665pSimpleCon syn

646− = do cn <- pfName

666+ = do cn_in <- pfName

667+ let cn = expandNS syn cn_in

647 fc <- pfc

668 fc <- pfc

648 args <- many (pSimpleExpr syn)

669 args <- many (pSimpleExpr syn)

649 return (cn, args, fc)

670 return (cn, args, fc)

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

668

689

669pClause :: SyntaxInfo -> IParser PClause

690pClause :: SyntaxInfo -> IParser PClause

670pClause syn

691pClause syn

671− = try (do n <- pfName

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

672 cargs <- many (pConstraintArg syn)

693 cargs <- many (pConstraintArg syn)

673 iargs <- many (pImplicitArg syn)

694 iargs <- many (pImplicitArg syn)

674 fc <- pfc

695 fc <- pfc

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

677 rhs <- pRHS syn n

698 rhs <- pRHS syn n

678 ist <- getState

699 ist <- getState

679 let ctxt = tt_ctxt ist

700 let ctxt = tt_ctxt ist

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

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

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

703+ do lchar ';'

681− return ([], [])]

704+ return ([], [])]

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

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

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

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

685 cargs <- many (pConstraintArg syn)

708 cargs <- many (pConstraintArg syn)

686 iargs <- many (pImplicitArg syn)

709 iargs <- many (pImplicitArg syn)

687 fc <- pfc

710 fc <- pfc

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

698

721

699 <|> do l <- pArgExpr syn

722 <|> do l <- pArgExpr syn

700 op <- operator

723 op <- operator

701− let n = UN op

724+ let n = expandNS syn (UN op)

702 r <- pArgExpr syn

725 r <- pArgExpr syn

703 fc <- pfc

726 fc <- pfc

704 wargs <- many (pWExpr syn)

727 wargs <- many (pWExpr syn)

705 rhs <- pRHS syn n

728 rhs <- pRHS syn n

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

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

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

731+ do lchar ';'

707− return ([], [])]

732+ return ([], [])]

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

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

709 wargs rhs wheres

734 wargs rhs wheres

710

735

711 <|> do l <- pArgExpr syn

736 <|> do l <- pArgExpr syn

712 op <- operator

737 op <- operator

713− let n = UN op

738+ let n = expandNS syn (UN op)

714 r <- pArgExpr syn

739 r <- pArgExpr syn

715 fc <- pfc

740 fc <- pfc

716 wargs <- many (pWExpr syn)

741 wargs <- many (pWExpr syn)

test/test001/test001.idr+1−1

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

8using (G : Vect Ty n) {

9

10 data Env : Vect Ty n -> Set where

11− Empty : Env VNil

11+ Empty : Env Nil

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

13

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