3bdfa26 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added [static] annotations (which do nothing yet) and state to evaluator

commit3bdfa2697d52699021b01c9952473e0ae30a7a85 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 27 Oct 2011, 14:57 (15 years ago) parentb85965e

5 files changed+188−84

compare with master

unifiedsplit

interp.idr+1−1 src/Core/Evaluate.hs+92−65 src/Core/TT.hs+14 src/Idris/AbsSyntax.hs+58−13 src/Idris/Parser.hs+23−5

interp.idr+1−1

@@ -22,7 +22,7 @@ using (G : Vect Ty n) {

2222 | Add : Expr G TyNat -> Expr G TyNat -> Expr G TyNat

2323 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

2424

25− interp : Env G -> Expr G t -> interpTy t;

25+ interp : Env G -> [static] Expr G t -> interpTy t;

2626 interp env (Var i) = envLookup i env;

2727 interp env (Val x) = x;

2828 interp env (Lam sc) = \x => interp (Extend x env) sc;

src/Core/Evaluate.hs+92−65

@@ -8,22 +8,27 @@ module Core.Evaluate(normalise,

88 Value(..)) where

1010import Debug.Trace

11+import Control.Monad.State

1112

1213import Core.TT

1314import Core.CaseTree

1415

1516-- VALUES (as HOAS) ---------------------------------------------------------

1617

18+type EvalState = ()

19+type Eval a = State EvalState a

20+

1721data Value = VP NameType Name Value

1822 | VV Int

19− | VBind Name (Binder Value) (Value -> Value)

23+ | VBind Name (Binder Value) (Value -> Eval Value)

2024 | VApp Value Value

2125 | VSet Int

2226 | VConstant Const

2327 | VTmp Int

2428

2529instance Show Value where

26− show = show . quote 0

30+ show v = "<<Value>>"

31+

2732

2833-- THE EVALUATOR ------------------------------------------------------------

2934

@@ -33,7 +38,8 @@ instance Show Value where

3338-- while building a proof.

3439

3540normalise :: 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) ()

3743

3844-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))

3945

@@ -52,70 +58,85 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

5258-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,

5359-- such as we might have during construction of a proof)

5460

55−eval :: Context -> Env -> TT Name -> Value

61+eval :: Context -> Env -> TT Name -> Eval Value

5662eval ctxt genv tm = ev [] tm where

5763 ev env (P _ n ty)

5864 | Just (Let t v) <- lookup n genv = ev env v

5965 ev env (P Ref n ty) = case lookupDef n ctxt of

60− Just (Function (Fun _ _ _ v)) -> v

61− Just (TyDecl nt ty hty) -> VP nt n hty

66+ Just (Function (Fun _ _ _ v)) -> return v

67+ Just (TyDecl nt ty hty) -> return $ VP nt n hty

6268 Just (CaseOp _ _ [] tree) ->

63− case evCase env [] [] tree of

64− (Nothing, _) -> VP Ref n (ev env ty)

65− (Just v, _) -> v

66− _ -> VP Ref n (ev env ty)

67− ev env (P nt n ty) = VP nt n (ev env ty)

68− ev env (V i) | i < length env = env !! i

69− | otherwise = VV i --error $ "Internal error: V" ++ show i ++ " "

70− -- ++ showEnv genv tm ++ "\n" ++ show genv

69+ do c <- evCase env [] [] tree

70+ case c of

71+ (Nothing, _) -> liftM (VP Ref n) (ev env ty)

72+ (Just v, _) -> return v

73+ _ -> liftM (VP Ref n) (ev env ty)

74+ ev env (P nt n ty) = liftM (VP nt n) (ev env ty)

75+ ev env (V i) | i < length env = return $ env !! i

76+ | otherwise = return $ VV i

7177 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'

7381 ev env (Bind n (NLet t v) sc)

74− = VBind n (Let (ev env (finalise t)) (ev env (finalise v)))

75− $ (\x -> ev (ev env v : env) sc)

76− ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)

77− where vbind env t = fmap (\tm -> ev env (finalise tm)) t

78− ev env (App f a) = evApply env [ev env a] (ev env f)

79− ev env (Constant c) = VConstant c

80− ev env (Set i) = VSet i

