de89a04 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add ElabInfo to pass through elaborator

de89a04Edwin Brady15 years ago

impl-paper/literature.bib+3−2

compare with master

unifiedsplit

@@ -52,11 +52,12 @@

52 bibsource = {DBLP, http://dblp.uni-trier.de}

53}

55−@inproceedings{epicdraft,

55+@inproceedings{epic-tfp,

56 author = {Edwin Brady},

57 title = {Epic --- a library for generating compilers},

58 year = 2011,

59− booktitle = {Draft Proceedings of {Trends in Functional Programming} ({TFP} '11)}

59+ booktitle = {{Trends in Functional Programming} ({TFP} '11)},

60+ note = {To appear}

60}

61}

62@inproceedings{ynot08,

63@inproceedings{ynot08,

impl-paper/overview.tex+3−1

@@ -24,7 +24,9 @@ High level view of steps we've taken to implement this new version:

24 report an error.

25\end{itemize}

26\item An Elaborator, as an EDSL, which is a language for applying primitive tactics and

27− constructing derived tactics.

27+ constructing derived tactics, from a high level syntax withe implicit arguments.

28+\item Advanced elaborations: using declarations, where clauses.

29+\item Adding primitive operators and a link to Epic~\cite{epic-tfp}.

28\end{itemize}

30\end{itemize}

30For the high level language: we need nothing more than the core type theory,

32For the high level language: we need nothing more than the core type theory,

src/Idris/AbsSyntax.hs+14

@@ -37,6 +37,9 @@ type Idris a = StateT IState IO a

37getContext :: Idris Context

38getContext = do i <- get; return (tt_ctxt i)

40+getIState :: Idris IState

41+getIState = get

42+

40setContext :: Context -> Idris ()

43setContext :: Context -> Idris ()

41setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )

44setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )

@@ -115,6 +118,14 @@ type PDecl = PDecl' PTerm

115type PData = PData' PTerm

118type PData = PData' PTerm

116type PClause = PClause' PTerm

119type PClause = PClause' PTerm

117

120

121+-- get all the names declared in a decl

122+

123+declared :: PDecl -> [Name]

124+declared (PFix _ _) = []

125+declared (PTy n t) = [n]

126+declared (PClauses n _) = [] -- not a declaration

127+declared (PData (PDatadecl n _ ts)) = n : map fst ts

128+

118-- High level language terms

129-- High level language terms

119--

130--

120data PTerm = PQuote Raw

131data PTerm = PQuote Raw

@@ -261,6 +272,9 @@ getInferTerm tm = error ("getInferTerm " ++ show tm)

261getInferType (Bind n b sc) = Bind n b $ getInferType sc

272getInferType (Bind n b sc) = Bind n b $ getInferType sc

262getInferType (App (App _ ty) _) = ty

273getInferType (App (App _ ty) _) = ty

263

274

275+piBind :: [(Name, PTerm)] -> PTerm -> PTerm

276+piBind [] t = t

277+piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)

264

278

265-- Dealing with implicit arguments

279-- Dealing with implicit arguments

266

280

src/Idris/ElabDecls.hs+74−27

@@ -4,6 +4,7 @@ module Idris.ElabDecls where

5import Idris.AbsSyntax

6import Idris.Error

7+import Idris.Delaborate

8import Core.TT

9import Core.TT

9import Core.Elaborate

10import Core.Elaborate

@@ -14,8 +15,16 @@ import Core.CaseTree

14import Control.Monad

15import Control.Monad

15import Debug.Trace

16import Debug.Trace

18+-- Data to pass to recursively called elaborators; e.g. for where blocks,

19+-- paramaterised declarations, etc.

20+

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

22+ liftname :: Name -> Name }

23+

24+toplevel = EInfo [] id

25+

17−elabType :: Name -> PTerm -> Idris ()

26+elabType :: ElabInfo -> Name -> PTerm -> Idris ()

18−elabType n ty

27+elabType info n ty

19 = do ctxt <- getContext

28 = do ctxt <- getContext

20 logLvl 2 $ "Type " ++ showImp True ty

29 logLvl 2 $ "Type " ++ showImp True ty

21 (ty', log) <- tclift $ elaborate ctxt n (Set 0) (build False ty)

30 (ty', log) <- tclift $ elaborate ctxt n (Set 0) (build False ty)

@@ -23,18 +32,18 @@ elabType n ty

23 logLvl 2 $ "---> " ++ show cty

32 logLvl 2 $ "---> " ++ show cty

24 updateContext (addTyDecl n (normalise ctxt [] cty))

33 updateContext (addTyDecl n (normalise ctxt [] cty))

26−elabData :: PData -> Idris ()

35+elabData :: ElabInfo -> PData -> Idris ()

27−elabData (PDatadecl n t dcons)

36+elabData info (PDatadecl n t dcons)

28 = do ctxt <- getContext

37 = do ctxt <- getContext

29 (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)

38 (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)

30 (cty, _) <- tclift $ recheck ctxt [] t'

39 (cty, _) <- tclift $ recheck ctxt [] t'

31 logLvl 2 $ "---> " ++ show cty

40 logLvl 2 $ "---> " ++ show cty

32 updateContext (addTyDecl n cty) -- temporary, to check cons

41 updateContext (addTyDecl n cty) -- temporary, to check cons

33− cons <- mapM elabCon dcons

42+ cons <- mapM (elabCon info) dcons

34 setContext (addDatatype (Data n cty cons) ctxt)

43 setContext (addDatatype (Data n cty cons) ctxt)

36−elabCon :: (Name, PTerm) -> Idris (Name, Type)

45+elabCon :: ElabInfo -> (Name, PTerm) -> Idris (Name, Type)

37−elabCon (n, t)

46+elabCon info (n, t)

38 = do ctxt <- getContext

47 = do ctxt <- getContext

39 iLOG $ "Constructor " ++ show n ++ " : " ++ showImp True t

48 iLOG $ "Constructor " ++ show n ++ " : " ++ showImp True t

40 (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)

49 (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)

@@ -43,9 +52,9 @@ elabCon (n, t)

43 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

52 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

44 return (n, cty)

53 return (n, cty)

46−elabClauses :: Name -> [PClause] -> Idris ()

55+elabClauses :: ElabInfo -> Name -> [PClause] -> Idris ()

47−elabClauses n cs

56+elabClauses info n cs

48− = do pats <- mapM elabClause cs

57+ = do pats <- mapM (elabClause info) cs

49 logLvl 3 (showSep "\n" (map (\ (l,r) ->

58 logLvl 3 (showSep "\n" (map (\ (l,r) ->

50 show l ++ " = " ++

59 show l ++ " = " ++

51 show r) pats))

60 show r) pats))

@@ -60,8 +69,8 @@ elabClauses n cs

60 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)

69 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)

61 depat x = x

70 depat x = x

63−elabVal :: PTerm -> Idris (Term, Type)

72+elabVal :: ElabInfo -> PTerm -> Idris (Term, Type)

64−elabVal tm

73+elabVal info tm

65 = do ctxt <- getContext

74 = do ctxt <- getContext

66 logLvl 10 (show tm)

75 logLvl 10 (show tm)

67 (tm', _) <- tclift $ elaborate ctxt (MN 0 "val") infP

76 (tm', _) <- tclift $ elaborate ctxt (MN 0 "val") infP

@@ -71,8 +80,8 @@ elabVal tm

71 iLOG (show vtm)

80 iLOG (show vtm)

72 tclift $ recheck ctxt [] vtm

81 tclift $ recheck ctxt [] vtm

74−elabClause :: PClause -> Idris (Term, Term)

83+elabClause :: ElabInfo -> PClause -> Idris (Term, Term)

75−elabClause (PClause _ lhs rhs whereblock)

84+elabClause info (PClause _ lhs rhs whereblock)

76 = do ctxt <- getContext

85 = do ctxt <- getContext

77 -- Build the LHS as an "Infer", and pull out its type and

86 -- Build the LHS as an "Infer", and pull out its type and

78 -- pattern bindings

87 -- pattern bindings

@@ -83,10 +92,11 @@ elabClause (PClause _ lhs rhs whereblock)

83 logLvl 3 (show lhs_tm)

92 logLvl 3 (show lhs_tm)

84 (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm

93 (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm

85 -- TODO: elaborate where block here.

94 -- TODO: elaborate where block here.

86− -- probably the way to check the where clauses is to

95+ -- probably the way to check the where clauses is to recursively

87− -- treat them as in a params block.

96+ -- call the elaborator with a list of variables assumed by the

88− -- Will need to know what the params are and add them while

97+ -- where block (i.e. add those variables to all types and clauses

89− -- elaborating.

98+ -- which are elaborated).

99+

90 -- Now build the RHS, using the type of the LHS as the goal.

100 -- Now build the RHS, using the type of the LHS as the goal.

91 iLOG (showImp True rhs)

101 iLOG (showImp True rhs)

92 (rhs', _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

102 (rhs', _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

@@ -105,16 +115,53 @@ elabClause (PClause _ lhs rhs whereblock)

105 psolve (Bind n (PVar t) sc) = do solve; psolve sc

115 psolve (Bind n (PVar t) sc) = do solve; psolve sc

106 psolve tm = return ()

116 psolve tm = return ()

107

117

118+ pvars (Bind n (PVar t) sc) = (n, t) : pvars sc

119+ pvars _ = []

120+

108−elabDecl :: PDecl -> Idris ()

121+elabDecl :: ElabInfo -> PDecl -> Idris ()

109−elabDecl d = idrisCatch (elabDecl' d) (\e -> iputStrLn (report e))

122+elabDecl info d = idrisCatch (elabDecl' info d) (\e -> iputStrLn (report e))

123+

124+elabDecl' info (PFix _ _) = return () -- nothing to elaborate

125+elabDecl' info (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n

126+ elabType info n ty

127+elabDecl' info (PData d) = do iLOG $ "Elaborating " ++ show d

128+ elabData info d

129+elabDecl' info d@(PClauses n ps) = do iLOG $ "Elaborating " ++ show n

130+ elabClauses info n ps

131+

132+{- not finished...

133+parameterise :: [(Name, Type)] -> (Name -> Name) -> [PDecl] -> Idris [PDecl]

134+parameterise ns hide ds = do

135+ i <- getIState

136+ let pns = map (\ (n, t) -> (n, delab i t)) ns

137+ mapM (paramDecl (concatMap declared ds) hide pns) ds

138+

139+paramDecl :: [Name] -> -- Names defined in this block

140+ (Name -> Name) -> -- what to call the lifted functions

141+ [(Name, PTerm)] -> -- parameters to add

142+ PDecl -> Idris PDecl

143+paramDecl ns newname ps (PTy n ty)

144+ = do let ty' = piBind ps ty

145+ return (PTy (newname n) (addNs ns newname (map fst ps) ty'))

146+paramDecl ns newname ps (PClauses n cs)

147+ = do cs' <- mapM pclause cs

148+ return (PClauses n cs')

149+ where

150+ pclause (PClause n lhs rhs [])

151+ = return $ PClause n [] (addNs ns newname (map fst ps) lhs)

152+ (addNs ns newname (map fst ps) rhs)

153+paramDecl ns newname ps (PData (PDatadecl n ty cons))

154+ = do let ty' = piBind ps ty

155+ cons' <- mapM con cons

156+ return (PData (PDatadecl n ty' cons'))

157+ where

158+ con (n, ty) = do let ty' = piBind ps ty

159+ return (n, addNs ns newname (map fst ps) ty')

160+paramDecl ns newname ps d = return d

161+-}

110

162

111−elabDecl' (PFix _ _) = return () -- nothing to elaborate

163+addNs :: [Name] -> (Name -> Name) -> [Name] -> PTerm -> PTerm

112−elabDecl' (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n

164+addNs = undefined

113− elabType n ty

114−elabDecl' (PData d) = do iLOG $ "Elaborating " ++ show d

115− elabData d

116−elabDecl' d@(PClauses n ps) = do iLOG $ "Elaborating " ++ show n

117− elabClauses n ps

118

165

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

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

120-- elaborated, typechecked term.

167-- elaborated, typechecked term.

src/Idris/Parser.hs+6−4

@@ -70,7 +70,6 @@ pFullExpr syn

70pDecl :: SyntaxInfo -> IParser [PDecl]

71pDecl syn

72 = do d <- pDecl' syn

73− lchar ';'

74 i <- getState

73 i <- getState

75 return [fmap (addImpl i) d]

74 return [fmap (addImpl i) d]

76 <|> try (pUsing syn)

75 <|> try (pUsing syn)

@@ -78,7 +77,6 @@ pDecl syn

78pFunDecl :: SyntaxInfo -> IParser [PDecl]

77pFunDecl :: SyntaxInfo -> IParser [PDecl]

79pFunDecl syn

78pFunDecl syn

80 = try (do d <- pFunDecl' syn

79 = try (do d <- pFunDecl' syn

81− lchar ';'

82 i <- getState

80 i <- getState

83 return [fmap (addImpl i) d])

81 return [fmap (addImpl i) d])

@@ -92,6 +90,7 @@ pDecl' syn

93pFunDecl' :: SyntaxInfo -> IParser PDecl

91pFunDecl' :: SyntaxInfo -> IParser PDecl

94pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn

92pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn

93+ lchar ';'

95 ty' <- implicit syn n ty

94 ty' <- implicit syn n ty

96 return (PTy n ty'))

95 return (PTy n ty'))

97 <|> try (pPattern syn)

96 <|> try (pPattern syn)

@@ -112,6 +111,7 @@ pUsing syn =

112

111

113pFixity :: IParser PDecl

112pFixity :: IParser PDecl

114pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')

113pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')

114+ lchar ';'

115 let prec = fromInteger i

116 istate <- getState

117 let fs = map (Fix (f prec)) ops

@@ -228,10 +228,12 @@ pData syn = try (do reserved "data"; tyn <- pfName; ty <- pTSig syn

228 reserved "where"

229 ty' <- implicit syn tyn ty

230 cons <- sepBy1 (pConstructor syn) (lchar '|')

231+ lchar ';'

231 return $ PData (PDatadecl tyn ty' cons))

232 return $ PData (PDatadecl tyn ty' cons))

232 <|> do reserved "data"; tyn <- pfName; args <- many iName

233 <|> do reserved "data"; tyn <- pfName; args <- many iName

233 lchar '='

234 lchar '='

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

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

236+ lchar ';'

235 let conty = mkPApp (PRef tyn) (map PRef args)

237 let conty = mkPApp (PRef tyn) (map PRef args)

236 let ty = bindArgs (map (\a -> PSet) args) PSet

238 let ty = bindArgs (map (\a -> PSet) args) PSet

237 ty' <- implicit syn tyn ty

239 ty' <- implicit syn tyn ty

@@ -272,7 +274,7 @@ pClause syn

272 args <- many (pHSimpleExpr syn)

274 args <- many (pHSimpleExpr syn)

273 lchar '='

275 lchar '='

274 rhs <- pExpr syn

276 rhs <- pExpr syn

275− wheres <- option [] (pWhereblock syn)

277+ wheres <- choice [pWhereblock syn, do lchar ';'; return []]

276 return $ PClause n (PApp (PRef n) (iargs ++ map PExp args)) rhs wheres)

278 return $ PClause n (PApp (PRef n) (iargs ++ map PExp args)) rhs wheres)

277 <|> do l <- pSimpleExpr syn

279 <|> do l <- pSimpleExpr syn

278 op <- operator

280 op <- operator

@@ -280,7 +282,7 @@ pClause syn

280 r <- pSimpleExpr syn

282 r <- pSimpleExpr syn

281 lchar '='

283 lchar '='

282 rhs <- pExpr syn

284 rhs <- pExpr syn

283− wheres <- option [] (pWhereblock syn)

285+ wheres <- choice [pWhereblock syn, do lchar ';'; return []]

284 return $ PClause n (PApp (PRef n) [PExp l,PExp r]) rhs wheres

286 return $ PClause n (PApp (PRef n) [PExp l,PExp r]) rhs wheres

285

287

286pWhereblock :: SyntaxInfo -> IParser [PDecl]

288pWhereblock :: SyntaxInfo -> IParser [PDecl]

src/Idris/Primitives.hs+1−1

@@ -52,6 +52,6 @@ elabPrim :: Prim -> Idris ()

52elabPrim (Prim n ty i def) = updateContext (addOperator n ty i def)

54elabPrims :: Idris ()

55−elabPrims = do elabDecl (PData inferDecl)

55+elabPrims = do elabDecl toplevel (PData inferDecl)

56 mapM_ elabPrim primitives

src/Idris/REPL.hs+1−1

@@ -40,7 +40,7 @@ processInput cmd

40process :: Command -> Idris ()

41process Help

42 = iputStrLn "At some point I'll write some help text. Thanks for asking though."

43−process (Eval t) = do (tm, ty) <- elabVal t

43+process (Eval t) = do (tm, ty) <- elabVal toplevel t

44 ctxt <- getContext

45 ist <- get

46 let tm' = normalise ctxt [] tm

src/Main.hs+1−1

@@ -51,7 +51,7 @@ loadModule f = do iLOG ("Reading " ++ show f)

51 i <- get

52 iLOG (show (idris_infixes i))

53 -- Now add all the declarations to the context

54− mapM_ elabDecl ds

54+ mapM_ (elabDecl toplevel) ds

55 return ()

57dumpDecls :: [PDecl] -> String