169d8c0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Elaborating instance declarations

169d8c0Edwin Brady15 years ago

lib/prelude.idr+47−21

compare with master

unifiedsplit

@@ -11,38 +11,30 @@ class Show a where {

11 show : a -> String;

12}

14−instance showNat : Show Nat;

15−instance showNat = instanceShow show where {

16− show : Nat -> String;

17− show O = "O";

18− show (S k) = "s" ++ show k;

19−}

20−

21−{-

22−

23instance Show Nat where {

14instance Show Nat where {

24 show O = "O";

15 show O = "O";

25 show (S k) = "s" ++ show k;

16 show (S k) = "s" ++ show k;

26}

17}

28−-}

29−

30−instance showInt : Show Int;

19+instance Show Int where {

31−instance showInt = instanceShow show where {

32− show : Int -> String;

33 show = prim__intToStr;

20 show = prim__intToStr;

34}

21}

36−instance showFloat : Show Float;

23+instance Show Float where {

37−instance showFloat = instanceShow show where {

38− show : Float -> String;

39 show = prim__floatToStr;

24 show = prim__floatToStr;

40}

25}

42−instance showList : Show a => Show (List a);

27+instance Show Bool where {

43−instance showList = instanceShow lshow where {

28+ show True = "True";

29+ show False = "False";

30+}

31+

32+instance (Show a, Show b) => Show (a, b) where {

33+ show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")";

34+}

35+

44− lshow : Show a => List a -> String;

36+instance Show a => Show (List a) where {

45− lshow xs = "[" ++ show' xs ++ "]" where {

37+ show xs = "[" ++ show' xs ++ "]" where {

46 show' : Show a => List a -> String;

38 show' : Show a => List a -> String;

47 show' Nil = "";

39 show' Nil = "";

48 show' (Cons x Nil) = show x;

40 show' (Cons x Nil) = show x;

@@ -50,6 +42,40 @@ instance showList = instanceShow lshow where {

50 }

42 }

51}

43}

45+---- Monad and instances

46+

47+infixl 5 >>= ;

48+

49+class Monad (m : Set -> Set) where {

50+ return : a -> m a;

51+ (>>=) : m a -> (a -> m b) -> m b;

52+}

53+

54+class Monad m => MonadPlus (m : Set -> Set) where {

55+ mplus : m a -> m a -> m a;

56+ mzero : m a;

57+}

58+

59+instance Monad IO where {

60+ return t = io_return t;

61+ b >>= k = io_bind b k;

62+}

63+

64+instance Monad Maybe where {

65+ return = Just;

66+

67+ Nothing >>= k = Nothing;

68+ (Just x) >>= k = k x;

69+}

70+

71+instance MonadPlus Maybe where {

72+ mzero = Nothing;

73+

74+ mplus (Just x) _ = Just x;

75+ mplus Nothing (Just y) = Just y;

76+ mplus Nothing Nothing = Nothing;

77+}

78+

54---- some basic io

80---- some basic io

src/Core/CoreParser.hs+1−1

