@@ -486,7 +486,7 @@ intTyName (ITFixed sized) = "B" ++ show (nativeTyWidth sized)
486intTyName (ITChar) = "Char"
486intTyName (ITChar) = "Char"
487intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show count
487intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show count
489−data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors
489+data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors https://github.com/idris-lang/Idris-dev/issues/1723
490 deriving (Show, Eq, Ord)
490 deriving (Show, Eq, Ord)
492deriving instance NFData IntTy
492deriving instance NFData IntTy
@@ -792,7 +792,7 @@ instance TermSize (TT Name) where
792 | otherwise = 1
792 | otherwise = 1
793 termsize n (V _) = 1
793 termsize n (V _) = 1
794 -- for `Bind` terms, we can erroneously declare a term
794 -- for `Bind` terms, we can erroneously declare a term
795− -- "recursive => really big" if the name of the bound
795+ -- "recursive => really big" if the name of the bound
796 -- variable is the same as the name we're using
796 -- variable is the same as the name we're using
797 -- So generate a different name in that case.
797 -- So generate a different name in that case.
798 termsize n (Bind n' (Let t v) sc)
798 termsize n (Bind n' (Let t v) sc)
@@ -971,19 +971,19 @@ subst n v tm = fst $ subst' 0 tm
971 subst' i t@(Bind x b sc) | x /= n
971 subst' i t@(Bind x b sc) | x /= n
972 = let (b', ub) = substB' i b
972 = let (b', ub) = substB' i b
973 (sc', usc) = subst' (i+1) sc in
973 (sc', usc) = subst' (i+1) sc in
974− if ub || usc then (Bind x b' sc', True) else (t, False)
974+ if ub || usc then (Bind x b' sc', True) else (t, False)
975− subst' i t@(App f a) = let (f', uf) = subst' i f
975+ subst' i t@(App f a) = let (f', uf) = subst' i f
976 (a', ua) = subst' i a in
976 (a', ua) = subst' i a in
977 if uf || ua then (App f' a', True) else (t, False)
977 if uf || ua then (App f' a', True) else (t, False)
978 subst' i t@(Proj x idx) = let (x', u) = subst' i x in
978 subst' i t@(Proj x idx) = let (x', u) = subst' i x in
979 if u then (Proj x' idx, u) else (t, False)
979 if u then (Proj x' idx, u) else (t, False)
980 subst' i t = (t, False)
980 subst' i t = (t, False)
982− substB' i b@(Let t v) = let (t', ut) = subst' i t
982+ substB' i b@(Let t v) = let (t', ut) = subst' i t
983 (v', uv) = subst' i v in
983 (v', uv) = subst' i v in
984 if ut || uv then (Let t' v', True)
984 if ut || uv then (Let t' v', True)
985 else (b, False)
985 else (b, False)
986− substB' i b@(Guess t v) = let (t', ut) = subst' i t
986+ substB' i b@(Guess t v) = let (t', ut) = subst' i t
987 (v', uv) = subst' i v in
987 (v', uv) = subst' i v in
988 if ut || uv then (Guess t' v', True)
988 if ut || uv then (Guess t' v', True)
989 else (b, False)
989 else (b, False)
@@ -1090,7 +1090,7 @@ unList tm = case unApply tm of
1090-- Bruijn indices.
1090-- Bruijn indices.
1091forget :: TT Name -> Raw
1091forget :: TT Name -> Raw
1092forget tm = forgetEnv [] tm
1092forget tm = forgetEnv [] tm
1094forgetEnv :: [Name] -> TT Name -> Raw
1094forgetEnv :: [Name] -> TT Name -> Raw
1095forgetEnv env (P _ n _) = Var n
1095forgetEnv env (P _ n _) = Var n
1096forgetEnv env (V i) = Var (env !! i)
1096forgetEnv env (V i) = Var (env !! i)
@@ -1384,7 +1384,7 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in
1384 orderPats $ bindPats (reverse ps) tm'
1384 orderPats $ bindPats (reverse ps) tm'
1386 bindPats [] tm = tm
1386 bindPats [] tm = tm
1387− bindPats ((n, t):ps) tm
1387+ bindPats ((n, t):ps) tm
1388 | n `notElem` map fst ps = Bind n (PVar t) (bindPats ps tm)
1388 | n `notElem` map fst ps = Bind n (PVar t) (bindPats ps tm)
1389 | otherwise = bindPats ps tm
1389 | otherwise = bindPats ps tm