-- I have made minor changes to the file below to make it compile | |
-- with GHC 8.0 | |
----------------------------------------------------------------------------- | |
-- Thih: Typing Haskell in Haskell, main program | |
-- | |
-- Part of `Typing Haskell in Haskell', version of November 23, 2000 | |
-- Copyright (c) Mark P Jones and the Oregon Graduate Institute | |
-- of Science and Technology, 1999-2000 | |
-- | |
-- This program is distributed as Free Software under the terms | |
-- in the file "License" that is included in the distribution | |
-- of this software, copies of which may be obtained from: | |
-- http://www.cse.ogi.edu/~mpj/thih/ | |
-- | |
-- | |
-- This file contains all the text from the paper in one single file | |
-- that can be loaded into Hugs for type checking. No additional code | |
-- is included. | |
-- | |
-- Like other incarnations of this program, this version is generated | |
-- automatically from the very same source code as the others. Its | |
-- *sole* purpose in life is to provide a quick way to check that the | |
-- code in the paper is free from syntax and type errors. If you | |
-- actually want to run the program with real data, use the multiple | |
-- file version. | |
-- | |
----------------------------------------------------------------------------- | |
module TypingHaskellInHaskell where | |
import Data.List(nub, (\\), intersect, union, partition) | |
import Control.Monad(msum, ap, liftM) | |
----------------------------------------------------------------------------- | |
-- Id: Identifiers | |
----------------------------------------------------------------------------- | |
type Id = String | |
enumId :: Int -> Id | |
enumId n = "v" ++ show n | |
----------------------------------------------------------------------------- | |
-- Kind: Kinds | |
----------------------------------------------------------------------------- | |
data Kind = Star | Kfun Kind Kind | |
deriving Eq | |
----------------------------------------------------------------------------- | |
-- Type: Types | |
----------------------------------------------------------------------------- | |
data Type = TVar Tyvar | TCon Tycon | TAp Type Type | TGen Int | |
deriving Eq | |
data Tyvar = Tyvar Id Kind | |
deriving Eq | |
data Tycon = Tycon Id Kind | |
deriving Eq | |
tUnit = TCon (Tycon "()" Star) | |
tChar = TCon (Tycon "Char" Star) | |
tInt = TCon (Tycon "Int" Star) | |
tInteger = TCon (Tycon "Integer" Star) | |
tFloat = TCon (Tycon "Float" Star) | |
tDouble = TCon (Tycon "Double" Star) | |
tList = TCon (Tycon "[]" (Kfun Star Star)) | |
tArrow = TCon (Tycon "(->)" (Kfun Star (Kfun Star Star))) | |
tTuple2 = TCon (Tycon "(,)" (Kfun Star (Kfun Star Star))) | |
tString :: Type | |
tString = list tChar | |
infixr 4 `fn` | |
fn :: Type -> Type -> Type | |
a `fn` b = TAp (TAp tArrow a) b | |
list :: Type -> Type | |
list t = TAp tList t | |
pair :: Type -> Type -> Type | |
pair a b = TAp (TAp tTuple2 a) b | |
class HasKind t where | |
kind :: t -> Kind | |
instance HasKind Tyvar where | |
kind (Tyvar v k) = k | |
instance HasKind Tycon where | |
kind (Tycon v k) = k | |
instance HasKind Type where | |
kind (TCon tc) = kind tc | |
kind (TVar u) = kind u | |
kind (TAp t _) = case (kind t) of | |
(Kfun _ k) -> k | |
----------------------------------------------------------------------------- | |
-- Subst: Substitutions | |
----------------------------------------------------------------------------- | |
type Subst = [(Tyvar, Type)] | |
nullSubst :: Subst | |
nullSubst = [] | |
(+->) :: Tyvar -> Type -> Subst | |
u +-> t = [(u, t)] | |
class Types t where | |
apply :: Subst -> t -> t | |
tv :: t -> [Tyvar] | |
instance Types Type where | |
apply s (TVar u) = case lookup u s of | |
Just t -> t | |
Nothing -> TVar u | |
apply s (TAp l r) = TAp (apply s l) (apply s r) | |
apply s t = t | |
tv (TVar u) = [u] | |
tv (TAp l r) = tv l `union` tv r | |
tv t = [] | |
instance Types a => Types [a] where | |
apply s = map (apply s) | |
tv = nub . concat . map tv | |
infixr 4 @@ | |
(@@) :: Subst -> Subst -> Subst | |
s1 @@ s2 = [ (u, apply s1 t) | (u,t) <- s2 ] ++ s1 | |
merge :: Monad m => Subst -> Subst -> m Subst | |
merge s1 s2 = if agree then return (s1++s2) else fail "merge fails" | |
where agree = all (\v -> apply s1 (TVar v) == apply s2 (TVar v)) | |
(map fst s1 `intersect` map fst s2) | |
----------------------------------------------------------------------------- | |
-- Unify: Unification | |
----------------------------------------------------------------------------- | |
mgu :: Monad m => Type -> Type -> m Subst | |
varBind :: Monad m => Tyvar -> Type -> m Subst | |
mgu (TAp l r) (TAp l' r') = do s1 <- mgu l l' | |
s2 <- mgu (apply s1 r) (apply s1 r') | |
return (s2 @@ s1) | |
mgu (TVar u) t = varBind u t | |
mgu t (TVar u) = varBind u t | |
mgu (TCon tc1) (TCon tc2) | |
| tc1==tc2 = return nullSubst | |
mgu t1 t2 = fail "types do not unify" | |
varBind u t | t == TVar u = return nullSubst | |
| u `elem` tv t = fail "occurs check fails" | |
| kind u /= kind t = fail "kinds do not match" | |
| otherwise = return (u +-> t) | |
match :: Monad m => Type -> Type -> m Subst | |
match (TAp l r) (TAp l' r') = do sl <- match l l' | |
sr <- match r r' | |
merge sl sr | |
match (TVar u) t | kind u == kind t = return (u +-> t) | |
match (TCon tc1) (TCon tc2) | |
| tc1==tc2 = return nullSubst | |
match t1 t2 = fail "types do not match" | |
----------------------------------------------------------------------------- | |
-- Pred: Predicates | |
----------------------------------------------------------------------------- | |
data Qual t = [Pred] :=> t | |
deriving Eq | |
data Pred = IsIn Id Type | |
deriving Eq | |
instance Types t => Types (Qual t) where | |
apply s (ps :=> t) = apply s ps :=> apply s t | |
tv (ps :=> t) = tv ps `union` tv t | |
instance Types Pred where | |
apply s (IsIn i t) = IsIn i (apply s t) | |
tv (IsIn i t) = tv t | |
mguPred, matchPred :: Pred -> Pred -> Maybe Subst | |
mguPred = lift mgu | |
matchPred = lift match | |
lift m (IsIn i t) (IsIn i' t') | |
| i == i' = m t t' | |
| otherwise = fail "classes differ" | |
type Class = ([Id], [Inst]) | |
type Inst = Qual Pred | |
----------------------------------------------------------------------------- | |
data ClassEnv = ClassEnv { classes :: Id -> Maybe Class, | |
defaults :: [Type] } | |
super :: ClassEnv -> Id -> [Id] | |
super ce i = case classes ce i of Just (is, its) -> is | |
insts :: ClassEnv -> Id -> [Inst] | |
insts ce i = case classes ce i of Just (is, its) -> its | |
defined :: Maybe a -> Bool | |
defined (Just x) = True | |
defined Nothing = False | |
modify :: ClassEnv -> Id -> Class -> ClassEnv | |
modify ce i c = ce{classes = \j -> if i==j then Just c | |
else classes ce j} | |
initialEnv :: ClassEnv | |
initialEnv = ClassEnv { classes = \i -> fail "class not defined", | |
defaults = [tInteger, tDouble] } | |
type EnvTransformer = ClassEnv -> Maybe ClassEnv | |
infixr 5 <:> | |
(<:>) :: EnvTransformer -> EnvTransformer -> EnvTransformer | |
(f <:> g) ce = do ce' <- f ce | |
g ce' | |
addClass :: Id -> [Id] -> EnvTransformer | |
addClass i is ce | |
| defined (classes ce i) = fail "class already defined" | |
| any (not . defined . classes ce) is = fail "superclass not defined" | |
| otherwise = return (modify ce i (is, [])) | |
addPreludeClasses :: EnvTransformer | |
addPreludeClasses = addCoreClasses <:> addNumClasses | |
addCoreClasses :: EnvTransformer | |
addCoreClasses = addClass "Eq" [] | |
<:> addClass "Ord" ["Eq"] | |
<:> addClass "Show" [] | |
<:> addClass "Read" [] | |
<:> addClass "Bounded" [] | |
<:> addClass "Enum" [] | |
<:> addClass "Functor" [] | |
<:> addClass "Monad" [] | |
addNumClasses :: EnvTransformer | |
addNumClasses = addClass "Num" ["Eq", "Show"] | |
<:> addClass "Real" ["Num", "Ord"] | |
<:> addClass "Fractional" ["Num"] | |
<:> addClass "Integral" ["Real", "Enum"] | |
<:> addClass "RealFrac" ["Real", "Fractional"] | |
<:> addClass "Floating" ["Fractional"] | |
<:> addClass "RealFloat" ["RealFrac", "Floating"] | |
addInst :: [Pred] -> Pred -> EnvTransformer | |
addInst ps p@(IsIn i _) ce | |
| not (defined (classes ce i)) = fail "no class for instance" | |
| any (overlap p) qs = fail "overlapping instance" | |
| otherwise = return (modify ce i c) | |
where its = insts ce i | |
qs = [ q | (_ :=> q) <- its ] | |
c = (super ce i, (ps:=>p) : its) | |
overlap :: Pred -> Pred -> Bool | |
overlap p q = defined (mguPred p q) | |
exampleInsts :: EnvTransformer | |
exampleInsts = addPreludeClasses | |
<:> addInst [] (IsIn "Ord" tUnit) | |
<:> addInst [] (IsIn "Ord" tChar) | |
<:> addInst [] (IsIn "Ord" tInt) | |
<:> addInst [IsIn "Ord" (TVar (Tyvar "a" Star)), | |
IsIn "Ord" (TVar (Tyvar "b" Star))] | |
(IsIn "Ord" (pair (TVar (Tyvar "a" Star)) | |
(TVar (Tyvar "b" Star)))) | |
----------------------------------------------------------------------------- | |
bySuper :: ClassEnv -> Pred -> [Pred] | |
bySuper ce p@(IsIn i t) | |
= p : concat [ bySuper ce (IsIn i' t) | i' <- super ce i ] | |
byInst :: ClassEnv -> Pred -> Maybe [Pred] | |
byInst ce p@(IsIn i t) = msum [ tryInst it | it <- insts ce i ] | |
where tryInst (ps :=> h) = do u <- matchPred h p | |
Just (map (apply u) ps) | |
entail :: ClassEnv -> [Pred] -> Pred -> Bool | |
entail ce ps p = any (p `elem`) (map (bySuper ce) ps) || | |
case byInst ce p of | |
Nothing -> False | |
Just qs -> all (entail ce ps) qs | |
----------------------------------------------------------------------------- | |
inHnf :: Pred -> Bool | |
inHnf (IsIn c t) = hnf t | |
where hnf (TVar v) = True | |
hnf (TCon tc) = False | |
hnf (TAp t _) = hnf t | |
toHnfs :: Monad m => ClassEnv -> [Pred] -> m [Pred] | |
toHnfs ce ps = do pss <- mapM (toHnf ce) ps | |
return (concat pss) | |
toHnf :: Monad m => ClassEnv -> Pred -> m [Pred] | |
toHnf ce p | inHnf p = return [p] | |
| otherwise = case byInst ce p of | |
Nothing -> fail "context reduction" | |
Just ps -> toHnfs ce ps | |
simplify :: ClassEnv -> [Pred] -> [Pred] | |
simplify ce = loop [] | |
where loop rs [] = rs | |
loop rs (p:ps) | entail ce (rs++ps) p = loop rs ps | |
| otherwise = loop (p:rs) ps | |
reduce :: Monad m => ClassEnv -> [Pred] -> m [Pred] | |
reduce ce ps = do qs <- toHnfs ce ps | |
return (simplify ce qs) | |
scEntail :: ClassEnv -> [Pred] -> Pred -> Bool | |
scEntail ce ps p = any (p `elem`) (map (bySuper ce) ps) | |
----------------------------------------------------------------------------- | |
-- Scheme: Type schemes | |
----------------------------------------------------------------------------- | |
data Scheme = Forall [Kind] (Qual Type) | |
deriving Eq | |
instance Types Scheme where | |
apply s (Forall ks qt) = Forall ks (apply s qt) | |
tv (Forall ks qt) = tv qt | |
quantify :: [Tyvar] -> Qual Type -> Scheme | |
quantify vs qt = Forall ks (apply s qt) | |
where vs' = [ v | v <- tv qt, v `elem` vs ] | |
ks = map kind vs' | |
s = zip vs' (map TGen [0..]) | |
toScheme :: Type -> Scheme | |
toScheme t = Forall [] ([] :=> t) | |
----------------------------------------------------------------------------- | |
-- Assump: Assumptions | |
----------------------------------------------------------------------------- | |
data Assump = Id :>: Scheme | |
instance Types Assump where | |
apply s (i :>: sc) = i :>: (apply s sc) | |
tv (i :>: sc) = tv sc | |
find :: Monad m => Id -> [Assump] -> m Scheme | |
find i [] = fail ("unbound identifier: " ++ i) | |
find i ((i':>:sc):as) = if i==i' then return sc else find i as | |
----------------------------------------------------------------------------- | |
-- TIMonad: Type inference monad | |
----------------------------------------------------------------------------- | |
newtype TI a = TI (Subst -> Int -> (Subst, Int, a)) | |
instance Functor TI where | |
fmap = liftM | |
instance Applicative TI where | |
pure = return | |
(<*>) = ap | |
instance Monad TI where | |
return x = TI (\s n -> (s,n,x)) | |
TI f >>= g = TI (\s n -> case f s n of | |
(s',m,x) -> let TI gx = g x | |
in gx s' m) | |
runTI :: TI a -> a | |
runTI (TI f) = x where (s,n,x) = f nullSubst 0 | |
getSubst :: TI Subst | |
getSubst = TI (\s n -> (s,n,s)) | |
unify :: Type -> Type -> TI () | |
unify t1 t2 = do s <- getSubst | |
u <- mgu (apply s t1) (apply s t2) | |
extSubst u | |
extSubst :: Subst -> TI () | |
extSubst s' = TI (\s n -> (s'@@s, n, ())) | |
newTVar :: Kind -> TI Type | |
newTVar k = TI (\s n -> let v = Tyvar (enumId n) k | |
in (s, n+1, TVar v)) | |
freshInst :: Scheme -> TI (Qual Type) | |
freshInst (Forall ks qt) = do ts <- mapM newTVar ks | |
return (inst ts qt) | |
class Instantiate t where | |
inst :: [Type] -> t -> t | |
instance Instantiate Type where | |
inst ts (TAp l r) = TAp (inst ts l) (inst ts r) | |
inst ts (TGen n) = ts !! n | |
inst ts t = t | |
instance Instantiate a => Instantiate [a] where | |
inst ts = map (inst ts) | |
instance Instantiate t => Instantiate (Qual t) where | |
inst ts (ps :=> t) = inst ts ps :=> inst ts t | |
instance Instantiate Pred where | |
inst ts (IsIn c t) = IsIn c (inst ts t) | |
----------------------------------------------------------------------------- | |
-- TIMain: Type Inference Algorithm | |
----------------------------------------------------------------------------- | |
-- Infer: Basic definitions for type inference | |
----------------------------------------------------------------------------- | |
type Infer e t = ClassEnv -> [Assump] -> e -> TI ([Pred], t) | |
----------------------------------------------------------------------------- | |
-- Lit: Literals | |
----------------------------------------------------------------------------- | |
data Literal = LitInt Integer | |
| LitChar Char | |
| LitRat Rational | |
| LitStr String | |
tiLit :: Literal -> TI ([Pred],Type) | |
tiLit (LitChar _) = return ([], tChar) | |
tiLit (LitInt _) = do v <- newTVar Star | |
return ([IsIn "Num" v], v) | |
tiLit (LitStr _) = return ([], tString) | |
tiLit (LitRat _) = do v <- newTVar Star | |
return ([IsIn "Fractional" v], v) | |
----------------------------------------------------------------------------- | |
-- Pat: Patterns | |
----------------------------------------------------------------------------- | |
data Pat = PVar Id | |
| PWildcard | |
| PAs Id Pat | |
| PLit Literal | |
| PNpk Id Integer | |
| PCon Assump [Pat] | |
tiPat :: Pat -> TI ([Pred], [Assump], Type) | |
tiPat (PVar i) = do v <- newTVar Star | |
return ([], [i :>: toScheme v], v) | |
tiPat PWildcard = do v <- newTVar Star | |
return ([], [], v) | |
tiPat (PAs i pat) = do (ps, as, t) <- tiPat pat | |
return (ps, (i:>:toScheme t):as, t) | |
tiPat (PLit l) = do (ps, t) <- tiLit l | |
return (ps, [], t) | |
tiPat (PNpk i k) = do t <- newTVar Star | |
return ([IsIn "Integral" t], [i:>:toScheme t], t) | |
tiPat (PCon (i:>:sc) pats) = do (ps,as,ts) <- tiPats pats | |
t' <- newTVar Star | |
(qs :=> t) <- freshInst sc | |
unify t (foldr fn t' ts) | |
return (ps++qs, as, t') | |
tiPats :: [Pat] -> TI ([Pred], [Assump], [Type]) | |
tiPats pats = do psasts <- mapM tiPat pats | |
let ps = concat [ ps' | (ps',_,_) <- psasts ] | |
as = concat [ as' | (_,as',_) <- psasts ] | |
ts = [ t | (_,_,t) <- psasts ] | |
return (ps, as, ts) | |
----------------------------------------------------------------------------- | |
data Expr = Var Id | |
| Lit Literal | |
| Const Assump | |
| Ap Expr Expr | |
| Let BindGroup Expr | |
tiExpr :: Infer Expr Type | |
tiExpr ce as (Var i) = do sc <- find i as | |
(ps :=> t) <- freshInst sc | |
return (ps, t) | |
tiExpr ce as (Const (i:>:sc)) = do (ps :=> t) <- freshInst sc | |
return (ps, t) | |
tiExpr ce as (Lit l) = do (ps,t) <- tiLit l | |
return (ps, t) | |
tiExpr ce as (Ap e f) = do (ps,te) <- tiExpr ce as e | |
(qs,tf) <- tiExpr ce as f | |
t <- newTVar Star | |
unify (tf `fn` t) te | |
return (ps++qs, t) | |
tiExpr ce as (Let bg e) = do (ps, as') <- tiBindGroup ce as bg | |
(qs, t) <- tiExpr ce (as' ++ as) e | |
return (ps ++ qs, t) | |
----------------------------------------------------------------------------- | |
type Alt = ([Pat], Expr) | |
tiAlt :: Infer Alt Type | |
tiAlt ce as (pats, e) = do (ps, as', ts) <- tiPats pats | |
(qs,t) <- tiExpr ce (as'++as) e | |
return (ps++qs, foldr fn t ts) | |
tiAlts :: ClassEnv -> [Assump] -> [Alt] -> Type -> TI [Pred] | |
tiAlts ce as alts t = do psts <- mapM (tiAlt ce as) alts | |
mapM (unify t) (map snd psts) | |
return (concat (map fst psts)) | |
----------------------------------------------------------------------------- | |
split :: Monad m => ClassEnv -> [Tyvar] -> [Tyvar] -> [Pred] | |
-> m ([Pred], [Pred]) | |
split ce fs gs ps = do ps' <- reduce ce ps | |
let (ds, rs) = partition (all (`elem` fs) . tv) ps' | |
rs' <- defaultedPreds ce (fs++gs) rs | |
return (ds, rs \\ rs') | |
type Ambiguity = (Tyvar, [Pred]) | |
ambiguities :: ClassEnv -> [Tyvar] -> [Pred] -> [Ambiguity] | |
ambiguities ce vs ps = [ (v, filter (elem v . tv) ps) | v <- tv ps \\ vs ] | |
numClasses :: [Id] | |
numClasses = ["Num", "Integral", "Floating", "Fractional", | |
"Real", "RealFloat", "RealFrac"] | |
stdClasses :: [Id] | |
stdClasses = ["Eq", "Ord", "Show", "Read", "Bounded", "Enum", "Ix", | |
"Functor", "Monad", "MonadPlus"] ++ numClasses | |
candidates :: ClassEnv -> Ambiguity -> [Type] | |
candidates ce (v, qs) = [ t' | let is = [ i | IsIn i t <- qs ] | |
ts = [ t | IsIn i t <- qs ], | |
all ((TVar v)==) ts, | |
any (`elem` numClasses) is, | |
all (`elem` stdClasses) is, | |
t' <- defaults ce, | |
all (entail ce []) [ IsIn i t' | i <- is ] ] | |
withDefaults :: Monad m => ([Ambiguity] -> [Type] -> a) | |
-> ClassEnv -> [Tyvar] -> [Pred] -> m a | |
withDefaults f ce vs ps | |
| any null tss = fail "cannot resolve ambiguity" | |
| otherwise = return (f vps (map head tss)) | |
where vps = ambiguities ce vs ps | |
tss = map (candidates ce) vps | |
defaultedPreds :: Monad m => ClassEnv -> [Tyvar] -> [Pred] -> m [Pred] | |
defaultedPreds = withDefaults (\vps ts -> concat (map snd vps)) | |
defaultSubst :: Monad m => ClassEnv -> [Tyvar] -> [Pred] -> m Subst | |
defaultSubst = withDefaults (\vps ts -> zip (map fst vps) ts) | |
----------------------------------------------------------------------------- | |
type Expl = (Id, Scheme, [Alt]) | |
tiExpl :: ClassEnv -> [Assump] -> Expl -> TI [Pred] | |
tiExpl ce as (i, sc, alts) | |
= do (qs :=> t) <- freshInst sc | |
ps <- tiAlts ce as alts t | |
s <- getSubst | |
let qs' = apply s qs | |
t' = apply s t | |
fs = tv (apply s as) | |
gs = tv t' \\ fs | |
sc' = quantify gs (qs':=>t') | |
ps' = filter (not . entail ce qs') (apply s ps) | |
(ds,rs) <- split ce fs gs ps' | |
if sc /= sc' then | |
fail "signature too general" | |
else if not (null rs) then | |
fail "context too weak" | |
else | |
return ds | |
----------------------------------------------------------------------------- | |
type Impl = (Id, [Alt]) | |
restricted :: [Impl] -> Bool | |
restricted bs = any simple bs | |
where simple (i,alts) = any (null . fst) alts | |
tiImpls :: Infer [Impl] [Assump] | |
tiImpls ce as bs = do ts <- mapM (\_ -> newTVar Star) bs | |
let is = map fst bs | |
scs = map toScheme ts | |
as' = zipWith (:>:) is scs ++ as | |
altss = map snd bs | |
pss <- sequence (zipWith (tiAlts ce as') altss ts) | |
s <- getSubst | |
let ps' = apply s (concat pss) | |
ts' = apply s ts | |
fs = tv (apply s as) | |
vss = map tv ts' | |
gs = foldr1 union vss \\ fs | |
(ds,rs) <- split ce fs (foldr1 intersect vss) ps' | |
if restricted bs then | |
let gs' = gs \\ tv rs | |
scs' = map (quantify gs' . ([]:=>)) ts' | |
in return (ds++rs, zipWith (:>:) is scs') | |
else | |
let scs' = map (quantify gs . (rs:=>)) ts' | |
in return (ds, zipWith (:>:) is scs') | |
----------------------------------------------------------------------------- | |
type BindGroup = ([Expl], [[Impl]]) | |
tiBindGroup :: Infer BindGroup [Assump] | |
tiBindGroup ce as (es,iss) = | |
do let as' = [ v:>:sc | (v,sc,alts) <- es ] | |
(ps, as'') <- tiSeq tiImpls ce (as'++as) iss | |
qss <- mapM (tiExpl ce (as''++as'++as)) es | |
return (ps++concat qss, as''++as') | |
tiSeq :: Infer bg [Assump] -> Infer [bg] [Assump] | |
tiSeq ti ce as [] = return ([],[]) | |
tiSeq ti ce as (bs:bss) = do (ps,as') <- ti ce as bs | |
(qs,as'') <- tiSeq ti ce (as'++as) bss | |
return (ps++qs, as''++as') | |
----------------------------------------------------------------------------- | |
-- TIProg: Type Inference for Whole Programs | |
----------------------------------------------------------------------------- | |
type Program = [BindGroup] | |
tiProgram :: ClassEnv -> [Assump] -> Program -> [Assump] | |
tiProgram ce as bgs = runTI $ | |
do (ps, as') <- tiSeq tiBindGroup ce as bgs | |
s <- getSubst | |
rs <- reduce ce (apply s ps) | |
s' <- defaultSubst ce [] rs | |
return (apply (s'@@s) as') | |
----------------------------------------------------------------------------- |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment