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

git.iko.soy/Idris-dev

on master help sign in

Added using blocks

9fe3473Edwin Brady15 years ago

interp.mi+48−57

compare with master

unifiedsplit

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

20 VNil : Vect a O

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

23+using (G : Vect Ty n) {

24+

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

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

24− Empty : Env VNil

26+ Empty : Env VNil

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

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

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

27−

28+

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

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

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

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

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

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

31−

32+

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

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

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

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

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

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

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

36−

36+

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

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

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

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

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

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

41− Nat -> Expr G TyNat

39+ | Val : Nat -> Expr G TyNat

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

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

40+ | Lam : 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

41+ | App : 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

42+ | Add : 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;

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

50−

44+

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

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

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

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

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

54−interp env (Val x) = x;

47+ interp env (Val x) = x;

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

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

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

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

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

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

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

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

59−

52+

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

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

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

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

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

63−

55+

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

65− Expr G (TyFun TyNat TyNat);

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

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

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

67−

58+

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

69− Expr G (TyFun TyNat TyNat);

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

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

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

71−

61+

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

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

73−

63+

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

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

75−eProg = Lam (Lam

65+ eProg = Lam (Lam

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

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

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

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

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

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

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

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

70+}

81test : Nat;

72test : Nat;

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

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

src/Idris/AbsSyntax.hs+18−6

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

136 | PSet

137 | Placeholder

138

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

140+

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

142+ deriving Show

143+

144+defaultSyntax = Syn []

145+

139--- Pretty printing declarations and terms

146--- Pretty printing declarations and terms

140

147

141instance Show PTerm where

148instance Show PTerm where

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

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

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

249-- argument position.

256-- argument position.

250

257

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

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

252−implicitise ist tm

259+implicitise syn ist tm

260+ = let uvars = using syn

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

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

262+ if null ns

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

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

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

255 where

265 where

256 imps env (PApp f is es)

266 imps env (PApp f is es)

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

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

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

274 imps env (PHidden tm) = imps env tm

284 imps env (PHidden tm) = imps env tm

275 imps env _ = return ()

285 imps env _ = return ()

276

286

277− pibind [] sc = 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)

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

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

279

291

280addImpl :: IState -> PTerm -> PTerm

292addImpl :: IState -> PTerm -> PTerm

281addImpl ist ptm = ai [] ptm

293addImpl ist ptm = ai [] ptm

src/Idris/Parser.hs+113−95

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

34reservedOp= PTok.reservedOp lexer

35lchar = lexeme.char

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

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

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

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

40+parseProg syn fname

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

41+ = do file <- lift $ readFile fname

41 i <- get

42 i <- get

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

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

43 eof

44 eof

44 i' <- getState

45 i' <- getState

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

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

46 Left err -> fail (show err)

47 Left err -> fail (show err)

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

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

48 return (collect x)

49 return (collect x)

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

56collect (d : ds) = d : collect ds

57collect (d : ds) = d : collect ds

57collect [] = []

58collect [] = []

59−pFullExpr :: IParser PTerm

60+pFullExpr :: SyntaxInfo -> IParser PTerm

61+pFullExpr syn

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

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

61 i <- getState

63 i <- getState

62 return (addImpl i x)

64 return (addImpl i x)

64−pDecl :: IParser PDecl

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

67+pDecl syn

65−pDecl = do d <- pDecl'

68+ = do d <- pDecl' syn

66 lchar ';'

69 lchar ';'

67 i <- getState

70 i <- getState

68− return (fmap (addImpl i) d)

71+ return [fmap (addImpl i) d]

72+ <|> try (pUsing syn)

70--------- Top Level Declarations ---------

74--------- Top Level Declarations ---------

72−pDecl' :: IParser PDecl

76+pDecl' :: SyntaxInfo -> IParser PDecl

77+pDecl' syn

73−pDecl' = try pFixity

78+ = try pFixity

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

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

75− ty' <- implicit n ty

80+ ty' <- implicit syn n ty

76 return (PTy n ty'))

81 return (PTy n ty'))

77− <|> try pData

82+ <|> try (pData syn)

78− <|> try pPattern

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)

80--------- Fixity ---------

98--------- Fixity ---------

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

113

96--------- Expressions ---------

114--------- Expressions ---------

115

98−pExpr = do i <- getState

116+pExpr syn = do i <- getState

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

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

100

118

101−pExpr' :: IParser PTerm

119+pExpr' :: SyntaxInfo -> IParser PTerm

120+pExpr' syn

102−pExpr' = try pApp

121+ = try (pApp syn)

103− <|> pSimpleExpr

122+ <|> pSimpleExpr syn

104− <|> try pLambda

123+ <|> try (pLambda syn)

105− <|> try pPi

124+ <|> try (pPi syn)

106

125

107pfName = try iName

126pfName = try iName

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

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

109

128

110−pSimpleExpr =

129+pSimpleExpr syn =

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

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

112 return $ PQuote t)

131 return $ PQuote t)

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

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

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

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

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

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

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

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

117

136

137+pHSimpleExpr syn

118−pHSimpleExpr = try pSimpleExpr

