git.iko.soy/Idris-dev
on master help sign in
Functor for PTerm/PDecl
596e9aaEdwin Brady
decls.mi+1−1
compare with master
unifiedsplit
@@ -16,7 +16,7 @@ plus (S k) y = S (plus k y);
16
16
17app : Vect a n -> Vect a m -> Vect a (plus n m);
17app : Vect a n -> Vect a m -> Vect a (plus n m);
18app VNil ys = ys;
18app VNil ys = ys;
19−app (x :: xs) ys = x :: (app xs ys);
19+app (x :: xs) ys = x :: app xs ys;
20
20
21infixl 5 .+. ;
21infixl 5 .+. ;
22
22
src/Idris/AbsSyntax.hs+21−9
@@ -64,16 +64,22 @@ instance Ord FixDecl where
64
64
65data Plicity = Imp | Exp deriving Show
65data Plicity = Imp | Exp deriving Show
66
66
67−data PDecl = PFix Fixity [String] -- fixity declaration
67+data PDecl' t = PFix Fixity [String] -- fixity declaration
68− | PTy Name PTerm -- type declaration
68+ | PTy Name t -- type declaration
69− | PClause PTerm PTerm -- pattern clause
69+ | PClause t t -- pattern clause
70− | PData PData -- data declaration
70+ | PData (PData' t) -- data declaration
71− deriving Show
71+ deriving (Show, Functor)
72
72
73−data PData = PDatadecl { d_name :: Name,
73+data PData' t = PDatadecl { d_name :: Name,
74− d_tcon :: PTerm,
74+ d_tcon :: t,
75− d_cons :: [(Name, PTerm)] }
75+ d_cons :: [(Name, t)] }
76− deriving Show
76+ deriving (Show, Functor)
77+
78+-- Handy to get a free function for applying PTerm -> PTerm functions
79+-- across a program, by deriving Functor
80+
81+type PDecl = PDecl' PTerm
82+type PData = PData' PTerm
77
83
78-- High level language terms
84-- High level language terms
79
85
@@ -87,4 +93,10 @@ data PTerm = PQuote Raw
87 | Placeholder
93 | Placeholder
88 deriving Show
94 deriving Show
89
95
96+-- Dealing with implicit arguments
97+
98+implicitise :: IState -> PTerm -> (PTerm, [Name])
99+implicitise ist tm = (tm, [])
90
100
101+addImpl :: IState -> PTerm -> PTerm
102+addImpl ist ptm = ptm
src/Idris/Parser.hs+28−7
@@ -51,18 +51,21 @@ parseProg fname = do file <- lift $ readFile fname
51pFullExpr = do x <- pExpr; eof; return x
51pFullExpr = do x <- pExpr; eof; return x
52
52
53pDecl :: IParser PDecl
53pDecl :: IParser PDecl
54−pDecl = do d <- pDecl'; lchar ';'; return d
54+pDecl = do d <- pDecl'; lchar ';';
55+ i <- getState
56+ return (fmap (addImpl i) d)
55
57
56--------- Top Level Declarations ---------
58--------- Top Level Declarations ---------
57
59
58pDecl' :: IParser PDecl
60pDecl' :: IParser PDecl
59pDecl' = try pFixity
61pDecl' = try pFixity
60 <|> try (do n <- pfName; ty <- pTSig
62 <|> try (do n <- pfName; ty <- pTSig
63+ ty' <- implicit n ty
61− return (PTy n ty))
64+ return (PTy n ty'))
62 <|> try pData
65 <|> try pData
63 <|> try pPattern
66 <|> try pPattern
64
67
65−-------- Fixity --------
68+--------- Fixity ---------
66
69
67pFixity :: IParser PDecl
70pFixity :: IParser PDecl
68pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
71pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
@@ -146,15 +149,19 @@ binary name f assoc = Infix (do { reservedOp name; return f }) assoc
146pData :: IParser PDecl
149pData :: IParser PDecl
147pData = try (do reserved "data"; tyn <- pfName; ty <- pTSig
150pData = try (do reserved "data"; tyn <- pfName; ty <- pTSig
148 reserved "where"
151 reserved "where"
152+ ty' <- implicit tyn ty
149 cons <- sepBy1 pConstructor (lchar '|')
153 cons <- sepBy1 pConstructor (lchar '|')
150− return $ PData (PDatadecl tyn ty cons))
154+ return $ PData (PDatadecl tyn ty' cons))
151 <|> do reserved "data"; tyn <- pfName; args <- many iName
155 <|> do reserved "data"; tyn <- pfName; args <- many iName
152 lchar '='
156 lchar '='
153 cons <- sepBy1 pSimpleCon (lchar '|')
157 cons <- sepBy1 pSimpleCon (lchar '|')
154 let conty = mkPApp (PRef tyn) (map PRef args)
158 let conty = mkPApp (PRef tyn) (map PRef args)
155− return $ PData (PDatadecl tyn (bindArgs (map (\a -> PSet) args) PSet)
159+ let ty = bindArgs (map (\a -> PSet) args) PSet
156− (map (\ (x, cargs) ->
160+ ty' <- implicit tyn ty
157− (x, bindArgs cargs conty)) cons))
161+ cons' <- mapM (\ (x, cargs) -> do let cty = bindArgs cargs conty
162+ cty' <- implicit x cty
163+ return (x, cty')) cons
164+ return $ PData (PDatadecl tyn ty' cons')
158
165
159mkPApp t [] = t
166mkPApp t [] = t
160mkPApp t xs = PApp t [] xs
167mkPApp t xs = PApp t [] xs
@@ -188,3 +195,17 @@ pPattern = try (do n <- pfName
188 rhs <- pExpr
195 rhs <- pExpr
189 return $ PClause (PApp (PRef (UN [op])) [] [l,r]) rhs
196 return $ PClause (PApp (PRef (UN [op])) [] [l,r]) rhs
190
197
198+-- Dealing with implicit arguments
199+
200+implicit :: Name -> PTerm -> IParser PTerm
201+implicit n ptm
202+ = do i <- getState
203+ let (tm', names) = implicitise i ptm
204+ setState (i { idris_implicits = addDef n names (idris_implicits i) })
205+ return tm'
206+
207+addImplicits :: PTerm -> IParser PTerm
208+addImplicits tm
209+ = do i <- getState
210+ return (addImpl i tm)
211+