0 | module TTImp.WithClause

  2 | import Core.Context.Log

  3 | import Core.Metadata

  5 | import TTImp.BindImplicits

  6 | import TTImp.TTImp

  7 | import TTImp.Elab.Check

  9 | %default covering

 11 | matchFail : FC -> Core a

 12 | matchFail loc = throw (GenericMsg loc "With clause does not match parent")

 16 | getHeadLoc : RawImp -> Core FC

 17 | getHeadLoc (IVar fc _) = pure fc

 18 | getHeadLoc (IApp _ f _) = getHeadLoc f

 19 | getHeadLoc (IWithApp _ f _) = getHeadLoc f

 20 | getHeadLoc (IAutoApp _ f _) = getHeadLoc f

 21 | getHeadLoc (INamedApp _ f _ _) = getHeadLoc f

 22 | getHeadLoc t = throw (InternalError $ "Could not find head of LHS: " ++ show t)

 24 | addAlias : {auto m : Ref MD Metadata} ->

 25 |            {auto c : Ref Ctxt Defs} ->

 26 |            FC -> FC -> Core ()

 27 | addAlias from to =

 28 |   whenJust (isConcreteFC from) $ \ from =>

 29 |     whenJust (isConcreteFC to) $ \ to => do

 30 |       log "ide-mode.highlight.alias" 25 $

 31 |         "Adding alias: " ++ show from ++ " -> " ++ show to

 32 |       addSemanticAlias from to

 35 |   export

 36 |   getMatch : {auto m : Ref MD Metadata} ->

 37 |              {auto c : Ref Ctxt Defs} ->

 38 |              (lhs : Bool) -> RawImp -> RawImp ->

 39 |              Core (List (Name, RawImp))

 40 |   getMatch lhs (IBindVar to n) tm@(IBindVar from _)

 41 |       = [(n, tm)] <$ addAlias from to

 42 |   getMatch lhs (IBindVar _ n) tm = pure [(n, tm)]

 43 |   getMatch lhs (Implicit {}) tm = pure []

 44 |   getMatch lhs _ (IMustUnify _ UserDotted _) = pure []

 46 |   getMatch lhs (IVar to (NS ns n)) (IVar from (NS ns' n'))

 47 |       = if n == n' && isParentOf ns' ns

 48 |           then [] <$ addAlias from to -- <$ decorateName loc nm

 49 |           else matchFail from

 50 |   getMatch lhs (IVar to (NS ns n)) (IVar from n')

 51 |       = if n == n'

 52 |           then [] <$ addAlias from to -- <$ decorateName loc (NS ns n')

 53 |           else matchFail from

 54 |   getMatch lhs (IVar to n) (IVar from n')

 55 |       = if n == n'

 56 |           then [] <$ addAlias from to -- <$ decorateName loc n'

 57 |           else matchFail from

 58 |   getMatch lhs (IPi _ c p n arg ret) (IPi loc c' p' n' arg' ret')

 59 |       = if c == c' && eqPiInfoBy (\_, _ => True) p p' && n == n'

 60 |            then matchAll lhs [(arg, arg'), (ret, ret')]

 61 |            else matchFail loc

 62 |   -- TODO: Lam, Let, Case, Local, Update

 63 |   getMatch lhs (IApp _ f a) (IApp loc f' a')

 64 |       = matchAll lhs [(f, f'), (a, a')]

 65 |   getMatch lhs (IAutoApp _ f a) (IAutoApp loc f' a')

 66 |       = matchAll lhs [(f, f'), (a, a')]

 67 |   getMatch lhs (INamedApp _ f n a) (INamedApp loc f' n' a')

 68 |       = if n == n'

 69 |            then matchAll lhs [(f, f'), (a, a')]

 70 |            else matchFail loc

 71 |   getMatch lhs (IWithApp _ f a) (IWithApp loc f' a')

 72 |       = matchAll lhs [(f, f'), (a, a')]

 73 |   -- On LHS: If there's an implicit in the parent, but not the clause, add the

 74 |   -- implicit to the clause. This will propagate the implicit through to the

 75 |   -- body

 76 |   getMatch True (INamedApp fc f n a) f'

 77 |       = matchAll True [(f, f'), (a, a)]

 78 |   getMatch True (IAutoApp fc f a) f'

 79 |       = matchAll True [(f, f'), (a, a)]

 80 |   -- On RHS: Rely on unification to fill in the implicit

 81 |   getMatch False (INamedApp fc f n a) f'

 82 |       = getMatch False f f'

 83 |   getMatch False (IAutoApp fc f a) f'

 84 |       = getMatch False f f'

 85 |   -- Can't have an implicit in the clause if there wasn't a matching

 86 |   -- implicit in the parent

 87 |   getMatch lhs f (INamedApp fc f' n a)

 88 |       = matchFail fc

 89 |   getMatch lhs f (IAutoApp fc f' a)

 90 |       = matchFail fc

 91 |   -- Alternatives are okay as long as the alternatives correspond, and

 92 |   -- one of them is okay

 93 |   getMatch lhs (IAlternative _ _ as) (IAlternative fc _ as')

 94 |       = matchAny fc lhs (zip as as')

 95 |   getMatch lhs (IAs _ _ _ nm@(UN (Basic _)) p) (IAs _ fc _ nm'@(UN (Basic _)) p')

 96 |       = do ms <- getMatch lhs p p'

 97 |            mergeMatches lhs ((nm, IAs fc emptyFC UseLeft nm' (Implicit fc True)) :: ms)

 98 |   getMatch lhs (IAs _ _ _ nm@(UN (Basic _)) p) p'

 99 |       = do ms <- getMatch lhs p p'

100 |            mergeMatches lhs ((nm, p') :: ms)

101 |   getMatch lhs (IAs _ _ _ _ p) p' = getMatch lhs p p'

102 |   getMatch lhs p (IAs _ _ _ _ p') = getMatch lhs p p'

103 |   getMatch lhs (IType _) (IType _) = pure []

104 |   getMatch lhs (IPrimVal fc c) (IPrimVal fc' c') =

105 |     if c == c'

106 |     then pure []

107 |     else matchFail fc'

108 |   getMatch lhs pat spec = matchFail (getFC spec)

110 |   matchAny : {auto m : Ref MD Metadata} ->

111 |              {auto c : Ref Ctxt Defs} ->

112 |              FC -> (lhs : Bool) -> List (RawImp, RawImp) ->

113 |              Core (List (Name, RawImp))

114 |   matchAny fc lhs [] = matchFail fc

115 |   matchAny fc lhs ((x, y) :: ms)

116 |       = catch (getMatch lhs x y)

117 |               (\err => matchAny fc lhs ms)

119 |   matchAll : {auto m : Ref MD Metadata} ->

120 |              {auto c : Ref Ctxt Defs} ->

121 |              (lhs : Bool) -> List (RawImp, RawImp) ->

122 |              Core (List (Name, RawImp))

123 |   matchAll lhs [] = pure []

124 |   matchAll lhs ((x, y) :: ms)

125 |       = do matches <- matchAll lhs ms

126 |            mxy <- getMatch lhs x y

127 |            mergeMatches lhs (mxy ++ matches)

129 |   mergeMatches : {auto m : Ref MD Metadata} ->

130 |                  {auto c : Ref Ctxt Defs} ->

131 |                  (lhs : Bool) -> List (Name, RawImp) ->

132 |                  Core (List (Name, RawImp))

133 |   mergeMatches lhs [] = pure []

134 |   mergeMatches lhs ((n, tm) :: rest)

135 |       = do rest' <- mergeMatches lhs rest

136 |            case lookup n rest' of

137 |                 Nothing => pure ((n, tm) :: rest')

138 |                 Just tm' =>

139 |                    do ignore $ getMatch lhs tm tm'

140 |                       -- ^ just need to know it succeeds

141 |                       pure rest'

145 | getArgMatch : FC -> (side : ElabMode) -> (search : Bool) ->

146 |               (warg : RawImp) -> (matches : List (Name, RawImp)) ->

147 |               (arg : Maybe (PiInfo RawImp, Name)) -> RawImp

148 | getArgMatch ploc mode search warg ms Nothing = warg

149 | getArgMatch ploc mode True warg ms (Just (AutoImplicit, nm))

150 |     = case lookup nm ms of

151 |         Just tm => tm

152 |         Nothing =>

153 |           let arg = ISearch ploc 500 in

154 |           if isJust (isLHS mode)

155 |             then IAs ploc ploc UseLeft nm arg

156 |              else arg

157 | getArgMatch ploc mode search warg ms (Just (_, nm))

158 |     = case lookup nm ms of

159 |         Just tm => tm

160 |         Nothing =>

161 |           let arg = Implicit ploc True in

162 |            if isJust (isLHS mode)

163 |              then IAs ploc ploc UseLeft nm arg

164 |              else arg

167 | getNewLHS : {auto c : Ref Ctxt Defs} ->

168 |             {auto m : Ref MD Metadata} ->

169 |             FC -> (drop : Nat) -> NestedNames vars ->

170 |             Name -> List (Maybe (PiInfo RawImp, Name)) ->

171 |             RawImp -> RawImp -> Core RawImp

172 | getNewLHS iploc drop nest wname wargnames lhs_raw patlhs

173 |     = do let vploc = virtualiseFC iploc

174 |          (mlhs_raw, wrest) <- dropWithArgs drop patlhs

176 |          log "declare.def.clause.with" 20 $ "Parent LHS: " ++ show lhs_raw

177 |          log "declare.def.clause.with" 20 $ "Modified LHS: " ++ show mlhs_raw

179 |          autoimp <- isUnboundImplicits

180 |          setUnboundImplicits True

181 |          (_, lhs) <- bindNames False lhs_raw

182 |          (_, mlhs) <- bindNames False mlhs_raw

183 |          setUnboundImplicits autoimp

185 |          log "declare.def.clause.with" 20 $ "Parent LHS (with implicits): " ++ show lhs

186 |          log "declare.def.clause.with" 20 $ "Modified LHS (with implicits): " ++ show mlhs

188 |          let (warg :: rest) = reverse wrest

189 |              | _ => throw (GenericMsg iploc "Badly formed 'with' clause")

190 |          log "declare.def.clause.with" 5 $ show lhs ++ " against " ++ show mlhs ++

191 |                  " dropping " ++ show (warg :: rest)

192 |          ms <- getMatch True lhs mlhs

193 |          log "declare.def.clause.with" 5 $ "Matches: " ++ show ms

194 |          let params = map (getArgMatch vploc (InLHS top) False warg ms) wargnames

195 |          log "declare.def.clause.with" 5 $ "Parameters: " ++ show params

197 |          hdloc <- getHeadLoc patlhs

198 |          let newlhs = apply (IVar hdloc wname) (params ++ rest)

199 |          log "declare.def.clause.with" 5 $ "New LHS: " ++ show newlhs

200 |          pure newlhs

201 |   where

202 |     dropWithArgs : Nat -> RawImp ->

203 |                    Core (RawImp, List RawImp)

204 |     dropWithArgs Z tm = pure (tm, [])

205 |     dropWithArgs (S k) (IApp _ f arg)

206 |         = do (tm, rest) <- dropWithArgs k f

207 |              pure (tm, arg :: rest)

208 |     dropWithArgs (S k) (IWithApp _ f arg)

209 |         = do (tm, rest) <- dropWithArgs k f

210 |              pure (tm, arg :: rest)

211 |     -- Shouldn't happen if parsed correctly, but there's no guarantee that

212 |     -- inputs come from parsed source so throw an error.

213 |     dropWithArgs _ _ = throw (GenericMsg iploc "Badly formed 'with' clause")

217 | withRHS : {auto c : Ref Ctxt Defs} ->

218 |           {auto m : Ref MD Metadata} ->

219 |           FC -> (drop : Nat) -> Name -> List (Maybe (PiInfo RawImp, Name)) ->

220 |           RawImp -> RawImp ->

221 |           Core RawImp

222 | withRHS fc drop wname wargnames tm toplhs

223 |     = wrhs tm

224 |   where

225 |     withApply : FC -> RawImp -> List RawImp -> RawImp

226 |     withApply fc f [] = f

227 |     withApply fc f (a :: as) = withApply fc (IWithApp fc f a) as

229 |     updateWith : FC -> RawImp -> List RawImp -> Core RawImp

230 |     updateWith fc (IWithApp _ f a) ws = updateWith fc f (a :: ws)

231 |     updateWith fc tm []

232 |         = throw (GenericMsg fc "Badly formed 'with' application")

233 |     updateWith fc tm (arg :: args)

234 |         = do log "declare.def.clause.with" 10 $ "With-app: Matching " ++ show toplhs ++ " against " ++ show tm

235 |              ms <- getMatch False toplhs tm

236 |              hdloc <- getHeadLoc tm

237 |              log "declare.def.clause.with" 10 $ "Result: " ++ show ms

238 |              let newrhs = apply (IVar hdloc wname)

239 |                                 (map (getArgMatch fc InExpr True arg ms) wargnames)

240 |              log "declare.def.clause.with" 10 $ "With args for RHS: " ++ show wargnames

241 |              log "declare.def.clause.with" 10 $ "New RHS: " ++ show newrhs

242 |              pure (withApply fc newrhs args)

244 |     mutual

245 |       wrhs : RawImp -> Core RawImp

246 |       wrhs (IPi fc c p n ty sc)

247 |           = pure $ IPi fc c p n !(wrhs ty) !(wrhs sc)

248 |       wrhs (ILam fc c p n ty sc)

249 |           = pure $ ILam fc c p n !(wrhs ty) !(wrhs sc)

250 |       wrhs (ILet fc lhsFC c n ty val sc)

251 |           = pure $ ILet fc lhsFC c n !(wrhs ty) !(wrhs val) !(wrhs sc)

252 |       wrhs (ICase fc opts sc ty clauses)

253 |           = pure $ ICase fc opts !(wrhs sc) !(wrhs ty) !(traverse wrhsC clauses)

254 |       wrhs (ILocal fc decls sc)

255 |           = pure $ ILocal fc decls !(wrhs sc) -- TODO!

256 |       wrhs (IUpdate fc upds tm)

257 |           = pure $ IUpdate fc upds !(wrhs tm) -- TODO!

258 |       wrhs (IApp fc f a)

259 |           = pure $ IApp fc !(wrhs f) !(wrhs a)

260 |       wrhs (IAutoApp fc f a)

261 |           = pure $ IAutoApp fc !(wrhs f) !(wrhs a)

262 |       wrhs (INamedApp fc f n a)

263 |           = pure $ INamedApp fc !(wrhs f) n !(wrhs a)

264 |       wrhs (IWithApp fc f a) = updateWith fc f [a]

265 |       wrhs (IRewrite fc rule tm) = pure $ IRewrite fc !(wrhs rule) !(wrhs tm)

266 |       wrhs (IDelayed fc r tm) = pure $ IDelayed fc r !(wrhs tm)

267 |       wrhs (IDelay fc tm) = pure $ IDelay fc !(wrhs tm)

268 |       wrhs (IForce fc tm) = pure $ IForce fc !(wrhs tm)

269 |       wrhs tm = pure tm

271 |       wrhsC : ImpClause -> Core ImpClause

272 |       wrhsC (PatClause fc lhs rhs) = pure $ PatClause fc lhs !(wrhs rhs)

273 |       wrhsC c = pure c