git.iko.soy/Idris-dev
on master help sign in
Some progress towards specialisation
7c4f79cEdwin Brady
interp.idr+41−24
compare with master
unifiedsplit
@@ -1,7 +1,8 @@
1−data Ty = TyNat | TyFun Ty Ty;
1+data Ty = TyInt | TyBool| TyFun Ty Ty;
2
2
3interpTy : Ty -> Set;
3interpTy : Ty -> Set;
4−interpTy TyNat = Nat;
4+interpTy TyInt = Int;
5+interpTy TyBool = Bool;
5interpTy (TyFun s t) = interpTy s -> interpTy t;
6interpTy (TyFun s t) = interpTy s -> interpTy t;
6
7
7using (G : Vect Ty n) {
8using (G : Vect Ty n) {
@@ -16,32 +17,45 @@ using (G : Vect Ty n) {
16
17
17 data Expr : Vect Ty n -> Ty -> Set where
18 data Expr : Vect Ty n -> Ty -> Set where
18 Var : (i : Fin n) -> Expr G (vlookup i G)
19 Var : (i : Fin n) -> Expr G (vlookup i G)
19− | Val : Nat -> Expr G TyNat
20+ | Val : (x : interpTy a) -> Expr G a
20 | Lam : Expr (a :: G) t -> Expr G (TyFun a t)
21 | Lam : Expr (a :: G) t -> Expr G (TyFun a t)
21 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t
22 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t
23+ | Op : (Int -> Int -> interpTy c) ->
24+ Expr G TyInt -> Expr G TyInt -> Expr G c
22− | Add : Expr G TyNat -> Expr G TyNat -> Expr G TyNat
25+ | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
23 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
26 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
24
27
25 interp : Env G -> [static] Expr G t -> interpTy t;
28 interp : Env G -> [static] Expr G t -> interpTy t;
26− interp env (Var i) = envLookup i env;
29+ interp env (Var i) = envLookup i env;
27− interp env (Val x) = x;
30+ interp env (Val x) = x;
28− interp env (Lam sc) = \x => interp (Extend x env) sc;
31+ interp env (Lam sc) = \x => interp (Extend x env) sc;
29− interp env (App f s) = (interp env f) (interp env s);
32+ interp env (App f s) = (interp env f) (interp env s);
33+ interp env (Op op x y) = op (interp env x) (interp env y);
30− interp env (Add x y) = plus (interp env x) (interp env y);
34+ interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);
31− interp env (Bind v f) = interp env (f (interp env v));
35+ interp env (Bind v f) = interp env (f (interp env v));
36+
37+ eId : Expr G (TyFun TyInt TyInt);
38+ eId = Lam (Var fO);
39+
40+ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));
41+ eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));
32
42
33− eAdd : Expr G (TyFun TyNat (TyFun TyNat TyNat));
43+ eDouble : Expr G (TyFun TyInt TyInt);
34− eAdd = Lam (Lam (Add (Var fO) (Var (fS fO))));
44+ eDouble = Lam (App (App (Lam (Lam (Op (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));
35
45
36− eDouble : Expr G (TyFun TyNat TyNat);
46+ eDouble' : Expr G (TyFun TyInt TyInt);
37− eDouble = Lam (App (App (Lam (Lam (Add (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));
38−
39− eDouble' : Expr G (TyFun TyNat TyNat);
40 eDouble' = Lam (App (App eAdd (Var fO)) (Var fO));
47 eDouble' = Lam (App (App eAdd (Var fO)) (Var fO));
41−
48+
49+ app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;
50+ app = \f, a => App f a;
51+
52+ eFac : Expr G (TyFun TyInt TyInt);
53+ eFac = Lam (If (Op (==) (Var fO) (Val 0))
54+ (Val 1) (Op (*) (app eFac (Op (-) (Var fO) (Val 1))) (Var fO)));
55+
42 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
56 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
43
57
44− eProg : Expr G (TyFun TyNat (TyFun TyNat TyNat));
58+ eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt));
45 eProg = Lam (Lam
59 eProg = Lam (Lam
46 (Bind (App eDouble (Var (fS fO)))
60 (Bind (App eDouble (Var (fS fO)))
47 (\x => Bind (App eDouble (Var fO))
61 (\x => Bind (App eDouble (Var fO))
@@ -49,13 +63,16 @@ using (G : Vect Ty n) {
49 (\z => App (App eAdd (Val y)) (Val z))))));
63 (\z => App (App eAdd (Val y)) (Val z))))));
50}
64}
51
65
52−test : Nat;
66+test : Int;
53−test = interp Empty eProg (S (S O)) (S (S O));
67+test = interp Empty eProg 2 2;
68+
69+testFac : Int;
70+testFac = interp Empty eFac 3;
54
71
55−natToStr : Nat -> String;
72+intToStr : Int -> String;
56−natToStr O = "O";
73+intToStr 0 = "O";
57−natToStr (S k) = "s" ++ natToStr k;
74+intToStr n = "s" ++ intToStr (n - 1);
58
75
59main : IO ();
76main : IO ();
60−main = putStrLn (natToStr test);
77+main = putStrLn (intToStr testFac);
61
78
src/Core/Elaborate.hs+2−1
@@ -27,7 +27,8 @@ data Command = Theorem Name Raw
27 | Print Name
27 | Print Name
28 | Tac (Elab ())
28 | Tac (Elab ())
29
29
30−type Elab a = StateT (ProofState, String) TC a
30+type ElabState = (ProofState, String)
31+type Elab a = StateT ElabState TC a
31
32
32erun :: FC -> Elab a -> Elab a
33erun :: FC -> Elab a -> Elab a
33erun f elab = do s <- get
34erun f elab = do s <- get
src/Core/Evaluate.hs+280−82
@@ -1,7 +1,7 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
2 PatternGuards #-}
2 PatternGuards #-}
3
3
4−module Core.Evaluate(normalise,
4+module Core.Evaluate(normalise, specialise, hnf,
5 Fun(..), Def(..), Context,
5 Fun(..), Def(..), Context,
6 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,
6 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,
7 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,
7 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,
@@ -13,11 +13,14 @@ import Control.Monad.State
13import Core.TT
13import Core.TT
14import Core.CaseTree
14import Core.CaseTree
15
15
16−-- VALUES (as HOAS) ---------------------------------------------------------
17−
18type EvalState = ()
16type EvalState = ()
19type Eval a = State EvalState a
17type Eval a = State EvalState a
20
18
19+data EvalOpt = Spec | HNF
20+ deriving (Show, Eq)
21+
22+-- VALUES (as HOAS) ---------------------------------------------------------
23+
21data Value = VP NameType Name Value
24data Value = VP NameType Name Value
22 | VV Int
25 | VV Int
23 | VBind Name (Binder Value) (Value -> Eval Value)
26 | VBind Name (Binder Value) (Value -> Eval Value)
@@ -26,9 +29,20 @@ data Value = VP NameType Name Value
26 | VConstant Const
29 | VConstant Const
27 | VTmp Int
30 | VTmp Int
28
31
32+data HNF = HP NameType Name (TT Name)
33+ | HV Int
34+ | HBind Name (Binder HNF) (HNF -> Eval HNF)
35+ | HApp HNF [HNF] [TT Name]
36+ | HSet Int
37+ | HConstant Const
38+ | HTmp Int
39+ deriving Show
40+
29instance Show Value where
41instance Show Value where
30− show v = "<<Value>>"
42+ show x = show $ evalState (quote 10 x) ()
31
43
44+instance Show (a -> b) where
45+ show x = "<<fn>>"
32
46
33-- THE EVALUATOR ------------------------------------------------------------
47-- THE EVALUATOR ------------------------------------------------------------
34
48
@@ -38,8 +52,20 @@ instance Show Value where
38-- while building a proof.
52-- while building a proof.
39
53
40normalise :: Context -> Env -> TT Name -> TT Name
54normalise :: Context -> Env -> TT Name -> TT Name
55+normalise ctxt env t
41−normalise ctxt env t = evalState (do val <- eval ctxt (map finalEntry env) (finalise t)
56+ = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) []
42− quote 0 val) ()
57+ quote 0 val) ()
58+
59+specialise :: Context -> Ctxt [Bool] -> TT Name -> TT Name
60+specialise ctxt statics t
61+ = evalState (do val <- eval ctxt statics [] (finalise t) [Spec]
62+ quote 0 val) ()
63+
64+hnf :: Context -> Env -> TT Name -> TT Name
65+hnf ctxt env t
66+ = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [HNF]
67+ quote 0 val) ()
68+
43
69
44-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
70-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
45
71
@@ -58,98 +84,113 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
58-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
84-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
59-- such as we might have during construction of a proof)
85-- such as we might have during construction of a proof)
60
86
61−eval :: Context -> Env -> TT Name -> Eval Value
87+eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value
62−eval ctxt genv tm = ev [] tm where
88+eval ctxt statics genv tm opts = ev True [] tm where
89+ spec = Spec `elem` opts
90+
63− ev env (P _ n ty)
91+ ev top env (P _ n ty)
64− | Just (Let t v) <- lookup n genv = ev env v
92+ | Just (Let t v) <- lookup n genv = ev top env v
65− ev env (P Ref n ty) = case lookupDef n ctxt of
93+ ev top env (P Ref n ty) = case lookupDef n ctxt of
66 Just (Function (Fun _ _ _ v)) -> return v
94 Just (Function (Fun _ _ _ v)) -> return v
67 Just (TyDecl nt ty hty) -> return $ VP nt n hty
95 Just (TyDecl nt ty hty) -> return $ VP nt n hty
68 Just (CaseOp _ _ [] tree) ->
96 Just (CaseOp _ _ [] tree) ->
69− do c <- evCase env [] [] tree
97+ do c <- evCase top env [] [] tree
70 case c of
98 case c of
71− (Nothing, _) -> liftM (VP Ref n) (ev env ty)
99+ (Nothing, _) -> liftM (VP Ref n) (ev top env ty)
72 (Just v, _) -> return v
100 (Just v, _) -> return v
73− _ -> liftM (VP Ref n) (ev env ty)
101+ _ -> liftM (VP Ref n) (ev top env ty)
74− ev env (P nt n ty) = liftM (VP nt n) (ev env ty)
102+ ev top env (P nt n ty) = liftM (VP nt n) (ev top env ty)
75− ev env (V i) | i < length env = return $ env !! i
103+ ev top env (V i) | i < length env = return $ env !! i
76− | otherwise = return $ VV i
104+ | otherwise = return $ VV i
77− ev env (Bind n (Let t v) sc)
105+ ev top env (Bind n (Let t v) sc)
78− = do v' <- ev env (finalise v)
106+ = do v' <- ev top env (finalise v)
79− sc' <- ev (v' : env) sc
107+ sc' <- ev top (v' : env) sc
80 wknV (-1) sc'
108 wknV (-1) sc'
81− ev env (Bind n (NLet t v) sc)
109+ ev top env (Bind n (NLet t v) sc)
82− = do t' <- ev env (finalise t)
110+ = do t' <- ev top env (finalise t)
83− v' <- ev env (finalise v)
111+ v' <- ev top env (finalise v)
84− sc' <- ev (v' : env) sc
112+ sc' <- ev top (v' : env) sc
85 return $ VBind n (Let t' v') (\x -> return sc')
113 return $ VBind n (Let t' v') (\x -> return sc')
86− ev env (Bind n b sc)
114+ ev top env (Bind n b sc)
87 = do b' <- vbind env b
115 = do b' <- vbind env b
88− return $ VBind n b' (\x -> ev (x:env) sc)
116+ return $ VBind n b' (\x -> ev top (x:env) sc)
89− where vbind env t = fmapMB (\tm -> ev env (finalise tm)) t
117+ where vbind env t = fmapMB (\tm -> ev top env (finalise tm)) t
90− ev env (App f a) = do f' <- ev env f
118+ ev top env (App f a) = do f' <- ev top env f
91− a' <- ev env a
119+ a' <- ev False env a
92− evApply env [a'] f'
120+ evApply top env [a'] f'
93− ev env (Constant c) = return $ VConstant c
121+ ev top env (Constant c) = return $ VConstant c
94− ev env (Set i) = return $ VSet i
122+ ev top env (Set i) = return $ VSet i
95
123
96− evApply env args (VApp f a) =
124+ evApply top env args (VApp f a) =
97− evApply env (a:args) f
125+ evApply top env (a:args) f
98− evApply env args f = apply env f args
126+ evApply top env args f = apply top env f args
99−
127+
100− apply env (VBind n (Lam t) sc) (a:as) = do a' <- sc a
128+ apply top env (VBind n (Lam t) sc) (a:as)
129+ = do a' <- sc a
101− app <- apply env a' as
130+ app <- apply top env a' as
102− wknV (-1) app
131+ wknV (-1) app
132+ apply False env f args
133+ | spec = return $ unload env f args
103− apply env (VP Ref n ty) args
134+ apply top env (VP Ref n ty) args
104 | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt
135 | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt
136+ = -- traceWhen (n == UN ["interp"]) (show (n, args)) $
105− = do c <- evCase env ns args tree
137+ do c <- evCase top env ns args tree
106 case c of
138 case c of
107 (Nothing, _) -> return $ unload env (VP Ref n ty) args
139 (Nothing, _) -> return $ unload env (VP Ref n ty) args
108− (Just v, rest) -> evApply env rest v
140+ (Just v, rest) -> evApply top env rest v
109 | Just (Operator _ i op) <- lookupDef n ctxt
141 | Just (Operator _ i op) <- lookupDef n ctxt
110 = if (i <= length args)
142 = if (i <= length args)
111 then case op (take i args) of
143 then case op (take i args) of
112 Nothing -> return $ unload env (VP Ref n ty) args
144 Nothing -> return $ unload env (VP Ref n ty) args
113− Just v -> evApply env (drop i args) v
145+ Just v -> evApply top env (drop i args) v
114 else return $ unload env (VP Ref n ty) args
146 else return $ unload env (VP Ref n ty) args
115− apply env f (a:as) = return $ unload env f (a:as)
147+ apply top env f (a:as) = return $ unload env f (a:as)
116− apply env f [] = return f
148+ apply top env f [] = return f
117
149
118 unload env f [] = f
150 unload env f [] = f
119 unload env f (a:as) = unload env (VApp f a) as
151 unload env f (a:as) = unload env (VApp f a) as
120
152
121− evCase env ns args tree
153+ evCase top env ns args tree
122 | length ns <= length args
154 | length ns <= length args
123 = do let args' = take (length ns) args
155 = do let args' = take (length ns) args
124 let rest = drop (length ns) args
156 let rest = drop (length ns) args
125− t <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
157+ t <- evTree top env (zipWith (\n t -> (n, t)) ns args') tree
126 return (t, rest)
158 return (t, rest)
127 | otherwise = return (Nothing, args)
159 | otherwise = return (Nothing, args)
128
160
129− evTree :: [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
161+ evTree :: Bool -> [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
130− evTree env amap (UnmatchedCase str) = return Nothing
162+ evTree top env amap (UnmatchedCase str) = return Nothing
131− evTree env amap (STerm tm)
163+ evTree top env amap (STerm tm)
132 = do let etm = pToVs (map fst amap) tm
164 = do let etm = pToVs (map fst amap) tm
133− etm' <- ev (map snd amap ++ env) etm
165+ etm' <- ev top (map snd amap ++ env) etm
134 return $ Just etm'
166 return $ Just etm'
135− evTree env amap (Case n alts)
167+ evTree top env amap (Case n alts)
136− = case (do v <- lookup n amap
168+ = case lookup n amap of
137− chooseAlt v (getValArgs v) alts amap) of
169+ Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
170+ case c of
171+ Just (altmap, sc) -> evTree top env altmap sc
172+ _ -> do c' <- chooseAlt' env v (getValArgs v) alts amap
173+ case c' of
138− Just (altmap, sc) -> evTree env altmap sc
174+ Just (altmap, sc) -> evTree top env altmap sc
175+ _ -> return Nothing
139− _ -> return Nothing
176+ _ -> return Nothing
140−
177+
178+ chooseAlt' env _ (f, args) alts amap
179+ = do f' <- apply True env f args
180+ chooseAlt env f' (getValArgs f') alts amap
181+
141− chooseAlt :: Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
182+ chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
142− Maybe ([(Name, Value)], SC)
183+ Eval (Maybe ([(Name, Value)], SC))
143− chooseAlt _ (VP (DCon i a) _ _, args) alts amap
184+ chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
144− | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
185+ | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
145− | Just v <- findDefault alts = Just (amap, v)
186+ | Just v <- findDefault alts = return $ Just (amap, v)
146− chooseAlt _ (VP (TCon i a) _ _, args) alts amap
187+ chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
147− | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
188+ | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
148− | Just v <- findDefault alts = Just (amap, v)
189+ | Just v <- findDefault alts = return $ Just (amap, v)
149− chooseAlt _ (VConstant c, []) alts amap
190+ chooseAlt env _ (VConstant c, []) alts amap
150− | Just v <- findConst c alts = Just (amap, v)
191+ | Just v <- findConst c alts = return $ Just (amap, v)
151− | Just v <- findDefault alts = Just (amap, v)
192+ | Just v <- findDefault alts = return $ Just (amap, v)
152− chooseAlt _ _ _ _ = Nothing
193+ chooseAlt _ _ _ _ _ = return Nothing
153
194
154 -- Replace old variable names in the map with new matches
195 -- Replace old variable names in the map with new matches
155 -- (This is possibly unnecessary since we make unique names and don't
196 -- (This is possibly unnecessary since we make unique names and don't
@@ -177,18 +218,37 @@ eval ctxt genv tm = ev [] tm where
177 getValArgs' (VApp f a) as = getValArgs' f (a:as)
218 getValArgs' (VApp f a) as = getValArgs' f (a:as)
178 getValArgs' f as = (f, as)
219 getValArgs' f as = (f, as)
179
220
221+class Quote a where
180−quote :: Int -> Value -> Eval (TT Name)
222+ quote :: Int -> a -> Eval (TT Name)
223+
224+instance Quote Value where
181−quote i (VP nt n v) = liftM (P nt n) (quote i v)
225+ quote i (VP nt n v) = liftM (P nt n) (quote i v)
182−quote i (VV x) = return $ V x
226+ quote i (VV x) = return $ V x
183−quote i (VBind n b sc) = do sc' <- sc (VTmp i)
227+ quote i (VBind n b sc) = do sc' <- sc (VTmp i)
184− b' <- quoteB b
228+ b' <- quoteB b
185− liftM (Bind n b') (quote (i+1) sc')
229+ liftM (Bind n b') (quote (i+1) sc')
186− where quoteB t = fmapMB (quote i) t
230+ where quoteB t = fmapMB (quote i) t
187−quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
231+ quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
188−quote i (VSet u) = return $ Set u
232+ quote i (VSet u) = return $ Set u
189−quote i (VConstant c) = return $ Constant c
233+ quote i (VConstant c) = return $ Constant c
190−quote i (VTmp x) = return $ V (i - x - 1)
234+ quote i (VTmp x) = return $ V (i - x - 1)
191−
235+
236+instance Quote HNF where
237+ quote i (HP nt n t) = return (P nt n t)
238+ quote i (HV x) = return $ V x
239+ quote i (HBind n b sc) = do sc' <- sc (HTmp i)
240+ b' <- quoteB b
241+ liftM (Bind n b') (quote (i+1) sc')
242+ where quoteB t = fmapMB (quote i) t
243+ quote i (HApp f env as) = do f' <- quote i f
244+ as' <- mapM (iEnv env) as
245+ return $ mkApp f' as'
246+ where iEnv [] a = return a
247+ iEnv (x:xs) a = do x' <- quote i x
248+ iEnv xs (weakenTm (-1) (instantiate x' a))
249+ quote i (HSet u) = return $ Set u
250+ quote i (HConstant c) = return $ Constant c
251+ quote i (HTmp x) = return $ V (i - x - 1)
192
252
193wknV :: Int -> Value -> Eval Value
253wknV :: Int -> Value -> Eval Value
194wknV i (VV x) = return $ VV (x + i)
254wknV i (VV x) = return $ VV (x + i)
@@ -198,6 +258,144 @@ wknV i (VBind n b sc) = do b' <- fmapMB (wknV i) b
198wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
258wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
199wknV i t = return t
259wknV i t = return t
200
260
261+wknH :: Int -> HNF -> Eval HNF
262+wknH i (HV x) = return $ HV (x + i)
263+wknH i (HBind n b sc) = do b' <- fmapMB (wknH i) b
264+ return $ HBind n b' (\x -> do x' <- sc x
265+ wknH i x')
266+wknH i (HApp f env as) = liftM3 HApp (wknH i f) (return env)
267+ (return as)
268+wknH i t = return t
269+
270+-- HEAD NORMAL FORM ---------------------------------------------------------
271+
272+eval_hnf :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval HNF
273+eval_hnf ctxt statics genv tm = ev [] tm where
274+ ev :: [HNF] -> TT Name -> Eval HNF
275+ ev env (P _ n ty)
276+ | Just (Let t v) <- lookup n genv = ev env v
277+ ev env (P Ref n ty) = case lookupDef n ctxt of
278+ Just (Function (Fun _ _ t _)) -> ev env t
279+ Just (TyDecl nt ty hty) -> return $ HP nt n ty
280+ Just (CaseOp _ _ [] tree) ->
281+ do c <- evCase env [] [] tree
282+ case c of
283+ (Nothing, _, _) -> return $ HP Ref n ty
284+ (Just v, _, _) -> return v
285+ _ -> return $ HP Ref n ty
286+ ev env (P nt n ty) = return $ HP nt n ty
287+ ev env (V i) | i < length env = return $ env !! i
288+ | otherwise = return $ HV i
289+ ev env (Bind n (Let t v) sc)
290+ = do v' <- ev env (finalise v)
291+ sc' <- ev (v' : env) sc
292+ wknH (-1) sc'
293+ ev env (Bind n b sc)
294+ = do b' <- hbind env b
295+ return $ HBind n b' (\x -> ev (x : env) sc)
296+ where hbind env t = fmapMB (\tm -> ev env (finalise tm)) t
297+ ev env (App f a) = evApply env [a] f
298+ ev env (Constant c) = return $ HConstant c
299+ ev env (Set i) = return $ HSet i
300+
301+ evApply env args (App f a) = evApply env (a : args) f
302+ evApply env args f = do f' <- ev env f
303+ apply env f' args
304+
305+ apply env (HBind n (Lam t) sc) (a:as) = do a' <- ev env a
306+ sc' <- sc a'
307+ app <- apply env sc' as
308+ wknH (-1) app
309+ apply env (HP Ref n ty) args
310+ | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt
311+ = do c <- evCase env ns args tree
312+ case c of
313+ (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
314+ (Just v, rest, env') -> do v' <- quote 0 v
315+ apply env' v rest
316+-- | Just (Operator _ i op) <- lookupDef n ctxt
317+-- = if (i <= length args)
318+-- then case op (take i args) of
319+-- Nothing -> return $ unload env (HP Ref n ty) args
320+-- Just v -> evApply env (drop i args) v
321+-- else return $ unload env (HP Ref n ty) args
322+ apply env f (a:as) = return $ unload env f (a:as)
323+ apply env f [] = return f
324+
325+ unload env f [] = f
326+ unload env f as = HApp f env as
327+
328+ evCase env ns args tree
329+ | length ns <= length args
330+ = do let args' = take (length ns) args
331+ let rest = drop (length ns) args
332+ (t, env') <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
333+ return (t, rest, env')
334+ | otherwise = return (Nothing, args, env)
335+
336+ evTree :: [HNF] -> [(Name, TT Name)] -> SC -> Eval (Maybe HNF, [HNF])
337+ evTree env amap (UnmatchedCase str) = return (Nothing, env)
338+ evTree env amap (STerm tm)
339+ = do let etm = pToVs (map fst amap) tm
340+ amap' <- mapM (ev env) (map snd amap)
341+ envw <- mapM (wknH (length amap)) env
342+ let env' = amap' ++ envw
343+ etm' <- trace (show etm) $ ev env' etm
344+ etmq <- quote 0 etm'
345+ trace ("Ev: " ++ show (etm, etmq)) $ return $ (Just etm', env')
346+ evTree env amap (Case n alts)
347+ = case lookup n amap of
348+ Just v -> do v' <- ev env v
349+ case chooseAlt v' (getValArgs v') alts amap of
350+ Just (altmap, sc) -> evTree env altmap sc
351+ _ -> return (Nothing, env)
352+
353+ chooseAlt :: HNF -> (HNF, [HNF], [TT Name]) ->
354+ [CaseAlt] -> [(Name, TT Name)] ->
355+ Maybe ([(Name, TT Name)], SC)
356+ chooseAlt _ (HP (DCon i a) _ _, env, args) alts amap
357+ | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
358+ | Just v <- findDefault alts = Just (amap, v)
359+ chooseAlt _ (HP (TCon i a) _ _, env, args) alts amap
360+ | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
361+ | Just v <- findDefault alts = Just (amap, v)
362+ chooseAlt _ (HConstant c, env, []) alts amap
363+ | Just v <- findConst c alts = Just (amap, v)
364+ | Just v <- findDefault alts = Just (amap, v)
365+ chooseAlt _ _ _ _ = Nothing
366+
367+ -- Replace old variable names in the map with new matches
368+ -- (This is possibly unnecessary since we make unique names and don't
369+ -- allow repeated variables...?)
370+ updateAmap newm amap
371+ = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
372+ findTag i [] = Nothing
373+ findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
374+ findTag i (_ : xs) = findTag i xs
375+
376+ findDefault [] = Nothing
377+ findDefault (DefaultCase sc : xs) = Just sc
378+ findDefault (_ : xs) = findDefault xs
379+
380+ findConst c [] = Nothing
381+ findConst c (ConstCase c' v : xs) | c == c' = Just v
382+ findConst IType (ConCase n 1 [] v : xs) = Just v
383+ findConst FlType (ConCase n 2 [] v : xs) = Just v
384+ findConst ChType (ConCase n 3 [] v : xs) = Just v
385+ findConst StrType (ConCase n 4 [] v : xs) = Just v
386+ findConst PtrType (ConCase n 5 [] v : xs) = Just v
387+ findConst c (_ : xs) = findConst c xs
388+
389+ getValArgs (HApp t env args) = (t, env, args)
390+ getValArgs t = (t, [], [])
391+
392+-- SPECIALISATION -----------------------------------------------------------
393+-- We need too much control to be able to do this by tweaking the main
394+-- evaluator
395+
396+spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
397+spec ctxt statics genv tm = undefined
398+
201-- CONTEXTS -----------------------------------------------------------------
399-- CONTEXTS -----------------------------------------------------------------
202
400
203data Fun = Fun Type Value Term Value
401data Fun = Fun Type Value Term Value
@@ -224,7 +422,7 @@ instance Show Def where
224
422
225type Context = Ctxt Def
423type Context = Ctxt Def
226
424
227−veval ctxt env t = evalState (eval ctxt env t) ()
425+veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()
228
426
229addToCtxt :: Name -> Term -> Type -> Context -> Context
427addToCtxt :: Name -> Term -> Type -> Context -> Context
230addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (veval ctxt [] ty)
428addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (veval ctxt [] ty)
src/Idris/AbsSyntax.hs+12−9
@@ -5,6 +5,7 @@ module Idris.AbsSyntax where
5
5
6import Core.TT
6import Core.TT
7import Core.Evaluate
7import Core.Evaluate
8+import Core.Elaborate
8
9
9import Control.Monad.State
10import Control.Monad.State
10import Data.List
11import Data.List
@@ -28,7 +29,7 @@ defaultOpts = IOption 0 False
28data IState = IState { tt_ctxt :: Context,
29data IState = IState { tt_ctxt :: Context,
29 idris_infixes :: [FixDecl],
30 idris_infixes :: [FixDecl],
30 idris_implicits :: Ctxt [PArg],
31 idris_implicits :: Ctxt [PArg],
31− idris_statics :: Ctxt [Int],
32+ idris_statics :: Ctxt [Bool],
32 idris_log :: String,
33 idris_log :: String,
33 idris_options :: IOption,
34 idris_options :: IOption,
34 idris_name :: Int,
35 idris_name :: Int,
@@ -119,7 +120,7 @@ data Command = Quit | Help | Eval PTerm
119 | Compile String
120 | Compile String
120 | Metavars
121 | Metavars
121 | TTShell
122 | TTShell
122− | LogLvl Int
123+ | LogLvl Int | Spec PTerm | HNF PTerm
123 | NOP
124 | NOP
124
125
125-- Parsed declarations
126-- Parsed declarations
@@ -588,9 +589,9 @@ addImpl ist ptm = ai [] ptm
588-- statics)
589-- statics)
589-- FIXME: It's possible that this really has to happen after elaboration
590-- FIXME: It's possible that this really has to happen after elaboration
590
591
591−findStatics :: IState -> PTerm -> (PTerm, [Int])
592+findStatics :: IState -> PTerm -> (PTerm, [Bool])
592findStatics ist tm = let (ns, ss) = fs tm in
593findStatics ist tm = let (ns, ss) = fs tm in
593− runState (pos 0 ns ss tm) []
594+ runState (pos ns ss tm) []
594 where fs (PPi p n t sc)
595 where fs (PPi p n t sc)
595 | Static <- pstatic p
596 | Static <- pstatic p
596 = let (ns, ss) = fs sc in
597 = let (ns, ss) = fs sc in
@@ -601,15 +602,17 @@ findStatics ist tm = let (ns, ss) = fs tm in
601
602
602 inOne n ns = length (filter id (map (elem n) ns)) == 1
603 inOne n ns = length (filter id (map (elem n) ns)) == 1
603
604
604− pos i ns ss (PPi p n t sc)
605+ pos ns ss (PPi p n t sc)
605 | n `inOne` ns && elem n ss
606 | n `inOne` ns && elem n ss
606− = do sc' <- pos i ns ss sc
607+ = do sc' <- pos ns ss sc
607 spos <- get
608 spos <- get
608− put (i : spos)
609+ put (True : spos)
609 return (PPi (p { pstatic = Static }) n t sc')
610 return (PPi (p { pstatic = Static }) n t sc')
610− | otherwise = do sc' <- pos (i+1) ns ss sc
611+ | otherwise = do sc' <- pos ns ss sc
612+ spos <- get
613+ put (False : spos)
611 return (PPi p n t sc')
614 return (PPi p n t sc')
612− pos i ns ss t = return t
615+ pos ns ss t = return t
613
616
614-- Debugging/logging stuff
617-- Debugging/logging stuff
615
618
src/Idris/REPL.hs+10
@@ -50,6 +50,16 @@ process (Eval t) = do (tm, ty) <- elabVal toplevel t
50 logLvl 3 $ "Raw: " ++ show tm'
50 logLvl 3 $ "Raw: " ++ show tm'
51 iputStrLn (show (delab ist tm') ++ " : " ++
51 iputStrLn (show (delab ist tm') ++ " : " ++
52 show (delab ist ty'))
52 show (delab ist ty'))
53+process (Spec t) = do (tm, ty) <- elabVal toplevel t
54+ ctxt <- getContext
55+ ist <- get
56+ let tm' = specialise ctxt (idris_statics ist) tm
57+ iputStrLn (show (delab ist tm'))
58+process (HNF t) = do (tm, ty) <- elabVal toplevel t
59+ ctxt <- getContext
60+ ist <- get
61+ let tm' = hnf ctxt [] tm
62+ iputStrLn (show (delab ist tm'))
53process TTShell = do ist <- get
63process TTShell = do ist <- get
54 let shst = initState (tt_ctxt ist)
64 let shst = initState (tt_ctxt ist)
55 shst' <- lift $ runShell shst
65 shst' <- lift $ runShell shst
src/Idris/REPLParser.hs+11−7
@@ -10,20 +10,24 @@ import Text.ParserCombinators.Parsec.Language
10import qualified Text.ParserCombinators.Parsec.Token as PTok
10import qualified Text.ParserCombinators.Parsec.Token as PTok
11
11
12import Debug.Trace
12import Debug.Trace
13+import Data.List
13
14
14parseCmd i = runParser pCmd i "(input)"
15parseCmd i = runParser pCmd i "(input)"
15
16
16cmd :: [String] -> IParser ()
17cmd :: [String] -> IParser ()
17−cmd xs = do lchar ':'; docmd xs
18+cmd xs = do lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)
18 where docmd [] = fail "No such command"
19 where docmd [] = fail "No such command"
19 docmd (x:xs) = try (discard (symbol x)) <|> docmd xs
20 docmd (x:xs) = try (discard (symbol x)) <|> docmd xs
20
21
21pCmd :: IParser Command
22pCmd :: IParser Command
22−pCmd = try (do cmd ["q", "quit"]; return Quit)
23+pCmd = try (do cmd ["q", "quit"]; eof; return Quit)
23− <|> try (do cmd ["h", "?", "help"]; return Help)
24+ <|> try (do cmd ["h", "?", "help"]; eof; return Help)
24− <|> try (do cmd ["ttshell"]; return TTShell)
25+ <|> try (do cmd ["ttshell"]; eof; return TTShell)
25− <|> try (do cmd ["c", "compile"]; f <- identifier; return (Compile f))
26+ <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile f))
26− <|> try (do cmd ["m", "metavars"]; return Metavars)
27+ <|> try (do cmd ["m", "metavars"]; eof; return Metavars)
27− <|> try (do cmd ["log"]; i <- natural; return (LogLvl (fromIntegral i)))
28+ <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))
29+ <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))
30+ <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))
28 <|> do t <- pFullExpr defaultSyntax; return (Eval t)
31 <|> do t <- pFullExpr defaultSyntax; return (Eval t)
29 <|> do eof; return NOP
32 <|> do eof; return NOP
33+