
   0 | module Language.Reflection.Expr
   1 | 
   2 | import public Control.Applicative.Const -- public due to compiler's bug #2439
   3 | 
   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
  13 | 
  14 | import public Language.Reflection
  15 | import public Language.Reflection.Syntax
  16 | import Language.Reflection.Syntax.Ops
  17 | 
  18 | import public Syntax.IHateParens.List
  19 | 
  20 | %default total
  21 | 
  22 | --------------------------
  23 | --- Namedness property ---
  24 | --------------------------
  25 | 
  26 | public export
  27 | data IsNamedArg : Arg -> Type where
  28 |   ItIsNamed : IsNamedArg $ MkArg cnt pii (Just n) ty
  29 | 
  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
  34 | 
  35 | ------------------------------------
  36 | --- General pure transformations ---
  37 | ------------------------------------
  38 | 
  39 | public export
  40 | stname : Maybe Name -> Name
  41 | stname = fromMaybe $ UN Underscore
  42 | 
  43 | public export
  44 | argName : (a : Arg) -> (0 _ : IsNamedArg a) => Name
  45 | argName (MkArg _ _ Nothing _) impossible
  46 | argName (MkArg _ _ (Just x) _) = x
  47 | 
  48 | public export
  49 | argName' : Arg -> Name
  50 | argName' = stname . (.name)
  51 | 
  52 | export
  53 | cleanupNamedHoles : TTImp -> TTImp
  54 | cleanupNamedHoles = mapTTImp $ \case
  55 |   IHole {} => implicitFalse
  56 |   e        => e
  57 | 
  58 | ||| Run `cleanupNamedHoles` over all `Arg`'s `TTImp`s
  59 | public export
  60 | cleanupArg : Arg -> Arg
  61 | cleanupArg = { type $= cleanupNamedHoles, piInfo $= map cleanupNamedHoles }
  62 | 
  63 | export
  64 | argNames : (l : List Arg) -> (0 _ : All IsNamedArg l) => List Name
  65 | argNames [] = []
  66 | argNames (x :: xs) @{_ :: _} = Expr.argName x :: argNames xs
  67 | 
  68 | ----------------------------------------------
  69 | --- Compiler-based `TTImp` transformations ---
  70 | ----------------------------------------------
  71 | 
  72 | export
  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''
  85 | 
  86 | public export %inline
  87 | normaliseAs : Elaboration m => (0 expected : Type) -> TTImp -> m TTImp
  88 | normaliseAs ty = normaliseAs' ty id id
  89 | 
  90 | -- Normalises expression of any type; it is known to struggle with `let`s
  91 | public export %inline
  92 | normalise : Elaboration m => TTImp -> m TTImp
  93 | normalise = normaliseAs' (ty ** ty) (\expr => `((_ ** ~expr))) snd
  94 | 
  95 | -- More precise normalisation of type expressions
  96 | public export %inline
  97 | normaliseAsType : Elaboration m => TTImp -> m TTImp
  98 | normaliseAsType = normaliseAs Type
  99 | 
 100 | ------------------------------------------------------------------------
 101 | --- Facilities for managing any kind of function application at once ---
 102 | ------------------------------------------------------------------------
 103 | 
 104 | public export
 105 | data AnyApp
 106 |   = PosApp TTImp
 107 |   | NamedApp Name TTImp
 108 |   | AutoApp TTImp
 109 |   | WithApp TTImp
 110 | 
 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
 117 | 
 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
 124 | 
 125 | -- Shallow expression mapping
 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
 132 | 
 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)
 142 | 
 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
 149 | 
 150 | public export %inline
 151 | reAppAny : Foldable f => TTImp -> f AnyApp -> TTImp
 152 | reAppAny = foldl reAppAny1
 153 | 
 154 | ---------------------------------------
 155 | --- Building of special expressions ---
 156 | ---------------------------------------
 157 | 
 158 | ||| Lifts the given foldable of elements to an expression of a list-like data type
 159 | public export
 160 | liftList : Foldable f => f TTImp -> TTImp
 161 | liftList = foldr (\l, r => `(~l :: ~r)) `([])
 162 | 
 163 | ||| Lifts the given foldable of elements to an expression of `Prelude.List`
 164 | public export
 165 | liftList' : Foldable f => f TTImp -> TTImp
 166 | liftList' = foldr (\l, r => `(Prelude.(::) ~l ~r)) `(Prelude.Nil)
 167 | 
 168 | -- Apply syntactically, optimise if LHS is `ILam`.
 169 | -- This implementation does not take shadowing into account.
 170 | -- Also, currently, the type of lambda argument is not used in the final expression, this can break typechecking in complex cases.
 171 | public export
 172 | applySyn : TTImp -> TTImp -> TTImp
 173 | applySyn (ILam _ _ _ Nothing  _ lamExpr) _ = lamExpr
 174 | applySyn (ILam _ _ _ (Just n) _ lamExpr) rhs = mapTTImp (\case orig@(IVar _ n') => if n == n' then rhs else orig; e => e) lamExpr
 175 | applySyn lhs rhs = lhs `app` rhs
 176 | 
 177 | --- `DPair` type parsing and rebuilding stuff ---
 178 | 
 179 | public export
 180 | unDPair : TTImp -> (List Arg, TTImp)
 181 | unDPair (IApp _ (IApp _ (IVar _ `{Builtin.DPair.DPair}) typ) (ILam _ cnt piInfo mbname _ lamTy)) =
 182 |     mapFst (MkArg cnt piInfo mbname typ ::) $ unDPair lamTy
 183 | unDPair expr = ([], expr)
 184 | 
 185 | public export
 186 | unDPairUnAlt : TTImp -> Maybe (List Arg, TTImp)
 187 | unDPairUnAlt (IAlternative _ _ alts) = case filter (not . null . Builtin.fst) $ unDPair <$> alts of
 188 |   [x] => Just x
 189 |   _   => Nothing
 190 | unDPairUnAlt x = Just $ unDPair x
 191 | 
 192 | public export
 193 | buildDPair : (rhs : TTImp) -> List (Name, TTImp) -> TTImp
 194 | buildDPair = foldr $ \(name, type), res =>
 195 |   var `{Builtin.DPair.DPair} .$ type .$ lam (MkArg MW ExplicitArg (Just name) type) res
 196 | 
 197 | -----------------------------------------------------
 198 | --- Analysis of pieces inside `TTImp` expressions ---
 199 | -----------------------------------------------------
 200 | 
 201 | ||| Returns unnamespaced name and list of all namespaces stored in direct order
 202 | |||
 203 | ||| Say, for `Data.Vect.Vect` it would return (["Data", "Vect"], `{Vect}).
 204 | export
 205 | unNS : Name -> (List String, Name)
 206 | unNS (NS (MkNS revNSs) nm) = mapFst (reverse revNSs ++) $ unNS nm
 207 | unNS (DN _ nm)             = unNS nm
 208 | unNS nm                    = ([], nm)
 209 | 
 210 | ||| Returns all names that are suffixes of a given name (including the original name itself).
 211 | |||
 212 | ||| For example, for the name `Data.Vect.Vect` suffixes set would include
 213 | ||| `Data.Vect.Vect`, `Vect.Vect` and `Vect`.
 214 | export
 215 | allNameSuffixes : Name -> List Name
 216 | allNameSuffixes nm = do
 217 |   let (nss, n) = unNS nm
 218 |   tails nss <&> \case
 219 |     [] => n
 220 |     ns => NS (MkNS $ reverse ns) n
 221 | 
 222 | export
 223 | isNamespaced : Name -> Bool
 224 | isNamespaced = not . null . fst . unNS
 225 | 
 226 | public export
 227 | isImplicit : PiInfo c -> Bool
 228 | isImplicit ImplicitArg     = True
 229 | isImplicit (DefImplicit x) = True
 230 | isImplicit AutoImplicit    = True
 231 | isImplicit ExplicitArg     = False
 232 | 
 233 | -------------------------------------------------
 234 | --- Syntactic analysis of `TTImp` expressions ---
 235 | -------------------------------------------------
 236 | 
 237 | public export
 238 | isSameTypeAs : Name -> Name -> Elab Bool
 239 | isSameTypeAs n m = let eq = (==) `on` fst in [| lookupName n `eq` lookupName m |]
 240 | 
 241 | export
 242 | nameConformsTo : (cand, origin : Name) -> Bool
 243 | nameConformsTo cand origin = do
 244 |   let (cns, cn) = simplify cand
 245 |   let (ons, on) = simplify origin
 246 |   cn == on && (cns `isPrefixOf` ons) -- notice that namespaces are stored in the reverse order
 247 |   where
 248 |     simplify : Name -> (List String, Name)
 249 |     simplify (NS (MkNS ns) nm) = mapFst (++ ns) $ simplify nm
 250 |     simplify (DN _ nm)         = simplify nm
 251 |     simplify x                 = ([], x)
 252 | 
 253 | 0 nct_corr_eq : nameConformsTo `{A.B.c} `{A.B.c} = True;  nct_corr_eq = Refl
 254 | 0 nct_corr_le : nameConformsTo `{B.c}   `{A.B.c} = True;  nct_corr_le = Refl
 255 | 0 nct_corr_ge : nameConformsTo `{A.B.c} `{B.c}   = False; nct_corr_ge = Refl
 256 | 
 257 | -- simple syntactic search of a `IVar`, disregarding shadowing or whatever
 258 | export
 259 | allVarNames' : TTImp -> SortedSet Name
 260 | allVarNames' = runConst . mapATTImp' f where
 261 |   f : TTImp -> Const (SortedSet Name) TTImp -> Const (SortedSet Name) TTImp
 262 |   f (IVar _ n) = const $ MkConst $ singleton n
 263 |   f _          = id
 264 | 
 265 | -- Same as `allVarNames'`, but returning `List`
 266 | export
 267 | allVarNames : TTImp -> List Name
 268 | allVarNames = Prelude.toList . allVarNames'
 269 | 
 270 | public export
 271 | isVar : TTImp -> Bool
 272 | isVar $ IVar {} = True
 273 | isVar _         = False
 274 | 
 275 | public export
 276 | 0 ArgDeps : Nat -> Type
 277 | ArgDeps n = DVect n $ FinSet . Fin.finToNat
 278 | 
 279 | export
 280 | argDeps : (args : List Arg) -> ArgDeps args.length
 281 | argDeps args = do
 282 |   let nameToIndices = SortedMap.fromList $ mapI args $ \i, arg => (argName' arg, Fin.Set.singleton i)
 283 |   let args = Vect.fromList args <&> \arg => allVarNames arg.type <&> fromMaybe empty . lookup' nameToIndices
 284 |   flip upmapI args $ \i, deps => flip concatMap deps $ \candidates =>
 285 |     maybe empty singleton $ last' $ mapMaybe tryToFit $ Fin.Set.toList candidates
 286 | 
 287 | export
 288 | dependees : (args : List Arg) -> FinSet args.length
 289 | dependees args = do
 290 |   let nameToIndex = SortedMap.fromList $ mapI args $ \i, arg => (argName' arg, i)
 291 |   let varsInTypes = concatMap (\arg => allVarNames' arg.type) args
 292 |   fromList $ mapMaybe (lookup' nameToIndex) $ Prelude.toList varsInTypes
 293 | 
 294 | namespace UpToRenaming
 295 | 
 296 |   mutual
 297 | 
 298 |     compWithSubst : (subst : List $ These Name Name) => (from, to : Maybe Name) -> TTImp -> TTImp -> Bool
 299 |     compWithSubst (Just n) (Just n') e e' = n == n' && (e == e') @{UpToSubst} || (e == e') @{UpToSubst @{Both n n' :: subst}}
 300 |     compWithSubst (Just n) Nothing   e e' = (e == e') @{UpToSubst @{This n  :: subst}}
 301 |     compWithSubst Nothing  (Just n') e e' = (e == e') @{UpToSubst @{That n' :: subst}}
 302 |     compWithSubst Nothing  Nothing   e e' = (e == e') @{UpToSubst}
 303 | 
 304 |     [UpToSubst] (subst : List $ These Name Name) => Eq TTImp where
 305 |       IVar _ v == IVar _ v' = maybe (v == v') (== Both v v') $ flip find subst $ \ior => fromThis ior == Just v || fromThat ior == Just v'
 306 |       IPi _ c i n a r == IPi _ c' i' n' a' r' =
 307 |         c == c' && (assert_total $ i == i') && a == a' && (assert_total $ compWithSubst n n' r r')
 308 |       ILam _ c i n a r == ILam _ c' i' n' a' r' =
 309 |         c == c' && (assert_total $ i == i') && a == a' && (assert_total $ compWithSubst n n' r r')
 310 |       ILet _ _ c n ty val s == ILet _ _ c' n' ty' val' s' =
 311 |         c == c' && ty == ty' && val == val' && (assert_total $ compWithSubst (Just n) (Just n') s s')
 312 | 
 313 |       ICase _ os t ty cs == ICase _ os' t' ty' cs' =
 314 |         t == t' && (assert_total $ os == os') && ty == ty' && (assert_total $ cs == cs')
 315 |       ILocal _ ds e == ILocal _ ds' e' =
 316 |         (assert_total $ ds == ds') && e == e'
 317 |       IUpdate _ fs t == IUpdate _ fs' t' =
 318 |         (assert_total $ fs == fs') && t == t'
 319 | 
 320 |       IApp _ f x == IApp _ f' x' = f == f' && x == x'
 321 |       INamedApp _ f n x == INamedApp _ f' n' x' =
 322 |         f == f' && n == n' && x == x'
 323 |       IAutoApp _ f x == IAutoApp _ f' x' = f == f' && x == x'
 324 |       IWithApp _ f x == IWithApp _ f' x' = f == f' && x == x'
 325 | 
 326 |       ISearch _ n == ISearch _ n' = n == n'
 327 |       IAlternative _ t as == IAlternative _ t' as' =
 328 |         (assert_total $ t == t') && (assert_total $ as == as')
 329 |       IRewrite _ p q == IRewrite _ p' q' =
 330 |         p == p' && q == q'
 331 | 
 332 |       IBindHere _ m t == IBindHere _ m' t' =
 333 |         m == m' && t == t'
 334 |       IBindVar _ s == IBindVar _ s' = s == s'
 335 |       IAs _ _ u n t == IAs _ _ u' n' t' =
 336 |         u == u' && n == n' && t == t'
 337 |       IMustUnify _ r t == IMustUnify _ r' t' =
 338 |         r == r' && t == t'
 339 | 
 340 |       IDelayed _ r t == IDelayed _ r' t' = r == r' && t == t'
 341 |       IDelay _ t == IDelay _ t' = t == t'
 342 |       IForce _ t == IForce _ t' = t == t'
 343 | 
 344 |       IQuote _ tm == IQuote _ tm' = tm == tm'
 345 |       IQuoteName _ n == IQuoteName _ n' = n == n'
 346 |       IQuoteDecl _ ds == IQuoteDecl _ ds' = assert_total $ ds == ds'
 347 |       IUnquote _ tm == IUnquote _ tm' = tm == tm'
 348 | 
 349 |       IPrimVal _ c == IPrimVal _ c' = c == c'
 350 |       IType _ == IType _ = True
 351 |       IHole _ s == IHole _ s' = True -- Holes are anyway unique and does not matter what the names are.
 352 | 
 353 |       Implicit _ b == Implicit _ b' = b == b'
 354 |       IWithUnambigNames _ ns t == IWithUnambigNames _ ns' t' =
 355 |         map snd ns == map snd ns' && t == t'
 356 | 
 357 |       _ == _ = False
 358 | 
 359 |   export
 360 |   [UpToRenaming] Eq TTImp where
 361 |     x == y = (x == y) @{UpToSubst @{empty}}
 362 |