083fc70 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added 'where' clauses in pattern matches

083fc70Edwin Brady15 years ago

prims.mi+1−1

compare with master

unifiedsplit

@@ -10,7 +10,7 @@ intToBool : Int -> Bool;

10intToBool 0 = False;

11intToBool x = True;

13−boolOp : {a:Set} -> (a -> a -> Int) -> a -> a -> Bool;

13+boolOp : (a -> a -> Int) -> a -> a -> Bool;

14boolOp op x y = intToBool (op x y);

16(+) : Int -> Int -> Int;

src/Core/TT.hs+4

@@ -96,6 +96,10 @@ lookupCtxt = Map.lookup

96toAlist :: Ctxt a -> [(Name, a)]

97toAlist = Map.toList

99+addAlist :: [(Name, a)] -> Ctxt a -> Ctxt a

100+addAlist [] ctxt = ctxt

101+addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

102+

99data Const = I Int | Fl Double | Ch Char | Str String

103data Const = I Int | Fl Double | Ch Char | Str String

101 deriving Eq

105 deriving Eq

src/Idris/AbsSyntax.hs+17−5

@@ -25,10 +25,11 @@ data IState = IState { tt_ctxt :: Context,

25 idris_infixes :: [FixDecl],

26 idris_implicits :: Ctxt [PArg],

27 idris_log :: String,

28− idris_options :: IOption

28+ idris_options :: IOption,

29+ idris_name :: Int

29 }

30 }

31−idrisInit = IState emptyContext [] emptyContext "" defaultOpts

32+idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0

33-- The monad for the main REPL - reading and processing files and updating

34-- The monad for the main REPL - reading and processing files and updating

34-- global state (hence the IO inner monad).

35-- global state (hence the IO inner monad).

@@ -40,6 +41,12 @@ getContext = do i <- get; return (tt_ctxt i)

40getIState :: Idris IState

41getIState :: Idris IState

41getIState = get

42getIState = get

44+getName :: Idris Int

45+getName = do i <- get;

46+ let idx = idris_name i;

47+ put (i { idris_name = idx + 1 })

48+ return idx

49+

43setContext :: Context -> Idris ()

50setContext :: Context -> Idris ()

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

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

@@ -101,6 +108,7 @@ data PDecl' t = PFix Fixity [String] -- fixity declaration

101 | PTy Name t -- type declaration

108 | PTy Name t -- type declaration

102 | PClauses Name [PClause' t] -- pattern clause

109 | PClauses Name [PClause' t] -- pattern clause

103 | PData (PData' t) -- data declaration

110 | PData (PData' t) -- data declaration

111+ | PParams [(Name, PTerm)] [PDecl' t] -- params block

104 deriving Functor

112 deriving Functor

105

113

106data PClause' t = PClause Name t t [PDecl]

114data PClause' t = PClause Name t t [PDecl]

@@ -125,6 +133,7 @@ declared (PFix _ _) = []

125declared (PTy n t) = [n]

133declared (PTy n t) = [n]

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

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

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

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

136+declared (PParams _ ds) = concatMap declared ds

128

137

129-- High level language terms

138-- High level language terms

130--

139--

@@ -147,10 +156,11 @@ type PArg = PArg' PTerm

147

156

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

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

149

158

150−data SyntaxInfo = Syn { using :: [(Name, PTerm)] }

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

160+ syn_params :: [(Name, PTerm)] }

151 deriving Show

161 deriving Show

152

162

153−defaultSyntax = Syn []

163+defaultSyntax = Syn [] []

154

164

155--- Pretty printing declarations and terms

165--- Pretty printing declarations and terms

156

166

@@ -284,7 +294,9 @@ piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)

284implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])

294implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])

285implicitise syn ist tm

295implicitise syn ist tm

286 = let uvars = using syn

296 = let uvars = using syn

297+ pvars = syn_params syn

287− (declimps, ns) = execState (imps True [] tm) ([], []) in

298+ (declimps, ns') = execState (imps True [] tm) ([], [])

299+ ns = ns' \\ map fst pvars in

288 if null ns

300 if null ns

289 then (tm, reverse declimps)

301 then (tm, reverse declimps)

290 else implicitise syn ist (pibind uvars ns tm)

302 else implicitise syn ist (pibind uvars ns tm)

src/Idris/ElabDecls.hs+69−35

@@ -19,15 +19,17 @@ import Debug.Trace

19-- paramaterised declarations, etc.

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

22+ inblock :: Ctxt [Name], -- names in the block, and their params

22 liftname :: Name -> Name }