82+ = do t' <- ev env (finalise t)

83+ v' <- ev env (finalise v)

84+ sc' <- ev (v' : env) sc

85+ return $ VBind n (Let t' v') (\x -> return sc')

86+ ev env (Bind n b sc)

87+ = do b' <- vbind env b

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

8195

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

8398 evApply env args f = apply env f args

8499

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

86103 apply env (VP Ref n ty) args

87104 | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt

88− = case evCase env ns args tree of

89− (Nothing, _) -> unload env (VP Ref n ty) args

105+ = do c <- evCase env ns args tree

106+ case c of

107+ (Nothing, _) -> return $ unload env (VP Ref n ty) args

90108 (Just v, rest) -> evApply env rest v

91109 | Just (Operator _ i op) <- lookupDef n ctxt

92110 = if (i <= length args)

93− then case op (take i args) of

94− Nothing -> unload env (VP Ref n ty) args

95− Just v -> evApply env (drop i args) v

96− else unload env (VP Ref n ty) args

97− apply env f (a:as) = unload env f (a:as)

98− apply env f [] = f

111+ then case op (take i args) of

112+ Nothing -> return $ unload env (VP Ref n ty) args

113+ Just v -> evApply env (drop i args) v

114+ else return $ unload env (VP Ref n ty) args

115+ apply env f (a:as) = return $ unload env f (a:as)

116+ apply env f [] = return f

99117

100118 unload env f [] = f

101119 unload env f (a:as) = unload env (VApp f a) as

102120

103121 evCase env ns args tree

104122 | length ns <= length args

105− = let args' = take (length ns) args

106− rest = drop (length ns) args in

107− (evTree env (zipWith (\n t -> (n, t)) ns args') tree, rest)

108− | otherwise = (Nothing, args)

109−

110− evTree :: [Value] -> [(Name, Value)] -> SC -> Maybe Value

111− evTree env amap (UnmatchedCase str) = Nothing

123+ = do let args' = take (length ns) args

124+ let rest = drop (length ns) args

125+ t <- evTree env (zipWith (\n t -> (n, t)) ns args') tree

126+ return (t, rest)

127+ | otherwise = return (Nothing, args)

128+

129+ evTree :: [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)

130+ evTree env amap (UnmatchedCase str) = return Nothing

112131 evTree env amap (STerm tm)

113− = let etm = pToVs (map fst amap) tm in

114− Just $ ev (map snd amap ++ env) etm

132+ = do let etm = pToVs (map fst amap) tm

133+ etm' <- ev (map snd amap ++ env) etm

134+ return $ Just etm'

115135 evTree env amap (Case n alts)

116− = do v <- lookup n amap

117− (altmap, sc) <- chooseAlt v (getValArgs v) alts amap

118− evTree env altmap sc

136+ = case (do v <- lookup n amap

137+ chooseAlt v (getValArgs v) alts amap) of

138+ Just (altmap, sc) -> evTree env altmap sc

139+ _ -> return Nothing

119140

120141 chooseAlt :: Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->

121142 Maybe ([(Name, Value)], SC)

@@ -156,22 +177,26 @@ eval ctxt genv tm = ev [] tm where

156177 getValArgs' (VApp f a) as = getValArgs' f (a:as)

157178 getValArgs' f as = (f, as)

158179

159−quote :: Int -> Value -> TT Name

160−quote i (VP nt n v) = P nt n (quote i v)

161−quote i (VV x) = V x

162−quote i (VBind n b sc) = Bind n (quoteB b) (quote (i+1) (sc (VTmp i)))

163− where quoteB t = fmap (quote i) t

164−quote i (VApp f a) = App (quote i f) (quote i a)

165−quote i (VSet u) = Set u

166−quote i (VConstant c) = Constant c

167−quote i (VTmp x) = V (i - x - 1)

168−

169−

170−wknV :: Int -> Value -> Value

171−wknV i (VV x) = VV (x + i)

172−wknV i (VBind n b sc) = VBind n (fmap (wknV i) b) (\x -> (wknV i (sc x)))

173−wknV i (VApp f a) = VApp (wknV i f) (wknV i a)

174−wknV i t = t

180+quote :: Int -> Value -> Eval (TT Name)

181+quote i (VP nt n v) = liftM (P nt n) (quote i v)

182+quote i (VV x) = return $ V x

183+quote i (VBind n b sc) = do sc' <- sc (VTmp i)

184+ b' <- quoteB b

185+ liftM (Bind n b') (quote (i+1) sc')

186+ where quoteB t = fmapMB (quote i) t

187+quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

188+quote i (VSet u) = return $ Set u

189+quote i (VConstant c) = return $ Constant c

190+quote i (VTmp x) = return $ V (i - x - 1)

191+

192+

193+wknV :: Int -> Value -> Eval Value

194+wknV i (VV x) = return $ VV (x + i)

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

175200

176201-- CONTEXTS -----------------------------------------------------------------

177202

@@ -199,24 +224,26 @@ instance Show Def where

199224

200225type Context = Ctxt Def

201226

227+veval ctxt env t = evalState (eval ctxt env t) ()

228+

202229addToCtxt :: Name -> Term -> Type -> Context -> Context

203−addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (eval ctxt [] ty)

204− tm (eval ctxt [] tm))) ctxt

230+addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (veval ctxt [] ty)

231+ tm (veval ctxt [] tm))) ctxt

