git.iko.soy/Idris-dev
on master help sign in
Added [static] annotations (which do nothing yet) and state to evaluator
3bdfa26Edwin Brady
interp.idr+1−1
compare with master
unifiedsplit
@@ -22,7 +22,7 @@ using (G : Vect Ty n) {
22 | Add : Expr G TyNat -> Expr G TyNat -> Expr G TyNat
22 | Add : Expr G TyNat -> Expr G TyNat -> Expr G TyNat
23 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
23 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
24
24
25− interp : Env G -> Expr G t -> interpTy t;
25+ interp : Env G -> [static] Expr G t -> interpTy t;
26 interp env (Var i) = envLookup i env;
26 interp env (Var i) = envLookup i env;
27 interp env (Val x) = x;
27 interp env (Val x) = x;
28 interp env (Lam sc) = \x => interp (Extend x env) sc;
28 interp env (Lam sc) = \x => interp (Extend x env) sc;
src/Core/Evaluate.hs+92−65
@@ -8,22 +8,27 @@ module Core.Evaluate(normalise,
8 Value(..)) where
8 Value(..)) where
9
9
10import Debug.Trace
10import Debug.Trace
11+import Control.Monad.State
11
12
12import Core.TT
13import Core.TT
13import Core.CaseTree
14import Core.CaseTree
14
15
15-- VALUES (as HOAS) ---------------------------------------------------------
16-- VALUES (as HOAS) ---------------------------------------------------------
16
17
18+type EvalState = ()
19+type Eval a = State EvalState a
20+
17data Value = VP NameType Name Value
21data Value = VP NameType Name Value
18 | VV Int
22 | VV Int
19− | VBind Name (Binder Value) (Value -> Value)
23+ | VBind Name (Binder Value) (Value -> Eval Value)
20 | VApp Value Value
24 | VApp Value Value
21 | VSet Int
25 | VSet Int
22 | VConstant Const
26 | VConstant Const
23 | VTmp Int
27 | VTmp Int
24
28
25instance Show Value where
29instance Show Value where
26− show = show . quote 0
30+ show v = "<<Value>>"
31+
27
32
28-- THE EVALUATOR ------------------------------------------------------------
33-- THE EVALUATOR ------------------------------------------------------------
29
34
@@ -33,7 +38,8 @@ instance Show Value where
33-- while building a proof.
38-- while building a proof.
34
39
35normalise :: Context -> Env -> TT Name -> TT Name
40normalise :: Context -> Env -> TT Name -> TT Name
36−normalise ctxt env t = quote 0 (eval ctxt (map finalEntry env) (finalise t))
41+normalise ctxt env t = evalState (do val <- eval ctxt (map finalEntry env) (finalise t)
42+ quote 0 val) ()
37
43
38-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
44-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
39
45
@@ -52,70 +58,85 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
52-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
58-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
53-- such as we might have during construction of a proof)
59-- such as we might have during construction of a proof)
54
60
55−eval :: Context -> Env -> TT Name -> Value
61+eval :: Context -> Env -> TT Name -> Eval Value
56eval ctxt genv tm = ev [] tm where
62eval ctxt genv tm = ev [] tm where
57 ev env (P _ n ty)
63 ev env (P _ n ty)
58 | Just (Let t v) <- lookup n genv = ev env v
64 | Just (Let t v) <- lookup n genv = ev env v
59 ev env (P Ref n ty) = case lookupDef n ctxt of
65 ev env (P Ref n ty) = case lookupDef n ctxt of
60− Just (Function (Fun _ _ _ v)) -> v
66+ Just (Function (Fun _ _ _ v)) -> return v
61− Just (TyDecl nt ty hty) -> VP nt n hty
67+ Just (TyDecl nt ty hty) -> return $ VP nt n hty
62 Just (CaseOp _ _ [] tree) ->
68 Just (CaseOp _ _ [] tree) ->
63− case evCase env [] [] tree of
69+ do c <- evCase env [] [] tree
64− (Nothing, _) -> VP Ref n (ev env ty)
70+ case c of
65− (Just v, _) -> v
71+ (Nothing, _) -> liftM (VP Ref n) (ev env ty)
66− _ -> VP Ref n (ev env ty)
72+ (Just v, _) -> return v
67− ev env (P nt n ty) = VP nt n (ev env ty)
73+ _ -> liftM (VP Ref n) (ev env ty)
68− ev env (V i) | i < length env = env !! i
74+ ev env (P nt n ty) = liftM (VP nt n) (ev env ty)
69− | otherwise = VV i --error $ "Internal error: V" ++ show i ++ " "
75+ ev env (V i) | i < length env = return $ env !! i
70− -- ++ showEnv genv tm ++ "\n" ++ show genv
76+ | otherwise = return $ VV i
71 ev env (Bind n (Let t v) sc)
77 ev env (Bind n (Let t v) sc)
72− = wknV (-1) $ ev (ev env (finalise v) : env) sc
78+ = do v' <- ev env (finalise v)
79+ sc' <- ev (v' : env) sc
80+ wknV (-1) sc'
73 ev env (Bind n (NLet t v) sc)
81 ev env (Bind n (NLet t v) sc)
74− = VBind n (Let (ev env (finalise t)) (ev env (finalise v)))
82+ = do t' <- ev env (finalise t)
75− $ (\x -> ev (ev env v : env) sc)
83+ v' <- ev env (finalise v)
76− ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)
84+ sc' <- ev (v' : env) sc
77− where vbind env t = fmap (\tm -> ev env (finalise tm)) t
85+ return $ VBind n (Let t' v') (\x -> return sc')
78− ev env (App f a) = evApply env [ev env a] (ev env f)
86+ ev env (Bind n b sc)
79− ev env (Constant c) = VConstant c
87+ = do b' <- vbind env b
80− ev env (Set i) = VSet i
88+ return $ VBind n b' (\x -> ev (x:env) sc)
89+ where vbind env t = fmapMB (\tm -> ev env (finalise tm)) t
90+ ev env (App f a) = do f' <- ev env f
91+ a' <- ev env a
92+ evApply env [a'] f'
93+ ev env (Constant c) = return $ VConstant c
94+ ev env (Set i) = return $ VSet i
81
95
82− evApply env args (VApp f a) = evApply env (a:args) f
96+ evApply env args (VApp f a) =
97+ evApply env (a:args) f
83 evApply env args f = apply env f args
98 evApply env args f = apply env f args
84
99
85− apply env (VBind n (Lam t) sc) (a:as) = wknV (-1) $ apply env (sc a) as
100+ apply env (VBind n (Lam t) sc) (a:as) = do a' <- sc a
101+ app <- apply env a' as
102+ wknV (-1) app
86 apply env (VP Ref n ty) args
103 apply env (VP Ref n ty) args
87 | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt
104 | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt
88− = case evCase env ns args tree of
105+ = do c <- evCase env ns args tree
89− (Nothing, _) -> unload env (VP Ref n ty) args
106+ case c of
107+ (Nothing, _) -> return $ unload env (VP Ref n ty) args
90 (Just v, rest) -> evApply env rest v
108 (Just v, rest) -> evApply env rest v
91 | Just (Operator _ i op) <- lookupDef n ctxt
109 | Just (Operator _ i op) <- lookupDef n ctxt
92 = if (i <= length args)
110 = if (i <= length args)
93− then case op (take i args) of
111+ then case op (take i args) of
94− Nothing -> unload env (VP Ref n ty) args
112+ Nothing -> return $ unload env (VP Ref n ty) args
95− Just v -> evApply env (drop i args) v
113+ Just v -> evApply env (drop i args) v
96− else unload env (VP Ref n ty) args
114+ else return $ unload env (VP Ref n ty) args
97− apply env f (a:as) = unload env f (a:as)
115+ apply env f (a:as) = return $ unload env f (a:as)
98− apply env f [] = f
116+ apply env f [] = return f
99
117
100 unload env f [] = f
118 unload env f [] = f
101 unload env f (a:as) = unload env (VApp f a) as
119 unload env f (a:as) = unload env (VApp f a) as
102
120
103 evCase env ns args tree
121 evCase env ns args tree
104 | length ns <= length args
122 | length ns <= length args
105− = let args' = take (length ns) args
123+ = do let args' = take (length ns) args
106− rest = drop (length ns) args in
124+ let rest = drop (length ns) args
107− (evTree env (zipWith (\n t -> (n, t)) ns args') tree, rest)
125+ t <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
108− | otherwise = (Nothing, args)
126+ return (t, rest)
109−
127+ | otherwise = return (Nothing, args)
110− evTree :: [Value] -> [(Name, Value)] -> SC -> Maybe Value
128+
111− evTree env amap (UnmatchedCase str) = Nothing
129+ evTree :: [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
130+ evTree env amap (UnmatchedCase str) = return Nothing
112 evTree env amap (STerm tm)
131 evTree env amap (STerm tm)
113− = let etm = pToVs (map fst amap) tm in
132+ = do let etm = pToVs (map fst amap) tm
114− Just $ ev (map snd amap ++ env) etm
133+ etm' <- ev (map snd amap ++ env) etm
134+ return $ Just etm'
115 evTree env amap (Case n alts)
135 evTree env amap (Case n alts)
116− = do v <- lookup n amap
136+ = case (do v <- lookup n amap
117− (altmap, sc) <- chooseAlt v (getValArgs v) alts amap
137+ chooseAlt v (getValArgs v) alts amap) of
118− evTree env altmap sc
138+ Just (altmap, sc) -> evTree env altmap sc
139+ _ -> return Nothing
119
140
120 chooseAlt :: Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
141 chooseAlt :: Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
121 Maybe ([(Name, Value)], SC)
142 Maybe ([(Name, Value)], SC)
@@ -156,22 +177,26 @@ eval ctxt genv tm = ev [] tm where
156 getValArgs' (VApp f a) as = getValArgs' f (a:as)
177 getValArgs' (VApp f a) as = getValArgs' f (a:as)
157 getValArgs' f as = (f, as)
178 getValArgs' f as = (f, as)
158
179
159−quote :: Int -> Value -> TT Name
180+quote :: Int -> Value -> Eval (TT Name)
160−quote i (VP nt n v) = P nt n (quote i v)
181+quote i (VP nt n v) = liftM (P nt n) (quote i v)
161−quote i (VV x) = V x
182+quote i (VV x) = return $ V x
162−quote i (VBind n b sc) = Bind n (quoteB b) (quote (i+1) (sc (VTmp i)))
183+quote i (VBind n b sc) = do sc' <- sc (VTmp i)
163− where quoteB t = fmap (quote i) t
184+ b' <- quoteB b
164−quote i (VApp f a) = App (quote i f) (quote i a)
185+ liftM (Bind n b') (quote (i+1) sc')
165−quote i (VSet u) = Set u
186+ where quoteB t = fmapMB (quote i) t
166−quote i (VConstant c) = Constant c
187+quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
167−quote i (VTmp x) = V (i - x - 1)
188+quote i (VSet u) = return $ Set u
168−
189+quote i (VConstant c) = return $ Constant c
169−
190+quote i (VTmp x) = return $ V (i - x - 1)
170−wknV :: Int -> Value -> Value
191+
171−wknV i (VV x) = VV (x + i)
192+
172−wknV i (VBind n b sc) = VBind n (fmap (wknV i) b) (\x -> (wknV i (sc x)))
193+wknV :: Int -> Value -> Eval Value
173−wknV i (VApp f a) = VApp (wknV i f) (wknV i a)
194+wknV i (VV x) = return $ VV (x + i)
174−wknV i t = t
195+wknV i (VBind n b sc) = do b' <- fmapMB (wknV i) b
196+ return $ VBind n b' (\x -> do x' <- sc x
197+ wknV i x')
198+wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
199+wknV i t = return t
175
200
176-- CONTEXTS -----------------------------------------------------------------
201-- CONTEXTS -----------------------------------------------------------------
177
202
@@ -199,24 +224,26 @@ instance Show Def where
199
224
200type Context = Ctxt Def
225type Context = Ctxt Def
201
226
227+veval ctxt env t = evalState (eval ctxt env t) ()
228+
202addToCtxt :: Name -> Term -> Type -> Context -> Context
229addToCtxt :: Name -> Term -> Type -> Context -> Context
203−addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (eval ctxt [] ty)
230+addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (veval ctxt [] ty)
204− tm (eval ctxt [] tm))) ctxt
231+ tm (veval ctxt [] tm))) ctxt
205
232
206addTyDecl :: Name -> Type -> Context -> Context
233addTyDecl :: Name -> Type -> Context -> Context
207−addTyDecl n ty ctxt = addDef n (TyDecl Ref ty (eval ctxt [] ty)) ctxt
234+addTyDecl n ty ctxt = addDef n (TyDecl Ref ty (veval ctxt [] ty)) ctxt
208
235
209addDatatype :: Datatype Name -> Context -> Context
236addDatatype :: Datatype Name -> Context -> Context
210addDatatype (Data n tag ty cons) ctxt
237addDatatype (Data n tag ty cons) ctxt
211 = let ty' = normalise ctxt [] ty in
238 = let ty' = normalise ctxt [] ty in
212 addCons 0 cons (addDef n
239 addCons 0 cons (addDef n
213− (TyDecl (TCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)
240+ (TyDecl (TCon tag (arity ty')) ty (veval ctxt [] ty)) ctxt)
214 where
241 where
215 addCons tag [] ctxt = ctxt
242 addCons tag [] ctxt = ctxt
216 addCons tag ((n, ty) : cons) ctxt
243 addCons tag ((n, ty) : cons) ctxt
217 = let ty' = normalise ctxt [] ty in
244 = let ty' = normalise ctxt [] ty in
218 addCons (tag+1) cons (addDef n
245 addCons (tag+1) cons (addDef n
219− (TyDecl (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)
246+ (TyDecl (DCon tag (arity ty')) ty (veval ctxt [] ty)) ctxt)
220
247
221addCasedef :: Name -> Bool -> [(Term, Term)] -> Type -> Context -> Context
248addCasedef :: Name -> Bool -> [(Term, Term)] -> Type -> Context -> Context
222addCasedef n tcase ps ty ctxt
249addCasedef n tcase ps ty ctxt
src/Core/TT.hs+14
@@ -77,6 +77,9 @@ showSep sep [] = ""
77showSep sep [x] = x
77showSep sep [x] = x
78showSep sep (x:xs) = x ++ sep ++ showSep sep xs
78showSep sep (x:xs) = x ++ sep ++ showSep sep xs
79
79
80+traceWhen True msg a = trace msg a
81+traceWhen False _ a = a
82+
80-- RAW TERMS ----------------------------------------------------------------
83-- RAW TERMS ----------------------------------------------------------------
81
84
82-- Names are hierarchies of strings, describing scope (so no danger of
85-- Names are hierarchies of strings, describing scope (so no danger of
@@ -137,6 +140,17 @@ data Binder b = Lam { binderTy :: b }
137 | PVTy { binderTy :: b }
140 | PVTy { binderTy :: b }
138 deriving (Show, Eq, Functor)
141 deriving (Show, Eq, Functor)
139
142
143+fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
144+fmapMB f (Let t v) = liftM2 Let (f t) (f v)
145+fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)
146+fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)
147+fmapMB f (Lam t) = liftM Lam (f t)
148+fmapMB f (Pi t) = liftM Pi (f t)
149+fmapMB f (Hole t) = liftM Hole (f t)
150+fmapMB f (GHole t) = liftM GHole (f t)
151+fmapMB f (PVar t) = liftM PVar (f t)
152+fmapMB f (PVTy t) = liftM PVTy (f t)
153+
140raw_apply :: Raw -> [Raw] -> Raw
154raw_apply :: Raw -> [Raw] -> Raw
141raw_apply f [] = f
155raw_apply f [] = f
142raw_apply f (a : as) = raw_apply (RApp f a) as
156raw_apply f (a : as) = raw_apply (RApp f a) as
src/Idris/AbsSyntax.hs+58−13
@@ -28,6 +28,7 @@ defaultOpts = IOption 0 False
28data IState = IState { tt_ctxt :: Context,
28data IState = IState { tt_ctxt :: Context,
29 idris_infixes :: [FixDecl],
29 idris_infixes :: [FixDecl],
30 idris_implicits :: Ctxt [PArg],
30 idris_implicits :: Ctxt [PArg],
31+ idris_statics :: Ctxt [Int],
31 idris_log :: String,
32 idris_log :: String,
32 idris_options :: IOption,
33 idris_options :: IOption,
33 idris_name :: Int,
34 idris_name :: Int,
@@ -38,7 +39,8 @@ data IState = IState { tt_ctxt :: Context,
38 idris_prims :: [(Name, ([E.Name], E.Term))]
39 idris_prims :: [(Name, ([E.Name], E.Term))]
39 }
40 }
40
41
41−idrisInit = IState emptyContext [] emptyContext "" defaultOpts 6 [] [] [] [] []
42+idrisInit = IState emptyContext [] emptyContext emptyContext
43+ "" defaultOpts 6 [] [] [] [] []
42
44
43-- The monad for the main REPL - reading and processing files and updating
45-- The monad for the main REPL - reading and processing files and updating
44-- global state (hence the IO inner monad).
46-- global state (hence the IO inner monad).
@@ -140,11 +142,19 @@ data FixDecl = Fix Fixity String
140instance Ord FixDecl where
142instance Ord FixDecl where
141 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
143 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
142
144
145+
146+data Static = Static | Dynamic
147+ deriving (Show, Eq)
148+
143-- Mark bindings with their explicitness, and laziness
149-- Mark bindings with their explicitness, and laziness
144−data Plicity = Imp Bool | Exp Bool deriving (Show, Eq)
150+data Plicity = Imp { plazy :: Bool,
151+ pstatic :: Static }
152+ | Exp { plazy :: Bool,
153+ pstatic :: Static }
154+ deriving (Show, Eq)
145
155
146−impl = Imp False
156+impl = Imp False Dynamic
147−expl = Exp False
157+expl = Exp False Dynamic
148
158
149data PDecl' t = PFix FC Fixity [String] -- fixity declaration
159data PDecl' t = PFix FC Fixity [String] -- fixity declaration
150 | PTy FC Name t -- type declaration
160 | PTy FC Name t -- type declaration
@@ -301,17 +311,24 @@ showImp impl tm = se 10 tm where
301 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
311 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
302 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
312 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
303 " in " ++ se 10 sc
313 " in " ++ se 10 sc
304− se p (PPi (Exp l) n ty sc)
314+ se p (PPi (Exp l s) n ty sc)
305 | n `elem` allNamesIn sc = bracket p 2 $
315 | n `elem` allNamesIn sc = bracket p 2 $
306 if l then "|(" else "(" ++
316 if l then "|(" else "(" ++
307 show n ++ " : " ++ se 10 ty ++
317 show n ++ " : " ++ se 10 ty ++
308− ") -> " ++ se 10 sc
318+ ") " ++ st ++
309− | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc
319+ "-> " ++ se 10 sc
310− se p (PPi (Imp l) n ty sc)
320+ | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
321+ where st = case s of
322+ Static -> "[static] "
323+ _ -> ""
324+ se p (PPi (Imp l s) n ty sc)
311 | impl = bracket p 2 $ if l then "|{" else "{" ++
325 | impl = bracket p 2 $ if l then "|{" else "{" ++
312 show n ++ " : " ++ se 10 ty ++
326 show n ++ " : " ++ se 10 ty ++
313− "} -> " ++ se 10 sc
327+ "} " ++ st ++ "-> " ++ se 10 sc
314 | otherwise = se 10 sc
328 | otherwise = se 10 sc
329+ where st = case s of
330+ Static -> "[static] "
331+ _ -> ""
315 se p (PApp _ (PRef _ f) [])
332 se p (PApp _ (PRef _ f) [])
316 | not impl = show f
333 | not impl = show f
317 se p (PApp _ (PRef _ op@(UN [f:_])) args)
334 se p (PApp _ (PRef _ op@(UN [f:_])) args)
@@ -461,13 +478,13 @@ implicitise syn ist tm
461 = do (decls, ns) <- get
478 = do (decls, ns) <- get
462 let isn = concatMap (namesIn ist) (map getTm as)
479 let isn = concatMap (namesIn ist) (map getTm as)
463 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
480 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
464− imps top env (PPi (Imp l) n ty sc)
481+ imps top env (PPi (Imp l _) n ty sc)
465 = do let isn = nub (namesIn ist ty) `dropAll` [n]
482 = do let isn = nub (namesIn ist ty) `dropAll` [n]
466 (decls , ns) <- get
483 (decls , ns) <- get
467 put (PImp l n ty : decls,
484 put (PImp l n ty : decls,
468 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
485 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
469 imps True (n:env) sc
486 imps True (n:env) sc
470− imps top env (PPi (Exp l) n ty sc)
487+ imps top env (PPi (Exp l _) n ty sc)
471 = do let isn = nub (namesIn ist ty ++ case sc of
488 = do let isn = nub (namesIn ist ty ++ case sc of
472 (PRef _ x) -> namesIn ist sc `dropAll` [n]
489 (PRef _ x) -> namesIn ist sc `dropAll` [n]
473 _ -> [])
490 _ -> [])
@@ -500,8 +517,8 @@ implicitise syn ist tm
500 pibind using [] sc = sc
517 pibind using [] sc = sc
501 pibind using (n:ns) sc
518 pibind using (n:ns) sc
502 = case lookup n using of
519 = case lookup n using of
503− Just ty -> PPi (Imp False) n ty (pibind using ns sc)
520+ Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
504− Nothing -> PPi (Imp False) n Placeholder (pibind using ns sc)
521+ Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
505
522
506-- Add implicit arguments in function calls
523-- Add implicit arguments in function calls
507
524
@@ -566,6 +583,34 @@ addImpl ist ptm = ai [] ptm
566 | n == n' = Just (t, reverse acc ++ gs)
583 | n == n' = Just (t, reverse acc ++ gs)
567 find n (g : gs) acc = find n gs (g : acc)
584 find n (g : gs) acc = find n gs (g : acc)
568
585
586+-- Find 'static' argument positions
587+-- (the declared ones, plus any names in argument position in the declared
588+-- statics)
589+-- FIXME: It's possible that this really has to happen after elaboration
590+
591+findStatics :: IState -> PTerm -> (PTerm, [Int])
592+findStatics ist tm = let (ns, ss) = fs tm in
593+ runState (pos 0 ns ss tm) []
594+ where fs (PPi p n t sc)
595+ | Static <- pstatic p
596+ = let (ns, ss) = fs sc in
597+ (namesIn ist t : ns, namesIn ist t ++ n : ss)
598+ | otherwise = let (ns, ss) = fs sc in
599+ (namesIn ist t : ns, ss)
600+ fs _ = ([], [])
601+
602+ inOne n ns = length (filter id (map (elem n) ns)) == 1
603+
604+ pos i ns ss (PPi p n t sc)
605+ | n `inOne` ns && elem n ss
606+ = do sc' <- pos i ns ss sc
607+ spos <- get
608+ put (i : spos)
609+ return (PPi (p { pstatic = Static }) n t sc')
610+ | otherwise = do sc' <- pos (i+1) ns ss sc
611+ return (PPi p n t sc')
612+ pos i ns ss t = return t
613+
569-- Debugging/logging stuff
614-- Debugging/logging stuff
570
615
571dumpDecls :: [PDecl] -> String
616dumpDecls :: [PDecl] -> String
src/Idris/Parser.hs+23−5
@@ -380,16 +380,26 @@ pLet syn = do reserved "let"; n <- pName; lchar '='; v <- pExpr syn
380 reserved "in"; sc <- pExpr syn
380 reserved "in"; sc <- pExpr syn
381 return (PLet n Placeholder v sc)
381 return (PLet n Placeholder v sc)
382
382
383−pPi syn = do lazy <- option False (do lchar '|'; return True)
383+pPi syn =
384+ try (do lazy <- option False (do lchar '|'; return True)
385+ st <- pStatic
384 lchar '('; xt <- tyDeclList syn; lchar ')'
386 lchar '('; xt <- tyDeclList syn; lchar ')'
385 symbol "->"
387 symbol "->"
386 sc <- pExpr syn
388 sc <- pExpr syn
387− return (bindList (PPi (Exp lazy)) xt sc)
389+ return (bindList (PPi (Exp lazy st)) xt sc))
388− <|> do lazy <- option False (do lchar '|'; return True)
390+ <|> try (do lazy <- option False (do lchar '|'; return True)
391+ st <- pStatic
389 lchar '{'; xt <- tyDeclList syn; lchar '}'
392 lchar '{'; xt <- tyDeclList syn; lchar '}'
390 symbol "->"
393 symbol "->"
391 sc <- pExpr syn
394 sc <- pExpr syn
392− return (bindList (PPi (Imp lazy)) xt sc)
395+ return (bindList (PPi (Imp lazy st)) xt sc))
396+ <|> do --lazy <- option False (do lchar '|'; return True)
397+ lchar '['; reserved "static"; lchar ']'
398+ t <- pExpr' syn
399+ symbol "->"
400+ sc <- pExpr syn
401+ return (PPi (Exp False Static) (MN 0 "X") t sc)
402+
393
403
394tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
404tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
395 (lchar ',')
405 (lchar ',')
@@ -428,6 +438,11 @@ pConstant = do reserved "Int"; return IType
428 <|> try (do s <- strlit; return $ Str s)
438 <|> try (do s <- strlit; return $ Str s)
429 <|> try (do c <- chlit; return $ Ch c)
439 <|> try (do c <- chlit; return $ Ch c)
430
440
441+pStatic :: IParser Static
442+pStatic = do lchar '['; reserved "static"; lchar ']';
443+ return Static
444+ <|> return Dynamic
445+
431table fixes
446table fixes
432 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN ["-"])) [pexp (PConstant (I 0)), pexp x])]]
447 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN ["-"])) [pexp (PConstant (I 0)), pexp x])]]
433 ++ toTable (reverse fixes) ++
448 ++ toTable (reverse fixes) ++
@@ -575,8 +590,11 @@ implicit :: SyntaxInfo -> Name -> PTerm -> IParser PTerm
575implicit syn n ptm
590implicit syn n ptm
576 = do i <- getState
591 = do i <- getState
577 let (tm', impdata) = implicitise syn i ptm
592 let (tm', impdata) = implicitise syn i ptm
593+ let (tm'', spos) = findStatics i tm'
578 setState (i { idris_implicits = addDef n impdata (idris_implicits i) })
594 setState (i { idris_implicits = addDef n impdata (idris_implicits i) })
579− return tm'
595+ i <- getState
596+ setState (i { idris_statics = addDef n spos (idris_statics i) })
597+ return tm''
580
598
581desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
599desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
582desugar syn i t = let t' = expandDo (dsl_info syn) t in
600desugar syn i t = let t' = expandDo (dsl_info syn) t in