138+ = try (pSimpleExpr syn)

119 <|> do lchar '.'

139 <|> do lchar '.'

120− e <- pSimpleExpr

140+ e <- pSimpleExpr syn

121 return $ PHidden e

141 return $ PHidden e

122

142

123−pApp = do f <- pSimpleExpr

143+pApp syn = do f <- pSimpleExpr syn

124− iargs <- many pImplicitArg

144+ iargs <- many (pImplicitArg syn)

125− args <- many1 pSimpleExpr

145+ args <- many1 (pSimpleExpr syn)

126− return (PApp f iargs args)

146+ return (PApp f iargs args)

127−

147+

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

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

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

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

130− lchar '}'

150+ lchar '}'

131− return (n, v)

151+ return (n, v)

132−

152+

133−pTSig = do lchar ':'

153+pTSig syn = do lchar ':'

134− pExpr

154+ pExpr syn

135−

155+

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

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

137− symbol "=>"

157+ symbol "=>"

138− sc <- pExpr

158+ sc <- pExpr syn

139− return (PLam x t sc)

159+ return (PLam x t sc)

140−

160+

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

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

142− symbol "->"

162+ symbol "->"

143− sc <- pExpr

163+ sc <- pExpr syn

144− return (PPi Exp x t sc)

164+ return (PPi Exp x t sc)

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

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

146− symbol "->"

166+ symbol "->"

147− sc <- pExpr

167+ sc <- pExpr syn

148− return (PPi Imp x t sc)

168+ return (PPi Imp x t sc)

149

169

150table fixes

170table fixes

151 = toTable (reverse fixes) ++

171 = toTable (reverse fixes) ++

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

164

184

165--------- Data declarations ---------

185--------- Data declarations ---------

166

186

167−pData :: IParser PDecl

187+pData :: SyntaxInfo -> IParser PDecl

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

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

169− reserved "where"

189+ reserved "where"

170− ty' <- implicit tyn ty

190+ ty' <- implicit syn tyn ty

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

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

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

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

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

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

174− lchar '='

194+ lchar '='

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

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

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

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

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

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

178− ty' <- implicit tyn ty

198+ ty' <- implicit syn tyn ty

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

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

180− cty' <- implicit x cty

200+ cty' <- implicit syn x cty

181− return (x, cty')) cons

201+ return (x, cty')) cons

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

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

183

203

184mkPApp t [] = t

204mkPApp t [] = t

185mkPApp t xs = PApp t [] xs

205mkPApp t xs = PApp t [] xs

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

188bindArgs [] t = t

208bindArgs [] t = t

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

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

190

210

191−pConstructor :: IParser (Name, PTerm)

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

192−pConstructor

212+pConstructor syn

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

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

194− ty' <- implicit cn ty

214+ ty' <- implicit syn cn ty

195 return (cn, ty')

215 return (cn, ty')

196

216

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

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

218+pSimpleCon syn

198−pSimpleCon = do cn <- pfName

219+ = do cn <- pfName

199− args <- many pSimpleExpr

220+ args <- many (pSimpleExpr syn)

200− return (cn, args)

221+ return (cn, args)

201

222

202--------- Pattern match clauses ---------

223--------- Pattern match clauses ---------

203

224

204−pPattern :: IParser PDecl

225+pPattern :: SyntaxInfo -> IParser PDecl

205−pPattern = do clause <- pClause

226+pPattern syn = do clause <- pClause syn

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

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

207

228

208−pClause :: IParser PClause

229+pClause :: SyntaxInfo -> IParser PClause

230+pClause syn

209−pClause = try (do n <- pfName

231+ = try (do n <- pfName

210− iargs <- many pImplicitArg

232+ iargs <- many (pImplicitArg syn)

211− args <- many pHSimpleExpr

233+ args <- many (pHSimpleExpr syn)

212 lchar '='

234 lchar '='

213− rhs <- pExpr

235+ rhs <- pExpr syn

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

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

215− <|> do l <- pSimpleExpr

237+ <|> do l <- pSimpleExpr syn

216 op <- operator

238 op <- operator

217 let n = UN [op]

239 let n = UN [op]

218− r <- pSimpleExpr

240+ r <- pSimpleExpr syn

219 lchar '='

241 lchar '='

220− rhs <- pExpr

242+ rhs <- pExpr syn

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

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

222

244

223-- Dealing with implicit arguments

245-- Dealing with implicit arguments

224

246

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

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

226−implicit n ptm

248+implicit syn n ptm

227 = do i <- getState

249 = do i <- getState

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

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

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

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

230 return tm'

252 return tm'

231

253

232−addImplicits :: PTerm -> IParser PTerm

233−addImplicits tm

234− = do i <- getState

235− return (addImpl i tm)

236

254

src/Idris/REPLParser.hs+1−1

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

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

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

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

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

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

26 <|> do eof; return NOP

src/Main.hs+1−1

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

45loadModule :: FilePath -> Idris ()

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

47− ds <- parseProg f

47+ ds <- parseProg defaultSyntax f

48 iLOG (dumpDecls ds)

49 i <- get

50 iLOG (show (idris_infixes i))