0 | module Language.Reflection.Expr

  2 | import public Control.Applicative.Const -- public due to compiler's bug #2439

  4 | import public Data.Bits -- public due to compiler's bug #2439

  5 | import public Data.Cozippable -- public due to compiler's bug #2439

  6 | import public Data.Fin.Set

  7 | import public Data.Fin.ToFin -- public due to compiler's bug #2439

  8 | import public Data.List.Ex -- public due to compiler's bug #2439

  9 | import public Data.List.Quantifiers

 10 | import public Data.SortedSet

 11 | import public Data.These -- public due to compiler's bug #2439

 12 | import public Data.Vect.Dependent

 14 | import public Language.Reflection

 15 | import public Language.Reflection.Syntax

 16 | import Language.Reflection.Syntax.Ops

 18 | import public Syntax.IHateParens.List

 20 | %default total

 26 | public export

 27 | data IsNamedArg : Arg -> Type where

 28 |   ItIsNamed : IsNamedArg $ MkArg cnt pii (Just n) ty

 30 | public export

 31 | isNamedArg : (arg : Arg) -> Dec $ IsNamedArg arg

 32 | isNamedArg (MkArg count piInfo (Just x) type) = Yes ItIsNamed

 33 | isNamedArg (MkArg count piInfo Nothing type)  = No $ \case ItIsNamed impossible

 39 | public export

 40 | stname : Maybe Name -> Name

 41 | stname = fromMaybe $ UN Underscore

 43 | public export

 44 | argName : (a : Arg) -> (0 _ : IsNamedArg a) => Name

 45 | argName (MkArg _ _ Nothing _) impossible

 46 | argName (MkArg _ _ (Just x) _) = x

 48 | public export

 49 | argName' : Arg -> Name

 50 | argName' = stname . (.name)

 53 | cleanupNamedHoles : TTImp -> TTImp

 54 | cleanupNamedHoles = mapTTImp $ \case

 55 |   IHole {} => implicitFalse

 56 |   e        => e

 59 | public export

 60 | cleanupArg : Arg -> Arg

 61 | cleanupArg = { type $= cleanupNamedHoles, piInfo $= map cleanupNamedHoles }

 64 | argNames : (l : List Arg) -> (0 _ : All IsNamedArg l) => List Name

 65 | argNames [] = []

 66 | argNames (x :: xs) @{_ :: _} = Expr.argName x :: argNames xs

 73 | normaliseAs' : Elaboration m =>

 74 |                (0 expected : Type) ->

 75 |                (preProcess : TTImp -> TTImp) ->

 76 |                {0 resulting : _} -> (0 postProcess : (x : expected) -> resulting x) ->

 77 |                TTImp -> m TTImp

 78 | normaliseAs' expected pre post expr = do

 79 |   let expr = cleanupNamedHoles expr

 80 |   expr' <- quote $ post !(check {expected} $ pre expr)

 81 |   let (args, _) = unPi expr

 82 |   let (args', ty) = unPi expr'

 83 |   let args'' = comergeWith (\pre => {name := pre.name}) args args'

 84 |   pure $ piAll ty args''

 86 | public export %inline

 87 | normaliseAs : Elaboration m => (0 expected : Type) -> TTImp -> m TTImp

 88 | normaliseAs ty = normaliseAs' ty id id

 91 | public export %inline

 92 | normalise : Elaboration m => TTImp -> m TTImp

 93 | normalise = normaliseAs' (ty ** ty) (\expr => `((_ ** ~expr))) snd

 96 | public export %inline

 97 | normaliseAsType : Elaboration m => TTImp -> m TTImp

 98 | normaliseAsType = normaliseAs Type

104 | public export

105 | data AnyApp

106 |   = PosApp TTImp

107 |   | NamedApp Name TTImp

108 |   | AutoApp TTImp

109 |   | WithApp TTImp

111 | public export

112 | appArg : Arg -> TTImp -> AnyApp

113 | appArg (MkArg {piInfo=ExplicitArg, _})         expr = PosApp expr

114 | appArg (MkArg {piInfo=ImplicitArg, name, _})   expr = NamedApp (stname name) expr

115 | appArg (MkArg {piInfo=DefImplicit _, name, _}) expr = NamedApp (stname name) expr

116 | appArg (MkArg {piInfo=AutoImplicit, _})        expr = AutoApp expr

118 | public export

119 | getExpr : AnyApp -> TTImp

120 | getExpr $ PosApp e     = e

121 | getExpr $ NamedApp _ e = e

122 | getExpr $ AutoApp e    = e

123 | getExpr $ WithApp e    = e

126 | public export

127 | mapExpr : (TTImp -> TTImp) -> AnyApp -> AnyApp

128 | mapExpr f $ PosApp e     = PosApp $ f e

129 | mapExpr f $ NamedApp n e = NamedApp n $ f e

130 | mapExpr f $ AutoApp e    = AutoApp $ f e

131 | mapExpr f $ WithApp e    = WithApp $ f e

133 | public export

134 | unAppAny : TTImp -> (TTImp, List AnyApp)

135 | unAppAny = runTR [] where

136 |   runTR : List AnyApp -> TTImp -> (TTImp, List AnyApp)

137 |   runTR curr $ IApp      _ lhs   rhs = runTR (PosApp rhs     :: curr) lhs

138 |   runTR curr $ INamedApp _ lhs n rhs = runTR (NamedApp n rhs :: curr) lhs

139 |   runTR curr $ IAutoApp  _ lhs   rhs = runTR (AutoApp rhs    :: curr) lhs

140 |   runTR curr $ IWithApp  _ lhs   rhs = runTR (WithApp rhs    :: curr) lhs

141 |   runTR curr lhs                     = (lhs, curr)

143 | public export

144 | reAppAny1 : TTImp -> AnyApp -> TTImp

145 | reAppAny1 l $ PosApp e     = app l e

146 | reAppAny1 l $ NamedApp n e = namedApp l n e

147 | reAppAny1 l $ AutoApp e    = autoApp l e

148 | reAppAny1 l $ WithApp e    = IWithApp EmptyFC l e

150 | public export %inline

151 | reAppAny : Foldable f => TTImp -> f AnyApp -> TTImp

152 | reAppAny = foldl reAppAny1

161 | public export

162 | record AllApps where

163 |   constructor MkAllApps

164 |   explicitArgs : List TTImp

165 |   autoArgs : List TTImp

166 |   namedArgs : SortedMap Name TTImp

169 | public export

170 | addApp : AnyApp -> AllApps -> AllApps

171 | addApp (PosApp s) = {explicitArgs $= (s ::)}

172 | addApp (NamedApp nm s) = {namedArgs $= insert nm s}

173 | addApp (AutoApp s) = {autoArgs $= (s ::)}

174 | addApp (WithApp s) = id

179 | public export

180 | mkAllApps : List AnyApp -> AllApps

181 | mkAllApps laa = foldl (flip addApp) (MkAllApps [] [] empty) $ reverse laa

186 | public export

187 | popNamed : Maybe Name -> AllApps -> Maybe (TTImp, AllApps)

188 | popNamed Nothing ap = Nothing

189 | popNamed (Just x) ap =

190 |   case lookup x ap.namedArgs of

191 |     Nothing => Nothing

192 |     Just t => Just (t, {namedArgs $= delete x} ap)

197 | public export

198 | popArgVal : Arg -> AllApps -> Maybe (TTImp, AllApps)

199 | popArgVal (MkArg _ ImplicitArg name _) ap = popNamed name ap

200 | popArgVal (MkArg _ ExplicitArg name _) (MkAllApps (x :: xs) autoArgs namedArgs) = Just (x, MkAllApps xs autoArgs namedArgs)

201 | popArgVal (MkArg _ ExplicitArg name _) ap = popNamed name ap

202 | popArgVal (MkArg _ AutoImplicit name _) (MkAllApps explicitArgs (x :: xs) namedArgs) = Just (x, MkAllApps explicitArgs xs namedArgs)

203 | popArgVal (MkArg _ AutoImplicit name _) ap = popNamed name ap

204 | popArgVal (MkArg _ (DefImplicit x) Nothing _) ap = Just (x, ap)

205 | popArgVal (MkArg _ (DefImplicit x) (Just n) _) ap =

206 |   case lookup n ap.namedArgs of

207 |     Nothing => Just (x, ap)

208 |     Just t => Just (t , {namedArgs $= delete n} ap)

211 | public export

212 | popArgVals : List Arg -> AllApps -> List (Maybe TTImp)

213 | popArgVals [] aa = []

214 | popArgVals (x :: xs) aa = do

215 |   let pav = popArgVal x aa

216 |   let mr = fst <$> pav

217 |   let aa = fromMaybe aa $ snd <$> pav

218 |   mr :: popArgVals xs aa

225 | public export

226 | liftList : Foldable f => f TTImp -> TTImp

227 | liftList = foldr (\l, r => `(~l :: ~r)) `([])

230 | public export

231 | liftList' : Foldable f => f TTImp -> TTImp

232 | liftList' = foldr (\l, r => `(Prelude.(::) ~l ~r)) `(Prelude.Nil)

237 | public export

238 | applySyn : TTImp -> TTImp -> TTImp

239 | applySyn (ILam _ _ _ Nothing  _ lamExpr) _ = lamExpr

240 | applySyn (ILam _ _ _ (Just n) _ lamExpr) rhs = mapTTImp (\case orig@(IVar _ n') => if n == n' then rhs else orig; e => e) lamExpr

241 | applySyn lhs rhs = lhs `app` rhs

245 | public export

246 | unDPair : TTImp -> (List Arg, TTImp)

247 | unDPair (IApp _ (IApp _ (IVar _ `{Builtin.DPair.DPair}) typ) (ILam _ cnt piInfo mbname _ lamTy)) =

248 |     mapFst (MkArg cnt piInfo mbname typ ::) $ unDPair lamTy

249 | unDPair expr = ([], expr)

251 | public export

252 | unDPairUnAlt : TTImp -> Maybe (List Arg, TTImp)

253 | unDPairUnAlt (IAlternative _ _ alts) = case filter (not . null . Builtin.fst) $ unDPair <$> alts of

254 |   [x] => Just x

255 |   _   => Nothing

256 | unDPairUnAlt x = Just $ unDPair x

258 | public export

259 | buildDPair : (rhs : TTImp) -> List (Name, TTImp) -> TTImp

260 | buildDPair = foldr $ \(name, type), res =>

261 |   var `{Builtin.DPair.DPair} .$ type .$ lam (MkArg MW ExplicitArg (Just name) type) res

271 | unNS : Name -> (List String, Name)

272 | unNS (NS (MkNS revNSs) nm) = mapFst (reverse revNSs ++) $ unNS nm

273 | unNS (DN _ nm)             = unNS nm

274 | unNS nm                    = ([], nm)

281 | allNameSuffixes : Name -> List Name

282 | allNameSuffixes nm = do

283 |   let (nss, n) = unNS nm

284 |   tails nss <&> \case

285 |     [] => n

286 |     ns => NS (MkNS $ reverse ns) n

289 | isNamespaced : Name -> Bool

290 | isNamespaced = not . null . fst . unNS

292 | public export

293 | isImplicit : PiInfo c -> Bool

294 | isImplicit ImplicitArg     = True

295 | isImplicit (DefImplicit x) = True

296 | isImplicit AutoImplicit    = True

297 | isImplicit ExplicitArg     = False

303 | public export

304 | isSameTypeAs : Name -> Name -> Elab Bool

305 | isSameTypeAs n m = let eq = (==) `on` fst in [| lookupName n `eq` lookupName m |]

308 | nameConformsTo : (cand, origin : Name) -> Bool

309 | nameConformsTo cand origin = do

310 |   let (cns, cn) = simplify cand

311 |   let (ons, on) = simplify origin

312 |   cn == on && (cns `isPrefixOf` ons) -- notice that namespaces are stored in the reverse order

313 |   where

314 |     simplify : Name -> (List String, Name)

315 |     simplify (NS (MkNS ns) nm) = mapFst (++ ns) $ simplify nm

316 |     simplify (DN _ nm)         = simplify nm

317 |     simplify x                 = ([], x)

319 | 0 nct_corr_eq : nameConformsTo `{A.B.c} `{A.B.c} = True;  nct_corr_eq = Refl

320 | 0 nct_corr_le : nameConformsTo `{B.c}   `{A.B.c} = True;  nct_corr_le = Refl

321 | 0 nct_corr_ge : nameConformsTo `{A.B.c} `{B.c}   = False; nct_corr_ge = Refl

325 | allVarNames' : TTImp -> SortedSet Name

326 | allVarNames' = runConst . mapATTImp' f where

327 |   f : TTImp -> Const (SortedSet Name) TTImp -> Const (SortedSet Name) TTImp

328 |   f (IVar _ n) = const $ MkConst $ singleton n

329 |   f _          = id

333 | allVarNames : TTImp -> List Name

334 | allVarNames = Prelude.toList . allVarNames'

336 | public export

337 | isVar : TTImp -> Bool

338 | isVar $ IVar {} = True

339 | isVar _         = False

341 | public export

342 | 0 ArgDeps : Nat -> Type

343 | ArgDeps n = DVect n $ FinSet . Fin.finToNat

346 | argDeps : (args : List Arg) -> ArgDeps args.length

347 | argDeps args = do

348 |   let nameToIndices = SortedMap.fromList $ mapI args $ \i, arg => (argName' arg, Fin.Set.singleton i)

349 |   let args = Vect.fromList args <&> \arg => allVarNames arg.type <&> fromMaybe empty . lookup' nameToIndices

350 |   flip upmapI args $ \i, deps => flip concatMap deps $ \candidates =>

351 |     maybe empty singleton $ last' $ mapMaybe tryToFit $ Fin.Set.toList candidates

354 | dependees : (args : List Arg) -> FinSet args.length

355 | dependees args = do

356 |   let nameToIndex = SortedMap.fromList $ mapI args $ \i, arg => (argName' arg, i)

357 |   let varsInTypes = concatMap (\arg => allVarNames' arg.type) args

358 |   fromList $ mapMaybe (lookup' nameToIndex) $ Prelude.toList varsInTypes

360 | namespace UpToRenaming

362 |   mutual

364 |     compWithSubst : (subst : List $ These Name Name) => (from, to : Maybe Name) -> TTImp -> TTImp -> Bool

365 |     compWithSubst (Just n) (Just n') e e' = n == n' && (e == e') @{UpToSubst} || (e == e') @{UpToSubst @{Both n n' :: subst}}

366 |     compWithSubst (Just n) Nothing   e e' = (e == e') @{UpToSubst @{This n  :: subst}}

367 |     compWithSubst Nothing  (Just n') e e' = (e == e') @{UpToSubst @{That n' :: subst}}

368 |     compWithSubst Nothing  Nothing   e e' = (e == e') @{UpToSubst}

370 |     [UpToSubst] (subst : List $ These Name Name) => Eq TTImp where

371 |       IVar _ v == IVar _ v' = maybe (v == v') (== Both v v') $ flip find subst $ \ior => fromThis ior == Just v || fromThat ior == Just v'

372 |       IPi _ c i n a r == IPi _ c' i' n' a' r' =

373 |         c == c' && (assert_total $ i == i') && a == a' && (assert_total $ compWithSubst n n' r r')

374 |       ILam _ c i n a r == ILam _ c' i' n' a' r' =

375 |         c == c' && (assert_total $ i == i') && a == a' && (assert_total $ compWithSubst n n' r r')

376 |       ILet _ _ c n ty val s == ILet _ _ c' n' ty' val' s' =

377 |         c == c' && ty == ty' && val == val' && (assert_total $ compWithSubst (Just n) (Just n') s s')

379 |       ICase _ os t ty cs == ICase _ os' t' ty' cs' =

380 |         t == t' && (assert_total $ os == os') && ty == ty' && (assert_total $ cs == cs')

381 |       ILocal _ ds e == ILocal _ ds' e' =

382 |         (assert_total $ ds == ds') && e == e'

383 |       IUpdate _ fs t == IUpdate _ fs' t' =

384 |         (assert_total $ fs == fs') && t == t'

386 |       IApp _ f x == IApp _ f' x' = f == f' && x == x'

387 |       INamedApp _ f n x == INamedApp _ f' n' x' =

388 |         f == f' && n == n' && x == x'

389 |       IAutoApp _ f x == IAutoApp _ f' x' = f == f' && x == x'

390 |       IWithApp _ f x == IWithApp _ f' x' = f == f' && x == x'

392 |       ISearch _ n == ISearch _ n' = n == n'

393 |       IAlternative _ t as == IAlternative _ t' as' =

394 |         (assert_total $ t == t') && (assert_total $ as == as')

395 |       IRewrite _ p q == IRewrite _ p' q' =

396 |         p == p' && q == q'

398 |       IBindHere _ m t == IBindHere _ m' t' =

399 |         m == m' && t == t'

400 |       IBindVar _ s == IBindVar _ s' = s == s'

401 |       IAs _ _ u n t == IAs _ _ u' n' t' =

402 |         u == u' && n == n' && t == t'

403 |       IMustUnify _ r t == IMustUnify _ r' t' =

404 |         r == r' && t == t'

406 |       IDelayed _ r t == IDelayed _ r' t' = r == r' && t == t'

407 |       IDelay _ t == IDelay _ t' = t == t'

408 |       IForce _ t == IForce _ t' = t == t'

410 |       IQuote _ tm == IQuote _ tm' = tm == tm'

411 |       IQuoteName _ n == IQuoteName _ n' = n == n'

412 |       IQuoteDecl _ ds == IQuoteDecl _ ds' = assert_total $ ds == ds'

413 |       IUnquote _ tm == IUnquote _ tm' = tm == tm'

415 |       IPrimVal _ c == IPrimVal _ c' = c == c'

416 |       IType _ == IType _ = True

417 |       IHole _ s == IHole _ s' = True -- Holes are anyway unique and does not matter what the names are.

419 |       Implicit _ b == Implicit _ b' = b == b'

420 |       IWithUnambigNames _ ns t == IWithUnambigNames _ ns' t' =

421 |         map snd ns == map snd ns' && t == t'

423 |       _ == _ = False

425 |   export

426 |   [UpToRenaming] Eq TTImp where

427 |     x == y = (x == y) @{UpToSubst @{empty}}