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

git.iko.soy/Idris-dev

Added 'where' clauses in pattern matches

commit083fc7024122e48cd87417a3a5f944225de928fb authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 13 Oct 2011, 15:24 (15 years ago) parentde89a04

7 files changed+147−44

compare with master

unifiedsplit

prims.mi+1−1 src/Core/TT.hs+4 src/Idris/AbsSyntax.hs+17−5 src/Idris/ElabDecls.hs+69−35 src/Idris/Parser.hs+15−1 src/Main.hs+3−2 wheres.mi+38

prims.mi+1−1

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

1010intToBool 0 = False;

1111intToBool x = True;

1212

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

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

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

1515

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

src/Core/TT.hs+4

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

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

9797toAlist = Map.toList

9898

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+

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

101105 deriving Eq

src/Idris/AbsSyntax.hs+17−5

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

2525 idris_infixes :: [FixDecl],

2626 idris_implicits :: Ctxt [PArg],

2727 idris_log :: String,

28− idris_options :: IOption

28+ idris_options :: IOption,

29+ idris_name :: Int

2930 }

3031

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

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

3233

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

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

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

4041getIState :: Idris IState

4142getIState = get

4243

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+

4350setContext :: Context -> Idris ()

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

4552

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

101108 | PTy Name t -- type declaration

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

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

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

104112 deriving Functor

105113

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

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

125133declared (PTy n t) = [n]

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

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

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

128137

129138-- High level language terms

130139--

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

147156

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

149158

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

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

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

151161 deriving Show

152162

153−defaultSyntax = Syn []

163+defaultSyntax = Syn [] []

154164

155165--- Pretty printing declarations and terms

156166

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

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

285295implicitise syn ist tm

286296 = let uvars = using syn

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

297+ pvars = syn_params syn

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

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

288300 if null ns

289301 then (tm, reverse declimps)

290302 else implicitise syn ist (pibind uvars ns tm)

src/Idris/ElabDecls.hs+69−35

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

1919-- paramaterised declarations, etc.

2020

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

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

2223 liftname :: Name -> Name }

2324

24−toplevel = EInfo [] id

25+toplevel = EInfo [] emptyContext id

2526

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

27−elabType info n ty

28− = do ctxt <- getContext

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

29+ n = liftname info n_in in

30+ do ctxt <- getContext

2931 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)

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

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

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

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

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

3638elabData info (PDatadecl n t dcons)

3739 = 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)

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

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

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

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

4648elabCon info (n, t)

4749 = do ctxt <- getContext

4850 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)

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

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

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

5355 return (n, cty)

5456

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

56−elabClauses info n cs

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

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

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

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

5961 show l ++ " = " ++

6062 show r) pats))

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

7476 = do ctxt <- getContext

7577 logLvl 10 (show tm)

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

77− (build True (infTerm tm))

79+ (build info True (infTerm tm))

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

7981 let vtm = getInferTerm tm'

8082 iLOG (show vtm)

8183 tclift $ recheck ctxt [] vtm

8284

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

84−elabClause info (PClause _ lhs rhs whereblock)

86+elabClause info (PClause fname lhs rhs whereblock)

8587 = do ctxt <- getContext

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

8789 -- pattern bindings

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

89− (build True (infTerm lhs))

91+ (build info True (infTerm lhs))

9092 let lhs_tm = getInferTerm lhs'

9193 let lhs_ty = getInferType lhs'

9294 logLvl 3 (show lhs_tm)

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

94− -- TODO: elaborate where block here.

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−

96+ -- Elaborate where block

97+ ist <- getIState

98+ windex <- getName

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

100+ mapM_ (elabDecl' winfo) whereblock

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

101102 iLOG (showImp True rhs)

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

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

103105 (do pbinds lhs_tm

104− build False rhs

106+ build winfo False rhs

105107 psolve lhs_tm

106108 get_term)

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

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

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

116118 psolve tm = return ()

117119

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

119− pvars _ = []

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

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

120135

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

122137elabDecl 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

126141 elabType info n ty

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

128143 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

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

131155

132156{- not finished...

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

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

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

170194-- holes to pattern bindings.

171195

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

173−build pattern tm = do elab pattern tm

174− get_term

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

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

198+ get_term

175199

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

177−elab pattern tm = do elab' tm

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

179− mkPat

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

201+elab info pattern tm = do elab' tm

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

203+ mkPat

180204 where

181205 isph arg = case getTm arg of

182206 Placeholder -> True

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

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

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

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

197− elab' (PRef n) | pattern

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

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

199223 (patvar n)

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

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) [])

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

201231 elab' (PLam n Placeholder sc)

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

203233 elab' (PPi _ n Placeholder sc)

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

211241 elab' sc

212242 solve

213243 elab' (PApp (PRef f) args)

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

215− solve

216− elabArgs ns (map getTm args))

217− (do apply_elab f (map toElab args)

218− solve)

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

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

249+ solve

250+ elabArgs ns (map getTm args))

251+ (do apply_elab f (map toElab args)

252+ solve)

219253 elab' (PApp f [arg])

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

221255 solve

src/Idris/Parser.hs+15−1

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

5454

5555-- Collect PClauses with the same function name

5656collect :: [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)

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

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

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

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

6162collect (d : ds) = d : collect ds

6263collect [] = []

6364

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

7374 i <- getState

7475 return [fmap (addImpl i) d]

7576 <|> try (pUsing syn)

77+ <|> try (pParams syn)

7678

7779pFunDecl :: SyntaxInfo -> IParser [PDecl]

7880pFunDecl syn

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

107109 lchar '}'

108110 return (concat ds)

109111

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+

110124--------- Fixity ---------

111125

112126pFixity :: IParser PDecl

src/Main.hs+3−2

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

4747loadModule :: FilePath -> Idris ()

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

4949 ds <- parseProg defaultSyntax f

50− iLOG (dumpDecls ds)

50+ logLvl 3 (dumpDecls ds)

5151 i <- get

52− iLOG (show (idris_infixes i))

52+ logLvl 3 (show (idris_infixes i))

5353 -- Now add all the declarations to the context

5454 mapM_ (elabDecl toplevel) ds

5555 return ()

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

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

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

6464dumpDecl (PData d) = showDImp True d

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

6566

6667getFile :: Opt -> Maybe String

6768getFile (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+