mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-21 09:02:50 -06:00
incomplete support for record types in the abstract syntax
This commit is contained in:
@@ -23,9 +23,12 @@ module GF.Compile.TC (AExp(..),
|
|||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
import GF.Grammar.Predef
|
import GF.Grammar.Predef
|
||||||
import GF.Grammar.Abstract
|
import GF.Grammar.Abstract
|
||||||
|
import GF.Grammar.Printer
|
||||||
|
|
||||||
import Control.Monad
|
import Control.Monad
|
||||||
import Data.List (sortBy)
|
import Data.List (sortBy)
|
||||||
|
import Data.Maybe
|
||||||
|
import Text.PrettyPrint
|
||||||
|
|
||||||
data AExp =
|
data AExp =
|
||||||
AVr Ident Val
|
AVr Ident Val
|
||||||
@@ -39,9 +42,15 @@ data AExp =
|
|||||||
| AAbs Ident Val AExp
|
| AAbs Ident Val AExp
|
||||||
| AProd Ident AExp AExp
|
| AProd Ident AExp AExp
|
||||||
| AEqs [([Exp],AExp)] --- not used
|
| AEqs [([Exp],AExp)] --- not used
|
||||||
|
| ARecType [ALabelling]
|
||||||
|
| AR [AAssign]
|
||||||
|
| AP AExp Label Val
|
||||||
| AData Val
|
| AData Val
|
||||||
deriving (Eq,Show)
|
deriving (Eq,Show)
|
||||||
|
|
||||||
|
type ALabelling = (Label, AExp)
|
||||||
|
type AAssign = (Label, (Val, AExp))
|
||||||
|
|
||||||
type Theory = QIdent -> Err Val
|
type Theory = QIdent -> Err Val
|
||||||
|
|
||||||
lookupConst :: Theory -> QIdent -> Err Val
|
lookupConst :: Theory -> QIdent -> Err Val
|
||||||
@@ -79,6 +88,8 @@ eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
|
|||||||
QC m c -> return $ VCn (m,c) ---- == Q ?
|
QC m c -> return $ VCn (m,c) ---- == Q ?
|
||||||
Sort c -> return $ VType --- the only sort is Type
|
Sort c -> return $ VType --- the only sort is Type
|
||||||
App f a -> join $ liftM2 app (eval env f) (eval env a)
|
App f a -> join $ liftM2 app (eval env f) (eval env a)
|
||||||
|
RecType xs -> do xs <- mapM (\(l,e) -> eval env e >>= \e -> return (l,e)) xs
|
||||||
|
return (VRecType xs)
|
||||||
_ -> return $ VClos env e
|
_ -> return $ VClos env e
|
||||||
|
|
||||||
eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
|
eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
|
||||||
@@ -93,7 +104,7 @@ eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
|
|||||||
eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
|
eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
|
||||||
(VClos env1 (Prod x1 a1 e1), VClos env2 (Prod x2 a2 e2)) ->
|
(VClos env1 (Prod x1 a1 e1), VClos env2 (Prod x2 a2 e2)) ->
|
||||||
liftM2 (++)
|
liftM2 (++)
|
||||||
(eqVal k (VClos env1 a1) (VClos env2 a2))
|
(eqVal k (VClos env1 a1) (VClos env2 a2))
|
||||||
(eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
|
(eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
|
||||||
(VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
|
(VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
|
||||||
(VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j]
|
(VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j]
|
||||||
@@ -132,6 +143,19 @@ checkExp th tenv@(k,rho,gamma) e ty = do
|
|||||||
(b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
|
(b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
|
||||||
return (AProd x a' b', csa ++ csb)
|
return (AProd x a' b', csa ++ csb)
|
||||||
|
|
||||||
|
R xs ->
|
||||||
|
case typ of
|
||||||
|
VRecType ys -> do case [l | (l,_) <- ys, isNothing (lookup l xs)] of
|
||||||
|
[] -> return ()
|
||||||
|
ls -> fail (render (text "no value given for label:" <+> fsep (punctuate comma (map ppLabel ls))))
|
||||||
|
r <- mapM (checkAssign th tenv ys) xs
|
||||||
|
let (xs,css) = unzip r
|
||||||
|
return (AR xs, concat css)
|
||||||
|
_ -> prtBad ("record type expected for" +++ prt e +++ "instead of") typ
|
||||||
|
|
||||||
|
P r l -> do (r',cs) <- checkExp th tenv r (VRecType [(l,typ)])
|
||||||
|
return (AP r' l typ,cs)
|
||||||
|
|
||||||
_ -> checkInferExp th tenv e typ
|
_ -> checkInferExp th tenv e typ
|
||||||
|
|
||||||
checkInferExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
|
checkInferExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
|
||||||
@@ -151,6 +175,9 @@ inferExp th tenv@(k,rho,gamma) e = case e of
|
|||||||
EFloat i -> return (AFloat i, valAbsFloat, [])
|
EFloat i -> return (AFloat i, valAbsFloat, [])
|
||||||
K i -> return (AStr i, valAbsString, [])
|
K i -> return (AStr i, valAbsString, [])
|
||||||
Sort _ -> return (AType, vType, [])
|
Sort _ -> return (AType, vType, [])
|
||||||
|
RecType xs -> do r <- mapM (checkLabelling th tenv) xs
|
||||||
|
let (xs,css) = unzip r
|
||||||
|
return (ARecType xs, vType, concat css)
|
||||||
App f t -> do
|
App f t -> do
|
||||||
(f',w,csf) <- inferExp th tenv f
|
(f',w,csf) <- inferExp th tenv f
|
||||||
typ <- whnf w
|
typ <- whnf w
|
||||||
@@ -162,6 +189,27 @@ inferExp th tenv@(k,rho,gamma) e = case e of
|
|||||||
_ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
|
_ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
|
||||||
_ -> prtBad "cannot infer type of expression" e
|
_ -> prtBad "cannot infer type of expression" e
|
||||||
|
|
||||||
|
checkLabelling :: Theory -> TCEnv -> Labelling -> Err (ALabelling, [(Val,Val)])
|
||||||
|
checkLabelling th tenv (lbl,typ) = do
|
||||||
|
(atyp,cs) <- checkType th tenv typ
|
||||||
|
return ((lbl,atyp),cs)
|
||||||
|
|
||||||
|
checkAssign :: Theory -> TCEnv -> [(Label,Val)] -> Assign -> Err (AAssign, [(Val,Val)])
|
||||||
|
checkAssign th tenv@(k,rho,gamma) typs (lbl,(Just typ,exp)) = do
|
||||||
|
(atyp,cs1) <- checkType th tenv typ
|
||||||
|
val <- eval rho typ
|
||||||
|
cs2 <- case lookup lbl typs of
|
||||||
|
Nothing -> return []
|
||||||
|
Just val0 -> eqVal k val val0
|
||||||
|
(aexp,cs3) <- checkExp th tenv exp val
|
||||||
|
return ((lbl,(val,aexp)),cs1++cs2++cs3)
|
||||||
|
checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do
|
||||||
|
case lookup lbl typs of
|
||||||
|
Nothing -> do (aexp,val,cs) <- inferExp th tenv exp
|
||||||
|
return ((lbl,(val,aexp)),cs)
|
||||||
|
Just val -> do (aexp,cs) <- checkExp th tenv exp val
|
||||||
|
return ((lbl,(val,aexp)),cs)
|
||||||
|
|
||||||
checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
|
checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
|
||||||
checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
|
checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
|
||||||
chB tenv' ps' ty
|
chB tenv' ps' ty
|
||||||
|
|||||||
@@ -186,6 +186,8 @@ val2expP safe v = case v of
|
|||||||
VGen i x -> if safe
|
VGen i x -> if safe
|
||||||
then prtBad "unsafe val2exp" v
|
then prtBad "unsafe val2exp" v
|
||||||
else return $ Vr $ x --- in editing, no alpha conversions presentv
|
else return $ Vr $ x --- in editing, no alpha conversions presentv
|
||||||
|
VRecType xs->do xs <- mapM (\(l,v) -> val2expP safe v >>= \e -> return (l,e)) xs
|
||||||
|
return (RecType xs)
|
||||||
VType -> return typeType
|
VType -> return typeType
|
||||||
where
|
where
|
||||||
substVal g e = mapPairsM (val2expP safe) g >>= return . (\s -> substTerm [] s e)
|
substVal g e = mapPairsM (val2expP safe) g >>= return . (\s -> substTerm [] s e)
|
||||||
|
|||||||
@@ -189,6 +189,7 @@ instance Print Val where
|
|||||||
prt (VClos env e) = case e of
|
prt (VClos env e) = case e of
|
||||||
Meta _ -> prt_ e ++ prEnv env
|
Meta _ -> prt_ e ++ prEnv env
|
||||||
_ -> prt_ e ---- ++ prEnv env ---- for debugging
|
_ -> prt_ e ---- ++ prEnv env ---- for debugging
|
||||||
|
prt (VRecType xs) = prCurly (concat (intersperse "," [prt l ++ "=" ++ prt v | (l,v) <- xs]))
|
||||||
prt VType = "Type"
|
prt VType = "Type"
|
||||||
|
|
||||||
prv1 v = case v of
|
prv1 v = case v of
|
||||||
|
|||||||
@@ -65,6 +65,7 @@ unify e1 e2 g =
|
|||||||
(App c a, App d b) -> case unify c d g of
|
(App c a, App d b) -> case unify c d g of
|
||||||
Ok g1 -> unify a b g1
|
Ok g1 -> unify a b g1
|
||||||
_ -> prtBad "fail unify" e1
|
_ -> prtBad "fail unify" e1
|
||||||
|
(RecType xs,RecType ys) | xs == ys -> return g
|
||||||
_ -> prtBad "fail unify" e1
|
_ -> prtBad "fail unify" e1
|
||||||
|
|
||||||
extend :: Unifier -> MetaSymb -> Term -> Err Unifier
|
extend :: Unifier -> MetaSymb -> Term -> Err Unifier
|
||||||
|
|||||||
@@ -35,7 +35,7 @@ import GF.Grammar.Predef
|
|||||||
|
|
||||||
type Exp = Term
|
type Exp = Term
|
||||||
|
|
||||||
data Val = VGen Int Ident | VApp Val Val | VCn QIdent | VType | VClos Env Exp
|
data Val = VGen Int Ident | VApp Val Val | VCn QIdent | VRecType [(Label,Val)] | VType | VClos Env Exp
|
||||||
deriving (Eq,Show)
|
deriving (Eq,Show)
|
||||||
|
|
||||||
type Env = [(Ident,Val)]
|
type Env = [(Ident,Val)]
|
||||||
|
|||||||
Reference in New Issue
Block a user