diff --git a/src/GF/Compile/TC.hs b/src/GF/Compile/TC.hs index c0c8a83ae..f6e15b175 100644 --- a/src/GF/Compile/TC.hs +++ b/src/GF/Compile/TC.hs @@ -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 "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 Eqs es -> liftM concat $ mapM checkBranch es _ -> liftM snd $ checkExp th tenv def val diff --git a/src/GF/Compile/TypeCheck.hs b/src/GF/Compile/TypeCheck.hs index 99f46f86f..04fb44b18 100644 --- a/src/GF/Compile/TypeCheck.hs +++ b/src/GF/Compile/TypeCheck.hs @@ -106,7 +106,7 @@ checkContext st = checkTyp st . cont2exp checkTyp :: Grammar -> Type -> [String] 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 typ <- lookupFunType gr m fun cs <- justTypeCheck gr def (vClos typ) diff --git a/src/GF/Grammar/Grammar.hs b/src/GF/Grammar/Grammar.hs index c1ec709f3..19b8d4c9b 100644 --- a/src/GF/Grammar/Grammar.hs +++ b/src/GF/Grammar/Grammar.hs @@ -43,9 +43,6 @@ module GF.Grammar.Grammar (SourceGrammar, Param, Altern, Substitution, - Branch(..), - Con, - Trm, wildPatt, varLabel, tupleLabel, linLabel, theLinLabel, ident2label, label2ident @@ -233,10 +230,6 @@ type Altern = (Term, [(Term, 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 = LVar @@ -256,5 +249,3 @@ label2ident (LVar i) = identC (BS.pack ('$':show i)) wildPatt :: Patt wildPatt = PV identW - -type Trm = Term diff --git a/src/GF/Grammar/Macros.hs b/src/GF/Grammar/Macros.hs index 065dcef60..34c6302fd 100644 --- a/src/GF/Grammar/Macros.hs +++ b/src/GF/Grammar/Macros.hs @@ -405,7 +405,7 @@ freshMeta :: [MetaSymb] -> MetaSymb freshMeta ms = MetaSymb (minimum [n | n <- [0..length ms], notElem n (map metaSymbInt ms)]) -mkFreshMetasInTrm :: [MetaSymb] -> Trm -> Trm +mkFreshMetasInTrm :: [MetaSymb] -> Term -> Term mkFreshMetasInTrm metas = fst . rms minMeta where rms meta trm = case trm of Meta m -> (Meta (MetaSymb meta), meta + 1) diff --git a/src/GF/Grammar/Unify.hs b/src/GF/Grammar/Unify.hs index 588c1b306..58c0e37fd 100644 --- a/src/GF/Grammar/Unify.hs +++ b/src/GF/Grammar/Unify.hs @@ -38,8 +38,8 @@ unifyVal cs0 = do (_,VClos (_:_) _) -> True _ -> False -type Unifier = [(MetaSymb, Trm)] -type Constrs = [(Trm, Trm)] +type Unifier = [(MetaSymb, Term)] +type Constrs = [(Term, Term)] unifyAll :: Constrs -> Unifier -> (Unifier,Constrs) unifyAll [] g = (g, []) @@ -49,7 +49,7 @@ unifyAll ((a@(s, t)) : l) g = Ok g2 -> (g2, c) _ -> (g1, a : c) -unify :: Trm -> Trm -> Unifier -> Err Unifier +unify :: Term -> Term -> Unifier -> Err Unifier unify e1 e2 g = case (e1, e2) of (Meta s, t) -> do @@ -67,12 +67,12 @@ unify e1 e2 g = _ -> 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 | occCheck s t = prtBad "occurs check" t | True = return ((s, t) : g) -subst_all :: Unifier -> Trm -> Err Trm +subst_all :: Unifier -> Term -> Err Term subst_all s u = case (s,u) of ([], t) -> return t @@ -80,14 +80,14 @@ subst_all s u = t' <- (subst_all l t) --- successive substs - why ? return $ substMetas [a] t' -substMetas :: [(MetaSymb,Trm)] -> Trm -> Trm +substMetas :: [(MetaSymb,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 -> Trm -> Bool +occCheck :: MetaSymb -> Term -> Bool occCheck s u = case u of Meta v -> s == v App c a -> occCheck s c || occCheck s a