-
Notifications
You must be signed in to change notification settings - Fork 139
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Signed-off-by: Sergei Trofimovich <slyfox@gentoo.org>
- Loading branch information
Sergei Trofimovich
committed
Dec 9, 2012
1 parent
97cd04f
commit f191742
Showing
2 changed files
with
216 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,211 @@ | ||
diff --git a/Infer.hs b/Infer.hs | ||
index a7e0cf0..03ef533 100644 | ||
--- a/Infer.hs | ||
+++ b/Infer.hs | ||
@@ -16,8 +16,7 @@ import qualified Data.Map as Map | ||
import Data.List(intersperse) | ||
import Data.IORef(newIORef,readIORef,writeIORef,IORef) | ||
import System.IO.Unsafe(unsafePerformIO) | ||
-import System.Time(getClockTime) | ||
-import System.Time(ClockTime) | ||
+import Data.Time(UTCTime) | ||
|
||
import PureReadline | ||
|
||
@@ -238,7 +237,7 @@ data TcEnv | ||
, rules :: FiniteMap String [RWrule] -- Proposition simplifying rules | ||
, refutations :: FiniteMap String Refutation | ||
, runtime_env :: Ev -- current value bindings | ||
- , imports :: [(String,ClockTime,[(String,ClockTime)],TcEnv)] -- already imported Modules | ||
+ , imports :: [(String,UTCTime,[(String,UTCTime)],TcEnv)] -- already imported Modules | ||
, tyfuns :: [(String,DefTree TcTv Tau)] | ||
, sourceFiles :: [String] | ||
, syntaxExt :: [SynExt String] | ||
diff --git a/RankN.hs b/RankN.hs | ||
index 5bd7ebe..f5e56ec 100644 | ||
--- a/RankN.hs | ||
+++ b/RankN.hs | ||
@@ -1118,6 +1118,7 @@ unify x y = | ||
f (TyEx x) (TyEx y) = unifyEx x y | ||
f s t = matchErr "\nDifferent types" s t | ||
|
||
+emit :: TyCh m => Tau -> Tau -> m () | ||
emit x y = | ||
do { a <- zonk x | ||
; let f (TcTv(tv@(Tv _ (Flexi _) _))) = | ||
@@ -1137,6 +1138,7 @@ emit x y = | ||
; f y} | ||
|
||
|
||
+unifyEx :: TyCh m => L ([Pred], Tau) -> L ([Pred], Tau) -> m () | ||
unifyEx x y = | ||
do { (tripsX,(eqn1,x1)) <- unwind x | ||
; (tripsY,(eqn2,y1)) <- unwind y | ||
@@ -1156,6 +1158,7 @@ unifyEx x y = | ||
|
||
predsEq xs ys = (all (`elem` xs) ys) && (all (`elem` ys) xs) | ||
|
||
+unifyVar :: TyCh m => TcTv -> Tau -> m () | ||
unifyVar (x@(Tv u1 r1 k1)) (t@(TcTv (Tv u2 r2 k2))) | u1==u2 = return () | ||
-- Always bind newer vars to older ones, this way | ||
-- makes the pretty printing work better | ||
@@ -1709,6 +1712,7 @@ kindOfM x = do { -- verbose <- getIoMode "verbose"; | ||
|
||
|
||
|
||
+matchKind :: TyCh m => Tau -> [Tau] -> m Tau | ||
matchKind (Karr a b) (t:ts) = | ||
do { k <- kindOfM t | ||
; unify a k | ||
@@ -2247,6 +2251,7 @@ toEqs env ((Rel' nm ts):xs) = | ||
; return((makeRel zs):ys) } | ||
|
||
|
||
+toRho :: TyCh m => TransEnv -> PT -> m Rho | ||
toRho env (Rarrow' x y) = | ||
do { (s,_) <- toSigma env x; r <- toRho env y; return(arrow s r)} | ||
toRho env (TyApp' (TyApp' (TyCon' "(,)" _) x) y) = | ||
@@ -2284,6 +2289,7 @@ readName mess ((x,tau,k):xs,loc,exts,levels) s = | ||
; instanLevel free tau } | ||
else readName mess (xs,loc,exts,levels) s | ||
|
||
+toTau :: TyCh m => TransEnv -> PT -> m Tau | ||
toTau env x = readTau 0 env x | ||
|
||
readTau :: TyCh m => Int -> TransEnv -> PT -> m Tau | ||
@@ -3174,11 +3180,13 @@ match2 env ((TySyn nm n fs as x,y):xs) = match2 env ((x,y):xs) | ||
match2 env ((y,TySyn nm n fs as x):xs) = match2 env ((y,x):xs) | ||
match2 env ((x,y):xs) = fail "No Match" | ||
|
||
+match2Var :: Monad m => ([(TcLv, Level)], [(TcTv, Tau)]) -> TcTv -> Tau -> [(Tau, Tau)] -> m Unifier2 | ||
match2Var (env@(ls,vs)) x tau xs = | ||
case find (\ (v,t) -> v==x) vs of | ||
Just (v,t) -> if t==tau then match2 env xs else fail "Duplicate" | ||
Nothing -> match2 (ls,(x,tau):vs) xs | ||
|
||
+matchLevel :: Monad m => Unifier2 -> Level -> Level -> [(Tau, Tau)] -> m Unifier2 | ||
matchLevel env LvZero LvZero xs = match2 env xs | ||
matchLevel env (LvSucc x) (LvSucc y) xs = matchLevel env x y xs | ||
matchLevel (env@(ls,vs)) (TcLv x) l xs = | ||
@@ -3533,6 +3541,7 @@ thread f sep d (x:xs) = (d2,y<>sep:ys) | ||
where (d1,y) = f d x | ||
(d2,ys) = thread f sep d1 xs | ||
|
||
+arrowTau :: NameStore d => d -> Tau -> (d, [Doc]) | ||
arrowTau d (TyApp (TyApp (TyCon sx _ "(->)" _) x) y) = (d3, (contra x doc <> text " -> "):docs) | ||
where (d2,doc) = dTau d x | ||
(d3,docs) = arrowTau d2 y | ||
@@ -3541,6 +3550,7 @@ arrowTau d (TyApp (TyApp (TyCon sx _ "(->)" _) x) y) = (d3, (contra x doc <> tex | ||
arrowTau d x = (d2,[doc]) | ||
where (d2,doc) = dTau d x | ||
|
||
+arrowRho :: NameStore d => d -> Rho -> (d, [Doc]) | ||
arrowRho d (Rarrow s r) = (d3,lhs : docs) | ||
where (d2,doc) = dSigma d s | ||
(d3,docs) = arrowRho d2 r | ||
@@ -3768,6 +3778,7 @@ exSynItemD d (t@(TyApp (TyCon ext _ c1 _) x)) | itemItem c1 ext | ||
where (d1,x') = dTau d x | ||
|
||
|
||
+dPar :: forall t. (NameStore t) => t -> Tau -> (t,Doc) | ||
dPar xs z@(TyApp (TyCon sx _ "[]" _) x) = dTau xs z | ||
dPar xs z@(TyApp (TyApp (TyCon sx _ "(,)" _) x) y) = dTau xs z | ||
dPar xs z@(TyApp (TyApp (TyCon sx _ "(+)" _) x) y) = dTau xs z | ||
@@ -3789,6 +3800,7 @@ dPar xs x@(TyEx _) = (ys, PP.parens ans) | ||
dPar xs x = dTau xs x | ||
|
||
|
||
+dArrow :: forall t. (NameStore t) => t -> Tau -> (t,Doc) | ||
dArrow xs (t@(TyApp (TyApp (TyCon sx _ "(->)" _) x) y)) = (ys, PP.parens z) | ||
where (ys,z) = dTau xs t | ||
dArrow xs (t@(Karr _ _)) = (ys, PP.parens z) | ||
@@ -3905,11 +3917,13 @@ toPT d (TyEx ys) = (dn,Forallx Ex vs preds body) | ||
(d2,preds) = toL toPPred d1 ps | ||
(dn,vs) = toL toTrip d2 args | ||
|
||
+toPPred :: NameStore t => t -> Pred -> (t, PPred) | ||
toPPred d (Equality x y) = (d2,Equality' a b) | ||
where (d1,a) = toPT d x | ||
(d2,b) = toPT d1 y | ||
toPPred d (Rel x) = (d1,Rel' "" a) where (d1,a) = toPT d x | ||
|
||
+toTrip :: NameStore t => t -> (Name, Kind, Quant) -> (t, (String, PT, Quant)) | ||
toTrip d (nm,MK k,q) = (d2,(s,a,q)) | ||
where (d1,s) = useStoreName nm (MK k) ("'"++) d | ||
(d2,a) = toPT d1 k | ||
@@ -4178,6 +4192,7 @@ emitStar pair (Right x) = Right x | ||
|
||
-- mguStarVar is only called from mguStar | ||
-- | ||
+mguStarVar :: TyCh m => (IO String, Loc) -> [TcTv] -> TcTv -> Tau -> [(Tau, Tau)] -> m (Either ([(TcTv, Tau)], [Pred]) (String, Tau, Tau)) | ||
mguStarVar str beta (x@(Tv n _ _)) (tau@(TyFun _ _ _)) xs | elem x (tvsTau tau) = | ||
do { norm <- normTyFun tau | ||
; case norm of | ||
diff --git a/SyntaxExt.hs b/SyntaxExt.hs | ||
index d52d73a..bc47c2f 100644 | ||
--- a/SyntaxExt.hs | ||
+++ b/SyntaxExt.hs | ||
@@ -335,7 +335,7 @@ buildExt loc (lift0,lift1,lift2,lift3) x ys = | ||
(Pairx (Left xs) _,Ix(tag,_,_,Just(Left pair),_,_,_,_)) -> return(buildTuple (flip $ lift2 pair) (reverse xs)) | ||
_ -> fail ("\nSyntax extension: "++extKey x++" doesn't match use, at "++loc)} | ||
|
||
-buildNat :: Num a => b -> (b -> b) -> a -> b | ||
+buildNat :: (Eq a, Num a) => b -> (b -> b) -> a -> b | ||
buildNat z s 0 = z | ||
buildNat z s n = s(buildNat z s (n-1)) | ||
|
||
diff --git a/Toplevel.hs b/Toplevel.hs | ||
index 4c3d16c..e6e79f4 100644 | ||
--- a/Toplevel.hs | ||
+++ b/Toplevel.hs | ||
@@ -34,9 +34,10 @@ import Commands | ||
import SyntaxExt(synName,synKey) | ||
|
||
import System.Environment(getArgs) | ||
-import System.Time(ClockTime,getClockTime) | ||
+import Data.Time(UTCTime,getCurrentTime) | ||
import System.IO(hClose) | ||
-import System.IO.Error(try,ioeGetErrorString) | ||
+import qualified System.IO.Error as E (ioeGetErrorString) | ||
+import qualified Control.Exception as E (try, IOException) | ||
import System.FilePath(splitFileName) | ||
import System.Directory(setCurrentDirectory,getDirectoryContents,getModificationTime) | ||
|
||
@@ -180,7 +181,7 @@ display ss = plistf id "(" ss " " ")" | ||
|
||
parseDecs :: String -> FIO [Dec] | ||
parseDecs file = | ||
- do { hndl <- eitherM (fio (try(openFile file ReadMode))) | ||
+ do { hndl <- eitherM (fio ((E.try :: IO a -> IO (Either E.IOException a)) (openFile file ReadMode))) | ||
(\ err -> fail ("\nProblem opening file: "++file)) | ||
return | ||
; let err mess = fio((hClose hndl) >> fail mess) | ||
@@ -213,9 +214,9 @@ importName (Import s vs) = s | ||
indent n = replicate ((n-1)*3) ' ' | ||
nameOf (name,time,deps,env) = name | ||
|
||
-elabFile :: Int -> String -> TcEnv -> FIO(TcEnv,ClockTime) | ||
+elabFile :: Int -> String -> TcEnv -> FIO(TcEnv,UTCTime) | ||
elabFile count file (tenv) = | ||
- do { time <- fio getClockTime | ||
+ do { time <- fio getCurrentTime | ||
; all <- parseDecs file | ||
; let (importL,ds) = partition importP all | ||
(dss,pairs) = topSortR freeOfDec ds | ||
@@ -253,14 +254,14 @@ lookupDeps nm env = case find match (imports env) of | ||
|
||
showimp message env = message++plistf nameOf "(" (imports env) "," ")." | ||
|
||
-importManyFiles:: Int -> [Dec] -> TcEnv -> FIO (TcEnv, [(String, ClockTime)]) | ||
+importManyFiles:: Int -> [Dec] -> TcEnv -> FIO (TcEnv, [(String, UTCTime)]) | ||
importManyFiles count [] tenv = return (tenv,[]) | ||
importManyFiles count (d:ds) tenv = | ||
do { (next,name,time) <- importFile count d tenv | ||
; (next2,ts) <- importManyFiles count ds next | ||
; return(next2,(name,time):ts) } | ||
|
||
-importFile :: Int -> Dec -> TcEnv -> FIO(TcEnv,String,ClockTime) | ||
+importFile :: Int -> Dec -> TcEnv -> FIO(TcEnv,String,UTCTime) | ||
importFile count (Import name vs) tenv = | ||
case find (\(nm,time,deps,env)->name==nm) (imports tenv) of | ||
Just (nm,time,deps,env) -> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters