mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-07 02:02:51 -06:00
hopefully complete and correct typechecker in PGF
This commit is contained in:
krasimir
@@ -104,20 +104,24 @@ instance Binary Term where
|
||||
instance Binary Expr where
|
||||
put (EAbs x exp) = putWord8 0 >> put (x,exp)
|
||||
put (EApp e1 e2) = putWord8 1 >> put (e1,e2)
|
||||
put (EVar x) = putWord8 2 >> put x
|
||||
put (ELit (LStr s)) = putWord8 3 >> put s
|
||||
put (ELit (LFlt d)) = putWord8 4 >> put d
|
||||
put (ELit (LInt i)) = putWord8 5 >> put i
|
||||
put (EMeta i) = putWord8 6 >> put i
|
||||
put (ELit (LStr s)) = putWord8 2 >> put s
|
||||
put (ELit (LFlt d)) = putWord8 3 >> put d
|
||||
put (ELit (LInt i)) = putWord8 4 >> put i
|
||||
put (EMeta i) = putWord8 5 >> put i
|
||||
put (EFun f) = putWord8 6 >> put f
|
||||
put (EVar i) = putWord8 7 >> put i
|
||||
put (ETyped e ty) = putWord8 8 >> put (e,ty)
|
||||
get = do tag <- getWord8
|
||||
case tag of
|
||||
0 -> liftM2 EAbs get get
|
||||
1 -> liftM2 EApp get get
|
||||
2 -> liftM EVar get
|
||||
3 -> liftM (ELit . LStr) get
|
||||
4 -> liftM (ELit . LFlt) get
|
||||
5 -> liftM (ELit . LInt) get
|
||||
6 -> liftM EMeta get
|
||||
2 -> liftM (ELit . LStr) get
|
||||
3 -> liftM (ELit . LFlt) get
|
||||
4 -> liftM (ELit . LInt) get
|
||||
5 -> liftM EMeta get
|
||||
6 -> liftM EFun get
|
||||
7 -> liftM EVar get
|
||||
8 -> liftM2 ETyped get get
|
||||
_ -> decodingError
|
||||
|
||||
instance Binary Patt where
|
||||
|
||||
261
src/PGF/Expr.hs
261
src/PGF/Expr.hs
@@ -7,12 +7,12 @@ module PGF.Expr(Tree(..), Literal(..),
|
||||
tree2expr, expr2tree, normalForm,
|
||||
|
||||
-- needed in the typechecker
|
||||
Value(..), Env, eval, apply, eqValue,
|
||||
Value(..), Env, Funs, eval, apply,
|
||||
|
||||
MetaId,
|
||||
|
||||
-- helpers
|
||||
pStr,pFactor,
|
||||
pStr,pFactor,freshName,ppMeta
|
||||
) where
|
||||
|
||||
import PGF.CId
|
||||
@@ -20,16 +20,17 @@ import PGF.Type
|
||||
|
||||
import Data.Char
|
||||
import Data.Maybe
|
||||
import Data.List as List
|
||||
import Data.Map as Map hiding (showTree)
|
||||
import Control.Monad
|
||||
import qualified Text.PrettyPrint as PP
|
||||
import qualified Text.ParserCombinators.ReadP as RP
|
||||
import qualified Data.Map as Map
|
||||
|
||||
data Literal =
|
||||
LStr String -- ^ string constant
|
||||
| LInt Integer -- ^ integer constant
|
||||
| LFlt Double -- ^ floating point constant
|
||||
deriving (Eq,Ord)
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
type MetaId = Int
|
||||
|
||||
@@ -52,9 +53,10 @@ data Expr =
|
||||
| EApp Expr Expr -- ^ application
|
||||
| ELit Literal -- ^ literal
|
||||
| EMeta {-# UNPACK #-} !MetaId -- ^ meta variable
|
||||
| EVar CId -- ^ variable or function reference
|
||||
| EPi CId Expr Expr -- ^ dependent function type
|
||||
deriving (Eq,Ord)
|
||||
| EFun CId -- ^ function or data constructor
|
||||
| EVar {-# UNPACK #-} !Int -- ^ variable with de Bruijn index
|
||||
| ETyped Expr Type
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
-- | The pattern is used to define equations in the abstract syntax of the grammar.
|
||||
data Patt =
|
||||
@@ -94,12 +96,12 @@ readExpr s = case [x | (x,cs) <- RP.readP_to_S pExpr s, all isSpace cs] of
|
||||
[x] -> Just x
|
||||
_ -> Nothing
|
||||
|
||||
-- | renders expression as 'String'
|
||||
showExpr :: Expr -> String
|
||||
showExpr = PP.render . ppExpr 0
|
||||
|
||||
instance Show Expr where
|
||||
showsPrec i x = showString (PP.render (ppExpr i x))
|
||||
-- | renders expression as 'String'. The list
|
||||
-- of identifiers is the list of all free variables
|
||||
-- in the expression in order reverse to the order
|
||||
-- of binding.
|
||||
showExpr :: [CId] -> Expr -> String
|
||||
showExpr vars = PP.render . ppExpr 0 vars
|
||||
|
||||
instance Read Expr where
|
||||
readsPrec _ = RP.readP_to_S pExpr
|
||||
@@ -124,24 +126,31 @@ pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Li
|
||||
return (Fun f ts)
|
||||
|
||||
pExpr :: RP.ReadP Expr
|
||||
pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm)
|
||||
pExpr = pExpr0 >>= optTyped
|
||||
where
|
||||
pExpr0 = RP.skipSpaces >> (pAbs RP.<++ pTerm)
|
||||
|
||||
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
|
||||
e <- pExpr0
|
||||
return (foldr EAbs e xs)
|
||||
|
||||
pFactor = fmap EVar pCId
|
||||
optTyped e = do RP.skipSpaces
|
||||
RP.char ':'
|
||||
RP.skipSpaces
|
||||
ty <- pType
|
||||
return (ETyped e ty)
|
||||
RP.<++
|
||||
return e
|
||||
|
||||
pFactor = fmap EFun pCId
|
||||
RP.<++ fmap ELit pLit
|
||||
RP.<++ fmap EMeta pMeta
|
||||
RP.<++ RP.between (RP.char '(') (RP.char ')') pExpr
|
||||
|
||||
pMeta = do RP.char '?'
|
||||
cs <- RP.look
|
||||
case cs of
|
||||
(c:_) | isDigit c -> fmap read (RP.munch1 isDigit)
|
||||
_ -> return 0
|
||||
return 0
|
||||
|
||||
pLit :: RP.ReadP Literal
|
||||
pLit = pNum RP.<++ liftM LStr pStr
|
||||
@@ -161,35 +170,37 @@ pStr = RP.char '"' >> (RP.manyTill (pEsc RP.<++ RP.get) (RP.char '"'))
|
||||
-----------------------------------------------------
|
||||
|
||||
ppTree d (Abs xs t) = ppParens (d > 0) (PP.char '\\' PP.<>
|
||||
PP.hsep (PP.punctuate PP.comma (map (PP.text . prCId) xs)) PP.<+>
|
||||
PP.hsep (PP.punctuate PP.comma (List.map (PP.text . prCId) xs)) PP.<+>
|
||||
PP.text "->" PP.<+>
|
||||
ppTree 0 t)
|
||||
ppTree d (Fun f []) = PP.text (prCId f)
|
||||
ppTree d (Fun f ts) = ppParens (d > 0) (PP.text (prCId f) PP.<+> PP.hsep (map (ppTree 1) ts))
|
||||
ppTree d (Fun f ts) = ppParens (d > 0) (PP.text (prCId f) PP.<+> PP.hsep (List.map (ppTree 1) ts))
|
||||
ppTree d (Lit l) = ppLit l
|
||||
ppTree d (Meta n) = ppMeta 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.<+>
|
||||
PP.text "->" PP.<+>
|
||||
ppExpr 0 e1)
|
||||
where
|
||||
getVars (EAbs x e) = let (xs,e1) = getVars e in (x:xs,e1)
|
||||
getVars e = ([],e)
|
||||
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) = ppMeta n
|
||||
ppExpr d (EVar f) = PP.text (prCId f)
|
||||
ppExpr d (EPi x e1 e2)= PP.parens (PP.text (prCId x) PP.<+> PP.colon PP.<+> ppExpr 0 e1) PP.<+> PP.text "->" PP.<+> ppExpr 0 e2
|
||||
ppExpr :: Int -> [CId] -> Expr -> PP.Doc
|
||||
ppExpr d scope (EAbs x e) = let (xs,e1) = getVars [x] e
|
||||
in ppParens (d > 1) (PP.char '\\' PP.<>
|
||||
PP.hsep (PP.punctuate PP.comma (List.map (PP.text . prCId) (reverse xs))) PP.<+>
|
||||
PP.text "->" PP.<+>
|
||||
ppExpr 1 (xs++scope) e1)
|
||||
where
|
||||
getVars xs (EAbs x e) = getVars (freshName x xs:xs) e
|
||||
getVars xs e = (xs,e)
|
||||
ppExpr d scope (EApp e1 e2) = ppParens (d > 3) ((ppExpr 3 scope e1) PP.<+> (ppExpr 4 scope e2))
|
||||
ppExpr d scope (ELit l) = ppLit l
|
||||
ppExpr d scope (EMeta n) = ppMeta n
|
||||
ppExpr d scope (EFun f) = PP.text (prCId f)
|
||||
ppExpr d scope (EVar i) = PP.text (prCId (scope !! i))
|
||||
ppExpr d scope (ETyped e ty)= ppParens (d > 0) (ppExpr 0 scope e PP.<+> PP.colon PP.<+> ppType 0 scope ty)
|
||||
|
||||
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 '_'
|
||||
ppPatt d scope (PApp f ps) = let (scope',ds) = mapAccumL (ppPatt 2) scope ps
|
||||
in (scope',ppParens (not (List.null ps) && d > 1) (PP.text (prCId f) PP.<+> PP.hsep ds))
|
||||
ppPatt d scope (PLit l) = (scope,ppLit l)
|
||||
ppPatt d scope (PVar f) = (scope,PP.text (prCId f))
|
||||
ppPatt d scope PWild = (scope,PP.char '_')
|
||||
|
||||
ppLit (LStr s) = PP.text (show s)
|
||||
ppLit (LInt n) = PP.integer n
|
||||
@@ -203,6 +214,12 @@ ppMeta n
|
||||
ppParens True = PP.parens
|
||||
ppParens False = id
|
||||
|
||||
freshName :: CId -> [CId] -> CId
|
||||
freshName x xs = loop 1 x
|
||||
where
|
||||
loop i y
|
||||
| elem y xs = loop (i+1) (mkCId (show x++"'"++show i))
|
||||
| otherwise = y
|
||||
|
||||
-----------------------------------------------------
|
||||
-- Conversion Expr <-> Tree
|
||||
@@ -211,33 +228,38 @@ ppParens False = id
|
||||
-- | Converts a tree to expression. The conversion
|
||||
-- is always total, every tree is a valid expression.
|
||||
tree2expr :: Tree -> Expr
|
||||
tree2expr (Fun x ts) = foldl EApp (EVar x) (map tree2expr ts)
|
||||
tree2expr (Lit l) = ELit l
|
||||
tree2expr (Meta n) = EMeta n
|
||||
tree2expr (Abs xs t) = foldr EAbs (tree2expr t) xs
|
||||
tree2expr (Var x) = EVar x
|
||||
tree2expr = tree2expr []
|
||||
where
|
||||
tree2expr ys (Fun x ts) = foldl EApp (EFun x) (List.map (tree2expr ys) ts)
|
||||
tree2expr ys (Lit l) = ELit l
|
||||
tree2expr ys (Meta n) = EMeta n
|
||||
tree2expr ys (Abs xs t) = foldr EAbs (tree2expr (reverse xs++ys) t) xs
|
||||
tree2expr ys (Var x) = case List.lookup x (zip ys [0..]) of
|
||||
Just i -> EVar i
|
||||
Nothing -> error "unknown variable"
|
||||
|
||||
-- | Converts an expression to tree. The conversion is only partial.
|
||||
-- Variables and meta variables of function type and beta redexes are not allowed.
|
||||
expr2tree :: Expr -> Tree
|
||||
expr2tree e = abs [] [] e
|
||||
where
|
||||
abs ys xs (EAbs x e) = abs ys (x:xs) e
|
||||
abs ys xs e = case xs of
|
||||
[] -> app ys [] e
|
||||
xs -> Abs (reverse xs) (app (xs++ys) [] e)
|
||||
abs ys xs (EAbs x e) = abs ys (x:xs) e
|
||||
abs ys xs (ETyped e _) = abs ys xs e
|
||||
abs ys xs e = case xs of
|
||||
[] -> app ys [] e
|
||||
xs -> Abs (reverse xs) (app (xs++ys) [] e)
|
||||
|
||||
app xs as (EApp e1 e2) = app xs ((abs xs [] e2) : as) e1
|
||||
app xs as (EApp e1 e2) = app xs ((abs xs [] e2) : as) e1
|
||||
app xs as (ELit l)
|
||||
| null as = Lit l
|
||||
| otherwise = error "literal of function type encountered"
|
||||
| List.null as = Lit l
|
||||
| otherwise = error "literal of function type encountered"
|
||||
app xs as (EMeta n)
|
||||
| null as = Meta n
|
||||
| otherwise = error "meta variables of function type are not allowed in trees"
|
||||
app xs as (EAbs x e) = error "beta redexes are not allowed in trees"
|
||||
app xs as (EVar x)
|
||||
| x `elem` xs = Var x
|
||||
| otherwise = Fun x as
|
||||
| List.null as = Meta n
|
||||
| otherwise = error "meta variables of function type are not allowed in trees"
|
||||
app xs as (EAbs x e) = error "beta redexes are not allowed in trees"
|
||||
app xs as (EVar i) = Var (xs !! i)
|
||||
app xs as (EFun f) = Fun f as
|
||||
app xs as (ETyped e _) = app xs as e
|
||||
|
||||
|
||||
-----------------------------------------------------
|
||||
@@ -245,109 +267,84 @@ expr2tree e = abs [] [] e
|
||||
-----------------------------------------------------
|
||||
|
||||
-- | Compute an expression to normal form
|
||||
normalForm :: Funs -> Expr -> Expr
|
||||
normalForm funs e = value2expr 0 (eval funs Map.empty e)
|
||||
normalForm :: Funs -> Int -> Env -> Expr -> Expr
|
||||
normalForm funs k env e = value2expr k (eval funs env e)
|
||||
where
|
||||
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 (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 (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr i) vs)
|
||||
value2expr i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr i) vs)
|
||||
value2expr i (VMeta j env vs) = foldl EApp (EMeta j) (List.map (value2expr i) vs)
|
||||
value2expr i (VSusp j env vs k) = value2expr i (k (VGen j vs))
|
||||
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))
|
||||
|
||||
var i = mkCId ('v':show i)
|
||||
|
||||
ret [] t = t
|
||||
ret xs t = Abs (reverse xs) t
|
||||
value2expr i (VClosure env (EAbs x e)) = EAbs x (value2expr (i+1) (eval funs ((VGen i []):env) e))
|
||||
|
||||
data Value
|
||||
= VApp CId [Value]
|
||||
| VLit Literal
|
||||
| VMeta {-# UNPACK #-} !MetaId [Value]
|
||||
| VGen {-# UNPACK #-} !MetaId [Value]
|
||||
| VSusp {-# UNPACK #-} !MetaId [Value] (Value -> Value)
|
||||
| VMeta {-# UNPACK #-} !MetaId Env [Value]
|
||||
| VSusp {-# UNPACK #-} !MetaId Env [Value] (Value -> Value)
|
||||
| VGen {-# UNPACK #-} !Int [Value]
|
||||
| VClosure Env Expr
|
||||
|
||||
type Funs = Map.Map CId (Type,Int,[Equation]) -- type and def of a fun
|
||||
type Env = Map.Map CId Value
|
||||
type Env = [Value]
|
||||
|
||||
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 (_,a,eqs) -> if a == 0
|
||||
then case eqs of
|
||||
Equ [] e : _ -> eval funs Map.empty e
|
||||
_ -> VApp x []
|
||||
else VApp x []
|
||||
Nothing -> error ("unknown variable "++prCId x)
|
||||
eval funs env (EVar i) = env !! i
|
||||
eval funs env (EFun f) = case Map.lookup f funs of
|
||||
Just (_,a,eqs) -> if a == 0
|
||||
then case eqs of
|
||||
Equ [] e : _ -> eval funs [] e
|
||||
_ -> VApp f []
|
||||
else VApp f []
|
||||
Nothing -> error ("unknown function "++prCId f)
|
||||
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 (EMeta i) = VMeta i env []
|
||||
eval funs env (ELit l) = VLit l
|
||||
eval funs env (EPi x e1 e2)= VClosure env (EPi x e1 e2)
|
||||
eval funs env (ETyped e _) = eval funs env e
|
||||
|
||||
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 -> applyValue funs env v vs
|
||||
Nothing -> case Map.lookup x funs of
|
||||
Just (_,a,eqs) -> if a <= length vs
|
||||
then let (as,vs') = splitAt a vs
|
||||
in match funs x eqs as vs'
|
||||
else VApp x vs
|
||||
Nothing -> error ("unknown variable "++prCId x)
|
||||
apply funs env (EVar i) vs = applyValue funs (env !! i) vs
|
||||
apply funs env (EFun f) vs = case Map.lookup f funs of
|
||||
Just (_,a,eqs) -> if a <= length vs
|
||||
then let (as,vs') = splitAt a vs
|
||||
in match funs f eqs as vs'
|
||||
else VApp f vs
|
||||
Nothing -> error ("unknown function "++prCId f)
|
||||
apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs)
|
||||
apply funs env (EAbs x e) (v:vs) = apply funs (Map.insert x v env) e vs
|
||||
apply funs env (EMeta k) vs = VMeta k vs
|
||||
apply funs env (EAbs x e) (v:vs) = apply funs (v:env) e vs
|
||||
apply funs env (EMeta i) vs = VMeta i env vs
|
||||
apply funs env (ELit l) vs = error "literal of function type"
|
||||
apply funs env (ETyped e _) vs = apply funs env e vs
|
||||
|
||||
applyValue funs env (VApp f vs0) vs = apply funs env (EVar f) (vs0++vs)
|
||||
applyValue funs env (VLit _) vs = error "literal of function type"
|
||||
applyValue funs env (VMeta i vs0) vs = VMeta i (vs0++vs)
|
||||
applyValue funs env (VGen i vs0) vs = VGen i (vs0++vs)
|
||||
applyValue funs env (VSusp i vs0 k) vs = VSusp i vs0 (\v -> applyValue funs env (k v) vs)
|
||||
applyValue funs _ (VClosure env (EAbs x e)) (v:vs) = apply funs (Map.insert x v env) e vs
|
||||
applyValue funs v [] = v
|
||||
applyValue funs (VApp f vs0) vs = apply funs [] (EFun f) (vs0++vs)
|
||||
applyValue funs (VLit _) vs = error "literal of function type"
|
||||
applyValue funs (VMeta i env vs0) vs = VMeta i env (vs0++vs)
|
||||
applyValue funs (VGen i vs0) vs = VGen i (vs0++vs)
|
||||
applyValue funs (VSusp i env vs0 k) vs = VSusp i env vs0 (\v -> applyValue funs (k v) vs)
|
||||
applyValue funs (VClosure env (EAbs x e)) (v:vs) = apply funs (v:env) e vs
|
||||
|
||||
-----------------------------------------------------
|
||||
-- Pattern matching
|
||||
-----------------------------------------------------
|
||||
|
||||
match :: Funs -> CId -> [Equation] -> [Value] -> [Value] -> Value
|
||||
match funs f eqs as0 vs0 =
|
||||
match sig f eqs as0 vs0 =
|
||||
case eqs of
|
||||
[] -> VApp f (as0++vs0)
|
||||
(Equ ps res):eqs -> tryMatches eqs ps as0 res Map.empty
|
||||
(Equ ps res):eqs -> tryMatches eqs ps as0 res []
|
||||
where
|
||||
tryMatches eqs [] [] res env = apply funs env res vs0
|
||||
tryMatches eqs [] [] res env = apply sig env res vs0
|
||||
tryMatches eqs (p:ps) (a:as) res env = tryMatch p a env
|
||||
where
|
||||
tryMatch (PVar x ) (v ) env = tryMatches eqs ps as res (Map.insert x v env)
|
||||
tryMatch (PWild ) (_ ) env = tryMatches eqs ps as res env
|
||||
tryMatch (p ) (VMeta i vs ) env = VSusp i vs (\v -> tryMatch p v env)
|
||||
tryMatch (p ) (VGen i vs ) env = VApp f (as0++vs0)
|
||||
tryMatch (p ) (VSusp i vs k) env = VSusp i vs (\v -> tryMatch p (k v) env)
|
||||
tryMatch (PApp f1 ps1) (VApp f2 vs2 ) env | f1 == f2 = tryMatches eqs (ps1++ps) (vs2++as) res env
|
||||
tryMatch (PLit l1 ) (VLit l2 ) env | l1 == l2 = tryMatches eqs ps as res env
|
||||
tryMatch _ _ env = match funs f eqs as0 vs0
|
||||
|
||||
|
||||
-----------------------------------------------------
|
||||
-- Equality checking
|
||||
-----------------------------------------------------
|
||||
|
||||
eqValue :: Funs -> Int -> Value -> Value -> [(Value,Value)]
|
||||
eqValue funs k v1 v2 =
|
||||
case (whnf v1,whnf v2) of
|
||||
(VApp f1 vs1, VApp f2 vs2) | f1 == f2 -> concat (zipWith (eqValue funs k) vs1 vs2)
|
||||
(VLit l1, VLit l2 ) | l1 == l2 -> []
|
||||
(VMeta i vs1, VMeta j vs2) | i == j -> concat (zipWith (eqValue funs k) vs1 vs2)
|
||||
(VGen i vs1, VGen j vs2) | i == j -> concat (zipWith (eqValue funs k) vs1 vs2)
|
||||
(VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) ->
|
||||
let v = VGen k []
|
||||
in eqValue funs (k+1) (VClosure (Map.insert x1 v env1) e1) (VClosure (Map.insert x2 v env2) e2)
|
||||
_ -> [(v1,v2)]
|
||||
where
|
||||
whnf (VClosure env e) = eval funs env e -- should be removed when the typechecker is improved
|
||||
whnf v = v
|
||||
tryMatch (PVar x ) (v ) env = tryMatches eqs ps as res (v:env)
|
||||
tryMatch (PWild ) (_ ) env = tryMatches eqs ps as res env
|
||||
tryMatch (p ) (VMeta i envi vs ) env = VSusp i envi vs (\v -> tryMatch p v env)
|
||||
tryMatch (p ) (VGen i vs ) env = VApp f (as0++vs0)
|
||||
tryMatch (p ) (VSusp i envi vs k) env = VSusp i envi vs (\v -> tryMatch p (k v) env)
|
||||
tryMatch (PApp f1 ps1) (VApp f2 vs2 ) env | f1 == f2 = tryMatches eqs (ps1++ps) (vs2++as) res env
|
||||
tryMatch (PLit l1 ) (VLit l2 ) env | l1 == l2 = tryMatches eqs ps as res env
|
||||
tryMatch _ _ env = match sig f eqs as0 vs0
|
||||
|
||||
|
||||
@@ -1,13 +1,17 @@
|
||||
module PGF.Expr where
|
||||
|
||||
import PGF.CId
|
||||
import qualified Text.PrettyPrint as PP
|
||||
import qualified Text.ParserCombinators.ReadP as RP
|
||||
|
||||
data Expr
|
||||
|
||||
instance Eq Expr
|
||||
instance Ord Expr
|
||||
instance Eq Expr
|
||||
instance Ord Expr
|
||||
instance Show Expr
|
||||
|
||||
pFactor :: RP.ReadP Expr
|
||||
|
||||
ppExpr :: Int -> Expr -> PP.Doc
|
||||
ppExpr :: Int -> [CId] -> Expr -> PP.Doc
|
||||
|
||||
freshName :: CId -> [CId] -> CId
|
||||
@@ -5,22 +5,22 @@ module PGF.Type ( Type(..), Hypo(..),
|
||||
import PGF.CId
|
||||
import {-# SOURCE #-} PGF.Expr
|
||||
import Data.Char
|
||||
import Data.List
|
||||
import qualified Text.PrettyPrint as PP
|
||||
import qualified Text.ParserCombinators.ReadP as RP
|
||||
import Control.Monad
|
||||
import Debug.Trace
|
||||
|
||||
-- | To read a type from a 'String', use 'read' or 'readType'.
|
||||
data Type =
|
||||
DTyp [Hypo] CId [Expr]
|
||||
deriving (Eq,Ord)
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
-- | 'Hypo' represents a hypothesis in a type i.e. in the type A -> B, A is the hypothesis
|
||||
data Hypo =
|
||||
Hyp Type -- ^ hypothesis without bound variable like in A -> B
|
||||
| HypV CId Type -- ^ hypothesis with bound variable like in (x : A) -> B x
|
||||
| HypI CId Type -- ^ hypothesis with bound implicit variable like in {x : A} -> B x
|
||||
deriving (Eq,Ord)
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
-- | Reads a 'Type' from a 'String'.
|
||||
readType :: String -> Maybe Type
|
||||
@@ -28,15 +28,12 @@ readType s = case [x | (x,cs) <- RP.readP_to_S pType s, all isSpace cs] of
|
||||
[x] -> Just x
|
||||
_ -> Nothing
|
||||
|
||||
instance Show Type where
|
||||
showsPrec i x = showString (PP.render (ppType i x))
|
||||
|
||||
instance Read Type where
|
||||
readsPrec _ = RP.readP_to_S pType
|
||||
|
||||
-- | renders type as 'String'
|
||||
showType :: Type -> String
|
||||
showType = PP.render . ppType 0
|
||||
-- | renders type as 'String'. The list
|
||||
-- of identifiers is the list of all free variables
|
||||
-- in the expression in order reverse to the order
|
||||
-- of binding.
|
||||
showType :: [CId] -> Type -> String
|
||||
showType vars = PP.render . ppType 0 vars
|
||||
|
||||
pType :: RP.ReadP Type
|
||||
pType = do
|
||||
@@ -72,17 +69,19 @@ pType = do
|
||||
args <- RP.sepBy pFactor RP.skipSpaces
|
||||
return (cat, args)
|
||||
|
||||
ppType :: Int -> Type -> PP.Doc
|
||||
ppType d (DTyp ctxt cat args)
|
||||
| null ctxt = ppRes cat args
|
||||
| otherwise = ppParens (d > 0) (foldr ppCtxt (ppRes cat args) ctxt)
|
||||
ppType :: Int -> [CId] -> Type -> PP.Doc
|
||||
ppType d scope (DTyp hyps cat args)
|
||||
| null hyps = ppRes scope cat args
|
||||
| otherwise = let (scope',hdocs) = mapAccumL ppHypo scope hyps
|
||||
in ppParens (d > 0) (foldr (\hdoc doc -> hdoc PP.<+> PP.text "->" PP.<+> doc) (ppRes scope' cat args) hdocs)
|
||||
where
|
||||
ppCtxt hyp doc = ppHypo hyp PP.<+> PP.text "->" PP.<+> doc
|
||||
ppRes cat es = PP.text (prCId cat) PP.<+> PP.hsep (map (ppExpr 2) es)
|
||||
ppRes scope cat es = PP.text (prCId cat) PP.<+> PP.hsep (map (ppExpr 4 scope) es)
|
||||
|
||||
ppHypo (Hyp typ) = ppType 1 typ
|
||||
ppHypo (HypV x typ) = PP.parens (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)
|
||||
ppHypo (HypI x typ) = PP.braces (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)
|
||||
ppHypo scope (Hyp typ) = ( scope,ppType 1 scope typ)
|
||||
ppHypo scope (HypV x typ) = let y = freshName x scope
|
||||
in (y:scope,PP.parens (PP.text (prCId y) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
ppHypo scope (HypI x typ) = let y = freshName x scope
|
||||
in (y:scope,PP.braces (PP.text (prCId y) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
|
||||
ppParens :: Bool -> PP.Doc -> PP.Doc
|
||||
ppParens True = PP.parens
|
||||
|
||||
@@ -1,201 +1,463 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : TypeCheck
|
||||
-- Maintainer : AR
|
||||
-- Module : PGF.TypeCheck
|
||||
-- Maintainer : Krasimir Angelov
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- type checking in abstract syntax with dependent types.
|
||||
-- Type checking in abstract syntax with dependent types.
|
||||
-- The type checker also performs renaming and checking for unknown
|
||||
-- functions. The variable references are replaced by de Bruijn indices.
|
||||
--
|
||||
-- modified from src GF TC
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module PGF.TypeCheck (
|
||||
typecheck
|
||||
) where
|
||||
module PGF.TypeCheck (checkType, checkExpr, inferExpr,
|
||||
|
||||
ppTcError, TcError(..)
|
||||
) where
|
||||
|
||||
import PGF.Data
|
||||
import PGF.Macros (lookDef,isData)
|
||||
import PGF.Expr
|
||||
import PGF.Macros (typeOfHypo)
|
||||
import PGF.CId
|
||||
|
||||
import GF.Data.ErrM
|
||||
import qualified Data.Map as Map
|
||||
import Control.Monad (liftM2,foldM)
|
||||
import Data.List (partition,sort,groupBy)
|
||||
import Data.Map as Map
|
||||
import Data.IntMap as IntMap
|
||||
import Data.Maybe as Maybe
|
||||
import Data.List as List
|
||||
import Control.Monad
|
||||
import Text.PrettyPrint
|
||||
|
||||
import Debug.Trace
|
||||
-----------------------------------------------------
|
||||
-- The Scope
|
||||
-----------------------------------------------------
|
||||
|
||||
typecheck :: PGF -> Expr -> [Expr]
|
||||
typecheck pgf e = case inferExpr pgf (newMetas e) of
|
||||
Ok e -> [e]
|
||||
Bad s -> trace s []
|
||||
data TType = TTyp Env Type
|
||||
newtype Scope = Scope [(CId,TType)]
|
||||
|
||||
inferExpr :: PGF -> Expr -> Err Expr
|
||||
inferExpr pgf e = case infer pgf emptyTCEnv e of
|
||||
Ok (e,_,cs) -> let (ms,cs2) = splitConstraints pgf cs in case cs2 of
|
||||
[] -> trace (prConstraints cs ++"\n"++ show ms) $ Ok (metaSubst ms e)
|
||||
_ -> Bad ("Error in tree " ++ showExpr e ++ " :\n " ++ prConstraints cs2)
|
||||
Bad s -> Bad s
|
||||
emptyScope = Scope []
|
||||
|
||||
infer :: PGF -> TCEnv -> Expr -> Err (Expr, Value, [(Value,Value)])
|
||||
infer pgf tenv@(k,rho,gamma) e = case e of
|
||||
EVar x -> do
|
||||
ty <- lookupEVar pgf tenv x
|
||||
return (e,ty,[])
|
||||
addScopedVar :: CId -> TType -> Scope -> Scope
|
||||
addScopedVar x tty (Scope gamma) = Scope ((x,tty):gamma)
|
||||
|
||||
-- EInt i -> return (AInt i, valAbsInt, [])
|
||||
-- EFloat i -> return (AFloat i, valAbsFloat, [])
|
||||
-- K i -> return (AStr i, valAbsString, [])
|
||||
-- | returns the type and the De Bruijn index of a local variable
|
||||
lookupVar :: CId -> Scope -> Maybe (Int,TType)
|
||||
lookupVar x (Scope gamma) = listToMaybe [(i,tty) | ((y,tty),i) <- zip gamma [0..], x == y]
|
||||
|
||||
EApp f t -> do
|
||||
(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)
|
||||
let b' = eval (getFunEnv (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)
|
||||
-- | returns the type and the name of a local variable
|
||||
getVar :: Int -> Scope -> (CId,TType)
|
||||
getVar i (Scope gamma) = gamma !! i
|
||||
|
||||
scopeEnv :: Scope -> Env
|
||||
scopeEnv (Scope gamma) = let n = length gamma
|
||||
in [VGen (n-i-1) [] | i <- [0..n-1]]
|
||||
|
||||
checkExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
|
||||
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
|
||||
let a' = eval (getFunEnv (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)
|
||||
_ -> Bad ("function type expected for " ++ show e)
|
||||
_ -> checkInferExp pgf tenv e typ
|
||||
scopeVars :: Scope -> [CId]
|
||||
scopeVars (Scope gamma) = List.map fst gamma
|
||||
|
||||
getFunEnv abs = Map.union (funs abs) (Map.map (\hypos -> (DTyp hypos cidType [],0,[])) (cats abs))
|
||||
scopeSize :: Scope -> Int
|
||||
scopeSize (Scope gamma) = length gamma
|
||||
|
||||
-----------------------------------------------------
|
||||
-- The Monad
|
||||
-----------------------------------------------------
|
||||
|
||||
type MetaStore = IntMap MetaValue
|
||||
data MetaValue
|
||||
= MUnbound Scope [Expr -> TcM ()]
|
||||
| MBound Expr
|
||||
| MGuarded Expr [Expr -> TcM ()] {-# UNPACK #-} !Int -- the Int is the number of constraints that have to be solved
|
||||
-- to unlock this meta variable
|
||||
|
||||
newtype TcM a = TcM {unTcM :: Abstr -> MetaId -> MetaStore -> TcResult a}
|
||||
data TcResult a
|
||||
= Ok {-# UNPACK #-} !MetaId MetaStore a
|
||||
| Fail TcError
|
||||
|
||||
instance Monad TcM where
|
||||
return x = TcM (\abstr metaid ms -> Ok metaid ms x)
|
||||
f >>= g = TcM (\abstr metaid ms -> case unTcM f abstr metaid ms of
|
||||
Ok metaid ms x -> unTcM (g x) abstr metaid ms
|
||||
Fail e -> Fail e)
|
||||
|
||||
instance Functor TcM where
|
||||
fmap f x = TcM (\abstr metaid ms -> case unTcM x abstr metaid ms of
|
||||
Ok metaid ms x -> Ok metaid ms (f x)
|
||||
Fail e -> Fail e)
|
||||
|
||||
lookupCatHyps :: CId -> TcM [Hypo]
|
||||
lookupCatHyps cat = TcM (\abstr metaid ms -> case Map.lookup cat (cats abstr) of
|
||||
Just hyps -> Ok metaid ms hyps
|
||||
Nothing -> Fail (UnknownCat cat))
|
||||
|
||||
lookupFunType :: CId -> TcM TType
|
||||
lookupFunType fun = TcM (\abstr metaid ms -> case Map.lookup fun (funs abstr) of
|
||||
Just (ty,_,_) -> Ok metaid ms (TTyp [] ty)
|
||||
Nothing -> Fail (UnknownFun fun))
|
||||
|
||||
newMeta :: Scope -> TcM MetaId
|
||||
newMeta scope = TcM (\abstr metaid ms -> Ok (metaid+1) (IntMap.insert metaid (MUnbound scope []) ms) metaid)
|
||||
|
||||
newGuardedMeta :: Scope -> Expr -> TcM MetaId
|
||||
newGuardedMeta scope e = getFuns >>= \funs -> TcM (\abstr metaid ms -> Ok (metaid+1) (IntMap.insert metaid (MGuarded e [] 0) ms) metaid)
|
||||
|
||||
getMeta :: MetaId -> TcM MetaValue
|
||||
getMeta i = TcM (\abstr metaid ms -> Ok metaid ms $! case IntMap.lookup i ms of
|
||||
Just mv -> mv)
|
||||
setMeta :: MetaId -> MetaValue -> TcM ()
|
||||
setMeta i mv = TcM (\abstr metaid ms -> Ok metaid (IntMap.insert i mv ms) ())
|
||||
|
||||
tcError :: TcError -> TcM a
|
||||
tcError e = TcM (\abstr metaid ms -> Fail e)
|
||||
|
||||
getFuns :: TcM Funs
|
||||
getFuns = TcM (\abstr metaid ms -> Ok metaid ms (funs abstr))
|
||||
|
||||
addConstraint :: MetaId -> MetaId -> Env -> [Value] -> (Value -> TcM ()) -> TcM ()
|
||||
addConstraint i j env vs c = do
|
||||
funs <- getFuns
|
||||
mv <- getMeta j
|
||||
case mv of
|
||||
MUnbound scope cs -> addRef >> setMeta j (MUnbound scope ((\e -> release >> c (apply funs env e vs)) : cs))
|
||||
MBound e -> c (apply funs env e vs)
|
||||
MGuarded e cs x | x == 0 -> c (apply funs env e vs)
|
||||
| otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> c (apply funs env e vs)) : cs) x)
|
||||
where
|
||||
cidType = mkCId "Type"
|
||||
addRef = TcM (\abstr metaid ms -> case IntMap.lookup i ms of
|
||||
Just (MGuarded e cs x) -> Ok metaid (IntMap.insert i (MGuarded e cs (x+1)) ms) ())
|
||||
|
||||
checkInferExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
|
||||
checkInferExp pgf tenv@(k,_,_) e typ = do
|
||||
(e',w,cs1) <- infer pgf tenv e
|
||||
let cs2 = eqValue (getFunEnv (abstract pgf)) k w typ
|
||||
return (e',cs1 ++ cs2)
|
||||
|
||||
lookupEVar :: PGF -> TCEnv -> CId -> Err Value
|
||||
lookupEVar pgf (_,g,_) x = case Map.lookup x g of
|
||||
Just v -> return v
|
||||
_ -> maybe (Bad "var not found") (return . VClosure eempty . type2expr . (\(a,b,c) -> a)) $
|
||||
Map.lookup x (funs (abstract pgf))
|
||||
release = TcM (\abstr metaid ms -> case IntMap.lookup i ms of
|
||||
Just (MGuarded e cs x) -> if x == 1
|
||||
then unTcM (sequence_ [c e | c <- cs]) abstr metaid (IntMap.insert i (MGuarded e [] 0) ms)
|
||||
else Ok metaid (IntMap.insert i (MGuarded e cs (x-1)) ms) ())
|
||||
|
||||
type2expr :: Type -> Expr
|
||||
type2expr (DTyp hyps cat es) =
|
||||
foldr (uncurry EPi) (foldl EApp (EVar cat) es) [toPair h | h <- hyps]
|
||||
-----------------------------------------------------
|
||||
-- Type errors
|
||||
-----------------------------------------------------
|
||||
|
||||
data TcError
|
||||
= UnknownCat CId
|
||||
| UnknownFun CId
|
||||
| WrongCatArgs Scope Type CId Int Int
|
||||
| TypeMismatch Scope Expr Type Type
|
||||
| NotFunType Scope Expr Type
|
||||
| CannotInferType Scope Expr
|
||||
| UnresolvedMetaVars Scope Expr [MetaId]
|
||||
|
||||
ppTcError :: TcError -> Doc
|
||||
ppTcError (UnknownCat cat) = text "Category" <+> text (prCId cat) <+> text "is not in scope"
|
||||
ppTcError (UnknownFun fun) = text "Function" <+> text (prCId fun) <+> text "is not in scope"
|
||||
ppTcError (WrongCatArgs scope ty cat m n) =
|
||||
text "Category" <+> text (prCId cat) <+> text "should have" <+> int m <+> text "argument(s), but has been given" <+> int n $$
|
||||
text "In the type:" <+> ppType 0 (scopeVars scope) ty
|
||||
ppTcError (TypeMismatch scope e ty1 ty2) = text "Couldn't match expected type" <+> ppType 0 (scopeVars scope) ty1 $$
|
||||
text " against inferred type" <+> ppType 0 (scopeVars scope) ty2 $$
|
||||
text "In the expression:" <+> ppExpr 0 (scopeVars scope) e
|
||||
ppTcError (NotFunType scope e ty) = text "A function type is expected for the expression" <+> ppExpr 0 (scopeVars scope) e <+> text "instead of type" <+> ppType 0 (scopeVars scope) ty
|
||||
ppTcError (CannotInferType scope e) = text "Cannot infer the type of expression" <+> ppExpr 0 (scopeVars scope) e
|
||||
ppTcError (UnresolvedMetaVars scope e xs) = text "Meta variable(s)" <+> fsep (List.map ppMeta xs) <+> text "should be resolved" $$
|
||||
text "in the expression:" <+> ppExpr 0 (scopeVars scope) e
|
||||
|
||||
-----------------------------------------------------
|
||||
-- checkType
|
||||
-----------------------------------------------------
|
||||
|
||||
checkType :: PGF -> Type -> Either TcError Type
|
||||
checkType pgf ty =
|
||||
case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) 0 IntMap.empty of
|
||||
Ok _ ms ty -> Right ty
|
||||
Fail err -> Left err
|
||||
|
||||
tcType :: Scope -> Type -> TcM Type
|
||||
tcType scope ty@(DTyp hyps cat es) = do
|
||||
(scope,hyps) <- tcHypos scope hyps
|
||||
c_hyps <- lookupCatHyps cat
|
||||
let m = length es
|
||||
n = length c_hyps
|
||||
if m == n
|
||||
then do (delta,es) <- tcHypoExprs scope [] (zip es c_hyps)
|
||||
return (DTyp hyps cat es)
|
||||
else tcError (WrongCatArgs scope ty cat n m)
|
||||
|
||||
tcHypos :: Scope -> [Hypo] -> TcM (Scope,[Hypo])
|
||||
tcHypos scope [] = return (scope,[])
|
||||
tcHypos scope (h:hs) = do
|
||||
(scope,h ) <- tcHypo scope h
|
||||
(scope,hs) <- tcHypos scope hs
|
||||
return (scope,h:hs)
|
||||
|
||||
tcHypo :: Scope -> Hypo -> TcM (Scope,Hypo)
|
||||
tcHypo scope (Hyp ty) = do
|
||||
ty <- tcType scope ty
|
||||
return (scope,Hyp ty)
|
||||
tcHypo scope (HypV x ty) = do
|
||||
ty <- tcType scope ty
|
||||
return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,HypV x ty)
|
||||
|
||||
tcHypoExprs :: Scope -> Env -> [(Expr,Hypo)] -> TcM (Env,[Expr])
|
||||
tcHypoExprs scope delta [] = return (delta,[])
|
||||
tcHypoExprs scope delta ((e,h):xs) = do
|
||||
(delta,e ) <- tcHypoExpr scope delta e h
|
||||
(delta,es) <- tcHypoExprs scope delta xs
|
||||
return (delta,e:es)
|
||||
|
||||
tcHypoExpr :: Scope -> Env -> Expr -> Hypo -> TcM (Env,Expr)
|
||||
tcHypoExpr scope delta e (Hyp ty) = do
|
||||
e <- tcExpr scope e (TTyp delta ty)
|
||||
return (delta,e)
|
||||
tcHypoExpr scope delta e (HypV x ty) = do
|
||||
e <- tcExpr scope e (TTyp delta ty)
|
||||
funs <- getFuns
|
||||
return (eval funs (scopeEnv scope) e:delta,e)
|
||||
|
||||
|
||||
-----------------------------------------------------
|
||||
-- checkExpr
|
||||
-----------------------------------------------------
|
||||
|
||||
checkExpr :: PGF -> Expr -> Type -> Either TcError Expr
|
||||
checkExpr pgf e ty =
|
||||
case unTcM (do e <- tcExpr emptyScope e (TTyp [] ty)
|
||||
e <- refineExpr e
|
||||
checkResolvedMetaStore emptyScope e
|
||||
return e) (abstract pgf) 0 IntMap.empty of
|
||||
Ok _ ms e -> Right e
|
||||
Fail err -> Left err
|
||||
|
||||
tcExpr :: Scope -> Expr -> TType -> TcM Expr
|
||||
tcExpr scope e0@(EAbs x e) tty =
|
||||
case tty of
|
||||
TTyp delta (DTyp (h:hs) c es) -> do e <- case h of
|
||||
Hyp ty -> tcExpr (addScopedVar x (TTyp delta ty) scope)
|
||||
e (TTyp delta (DTyp hs c es))
|
||||
HypV y ty -> tcExpr (addScopedVar x (TTyp delta ty) scope)
|
||||
e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
|
||||
return (EAbs x e)
|
||||
_ -> do ty <- evalType (scopeSize scope) tty
|
||||
tcError (NotFunType scope e0 ty)
|
||||
tcExpr scope (EMeta _) tty = do
|
||||
i <- newMeta scope
|
||||
return (EMeta i)
|
||||
tcExpr scope e0 tty = do
|
||||
(e0,tty0) <- infExpr scope e0
|
||||
i <- newGuardedMeta scope e0
|
||||
eqType scope (scopeSize scope) i tty tty0
|
||||
return (EMeta i)
|
||||
|
||||
|
||||
-----------------------------------------------------
|
||||
-- inferExpr
|
||||
-----------------------------------------------------
|
||||
|
||||
inferExpr :: PGF -> Expr -> Either TcError (Expr,Type)
|
||||
inferExpr pgf e =
|
||||
case unTcM (do (e,tty) <- infExpr emptyScope e
|
||||
e <- refineExpr e
|
||||
checkResolvedMetaStore emptyScope e
|
||||
ty <- evalType 0 tty
|
||||
return (e,ty)) (abstract pgf) 1 IntMap.empty of
|
||||
Ok _ ms (e,ty) -> Right (e,ty)
|
||||
Fail err -> Left err
|
||||
|
||||
infExpr :: Scope -> Expr -> TcM (Expr,TType)
|
||||
infExpr scope e0@(EApp e1 e2) = do
|
||||
(e1,tty1) <- infExpr scope e1
|
||||
case tty1 of
|
||||
(TTyp delta1 (DTyp (h:hs) c es)) -> do (delta1,e2) <- tcHypoExpr scope delta1 e2 h
|
||||
return (EApp e1 e2,TTyp delta1 (DTyp hs c es))
|
||||
_ -> do ty1 <- evalType (scopeSize scope) tty1
|
||||
tcError (NotFunType scope e1 ty1)
|
||||
infExpr scope e0@(EFun x) = do
|
||||
case lookupVar x scope of
|
||||
Just (i,tty) -> return (EVar i,tty)
|
||||
Nothing -> do tty <- lookupFunType x
|
||||
return (e0,tty)
|
||||
infExpr scope e0@(EVar i) = do
|
||||
return (e0,snd (getVar i scope))
|
||||
infExpr scope e0@(ELit l) = do
|
||||
let cat = case l of
|
||||
LStr _ -> mkCId "String"
|
||||
LInt _ -> mkCId "Int"
|
||||
LFlt _ -> mkCId "Float"
|
||||
return (e0,TTyp [] (DTyp [] cat []))
|
||||
infExpr scope (ETyped e ty) = do
|
||||
ty <- tcType scope ty
|
||||
e <- tcExpr scope e (TTyp (scopeEnv scope) ty)
|
||||
return (ETyped e ty,TTyp (scopeEnv scope) ty)
|
||||
infExpr scope e = tcError (CannotInferType scope e)
|
||||
|
||||
-----------------------------------------------------
|
||||
-- eqType
|
||||
-----------------------------------------------------
|
||||
|
||||
eqType :: Scope -> Int -> MetaId -> TType -> TType -> TcM ()
|
||||
eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 ty2@(DTyp hyps2 cat2 es2))
|
||||
| cat1 == cat2 = do (k,delta1,delta2) <- eqHyps k delta1 hyps1 delta2 hyps2
|
||||
sequence_ [eqExpr k delta1 e1 delta2 e2 | (e1,e2) <- zip es1 es2]
|
||||
| otherwise = raiseTypeMatchError
|
||||
where
|
||||
toPair (Hyp t) = (wildCId, type2expr t)
|
||||
toPair (HypV x t) = (x, type2expr t)
|
||||
raiseTypeMatchError = do ty1 <- evalType k tty1
|
||||
ty2 <- evalType k tty2
|
||||
e <- refineExpr (EMeta i0)
|
||||
tcError (TypeMismatch scope e ty1 ty2)
|
||||
|
||||
type TCEnv = (Int,Env,Env)
|
||||
eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM (Int,Env,Env)
|
||||
eqHyps k delta1 [] delta2 [] =
|
||||
return (k,delta1,delta2)
|
||||
eqHyps k delta1 (Hyp ty1 : h1s) delta2 (Hyp ty2 : h2s) = do
|
||||
eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2)
|
||||
(k,delta1,delta2) <- eqHyps k delta1 h1s delta2 h2s
|
||||
return (k,delta1,delta2)
|
||||
eqHyps k delta1 (HypV x ty1 : h1s) delta2 (HypV y ty2 : h2s) = do
|
||||
eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2)
|
||||
(k,delta1,delta2) <- eqHyps (k+1) ((VGen k []):delta1) h1s ((VGen k []):delta2) h2s
|
||||
return (k,delta1,delta2)
|
||||
eqHyps k delta1 h1s delta2 h2s = raiseTypeMatchError
|
||||
|
||||
eempty = Map.empty
|
||||
eins = Map.insert
|
||||
eqExpr :: Int -> Env -> Expr -> Env -> Expr -> TcM ()
|
||||
eqExpr k env1 e1 env2 e2 = do
|
||||
funs <- getFuns
|
||||
eqValue k (eval funs env1 e1) (eval funs env2 e2)
|
||||
|
||||
emptyTCEnv :: TCEnv
|
||||
emptyTCEnv = (0,eempty,eempty)
|
||||
eqValue :: Int -> Value -> Value -> TcM ()
|
||||
eqValue k v1 v2 = do
|
||||
v1 <- deRef v1
|
||||
v2 <- deRef v2
|
||||
eqValue' k v1 v2
|
||||
|
||||
deRef v@(VMeta i env vs) = do
|
||||
mv <- getMeta i
|
||||
funs <- getFuns
|
||||
case mv of
|
||||
MBound e -> deRef (apply funs env e vs)
|
||||
MGuarded e _ x | x == 0 -> deRef (apply funs env e vs)
|
||||
| otherwise -> return v
|
||||
MUnbound _ _ -> return v
|
||||
deRef v = return v
|
||||
|
||||
eqValue' k (VSusp i env vs1 c) v2 = addConstraint i0 i env vs1 (\v1 -> eqValue k (c v1) v2)
|
||||
eqValue' k v1 (VSusp i env vs2 c) = addConstraint i0 i env vs2 (\v2 -> eqValue k v1 (c v2))
|
||||
eqValue' k (VMeta i env1 vs1) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2
|
||||
eqValue' k (VMeta i env1 vs1) v2 = do (MUnbound scopei cs) <- getMeta i
|
||||
e2 <- mkLam i scopei env1 vs1 v2
|
||||
sequence_ [c e2 | c <- cs]
|
||||
setMeta i (MBound e2)
|
||||
eqValue' k v1 (VMeta i env2 vs2) = do (MUnbound scopei cs) <- getMeta i
|
||||
e1 <- mkLam i scopei env2 vs2 v1
|
||||
sequence_ [c e1 | c <- cs]
|
||||
setMeta i (MBound e1)
|
||||
eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2
|
||||
eqValue' k (VLit l1) (VLit l2 ) | l1 == l2 = return ()
|
||||
eqValue' k (VGen i vs1) (VGen j vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2
|
||||
eqValue' k (VClosure env1 (EAbs x1 e1)) (VClosure env2 (EAbs x2 e2)) = let v = VGen k []
|
||||
in eqExpr (k+1) (v:env1) e1 (v:env2) e2
|
||||
eqValue' k v1 v2 = raiseTypeMatchError
|
||||
|
||||
mkLam i scope env vs0 v = do
|
||||
let k = scopeSize scope
|
||||
vs = reverse (take k env) ++ vs0
|
||||
xs = nub [i | VGen i [] <- vs]
|
||||
if length vs == length xs
|
||||
then return ()
|
||||
else raiseTypeMatchError
|
||||
v <- occurCheck i k xs v
|
||||
funs <- getFuns
|
||||
return (addLam vs0 (value2expr funs (length xs) v))
|
||||
where
|
||||
addLam [] e = e
|
||||
addLam (v:vs) e = EAbs var (addLam vs e)
|
||||
|
||||
var = mkCId "v"
|
||||
|
||||
occurCheck i0 k xs (VApp f vs) = do vs <- mapM (occurCheck i0 k xs) vs
|
||||
return (VApp f vs)
|
||||
occurCheck i0 k xs (VLit l) = return (VLit l)
|
||||
occurCheck i0 k xs (VMeta i env vs) = do if i == i0
|
||||
then raiseTypeMatchError
|
||||
else return ()
|
||||
mv <- getMeta i
|
||||
funs <- getFuns
|
||||
case mv of
|
||||
MBound e -> occurCheck i0 k xs (apply funs env e vs)
|
||||
MGuarded e _ _ -> occurCheck i0 k xs (apply funs env e vs)
|
||||
MUnbound scopei _ | scopeSize scopei > k -> raiseTypeMatchError
|
||||
| otherwise -> do vs <- mapM (occurCheck i0 k xs) vs
|
||||
return (VMeta i env vs)
|
||||
occurCheck i0 k xs (VSusp i env vs cnt) = do addConstraint i0 i env vs (\v -> occurCheck i0 k xs (cnt v) >> return ())
|
||||
return (VSusp i env vs cnt)
|
||||
occurCheck i0 k xs (VGen i vs) = case List.findIndex (==i) xs of
|
||||
Just i -> do vs <- mapM (occurCheck i0 k xs) vs
|
||||
return (VGen i vs)
|
||||
Nothing -> raiseTypeMatchError
|
||||
occurCheck i0 k xs (VClosure env e) = do env <- mapM (occurCheck i0 k xs) env
|
||||
return (VClosure env e)
|
||||
|
||||
|
||||
-- this is not given in Expr
|
||||
prValue = showExpr . value2expr
|
||||
-----------------------------------------------------------
|
||||
-- check for meta variables that still have to be resolved
|
||||
-----------------------------------------------------------
|
||||
|
||||
value2expr v = case v of
|
||||
VApp f vs -> foldl EApp (EVar f) (map value2expr vs)
|
||||
VMeta i vs -> foldl EApp (EMeta i) (map value2expr vs)
|
||||
VClosure g e -> e ----
|
||||
VLit l -> ELit l
|
||||
checkResolvedMetaStore :: Scope -> Expr -> TcM ()
|
||||
checkResolvedMetaStore scope e = TcM (\abstr metaid ms ->
|
||||
let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)]
|
||||
in if List.null xs
|
||||
then Ok metaid ms ()
|
||||
else Fail (UnresolvedMetaVars scope e xs))
|
||||
where
|
||||
isResolved (MUnbound _ []) = True
|
||||
isResolved (MGuarded _ _ _) = True
|
||||
isResolved (MBound _) = True
|
||||
isResolved _ = False
|
||||
|
||||
prConstraints :: [(Value,Value)] -> String
|
||||
prConstraints cs = unwords
|
||||
["(" ++ prValue v ++ " <> " ++ prValue w ++ ")" | (v,w) <- cs]
|
||||
-----------------------------------------------------
|
||||
-- evalType
|
||||
-----------------------------------------------------
|
||||
|
||||
-- work more on this: unification, compute,...
|
||||
|
||||
{-
|
||||
splitConstraints :: PGF -> [(Value,Value)] -> ([(Int,Expr)],[(Value,Value)])
|
||||
splitConstraints pgf = mkSplit . partition isSubst . regroup . map reorder . map reduce where
|
||||
reorder (v,w) = case w of
|
||||
VMeta _ _ -> (w,v)
|
||||
_ -> (v,w)
|
||||
|
||||
reduce (v,w) = (whnf v,whnf w)
|
||||
|
||||
whnf (VClosure env e) = eval (getFunEnv (abstract pgf)) env e -- should be removed when the typechecker is improved
|
||||
whnf v = v
|
||||
|
||||
regroup = groupBy (\x y -> fst x == fst y) . sort
|
||||
|
||||
isSubst cs@((v,u):_) = case v of
|
||||
VMeta _ _ -> all ((==u) . snd) cs
|
||||
_ -> False
|
||||
mkSplit (ms,cs) = ([(i,value2expr v) | (VMeta i _,v):_ <- ms], concat cs)
|
||||
-}
|
||||
|
||||
splitConstraints :: PGF -> [(Value,Value)] -> ([(Int,Expr)],[(Value,Value)])
|
||||
splitConstraints pgf = mkSplit . unifyAll [] . map reduce where
|
||||
reduce (v,w) = (whnf v,whnf w)
|
||||
|
||||
whnf (VClosure env e) = eval (getFunEnv (abstract pgf)) env e -- should be removed when the typechecker is improved
|
||||
whnf v = v
|
||||
mkSplit (ms,cs) = ([(i,value2expr v) | (i,v) <- ms], cs)
|
||||
|
||||
unifyAll g [] = (g, [])
|
||||
unifyAll g ((a@(s, t)) : l) =
|
||||
let (g1, c) = unifyAll g l
|
||||
in case unify s t g1 of
|
||||
Just g2 -> (g2, c)
|
||||
_ -> (g1, a : c)
|
||||
|
||||
unify e1 e2 g = case (e1, e2) of
|
||||
(VMeta s _, t) -> do
|
||||
let tg = substMetas g t
|
||||
let sg = maybe e1 id (lookup s g)
|
||||
if null (eqValue (funs (abstract pgf)) 0 sg e1) then extend s tg g else unify sg tg g
|
||||
(t, VMeta _ _) -> unify e2 e1 g
|
||||
(VApp c as, VApp d bs) | c == d ->
|
||||
foldM (\ h (a,b) -> unify a b h) g (zip as bs)
|
||||
_ -> Nothing
|
||||
|
||||
extend s t g = case t of
|
||||
VMeta u _ | u == s -> return g
|
||||
_ | occCheck s t -> Nothing
|
||||
_ -> return ((s, t) : g)
|
||||
|
||||
substMetas subst trm = case trm of
|
||||
VMeta s _ -> maybe trm id (lookup s subst)
|
||||
VApp c vs -> VApp c (map (substMetas subst) vs)
|
||||
_ -> trm
|
||||
|
||||
occCheck s u = case u of
|
||||
VMeta t _ -> s == t
|
||||
VApp c as -> any (occCheck s) as
|
||||
_ -> False
|
||||
evalType :: Int -> TType -> TcM Type
|
||||
evalType k (TTyp delta ty) = do funs <- getFuns
|
||||
refineType (evalTy funs k delta ty)
|
||||
where
|
||||
evalTy sig k delta (DTyp hyps cat es) =
|
||||
let ((k1,delta1),hyps1) = mapAccumL (evalHypo sig) (k,delta) hyps
|
||||
in DTyp hyps1 cat (List.map (normalForm sig k1 delta1) es)
|
||||
|
||||
evalHypo sig (k,delta) (Hyp ty) = ((k, delta),Hyp (evalTy sig k delta ty))
|
||||
evalHypo sig (k,delta) (HypV x ty) = ((k+1,(VGen k []):delta),HypV x (evalTy sig k delta ty))
|
||||
evalHypo sig (k,delta) (HypI x ty) = ((k+1,(VGen k []):delta),HypI x (evalTy sig k delta ty))
|
||||
|
||||
|
||||
metaSubst :: [(Int,Expr)] -> Expr -> Expr
|
||||
metaSubst vs exp = case exp of
|
||||
EApp u v -> EApp (subst u) (subst v)
|
||||
EMeta i -> maybe exp id $ lookup i vs
|
||||
EPi x a b -> EPi x (subst a) (subst b)
|
||||
EAbs x b -> EAbs x (subst b)
|
||||
_ -> exp
|
||||
where
|
||||
subst = metaSubst vs
|
||||
-----------------------------------------------------
|
||||
-- refinement
|
||||
-----------------------------------------------------
|
||||
|
||||
--- use composOp and state monad...
|
||||
newMetas :: Expr -> Expr
|
||||
newMetas = fst . metas 0 where
|
||||
metas i exp = case exp of
|
||||
EAbs x e -> let (f,j) = metas i e in (EAbs x f, j)
|
||||
EApp f a -> let (g,j) = metas i f ; (b,k) = metas j a in (EApp g b,k)
|
||||
EMeta _ -> (EMeta i, i+1)
|
||||
_ -> (exp,i)
|
||||
refineExpr :: Expr -> TcM Expr
|
||||
refineExpr e = TcM (\abstr metaid ms -> Ok metaid ms (refineExpr_ ms e))
|
||||
|
||||
refineExpr_ ms e = refine e
|
||||
where
|
||||
refine (EAbs x e) = EAbs x (refine e)
|
||||
refine (EApp e1 e2) = EApp (refine e1) (refine e2)
|
||||
refine (ELit l) = ELit l
|
||||
refine (EMeta i) = case IntMap.lookup i ms of
|
||||
Just (MBound e ) -> refine e
|
||||
Just (MGuarded e _ _) -> refine e
|
||||
_ -> EMeta i
|
||||
refine (EFun f) = EFun f
|
||||
refine (EVar i) = EVar i
|
||||
refine (ETyped e ty) = ETyped (refine e) (refineType_ ms ty)
|
||||
|
||||
refineType :: Type -> TcM Type
|
||||
refineType ty = TcM (\abstr metaid ms -> Ok metaid ms (refineType_ ms ty))
|
||||
|
||||
refineType_ ms (DTyp hyps cat es) = DTyp (List.map (refineHypo_ ms) hyps) cat (List.map (refineExpr_ ms) es)
|
||||
|
||||
refineHypo_ ms (Hyp ty) = Hyp (refineType_ ms ty)
|
||||
refineHypo_ ms (HypV x ty) = HypV x (refineType_ ms ty)
|
||||
refineHypo_ ms (HypI x ty) = HypI x (refineType_ ms ty)
|
||||
|
||||
value2expr sig i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr sig i) vs)
|
||||
value2expr sig i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr sig i) vs)
|
||||
value2expr sig i (VMeta j env vs) = foldl EApp (EMeta j) (List.map (value2expr sig i) vs)
|
||||
value2expr sig i (VSusp j env vs k) = value2expr sig i (k (VGen j vs))
|
||||
value2expr sig i (VLit l) = ELit l
|
||||
value2expr sig i (VClosure env (EAbs x e)) = EAbs x (value2expr sig (i+1) (eval sig ((VGen i []):env) e))
|
||||
|
||||
Reference in New Issue
Block a user