git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/DSL.hs
214 lines 9.1 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.DSL where
5import Data.Generics.Uniplate.Data (transform)
7import Idris.AbsSyntax
9import Idris.Core.TT
10import Idris.Core.Evaluate
12import Control.Monad.State.Strict
13import Debug.Trace
15debindApp :: SyntaxInfo -> PTerm -> PTerm
16debindApp syn t = debind (dsl_bind (dsl_info syn)) t
18dslify :: SyntaxInfo -> IState -> PTerm -> PTerm
19dslify syn i = transform dslifyApp
20 where
21 dslifyApp (PApp fc (PRef _ f) [a])
22 | [d] <- lookupCtxt f (idris_dsls i)
23 = desugar (syn { dsl_info = d }) i (getTm a)
24 dslifyApp t = t
26desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
27desugar syn i t = let t' = expandDo (dsl_info syn) t
28 in dslify syn i t'
30mkTTName :: FC -> Name -> PTerm
31mkTTName fc n =
32 let mkList fc [] = PRef fc (sNS (sUN "Nil") ["List", "Prelude"])
33 mkList fc (x:xs) = PApp fc (PRef fc (sNS (sUN "::") ["List", "Prelude"]))
34 [ pexp (stringC x)
35 , pexp (mkList fc xs)]
36 stringC = PConstant . Str . str
37 intC = PConstant . I
38 reflm n = sNS (sUN n) ["Reflection", "Language"]
39 in case n of
40 UN nm -> PApp fc (PRef fc (reflm "UN")) [ pexp (stringC nm)]
41 NS nm ns -> PApp fc (PRef fc (reflm "NS")) [ pexp (mkTTName fc nm)
42 , pexp (mkList fc ns)]
43 MN i nm -> PApp fc (PRef fc (reflm "MN")) [ pexp (intC i)
44 , pexp (stringC nm)]
45 otherwise -> PRef fc $ reflm "NErased"
47expandDo :: DSL -> PTerm -> PTerm
48expandDo dsl (PLam fc n ty tm)
49 | Just lam <- dsl_lambda dsl
50 = let sc = PApp fc lam [ pexp (mkTTName fc n)
51 , pexp (var dsl n tm 0)]
52 in expandDo dsl sc
53expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)
54expandDo dsl (PLet fc n ty v tm)
55 | Just letb <- dsl_let dsl
56 = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)
57 , pexp v
58 , pexp (var dsl n tm 0)]
59 in expandDo dsl sc
60expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)
61expandDo dsl (PPi p n ty tm)
62 | Just pi <- dsl_pi dsl
63 = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)
64 , pexp ty
65 , pexp (var dsl n tm 0)]
66 in expandDo dsl sc
67expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
68expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
69 (map (fmap (expandDo dsl)) args)
70expandDo dsl (PAppBind fc t args) = PAppBind fc (expandDo dsl t)
71 (map (fmap (expandDo dsl)) args)
72expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)
73 (map (pmap (expandDo dsl)) opts)
74expandDo dsl (PEq fc lt rt l r) = PEq fc (expandDo dsl lt) (expandDo dsl rt)
75 (expandDo dsl l) (expandDo dsl r)
76expandDo dsl (PPair fc p l r) = PPair fc p (expandDo dsl l) (expandDo dsl r)
77expandDo dsl (PDPair fc p l t r) = PDPair fc p (expandDo dsl l) (expandDo dsl t)
78 (expandDo dsl r)
79expandDo dsl (PAlternative a as) = PAlternative a (map (expandDo dsl) as)
80expandDo dsl (PHidden t) = PHidden (expandDo dsl t)
81expandDo dsl (PNoImplicits t) = PNoImplicits (expandDo dsl t)
82expandDo dsl (PUnifyLog t) = PUnifyLog (expandDo dsl t)
83expandDo dsl (PDisamb ns t) = PDisamb ns (expandDo dsl t)
84expandDo dsl (PReturn fc) = dsl_return dsl
85expandDo dsl (PRewrite fc r t ty)
86 = PRewrite fc r (expandDo dsl t) ty
87expandDo dsl (PGoal fc r n sc)
88 = PGoal fc (expandDo dsl r) n (expandDo dsl sc)
89expandDo dsl (PDoBlock ds)
90 = expandDo dsl $ debind (dsl_bind dsl) (block (dsl_bind dsl) ds)
91 where
92 block b [DoExp fc tm] = tm
93 block b [a] = PElabError (Msg "Last statement in do block must be an expression")
94 block b (DoBind fc n tm : rest)
95 = PApp fc b [pexp tm, pexp (PLam fc n Placeholder (block b rest))]
96 block b (DoBindP fc p tm alts : rest)
97 = PApp fc b [pexp tm, pexp (PLam fc (sMN 0 "bpat") Placeholder
98 (PCase fc (PRef fc (sMN 0 "bpat"))
99 ((p, block b rest) : alts)))]
100 block b (DoLet fc n ty tm : rest)
101 = PLet fc n ty tm (block b rest)
102 block b (DoLetP fc p tm : rest)
103 = PCase fc tm [(p, block b rest)]
104 block b (DoExp fc tm : rest)
105 = PApp fc b
106 [pexp tm,
107 pexp (PLam fc (sMN 0 "bindx") Placeholder (block b rest))]
108 block b _ = PElabError (Msg "Invalid statement in do block")
110expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
111expandDo dsl (PRunTactics fc tm) = PRunTactics fc $ expandDo dsl tm
112expandDo dsl t = t
114-- | Replace DSL-bound variable in a term
115var :: DSL -> Name -> PTerm -> Int -> PTerm
116var dsl n t i = v' i t where
117 v' i (PRef fc x) | x == n =
118 case dsl_var dsl of
119 Nothing -> PElabError (Msg "No 'variable' defined in dsl")
120 Just v -> PApp fc v [pexp (mkVar fc i)]
121 v' i (PLam fc n ty sc)
122 | Nothing <- dsl_lambda dsl
123 = PLam fc n ty (v' i sc)
124 | otherwise = PLam fc n (v' i ty) (v' (i + 1) sc)
125 v' i (PLet fc n ty val sc)
126 | Nothing <- dsl_let dsl
127 = PLet fc n (v' i ty) (v' i val) (v' i sc)
128 | otherwise = PLet fc n (v' i ty) (v' i val) (v' (i + 1) sc)
129 v' i (PPi p n ty sc)
130 | Nothing <- dsl_pi dsl
131 = PPi p n (v' i ty) (v' i sc)
132 | otherwise = PPi p n (v' i ty) (v' (i+1) sc)
133 v' i (PTyped l r) = PTyped (v' i l) (v' i r)
134 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)
135 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)
136 v' i (PEq f lt rt l r) = PEq f (v' i lt) (v' i rt) (v' i l) (v' i r)
137 v' i (PPair f p l r) = PPair f p (v' i l) (v' i r)
138 v' i (PDPair f p l t r) = PDPair f p (v' i l) (v' i t) (v' i r)
139 v' i (PAlternative a as) = PAlternative a $ map (v' i) as
140 v' i (PHidden t) = PHidden (v' i t)
141 v' i (PIdiom f t) = PIdiom f (v' i t)
142 v' i (PDoBlock ds) = PDoBlock (map (fmap (v' i)) ds)
143 v' i (PNoImplicits t) = PNoImplicits (v' i t)
144 v' i t = t
146 mkVar fc 0 = case index_first dsl of
147 Nothing -> PElabError (Msg "No index_first defined")
148 Just f -> setFC fc f
149 mkVar fc n = case index_next dsl of
150 Nothing -> PElabError (Msg "No index_next defined")
151 Just f -> PApp fc f [pexp (mkVar fc (n-1))]
153 setFC fc (PRef _ n) = PRef fc n
154 setFC fc (PApp _ f xs) = PApp fc (setFC fc f) (map (fmap (setFC fc)) xs)
155 setFC fc t = t
157unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
158unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in
159 mkap (getFn e)
160 where
161 getFn (PApp fc f args) = (PApp fc pure [pexp f], args)
162 getFn f = (f, [])
164 mkap (f, []) = f
165 mkap (f, a:as) = mkap (PApp fc ap [pexp f, a], as)
167unIdiom ap pure fc e = PApp fc pure [pexp e]
169debind :: PTerm -> PTerm -> PTerm
170-- For every arg which is an AppBind, lift it out
171debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in
172 bindAll (reverse bs) tm'
173 where
174 db' :: PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
175 db' (PAppBind _ (PApp fc t args) [])
176 = db' (PAppBind fc t args)
177 db' (PAppBind fc t args)
178 = do args' <- dbs args
179 (bs, n) <- get
180 let nm = sUN ("_bindApp" ++ show n)
181 put ((nm, fc, PApp fc t args') : bs, n+1)
182 return (PRef fc nm)
183 db' (PApp fc t args)
184 = do t' <- db' t
185 args' <- mapM dbArg args
186 return (PApp fc t' args')
187 db' (PLam fc n ty sc) = return (PLam fc n ty (debind b sc))
188 db' (PLet fc n ty v sc) = do v' <- db' v
189 return (PLet fc n ty v' (debind b sc))
190 db' (PCase fc s opts) = do s' <- db' s
191 return (PCase fc s' (map (pmap (debind b)) opts))
192 db' (PPair fc p l r) = do l' <- db' l
193 r' <- db' r
194 return (PPair fc p l' r')
195 db' (PDPair fc p l t r) = do l' <- db' l
196 r' <- db' r
197 return (PDPair fc p l' t r')
198 db' (PRunTactics fc t) = fmap (PRunTactics fc) (db' t)
199 db' t = return t
201 dbArg a = do t' <- db' (getTm a)
202 return (a { getTm = t' })
204 dbs [] = return []
205 dbs (a : as) = do let t = getTm a
206 t' <- db' t
207 as' <- dbs as
208 return (a { getTm = t' } : as')
210 bindAll [] tm = tm
211 bindAll ((n, fc, t) : bs) tm
212 = PApp fc b [pexp t, pexp (PLam fc n Placeholder (bindAll bs tm))]