more patterns in the partial evaluator

This commit is contained in:
krangelov
2021-09-24 19:14:48 +02:00
parent 466fd4a7da
commit f83ea160da
3 changed files with 77 additions and 30 deletions

View File

@@ -46,11 +46,13 @@ data Value s
| VMeta (Thunk s) (Env s) [Thunk s]
| VGen {-# UNPACK #-} !Int [Thunk s]
| VClosure (Env s) Term
| VRecType [(Label, Value s)]
| VR [(Label, Thunk s)]
| VP (Value s) Label
| VP (Value s) Label [Thunk s]
| VTable (Value s) (Value s)
| VT TInfo [Case]
| VV Type [Thunk s]
| VS (Value s) (Value s)
| VS (Value s) (Value s) [Thunk s]
| VSort Ident
| VInt Integer
| VFlt Double
@@ -61,29 +63,35 @@ data Value s
eval env (Vr x) vs = case lookup x env of
Just tnk -> force tnk vs
Nothing -> error "Unknown variable"
eval env (Sort s) vs = return (VSort s)
eval env (EInt n) vs = return (VInt n)
eval env (EFloat d) vs = return (VFlt d)
eval env (K t) vs = return (VStr t)
eval env Empty vs = return (VC [])
eval env (Sort s) [] = return (VSort s)
eval env (EInt n) [] = return (VInt n)
eval env (EFloat d) [] = return (VFlt d)
eval env (K t) [] = return (VStr t)
eval env Empty [] = return (VC [])
eval env (App t1 t2) vs = do tnk <- newThunk env t2
eval env t1 (tnk : vs)
eval env (Abs b x t) [] = return (VClosure env (Abs b x t))
eval env (Abs b x t) (v:vs) = eval ((x,v):env) t vs
eval env (Meta i) vs = do tnk <- newMeta i
return (VMeta tnk env vs)
eval env (ImplArg t) vs = eval env t vs
eval env (ImplArg t) [] = eval env t []
-- eval env (Prod b x t1 t2)[] = eval env t []
eval env (Typed t ty) vs = eval env t vs
eval env (R as) vs = do as <- mapM (\(lbl,(_,t)) -> fmap ((,) lbl) (newThunk env t)) as
eval env (RecType lbls) [] = do lbls <- mapM (\(lbl,ty) -> fmap ((,) lbl) (eval env ty [])) lbls
return (VRecType lbls)
eval env (R as) [] = do as <- mapM (\(lbl,(_,t)) -> fmap ((,) lbl) (newThunk env t)) as
return (VR as)
eval env (P t lbl) vs = do v <- eval env t []
case v of
VR as -> case lookup lbl as of
Nothing -> error ("Missing value for label "++show lbl)
Just tnk -> force tnk vs
v -> return (VP v lbl)
eval env (T i cs) vs = return (VT i cs)
eval env (V ty ts) vs = do tnks <- mapM (newThunk env) ts
v -> return (VP v lbl vs)
eval env (Table t1 t2) [] = do v1 <- eval env t1 []
v2 <- eval env t2 []
return (VTable v1 v2)
eval env (T i cs) [] = return (VT i cs)
eval env (V ty ts) [] = do tnks <- mapM (newThunk env) ts
return (VV ty tnks)
eval env (S t1 t2) vs = do v1 <- eval env t1 []
tnk2 <- newThunk env t2
@@ -91,21 +99,22 @@ eval env (S t1 t2) vs = do v1 <- eval env t1 []
VT _ cs -> do (env,t) <- patternMatch env cs tnk2
eval env t vs
v1 -> do v2 <- force tnk2 []
return (VS v1 v2)
return (VS v1 v2 vs)
eval env (Let (x,(_,t1)) t2) vs = do tnk <- newThunk env t1
eval ((x,tnk):env) t2 vs
eval env (Q q) vs = do t <- lookupGlobal q
eval env t vs
eval env (Q q) vs = do t <- lookupGlobal q
eval env t vs
eval env (QC q) vs = return (VApp q vs)
eval env (C t1 t2) vs = do v1 <- eval env t1 vs
v2 <- eval env t2 vs
eval env (C t1 t2) [] = do v1 <- eval env t1 []
v2 <- eval env t2 []
case (v1,v2) of
(VC vs1,VC vs2) -> return (VC (vs1++vs2))
(VC vs1,v2 ) -> return (VC (vs1++[v2]))
(v1, VC vs2) -> return (VC ([v1]++vs2))
(v1, v2 ) -> return (VC [v1,v2])
eval env (FV ts) vs = msum [eval env t vs | t <- ts]
eval env t vs = error (show t)
eval env (Error msg) vs = error msg
eval env t vs = error (show t)
apply v [] = return v
apply (VApp f vs0) vs = return (VApp f (vs0++vs))
@@ -120,21 +129,45 @@ patternMatch env ((p,t):cs) tnk = do
Nothing -> patternMatch env cs tnk
Just env -> return (env,t)
where
match env (PP q ps) tnk = do v <- force tnk []
case v of
VApp r tnks | q == r -> match' env ps tnks
_ -> return Nothing
match env (PV v) tnk = return (Just ((v,tnk):env))
match env PW tnk = return (Just env)
match env (PAs v p) tnk = match ((v,tnk):env) p tnk
match env (PP q ps) tnk = do v <- force tnk []
case v of
VApp r tnks | q == r -> matchArgs env ps tnks
_ -> return Nothing
match env (PV v) tnk = return (Just ((v,tnk):env))
match env PW tnk = return (Just env)
match env (PR pas) tnk = do v <- force tnk []
case v of
VR as -> matchRec env pas as
_ -> return Nothing
match env (PInt n) tnk = do v <- force tnk []
case v of
VInt m | n == m -> return (Just env)
_ -> return Nothing
match env (PFloat n) tnk = do v <- force tnk []
case v of
VFlt m | n == m -> return (Just env)
_ -> return Nothing
match env (PT ty p) tnk = match env p tnk
match env (PTilde _) tnk = return (Just env)
match env (PAs v p) tnk = match ((v,tnk):env) p tnk
match' env [] [] =
matchArgs env [] [] =
return (Just env)
match' env (p:ps) (tnk:tnks) = do
matchArgs env (p:ps) (tnk:tnks) = do
res <- match env p tnk
case res of
Nothing -> return Nothing
Just env -> match' env ps tnks
Just env -> matchArgs env ps tnks
matchRec env [] as =
return (Just env)
matchRec env ((lbl,p):pas) as =
case lookup lbl as of
Just tnk -> do res <- match env p tnk
case res of
Nothing -> return Nothing
Just env -> matchRec env pas as
Nothing -> error ("Missing value for label "++show lbl)
value2term i (VApp q tnks) =
foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (QC q) tnks
@@ -150,15 +183,25 @@ value2term i (VClosure env (Abs b x t)) = do
v <- eval ((x,tnk):env) t []
t <- value2term (i+1) v
return (Abs b (identS ('v':show i)) t)
value2term i (VRecType lbls) = do
lbls <- mapM (\(lbl,v) -> fmap ((,) lbl) (value2term i v)) lbls
return (RecType lbls)
value2term i (VR as) = do
as <- mapM (\(lbl,tnk) -> fmap (\t -> (lbl,(Nothing,t))) (force tnk [] >>= value2term i)) as
return (R as)
value2term i (VP v lbl) = do
value2term i (VP v lbl tnks) = do
t <- value2term i v
return (P t lbl)
foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (P t lbl) tnks
value2term i (VTable v1 v2) = do
t1 <- value2term i v1
t2 <- value2term i v2
return (Table t1 t2)
value2term i (VT ti cs) = return (T ti cs)
value2term i (VV ty tnks) = do ts <- mapM (\tnk -> force tnk [] >>= value2term i) tnks
return (V ty ts)
value2term i (VS v1 v2 tnks) = do t1 <- value2term i v1
t2 <- value2term i v2
foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (S t1 t2) tnks
value2term i (VSort s) = return (Sort s)
value2term i (VStr tok) = return (K tok)
value2term i (VInt n) = return (EInt n)

View File

@@ -7,3 +7,5 @@ cc table {P1 => "p1"; P2 q => "p2"} ! P2 (Q1|Q2)
cc table {P1 => "p1"; P2 Q1 => "p2q1"; P2 Q2 => "p2q2"} ! P2 (Q1|Q2)
cc table {P1 => "p1"; P2 Q1 => "p2q1"; P2 Q2 => "p2q2"} ! P2 Q1
cc table {P1 => "p1"; P2 q => case q of {Q1 => "p2q1"; Q2 => "p2q2"}} ! P2 Q1
cc case <Q1,Q2> of {<Q1,Q1> => "11"; <Q1,Q2> => "12"; _ => "??"}
cc case <Q2,Q2> of {<Q1,Q1> => "11"; <Q1,Q2> => "12"; _ => "??"}

View File

@@ -6,3 +6,5 @@ param_table.P2 param_table.Q1
variants {"p2q1"; "p2q2"}
"p2q1"
"p2q1"
"12"
"??"