git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/DSL.hs
175 lines 7.3 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.DSL where
5import Idris.AbsSyntax
7import Idris.Core.TT
8import Idris.Core.Evaluate
10import Control.Monad.State.Strict
11import Debug.Trace
13debindApp :: SyntaxInfo -> PTerm -> PTerm
14debindApp syn t = debind (dsl_bind (dsl_info syn)) t
16desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
17desugar syn i t = let t' = expandDo (dsl_info syn) t in
18 t' -- addImpl i t'
20expandDo :: DSL -> PTerm -> PTerm
21expandDo dsl (PLam n ty tm)
22 | Just lam <- dsl_lambda dsl
23 = let sc = PApp (fileFC "(dsl)") lam [pexp (var dsl n tm 0)] in
24 expandDo dsl sc
25expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)
26expandDo dsl (PLet n ty v tm)
27 | Just letb <- dsl_let dsl
28 = let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in
29 expandDo dsl sc
30expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)
31expandDo dsl (PPi p n ty tm)
32 | Just pi <- dsl_pi dsl
33 = let sc = PApp (fileFC "(dsl)") pi [pexp ty, pexp (var dsl n tm 0)] in
34 expandDo dsl sc
35expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
36expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
37 (map (fmap (expandDo dsl)) args)
38expandDo dsl (PAppBind fc t args) = PAppBind fc (expandDo dsl t)
39 (map (fmap (expandDo dsl)) args)
40expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)
41 (map (pmap (expandDo dsl)) opts)
42expandDo dsl (PEq fc lt rt l r) = PEq fc (expandDo dsl lt) (expandDo dsl rt)
43 (expandDo dsl l) (expandDo dsl r)
44expandDo dsl (PPair fc p l r) = PPair fc p (expandDo dsl l) (expandDo dsl r)
45expandDo dsl (PDPair fc p l t r) = PDPair fc p (expandDo dsl l) (expandDo dsl t)
46 (expandDo dsl r)
47expandDo dsl (PAlternative a as) = PAlternative a (map (expandDo dsl) as)
48expandDo dsl (PHidden t) = PHidden (expandDo dsl t)
49expandDo dsl (PNoImplicits t) = PNoImplicits (expandDo dsl t)
50expandDo dsl (PUnifyLog t) = PUnifyLog (expandDo dsl t)
51expandDo dsl (PDisamb ns t) = PDisamb ns (expandDo dsl t)
52expandDo dsl (PReturn fc) = dsl_return dsl
53expandDo dsl (PRewrite fc r t ty)
54 = PRewrite fc r (expandDo dsl t) ty
55expandDo dsl (PGoal fc r n sc)
56 = PGoal fc (expandDo dsl r) n (expandDo dsl sc)
57expandDo dsl (PDoBlock ds)
58 = expandDo dsl $ debind (dsl_bind dsl) (block (dsl_bind dsl) ds)
59 where
60 block b [DoExp fc tm] = tm
61 block b [a] = PElabError (Msg "Last statement in do block must be an expression")
62 block b (DoBind fc n tm : rest)
63 = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]
64 block b (DoBindP fc p tm alts : rest)
65 = PApp fc b [pexp tm, pexp (PLam (sMN 0 "bpat") Placeholder
66 (PCase fc (PRef fc (sMN 0 "bpat"))
67 ((p, block b rest) : alts)))]
68 block b (DoLet fc n ty tm : rest)
69 = PLet n ty tm (block b rest)
70 block b (DoLetP fc p tm : rest)
71 = PCase fc tm [(p, block b rest)]
72 block b (DoExp fc tm : rest)
73 = PApp fc b
74 [pexp tm,
75 pexp (PLam (sMN 0 "bindx") Placeholder (block b rest))]
76 block b _ = PElabError (Msg "Invalid statement in do block")
78expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
79expandDo dsl t = t
81var :: DSL -> Name -> PTerm -> Int -> PTerm
82var dsl n t i = v' i t where
83 v' i (PRef fc x) | x == n =
84 case dsl_var dsl of
85 Nothing -> PElabError (Msg "No 'variable' defined in dsl")
86 Just v -> PApp fc v [pexp (mkVar fc i)]
87 v' i (PLam n ty sc)
88 | Nothing <- dsl_lambda dsl
89 = PLam n ty (v' i sc)
90 | otherwise = PLam n (v' i ty) (v' (i + 1) sc)
91 v' i (PLet n ty val sc)
92 | Nothing <- dsl_let dsl
93 = PLet n (v' i ty) (v' i val) (v' i sc)
94 | otherwise = PLet n (v' i ty) (v' i val) (v' (i + 1) sc)
95 v' i (PPi p n ty sc)
96 | Nothing <- dsl_pi dsl
97 = PPi p n (v' i ty) (v' i sc)
98 | otherwise = PPi p n (v' i ty) (v' (i+1) sc)
99 v' i (PTyped l r) = PTyped (v' i l) (v' i r)
100 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)
101 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)
102 v' i (PEq f lt rt l r) = PEq f (v' i lt) (v' i rt) (v' i l) (v' i r)
103 v' i (PPair f p l r) = PPair f p (v' i l) (v' i r)
104 v' i (PDPair f p l t r) = PDPair f p (v' i l) (v' i t) (v' i r)
105 v' i (PAlternative a as) = PAlternative a $ map (v' i) as
106 v' i (PHidden t) = PHidden (v' i t)
107 v' i (PIdiom f t) = PIdiom f (v' i t)
108 v' i (PDoBlock ds) = PDoBlock (map (fmap (v' i)) ds)
109 v' i (PNoImplicits t) = PNoImplicits (v' i t)
110 v' i t = t
112 mkVar fc 0 = case index_first dsl of
113 Nothing -> PElabError (Msg "No index_first defined")
114 Just f -> f
115 mkVar fc n = case index_next dsl of
116 Nothing -> PElabError (Msg "No index_next defined")
117 Just f -> PApp fc f [pexp (mkVar fc (n-1))]
119unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
120unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in
121 mkap (getFn e)
122 where
123 getFn (PApp fc f args) = (PApp fc pure [pexp f], args)
124 getFn f = (f, [])
126 mkap (f, []) = f
127 mkap (f, a:as) = mkap (PApp fc ap [pexp f, a], as)
129unIdiom ap pure fc e = PApp fc pure [pexp e]
131debind :: PTerm -> PTerm -> PTerm
132-- For every arg which is an AppBind, lift it out
133debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in
134 bindAll (reverse bs) tm'
135 where
136 db' :: PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
137 db' (PAppBind _ (PApp fc t args) [])
138 = db' (PAppBind fc t args)
139 db' (PAppBind fc t args)
140 = do args' <- dbs args
141 (bs, n) <- get
142 let nm = sUN ("_bindApp" ++ show n)
143 put ((nm, fc, PApp fc t args') : bs, n+1)
144 return (PRef fc nm)
145 db' (PApp fc t args)
146 = do t' <- db' t
147 args' <- mapM dbArg args
148 return (PApp fc t' args')
149 db' (PLam n ty sc) = return (PLam n ty (debind b sc))
150 db' (PLet n ty v sc) = do v' <- db' v
151 return (PLet n ty v' (debind b sc))
152 db' (PCase fc s opts) = do s' <- db' s
153 return (PCase fc s' (map (pmap (debind b)) opts))
154 db' (PPair fc p l r) = do l' <- db' l
155 r' <- db' r
156 return (PPair fc p l' r')
157 db' (PDPair fc p l t r) = do l' <- db' l
158 r' <- db' r
159 return (PDPair fc p l' t r')
160 db' t = return t
162 dbArg a = do t' <- db' (getTm a)
163 return (a { getTm = t' })
165 dbs [] = return []
166 dbs (a : as) = do let t = getTm a
167 t' <- db' t
168 as' <- dbs as
169 return (a { getTm = t' } : as')
171 bindAll [] tm = tm
172 bindAll ((n, fc, t) : bs) tm
173 = PApp fc b [pexp t, pexp (PLam n Placeholder (bindAll bs tm))]