forked from GitHub/gf-core
remove some dead types from GF.Grammar.Grammar
This commit is contained in:
@@ -164,7 +164,7 @@ 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
|
||||||
|
|
||||||
checkEqs :: Theory -> TCEnv -> (Fun,Trm) -> Val -> Err [(Val,Val)]
|
checkEqs :: Theory -> TCEnv -> (Fun,Term) -> Val -> Err [(Val,Val)]
|
||||||
checkEqs th tenv@(k,rho,gamma) (fun@(m,f),def) val = case def of
|
checkEqs th tenv@(k,rho,gamma) (fun@(m,f),def) val = case def of
|
||||||
Eqs es -> liftM concat $ mapM checkBranch es
|
Eqs es -> liftM concat $ mapM checkBranch es
|
||||||
_ -> liftM snd $ checkExp th tenv def val
|
_ -> liftM snd $ checkExp th tenv def val
|
||||||
|
|||||||
@@ -106,7 +106,7 @@ checkContext st = checkTyp st . cont2exp
|
|||||||
checkTyp :: Grammar -> Type -> [String]
|
checkTyp :: Grammar -> Type -> [String]
|
||||||
checkTyp gr typ = err singleton prConstrs $ justTypeCheck gr typ vType
|
checkTyp gr typ = err singleton prConstrs $ justTypeCheck gr typ vType
|
||||||
|
|
||||||
checkEquation :: Grammar -> Fun -> Trm -> [String]
|
checkEquation :: Grammar -> Fun -> Term -> [String]
|
||||||
checkEquation gr (m,fun) def = err singleton id $ do
|
checkEquation gr (m,fun) def = err singleton id $ do
|
||||||
typ <- lookupFunType gr m fun
|
typ <- lookupFunType gr m fun
|
||||||
cs <- justTypeCheck gr def (vClos typ)
|
cs <- justTypeCheck gr def (vClos typ)
|
||||||
|
|||||||
@@ -43,9 +43,6 @@ module GF.Grammar.Grammar (SourceGrammar,
|
|||||||
Param,
|
Param,
|
||||||
Altern,
|
Altern,
|
||||||
Substitution,
|
Substitution,
|
||||||
Branch(..),
|
|
||||||
Con,
|
|
||||||
Trm,
|
|
||||||
wildPatt,
|
wildPatt,
|
||||||
varLabel, tupleLabel, linLabel, theLinLabel,
|
varLabel, tupleLabel, linLabel, theLinLabel,
|
||||||
ident2label, label2ident
|
ident2label, label2ident
|
||||||
@@ -233,10 +230,6 @@ type Altern = (Term, [(Term, Term)])
|
|||||||
|
|
||||||
type Substitution = [(Ident, Term)]
|
type Substitution = [(Ident, Term)]
|
||||||
|
|
||||||
-- | branches à la Alfa
|
|
||||||
newtype Branch = Branch (Con,([Ident],Term)) deriving (Eq, Ord,Show,Read)
|
|
||||||
type Con = Ident ---
|
|
||||||
|
|
||||||
varLabel :: Int -> Label
|
varLabel :: Int -> Label
|
||||||
varLabel = LVar
|
varLabel = LVar
|
||||||
|
|
||||||
@@ -256,5 +249,3 @@ label2ident (LVar i) = identC (BS.pack ('$':show i))
|
|||||||
|
|
||||||
wildPatt :: Patt
|
wildPatt :: Patt
|
||||||
wildPatt = PV identW
|
wildPatt = PV identW
|
||||||
|
|
||||||
type Trm = Term
|
|
||||||
|
|||||||
@@ -405,7 +405,7 @@ freshMeta :: [MetaSymb] -> MetaSymb
|
|||||||
freshMeta ms = MetaSymb (minimum [n | n <- [0..length ms],
|
freshMeta ms = MetaSymb (minimum [n | n <- [0..length ms],
|
||||||
notElem n (map metaSymbInt ms)])
|
notElem n (map metaSymbInt ms)])
|
||||||
|
|
||||||
mkFreshMetasInTrm :: [MetaSymb] -> Trm -> Trm
|
mkFreshMetasInTrm :: [MetaSymb] -> Term -> Term
|
||||||
mkFreshMetasInTrm metas = fst . rms minMeta where
|
mkFreshMetasInTrm metas = fst . rms minMeta where
|
||||||
rms meta trm = case trm of
|
rms meta trm = case trm of
|
||||||
Meta m -> (Meta (MetaSymb meta), meta + 1)
|
Meta m -> (Meta (MetaSymb meta), meta + 1)
|
||||||
|
|||||||
@@ -38,8 +38,8 @@ unifyVal cs0 = do
|
|||||||
(_,VClos (_:_) _) -> True
|
(_,VClos (_:_) _) -> True
|
||||||
_ -> False
|
_ -> False
|
||||||
|
|
||||||
type Unifier = [(MetaSymb, Trm)]
|
type Unifier = [(MetaSymb, Term)]
|
||||||
type Constrs = [(Trm, Trm)]
|
type Constrs = [(Term, Term)]
|
||||||
|
|
||||||
unifyAll :: Constrs -> Unifier -> (Unifier,Constrs)
|
unifyAll :: Constrs -> Unifier -> (Unifier,Constrs)
|
||||||
unifyAll [] g = (g, [])
|
unifyAll [] g = (g, [])
|
||||||
@@ -49,7 +49,7 @@ unifyAll ((a@(s, t)) : l) g =
|
|||||||
Ok g2 -> (g2, c)
|
Ok g2 -> (g2, c)
|
||||||
_ -> (g1, a : c)
|
_ -> (g1, a : c)
|
||||||
|
|
||||||
unify :: Trm -> Trm -> Unifier -> Err Unifier
|
unify :: Term -> Term -> Unifier -> Err Unifier
|
||||||
unify e1 e2 g =
|
unify e1 e2 g =
|
||||||
case (e1, e2) of
|
case (e1, e2) of
|
||||||
(Meta s, t) -> do
|
(Meta s, t) -> do
|
||||||
@@ -67,12 +67,12 @@ unify e1 e2 g =
|
|||||||
_ -> prtBad "fail unify" e1
|
_ -> prtBad "fail unify" e1
|
||||||
_ -> prtBad "fail unify" e1
|
_ -> prtBad "fail unify" e1
|
||||||
|
|
||||||
extend :: Unifier -> MetaSymb -> Trm -> Err Unifier
|
extend :: Unifier -> MetaSymb -> Term -> Err Unifier
|
||||||
extend g s t | (t == Meta s) = return g
|
extend g s t | (t == Meta s) = return g
|
||||||
| occCheck s t = prtBad "occurs check" t
|
| occCheck s t = prtBad "occurs check" t
|
||||||
| True = return ((s, t) : g)
|
| True = return ((s, t) : g)
|
||||||
|
|
||||||
subst_all :: Unifier -> Trm -> Err Trm
|
subst_all :: Unifier -> Term -> Err Term
|
||||||
subst_all s u =
|
subst_all s u =
|
||||||
case (s,u) of
|
case (s,u) of
|
||||||
([], t) -> return t
|
([], t) -> return t
|
||||||
@@ -80,14 +80,14 @@ subst_all s u =
|
|||||||
t' <- (subst_all l t) --- successive substs - why ?
|
t' <- (subst_all l t) --- successive substs - why ?
|
||||||
return $ substMetas [a] t'
|
return $ substMetas [a] t'
|
||||||
|
|
||||||
substMetas :: [(MetaSymb,Trm)] -> Trm -> Trm
|
substMetas :: [(MetaSymb,Term)] -> Term -> Term
|
||||||
substMetas subst trm = case trm of
|
substMetas subst trm = case trm of
|
||||||
Meta x -> case lookup x subst of
|
Meta x -> case lookup x subst of
|
||||||
Just t -> t
|
Just t -> t
|
||||||
_ -> trm
|
_ -> trm
|
||||||
_ -> composSafeOp (substMetas subst) trm
|
_ -> composSafeOp (substMetas subst) trm
|
||||||
|
|
||||||
occCheck :: MetaSymb -> Trm -> Bool
|
occCheck :: MetaSymb -> Term -> Bool
|
||||||
occCheck s u = case u of
|
occCheck s u = case u of
|
||||||
Meta v -> s == v
|
Meta v -> s == v
|
||||||
App c a -> occCheck s c || occCheck s a
|
App c a -> occCheck s c || occCheck s a
|
||||||
|
|||||||
Reference in New Issue
Block a user