9fe3473 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added using blocks

commit9fe3473d2a28440311d86a40c69c90474d5b7b1c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 10 Oct 2011, 15:16 (15 years ago) parente613365

5 files changed+181−160

compare with master

unifiedsplit

interp.mi+48−57 src/Idris/AbsSyntax.hs+18−6 src/Idris/Parser.hs+113−95 src/Idris/REPLParser.hs+1−1 src/Main.hs+1−1

interp.mi+48−57

@@ -20,63 +20,54 @@ data Vect : Set -> Nat -> Set where

2020 VNil : Vect a O

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

2222

23−data Env : Vect Ty n -> Set where

24− Empty : Env VNil

25− | Extend : {xs : Vect Ty n} ->

26− interpTy a -> Env xs -> Env (a :: xs);

27−

28−lookup : (i : Fin n) -> Vect a n -> a;

29−lookup fO (x :: xs) = x;

30−lookup (fS k) (x :: xs) = lookup k xs;

31−

32−envLookup : {xs : Vect Ty n} ->

33− (i : Fin n) -> Env xs -> interpTy (lookup i xs);

34−envLookup fO (Extend x xs) = x;

35−envLookup (fS i) (Extend x xs) = envLookup i xs;

36−

37−data Expr : Vect Ty n -> Ty -> Set where

38− Var : {G : Vect Ty n} ->

39− (i : Fin n) -> Expr G (lookup i G)

40− | Val : {G : Vect Ty n} ->

41− Nat -> Expr G TyNat

42− | Lam : {G : Vect Ty n} ->

43− Expr (a :: G) t -> Expr G (TyFun a t)

44− | App : {G : Vect Ty n} ->

45− Expr G (TyFun a t) -> Expr G a -> Expr G t

46− | Add : {G : Vect Ty n} ->

47− Expr G TyNat -> Expr G TyNat -> Expr G TyNat

48− | Bind : {G : Vect Ty n} ->

49− Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

50−

51−interp : {G : Vect Ty n} ->

52− Env G -> Expr G t -> interpTy t;

53−interp env (Var i) = envLookup i env;

54−interp env (Val x) = x;

55−interp env (Lam sc) = \x => interp (Extend x env) sc;

56−interp env (App f s) = (interp env f) (interp env s);

57−interp env (Add x y) = plus (interp env x) (interp env y);

58−interp env (Bind v f) = interp env (f (interp env v));

59−

60−eAdd : {G : Vect Ty n} ->

61− Expr G (TyFun TyNat (TyFun TyNat TyNat));

62−eAdd = Lam (Lam (Add (Var fO) (Var (fS fO))));

63−

64−eDouble : {G : Vect Ty n} ->

65− Expr G (TyFun TyNat TyNat);

