forked from GitHub/gf-core
021b5f06d3
The fact that identifiers are represented as ByteStrings is now an internal implentation detail in module GF.Infra.Ident. Conversion between ByteString and identifiers is only needed in the lexer and the Binary instances.
279 lines
7.7 KiB
Haskell
279 lines
7.7 KiB
Haskell
----------------------------------------------------------------------
|
|
-- |
|
|
-- Module : MMacros
|
|
-- Maintainer : AR
|
|
-- Stability : (stable)
|
|
-- Portability : (portable)
|
|
--
|
|
-- > CVS $Date: 2005/05/10 12:49:13 $
|
|
-- > CVS $Author: aarne $
|
|
-- > CVS $Revision: 1.9 $
|
|
--
|
|
-- some more abstractions on grammars, esp. for Edit
|
|
-----------------------------------------------------------------------------
|
|
|
|
module GF.Grammar.MMacros where
|
|
|
|
import GF.Data.Operations
|
|
--import GF.Data.Zipper
|
|
|
|
import GF.Grammar.Grammar
|
|
import GF.Grammar.Printer
|
|
import GF.Infra.Ident
|
|
--import GF.Compile.Refresh
|
|
import GF.Grammar.Values
|
|
----import GrammarST
|
|
import GF.Grammar.Macros
|
|
|
|
import Control.Monad
|
|
import Text.PrettyPrint
|
|
|
|
{-
|
|
nodeTree :: Tree -> TrNode
|
|
argsTree :: Tree -> [Tree]
|
|
|
|
nodeTree (Tr (n,_)) = n
|
|
argsTree (Tr (_,ts)) = ts
|
|
|
|
isFocusNode :: TrNode -> Bool
|
|
bindsNode :: TrNode -> Binds
|
|
atomNode :: TrNode -> Atom
|
|
valNode :: TrNode -> Val
|
|
constrsNode :: TrNode -> Constraints
|
|
metaSubstsNode :: TrNode -> MetaSubst
|
|
|
|
isFocusNode (N (_,_,_,_,b)) = b
|
|
bindsNode (N (b,_,_,_,_)) = b
|
|
atomNode (N (_,a,_,_,_)) = a
|
|
valNode (N (_,_,v,_,_)) = v
|
|
constrsNode (N (_,_,_,(c,_),_)) = c
|
|
metaSubstsNode (N (_,_,_,(_,m),_)) = m
|
|
|
|
atomTree :: Tree -> Atom
|
|
valTree :: Tree -> Val
|
|
|
|
atomTree = atomNode . nodeTree
|
|
valTree = valNode . nodeTree
|
|
|
|
mkNode :: Binds -> Atom -> Val -> (Constraints, MetaSubst) -> TrNode
|
|
mkNode binds atom vtyp cs = N (binds,atom,vtyp,cs,False)
|
|
|
|
metasTree :: Tree -> [MetaId]
|
|
metasTree = concatMap metasNode . scanTree where
|
|
metasNode n = [m | AtM m <- [atomNode n]] ++ map fst (metaSubstsNode n)
|
|
|
|
varsTree :: Tree -> [(Var,Val)]
|
|
varsTree t = [(x,v) | N (_,AtV x,v,_,_) <- scanTree t]
|
|
|
|
constrsTree :: Tree -> Constraints
|
|
constrsTree = constrsNode . nodeTree
|
|
|
|
allConstrsTree :: Tree -> Constraints
|
|
allConstrsTree = concatMap constrsNode . scanTree
|
|
|
|
changeConstrs :: (Constraints -> Constraints) -> TrNode -> TrNode
|
|
changeConstrs f (N (b,a,v,(c,m),x)) = N (b,a,v,(f c, m),x)
|
|
|
|
changeMetaSubst :: (MetaSubst -> MetaSubst) -> TrNode -> TrNode
|
|
changeMetaSubst f (N (b,a,v,(c,m),x)) = N (b,a,v,(c, f m),x)
|
|
|
|
changeAtom :: (Atom -> Atom) -> TrNode -> TrNode
|
|
changeAtom f (N (b,a,v,(c,m),x)) = N (b,f a,v,(c, m),x)
|
|
|
|
-- * on the way to Edit
|
|
|
|
uTree :: Tree
|
|
uTree = Tr (uNode, []) -- unknown tree
|
|
|
|
uNode :: TrNode
|
|
uNode = mkNode [] uAtom uVal ([],[])
|
|
|
|
|
|
uAtom :: Atom
|
|
uAtom = AtM meta0
|
|
|
|
mAtom :: Atom
|
|
mAtom = AtM meta0
|
|
-}
|
|
|
|
type Var = Ident
|
|
|
|
uVal :: Val
|
|
uVal = vClos uExp
|
|
|
|
vClos :: Exp -> Val
|
|
vClos = VClos []
|
|
|
|
uExp :: Exp
|
|
uExp = Meta meta0
|
|
|
|
mExp, mExp0 :: Exp
|
|
mExp = Meta meta0
|
|
mExp0 = mExp
|
|
|
|
meta2exp :: MetaId -> Exp
|
|
meta2exp = Meta
|
|
{-
|
|
atomC :: Fun -> Atom
|
|
atomC = AtC
|
|
|
|
funAtom :: Atom -> Err Fun
|
|
funAtom a = case a of
|
|
AtC f -> return f
|
|
_ -> prtBad "not function head" a
|
|
|
|
atomIsMeta :: Atom -> Bool
|
|
atomIsMeta atom = case atom of
|
|
AtM _ -> True
|
|
_ -> False
|
|
|
|
getMetaAtom :: Atom -> Err MetaId
|
|
getMetaAtom a = case a of
|
|
AtM m -> return m
|
|
_ -> Bad "the active node is not meta"
|
|
-}
|
|
cat2val :: Context -> Cat -> Val
|
|
cat2val cont cat = vClos $ mkApp (Q cat) [Meta i | i <- [1..length cont]]
|
|
|
|
val2cat :: Val -> Err Cat
|
|
val2cat v = liftM valCat (val2exp v)
|
|
|
|
substTerm :: [Ident] -> Substitution -> Term -> Term
|
|
substTerm ss g c = case c of
|
|
Vr x -> maybe c id $ lookup x g
|
|
App f a -> App (substTerm ss g f) (substTerm ss g a)
|
|
Abs b x t -> let y = mkFreshVarX ss x in
|
|
Abs b y (substTerm (y:ss) ((x, Vr y):g) t)
|
|
Prod b x a t -> let y = mkFreshVarX ss x in
|
|
Prod b y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) t)
|
|
_ -> c
|
|
|
|
metaSubstExp :: MetaSubst -> [(MetaId,Exp)]
|
|
metaSubstExp msubst = [(m, errVal (meta2exp m) (val2expSafe v)) | (m,v) <- msubst]
|
|
|
|
-- * belong here rather than to computation
|
|
|
|
substitute :: [Var] -> Substitution -> Exp -> Err Exp
|
|
substitute v s = return . substTerm v s
|
|
|
|
alphaConv :: [Var] -> (Var,Var) -> Exp -> Err Exp ---
|
|
alphaConv oldvars (x,x') = substitute (x:x':oldvars) [(x,Vr x')]
|
|
|
|
--alphaFresh :: [Var] -> Exp -> Err Exp
|
|
--alphaFresh vs = refreshTermN $ maxVarIndex vs
|
|
|
|
-- | done in a state monad
|
|
--alphaFreshAll :: [Var] -> [Exp] -> Err [Exp]
|
|
--alphaFreshAll vs = mapM $ alphaFresh vs
|
|
|
|
-- | for display
|
|
val2exp :: Val -> Err Exp
|
|
val2exp = val2expP False
|
|
|
|
-- | for type checking
|
|
val2expSafe :: Val -> Err Exp
|
|
val2expSafe = val2expP True
|
|
|
|
val2expP :: Bool -> Val -> Err Exp
|
|
val2expP safe v = case v of
|
|
|
|
VClos g@(_:_) e@(Meta _) -> if safe
|
|
then Bad (render (text "unsafe value substitution" <+> ppValue Unqualified 0 v))
|
|
else substVal g e
|
|
VClos g e -> substVal g e
|
|
VApp f c -> liftM2 App (val2expP safe f) (val2expP safe c)
|
|
VCn c -> return $ Q c
|
|
VGen i x -> if safe
|
|
then Bad (render (text "unsafe val2exp" <+> ppValue Unqualified 0 v))
|
|
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
|
|
where
|
|
substVal g e = mapPairsM (val2expP safe) g >>= return . (\s -> substTerm [] s e)
|
|
|
|
isConstVal :: Val -> Bool
|
|
isConstVal v = case v of
|
|
VApp f c -> isConstVal f && isConstVal c
|
|
VCn _ -> True
|
|
VClos [] e -> null $ freeVarsExp e
|
|
_ -> False --- could be more liberal
|
|
|
|
mkProdVal :: Binds -> Val -> Err Val ---
|
|
mkProdVal bs v = do
|
|
bs' <- mapPairsM val2exp bs
|
|
v' <- val2exp v
|
|
return $ vClos $ foldr (uncurry (Prod Explicit)) v' bs'
|
|
|
|
freeVarsExp :: Exp -> [Ident]
|
|
freeVarsExp e = case e of
|
|
Vr x -> [x]
|
|
App f c -> freeVarsExp f ++ freeVarsExp c
|
|
Abs _ x b -> filter (/=x) (freeVarsExp b)
|
|
Prod _ x a b -> freeVarsExp a ++ filter (/=x) (freeVarsExp b)
|
|
_ -> [] --- thus applies to abstract syntax only
|
|
|
|
int2var :: Int -> Ident
|
|
int2var = identS . ('$':) . show
|
|
|
|
meta0 :: MetaId
|
|
meta0 = 0
|
|
|
|
termMeta0 :: Term
|
|
termMeta0 = Meta meta0
|
|
|
|
identVar :: Term -> Err Ident
|
|
identVar (Vr x) = return x
|
|
identVar _ = Bad "not a variable"
|
|
|
|
|
|
-- | light-weight rename for user interaction; also change names of internal vars
|
|
qualifTerm :: Ident -> Term -> Term
|
|
qualifTerm m = qualif [] where
|
|
qualif xs t = case t of
|
|
Abs b x t -> let x' = chV x in Abs b x' $ qualif (x':xs) t
|
|
Prod b x a t -> Prod b x (qualif xs a) $ qualif (x:xs) t
|
|
Vr x -> let x' = chV x in if (elem x' xs) then (Vr x') else (Q (m,x))
|
|
Cn c -> Q (m,c)
|
|
Con c -> QC (m,c)
|
|
_ -> composSafeOp (qualif xs) t
|
|
chV x = string2var $ ident2raw x
|
|
|
|
string2var :: RawIdent -> Ident
|
|
string2var s = case showRawIdent s of
|
|
c:'_':i -> identV (rawIdentS [c]) (readIntArg i) ---
|
|
_ -> identC s
|
|
|
|
-- | reindex variables so that they tell nesting depth level
|
|
reindexTerm :: Term -> Term
|
|
reindexTerm = qualif (0,[]) where
|
|
qualif dg@(d,g) t = case t of
|
|
Abs b x t -> let x' = ind x d in Abs b x' $ qualif (d+1, (x,x'):g) t
|
|
Prod b x a t -> let x' = ind x d in Prod b x' (qualif dg a) $ qualif (d+1, (x,x'):g) t
|
|
Vr x -> Vr $ look x g
|
|
_ -> composSafeOp (qualif dg) t
|
|
look x = maybe x id . lookup x --- if x is not in scope it is unchanged
|
|
ind x d = identC $ ident2raw x `prefixRawIdent` rawIdentS "_" `prefixRawIdent` rawIdentS (show d)
|
|
|
|
{-
|
|
-- this method works for context-free abstract syntax
|
|
-- and is meant to be used in simple embedded GF applications
|
|
|
|
exp2tree :: Exp -> Err Tree
|
|
exp2tree e = do
|
|
(bs,f,xs) <- termForm e
|
|
cont <- case bs of
|
|
[] -> return []
|
|
_ -> prtBad "cannot convert bindings in" e
|
|
at <- case f of
|
|
Q m c -> return $ AtC (m,c)
|
|
QC m c -> return $ AtC (m,c)
|
|
Meta m -> return $ AtM m
|
|
K s -> return $ AtL s
|
|
EInt n -> return $ AtI n
|
|
EFloat n -> return $ AtF n
|
|
_ -> prtBad "cannot convert to atom" f
|
|
ts <- mapM exp2tree xs
|
|
return $ Tr (N (cont,at,uVal,([],[]),True),ts)
|
|
-}
|