0 | module Core.Normalise.Convert

  2 | import public Core.Normalise.Eval

  3 | import public Core.Normalise.Quote

  5 | import Core.Case.CaseTree

  6 | import Core.Context

  7 | import Core.Env

  8 | import Core.Value

 10 | import Libraries.Data.NatSet

 11 | import Libraries.Data.List.SizeOf

 13 | %default covering

 15 | public export

 16 | interface Convert tm where

 17 |   convert : {auto c : Ref Ctxt Defs} ->

 18 |             {vars : Scope} ->

 19 |             Defs -> Env Term vars ->

 20 |             tm vars -> tm vars -> Core Bool

 21 |   convertInf : {auto c : Ref Ctxt Defs} ->

 22 |                {vars : Scope} ->

 23 |                Defs -> Env Term vars ->

 24 |                tm vars -> tm vars -> Core Bool

 26 |   convGen : {auto c : Ref Ctxt Defs} ->

 27 |             {vars : _} ->

 28 |             Ref QVar Int ->

 29 |             Bool -> -- skip forced arguments (must have checked the type

 30 |                     -- elsewhere first)

 31 |             Defs -> Env Term vars ->

 32 |             tm vars -> tm vars -> Core Bool

 34 |   convert defs env tm tm'

 35 |       = do q <- newRef QVar 0

 36 |            convGen q False defs env tm tm'

 38 |   convertInf defs env tm tm'

 39 |       = do q <- newRef QVar 0

 40 |            convGen q True defs env tm tm'

 42 | tryUpdate : {vars, vars' : _} ->

 43 |             List (Var vars, Var vars') ->

 44 |             Term vars -> Maybe (Term vars')

 45 | tryUpdate ms (Local fc l idx p)

 46 |     = do MkVar p' <- findIdx ms (MkVar p)

 47 |          pure $ Local fc l _ p'

 48 |   where

 49 |     findIdx : List (Var vars, Var vars') -> Var vars -> Maybe (Var vars')

 50 |     findIdx [] _ = Nothing

 51 |     findIdx ((old, v) :: ps) n

 52 |         = if old == n then Just v else findIdx ps n

 53 | tryUpdate ms (Ref fc nt n) = pure $ Ref fc nt n

 54 | tryUpdate ms (Meta fc n i args) = pure $ Meta fc n i !(traverse (tryUpdate ms) args)

 55 | tryUpdate ms (Bind fc x b sc)

 56 |     = do b' <- tryUpdateB b

 57 |          pure $ Bind fc x b' !(tryUpdate (map weakenP ms) sc)

 58 |   where

 59 |     tryUpdatePi : PiInfo (Term vars) -> Maybe (PiInfo (Term vars'))

 60 |     tryUpdatePi Explicit = pure Explicit

 61 |     tryUpdatePi Implicit = pure Implicit

 62 |     tryUpdatePi AutoImplicit = pure AutoImplicit

 63 |     tryUpdatePi (DefImplicit t) = pure $ DefImplicit !(tryUpdate ms t)

 65 |     tryUpdateB : Binder (Term vars) -> Maybe (Binder (Term vars'))

 66 |     tryUpdateB (Lam fc r p t) = pure $ Lam fc r !(tryUpdatePi p) !(tryUpdate ms t)

 67 |     tryUpdateB (Let fc r v t) = pure $ Let fc r !(tryUpdate ms v) !(tryUpdate ms t)

 68 |     tryUpdateB (Pi fc r p t) = pure $ Pi fc r !(tryUpdatePi p) !(tryUpdate ms t)

 69 |     tryUpdateB _ = Nothing

 71 |     weakenP : {n : _} -> (Var vars, Var vars') ->

 72 |               (Var (n :: vars), Var (n :: vars'))

 73 |     weakenP (v, vs) = (weaken v, weaken vs)

 74 | tryUpdate ms (App fc f a) = pure $ App fc !(tryUpdate ms f) !(tryUpdate ms a)

 75 | tryUpdate ms (As fc s a p) = pure $ As fc s !(tryUpdate ms a) !(tryUpdate ms p)

 76 | tryUpdate ms (TDelayed fc r tm) = pure $ TDelayed fc r !(tryUpdate ms tm)

 77 | tryUpdate ms (TDelay fc r ty tm) = pure $ TDelay fc r !(tryUpdate ms ty) !(tryUpdate ms tm)

 78 | tryUpdate ms (TForce fc r tm) = pure $ TForce fc r !(tryUpdate ms tm)

 79 | tryUpdate ms (PrimVal fc c) = pure $ PrimVal fc c

 80 | tryUpdate ms (Erased fc a) = Erased fc <$> traverse (tryUpdate ms) a

 81 | tryUpdate ms (TType fc u) = pure $ TType fc u

 84 |   allConvNF : {auto c : Ref Ctxt Defs} ->

 85 |               {vars : _} ->

 86 |               Ref QVar Int -> Bool -> Defs -> Env Term vars ->

 87 |               List (NF vars) -> List (NF vars) -> Core Bool

 88 |   allConvNF q i defs env [] [] = pure True

 89 |   allConvNF q i defs env (x :: xs) (y :: ys)

 90 |       = do ok <- allConvNF q i defs env xs ys

 91 |            if ok then convGen q i defs env x y

 92 |                  else pure False

 93 |   allConvNF q i defs env _ _ = pure False

 95 |   -- return False if anything differs at the head, to quickly find

 96 |   -- conversion failures without going deeply into all the arguments.

 97 |   -- True means they might still match

 98 |   quickConv : List (NF vars) -> List (NF vars) -> Bool

 99 |   quickConv [] [] = True

100 |   quickConv (x :: xs) (y :: ys) = quickConvArg x y && quickConv xs ys

101 |     where

102 |       quickConvHead : NHead vars -> NHead vars -> Bool

103 |       quickConvHead (NLocal {}) (NLocal {}) = True

104 |       quickConvHead (NRef _ n) (NRef _ n') = n == n'

105 |       quickConvHead (NMeta n _ _) (NMeta n' _ _) = n == n'

106 |       quickConvHead _ _ = False

108 |       quickConvArg : NF vars -> NF vars -> Bool

109 |       quickConvArg (NBind {}) _ = True -- let's not worry about eta here...

110 |       quickConvArg _ (NBind {}) = True

111 |       quickConvArg (NApp _ h _) (NApp _ h' _) = quickConvHead h h'

112 |       quickConvArg (NDCon _ _ t _ _) (NDCon _ _ t' _ _) = t == t'

113 |       quickConvArg (NTCon _ n _ _) (NTCon _ n' _ _) = n == n'

114 |       quickConvArg (NAs _ _ _ t) (NAs _ _ _ t') = quickConvArg t t'

115 |       quickConvArg (NDelayed _ _ t) (NDelayed _ _ t') = quickConvArg t t'

116 |       quickConvArg (NDelay {}) (NDelay {}) = True

117 |       quickConvArg (NForce _ _ t _) (NForce _ _ t' _) = quickConvArg t t'

118 |       quickConvArg (NPrimVal _ c) (NPrimVal _ c') = c == c'

119 |       quickConvArg (NType {}) (NType {}) = True

120 |       quickConvArg (NErased {}) _ = True

121 |       quickConvArg _ (NErased {}) = True

122 |       quickConvArg _ _ = False

123 |   quickConv _ _ = False

125 |   allConv : {auto c : Ref Ctxt Defs} ->

126 |             {vars : _} ->

127 |             Ref QVar Int -> Bool -> Defs -> Env Term vars ->

128 |             List (Closure vars) -> List (Closure vars) -> Core Bool

129 |   allConv q i defs env xs ys

130 |       = do xsnf <- traverse (evalClosure defs) xs

131 |            ysnf <- traverse (evalClosure defs) ys

132 |            if quickConv xsnf ysnf

133 |               then allConvNF q i defs env xsnf ysnf

134 |               else pure False

136 |   -- If the case trees match in structure, get the list of variables which

137 |   -- have to match in the call

138 |   getMatchingVarAlt : {auto c : Ref Ctxt Defs} ->

139 |                       {args, args' : _} ->

140 |                       Defs ->

141 |                       List (Var args, Var args') ->

142 |                       CaseAlt args -> CaseAlt args' ->

143 |                       Core (Maybe (List (Var args, Var args')))

144 |   getMatchingVarAlt defs ms (ConCase n tag cargs t) (ConCase n' tag' cargs' t')

145 |       = if n == n'

146 |            then do let Just ms' = extend cargs cargs' ms

147 |                         | Nothing => pure Nothing

148 |                    Just ms <- getMatchingVars defs ms' t t'

149 |                         | Nothing => pure Nothing

150 |                    -- drop the prefix from cargs/cargs' since they won't

151 |                    -- be in the caller

152 |                    pure (Just (mapMaybe (dropP (mkSizeOf cargs) (mkSizeOf cargs')) ms))

153 |            else pure Nothing

154 |     where

155 |       weakenP : {0 c, c' : _} -> {0 args, args' : Scope} ->

156 |                 (Var args, Var args') ->

157 |                 (Var (c :: args), Var (c' :: args'))

158 |       weakenP (v, vs) = (weaken v, weaken vs)

160 |       extend : (cs : List Name) -> (cs' : List Name) ->

161 |                (List (Var args, Var args')) ->

162 |                Maybe (List (Var (cs ++ args), Var (cs' ++ args')))

163 |       extend [] [] ms = pure ms

164 |       extend (c :: cs) (c' :: cs') ms

165 |           = do rest <- extend cs cs' ms

166 |                pure ((first, first) :: map weakenP rest)

167 |       extend _ _ _ = Nothing

169 |       dropP : SizeOf cs -> SizeOf cs' ->

170 |               (Var (cs ++ args), Var (cs' ++ args')) ->

171 |               Maybe (Var args, Var args')

172 |       dropP cs cs' (x, y) = pure (!(strengthenNs cs x), !(strengthenNs cs' y))

174 |   getMatchingVarAlt defs ms (ConstCase c t) (ConstCase c' t')

175 |       = if c == c'

176 |            then getMatchingVars defs ms t t'

177 |            else pure Nothing

178 |   getMatchingVarAlt defs ms (DefaultCase t) (DefaultCase t')

179 |       = getMatchingVars defs ms t t'

180 |   getMatchingVarAlt defs _ _ _ = pure Nothing

182 |   getMatchingVarAlts : {auto c : Ref Ctxt Defs} ->

183 |                        {args, args' : _} ->

184 |                        Defs ->

185 |                        List (Var args, Var args') ->

186 |                        List (CaseAlt args) -> List (CaseAlt args') ->

187 |                        Core (Maybe (List (Var args, Var args')))

188 |   getMatchingVarAlts defs ms [] [] = pure (Just ms)

189 |   getMatchingVarAlts defs ms (a :: as) (a' :: as')

190 |       = do Just ms <- getMatchingVarAlt defs ms a a'

191 |                 | Nothing => pure Nothing

192 |            getMatchingVarAlts defs ms as as'

193 |   getMatchingVarAlts defs _ _ _ = pure Nothing

195 |   getMatchingVars : {auto c : Ref Ctxt Defs} ->

196 |                     {args, args' : _} ->

197 |                     Defs ->

198 |                     List (Var args, Var args') ->

199 |                     CaseTree args -> CaseTree args' ->

200 |                     Core (Maybe (List (Var args, Var args')))

201 |   getMatchingVars defs ms (Case _ p _ alts) (Case _ p' _ alts')

202 |       = getMatchingVarAlts defs ((MkVar p, MkVar p') :: ms) alts alts'

203 |   getMatchingVars defs ms (STerm i tm) (STerm i' tm')

204 |       = do let Just tm'' = tryUpdate ms tm

205 |                | Nothing => pure Nothing

206 |            if !(convert defs (mkEnv (getLoc tm) args') tm'' tm')

207 |               then pure (Just ms)

208 |               else pure Nothing

209 |   getMatchingVars defs ms (Unmatched _) (Unmatched _) = pure (Just ms)

210 |   getMatchingVars defs ms Impossible Impossible = pure (Just ms)

211 |   getMatchingVars _ _ _ _ = pure Nothing

213 |   chkSameDefs : {auto c : Ref Ctxt Defs} ->

214 |                 {vars : _} ->

215 |                 Ref QVar Int -> Bool -> Defs -> Env Term vars ->

216 |                 Name -> Name ->

217 |                 List (Closure vars) -> List (Closure vars) -> Core Bool

218 |   chkSameDefs q i defs env n n' nargs nargs'

219 |      = do Just (PMDef _ args ct rt _) <- lookupDefExact n (gamma defs)

220 |                | _ => pure False

221 |           Just (PMDef _ args' ct' rt' _) <- lookupDefExact n' (gamma defs)

222 |                | _ => pure False

224 |           -- If the two case blocks match in structure, get which variables

225 |           -- correspond. If corresponding variables convert, the two case

226 |           -- blocks convert.

227 |           Just ms <- getMatchingVars defs [] ct ct'

228 |                | Nothing => pure False

229 |           convertMatches ms

230 |      where

231 |        -- We've only got the index into the argument list, and the indices

232 |        -- don't match up, which is annoying. But it'll always be there!

233 |        getArgPos : Nat -> List (Closure vars) -> Maybe (Closure vars)

234 |        getArgPos _ [] = Nothing

235 |        getArgPos Z (c :: cs) = pure c

236 |        getArgPos (S k) (c :: cs) = getArgPos k cs

238 |        convertMatches : {vs, vs' : _} ->

239 |                         List (Var vs, Var vs') ->

240 |                         Core Bool

241 |        convertMatches [] = pure True

242 |        convertMatches ((MkVar {varIdx = ix} p, MkVar {varIdx = iy} p') :: vs)

243 |           = do let Just varg = getArgPos ix nargs

244 |                    | Nothing => pure False

245 |                let Just varg' = getArgPos iy nargs'

246 |                    | Nothing => pure False

247 |                pure $ !(convGen q i defs env varg varg') &&

248 |                       !(convertMatches vs)

250 |   -- If two names are standing for case blocks, check the blocks originate

251 |   -- from the same place, and have the same scrutinee

252 |   chkConvCaseBlock : {auto c : Ref Ctxt Defs} ->

253 |                      {vars : _} ->

254 |                      FC -> Ref QVar Int -> Bool -> Defs -> Env Term vars ->

255 |                      NHead vars -> List (Closure vars) ->

256 |                      NHead vars -> List (Closure vars) -> Core Bool

257 |   chkConvCaseBlock fc q i defs env (NRef _ n) nargs (NRef _ n') nargs'

258 |       = do NS _ (CaseBlock {}) <- full (gamma defs) n

259 |               | _ => pure False

260 |            NS _ (CaseBlock {}) <- full (gamma defs) n'

261 |               | _ => pure False

262 |            False <- chkSameDefs q i defs env n n' nargs nargs'

263 |               | True => pure True

264 |            -- both case operators. Due to the way they're elaborated, two

265 |            -- blocks might arise from the same source but have different

266 |            -- names. So we consider them the same if the scrutinees convert,

267 |            -- and the functions are defined at the same location. This is a

268 |            -- bit of a hack - and relies on the location being stored in the

269 |            -- term accurately - but otherwise it's a quick way to find out!

270 |            Just def <- lookupCtxtExact n (gamma defs)

271 |                 | _ => pure False

272 |            Just def' <- lookupCtxtExact n' (gamma defs)

273 |                 | _ => pure False

274 |            let PMDef _ _ tree _ _ = definition def

275 |                 | _ => pure False

276 |            let PMDef _ _ tree' _ _ = definition def'

277 |                 | _ => pure False

278 |            let Just scpos = findArgPos tree

279 |                 | Nothing => pure False

280 |            let Just scpos' = findArgPos tree'

281 |                 | Nothing => pure False

282 |            let Just sc = getScrutinee scpos nargs

283 |                 | Nothing => pure False

284 |            let Just sc' = getScrutinee scpos' nargs'

285 |                 | Nothing => pure False

286 |            ignore $ convGen q i defs env sc sc'

287 |            pure (location def == location def')

288 |     where

289 |       -- Need to find the position of the scrutinee to see if they are the

290 |       -- same

291 |       findArgPos : CaseTree as -> Maybe Nat

292 |       findArgPos (Case idx p _ _) = Just idx

293 |       findArgPos _ = Nothing

295 |       getScrutinee : Nat -> List (Closure vs) -> Maybe (Closure vs)

296 |       getScrutinee Z (x :: xs) = Just x

297 |       getScrutinee (S k) (x :: xs) = getScrutinee k xs

298 |       getScrutinee _ _ = Nothing

299 |   chkConvCaseBlock _ _ _ _ _ _ _ _ _ = pure False

301 |   chkConvHead : {auto c : Ref Ctxt Defs} ->

302 |                 {vars : _} ->

303 |                 Ref QVar Int -> Bool -> Defs -> Env Term vars ->

304 |                 NHead vars -> NHead vars -> Core Bool

305 |   chkConvHead q i defs env (NLocal _ idx _) (NLocal _ idx' _) = pure $ idx == idx'

306 |   chkConvHead q i defs env (NRef _ n) (NRef _ n') = pure $ n == n'

307 |   chkConvHead q inf defs env (NMeta n i args) (NMeta n' i' args')

308 |      = if i == i'

309 |           then allConv q inf defs env args args'

310 |           else pure False

311 |   chkConvHead q i defs env _ _ = pure False

313 |   convPiInfo : {auto c : Ref Ctxt Defs} ->

314 |                {vars : _} ->

315 |                Ref QVar Int -> Bool -> Defs -> Env Term vars ->

316 |                PiInfo (Closure vars) -> PiInfo (Closure vars) -> Core Bool

317 |   convPiInfo q i defs env Implicit Implicit = pure True

318 |   convPiInfo q i defs env Explicit Explicit = pure True

319 |   convPiInfo q i defs env AutoImplicit AutoImplicit = pure True

320 |   convPiInfo q i defs env (DefImplicit x) (DefImplicit y) = convGen q i defs env x y

321 |   convPiInfo q i defs env _ _ = pure False

323 |   convBinders : {auto c : Ref Ctxt Defs} ->

324 |                 {vars : _} ->

325 |                 Ref QVar Int -> Bool -> Defs -> Env Term vars ->

326 |                 Binder (Closure vars) -> Binder (Closure vars) -> Core Bool

327 |   convBinders q i defs env bx by

328 |     = if sameBinders bx by && multiplicity bx == multiplicity by

329 |          then allM id [ convPiInfo q i defs env (piInfo bx) (piInfo by)

330 |                       , convGen q i defs env (binderType bx) (binderType by)]

331 |          else pure False

332 |     where

333 |       sameBinders : Binder (Closure vars) -> Binder (Closure vars) -> Bool

334 |       sameBinders (Pi {}) (Pi {}) = True

335 |       sameBinders (Lam {}) (Lam {}) = True

336 |       sameBinders _ _ = False

338 |   export

339 |   Convert NF where

340 |     convGen q i defs env (NBind fc x b sc) (NBind _ x' b' sc')

341 |         = do var <- genName "conv"

342 |              let c = MkClosure defaultOpts LocalEnv.empty env (Ref fc Bound var)

343 |              bok <- convBinders q i defs env b b'

344 |              if bok

345 |                 then do bsc <- sc defs c

346 |                         bsc' <- sc' defs c

347 |                         convGen q i defs env bsc bsc'

348 |                 else pure False

350 |     convGen q i defs env tmx@(NBind fc x (Lam fc' c ix tx) scx) tmy

351 |         = do empty <- clearDefs defs

352 |              etay <- nf defs env

353 |                         (Bind fc x (Lam fc' c !(traverse (quote empty env) ix) !(quote empty env tx))

354 |                            (App fc (weaken !(quote empty env tmy))

355 |                                 (Local fc Nothing _ First)))

356 |              convGen q i defs env tmx etay

357 |     convGen q i defs env tmx tmy@(NBind fc y (Lam fc' c iy ty) scy)

358 |         = do empty <- clearDefs defs

359 |              etax <- nf defs env

360 |                         (Bind fc y (Lam fc' c !(traverse (quote empty env) iy) !(quote empty env ty))

361 |                            (App fc (weaken !(quote empty env tmx))

362 |                                 (Local fc Nothing _ First)))

363 |              convGen q i defs env etax tmy

365 |     convGen q inf defs env (NApp fc val args) (NApp _ val' args')

366 |         = if !(chkConvHead q inf defs env val val')

367 |              then do i <- getInfPos val

368 |                      allConv q inf defs env (drop i args1) (drop i args2)

369 |              else chkConvCaseBlock fc q inf defs env val args1 val' args2

370 |         where

371 |           getInfPos : NHead vars -> Core NatSet

372 |           getInfPos (NRef _ n)

373 |               = if inf

374 |                    then do Just gdef <- lookupCtxtExact n (gamma defs)

375 |                                 | _ => pure NatSet.empty

376 |                            pure (inferrable gdef)

377 |                    else pure NatSet.empty

378 |           getInfPos _ = pure NatSet.empty

380 |           -- Discard file context information irrelevant for conversion checking

381 |           args1 : List (Closure vars)

382 |           args1 = map snd args

384 |           args2 : List (Closure vars)

385 |           args2 = map snd args'

387 |     convGen q i defs env (NDCon _ nm tag _ args) (NDCon _ nm' tag' _ args')

388 |         = if tag == tag'

389 |              then allConv q i defs env (map snd args) (map snd args')

390 |              else pure False

391 |     convGen q i defs env (NTCon _ nm _ args) (NTCon _ nm' _ args')

392 |         = if nm == nm'

393 |              then allConv q i defs env (map snd args) (map snd args')

394 |              else pure False

395 |     convGen q i defs env (NAs _ _ _ tm) (NAs _ _ _ tm')

396 |         = convGen q i defs env tm tm'

398 |     convGen q i defs env (NDelayed _ r arg) (NDelayed _ r' arg')

399 |         = if compatible r r'

400 |              then convGen q i defs env arg arg'

401 |              else pure False

402 |     convGen q i defs env (NDelay _ r _ arg) (NDelay _ r' _ arg')

403 |         = if compatible r r'

404 |              then do -- if it's codata, don't reduce the argument or we might

405 |                      -- go for ever, if it's infinite

406 |                      adefs <- case r of

407 |                                    LLazy => pure defs

408 |                                    _ => clearDefs defs

409 |                      convGen q i adefs env arg arg'

410 |              else pure False

411 |     convGen q i defs env (NForce _ r arg args) (NForce _ r' arg' args')

412 |         = if compatible r r'

413 |              then if !(convGen q i defs env arg arg')

414 |                      then allConv q i defs env (map snd args) (map snd args')

415 |                      else pure False

416 |              else pure False

418 |     convGen q i defs env (NPrimVal _ c) (NPrimVal _ c') = pure (c == c')

419 |     convGen q i defs env (NErased _ (Dotted t)) u = convGen q i defs env t u

420 |     convGen q i defs env t (NErased _ (Dotted u)) = convGen q i defs env t u

421 |     convGen q i defs env (NErased {}) _ = pure True

422 |     convGen q i defs env _ (NErased {}) = pure True

423 |     convGen q i defs env (NType _ ul) (NType _ ur)

424 |         = -- TODO Cumulativity: Add constraint here

425 |           pure True

426 |     convGen q i defs env x y = pure False

428 |   export

429 |   Convert Term where

430 |     convGen q i defs env x y

431 |         = convGen q i defs env !(nf defs env x) !(nf defs env y)

433 |   export

434 |   Convert Closure where

435 |     convGen q i defs env x y

436 |         = convGen q i defs env !(evalClosure defs x) !(evalClosure defs y)