205232

206233addTyDecl :: 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

208235

209236addDatatype :: Datatype Name -> Context -> Context

210237addDatatype (Data n tag ty cons) ctxt

211238 = let ty' = normalise ctxt [] ty in

212239 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)

214241 where

215242 addCons tag [] ctxt = ctxt

216243 addCons tag ((n, ty) : cons) ctxt

217244 = let ty' = normalise ctxt [] ty in

218245 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)

220247

221248addCasedef :: Name -> Bool -> [(Term, Term)] -> Type -> Context -> Context

222249addCasedef n tcase ps ty ctxt

src/Core/TT.hs+14

@@ -77,6 +77,9 @@ showSep sep [] = ""

7777showSep sep [x] = x

7878showSep sep (x:xs) = x ++ sep ++ showSep sep xs

7979

80+traceWhen True msg a = trace msg a

81+traceWhen False _ a = a

82+

8083-- RAW TERMS ----------------------------------------------------------------

8184

8285-- Names are hierarchies of strings, describing scope (so no danger of

@@ -137,6 +140,17 @@ data Binder b = Lam { binderTy :: b }

137140 | PVTy { binderTy :: b }

138141 deriving (Show, Eq, Functor)

139142

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+

140154raw_apply :: Raw -> [Raw] -> Raw

141155raw_apply f [] = f

142156raw_apply f (a : as) = raw_apply (RApp f a) as

src/Idris/AbsSyntax.hs+58−13

@@ -28,6 +28,7 @@ defaultOpts = IOption 0 False

2828data IState = IState { tt_ctxt :: Context,

2929 idris_infixes :: [FixDecl],

3030 idris_implicits :: Ctxt [PArg],

31+ idris_statics :: Ctxt [Int],

3132 idris_log :: String,

3233 idris_options :: IOption,

3334 idris_name :: Int,

@@ -38,7 +39,8 @@ data IState = IState { tt_ctxt :: Context,

3839 idris_prims :: [(Name, ([E.Name], E.Term))]

3940 }

4041

41−idrisInit = IState emptyContext [] emptyContext "" defaultOpts 6 [] [] [] [] []

42+idrisInit = IState emptyContext [] emptyContext emptyContext

43+ "" defaultOpts 6 [] [] [] [] []

4244

4345-- The monad for the main REPL - reading and processing files and updating

4446-- global state (hence the IO inner monad).

@@ -140,11 +142,19 @@ data FixDecl = Fix Fixity String

140142instance Ord FixDecl where

141143 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)

142144

145+

146+data Static = Static | Dynamic

147+ deriving (Show, Eq)

148+

143149-- 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)

145155

146−impl = Imp False

147−expl = Exp False

156+impl = Imp False Dynamic

157+expl = Exp False Dynamic

148158

149159data PDecl' t = PFix FC Fixity [String] -- fixity declaration

150160 | PTy FC Name t -- type declaration

@@ -301,17 +311,24 @@ showImp impl tm = se 10 tm where

