@@ -808,6 +808,11 @@ instance Eq NameType where
808 TCon _ a == TCon _ b = (a == b) -- ignore tag
808 TCon _ a == TCon _ b = (a == b) -- ignore tag
809 _ == _ = False
809 _ == _ = False
811+data AppStatus n = Complete
814+ deriving (Eq, Ord, Functor, Data, Typeable, Show)
811-- | Terms in the core language. The type parameter is the type of
816-- | Terms in the core language. The type parameter is the type of
812-- identifiers used for bindings and explicit named references;
817-- identifiers used for bindings and explicit named references;
813-- usually we use @TT 'Name'@.
818-- usually we use @TT 'Name'@.
@@ -816,7 +821,7 @@ data TT n = P NameType n (TT n) -- ^ named references with type
816 -- Pure Type Systems Formalized)
821 -- Pure Type Systems Formalized)
817 | V !Int -- ^ a resolved de Bruijn-indexed variable
822 | V !Int -- ^ a resolved de Bruijn-indexed variable
818 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
823 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
819− | App !(TT n) (TT n) -- ^ function, function type, arg
824+ | App (AppStatus n) !(TT n) (TT n) -- ^ function, function type, arg
820 | Constant Const -- ^ constant
825 | Constant Const -- ^ constant
821 | Proj (TT n) !Int -- ^ argument projection; runtime only
826 | Proj (TT n) !Int -- ^ argument projection; runtime only
822 -- (-1) is a special case for 'subtract one from BI'
827 -- (-1) is a special case for 'subtract one from BI'
@@ -852,7 +857,7 @@ instance TermSize (TT Name) where
852 termsize n (Bind n' b sc)
857 termsize n (Bind n' b sc)
853 = let rn = if n == n' then sMN 0 "noname" else n in
858 = let rn = if n == n' then sMN 0 "noname" else n in
854 termsize rn sc
859 termsize rn sc
855− termsize n (App f a) = termsize n f + termsize n a
860+ termsize n (App _ f a) = termsize n f + termsize n a
856 termsize n (Proj t i) = termsize n t
861 termsize n (Proj t i) = termsize n t
857 termsize n _ = 1
862 termsize n _ = 1
@@ -860,7 +865,7 @@ instance Sized a => Sized (TT a) where
860 size (P name n trm) = 1 + size name + size n + size trm
865 size (P name n trm) = 1 + size name + size n + size trm
861 size (V v) = 1
866 size (V v) = 1
862 size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy
867 size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy
863− size (App l r) = 1 + size l + size r
868+ size (App _ l r) = 1 + size l + size r
864 size (Constant c) = size c
869 size (Constant c) = size c
865 size Erased = 1
870 size Erased = 1
866 size (TType u) = 1 + size u
871 size (TType u) = 1 + size u
@@ -881,8 +886,8 @@ instance Eq n => Eq (TT n) where
881 (==) (P xt x _) (P yt y _) = x == y
886 (==) (P xt x _) (P yt y _) = x == y
882 (==) (V x) (V y) = x == y
887 (==) (V x) (V y) = x == y
883 (==) (Bind _ xb xs) (Bind _ yb ys) = xs == ys && xb == yb
888 (==) (Bind _ xb xs) (Bind _ yb ys) = xs == ys && xb == yb
884− (==) (App fx ax) (App fy ay) = ax == ay && fx == fy
889+ (==) (App _ fx ax) (App _ fy ay) = ax == ay && fx == fy
885− (==) (TType _) (TType _) = True -- deal with constraints later
890+ (==) (TType _) (TType _) = True -- deal with constraints later
886 (==) (Constant x) (Constant y) = x == y
891 (==) (Constant x) (Constant y) = x == y
887 (==) (Proj x i) (Proj y j) = x == y && i == j
892 (==) (Proj x i) (Proj y j) = x == y && i == j
888 (==) Erased _ = True
893 (==) Erased _ = True
@@ -898,15 +903,15 @@ isInjective :: TT n -> Bool
898isInjective (P (DCon _ _ _) _ _) = True
903isInjective (P (DCon _ _ _) _ _) = True
899isInjective (P (TCon _ _) _ _) = True
904isInjective (P (TCon _ _) _ _) = True
900isInjective (Constant _) = True
905isInjective (Constant _) = True
901−isInjective (TType x) = True
906+isInjective (TType x) = True
902isInjective (Bind _ (Pi _ _ _) sc) = True
907isInjective (Bind _ (Pi _ _ _) sc) = True
903−isInjective (App f a) = isInjective f
908+isInjective (App _ f a) = isInjective f
904isInjective _ = False
909isInjective _ = False
906-- | Count the number of instances of a de Bruijn index in a term
911-- | Count the number of instances of a de Bruijn index in a term
907vinstances :: Int -> TT n -> Int
912vinstances :: Int -> TT n -> Int
908vinstances i (V x) | i == x = 1
913vinstances i (V x) | i == x = 1
909−vinstances i (App f a) = vinstances i f + vinstances i a
914+vinstances i (App _ f a) = vinstances i f + vinstances i a
910vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc
915vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc
911 where instancesB (Let t v) = vinstances i v
916 where instancesB (Let t v) = vinstances i v
912 instancesB _ = 0
917 instancesB _ = 0
@@ -918,7 +923,7 @@ instantiate e = subst 0 where
918 subst i (P nt x ty) = P nt x (subst i ty)
923 subst i (P nt x ty) = P nt x (subst i ty)
919 subst i (V x) | i == x = e
924 subst i (V x) | i == x = e
920 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)
925 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)
921− subst i (App f a) = App (subst i f) (subst i a)
926+ subst i (App s f a) = App s (subst i f) (subst i a)
922 subst i (Proj x idx) = Proj (subst i x) idx
927 subst i (Proj x idx) = Proj (subst i x) idx
923 subst i t = t
928 subst i t = t
@@ -931,7 +936,7 @@ substV x tm = dropV 0 (instantiate x tm) where
931 dropV i (V x) | x > i = V (x - 1)
936 dropV i (V x) | x > i = V (x - 1)
932 | otherwise = V x
937 | otherwise = V x
933 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)
938 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)
934− dropV i (App f a) = App (dropV i f) (dropV i a)
939+ dropV i (App s f a) = App s (dropV i f) (dropV i a)
935 dropV i (Proj x idx) = Proj (dropV i x) idx
940 dropV i (Proj x idx) = Proj (dropV i x) idx
936 dropV i t = t
941 dropV i t = t
@@ -942,7 +947,7 @@ explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
942 Bind x b'
947 Bind x b'
943 (explicitNames (instantiate
948 (explicitNames (instantiate
944 (P Bound x (binderTy b')) sc))
949 (P Bound x (binderTy b')) sc))
945−explicitNames (App f a) = App (explicitNames f) (explicitNames a)
950+explicitNames (App s f a) = App s (explicitNames f) (explicitNames a)
946explicitNames (Proj x idx) = Proj (explicitNames x) idx
951explicitNames (Proj x idx) = Proj (explicitNames x) idx
947explicitNames t = t
952explicitNames t = t
@@ -956,7 +961,7 @@ pToV' n i (Bind x b sc)
956-- resolve names from the *outer* scope which may happen to have the same id.
961-- resolve names from the *outer* scope which may happen to have the same id.
957 | n == x = Bind x (fmap (pToV' n i) b) sc
962 | n == x = Bind x (fmap (pToV' n i) b) sc
958 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)
963 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)
959−pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)
964+pToV' n i (App s f a) = App s (pToV' n i f) (pToV' n i a)
960pToV' n i (Proj t idx) = Proj (pToV' n i t) idx
965pToV' n i (Proj t idx) = Proj (pToV' n i t) idx
961pToV' n i t = t
966pToV' n i t = t
@@ -967,7 +972,7 @@ addBinder t = ab 0 t
967 ab top (V i) | i >= top = V (i + 1)
972 ab top (V i) | i >= top = V (i + 1)
968 | otherwise = V i
973 | otherwise = V i
969 ab top (Bind x b sc) = Bind x (fmap (ab top) b) (ab (top + 1) sc)
974 ab top (Bind x b sc) = Bind x (fmap (ab top) b) (ab (top + 1) sc)
970− ab top (App f a) = App (ab top f) (ab top a)
975+ ab top (App s f a) = App s (ab top f) (ab top a)
971 ab top (Proj t idx) = Proj (ab top t) idx
976 ab top (Proj t idx) = Proj (ab top t) idx
972 ab top t = t
977 ab top t = t
@@ -986,14 +991,14 @@ vToP = vToP' [] where
986 P Bound n (binderTy b)
991 P Bound n (binderTy b)
987 vToP' env (Bind n b sc) = let b' = fmap (vToP' env) b in
992 vToP' env (Bind n b sc) = let b' = fmap (vToP' env) b in
988 Bind n b' (vToP' ((n, b'):env) sc)
993 Bind n b' (vToP' ((n, b'):env) sc)
989− vToP' env (App f a) = App (vToP' env f) (vToP' env a)
994+ vToP' env (App s f a) = App s (vToP' env f) (vToP' env a)
990 vToP' env t = t
995 vToP' env t = t
992-- | Replace every non-free reference to the name of a binding in
997-- | Replace every non-free reference to the name of a binding in
993-- the given term with a de Bruijn index.
998-- the given term with a de Bruijn index.
994finalise :: Eq n => TT n -> TT n
999finalise :: Eq n => TT n -> TT n
995finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
1000finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
996−finalise (App f a) = App (finalise f) (finalise a)
1001+finalise (App s f a) = App s (finalise f) (finalise a)
997finalise t = t
1002finalise t = t
999-- Once we've finished checking everything about a term we no longer need
1004-- Once we've finished checking everything about a term we no longer need
@@ -1001,7 +1006,7 @@ finalise t = t
1002pEraseType :: TT n -> TT n
1007pEraseType :: TT n -> TT n
1003pEraseType (P nt t _) = P nt t Erased
1008pEraseType (P nt t _) = P nt t Erased
1004−pEraseType (App f a) = App (pEraseType f) (pEraseType a)
1009+pEraseType (App s f a) = App s (pEraseType f) (pEraseType a)
1005pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)
1010pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)
1006pEraseType t = t
1011pEraseType t = t
@@ -1028,9 +1033,9 @@ subst n v tm = fst $ subst' 0 tm
1028 = let (b', ub) = substB' i b
1033 = let (b', ub) = substB' i b
1029 (sc', usc) = subst' (i+1) sc in
1034 (sc', usc) = subst' (i+1) sc in
1030 if ub || usc then (Bind x b' sc', True) else (t, False)
1035 if ub || usc then (Bind x b' sc', True) else (t, False)
1031− subst' i t@(App f a) = let (f', uf) = subst' i f
1036+ subst' i t@(App s f a) = let (f', uf) = subst' i f
1032− (a', ua) = subst' i a in
1037+ (a', ua) = subst' i a in
1033− if uf || ua then (App f' a', True) else (t, False)
1038+ if uf || ua then (App s f' a', True) else (t, False)
1034 subst' i t@(Proj x idx) = let (x', u) = subst' i x in
1039 subst' i t@(Proj x idx) = let (x', u) = subst' i x in
1035 if u then (Proj x' idx, u) else (t, False)
1040 if u then (Proj x' idx, u) else (t, False)
1036 subst' i t = (t, False)
1041 subst' i t = (t, False)
@@ -1055,7 +1060,7 @@ psubst n v tm = s' 0 tm where
1055 s' i (P _ x _) | n == x = v
1060 s' i (P _ x _) | n == x = v
1056 s' i (Bind x b sc) | n == x = Bind x (fmap (s' i) b) sc
1061 s' i (Bind x b sc) | n == x = Bind x (fmap (s' i) b) sc
1057 | otherwise = Bind x (fmap (s' i) b) (s' (i+1) sc)
1062 | otherwise = Bind x (fmap (s' i) b) (s' (i+1) sc)
1058− s' i (App f a) = App (s' i f) (s' i a)
1063+ s' i (App st f a) = App st (s' i f) (s' i a)
1059 s' i (Proj t idx) = Proj (s' i t) idx
1064 s' i (Proj t idx) = Proj (s' i t) idx
1060 s' i t = t
1065 s' i t = t
@@ -1073,7 +1078,7 @@ substTerm :: Eq n => TT n {-^ Old term -} ->
1074substTerm old new = st where
1079substTerm old new = st where
1075 st t | t == old = new
1080 st t | t == old = new
1076− st (App f a) = App (st f) (st a)
1081+ st (App s f a) = App s (st f) (st a)
1077 st (Bind x b sc) = Bind x (fmap st b) (st sc)
1082 st (Bind x b sc) = Bind x (fmap st b) (st sc)
1078 st t = t
1083 st t = t
@@ -1087,7 +1092,7 @@ occurrences n t = execState (no' 0 t) 0
1087 where noB' i (Let t v) = do no' i t; no' i v
1092 where noB' i (Let t v) = do no' i t; no' i v
1088 noB' i (Guess t v) = do no' i t; no' i v
1093 noB' i (Guess t v) = do no' i t; no' i v
1089 noB' i b = no' i (binderTy b)
1094 noB' i b = no' i (binderTy b)
1090− no' i (App f a) = do no' i f; no' i a
1095+ no' i (App _ f a) = do no' i f; no' i a
1091 no' i (Proj x _) = no' i x
1096 no' i (Proj x _) = no' i x
1092 no' i _ = return ()
1097 no' i _ = return ()
@@ -1101,7 +1106,7 @@ noOccurrence n t = no' 0 t
1101 where noB' i (Let t v) = no' i t && no' i v
1106 where noB' i (Let t v) = no' i t && no' i v
1102 noB' i (Guess t v) = no' i t && no' i v
1107 noB' i (Guess t v) = no' i t && no' i v
1103 noB' i b = no' i (binderTy b)
1108 noB' i b = no' i (binderTy b)
1104− no' i (App f a) = no' i f && no' i a
1109+ no' i (App _ f a) = no' i f && no' i a
1105 no' i (Proj x _) = no' i x
1110 no' i (Proj x _) = no' i x
1106 no' i _ = True
1111 no' i _ = True
@@ -1113,7 +1118,7 @@ freeNames t = nub $ freeNames' t
1113 freeNames' (Bind n (Let t v) sc) = freeNames' v ++ (freeNames' sc \\ [n])
1118 freeNames' (Bind n (Let t v) sc) = freeNames' v ++ (freeNames' sc \\ [n])
1114 ++ freeNames' t
1119 ++ freeNames' t
1115 freeNames' (Bind n b sc) = freeNames' (binderTy b) ++ (freeNames' sc \\ [n])
1120 freeNames' (Bind n b sc) = freeNames' (binderTy b) ++ (freeNames' sc \\ [n])
1116− freeNames' (App f a) = freeNames' f ++ freeNames' a
1121+ freeNames' (App _ f a) = freeNames' f ++ freeNames' a
1117 freeNames' (Proj x i) = freeNames' x
1122 freeNames' (Proj x i) = freeNames' x
1118 freeNames' _ = []
1123 freeNames' _ = []
@@ -1125,14 +1130,14 @@ arity _ = 0
1125-- | Deconstruct an application; returns the function and a list of arguments
1130-- | Deconstruct an application; returns the function and a list of arguments
1126unApply :: TT n -> (TT n, [TT n])
1131unApply :: TT n -> (TT n, [TT n])
1127unApply t = ua [] t where
1132unApply t = ua [] t where
1128− ua args (App f a) = ua (a:args) f
1133+ ua args (App _ f a) = ua (a:args) f
1129 ua args t = (t, args)
1134 ua args t = (t, args)
1131-- | Returns a term representing the application of the first argument
1136-- | Returns a term representing the application of the first argument
1132-- (a function) to every element of the second argument.
1137-- (a function) to every element of the second argument.
1133mkApp :: TT n -> [TT n] -> TT n
1138mkApp :: TT n -> [TT n] -> TT n
1134mkApp f [] = f
1139mkApp f [] = f
1135−mkApp f (a:as) = mkApp (App f a) as
1140+mkApp f (a:as) = mkApp (App MaybeHoles f a) as
1137unList :: Term -> Maybe [Term]
1142unList :: Term -> Maybe [Term]
1138unList tm = case unApply tm of
1143unList tm = case unApply tm of
@@ -1173,7 +1178,7 @@ safeForgetEnv env (Bind n b sc)
1173 (safeForgetEnv env v)
1178 (safeForgetEnv env v)
1174 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)
1179 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)
1175 Just $ fmap (\_ -> ty') b
1180 Just $ fmap (\_ -> ty') b
1176−safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)
1181+safeForgetEnv env (App _ f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)
1177safeForgetEnv env (Constant c) = Just $ RConstant c
1182safeForgetEnv env (Constant c) = Just $ RConstant c
1178safeForgetEnv env (TType i) = Just RType
1183safeForgetEnv env (TType i) = Just RType
1179safeForgetEnv env (UType u) = Just $ RUType u
1184safeForgetEnv env (UType u) = Just $ RUType u
@@ -1226,7 +1231,7 @@ uniqueBinders ns = ubSet (fromList ns) where
1226 = let n' = uniqueNameSet n ns
1231 = let n' = uniqueNameSet n ns
1227 ns' = insert n' ns in
1232 ns' = insert n' ns in
1228 Bind n' (fmap (ubSet ns') b) (ubSet ns' sc)
1233 Bind n' (fmap (ubSet ns') b) (ubSet ns' sc)
1229− ubSet ns (App f a) = App (ubSet ns f) (ubSet ns a)
1234+ ubSet ns (App s f a) = App s (ubSet ns f) (ubSet ns a)
1230 ubSet ns t = t
1235 ubSet ns t = t
@@ -1319,7 +1324,7 @@ prettyEnv env t = prettyEnv' env t False
1319 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
1324 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
1320 prettySe p env (Bind n b sc) debug =
1325 prettySe p env (Bind n b sc) debug =
1321 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
1326 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
1322− prettySe p env (App f a) debug =
1327+ prettySe p env (App _ f a) debug =
1323 bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug
1328 bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug
1324 prettySe p env (Proj x i) debug =
1329 prettySe p env (Proj x i) debug =
1325 prettySe 1 env x debug <+> text ("!" ++ show i)
1330 prettySe 1 env x debug <+> text ("!" ++ show i)
@@ -1363,7 +1368,7 @@ showEnv' env t dbg = se 10 env t where
1363 where arrow (TType _) = " -> "
1368 where arrow (TType _) = " -> "
1364 arrow u = " [" ++ show u ++ "] -> "
1369 arrow u = " [" ++ show u ++ "] -> "
1365 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc
1370 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc
1366− se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a
1371+ se p env (App _ f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a
1367 se p env (Proj x i) = se 1 env x ++ "!" ++ show i
1372 se p env (Proj x i) = se 1 env x ++ "!" ++ show i
1368 se p env (Constant c) = show c
1373 se p env (Constant c) = show c
1369 se p env Erased = "[__]"
1374 se p env Erased = "[__]"
@@ -1388,9 +1393,9 @@ showEnv' env t dbg = se 10 env t where
1388 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1393 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1389 | otherwise = str
1394 | otherwise = str
1391−-- | Check whether a term has any holes in it - impure if so
1396+-- | Check whether a term has any hole bindings in it - impure if so
1392pureTerm :: TT Name -> Bool
1397pureTerm :: TT Name -> Bool
1393−pureTerm (App f a) = pureTerm f && pureTerm a
1398+pureTerm (App _ f a) = pureTerm f && pureTerm a
1394pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where
1399pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where
1395 pureBinder (Hole _) = False
1400 pureBinder (Hole _) = False
1396 pureBinder (Guess _ _) = False
1401 pureBinder (Guess _ _) = False
@@ -1406,7 +1411,7 @@ pureTerm _ = True
1406weakenTm :: Int -> TT n -> TT n
1411weakenTm :: Int -> TT n -> TT n
1407weakenTm i t = wk i 0 t
1412weakenTm i t = wk i 0 t
1408 where wk i min (V x) | x >= min = V (i + x)
1413 where wk i min (V x) | x >= min = V (i + x)
1409− wk i m (App f a) = App (wk i m f) (wk i m a)
1414+ wk i m (App s f a) = App s (wk i m f) (wk i m a)
1410 wk i m (Bind x b sc) = Bind x (wkb i m b) (wk i (m + 1) sc)
1415 wk i m (Bind x b sc) = Bind x (wkb i m b) (wk i (m + 1) sc)
1411 wk i m t = t
1416 wk i m t = t
1412 wkb i m t = fmap (wk i m) t
1417 wkb i m t = fmap (wk i m) t
@@ -1431,7 +1436,7 @@ weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
1431orderPats :: Term -> Term
1436orderPats :: Term -> Term
1432orderPats tm = op [] tm
1437orderPats tm = op [] tm
1434− op [] (App f a) = App f (op [] a) -- for Infer terms
1439+ op [] (App s f a) = App s f (op [] a) -- for Infer terms
1436 op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc
1441 op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc
1437 op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc
1442 op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc
@@ -1456,7 +1461,7 @@ refsIn (Bind n b t) = nub $ nb b ++ refsIn t
1456 where nb (Let t v) = nub (refsIn t) ++ nub (refsIn v)
1461 where nb (Let t v) = nub (refsIn t) ++ nub (refsIn v)
1457 nb (Guess t v) = nub (refsIn t) ++ nub (refsIn v)
1462 nb (Guess t v) = nub (refsIn t) ++ nub (refsIn v)
1458 nb t = refsIn (binderTy t)
1463 nb t = refsIn (binderTy t)
1459−refsIn (App f a) = nub (refsIn f ++ refsIn a)
1464+refsIn (App s f a) = nub (refsIn f ++ refsIn a)
1460refsIn _ = []
1465refsIn _ = []
1462-- Make sure all the pattern bindings are as far out as possible
1467-- Make sure all the pattern bindings are as far out as possible
@@ -1493,9 +1498,9 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in
1493 return (Bind n (Hole t') sc')
1498 return (Bind n (Hole t') sc')
1496− getPats (App f a) = do f' <- getPats f
1501+ getPats (App s f a) = do f' <- getPats f
1497− a' <- getPats a
1502+ a' <- getPats a
1498− return (App f' a')
1503+ return (App s f' a')
1499 getPats t = return t
1504 getPats t = return t
1501allTTNames :: Eq n => TT n -> [n]
1506allTTNames :: Eq n => TT n -> [n]
@@ -1505,7 +1510,7 @@ allTTNames = nub . allNamesIn
1505 where nb (Let t v) = allNamesIn t ++ allNamesIn v
1510 where nb (Let t v) = allNamesIn t ++ allNamesIn v
1506 nb (Guess t v) = allNamesIn t ++ allNamesIn v
1511 nb (Guess t v) = allNamesIn t ++ allNamesIn v
1507 nb t = allNamesIn (binderTy t)
1512 nb t = allNamesIn (binderTy t)
1508− allNamesIn (App f a) = allNamesIn f ++ allNamesIn a
1513+ allNamesIn (App _ f a) = allNamesIn f ++ allNamesIn a
1509 allNamesIn _ = []
1514 allNamesIn _ = []
@@ -1528,7 +1533,7 @@ pprintTT bound tm = pp startPrec bound tm
1528 | otherwise = text ("{{{V" ++ show i ++ "}}}")
1533 | otherwise = text ("{{{V" ++ show i ++ "}}}")
1529 pp p bound (Bind n b sc) = ppb p bound n b $
1534 pp p bound (Bind n b sc) = ppb p bound n b $
1530 pp startPrec (n:bound) sc
1535 pp startPrec (n:bound) sc
1531− pp p bound (App tm1 tm2) =
1536+ pp p bound (App _ tm1 tm2) =
1532 bracket p appPrec . group . hang 2 $
1537 bracket p appPrec . group . hang 2 $
1533 pp appPrec bound tm1 <> line <>
1538 pp appPrec bound tm1 <> line <>
1534 pp (appPrec + 1) bound tm2
1539 pp (appPrec + 1) bound tm2