66−eDouble = Lam (App (App (Lam (Lam (Add (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));

67−

68−eDouble' : {G : Vect Ty n} ->

69− Expr G (TyFun TyNat TyNat);

70−eDouble' = Lam (App (App eAdd (Var fO)) (Var fO));

71−

72−-- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

73−

74−eProg : {G : Vect Ty n} -> Expr G (TyFun TyNat (TyFun TyNat TyNat));

75−eProg = Lam (Lam

76− (Bind (App eDouble (Var (fS fO)))

77− (\x => Bind (App eDouble (Var fO))

78− (\y => Bind (App eDouble (Val x))

79− (\z => App (App eAdd (Val y)) (Val z))))));

23+using (G : Vect Ty n) {

24+

25+ data Env : Vect Ty n -> Set where

26+ Empty : Env VNil

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

28+

29+ lookup : (i : Fin n) -> Vect a n -> a;

30+ lookup fO (x :: xs) = x;

31+ lookup (fS k) (x :: xs) = lookup k xs;

32+

33+ envLookup : (i : Fin n) -> Env G -> interpTy (lookup i G);

34+ envLookup fO (Extend x xs) = x;

35+ envLookup (fS i) (Extend x xs) = envLookup i xs;

36+

37+ data Expr : Vect Ty n -> Ty -> Set where

38+ Var : (i : Fin n) -> Expr G (lookup i G)

39+ | Val : Nat -> Expr G TyNat

40+ | Lam : Expr (a :: G) t -> Expr G (TyFun a t)

41+ | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

42+ | Add : Expr G TyNat -> Expr G TyNat -> Expr G TyNat

43+ | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

44+

45+ interp : Env G -> Expr G t -> interpTy t;

46+ interp env (Var i) = envLookup i env;

47+ interp env (Val x) = x;

48+ interp env (Lam sc) = \x => interp (Extend x env) sc;

49+ interp env (App f s) = (interp env f) (interp env s);

50+ interp env (Add x y) = plus (interp env x) (interp env y);

51+ interp env (Bind v f) = interp env (f (interp env v));

52+

53+ eAdd : Expr G (TyFun TyNat (TyFun TyNat TyNat));

54+ eAdd = Lam (Lam (Add (Var fO) (Var (fS fO))));

55+

56+ eDouble : Expr G (TyFun TyNat TyNat);

57+ eDouble = Lam (App (App (Lam (Lam (Add (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));

58+

59+ eDouble' : Expr G (TyFun TyNat TyNat);

60+ eDouble' = Lam (App (App eAdd (Var fO)) (Var fO));

61+

62+ -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

63+

64+ eProg : Expr G (TyFun TyNat (TyFun TyNat TyNat));

65+ eProg = Lam (Lam

66+ (Bind (App eDouble (Var (fS fO)))

67+ (\x => Bind (App eDouble (Var fO))

68+ (\y => Bind (App eDouble (Val x))

69+ (\z => App (App eAdd (Val y)) (Val z))))));

70+}

8071

8172test : Nat;

8273test = interp Empty eAdd (S (S O)) (S (S O));

src/Idris/AbsSyntax.hs+18−6

@@ -136,6 +136,13 @@ data PTerm = PQuote Raw

136136 | PSet

137137 | Placeholder

138138

139+-- Syntactic sugar info (TODO: namespaces, parameters, modules)

140+

141+data SyntaxInfo = Syn { using :: [(Name, PTerm)] }

142+ deriving Show

143+

144+defaultSyntax = Syn []

145+

139146--- Pretty printing declarations and terms

140147

141148instance Show PTerm where

@@ -248,10 +255,13 @@ getInferType (App (App _ ty) _) = ty

248255-- Add implicit Pi bindings for any names in the term which appear in an

249256-- argument position.

250257

251−implicitise :: IState -> PTerm -> (PTerm, ([Name], Int))

252−implicitise ist tm

253− = let (declimps, a, ns) = execState (imps [] tm) ([], 0, []) in

254− (pibind ns tm, (ns ++ reverse declimps, a))

258+implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, ([Name], Int))

259+implicitise syn ist tm

260+ = let uvars = using syn

261+ (declimps, a, ns) = execState (imps [] tm) ([], 0, []) in

262+ if null ns

263+ then (tm, (reverse declimps, a))

264+ else implicitise syn ist (pibind uvars ns tm)

255265 where

256266 imps env (PApp f is es)

257267 = do (decls, a, ns) <- get

@@ -274,8 +284,10 @@ implicitise ist tm

274284 imps env (PHidden tm) = imps env tm

275285 imps env _ = return ()

276286

277− pibind [] sc = sc

278− pibind (n:ns) sc = PPi Imp n Placeholder (pibind ns sc)

287+ pibind using [] sc = sc

288+ pibind using (n:ns) sc = case lookup n using of

289+ Just ty -> PPi Imp n ty (pibind using ns sc)

290+ Nothing -> PPi Imp n Placeholder (pibind using ns sc)

279291

280292addImpl :: IState -> PTerm -> PTerm

281293addImpl ist ptm = ai [] ptm

src/Idris/Parser.hs+113−95

@@ -34,15 +34,16 @@ operator = PTok.operator lexer

3434reservedOp= PTok.reservedOp lexer

3535lchar = lexeme.char

3636

37−parseExpr i = runParser pFullExpr i "(input)"

37+parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"

3838

39−parseProg :: String -> Idris [PDecl]

40−parseProg fname = do file <- lift $ readFile fname

39+parseProg :: SyntaxInfo -> String -> Idris [PDecl]

40+parseProg syn fname

41+ = do file <- lift $ readFile fname

4142 i <- get

42− case (runParser (do ps <- many1 pDecl

43+ case (runParser (do ps <- many1 (pDecl syn)

4344 eof

4445 i' <- getState

45− return (ps, i')) i fname file) of

46+ return (concat ps, i')) i fname file) of

4647 Left err -> fail (show err)

4748 Right (x, i) -> do put i

4849 return (collect x)

@@ -56,26 +57,43 @@ collect (PClauses _ [c@(PClause n l r)] : ds) = clauses n [c] ds

5657collect (d : ds) = d : collect ds

5758collect [] = []

5859

59−pFullExpr :: IParser PTerm

60−pFullExpr = do x <- pExpr; eof;

60+pFullExpr :: SyntaxInfo -> IParser PTerm

61+pFullExpr syn

62+ = do x <- pExpr syn; eof;

6163 i <- getState

6264 return (addImpl i x)

6365

64−pDecl :: IParser PDecl

65−pDecl = do d <- pDecl'

66+pDecl :: SyntaxInfo -> IParser [PDecl]

67+pDecl syn

68+ = do d <- pDecl' syn

6669 lchar ';'

6770 i <- getState

68− return (fmap (addImpl i) d)

71+ return [fmap (addImpl i) d]

72+ <|> try (pUsing syn)

6973

7074--------- Top Level Declarations ---------

7175

72−pDecl' :: IParser PDecl

73−pDecl' = try pFixity

74− <|> try (do n <- pfName; ty <- pTSig

75− ty' <- implicit n ty

76+pDecl' :: SyntaxInfo -> IParser PDecl

77+pDecl' syn

78+ = try pFixity

79+ <|> try (do n <- pfName; ty <- pTSig syn

80+ ty' <- implicit syn n ty

7681 return (PTy n ty'))

77− <|> try pData

78− <|> try pPattern

82+ <|> try (pData syn)

83+ <|> try (pPattern syn)

84+

85+pUsing :: SyntaxInfo -> IParser [PDecl]

86+pUsing syn =

87+ do reserved "using";

88+ lchar '('

89+ ns <- sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))

90+ (lchar ',')

91+ lchar ')'

92+ lchar '{'

93+ let uvars = using syn

94+ ds <- many1 (pDecl (syn { using = uvars ++ ns }))

95+ lchar '}'

96+ return (concat ds)

7997

8098--------- Fixity ---------

8199

@@ -95,57 +113,59 @@ fixity = try (do reserved "infixl"; return Infixl)

95113

96114--------- Expressions ---------

97115

98−pExpr = do i <- getState

99− buildExpressionParser (table (idris_infixes i)) pExpr'

116+pExpr syn = do i <- getState

117+ buildExpressionParser (table (idris_infixes i)) (pExpr' syn)

100118

101−pExpr' :: IParser PTerm

102−pExpr' = try pApp

103− <|> pSimpleExpr

104− <|> try pLambda

105− <|> try pPi

119+pExpr' :: SyntaxInfo -> IParser PTerm

120+pExpr' syn

121+ = try (pApp syn)

122+ <|> pSimpleExpr syn

123+ <|> try (pLambda syn)

124+ <|> try (pPi syn)

106125

107126pfName = try iName

108127 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])

109128

110−pSimpleExpr =

129+pSimpleExpr syn =

111130 try (do symbol "!["; t <- pTerm; lchar ']'

112131 return $ PQuote t)

113132 <|> try (do x <- pfName; return (PRef x))

114133 <|> try (do lchar '_'; return Placeholder)

115− <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)

134+ <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

116135 <|> try (do reserved "Set"; return PSet)

117136

118−pHSimpleExpr = try pSimpleExpr

137+pHSimpleExpr syn

138+ = try (pSimpleExpr syn)

119139 <|> do lchar '.'

120− e <- pSimpleExpr

140+ e <- pSimpleExpr syn

121141 return $ PHidden e

122142

123−pApp = do f <- pSimpleExpr

124− iargs <- many pImplicitArg

125− args <- many1 pSimpleExpr

126− return (PApp f iargs args)

127−

128−pImplicitArg = do lchar '{'; n <- iName

129− v <- option (PRef n) (do lchar '='; pExpr)

130− lchar '}'

131− return (n, v)

132−

133−pTSig = do lchar ':'

134− pExpr

135−

136−pLambda = do lchar '\\'; x <- iName; t <- option Placeholder pTSig

137− symbol "=>"

138− sc <- pExpr

139− return (PLam x t sc)

140−

141−pPi = do lchar '('; x <- iName; t <- pTSig; lchar ')'

142− symbol "->"

143− sc <- pExpr

144− return (PPi Exp x t sc)

145− <|> do lchar '{'; x <- iName; t <- pTSig; lchar '}'

146− symbol "->"

147− sc <- pExpr

148− return (PPi Imp x t sc)

143+pApp syn = do f <- pSimpleExpr syn

144+ iargs <- many (pImplicitArg syn)

145+ args <- many1 (pSimpleExpr syn)

146+ return (PApp f iargs args)

147+

148+pImplicitArg syn = do lchar '{'; n <- iName

149+ v <- option (PRef n) (do lchar '='; pExpr syn)

150+ lchar '}'

151+ return (n, v)

152+

153+pTSig syn = do lchar ':'

154+ pExpr syn

155+

156+pLambda syn = do lchar '\\'; x <- iName; t <- option Placeholder (pTSig syn)

157+ symbol "=>"

158+ sc <- pExpr syn

159+ return (PLam x t sc)

160+

161+pPi syn = do lchar '('; x <- iName; t <- pTSig syn; lchar ')'

162+ symbol "->"

163+ sc <- pExpr syn

164+ return (PPi Exp x t sc)

165+ <|> do lchar '{'; x <- iName; t <- pTSig syn; lchar '}'

166+ symbol "->"

167+ sc <- pExpr syn

168+ return (PPi Imp x t sc)

149169

150170table fixes

151171 = toTable (reverse fixes) ++

@@ -164,22 +184,22 @@ binary name f assoc = Infix (do { reservedOp name; return f }) assoc

164184

165185--------- Data declarations ---------

166186

167−pData :: IParser PDecl

168−pData = try (do reserved "data"; tyn <- pfName; ty <- pTSig

169− reserved "where"

170− ty' <- implicit tyn ty

171− cons <- sepBy1 pConstructor (lchar '|')

172− return $ PData (PDatadecl tyn ty' cons))

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

174− lchar '='

175− cons <- sepBy1 pSimpleCon (lchar '|')

176− let conty = mkPApp (PRef tyn) (map PRef args)

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

178− ty' <- implicit tyn ty

179− cons' <- mapM (\ (x, cargs) -> do let cty = bindArgs cargs conty

180− cty' <- implicit x cty

181− return (x, cty')) cons

182− return $ PData (PDatadecl tyn ty' cons')

187+pData :: SyntaxInfo -> IParser PDecl

188+pData syn = try (do reserved "data"; tyn <- pfName; ty <- pTSig syn

189+ reserved "where"

190+ ty' <- implicit syn tyn ty

191+ cons <- sepBy1 (pConstructor syn) (lchar '|')

192+ return $ PData (PDatadecl tyn ty' cons))

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

194+ lchar '='

195+ cons <- sepBy1 (pSimpleCon syn) (lchar '|')

196+ let conty = mkPApp (PRef tyn) (map PRef args)

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

198+ ty' <- implicit syn tyn ty

199+ cons' <- mapM (\ (x, cargs) -> do let cty = bindArgs cargs conty

200+ cty' <- implicit syn x cty

201+ return (x, cty')) cons

202+ return $ PData (PDatadecl tyn ty' cons')

183203

184204mkPApp t [] = t

185205mkPApp t xs = PApp t [] xs

@@ -188,49 +208,47 @@ bindArgs :: [PTerm] -> PTerm -> PTerm

188208bindArgs [] t = t

189209bindArgs (x:xs) t = PPi Exp (MN 0 "t") x (bindArgs xs t)

190210

191−pConstructor :: IParser (Name, PTerm)

192−pConstructor

193− = do cn <- pfName; ty <- pTSig

194− ty' <- implicit cn ty

211+pConstructor :: SyntaxInfo -> IParser (Name, PTerm)

212+pConstructor syn

213+ = do cn <- pfName; ty <- pTSig syn

214+ ty' <- implicit syn cn ty

195215 return (cn, ty')

196216

197−pSimpleCon :: IParser (Name, [PTerm])

198−pSimpleCon = do cn <- pfName

199− args <- many pSimpleExpr

200− return (cn, args)

217+pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm])

218+pSimpleCon syn

219+ = do cn <- pfName

220+ args <- many (pSimpleExpr syn)

221+ return (cn, args)

201222

202223--------- Pattern match clauses ---------

203224

204−pPattern :: IParser PDecl

205−pPattern = do clause <- pClause

206− return (PClauses (MN 0 "_") [clause]) -- collect together later

225+pPattern :: SyntaxInfo -> IParser PDecl

226+pPattern syn = do clause <- pClause syn

227+ return (PClauses (MN 0 "_") [clause]) -- collect together later

207228

208−pClause :: IParser PClause

209−pClause = try (do n <- pfName

210− iargs <- many pImplicitArg

211− args <- many pHSimpleExpr

229+pClause :: SyntaxInfo -> IParser PClause

230+pClause syn

231+ = try (do n <- pfName

232+ iargs <- many (pImplicitArg syn)

233+ args <- many (pHSimpleExpr syn)

212234 lchar '='

213− rhs <- pExpr

235+ rhs <- pExpr syn

214236 return $ PClause n (PApp (PRef n) iargs args) rhs)

215− <|> do l <- pSimpleExpr

237+ <|> do l <- pSimpleExpr syn

216238 op <- operator

217239 let n = UN [op]

218− r <- pSimpleExpr

240+ r <- pSimpleExpr syn

219241 lchar '='

220− rhs <- pExpr

242+ rhs <- pExpr syn

221243 return $ PClause n (PApp (PRef n) [] [l,r]) rhs

222244

223245-- Dealing with implicit arguments

224246

225−implicit :: Name -> PTerm -> IParser PTerm

226−implicit n ptm

247+implicit :: SyntaxInfo -> Name -> PTerm -> IParser PTerm

248+implicit syn n ptm

227249 = do i <- getState

228− let (tm', name_arity) = implicitise i ptm

250+ let (tm', name_arity) = implicitise syn i ptm

229251 setState (i { idris_implicits = addDef n name_arity (idris_implicits i) })

230252 return tm'

231253

232−addImplicits :: PTerm -> IParser PTerm

233−addImplicits tm

234− = do i <- getState

235− return (addImpl i tm)

236254

src/Idris/REPLParser.hs+1−1

@@ -22,5 +22,5 @@ pCmd :: IParser Command

2222pCmd = try (do cmd ["q", "quit"]; return Quit)

2323 <|> try (do cmd ["h", "?", "help"]; return Help)

2424 <|> try (do cmd ["ttshell"]; return TTShell)

25− <|> do t <- pFullExpr; return (Eval t)

25+ <|> do t <- pFullExpr defaultSyntax; return (Eval t)

2626 <|> do eof; return NOP

src/Main.hs+1−1

@@ -44,7 +44,7 @@ runIdris opts =

4444

4545loadModule :: FilePath -> Idris ()

4646loadModule f = do iLOG ("Reading " ++ show f)

47− ds <- parseProg f

47+ ds <- parseProg defaultSyntax f

4848 iLOG (dumpDecls ds)

4949 i <- get

5050 iLOG (show (idris_infixes i))