de89a04 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add ElabInfo to pass through elaborator

commitde89a04fd328e1d635734f64976af8a0e8627336 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 12 Oct 2011, 18:28 (15 years ago) parenta2a5141

8 files changed+103−37

compare with master

unifiedsplit

impl-paper/literature.bib+3−2 impl-paper/overview.tex+3−1 src/Idris/AbsSyntax.hs+14 src/Idris/ElabDecls.hs+74−27 src/Idris/Parser.hs+6−4 src/Idris/Primitives.hs+1−1 src/Idris/REPL.hs+1−1 src/Main.hs+1−1

impl-paper/literature.bib+3−2

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

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

5353}

5454

55−@inproceedings{epicdraft,

55+@inproceedings{epic-tfp,

5656 author = {Edwin Brady},

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

5858 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}

6061}

6162

6263@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:

2424 report an error.

2525\end{itemize}

2626\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}.

2830\end{itemize}

2931

3032For 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

3737getContext :: Idris Context

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

3939

40+getIState :: Idris IState

41+getIState = get

42+

4043setContext :: Context -> Idris ()

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

4245

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

115118type PData = PData' PTerm

116119type PClause = PClause' PTerm

117120

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+

118129-- High level language terms

119130--

120131data PTerm = PQuote Raw

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

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

262273getInferType (App (App _ ty) _) = ty

263274

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

276+piBind [] t = t

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

264278

265279-- Dealing with implicit arguments

266280

src/Idris/ElabDecls.hs+74−27

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

55import Idris.AbsSyntax

66import Idris.Error

7+import Idris.Delaborate

89import Core.TT

910import Core.Elaborate

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

1415import Control.Monad

1516import Debug.Trace

1617

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

18−elabType n ty

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+

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

27+elabType info n ty

1928 = do ctxt <- getContext

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

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

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

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

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

2534

26−elabData :: PData -> Idris ()

27−elabData (PDatadecl n t dcons)

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

36+elabData info (PDatadecl n t dcons)

2837 = do ctxt <- getContext

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

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

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

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

33− cons <- mapM elabCon dcons

42+ cons <- mapM (elabCon info) dcons

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

3544

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

37−elabCon (n, t)

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

46+elabCon info (n, t)

3847 = do ctxt <- getContext

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

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

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

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

4453 return (n, cty)

4554

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

47−elabClauses n cs

48− = do pats <- mapM elabClause cs

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

56+elabClauses info n cs

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

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

5059 show l ++ " = " ++

5160 show r) pats))

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

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

6170 depat x = x

6271

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

64−elabVal tm

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

73+elabVal info tm

6574 = do ctxt <- getContext

6675 logLvl 10 (show tm)

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

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

7180 iLOG (show vtm)

7281 tclift $ recheck ctxt [] vtm

7382

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

75−elabClause (PClause _ lhs rhs whereblock)

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

84+elabClause info (PClause _ lhs rhs whereblock)

7685 = do ctxt <- getContext

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

7887 -- pattern bindings

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

8392 logLvl 3 (show lhs_tm)

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

8594 -- TODO: elaborate where block here.

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

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

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

89− -- elaborating.

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

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

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

98+ -- which are elaborated).

99+

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

91101 iLOG (showImp True rhs)

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

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

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

106116 psolve tm = return ()

107117

108−elabDecl :: PDecl -> Idris ()

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

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

119+ pvars _ = []

120+

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

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+-}

110162

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

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

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

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

164+addNs = undefined

118165

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

120167-- elaborated, typechecked term.

src/Idris/Parser.hs+6−4

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

7070pDecl :: SyntaxInfo -> IParser [PDecl]

7171pDecl syn

7272 = do d <- pDecl' syn

73− lchar ';'

7473 i <- getState

7574 return [fmap (addImpl i) d]

7675 <|> try (pUsing syn)

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

7877pFunDecl :: SyntaxInfo -> IParser [PDecl]

7978pFunDecl syn

8079 = try (do d <- pFunDecl' syn

81− lchar ';'

8280 i <- getState

8381 return [fmap (addImpl i) d])

8482

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

9290

9391pFunDecl' :: SyntaxInfo -> IParser PDecl

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

93+ lchar ';'

9594 ty' <- implicit syn n ty

9695 return (PTy n ty'))

9796 <|> try (pPattern syn)

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

112111

113112pFixity :: IParser PDecl

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

114+ lchar ';'

115115 let prec = fromInteger i

116116 istate <- getState

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

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

228228 reserved "where"

229229 ty' <- implicit syn tyn ty

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

231+ lchar ';'

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

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

233234 lchar '='

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

236+ lchar ';'

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

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

237239 ty' <- implicit syn tyn ty

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

272274 args <- many (pHSimpleExpr syn)

273275 lchar '='

274276 rhs <- pExpr syn

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

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

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

277279 <|> do l <- pSimpleExpr syn

278280 op <- operator

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

280282 r <- pSimpleExpr syn

281283 lchar '='

282284 rhs <- pExpr syn

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

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

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

285287

286288pWhereblock :: SyntaxInfo -> IParser [PDecl]

src/Idris/Primitives.hs+1−1

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

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

5353

5454elabPrims :: Idris ()

55−elabPrims = do elabDecl (PData inferDecl)

55+elabPrims = do elabDecl toplevel (PData inferDecl)

5656 mapM_ elabPrim primitives

5757

src/Idris/REPL.hs+1−1

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

4040process :: Command -> Idris ()

4141process Help

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

4444 ctxt <- getContext

4545 ist <- get

4646 let tm' = normalise ctxt [] tm

src/Main.hs+1−1

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

5151 i <- get

5252 iLOG (show (idris_infixes i))

5353 -- Now add all the declarations to the context

54− mapM_ elabDecl ds

54+ mapM_ (elabDecl toplevel) ds

5555 return ()

5656

5757dumpDecls :: [PDecl] -> String