forked from GitHub/gf-core
rename MetaSymb in GF.Grammar.Grammar to MetaId to match the convention in PGF
This commit is contained in:
@@ -139,7 +139,7 @@ mkExp scope t = case GM.termForm t of
|
||||
EInt i -> C.ELit (C.LInt i)
|
||||
EFloat f -> C.ELit (C.LFlt f)
|
||||
K s -> C.ELit (C.LStr s)
|
||||
Meta (MetaSymb i) -> C.EMeta i
|
||||
Meta i -> C.EMeta i
|
||||
_ -> C.EMeta 0
|
||||
|
||||
mkPatt scope p =
|
||||
|
||||
@@ -37,7 +37,7 @@ data AExp =
|
||||
| AInt Integer
|
||||
| AFloat Double
|
||||
| AStr String
|
||||
| AMeta MetaSymb Val
|
||||
| AMeta MetaId Val
|
||||
| AApp AExp AExp Val
|
||||
| AAbs Ident Val AExp
|
||||
| AProd Ident AExp AExp
|
||||
@@ -234,7 +234,7 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
|
||||
|
||||
ps2ts k = foldr p2t ([],0,[],k)
|
||||
p2t p (ps,i,g,k) = case p of
|
||||
PW -> (Meta (MetaSymb i) : ps, i+1,g,k)
|
||||
PW -> (Meta i : ps, i+1,g,k)
|
||||
PV x -> (Vr x : ps, i, upd x k g,k+1)
|
||||
PString s -> (K s : ps, i, g, k)
|
||||
PInt n -> (EInt n : ps, i, g, k)
|
||||
|
||||
@@ -254,10 +254,6 @@ instance Binary Label where
|
||||
1 -> fmap LVar get
|
||||
_ -> decodingError
|
||||
|
||||
instance Binary MetaSymb where
|
||||
put (MetaSymb m) = put m
|
||||
get = fmap MetaSymb get
|
||||
|
||||
decodeModHeader :: FilePath -> IO SourceModule
|
||||
decodeModHeader fpath = do
|
||||
(m,mtype,mstatus,flags,extend,mwith,opens,med) <- decodeFile fpath
|
||||
|
||||
@@ -29,7 +29,7 @@ module GF.Grammar.Grammar (SourceGrammar,
|
||||
Patt(..),
|
||||
TInfo(..),
|
||||
Label(..),
|
||||
MetaSymb(..),
|
||||
MetaId,
|
||||
Hypo,
|
||||
Context,
|
||||
Equation,
|
||||
@@ -115,7 +115,7 @@ data Term =
|
||||
|
||||
| App Term Term -- ^ application: @f a@
|
||||
| Abs Ident Term -- ^ abstraction: @\x -> b@
|
||||
| Meta MetaSymb -- ^ metavariable: @?i@ (only parsable: ? = ?0)
|
||||
| Meta {-# UNPACK #-} !MetaId -- ^ metavariable: @?i@ (only parsable: ? = ?0)
|
||||
| Prod Ident Term Term -- ^ function type: @(x : A) -> B@
|
||||
| Typed Term Term -- ^ type-annotated term
|
||||
--
|
||||
@@ -198,7 +198,7 @@ data Label =
|
||||
| LVar Int
|
||||
deriving (Show, Eq, Ord)
|
||||
|
||||
newtype MetaSymb = MetaSymb Int deriving (Show, Eq, Ord)
|
||||
type MetaId = Int
|
||||
|
||||
type Hypo = (Ident,Term) -- (x:A) (_:A) A
|
||||
type Context = [Hypo] -- (x:A)(y:B) (x,y:A) (_,_:A)
|
||||
|
||||
@@ -59,7 +59,7 @@ valTree = valNode . nodeTree
|
||||
mkNode :: Binds -> Atom -> Val -> (Constraints, MetaSubst) -> TrNode
|
||||
mkNode binds atom vtyp cs = N (binds,atom,vtyp,cs,False)
|
||||
|
||||
metasTree :: Tree -> [Meta]
|
||||
metasTree :: Tree -> [MetaId]
|
||||
metasTree = concatMap metasNode . scanTree where
|
||||
metasNode n = [m | AtM m <- [atomNode n]] ++ map fst (metaSubstsNode n)
|
||||
|
||||
@@ -98,7 +98,6 @@ mAtom = AtM meta0
|
||||
-}
|
||||
|
||||
type Var = Ident
|
||||
type Meta = MetaSymb
|
||||
|
||||
uVal :: Val
|
||||
uVal = vClos uExp
|
||||
@@ -113,7 +112,7 @@ mExp, mExp0 :: Exp
|
||||
mExp = Meta meta0
|
||||
mExp0 = mExp
|
||||
|
||||
meta2exp :: MetaSymb -> Exp
|
||||
meta2exp :: MetaId -> Exp
|
||||
meta2exp = Meta
|
||||
{-
|
||||
atomC :: Fun -> Atom
|
||||
@@ -129,13 +128,13 @@ atomIsMeta atom = case atom of
|
||||
AtM _ -> True
|
||||
_ -> False
|
||||
|
||||
getMetaAtom :: Atom -> Err Meta
|
||||
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 (qq cat) [mkMeta i | i <- [1..length cont]]
|
||||
cat2val cont cat = vClos $ mkApp (qq cat) [Meta i | i <- [1..length cont]]
|
||||
|
||||
val2cat :: Val -> Err Cat
|
||||
val2cat v = val2exp v >>= valCat
|
||||
@@ -150,7 +149,7 @@ substTerm ss g c = case c of
|
||||
Prod y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) b)
|
||||
_ -> c
|
||||
|
||||
metaSubstExp :: MetaSubst -> [(Meta,Exp)]
|
||||
metaSubstExp :: MetaSubst -> [(MetaId,Exp)]
|
||||
metaSubstExp msubst = [(m, errVal (meta2exp m) (val2expSafe v)) | (m,v) <- msubst]
|
||||
|
||||
-- * belong here rather than to computation
|
||||
@@ -230,21 +229,6 @@ addBinds b (Tr (N (b0,at,t,c,x),ts)) = Tr (N (b ++ b0,at,t,c,x),ts)
|
||||
bodyTree :: Tree -> Tree
|
||||
bodyTree (Tr (N (_,a,t,c,x),ts)) = Tr (N ([],a,t,c,x),ts)
|
||||
-}
|
||||
refreshMetas :: [Meta] -> Exp -> Exp
|
||||
refreshMetas metas = fst . rms minMeta where
|
||||
rms meta trm = case trm of
|
||||
Meta m -> (Meta meta, nextMeta meta)
|
||||
App f a -> let (f',msf) = rms meta f
|
||||
(a',msa) = rms msf a
|
||||
in (App f' a', msa)
|
||||
Prod x a b ->
|
||||
let (a',msa) = rms meta a
|
||||
(b',msb) = rms msa b
|
||||
in (Prod x a' b', msb)
|
||||
Abs x b -> let (b',msb) = rms meta b in (Abs x b', msb)
|
||||
_ -> (trm,meta)
|
||||
minMeta = int2meta $
|
||||
if null metas then 0 else (maximum (map metaSymbInt metas) + 1)
|
||||
|
||||
ref2exp :: [Var] -> Type -> Ref -> Err Exp
|
||||
ref2exp bounds typ ref = do
|
||||
@@ -284,8 +268,8 @@ mkJustProd cont typ = mkProd (cont,typ,[])
|
||||
int2var :: Int -> Ident
|
||||
int2var = identC . BS.pack . ('$':) . show
|
||||
|
||||
meta0 :: Meta
|
||||
meta0 = int2meta 0
|
||||
meta0 :: MetaId
|
||||
meta0 = 0
|
||||
|
||||
termMeta0 :: Term
|
||||
termMeta0 = Meta meta0
|
||||
|
||||
@@ -364,49 +364,6 @@ justIdentOf (Vr x) = Just x
|
||||
justIdentOf (Cn x) = Just x
|
||||
justIdentOf _ = Nothing
|
||||
|
||||
isMeta :: Term -> Bool
|
||||
isMeta (Meta _) = True
|
||||
isMeta _ = False
|
||||
|
||||
mkMeta :: Int -> Term
|
||||
mkMeta = Meta . MetaSymb
|
||||
|
||||
nextMeta :: MetaSymb -> MetaSymb
|
||||
nextMeta = int2meta . succ . metaSymbInt
|
||||
|
||||
int2meta :: Int -> MetaSymb
|
||||
int2meta = MetaSymb
|
||||
|
||||
metaSymbInt :: MetaSymb -> Int
|
||||
metaSymbInt (MetaSymb k) = k
|
||||
|
||||
freshMeta :: [MetaSymb] -> MetaSymb
|
||||
freshMeta ms = MetaSymb (minimum [n | n <- [0..length ms],
|
||||
notElem n (map metaSymbInt ms)])
|
||||
|
||||
mkFreshMetasInTrm :: [MetaSymb] -> Term -> Term
|
||||
mkFreshMetasInTrm metas = fst . rms minMeta where
|
||||
rms meta trm = case trm of
|
||||
Meta m -> (Meta (MetaSymb meta), meta + 1)
|
||||
App f a -> let (f',msf) = rms meta f
|
||||
(a',msa) = rms msf a
|
||||
in (App f' a', msa)
|
||||
Prod x a b ->
|
||||
let (a',msa) = rms meta a
|
||||
(b',msb) = rms msa b
|
||||
in (Prod x a' b', msb)
|
||||
Abs x b -> let (b',msb) = rms meta b in (Abs x b', msb)
|
||||
_ -> (trm,meta)
|
||||
minMeta = if null metas then 0 else (maximum (map metaSymbInt metas) + 1)
|
||||
|
||||
-- | decides that a term has no metavariables
|
||||
isCompleteTerm :: Term -> Bool
|
||||
isCompleteTerm t = case t of
|
||||
Meta _ -> False
|
||||
Abs _ b -> isCompleteTerm b
|
||||
App f a -> isCompleteTerm f && isCompleteTerm a
|
||||
_ -> True
|
||||
|
||||
linTypeStr :: Type
|
||||
linTypeStr = mkRecType linLabel [typeStr] -- default lintype {s :: Str}
|
||||
|
||||
@@ -696,9 +653,6 @@ noExist = FV []
|
||||
defaultLinType :: Type
|
||||
defaultLinType = mkRecType linLabel [typeStr]
|
||||
|
||||
metaTerms :: [Term]
|
||||
metaTerms = map (Meta . MetaSymb) [0..]
|
||||
|
||||
-- | from GF1, 20\/9\/2003
|
||||
isInOneType :: Type -> Bool
|
||||
isInOneType t = case t of
|
||||
|
||||
@@ -437,7 +437,7 @@ Exp6
|
||||
| String { K $1 }
|
||||
| Integer { EInt $1 }
|
||||
| Double { EFloat $1 }
|
||||
| '?' { Meta (int2meta 0) }
|
||||
| '?' { Meta 0 }
|
||||
| '[' ']' { Empty }
|
||||
| '[' Ident Exps ']' { foldl App (Vr (mkListId $2)) $3 }
|
||||
| '[' String ']' { case $2 of
|
||||
|
||||
@@ -38,7 +38,7 @@ unifyVal cs0 = do
|
||||
(_,VClos (_:_) _) -> True
|
||||
_ -> False
|
||||
|
||||
type Unifier = [(MetaSymb, Term)]
|
||||
type Unifier = [(MetaId, Term)]
|
||||
type Constrs = [(Term, Term)]
|
||||
|
||||
unifyAll :: Constrs -> Unifier -> (Unifier,Constrs)
|
||||
@@ -68,7 +68,7 @@ unify e1 e2 g =
|
||||
(RecType xs,RecType ys) | xs == ys -> return g
|
||||
_ -> Bad (render (text "fail unify" <+> ppTerm Unqualified 0 e1))
|
||||
|
||||
extend :: Unifier -> MetaSymb -> Term -> Err Unifier
|
||||
extend :: Unifier -> MetaId -> Term -> Err Unifier
|
||||
extend g s t | (t == Meta s) = return g
|
||||
| occCheck s t = Bad (render (text "occurs check" <+> ppTerm Unqualified 0 t))
|
||||
| True = return ((s, t) : g)
|
||||
@@ -81,14 +81,14 @@ subst_all s u =
|
||||
t' <- (subst_all l t) --- successive substs - why ?
|
||||
return $ substMetas [a] t'
|
||||
|
||||
substMetas :: [(MetaSymb,Term)] -> Term -> Term
|
||||
substMetas :: [(MetaId,Term)] -> Term -> Term
|
||||
substMetas subst trm = case trm of
|
||||
Meta x -> case lookup x subst of
|
||||
Just t -> t
|
||||
_ -> trm
|
||||
_ -> composSafeOp (substMetas subst) trm
|
||||
|
||||
occCheck :: MetaSymb -> Term -> Bool
|
||||
occCheck :: MetaId -> Term -> Bool
|
||||
occCheck s u = case u of
|
||||
Meta v -> s == v
|
||||
App c a -> occCheck s c || occCheck s a
|
||||
|
||||
@@ -49,12 +49,12 @@ newtype TrNode = N (Binds,Atom,Val,(Constraints,MetaSubst),Bool)
|
||||
deriving (Eq,Show)
|
||||
|
||||
data Atom =
|
||||
AtC Fun | AtM MetaSymb | AtV Ident | AtL String | AtI Integer | AtF Double
|
||||
AtC Fun | AtM MetaId | AtV Ident | AtL String | AtI Integer | AtF Double
|
||||
deriving (Eq,Show)
|
||||
-}
|
||||
type Binds = [(Ident,Val)]
|
||||
type Constraints = [(Val,Val)]
|
||||
type MetaSubst = [(MetaSymb,Val)]
|
||||
type MetaSubst = [(MetaId,Val)]
|
||||
|
||||
|
||||
-- for TC
|
||||
|
||||
Reference in New Issue
Block a user