23 liftname :: Name -> Name }

24−toplevel = EInfo [] id

25+toplevel = EInfo [] emptyContext id

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

27elabType :: ElabInfo -> Name -> PTerm -> Idris ()

27−elabType info n ty

28+elabType info n_in ty_in = let ty = piBind (params info) ty_in

29+ n = liftname info n_in in

28− = do ctxt <- getContext

30+ do ctxt <- getContext

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

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

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

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

31 (cty, _) <- tclift $ recheck ctxt [] ty'

33 (cty, _) <- tclift $ recheck ctxt [] ty'

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

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

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

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

@@ -35,7 +37,7 @@ elabType info n ty

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

37elabData :: ElabInfo -> PData -> Idris ()

36elabData info (PDatadecl n t dcons)

38elabData info (PDatadecl n t dcons)

37 = do ctxt <- getContext

39 = do ctxt <- getContext

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

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

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

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

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

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

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

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

@@ -46,15 +48,15 @@ elabCon :: ElabInfo -> (Name, PTerm) -> Idris (Name, Type)

46elabCon info (n, t)

48elabCon info (n, t)

47 = do ctxt <- getContext

49 = do ctxt <- getContext

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

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

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

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

50-- iLOG $ "Rechecking " ++ show t'

52-- iLOG $ "Rechecking " ++ show t'

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

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

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

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

53 return (n, cty)

55 return (n, cty)

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

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

56−elabClauses info n cs

58+elabClauses info n_in cs = let n = liftname info n_in in

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

59+ do pats <- mapM (elabClause info) cs

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

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

59 show l ++ " = " ++

61 show l ++ " = " ++

60 show r) pats))

62 show r) pats))

@@ -74,34 +76,34 @@ elabVal info tm

74 = do ctxt <- getContext

76 = do ctxt <- getContext

75 logLvl 10 (show tm)

77 logLvl 10 (show tm)

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

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

77− (build True (infTerm tm))

79+ (build info True (infTerm tm))

