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

git.iko.soy/Idris-dev

Elaborating instance declarations

commit169d8c01f78156dddb4209c1c44cf5d244a72c91 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 8 Nov 2011, 19:54 (15 years ago) parentf2459a5

5 files changed+126−36

compare with master

unifiedsplit

lib/prelude.idr+47−21 src/Core/CoreParser.hs+1−1 src/Idris/AbsSyntax.hs+17−4 src/Idris/ElabDecls.hs+57−7 src/Idris/Parser.hs+4−3

lib/prelude.idr+47−21

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

1111 show : a -> String;

1212}

1313

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−

2314instance Show Nat where {

2415 show O = "O";

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

2617}

2718

28−-}

29−

30−instance showInt : Show Int;

31−instance showInt = instanceShow show where {

32− show : Int -> String;

19+instance Show Int where {

3320 show = prim__intToStr;

3421}

3522

36−instance showFloat : Show Float;

37−instance showFloat = instanceShow show where {

38− show : Float -> String;

23+instance Show Float where {

3924 show = prim__floatToStr;

4025}

4126

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

43−instance showList = instanceShow lshow where {

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

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

27+instance Show Bool 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+

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

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

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

4739 show' Nil = "";

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

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

5042 }

5143}

5244

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+

5379

5480---- some basic io

5581

src/Core/CoreParser.hs+1−1

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

1919 opLetter = iOpLetter,

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

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

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

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

2323 "infix", "infixl", "infixr", "prefix",

2424 "where", "with", "forall", "syntax", "proof",

2525 "using", "params", "namespace", "class", "instance",

src/Idris/AbsSyntax.hs+17−4

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

3131 idris_infixes :: [FixDecl],

3232 idris_implicits :: Ctxt [PArg],

3333 idris_statics :: Ctxt [Bool],

34− idris_classes :: Ctxt [Name],

34+ idris_classes :: Ctxt ClassInfo,

3535 idris_log :: String,

3636 idris_options :: IOption,

3737 idris_name :: Int,

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

190190 Name

191191 [(Name, t)] -- parameters

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

194198 | PSyntax FC Syntax

195199 deriving Functor

196200

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

319323

320324type PArg = PArg' PTerm

321325

326+-- Type class data

327+

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

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

330+ class_params :: [Name] }

331+

332+

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

323334

324335data DSL = DSL { dsl_bind :: Name,

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

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

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

579590

591+ en (PQuote (Var n))

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

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

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

582595 (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 ++ "}

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

837850dumpDecl (PClass _ _ cs n ps ds)

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

839−dumpDecl (PInstance _ _ n t ds)

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

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

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

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

842855

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

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

297297 elabDecl info ddecl

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

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

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

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

300301 mapM_ (elabDecl info) (concat fns)

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

303305 where

304306 pibind [] x = x

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

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

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

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

316318

317− tfun cn c all (m, ty)

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

318320 = do let ty' = insertConstraint c ty

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

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

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

355357 toExp ns e sc = sc

356358

357359elabInstance :: ElabInfo -> SyntaxInfo ->

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

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

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

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

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

360409

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

362411 pbinds sc

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

405454 inblock = newb }

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

407456 elabClass info s f cs n ps ds

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

409− elabInstance info s f n t ds

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

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

459+ elabInstance info s f cs n ps t ds

410460

411461

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

src/Idris/Parser.hs+4−3

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

146146

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

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

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

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

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

150151collect (d : ds) = d : collect ds

151152collect [] = []

152153

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

311312 reserved "where"; lchar '{'

312313 ds <- many1 $ pFunDecl syn;

313314 lchar '}'

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

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

315316

316317--------- Expressions ---------

317318

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

383384 return $ PQuote t)

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

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

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

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

389390 lchar '}'