@@ -755,14 +755,14 @@ allNamesIn tm = nub $ ni [] tm
755 ni env (PAlternative ls) = concatMap (ni env) ls
755 ni env (PAlternative ls) = concatMap (ni env) ls
756 ni env _ = []
756 ni env _ = []
758−namesIn :: IState -> PTerm -> [Name]
758+namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
759−namesIn ist tm = nub $ ni [] tm
759+namesIn uvars ist tm = nub $ ni [] tm
761 ni env (PRef _ n)
761 ni env (PRef _ n)
762 | not (n `elem` env)
762 | not (n `elem` env)
763 = case lookupTy Nothing n (tt_ctxt ist) of
763 = case lookupTy Nothing n (tt_ctxt ist) of
764 [] -> [n]
764 [] -> [n]
765− _ -> []
765+ _ -> if n `elem` (map fst uvars) then [n] else []
766 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
766 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
767 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
767 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
768 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
768 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
@@ -911,7 +911,7 @@ expandParamsD ist dec ps ns (PClauses fc opts n cs)
912 expandParamsC (PClause n lhs ws rhs ds)
912 expandParamsC (PClause n lhs ws rhs ds)
913 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
913 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
914− ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
914+ ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
915 n' = if n `elem` ns then dec n else n in
915 n' = if n `elem` ns then dec n else n in
916 PClause n' (expandParams dec ps'' ns lhs)
916 PClause n' (expandParams dec ps'' ns lhs)
917 (map (expandParams dec ps'' ns) ws)
917 (map (expandParams dec ps'' ns) ws)
@@ -919,7 +919,7 @@ expandParamsD ist dec ps ns (PClauses fc opts n cs)
919 (map (expandParamsD ist dec ps'' ns) ds)
919 (map (expandParamsD ist dec ps'' ns) ds)
920 expandParamsC (PWith n lhs ws wval ds)
920 expandParamsC (PWith n lhs ws wval ds)
921 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
921 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
922− ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
922+ ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
923 n' = if n `elem` ns then dec n else n in
923 n' = if n `elem` ns then dec n else n in
924 PWith n' (expandParams dec ps'' ns lhs)
924 PWith n' (expandParams dec ps'' ns lhs)
925 (map (expandParams dec ps'' ns) ws)
925 (map (expandParams dec ps'' ns) ws)
@@ -983,39 +983,40 @@ implicit syn n ptm
984implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
984implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
985implicitise syn ist tm
985implicitise syn ist tm
986− = let uvars = using syn
987− pvars = syn_params syn
988− (declimps, ns') = execState (imps True [] tm) ([], [])
986+ = let (declimps, ns') = execState (imps True [] tm) ([], [])
989 ns = ns' \\ (map fst pvars ++ no_imp syn) in
987 ns = ns' \\ (map fst pvars ++ no_imp syn) in
990 if null ns
988 if null ns
991 then (tm, reverse declimps)
989 then (tm, reverse declimps)
992 else implicitise syn ist (pibind uvars ns tm)
990 else implicitise syn ist (pibind uvars ns tm)
993+ pvars = syn_params syn
994 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
995 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
995 | otherwise = x : dropAll xs ys
996 | otherwise = x : dropAll xs ys
996 dropAll [] ys = []
997 dropAll [] ys = []
998 imps top env (PApp _ f as)
999 imps top env (PApp _ f as)
999 = do (decls, ns) <- get
1000 = do (decls, ns) <- get
1000− let isn = concatMap (namesIn ist) (map getTm as)
1001+ let isn = concatMap (namesIn uvars ist) (map getTm as)
1001 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1002 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1002 imps top env (PPi (Imp l _) n ty sc)
1003 imps top env (PPi (Imp l _) n ty sc)
1003− = do let isn = nub (namesIn ist ty) `dropAll` [n]
1004+ = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1004 (decls , ns) <- get
1005 (decls , ns) <- get
1005 put (PImp (getPriority ist ty) l n ty : decls,
1006 put (PImp (getPriority ist ty) l n ty : decls,
1006 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1007 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1007 imps True (n:env) sc
1008 imps True (n:env) sc
1008 imps top env (PPi (Exp l _) n ty sc)
1009 imps top env (PPi (Exp l _) n ty sc)
1009− = do let isn = nub (namesIn ist ty ++ case sc of
1010+ = do let isn = nub (namesIn uvars ist ty ++ case sc of
1010− (PRef _ x) -> namesIn ist sc `dropAll` [n]
1011+ (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1011 _ -> [])
1012 _ -> [])
1012 (decls, ns) <- get -- ignore decls in HO types
1013 (decls, ns) <- get -- ignore decls in HO types
1013 put (PExp (getPriority ist ty) l ty : decls,
1014 put (PExp (getPriority ist ty) l ty : decls,
1014 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1015 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1015 imps True (n:env) sc
1016 imps True (n:env) sc
1016 imps top env (PPi (Constraint l _) n ty sc)
1017 imps top env (PPi (Constraint l _) n ty sc)
1017− = do let isn = nub (namesIn ist ty ++ case sc of
1018+ = do let isn = nub (namesIn uvars ist ty ++ case sc of
1018− (PRef _ x) -> namesIn ist sc `dropAll` [n]
1019+ (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1019 _ -> [])
1020 _ -> [])
1020 (decls, ns) <- get -- ignore decls in HO types
1021 (decls, ns) <- get -- ignore decls in HO types
1021 put (PConstraint 10 l ty : decls,
1022 put (PConstraint 10 l ty : decls,
@@ -1023,23 +1024,24 @@ implicitise syn ist tm
1023 imps True (n:env) sc
1024 imps True (n:env) sc
1024 imps top env (PEq _ l r)
1025 imps top env (PEq _ l r)
1025 = do (decls, ns) <- get
1026 = do (decls, ns) <- get
1026− let isn = namesIn ist l ++ namesIn ist r
1027+ let isn = namesIn uvars ist l ++ namesIn uvars ist r
1027 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1028 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1028 imps top env (PPair _ l r)
1029 imps top env (PPair _ l r)
1029 = do (decls, ns) <- get
1030 = do (decls, ns) <- get
1030− let isn = namesIn ist l ++ namesIn ist r
1031+ let isn = namesIn uvars ist l ++ namesIn uvars ist r
1031 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1032 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1032 imps top env (PDPair _ (PRef _ n) t r)
1033 imps top env (PDPair _ (PRef _ n) t r)
1033 = do (decls, ns) <- get
1034 = do (decls, ns) <- get
1034− let isn = nub (namesIn ist t ++ namesIn ist r) \\ [n]
1035+ let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1035 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1036 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1036 imps top env (PDPair _ l t r)
1037 imps top env (PDPair _ l t r)
1037 = do (decls, ns) <- get
1038 = do (decls, ns) <- get
1038− let isn = namesIn ist l ++ namesIn ist t ++ namesIn ist r
1039+ let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1040+ namesIn uvars ist r
1039 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1041 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1040 imps top env (PAlternative as)
1042 imps top env (PAlternative as)
1041 = do (decls, ns) <- get
1043 = do (decls, ns) <- get
1042− let isn = concatMap (namesIn ist) as
1044+ let isn = concatMap (namesIn uvars ist) as
1043 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1045 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1044 imps top env (PLam n ty sc)
1046 imps top env (PLam n ty sc)
1045 = do imps False env ty
1047 = do imps False env ty
@@ -1149,9 +1151,9 @@ findStatics ist tm = let (ns, ss) = fs tm in
1149 where fs (PPi p n t sc)
1151 where fs (PPi p n t sc)
1150 | Static <- pstatic p
1152 | Static <- pstatic p
1151 = let (ns, ss) = fs sc in
1153 = let (ns, ss) = fs sc in
1152− (namesIn ist t : ns, namesIn ist t ++ n : ss)
1154+ (namesIn [] ist t : ns, namesIn [] ist t ++ n : ss)
1153 | otherwise = let (ns, ss) = fs sc in
1155 | otherwise = let (ns, ss) = fs sc in
1154− (namesIn ist t : ns, ss)
1156+ (namesIn [] ist t : ns, ss)
1155 fs _ = ([], [])
1157 fs _ = ([], [])
1157 inOne n ns = length (filter id (map (elem n) ns)) == 1
1159 inOne n ns = length (filter id (map (elem n) ns)) == 1