0 | module TTImp.BindImplicits
  1 |
  2 | import Core.Context.Log
  3 | import TTImp.TTImp
  4 | import TTImp.Utils
  5 |
  6 | import Control.Monad.State
  7 |
  8 | import Data.List
  9 |
 10 | %default covering
 11 |
 12 | -- Rename the IBindVars in a term. Anything which appears in the list 'renames'
 13 | -- should be renamed, to something which is *not* in the list 'used'
 14 | export
 15 | renameIBinds : (renames : List String) ->
 16 |                (used : List String) ->
 17 |                RawImp -> State (List (String, String)) RawImp
 18 | renameIBinds rs us (IPi fc c p (Just un@(UN (Basic n))) ty sc)
 19 |     = if n `elem` rs
 20 |          then let n' = genUniqueStr (rs ++ us) n
 21 |                   un' = UN (Basic n')
 22 |                   sc' = substNames (map (UN . Basic) (filter (/= n) us))
 23 |                                    [(un, IVar fc un')] sc in
 24 |              do scr <- renameIBinds rs (n' :: us) sc'
 25 |                 ty' <- renameIBinds rs us ty
 26 |                 upds <- get
 27 |                 put ((n, n') :: upds)
 28 |                 pure $ IPi fc c p (Just un') ty' scr
 29 |          else do scr <- renameIBinds rs us sc
 30 |                  ty' <- renameIBinds rs us ty
 31 |                  pure $ IPi fc c p (Just un) ty' scr
 32 | renameIBinds rs us (IPi fc c p n ty sc)
 33 |     = pure $ IPi fc c p n !(renameIBinds rs us ty) !(renameIBinds rs us sc)
 34 | renameIBinds rs us (ILam fc c p n ty sc)
 35 |     = pure $ ILam fc c p n !(renameIBinds rs us ty) !(renameIBinds rs us sc)
 36 | renameIBinds rs us (IApp fc fn arg)
 37 |     = pure $ IApp fc !(renameIBinds rs us fn) !(renameIBinds rs us arg)
 38 | renameIBinds rs us (IAutoApp fc fn arg)
 39 |     = pure $ IAutoApp fc !(renameIBinds rs us fn) !(renameIBinds rs us arg)
 40 | renameIBinds rs us (INamedApp fc fn n arg)
 41 |     = pure $ INamedApp fc !(renameIBinds rs us fn) n !(renameIBinds rs us arg)
 42 | renameIBinds rs us (IWithApp fc fn arg)
 43 |     = pure $ IWithApp fc !(renameIBinds rs us fn) !(renameIBinds rs us arg)
 44 | renameIBinds rs us (IAs fc nameFC s n pat)
 45 |     = pure $ IAs fc nameFC s n !(renameIBinds rs us pat)
 46 | renameIBinds rs us (IMustUnify fc r pat)
 47 |     = pure $ IMustUnify fc r !(renameIBinds rs us pat)
 48 | renameIBinds rs us (IDelayed fc r t)
 49 |     = pure $ IDelayed fc r !(renameIBinds rs us t)
 50 | renameIBinds rs us (IDelay fc t)
 51 |     = pure $ IDelay fc !(renameIBinds rs us t)
 52 | renameIBinds rs us (IForce fc t)
 53 |     = pure $ IForce fc !(renameIBinds rs us t)
 54 | renameIBinds rs us (IUpdate fc updates tm)
 55 |     = pure $ IUpdate fc !(traverse f updates) !(renameIBinds rs us tm)
 56 |   where
 57 |       f : IFieldUpdate -> State (List (String, String)) IFieldUpdate
 58 |       f (ISetField path x)    = ISetField path <$> renameIBinds rs us x
 59 |       f (ISetFieldApp path x) = ISetFieldApp path <$> renameIBinds rs us x
 60 | renameIBinds rs us (IAlternative fc u alts)
 61 |     = pure $ IAlternative fc !(renameAlt u)
 62 |                              !(traverse (renameIBinds rs us) alts)
 63 |   where
 64 |     renameAlt : AltType -> State (List (String, String)) AltType
 65 |     renameAlt (UniqueDefault t) = pure $ UniqueDefault !(renameIBinds rs us t)
 66 |     renameAlt u = pure u
 67 | renameIBinds rs us (IBindVar fc nm@(UN (Basic n)))
 68 |     = if n `elem` rs
 69 |          then do let n' = genUniqueStr (rs ++ us) n
 70 |                  upds <- get
 71 |                  put ((n, n') :: upds)
 72 |                  pure $ IBindVar fc (UN (Basic n'))
 73 |          else pure $ IBindVar fc nm
 74 | renameIBinds rs us tm = pure $ tm
 75 |
 76 | export
 77 | doBind : List (Name, Name) -> RawImp -> RawImp
 78 | doBind [] tm = tm
 79 | doBind ns (IVar fc nm)
 80 |     = maybe (IVar fc nm) (IBindVar fc) (lookup nm ns)
 81 | doBind ns (IPi fc rig p mn aty retty)
 82 |     = let ns' = case mn of
 83 |                      Just nm => filter (\x => fst x /= nm) ns
 84 |                      _ => ns in
 85 |           IPi fc rig p mn (doBind ns' aty) (doBind ns' retty)
 86 | doBind ns (ILam fc rig p mn aty sc)
 87 |     = let ns' = case mn of
 88 |                      Just nm => filter (\x => fst x /= nm) ns
 89 |                      _ => ns in
 90 |           ILam fc rig p mn (doBind ns' aty) (doBind ns' sc)
 91 | doBind ns (IApp fc fn av)
 92 |     = IApp fc (doBind ns fn) (doBind ns av)
 93 | doBind ns (IAutoApp fc fn av)
 94 |     = IAutoApp fc (doBind ns fn) (doBind ns av)
 95 | doBind ns (INamedApp fc fn n av)
 96 |     = INamedApp fc (doBind ns fn) n (doBind ns av)
 97 | doBind ns (IWithApp fc fn av)
 98 |     = IWithApp fc (doBind ns fn) (doBind ns av)
 99 | doBind ns (IAs fc nameFC s n pat)
100 |     = IAs fc nameFC s n (doBind ns pat)
101 | doBind ns (IMustUnify fc r pat)
102 |     = IMustUnify fc r (doBind ns pat)
103 | doBind ns (IDelayed fc r ty)
104 |     = IDelayed fc r (doBind ns ty)
105 | doBind ns (IDelay fc tm)
106 |     = IDelay fc (doBind ns tm)
107 | doBind ns (IForce fc tm)
108 |     = IForce fc (doBind ns tm)
109 | doBind ns (IQuote fc tm)
110 |     = IQuote fc (doBind ns tm)
111 | doBind ns (IUnquote fc tm)
112 |     = IUnquote fc (doBind ns tm)
113 | doBind ns (IAlternative fc u alts)
114 |     = IAlternative fc (mapAltType (doBind ns) u) (map (doBind ns) alts)
115 | doBind ns (IUpdate fc updates tm)
116 |     = IUpdate fc (map (mapFieldUpdateTerm $ doBind ns) updates) (doBind ns tm)
117 | doBind ns tm = tm
118 |
119 | export
120 | bindNames : {auto c : Ref Ctxt Defs} ->
121 |             (arg : Bool) -> RawImp -> Core (List Name, RawImp)
122 | bindNames arg tm
123 |     = if !isUnboundImplicits
124 |          then do let ns = nub (findBindableNames arg [] [] tm)
125 |                  log "elab.bindnames" 10 $ "Found names :" ++ show ns
126 |                  pure (map snd ns, doBind ns tm)
127 |          else pure ([], tm)
128 |
129 | -- if the name is part of the using decls, add the relevant binder for it:
130 | -- either an implicit pi binding, if there's a name, or an autoimplicit type
131 | -- binding if the name just appears as part of the type
132 | getUsing : Name -> List (Int, Maybe Name, RawImp) ->
133 |            List (Int, (RigCount, PiInfo RawImp, Maybe Name, RawImp))
134 | getUsing n [] = []
135 | getUsing n ((t, Just n', ty) :: us) -- implicit binder
136 |     = if n == n'
137 |          then (t, (erased, Implicit, Just n, ty)) :: getUsing n us
138 |          else getUsing n us
139 | getUsing n ((t, Nothing, ty) :: us) -- autoimplicit binder
140 |     = let ns = nub (findIBindVars ty) in
141 |           if n `elem` ns
142 |              then (t, (top, AutoImplicit, Nothing, ty)) ::
143 |                       getUsing n us
144 |              else getUsing n us
145 |
146 | getUsings : List Name -> List (Int, Maybe Name, RawImp) ->
147 |             List (Int, (RigCount, PiInfo RawImp, Maybe Name, RawImp))
148 | getUsings ns u = concatMap (flip getUsing u) ns
149 |
150 | bindUsings : List (RigCount, PiInfo RawImp, Maybe Name, RawImp) -> RawImp -> RawImp
151 | bindUsings [] tm = tm
152 | bindUsings ((rig, p, mn, ty) :: us) tm
153 |     = IPi (getFC ty) rig p mn ty (bindUsings us tm)
154 |
155 | addUsing : List (Maybe Name, RawImp) ->
156 |            RawImp -> RawImp
157 | addUsing uimpls tm
158 |     = let ns = nub (findIBindVars tm)
159 |           bs = nubBy (\x, y => fst x == fst y)
160 |                      (getUsings ns (tag 0 uimpls)) in
161 |           bindUsings (map snd bs) tm
162 |   where
163 |     tag : Int -> List a -> List (Int, a) -- to check uniqueness of resulting uimps
164 |     tag t xs = zip (map (+t) [0..cast (length xs)]) xs
165 |
166 | export
167 | bindTypeNames : {auto c : Ref Ctxt Defs} ->
168 |                 FC -> List (Maybe Name, RawImp) ->
169 |                 List Name -> RawImp-> Core RawImp
170 | bindTypeNames fc uimpls env tm
171 |     = if !isUnboundImplicits
172 |              then do ns <- findUniqueBindableNames fc True env [] tm
173 |                      let btm = doBind ns tm
174 |                      pure (addUsing uimpls btm)
175 |              else pure tm
176 |
177 | export
178 | bindTypeNamesUsed : {auto c : Ref Ctxt Defs} ->
179 |                     FC -> List String -> List Name -> RawImp -> Core RawImp
180 | bindTypeNamesUsed fc used env tm
181 |     = if !isUnboundImplicits
182 |          then do ns <- findUniqueBindableNames fc True env used tm
183 |                  pure (doBind ns tm)
184 |          else pure tm
185 |
186 | export
187 | piBindNames : {auto c : Ref Ctxt Defs} ->
188 |               FC -> List Name -> RawImp -> Core RawImp
189 | piBindNames loc env tm
190 |     = do ns <- findUniqueBindableNames loc True env [] tm
191 |          pure $ piBind (map fst ns) tm
192 |   where
193 |     piBind : List Name -> RawImp -> RawImp
194 |     piBind [] ty = ty
195 |     piBind (n :: ns) ty
196 |        = IPi loc erased Implicit (Just n) (Implicit loc False)
197 |        $ piBind ns ty
198 |