mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-07 02:02:51 -06:00
refactor the PGF.Expr type and the evaluation of abstract expressions
This commit is contained in:
krasimir
@@ -1,106 +0,0 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : AbsCompute
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- computation in abstract syntax with def definitions.
|
||||
--
|
||||
-- modified from src GF computation
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module PGF.AbsCompute (
|
||||
compute
|
||||
) where
|
||||
|
||||
import PGF.Data
|
||||
import PGF.Macros (lookDef,isData)
|
||||
import PGF.Expr
|
||||
import PGF.CId
|
||||
|
||||
compute :: PGF -> Tree -> Tree
|
||||
compute pgf = computeAbsTermIn pgf []
|
||||
|
||||
computeAbsTermIn :: PGF -> [CId] -> Tree -> Tree
|
||||
computeAbsTermIn pgf vv = expr2tree . compt vv . tree2expr where
|
||||
compt vv t =
|
||||
let
|
||||
t' = beta vv t
|
||||
(yy,f,aa) = exprForm t'
|
||||
vv' = yy ++ vv
|
||||
aa' = map (compt vv') aa
|
||||
in
|
||||
mkAbs yy $ case look f of
|
||||
Left (EEq eqs) -> case match eqs aa' of
|
||||
Just (d,g) -> compt vv' $ subst vv' g d
|
||||
_ -> mkApp f aa'
|
||||
Left (EMeta _) -> mkApp f aa' -- canonical or primitive
|
||||
Left d -> compt vv' $ mkApp d aa'
|
||||
_ -> mkApp f aa' -- literal
|
||||
look f = case f of
|
||||
EVar c -> Left $ lookDef pgf c
|
||||
_ -> Right f
|
||||
match = findMatch pgf
|
||||
|
||||
beta :: [CId] -> Expr -> Expr
|
||||
beta vv c = case c of
|
||||
EApp f a ->
|
||||
let (a',f') = (beta vv a, beta vv f) in
|
||||
case f' of
|
||||
EAbs x b -> beta vv $ subst vv [(x,a')] (beta (x:vv) b)
|
||||
_ -> (if a'==a && f'==f then id else beta vv) $ EApp f' a'
|
||||
EAbs x b -> EAbs x (beta (x:vv) b)
|
||||
_ -> c
|
||||
|
||||
|
||||
subst :: [CId] -> Subst -> Expr -> Expr
|
||||
subst xs g e = case e of
|
||||
EAbs x b -> EAbs x (subst (x:xs) g e) ---- TODO: refresh variables
|
||||
EApp f a -> EApp (substg f) (substg a)
|
||||
EVar x -> maybe e id $ lookup x g
|
||||
_ -> e
|
||||
where
|
||||
substg = subst xs g
|
||||
|
||||
type Subst = [(CId,Expr)]
|
||||
type Patt = Expr
|
||||
|
||||
|
||||
exprForm :: Expr -> ([CId],Expr,[Expr])
|
||||
exprForm exp = upd ([],exp,[]) where
|
||||
upd (xs,f,es) = case f of
|
||||
EAbs x b -> upd (x:xs,b,es)
|
||||
EApp c a -> upd (xs,c,a:es)
|
||||
_ -> (reverse xs,f,es)
|
||||
|
||||
mkAbs xs b = foldr EAbs b xs
|
||||
mkApp f es = foldl EApp f es
|
||||
|
||||
-- special version of pattern matching, to deal with comp under lambda
|
||||
|
||||
findMatch :: PGF -> [Equation] -> [Expr] -> Maybe (Expr, Subst)
|
||||
findMatch pgf cases terms = case cases of
|
||||
[] -> Nothing
|
||||
(Equ patts _):_ | length patts /= length terms -> Nothing
|
||||
(Equ patts val):cc -> case mapM tryMatch (zip patts terms) of
|
||||
Just substs -> return (val, concat substs)
|
||||
_ -> findMatch pgf cc terms
|
||||
where
|
||||
|
||||
tryMatch (p,t) = case (exprForm p, exprForm t) of
|
||||
(([],EVar c,[]),_) | constructor c -> if p==t then return [] else Nothing
|
||||
(([],EVar x,[]),_) | notMeta t -> return [(x,t)]
|
||||
(([],p, pp), ([], f, tt)) | p == f && length pp == length tt -> do
|
||||
matches <- mapM tryMatch (zip pp tt)
|
||||
return (concat matches)
|
||||
_ -> if p==t then return [] else Nothing
|
||||
|
||||
notMeta e = case e of
|
||||
EMeta _ -> False
|
||||
EApp f a -> notMeta f && notMeta a
|
||||
EAbs _ b -> notMeta b
|
||||
_ -> True
|
||||
|
||||
constructor = isData pgf
|
||||
|
||||
@@ -109,7 +109,6 @@ instance Binary Expr where
|
||||
put (ELit (LFlt d)) = putWord8 4 >> put d
|
||||
put (ELit (LInt i)) = putWord8 5 >> put i
|
||||
put (EMeta i) = putWord8 6 >> put i
|
||||
put (EEq eqs) = putWord8 7 >> put eqs
|
||||
get = do tag <- getWord8
|
||||
case tag of
|
||||
0 -> liftM2 EAbs get get
|
||||
@@ -119,9 +118,25 @@ instance Binary Expr where
|
||||
4 -> liftM (ELit . LFlt) get
|
||||
5 -> liftM (ELit . LInt) get
|
||||
6 -> liftM EMeta get
|
||||
7 -> liftM EEq get
|
||||
_ -> decodingError
|
||||
|
||||
|
||||
instance Binary Patt where
|
||||
put (PApp f ps) = putWord8 0 >> put (f,ps)
|
||||
put (PVar x) = putWord8 1 >> put x
|
||||
put PWild = putWord8 2
|
||||
put (PLit (LStr s)) = putWord8 3 >> put s
|
||||
put (PLit (LFlt d)) = putWord8 4 >> put d
|
||||
put (PLit (LInt i)) = putWord8 5 >> put i
|
||||
get = do tag <- getWord8
|
||||
case tag of
|
||||
0 -> liftM2 PApp get get
|
||||
1 -> liftM PVar get
|
||||
2 -> return PWild
|
||||
3 -> liftM (PLit . LStr) get
|
||||
4 -> liftM (PLit . LFlt) get
|
||||
5 -> liftM (PLit . LInt) get
|
||||
_ -> decodingError
|
||||
|
||||
instance Binary Equation where
|
||||
put (Equ ps e) = put (ps,e)
|
||||
get = liftM2 Equ get get
|
||||
|
||||
@@ -24,7 +24,7 @@ data PGF = PGF {
|
||||
|
||||
data Abstr = Abstr {
|
||||
aflags :: Map.Map CId String, -- value of a flag
|
||||
funs :: Map.Map CId (Type,Expr), -- type and def of a fun
|
||||
funs :: Map.Map CId (Type,[Equation]), -- type and def of a fun
|
||||
cats :: Map.Map CId [Hypo], -- context of a cat
|
||||
catfuns :: Map.Map CId [CId] -- funs to a cat (redundant, for fast lookup)
|
||||
}
|
||||
|
||||
151
src/PGF/Expr.hs
151
src/PGF/Expr.hs
@@ -1,13 +1,13 @@
|
||||
module PGF.Expr(Tree(..), Literal(..),
|
||||
readTree, showTree, pTree, ppTree,
|
||||
|
||||
Expr(..), Equation(..),
|
||||
readExpr, showExpr, pExpr, ppExpr,
|
||||
Expr(..), Patt(..), Equation(..),
|
||||
readExpr, showExpr, pExpr, ppExpr, ppPatt,
|
||||
|
||||
tree2expr, expr2tree,
|
||||
|
||||
-- needed in the typechecker
|
||||
Value(..), Env, eval, apply,
|
||||
Value(..), Env, eval, apply, eqValue,
|
||||
|
||||
-- helpers
|
||||
pStr,pFactor,
|
||||
@@ -17,6 +17,7 @@ module PGF.Expr(Tree(..), Literal(..),
|
||||
) where
|
||||
|
||||
import PGF.CId
|
||||
import PGF.Type
|
||||
|
||||
import Data.Char
|
||||
import Data.Maybe
|
||||
@@ -29,7 +30,7 @@ data Literal =
|
||||
LStr String -- ^ string constant
|
||||
| LInt Integer -- ^ integer constant
|
||||
| LFlt Double -- ^ floating point constant
|
||||
deriving (Eq,Ord,Show)
|
||||
deriving (Eq,Ord)
|
||||
|
||||
-- | The tree is an evaluated expression in the abstract syntax
|
||||
-- of the grammar. The type is especially restricted to not
|
||||
@@ -53,17 +54,24 @@ data Expr =
|
||||
| ELit Literal -- ^ literal
|
||||
| EMeta Int -- ^ meta variable
|
||||
| EVar CId -- ^ variable or function reference
|
||||
| EEq [Equation] -- ^ lambda function defined as a set of equations with pattern matching
|
||||
| EPi CId Expr Expr -- ^ dependent function type
|
||||
deriving (Eq,Ord)
|
||||
|
||||
-- | The pattern is used to define equations in the abstract syntax of the grammar.
|
||||
data Patt =
|
||||
PApp CId [Patt] -- ^ application. The identifier should be constructor i.e. defined with 'data'
|
||||
| PLit Literal -- ^ literal
|
||||
| PVar CId -- ^ variable
|
||||
| PWild -- ^ wildcard
|
||||
deriving (Eq,Ord)
|
||||
|
||||
-- | The equation is used to define lambda function as a sequence
|
||||
-- of equations with pattern matching. The list of 'Expr' represents
|
||||
-- the patterns and the second 'Expr' is the function body for this
|
||||
-- equation.
|
||||
data Equation =
|
||||
Equ [Expr] Expr
|
||||
deriving (Eq,Ord,Show)
|
||||
Equ [Patt] Expr
|
||||
deriving (Eq,Ord)
|
||||
|
||||
-- | parses 'String' as an expression
|
||||
readTree :: String -> Maybe Tree
|
||||
@@ -120,24 +128,13 @@ pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Li
|
||||
return (Meta n)
|
||||
|
||||
pExpr :: RP.ReadP Expr
|
||||
pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm RP.<++ pEqs)
|
||||
pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm)
|
||||
where
|
||||
pTerm = fmap (foldl1 EApp) (RP.sepBy1 pFactor RP.skipSpaces)
|
||||
|
||||
pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") (RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ','))
|
||||
e <- pExpr
|
||||
return (foldr EAbs e xs)
|
||||
|
||||
pEqs = fmap EEq $
|
||||
RP.between (RP.skipSpaces >> RP.char '{')
|
||||
(RP.skipSpaces >> RP.char '}')
|
||||
(RP.sepBy1 (RP.skipSpaces >> pEq)
|
||||
(RP.skipSpaces >> RP.string ";"))
|
||||
|
||||
pEq = do pats <- (RP.sepBy1 pExpr RP.skipSpaces)
|
||||
RP.skipSpaces >> RP.string "=>"
|
||||
e <- pExpr
|
||||
return (Equ pats e)
|
||||
|
||||
pFactor = fmap EVar pCId
|
||||
RP.<++ fmap ELit pLit
|
||||
@@ -176,6 +173,7 @@ ppTree d (Meta n) = PP.char '?' PP.<> PP.int n
|
||||
ppTree d (Var id) = PP.text (prCId id)
|
||||
|
||||
|
||||
ppExpr :: Int -> Expr -> PP.Doc
|
||||
ppExpr d (EAbs x e) = let (xs,e1) = getVars (EAbs x e)
|
||||
in ppParens (d > 0) (PP.char '\\' PP.<>
|
||||
PP.hsep (PP.punctuate PP.comma (map (PP.text . prCId) xs)) PP.<+>
|
||||
@@ -188,9 +186,11 @@ ppExpr d (EApp e1 e2) = ppParens (d > 1) ((ppExpr 1 e1) PP.<+> (ppExpr 2 e2))
|
||||
ppExpr d (ELit l) = ppLit l
|
||||
ppExpr d (EMeta n) = PP.char '?' PP.<+> PP.int n
|
||||
ppExpr d (EVar f) = PP.text (prCId f)
|
||||
ppExpr d (EEq eqs) = PP.braces (PP.sep (PP.punctuate PP.semi (map ppEquation eqs)))
|
||||
|
||||
ppEquation (Equ pats e) = PP.hsep (map (ppExpr 2) pats) PP.<+> PP.text "=>" PP.<+> ppExpr 0 e
|
||||
ppPatt d (PApp f ps) = ppParens (d > 1) (PP.text (prCId f) PP.<+> PP.hsep (map (ppPatt 2) ps))
|
||||
ppPatt d (PLit l) = ppLit l
|
||||
ppPatt d (PVar f) = PP.text (prCId f)
|
||||
ppPatt d PWild = PP.char '_'
|
||||
|
||||
ppLit (LStr s) = PP.text (show s)
|
||||
ppLit (LInt n) = PP.integer n
|
||||
@@ -212,46 +212,97 @@ tree2expr (Meta n) = EMeta n
|
||||
tree2expr (Abs xs t) = foldr EAbs (tree2expr t) xs
|
||||
tree2expr (Var x) = EVar x
|
||||
|
||||
-- | Converts an expression to tree. If the expression
|
||||
-- contains unevaluated applications they will be applied.
|
||||
expr2tree :: Expr -> Tree
|
||||
expr2tree e = value2tree (eval Map.empty e) [] []
|
||||
-- | Converts an expression to tree. The expression
|
||||
-- is first reduced to beta-eta-alfa normal form and
|
||||
-- after that converted to tree.
|
||||
expr2tree :: Funs -> Expr -> Tree
|
||||
expr2tree funs e = value2tree [] (eval funs Map.empty e)
|
||||
where
|
||||
value2tree (VApp v1 v2) xs ts = value2tree v1 xs (value2tree v2 [] []:ts)
|
||||
value2tree (VVar x) xs ts = ret xs (fun xs x ts)
|
||||
value2tree (VMeta n) xs [] = ret xs (Meta n)
|
||||
value2tree (VLit l) xs [] = ret xs (Lit l)
|
||||
value2tree (VClosure env (EAbs x e)) xs [] = value2tree (eval (Map.insert x (VVar x) env) e) (x:xs) []
|
||||
|
||||
fun xs x ts
|
||||
| x `elem` xs = Var x
|
||||
| otherwise = Fun x ts
|
||||
value2tree xs (VApp f vs) = case Map.lookup f funs of
|
||||
Just (DTyp hyps _ _,_) -> -- eta conversion
|
||||
let a1 = length hyps
|
||||
a2 = length vs
|
||||
a = a1 - a2
|
||||
i = length xs
|
||||
xs' = [var i | i <- [i..i+a-1]]
|
||||
in ret (reverse xs'++xs)
|
||||
(Fun f (map (value2tree []) vs++map Var xs'))
|
||||
Nothing -> error ("unknown variable "++prCId f)
|
||||
value2tree xs (VGen i) = ret xs (Var (var i))
|
||||
value2tree xs (VMeta n) = ret xs (Meta n)
|
||||
value2tree xs (VLit l) = ret xs (Lit l)
|
||||
value2tree xs (VClosure env (EAbs x e)) = let i = length xs
|
||||
in value2tree (var i:xs) (eval funs (Map.insert x (VGen i) env) e)
|
||||
|
||||
var i = mkCId ('v':show i)
|
||||
|
||||
ret [] t = t
|
||||
ret xs t = Abs (reverse xs) t
|
||||
|
||||
data Value
|
||||
= VGen Int
|
||||
| VApp Value Value
|
||||
| VVar CId
|
||||
| VMeta Int
|
||||
= VApp CId [Value]
|
||||
| VLit Literal
|
||||
| VMeta Int
|
||||
| VGen Int
|
||||
| VClosure Env Expr
|
||||
deriving (Show,Eq,Ord)
|
||||
deriving (Eq,Ord)
|
||||
|
||||
type Env = Map.Map CId Value
|
||||
type Funs = Map.Map CId (Type,[Equation]) -- type and def of a fun
|
||||
type Env = Map.Map CId Value
|
||||
|
||||
eval :: Env -> Expr -> Value
|
||||
eval env (EVar x) = fromMaybe (VVar x) (Map.lookup x env)
|
||||
eval env (EApp e1 e2) = apply (eval env e1) (eval env e2)
|
||||
eval env (EAbs x e) = VClosure env (EAbs x e)
|
||||
eval env (EMeta k) = VMeta k
|
||||
eval env (ELit l) = VLit l
|
||||
eval env e = VClosure env e
|
||||
eval :: Funs -> Env -> Expr -> Value
|
||||
eval funs env (EVar x) = case Map.lookup x env of
|
||||
Just v -> v
|
||||
Nothing -> case Map.lookup x funs of
|
||||
Just (_,eqs) -> case eqs of
|
||||
Equ [] e : _ -> eval funs env e
|
||||
[] -> VApp x []
|
||||
Nothing -> error ("unknown variable "++prCId x)
|
||||
eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2]
|
||||
eval funs env (EAbs x e) = VClosure env (EAbs x e)
|
||||
eval funs env (EMeta k) = VMeta k
|
||||
eval funs env (ELit l) = VLit l
|
||||
|
||||
apply :: Value -> Value -> Value
|
||||
apply (VClosure env (EAbs x e)) v = eval (Map.insert x v env) e
|
||||
apply v0 v = VApp v0 v
|
||||
apply :: Funs -> Env -> Expr -> [Value] -> Value
|
||||
apply funs env e [] = eval funs env e
|
||||
apply funs env (EVar x) vs = case Map.lookup x env of
|
||||
Just v -> case (v,vs) of
|
||||
(VClosure env (EAbs x e),v:vs) -> apply funs (Map.insert x v env) e vs
|
||||
Nothing -> case Map.lookup x funs of
|
||||
Just (_,eqs) -> case match eqs vs of
|
||||
Just (e,vs,env) -> apply funs env e vs
|
||||
Nothing -> VApp x vs
|
||||
Nothing -> error ("unknown variable "++prCId x)
|
||||
apply funs env (EAbs x e) (v:vs) = apply funs (Map.insert x v env) e vs
|
||||
apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs)
|
||||
|
||||
match :: [Equation] -> [Value] -> Maybe (Expr, [Value], Env)
|
||||
match eqs vs =
|
||||
case eqs of
|
||||
[] -> Nothing
|
||||
(Equ ps res):eqs -> let (as,vs') = splitAt (length ps) vs
|
||||
in case zipWithM tryMatch ps as of
|
||||
Just envs -> Just (res, vs', Map.unions envs)
|
||||
Nothing -> match eqs vs
|
||||
where
|
||||
tryMatch p v = case (p, v) of
|
||||
(PVar x, _ ) -> Just (Map.singleton x v)
|
||||
(PApp f ps, VApp fe vs) | f == fe -> do envs <- zipWithM tryMatch ps vs
|
||||
return (Map.unions envs)
|
||||
(PLit l, VLit le ) | l == le -> Just Map.empty
|
||||
_ -> Nothing
|
||||
|
||||
eqValue :: Int -> Value -> Value -> [(Value,Value)]
|
||||
eqValue k v1 v2 =
|
||||
case (v1,v2) of
|
||||
(VApp f1 vs1, VApp f2 vs2) | f1 == f2 -> concat (zipWith (eqValue k) vs1 vs2)
|
||||
(VLit l1, VLit l2 ) | l1 == l2 -> []
|
||||
(VMeta i, VMeta j ) | i == j -> []
|
||||
(VGen i, VGen j ) | i == j -> []
|
||||
(VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) ->
|
||||
let v = VGen k
|
||||
in eqValue (k+1) (VClosure (Map.insert x1 v env1) e1) (VClosure (Map.insert x2 v env2) e2)
|
||||
_ -> [(v1,v2)]
|
||||
|
||||
--- use composOp and state monad...
|
||||
newMetas :: Expr -> Expr
|
||||
|
||||
13
src/PGF/Expr.hs-boot
Normal file
13
src/PGF/Expr.hs-boot
Normal file
@@ -0,0 +1,13 @@
|
||||
module PGF.Expr where
|
||||
|
||||
import qualified Text.PrettyPrint as PP
|
||||
import qualified Text.ParserCombinators.ReadP as RP
|
||||
|
||||
data Expr
|
||||
|
||||
instance Eq Expr
|
||||
instance Ord Expr
|
||||
|
||||
pFactor :: RP.ReadP Expr
|
||||
|
||||
ppExpr :: Int -> Expr -> PP.Doc
|
||||
@@ -37,14 +37,15 @@ lookType :: PGF -> CId -> Type
|
||||
lookType pgf f =
|
||||
fst $ lookMap (error $ "lookType " ++ show f) f (funs (abstract pgf))
|
||||
|
||||
lookDef :: PGF -> CId -> Expr
|
||||
lookDef :: PGF -> CId -> [Equation]
|
||||
lookDef pgf f =
|
||||
snd $ lookMap (error $ "lookDef " ++ show f) f (funs (abstract pgf))
|
||||
|
||||
isData :: PGF -> CId -> Bool
|
||||
isData pgf f = case Map.lookup f (funs (abstract pgf)) of
|
||||
Just (_,EMeta 0) -> True ---- the encoding of data constrs
|
||||
_ -> False
|
||||
isData pgf f =
|
||||
case Map.lookup f (funs (abstract pgf)) of
|
||||
Just (_,[]) -> True -- the encoding of data constrs
|
||||
_ -> False
|
||||
|
||||
lookValCat :: PGF -> CId -> CId
|
||||
lookValCat pgf = valCat . lookType pgf
|
||||
@@ -120,9 +121,6 @@ contextLength :: Type -> Int
|
||||
contextLength ty = case ty of
|
||||
DTyp hyps _ _ -> length hyps
|
||||
|
||||
primNotion :: Expr
|
||||
primNotion = EEq []
|
||||
|
||||
term0 :: CId -> Term
|
||||
term0 = TM . prCId
|
||||
|
||||
|
||||
@@ -49,13 +49,8 @@ fromDef pgf t@(Fun f ts) = defDown t ++ defUp t where
|
||||
[(ps,p) | (p,d@(Fun g ps)) <- equs, g==f,
|
||||
isClosed d || (length equs == 1 && isLinear d)]
|
||||
|
||||
equss = [(f,[(Fun f (map expr2tree ps), expr2tree d) | (Equ ps d) <- eqs]) |
|
||||
(f,(_,d)) <- Map.assocs (funs (abstract pgf)), eqs <- defs d]
|
||||
|
||||
defs d = case d of
|
||||
EEq eqs -> [eqs]
|
||||
EMeta _ -> []
|
||||
_ -> [[Equ [] d]]
|
||||
equss = [(f,[(Fun f (map patt2tree ps), expr2tree (funs (abstract pgf)) d) | (Equ ps d) <- eqs]) |
|
||||
(f,(_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)]
|
||||
|
||||
trequ s f e = True ----trace (s ++ ": " ++ show f ++ " " ++ show e) True
|
||||
|
||||
@@ -86,8 +81,6 @@ isLinear = nodup . vars where
|
||||
nodup = all ((<2) . length) . group . sort
|
||||
|
||||
|
||||
-- special version of AbsCompute.findMatch, working on Tree
|
||||
|
||||
match :: [([Tree],Tree)] -> [Tree] -> [(Tree, Subst)]
|
||||
match cases terms = case cases of
|
||||
[] -> []
|
||||
@@ -108,3 +101,9 @@ match cases terms = case cases of
|
||||
Fun f ts -> all notMeta ts
|
||||
_ -> True
|
||||
|
||||
-- | Converts a pattern to tree.
|
||||
patt2tree :: Patt -> Tree
|
||||
patt2tree (PApp f ps) = Fun f (map patt2tree ps)
|
||||
patt2tree (PLit l) = Lit l
|
||||
patt2tree (PVar x) = Var x
|
||||
patt2tree PWild = Meta 0
|
||||
|
||||
@@ -3,7 +3,7 @@ module PGF.Type ( Type(..), Hypo(..),
|
||||
pType, ppType, ppHypo ) where
|
||||
|
||||
import PGF.CId
|
||||
import PGF.Expr
|
||||
import {-# SOURCE #-} PGF.Expr
|
||||
import Data.Char
|
||||
import qualified Text.PrettyPrint as PP
|
||||
import qualified Text.ParserCombinators.ReadP as RP
|
||||
|
||||
@@ -17,7 +17,6 @@ module PGF.TypeCheck (
|
||||
import PGF.Data
|
||||
import PGF.Macros (lookDef,isData)
|
||||
import PGF.Expr
|
||||
import PGF.AbsCompute
|
||||
import PGF.CId
|
||||
|
||||
import GF.Data.ErrM
|
||||
@@ -29,7 +28,7 @@ import Debug.Trace
|
||||
|
||||
typecheck :: PGF -> Tree -> [Tree]
|
||||
typecheck pgf t = case inferExpr pgf (newMetas (tree2expr t)) of
|
||||
Ok t -> [expr2tree t]
|
||||
Ok t -> [expr2tree (funs (abstract pgf)) t]
|
||||
Bad s -> trace s []
|
||||
|
||||
inferExpr :: PGF -> Expr -> Err Expr
|
||||
@@ -50,26 +49,24 @@ infer pgf tenv@(k,rho,gamma) e = case e of
|
||||
-- K i -> return (AStr i, valAbsString, [])
|
||||
|
||||
EApp f t -> do
|
||||
(f',w,csf) <- infer pgf tenv f
|
||||
typ <- whnf w
|
||||
(f',typ,csf) <- infer pgf tenv f
|
||||
case typ of
|
||||
VClosure env (EPi x a b) -> do
|
||||
(a',csa) <- checkExp pgf tenv t (VClosure env a)
|
||||
b' <- whnf $ VClosure (eins x (VClosure rho t) env) b
|
||||
let b' = eval (funs (abstract pgf)) (eins x (VClosure rho t) env) b
|
||||
return $ (EApp f' a', b', csf ++ csa)
|
||||
_ -> Bad ("function type expected for function " ++ show f)
|
||||
_ -> Bad ("cannot infer type of expression" ++ show e)
|
||||
|
||||
|
||||
checkExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
|
||||
checkExp pgf tenv@(k,rho,gamma) e ty = do
|
||||
typ <- whnf ty
|
||||
checkExp pgf tenv@(k,rho,gamma) e typ = do
|
||||
let v = VGen k
|
||||
case e of
|
||||
EMeta m -> return $ (e,[])
|
||||
EAbs x t -> case typ of
|
||||
VClosure env (EPi y a b) -> do
|
||||
a' <- whnf $ VClosure env a
|
||||
let a' = eval (funs (abstract pgf)) env a
|
||||
(t',cs) <- checkExp pgf (k+1,eins x v rho, eins x a' gamma) t
|
||||
(VClosure (eins y v env) b)
|
||||
return (EAbs x t', cs)
|
||||
@@ -79,7 +76,7 @@ checkExp pgf tenv@(k,rho,gamma) e ty = do
|
||||
checkInferExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
|
||||
checkInferExp pgf tenv@(k,_,_) e typ = do
|
||||
(e',w,cs1) <- infer pgf tenv e
|
||||
cs2 <- eqValue k w typ
|
||||
let cs2 = eqValue k w typ
|
||||
return (e',cs1 ++ cs2)
|
||||
|
||||
lookupEVar :: PGF -> TCEnv -> CId -> Err Value
|
||||
@@ -100,40 +97,12 @@ eins = Map.insert
|
||||
emptyTCEnv :: TCEnv
|
||||
emptyTCEnv = (0,eempty,eempty)
|
||||
|
||||
whnf :: Value -> Err Value
|
||||
whnf v = case v of
|
||||
VApp u w -> do
|
||||
u' <- whnf u
|
||||
w' <- whnf w
|
||||
return $ apply u' w'
|
||||
VClosure env e -> return $ eval env e
|
||||
_ -> return v
|
||||
|
||||
eqValue :: Int -> Value -> Value -> Err [(Value,Value)]
|
||||
eqValue k u1 u2 = do
|
||||
w1 <- whnf u1
|
||||
w2 <- whnf u2
|
||||
let v = VGen k
|
||||
case (w1,w2) of
|
||||
(VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqValue k f1 f2) (eqValue k a1 a2)
|
||||
(VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) ->
|
||||
eqValue (k+1) (VClosure (eins x1 v env1) e1) (VClosure (eins x2 v env2) e2)
|
||||
(VClosure env1 (EPi x1 a1 b1), VClosure env2 (EPi x2 a2 b2)) ->
|
||||
liftM2 (++)
|
||||
(eqValue k (VClosure env1 a1) (VClosure env2 a2))
|
||||
(eqValue (k+1) (VClosure (eins x1 v env1) b1) (VClosure (eins x2 v env2) b2))
|
||||
(VGen i, VGen j) -> return [(w1,w2) | i /= j]
|
||||
(VVar i, VVar j) -> return [(w1,w2) | i /= j]
|
||||
_ -> return [(w1,w2) | w1 /= w2]
|
||||
-- invariant: constraints are in whnf
|
||||
|
||||
|
||||
-- this is not given in Expr
|
||||
prValue = showExpr . value2expr
|
||||
|
||||
value2expr v = case v of
|
||||
VApp v u -> EApp (value2expr v) (value2expr u)
|
||||
VVar x -> EVar x
|
||||
VApp f vs -> foldl EApp (EVar f) (map value2expr vs)
|
||||
VMeta i -> EMeta i
|
||||
VClosure g e -> e ----
|
||||
VLit l -> ELit l
|
||||
|
||||
Reference in New Issue
Block a user