0 | module Deriving.SpecialiseData

   2 | import Control.Monad.Either

   3 | import Control.Monad.Error.Either

   4 | import Control.Monad.Error.Interface

   5 | import Control.Monad.Reader.Tuple

   6 | import Control.Monad.Trans

   7 | import Data.SnocList

   8 | import Data.DPair

   9 | import Data.List1

  10 | import Data.Vect

  11 | import Data.Vect.Quantifiers

  12 | import Data.List

  13 | import Data.List.Quantifiers

  14 | import Data.Either

  15 | import Data.SortedMap

  16 | import Data.SortedSet

  17 | import Data.SortedMap.Dependent

  18 | import Decidable.Equality

  19 | import Deriving.Show

  20 | import public Language.Mk

  21 | import Language.Reflection.Compat

  22 | import Language.Reflection.Compat.Constr

  23 | import Language.Reflection.Compat.TypeInfo

  24 | import Language.Reflection.Expr

  25 | import Language.Reflection.Logging

  26 | import Language.Reflection.Unify

  27 | import Language.Reflection.VarSubst

  28 | import Syntax.IHateParens

  30 | %language ElabReflection

  32 | %default total

  40 | data SpecialisationError : Type where

  41 |   ||| Failed to extract polymorphic type name from task

  42 |   TaskTypeExtractionError   : SpecialisationError

  43 |   ||| Unused variable

  44 |   UnusedVarError            : SpecialisationError

  45 |   ||| Partial specification

  46 |   PartialSpecError          : SpecialisationError

  47 |   ||| Internal error

  48 |   InternalError             : String -> SpecialisationError

  49 |   ||| Lambda has unnamed arguments

  50 |   UnnamedArgInLambdaError   : SpecialisationError

  51 |   ||| Polymorphic type has unnamed arguments

  52 |   UnnamedArgInPolyTyError   : Name -> SpecialisationError

  53 |   ||| Failed to get TypeInfo

  57 |   MissingTypeInfoError      : Name -> SpecialisationError

  61 | showSE : Show SpecialisationError

  62 | showSE = %runElab derive

  69 | record SpecTask where

  70 |   constructor MkSpecTask

  71 |   ||| Full unification task

  72 |   tqArgs              : List Arg

  73 |   tqRet               : TTImp

  74 |   {auto 0 tqArgsNamed : All IsNamedArg tqArgs}

  75 |   ||| Unification task type

  76 |   ttArgs              : List Arg

  77 |   {auto 0 ttArgsNamed : All IsNamedArg ttArgs}

  78 |   ||| Namespace in which specialiseData was called

  79 |   currentNs           : Namespace

  80 |   ||| Name of specialised type

  81 |   resultName          : Name

  82 |   ||| Invocation of polymorphic type extracted from unification task

  83 |   fullInvocation      : TTImp

  84 |   ||| Polymorphic type's TypeInfo

  85 |   polyTy              : TypeInfo

  86 |   ||| Proof that all the constructors of the polymorphic type are named

  87 |   {auto 0 polyTyNamed : AllTyArgsNamed polyTy}

  89 | Show SpecTask where

  90 |   showPrec p t =

  91 |     showCon p "SpecTask" $ joinBy "" $

  92 |       [ showArg t.tqArgs

  93 |       , showArg t.tqRet

  94 |       , showArg t.ttArgs

  95 |       , showArg t.currentNs

  96 |       , showArg t.resultName

  97 |       , showArg t.fullInvocation

  98 |       , showArg "<polyTy>"

  99 |       ]

 102 | UniResults : Type

 103 | UniResults = List UnificationVerdict

 109 | public export

 110 | interface NamespaceProvider (0 m : Type -> Type) where

 111 |   constructor MkNSProvider

 112 |   provideNS : m Namespace

 114 | export %defaulthint

 115 | CurrentNS : Elaboration m => NamespaceProvider m

 116 | CurrentNS = MkNSProvider $ do

 117 |     NS nsn _ <- inCurrentNS ""

 118 |     | _ => fail "Internal error: inCurrentNS did not return NS"

 119 |     pure nsn

 122 | Monad m => MonadTrans t => NamespaceProvider m => NamespaceProvider (t m) where

 123 |   provideNS = lift provideNS

 126 | inNS : Monad m => Namespace -> NamespaceProvider m

 127 | inNS ns = MkNSProvider $ pure ns

 130 | inGenNS : SpecTask -> Name -> Name

 131 | inGenNS task n = do

 132 |   let MkNS tns = task.currentNs

 133 |   let newNS =

 134 |     case n of

 135 |        (NS (MkNS subs) n) => subs

 136 |        n => []

 137 |   NS (MkNS $ newNS ++ show task.resultName :: tns) $ dropNS n

 140 | argsToBindMap : Foldable f => f Arg -> List (Name, TTImp)

 141 | argsToBindMap = foldMap $ toList . map (\y => (y, bindVar y)) . name

 144 | applyArgAliases :

 145 |   (as : List Arg) ->

 146 |   (0 _ : All IsNamedArg as) =>

 147 |   List (Name, Name) ->

 148 |   SortedMap Name TTImp ->

 149 |   Subset (List Arg) (All IsNamedArg)

 150 | applyArgAliases []        @{[]}     _  _   = Element [] []

 151 | applyArgAliases (x :: xs) @{_ :: _} ys ins = do

 152 |   let (newIns, newName, ys) : (SortedMap _ _, Name, List (Name, Name)) =

 153 |     case ys of

 154 |        []              => (ins                  , argName x, [])

 155 |        ((y, y') :: ys) => (insert y (var y') ins, y'       , ys)

 156 |   let Element rec prec = applyArgAliases xs ys newIns

 157 |   Element

 158 |     (MkArg x.count x.piInfo (Just newName) (substituteVariables newIns x.type) :: rec)

 159 |     (ItIsNamed :: prec)

 161 | prependS : String -> Name -> Name

 162 | prependS s n = UN $ Basic $ s ++ show n

 165 | transformArgNames' : (f : Name -> Name) -> (as : List Arg) -> (0 _ : All IsNamedArg as) => List (Name, Name)

 166 | transformArgNames' _ [] = []

 167 | transformArgNames' f (x :: xs) @{_ :: _} =

 168 |   (argName x, f $ Expr.argName x) :: transformArgNames' f xs

 172 | transformArgNames :

 173 |   (f : Name -> Name) ->

 174 |   (as : List Arg) ->

 175 |   (0 _ : All IsNamedArg as) =>

 176 |   (Subset (List Arg) (All IsNamedArg), List (Name, Name))

 177 | transformArgNames f as = do

 178 |   let aliases = transformArgNames' f as

 179 |   (applyArgAliases as aliases empty, aliases)

 183 | mkEqualsTuple : List (Subset Arg IsNamedArg, Subset Arg IsNamedArg) -> TTImp

 184 | mkEqualsTuple [] = `(MkUnit)

 185 | mkEqualsTuple [(Element a1 _, Element a2 _)] =

 186 |   `(~(var $ argName a1) ~=~ ~(var $ argName a2))

 187 | mkEqualsTuple ((Element a1 _, Element a2 _) :: as) =

 188 |   `(Pair (~(var $ argName a1) ~=~ ~(var $ argName a2)) ~(mkEqualsTuple as))

 192 | mkDoubleBinds : SnocList (Arg, Arg) -> TTImp -> TTImp

 193 | mkDoubleBinds [<] t = t

 194 | mkDoubleBinds (as :< (a1, a2)) t =

 195 |   case (a1.name, a2.name) of

 196 |     (Just a1n, Just a2n) =>

 197 |       mkDoubleBinds as t .! (a1n, bindVar a1n) .! (a2n, bindVar a1n)

 198 |     _ => mkDoubleBinds as t

 201 | hideExplicitArg : Arg -> Arg

 202 | hideExplicitArg a = { piInfo := if a.piInfo == ExplicitArg then ImplicitArg else a.piInfo } a

 205 | makeImplicit : Arg -> Arg

 206 | makeImplicit = { piInfo := ImplicitArg }

 209 | makeTypeArgM0 : Arg -> Arg

 210 | makeTypeArgM0 a = { count := if a.type == `(Type) then M0 else a.count } a

 213 | tupleOfN : Nat -> TTImp -> TTImp

 214 | tupleOfN 0 _ = `(Unit)

 215 | tupleOfN 1 t = t

 216 | tupleOfN (S n) t = `(MkPair ~(t) ~(tupleOfN n t))

 219 | mergeAliases : SortedMap Name TTImp -> List (Name, Name) -> SortedMap Name TTImp

 220 | mergeAliases m = mergeWith (Prelude.curry fst) m . fromList . map (mapSnd var)

 223 | hideExplicitArgPreservesNames :

 224 |   (args : List Arg) ->

 225 |   (0 _ : All IsNamedArg args) =>

 226 |   All IsNamedArg (SpecialiseData.hideExplicitArg <$> args)

 227 | hideExplicitArgPreservesNames [] @{[]} = []

 228 | hideExplicitArgPreservesNames (x :: xs) @{_ :: _} with (x)

 229 |   hideExplicitArgPreservesNames (x :: xs) @{_ :: _} | (MkArg _ _ (Just n) _) =

 230 |     ItIsNamed :: hideExplicitArgPreservesNames xs

 233 | makeImplicitPreservesNames :

 234 |   (args : List Arg) ->

 235 |   (0 _ : All IsNamedArg args) =>

 236 |   All IsNamedArg (SpecialiseData.makeImplicit <$> args)

 237 | makeImplicitPreservesNames [] @{[]} = []

 238 | makeImplicitPreservesNames (x :: xs) @{_ :: _} with (x) -- This `with` match is a workaround for coverage checking bug

 239 |   makeImplicitPreservesNames (x :: xs) @{_ :: _} | (MkArg _ _ (Just n) _) =

 240 |     ItIsNamed :: makeImplicitPreservesNames xs

 243 | hideExplicitArgs : (xs : List Arg) -> (0 _ : All IsNamedArg xs) => Subset (List Arg) (All IsNamedArg)

 244 | hideExplicitArgs xs = hideExplicitArg <$> xs `Element` hideExplicitArgPreservesNames xs

 247 | makeArgsImplicit : (xs : List Arg) -> (0 _ : All IsNamedArg xs) => Subset (List Arg) (All IsNamedArg)

 248 | makeArgsImplicit xs = makeImplicit <$> xs `Element` makeImplicitPreservesNames xs

 252 | aliasedAppBind : SnocList (Name, Name) -> TTImp -> TTImp

 253 | aliasedAppBind [<] t = t

 254 | aliasedAppBind (xs :< (n, an)) t = aliasedAppBind xs t .! (an, `(_))

 258 | aliasedApp : SnocList (Name, Name) -> TTImp -> TTImp

 259 | aliasedApp [<] t = t

 260 | aliasedApp (xs :< (n, an)) t = aliasedApp xs t .! (n, var an)

 268 | checkArgsUse :

 269 |   MonadError SpecialisationError m =>

 270 |   List Arg ->

 271 |   SortedSet Name ->

 272 |   m ()

 273 | checkArgsUse [] _ = pure ()

 274 | checkArgsUse (x :: xs) t = do

 275 |   let Just n = x.name

 276 |   | _ => checkArgsUse xs t

 277 |   if contains n t

 278 |     then checkArgsUse xs t

 279 |     else throwError UnusedVarError

 281 | cleanupHoleAutoImplicitsImpl : TTImp -> TTImp

 282 | cleanupHoleAutoImplicitsImpl (IAutoApp _ x (Implicit _ _)) = x

 283 | cleanupHoleAutoImplicitsImpl (INamedApp _ x _ (Implicit _ _)) = x

 284 | cleanupHoleAutoImplicitsImpl x = x

 287 | getTask :

 288 |   Monad m =>

 289 |   NamespaceProvider m =>

 290 |   MonadError SpecialisationError m =>

 291 |   NamesInfoInTypes =>

 292 |   (resultName : Name) ->

 293 |   (resultKind : TTImp) ->

 294 |   (resultContent : TTImp) ->

 295 |   m SpecTask

 296 | getTask resultName resultKind resultContent = do

 297 |   let (tqArgs, tqRet) = unLambda resultContent

 298 |   -- Check for unused arguments

 299 |   checkArgsUse tqArgs $ usesVariables tqRet

 300 |   -- Extract name of polymorphic type

 301 |   let (IVar _ typeName, _) = Expr.unAppAny tqRet

 302 |   | _ => throwError TaskTypeExtractionError

 303 |   -- Prove that all spec lambda arguments are named

 304 |   let Yes tqArgsNamed = all isNamedArg tqArgs

 305 |   | _ => throwError UnnamedArgInLambdaError

 306 |   -- Create aliases for spec lambda's arguments and perform substitution

 307 |   let (Element tqArgs tqArgsNamed, tqAlias) = transformArgNames (prependS "fv^") tqArgs

 308 |   let tqRet = substituteVariables (fromList $ mapSnd var <$> tqAlias) tqRet

 309 |   let (ttArgs, _) = unPi resultKind

 310 |   -- Check for partial application in spec

 311 |   let True = (length tqArgs == length ttArgs)

 312 |   | _ => throwError PartialSpecError

 313 |   -- Prove that all spec lambda type's arguments are named

 314 |   let Yes ttArgsNamed = all isNamedArg ttArgs

 315 |   | _ => throwError UnnamedArgInLambdaError

 316 |   -- Apply aliasing to spec lambda type's info

 317 |   let Element ttArgs ttArgsNamed = applyArgAliases ttArgs tqAlias empty

 318 |   -- Get current namespace

 319 |   currentNs <- provideNS

 320 |   -- Get polymorphic type's info

 321 |   let Just polyTy = lookupType typeName

 322 |   | _ => throwError $ MissingTypeInfoError typeName

 323 |   -- Prove all its arguments/constructors/constructor arguments are named

 324 |   let Yes polyTyNamed = areAllTyArgsNamed polyTy

 325 |     | No _ => throwError $ UnnamedArgInPolyTyError polyTy.name

 326 |   pure $ MkSpecTask

 327 |     { tqArgs

 328 |     , tqRet

 329 |     , tqArgsNamed

 330 |     , ttArgs

 331 |     , ttArgsNamed

 332 |     , currentNs

 333 |     , resultName

 334 |     , fullInvocation = tqRet --- TODO: intelligent full invocation

 335 |     , polyTy

 336 |     , polyTyNamed

 337 |     }

 341 | (.appWith) :

 342 |   (arg : Arg) ->

 343 |   (0 _ : IsNamedArg arg) =>

 344 |   (fallback : Name -> TTImp) ->

 345 |   (argValues : SortedMap Name TTImp) ->

 346 |   AnyApp

 347 | (.appWith) arg@(MkArg _ _ (Just n) _) f argVals =

 348 |   appArg arg $ fromMaybe (f n) $ lookup n argVals

 352 | (.appsWith) :

 353 |   (args: List Arg) ->

 354 |   (0 _ : All IsNamedArg args) =>

 355 |   (fallback : Name -> TTImp) ->

 356 |   (argValues : SortedMap Name TTImp) ->

 357 |   List AnyApp

 358 | (.appsWith) [] _ _ = []

 359 | (.appsWith) (x :: xs) @{_ :: _} f argVals =

 360 |   x.appWith f argVals :: xs.appsWith f argVals

 362 | namespace TypeInfoInvoke

 363 |   ||| Returns a full application of the given type constructor

 366 |   export

 367 |   (.apply) :

 368 |     (ti : TypeInfo) ->

 369 |     (0 tiN : AllTyArgsNamed ti) =>

 370 |     (fallback : Name -> TTImp) ->

 371 |     (argValues : SortedMap Name TTImp) ->

 372 |     TTImp

 373 |   (.apply) t f vals = do

 374 |     reAppAny (var t.name) $ t.args.appsWith @{tiN.tyArgsNamed} f vals

 376 | namespace ConInvoke

 377 |   ||| Returns a full application of the given constructor

 380 |   export

 381 |   (.apply) :

 382 |     (con : Con) ->

 383 |     (0 _ : ConArgsNamed con) =>

 384 |     (fallback : Name -> TTImp) ->

 385 |     (argValues : SortedMap Name TTImp) ->

 386 |     TTImp

 387 |   (.apply) con f vals = reAppAny (var con.name) $ con.args.appsWith f vals @{conArgsNamed}

 389 | allL2V : (l : List t) -> (0 pr : All p l) => Subset (Vect (length l) t) (All p)

 390 | allL2V [] = Element [] []

 391 | allL2V (x :: xs) @{p :: ps} = do

 392 |   let Element xs' ps' = allL2V xs @{ps}

 393 |   Element (x :: xs') (p :: ps')

 395 | parameters (t : SpecTask)

 396 |   ---------------------------

 397 |   --- CONSTRUCTOR MAPPING ---

 398 |   ---------------------------

 399 |   ||| Run monadic operation on all constructors of specialised type

 400 |   mapCons :

 401 |     (f : (pCon : Con) ->

 402 |          (0 _ : ConArgsNamed pCon) =>

 403 |          r) ->

 404 |     List r

 405 |   mapCons f = do

 406 |     let adp = pushIn t.polyTy.cons t.polyTyNamed.tyConArgsNamed

 407 |     map (\(Element c pc) => f c) adp

 409 |   ||| Map over all constructors for which unification succeeded

 410 |   mapUCons :

 411 |     (f : UnificationResult ->

 412 |          (pCon : Con) ->

 413 |          (0 _ : ConArgsNamed pCon) =>

 414 |          r) ->

 415 |     UniResults ->

 416 |     List r

 417 |   mapUCons f rs = do

 418 |     let adp = pushIn t.polyTy.cons t.polyTyNamed.tyConArgsNamed

 419 |     let f' : List (Subset Con ConArgsNamed) -> UniResults -> List r

 420 |         f' (Element con _ :: xs) (Success res :: ys) = f res con :: f' xs ys

 421 |         f' (_ :: xs)             (_ :: ys)           = f' xs ys

 422 |         f' _ _ = []

 423 |     f' adp rs

 425 |   ||| Run monadic operation on all pairs of specified and polymorphic constructors

 426 |   map2UConsN :

 427 |     (f : UnificationResult ->

 428 |          (mt : TypeInfo) ->

 429 |          (0 _ : AllTyArgsNamed mt) =>

 430 |          (con : Con) ->

 431 |          (0 _ : ConArgsNamed con) =>

 432 |          (mcon : Con) ->

 433 |          (0 _ : ConArgsNamed mcon) =>

 434 |          Nat ->

 435 |          r) ->

 436 |     UniResults ->

 437 |     (mt : TypeInfo) ->

 438 |     (0 _ : AllTyArgsNamed mt) =>

 439 |     List r

 440 |   map2UConsN f rs mt @{mtp} = do

 441 |     let p1 = pushIn t.polyTy.cons t.polyTyNamed.tyConArgsNamed

 442 |     let p2 = pushIn mt.cons mtp.tyConArgsNamed

 443 |     f' 0 p1 p2 rs

 444 |     where

 445 |       f' :

 446 |         Nat ->

 447 |         List (Subset Con ConArgsNamed) ->

 448 |         List (Subset Con ConArgsNamed) ->

 449 |         UniResults ->

 450 |         List r

 451 |       f' n (Element con _ :: xs) (Element mcon _ :: ys) (Success res :: zs) =

 452 |         f res mt con mcon n :: f' (S n) xs ys zs

 453 |       f' n (_             :: xs)                    ys  (_:: zs) =

 454 |         f' n xs ys zs

 455 |       f' _ _ _ _ = []

 457 |   -------------------------------

 458 |   --- CONSTRUCTOR UNIFICATION ---

 459 |   -------------------------------

 461 |   ||| Run unification for a given polymorphic constructor

 462 |   unifyCon :

 463 |     MonadLog m =>

 464 |     (unifier : CanUnify m) =>

 465 |     (con : Con) ->

 466 |     (0 conN : ConArgsNamed con) =>

 467 |     m UnificationVerdict

 468 |   unifyCon con = logBounds Debug "specialiseData.unifyCon" [t.polyTy, con] $ do

 469 |     let Element ca _ = allL2V con.args @{conArgsNamed}

 470 |     let Element ta _ = allL2V t.tqArgs @{t.tqArgsNamed}

 471 |     let uniTask =

 472 |       MkUniTask {lfv=_} ca con.type

 473 |                 {rfv=_} ta t.fullInvocation

 474 |     logPoint DetailedDebug "specialiseData.unifyCon" [t.polyTy, con] "Unifier task: \{show uniTask}"

 475 |     uniRes <- unify uniTask

 476 |     logPoint DetailedDebug "specialiseData.unifyCon" [t.polyTy, con] "Unifier output: \{show uniRes}"

 477 |     pure uniRes

 479 |   ---------------------------------

 480 |   --- SPECIFIED TYPE GENERATION ---

 481 |   ---------------------------------

 483 |   ||| Generate argument of a specified constructor

 484 |   mkSpecArg :

 485 |     (ur : UnificationResult) ->

 486 |     Fin (ur.uniDg.freeVars) ->

 487 |     (Subset Arg IsNamedArg)

 488 |   mkSpecArg ur fvId = do

 489 |     let fvData = index fvId ur.uniDg.fvData

 490 |     let fromLambda = finToNat fvId >= ur.task.lfv

 491 |     let rig = if fromLambda then M0 else fvData.rig

 492 |     let piInfo = if fromLambda && (fvData.piInfo == ExplicitArg) then ImplicitArg else fvData.piInfo

 493 |     Element (MkArg rig piInfo (Just fvData.name) fvData.type) ItIsNamed

 495 |   ||| Generate a specialised constructor

 496 |   mkSpecCon :

 497 |     (newArgs : _) ->

 498 |     (0 _ : All IsNamedArg newArgs) =>

 499 |     UnificationResult ->

 500 |     (con : Con) ->

 501 |     (0 _ : ConArgsNamed con) =>

 502 |     Subset Con ConArgsNamed

 503 |   mkSpecCon newArgs ur pCon = do

 504 |     let Element args allArgs =

 505 |       pullOut $ mkSpecArg ur <$> ur.order

 506 |     let typeArgs = newArgs.appsWith var ur.fullResult

 507 |     let tyRet = reAppAny (var t.resultName) typeArgs

 508 |     MkCon

 509 |       { name = inGenNS t $ dropNS pCon.name

 510 |       , args

 511 |       , type = tyRet

 512 |       } `Element` TheyAreNamed allArgs

 514 |   ||| Generate a specialised type

 515 |   mkSpecTy : UniResults -> Subset TypeInfo AllTyArgsNamed

 516 |   mkSpecTy ur = do

 517 |     let Element cons consAreNamed =

 518 |       pullOut $ mapUCons (mkSpecCon t.ttArgs @{t.ttArgsNamed}) ur

 519 |     MkTypeInfo

 520 |       { name = inGenNS t t.resultName

 521 |       , args = t.ttArgs

 522 |       , cons

 523 |       } `Element` TheyAllAreNamed t.ttArgsNamed consAreNamed

 525 |   ------------------------------------

 526 |   --- POLY TO POLY CAST DERIVATION ---

 527 |   ------------------------------------

 529 |   ||| Generate IPi with implicit type arguments and given return

 530 |   forallMTArgs : TTImp -> TTImp

 531 |   forallMTArgs = flip (foldr pi) $ makeTypeArgM0 . hideExplicitArg <$> t.ttArgs

 534 |   ||| Generate specialised to polymorphic type conversion function signature

 535 |   mkMToPImplSig : UniResults -> (mt : TypeInfo) -> (0 _ : AllTyArgsNamed mt) => TTImp

 536 |   mkMToPImplSig _ mt =

 537 |     forallMTArgs $ arg (mt.apply var empty) .-> t.fullInvocation

 539 |   ||| Generate specialised to polymorphic type conversion function clause

 541 |   mkMToPImplClause :

 542 |     UnificationResult ->

 543 |     (mt : TypeInfo) ->

 544 |     (0 _ : AllTyArgsNamed mt) =>

 545 |     (pCon : Con) ->

 546 |     (0 _ : ConArgsNamed pCon) =>

 547 |     (mCon : Con) ->

 548 |     (0 _ : ConArgsNamed mCon) =>

 549 |     Nat ->

 550 |     Clause

 551 |   mkMToPImplClause ur _ con mcon _ =

 552 |     var "mToPImpl" .$

 553 |       mcon.apply bindVar

 554 |         (substituteVariables

 555 |           (fromList $ argsToBindMap mcon.args) <$> ur.fullResult)

 556 |       .= con.apply var ur.fullResult

 558 |   ||| Generate specialised to polymorphic type conversion function declarations

 559 |   mkMToPImplDecls :

 560 |     UniResults ->

 561 |     (mt : TypeInfo) ->

 562 |     (0 _ : AllTyArgsNamed mt) =>

 563 |     List Decl

 564 |   mkMToPImplDecls urs mt = do

 565 |     let sig = mkMToPImplSig urs mt

 566 |     let clauses = map2UConsN mkMToPImplClause urs mt

 567 |     [ public' "mToPImpl" sig

 568 |     , def "mToPImpl" clauses

 569 |     ]

 571 |   ||| Generate specialised to polymorphic cast signature

 572 |   mkMToPSig : (mt : TypeInfo) -> (0 _ : AllTyArgsNamed mt) => TTImp

 573 |   mkMToPSig mt = do

 574 |     forallMTArgs $ `(Cast ~(mt.apply var empty) ~(t.fullInvocation))

 576 |   ||| Generate specialised to polymorphic cast declarations

 577 |   mkMToPDecls : (mt : TypeInfo) -> (0 _ : AllTyArgsNamed mt) => List Decl

 578 |   mkMToPDecls mt =

 579 |     [ interfaceHint Public "mToP" $ mkMToPSig mt

 580 |     , def "mToP" [ (var "mToP") .= `(MkCast mToPImpl)]

 581 |     ]

 583 |   -----------------------------------

 584 |   --- MULTIINJECTIVITY DERIVATION ---

 585 |   -----------------------------------

 587 |   ||| Derive multiinjectivity for a polymorphic constructor that has a

 589 |   mkMultiInjDecl :

 590 |     UnificationResult ->

 591 |     (mt : TypeInfo) ->

 592 |     (0 _ : AllTyArgsNamed mt) =>

 593 |     (pCon : Con) ->

 594 |     (0 _ : ConArgsNamed pCon) =>

 595 |     (mCon : Con) ->

 596 |     (0 mn : ConArgsNamed mCon) =>

 597 |     Nat ->

 598 |     List Decl

 599 |   mkMultiInjDecl ur mt con mcon i = do

 600 |     let S _ = length mcon.args

 601 |     | _ => []

 602 |     let n = fromString "mInj\{show i}"

 603 |     let 0 _ = conArgsNamed @{mn}

 604 |     let Element ourArgs _ = makeArgsImplicit mcon.args

 605 |     let (Element a1 _, am1) = transformArgNames (prependS "lhs^") ourArgs

 606 |     let (Element a2 _, am2) = transformArgNames (prependS "rhs^") ourArgs

 607 |     let lhsCon = substituteVariables (fromList $ mapSnd var <$> am1) $

 608 |                   con.apply var $ mergeAliases ur.fullResult am1

 609 |     let rhsCon = substituteVariables (fromList $ mapSnd var <$> am2) $

 610 |                   con.apply var $ mergeAliases ur.fullResult am2

 612 |     let eqs = mkEqualsTuple $ zip (pushIn a1 %search) (pushIn a2 %search)

 613 |     let sig =

 614 |       flip piAll a1 $

 615 |         flip piAll a2 $ `((~(lhsCon) ~=~ ~(rhsCon)) -> ~(eqs))

 616 |     let lhs = mkDoubleBinds (cast $ zip a1 a2) (var n) .$ `(Refl)

 617 |     [ public' n sig

 618 |     , def n $ singleton $ patClause lhs $ tupleOfN (length mcon.args) `(Refl)

 619 |     ]

 621 |   ||| Derive multiinjectivity for all polymorphic constructors that have

 623 |   mkMultiInjDecls :

 624 |     UniResults -> (mt : TypeInfo) -> (0 _ : AllTyArgsNamed mt) => List Decl

 625 |   mkMultiInjDecls ur specTy = do

 626 |     join $ map2UConsN mkMultiInjDecl ur specTy

 628 |   ----------------------------------

 629 |   --- MULTICONGRUENCY DERIVATION ---

 630 |   ----------------------------------

 632 |   ||| Derive multicongruency for a specialised constructor

 635 |   mkMultiCongDecl :

 636 |     UnificationResult ->

 637 |     (mt : TypeInfo) ->

 638 |     (0 _ : AllTyArgsNamed mt) =>

 639 |     (pCon : Con) ->

 640 |     (0 _ : ConArgsNamed pCon) =>

 641 |     (mCon : Con) ->

 642 |     (0 mn : ConArgsNamed mCon) =>

 643 |     Nat ->

 644 |     List Decl

 645 |   mkMultiCongDecl ur mt _ mcon i = do

 646 |     let S _ = length mcon.args

 647 |     | _ => []

 648 |     let n = fromString "mCong\{show i}"

 649 |     let 0 _ = conArgsNamed @{mn}

 650 |     let Element ourArgs _ = makeArgsImplicit mcon.args

 651 |     let (Element a1 _, am1) = transformArgNames (prependS "lhs^") ourArgs

 652 |     let (Element a2 _, am2) = transformArgNames (prependS "rhs^") ourArgs

 653 |     let lhsCon = mcon.apply var $ mergeAliases ur.fullResult am1

 654 |     let rhsCon = mcon.apply var $ mergeAliases ur.fullResult am2

 655 |     let eqs = mkEqualsTuple $ zip (pushIn a1 %search) (pushIn a2 %search)

 656 |     let sig =

 657 |       flip piAll a1 $ flip piAll a2 $ `(~(eqs) -> (~(lhsCon) ~=~ ~(rhsCon)))

 658 |     let lhs = mkDoubleBinds (cast $ zip a1 a2) (var n) .$ tupleOfN (length mcon.args) `(Refl)

 659 |     [ public' n sig

 660 |     , def n $ singleton $ patClause lhs $ `(Refl)

 661 |     ]

 663 |   ||| Derive multicongruency for all specialised constructors

 664 |   mkMultiCongDecls :

 665 |     UniResults -> (mt : TypeInfo) -> (0 _ : AllTyArgsNamed mt) => List Decl

 666 |   mkMultiCongDecls ur specTy = do

 667 |     join $ map2UConsN mkMultiCongDecl ur specTy

 669 |   -----------------------------------

 670 |   --- CAST INJECTIVITY DERIVATION ---

 671 |   -----------------------------------

 673 |   ||| Make a clause for the cast injectivity proof

 674 |   mkCastInjClause :

 675 |     (tal1, tal2 : (List Arg, List (Name, Name))) ->

 676 |     (n1, n2 : Name) ->

 677 |     UnificationResult ->

 678 |     (mt : TypeInfo) ->

 679 |     (0 _ : AllTyArgsNamed mt) =>

 680 |     (con : Con) ->

 681 |     (0 cn : ConArgsNamed con) =>

 682 |     (mcon : Con) ->

 683 |     (0 mcn : ConArgsNamed mcon) =>

 684 |     Nat ->

 685 |     Clause

 686 |   mkCastInjClause (ta1, tam1) (ta2, tam2) n1 n2 ur mt _ con n = do

 687 |     let 0 _ = conArgsNamed @{mcn}

 688 |     let (Element a1 _, am1) = transformArgNames (prependS "lhs^") con.args

 689 |     let (Element a2 _, am2) = transformArgNames (prependS "rhs^") con.args

 690 |     let am1' = fromList $ mapSnd (const `(_)) <$> am1

 691 |     let am2' = fromList $ mapSnd (const `(_)) <$> am2

 692 |     let ures1 = substituteVariables am1' <$> ur.fullResult

 693 |     let ures2 = substituteVariables am2' <$> ur.fullResult

 694 |     let bta1 = aliasedAppBind (cast tam1) `(castInjImpl)

 695 |     let bta2 = aliasedAppBind (cast tam2) bta1

 696 |     let lhsCon = con.apply bindVar $ am1'

 697 |     let rhsCon = con.apply bindVar $ am1'

 698 |     let patRhs : TTImp

 699 |         patRhs = case (length a1) of

 700 |           0 => `(Refl)

 701 |           _ => (var $ inGenNS t $ fromString $ "mCong\{show n}") .$

 702 |                 ((var $ inGenNS t $ fromString $ "mInj\{show n}") .$ var "r")

 703 |     bta2 .! (n1, lhsCon) .! (n2, rhsCon) .$ bindVar "r" .= patRhs

 705 |   ||| Derive cast injectivity proof

 706 |   mkCastInjDecls :

 707 |     UniResults ->

 708 |     (mt : TypeInfo) ->

 709 |     (0 mtp : AllTyArgsNamed mt) =>

 710 |     List Decl

 711 |   mkCastInjDecls ur ti = do

 712 |     let Element prepArgs prf = hideExplicitArgs ti.args @{mtp.tyArgsNamed}

 713 |     let ta1@(Element a1 _, am1) = transformArgNames (prependS "lhs^") prepArgs

 714 |     let ta2@(Element a2 _, am2) = transformArgNames (prependS "rhs^") prepArgs

 715 |     let xVar = "castInj^x"

 716 |     let yVar = "castInj^y"

 717 |     let mToPVar = var $ inGenNS t "mToP"

 718 |     let mToPImplVar = var $ inGenNS t "mToPImpl"

 719 |     let arg1 = MkArg MW ImplicitArg (Just xVar) $

 720 |                 ti.apply var $ fromList $ mapSnd var <$> am1

 721 |     let arg2 = MkArg MW ImplicitArg (Just yVar) $

 722 |                 ti.apply var $ fromList $ mapSnd var <$> am2

 723 |     let eqs =

 724 |       `((~(aliasedApp (cast am1) mToPImplVar .$ var xVar)

 725 |           ~=~

 726 |           ~(aliasedApp (cast am2) $ mToPImplVar .$ var yVar)) ->

 727 |           ~(var xVar) ~=~ ~(var yVar))

 728 |     let castInjImplClauses = map2UConsN (mkCastInjClause (a1, am1) (a2, am2) xVar yVar) ur ti

 729 |     let tyArgPairs = cast $ zip ti.argNames ti.argNames

 730 |     [ public' "castInjImpl" $

 731 |         flip piAll (makeTypeArgM0 <$> a1) $

 732 |           flip piAll (makeTypeArgM0 <$> a2) $

 733 |             pi arg1 $ pi arg2 $ eqs

 734 |     , def "castInjImpl" castInjImplClauses

 735 |     , interfaceHint Public "castInj" $ forallMTArgs $

 736 |         `(Injective ~(aliasedApp tyArgPairs mToPImplVar))

 737 |     , def "castInj" $ singleton $

 738 |         aliasedAppBind tyArgPairs `(castInj) .= `(MkInjective castInjImpl)

 739 |     ]

 741 |   -------------------------------------

 742 |   --- DECIDABLE EQUALITY DERIVATION ---

 743 |   -------------------------------------

 745 |   ||| Decidable equality signatures

 746 |   mkDecEqImplSig : (mt : TypeInfo) -> (0 _ : AllTyArgsNamed mt) => TTImp

 747 |   mkDecEqImplSig ti =

 748 |     let tInv = ti.apply var empty

 749 |     in forallMTArgs $

 750 |       piAll

 751 |         `(Dec (Equal {a = ~tInv} {b = ~tInv} x1 x2))

 752 |         [ MkArg MW AutoImplicit Nothing `(DecEq ~(t.fullInvocation))

 753 |         , MkArg MW ExplicitArg (Just "x1") tInv

 754 |         , MkArg MW ExplicitArg (Just "x2") tInv

 755 |         ]

 757 |   ||| Decidable equality clause

 758 |   mkDecEqImplClause : Clause

 759 |   mkDecEqImplClause =

 760 |     let mToPImpl = var $ inGenNS t "mToPImpl"

 761 |     in `(decEqImpl x1 x2)

 762 |         .= `(decEqInj {f = ~mToPImpl} $ decEq (~mToPImpl x1) (~mToPImpl x2))

 765 |   ||| Derive decidable equality

 766 |   mkDecEqDecls :

 767 |     UniResults ->

 768 |     (mt : TypeInfo) ->

 769 |     (0 _ : AllTyArgsNamed mt) =>

 770 |     List Decl

 771 |   mkDecEqDecls _ ti = do

 772 |     [ public' "decEqImpl" $ mkDecEqImplSig ti

 773 |     , def "decEqImpl" [ mkDecEqImplClause ]

 774 |     , interfaceHint Public "decEq'" $ forallMTArgs

 775 |       `(DecEq ~(t.fullInvocation) => DecEq ~(ti.apply var empty))

 776 |     , def "decEq'"

 777 |       [ `(decEq') .= `((Mk DecEq) ~(var $ inGenNS t "decEqImpl")) ]

 778 |     ]

 780 |   -----------------------

 781 |   --- SHOW DERIVATION ---

 782 |   -----------------------

 784 |   ||| Derive Show implementation via cast

 785 |   mkShowDecls :

 786 |     UniResults ->

 787 |     (mt : TypeInfo) ->

 788 |     (0 _ : AllTyArgsNamed mt) =>

 789 |     List Decl

 790 |   mkShowDecls _ ti = do

 791 |     let mToPImpl = var $ inGenNS t "mToPImpl"

 792 |     [ public' "showImpl" $

 793 |       forallMTArgs

 794 |         `(Show ~(t.fullInvocation) => ~(ti.apply var empty) -> String)

 795 |     , def "showImpl" [ `(showImpl x) .= `(show $ ~mToPImpl x) ]

 796 |     , public' "showPrecImpl" $

 797 |       forallMTArgs

 798 |         `(Show ~(t.fullInvocation) => Prec -> ~(ti.apply var empty) -> String)

 799 |     , def "showPrecImpl"

 800 |       [ `(showPrecImpl p x) .= `(showPrec p $ ~mToPImpl x) ]

 801 |     , interfaceHint Public "show'" $ forallMTArgs $

 802 |       `(Show ~(t.fullInvocation) => Show ~(ti.apply var empty))

 803 |     , def "show'" [ `(show') .= `(MkShow showImpl showPrecImpl) ]

 804 |     ]

 806 |   ---------------------

 807 |   --- EQ DERIVATION ---

 808 |   ---------------------

 810 |   ||| Derive Eq implementation via cast

 811 |   mkEqDecls :

 812 |     UniResults ->

 813 |     (mt : TypeInfo) ->

 814 |     (0 _ : AllTyArgsNamed mt) =>

 815 |     List Decl

 816 |   mkEqDecls _ ti = do

 817 |     let mToPImpl = var $ inGenNS t "mToPImpl"

 818 |     let tInv = ti.apply var empty

 819 |     [ public' "eqImpl" $

 820 |       forallMTArgs

 821 |         `(Eq ~(t.fullInvocation) => ~tInv -> ~tInv -> Bool)

 822 |     , def "eqImpl" [ `(eqImpl x y) .= `((~mToPImpl x) == (~mToPImpl y)) ]

 823 |     , public' "neqImpl" $

 824 |       forallMTArgs

 825 |         `(Eq ~(t.fullInvocation) => ~tInv -> ~tInv -> Bool)

 826 |     , def "neqImpl" [ `(neqImpl x y) .= `((~mToPImpl x) /= (~mToPImpl y)) ]

 827 |     , interfaceHint Public "eq'" $ forallMTArgs $

 828 |       `(Eq ~(t.fullInvocation) => Eq ~tInv)

 829 |     , def "eq'" [ `(eq') .= `(MkEq eqImpl neqImpl) ]

 830 |     ]

 832 |   ------------------------------------

 833 |   --- POLY TO POLY CAST DERIVATION ---

 834 |   ------------------------------------

 836 |   ||| Generate specialised to polymorphic type conversion function signature

 837 |   mkPToMImplSig :

 838 |     UniResults ->

 839 |     (mt : TypeInfo) ->

 840 |     (0 _ : AllTyArgsNamed mt) =>

 841 |     TTImp

 842 |   mkPToMImplSig _ mt =

 843 |     forallMTArgs $ arg t.fullInvocation .-> mt.apply var empty

 845 |   ||| Generate specialised to polymorphic type conversion function clause

 847 |   mkPToMImplClause :

 848 |     UnificationResult ->

 849 |     (mt : TypeInfo) ->

 850 |     (0 _ : AllTyArgsNamed mt) =>

 851 |     (pCon : Con) ->

 852 |     (0 _ : ConArgsNamed pCon) =>

 853 |     (mCon : Con) ->

 854 |     (0 _ : ConArgsNamed mCon) =>

 855 |     Nat ->

 856 |     Clause

 857 |   mkPToMImplClause ur _ con mcon _ =

 858 |     var "pToMImpl" .$ con.apply bindVar

 859 |       (substituteVariables

 860 |         (fromList $ argsToBindMap $ con.args) <$> ur.fullResult)

 861 |       .= mcon.apply var ur.fullResult

 863 |   ||| Generate specialised to polymorphic type conversion function declarations

 864 |   mkPToMImplDecls :

 865 |     UniResults ->

 866 |     (mt : TypeInfo) ->

 867 |     (0 _ : AllTyArgsNamed mt) =>

 868 |     List Decl

 869 |   mkPToMImplDecls urs mt = do

 870 |     let sig = mkPToMImplSig urs mt

 871 |     let clauses = map2UConsN mkPToMImplClause urs mt

 872 |     [ public' "pToMImpl" sig

 873 |     , def "pToMImpl" clauses

 874 |     ]

 876 |   ||| Generate specialised to polymorphic cast signature

 877 |   mkPToMSig : (mt : TypeInfo) -> (0 _ : AllTyArgsNamed mt) => TTImp

 878 |   mkPToMSig mt = do

 879 |     forallMTArgs $ `(Cast ~(t.fullInvocation) ~(mt.apply var empty))

 881 |   ||| Generate specialised to polymorphic cast declarations

 882 |   mkPToMDecls : (mt : TypeInfo) -> (0 _ : AllTyArgsNamed mt) => List Decl

 883 |   mkPToMDecls mt =

 884 |     [ interfaceHint Public "pToM" $ mkPToMSig mt

 885 |     , def "pToM" [ (var "pToM") .= `(MkCast pToMImpl)]

 886 |     ]

 888 |   -----------------------------

 889 |   --- FROMSTRING DERIVATION ---

 890 |   -----------------------------

 892 |   mkFromStringDecls :

 893 |     (mt : TypeInfo) ->

 894 |     (0 _ : AllTyArgsNamed mt) =>

 895 |     List Decl

 896 |   mkFromStringDecls ti = do

 897 |     let pToMImpl = var $ inGenNS t "pToMImpl"

 898 |     let tInv = ti.apply var empty

 899 |     [ public' "fromStringImpl" $

 900 |         forallMTArgs

 901 |           `(FromString ~(t.fullInvocation) => String -> ~tInv)

 902 |     , def "fromStringImpl"

 903 |       [ `(fromStringImpl @{fs} s) .= `(~pToMImpl $ fromString @{fs} s) ]

 904 |     , interfaceHint Public "fromString'" $

 905 |         forallMTArgs `(FromString ~(t.fullInvocation) => FromString ~tInv)

 906 |     , def "fromString'"

 907 |         [ `(fromString' @{fs}) .= `(MkFromString $ ~(var $ inGenNS t "fromStringImpl") @{fs}) ]

 908 |     ]

 910 |   ----------------------

 911 |   --- NUM DERIVATION ---

 912 |   ----------------------

 914 |   mkNumDecls :

 915 |     (mt : TypeInfo) ->

 916 |     (0 _ : AllTyArgsNamed mt) =>

 917 |     List Decl

 918 |   mkNumDecls ti = do

 919 |     let pToMImpl = var $ inGenNS t "pToMImpl"

 920 |     let mToPImpl = var $ inGenNS t "mToPImpl"

 921 |     let tInv = ti.apply var empty

 922 |     [ public' "numImpl" $

 923 |         forallMTArgs

 924 |           `(Num ~(t.fullInvocation) => Integer -> ~tInv)

 925 |     , def "numImpl"

 926 |       [ `(numImpl @{fs} s) .= `(~pToMImpl $ Num.fromInteger @{fs} s) ]

 927 |     , public' "plusImpl" $

 928 |         forallMTArgs

 929 |           `(Num ~(t.fullInvocation) => ~tInv -> ~tInv -> ~tInv)

 930 |     , def "plusImpl"

 931 |         [ `(plusImpl @{fs} a b ) .= `(~pToMImpl $ (+) @{fs} (~mToPImpl a) (~mToPImpl b)) ]

 932 |     , public' "starImpl" $

 933 |         forallMTArgs

 934 |           `(Num ~(t.fullInvocation) => ~tInv -> ~tInv -> ~tInv)

 935 |     , def "starImpl"

 936 |         [ `(starImpl @{fs} a b ) .= `(~pToMImpl $ (*) @{fs} (~mToPImpl a) (~mToPImpl b)) ]

 937 |     , interfaceHint Public "num'" $

 938 |         forallMTArgs `(Num ~(t.fullInvocation) => Num ~tInv)

 939 |     , def "num'"

 940 |         [ `(num' @{fs}) .=

 941 |             `(MkNum

 942 |               (~(var $ inGenNS t "plusImpl") @{fs})

 943 |               (~(var $ inGenNS t "starImpl") @{fs})

 944 |               (~(var $ inGenNS t "numImpl") @{fs}))

 945 |         ]

 946 |     ]

 948 |   ------------------------------------

 949 |   --- SPECIALISED TYPE DECLARATION ---

 950 |   ------------------------------------

 952 |   ||| Generate declarations for given task, unification results, and specialised type

 953 |   specDecls : MonadLog m => UniResults -> (mt : TypeInfo) -> (0 _ : AllTyArgsNamed mt) => m $ List Decl

 954 |   specDecls uniResults specTy = do

 955 |     let specTyDecl = specTy.decl

 956 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 957 |       "specTyDecl : \{show specTyDecl}"

 958 |     let mToPImplDecls = mkMToPImplDecls uniResults specTy

 959 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 960 |       "mToPImplDecls : \{show mToPImplDecls}"

 961 |     let mToPDecls = mkMToPDecls specTy

 962 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 963 |       "mToP : \{show mToPDecls}"

 964 |     let multiInjDecls = mkMultiInjDecls uniResults specTy

 965 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 966 |       "multiInj : \{show multiInjDecls}"

 967 |     let multiCongDecls = mkMultiCongDecls uniResults specTy

 968 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 969 |       "multiCong : \{show multiCongDecls}"

 970 |     let castInjDecls = mkCastInjDecls uniResults specTy

 971 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 972 |       "castInj : \{show castInjDecls}"

 973 |     let decEqDecls = mkDecEqDecls uniResults specTy

 974 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 975 |       "decEq : \{show decEqDecls}"

 976 |     let showDecls = mkShowDecls uniResults specTy

 977 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 978 |       "Show : \{show showDecls}"

 979 |     let eqDecls = mkEqDecls uniResults specTy

 980 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 981 |       "Eq : \{show eqDecls}"

 982 |     let pToMImplDecls = mkPToMImplDecls uniResults specTy

 983 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 984 |       "pToMImplDecls : \{show pToMImplDecls}"

 985 |     let pToMDecls = mkPToMDecls specTy

 986 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 987 |       "pToM : \{show pToMDecls}"

 988 |     let fromStringDecls = mkFromStringDecls specTy

 989 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 990 |       "fromString : \{show fromStringDecls}"

 991 |     let numDecls = mkNumDecls specTy

 992 |     logPoint DetailedDebug "specialiseData.specDecls" [specTy]

 993 |       "num : \{show numDecls}"

 994 |     let onFull : List Decl =

 995 |       if any isUndecided uniResults

 996 |           then []

 997 |           else join

 998 |             [ pToMImplDecls

 999 |             , pToMDecls

1000 |             , fromStringDecls

1001 |             , numDecls

1002 |             ]

1003 |     pure $ singleton $ INamespace EmptyFC (MkNS [ show t.resultName ]) $

1004 |       specTyDecl :: join

1005 |         [ mToPImplDecls

1006 |         , mToPDecls

1007 |         , multiInjDecls

1008 |         , multiCongDecls

1009 |         , castInjDecls

1010 |         , decEqDecls

1011 |         , showDecls

1012 |         , eqDecls

1013 |         ] ++ onFull

1023 | interface TaskLambda (t : Type) where

1026 | TaskLambda Type

1029 | TaskLambda b => TaskLambda (a -> b)

1032 | TaskLambda b => TaskLambda (a => b)

1035 | TaskLambda b => TaskLambda ({_ : a} -> b)

1038 | TaskLambda b => TaskLambda ((0 _ : a) -> b)

1041 | TaskLambda b => TaskLambda ((0 _ : a) => b)

1044 | TaskLambda b => TaskLambda ({0 _ : a} -> b)

1062 | specialiseDataRaw :

1063 |   Monad m =>

1064 |   (nsProvider : NamespaceProvider m) =>

1065 |   (unifier : CanUnify m) =>

1066 |   MonadLog m =>

1067 |   MonadError SpecialisationError m =>

1068 |   (namesInfo : NamesInfoInTypes) =>

1069 |   (resultName : Name) ->

1070 |   (resultKind : TTImp) ->

1071 |   (resultContent : TTImp) ->

1072 |   m (TypeInfo, List Decl)

1073 | specialiseDataRaw resultName resultKind resultContent = do

1074 |   let resultKind = mapTTImp cleanupHoleAutoImplicitsImpl $ cleanupNamedHoles resultKind

1075 |   let resultContent = mapTTImp cleanupHoleAutoImplicitsImpl $ cleanupNamedHoles resultContent

1076 |   task <- getTask resultName resultKind resultContent

1077 |   logPoint DetailedDebug "specialiseData" [task.polyTy] "Specialisation task: \{show task}"

1078 |   uniResults <- sequence $ mapCons task $ unifyCon task

1079 |   let Element specTy specTyNamed = mkSpecTy task uniResults

1080 |   decls <- specDecls task uniResults specTy

1081 |   pure (specTy, decls)

1095 | specialiseData :

1096 |   TaskLambda taskT =>

1097 |   Monad m =>

1098 |   Elaboration m =>

1099 |   (nsProvider : NamespaceProvider m) =>

1100 |   (unifier : CanUnify m) =>

1101 |   MonadError SpecialisationError m =>

1102 |   (namesInfo : NamesInfoInTypes) =>

1103 |   (resultName : Name) ->

1104 |   (0 task : taskT) ->

1105 |   m (TypeInfo, List Decl)

1106 | specialiseData resultName task = do

1107 |   -- Quote spec lambda type

1108 |   resultKind <- quote taskT

1109 |   -- Quote spec lambda

1110 |   resultContent <- quote task

1111 |   specialiseDataRaw resultName resultKind resultContent

1127 | specialiseData'' :

1128 |   Elaboration m =>

1129 |   (nsProvider : NamespaceProvider m) =>

1130 |   (unifier : CanUnify m) =>

1131 |   TaskLambda taskT =>

1132 |   Name ->

1133 |   (0 task: taskT) ->

1134 |   m $ List Decl

1135 | specialiseData'' resultName task = do

1136 |   tq <- quote task

1137 |   nit <- getNamesInfoInTypes' tq

1138 |   Right (specTy, decls) <-

1139 |     runEitherT {m} {e=SpecialisationError} $

1140 |       specialiseData resultName task

1141 |   | Left err => fail "Specialisation error: \{show err}"

1142 |   pure decls

1157 | specialiseData' :

1158 |   Elaboration m =>

1159 |   (nsProvider : NamespaceProvider m) =>

1160 |   (unifier : CanUnify m) =>

1161 |   TaskLambda taskT =>

1162 |   Name ->

1163 |   (0 task: taskT) ->

1164 |   m ()

1165 | specialiseData' resultName task =

1166 |   specialiseData'' resultName task >>= declare