301311 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc

302312 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++

303313 " in " ++ se 10 sc

304− se p (PPi (Exp l) n ty sc)

314+ se p (PPi (Exp l s) n ty sc)

305315 | n `elem` allNamesIn sc = bracket p 2 $

306316 if l then "|(" else "(" ++

307317 show n ++ " : " ++ se 10 ty ++

308− ") -> " ++ se 10 sc

309− | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc

310− se p (PPi (Imp l) n ty sc)

318+ ") " ++ st ++

319+ "-> " ++ se 10 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)

311325 | impl = bracket p 2 $ if l then "|{" else "{" ++

312326 show n ++ " : " ++ se 10 ty ++

313− "} -> " ++ se 10 sc

327+ "} " ++ st ++ "-> " ++ se 10 sc

314328 | otherwise = se 10 sc

329+ where st = case s of

330+ Static -> "[static] "

331+ _ -> ""

315332 se p (PApp _ (PRef _ f) [])

316333 | not impl = show f

317334 se p (PApp _ (PRef _ op@(UN [f:_])) args)

@@ -461,13 +478,13 @@ implicitise syn ist tm

461478 = do (decls, ns) <- get

462479 let isn = concatMap (namesIn ist) (map getTm as)

463480 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)

465482 = do let isn = nub (namesIn ist ty) `dropAll` [n]

466483 (decls , ns) <- get

467484 put (PImp l n ty : decls,

468485 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

469486 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)

471488 = do let isn = nub (namesIn ist ty ++ case sc of

472489 (PRef _ x) -> namesIn ist sc `dropAll` [n]

473490 _ -> [])

@@ -500,8 +517,8 @@ implicitise syn ist tm

500517 pibind using [] sc = sc

501518 pibind using (n:ns) sc

502519 = case lookup n using of

503− Just ty -> PPi (Imp False) n ty (pibind using ns sc)

504− Nothing -> PPi (Imp False) n Placeholder (pibind using ns sc)

520+ Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)

521+ Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)

505522

506523-- Add implicit arguments in function calls

507524

@@ -566,6 +583,34 @@ addImpl ist ptm = ai [] ptm

566583 | n == n' = Just (t, reverse acc ++ gs)

567584 find n (g : gs) acc = find n gs (g : acc)

568585

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+

569614-- Debugging/logging stuff

570615

571616dumpDecls :: [PDecl] -> String

src/Idris/Parser.hs+23−5

@@ -380,16 +380,26 @@ pLet syn = do reserved "let"; n <- pName; lchar '='; v <- pExpr syn

380380 reserved "in"; sc <- pExpr syn

381381 return (PLet n Placeholder v sc)

382382

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

384386 lchar '('; xt <- tyDeclList syn; lchar ')'

385387 symbol "->"

386388 sc <- pExpr syn

387− return (bindList (PPi (Exp lazy)) xt sc)

388− <|> do lazy <- option False (do lchar '|'; return True)

389+ return (bindList (PPi (Exp lazy st)) xt sc))

390+ <|> try (do lazy <- option False (do lchar '|'; return True)

391+ st <- pStatic

389392 lchar '{'; xt <- tyDeclList syn; lchar '}'

390393 symbol "->"

391394 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+

393403

394404tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))

395405 (lchar ',')

@@ -428,6 +438,11 @@ pConstant = do reserved "Int"; return IType

428438 <|> try (do s <- strlit; return $ Str s)

429439 <|> try (do c <- chlit; return $ Ch c)

430440

441+pStatic :: IParser Static

442+pStatic = do lchar '['; reserved "static"; lchar ']';

443+ return Static

444+ <|> return Dynamic

445+

431446table fixes

432447 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN ["-"])) [pexp (PConstant (I 0)), pexp x])]]

433448 ++ toTable (reverse fixes) ++

@@ -575,8 +590,11 @@ implicit :: SyntaxInfo -> Name -> PTerm -> IParser PTerm

575590implicit syn n ptm

576591 = do i <- getState

577592 let (tm', impdata) = implicitise syn i ptm

593+ let (tm'', spos) = findStatics i tm'

578594 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''

580598

581599desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

582600desugar syn i t = let t' = expandDo (dsl_info syn) t in