78 logLvl 3 ("Value: " ++ show tm')

80 logLvl 3 ("Value: " ++ show tm')

79 let vtm = getInferTerm tm'

81 let vtm = getInferTerm tm'

80 iLOG (show vtm)

82 iLOG (show vtm)

81 tclift $ recheck ctxt [] vtm

83 tclift $ recheck ctxt [] vtm

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

85elabClause :: ElabInfo -> PClause -> Idris (Term, Term)

84−elabClause info (PClause _ lhs rhs whereblock)

86+elabClause info (PClause fname lhs rhs whereblock)

85 = do ctxt <- getContext

87 = do ctxt <- getContext

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

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

87 -- pattern bindings

89 -- pattern bindings

88 (lhs', _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

90 (lhs', _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

89− (build True (infTerm lhs))

91+ (build info True (infTerm lhs))

90 let lhs_tm = getInferTerm lhs'

92 let lhs_tm = getInferTerm lhs'

91 let lhs_ty = getInferType lhs'

93 let lhs_ty = getInferType lhs'

92 logLvl 3 (show lhs_tm)

94 logLvl 3 (show lhs_tm)

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

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

94− -- TODO: elaborate where block here.

96+ -- Elaborate where block

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

97+ ist <- getIState

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

98+ windex <- getName

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

99+ let winfo = pinfo (pvars ist lhs_tm) whereblock windex

98− -- which are elaborated).

100+ mapM_ (elabDecl' winfo) whereblock

99−

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

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

101 iLOG (showImp True rhs)

102 iLOG (showImp True rhs)

103+ ctxt <- getContext -- new context with where block added

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

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

103 (do pbinds lhs_tm

105 (do pbinds lhs_tm

104− build False rhs

106+ build winfo False rhs

105 psolve lhs_tm

107 psolve lhs_tm

106 get_term)

108 get_term)

107 logLvl 2 $ "---> " ++ show rhs'

109 logLvl 2 $ "---> " ++ show rhs'

@@ -115,8 +117,21 @@ elabClause info (PClause _ lhs rhs whereblock)

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

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

116 psolve tm = return ()

118 psolve tm = return ()

117

119

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

120+ pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc

119− pvars _ = []

121+ pvars ist _ = []

122+

123+ pinfo ns ps i

124+ = let ds = concatMap declared ps

125+ newps = params info ++ ns

126+ dsParams = map (\n -> (n, map fst newps)) ds

127+ newb = addAlist dsParams (inblock info)

128+ l = liftname info in

129+ info { params = newps,

130+ inblock = newb,

131+ liftname = (\n -> case lookupCtxt n newb of

132+ Nothing -> n

133+ _ -> MN i (show n)) . l

134+ }

120

135

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

136elabDecl :: ElabInfo -> PDecl -> Idris ()

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

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

@@ -126,8 +141,17 @@ elabDecl' info (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n

126 elabType info n ty

141 elabType info n ty

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

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

128 elabData info d

143 elabData info d

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

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

130 elabClauses info n ps

145 elabClauses info n ps

146+elabDecl' info (PParams ns ps) = do iLOG $ "Params block " ++ show ns

147+ mapM_ (elabDecl' pinfo) ps

148+ where

149+ pinfo = let ds = concatMap declared ps

150+ newps = params info ++ ns

151+ dsParams = map (\n -> (n, map fst newps)) ds

152+ newb = addAlist dsParams (inblock info) in

153+ info { params = newps,

154+ inblock = newb }

131

155

132{- not finished...

156{- not finished...

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

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

@@ -169,14 +193,14 @@ addNs = undefined

169-- If building a pattern match, we convert undeclared variables from

193-- If building a pattern match, we convert undeclared variables from

170-- holes to pattern bindings.

194-- holes to pattern bindings.

171

195

172−build :: Bool -> PTerm -> Elab Term

196+build :: ElabInfo -> Bool -> PTerm -> Elab Term

173−build pattern tm = do elab pattern tm

197+build info pattern tm = do elab info pattern tm

174− get_term

198+ get_term

175

199

176−elab :: Bool -> PTerm -> Elab ()

200+elab :: ElabInfo -> Bool -> PTerm -> Elab ()

177−elab pattern tm = do elab' tm

201+elab info pattern tm = do elab' tm

178− when pattern -- convert remaining holes to pattern vars

202+ when pattern -- convert remaining holes to pattern vars

179− mkPat

203+ mkPat

180 where

204 where

181 isph arg = case getTm arg of

205 isph arg = case getTm arg of

182 Placeholder -> True

206 Placeholder -> True

@@ -194,10 +218,16 @@ elab pattern tm = do elab' tm

194 elab' PSet = do fill (RSet 0); solve

218 elab' PSet = do fill (RSet 0); solve

195 elab' (PConstant c) = do fill (RConstant c); solve

219 elab' (PConstant c) = do fill (RConstant c); solve

196 elab' (PQuote r) = do fill r; solve

220 elab' (PQuote r) = do fill r; solve

197− elab' (PRef n) | pattern

221+ elab' (PRef n) | pattern && not (inparamBlock n)

198 = try (do apply (Var n) []; solve)

222 = try (do apply (Var n) []; solve)

199 (patvar n)

223 (patvar n)

224+ where inparamBlock n = case lookupCtxt n (inblock info) of

225+ Nothing -> False

226+ _ -> True

227+ elab' (PRef n)

228+ | Just ps <- lookupCtxt n (inblock info)

229+ = elab' (PApp (PRef n) [])

200− elab' (PRef n) = do apply (Var n) []; solve

230+ | otherwise = do apply (Var n) []; solve

201 elab' (PLam n Placeholder sc)

231 elab' (PLam n Placeholder sc)

202 = do attack; intro n; elab' sc; solve

232 = do attack; intro n; elab' sc; solve

203 elab' (PPi _ n Placeholder sc)

233 elab' (PPi _ n Placeholder sc)

@@ -211,11 +241,15 @@ elab pattern tm = do elab' tm

211 elab' sc

241 elab' sc

212 solve

242 solve

213 elab' (PApp (PRef f) args)

243 elab' (PApp (PRef f) args)

244+ | Just ps <- lookupCtxt f (inblock info)

245+ = elabApp (liftname info f) (map (PExp . PRef) ps ++ args)

246+ | otherwise = elabApp f args

247+ where elabApp f args

214− = try (do ns <- apply (Var f) (map isph args)

248+ = try (do ns <- apply (Var f) (map isph args)

215− solve

249+ solve

216− elabArgs ns (map getTm args))

250+ elabArgs ns (map getTm args))

217− (do apply_elab f (map toElab args)

251+ (do apply_elab f (map toElab args)

218− solve)

252+ solve)

219 elab' (PApp f [arg])

253 elab' (PApp f [arg])

220 = do simple_app (elab' f) (elab' (getTm arg))

254 = do simple_app (elab' f) (elab' (getTm arg))

221 solve

255 solve

src/Idris/Parser.hs+15−1

@@ -54,10 +54,11 @@ parseProg syn fname

55-- Collect PClauses with the same function name

56collect :: [PDecl] -> [PDecl]

57−collect (PClauses _ [c@(PClause n l r w)] : ds) = clauses n [c] ds

57+collect (c@(PClauses _ [PClause n l r w]) : ds) = clauses n [] (c:ds)

58 where clauses n acc (PClauses _ [PClause n' l r w] : ds)

59 | n == n' = clauses n (PClause n' l r (collect w) : acc) ds

60 clauses n acc xs = PClauses n (reverse acc) : collect xs

61+collect (PParams ns ps : ds) = PParams ns (collect ps) : (collect ds)

61collect (d : ds) = d : collect ds

62collect (d : ds) = d : collect ds

62collect [] = []

63collect [] = []

@@ -73,6 +74,7 @@ pDecl syn

73 i <- getState

74 i <- getState

74 return [fmap (addImpl i) d]

75 return [fmap (addImpl i) d]

75 <|> try (pUsing syn)

76 <|> try (pUsing syn)

77+ <|> try (pParams syn)

77pFunDecl :: SyntaxInfo -> IParser [PDecl]

79pFunDecl :: SyntaxInfo -> IParser [PDecl]

78pFunDecl syn

80pFunDecl syn

@@ -107,6 +109,18 @@ pUsing syn =

107 lchar '}'

109 lchar '}'

108 return (concat ds)

110 return (concat ds)

109

111

112+pParams :: SyntaxInfo -> IParser [PDecl]

113+pParams syn =

114+ do reserved "params";

115+ lchar '('

116+ ns <- tyDeclList syn

117+ lchar ')'

118+ lchar '{'

119+ let pvars = syn_params syn

120+ ds <- many1 (pDecl syn { syn_params = pvars ++ ns })

121+ lchar '}'

122+ return [PParams ns (concat ds)]

123+

110--------- Fixity ---------

124--------- Fixity ---------

111

125

112pFixity :: IParser PDecl

126pFixity :: IParser PDecl

src/Main.hs+3−2

@@ -47,9 +47,9 @@ runIdris opts =

47loadModule :: FilePath -> Idris ()

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

49 ds <- parseProg defaultSyntax f

50− iLOG (dumpDecls ds)

50+ logLvl 3 (dumpDecls ds)

51 i <- get

52− iLOG (show (idris_infixes i))

52+ logLvl 3 (show (idris_infixes i))

53 -- Now add all the declarations to the context

54 mapM_ (elabDecl toplevel) ds

55 return ()

@@ -62,6 +62,7 @@ dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops

62dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

63dumpDecl (PClauses n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)

64dumpDecl (PData d) = showDImp True d

65+dumpDecl (PParams ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

66getFile :: Opt -> Maybe String

67getFile :: Opt -> Maybe String

67getFile (Filename str) = Just str

68getFile (Filename str) = Just str

wheres.minew file+38

@@ -0,0 +1,38 @@

1+data Bool = False | True;

3+infixl 5 ==, /=, ==.;

4+infixl 6 <, <=, >, >=, <., <=., >., >=.;

5+infixl 7 <<, >>;

6+infixl 8 +,-,++,+.,-.;

7+infixl 9 *,/,*.,/.;

9+intToBool : Int -> Bool;

10+intToBool 0 = False;

11+intToBool x = True;

12+

13+boolOp : {a:Set} -> (a -> a -> Int) -> a -> a -> Bool;

14+boolOp op x y = intToBool (op x y);

15+

16+(+) : Int -> Int -> Int;

17+(+) = prim__addInt;

18+

19+(-) : Int -> Int -> Int;

20+(-) = prim__subInt;

21+

22+(*) : Int -> Int -> Int;

23+(*) = prim__mulInt;

24+

25+data Pair x y = MkPair x y;

26+

27+fact : Int -> Pair Int Int;

28+fact x = factAux 1 x

29+ where {

30+ factAux : Int -> Int -> Pair Int Int;

31+ factAux acc 0 = acc'

32+ where {

33+ acc' : Pair Int Int;

34+ acc' = MkPair acc x;

35+ }

36+ factAux acc n = factAux (acc * n) (n - 1);

37+ }

38+