git.iko.soy/Idris-dev
on master help sign in
Functor for PTerm/PDecl
commit596e9aa608d39ae50e4ee561d6c2c590728898a0 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 6 Oct 2011, 19:54 (15 years ago) parent2eb5b52
3 files changed+50−17
compare with master
unifiedsplit
decls.mi+1−1 src/Idris/AbsSyntax.hs+21−9 src/Idris/Parser.hs+28−7
decls.mi+1−1
@@ -16,7 +16,7 @@ plus (S k) y = S (plus k y);
1616
1717app : Vect a n -> Vect a m -> Vect a (plus n m);
1818app VNil ys = ys;
19−app (x :: xs) ys = x :: (app xs ys);
19+app (x :: xs) ys = x :: app xs ys;
2020
2121infixl 5 .+. ;
2222
src/Idris/AbsSyntax.hs+21−9
@@ -64,16 +64,22 @@ instance Ord FixDecl where
6464
6565data Plicity = Imp | Exp deriving Show
6666
67−data PDecl = PFix Fixity [String] -- fixity declaration
68− | PTy Name PTerm -- type declaration
69− | PClause PTerm PTerm -- pattern clause
70− | PData PData -- data declaration
71− deriving Show
67+data PDecl' t = PFix Fixity [String] -- fixity declaration
68+ | PTy Name t -- type declaration
69+ | PClause t t -- pattern clause
70+ | PData (PData' t) -- data declaration
71+ deriving (Show, Functor)
7272
73−data PData = PDatadecl { d_name :: Name,
74− d_tcon :: PTerm,
75− d_cons :: [(Name, PTerm)] }
76− deriving Show
73+data PData' t = PDatadecl { d_name :: Name,
74+ d_tcon :: t,
75+ d_cons :: [(Name, t)] }
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
7783
7884-- High level language terms
7985
@@ -87,4 +93,10 @@ data PTerm = PQuote Raw
8793 | Placeholder
8894 deriving Show
8995
96+-- Dealing with implicit arguments
97+
98+implicitise :: IState -> PTerm -> (PTerm, [Name])
99+implicitise ist tm = (tm, [])
90100
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
5151pFullExpr = do x <- pExpr; eof; return x
5252
5353pDecl :: 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)
5557
5658--------- Top Level Declarations ---------
5759
5860pDecl' :: IParser PDecl
5961pDecl' = try pFixity
6062 <|> try (do n <- pfName; ty <- pTSig
61− return (PTy n ty))
63+ ty' <- implicit n ty
64+ return (PTy n ty'))
6265 <|> try pData
6366 <|> try pPattern
6467
65−-------- Fixity --------
68+--------- Fixity ---------
6669
6770pFixity :: IParser PDecl
6871pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
@@ -146,15 +149,19 @@ binary name f assoc = Infix (do { reservedOp name; return f }) assoc
146149pData :: IParser PDecl
147150pData = try (do reserved "data"; tyn <- pfName; ty <- pTSig
148151 reserved "where"
152+ ty' <- implicit tyn ty
149153 cons <- sepBy1 pConstructor (lchar '|')
150− return $ PData (PDatadecl tyn ty cons))
154+ return $ PData (PDatadecl tyn ty' cons))
151155 <|> do reserved "data"; tyn <- pfName; args <- many iName
152156 lchar '='
153157 cons <- sepBy1 pSimpleCon (lchar '|')
154158 let conty = mkPApp (PRef tyn) (map PRef args)
155− return $ PData (PDatadecl tyn (bindArgs (map (\a -> PSet) args) PSet)
156− (map (\ (x, cargs) ->
157− (x, bindArgs cargs conty)) cons))
159+ let ty = bindArgs (map (\a -> PSet) args) PSet
160+ ty' <- implicit tyn ty
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')
158165
159166mkPApp t [] = t
160167mkPApp t xs = PApp t [] xs
@@ -188,3 +195,17 @@ pPattern = try (do n <- pfName
188195 rhs <- pExpr
189196 return $ PClause (PApp (PRef (UN [op])) [] [l,r]) rhs
190197
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+