[fixed README, removed some unnecessary files stefanh@cse.unsw.edu.au**20050525055239] { hunk ./Main.hs 31 -import TyInfer -import TyCheck ---import Eval hunk ./README 14 +You need autoreconf, (GNU) make, m4, ghc 6.4, alex and happy. + +In the toplevel directory execute: + hunk ./README 21 -Edit config.mk for your environment, then type - "make" +If necessary: edit config.mk for your environment. + + make hunk ./README 25 - "make clean" - "make distclean" - -Should work with GNU make. + make clean + make distclean hunk ./README 34 + + +Using ghci: + +PHRaC uses the m4 preprocessor the provide filename/linenumber information +in debug messages. The script `ghci' in the toplevel directory is a wrapper +which calls the real ghci with the right commandline arguments for invoking +the preprocessor. hunk ./README 46 + +PHRaC was developed with GHC 6.4 under Linux x86. Should work an other +platforms as well. hunk ./README 50 -PHRaC was developed with GHC 6.4 under Linux x86. hunk ./TypeInference.hs.old 1 -module TypeInference where - -import Control.Monad.State -import Control.Monad.Error -import qualified Map -import qualified Data.Set as Set -import List (partition, intersperse) - -import qualified Builtins -import UniqIdents ( builtinTypeId ) -import Builtins -import AbstractSyntax -import Substitution -import Error -import Pretty -import Symtab -import Unification hiding (unify) -import Entailment ( entail, split, reduce ) -import Kinds - -type Assumps = Map.Map ValId TypeScheme - -emptyAssumps = Map.empty - -find :: ValId -> Assumps -> TypeScheme -find i as = case Map.lookup i as of - Just t -> t - Nothing -> panic ("variable `" ++ showPpr i ++ - "' not found in assumptions") - -add :: ValId -> TypeScheme -> Assumps -> Assumps -add i t as = Map.insert i t as - -merge :: Assumps -> Assumps -> Assumps -merge as as' = - if not (Set.null $ Map.keysSet as `Set.intersection` Map.keysSet as') - then panic ("cannot merge assumptions, they have at most one key " ++ - "in common:\n\nAssumptions 1:\n" ++ dumpAssumps as ++ - "\n\nAssumptions 2:\n" ++ dumpAssumps as') - else Map.union as as' - -buildAssumps :: [ValId] -> [TypeScheme] -> Assumps -buildAssumps is ts = Map.fromList (zip is ts) - -dumpAssumps :: Assumps -> String -dumpAssumps as = - "{Assumptions: " ++ - showCommaListed (map (\ (k,v) -> ppr k <+> text "=" <+> ppr v) - (Map.assocs as)) - ++ "}" - - -tiDebug :: Location -> String -> ([ClassConstraint], [EqConstraint]) - -> Type -> TI () -tiDebug loc str constrs t = - do s <- gets ti_subst - let (cs, es) = applySubst s constrs - t' = applySubst s t - msg = "TypeInference, " ++ str ++ ": " ++ dumpClassConstraints cs ++ - ", " ++ dumpEqConstraints es ++ ", type = " ++ showPpr t - debug_ loc msg - -data TIState = TIState { ti_subst :: TypeSubst } - -emptyTIState = TIState { ti_subst = nullSubst } - -type TI = StateT TIState ST - -liftST :: ST a -> TI a -liftST x = lift x - -runTI :: TI a -> ST a -runTI ti = evalStateT ti emptyTIState - -unify :: [EqConstraint] -> Type -> Type -> TI [EqConstraint] -unify eqc t1 t2 = - do s <- gets ti_subst - eqEnv <- liftST getEqEnv - let eq = (applySubst s t1) :=: (applySubst s t2) - eqs = map toTypeEq (applySubst s eqc) - ures <- liftST $ runUnify eqEnv (eq : eqs) - case ures of - Left err -> phasefail err - Right (eqc', s') -> - let newSubst = s' `composeSubst` s - in do modify (\state -> state { ti_subst = newSubst }) - return eqc' - where toTypeEq (EqConstraint l r) = TyAssoc l :=: r - - -type Infer e t = Assumps -> e -> TI ([Constraint], t) - -tiExpr :: Infer Exp Type -tiExpr as (Var i) = - do let sc = find i as - (ps, t) <- freshInst sc - return (splitConstraints ps, t) - -tiExpr as (Num _) = return $ (([], []), TyConstruct intTypeId) - -tiExpr as (Prim op es) = - do l <- mapM (tiExpr as) es - alpha <- liftST $ freshTypeVar KindStar - let (constrs, operandTypes) = unzip l - opTy = typeOfPrimOp op - resTy = tyFuns operandTypes alpha - unify [] opTy resTy - return (unzipConstraints constrs, alpha) - -tiExpr as (App e1 e2) = - do ((theta1, u1), tau1) <- tiExpr as e1 - ((theta2, u2), tau2) <- tiExpr as e2 - alpha <- liftST $ freshTypeVar KindStar - u <- unify (u1 ++ u2) tau1 (tau2 `tyFun` alpha) - return ((theta1 ++ theta2, u), alpha) - --- \x1 .. xN -> e is rewritten as \x1 -> .. \xN -> e -tiExpr as (Lam [] e) = tiExpr as e -tiExpr as (Lam (x:xs) e) = - do alpha <- liftST $ freshTypeVar KindStar - (ps, tau) <- tiExpr (add x (toScheme alpha) as) (Lam xs e) - return (ps, alpha `tyFun` tau) - -tiExpr as (Letrec binds e) = - do ((ps, psEq), as') <- tiBindGroup as binds - ((qs, qsEq), t) <- tiExpr (as' `merge` as) e - return ((ps ++ qs, psEq ++ qsEq), t) - -tiExpr as e = - do panic ("tiExpr for " ++ showPpr' e ++ " not yet implemented") - --- the Bind type here corresponds to the Alt type in THIH -type Bind = ([ValId] {- arguments -} , Exp) - -tiBind :: Infer Bind Type -tiBind as (is, e) = - do alphas <- mapM (\_ -> liftST $ freshTypeVar KindStar) is - let ts = map toScheme alphas - as' = buildAssumps is ts - (qs, t) <- tiExpr (as' `merge` as) e - let resTy = tyFuns alphas t - return (qs, resTy) - - -subsumes :: TypeScheme -> TypeScheme -> TI Bool -subsumes sc1@(TypeScheme quants1 qt1) sc2@(TypeScheme quants2 qt2) = - do debug $ "checking if " ++ showPpr' sc1 ++ " subsumes " ++ showPpr' sc2 - kinds <- liftST $ mapM kindOf quants2 - tycons <- liftST $ mapM freshTyConstruct kinds - let subst = substFromAssocs (zip quants2 tycons) - -- instantiate qt2 with the fresh type constructors - qt2' = applySubst subst qt2 - (pi2', tau2') = splitQType qt2' - -- empty EqScheme is because quantified variables were replaced - -- by fresh type constructors - pi2Eqs = map (EqScheme []) (eqConstraints pi2') - (pi1, tau1) = splitQType qt1 - eqEnv <- liftST getEqEnv - ures <- liftST $ runUnify (eqEnv ++ pi2Eqs) [tau1 :=: tau2'] - case ures of - Left _ -> - do debug "Subsumption check failed because unification failed" - return False - Right (peqs, subst) -> - if not (null peqs) - then do debug "Subsumption failed because unification returned \ - \non-empty pending equalities" - return False - else do let pi1' = applySubst subst pi1 - xs <- liftST $ mapM (entail pi2') pi1' - if and xs - then do debug "Subsumption succeeded" - return True - else do debug "Subsumption failed because entailment \ - \failed" - return False - - -type Expl = (ValId, TypeScheme, Bind) - --- returns the deferred constraints -tiExpl :: Assumps -> Expl -> TI ([ClassConstraint], [EqConstraint]) -tiExpl as (i, sc, bind) = - do debug ("typing explicitly type binding " ++ showPpr' i ++ "\n") - (ps, t) <- tiBind as bind -- infered type - s <- gets ti_subst - let t' = applySubst s t - ps' = mergeConstraints $ applySubst s ps - fs = freeTypeVars (applySubst s as) - -- we must simplify the infered constraints by filtering out those - -- constraints which contain only fixed variables (i.e. variables - -- appearing in the assumptions). Such contraints are deferred - -- to the enclosing bindings. - (ds, ps'') = partition (all (`Set.member` fs) . freeTypeVarsList) ps' - gs = (freeTypeVars ps'' `Set.union` freeTypeVars t') - `Set.difference` fs - sc' = TypeScheme (Set.toList gs) - (if null ps' then UnconstrainedType t' - else ConstrainedType ps'' t') - debug ("type infered for " ++ showPpr' i ++ ": " ++ showPpr sc' ++ - ", new checking for subsumption\n--------") - b <- subsumes sc' sc - if not b - then phasefail ("type error while checking explicitly typed binding " - ++ showPpr' i ++ "\n infered signature: " - ++ showPpr sc' ++ "\n user-supplied signature: " - ++ showPpr sc) - else do debug ("Finished typing explicitly typed binding " ++ - showPpr' i ++ " deferred constraints: " ++ - showCommaListed ds ++ "\n\n" ++ showTypeSig (i,sc) - ++ "\n\n") - return (splitConstraints ds) - - -type Impl = (ValId, Bind) - --- returns the deferred constraints and the types for the bindings -tiImpls :: Infer [Impl] Assumps -tiImpls as bs = - do let is = map fst bs - debug ("typing implicitly typed bindings " ++ showCommaListed is) - -- type for every bindind - ts <- liftST $ mapM (\_ -> freshTypeVar KindStar) bs - let scs = map toScheme ts - as' = as `merge` buildAssumps is scs - l <- mapM (tiBind as') (map snd bs) - let (constrs, types) = unzip l - ps = mergeConstraints (unzipConstraints constrs) - mapM (uncurry $ unify []) (zip ts types) - s <- gets ti_subst - let ps' = applySubst s ps - ts' = applySubst s ts - fs = freeTypeVars (applySubst s as) - vss = map freeTypeVars ts' - gs = Set.unions vss `Set.difference` fs - debug ("monotypes for implicitly type bindings: " ++ - showCommaListed (map (\ (i, t) -> ppr i <+> text " :: " <+> - ppr t) (zip is ts')) ++ - ", constraints: " ++ showCommaListed ps') - (ds, rs) <- liftST $ split (Set.toList fs) - (Set.toList $ foldr1 Set.intersection vss) - ps' - (constrs, scs') <- - if restricted bs - then - let gs' = gs `Set.difference` (freeTypeVars rs) - scs'' = map (\t -> TypeScheme (Set.toList gs') - (UnconstrainedType t)) ts' - in do debug ("The monomorphism restriction applies") - return (ds ++ rs, scs'') - else - let scs'' = map (\t -> TypeScheme (Set.toList gs) - (ConstrainedType rs t)) ts' - in do debug ("The monomorphism restriction does not apply") - return (ds, scs'') - let resAssumps = buildAssumps is scs' - debug ("finished typing implicitly typed bindings, deferred " ++ - "constraints: " ++ showCommaListed constrs ++ "\n\n" ++ - (showTypeSigs (Map.assocs resAssumps)) ++ "\n\n") - return (splitConstraints constrs, resAssumps) - where - restricted :: [Impl] -> Bool - restricted bs = - let simple (i, b) = null (fst b) - in any simple bs - -{- -tiImpls :: Infer [Impl] Assumps -tiImpls as bs = - let groups = getBindGroups bs fst getDeps - in do - where - getDeps (id, (args, e) = [] -- FIXME - - -tiImplsSeq :: Infer [[Impl]] Assumps -tiImplsSeq as [] = return (([], []), emptyAssumps) -tiImplsSeq as (bs:bss) = - do (ps, as') <- tiImpls as bs - (qs, as'') <- tiSeq (as' `merge` as) bss - return - -} -tiBindGroup :: Infer [ValBind] Assumps -tiBindGroup as binds = - do let ids = map vbind_name binds - debug ("typing binding group " ++ showCommaListed ids ++ - " under the assumption " ++ dumpAssumps as) - let (as', expls, impls) = collect emptyAssumps binds - debug ("assumptions resulting from explicitly typed bindings: " ++ - dumpAssumps as') - (ps, as'') <- tiImpls (as' `merge` as) impls - debug ("assumptions obtained by typing the implicitly typed bindings: " - ++ dumpAssumps as'' ++ ", constraints: " ++ - showCommaListed (mergeConstraints ps)) - qss <- mapM (tiExpl (as'' `merge` as' `merge` as)) expls - let resConstrs = let (q1, q2) = unzipConstraints qss - (p1, p2) = ps - in (q1 ++ p1, q2 ++ p2) - resAssumps = as'' `merge` as' - mapM checkForAmbiguity (Map.assocs resAssumps) - debug ("finished typing binding group " ++ showCommaListed ids ++ - ", resulting assumptions: " ++ dumpAssumps resAssumps ++ - ", resulting constraints: " - ++ showCommaListed (mergeConstraints resConstrs)) - return (resConstrs, resAssumps) - where - collect as [] = (as, [], []) - collect as (ValBind id Nothing params e : rest) = - let (as', expls, impls) = collect as rest - in (as', expls, (id, (params, e)) : impls) - collect as (ValBind id (Just t) params e : rest) = - let (as', expls, impls) = collect as rest - in (add id t as', (id, t, (params, e)) : expls, impls) - checkForAmbiguity :: (ValId, TypeScheme) -> TI () - checkForAmbiguity (id, sc@(TypeScheme alphas rho)) = - let fv_rho = freeTypeVars rho - fixv_rho = fixedTypeVars rho - in if not ((Set.fromList alphas `Set.intersection` fv_rho) - `Set.isSubsetOf` fixv_rho) - then phasefail ("ambiguous signature for " ++ showPpr' id - ++ ": " ++ showPpr sc) - else return () - - -tiMain :: Program -> ST Assumps -tiMain (Program _ _ _ valBinds) = - do debug "\n\n ==> STARTING TYPE INFERENCE <== \n\n" - ((cs,es), as) <- runTI $ ti emptyAssumps valBinds - if not (null cs) || not (null es) - then panic ("Non-empty set of constraints after type inference:\n" ++ - dumpAssumps as ++ "\n" ++ dumpClassConstraints cs ++ - "\n" ++ dumpEqConstraints es) - else return as - where ti as binds = - do (ctx, as') <- tiBindGroup as binds - s <- gets ti_subst - return (applySubst s ctx, applySubst s as') - --- --- Helpers --- - -unzipConstraints :: [([ClassConstraint], [EqConstraint])] - -> ([ClassConstraint], [EqConstraint]) -unzipConstraints l = - let (css, ess) = unzip l - cs = concat css - es = concat ess - in (cs, es) - -freshInst :: TypeScheme -> TI ([Constraint], Type) -freshInst sc = - let quants = tyscheme_quants sc - (constrs, ty) = case tyscheme_qtype sc of - UnconstrainedType t -> ([], t) - ConstrainedType cs t -> (cs, t) - in do ((constrs', ty'), _) <- liftST $ instantiate quants (constrs, ty) - return (constrs', ty') - -toScheme :: Type -> TypeScheme -toScheme t = TypeScheme [] (UnconstrainedType t) - -funTypeId = builtinTypeId Builtins.funTypeConstructor -intTypeId = builtinTypeId Builtins.intTypeConstructor -boolTypeId = builtinTypeId Builtins.boolTypeConstructor - -intType = TyConstruct intTypeId -boolType = TyConstruct boolTypeId - -tyFun :: Type -> Type -> Type -tyFun t1 t2 = ((TyConstruct funTypeId) `TyApp` t1) `TyApp` t2 - -tyFuns :: [Type] -> Type -> Type -tyFuns [] t = t -tyFuns (t:ts) t2 = tyFun t (tyFuns ts t2) - -binIntTy = tyFuns [intType, intType] intType -binCmpTy = tyFuns [intType, intType] boolType - -typeOfPrimOp :: Builtins.Op -> Type -typeOfPrimOp Builtins.IntAddOp = binIntTy -typeOfPrimOp Builtins.IntSubOp = binIntTy -typeOfPrimOp Builtins.IntMulOp = binIntTy -typeOfPrimOp Builtins.IntQuotOp = binIntTy -typeOfPrimOp Builtins.IntRemOp = binIntTy -typeOfPrimOp Builtins.IntNegOp = tyFun intType intType -typeOfPrimOp Builtins.IntGtOp = binCmpTy -typeOfPrimOp Builtins.IntGeOp = binCmpTy -typeOfPrimOp Builtins.IntLtOp = binCmpTy -typeOfPrimOp Builtins.IntLeOp = binCmpTy -typeOfPrimOp Builtins.IntEqOp = binCmpTy -typeOfPrimOp Builtins.IntNeOp = binCmpTy - -dumpTypeInference :: Assumps -> Program -> String -dumpTypeInference as (Program _ classes _ binds) = - let methods = concatMap dumpMethods classes - values = map dumpValue binds - in concat (intersperse "\n" $ methods ++ values) - where - dumpMethods :: ClassDec -> [String] - dumpMethods cd = [] -- FIXME map dump (class_tsigs cd) - dumpValue :: ValBind -> String - dumpValue vb = dump (vbind_name vb) - dump i = showTypeSig (i, (find i as)) - -showTypeSig (i, sc) = showPpr i ++ " :: " ++ showPpr sc - -showTypeSigs l = concat (intersperse "\n" $ map showTypeSig l) + rmfile ./TypeInference.hs.old }