Skip to content
Browse files

Another unification fix

Ignore-this: c15a15a00d9ed5618e4c44f2c4731272

darcs-hash:20090810121841-228f4-2a1ab82df621fec172460f96bc85a338d3a24ffd.gz
  • Loading branch information...
1 parent a4e1e86 commit bf0effd48d98f096f33d740f7357feb88ddc2a28 eb committed Aug 10, 2009
Showing with 9 additions and 2 deletions.
  1. +1 −0 Ivor/TTCore.lhs
  2. +4 −2 Ivor/Typecheck.lhs
  3. +4 −0 Ivor/Unify.lhs
View
1 Ivor/TTCore.lhs
@@ -742,6 +742,7 @@ Apply a function to a list of arguments
> fPrec _ (RInfer) = "_"
> fPrec _ (RMeta n) = "?"++forget n
> fPrec p (RFileLoc f l t) = fPrec p t
+> fPrec p (RAnnot s) = "[" ++ s ++ "]"
> bracket outer inner str | inner>outer = "("++str++")"
> | otherwise = str
View
6 Ivor/Typecheck.lhs
@@ -130,14 +130,16 @@ Handy to pass through all the variables, for tracing purposes when debugging.
> mkSubst' acc' xs all
>
> eqn (ok, (env, x, y, fc)) = if ok then (x,y,fc) else (x,y,Nothing)
+> showeqn all = concat $ map ((++"\n").show.eqn) all
> mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,fc)) all
> = do -- (s',nms) <- mkSubst xs
> let x' = papp s' x
> let (Ind y') = normalise gam (Ind (papp s' y))
> uns <- case unifyenvErr ok gam env (Ind y') (Ind x') of
-> Right x' -> return x'
-> Left err -> ifail (errCtxt fc (ICantUnify (Ind y') (Ind x')))
+> Right uns -> {- trace (show (y', x', uns)) $ -} return uns
+> Left err -> {- trace (showeqn all) $ -}
+> ifail (errCtxt fc (ICantUnify (Ind y') (Ind x')))
Failure err -> fail $ err ++"\n" ++ show nms ++"\n" ++ show constraints -- $ -} ++ " Can't convert "++show x'++" and "++show y' ++ "\n" ++ show constraints ++ "\n" ++ show nms
View
4 Ivor/Unify.lhs
@@ -87,6 +87,10 @@ Collect names which do unify, and ignore errors
> un envl envr (Bind x b (Sc sc)) (Bind x' b' (Sc sc')) acc =
> do acc' <- unb envl envr b b' acc
> un ((x,b):envl) ((x',b'):envr) sc sc' acc'
+> un envl envr (Bind x b@(B (Let v) ty) (Sc sc)) t acc
+> = un ((x,b):envl) envr sc t acc
+> un envl envr t (Bind x b@(B (Let v) ty) (Sc sc)) acc
+> = un envl ((x,b):envr) t sc acc
> -- combine bu scu
> -- if unifying the functions fails because the names are different,
> -- unifying the arguments is going to be a waste of time bec

0 comments on commit bf0effd

Please sign in to comment.
Something went wrong with that request. Please try again.