forked from GitHub/gf-core
PGF.Expr.eval now returns suspension when a meta variable is encountered
This commit is contained in:
krasimir
@@ -9,6 +9,8 @@ module PGF.Expr(Tree(..), Literal(..),
|
|||||||
-- needed in the typechecker
|
-- needed in the typechecker
|
||||||
Value(..), Env, eval, apply, eqValue,
|
Value(..), Env, eval, apply, eqValue,
|
||||||
|
|
||||||
|
MetaId,
|
||||||
|
|
||||||
-- helpers
|
-- helpers
|
||||||
pStr,pFactor,
|
pStr,pFactor,
|
||||||
) where
|
) where
|
||||||
@@ -29,6 +31,8 @@ data Literal =
|
|||||||
| LFlt Double -- ^ floating point constant
|
| LFlt Double -- ^ floating point constant
|
||||||
deriving (Eq,Ord)
|
deriving (Eq,Ord)
|
||||||
|
|
||||||
|
type MetaId = Int
|
||||||
|
|
||||||
-- | The tree is an evaluated expression in the abstract syntax
|
-- | The tree is an evaluated expression in the abstract syntax
|
||||||
-- of the grammar. The type is especially restricted to not
|
-- of the grammar. The type is especially restricted to not
|
||||||
-- allow unapplied lambda abstractions. The tree is used directly
|
-- allow unapplied lambda abstractions. The tree is used directly
|
||||||
@@ -38,7 +42,7 @@ data Tree =
|
|||||||
| Var CId -- ^ variable
|
| Var CId -- ^ variable
|
||||||
| Fun CId [Tree] -- ^ function application
|
| Fun CId [Tree] -- ^ function application
|
||||||
| Lit Literal -- ^ literal
|
| Lit Literal -- ^ literal
|
||||||
| Meta {-# UNPACK #-} !Int -- ^ meta variable
|
| Meta {-# UNPACK #-} !MetaId -- ^ meta variable
|
||||||
deriving (Eq, Ord)
|
deriving (Eq, Ord)
|
||||||
|
|
||||||
-- | An expression represents a potentially unevaluated expression
|
-- | An expression represents a potentially unevaluated expression
|
||||||
@@ -47,7 +51,7 @@ data Expr =
|
|||||||
EAbs CId Expr -- ^ lambda abstraction
|
EAbs CId Expr -- ^ lambda abstraction
|
||||||
| EApp Expr Expr -- ^ application
|
| EApp Expr Expr -- ^ application
|
||||||
| ELit Literal -- ^ literal
|
| ELit Literal -- ^ literal
|
||||||
| EMeta {-# UNPACK #-} !Int -- ^ meta variable
|
| EMeta {-# UNPACK #-} !MetaId -- ^ meta variable
|
||||||
| EVar CId -- ^ variable or function reference
|
| EVar CId -- ^ variable or function reference
|
||||||
| EPi CId Expr Expr -- ^ dependent function type
|
| EPi CId Expr Expr -- ^ dependent function type
|
||||||
deriving (Eq,Ord)
|
deriving (Eq,Ord)
|
||||||
@@ -191,6 +195,7 @@ ppLit (LStr s) = PP.text (show s)
|
|||||||
ppLit (LInt n) = PP.integer n
|
ppLit (LInt n) = PP.integer n
|
||||||
ppLit (LFlt d) = PP.double d
|
ppLit (LFlt d) = PP.double d
|
||||||
|
|
||||||
|
ppMeta :: MetaId -> PP.Doc
|
||||||
ppMeta n
|
ppMeta n
|
||||||
| n == 0 = PP.char '?'
|
| n == 0 = PP.char '?'
|
||||||
| otherwise = PP.char '?' PP.<> PP.int n
|
| otherwise = PP.char '?' PP.<> PP.int n
|
||||||
@@ -245,7 +250,8 @@ normalForm funs e = value2expr 0 (eval funs Map.empty e)
|
|||||||
where
|
where
|
||||||
value2expr i (VApp f vs) = foldl EApp (EVar f) (map (value2expr i) vs)
|
value2expr i (VApp f vs) = foldl EApp (EVar f) (map (value2expr i) vs)
|
||||||
value2expr i (VGen j vs) = foldl EApp (EVar (var j)) (map (value2expr i) vs)
|
value2expr i (VGen j vs) = foldl EApp (EVar (var j)) (map (value2expr i) vs)
|
||||||
value2expr i (VMeta n vs) = foldl EApp (EMeta n) (map (value2expr i) vs)
|
value2expr i (VMeta j vs) = foldl EApp (EMeta j) (map (value2expr i) vs)
|
||||||
|
value2expr i (VSusp j vs k) = value2expr i (k (VGen j vs))
|
||||||
value2expr i (VLit l) = ELit l
|
value2expr i (VLit l) = ELit l
|
||||||
value2expr i (VClosure env (EAbs x e)) = EAbs (var i) (value2expr (i+1) (eval funs (Map.insert x (VGen i []) env) e))
|
value2expr i (VClosure env (EAbs x e)) = EAbs (var i) (value2expr (i+1) (eval funs (Map.insert x (VGen i []) env) e))
|
||||||
|
|
||||||
@@ -257,10 +263,10 @@ normalForm funs e = value2expr 0 (eval funs Map.empty e)
|
|||||||
data Value
|
data Value
|
||||||
= VApp CId [Value]
|
= VApp CId [Value]
|
||||||
| VLit Literal
|
| VLit Literal
|
||||||
| VMeta {-# UNPACK #-} !Int [Value]
|
| VMeta {-# UNPACK #-} !MetaId [Value]
|
||||||
| VGen {-# UNPACK #-} !Int [Value]
|
| VGen {-# UNPACK #-} !MetaId [Value]
|
||||||
|
| VSusp {-# UNPACK #-} !MetaId [Value] (Value -> Value)
|
||||||
| VClosure Env Expr
|
| VClosure Env Expr
|
||||||
deriving (Eq,Ord)
|
|
||||||
|
|
||||||
type Funs = Map.Map CId (Type,Int,[Equation]) -- type and def of a fun
|
type Funs = Map.Map CId (Type,Int,[Equation]) -- type and def of a fun
|
||||||
type Env = Map.Map CId Value
|
type Env = Map.Map CId Value
|
||||||
@@ -271,7 +277,7 @@ eval funs env (EVar x) = case Map.lookup x env of
|
|||||||
Nothing -> case Map.lookup x funs of
|
Nothing -> case Map.lookup x funs of
|
||||||
Just (_,a,eqs) -> if a == 0
|
Just (_,a,eqs) -> if a == 0
|
||||||
then case eqs of
|
then case eqs of
|
||||||
Equ [] e : _ -> eval funs env e
|
Equ [] e : _ -> eval funs Map.empty e
|
||||||
_ -> VApp x []
|
_ -> VApp x []
|
||||||
else VApp x []
|
else VApp x []
|
||||||
Nothing -> error ("unknown variable "++prCId x)
|
Nothing -> error ("unknown variable "++prCId x)
|
||||||
@@ -289,14 +295,12 @@ apply funs env (EVar x) vs = case Map.lookup x env of
|
|||||||
(VLit _ , vs) -> error "literal of function type"
|
(VLit _ , vs) -> error "literal of function type"
|
||||||
(VMeta i vs0 , vs) -> VMeta i (vs0++vs)
|
(VMeta i vs0 , vs) -> VMeta i (vs0++vs)
|
||||||
(VGen i vs0 , vs) -> VGen i (vs0++vs)
|
(VGen i vs0 , vs) -> VGen i (vs0++vs)
|
||||||
|
(VSusp i vs0 k , vs) -> VSusp i (vs0++vs) k
|
||||||
(VClosure env (EAbs x e),v:vs) -> apply funs (Map.insert x v env) e vs
|
(VClosure env (EAbs x e),v:vs) -> apply funs (Map.insert x v env) e vs
|
||||||
Nothing -> case Map.lookup x funs of
|
Nothing -> case Map.lookup x funs of
|
||||||
Just (_,a,eqs) -> if a <= length vs
|
Just (_,a,eqs) -> if a <= length vs
|
||||||
then let (as,vs') = splitAt a vs
|
then let (as,vs') = splitAt a vs
|
||||||
in case match eqs as of
|
in match funs x eqs as vs'
|
||||||
Match e env -> apply funs env e vs'
|
|
||||||
Fail -> VApp x vs
|
|
||||||
Susp -> VApp x vs
|
|
||||||
else VApp x vs
|
else VApp x vs
|
||||||
Nothing -> error ("unknown variable "++prCId x)
|
Nothing -> error ("unknown variable "++prCId x)
|
||||||
apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs)
|
apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs)
|
||||||
@@ -309,31 +313,23 @@ apply funs env (ELit l) vs = error "literal of function type"
|
|||||||
-- Pattern matching
|
-- Pattern matching
|
||||||
-----------------------------------------------------
|
-----------------------------------------------------
|
||||||
|
|
||||||
data MatchRes
|
match :: Funs -> CId -> [Equation] -> [Value] -> [Value] -> Value
|
||||||
= Match Expr Env
|
match funs f eqs as0 vs0 =
|
||||||
| Susp
|
|
||||||
| Fail
|
|
||||||
|
|
||||||
match :: [Equation] -> [Value] -> MatchRes
|
|
||||||
match eqs as =
|
|
||||||
case eqs of
|
case eqs of
|
||||||
[] -> Fail
|
[] -> VApp f (as0++vs0)
|
||||||
(Equ ps res):eqs -> case tryMatches ps as res Map.empty of
|
(Equ ps res):eqs -> tryMatches eqs ps as0 res Map.empty
|
||||||
Fail -> match eqs as
|
|
||||||
res -> res
|
|
||||||
where
|
where
|
||||||
tryMatches [] [] res env = Match res env
|
tryMatches eqs [] [] res env = apply funs env res vs0
|
||||||
tryMatches (p:ps) (a:as) res env = tryMatch p a env
|
tryMatches eqs (p:ps) (a:as) res env = tryMatch p a env
|
||||||
where
|
where
|
||||||
tryMatch (PApp f1 ps1) (VApp f2 vs2) env | f1 == f2 = tryMatches (ps1++ps) (vs2++as) res env
|
tryMatch (PVar x ) (v ) env = tryMatches eqs ps as res (Map.insert x v env)
|
||||||
tryMatch (PApp f1 ps1) (VMeta _ _ ) env = Susp
|
tryMatch (PWild ) (_ ) env = tryMatches eqs ps as res env
|
||||||
tryMatch (PApp f1 ps1) (VGen _ _ ) env = Susp
|
tryMatch (p ) (VMeta i vs ) env = VSusp i vs (\v -> tryMatch p v env)
|
||||||
tryMatch (PLit l1 ) (VLit l2 ) env | l1 == l2 = tryMatches ps as res env
|
tryMatch (p ) (VGen i vs ) env = VApp f (as0++vs0)
|
||||||
tryMatch (PLit l1 ) (VMeta _ _ ) env = Susp
|
tryMatch (p ) (VSusp i vs k) env = VSusp i vs (\v -> tryMatch p (k v) env)
|
||||||
tryMatch (PLit l1 ) (VGen _ _ ) env = Susp
|
tryMatch (PApp f1 ps1) (VApp f2 vs2 ) env | f1 == f2 = tryMatches eqs (ps1++ps) (vs2++as) res env
|
||||||
tryMatch (PVar x ) (v ) env = tryMatches ps as res (Map.insert x v env)
|
tryMatch (PLit l1 ) (VLit l2 ) env | l1 == l2 = tryMatches eqs ps as res env
|
||||||
tryMatch (PWild ) (_ ) env = tryMatches ps as res env
|
tryMatch _ _ env = match funs f eqs as0 vs0
|
||||||
tryMatch _ _ env = Fail
|
|
||||||
|
|
||||||
|
|
||||||
-----------------------------------------------------
|
-----------------------------------------------------
|
||||||
|
|||||||
Reference in New Issue
Block a user