@@ -19,7 +19,7 @@ idrisDef = haskellDef {

19 opLetter = iOpLetter,

20 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

21 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",

22− "do", "dsl", "import", "return", -- "refl",

22+ "do", "dsl", "import", -- "refl",

23 "infix", "infixl", "infixr", "prefix",

24 "where", "with", "forall", "syntax", "proof",

25 "using", "params", "namespace", "class", "instance",

src/Idris/AbsSyntax.hs+17−4

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

31 idris_infixes :: [FixDecl],

32 idris_implicits :: Ctxt [PArg],

33 idris_statics :: Ctxt [Bool],

34− idris_classes :: Ctxt [Name],

34+ idris_classes :: Ctxt ClassInfo,

35 idris_log :: String,

36 idris_options :: IOption,

37 idris_name :: Int,

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

190 Name

191 [(Name, t)] -- parameters

192 [PDecl' t] -- declarations

193− | PInstance SyntaxInfo FC Name t [PDecl' t]

193+ | PInstance SyntaxInfo FC [t] -- constraints

194+ Name -- class

195+ [t] -- parameters

196+ t -- full instance type

197+ [PDecl' t]

194 | PSyntax FC Syntax

198 | PSyntax FC Syntax

195 deriving Functor

199 deriving Functor

196

200

@@ -319,6 +323,13 @@ pconst = PConstraint 0 False

319

323

320type PArg = PArg' PTerm

324type PArg = PArg' PTerm

321

325

326+-- Type class data

327+

328+data ClassInfo = CI { instanceName :: Name,

329+ class_methods :: [(Name, PTerm)],

330+ class_params :: [Name] }

331+

332+

322-- Syntactic sugar info (TODO: namespaces, modules)

333-- Syntactic sugar info (TODO: namespaces, modules)

323

334

324data DSL = DSL { dsl_bind :: Name,

335data DSL = DSL { dsl_bind :: Name,

@@ -577,6 +588,8 @@ expandParams dec ps ns tm = en tm

577 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

588 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

578 en (PProof ts) = PProof (map (fmap en) ts)

589 en (PProof ts) = PProof (map (fmap en) ts)

579

590

591+ en (PQuote (Var n))

592+ | n `elem` ns = PQuote (Var (dec n))

580 en (PApp fc (PRef fc' n) as)

593 en (PApp fc (PRef fc' n) as)

581 | n `elem` ns = PApp fc (PRef fc' (dec n))

594 | n `elem` ns = PApp fc (PRef fc' (dec n))

582 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

595 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

@@ -836,8 +849,8 @@ dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}

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

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

837dumpDecl (PClass _ _ cs n ps ds)

850dumpDecl (PClass _ _ cs n ps ds)

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

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

839−dumpDecl (PInstance _ _ n t ds)

852+dumpDecl (PInstance _ _ cs n _ t ds)

840− = "instance " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds

853+ = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds

841-- dumpDecl (PImport i) = "import " ++ i

854-- dumpDecl (PImport i) = "import " ++ i

842

855

843-- syntactic match of a against b, returning pair of variables in a

856-- syntactic match of a against b, returning pair of variables in a

src/Idris/ElabDecls.hs+57−7

@@ -296,10 +296,12 @@ elabClass info syn fc constraints tn ps ds

296 let ddecl = PData syn fc (PDatadecl tn tty cons)

297 elabDecl info ddecl

298 -- for each method, build a top level function

299+ let usyn = syn { using = ps ++ using syn }

299− fns <- mapM (tfun cn constraint (map fst imethods)) imethods

300+ fns <- mapM (tfun cn constraint usyn (map fst imethods)) imethods

300 mapM_ (elabDecl info) (concat fns)

301 mapM_ (elabDecl info) (concat fns)

301 i <- get

302 i <- get

302− put (i { idris_classes = addDef tn (map fst methods) (idris_classes i) })

303+ put (i { idris_classes = addDef tn (CI cn imethods (map fst ps))

304+ (idris_classes i) })

303 where

305 where

304 pibind [] x = x

306 pibind [] x = x

305 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

307 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

@@ -314,7 +316,7 @@ elabClass info syn fc constraints tn ps ds

314 tdecl (PClauses _ _ _) = fail "No default definitions allowed yet"

316 tdecl (PClauses _ _ _) = fail "No default definitions allowed yet"

315 tdecl _ = fail "Not allowed in a class declaration"

317 tdecl _ = fail "Not allowed in a class declaration"

316

318

317− tfun cn c all (m, ty)

319+ tfun cn c syn all (m, ty)

318 = do let ty' = insertConstraint c ty

320 = do let ty' = insertConstraint c ty

319 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]

321 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]

320 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

322 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

@@ -355,8 +357,55 @@ elabClass info syn fc constraints tn ps ds

355 toExp ns e sc = sc

357 toExp ns e sc = sc

356

358

357elabInstance :: ElabInfo -> SyntaxInfo ->

359elabInstance :: ElabInfo -> SyntaxInfo ->

360+ FC -> [PTerm] -> Name ->

358− FC -> Name -> PTerm -> [PDecl] -> Idris ()

361+ [PTerm] -> PTerm -> [PDecl] -> Idris ()

359−elabInstance info syn fc n t ds = fail "Not implemented"

362+elabInstance info syn fc cs n ps t ds

363+ = do i <- get

364+ ci <- case lookupCtxt n (idris_classes i) of

365+ Just c -> return c

366+ Nothing -> fail $ show n ++ " is not a type class"

367+ let iname = UN ['@':show n ++ "$" ++ show ps]

368+ elabType info syn fc iname t

369+ let ips = zip (class_params ci) ps

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

371+ (class_methods ci)

372+ logLvl 3 (show (mtys, ips))

373+ let wb = map mkTyDecl mtys ++ map decorateid ds

374+ let lhs = PRef fc iname

375+ let rhs = PApp fc (PRef fc (instanceName ci))

376+ (map (pexp . mkMethApp) mtys)

377+ let idecl = PClauses fc iname [PClause iname lhs [] rhs wb]

378+ iLOG (show idecl)

379+ elabDecl info idecl

380+ where

381+ mkMethApp (n, ty) = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

382+ lamBind i (PPi (Constraint _ _) _ _ sc) sc' = lamBind i sc sc'

383+ lamBind i (PPi _ n ty sc) sc' = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

384+ lamBind i _ sc = sc

385+ methArgs i (PPi (Imp _ _) n ty sc)

386+ = PImp 0 False n (PRef fc (MN i "meth")) : methArgs (i+1) sc

387+ methArgs i (PPi (Exp _ _) n ty sc)

388+ = PExp 0 False (PRef fc (MN i "meth")) : methArgs (i+1) sc

389+ methArgs i (PPi (Constraint _ _) n ty sc)

390+ = methArgs i sc

391+ methArgs i _ = []

392+

393+ papp fc f [] = f

394+ papp fc f as = PApp fc f as

395+ decorate (UN (n:ns)) = UN (('!':n) : ns)

396+ decorateid (PTy s f n t) = PTy s f (decorate n) t

397+ decorateid (PClauses f n cs) = PClauses f (decorate n) (map dc cs)

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

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

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

401+ dappname t = t

402+ mkTyDecl (n, t) = PTy syn fc n t

403+

404+ conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)

405+ conbind [] x = x

406+

407+ coninsert cs (PPi p@(Imp _ _) n t sc) = PPi p n t (coninsert cs sc)

408+ coninsert cs sc = conbind cs sc

360

409

361pbinds (Bind n (PVar t) sc) = do attack; patbind n

410pbinds (Bind n (PVar t) sc) = do attack; patbind n

362 pbinds sc

411 pbinds sc

@@ -405,8 +454,9 @@ elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

405 inblock = newb }

454 inblock = newb }

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

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

407 elabClass info s f cs n ps ds

456 elabClass info s f cs n ps ds

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

408−elabDecl' info (PInstance s f n t ds) = do iLOG $ "Elaborating instance " ++ show n

458+ = do iLOG $ "Elaborating instance " ++ show n

409− elabInstance info s f n t ds

459+ elabInstance info s f cs n ps t ds

410

460

411

461

412-- elabDecl' info (PImport i) = loadModule i

462-- elabDecl' info (PImport i) = loadModule i

src/Idris/Parser.hs+4−3

@@ -146,7 +146,8 @@ collect (c@(PClauses _ _ _) : ds)

146

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

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

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

149−collect (PInstance f s n t ds : ds') = PInstance f s n t (collect ds) : collect ds'

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

150collect (d : ds) = d : collect ds

151collect (d : ds) = d : collect ds

151collect [] = []

152collect [] = []

152

153

@@ -311,7 +312,7 @@ pInstance syn = do reserved "instance"

311 reserved "where"; lchar '{'

312 reserved "where"; lchar '{'

312 ds <- many1 $ pFunDecl syn;

313 ds <- many1 $ pFunDecl syn;

313 lchar '}'

314 lchar '}'

314− return [PInstance syn fc cn t (concat ds)]

315+ return [PInstance syn fc cs cn args t (concat ds)]

315

316

316--------- Expressions ---------

317--------- Expressions ---------

317

318

@@ -383,7 +384,7 @@ pSimpleExpr syn =

383 return $ PQuote t)

384 return $ PQuote t)

384 <|> do lchar '?'; x <- pName; return (PMetavar x)

385 <|> do lchar '?'; x <- pName; return (PMetavar x)

385 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)

386 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)

386− <|> do reserved "return"; fc <- pfc; return (PReturn fc)

387+-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)

387 <|> do reserved "proof"; lchar '{';

388 <|> do reserved "proof"; lchar '{';

388 ts <- endBy (pTactic syn) (lchar ';')

389 ts <- endBy (pTactic syn) (lchar ';')

389 lchar '}'

390 lchar '}'