mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
change the data types and the syntax in PGF to match the new syntax for implict arguments
This commit is contained in:
krasimir
@@ -74,7 +74,7 @@ appCommand xs c@(Command i os arg) = case arg of
|
||||
_ -> c
|
||||
where
|
||||
app e = case e of
|
||||
EAbs x e -> EAbs x (app e)
|
||||
EAbs b x e -> EAbs b x (app e)
|
||||
EApp e1 e2 -> EApp (app e1) (app e2)
|
||||
ELit l -> ELit l
|
||||
EMeta i -> xs !! i
|
||||
|
||||
@@ -27,6 +27,6 @@ allTreeOps pgf = [
|
||||
smallest :: [Expr] -> [Expr]
|
||||
smallest = sortBy (\t u -> compare (size t) (size u)) where
|
||||
size t = case t of
|
||||
EAbs _ e -> size e + 1
|
||||
EAbs _ _ e -> size e + 1
|
||||
EApp e1 e2 -> size e1 + size e2 + 1
|
||||
_ -> 1
|
||||
|
||||
@@ -19,7 +19,7 @@ import GF.Text.UTF8
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import Data.Char (isAlphaNum, isAsciiLower, isAsciiUpper, ord)
|
||||
import Data.List (isPrefixOf)
|
||||
import Data.List (isPrefixOf,mapAccumL)
|
||||
|
||||
grammar2prolog, grammar2prolog_abs :: PGF -> String
|
||||
-- Most prologs have problems with UTF8 encodings, so we skip that:
|
||||
@@ -67,7 +67,7 @@ plAbstract (name, Abstr aflags funs cats _catfuns) =
|
||||
|
||||
plCat :: (CId, [Hypo]) -> String
|
||||
plCat (cat, hypos) = plFact "cat" (plTypeWithHypos typ)
|
||||
where ((_,subst), hypos') = alphaConvert emptyEnv hypos
|
||||
where ((_,subst), hypos') = mapAccumL alphaConvertHypo emptyEnv hypos
|
||||
args = reverse [EFun x | (_,x) <- subst]
|
||||
typ = DTyp hypos' cat args
|
||||
|
||||
@@ -76,7 +76,7 @@ plFun (fun, (typ,_,_)) = plFact "fun" (plp fun : plTypeWithHypos typ')
|
||||
where typ' = snd $ alphaConvert emptyEnv typ
|
||||
|
||||
plTypeWithHypos :: Type -> [String]
|
||||
plTypeWithHypos (DTyp hypos cat args) = [plTerm (plp cat) (map plp args), plp hypos]
|
||||
plTypeWithHypos (DTyp hypos cat args) = [plTerm (plp cat) (map plp args), plList (map (\(_,x,ty) -> plOper ":" (plp x) (plp ty)) hypos)]
|
||||
|
||||
plFundef :: (CId, (Type,Int,[Equation])) -> [String]
|
||||
plFundef (fun, (_,_,[])) = []
|
||||
@@ -110,17 +110,12 @@ plConcrete (cncname, Concr cflags lins opers lincats lindefs
|
||||
|
||||
instance PLPrint Type where
|
||||
plp (DTyp hypos cat args) | null hypos = result
|
||||
| otherwise = plOper " -> " (plp hypos) result
|
||||
| otherwise = plOper " -> " (plList (map (\(_,x,ty) -> plOper ":" (plp x) (plp ty)) hypos)) result
|
||||
where result = plTerm (plp cat) (map plp args)
|
||||
|
||||
instance PLPrint Hypo where
|
||||
plp (Hyp typ) = plOper ":" (plp wildCId) (plp typ)
|
||||
plp (HypI var typ) = plOper ":" (plp var) (plp typ)
|
||||
plp (HypV var typ) = plOper ":" (plp var) (plp typ)
|
||||
|
||||
instance PLPrint Expr where
|
||||
plp (EFun x) = plp x
|
||||
plp (EAbs x e) = plOper "^" (plp x) (plp e)
|
||||
plp (EAbs _ x e)= plOper "^" (plp x) (plp e)
|
||||
plp (EApp e e') = plOper " * " (plp e) (plp e')
|
||||
plp (ELit lit) = plp lit
|
||||
plp (EMeta n) = "Meta_" ++ show n
|
||||
@@ -259,21 +254,15 @@ instance AlphaConvert a => AlphaConvert [a] where
|
||||
instance AlphaConvert Type where
|
||||
alphaConvert env@(_,subst) (DTyp hypos cat args)
|
||||
= ((ctr,subst), DTyp hypos' cat args')
|
||||
where (env', hypos') = alphaConvert env hypos
|
||||
where (env', hypos') = mapAccumL alphaConvertHypo env hypos
|
||||
((ctr,_), args') = alphaConvert env' args
|
||||
|
||||
instance AlphaConvert Hypo where
|
||||
alphaConvert env (Hyp typ) = ((ctr+1,subst), Hyp typ')
|
||||
where ((ctr,subst), typ') = alphaConvert env typ
|
||||
alphaConvert env (HypI x typ) = ((ctr+1,(x,x'):subst), HypI x' typ')
|
||||
where ((ctr,subst), typ') = alphaConvert env typ
|
||||
x' = createLogicalVariable ctr
|
||||
alphaConvert env (HypV x typ) = ((ctr+1,(x,x'):subst), HypV x' typ')
|
||||
where ((ctr,subst), typ') = alphaConvert env typ
|
||||
x' = createLogicalVariable ctr
|
||||
alphaConvertHypo env (b,x,typ) = ((ctr+1,(x,x'):subst), (b,x',typ'))
|
||||
where ((ctr,subst), typ') = alphaConvert env typ
|
||||
x' = createLogicalVariable ctr
|
||||
|
||||
instance AlphaConvert Expr where
|
||||
alphaConvert (ctr,subst) (EAbs x e) = ((ctr',subst), EAbs x' e')
|
||||
alphaConvert (ctr,subst) (EAbs b x e) = ((ctr',subst), EAbs b x' e')
|
||||
where ((ctr',_), e') = alphaConvert (ctr+1,(x,x'):subst) e
|
||||
x' = createLogicalVariable ctr
|
||||
alphaConvert env (EApp e1 e2) = (env'', EApp e1' e2')
|
||||
|
||||
@@ -129,7 +129,7 @@ mkExp :: [Ident] -> A.Term -> C.Expr
|
||||
mkExp scope t = case GM.termForm t of
|
||||
Ok (xs,c,args) -> mkAbs xs (mkApp (reverse xs++scope) c (map (mkExp scope) args))
|
||||
where
|
||||
mkAbs xs t = foldr (C.EAbs . i2i) t xs
|
||||
mkAbs xs t = foldr (C.EAbs C.Explicit . i2i) t xs
|
||||
mkApp scope c args = case c of
|
||||
Q _ c -> foldl C.EApp (C.EFun (i2i c)) args
|
||||
QC _ c -> foldl C.EApp (C.EFun (i2i c)) args
|
||||
@@ -156,8 +156,8 @@ mkPatt scope p =
|
||||
mkContext :: [Ident] -> A.Context -> ([Ident],[C.Hypo])
|
||||
mkContext scope hyps = mapAccumL (\scope (x,ty) -> let ty' = mkType scope ty
|
||||
in if x == identW
|
||||
then ( scope,C.Hyp ty')
|
||||
else (x:scope,C.HypV (i2i x) ty')) scope hyps
|
||||
then ( scope,(C.Explicit,i2i x,ty'))
|
||||
else (x:scope,(C.Explicit,i2i x,ty'))) scope hyps
|
||||
|
||||
mkTerm :: Term -> C.Term
|
||||
mkTerm tr = case tr of
|
||||
|
||||
@@ -102,7 +102,7 @@ instance Binary Term where
|
||||
_ -> decodingError
|
||||
|
||||
instance Binary Expr where
|
||||
put (EAbs x exp) = putWord8 0 >> put (x,exp)
|
||||
put (EAbs b x exp) = putWord8 0 >> put (b,x,exp)
|
||||
put (EApp e1 e2) = putWord8 1 >> put (e1,e2)
|
||||
put (ELit (LStr s)) = putWord8 2 >> put s
|
||||
put (ELit (LFlt d)) = putWord8 3 >> put d
|
||||
@@ -113,7 +113,7 @@ instance Binary Expr where
|
||||
put (ETyped e ty) = putWord8 8 >> put (e,ty)
|
||||
get = do tag <- getWord8
|
||||
case tag of
|
||||
0 -> liftM2 EAbs get get
|
||||
0 -> liftM3 EAbs get get get
|
||||
1 -> liftM2 EApp get get
|
||||
2 -> liftM (ELit . LStr) get
|
||||
3 -> liftM (ELit . LFlt) get
|
||||
@@ -149,15 +149,14 @@ instance Binary Type where
|
||||
put (DTyp hypos cat exps) = put (hypos,cat,exps)
|
||||
get = liftM3 DTyp get get get
|
||||
|
||||
instance Binary Hypo where
|
||||
put (Hyp t) = putWord8 0 >> put t
|
||||
put (HypV v t) = putWord8 1 >> put (v,t)
|
||||
put (HypI v t) = putWord8 2 >> put (v,t)
|
||||
instance Binary BindType where
|
||||
put Explicit = putWord8 0
|
||||
put Implicit = putWord8 1
|
||||
get = do tag <- getWord8
|
||||
case tag of
|
||||
0 -> liftM Hyp get
|
||||
1 -> liftM2 HypV get get
|
||||
2 -> liftM2 HypI get get
|
||||
0 -> return Explicit
|
||||
1 -> return Implicit
|
||||
_ -> decodingError
|
||||
|
||||
instance Binary FFun where
|
||||
put (FFun fun prof lins) = put (fun,prof,lins)
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
module PGF.Expr(Tree, Expr(..), Literal(..), Patt(..), Equation(..),
|
||||
readExpr, showExpr, pExpr, ppExpr, ppPatt,
|
||||
module PGF.Expr(Tree, BindType(..), Expr(..), Literal(..), Patt(..), Equation(..),
|
||||
readExpr, showExpr, pExpr, pBinds, ppExpr, ppPatt,
|
||||
|
||||
mkApp, unApp,
|
||||
mkStr, unStr,
|
||||
@@ -36,6 +36,11 @@ data Literal =
|
||||
|
||||
type MetaId = Int
|
||||
|
||||
data BindType =
|
||||
Explicit
|
||||
| Implicit
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
-- | Tree is the abstract syntax representation of a given sentence
|
||||
-- in some concrete syntax. Technically 'Tree' is a type synonym
|
||||
-- of 'Expr'.
|
||||
@@ -45,7 +50,7 @@ type Tree = Expr
|
||||
-- both parameter of a dependent type or an abstract syntax tree for
|
||||
-- for some sentence.
|
||||
data Expr =
|
||||
EAbs CId Expr -- ^ lambda abstraction
|
||||
EAbs BindType CId Expr -- ^ lambda abstraction
|
||||
| EApp Expr Expr -- ^ application
|
||||
| ELit Literal -- ^ literal
|
||||
| EMeta {-# UNPACK #-} !MetaId -- ^ meta variable
|
||||
@@ -131,10 +136,24 @@ 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 ','))
|
||||
pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") pBinds
|
||||
e <- pExpr
|
||||
return (foldr EAbs e xs)
|
||||
|
||||
return (foldr (\(b,x) e -> EAbs b x e) e xs)
|
||||
|
||||
pBinds :: RP.ReadP [(BindType,CId)]
|
||||
pBinds = do xss <- RP.sepBy1 (RP.skipSpaces >> pBind) (RP.skipSpaces >> RP.char ',')
|
||||
return (concat xss)
|
||||
where
|
||||
pCIdOrWild = pCId `mplus` (RP.char '_' >> return wildCId)
|
||||
|
||||
pBind =
|
||||
do x <- pCIdOrWild
|
||||
return [(Explicit,x)]
|
||||
`mplus`
|
||||
RP.between (RP.char '{')
|
||||
(RP.skipSpaces >> RP.char '}')
|
||||
(RP.sepBy1 (RP.skipSpaces >> pCIdOrWild >>= \id -> return (Implicit,id)) (RP.skipSpaces >> RP.char ','))
|
||||
|
||||
pFactor = fmap EFun pCId
|
||||
RP.<++ fmap ELit pLit
|
||||
RP.<++ fmap EMeta pMeta
|
||||
@@ -170,14 +189,14 @@ pStr = RP.char '"' >> (RP.manyTill (pEsc RP.<++ RP.get) (RP.char '"'))
|
||||
-----------------------------------------------------
|
||||
|
||||
ppExpr :: Int -> [CId] -> Expr -> PP.Doc
|
||||
ppExpr d scope (EAbs x e) = let (xs,e1) = getVars [x] e
|
||||
ppExpr d scope (EAbs b x e) = let (bs,xs,e1) = getVars [] [] (EAbs b x e)
|
||||
in ppParens (d > 1) (PP.char '\\' PP.<>
|
||||
PP.hsep (PP.punctuate PP.comma (List.map ppCId (reverse xs))) PP.<+>
|
||||
PP.hsep (PP.punctuate PP.comma (reverse (List.zipWith ppBind bs 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)
|
||||
getVars bs xs (EAbs b x e) = getVars (b:bs) ((freshName x xs):xs) e
|
||||
getVars bs xs e = (bs,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
|
||||
@@ -192,6 +211,9 @@ ppPatt d scope (PLit l) = (scope,ppLit l)
|
||||
ppPatt d scope (PVar f) = (f:scope,ppCId f)
|
||||
ppPatt d scope PWild = (scope,PP.char '_')
|
||||
|
||||
ppBind Explicit x = ppCId x
|
||||
ppBind Implicit x = PP.braces (ppCId x)
|
||||
|
||||
ppLit (LStr s) = PP.text (show s)
|
||||
ppLit (LInt n) = PP.integer n
|
||||
ppLit (LFlt d) = PP.double d
|
||||
@@ -205,10 +227,12 @@ ppParens True = PP.parens
|
||||
ppParens False = id
|
||||
|
||||
freshName :: CId -> [CId] -> CId
|
||||
freshName x xs = loop 1 x
|
||||
freshName x xs0 = loop 1 x
|
||||
where
|
||||
xs = wildCId : xs0
|
||||
|
||||
loop i y
|
||||
| elem y xs = loop (i+1) (mkCId (show x++"'"++show i))
|
||||
| elem y xs = loop (i+1) (mkCId (show x++show i))
|
||||
| otherwise = y
|
||||
|
||||
|
||||
@@ -220,12 +244,12 @@ freshName x xs = loop 1 x
|
||||
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 (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 x (value2expr (i+1) (eval funs ((VGen i []):env) e))
|
||||
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 b x e)) = EAbs b x (value2expr (i+1) (eval funs ((VGen i []):env) e))
|
||||
|
||||
data Value
|
||||
= VApp CId [Value]
|
||||
@@ -248,7 +272,7 @@ eval funs env (EFun f) = case Map.lookup f funs of
|
||||
else VApp f []
|
||||
Nothing -> error ("unknown function "++showCId 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 (EAbs b x e) = VClosure env (EAbs b x e)
|
||||
eval funs env (EMeta i) = VMeta i env []
|
||||
eval funs env (ELit l) = VLit l
|
||||
eval funs env (ETyped e _) = eval funs env e
|
||||
@@ -263,18 +287,18 @@ apply funs env (EFun f) vs = case Map.lookup f funs of
|
||||
else VApp f vs
|
||||
Nothing -> error ("unknown function "++showCId 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 (v:env) e 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 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
|
||||
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 b x e)) (v:vs) = apply funs (v:env) e vs
|
||||
|
||||
-----------------------------------------------------
|
||||
-- Pattern matching
|
||||
|
||||
@@ -10,7 +10,16 @@ instance Eq Expr
|
||||
instance Ord Expr
|
||||
instance Show Expr
|
||||
|
||||
|
||||
data BindType = Explicit | Implicit
|
||||
|
||||
instance Eq BindType
|
||||
instance Ord BindType
|
||||
instance Show BindType
|
||||
|
||||
|
||||
pFactor :: RP.ReadP Expr
|
||||
pBinds :: RP.ReadP [(BindType,CId)]
|
||||
|
||||
ppExpr :: Int -> [CId] -> Expr -> PP.Doc
|
||||
|
||||
|
||||
@@ -59,8 +59,8 @@ linTree :: PGF -> CId -> Expr -> Term
|
||||
linTree pgf lang = lin . expr2tree
|
||||
where
|
||||
lin (Abs xs e ) = case lin e of
|
||||
R ts -> R $ ts ++ (Data.List.map (kks . showCId) xs)
|
||||
TM s -> R $ (TM s) : (Data.List.map (kks . showCId) xs)
|
||||
R ts -> R $ ts ++ (Data.List.map (kks . showCId . snd) xs)
|
||||
TM s -> R $ (TM s) : (Data.List.map (kks . showCId . snd) xs)
|
||||
lin (Fun fun es) = let argVariants = mapM (liftVariants . lin) es
|
||||
in variants [compute pgf lang args $ look fun | args <- argVariants]
|
||||
lin (Lit (LStr s)) = R [kks (show s)] -- quoted
|
||||
@@ -130,8 +130,8 @@ linTreeMark :: PGF -> CId -> Expr -> Term
|
||||
linTreeMark pgf lang = lin [] . expr2tree
|
||||
where
|
||||
lin p (Abs xs e ) = case lin p e of
|
||||
R ts -> R $ ts ++ (Data.List.map (kks . showCId) xs)
|
||||
TM s -> R $ (TM s) : (Data.List.map (kks . showCId) xs)
|
||||
R ts -> R $ ts ++ (Data.List.map (kks . showCId . snd) xs)
|
||||
TM s -> R $ (TM s) : (Data.List.map (kks . showCId . snd) xs)
|
||||
lin p (Fun fun es) = let argVariants =
|
||||
mapM (\ (i,e) -> liftVariants $ lin (sub p i) e) (zip [0..] es)
|
||||
in variants [mark p $ compute pgf lang args $ look fun | args <- argVariants]
|
||||
|
||||
@@ -100,17 +100,15 @@ restrictPGF cond pgf = pgf {
|
||||
abstr = abstract pgf
|
||||
|
||||
depth :: Expr -> Int
|
||||
depth (EAbs _ t) = depth t
|
||||
depth (EAbs _ _ t) = depth t
|
||||
depth (EApp e1 e2) = max (depth e1) (depth e2) + 1
|
||||
depth _ = 1
|
||||
|
||||
cftype :: [CId] -> CId -> Type
|
||||
cftype args val = DTyp [Hyp (cftype [] arg) | arg <- args] val []
|
||||
cftype args val = DTyp [(Explicit,wildCId,cftype [] arg) | arg <- args] val []
|
||||
|
||||
typeOfHypo :: Hypo -> Type
|
||||
typeOfHypo (Hyp ty) = ty
|
||||
typeOfHypo (HypV _ ty) = ty
|
||||
typeOfHypo (HypI _ ty) = ty
|
||||
typeOfHypo (_,_,ty) = ty
|
||||
|
||||
catSkeleton :: Type -> ([CId],CId)
|
||||
catSkeleton ty = case ty of
|
||||
|
||||
@@ -134,7 +134,7 @@ extractTrees (State pgf pinfo chart items) ty@(DTyp _ start _) =
|
||||
|
||||
check_ho_fun fun args
|
||||
| fun == _V = return (head args)
|
||||
| fun == _B = return (foldl1 Set.difference (map fst args), foldr (\x e -> EAbs (mkVar (snd x)) e) (snd (head args)) (tail args))
|
||||
| fun == _B = return (foldl1 Set.difference (map fst args), foldr (\x e -> EAbs Explicit (mkVar (snd x)) e) (snd (head args)) (tail args))
|
||||
| otherwise = return (Set.unions (map fst args),foldl (\e x -> EApp e (snd x)) (EFun fun) args)
|
||||
|
||||
mkVar (EFun v) = v
|
||||
|
||||
@@ -1,6 +1,5 @@
|
||||
module PGF.Tree
|
||||
( Tree(..),
|
||||
readTree, showTree, pTree, ppTree,
|
||||
tree2expr, expr2tree
|
||||
) where
|
||||
|
||||
@@ -18,54 +17,13 @@ import qualified Text.ParserCombinators.ReadP as RP
|
||||
-- allow unapplied lambda abstractions. The tree is used directly
|
||||
-- from the linearizer and is produced directly from the parser.
|
||||
data Tree =
|
||||
Abs [CId] Tree -- ^ lambda abstraction. The list of variables is non-empty
|
||||
Abs [(BindType,CId)] Tree -- ^ lambda abstraction. The list of variables is non-empty
|
||||
| Var CId -- ^ variable
|
||||
| Fun CId [Tree] -- ^ function application
|
||||
| Lit Literal -- ^ literal
|
||||
| Meta {-# UNPACK #-} !MetaId -- ^ meta variable
|
||||
deriving (Eq, Ord)
|
||||
|
||||
-- | parses 'String' as an expression
|
||||
readTree :: String -> Maybe Tree
|
||||
readTree s = case [x | (x,cs) <- RP.readP_to_S (pTree False) s, all isSpace cs] of
|
||||
[x] -> Just x
|
||||
_ -> Nothing
|
||||
|
||||
-- | renders expression as 'String'
|
||||
showTree :: Tree -> String
|
||||
showTree = PP.render . ppTree 0
|
||||
|
||||
instance Show Tree where
|
||||
showsPrec i x = showString (PP.render (ppTree i x))
|
||||
|
||||
instance Read Tree where
|
||||
readsPrec _ = RP.readP_to_S (pTree False)
|
||||
|
||||
pTrees :: RP.ReadP [Tree]
|
||||
pTrees = liftM2 (:) (pTree True) pTrees RP.<++ (RP.skipSpaces >> return [])
|
||||
|
||||
pTree :: Bool -> RP.ReadP Tree
|
||||
pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Lit pLit RP.<++ fmap Meta pMeta)
|
||||
where
|
||||
pParen = RP.between (RP.char '(') (RP.char ')') (pTree False)
|
||||
pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") (RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ','))
|
||||
t <- pTree False
|
||||
return (Abs xs t)
|
||||
pApp = do f <- pCId
|
||||
ts <- (if isNested then return [] else pTrees)
|
||||
return (Fun f ts)
|
||||
|
||||
ppTree d (Abs xs t) = ppParens (d > 0) (PP.char '\\' PP.<>
|
||||
PP.hsep (PP.punctuate PP.comma (List.map ppCId xs)) PP.<+>
|
||||
PP.text "->" PP.<+>
|
||||
ppTree 0 t)
|
||||
ppTree d (Fun f []) = ppCId f
|
||||
ppTree d (Fun f ts) = ppParens (d > 0) (ppCId 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) = ppCId id
|
||||
|
||||
|
||||
-----------------------------------------------------
|
||||
-- Conversion Expr <-> Tree
|
||||
-----------------------------------------------------
|
||||
@@ -78,7 +36,7 @@ tree2expr = tree2expr []
|
||||
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 (Abs xs t) = foldr (\(b,x) e -> EAbs b x e) (tree2expr (List.map snd (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"
|
||||
@@ -88,11 +46,11 @@ tree2expr = tree2expr []
|
||||
expr2tree :: Expr -> Tree
|
||||
expr2tree e = abs [] [] e
|
||||
where
|
||||
abs ys xs (EAbs x e) = abs ys (x:xs) e
|
||||
abs ys xs (EAbs b x e) = abs ys ((b,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)
|
||||
xs -> Abs (reverse xs) (app (map snd xs++ys) [] e)
|
||||
|
||||
app xs as (EApp e1 e2) = app xs ((abs xs [] e2) : as) e1
|
||||
app xs as (ELit l)
|
||||
@@ -101,7 +59,7 @@ expr2tree e = abs [] [] e
|
||||
app xs as (EMeta n)
|
||||
| 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 (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
|
||||
|
||||
@@ -1,4 +1,4 @@
|
||||
module PGF.Type ( Type(..), Hypo(..),
|
||||
module PGF.Type ( Type(..), Hypo,
|
||||
readType, showType,
|
||||
pType, ppType, ppHypo ) where
|
||||
|
||||
@@ -16,11 +16,7 @@ data Type =
|
||||
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,Show)
|
||||
type Hypo = (BindType,CId,Type)
|
||||
|
||||
-- | Reads a 'Type' from a 'String'.
|
||||
readType :: String -> Maybe Type
|
||||
@@ -45,23 +41,23 @@ pType = do
|
||||
where
|
||||
pHypo =
|
||||
do (cat,args) <- pAtom
|
||||
return [Hyp (DTyp [] cat args)]
|
||||
return [(Explicit,wildCId,DTyp [] cat args)]
|
||||
RP.<++
|
||||
(RP.between (RP.char '(') (RP.char ')') $ do
|
||||
hyp <- RP.option (\ty -> [Hyp ty]) $ do
|
||||
vs <- RP.sepBy (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',')
|
||||
xs <- RP.option [(Explicit,wildCId)] $ do
|
||||
xs <- pBinds
|
||||
RP.skipSpaces
|
||||
RP.char ':'
|
||||
return (\ty -> [HypV v ty | v <- vs])
|
||||
return xs
|
||||
ty <- pType
|
||||
return (hyp ty))
|
||||
return [(b,v,ty) | (b,v) <- xs])
|
||||
RP.<++
|
||||
(RP.between (RP.char '{') (RP.char '}') $ do
|
||||
vs <- RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',')
|
||||
RP.skipSpaces
|
||||
RP.char ':'
|
||||
ty <- pType
|
||||
return [HypI v ty | v <- vs])
|
||||
return [(Implicit,v,ty) | v <- vs])
|
||||
|
||||
pAtom = do
|
||||
cat <- pCId
|
||||
@@ -77,8 +73,11 @@ ppType d scope (DTyp hyps cat args)
|
||||
where
|
||||
ppRes scope cat es = ppCId cat PP.<+> PP.hsep (map (ppExpr 4 scope) es)
|
||||
|
||||
ppHypo scope (Hyp typ) = ( scope,ppType 1 scope typ)
|
||||
ppHypo scope (HypV x typ) = let y = freshName x scope
|
||||
in (y:scope,PP.parens (ppCId y PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
ppHypo scope (HypI x typ) = let y = freshName x scope
|
||||
in (y:scope,PP.braces (ppCId y PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
ppHypo scope (Explicit,x,typ) = if x == wildCId
|
||||
then (scope,ppType 1 scope typ)
|
||||
else let y = freshName x scope
|
||||
in (y:scope,PP.parens (ppCId y PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
ppHypo scope (Implicit,x,typ) = if x == wildCId
|
||||
then (scope,PP.parens (PP.braces (ppCId x) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
else let y = freshName x scope
|
||||
in (y:scope,PP.parens (PP.braces (ppCId y) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
|
||||
@@ -200,12 +200,11 @@ tcHypos scope (h:hs) = do
|
||||
return (scope,h:hs)
|
||||
|
||||
tcHypo :: Scope -> Hypo -> TcM (Scope,Hypo)
|
||||
tcHypo scope (Hyp ty) = do
|
||||
tcHypo scope (b,x,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)
|
||||
if x == wildCId
|
||||
then return (scope,(b,x,ty))
|
||||
else return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,(b,x,ty))
|
||||
|
||||
tcHypoExprs :: Scope -> Env -> [(Expr,Hypo)] -> TcM (Env,[Expr])
|
||||
tcHypoExprs scope delta [] = return (delta,[])
|
||||
@@ -215,13 +214,12 @@ tcHypoExprs scope delta ((e,h):xs) = do
|
||||
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)
|
||||
tcHypoExpr scope delta e (b,x,ty) = do
|
||||
e <- tcExpr scope e (TTyp delta ty)
|
||||
funs <- getFuns
|
||||
if x == wildCId
|
||||
then return ( delta,e)
|
||||
else return (eval funs (scopeEnv scope) e:delta,e)
|
||||
|
||||
|
||||
-----------------------------------------------------
|
||||
@@ -239,16 +237,16 @@ checkExpr pgf e ty =
|
||||
Fail err -> Left err
|
||||
|
||||
tcExpr :: Scope -> Expr -> TType -> TcM Expr
|
||||
tcExpr scope e0@(EAbs x e) tty =
|
||||
tcExpr scope e0@(EAbs b 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 (scopeVars scope) e0 ty)
|
||||
TTyp delta (DTyp ((_,y,ty):hs) c es) -> do e <- if y == wildCId
|
||||
then tcExpr (addScopedVar x (TTyp delta ty) scope)
|
||||
e (TTyp delta (DTyp hs c es))
|
||||
else tcExpr (addScopedVar x (TTyp delta ty) scope)
|
||||
e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
|
||||
return (EAbs b x e)
|
||||
_ -> do ty <- evalType (scopeSize scope) tty
|
||||
tcError (NotFunType (scopeVars scope) e0 ty)
|
||||
tcExpr scope (EMeta _) tty = do
|
||||
i <- newMeta scope
|
||||
return (EMeta i)
|
||||
@@ -322,14 +320,13 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
|
||||
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
|
||||
eqHyps k delta1 ((_,x,ty1) : h1s) delta2 ((_,y,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)
|
||||
if x == wildCId && y == wildCId
|
||||
then eqHyps k delta1 h1s delta2 h2s
|
||||
else if x /= wildCId && y /= wildCId
|
||||
then eqHyps (k+1) ((VGen k []):delta1) h1s ((VGen k []):delta2) h2s
|
||||
else raiseTypeMatchError
|
||||
eqHyps k delta1 h1s delta2 h2s = raiseTypeMatchError
|
||||
|
||||
eqExpr :: Int -> Env -> Expr -> Env -> Expr -> TcM ()
|
||||
@@ -353,23 +350,23 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
|
||||
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
|
||||
setMeta i (MBound e2)
|
||||
sequence_ [c e2 | c <- cs]
|
||||
eqValue' k v1 (VMeta i env2 vs2) = do (MUnbound scopei cs) <- getMeta i
|
||||
e1 <- mkLam i scopei env2 vs2 v1
|
||||
setMeta i (MBound e1)
|
||||
sequence_ [c e1 | c <- cs]
|
||||
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
|
||||
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
|
||||
setMeta i (MBound e2)
|
||||
sequence_ [c e2 | c <- cs]
|
||||
eqValue' k v1 (VMeta i env2 vs2) = do (MUnbound scopei cs) <- getMeta i
|
||||
e1 <- mkLam i scopei env2 vs2 v1
|
||||
setMeta i (MBound e1)
|
||||
sequence_ [c e1 | c <- cs]
|
||||
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
|
||||
@@ -383,7 +380,7 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
|
||||
return (addLam vs0 (value2expr funs (length xs) v))
|
||||
where
|
||||
addLam [] e = e
|
||||
addLam (v:vs) e = EAbs var (addLam vs e)
|
||||
addLam (v:vs) e = EAbs Explicit var (addLam vs e)
|
||||
|
||||
var = mkCId "v"
|
||||
|
||||
@@ -439,9 +436,10 @@ evalType k (TTyp delta ty) = do funs <- getFuns
|
||||
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))
|
||||
evalHypo sig (k,delta) (b,x,ty) =
|
||||
if x == wildCId
|
||||
then ((k, delta),(b,x,evalTy sig k delta ty))
|
||||
else ((k+1,(VGen k []):delta),(b,x,evalTy sig k delta ty))
|
||||
|
||||
|
||||
-----------------------------------------------------
|
||||
@@ -453,7 +451,7 @@ 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 (EAbs b x e) = EAbs b 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
|
||||
@@ -467,15 +465,11 @@ refineExpr_ ms e = refine e
|
||||
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)
|
||||
refineType_ ms (DTyp hyps cat es) = DTyp [(b,x,refineType_ ms ty) | (b,x,ty) <- 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))
|
||||
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 b x e)) = EAbs b x (value2expr sig (i+1) (eval sig ((VGen i []):env) e))
|
||||
|
||||
@@ -30,7 +30,7 @@ In the expression: mkMorph (\x -> succ zero)
|
||||
|
||||
Type: Vector (plus (succ (succ zero)) (succ zero))
|
||||
|
||||
|
||||
|
||||
|
||||
Expression: <\m, n -> vector (plus m n) : (m : Nat) -> (n : Nat) -> Vector (plus m n)>
|
||||
|
||||
|
||||
Reference in New Issue
Block a user